250 "op = ===> op \<approx> ===> op \<approx> op # op #" |
250 "op = ===> op \<approx> ===> op \<approx> op # op #" |
251 apply (simp add: FUN_REL.simps) |
251 apply (simp add: FUN_REL.simps) |
252 apply (metis cons_rsp) |
252 apply (metis cons_rsp) |
253 done |
253 done |
254 |
254 |
255 lemma append_respects_fst: |
255 lemma append_rsp_fst: |
256 assumes a : "list_eq l1 l2" |
256 assumes a : "list_eq l1 l2" |
257 shows "list_eq (l1 @ s) (l2 @ s)" |
257 shows "list_eq (l1 @ s) (l2 @ s)" |
258 using a |
258 using a |
259 apply(induct) |
259 apply(induct) |
260 apply(auto intro: list_eq.intros) |
260 apply(auto intro: list_eq.intros) |
261 apply(simp add: list_eq_refl) |
261 apply(rule list_eq_refl) |
262 done |
262 done |
|
263 |
|
264 lemma "(a @ b) \<approx> (b @ a)" |
|
265 sorry |
|
266 |
|
267 lemma (* ho_append_rsp: *) |
|
268 "op \<approx> ===> op \<approx> ===> op \<approx> op @ op @" |
|
269 sorry |
263 |
270 |
264 thm list.induct |
271 thm list.induct |
265 lemma list_induct_hol4: |
272 lemma list_induct_hol4: |
266 fixes P :: "'a list \<Rightarrow> bool" |
273 fixes P :: "'a list \<Rightarrow> bool" |
267 assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))" |
274 assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))" |
279 val g = build_regularize_goal thm rty rel lthy; |
286 val g = build_regularize_goal thm rty rel lthy; |
280 fun tac ctxt = |
287 fun tac ctxt = |
281 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
288 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
282 [(@{thm equiv_res_forall} OF [rel_eqv]), |
289 [(@{thm equiv_res_forall} OF [rel_eqv]), |
283 (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW |
290 (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW |
284 (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac])) ORELSE' |
291 (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN' |
285 (MetisTools.metis_tac ctxt [])); |
292 (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); |
286 val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1); |
293 val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1); |
287 in |
294 in |
288 cthm OF [thm] |
295 cthm OF [thm] |
289 end |
296 end |
290 *} |
297 *} |
386 ), |
393 ), |
387 WEAK_LAMBDA_RES_TAC ctxt |
394 WEAK_LAMBDA_RES_TAC ctxt |
388 ]) |
395 ]) |
389 *} |
396 *} |
390 |
397 |
391 ML Goal.prove |
|
392 |
|
393 ML {* |
398 ML {* |
394 fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = |
399 fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = |
395 let |
400 let |
396 val rt = build_repabs_term lthy thm constructors rty qty; |
401 val rt = build_repabs_term lthy thm constructors rty qty; |
397 val rg = Logic.mk_equals ((Thm.prop_of thm), rt); |
402 val rg = Logic.mk_equals ((Thm.prop_of thm), rt); |
467 val lam_prs = MetaSimplifier.rewrite_rule [@{thm id_apply2}] lpist |
472 val lam_prs = MetaSimplifier.rewrite_rule [@{thm id_apply2}] lpist |
468 *} |
473 *} |
469 |
474 |
470 text {* the proper way to do it *} |
475 text {* the proper way to do it *} |
471 ML {* |
476 ML {* |
|
477 fun findabs rty tm = |
|
478 case tm of |
|
479 Abs(_, T, b) => |
|
480 let |
|
481 val b' = subst_bound ((Free ("x", T)), b); |
|
482 val tys = findabs rty b' |
|
483 val ty = fastype_of tm |
|
484 in if needs_lift rty ty then (ty :: tys) else tys |
|
485 end |
|
486 | f $ a => (findabs rty f) @ (findabs rty a) |
|
487 | _ => [] |
|
488 *} |
|
489 |
|
490 ML {* findabs @{typ "'a list"} (prop_of (atomize_thm @{thm list_induct_hol4})) *} |
|
491 |
|
492 ML {* |
472 val lpi = Drule.instantiate' |
493 val lpi = Drule.instantiate' |
473 [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}, SOME @{ctyp "bool"}, SOME @{ctyp "bool"}] [] @{thm LAMBDA_PRS}; |
494 [SOME @{ctyp "'a list"}, NONE, SOME @{ctyp "bool"}, NONE] [] @{thm LAMBDA_PRS}; |
474 *} |
495 *} |
475 prove asdfasdf : {* concl_of lpi *} |
496 prove lambda_prs_l_b : {* concl_of lpi *} |
476 apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *}) |
497 apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *}) |
477 apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *}) |
498 apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *}) |
478 apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *}) |
499 apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *}) |
479 done |
500 done |
480 thm HOL.sym[OF asdfasdf,simplified] |
501 thm HOL.sym[OF lambda_prs_l_b,simplified] |
|
502 ML {* |
|
503 val lpi = Drule.instantiate' |
|
504 [SOME @{ctyp "'a list \<Rightarrow> bool"}, NONE, SOME @{ctyp "bool"}, NONE] [] @{thm LAMBDA_PRS}; |
|
505 *} |
|
506 prove lambda_prs_lb_b : {* concl_of lpi *} |
|
507 apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *}) |
|
508 apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *}) |
|
509 apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *}) |
|
510 done |
|
511 thm HOL.sym[OF lambda_prs_lb_b,simplified] |
481 |
512 |
482 ML {* |
513 ML {* |
483 fun eqsubst_thm ctxt thms thm = |
514 fun eqsubst_thm ctxt thms thm = |
484 let |
515 let |
485 val goalstate = Goal.init (Thm.cprop_of thm) |
516 val goalstate = Goal.init (Thm.cprop_of thm) |
492 in |
523 in |
493 Simplifier.rewrite_rule [rt] thm |
524 Simplifier.rewrite_rule [rt] thm |
494 end |
525 end |
495 *} |
526 *} |
496 |
527 |
497 (* @{thms HOL.sym[OF asdfasdf,simplified]} *) |
528 |
498 |
529 ML {* |
499 ML {* |
530 fun simp_lam_prs lthy thm = |
500 fun simp_lam_prs lthy thm = |
531 simp_lam_prs lthy (eqsubst_thm lthy |
501 simp_lam_prs lthy (eqsubst_thm lthy [lam_prs] thm) |
532 @{thms HOL.sym[OF lambda_prs_lb_b,simplified] HOL.sym[OF lambda_prs_l_b,simplified]} |
|
533 thm) |
502 handle _ => thm |
534 handle _ => thm |
503 *} |
535 *} |
504 |
536 |
505 ML {* val m2_t' = eqsubst_thm @{context} [lam_prs] @{thm m2_t} *} |
537 ML {* val m2_t' = eqsubst_thm @{context} [lam_prs] @{thm m2_t} *} |
506 |
538 |
542 apply (tactic {* rtac card1_suc_r 1 *}) |
574 apply (tactic {* rtac card1_suc_r 1 *}) |
543 done |
575 done |
544 |
576 |
545 |
577 |
546 ML {* val card1_suc_t_n = @{thm card1_suc_t} *} |
578 ML {* val card1_suc_t_n = @{thm card1_suc_t} *} |
547 ML {* val card1_suc_t' = eqsubst_thm @{context} @{thms HOL.sym[OF asdfasdf,simplified]} @{thm card1_suc_t} *} |
579 ML {* val card1_suc_t' = eqsubst_thm @{context} @{thms HOL.sym[OF lambda_prs_l_b,simplified]} @{thm card1_suc_t} *} |
548 ML {* val card1_suc_t'' = eqsubst_thm @{context} @{thms HOL.sym[OF asdfasdf,simplified]} card1_suc_t' *} |
580 ML {* val card1_suc_t'' = eqsubst_thm @{context} @{thms HOL.sym[OF lambda_prs_l_b,simplified]} card1_suc_t' *} |
549 ML {* val ithm = simp_allex_prs @{context} card1_suc_t'' *} |
581 ML {* val ithm = simp_allex_prs @{context} card1_suc_t'' *} |
550 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
582 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
551 ML {* val qthm = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} rthm *} |
583 ML {* val qthm = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} rthm *} |
552 ML {* ObjectLogic.rulify qthm *} |
584 ML {* ObjectLogic.rulify qthm *} |
553 |
585 |
554 thm fold1.simps(2) |
586 thm fold1.simps(2) |
555 thm list.recs(2) |
587 thm list.recs(2) |
556 |
588 |
557 ML {* val ind_r_a = atomize_thm @{thm m2} *} |
589 ML {* val ind_r_a = atomize_thm @{thm list_induct_hol4} *} |
558 (* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
590 (* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
559 apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq]) done *) |
591 ML_prf {* fun tac ctxt = |
560 |
592 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
|
593 [(@{thm equiv_res_forall} OF [@{thm equiv_list_eq}]), |
|
594 (@{thm equiv_res_exists} OF [@{thm equiv_list_eq}])])) THEN_ALL_NEW |
|
595 (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN' |
|
596 (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); *} |
|
597 apply (tactic {* tac @{context} 1 *}) *) |
561 ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *} |
598 ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *} |
562 ML {* |
599 ML {* |
563 val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
600 val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
564 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
601 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
565 *} |
602 *} |
588 *} |
625 *} |
589 ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *} |
626 ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *} |
590 ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l *} |
627 ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l *} |
591 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a *} |
628 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a *} |
592 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
629 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
|
630 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1" |
|
631 apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10) |
|
632 done |
593 |
633 |
594 ML {* |
634 ML {* |
595 fun lift thm = |
635 fun lift thm = |
596 let |
636 let |
597 val ind_r_a = atomize_thm thm; |
637 val ind_r_a = atomize_thm thm; |
612 |
652 |
613 ML {* lift @{thm m2} *} |
653 ML {* lift @{thm m2} *} |
614 ML {* lift @{thm m1} *} |
654 ML {* lift @{thm m1} *} |
615 ML {* lift @{thm list_eq.intros(4)} *} |
655 ML {* lift @{thm list_eq.intros(4)} *} |
616 ML {* lift @{thm list_eq.intros(5)} *} |
656 ML {* lift @{thm list_eq.intros(5)} *} |
617 (* ML {* lift @{thm length_append} *} *) |
657 ML {* lift @{thm card1_suc} *} |
|
658 (* ML {* lift @{thm append_assoc} *} *) |
618 |
659 |
619 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
660 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
620 notation ( output) "Trueprop" ("#_" [1000] 1000) |
661 notation ( output) "Trueprop" ("#_" [1000] 1000) |
621 |
662 |
622 ML {* |
663 ML {* |