1.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Jun 25 19:12:04 2010 +0200
1.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sat Jun 26 08:23:40 2010 +0100
1.3 @@ -649,13 +649,21 @@
1.4 so we do it both in the original theorem *)
1.5 val thm' = Drule.eta_contraction_rule thm
1.6 val ((_, [thm'']), ctxt') = Variable.import false [thm'] ctxt
1.7 - val goal = (quotient_lift_all qtys ctxt' o prop_of) thm''
1.8 + val goal = derive_qtrm qtys (prop_of thm'') ctxt'
1.9 in
1.10 Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm'] 1))
1.11 |> singleton (ProofContext.export ctxt' ctxt)
1.12 end;
1.13
1.14 -(* An Attribute which automatically constructs the qthm *)
1.15 -val lifted_attrib = Thm.rule_attribute (fn ctxt => lifted [] (Context.proof_of ctxt))
1.16 +(* An attribute which automatically constructs the qthm
1.17 + using all quotients defined so far.
1.18 +*)
1.19 +val lifted_attrib = Thm.rule_attribute (fn context =>
1.20 + let
1.21 + val ctxt = Context.proof_of context
1.22 + val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
1.23 + in
1.24 + lifted qtys ctxt
1.25 + end)
1.26
1.27 end; (* structure *)
2.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Jun 25 19:12:04 2010 +0200
2.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Sat Jun 26 08:23:40 2010 +0100
2.3 @@ -27,7 +27,7 @@
2.4 val inj_repabs_trm_chk: Proof.context -> term * term -> term
2.5
2.6 val derive_qtyp: typ list -> typ -> Proof.context -> typ
2.7 - val quotient_lift_all: typ list -> Proof.context -> term -> term
2.8 + val derive_qtrm: typ list -> term -> Proof.context -> term
2.9 end;
2.10
2.11 structure Quotient_Term: QUOTIENT_TERM =
2.12 @@ -692,94 +692,85 @@
2.13
2.14 (* subst_tys takes a list of (rty, qty) substitution pairs
2.15 and replaces all occurences of rty in the given type
2.16 - by appropriate qty, with substitution *)
2.17 -fun subst_ty thy ty (rty, qty) r =
2.18 - if r <> NONE then r else
2.19 - case try (Sign.typ_match thy (rty, ty)) Vartab.empty of
2.20 - SOME inst => SOME (Envir.subst_type inst qty)
2.21 - | NONE => NONE
2.22 -fun subst_tys thy substs ty =
2.23 - case fold (subst_ty thy ty) substs NONE of
2.24 - SOME ty => ty
2.25 - | NONE =>
2.26 - (case ty of
2.27 - Type (s, tys) => Type (s, map (subst_tys thy substs) tys)
2.28 - | x => x)
2.29 + by an appropriate qty
2.30 +*)
2.31 +fun subst_rtyp ctxt ty_subst rty =
2.32 + case rty of
2.33 + Type (s, rtys) =>
2.34 + let
2.35 + val thy = ProofContext.theory_of ctxt
2.36 + val rty' = Type (s, map (subst_rtyp ctxt ty_subst) rtys)
2.37
2.38 -(* subst_trms takes a list of (rtrm, qtrm) substitution pairs
2.39 - and if the given term matches any of the raw terms it
2.40 - returns the appropriate qtrm instantiated. If none of
2.41 - them matched it returns NONE. *)
2.42 -fun subst_trm thy t (rtrm, qtrm) s =
2.43 - if s <> NONE then s else
2.44 - case try (Pattern.match thy (rtrm, t)) (Vartab.empty, Vartab.empty) of
2.45 - SOME inst => SOME (Envir.subst_term inst qtrm)
2.46 - | NONE => NONE;
2.47 -fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE
2.48 + fun matches [] = rty'
2.49 + | matches ((rty, qty)::tail) =
2.50 + case try (Sign.typ_match thy (rty, rty')) Vartab.empty of
2.51 + NONE => matches tail
2.52 + | SOME inst => Envir.subst_type inst qty
2.53 + in
2.54 + matches ty_subst
2.55 + end
2.56 + | _ => rty
2.57
2.58 -(* prepares type and term substitution pairs to be used by above
2.59 - functions that let replace all raw constructs by appropriate
2.60 - lifted counterparts. *)
2.61 -fun get_ty_trm_substs qtys ctxt =
2.62 -let
2.63 - val thy = ProofContext.theory_of ctxt
2.64 - val quot_infos = Quotient_Info.quotdata_dest ctxt
2.65 - val const_infos = Quotient_Info.qconsts_dest ctxt
2.66 - val all_ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
2.67 - val ty_substs =
2.68 - if qtys = [] then all_ty_substs else
2.69 - filter (fn (_, qty) => member (op =) qtys qty) all_ty_substs
2.70 - val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos
2.71 - fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel)))
2.72 - val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos
2.73 - fun valid_trm_subst (rt, qt) = (subst_tys thy ty_substs (fastype_of rt) = fastype_of qt)
2.74 - val all_trm_substs = const_substs @ rel_substs
2.75 +(* subst_trms takes a list of (rconst, qconst) substitution pairs,
2.76 + as well as (rty, qty) substitution pairs, and replaces all
2.77 + occurences of rconst and rty by appropriate instances of
2.78 + qconst and qty
2.79 +*)
2.80 +fun subst_rtrm ctxt ty_subst trm_subst rtrm =
2.81 + case rtrm of
2.82 + t1 $ t2 => (subst_rtrm ctxt ty_subst trm_subst t1) $ (subst_rtrm ctxt ty_subst trm_subst t2)
2.83 + | Abs (x, ty, t) => Abs (x, subst_rtyp ctxt ty_subst ty, subst_rtrm ctxt ty_subst trm_subst t)
2.84 + | Free(n, ty) => Free(n, subst_rtyp ctxt ty_subst ty)
2.85 + | Var(n, ty) => Var(n, subst_rtyp ctxt ty_subst ty)
2.86 + | Bound i => Bound i
2.87 + | Const (a, ty) =>
2.88 + let
2.89 + val thy = ProofContext.theory_of ctxt
2.90 +
2.91 + fun matches [] = Const (a, subst_rtyp ctxt ty_subst ty)
2.92 + | matches ((rconst, qconst)::tail) =
2.93 + case try (Pattern.match thy (rconst, rtrm)) (Vartab.empty, Vartab.empty) of
2.94 + NONE => matches tail
2.95 + | SOME inst => Envir.subst_term inst qconst
2.96 + in
2.97 + matches trm_subst
2.98 + end
2.99 +
2.100 +(* generates type substitutions out of the
2.101 + types involved in a quotient
2.102 +*)
2.103 +fun get_ty_subst qtys ctxt =
2.104 + Quotient_Info.quotdata_dest ctxt
2.105 + |> map (fn x => (#rtyp x, #qtyp x))
2.106 + |> filter (fn (_, qty) => member (op =) qtys qty)
2.107 +
2.108 +(* generates term substitutions out of the qconst
2.109 + definitions and relations in a quotient
2.110 +*)
2.111 +fun get_trm_subst qtys ctxt =
2.112 +let
2.113 + val subst_rtyp' = subst_rtyp ctxt (get_ty_subst qtys ctxt)
2.114 + fun proper (rt, qt) = (subst_rtyp' (fastype_of rt) = fastype_of qt)
2.115 +
2.116 + val const_substs =
2.117 + Quotient_Info.qconsts_dest ctxt
2.118 + |> map (fn x => (#rconst x, #qconst x))
2.119 +
2.120 + val rel_substs =
2.121 + Quotient_Info.quotdata_dest ctxt
2.122 + |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
2.123 in
2.124 - (ty_substs, filter valid_trm_subst all_trm_substs)
2.125 + filter proper (const_substs @ rel_substs)
2.126 end
2.127
2.128 +(* derives a qtyp and qtrm out of a rtyp and rtrm,
2.129 + respectively
2.130 +*)
2.131 fun derive_qtyp qtys rty ctxt =
2.132 -let
2.133 - val thy = ProofContext.theory_of ctxt
2.134 - val (ty_substs, _) = get_ty_trm_substs qtys ctxt
2.135 -in
2.136 - subst_tys thy ty_substs rty
2.137 -end
2.138 + subst_rtyp ctxt (get_ty_subst qtys ctxt) rty
2.139
2.140 -(*
2.141 -Takes a term and
2.142 +fun derive_qtrm qtys rtrm ctxt =
2.143 + subst_rtrm ctxt (get_ty_subst qtys ctxt) (get_trm_subst qtys ctxt) rtrm
2.144
2.145 -* replaces raw constants by the quotient constants
2.146 -
2.147 -* replaces equivalence relations by equalities
2.148 -
2.149 -* replaces raw types by the quotient types
2.150 -
2.151 -*)
2.152 -
2.153 -fun quotient_lift_all qtys ctxt t =
2.154 -let
2.155 - val thy = ProofContext.theory_of ctxt
2.156 - val (ty_substs, substs) = get_ty_trm_substs qtys ctxt
2.157 - fun lift_aux t =
2.158 - case subst_trms thy substs t of
2.159 - SOME x => x
2.160 - | NONE =>
2.161 - (case t of
2.162 - a $ b => lift_aux a $ lift_aux b
2.163 - | Abs(a, ty, s) =>
2.164 - let
2.165 - val (y, s') = Term.dest_abs (a, ty, s)
2.166 - val nty = subst_tys thy ty_substs ty
2.167 - in
2.168 - Abs(y, nty, abstract_over (Free (y, nty), lift_aux s'))
2.169 - end
2.170 - | Free(n, ty) => Free(n, subst_tys thy ty_substs ty)
2.171 - | Var(n, ty) => Var(n, subst_tys thy ty_substs ty)
2.172 - | Bound i => Bound i
2.173 - | Const(s, ty) => Const(s, subst_tys thy ty_substs ty))
2.174 -in
2.175 - lift_aux t
2.176 -end
2.177
2.178 end; (* structure *)