509 DT ctxt "2" atac, |
509 DT ctxt "2" atac, |
510 DT ctxt "3" (rtac @{thm universal_twice}), |
510 DT ctxt "3" (rtac @{thm universal_twice}), |
511 DT ctxt "4" (rtac @{thm impI} THEN' atac), |
511 DT ctxt "4" (rtac @{thm impI} THEN' atac), |
512 DT ctxt "5" (rtac @{thm implication_twice}), |
512 DT ctxt "5" (rtac @{thm implication_twice}), |
513 DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0] |
513 DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0] |
514 [(@{thm equiv_res_forall} OF [rel_eqv]), |
514 [(@{thm ball_reg_eqv} OF [rel_eqv]), |
515 (@{thm equiv_res_exists} OF [rel_eqv])]), |
515 (@{thm ball_reg_eqv} OF [rel_eqv])]), |
516 (* For a = b \<longrightarrow> a \<approx> b *) |
516 (* For a = b \<longrightarrow> a \<approx> b *) |
517 DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl)), |
517 DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl)), |
518 DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
518 DT ctxt "8" (rtac @{thm ball_reg_right}) |
519 ]); |
519 ]); |
520 *} |
520 *} |
521 |
521 |
522 lemma move_forall: |
522 lemma move_forall: |
523 "(\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))" |
523 "(\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))" |
531 "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)" |
531 "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)" |
532 by blast |
532 by blast |
533 |
533 |
534 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P" |
534 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P" |
535 by auto |
535 by auto |
536 |
|
537 lemma ball_respects_refl: |
|
538 fixes P Q::"'a \<Rightarrow> bool" |
|
539 and x::"'a" |
|
540 assumes a: "EQUIV R2" |
|
541 and b: "\<And>f. Q (f x) \<longrightarrow> P (f x)" |
|
542 shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. Q (f x)) \<longrightarrow> All (\<lambda>f. P (f x)))" |
|
543 apply(rule impI) |
|
544 apply(rule allI) |
|
545 apply(drule_tac x="\<lambda>y. f x" in bspec) |
|
546 apply(simp add: Respects_def IN_RESPECTS) |
|
547 apply(rule impI) |
|
548 using a EQUIV_REFL_SYM_TRANS[of "R2"] |
|
549 apply(simp add: REFL_def) |
|
550 using b |
|
551 apply(simp) |
|
552 done |
|
553 |
|
554 lemma bex_respects_refl: |
|
555 fixes P Q::"'a \<Rightarrow> bool" |
|
556 and x::"'a" |
|
557 assumes a: "EQUIV R2" |
|
558 and b: "\<And>f. P (f x) \<longrightarrow> Q (f x)" |
|
559 shows "(Ex (\<lambda>f. P (f x))) \<longrightarrow> (Bex (Respects (R1 ===> R2)) (\<lambda>f. Q (f x)))" |
|
560 apply(rule impI) |
|
561 apply(erule exE) |
|
562 thm bexI |
|
563 apply(rule_tac x="\<lambda>y. f x" in bexI) |
|
564 using b |
|
565 apply(simp) |
|
566 apply(simp add: Respects_def IN_RESPECTS) |
|
567 apply(rule impI) |
|
568 using a EQUIV_REFL_SYM_TRANS[of "R2"] |
|
569 apply(simp add: REFL_def) |
|
570 done |
|
571 |
536 |
572 (* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *) |
537 (* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *) |
573 ML {* |
538 ML {* |
574 fun equiv_tac rel_eqvs = |
539 fun equiv_tac rel_eqvs = |
575 REPEAT_ALL_NEW (FIRST' |
540 REPEAT_ALL_NEW (FIRST' |
601 rtac @{thm move_forall}, |
567 rtac @{thm move_forall}, |
602 rtac @{thm move_exists}, |
568 rtac @{thm move_exists}, |
603 (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl))]) |
569 (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl))]) |
604 end |
570 end |
605 *} |
571 *} |
|
572 *) |
606 |
573 |
607 section {* Injections of REP and ABSes *} |
574 section {* Injections of REP and ABSes *} |
608 |
575 |
609 (* |
576 (* |
610 Injecting REPABS means: |
577 Injecting REPABS means: |
1013 in |
980 in |
1014 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
981 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
1015 end |
982 end |
1016 *} |
983 *} |
1017 |
984 |
|
985 (* Rewrites the term with LAMBDA_PRS thm. |
|
986 |
|
987 Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) |
|
988 with: f |
|
989 |
|
990 It proves the QUOTIENT assumptions by calling quotient_tac |
|
991 *) |
1018 ML {* |
992 ML {* |
1019 fun lambda_prs_conv1 ctxt quot_thms ctrm = |
993 fun lambda_prs_conv1 ctxt quot_thms ctrm = |
1020 case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) => |
994 case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) => |
1021 let |
995 let |
1022 val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1); |
996 val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1); |
1194 val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv |
1168 val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv |
1195 in |
1169 in |
1196 EVERY1 |
1170 EVERY1 |
1197 [rtac rule, |
1171 [rtac rule, |
1198 RANGE [rtac rthm', |
1172 RANGE [rtac rthm', |
1199 regularize_tac lthy rel_eqv rel_refl, |
1173 regularize_tac lthy (hd rel_eqv) rel_refl, (* temporary hd *) |
1200 REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), |
1174 REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), |
1201 clean_tac lthy quot defs aps]] |
1175 clean_tac lthy quot defs aps]] |
1202 end) lthy |
1176 end) lthy |
1203 *} |
1177 *} |
1204 |
1178 |