(* Title: HOL/Library/List_lexord.thy Author: Norbert Voelker *) header {* Lexicographic order on lists *} theory List_lexord imports List Main begin instantiation list :: (ord) ord begin definition list_less_def: "xs < ys \ (xs, ys) \ lexord {(u, v). u < v}" definition list_le_def: "(xs :: _ list) \ ys \ xs < ys \ xs = ys" instance .. end instance list :: (order) order proof fix xs :: "'a list" show "xs \ xs" by (simp add: list_le_def) next fix xs ys zs :: "'a list" assume "xs \ ys" and "ys \ zs" then show "xs \ zs" by (auto simp add: list_le_def list_less_def) (rule lexord_trans, auto intro: transI) next fix xs ys :: "'a list" assume "xs \ ys" and "ys \ xs" then show "xs = ys" apply (auto simp add: list_le_def list_less_def) apply (rule lexord_irreflexive [THEN notE]) defer apply (rule lexord_trans) apply (auto intro: transI) done next fix xs ys :: "'a list" show "xs < ys \ xs \ ys \ \ ys \ xs" apply (auto simp add: list_less_def list_le_def) defer apply (rule lexord_irreflexive [THEN notE]) apply auto apply (rule lexord_irreflexive [THEN notE]) defer apply (rule lexord_trans) apply (auto intro: transI) done qed instance list :: (linorder) linorder proof fix xs ys :: "'a list" have "(xs, ys) \ lexord {(u, v). u < v} \ xs = ys \ (ys, xs) \ lexord {(u, v). u < v}" by (rule lexord_linear) auto then show "xs \ ys \ ys \ xs" by (auto simp add: list_le_def list_less_def) qed instantiation list :: (linorder) distrib_lattice begin definition "(inf \ 'a list \ _) = min" definition "(sup \ 'a list \ _) = max" instance by intro_classes (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1) end lemma not_less_Nil [simp]: "\ (x < [])" by (unfold list_less_def) simp lemma Nil_less_Cons [simp]: "[] < a # x" by (unfold list_less_def) simp lemma Cons_less_Cons [simp]: "a # x < b # y \ a < b \ a = b \ x < y" by (unfold list_less_def) simp lemma le_Nil [simp]: "x \ [] \ x = []" by (unfold list_le_def, cases x) auto lemma Nil_le_Cons [simp]: "[] \ x" by (unfold list_le_def, cases x) auto lemma Cons_le_Cons [simp]: "a # x \ b # y \ a < b \ a = b \ x \ y" by (unfold list_le_def) auto instantiation list :: (order) bot begin definition "bot = []" instance proof qed (simp add: bot_list_def) end lemma less_list_code [code]: "xs < ([]\'a\{equal, order} list) \ False" "[] < (x\'a\{equal, order}) # xs \ True" "(x\'a\{equal, order}) # xs < y # ys \ x < y \ x = y \ xs < ys" by simp_all lemma less_eq_list_code [code]: "x # xs \ ([]\'a\{equal, order} list) \ False" "[] \ (xs\'a\{equal, order} list) \ True" "(x\'a\{equal, order}) # xs \ y # ys \ x < y \ x = y \ xs \ ys" by simp_all end