--- a/QuotMain.thy Fri Dec 04 14:11:20 2009 +0100
+++ b/QuotMain.thy Fri Dec 04 14:35:36 2009 +0100
@@ -776,58 +776,6 @@
end
*}
-ML {*
-val APPLY_RSP_TAC =
- Subgoal.FOCUS (fn {concl, asms, context,...} =>
- case ((HOLogic.dest_Trueprop (term_of concl))) of
- ((R2 $ (f $ x) $ (g $ y))) =>
- let
- val (asmf, asma) = find_qt_asm (map term_of asms);
- in
- if (fastype_of asmf) = (fastype_of f) then no_tac else let
- val ty_a = fastype_of x;
- val ty_b = fastype_of asma;
- val ty_c = range_type (type_of f);
- val ty_d = range_type (type_of asmf);
- val thy = ProofContext.theory_of context;
- val ty_inst = map (fn x => SOME (ctyp_of thy x)) [ty_a, ty_b, ty_c, ty_d];
- val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y];
- val t_inst = [NONE, NONE, NONE, SOME R2, NONE, NONE, SOME f, SOME g, SOME x, SOME y];
- val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP}
- val _ = tracing ("instantiated rule" ^ Syntax.string_of_term @{context} (prop_of thm))
- in
- rtac thm 1
- end
- end
- | _ => no_tac)
-*}
-
-ML {*
-val APPLY_RSP1_TAC =
- Subgoal.FOCUS (fn {concl, asms, context,...} =>
- case ((HOLogic.dest_Trueprop (term_of concl))) of
- ((R2 $ (f $ x) $ (g $ y))) =>
- let
- val (asmf, asma) = find_qt_asm (map term_of asms);
- in
- if (fastype_of asmf) = (fastype_of f) then no_tac else let
- val ty_a = fastype_of x;
- val ty_b = fastype_of asma;
- val ty_c = range_type (type_of f);
-(* val ty_d = range_type (type_of asmf);*)
- val thy = ProofContext.theory_of context;
- val ty_inst = map (fn x => SOME (ctyp_of thy x)) [ty_a, ty_b, ty_c];
- val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y];
- val t_inst = [NONE, NONE, NONE, SOME R2, SOME f, SOME g, SOME x, SOME y];
- val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP1}
- (*val _ = tracing (Syntax.string_of_term @{context} (prop_of thm))*)
- in
- rtac thm 1
- end
- end
- | _ => no_tac)
-*}
-
(* It proves the QUOTIENT assumptions by calling quotient_tac *)
ML {*
fun solve_quotient_assum i ctxt thm =
@@ -851,7 +799,7 @@
*}
ML {*
-val APPLY_RSP1_TAC' =
+val apply_rsp_tac =
Subgoal.FOCUS (fn {concl, asms, context,...} =>
case ((HOLogic.dest_Trueprop (term_of concl))) of
((R2 $ (f $ x) $ (g $ y))) =>
@@ -864,7 +812,7 @@
val ty_c = range_type (type_of f);
val thy = ProofContext.theory_of context;
val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c];
- val thm = Drule.instantiate' ty_inst [] @{thm APPLY_RSP1}
+ val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp}
val te = solve_quotient_assums context thm
val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
val thm = Drule.instantiate' [] t_inst te
@@ -1027,8 +975,8 @@
fun inj_repabs_tac ctxt rel_refl trans2 =
(FIRST' [
inj_repabs_tac_match ctxt trans2,
- (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *)
- NDT ctxt "A" (APPLY_RSP1_TAC' ctxt THEN'
+ (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp provided type of t needs lifting *)
+ NDT ctxt "A" (apply_rsp_tac ctxt THEN'
(RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
(* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *)
(* merge with previous tactic *)
@@ -1055,15 +1003,6 @@
section {* Cleaning of the theorem *}
-
-(* TODO: This is slow *)
-(*
-ML {*
-fun allex_prs_tac ctxt =
- (EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt)
-*}
-*)
-
ML {*
fun make_inst lhs t =
let
@@ -1089,7 +1028,7 @@
val thy = ProofContext.theory_of ctxt;
val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
- val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS};
+ val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs};
val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
val tl = Thm.lhs_of ts;
@@ -1140,10 +1079,10 @@
Cleaning the theorem consists of 6 kinds of rewrites.
The first two need to be done before fun_map is unfolded
- - LAMBDA_PRS:
+ - lambda_prs:
(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f
- - FORALL_PRS (and the same for exists: EXISTS_PRS)
+ - all_prs (and the same for exists: ex_prs)
\<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f
- Rewriting with definitions from the argument defs
@@ -1300,7 +1239,7 @@
val rule = procedure_inst context (prop_of rthm') (term_of concl)
val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv
val quotients = quotient_rules_get lthy
- val trans2 = map (fn x => @{thm EQUALS_RSP} OF [x]) quotients
+ val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients
val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i}
in
EVERY1
--- a/QuotScript.thy Fri Dec 04 14:11:20 2009 +0100
+++ b/QuotScript.thy Fri Dec 04 14:35:36 2009 +0100
@@ -266,14 +266,14 @@
shows "(x = y) = R (Rep x) (Rep y)"
by (rule QUOTIENT_REL_REP[OF q, symmetric])
-lemma EQUALS_RSP:
+lemma equals_rsp:
assumes q: "QUOTIENT R Abs Rep"
and a: "R xa xb" "R ya yb"
shows "R xa ya = R xb yb"
using QUOTIENT_SYM[OF q] QUOTIENT_TRANS[OF q] unfolding SYM_def TRANS_def
using a by blast
-lemma LAMBDA_PRS:
+lemma lambda_prs:
assumes q1: "QUOTIENT R1 Abs1 Rep1"
and q2: "QUOTIENT R2 Abs2 Rep2"
shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
@@ -281,10 +281,10 @@
using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]
by simp
-lemma LAMBDA_PRS1:
+lemma lambda_prs1:
assumes q1: "QUOTIENT R1 Abs1 Rep1"
and q2: "QUOTIENT R2 Abs2 Rep2"
- shows "(\<lambda>x. f x) = (Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x)"
+ shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
unfolding expand_fun_eq
using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]
by simp
@@ -334,7 +334,7 @@
(* ----------------------------------------------------- *)
(* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *)
-(* RES_FORALL, RES_EXISTS, RES_EXISTS_EQUIV *)
+(* Ball, Bex, RES_EXISTS_EQUIV *)
(* ----------------------------------------------------- *)
(* bool theory: COND, LET *)
@@ -374,32 +374,24 @@
(* FUNCTION APPLICATION *)
+(* Not used *)
lemma APPLY_PRS:
assumes q1: "QUOTIENT R1 Abs1 Rep1"
and q2: "QUOTIENT R2 Abs2 Rep2"
shows "f x = Abs2 (((Abs1 ---> Rep2) f) (Rep1 x))"
using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto
-(* ask peter: no use of q1 q2 *)
-(* Cez: I can answer,
- In the following theorem R2 can be instantiated with anything,
+(* In the following theorem R1 can be instantiated with anything,
but we know some of the types of the Rep and Abs functions;
so by solving QUOTIENT assumptions we can get a unique R2 that
- will be provable; which is why we need to use APPLY_RSP1 *)
-lemma APPLY_RSP:
- assumes q1: "QUOTIENT R1 Abs1 Rep1"
- and q2: "QUOTIENT R2 Abs2 Rep2"
- and a: "(R1 ===> R2) f g" "R1 x y"
- shows "R2 (f x) (g y)"
-using a by (rule FUN_REL_IMP)
-
-lemma APPLY_RSP1:
+ will be provable; which is why we need to use APPLY_RSP *)
+lemma apply_rsp:
assumes q: "QUOTIENT R1 Abs1 Rep1"
and a: "(R1 ===> R2) f g" "R1 x y"
shows "R2 ((f::'a\<Rightarrow>'c) x) ((g::'a\<Rightarrow>'c) y)"
using a by (rule FUN_REL_IMP)
-lemma APPLY_RSP2:
+lemma apply_rsp':
assumes a: "(R1 ===> R2) f g" "R1 x y"
shows "R2 (f x) (g y)"
using a by (rule FUN_REL_IMP)