# HG changeset patch # User Christian Urban # Date 1258844466 -3600 # Node ID 1a0f0b758071a155880c7091b5b8ae247f7f6740 # Parent 5d06e1dba69aa8be55d9401d09f190e2a7ef798c a little tuning of comments diff -r 5d06e1dba69a -r 1a0f0b758071 IntEx.thy --- 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 diff -r 5d06e1dba69a -r 1a0f0b758071 QuotMain.thy --- 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: - \x. P \ \x\(Respects R). P - - Abstractions over a type that needs lifting are replaced + \x. P \ \x \ (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: \x. P \ Ball (Respects R) (\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 \ A \ B - Example with more complicated types of A, B: + + example with more complicated types of A, B: A = B \ (op = \ op \) 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 *}