--- a/LFex.thy Sat Nov 28 04:37:04 2009 +0100
+++ b/LFex.thy Sat Nov 28 04:37:30 2009 +0100
@@ -182,56 +182,48 @@
thm akind_aty_atrm.induct
-lemma left_ball_regular:
- assumes a: "EQUIV R"
- shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
-apply (rule LEFT_RES_FORALL_REGULAR)
-using Respects_def[of "R"] a EQUIV_REFL_SYM_TRANS[of "R"] REFL_def[of "R"]
-apply (simp)
-done
-
-lemma right_bex_regular:
- assumes a: "EQUIV R"
- shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
-apply (rule RIGHT_RES_EXISTS_REGULAR)
-using Respects_def[of "R"] a EQUIV_REFL_SYM_TRANS[of "R"] REFL_def[of "R"]
-apply (simp)
-done
-
-lemma ball_respects_refl:
- fixes P::"'a \<Rightarrow> bool"
- and x::"'a"
- assumes a: "EQUIV R2"
- shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
-apply(rule iffI)
-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)
-apply(simp)
-apply(simp)
-done
-
ML {*
-fun ball_simproc rel_eqvs ss redex =
+fun ball_reg_eqv_simproc rel_eqvs ss redex =
let
val ctxt = Simplifier.the_context ss
val thy = ProofContext.theory_of ctxt
in
case redex of
(ogl as ((Const (@{const_name "Ball"}, _)) $
- ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ P1)) =>
+ ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
+ (let
+ val gl = Const (@{const_name "EQUIV"}, dummyT) $ R;
+ val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
+ val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
+ val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]);
+(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
+ in
+ SOME thm
+ end
+ handle _ => NONE
+ )
+ | _ => NONE
+ end
+*}
+
+ML {*
+fun ball_reg_eqv_range_simproc rel_eqvs ss redex =
+ let
+ val ctxt = Simplifier.the_context ss
+ val thy = ProofContext.theory_of ctxt
+ in
+ case redex of
+ (ogl as ((Const (@{const_name "Ball"}, _)) $
+ ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>
(let
val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;
val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
val _ = tracing (Syntax.string_of_term ctxt glc);
val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
- val thm = (@{thm eq_reflection} OF [@{thm ball_respects_refl} OF [eqv]]);
- val R1c = cterm_of @{theory} R1;
+ val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]);
+ val R1c = cterm_of thy R1;
val thmi = Drule.instantiate' [] [SOME R1c] thm;
- val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi));
+(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *)
val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
val _ = tracing "AAA";
val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
@@ -249,26 +241,22 @@
ML {*
fun regularize_tac ctxt rel_eqvs =
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);
- val pat = [@{term "Ball (Respects (R1 ===> R2)) P"}];
+ val pat1 = [@{term "Ball (Respects R) P"}];
+ val pat2 = [@{term "Ball (Respects (R1 ===> R2)) P"}];
val thy = ProofContext.theory_of ctxt
- val simproc = Simplifier.simproc_i thy "" pat (K (ball_simproc rel_eqvs))
- in
- (ObjectLogic.full_atomize_tac) THEN'
- (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc])) THEN'
+ val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs))
+ val simproc2 = Simplifier.simproc_i thy "" pat2 (K (ball_reg_eqv_range_simproc rel_eqvs))
+ val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2]
+ in
+ ObjectLogic.full_atomize_tac THEN'
+ simp_tac simp_ctxt THEN'
REPEAT_ALL_NEW (FIRST' [
- (rtac @{thm RIGHT_RES_FORALL_REGULAR}),
- (rtac @{thm LEFT_RES_EXISTS_REGULAR}),
- (rtac @{thm left_ball_regular} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
- (rtac @{thm right_bex_regular} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
- (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
- (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
- (resolve_tac (Inductive.get_monos ctxt)),
+ rtac @{thm ball_reg_right},
+ rtac @{thm bex_reg_left},
+ resolve_tac (Inductive.get_monos ctxt),
rtac @{thm move_forall},
rtac @{thm move_exists},
- (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc]))
+ simp_tac simp_ctxt
])
end
*}
@@ -337,9 +325,6 @@
val te = @{thm eq_reflection} OF [t]
val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
val tl = Thm.lhs_of ts;
-(* val _ = rrrt := ts;
- val _ = rrr1 := ctrm;
- val _ = rrr2 := tl;*)
val (insp, inst) = make_inst (term_of tl) (term_of ctrm);
val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts;
(* val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
@@ -378,12 +363,6 @@
ML_prf {* val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot *}
ML_prf {* val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same *}
apply (tactic {* simp_tac ((Simplifier.context @{context} empty_ss) addsimps (meta_reps_same @ meta_lower)) 1 *})
-thm FORALL_PRS[symmetric]
-ML_prf {*
-fun allex_prs_tac lthy quot =
- (EqSubst.eqsubst_tac lthy [1] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
- THEN' (quotient_tac quot);
-*}
apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *}
ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *}
--- a/QuotMain.thy Sat Nov 28 04:37:04 2009 +0100
+++ b/QuotMain.thy Sat Nov 28 04:37:30 2009 +0100
@@ -511,11 +511,11 @@
DT ctxt "4" (rtac @{thm impI} THEN' atac),
DT ctxt "5" (rtac @{thm implication_twice}),
DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0]
- [(@{thm equiv_res_forall} OF [rel_eqv]),
- (@{thm equiv_res_exists} OF [rel_eqv])]),
+ [(@{thm ball_reg_eqv} OF [rel_eqv]),
+ (@{thm ball_reg_eqv} OF [rel_eqv])]),
(* For a = b \<longrightarrow> a \<approx> b *)
DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl)),
- DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR})
+ DT ctxt "8" (rtac @{thm ball_reg_right})
]);
*}
@@ -534,41 +534,6 @@
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 =
@@ -582,6 +547,7 @@
fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
*}
+(*
ML {*
fun regularize_tac ctxt rel_eqvs rel_refl =
let
@@ -603,6 +569,7 @@
(rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl))])
end
*}
+*)
section {* Injections of REP and ABSes *}
@@ -1015,6 +982,13 @@
end
*}
+(* Rewrites the term with LAMBDA_PRS thm.
+
+Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))
+ with: f
+
+It proves the QUOTIENT assumptions by calling quotient_tac
+ *)
ML {*
fun lambda_prs_conv1 ctxt quot_thms ctrm =
case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>
@@ -1196,7 +1170,7 @@
EVERY1
[rtac rule,
RANGE [rtac rthm',
- regularize_tac lthy rel_eqv rel_refl,
+ regularize_tac lthy (hd rel_eqv) rel_refl, (* temporary hd *)
REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
clean_tac lthy quot defs aps]]
end) lthy
--- a/QuotScript.thy Sat Nov 28 04:37:04 2009 +0100
+++ b/QuotScript.thy Sat Nov 28 04:37:30 2009 +0100
@@ -429,67 +429,96 @@
by (auto)
-(* TODO: Put the following lemmas in proper places *)
-lemma equiv_res_forall:
+(* Set of lemmas for regularisation of ball and bex *)
+lemma ball_reg_eqv:
+ fixes P :: "'a \<Rightarrow> bool"
+ assumes a: "EQUIV R"
+ shows "Ball (Respects R) P = (All P)"
+ by (metis EQUIV_def IN_RESPECTS a)
+
+lemma bex_reg_eqv:
fixes P :: "'a \<Rightarrow> bool"
- assumes a: "EQUIV E"
- shows "Ball (Respects E) P = (All P)"
- using a by (metis EQUIV_def IN_RESPECTS a)
+ assumes a: "EQUIV R"
+ shows "Bex (Respects R) P = (Ex P)"
+ by (metis EQUIV_def IN_RESPECTS a)
+
+lemma ball_reg_right:
+ assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
+ shows "All P \<longrightarrow> Ball R Q"
+ by (metis COMBC_def Collect_def Collect_mem_eq a)
+
+lemma bex_reg_left:
+ assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
+ shows "Bex R Q \<longrightarrow> Ex P"
+ by (metis COMBC_def Collect_def Collect_mem_eq a)
+
+lemma ball_reg_left:
+ assumes a: "EQUIV R"
+ shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
+ by (metis EQUIV_REFL IN_RESPECTS a)
-lemma equiv_res_exists:
- fixes P :: "'a \<Rightarrow> bool"
- assumes a: "EQUIV E"
- shows "Bex (Respects E) P = (Ex P)"
- using a by (metis EQUIV_def IN_RESPECTS a)
+lemma bex_reg_right:
+ assumes a: "EQUIV R"
+ shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
+ by (metis EQUIV_REFL IN_RESPECTS a)
-lemma FORALL_REGULAR:
+lemma ball_reg_eqv_range:
+ fixes P::"'a \<Rightarrow> bool"
+ and x::"'a"
+ assumes a: "EQUIV R2"
+ shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
+ apply(rule iffI)
+ 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)
+ apply(simp)
+ apply(simp)
+ done
+
+lemma bex_reg_eqv_range:
+ fixes P::"'a \<Rightarrow> bool"
+ and x::"'a"
+ assumes a: "EQUIV R2"
+ shows "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
+ apply(auto)
+ apply(rule_tac x="\<lambda>y. f x" in bexI)
+ 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
+
+lemma all_reg:
assumes a: "!x :: 'a. (P x --> Q x)"
and b: "All P"
shows "All Q"
using a b by (metis)
-lemma EXISTS_REGULAR:
+lemma ex_reg:
assumes a: "!x :: 'a. (P x --> Q x)"
and b: "Ex P"
shows "Ex Q"
using a b by (metis)
-lemma RES_FORALL_REGULAR:
+lemma ball_reg:
assumes a: "!x :: 'a. (R x --> P x --> Q x)"
and b: "Ball R P"
shows "Ball R Q"
using a b by (metis COMBC_def Collect_def Collect_mem_eq)
-lemma RES_EXISTS_REGULAR:
+lemma bex_reg:
assumes a: "!x :: 'a. (R x --> P x --> Q x)"
and b: "Bex R P"
shows "Bex R Q"
using a b by (metis COMBC_def Collect_def Collect_mem_eq)
-lemma LEFT_RES_FORALL_REGULAR:
- assumes a: "\<And>x. (R x \<and> (Q x \<longrightarrow> P x))"
- shows "Ball R Q \<longrightarrow> All P"
- using a
- apply (metis COMBC_def Collect_def Collect_mem_eq a)
- done
-lemma RIGHT_RES_FORALL_REGULAR:
- assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
- shows "All P \<longrightarrow> Ball R Q"
- using a
- apply (metis COMBC_def Collect_def Collect_mem_eq a)
- done
-lemma LEFT_RES_EXISTS_REGULAR:
- assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
- shows "Bex R Q \<longrightarrow> Ex P"
- using a by (metis COMBC_def Collect_def Collect_mem_eq)
-
-lemma RIGHT_RES_EXISTS_REGULAR:
- assumes a: "\<And>x. (R x \<and> (P x \<longrightarrow> Q x))"
- shows "Ex P \<longrightarrow> Bex R Q"
- using a by (metis COMBC_def Collect_def Collect_mem_eq)
(* TODO: Add similar *)
lemma RES_FORALL_RSP: