# HG changeset patch # User Cezary Kaliszyk # Date 1258980931 -3600 # Node ID e6b6e5ba0cc5366eb4fa1227479dd5841f52cc06 # Parent 87eae6a2e5ff835d51761615ff8727f3c3b6348f Moved new repabs_inj code to QuotMain diff -r 87eae6a2e5ff -r e6b6e5ba0cc5 IntEx.thy --- a/IntEx.thy Mon Nov 23 13:46:14 2009 +0100 +++ b/IntEx.thy Mon Nov 23 13:55:31 2009 +0100 @@ -161,75 +161,6 @@ 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 is_lifted_const h gh = is_Const h andalso is_Const gh andalso not (h = gh) - -fun inj_REPABS lthy (rtrm, qtrm) = -let - val rty = fastype_of rtrm - val qty = fastype_of qtrm -in - case (rtrm, qtrm) of - (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 "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => - Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t')) - | (Const (@{const_name "Babs"}, T) $ r $ t, t') => - Const (@{const_name "Babs"}, T) $ r $ (inj_REPABS lthy (t, t')) - | (Abs (x, T, t), Abs (x', T', t')) => - let - val (y, s) = Term.dest_abs (x, T, t) - val (_, s') = Term.dest_abs (x', T', t') - val yvar = Free (y, T) - val res = lambda yvar (inj_REPABS lthy (s, s')) - in - if rty = qty - then res - else if T = T' - then mk_repabs lthy (rty, qty) res - else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res)) - end - | _ => - let - val (rhead, rargs) = strip_comb rtrm - val (qhead, qargs) = strip_comb qtrm - (* TODO: val rhead' = inj_REPABS lthy (rhead, qhead) *) - val rhead' = rhead; - val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs); - val result = list_comb (rhead', rargs'); - in - if rty = qty then result else - if (is_lifted_const rhead qhead) then mk_repabs lthy (rty, qty) result else - if ((Term.is_Free rhead) andalso (length rargs' > 0)) then mk_repabs lthy (rty, qty) result else - if rargs' = [] then rhead' else result - end -end -*} - -ML {* -fun mk_inj_REPABS_goal lthy (rtrm, qtrm) = - Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm))) -*} lemma plus_assoc_pre: shows "my_plus (my_plus i j) k \ my_plus i (my_plus j k)" @@ -244,7 +175,6 @@ ML {* val arthm = atomize_thm @{thm plus_assoc_pre} val aqthm = atomize_thm test2 - val aqtrm = prop_of aqthm val artrm = prop_of arthm *} @@ -258,6 +188,8 @@ ML {* val reg_atrm = prop_of (@{thm testtest} OF [arthm]) *} +(* +does not work. ML {* fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = (REPEAT1 o FIRST1) @@ -278,6 +210,7 @@ DT ctxt "E" (WEAK_LAMBDA_RES_TAC ctxt), DT ctxt "F" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))] *} +*) ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"} @@ -298,9 +231,8 @@ prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *} apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) -(* does not work *) -apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms *}) - +apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) +done ML {* inj_REPABS @{context} (reg_atrm, aqtrm) diff -r 87eae6a2e5ff -r e6b6e5ba0cc5 QuotMain.thy --- a/QuotMain.thy Mon Nov 23 13:46:14 2009 +0100 +++ b/QuotMain.thy Mon Nov 23 13:55:31 2009 +0100 @@ -1449,6 +1449,76 @@ end *} +(* 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 is_lifted_const h gh = is_Const h andalso is_Const gh andalso not (h = gh) + +fun inj_REPABS lthy (rtrm, qtrm) = +let + val rty = fastype_of rtrm + val qty = fastype_of qtrm +in + case (rtrm, qtrm) of + (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 "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => + Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t')) + | (Const (@{const_name "Babs"}, T) $ r $ t, t') => + Const (@{const_name "Babs"}, T) $ r $ (inj_REPABS lthy (t, t')) + | (Abs (x, T, t), Abs (x', T', t')) => + let + val (y, s) = Term.dest_abs (x, T, t) + val (_, s') = Term.dest_abs (x', T', t') + val yvar = Free (y, T) + val res = lambda yvar (inj_REPABS lthy (s, s')) + in + if rty = qty + then res + else if T = T' + then mk_repabs lthy (rty, qty) res + else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res)) + end + | _ => + let + val (rhead, rargs) = strip_comb rtrm + val (qhead, qargs) = strip_comb qtrm + (* TODO: val rhead' = inj_REPABS lthy (rhead, qhead) *) + val rhead' = rhead; + val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs); + val result = list_comb (rhead', rargs'); + in + if rty = qty then result else + if (is_lifted_const rhead qhead) then mk_repabs lthy (rty, qty) result else + if ((Term.is_Free rhead) andalso (length rargs' > 0)) then mk_repabs lthy (rty, qty) result else + if rargs' = [] then rhead' else result + end +end +*} + +ML {* +fun mk_inj_REPABS_goal lthy (rtrm, qtrm) = + Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm))) +*} + end