--- a/QuotMain.thy Thu Nov 26 19:51:31 2009 +0100
+++ b/QuotMain.thy Thu Nov 26 20:32:33 2009 +0100
@@ -474,41 +474,6 @@
*)
-lemma my_equiv_res_forallR:
- fixes P::"'a \<Rightarrow> bool"
- fixes Q::"'b \<Rightarrow> bool"
- assumes b: "(All Q) \<longrightarrow> (All P)"
- shows "(All Q) \<longrightarrow> Ball (Respects E) P"
-using b by auto
-
-lemma my_equiv_res_forallL:
- fixes P::"'a \<Rightarrow> bool"
- fixes Q::"'b \<Rightarrow> bool"
- assumes a: "EQUIV E"
- assumes b: "(All Q) \<longrightarrow> (All P)"
- shows "Ball (Respects E) P \<longrightarrow> (All P)"
-using a b
-unfolding EQUIV_def
-by (metis IN_RESPECTS)
-
-lemma my_equiv_res_existsR:
- fixes P::"'a \<Rightarrow> bool"
- fixes Q::"'b \<Rightarrow> bool"
- assumes a: "EQUIV E"
- and b: "(Ex Q) \<longrightarrow> (Ex P)"
- shows "(Ex Q) \<longrightarrow> Bex (Respects E) P"
-using a b
-unfolding EQUIV_def
-by (metis IN_RESPECTS)
-
-lemma my_equiv_res_existsL:
- fixes P::"'a \<Rightarrow> bool"
- fixes Q::"'b \<Rightarrow> bool"
- assumes b: "(Ex Q) \<longrightarrow> (Ex P)"
- shows "Bex (Respects E) Q \<longrightarrow> (Ex P)"
-using b
-by (auto)
-
lemma universal_twice:
assumes *: "\<And>x. (P x \<longrightarrow> Q x)"
shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
@@ -531,49 +496,15 @@
in
Seq.single thm
end
-
+
fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))]
*}
ML {*
-fun REGULARIZE_tac' lthy rel_refl rel_eqv =
- (REPEAT1 o FIRST1)
- [(K (print_tac "start")) THEN' (K no_tac),
- DT lthy "1" (rtac rel_refl),
- DT lthy "2" atac,
- DT lthy "3" (rtac @{thm universal_twice}),
- DT lthy "4" (rtac @{thm impI} THEN' atac),
- DT lthy "5" (rtac @{thm implication_twice}),
- DT lthy "6" (rtac @{thm my_equiv_res_forallR}),
- DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_existsR})),
- (* For a = b \<longrightarrow> a \<approx> b *)
- DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
- DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})]
-*}
-
-ML {*
fun regularize_tac ctxt rel_eqv rel_refl =
(ObjectLogic.full_atomize_tac) THEN'
- REPEAT_ALL_NEW (FIRST' [
- rtac rel_refl,
- atac,
- rtac @{thm universal_twice},
- rtac @{thm impI} THEN' atac,
- rtac @{thm implication_twice},
- EqSubst.eqsubst_tac ctxt [0]
- [(@{thm equiv_res_forall} OF [rel_eqv]),
- (@{thm equiv_res_exists} OF [rel_eqv])],
- (* For a = b \<longrightarrow> a \<approx> b *)
- (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
- (rtac @{thm RIGHT_RES_FORALL_REGULAR})
- ]);
-*}
-
-ML {*
-fun regularize_tac ctxt rel_eqv rel_refl =
- (ObjectLogic.full_atomize_tac) THEN'
- REPEAT_ALL_NEW (FIRST'
- [(K (print_tac "start")) THEN' (K no_tac),
+ REPEAT_ALL_NEW (FIRST'
+ [(K (print_tac "start")) THEN' (K no_tac),
DT ctxt "1" (rtac rel_refl),
DT ctxt "2" atac,
DT ctxt "3" (rtac @{thm universal_twice}),
@@ -588,7 +519,89 @@
]);
*}
-thm RIGHT_RES_FORALL_REGULAR
+lemma move_forall: "(\<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))"
+by auto
+
+lemma move_exists: "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))"
+by auto
+
+lemma [mono]: "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"
+by blast
+
+lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
+by auto
+
+lemma ball_respects_refl:
+ fixes P Q::"'a \<Rightarrow> bool"
+ and x::"'a"
+ assumes a: "EQUIV R2"
+ and b: "\<And>f. Q (f x) \<longrightarrow> P (f x)"
+ shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. Q (f x)) \<longrightarrow> All (\<lambda>f. P (f x)))"
+apply(rule impI)
+apply(rule allI)
+apply(drule_tac x="\<lambda>y. f x" in bspec)
+apply(simp add: Respects_def IN_RESPECTS)
+apply(rule impI)
+using a EQUIV_REFL_SYM_TRANS[of "R2"]
+apply(simp add: REFL_def)
+using b
+apply(simp)
+done
+
+lemma bex_respects_refl:
+ fixes P Q::"'a \<Rightarrow> bool"
+ and x::"'a"
+ assumes a: "EQUIV R2"
+ and b: "\<And>f. P (f x) \<longrightarrow> Q (f x)"
+ shows "(Ex (\<lambda>f. P (f x))) \<longrightarrow> (Bex (Respects (R1 ===> R2)) (\<lambda>f. Q (f x)))"
+apply(rule impI)
+apply(erule exE)
+thm bexI
+apply(rule_tac x="\<lambda>y. f x" in bexI)
+using b
+apply(simp)
+apply(simp add: Respects_def IN_RESPECTS)
+apply(rule impI)
+using a EQUIV_REFL_SYM_TRANS[of "R2"]
+apply(simp add: REFL_def)
+done
+
+(* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *)
+ML {*
+fun equiv_tac rel_eqvs =
+ REPEAT_ALL_NEW(FIRST' [
+ FIRST' (map rtac rel_eqvs),
+ rtac @{thm IDENTITY_EQUIV},
+ rtac @{thm LIST_EQUIV}
+ ])
+*}
+
+ML {*
+fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+*}
+
+ML {*
+fun regularize_tac ctxt rel_eqvs rel_refl =
+ let
+ val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) rel_eqvs
+ val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) rel_eqvs
+ val subs = map (fn x => @{thm eq_reflection} OF [x]) (subs1 @ subs2)
+ in
+ (ObjectLogic.full_atomize_tac) THEN'
+ (simp_tac ((Simplifier.context ctxt empty_ss) addsimps subs))
+ THEN'
+ REPEAT_ALL_NEW (FIRST' [
+ (rtac @{thm RIGHT_RES_FORALL_REGULAR}),
+ (rtac @{thm LEFT_RES_EXISTS_REGULAR}),
+ (resolve_tac (Inductive.get_monos ctxt)),
+ (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
+ (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
+ rtac @{thm move_forall},
+ rtac @{thm move_exists},
+ (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl)
+ ])
+ end
+*}
section {* Injections of REP and ABSes *}
@@ -808,10 +821,6 @@
*}
ML {*
-fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
-*}
-
-ML {*
fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
(FIRST' [
rtac trans_thm,
@@ -1285,7 +1294,7 @@
in
rtac rule THEN' RANGE [
rtac rthm',
- regularize_tac lthy rel_eqv rel_refl,
+ regularize_tac lthy [rel_eqv] rel_refl,
REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
clean_tac lthy quot defs reps_same absrep aps
]