183 @{const_name "map"}]; |
183 @{const_name "map"}]; |
184 *} |
184 *} |
185 |
185 |
186 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *} |
186 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *} |
187 |
187 |
188 ML {* MetaSimplifier.rewrite_rule*} |
|
189 |
|
190 |
|
191 ML {* |
188 ML {* |
192 fun add_lower_defs ctxt defs = |
189 fun add_lower_defs ctxt defs = |
193 let |
190 let |
194 val defs_pre_sym = map symmetric defs |
191 val defs_pre_sym = map symmetric defs |
195 val defs_atom = map atomize_thm defs_pre_sym |
192 val defs_atom = map atomize_thm defs_pre_sym |
196 val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom) |
193 val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom) |
197 val defs_sym = map (fn t => eq_reflection OF [t]) defs_all |
|
198 val defs_id = map (MetaSimplifier.rewrite_rule @{thms id_def_sym}) defs_sym |
|
199 in |
194 in |
200 map Thm.varifyT defs_id |
195 map Thm.varifyT defs_all |
201 end |
196 end |
202 *} |
197 *} |
203 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *} |
198 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *} |
|
199 |
204 |
200 |
205 lemma memb_rsp: |
201 lemma memb_rsp: |
206 fixes z |
202 fixes z |
207 assumes a: "list_eq x y" |
203 assumes a: "list_eq x y" |
208 shows "(z memb x) = (z memb y)" |
204 shows "(z memb x) = (z memb y)" |
454 ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *} |
450 ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *} |
455 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1" |
451 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1" |
456 apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10) |
452 apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10) |
457 done |
453 done |
458 |
454 |
459 (*ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *} |
455 ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *} |
460 ML {* val ind_r_l2 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l1 *} |
456 ML {* val ind_r_l2 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l1 *} |
461 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *} |
457 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *} |
462 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *}*) |
458 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *} |
463 ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l *} |
459 ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l4 *} |
464 (*ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *}*) |
460 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *} |
465 (*ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *}*) |
461 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *} |
466 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a *} |
462 ML {* val ind_r_d = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a1 *} |
467 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
463 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
468 ML {* val thm = atomize_thm @{thm fmap_def[symmetric]} *} |
464 ML {* ObjectLogic.rulify ind_r_s *} |
469 ML {* val e1 = @{thm fun_cong} OF [thm] *} |
|
470 ML {* val f1 = eqsubst_thm @{context} @{thms fun_map.simps} e1 *} |
|
471 ML {* val e2 = @{thm fun_cong} OF [f1] *} |
|
472 ML {* val f2 = eqsubst_thm @{context} @{thms fun_map.simps} e2 *} |
|
473 ML {* val h2 = MetaSimplifier.rewrite_rule @{thms id_def_sym} f2 *} |
|
474 ML {* val h3 = eqsubst_thm @{context} @{thms FUN_MAP_I} h2 *} |
|
475 ML {* val h2 = MetaSimplifier.rewrite_rule @{thms id_apply2} h3 *} |
|
476 ML {* val h4 = eq_reflection OF [h2] *} |
|
477 |
|
478 ML {* |
|
479 fun eqsubst_thm ctxt thms thm = |
|
480 let |
|
481 val goalstate = Goal.init (Thm.cprop_of thm) |
|
482 val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of |
|
483 NONE => error "eqsubst_thm" |
|
484 | SOME th => cprem_of th 1 |
|
485 val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 |
|
486 val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a')) |
|
487 val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac)); |
|
488 in |
|
489 @{thm Pure.equal_elim_rule1} OF [rt,thm] |
|
490 end |
|
491 *} |
|
492 |
|
493 ML {* val ind_r_d = eqsubst_thm @{context} [h4] ind_r_s *} |
|
494 ML {* val ind_r_d' = eqsubst_thm @{context} [h4] ind_r_d *} |
|
495 ML {* val ind_r_d'' = eqsubst_thm @{context} [h4] ind_r_d' *} |
|
496 ML {* ObjectLogic.rulify ind_r_d'' *} |
|
497 |
|
498 |
|
499 |
|
500 |
465 |
501 ML {* |
466 ML {* |
502 fun lift thm = |
467 fun lift thm = |
503 let |
468 let |
504 val ind_r_a = atomize_thm thm; |
469 val ind_r_a = atomize_thm thm; |
505 val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context}; |
470 val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context}; |
506 val (g, t, ot) = |
471 val (g, t, ot) = |
507 repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
472 repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
508 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
473 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
509 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} @ @{thms ho_all_prs ho_ex_prs}); |
474 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}); |
510 val ind_r_t = repabs_eq2 @{context} (g, t, ot); |
475 val ind_r_t = repabs_eq2 @{context} (g, t, ot); |
511 val ind_r_l = simp_lam_prs @{context} ind_r_t; |
476 val ind_r_l = simp_lam_prs @{context} ind_r_t; |
512 val ind_r_a = simp_allex_prs @{context} quot ind_r_l; |
477 val ind_r_a = simp_allex_prs @{context} quot ind_r_l; |
513 val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a; |
478 val ind_r_d = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a; |
514 val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d |
479 val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d |
515 in |
480 in |
516 ObjectLogic.rulify ind_r_s |
481 ObjectLogic.rulify ind_r_s |
517 end |
482 end |
518 *} |
483 *} |