--- a/LFex.thy Sat Nov 28 03:17:22 2009 +0100
+++ b/LFex.thy Sat Nov 28 04:02:54 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 *}