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: |
1204 val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv |
1171 val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv |
1205 in |
1172 in |
1206 EVERY1 |
1173 EVERY1 |
1207 [rtac rule, |
1174 [rtac rule, |
1208 RANGE [rtac rthm', |
1175 RANGE [rtac rthm', |
1209 regularize_tac lthy rel_eqv rel_refl, |
1176 regularize_tac lthy (hd rel_eqv) rel_refl, (* temporary hd *) |
1210 REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), |
1177 REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), |
1211 clean_tac lthy quot defs aps]] |
1178 clean_tac lthy quot defs aps]] |
1212 end) lthy |
1179 end) lthy |
1213 *} |
1180 *} |
1214 |
1181 |