--- 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
--- 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)
--- 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 *)