-
Notifications
You must be signed in to change notification settings - Fork 0
/
LexordList.thy
185 lines (147 loc) · 6.1 KB
/
LexordList.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*)
theory LexordList imports
Main
Eisbach_Methods (* for tests *)
begin
text \<open>
Wrapper for lexicographic string comparisons.
We need this to define search trees with string keys, etc.
This is mostly copied from HOL/Library/List_lexord, but we add
the wrapper type lexord_list to avoid clashing with the existing
prefix ordering on lists (HOL/Library/Prefix_Order).
\<close>
datatype 'a lexord_list = lexord_list "'a list"
primrec dest_lexord_list where
"dest_lexord_list (lexord_list xs) = xs"
instantiation lexord_list :: (ord) ord
begin
definition
lexord_list_less_def: "xs < ys \<longleftrightarrow> (dest_lexord_list xs, dest_lexord_list ys) \<in> lexord {(u, v). u < v}"
definition
lexord_list_le_def: "(xs :: _ lexord_list) \<le> ys \<longleftrightarrow> xs < ys \<or> xs = ys"
instance ..
end
instance lexord_list :: (order) order
proof
fix xs :: "'a lexord_list"
show "xs \<le> xs" by (simp add: lexord_list_le_def)
next
fix xs ys zs :: "'a lexord_list"
assume "xs \<le> ys" and "ys \<le> zs"
then show "xs \<le> zs"
apply (auto simp add: lexord_list_le_def lexord_list_less_def)
apply (rule lexord_trans)
apply (auto intro: transI)
done
next
fix xs ys :: "'a lexord_list"
assume "xs \<le> ys" and "ys \<le> xs"
then show "xs = ys"
apply (auto simp add: lexord_list_le_def lexord_list_less_def)
apply (rule lexord_irreflexive [THEN notE])
defer
apply (rule lexord_trans)
apply (auto intro: transI)
done
next
fix xs ys :: "'a lexord_list"
show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
apply (auto simp add: lexord_list_less_def lexord_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 lexord_list :: (linorder) linorder
proof
fix xs ys :: "'a lexord_list"
have "(dest_lexord_list xs, dest_lexord_list ys) \<in> lexord {(u, v). u < v} \<or>
dest_lexord_list xs = dest_lexord_list ys \<or>
(dest_lexord_list ys, dest_lexord_list xs) \<in> lexord {(u, v). u < v}"
by (rule lexord_linear) auto
then show "xs \<le> ys \<or> ys \<le> xs"
apply (case_tac xs)
apply (case_tac ys)
apply (auto simp add: lexord_list_le_def lexord_list_less_def)
done
qed
instantiation lexord_list :: (linorder) distrib_lattice
begin
definition inf_lexord_list_def: "(inf :: 'a lexord_list \<Rightarrow> _) = min"
definition sup_lexord_list_def: "(sup :: 'a lexord_list \<Rightarrow> _) = max"
instance
by standard (auto simp add: inf_lexord_list_def sup_lexord_list_def max_min_distrib2)
end
lemma lexord_not_less_Nil [simp]: "\<not> x < lexord_list []"
by (simp add: lexord_list_less_def)
lemma lexord_Nil_less_Cons [simp]: "lexord_list [] < lexord_list (a # x)"
by (simp add: lexord_list_less_def)
lemma lexord_Cons_less_Cons [simp]: "lexord_list (a # x) < lexord_list (b # y) \<longleftrightarrow> a < b \<or> a = b \<and> lexord_list x < lexord_list y"
by (simp add: lexord_list_less_def)
lemma lexord_le_Nil [simp]: "x \<le> lexord_list [] \<longleftrightarrow> x = lexord_list []"
unfolding lexord_list_le_def by (cases x) auto
lemma lexord_Nil_le_Cons [simp]: "lexord_list [] \<le> x"
unfolding lexord_list_le_def
apply (cases x, rename_tac x', case_tac x')
by auto
lemma lexord_Cons_le_Cons [simp]: "lexord_list (a # x) \<le> lexord_list (b # y) \<longleftrightarrow> a < b \<or> a = b \<and> lexord_list x \<le> lexord_list y"
unfolding lexord_list_le_def by auto
instantiation lexord_list :: (order) order_bot
begin
definition bot_lexord_list_def: "bot = lexord_list []"
instance
by standard (simp add: bot_lexord_list_def)
end
lemma lexord_less_list_code [code]:
"xs < lexord_list ([]::'a::{equal, order} list) \<longleftrightarrow> False"
"lexord_list [] < lexord_list ((x::'a::{equal, order}) # xs') \<longleftrightarrow> True"
"lexord_list ((x::'a::{equal, order}) # xs') < lexord_list (y # ys') \<longleftrightarrow> x < y \<or> x = y \<and> lexord_list xs' < lexord_list ys'"
by simp_all
lemma lexord_less_eq_list_code [code]:
"lexord_list (x # xs') \<le> lexord_list ([]::'a::{equal, order} list) \<longleftrightarrow> False"
"lexord_list [] \<le> (xs::'a::{equal, order} lexord_list) \<longleftrightarrow> True"
"lexord_list ((x::'a::{equal, order}) # xs') \<le> lexord_list (y # ys') \<longleftrightarrow> x < y \<or> x = y \<and> lexord_list xs' \<le> lexord_list ys'"
by simp_all
text \<open>
Some basic tests.
\<close>
experiment begin
value "lexord_list [1, 2, 3, 4] < lexord_list [1, 2, 3, 5 :: int]"
lemma "lexord_list [1, 2, 3, 4] < lexord_list [1, 2, 3, 5 :: int]"
by simp
lemma "\<not> (lexord_list [1, 2, 3, 5] < lexord_list [1, 2, 3, 4, 5 :: int])"
by simp
lemma "lexord_list [1, 2, 3, 4] \<le> lexord_list [1, 2, 3, 5 :: int]"
by simp
end
text \<open>
Minimal simpset for efficient lexord_list evaluation.
\<close>
lemmas lexord_list_simps =
simp_thms
lexord_list.inject list.distinct list.inject \<comment> \<open>eq\<close>
lexord_not_less_Nil lexord_Nil_less_Cons lexord_Cons_less_Cons \<comment> \<open>less\<close>
lexord_le_Nil lexord_Nil_le_Cons lexord_Cons_le_Cons \<comment> \<open>le\<close>
experiment begin
lemma "lexord_list [1, 2, 3] < lexord_list [1, 3 :: nat]"
apply (fails \<open>solves \<open>simp only: lexord_list_simps\<close>\<close>)
apply (fails \<open>solves \<open>simp only: rel_simps\<close>\<close>)
by (simp only: lexord_list_simps rel_simps)
lemma "lexord_list [1, 2, 3] \<le> lexord_list [1, 3 :: nat]"
apply (fails \<open>solves \<open>simp only: lexord_list_simps\<close>\<close>)
apply (fails \<open>solves \<open>simp only: rel_simps\<close>\<close>)
by (simp only: lexord_list_simps rel_simps)
lemma "lexord_list [1, 2, 3] \<le> lexord_list [1, 2, 3 :: nat]"
by (simp only: lexord_list_simps)
lemma "\<not> (lexord_list [1, 2, 3] < lexord_list [1, 2, 3 :: nat])"
by (simp only: lexord_list_simps rel_simps)
end
end