24 instance list :: (order) order |
24 instance list :: (order) order |
25 proof |
25 proof |
26 let ?r = "{(u, v::'a). u < v}" |
26 let ?r = "{(u, v::'a). u < v}" |
27 have tr: "trans ?r" |
27 have tr: "trans ?r" |
28 using trans_def by fastforce |
28 using trans_def by fastforce |
|
29 have *: "antisym {(u, v::'a). u < v}" |
|
30 using antisym_def by fastforce |
29 have \<section>: False |
31 have \<section>: False |
30 if "(xs,ys) \<in> lexord ?r" "(ys,xs) \<in> lexord ?r" for xs ys :: "'a list" |
32 if "(xs,ys) \<in> lexord ?r" "(ys,xs) \<in> lexord ?r" for xs ys :: "'a list" |
31 proof - |
33 proof - |
32 have "(xs,xs) \<in> lexord ?r" |
34 have "(xs,xs) \<in> lexord ?r" |
33 using that transD [OF lexord_transI [OF tr]] by blast |
35 using lexord_trans that tr * by blast |
34 then show False |
36 then show False |
35 by (meson case_prodD lexord_irreflexive less_irrefl mem_Collect_eq) |
37 by (meson case_prodD lexord_irreflexive less_irrefl mem_Collect_eq) |
36 qed |
38 qed |
37 show "xs \<le> xs" for xs :: "'a list" by (simp add: list_le_def) |
39 show "xs \<le> xs" for xs :: "'a list" by (simp add: list_le_def) |
38 show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs" for xs ys zs :: "'a list" |
40 show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs" for xs ys zs :: "'a list" |
39 using that transD [OF lexord_transI [OF tr]] by (auto simp add: list_le_def list_less_def) |
41 using that transD [OF lexord_transI [OF tr]] * |
|
42 by (auto simp add: list_le_def list_less_def) |
40 show "xs = ys" if "xs \<le> ys" "ys \<le> xs" for xs ys :: "'a list" |
43 show "xs = ys" if "xs \<le> ys" "ys \<le> xs" for xs ys :: "'a list" |
41 using \<section> that list_le_def list_less_def by blast |
44 using \<section> that list_le_def list_less_def by blast |
42 show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" for xs ys :: "'a list" |
45 show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" for xs ys :: "'a list" |
43 by (auto simp add: list_less_def list_le_def dest: \<section>) |
46 by (auto simp add: list_less_def list_le_def dest: \<section>) |
44 qed |
47 qed |
68 by (simp add: list_less_def) |
71 by (simp add: list_less_def) |
69 |
72 |
70 lemma Nil_less_Cons [simp]: "[] < a # x" |
73 lemma Nil_less_Cons [simp]: "[] < a # x" |
71 by (simp add: list_less_def) |
74 by (simp add: list_less_def) |
72 |
75 |
73 lemma Cons_less_Cons [simp]: "a # x < b # y \<longleftrightarrow> a < b \<or> a = b \<and> x < y" |
76 lemma Cons_less_Cons [simp]: "a # x < b # y \<longleftrightarrow> (if a = b then x < y else a < b)" |
74 by (simp add: list_less_def) |
77 by (simp add: list_less_def) |
75 |
78 |
76 lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []" |
79 lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []" |
77 unfolding list_le_def by (cases x) auto |
80 unfolding list_le_def by (cases x) auto |
78 |
81 |