equal
deleted
inserted
replaced
165 @{const_name "membship"}, @{const_name "card1"}, |
165 @{const_name "membship"}, @{const_name "card1"}, |
166 @{const_name "append"}, @{const_name "fold1"}]; |
166 @{const_name "append"}, @{const_name "fold1"}]; |
167 *} |
167 *} |
168 |
168 |
169 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
169 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
170 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *} |
170 text {* expects atomized definition *} |
|
171 ML {* |
|
172 fun add_lower_defs ctxt thm = |
|
173 let |
|
174 val e1 = @{thm fun_cong} OF [thm] |
|
175 val f = eqsubst_thm ctxt @{thms fun_map.simps} e1 |
|
176 in |
|
177 thm :: (add_lower_defs ctxt f) |
|
178 end |
|
179 handle _ => [thm] |
|
180 *} |
|
181 ML {* val fset_defs_pre_sym = map symmetric fset_defs *} |
|
182 ML {* val fset_defs_atom = map atomize_thm fset_defs_pre_sym *} |
|
183 ML {* val fset_defs_all = flat (map (add_lower_defs @{context}) fset_defs_atom) *} |
|
184 ML {* val fset_defs_sym = map (fn t => eq_reflection OF [t]) fset_defs_all *} |
|
185 ML {* val fset_defs_sym = map ObjectLogic.rulify fset_defs_sym *} |
|
186 ML {* val fset_defs_sym = map Thm.varifyT fset_defs_sym *} |
|
187 |
|
188 |
|
189 (* |
|
190 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *} |
|
191 *) |
|
192 |
171 |
193 |
172 thm fun_map.simps |
194 thm fun_map.simps |
173 text {* Respectfullness *} |
195 text {* Respectfullness *} |
174 |
196 |
175 lemma memb_rsp: |
197 lemma memb_rsp: |
390 end |
412 end |
391 handle _ => thm |
413 handle _ => thm |
392 *} |
414 *} |
393 |
415 |
394 ML {* val ithm = simp_allex_prs @{context} m2_t' *} |
416 ML {* val ithm = simp_allex_prs @{context} m2_t' *} |
|
417 ML fset_defs_sym |
|
418 |
395 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
419 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
396 ML {* ObjectLogic.rulify rthm *} |
420 ML {* ObjectLogic.rulify rthm *} |
397 |
421 |
398 |
422 |
399 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
423 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
413 |
437 |
414 prove card1_suc_t: card1_suc_t |
438 prove card1_suc_t: card1_suc_t |
415 apply (simp only: card1_suc_t_p[symmetric]) |
439 apply (simp only: card1_suc_t_p[symmetric]) |
416 apply (tactic {* rtac card1_suc_r 1 *}) |
440 apply (tactic {* rtac card1_suc_r 1 *}) |
417 done |
441 done |
418 |
|
419 |
442 |
420 ML {* val card1_suc_t_n = @{thm card1_suc_t} *} |
443 ML {* val card1_suc_t_n = @{thm card1_suc_t} *} |
421 ML {* val card1_suc_t' = eqsubst_thm @{context} @{thms HOL.sym[OF lambda_prs_l_b,simplified]} @{thm card1_suc_t} *} |
444 ML {* val card1_suc_t' = eqsubst_thm @{context} @{thms HOL.sym[OF lambda_prs_l_b,simplified]} @{thm card1_suc_t} *} |
422 ML {* val card1_suc_t'' = eqsubst_thm @{context} @{thms HOL.sym[OF lambda_prs_l_b,simplified]} card1_suc_t' *} |
445 ML {* val card1_suc_t'' = eqsubst_thm @{context} @{thms HOL.sym[OF lambda_prs_l_b,simplified]} card1_suc_t' *} |
423 ML {* val ithm = simp_allex_prs @{context} card1_suc_t'' *} |
446 ML {* val ithm = simp_allex_prs @{context} card1_suc_t'' *} |
476 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *} |
499 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *} |
477 ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l4 *} |
500 ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l4 *} |
478 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *} |
501 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *} |
479 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *} |
502 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *} |
480 |
503 |
|
504 |
|
505 ML {* hd fset_defs_sym *} |
481 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *} |
506 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *} |
482 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
507 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
483 ML {* ObjectLogic.rulify ind_r_s *} |
508 ML {* ObjectLogic.rulify ind_r_s *} |
484 |
509 |
485 ML {* |
510 ML {* |