author | Manuel Eberl <eberlm@in.tum.de> |
Fri, 29 Mar 2024 19:28:59 +0100 | |
changeset 80061 | 4c1347e172b1 |
parent 72184 | 881bd98bddee |
permissions | -rw-r--r-- |
68312 | 1 |
(* Title: HOL/Library/List_Lexorder.thy |
15737 | 2 |
Author: Norbert Voelker |
3 |
*) |
|
4 |
||
60500 | 5 |
section \<open>Lexicographic order on lists\<close> |
15737 | 6 |
|
68312 | 7 |
theory List_Lexorder |
53214 | 8 |
imports Main |
15737 | 9 |
begin |
10 |
||
25764 | 11 |
instantiation list :: (ord) ord |
12 |
begin |
|
13 |
||
14 |
definition |
|
37474 | 15 |
list_less_def: "xs < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u, v). u < v}" |
25764 | 16 |
|
17 |
definition |
|
37474 | 18 |
list_le_def: "(xs :: _ list) \<le> ys \<longleftrightarrow> xs < ys \<or> xs = ys" |
25764 | 19 |
|
20 |
instance .. |
|
21 |
||
22 |
end |
|
15737 | 23 |
|
17200 | 24 |
instance list :: (order) order |
27682 | 25 |
proof |
71766
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset
|
26 |
let ?r = "{(u, v::'a). u < v}" |
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset
|
27 |
have tr: "trans ?r" |
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset
|
28 |
using trans_def by fastforce |
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset
|
29 |
have \<section>: False |
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset
|
30 |
if "(xs,ys) \<in> lexord ?r" "(ys,xs) \<in> lexord ?r" for xs ys :: "'a list" |
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset
|
31 |
proof - |
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset
|
32 |
have "(xs,xs) \<in> lexord ?r" |
72184 | 33 |
using that transD [OF lexord_transI [OF tr]] by blast |
71766
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset
|
34 |
then show False |
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset
|
35 |
by (meson case_prodD lexord_irreflexive less_irrefl mem_Collect_eq) |
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset
|
36 |
qed |
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset
|
37 |
show "xs \<le> xs" for xs :: "'a list" by (simp add: list_le_def) |
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset
|
38 |
show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs" for xs ys zs :: "'a list" |
72184 | 39 |
using that transD [OF lexord_transI [OF tr]] by (auto simp add: list_le_def list_less_def) |
71766
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset
|
40 |
show "xs = ys" if "xs \<le> ys" "ys \<le> xs" for xs ys :: "'a list" |
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset
|
41 |
using \<section> that list_le_def list_less_def by blast |
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset
|
42 |
show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" for xs ys :: "'a list" |
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset
|
43 |
by (auto simp add: list_less_def list_le_def dest: \<section>) |
27682 | 44 |
qed |
15737 | 45 |
|
21458 | 46 |
instance list :: (linorder) linorder |
27682 | 47 |
proof |
48 |
fix xs ys :: "'a list" |
|
71766
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset
|
49 |
have "total (lexord {(u, v::'a). u < v})" |
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset
|
50 |
by (rule total_lexord) (auto simp: total_on_def) |
53214 | 51 |
then show "xs \<le> ys \<or> ys \<le> xs" |
71766
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset
|
52 |
by (auto simp add: total_on_def list_le_def list_less_def) |
27682 | 53 |
qed |
15737 | 54 |
|
25764 | 55 |
instantiation list :: (linorder) distrib_lattice |
56 |
begin |
|
57 |
||
61076 | 58 |
definition "(inf :: 'a list \<Rightarrow> _) = min" |
25764 | 59 |
|
61076 | 60 |
definition "(sup :: 'a list \<Rightarrow> _) = max" |
25764 | 61 |
|
62 |
instance |
|
60679 | 63 |
by standard (auto simp add: inf_list_def sup_list_def max_min_distrib2) |
22483 | 64 |
|
25764 | 65 |
end |
66 |
||
53214 | 67 |
lemma not_less_Nil [simp]: "\<not> x < []" |
68 |
by (simp add: list_less_def) |
|
15737 | 69 |
|
22177 | 70 |
lemma Nil_less_Cons [simp]: "[] < a # x" |
53214 | 71 |
by (simp add: list_less_def) |
15737 | 72 |
|
72184 | 73 |
lemma Cons_less_Cons [simp]: "a # x < b # y \<longleftrightarrow> a < b \<or> a = b \<and> x < y" |
53214 | 74 |
by (simp add: list_less_def) |
15737 | 75 |
|
22177 | 76 |
lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []" |
53214 | 77 |
unfolding list_le_def by (cases x) auto |
22177 | 78 |
|
79 |
lemma Nil_le_Cons [simp]: "[] \<le> x" |
|
53214 | 80 |
unfolding list_le_def by (cases x) auto |
15737 | 81 |
|
72184 | 82 |
lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y" |
53214 | 83 |
unfolding list_le_def by auto |
15737 | 84 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
38857
diff
changeset
|
85 |
instantiation list :: (order) order_bot |
37474 | 86 |
begin |
87 |
||
53214 | 88 |
definition "bot = []" |
37474 | 89 |
|
53214 | 90 |
instance |
60679 | 91 |
by standard (simp add: bot_list_def) |
37474 | 92 |
|
93 |
end |
|
94 |
||
95 |
lemma less_list_code [code]: |
|
61076 | 96 |
"xs < ([]::'a::{equal, order} list) \<longleftrightarrow> False" |
97 |
"[] < (x::'a::{equal, order}) # xs \<longleftrightarrow> True" |
|
98 |
"(x::'a::{equal, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys" |
|
22177 | 99 |
by simp_all |
100 |
||
37474 | 101 |
lemma less_eq_list_code [code]: |
61076 | 102 |
"x # xs \<le> ([]::'a::{equal, order} list) \<longleftrightarrow> False" |
103 |
"[] \<le> (xs::'a::{equal, order} list) \<longleftrightarrow> True" |
|
104 |
"(x::'a::{equal, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys" |
|
22177 | 105 |
by simp_all |
106 |
||
17200 | 107 |
end |