author Christian Urban Sat Jun 26 08:23:40 2010 +0100 (2010-06-26) changeset 37560 1b5bbc4a14bc parent 37559 9118ce1d1750 child 37561 19fca77829ea
streamlined the generation of quotient theorems out of raw theorems
```     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 +        fun matches [] = rty'
2.39 +          | matches ((rty, qty)::tail) =
2.40 +              case try (Sign.typ_match thy (rty, rty')) Vartab.empty of
2.41 +                NONE => matches tail
2.42 +              | SOME inst => Envir.subst_type inst qty
2.43 +      in
2.44 +        matches ty_subst
2.45 +      end
2.46 +  | _ => rty
2.47 +
2.48 +(* subst_trms takes a list of (rconst, qconst) substitution pairs,
2.49 +   as well as (rty, qty) substitution pairs, and replaces all
2.50 +   occurences of rconst and rty by appropriate instances of
2.51 +   qconst and qty
2.52 +*)
2.53 +fun subst_rtrm ctxt ty_subst trm_subst rtrm =
2.54 +  case rtrm of
2.55 +    t1 \$ t2 => (subst_rtrm ctxt ty_subst trm_subst t1) \$ (subst_rtrm ctxt ty_subst trm_subst t2)
2.56 +  | Abs (x, ty, t) => Abs (x, subst_rtyp ctxt ty_subst ty, subst_rtrm ctxt ty_subst trm_subst t)
2.57 +  | Free(n, ty) => Free(n, subst_rtyp ctxt ty_subst ty)
2.58 +  | Var(n, ty) => Var(n, subst_rtyp ctxt ty_subst ty)
2.59 +  | Bound i => Bound i
2.60 +  | Const (a, ty) =>
2.61 +      let
2.62 +        val thy = ProofContext.theory_of ctxt
2.63
2.64 -(* subst_trms takes a list of (rtrm, qtrm) substitution pairs
2.65 -   and if the given term matches any of the raw terms it
2.66 -   returns the appropriate qtrm instantiated. If none of
2.67 -   them matched it returns NONE. *)
2.68 -fun subst_trm thy t (rtrm, qtrm) s =
2.69 -  if s <> NONE then s else
2.70 -    case try (Pattern.match thy (rtrm, t)) (Vartab.empty, Vartab.empty) of
2.71 -      SOME inst => SOME (Envir.subst_term inst qtrm)
2.72 -    | NONE => NONE;
2.73 -fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE
2.74 +        fun matches [] = Const (a, subst_rtyp ctxt ty_subst ty)
2.75 +          | matches ((rconst, qconst)::tail) =
2.76 +              case try (Pattern.match thy (rconst, rtrm)) (Vartab.empty, Vartab.empty) of
2.77 +                NONE => matches tail
2.78 +              | SOME inst => Envir.subst_term inst qconst
2.79 +      in
2.80 +        matches trm_subst
2.81 +      end
2.82 +
2.83 +(* generates type substitutions out of the
2.84 +   types involved in a quotient
2.85 +*)
2.86 +fun get_ty_subst qtys ctxt =
2.87 +  Quotient_Info.quotdata_dest ctxt
2.88 +   |> map (fn x => (#rtyp x, #qtyp x))
2.89 +   |> filter (fn (_, qty) => member (op =) qtys qty)
2.90
2.91 -(* prepares type and term substitution pairs to be used by above
2.92 -   functions that let replace all raw constructs by appropriate
2.93 -   lifted counterparts. *)
2.94 -fun get_ty_trm_substs qtys ctxt =
2.95 -let
2.96 -  val thy = ProofContext.theory_of ctxt
2.97 -  val quot_infos  = Quotient_Info.quotdata_dest ctxt
2.98 -  val const_infos = Quotient_Info.qconsts_dest ctxt
2.99 -  val all_ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
2.100 -  val ty_substs =
2.101 -    if qtys = [] then all_ty_substs else
2.102 -    filter (fn (_, qty) => member (op =) qtys qty) all_ty_substs
2.103 -  val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos
2.104 -  fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel)))
2.105 -  val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos
2.106 -  fun valid_trm_subst (rt, qt) = (subst_tys thy ty_substs (fastype_of rt) = fastype_of qt)
2.107 -  val all_trm_substs = const_substs @ rel_substs
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 -
2.139 -(*
2.140 -Takes a term and
2.141 -
2.142 -* replaces raw constants by the quotient constants
2.143 -
2.144 -* replaces equivalence relations by equalities
2.145 -
2.146 -* replaces raw types by the quotient types
2.147 -
2.148 -*)
2.149 +  subst_rtyp ctxt (get_ty_subst qtys ctxt) rty
2.150
2.151 -fun quotient_lift_all qtys ctxt t =
2.152 -let
2.153 -  val thy = ProofContext.theory_of ctxt
2.154 -  val (ty_substs, substs) = get_ty_trm_substs qtys ctxt
2.155 -  fun lift_aux t =
2.156 -    case subst_trms thy substs t of
2.157 -      SOME x => x
2.158 -    | NONE =>
2.159 -      (case t of
2.160 -        a \$ b => lift_aux a \$ lift_aux b
2.161 -      | Abs(a, ty, s) =>
2.162 -          let
2.163 -            val (y, s') = Term.dest_abs (a, ty, s)
2.164 -            val nty = subst_tys thy ty_substs ty
2.165 -          in
2.166 -            Abs(y, nty, abstract_over (Free (y, nty), lift_aux s'))
2.167 -          end
2.168 -      | Free(n, ty) => Free(n, subst_tys thy ty_substs ty)
2.169 -      | Var(n, ty) => Var(n, subst_tys thy ty_substs ty)
2.170 -      | Bound i => Bound i
2.171 -      | Const(s, ty) => Const(s, subst_tys thy ty_substs ty))
2.172 -in
2.173 -  lift_aux t
2.174 -end
2.175 +fun derive_qtrm qtys rtrm ctxt =
2.176 +  subst_rtrm ctxt (get_ty_subst qtys ctxt) (get_trm_subst qtys ctxt) rtrm
2.177 +
2.178
2.179  end; (* structure *)
```