src/HOL/Tools/Quotient/quotient_term.ML
changeset 37592 e16495cfdde0
parent 37591 d3daea901123
child 37609 ebc157ab01b0
     1.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Mon Jun 28 15:03:07 2010 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Mon Jun 28 16:20:39 2010 +0100
     1.3 @@ -26,8 +26,10 @@
     1.4    val inj_repabs_trm: Proof.context -> term * term -> term
     1.5    val inj_repabs_trm_chk: Proof.context -> term * term -> term
     1.6  
     1.7 -  val derive_qtyp: typ list -> typ -> bool -> Proof.context -> typ
     1.8 -  val derive_qtrm: typ list -> term -> bool -> Proof.context -> term
     1.9 +  val derive_qtyp: typ list -> typ -> Proof.context -> typ
    1.10 +  val derive_qtrm: typ list -> term -> Proof.context -> term
    1.11 +  val derive_rtyp: typ list -> typ -> Proof.context -> typ
    1.12 +  val derive_rtrm: typ list -> term -> Proof.context -> term
    1.13  end;
    1.14  
    1.15  structure Quotient_Term: QUOTIENT_TERM =
    1.16 @@ -690,16 +692,15 @@
    1.17  
    1.18  (*** Wrapper for automatically transforming an rthm into a qthm ***)
    1.19  
    1.20 -(* subst_rty takes a list of (rty, qty) substitution pairs
    1.21 -   and replaces all occurences of rty in the given type
    1.22 -   by an appropriate qty
    1.23 +(* substitutions functions for r/q-types and
    1.24 +   r/q-constants, respectively
    1.25  *)
    1.26 -fun subst_rtyp ctxt ty_subst rty =
    1.27 +fun subst_typ ctxt ty_subst rty =
    1.28    case rty of
    1.29      Type (s, rtys) =>
    1.30        let
    1.31          val thy = ProofContext.theory_of ctxt
    1.32 -        val rty' = Type (s, map (subst_rtyp ctxt ty_subst) rtys)
    1.33 +        val rty' = Type (s, map (subst_typ ctxt ty_subst) rtys)
    1.34  
    1.35          fun matches [] = rty'
    1.36            | matches ((rty, qty)::tail) =
    1.37 @@ -711,23 +712,18 @@
    1.38        end 
    1.39    | _ => rty
    1.40  
    1.41 -(* subst_rtrm takes a list of (rconst, qconst) substitution pairs,
    1.42 -   as well as (rty, qty) substitution pairs, and replaces all
    1.43 -   occurences of rconst and rty by appropriate instances of
    1.44 -   qconst and qty
    1.45 -*)
    1.46 -fun subst_rtrm ctxt ty_subst trm_subst rtrm =
    1.47 +fun subst_trm ctxt ty_subst trm_subst rtrm =
    1.48    case rtrm of
    1.49 -    t1 $ t2 => (subst_rtrm ctxt ty_subst trm_subst t1) $ (subst_rtrm ctxt ty_subst trm_subst t2)
    1.50 -  | Abs (x, ty, t) => Abs (x, subst_rtyp ctxt ty_subst ty, subst_rtrm ctxt ty_subst trm_subst t)
    1.51 -  | Free(n, ty) => Free(n, subst_rtyp ctxt ty_subst ty)
    1.52 -  | Var(n, ty) => Var(n, subst_rtyp ctxt ty_subst ty)
    1.53 +    t1 $ t2 => (subst_trm ctxt ty_subst trm_subst t1) $ (subst_trm ctxt ty_subst trm_subst t2)
    1.54 +  | Abs (x, ty, t) => Abs (x, subst_typ ctxt ty_subst ty, subst_trm ctxt ty_subst trm_subst t)
    1.55 +  | Free(n, ty) => Free(n, subst_typ ctxt ty_subst ty)
    1.56 +  | Var(n, ty) => Var(n, subst_typ ctxt ty_subst ty)
    1.57    | Bound i => Bound i
    1.58    | Const (a, ty) => 
    1.59        let
    1.60          val thy = ProofContext.theory_of ctxt
    1.61  
    1.62 -        fun matches [] = Const (a, subst_rtyp ctxt ty_subst ty)
    1.63 +        fun matches [] = Const (a, subst_typ ctxt ty_subst ty)
    1.64            | matches ((rconst, qconst)::tail) =
    1.65                case try (Pattern.match thy (rconst, rtrm)) (Vartab.empty, Vartab.empty) of
    1.66                  NONE => matches tail
    1.67 @@ -736,44 +732,55 @@
    1.68          matches trm_subst
    1.69        end
    1.70  
    1.71 -(* generates type substitutions out of the
    1.72 -   types involved in a quotient
    1.73 +(* generate type and term substitutions out of the
    1.74 +   qtypes involved in a quotient; the direction flag 
    1.75 +   indicates in which direction the substitution work: 
    1.76 +   
    1.77 +     true:  quotient -> raw
    1.78 +     false: raw -> quotient
    1.79  *)
    1.80 -fun get_ty_subst qtys reverse ctxt =
    1.81 +fun mk_ty_subst qtys direction ctxt =
    1.82    Quotient_Info.quotdata_dest ctxt
    1.83     |> map (fn x => (#rtyp x, #qtyp x))
    1.84     |> filter (fn (_, qty) => member (op =) qtys qty)
    1.85 -   |> map (fn (x, y) => if reverse then (y, x) else (x, y))
    1.86 +   |> map (if direction then swap else I)
    1.87  
    1.88 -(* generates term substitutions out of the qconst 
    1.89 -   definitions and relations in a quotient
    1.90 -*)
    1.91 -fun get_trm_subst qtys reverse ctxt =
    1.92 +fun mk_trm_subst qtys direction ctxt =
    1.93  let
    1.94 -  val subst_rtyp' = subst_rtyp ctxt (get_ty_subst qtys reverse ctxt)
    1.95 -  fun proper (rt, qt) = (subst_rtyp' (fastype_of rt) = fastype_of qt)
    1.96 +  val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt)
    1.97 +  fun proper (t1, t2) = (subst_typ' (fastype_of t1) = fastype_of t2)
    1.98  
    1.99    val const_substs = 
   1.100      Quotient_Info.qconsts_dest ctxt
   1.101       |> map (fn x => (#rconst x, #qconst x))
   1.102 -     |> map (fn (x, y) => if reverse then (y, x) else (x, y))
   1.103 +     |> map (if direction then swap else I)
   1.104  
   1.105    val rel_substs =
   1.106      Quotient_Info.quotdata_dest ctxt
   1.107       |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
   1.108 -     |> map (fn (x, y) => if reverse then (y, x) else (x, y))
   1.109 +     |> map (if direction then swap else I)
   1.110  in
   1.111    filter proper (const_substs @ rel_substs)
   1.112  end
   1.113  
   1.114 +
   1.115  (* derives a qtyp and qtrm out of a rtyp and rtrm,
   1.116     respectively 
   1.117  *)
   1.118 -fun derive_qtyp qtys rty unlift ctxt =
   1.119 -  subst_rtyp ctxt (get_ty_subst qtys unlift ctxt) rty
   1.120 +fun derive_qtyp qtys rty ctxt =
   1.121 +  subst_typ ctxt (mk_ty_subst qtys false ctxt) rty
   1.122 +
   1.123 +fun derive_qtrm qtys rtrm ctxt =
   1.124 +  subst_trm ctxt (mk_ty_subst qtys false ctxt) (mk_trm_subst qtys false ctxt) rtrm
   1.125  
   1.126 -fun derive_qtrm qtys rtrm unlift ctxt =
   1.127 -  subst_rtrm ctxt (get_ty_subst qtys unlift ctxt) (get_trm_subst qtys unlift ctxt) rtrm
   1.128 +(* derives a rtyp and rtrm out of a qtyp and qtrm,
   1.129 +   respectively 
   1.130 +*)
   1.131 +fun derive_rtyp qtys qty ctxt =
   1.132 +  subst_typ ctxt (mk_ty_subst qtys true ctxt) qty
   1.133 +
   1.134 +fun derive_rtrm qtys qtrm ctxt =
   1.135 +  subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm
   1.136  
   1.137  
   1.138  end; (* structure *)