182 @{const_name "append"}, @{const_name "fold1"}, |
182 @{const_name "append"}, @{const_name "fold1"}, |
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 |
|
188 ML {* MetaSimplifier.rewrite_rule*} |
|
189 |
|
190 |
|
191 ML {* |
|
192 fun add_lower_defs ctxt defs = |
|
193 let |
|
194 val defs_pre_sym = map symmetric defs |
|
195 val defs_atom = map atomize_thm defs_pre_sym |
|
196 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 |
|
200 map Thm.varifyT defs_id |
|
201 end |
|
202 *} |
187 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *} |
203 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *} |
188 |
204 |
189 lemma memb_rsp: |
205 lemma memb_rsp: |
190 fixes z |
206 fixes z |
191 assumes a: "list_eq x y" |
207 assumes a: "list_eq x y" |
392 |
408 |
393 thm fold1.simps(2) |
409 thm fold1.simps(2) |
394 thm list.recs(2) |
410 thm list.recs(2) |
395 thm map_append |
411 thm map_append |
396 |
412 |
397 ML {* val ind_r_a = atomize_thm @{thm list_induct_hol4} *} |
413 ML {* val ind_r_a = atomize_thm @{thm map_append} *} |
398 (* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
414 (* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
399 ML_prf {* fun tac ctxt = |
415 ML_prf {* fun tac ctxt = |
400 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
416 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
401 [(@{thm equiv_res_forall} OF [@{thm equiv_list_eq}]), |
417 [(@{thm equiv_res_forall} OF [@{thm equiv_list_eq}]), |
402 (@{thm equiv_res_exists} OF [@{thm equiv_list_eq}])])) THEN_ALL_NEW |
418 (@{thm equiv_res_exists} OF [@{thm equiv_list_eq}])])) THEN_ALL_NEW |
438 ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *} |
454 ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *} |
439 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1" |
455 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1" |
440 apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10) |
456 apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10) |
441 done |
457 done |
442 |
458 |
443 ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *} |
459 (*ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *} |
444 ML {* val ind_r_l2 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l1 *} |
460 ML {* val ind_r_l2 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l1 *} |
445 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *} |
461 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *} |
446 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *} |
462 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *}*) |
447 ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l4 *} |
463 ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l *} |
448 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *} |
464 (*ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *}*) |
449 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *} |
465 (*ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *}*) |
450 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *} |
466 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a *} |
451 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
467 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
452 ML {* ObjectLogic.rulify ind_r_s *} |
468 ML {* val thm = atomize_thm @{thm fmap_def[symmetric]} *} |
|
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 |
453 |
500 |
454 ML {* |
501 ML {* |
455 fun lift thm = |
502 fun lift thm = |
456 let |
503 let |
457 val ind_r_a = atomize_thm thm; |
504 val ind_r_a = atomize_thm thm; |