blanchet@33197
|
1 |
(* Title: HOL/Nitpick_Examples/Manual_Nits.thy
|
blanchet@33197
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
blanchet@33197
|
3 |
Copyright 2009
|
blanchet@33197
|
4 |
|
blanchet@33197
|
5 |
Examples from the Nitpick manual.
|
blanchet@33197
|
6 |
*)
|
blanchet@33197
|
7 |
|
blanchet@33197
|
8 |
header {* Examples from the Nitpick Manual *}
|
blanchet@33197
|
9 |
|
blanchet@33197
|
10 |
theory Manual_Nits
|
blanchet@33197
|
11 |
imports Main Coinductive_List RealDef
|
blanchet@33197
|
12 |
begin
|
blanchet@33197
|
13 |
|
blanchet@33197
|
14 |
chapter {* 3. First Steps *}
|
blanchet@33197
|
15 |
|
blanchet@33197
|
16 |
nitpick_params [sat_solver = MiniSatJNI, max_threads = 1]
|
blanchet@33197
|
17 |
|
blanchet@33197
|
18 |
subsection {* 3.1. Propositional Logic *}
|
blanchet@33197
|
19 |
|
blanchet@33197
|
20 |
lemma "P \<longleftrightarrow> Q"
|
blanchet@33197
|
21 |
nitpick
|
blanchet@33197
|
22 |
apply auto
|
blanchet@33197
|
23 |
nitpick 1
|
blanchet@33197
|
24 |
nitpick 2
|
blanchet@33197
|
25 |
oops
|
blanchet@33197
|
26 |
|
blanchet@33197
|
27 |
subsection {* 3.2. Type Variables *}
|
blanchet@33197
|
28 |
|
blanchet@33197
|
29 |
lemma "P x \<Longrightarrow> P (THE y. P y)"
|
blanchet@33197
|
30 |
nitpick [verbose]
|
blanchet@33197
|
31 |
oops
|
blanchet@33197
|
32 |
|
blanchet@33197
|
33 |
subsection {* 3.3. Constants *}
|
blanchet@33197
|
34 |
|
blanchet@33197
|
35 |
lemma "P x \<Longrightarrow> P (THE y. P y)"
|
blanchet@33197
|
36 |
nitpick [show_consts]
|
blanchet@33197
|
37 |
nitpick [full_descrs, show_consts]
|
blanchet@33197
|
38 |
nitpick [dont_specialize, full_descrs, show_consts]
|
blanchet@33197
|
39 |
oops
|
blanchet@33197
|
40 |
|
blanchet@33197
|
41 |
lemma "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)"
|
blanchet@33197
|
42 |
nitpick
|
blanchet@33197
|
43 |
nitpick [card 'a = 1-50]
|
blanchet@33197
|
44 |
(* sledgehammer *)
|
blanchet@33197
|
45 |
apply (metis the_equality)
|
blanchet@33197
|
46 |
done
|
blanchet@33197
|
47 |
|
blanchet@33197
|
48 |
subsection {* 3.4. Skolemization *}
|
blanchet@33197
|
49 |
|
blanchet@33197
|
50 |
lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
|
blanchet@33197
|
51 |
nitpick
|
blanchet@33197
|
52 |
oops
|
blanchet@33197
|
53 |
|
blanchet@33197
|
54 |
lemma "\<exists>x. \<forall>f. f x = x"
|
blanchet@33197
|
55 |
nitpick
|
blanchet@33197
|
56 |
oops
|
blanchet@33197
|
57 |
|
blanchet@33197
|
58 |
lemma "refl r \<Longrightarrow> sym r"
|
blanchet@33197
|
59 |
nitpick
|
blanchet@33197
|
60 |
oops
|
blanchet@33197
|
61 |
|
blanchet@34123
|
62 |
subsection {* 3.5. Natural Numbers and Integers *}
|
blanchet@33197
|
63 |
|
blanchet@33197
|
64 |
lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
|
blanchet@33197
|
65 |
nitpick
|
blanchet@33197
|
66 |
oops
|
blanchet@33197
|
67 |
|
blanchet@33197
|
68 |
lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
|
blanchet@33197
|
69 |
nitpick [card nat = 100, check_potential]
|
blanchet@33197
|
70 |
oops
|
blanchet@33197
|
71 |
|
blanchet@33197
|
72 |
lemma "P Suc"
|
blanchet@33197
|
73 |
nitpick [card = 1-6]
|
blanchet@33197
|
74 |
oops
|
blanchet@33197
|
75 |
|
blanchet@33197
|
76 |
lemma "P (op +\<Colon>nat\<Rightarrow>nat\<Rightarrow>nat)"
|
blanchet@33197
|
77 |
nitpick [card nat = 1]
|
blanchet@33197
|
78 |
nitpick [card nat = 2]
|
blanchet@33197
|
79 |
oops
|
blanchet@33197
|
80 |
|
blanchet@33197
|
81 |
subsection {* 3.6. Inductive Datatypes *}
|
blanchet@33197
|
82 |
|
blanchet@33197
|
83 |
lemma "hd (xs @ [y, y]) = hd xs"
|
blanchet@33197
|
84 |
nitpick
|
blanchet@33197
|
85 |
nitpick [show_consts, show_datatypes]
|
blanchet@33197
|
86 |
oops
|
blanchet@33197
|
87 |
|
blanchet@33197
|
88 |
lemma "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> xs = ys"
|
blanchet@33197
|
89 |
nitpick [show_datatypes]
|
blanchet@33197
|
90 |
oops
|
blanchet@33197
|
91 |
|
blanchet@33197
|
92 |
subsection {* 3.7. Typedefs, Records, Rationals, and Reals *}
|
blanchet@33197
|
93 |
|
blanchet@33197
|
94 |
typedef three = "{0\<Colon>nat, 1, 2}"
|
blanchet@33197
|
95 |
by blast
|
blanchet@33197
|
96 |
|
blanchet@33197
|
97 |
definition A :: three where "A \<equiv> Abs_three 0"
|
blanchet@33197
|
98 |
definition B :: three where "B \<equiv> Abs_three 1"
|
blanchet@33197
|
99 |
definition C :: three where "C \<equiv> Abs_three 2"
|
blanchet@33197
|
100 |
|
blanchet@33197
|
101 |
lemma "\<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P x"
|
blanchet@33197
|
102 |
nitpick [show_datatypes]
|
blanchet@33197
|
103 |
oops
|
blanchet@33197
|
104 |
|
blanchet@33197
|
105 |
record point =
|
blanchet@33197
|
106 |
Xcoord :: int
|
blanchet@33197
|
107 |
Ycoord :: int
|
blanchet@33197
|
108 |
|
blanchet@33197
|
109 |
lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)"
|
blanchet@33197
|
110 |
nitpick [show_datatypes]
|
blanchet@33197
|
111 |
oops
|
blanchet@33197
|
112 |
|
blanchet@33197
|
113 |
lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
|
blanchet@33197
|
114 |
nitpick [show_datatypes]
|
blanchet@33197
|
115 |
oops
|
blanchet@33197
|
116 |
|
blanchet@33197
|
117 |
subsection {* 3.8. Inductive and Coinductive Predicates *}
|
blanchet@33197
|
118 |
|
blanchet@33197
|
119 |
inductive even where
|
blanchet@33197
|
120 |
"even 0" |
|
blanchet@33197
|
121 |
"even n \<Longrightarrow> even (Suc (Suc n))"
|
blanchet@33197
|
122 |
|
blanchet@33197
|
123 |
lemma "\<exists>n. even n \<and> even (Suc n)"
|
blanchet@34123
|
124 |
nitpick [card nat = 100, unary_ints, verbose]
|
blanchet@33197
|
125 |
oops
|
blanchet@33197
|
126 |
|
blanchet@33197
|
127 |
lemma "\<exists>n \<le> 99. even n \<and> even (Suc n)"
|
blanchet@34123
|
128 |
nitpick [card nat = 100, unary_ints, verbose]
|
blanchet@33197
|
129 |
oops
|
blanchet@33197
|
130 |
|
blanchet@33197
|
131 |
inductive even' where
|
blanchet@33197
|
132 |
"even' (0\<Colon>nat)" |
|
blanchet@33197
|
133 |
"even' 2" |
|
blanchet@33197
|
134 |
"\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
|
blanchet@33197
|
135 |
|
blanchet@33197
|
136 |
lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
|
blanchet@34123
|
137 |
nitpick [card nat = 10, unary_ints, verbose, show_consts] (* FIXME: should be genuine *)
|
blanchet@33197
|
138 |
oops
|
blanchet@33197
|
139 |
|
blanchet@33197
|
140 |
lemma "even' (n - 2) \<Longrightarrow> even' n"
|
blanchet@33197
|
141 |
nitpick [card nat = 10, show_consts]
|
blanchet@33197
|
142 |
oops
|
blanchet@33197
|
143 |
|
blanchet@33197
|
144 |
coinductive nats where
|
blanchet@33197
|
145 |
"nats (x\<Colon>nat) \<Longrightarrow> nats x"
|
blanchet@33197
|
146 |
|
blanchet@33197
|
147 |
lemma "nats = {0, 1, 2, 3, 4}"
|
blanchet@33197
|
148 |
nitpick [card nat = 10, show_consts]
|
blanchet@33197
|
149 |
oops
|
blanchet@33197
|
150 |
|
blanchet@33197
|
151 |
inductive odd where
|
blanchet@33197
|
152 |
"odd 1" |
|
blanchet@33197
|
153 |
"\<lbrakk>odd m; even n\<rbrakk> \<Longrightarrow> odd (m + n)"
|
blanchet@33197
|
154 |
|
blanchet@33197
|
155 |
lemma "odd n \<Longrightarrow> odd (n - 2)"
|
blanchet@33197
|
156 |
nitpick [card nat = 10, show_consts]
|
blanchet@33197
|
157 |
oops
|
blanchet@33197
|
158 |
|
blanchet@33197
|
159 |
subsection {* 3.9. Coinductive Datatypes *}
|
blanchet@33197
|
160 |
|
blanchet@33197
|
161 |
lemma "xs \<noteq> LCons a xs"
|
blanchet@33197
|
162 |
nitpick
|
blanchet@33197
|
163 |
oops
|
blanchet@33197
|
164 |
|
blanchet@33197
|
165 |
lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
|
blanchet@33197
|
166 |
nitpick [verbose]
|
blanchet@33197
|
167 |
nitpick [bisim_depth = -1, verbose]
|
blanchet@33197
|
168 |
oops
|
blanchet@33197
|
169 |
|
blanchet@33197
|
170 |
lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
|
blanchet@33197
|
171 |
nitpick [bisim_depth = -1, show_datatypes]
|
blanchet@33197
|
172 |
nitpick
|
blanchet@33197
|
173 |
sorry
|
blanchet@33197
|
174 |
|
blanchet@33197
|
175 |
subsection {* 3.10. Boxing *}
|
blanchet@33197
|
176 |
|
blanchet@33197
|
177 |
datatype tm = Var nat | Lam tm | App tm tm
|
blanchet@33197
|
178 |
|
blanchet@33197
|
179 |
primrec lift where
|
blanchet@33197
|
180 |
"lift (Var j) k = Var (if j < k then j else j + 1)" |
|
blanchet@33197
|
181 |
"lift (Lam t) k = Lam (lift t (k + 1))" |
|
blanchet@33197
|
182 |
"lift (App t u) k = App (lift t k) (lift u k)"
|
blanchet@33197
|
183 |
|
blanchet@33197
|
184 |
primrec loose where
|
blanchet@33197
|
185 |
"loose (Var j) k = (j \<ge> k)" |
|
blanchet@33197
|
186 |
"loose (Lam t) k = loose t (Suc k)" |
|
blanchet@33197
|
187 |
"loose (App t u) k = (loose t k \<or> loose u k)"
|
blanchet@33197
|
188 |
|
blanchet@33197
|
189 |
primrec subst\<^isub>1 where
|
blanchet@33197
|
190 |
"subst\<^isub>1 \<sigma> (Var j) = \<sigma> j" |
|
blanchet@33197
|
191 |
"subst\<^isub>1 \<sigma> (Lam t) =
|
blanchet@33197
|
192 |
Lam (subst\<^isub>1 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 1) t)" |
|
blanchet@33197
|
193 |
"subst\<^isub>1 \<sigma> (App t u) = App (subst\<^isub>1 \<sigma> t) (subst\<^isub>1 \<sigma> u)"
|
blanchet@33197
|
194 |
|
blanchet@33197
|
195 |
lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>1 \<sigma> t = t"
|
blanchet@33197
|
196 |
nitpick [verbose]
|
blanchet@33197
|
197 |
nitpick [eval = "subst\<^isub>1 \<sigma> t"]
|
blanchet@33197
|
198 |
nitpick [dont_box]
|
blanchet@33197
|
199 |
oops
|
blanchet@33197
|
200 |
|
blanchet@33197
|
201 |
primrec subst\<^isub>2 where
|
blanchet@33197
|
202 |
"subst\<^isub>2 \<sigma> (Var j) = \<sigma> j" |
|
blanchet@33197
|
203 |
"subst\<^isub>2 \<sigma> (Lam t) =
|
blanchet@33197
|
204 |
Lam (subst\<^isub>2 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 0) t)" |
|
blanchet@33197
|
205 |
"subst\<^isub>2 \<sigma> (App t u) = App (subst\<^isub>2 \<sigma> t) (subst\<^isub>2 \<sigma> u)"
|
blanchet@33197
|
206 |
|
blanchet@33197
|
207 |
lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
|
blanchet@33197
|
208 |
nitpick
|
blanchet@33197
|
209 |
sorry
|
blanchet@33197
|
210 |
|
blanchet@33197
|
211 |
subsection {* 3.11. Scope Monotonicity *}
|
blanchet@33197
|
212 |
|
blanchet@33197
|
213 |
lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
|
blanchet@33197
|
214 |
nitpick [verbose]
|
blanchet@33197
|
215 |
nitpick [card = 8, verbose]
|
blanchet@33197
|
216 |
oops
|
blanchet@33197
|
217 |
|
blanchet@33197
|
218 |
lemma "\<exists>g. \<forall>x\<Colon>'b. g (f x) = x \<Longrightarrow> \<forall>y\<Colon>'a. \<exists>x. y = f x"
|
blanchet@33197
|
219 |
nitpick [mono]
|
blanchet@33197
|
220 |
nitpick
|
blanchet@33197
|
221 |
oops
|
blanchet@33197
|
222 |
|
blanchet@34969
|
223 |
subsection {* 3.12. Inductive Properties *}
|
blanchet@34969
|
224 |
|
blanchet@34969
|
225 |
inductive_set reach where
|
blanchet@34969
|
226 |
"(4\<Colon>nat) \<in> reach" |
|
blanchet@34969
|
227 |
"n \<in> reach \<Longrightarrow> n < 4 \<Longrightarrow> 3 * n + 1 \<in> reach" |
|
blanchet@34969
|
228 |
"n \<in> reach \<Longrightarrow> n + 2 \<in> reach"
|
blanchet@34969
|
229 |
|
blanchet@34969
|
230 |
lemma "n \<in> reach \<Longrightarrow> 2 dvd n"
|
blanchet@34969
|
231 |
nitpick
|
blanchet@34969
|
232 |
apply (induct set: reach)
|
blanchet@34969
|
233 |
apply auto
|
blanchet@34969
|
234 |
nitpick
|
blanchet@34969
|
235 |
apply (thin_tac "n \<in> reach")
|
blanchet@34969
|
236 |
nitpick
|
blanchet@34969
|
237 |
oops
|
blanchet@34969
|
238 |
|
blanchet@34969
|
239 |
lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
|
blanchet@34969
|
240 |
nitpick
|
blanchet@34969
|
241 |
apply (induct set: reach)
|
blanchet@34969
|
242 |
apply auto
|
blanchet@34969
|
243 |
nitpick
|
blanchet@34969
|
244 |
apply (thin_tac "n \<in> reach")
|
blanchet@34969
|
245 |
nitpick
|
blanchet@34969
|
246 |
oops
|
blanchet@34969
|
247 |
|
blanchet@34969
|
248 |
lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"
|
blanchet@34969
|
249 |
by (induct set: reach) arith+
|
blanchet@34969
|
250 |
|
blanchet@34969
|
251 |
datatype 'a bin_tree = Leaf 'a | Branch "'a bin_tree" "'a bin_tree"
|
blanchet@34969
|
252 |
|
blanchet@34969
|
253 |
primrec labels where
|
blanchet@34969
|
254 |
"labels (Leaf a) = {a}" |
|
blanchet@34969
|
255 |
"labels (Branch t u) = labels t \<union> labels u"
|
blanchet@34969
|
256 |
|
blanchet@34969
|
257 |
primrec swap where
|
blanchet@34969
|
258 |
"swap (Leaf c) a b =
|
blanchet@34969
|
259 |
(if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
|
blanchet@34969
|
260 |
"swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
|
blanchet@34969
|
261 |
|
blanchet@34969
|
262 |
lemma "\<lbrakk>a \<in> labels t; b \<in> labels t; a \<noteq> b\<rbrakk> \<Longrightarrow> labels (swap t a b) = labels t"
|
blanchet@34969
|
263 |
nitpick
|
blanchet@34969
|
264 |
proof (induct t)
|
blanchet@34969
|
265 |
case Leaf thus ?case by simp
|
blanchet@34969
|
266 |
next
|
blanchet@34969
|
267 |
case (Branch t u) thus ?case
|
blanchet@34969
|
268 |
nitpick
|
blanchet@34969
|
269 |
nitpick [non_std "'a bin_tree", show_consts]
|
blanchet@34969
|
270 |
oops
|
blanchet@34969
|
271 |
|
blanchet@34969
|
272 |
lemma "labels (swap t a b) =
|
blanchet@34969
|
273 |
(if a \<in> labels t then
|
blanchet@34969
|
274 |
if b \<in> labels t then labels t else (labels t - {a}) \<union> {b}
|
blanchet@34969
|
275 |
else
|
blanchet@34969
|
276 |
if b \<in> labels t then (labels t - {b}) \<union> {a} else labels t)"
|
blanchet@34969
|
277 |
nitpick
|
blanchet@34969
|
278 |
proof (induct t)
|
blanchet@34969
|
279 |
case Leaf thus ?case by simp
|
blanchet@34969
|
280 |
next
|
blanchet@34969
|
281 |
case (Branch t u) thus ?case
|
blanchet@34969
|
282 |
nitpick [non_std "'a bin_tree", show_consts]
|
blanchet@34969
|
283 |
by auto
|
blanchet@34969
|
284 |
qed
|
blanchet@34969
|
285 |
|
blanchet@33197
|
286 |
section {* 4. Case Studies *}
|
blanchet@33197
|
287 |
|
blanchet@33197
|
288 |
nitpick_params [max_potential = 0, max_threads = 2]
|
blanchet@33197
|
289 |
|
blanchet@33197
|
290 |
subsection {* 4.1. A Context-Free Grammar *}
|
blanchet@33197
|
291 |
|
blanchet@33197
|
292 |
datatype alphabet = a | b
|
blanchet@33197
|
293 |
|
blanchet@33197
|
294 |
inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
|
blanchet@33197
|
295 |
"[] \<in> S\<^isub>1"
|
blanchet@33197
|
296 |
| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
|
blanchet@33197
|
297 |
| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
|
blanchet@33197
|
298 |
| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
|
blanchet@33197
|
299 |
| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
|
blanchet@33197
|
300 |
| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
|
blanchet@33197
|
301 |
|
blanchet@33197
|
302 |
theorem S\<^isub>1_sound:
|
blanchet@33197
|
303 |
"w \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
|
blanchet@33197
|
304 |
nitpick
|
blanchet@33197
|
305 |
oops
|
blanchet@33197
|
306 |
|
blanchet@33197
|
307 |
inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
|
blanchet@33197
|
308 |
"[] \<in> S\<^isub>2"
|
blanchet@33197
|
309 |
| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
|
blanchet@33197
|
310 |
| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
|
blanchet@33197
|
311 |
| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
|
blanchet@33197
|
312 |
| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
|
blanchet@33197
|
313 |
| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
|
blanchet@33197
|
314 |
|
blanchet@33197
|
315 |
theorem S\<^isub>2_sound:
|
blanchet@33197
|
316 |
"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
|
blanchet@33197
|
317 |
nitpick
|
blanchet@33197
|
318 |
oops
|
blanchet@33197
|
319 |
|
blanchet@33197
|
320 |
inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
|
blanchet@33197
|
321 |
"[] \<in> S\<^isub>3"
|
blanchet@33197
|
322 |
| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
|
blanchet@33197
|
323 |
| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
|
blanchet@33197
|
324 |
| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
|
blanchet@33197
|
325 |
| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
|
blanchet@33197
|
326 |
| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
|
blanchet@33197
|
327 |
|
blanchet@33197
|
328 |
theorem S\<^isub>3_sound:
|
blanchet@33197
|
329 |
"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
|
blanchet@33197
|
330 |
nitpick
|
blanchet@33197
|
331 |
sorry
|
blanchet@33197
|
332 |
|
blanchet@33197
|
333 |
theorem S\<^isub>3_complete:
|
blanchet@33197
|
334 |
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
|
blanchet@33197
|
335 |
nitpick
|
blanchet@33197
|
336 |
oops
|
blanchet@33197
|
337 |
|
blanchet@33197
|
338 |
inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
|
blanchet@33197
|
339 |
"[] \<in> S\<^isub>4"
|
blanchet@33197
|
340 |
| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
|
blanchet@33197
|
341 |
| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
|
blanchet@33197
|
342 |
| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
|
blanchet@33197
|
343 |
| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
|
blanchet@33197
|
344 |
| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
|
blanchet@33197
|
345 |
| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
|
blanchet@33197
|
346 |
|
blanchet@33197
|
347 |
theorem S\<^isub>4_sound:
|
blanchet@33197
|
348 |
"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
|
blanchet@33197
|
349 |
nitpick
|
blanchet@33197
|
350 |
sorry
|
blanchet@33197
|
351 |
|
blanchet@33197
|
352 |
theorem S\<^isub>4_complete:
|
blanchet@33197
|
353 |
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
|
blanchet@33197
|
354 |
nitpick
|
blanchet@33197
|
355 |
sorry
|
blanchet@33197
|
356 |
|
blanchet@33197
|
357 |
theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
|
blanchet@33197
|
358 |
"w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
|
blanchet@33197
|
359 |
"w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
|
blanchet@33197
|
360 |
"w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
|
blanchet@33197
|
361 |
nitpick
|
blanchet@33197
|
362 |
sorry
|
blanchet@33197
|
363 |
|
blanchet@33197
|
364 |
subsection {* 4.2. AA Trees *}
|
blanchet@33197
|
365 |
|
blanchet@34969
|
366 |
datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
|
blanchet@33197
|
367 |
|
blanchet@33197
|
368 |
primrec data where
|
blanchet@33197
|
369 |
"data \<Lambda> = undefined" |
|
blanchet@33197
|
370 |
"data (N x _ _ _) = x"
|
blanchet@33197
|
371 |
|
blanchet@33197
|
372 |
primrec dataset where
|
blanchet@33197
|
373 |
"dataset \<Lambda> = {}" |
|
blanchet@33197
|
374 |
"dataset (N x _ t u) = {x} \<union> dataset t \<union> dataset u"
|
blanchet@33197
|
375 |
|
blanchet@33197
|
376 |
primrec level where
|
blanchet@33197
|
377 |
"level \<Lambda> = 0" |
|
blanchet@33197
|
378 |
"level (N _ k _ _) = k"
|
blanchet@33197
|
379 |
|
blanchet@33197
|
380 |
primrec left where
|
blanchet@33197
|
381 |
"left \<Lambda> = \<Lambda>" |
|
blanchet@33197
|
382 |
"left (N _ _ t\<^isub>1 _) = t\<^isub>1"
|
blanchet@33197
|
383 |
|
blanchet@33197
|
384 |
primrec right where
|
blanchet@33197
|
385 |
"right \<Lambda> = \<Lambda>" |
|
blanchet@33197
|
386 |
"right (N _ _ _ t\<^isub>2) = t\<^isub>2"
|
blanchet@33197
|
387 |
|
blanchet@33197
|
388 |
fun wf where
|
blanchet@33197
|
389 |
"wf \<Lambda> = True" |
|
blanchet@33197
|
390 |
"wf (N _ k t u) =
|
blanchet@33197
|
391 |
(if t = \<Lambda> then
|
blanchet@33197
|
392 |
k = 1 \<and> (u = \<Lambda> \<or> (level u = 1 \<and> left u = \<Lambda> \<and> right u = \<Lambda>))
|
blanchet@33197
|
393 |
else
|
blanchet@33197
|
394 |
wf t \<and> wf u \<and> u \<noteq> \<Lambda> \<and> level t < k \<and> level u \<le> k \<and> level (right u) < k)"
|
blanchet@33197
|
395 |
|
blanchet@33197
|
396 |
fun skew where
|
blanchet@33197
|
397 |
"skew \<Lambda> = \<Lambda>" |
|
blanchet@33197
|
398 |
"skew (N x k t u) =
|
blanchet@33197
|
399 |
(if t \<noteq> \<Lambda> \<and> k = level t then
|
blanchet@33197
|
400 |
N (data t) k (left t) (N x k (right t) u)
|
blanchet@33197
|
401 |
else
|
blanchet@33197
|
402 |
N x k t u)"
|
blanchet@33197
|
403 |
|
blanchet@33197
|
404 |
fun split where
|
blanchet@33197
|
405 |
"split \<Lambda> = \<Lambda>" |
|
blanchet@33197
|
406 |
"split (N x k t u) =
|
blanchet@33197
|
407 |
(if u \<noteq> \<Lambda> \<and> k = level (right u) then
|
blanchet@33197
|
408 |
N (data u) (Suc k) (N x k t (left u)) (right u)
|
blanchet@33197
|
409 |
else
|
blanchet@33197
|
410 |
N x k t u)"
|
blanchet@33197
|
411 |
|
blanchet@33197
|
412 |
theorem dataset_skew_split:
|
blanchet@33197
|
413 |
"dataset (skew t) = dataset t"
|
blanchet@33197
|
414 |
"dataset (split t) = dataset t"
|
blanchet@33197
|
415 |
nitpick
|
blanchet@33197
|
416 |
sorry
|
blanchet@33197
|
417 |
|
blanchet@33197
|
418 |
theorem wf_skew_split:
|
blanchet@33197
|
419 |
"wf t \<Longrightarrow> skew t = t"
|
blanchet@33197
|
420 |
"wf t \<Longrightarrow> split t = t"
|
blanchet@33197
|
421 |
nitpick
|
blanchet@33197
|
422 |
sorry
|
blanchet@33197
|
423 |
|
blanchet@33197
|
424 |
primrec insort\<^isub>1 where
|
blanchet@33197
|
425 |
"insort\<^isub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
|
blanchet@33197
|
426 |
"insort\<^isub>1 (N y k t u) x =
|
blanchet@33197
|
427 |
(* (split \<circ> skew) *) (N y k (if x < y then insort\<^isub>1 t x else t)
|
blanchet@33197
|
428 |
(if x > y then insort\<^isub>1 u x else u))"
|
blanchet@33197
|
429 |
|
blanchet@33197
|
430 |
theorem wf_insort\<^isub>1: "wf t \<Longrightarrow> wf (insort\<^isub>1 t x)"
|
blanchet@33197
|
431 |
nitpick
|
blanchet@33197
|
432 |
oops
|
blanchet@33197
|
433 |
|
blanchet@33197
|
434 |
theorem wf_insort\<^isub>1_nat: "wf t \<Longrightarrow> wf (insort\<^isub>1 t (x\<Colon>nat))"
|
blanchet@33197
|
435 |
nitpick [eval = "insort\<^isub>1 t x"]
|
blanchet@33197
|
436 |
oops
|
blanchet@33197
|
437 |
|
blanchet@33197
|
438 |
primrec insort\<^isub>2 where
|
blanchet@33197
|
439 |
"insort\<^isub>2 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
|
blanchet@33197
|
440 |
"insort\<^isub>2 (N y k t u) x =
|
blanchet@33197
|
441 |
(split \<circ> skew) (N y k (if x < y then insort\<^isub>2 t x else t)
|
blanchet@33197
|
442 |
(if x > y then insort\<^isub>2 u x else u))"
|
blanchet@33197
|
443 |
|
blanchet@33197
|
444 |
theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
|
blanchet@33197
|
445 |
nitpick
|
blanchet@33197
|
446 |
sorry
|
blanchet@33197
|
447 |
|
blanchet@33197
|
448 |
theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
|
blanchet@33197
|
449 |
nitpick
|
blanchet@33197
|
450 |
sorry
|
blanchet@33197
|
451 |
|
blanchet@33197
|
452 |
end
|