# HG changeset patch # User Christian Urban # Date 1277738439 -3600 # Node ID e16495cfdde058fc5e6d18e849ac8f32baf944d8 # Parent d3daea901123646e8bb973955af33adcf7f86177 separation of translations in derive_qtrm / derive_rtrm (similarly for types) diff -r d3daea901123 -r e16495cfdde0 src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Mon Jun 28 15:03:07 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Mon Jun 28 16:20:39 2010 +0100 @@ -92,7 +92,7 @@ fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt = let val rty = fastype_of rconst - val qty = derive_qtyp qtys rty false ctxt + val qty = derive_qtyp qtys rty ctxt val lhs = Free (qconst_name, qty) in quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt diff -r d3daea901123 -r e16495cfdde0 src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Jun 28 15:03:07 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Jun 28 16:20:39 2010 +0100 @@ -624,7 +624,7 @@ [] => let val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt) - val rtrm = derive_qtrm qtys goal true ctxt + val rtrm = derive_rtrm qtys goal ctxt val rule = procedure_inst ctxt rtrm goal in rtac rule i @@ -670,7 +670,7 @@ so we do it both in the original theorem *) val thm' = Drule.eta_contraction_rule thm val ((_, [thm'']), ctxt') = Variable.import false [thm'] ctxt - val goal = derive_qtrm qtys (prop_of thm'') false ctxt' + val goal = derive_qtrm qtys (prop_of thm'') ctxt' in Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm'] 1)) |> singleton (ProofContext.export ctxt' ctxt) diff -r d3daea901123 -r e16495cfdde0 src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Mon Jun 28 15:03:07 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Mon Jun 28 16:20:39 2010 +0100 @@ -26,8 +26,10 @@ val inj_repabs_trm: Proof.context -> term * term -> term val inj_repabs_trm_chk: Proof.context -> term * term -> term - val derive_qtyp: typ list -> typ -> bool -> Proof.context -> typ - val derive_qtrm: typ list -> term -> bool -> Proof.context -> term + val derive_qtyp: typ list -> typ -> Proof.context -> typ + val derive_qtrm: typ list -> term -> Proof.context -> term + val derive_rtyp: typ list -> typ -> Proof.context -> typ + val derive_rtrm: typ list -> term -> Proof.context -> term end; structure Quotient_Term: QUOTIENT_TERM = @@ -690,16 +692,15 @@ (*** Wrapper for automatically transforming an rthm into a qthm ***) -(* subst_rty takes a list of (rty, qty) substitution pairs - and replaces all occurences of rty in the given type - by an appropriate qty +(* substitutions functions for r/q-types and + r/q-constants, respectively *) -fun subst_rtyp ctxt ty_subst rty = +fun subst_typ ctxt ty_subst rty = case rty of Type (s, rtys) => let val thy = ProofContext.theory_of ctxt - val rty' = Type (s, map (subst_rtyp ctxt ty_subst) rtys) + val rty' = Type (s, map (subst_typ ctxt ty_subst) rtys) fun matches [] = rty' | matches ((rty, qty)::tail) = @@ -711,23 +712,18 @@ end | _ => rty -(* subst_rtrm takes a list of (rconst, qconst) substitution pairs, - as well as (rty, qty) substitution pairs, and replaces all - occurences of rconst and rty by appropriate instances of - qconst and qty -*) -fun subst_rtrm ctxt ty_subst trm_subst rtrm = +fun subst_trm ctxt ty_subst trm_subst rtrm = case rtrm of - t1 $ t2 => (subst_rtrm ctxt ty_subst trm_subst t1) $ (subst_rtrm ctxt ty_subst trm_subst t2) - | Abs (x, ty, t) => Abs (x, subst_rtyp ctxt ty_subst ty, subst_rtrm ctxt ty_subst trm_subst t) - | Free(n, ty) => Free(n, subst_rtyp ctxt ty_subst ty) - | Var(n, ty) => Var(n, subst_rtyp ctxt ty_subst ty) + t1 $ t2 => (subst_trm ctxt ty_subst trm_subst t1) $ (subst_trm ctxt ty_subst trm_subst t2) + | Abs (x, ty, t) => Abs (x, subst_typ ctxt ty_subst ty, subst_trm ctxt ty_subst trm_subst t) + | Free(n, ty) => Free(n, subst_typ ctxt ty_subst ty) + | Var(n, ty) => Var(n, subst_typ ctxt ty_subst ty) | Bound i => Bound i | Const (a, ty) => let val thy = ProofContext.theory_of ctxt - fun matches [] = Const (a, subst_rtyp ctxt ty_subst ty) + fun matches [] = Const (a, subst_typ ctxt ty_subst ty) | matches ((rconst, qconst)::tail) = case try (Pattern.match thy (rconst, rtrm)) (Vartab.empty, Vartab.empty) of NONE => matches tail @@ -736,44 +732,55 @@ matches trm_subst end -(* generates type substitutions out of the - types involved in a quotient +(* generate type and term substitutions out of the + qtypes involved in a quotient; the direction flag + indicates in which direction the substitution work: + + true: quotient -> raw + false: raw -> quotient *) -fun get_ty_subst qtys reverse ctxt = +fun mk_ty_subst qtys direction ctxt = Quotient_Info.quotdata_dest ctxt |> map (fn x => (#rtyp x, #qtyp x)) |> filter (fn (_, qty) => member (op =) qtys qty) - |> map (fn (x, y) => if reverse then (y, x) else (x, y)) + |> map (if direction then swap else I) -(* generates term substitutions out of the qconst - definitions and relations in a quotient -*) -fun get_trm_subst qtys reverse ctxt = +fun mk_trm_subst qtys direction ctxt = let - val subst_rtyp' = subst_rtyp ctxt (get_ty_subst qtys reverse ctxt) - fun proper (rt, qt) = (subst_rtyp' (fastype_of rt) = fastype_of qt) + val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt) + fun proper (t1, t2) = (subst_typ' (fastype_of t1) = fastype_of t2) val const_substs = Quotient_Info.qconsts_dest ctxt |> map (fn x => (#rconst x, #qconst x)) - |> map (fn (x, y) => if reverse then (y, x) else (x, y)) + |> map (if direction then swap else I) val rel_substs = Quotient_Info.quotdata_dest ctxt |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x))) - |> map (fn (x, y) => if reverse then (y, x) else (x, y)) + |> map (if direction then swap else I) in filter proper (const_substs @ rel_substs) end + (* derives a qtyp and qtrm out of a rtyp and rtrm, respectively *) -fun derive_qtyp qtys rty unlift ctxt = - subst_rtyp ctxt (get_ty_subst qtys unlift ctxt) rty +fun derive_qtyp qtys rty ctxt = + subst_typ ctxt (mk_ty_subst qtys false ctxt) rty + +fun derive_qtrm qtys rtrm ctxt = + subst_trm ctxt (mk_ty_subst qtys false ctxt) (mk_trm_subst qtys false ctxt) rtrm -fun derive_qtrm qtys rtrm unlift ctxt = - subst_rtrm ctxt (get_ty_subst qtys unlift ctxt) (get_trm_subst qtys unlift ctxt) rtrm +(* derives a rtyp and rtrm out of a qtyp and qtrm, + respectively +*) +fun derive_rtyp qtys qty ctxt = + subst_typ ctxt (mk_ty_subst qtys true ctxt) qty + +fun derive_rtrm qtys qtrm ctxt = + subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm end; (* structure *)