--- a/QuotMain.thy Wed Nov 25 14:15:34 2009 +0100
+++ b/QuotMain.thy Wed Nov 25 14:16:33 2009 +0100
@@ -604,8 +604,28 @@
ML {*
-(* builds the relation for respects *)
+(*
+Regularizing an rtrm means:
+ - quantifiers over a type that needs lifting are replaced by
+ bounded quantifiers, for example:
+ \<forall>x. P \<Longrightarrow> \<forall>x \<in> (Respects R). P / All (Respects R) P
+
+ the relation R is given by the rty and qty;
+ - abstractions over a type that needs lifting are replaced
+ by bounded abstractions:
+ \<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P)
+
+ - equalities over the type being lifted are replaced by
+ corresponding relations:
+ A = B \<Longrightarrow> A \<approx> B
+
+ example with more complicated types of A, B:
+ A = B \<Longrightarrow> (op = \<Longrightarrow> op \<approx>) A B
+*)
+
+
+(* builds the relation that is the argument of respects *)
fun mk_resp_arg lthy (rty, qty) =
let
val thy = ProofContext.theory_of lthy
@@ -660,26 +680,6 @@
fun qnt_typ ty = domain_type (domain_type ty)
*}
-(*
-Regularizing an rtrm means:
- - quantifiers over a type that needs lifting are replaced by
- bounded quantifiers, for example:
- \<forall>x. P \<Longrightarrow> \<forall>x \<in> (Respects R). P / All (Respects R) P
-
- the relation R is given by the rty and qty;
-
- - abstractions over a type that needs lifting are replaced
- by bounded abstractions:
- \<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P)
-
- - equalities over the type being lifted are replaced by
- corresponding relations:
- A = B \<Longrightarrow> A \<approx> B
-
- example with more complicated types of A, B:
- A = B \<Longrightarrow> (op = \<Longrightarrow> op \<approx>) A B
-*)
-
ML {*
(* produces a regularized version of rtm *)
(* - the result is still not completely typed *)
@@ -746,8 +746,8 @@
*}
(*
-To prove that the old theorem implies the new one, we first
-atomize it and then try:
+To prove that the raw theorem implies the regularised one,
+we try in order:
- Reflexivity of the relation
- Assumption
@@ -835,16 +835,28 @@
*}
ML {*
-fun REGULARIZE_prove rtrm qtrm rel_eqv rel_refl lthy =
- let
- val goal = mk_REGULARIZE_goal lthy rtrm qtrm
- in
- Goal.prove lthy [] [] goal
- (fn {context, ...} => REGULARIZE_tac' context rel_refl rel_eqv)
- end
+fun regularize_tac ctxt rel_eqv rel_refl =
+ (ObjectLogic.full_atomize_tac) THEN'
+ REPEAT_ALL_NEW (FIRST' [
+ rtac rel_refl,
+ atac,
+ rtac @{thm universal_twice},
+ (rtac @{thm impI} THEN' atac),
+ rtac @{thm implication_twice},
+ EqSubst.eqsubst_tac ctxt [0]
+ [(@{thm equiv_res_forall} OF [rel_eqv]),
+ (@{thm equiv_res_exists} OF [rel_eqv])],
+ (* For a = b \<longrightarrow> a \<approx> b *)
+ (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
+ (rtac @{thm RIGHT_RES_FORALL_REGULAR})
+ ]);
*}
+
(*
+Injections of REP and Abses
+***************************
+
Injecting REPABS means:
For abstractions:
@@ -866,15 +878,12 @@
* Otherwise just recurse.
*)
-(* rep-abs injection *)
-
ML {*
fun mk_repabs lthy (T, T') trm =
Quotient_Def.get_fun repF lthy (T, T')
$ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
*}
-
ML {*
(* bound variables need to be treated properly, *)
(* as the type of subterms need to be calculated *)
@@ -939,35 +948,7 @@
*}
-
-(*
-To prove that the old theorem implies the new one, we first
-atomize it and then try:
- - 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 rel_eqv rel_refl =
- (ObjectLogic.full_atomize_tac) THEN'
- REPEAT_ALL_NEW (FIRST' [
- rtac rel_refl,
- atac,
- rtac @{thm universal_twice},
- (rtac @{thm impI} THEN' atac),
- rtac @{thm implication_twice},
- EqSubst.eqsubst_tac ctxt [0]
- [(@{thm equiv_res_forall} OF [rel_eqv]),
- (@{thm equiv_res_exists} OF [rel_eqv])],
- (* For a = b \<longrightarrow> a \<approx> b *)
- (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
- (rtac @{thm RIGHT_RES_FORALL_REGULAR})
- ]);
-*}
+(* Genralisation of free variables in a goal *)
ML {*
fun inst_spec ctrm =
@@ -999,6 +980,18 @@
end)
*}
+(* General outline of the lifting procedure *)
+(* **************************************** *)
+(* *)
+(* - A is the original raw theorem *)
+(* - B is the regularized theorem *)
+(* - C is the rep/abs injected version of B *)
+(* - D is the lifted theorem *)
+(* *)
+(* - b is the regularization step *)
+(* - c is the rep/abs injection step *)
+(* - d is the cleaning part *)
+
lemma procedure:
assumes a: "A"
and b: "A \<Longrightarrow> B"
@@ -1026,10 +1019,12 @@
val thy = ProofContext.theory_of ctxt
val rtrm' = HOLogic.dest_Trueprop rtrm
val qtrm' = HOLogic.dest_Trueprop qtrm
- val reg_goal = Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm')
- handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
- val inj_goal = Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm'))
- handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
+ val reg_goal =
+ Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm')
+ handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
+ val inj_goal =
+ Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm'))
+ handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
in
Drule.instantiate' []
[SOME (cterm_of thy rtrm'),