355 end |
355 end |
356 | f $ a => (findabs rty f) @ (findabs rty a) |
356 | f $ a => (findabs rty f) @ (findabs rty a) |
357 | _ => [] |
357 | _ => [] |
358 *} |
358 *} |
359 |
359 |
360 ML {* findabs @{typ "'a list"} (prop_of (atomize_thm @{thm list_induct_hol4})) *} |
360 ML {* val quot = @{thm QUOTIENT_fset} *} |
361 |
361 ML {* val abs = findabs @{typ "'a list"} (prop_of (atomize_thm @{thm list_induct_hol4})) *} |
362 ML {* |
362 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
363 val lpi = Drule.instantiate' |
|
364 [SOME @{ctyp "'a list"}, NONE, SOME @{ctyp "bool"}, NONE] [] @{thm LAMBDA_PRS}; |
|
365 *} |
|
366 prove lambda_prs_l_b : {* concl_of lpi *} |
|
367 apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *}) |
|
368 apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *}) |
|
369 apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *}) |
|
370 done |
|
371 thm HOL.sym[OF lambda_prs_l_b,simplified] |
|
372 ML {* |
|
373 val lpi = Drule.instantiate' |
|
374 [SOME @{ctyp "'a list \<Rightarrow> bool"}, NONE, SOME @{ctyp "bool"}, NONE] [] @{thm LAMBDA_PRS}; |
|
375 *} |
|
376 prove lambda_prs_lb_b : {* concl_of lpi *} |
|
377 apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *}) |
|
378 apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *}) |
|
379 apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *}) |
|
380 done |
|
381 thm HOL.sym[OF lambda_prs_lb_b,simplified] |
|
382 |
|
383 |
|
384 |
|
385 |
363 |
386 ML {* |
364 ML {* |
387 fun simp_lam_prs lthy thm = |
365 fun simp_lam_prs lthy thm = |
388 simp_lam_prs lthy (eqsubst_thm lthy |
366 simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) |
389 @{thms HOL.sym[OF lambda_prs_lb_b,simplified] HOL.sym[OF lambda_prs_l_b,simplified]} |
|
390 thm) |
|
391 handle _ => thm |
367 handle _ => thm |
392 *} |
368 *} |
393 |
369 |
394 ML {* val m2_t' = eqsubst_thm @{context} [lam_prs] @{thm m2_t} *} |
370 ML {* val m2_t' = eqsubst_thm @{context} [lam_prs] @{thm m2_t} *} |
395 |
371 |
396 ML {* |
372 ML {* val ithm = simp_allex_prs @{context} quot m2_t' *} |
397 fun simp_allex_prs lthy thm = |
|
398 let |
|
399 val rwf = @{thm FORALL_PRS[OF QUOTIENT_fset]}; |
|
400 val rwfs = @{thm "HOL.sym"} OF [rwf]; |
|
401 val rwe = @{thm EXISTS_PRS[OF QUOTIENT_fset]}; |
|
402 val rwes = @{thm "HOL.sym"} OF [rwe] |
|
403 in |
|
404 (simp_allex_prs lthy (eqsubst_thm lthy [rwfs, rwes] thm)) |
|
405 end |
|
406 handle _ => thm |
|
407 *} |
|
408 |
|
409 ML {* val ithm = simp_allex_prs @{context} m2_t' *} |
|
410 ML fset_defs_sym |
373 ML fset_defs_sym |
411 |
374 |
412 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
375 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
413 ML {* ObjectLogic.rulify rthm *} |
376 ML {* ObjectLogic.rulify rthm *} |
414 |
377 |
432 apply (simp only: card1_suc_t_p[symmetric]) |
395 apply (simp only: card1_suc_t_p[symmetric]) |
433 apply (tactic {* rtac card1_suc_r 1 *}) |
396 apply (tactic {* rtac card1_suc_r 1 *}) |
434 done |
397 done |
435 |
398 |
436 ML {* val card1_suc_t_n = @{thm card1_suc_t} *} |
399 ML {* val card1_suc_t_n = @{thm card1_suc_t} *} |
437 ML {* val card1_suc_t' = eqsubst_thm @{context} @{thms HOL.sym[OF lambda_prs_l_b,simplified]} @{thm card1_suc_t} *} |
400 ML {* val card1_suc_t' = simp_lam_prs @{context} @{thm card1_suc_t} *} |
438 ML {* val card1_suc_t'' = eqsubst_thm @{context} @{thms HOL.sym[OF lambda_prs_l_b,simplified]} card1_suc_t' *} |
401 ML {* val ithm = simp_allex_prs @{context} quot card1_suc_t' *} |
439 ML {* val ithm = simp_allex_prs @{context} card1_suc_t'' *} |
|
440 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
402 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
441 ML {* val qthm = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} rthm *} |
403 ML {* val qthm = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} rthm *} |
442 ML {* ObjectLogic.rulify qthm *} |
404 ML {* ObjectLogic.rulify qthm *} |
443 |
405 |
444 thm fold1.simps(2) |
406 thm fold1.simps(2) |
466 |
428 |
467 ML {* val (g, thm, othm) = |
429 ML {* val (g, thm, othm) = |
468 Toplevel.program (fn () => |
430 Toplevel.program (fn () => |
469 repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
431 repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
470 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
432 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
471 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
433 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
472 ) |
434 ) |
473 *} |
435 *} |
474 ML {* |
436 ML {* |
475 fun tac2 ctxt = |
437 fun tac2 ctxt = |
476 (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm])) |
438 (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm])) |