Theory List_Proper_Interval

```(*  Title:      Containers/List_Proper_Interval.thy
Author:     Andreas Lochbihler, ETH Zurich *)

theory List_Proper_Interval imports
"HOL-Library.List_Lexorder"
Collection_Order
begin

section ‹Instantiate @{class proper_interval} of for @{typ "'a list"}›

lemma Nil_less_conv_neq_Nil: "[] < xs ⟷ xs ≠ []"
by(cases xs) simp_all

lemma less_append_same_iff:
fixes xs :: "'a :: preorder list"
shows "xs < xs @ ys ⟷ [] < ys"
by(induct xs) simp_all

lemma less_append_same2_iff:
fixes xs :: "'a :: preorder list"
shows "xs @ ys < xs @ zs ⟷ ys < zs"
by(induct xs) simp_all

lemma Cons_less_iff:
fixes x :: "'a :: preorder" shows
"x # xs < ys ⟷ (∃y ys'. ys = y # ys' ∧ (x < y ∨ x = y ∧ xs < ys'))"
by(cases ys) auto

instantiation list :: ("{proper_interval, order}") proper_interval begin

definition proper_interval_list_aux :: "'a list ⇒ 'a list ⇒ bool"
where proper_interval_list_aux_correct:
"proper_interval_list_aux xs ys ⟷ (∃zs. xs < zs ∧ zs < ys)"

lemma proper_interval_list_aux_simps [code]:
"proper_interval_list_aux xs [] ⟷ False"
"proper_interval_list_aux [] (y # ys) ⟷ ys ≠ [] ∨ proper_interval None (Some y)"
"proper_interval_list_aux (x # xs) (y # ys) ⟷ x < y ∨ x = y ∧ proper_interval_list_aux xs ys"
apply(rule iffI)
apply(fastforce simp add: Cons_less_iff intro: less_trans)
apply(erule disjE)
apply(rule exI[where x="x # xs @ [undefined]"])
apply(auto 4 3 simp add: Cons_less_iff)
done

fun proper_interval_list :: "'a list option ⇒ 'a list option ⇒ bool" where
"proper_interval_list None None ⟷ True"
| "proper_interval_list None (Some xs) ⟷ (xs ≠ [])"
| "proper_interval_list (Some xs) None ⟷ True"
| "proper_interval_list (Some xs) (Some ys) ⟷ proper_interval_list_aux xs ys"
instance
proof(intro_classes)
fix xs ys :: "'a list"
show "proper_interval None (Some ys) ⟷ (∃zs. zs < ys)"
by(auto simp add: Nil_less_conv_neq_Nil intro: exI[where x="[]"])
show "proper_interval (Some xs) None ⟷ (∃zs. xs < zs)"
by(simp add: exI[where x="xs @ [undefined]"] less_append_same_iff)
show "proper_interval (Some xs) (Some ys) ⟷ (∃zs. xs < zs ∧ zs < ys)"