294 |
294 |
295 ML {* val qty = @{typ "'a fset"} *} |
295 ML {* val qty = @{typ "'a fset"} *} |
296 ML {* val rsp_thms = |
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} *} |
297 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *} |
298 |
298 |
299 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
|
300 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
|
301 ML {* fun lift_tac_fset lthy t = lift_tac lthy t *} |
|
302 |
|
303 lemma "IN x EMPTY = False" |
299 lemma "IN x EMPTY = False" |
304 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) |
300 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) |
305 apply(tactic {* regularize_tac @{context} 1 *}) |
301 apply(tactic {* regularize_tac @{context} 1 *}) |
306 apply(tactic {* all_inj_repabs_tac @{context} 1 *}) |
302 apply(tactic {* all_inj_repabs_tac @{context} 1 *}) |
307 apply(tactic {* clean_tac @{context} 1*}) |
303 apply(tactic {* clean_tac @{context} 1*}) |
308 done |
304 done |
309 |
305 |
310 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
306 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
311 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *}) |
307 by (tactic {* lift_tac @{context} @{thm m2} 1 *}) |
312 |
308 |
313 lemma "INSERT a (INSERT a x) = INSERT a x" |
309 lemma "INSERT a (INSERT a x) = INSERT a x" |
314 apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(4)} 1 *}) |
310 apply (tactic {* lift_tac @{context} @{thm list_eq.intros(4)} 1 *}) |
315 done |
311 done |
316 |
312 |
317 lemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa" |
313 lemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa" |
318 apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(5)} 1 *}) |
314 apply (tactic {* lift_tac @{context} @{thm list_eq.intros(5)} 1 *}) |
319 done |
315 done |
320 |
316 |
321 lemma "CARD x = Suc n \<Longrightarrow> (\<exists>a b. \<not> IN a b & x = INSERT a b)" |
317 lemma "CARD x = Suc n \<Longrightarrow> (\<exists>a b. \<not> IN a b & x = INSERT a b)" |
322 apply (tactic {* lift_tac_fset @{context} @{thm card1_suc} 1 *}) |
318 apply (tactic {* lift_tac @{context} @{thm card1_suc} 1 *}) |
323 done |
319 done |
324 |
320 |
325 lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))" |
321 lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))" |
326 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *}) |
322 apply (tactic {* lift_tac @{context} @{thm not_mem_card1} 1 *}) |
327 done |
323 done |
328 |
324 |
329 lemma "FOLD f g (z::'b) (INSERT a x) = |
325 lemma "FOLD f g (z::'b) (INSERT a x) = |
330 (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)" |
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)" |
331 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
327 apply(tactic {* lift_tac @{context} @{thm fold1.simps(2)} 1 *}) |
332 done |
328 done |
333 |
329 |
334 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
330 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
335 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
331 apply (tactic {* lift_tac @{context} @{thm map_append} 1 *}) |
336 done |
332 done |
337 |
333 |
338 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
334 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
339 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
335 apply (tactic {* lift_tac @{context} @{thm append_assoc} 1 *}) |
340 done |
336 done |
341 |
337 |
342 |
338 |
343 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
339 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
344 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
340 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
357 apply (rule a) |
353 apply (rule a) |
358 apply (rule b) |
354 apply (rule b) |
359 apply (assumption) |
355 apply (assumption) |
360 done |
356 done |
361 |
357 |
362 ML {* quot *} |
|
363 thm quotient_thm |
358 thm quotient_thm |
364 |
359 |
365 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" |
360 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" |
366 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) |
361 apply (tactic {* lift_tac @{context} @{thm list_induct_part} 1 *}) |
367 done |
362 done |
368 |
363 |
369 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" |
364 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" |
370 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) |
365 apply (tactic {* lift_tac @{context} @{thm list_induct_part} 1 *}) |
371 done |
366 done |
372 |
367 |
373 lemma "P (x :: 'a fset) ([] :: 'c list) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (e # t)) \<Longrightarrow> P x l" |
368 lemma "P (x :: 'a fset) ([] :: 'c list) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (e # t)) \<Longrightarrow> P x l" |
374 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) |
369 apply (tactic {* lift_tac @{context} @{thm list_induct_part} 1 *}) |
375 done |
370 done |
376 |
371 |
377 quotient fset2 = "'a list" / "list_eq" |
372 quotient fset2 = "'a list" / "list_eq" |
378 apply(rule equivp_list_eq) |
373 apply(rule equivp_list_eq) |
379 done |
374 done |
387 INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2" |
382 INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2" |
388 where |
383 where |
389 "INSERT2 \<equiv> op #" |
384 "INSERT2 \<equiv> op #" |
390 |
385 |
391 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" |
386 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" |
392 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) |
387 apply (tactic {* lift_tac @{context} @{thm list_induct_part} 1 *}) |
393 done |
388 done |
394 |
389 |
395 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" |
390 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" |
396 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) |
391 apply (tactic {* lift_tac @{context} @{thm list_induct_part} 1 *}) |
397 done |
392 done |
398 |
393 |
399 quotient_def |
394 quotient_def |
400 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
395 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
401 where |
396 where |
418 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
413 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
419 apply (auto) |
414 apply (auto) |
420 sorry |
415 sorry |
421 |
416 |
422 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" |
417 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" |
423 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) |
418 apply (tactic {* lift_tac @{context} @{thm list.recs(2)} 1 *}) |
424 done |
419 done |
425 |
420 |
426 lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa" |
421 lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa" |
427 apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *}) |
422 apply (tactic {* lift_tac @{context} @{thm list.cases(2)} 1 *}) |
428 done |
423 done |
429 |
424 |
430 lemma ttt: "((op @) x ((op #) e [])) = (((op #) e x))" |
425 lemma ttt: "((op @) x ((op #) e [])) = (((op #) e x))" |
431 sorry |
426 sorry |
432 lemma "(FUNION x (INSERT e EMPTY)) = ((INSERT e x))" |
427 lemma "(FUNION x (INSERT e EMPTY)) = ((INSERT e x))" |
438 |
433 |
439 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))" |
434 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))" |
440 apply (tactic {* procedure_tac @{context} @{thm ttt2} 1 *}) |
435 apply (tactic {* procedure_tac @{context} @{thm ttt2} 1 *}) |
441 apply(tactic {* regularize_tac @{context} 1 *}) |
436 apply(tactic {* regularize_tac @{context} 1 *}) |
442 defer |
437 defer |
443 apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1*}) |
438 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
444 (* apply(tactic {* clean_tac @{context} 1 *}) *) |
439 apply(tactic {* clean_tac @{context} 1 *}) |
|
440 thm lambda_prs[OF identity_quotient Quotient_fset] |
|
441 thm lambda_prs[OF identity_quotient Quotient_fset, simplified] |
|
442 apply(simp only: lambda_prs[OF identity_quotient Quotient_fset,simplified]) |
445 sorry |
443 sorry |
446 |
444 |
447 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))" |
445 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))" |
448 sorry |
446 sorry |
449 |
447 |
450 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))" |
448 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))" |
451 (* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *) |
449 apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) |
452 sorry |
450 sorry |
453 |
451 |
454 end |
452 end |