src/HOL/Tools/Quotient/quotient_term.ML
changeset 38624 9bb0016f7e60
parent 38558 32ad17fe2b9c
child 38694 9db37e912ee4
     1.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Aug 20 20:29:50 2010 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Sun Aug 22 10:45:53 2010 +0800
     1.3 @@ -26,10 +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 -> Proof.context -> typ
     1.8 -  val derive_qtrm: typ list -> term -> Proof.context -> term
     1.9 -  val derive_rtyp: typ list -> typ -> Proof.context -> typ
    1.10 -  val derive_rtrm: typ list -> term -> Proof.context -> term
    1.11 +  val derive_qtyp: Proof.context -> typ list -> typ -> typ
    1.12 +  val derive_qtrm: Proof.context -> typ list -> term -> term
    1.13 +  val derive_rtyp: Proof.context -> typ list -> typ -> typ
    1.14 +  val derive_rtrm: Proof.context -> typ list -> term -> term
    1.15  end;
    1.16  
    1.17  structure Quotient_Term: QUOTIENT_TERM =
    1.18 @@ -498,7 +498,7 @@
    1.19           else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
    1.20         end
    1.21  
    1.22 -  | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
    1.23 +  | (Const (@{const_name Ball}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
    1.24       Const (@{const_name All}, ty') $ t') =>
    1.25         let
    1.26           val subtrm = apply_subt (regularize_trm ctxt) (t, t')
    1.27 @@ -509,7 +509,7 @@
    1.28           else mk_ball $ (mk_resp $ resrel) $ subtrm
    1.29         end
    1.30  
    1.31 -  | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
    1.32 +  | (Const (@{const_name Bex}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
    1.33       Const (@{const_name Ex}, ty') $ t') =>
    1.34         let
    1.35           val subtrm = apply_subt (regularize_trm ctxt) (t, t')
    1.36 @@ -520,7 +520,7 @@
    1.37           else mk_bex $ (mk_resp $ resrel) $ subtrm
    1.38         end
    1.39  
    1.40 -  | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') =>
    1.41 +  | (Const (@{const_name Bex1_rel}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') =>
    1.42         let
    1.43           val subtrm = apply_subt (regularize_trm ctxt) (t, t')
    1.44           val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
    1.45 @@ -638,18 +638,18 @@
    1.46     as the type of subterms needs to be calculated   *)
    1.47  fun inj_repabs_trm ctxt (rtrm, qtrm) =
    1.48   case (rtrm, qtrm) of
    1.49 -    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name All}, _) $ t') =>
    1.50 -       Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
    1.51 +    (Const (@{const_name Ball}, T) $ r $ t, Const (@{const_name All}, _) $ t') =>
    1.52 +       Const (@{const_name Ball}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
    1.53  
    1.54 -  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name Ex}, _) $ t') =>
    1.55 -       Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
    1.56 +  | (Const (@{const_name Bex}, T) $ r $ t, Const (@{const_name Ex}, _) $ t') =>
    1.57 +       Const (@{const_name Bex}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
    1.58  
    1.59 -  | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
    1.60 +  | (Const (@{const_name Babs}, T) $ r $ t, t' as (Abs _)) =>
    1.61        let
    1.62          val rty = fastype_of rtrm
    1.63          val qty = fastype_of qtrm
    1.64        in
    1.65 -        mk_repabs ctxt (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm ctxt (t, t')))
    1.66 +        mk_repabs ctxt (rty, qty) (Const (@{const_name Babs}, T) $ r $ (inj_repabs_trm ctxt (t, t')))
    1.67        end
    1.68  
    1.69    | (Abs (x, T, t), Abs (x', T', t')) =>
    1.70 @@ -767,19 +767,19 @@
    1.71  (* derives a qtyp and qtrm out of a rtyp and rtrm,
    1.72     respectively 
    1.73  *)
    1.74 -fun derive_qtyp qtys rty ctxt =
    1.75 +fun derive_qtyp ctxt qtys rty =
    1.76    subst_typ ctxt (mk_ty_subst qtys false ctxt) rty
    1.77  
    1.78 -fun derive_qtrm qtys rtrm ctxt =
    1.79 +fun derive_qtrm ctxt qtys rtrm =
    1.80    subst_trm ctxt (mk_ty_subst qtys false ctxt) (mk_trm_subst qtys false ctxt) rtrm
    1.81  
    1.82  (* derives a rtyp and rtrm out of a qtyp and qtrm,
    1.83     respectively 
    1.84  *)
    1.85 -fun derive_rtyp qtys qty ctxt =
    1.86 +fun derive_rtyp ctxt qtys qty =
    1.87    subst_typ ctxt (mk_ty_subst qtys true ctxt) qty
    1.88  
    1.89 -fun derive_rtrm qtys qtrm ctxt =
    1.90 +fun derive_rtrm ctxt qtys qtrm =
    1.91    subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm
    1.92  
    1.93