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(simp_all add: proper_interval_list_aux_correct proper_interval_simps Nil_less_conv_neq_Nil)
 apply(fastforce simp add: neq_Nil_conv)
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(simp add: less_append_same_iff)
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)"
    by(simp add: proper_interval_list_aux_correct)
qed simp
end

end