24 |
24 |
25 quotient fset = "'a list" / "list_eq" |
25 quotient fset = "'a list" / "list_eq" |
26 apply(rule equivp_list_eq) |
26 apply(rule equivp_list_eq) |
27 done |
27 done |
28 |
28 |
29 print_theorems |
|
30 |
|
31 typ "'a fset" |
|
32 thm "Rep_fset" |
|
33 thm "ABS_fset_def" |
|
34 |
|
35 quotient_def |
29 quotient_def |
36 EMPTY :: "'a fset" |
30 EMPTY :: "'a fset" |
37 where |
31 where |
38 "EMPTY \<equiv> ([]::'a list)" |
32 "EMPTY \<equiv> ([]::'a list)" |
39 |
33 |
40 term Nil |
|
41 term EMPTY |
|
42 thm EMPTY_def |
|
43 |
|
44 quotient_def |
34 quotient_def |
45 INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
35 INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
46 where |
36 where |
47 "INSERT \<equiv> op #" |
37 "INSERT \<equiv> op #" |
48 |
38 |
49 term Cons |
|
50 term INSERT |
|
51 thm INSERT_def |
|
52 |
|
53 quotient_def |
39 quotient_def |
54 FUNION :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
40 FUNION :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
55 where |
41 where |
56 "FUNION \<equiv> (op @)" |
42 "FUNION \<equiv> (op @)" |
57 |
|
58 term append |
|
59 term FUNION |
|
60 thm FUNION_def |
|
61 |
|
62 thm Quotient_fset |
|
63 |
|
64 thm QUOT_TYPE_I_fset.thm11 |
|
65 |
|
66 |
43 |
67 fun |
44 fun |
68 membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100) |
45 membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100) |
69 where |
46 where |
70 m1: "(x memb []) = False" |
47 m1: "(x memb []) = False" |
146 quotient_def |
119 quotient_def |
147 IN :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" |
120 IN :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" |
148 where |
121 where |
149 "IN \<equiv> membship" |
122 "IN \<equiv> membship" |
150 |
123 |
151 term membship |
|
152 term IN |
|
153 thm IN_def |
|
154 |
|
155 term fold1 |
|
156 quotient_def |
124 quotient_def |
157 FOLD :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a" |
125 FOLD :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a" |
158 where |
126 where |
159 "FOLD \<equiv> fold1" |
127 "FOLD \<equiv> fold1" |
160 |
128 |
161 term fold1 |
|
162 term fold |
|
163 thm fold_def |
|
164 |
|
165 quotient_def |
129 quotient_def |
166 fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
130 fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
167 where |
131 where |
168 "fmap \<equiv> map" |
132 "fmap \<equiv> map" |
169 |
|
170 term map |
|
171 term fmap |
|
172 thm fmap_def |
|
173 |
133 |
174 lemma memb_rsp: |
134 lemma memb_rsp: |
175 fixes z |
135 fixes z |
176 assumes a: "x \<approx> y" |
136 assumes a: "x \<approx> y" |
177 shows "(z memb x) = (z memb y)" |
137 shows "(z memb x) = (z memb y)" |
288 |
248 |
289 lemma list_equiv_rsp[quot_respect]: |
249 lemma list_equiv_rsp[quot_respect]: |
290 shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>" |
250 shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>" |
291 by (auto intro: list_eq.intros) |
251 by (auto intro: list_eq.intros) |
292 |
252 |
293 print_quotients |
|
294 |
|
295 ML {* val qty = @{typ "'a fset"} *} |
|
296 ML {* val rsp_thms = |
|
297 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *} |
|
298 |
253 |
299 lemma "IN x EMPTY = False" |
254 lemma "IN x EMPTY = False" |
300 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) |
255 apply(lifting m1) |
301 apply(tactic {* regularize_tac @{context} 1 *}) |
|
302 apply(tactic {* all_inj_repabs_tac @{context} 1 *}) |
|
303 apply(tactic {* clean_tac @{context} 1*}) |
|
304 done |
256 done |
305 |
257 |
306 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
258 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
307 by (tactic {* lift_tac @{context} @{thm m2} 1 *}) |
259 by (lifting m2) |
308 |
260 |
309 lemma "INSERT a (INSERT a x) = INSERT a x" |
261 lemma "INSERT a (INSERT a x) = INSERT a x" |
310 apply (tactic {* lift_tac @{context} @{thm list_eq.intros(4)} 1 *}) |
262 apply (lifting list_eq.intros(4)) |
311 done |
263 done |
312 |
264 |
313 lemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa" |
265 lemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa" |
314 apply (tactic {* lift_tac @{context} @{thm list_eq.intros(5)} 1 *}) |
266 apply (lifting list_eq.intros(5)) |
315 done |
267 done |
316 |
268 |
317 lemma "CARD x = Suc n \<Longrightarrow> (\<exists>a b. \<not> IN a b & x = INSERT a b)" |
269 lemma "CARD x = Suc n \<Longrightarrow> (\<exists>a b. \<not> IN a b & x = INSERT a b)" |
318 apply (tactic {* lift_tac @{context} @{thm card1_suc} 1 *}) |
270 apply (lifting card1_suc) |
319 done |
271 done |
320 |
272 |
321 lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))" |
273 lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))" |
322 apply (tactic {* lift_tac @{context} @{thm not_mem_card1} 1 *}) |
274 apply (lifting not_mem_card1) |
323 done |
275 done |
324 |
276 |
325 lemma "FOLD f g (z::'b) (INSERT a x) = |
277 lemma "FOLD f g (z::'b) (INSERT a x) = |
326 (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)" |
278 (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)" |
327 apply(tactic {* lift_tac @{context} @{thm fold1.simps(2)} 1 *}) |
279 apply(lifting fold1.simps(2)) |
328 done |
280 done |
329 |
281 |
330 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
282 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
331 apply (tactic {* lift_tac @{context} @{thm map_append} 1 *}) |
283 apply (lifting map_append) |
332 done |
284 done |
333 |
285 |
334 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
286 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
335 apply (tactic {* lift_tac @{context} @{thm append_assoc} 1 *}) |
287 apply (lifting append_assoc) |
336 done |
288 done |
337 |
289 |
338 |
290 |
339 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
291 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
340 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
292 apply(lifting list.induct) |
341 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
|
342 apply(tactic {* regularize_tac @{context} 1 *}) |
|
343 apply(injection) |
|
344 apply(tactic {* clean_tac @{context} 1 *}) |
|
345 done |
293 done |
346 |
294 |
347 lemma list_induct_part: |
295 lemma list_induct_part: |
348 assumes a: "P (x :: 'a list) ([] :: 'c list)" |
296 assumes a: "P (x :: 'a list) ([] :: 'c list)" |
349 assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)" |
297 assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)" |
353 apply (rule b) |
301 apply (rule b) |
354 apply (assumption) |
302 apply (assumption) |
355 done |
303 done |
356 |
304 |
357 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
305 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
358 apply (tactic {* lift_tac @{context} @{thm list_induct_part} 1 *}) |
306 apply (lifting list_induct_part) |
359 done |
307 done |
360 |
308 |
361 lemma "P (x :: 'a fset) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
309 lemma "P (x :: 'a fset) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
362 apply (tactic {* lift_tac @{context} @{thm list_induct_part} 1 *}) |
310 apply (lifting list_induct_part) |
363 done |
311 done |
364 |
312 |
365 lemma "P (x :: 'a fset) ([] :: 'c list) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (e # t)) \<Longrightarrow> P x l" |
313 lemma "P (x :: 'a fset) ([] :: 'c list) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (e # t)) \<Longrightarrow> P x l" |
366 apply (tactic {* lift_tac @{context} @{thm list_induct_part} 1 *}) |
314 apply (lifting list_induct_part) |
367 done |
315 done |
368 |
316 |
369 quotient fset2 = "'a list" / "list_eq" |
317 quotient fset2 = "'a list" / "list_eq" |
370 apply(rule equivp_list_eq) |
318 by (rule equivp_list_eq) |
371 done |
|
372 |
319 |
373 quotient_def |
320 quotient_def |
374 EMPTY2 :: "'a fset2" |
321 EMPTY2 :: "'a fset2" |
375 where |
322 where |
376 "EMPTY2 \<equiv> ([]::'a list)" |
323 "EMPTY2 \<equiv> ([]::'a list)" |
379 INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2" |
326 INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2" |
380 where |
327 where |
381 "INSERT2 \<equiv> op #" |
328 "INSERT2 \<equiv> op #" |
382 |
329 |
383 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
330 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
384 apply (tactic {* lift_tac @{context} @{thm list_induct_part} 1 *}) |
331 apply (lifting list_induct_part) |
385 done |
332 done |
386 |
333 |
387 lemma "P (x :: 'a fset) (EMPTY2 :: 'c fset2) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT2 e t)) \<Longrightarrow> P x l" |
334 lemma "P (x :: 'a fset) (EMPTY2 :: 'c fset2) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT2 e t)) \<Longrightarrow> P x l" |
388 apply (tactic {* lift_tac @{context} @{thm list_induct_part} 1 *}) |
335 apply (lifting list_induct_part) |
389 done |
336 done |
390 |
337 |
391 quotient_def |
338 quotient_def |
392 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
339 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
393 where |
340 where |
410 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
357 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
411 apply (auto) |
358 apply (auto) |
412 sorry |
359 sorry |
413 |
360 |
414 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" |
361 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" |
415 apply (tactic {* lift_tac @{context} @{thm list.recs(2)} 1 *}) |
362 apply (lifting list.recs(2)) |
416 done |
363 done |
417 |
364 |
418 lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa" |
365 lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa" |
419 apply (tactic {* lift_tac @{context} @{thm list.cases(2)} 1 *}) |
366 apply (lifting list.cases(2)) |
420 done |
367 done |
421 |
368 |
422 lemma ttt: "((op @) x ((op #) e [])) = (((op #) e x))" |
369 lemma ttt: "((op @) x ((op #) e [])) = (((op #) e x))" |
423 sorry |
370 sorry |
|
371 |
424 lemma "(FUNION x (INSERT e EMPTY)) = ((INSERT e x))" |
372 lemma "(FUNION x (INSERT e EMPTY)) = ((INSERT e x))" |
425 apply (tactic {* lift_tac @{context} @{thm ttt} 1 *}) |
373 apply (lifting ttt) |
426 done |
374 done |
427 |
375 |
428 lemma ttt2: "(\<lambda>e. ((op @) x ((op #) e []))) = (\<lambda>e. ((op #) e x))" |
376 lemma ttt2: "(\<lambda>e. ((op @) x ((op #) e []))) = (\<lambda>e. ((op #) e x))" |
429 sorry |
377 sorry |
430 |
378 |
|
379 (* PROBLEM *) |
431 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))" |
380 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))" |
432 apply(lifting ttt2) |
381 apply(lifting ttt2) |
433 apply(regularize) |
382 apply(regularize) |
434 apply(rule impI) |
383 apply(rule impI) |
435 apply(simp) |
384 apply(simp) |
457 by simp |
406 by simp |
458 |
407 |
459 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))" |
408 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))" |
460 sorry |
409 sorry |
461 |
410 |
|
411 (* PROBLEM *) |
462 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))" |
412 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))" |
463 apply(lifting_setup hard) |
413 apply(lifting_setup hard) |
464 defer |
414 defer |
465 apply(injection) |
415 apply(injection) |
466 apply(subst babs_prs) |
|
467 apply(tactic {* quotient_tac @{context} 1 *}) |
|
468 apply(tactic {* quotient_tac @{context} 1 *}) |
|
469 apply(subst babs_prs) |
|
470 apply(tactic {* quotient_tac @{context} 1 *}) |
|
471 apply(tactic {* quotient_tac @{context} 1 *}) |
|
472 apply(subst babs_prs) |
|
473 apply(tactic {* quotient_tac @{context} 1 *}) |
|
474 apply(tactic {* quotient_tac @{context} 1 *}) |
|
475 apply(subst babs_prs) |
|
476 apply(tactic {* quotient_tac @{context} 1 *}) |
|
477 apply(tactic {* quotient_tac @{context} 1 *}) |
|
478 apply(subst all_prs) |
|
479 apply(tactic {* quotient_tac @{context} 1 *}) |
|
480 apply(tactic {* lambda_prs_tac @{context} 1 *}) |
|
481 apply(subst fun_map.simps) |
|
482 apply(tactic {* lambda_prs_tac @{context} 1 *}) |
|
483 apply(subst fun_map.simps) |
|
484 apply(subst fun_map.simps) |
|
485 apply(tactic {* lambda_prs_tac @{context} 1 *}) |
|
486 apply(cleaning) |
416 apply(cleaning) |
487 sorry |
417 sorry |
488 |
418 |
489 end |
419 end |