--- a/IntEx.thy Sat Nov 21 23:23:01 2009 +0100
+++ b/IntEx.thy Sun Nov 22 00:01:06 2009 +0100
@@ -119,10 +119,6 @@
where
"SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
-
-
-ML {* print_qconstinfo @{context} *}
-
ML {* print_qconstinfo @{context} *}
lemma plus_sym_pre:
@@ -165,18 +161,26 @@
apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *})
done
+(* rep-abs injection *)
+
ML {*
+(* FIXME: is this the right get_fun function for rep-abs injection *)
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 {*
+(* replaces a term for the bound variable, *)
+(* possible capture *)
fun replace_bnd0 (trm, Abs (x, T, t)) =
Abs (x, T, subst_bound (trm, t))
*}
ML {*
+(* bound variables need to be treated properly, *)
+(* as the type of subterms need to be calculated *)
+
fun inj_REPABS lthy (rtrm, qtrm) =
let
val rty = fastype_of rtrm
@@ -184,34 +188,34 @@
in
case (rtrm, qtrm) of
(Abs (x, T, t), Abs (x', T', t')) =>
- let
- val (y, s) = Term.dest_abs (x, T, t)
- val (y', s') = Term.dest_abs (x', T', t')
- val yvar = Free (y, T)
- val res = lambda yvar (inj_REPABS lthy (s, s'))
- in
- if T = T'
- then res
- else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res))
- end
- (* FIXME: Does one havae to look at the abstraction or go under the lambda. *)
+ let
+ val (y, s) = Term.dest_abs (x, T, t)
+ val (y', s') = Term.dest_abs (x', T', t')
+ val yvar = Free (y, T)
+ val res = lambda yvar (inj_REPABS lthy (s, s'))
+ in
+ if T = T'
+ then res
+ else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res))
+ end
+ (* FIXME: Does one have to look at the abstraction or have to go under the lambda? *)
| (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
- Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t'))
+ Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t'))
| (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
- Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t'))
- | (rtrm as _ $ _, qtrm as _ $ _) =>
- let
- val (rhead, rargs) = Term.strip_comb rtrm
- val (qhead, qargs) = Term.strip_comb qtrm
- val rhead' = inj_REPABS lthy (rhead, qhead)
- val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs)
- val res = list_comb (rhead', rargs')
- in
- if rty = qty
- then res
- else mk_repabs lthy (rty, qty) res
- end
- (* FIXME: cases for frees and vars *)
+ Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t'))
+ | (_ $ _, _ $ _) =>
+ let
+ val (rhead, rargs) = strip_comb rtrm
+ val (qhead, qargs) = strip_comb qtrm
+ val rhead' = inj_REPABS lthy (rhead, qhead)
+ val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs)
+ val result = list_comb (rhead', rargs')
+ in
+ if rty = qty
+ then result
+ else mk_repabs lthy (rty, qty) res
+ end
+ (* FIXME: cases for frees and vars? *)
| _ => rtrm
end
*}
@@ -278,8 +282,8 @@
ML {* cprem_of *}
ML {*
-(mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm)
- |> Syntax.check_term @{context})
+mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm)
+ |> Syntax.check_term @{context}
*}
prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *}
@@ -295,12 +299,6 @@
*}
-
-
-
-
-
-
lemma ho_tst: "foldl my_plus x [] = x"
apply simp
done
--- a/QuotMain.thy Sat Nov 21 23:23:01 2009 +0100
+++ b/QuotMain.thy Sun Nov 22 00:01:06 2009 +0100
@@ -1206,6 +1206,8 @@
(******************************************)
ML {*
+(* builds the relation for respects *)
+
fun mk_resp_arg lthy (rty, qty) =
let
val thy = ProofContext.theory_of lthy
@@ -1221,10 +1223,13 @@
end
else let
val SOME qinfo = quotdata_lookup_thy thy s'
+ (* FIXME: check in this case that the rty and qty *)
+ (* FIXME: correspond to each other *)
in
#rel qinfo
end
- | _ => HOLogic.eq_const dummyT
+ | _ => HOLogic.eq_const dummyT
+ (* FIXME: do the types correspond to each other? *)
end
*}
@@ -1247,33 +1252,46 @@
*}
ML {*
-(* applies f to the subterm of an abstractions, otherwise to the given term *)
-(* abstracted variables do not have to be treated specially *)
+(* - applies f to the subterm of an abstraction, *)
+(* otherwise to the given term, *)
+(* - used by REGUKARIZE, therefore abstracted *)
+(* variables do not have to be treated specially *)
+
fun apply_subt f trm1 trm2 =
case (trm1, trm2) of
(Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t')
| _ => f trm1 trm2
+(* the major type of All and Ex quantifiers *)
fun qnt_typ ty = domain_type (domain_type ty)
*}
(*
-Regularizing an rterm means:
- - Quantifiers over a type that needs lifting are replaced by
+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
- - Abstractions over a type that needs lifting are replaced
+ \<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
- appropriate relations:
+ - 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:
+
+ 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 *)
+(* - does not need any special treatment of *)
+(* bound variables *)
+
fun REGULARIZE_trm lthy rtrm qtrm =
case (rtrm, qtrm) of
(Abs (x, ty, t), Abs (x', ty', t')) =>
@@ -1313,7 +1331,7 @@
(REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2')
| (Free (x, ty), Free (x', ty')) =>
if x = x'
- then rtrm
+ then rtrm (* FIXME: check whether types corresponds *)
else trm_lift_error lthy rtrm qtrm
| (Bound i, Bound i') =>
if i = i'
@@ -1328,12 +1346,13 @@
ML {*
fun mk_REGULARIZE_goal lthy rtrm qtrm =
- Logic.mk_implies (rtrm, REGULARIZE_trm lthy rtrm qtrm |> Syntax.check_term lthy)
+ Logic.mk_implies (rtrm, Syntax.check_term lthy (REGULARIZE_trm lthy rtrm qtrm))
*}
(*
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
@@ -1362,6 +1381,7 @@
done
ML {*
+(* FIXME: get_rid of rel_refl rel_eqv *)
fun REGULARIZE_tac lthy rel_refl rel_eqv =
(REPEAT1 o FIRST1)
[rtac rel_refl,
@@ -1376,7 +1396,7 @@
rtac @{thm RIGHT_RES_FORALL_REGULAR}]
*}
-(* same version including debugging information *)
+(* version of REGULARIZE_tac including debugging information *)
ML {*
fun my_print_tac ctxt s thm =
let
@@ -1392,7 +1412,6 @@
*}
ML {*
-(* FIXME: change rel_refl rel_eqv *)
fun REGULARIZE_tac' lthy rel_refl rel_eqv =
(REPEAT1 o FIRST1)
[(K (print_tac "start")) THEN' (K no_tac),
@@ -1412,10 +1431,9 @@
fun REGULARIZE_prove rtrm qtrm rel_eqv rel_refl lthy =
let
val goal = mk_REGULARIZE_goal lthy rtrm qtrm
- val cthm = Goal.prove lthy [] [] goal
+ in
+ Goal.prove lthy [] [] goal
(fn {context, ...} => REGULARIZE_tac' context rel_refl rel_eqv)
- in
- cthm
end
*}