--- a/QuotMain.thy Mon Dec 07 01:28:10 2009 +0100
+++ b/QuotMain.thy Mon Dec 07 02:34:24 2009 +0100
@@ -494,21 +494,6 @@
raise (LIFT_MATCH "regularize (default)")
*}
-(*
-FIXME / TODO: needs to be adapted
-
-To prove that the raw theorem implies the regularised one,
-we try in order:
-
- - Reflexivity of the relation
- - Assumption
- - Elimnating quantifiers on both sides of toplevel implication
- - Simplifying implications on both sides of toplevel implication
- - Ball (Respects ?E) ?P = All ?P
- - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
-
-*)
-
ML {*
fun equiv_tac ctxt =
REPEAT_ALL_NEW (FIRST'
@@ -541,94 +526,74 @@
*}
ML {*
-fun ball_reg_eqv_range_simproc 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 "equivp"}, 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 {context,...} => equiv_tac context 1)
- 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 inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
- val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
-(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); *)
- in
- SOME thm2
- end
- handle _ => NONE
-
- )
- | _ => NONE
- end
+fun calculate_instance ctxt thm redex R1 R2 =
+let
+ val thy = ProofContext.theory_of ctxt
+ val goal = Const (@{const_name "equivp"}, dummyT) $ R2
+ |> Syntax.check_term ctxt
+ |> HOLogic.mk_Trueprop
+ val eqv_prem = Goal.prove ctxt [] [] goal (fn {context,...} => equiv_tac context 1)
+ val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]])
+ val R1c = cterm_of thy R1
+ val thmi = Drule.instantiate' [] [SOME R1c] thm
+ val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex
+ val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi)
+in
+ SOME thm2
+end
+handle _ => NONE
+(* FIXME/TODO: what is the place where the exception can be raised: matching_prs? *)
*}
-
-thm bex_reg_eqv_range
-thm ball_reg_eqv
-thm bex_reg_eqv
-
ML {*
-fun bex_reg_eqv_range_simproc ss redex =
- let
- val ctxt = Simplifier.the_context ss
- val thy = ProofContext.theory_of ctxt
- in
- case redex of
- (ogl as ((Const (@{const_name "Bex"}, _)) $
- ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) =>
- (let
- val gl = Const (@{const_name "equivp"}, 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 {context,...} => equiv_tac context 1)
- val thm = (@{thm eq_reflection} OF [@{thm bex_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 inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
- val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
-(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));*)
- in
- SOME thm2
- end
- handle _ => NONE
-
- )
+fun ball_bex_range_simproc ss redex =
+let
+ val ctxt = Simplifier.the_context ss
+in
+ case redex of
+ (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
+ (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
+ calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2
+ | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
+ (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
+ calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2
| _ => NONE
- end
+end
*}
-lemma eq_imp_rel: "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
+lemma eq_imp_rel:
+ shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
by (simp add: equivp_reflp)
+(* FIXME/TODO: How does regularizing work? *)
+(* FIXME/TODO: needs to be adapted
+
+To prove that the raw theorem implies the regularised one,
+we try in order:
+
+ - Reflexivity of the relation
+ - Assumption
+ - Elimnating quantifiers on both sides of toplevel implication
+ - Simplifying implications on both sides of toplevel implication
+ - Ball (Respects ?E) ?P = All ?P
+ - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
+
+*)
ML {*
fun regularize_tac ctxt =
- let
- val pat1 = [@{term "Ball (Respects R) P"}];
- val pat2 = [@{term "Bex (Respects R) P"}];
- val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}];
- val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}];
- val thy = ProofContext.theory_of ctxt
- val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc))
- val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc))
- val simp_set = (mk_minimal_ss ctxt)
+let
+ val thy = ProofContext.theory_of ctxt
+ val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"}
+ val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"}
+ val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc))
+ val simpset = (mk_minimal_ss ctxt)
addsimps @{thms ball_reg_eqv bex_reg_eqv}
- addsimprocs [simproc3, simproc4]
- addSolver equiv_solver
- (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
- val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
- in
+ addsimprocs [simproc] addSolver equiv_solver
+ (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
+ val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
+in
ObjectLogic.full_atomize_tac THEN'
- simp_tac simp_set THEN'
+ simp_tac simpset THEN'
REPEAT_ALL_NEW (FIRST' [
rtac @{thm ball_reg_right},
rtac @{thm bex_reg_left},
@@ -636,9 +601,8 @@
rtac @{thm ball_all_comm},
rtac @{thm bex_ex_comm},
resolve_tac eq_eqvs,
- simp_tac simp_set
- ])
- end
+ simp_tac simpset])
+end
*}
section {* Injections of rep and abses *}