--- a/QuotMain.thy Mon Nov 09 15:40:43 2009 +0100
+++ b/QuotMain.thy Tue Nov 10 09:32:16 2009 +0100
@@ -202,7 +202,7 @@
bounded quantifiers, for example:
\<forall>x. P \<Longrightarrow> \<forall>x\<in>(Respects R). P
- Abstractions over a type that needs lifting are replaced
- by bounded abstactions:
+ by bounded abstractions:
\<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P)
- Equalities over the type being lifted are replaced by
@@ -241,7 +241,8 @@
val tys_out = tys_rel ---> ty_out;
in
(case (maps_lookup (ProofContext.theory_of lthy) s) of
- SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys)
+ SOME (info) => list_comb (Const (#relfun info, tys_out),
+ map (fn ty => tyRel ty rty rel lthy) tys)
| NONE => HOLogic.eq_const ty
)
end
@@ -341,12 +342,12 @@
(*
ML {*
- text {*val r = term_of @{cpat "R::?'a list \<Rightarrow> ?'a list \<Rightarrow> bool"};*}
val r = Free ("R", dummyT);
- val t = (my_reg @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"});
+ val t = (my_reg_inst @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"});
val t2 = Syntax.check_term @{context} t;
- Toplevel.program (fn () => cterm_of @{theory} t2)
-*}*)
+ cterm_of @{theory} t2
+*}
+*)
text {* Assumes that the given theorem is atomized *}
ML {*
@@ -356,17 +357,16 @@
(my_reg_inst lthy rel rty (prop_of thm)))
*}
-lemma universal_twice:
- "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"
-by auto
+lemma universal_twice:
+ assumes *: "\<And>x. (P x \<longrightarrow> Q x)"
+ shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
+using * by auto
-lemma implication_twice:
- "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
-by auto
-
-(*lemma equality_twice:
- "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"
-by auto*)
+lemma implication_twice:
+ assumes a: "c \<longrightarrow> a"
+ assumes b: "a \<Longrightarrow> b \<longrightarrow> d"
+ shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
+using a b by auto
ML {*
fun regularize thm rty rel rel_eqv rel_refl lthy =
@@ -383,6 +383,7 @@
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})
]);
@@ -396,7 +397,12 @@
section {* RepAbs injection *}
(*
-Injecting RepAbs means:
+RepAbs injection is done in the following phases:
+ 1) build_repabs_term inserts rep-abs pairs in the term
+ 2) we prove the equality between the original theorem and this one
+ 3) we use Pure.equal_elim_rule1 to get the new theorem.
+
+build_repabs_term does:
For abstractions:
* If the type of the abstraction doesn't need lifting we recurse.
@@ -404,7 +410,9 @@
variable needs lifting.
* If it doesn't then we recurse
* If it does we recurse and put 'RepAbs' around all occurences
- of the variable in the obtained subterm.
+ of the variable in the obtained subterm. This in combination
+ with the RepAbs above will let us change the type of the
+ abstraction with rewriting.
For applications:
* If the term is 'Respects' applied to anything we leave it unchanged
* If the term needs lifting and the head is a constant that we know
@@ -414,27 +422,24 @@
put RepAbs and recurse
* Otherwise just recurse.
-The injection is done in the following phases:
- 1) build_repabs_term inserts rep-abs pairs in the term
- 2) we prove the equality between the original theorem and this one
- 3) we use Pure.equal_elim_rule1 to get the new theorem.
To prove that the old theorem implies the new one, we first
atomize it and then try:
- 1) theorems 'trans2' from the QUOT_TYPE
+ 1) theorems 'trans2' from the appropriate QUOT_TYPE
2) remove lambdas from both sides (LAMBDA_RES_TAC)
- 3) remove Ball/Bex
- 4) use RSP theorems
- 5) remove rep_abs from right side
- 6) reflexivity
+ 3) remove Ball/Bex from the right hand side
+ 4) use user-supplied RSP theorems
+ 5) remove rep_abs from the right side
+ 6) reflexivity of equality
7) split applications of lifted type (apply_rsp)
8) split applications of non-lifted type (cong_tac)
9) apply extentionality
-10) relation reflexive
+10) reflexivity of the relation
11) assumption
+ (Lambdas under respects may have left us some assumptions)
12) proving obvious higher order equalities by simplifying fun_rel
- (not sure if still needed?)
+ (not sure if it is still needed?)
13) unfolding lambda on one side
14) simplifying (= ===> =) for simpler respectfullness
@@ -632,9 +637,14 @@
lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
by (simp add: id_def)
+(* TODO: can be also obtained with: *)
+ML {* symmetric (eq_reflection OF @{thms id_def}) *}
+
ML {*
fun build_repabs_term lthy thm consts rty qty =
let
+ (* TODO: The rty and qty stored in the quotient_info should
+ be varified, so this will soon not be needed *)
val rty = Logic.varifyT rty;
val qty = Logic.varifyT qty;
@@ -664,8 +674,8 @@
else
let
val v' = mk_repabs v;
- (* TODO: I believe this is not needed any more *)
- val t1 = Envir.beta_norm (t' $ v')
+ (* TODO: I believe 'beta' is not needed any more *)
+ val t1 = (* Envir.beta_norm *) (t' $ v')
in
lambda v t1
end)
@@ -691,7 +701,7 @@
end
*}
-text {* Assumes that it is given a regularized theorem *}
+text {* Builds provable goals for regularized theorems *}
ML {*
fun build_repabs_goal ctxt thm cons rty qty =
Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty))
@@ -699,14 +709,17 @@
ML {*
fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
-let
- val pat = Drule.strip_imp_concl (cprop_of thm)
- val insts = Thm.match (pat, concl)
-in
- rtac (Drule.instantiate insts thm) 1
-end
-handle _ => no_tac
-)
+ let
+ val pat = Drule.strip_imp_concl (cprop_of thm)
+ val insts = Thm.match (pat, concl)
+ in
+ rtac (Drule.instantiate insts thm) 1
+ end
+ handle _ => no_tac)
+*}
+
+ML {*
+fun CHANGED' tac = (fn i => CHANGED (tac i))
*}
ML {*
@@ -715,9 +728,10 @@
rtac @{thm FUN_QUOTIENT},
rtac quot_thm,
rtac @{thm IDENTITY_QUOTIENT},
- (
- fn i => CHANGED (simp_tac (HOL_ss addsimps @{thms FUN_MAP_I}) i) THEN
- rtac @{thm IDENTITY_QUOTIENT} i
+ (* For functional identity quotients, (op = ---> op =) *)
+ CHANGED' (
+ (simp_tac (HOL_ss addsimps @{thms FUN_MAP_I})) THEN'
+ rtac @{thm IDENTITY_QUOTIENT}
)
])
*}
@@ -725,7 +739,7 @@
ML {*
fun LAMBDA_RES_TAC ctxt i st =
(case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
- (_ $ (_ $ (Abs(_, _, _))$(Abs(_, _, _)))) =>
+ (_ $ (_ $ (Abs(_, _, _)) $ (Abs(_, _, _)))) =>
(EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
(rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
| _ => fn _ => no_tac) i st
@@ -749,12 +763,12 @@
val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;
val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
val insts = Thm.match (pat, concl)
-in
- if needs_lift rty (type_of f) then
- rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
- else no_tac
-end
-handle _ => no_tac)
+ in
+ if needs_lift rty (type_of f) then
+ rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
+ else no_tac
+ end
+ handle _ => no_tac)
*}
ML {*
@@ -768,8 +782,7 @@
THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
(simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
end
- handle _ => no_tac
- )
+ handle _ => no_tac)
*}
ML {*
@@ -783,8 +796,11 @@
THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
(simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
end
- handle _ => no_tac
- )
+ handle _ => no_tac)
+*}
+
+ML {*
+fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
*}
ML {*
@@ -797,18 +813,14 @@
FIRST' (map rtac rsp_thms),
(instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
rtac refl,
-(* rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*)
(APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
Cong_Tac.cong_tac @{thm cong},
rtac @{thm ext},
rtac reflex_thm,
atac,
- (
- (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
- THEN_ALL_NEW (fn _ => no_tac)
- ),
+ SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
WEAK_LAMBDA_RES_TAC ctxt,
- (fn i => CHANGED (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}) i))
+ CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))
])
*}
@@ -828,12 +840,10 @@
section {* Cleaning the goal *}
lemma prod_fun_id: "prod_fun id id = id"
- apply (simp add: prod_fun_def)
-done
+by (simp add: prod_fun_def)
+
lemma map_id: "map id x = x"
- apply (induct x)
- apply (simp_all add: map.simps)
-done
+by (induct x) (simp_all)
ML {*
fun simp_ids lthy thm =
@@ -866,6 +876,7 @@
end
*}
+(* TODO: Check if it behaves properly with varifyed rty *)
ML {*
fun findabs_all rty tm =
case tm of
@@ -881,7 +892,6 @@
fun findabs rty tm = distinct (op =) (findabs_all rty tm)
*}
-
ML {*
fun findaps_all rty tm =
case tm of
@@ -894,6 +904,7 @@
fun findaps rty tm = distinct (op =) (findaps_all rty tm)
*}
+(* Currently useful only for LAMBDA_PRS *)
ML {*
fun make_simp_prs_thm lthy quot_thm thm typ =
let
@@ -936,6 +947,7 @@
in (a1 @ a2, e1 @ e2) end
| _ => ([], []);
*}
+
ML {*
fun findallex lthy rty qty tm =
let
@@ -1005,12 +1017,12 @@
*}
ML {*
-fun matches (ty1, ty2) =
- Type.raw_instance (ty1, Logic.varifyT ty2);
-
fun lookup_quot_data lthy qty =
let
+ fun matches (ty1, ty2) =
+ Type.raw_instance (ty1, Logic.varifyT ty2);
val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy)
+ (* TODO: Should no longer be needed *)
val rty = Logic.unvarifyT (#rtyp quotdata)
val rel = #rel quotdata
val rel_eqv = #equiv_thm quotdata