--- a/QuotMain.thy Mon Dec 07 04:39:42 2009 +0100
+++ b/QuotMain.thy Mon Dec 07 04:41:42 2009 +0100
@@ -170,11 +170,24 @@
(* lifting of constants *)
use "quotient_def.ML"
+section {* Bounded abstraction *}
+
definition
Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
where
"(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
+section {* Simset setup *}
+
+(* since HOL_basic_ss is too "big", we need to set up *)
+(* our own minimal simpset *)
+ML {*
+fun mk_minimal_ss ctxt =
+ Simplifier.context ctxt empty_ss
+ setsubgoaler asm_simp_tac
+ setmksimps (mksimps [])
+*}
+
section {* atomize *}
lemma atomize_eqv[atomize]:
@@ -481,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'
@@ -508,54 +506,6 @@
*}
ML {*
-fun ball_reg_eqv_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"}, _)) $ R) $ P1)) =>
- (let
- val gl = Const (@{const_name "equivp"}, dummyT) $ R;
- val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
- val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 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 bex_reg_eqv_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"}, _)) $ R) $ P1)) =>
- (let
- val gl = Const (@{const_name "equivp"}, dummyT) $ R;
- val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
- val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1)
- val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]);
-(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
- in
- SOME thm
- end
- handle _ => NONE
- )
- | _ => NONE
- end
-*}
-
-ML {*
fun prep_trm thy (x, (T, t)) =
(cterm_of thy (Var (x, T)), cterm_of thy t)
@@ -576,96 +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)
-(* does not work yet
+(* 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 simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc))
- val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc))
- 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 = HOL_basic_ss 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
+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 [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},
@@ -673,37 +601,7 @@
rtac @{thm ball_all_comm},
rtac @{thm bex_ex_comm},
resolve_tac eq_eqvs,
- simp_tac simp_set
- ])
- end
-*}*)
-
-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 simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc))
- val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc))
- 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_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4]
- (* 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_ctxt THEN'
- REPEAT_ALL_NEW (FIRST' [
- rtac @{thm ball_reg_right},
- rtac @{thm bex_reg_left},
- resolve_tac (Inductive.get_monos ctxt),
- rtac @{thm ball_all_comm},
- rtac @{thm bex_ex_comm},
- resolve_tac eq_eqvs,
- simp_tac simp_ctxt])
+ simp_tac simpset])
end
*}
@@ -1083,7 +981,7 @@
ML {*
fun lambda_prs_simple_conv ctxt ctrm =
case (term_of ctrm) of
- ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
+ ((Const (@{const_name fun_map}, _) $ r1 $ (a2 as (Const (s,_)))) $ (Abs _)) =>
let
val thy = ProofContext.theory_of ctxt
val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
@@ -1096,9 +994,14 @@
val tl = Thm.lhs_of ts
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 _ = tracing "lambda_prs"
- val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)))
- val _ = tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))*)
+ val _ = if not (s = @{const_name "id"}) then
+ (tracing "lambda_prs";
+ tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
+ tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi)));
+ tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
+ tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts)));
+ tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti))))
+ else ()
in
Conv.rewr_conv ti ctrm
end
@@ -1145,8 +1048,7 @@
val thms1 = @{thms all_prs ex_prs} @ defs
val thms2 = @{thms eq_reflection[OF fun_map.simps]}
@ @{thms id_simps Quotient_abs_rep Quotient_rel_rep}
- fun simps thms = HOL_basic_ss addsimps thms addSolver quotient_solver
- (* FIXME: use of someting smaller than HOL_basic_ss *)
+ fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
in
EVERY' [lambda_prs_tac lthy,
simp_tac (simps thms1),