# HG changeset patch # User Christian Urban # Date 1282445153 -28800 # Node ID 9bb0016f7e60714e9d1c1c565274d7562e4edf7a # Parent 08a789ef80448dbbf6242c341664f89b80d9da7b changed to a more convenient argument order diff -r 08a789ef8044 -r 9bb0016f7e60 src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Aug 20 20:29:50 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Sun Aug 22 10:45:53 2010 +0800 @@ -92,7 +92,7 @@ fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt = let val rty = fastype_of rconst - val qty = derive_qtyp qtys rty ctxt + val qty = derive_qtyp ctxt qtys rty val lhs = Free (qconst_name, qty) in quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt diff -r 08a789ef8044 -r 9bb0016f7e60 src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Aug 20 20:29:50 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Aug 22 10:45:53 2010 +0800 @@ -18,7 +18,7 @@ val lift_procedure_tac: Proof.context -> thm -> int -> tactic val lift_tac: Proof.context -> thm list -> int -> tactic - val lifted: typ list -> Proof.context -> thm -> thm + val lifted: Proof.context -> typ list -> thm -> thm val lifted_attrib: attribute end; @@ -627,7 +627,7 @@ THEN' SUBGOAL (fn (goal, i) => let val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt) - val rtrm = derive_rtrm qtys goal ctxt + val rtrm = derive_rtrm ctxt qtys goal val rule = procedure_inst ctxt rtrm goal in rtac rule i @@ -674,15 +674,15 @@ end -(** lifting as attribute **) +(** lifting as an attribute **) -fun lifted qtys ctxt thm = +fun lifted ctxt qtys thm = let (* When the theorem is atomized, eta redexes are contracted, so we do it both in the original theorem *) val thm' = Drule.eta_contraction_rule thm val ((_, [thm'']), ctxt') = Variable.import false [thm'] ctxt - val goal = derive_qtrm qtys (prop_of thm'') ctxt' + val goal = derive_qtrm ctxt qtys (prop_of thm'') in Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm'] 1)) |> singleton (ProofContext.export ctxt' ctxt) @@ -693,7 +693,7 @@ val ctxt = Context.proof_of context val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt) in - lifted qtys ctxt + lifted ctxt qtys end) end; (* structure *) diff -r 08a789ef8044 -r 9bb0016f7e60 src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Aug 20 20:29:50 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Sun Aug 22 10:45:53 2010 +0800 @@ -26,10 +26,10 @@ val inj_repabs_trm: Proof.context -> term * term -> term val inj_repabs_trm_chk: Proof.context -> term * term -> term - val derive_qtyp: typ list -> typ -> Proof.context -> typ - val derive_qtrm: typ list -> term -> Proof.context -> term - val derive_rtyp: typ list -> typ -> Proof.context -> typ - val derive_rtrm: typ list -> term -> Proof.context -> term + val derive_qtyp: Proof.context -> typ list -> typ -> typ + val derive_qtrm: Proof.context -> typ list -> term -> term + val derive_rtyp: Proof.context -> typ list -> typ -> typ + val derive_rtrm: Proof.context -> typ list -> term -> term end; structure Quotient_Term: QUOTIENT_TERM = @@ -498,7 +498,7 @@ else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm end - | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, + | (Const (@{const_name Ball}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t, Const (@{const_name All}, ty') $ t') => let val subtrm = apply_subt (regularize_trm ctxt) (t, t') @@ -509,7 +509,7 @@ else mk_ball $ (mk_resp $ resrel) $ subtrm end - | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, + | (Const (@{const_name Bex}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t, Const (@{const_name Ex}, ty') $ t') => let val subtrm = apply_subt (regularize_trm ctxt) (t, t') @@ -520,7 +520,7 @@ else mk_bex $ (mk_resp $ resrel) $ subtrm end - | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') => + | (Const (@{const_name Bex1_rel}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') => let val subtrm = apply_subt (regularize_trm ctxt) (t, t') val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') @@ -638,18 +638,18 @@ as the type of subterms needs to be calculated *) fun inj_repabs_trm ctxt (rtrm, qtrm) = case (rtrm, qtrm) of - (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name All}, _) $ t') => - Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t')) + (Const (@{const_name Ball}, T) $ r $ t, Const (@{const_name All}, _) $ t') => + Const (@{const_name Ball}, T) $ r $ (inj_repabs_trm ctxt (t, t')) - | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name Ex}, _) $ t') => - Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm ctxt (t, t')) + | (Const (@{const_name Bex}, T) $ r $ t, Const (@{const_name Ex}, _) $ t') => + Const (@{const_name Bex}, T) $ r $ (inj_repabs_trm ctxt (t, t')) - | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) => + | (Const (@{const_name Babs}, T) $ r $ t, t' as (Abs _)) => let val rty = fastype_of rtrm val qty = fastype_of qtrm in - mk_repabs ctxt (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))) + mk_repabs ctxt (rty, qty) (Const (@{const_name Babs}, T) $ r $ (inj_repabs_trm ctxt (t, t'))) end | (Abs (x, T, t), Abs (x', T', t')) => @@ -767,19 +767,19 @@ (* derives a qtyp and qtrm out of a rtyp and rtrm, respectively *) -fun derive_qtyp qtys rty ctxt = +fun derive_qtyp ctxt qtys rty = subst_typ ctxt (mk_ty_subst qtys false ctxt) rty -fun derive_qtrm qtys rtrm ctxt = +fun derive_qtrm ctxt qtys rtrm = subst_trm ctxt (mk_ty_subst qtys false ctxt) (mk_trm_subst qtys false ctxt) rtrm (* derives a rtyp and rtrm out of a qtyp and qtrm, respectively *) -fun derive_rtyp qtys qty ctxt = +fun derive_rtyp ctxt qtys qty = subst_typ ctxt (mk_ty_subst qtys true ctxt) qty -fun derive_rtrm qtys qtrm ctxt = +fun derive_rtrm ctxt qtys qtrm = subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm