streamlined the generation of quotient theorems out of raw theorems
authorChristian Urban <urbanc@in.tum.de>
Sat Jun 26 08:23:40 2010 +0100 (2010-06-26)
changeset 375601b5bbc4a14bc
parent 37559 9118ce1d1750
child 37561 19fca77829ea
streamlined the generation of quotient theorems out of raw theorems
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/Quotient/quotient_term.ML
     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 *)