302 @ @{thms ho_all_prs ho_ex_prs} *} |
302 @ @{thms ho_all_prs ho_ex_prs} *} |
303 |
303 |
304 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
304 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
305 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
305 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
306 ML {* val consts = lookup_quot_consts defs *} |
306 ML {* val consts = lookup_quot_consts defs *} |
307 ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *} |
307 ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs *} |
308 |
308 |
309 lemma "IN x EMPTY = False" |
309 lemma "IN x EMPTY = False" |
310 by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *}) |
310 by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *}) |
311 |
311 |
312 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
312 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
332 (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)" |
332 (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)" |
333 apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
333 apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
334 done |
334 done |
335 |
335 |
336 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
336 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
337 apply(tactic {* Induct.fix_tac @{context} 0 [("x", @{typ "'b fset"}), ("xa", @{typ "'b fset"})] 1 *}) |
|
338 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
|
339 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
337 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
340 done |
338 done |
341 |
339 |
342 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
340 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
343 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
341 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
344 done |
342 done |
345 |
343 |
346 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} |
|
347 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} |
|
348 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
344 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
349 apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *}) |
345 apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *}) |
350 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *}) |
|
351 apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) |
|
352 done |
346 done |
353 |
347 |
354 quotient_def |
348 quotient_def |
355 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
349 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
356 where |
350 where |
374 apply (auto simp add: FUN_REL_EQ) |
368 apply (auto simp add: FUN_REL_EQ) |
375 sorry |
369 sorry |
376 |
370 |
377 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} |
371 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} |
378 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *} |
372 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *} |
379 ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *} |
373 ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs *} |
380 |
374 |
381 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.recs(2)})) *} |
|
382 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} |
|
383 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" |
375 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" |
384 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) |
376 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) |
385 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *}) |
377 done |
386 apply (tactic {* (simp_tac (HOL_ss addsimps |
378 |
387 @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id})) 1 *}) |
|
388 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} |
|
389 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *}) |
|
390 apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) |
|
391 done |
|
392 |
|
393 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.cases(2)})) *} |
|
394 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} |
|
395 lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa" |
379 lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa" |
396 apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *}) |
380 apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *}) |
397 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *}) |
|
398 apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) |
|
399 done |
381 done |
400 |
382 |
401 lemma list_induct_part: |
383 lemma list_induct_part: |
402 assumes a: "P (x :: 'a list) ([] :: 'c list)" |
384 assumes a: "P (x :: 'a list) ([] :: 'c list)" |
403 assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)" |
385 assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)" |
414 |
396 |
415 |
397 |
416 |
398 |
417 (* Construction site starts here *) |
399 (* Construction site starts here *) |
418 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" |
400 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" |
419 apply (tactic {* procedure_tac @{thm list_induct_part} @{context} 1 *}) |
401 apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *}) |
420 apply (tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
402 apply (tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
421 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
403 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
422 apply (rule FUN_QUOTIENT) |
404 apply (rule FUN_QUOTIENT) |
423 apply (rule FUN_QUOTIENT) |
405 apply (rule FUN_QUOTIENT) |
424 apply (rule IDENTITY_QUOTIENT) |
406 apply (rule IDENTITY_QUOTIENT) |
440 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
422 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
441 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
423 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
442 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
424 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
443 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
425 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
444 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
426 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
445 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
|
446 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
427 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
447 apply (rule IDENTITY_QUOTIENT) |
428 apply (rule IDENTITY_QUOTIENT) |
448 apply (rule FUN_QUOTIENT) |
429 apply (rule FUN_QUOTIENT) |
449 apply (rule QUOTIENT_fset) |
430 apply (rule QUOTIENT_fset) |
450 apply (rule IDENTITY_QUOTIENT) |
431 apply (rule IDENTITY_QUOTIENT) |
464 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
445 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
465 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
446 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
466 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
447 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
467 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
448 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
468 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
449 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
469 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
|
470 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
450 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
471 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *}) |
451 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *}) |
472 apply assumption |
452 apply assumption |
473 apply (rule refl) |
453 apply (rule refl) |
474 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
454 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
484 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *}) |
464 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *}) |
485 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
465 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
486 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
466 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
487 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
467 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
488 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
468 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
489 apply (simp only:map_id) |
469 apply (tactic {* clean_tac @{context} quot defs reps_same absrep [(@{typ "('a list \<Rightarrow> 'c list \<Rightarrow> bool)"},@{typ "('a list \<Rightarrow> 'c fset \<Rightarrow> bool)"})] 1 *}) |
490 apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) |
|
491 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} |
|
492 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *}) |
|
493 apply (tactic {* lambda_prs_tac @{context} quot 1 *}) |
|
494 ML_prf {* val t = applic_prs @{context} rty qty absrep @{typ "('b \<Rightarrow> 'c list \<Rightarrow> bool)"} *} |
|
495 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] [t]) 1 *}) |
|
496 apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) |
|
497 done |
470 done |
498 |
471 |
499 end |
472 end |