tuned signature;
authorwenzelm
Fri, 26 Jul 2019 14:43:56 +0200
changeset 70602 eb6ff14767cd
parent 70601 5be1da847b24
child 70603 d23cfb85438a
tuned signature;
src/HOL/Tools/rewrite_hol_proof.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Proof/reconstruct.ML
src/Pure/proofterm.ML
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Fri Jul 26 14:27:46 2019 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Fri Jul 26 14:43:56 2019 +0200
@@ -317,7 +317,7 @@
   | make_subst Ts prf xs (f, ((x, y), (prf', clprf)) :: ps) =
       let val T = fastype_of1 (Ts, x)
       in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps)
-        else Proofterm.change_type (SOME [T]) subst_prf %> x %> y %>
+        else Proofterm.change_types (SOME [T]) subst_prf %> x %> y %>
           Abs ("z", T, list_comb (incr_boundvars 1 f,
             map (incr_boundvars 1) xs @ Bound 0 ::
             map (incr_boundvars 1 o snd o fst) ps)) %% clprf %% prf' %%
@@ -326,7 +326,7 @@
 
 fun make_sym Ts ((x, y), (prf, clprf)) =
   ((y, x),
-    (Proofterm.change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf));
+    (Proofterm.change_types (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf));
 
 fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
 
--- a/src/Pure/Proof/extraction.ML	Fri Jul 26 14:27:46 2019 +0200
+++ b/src/Pure/Proof/extraction.ML	Fri Jul 26 14:43:56 2019 +0200
@@ -116,7 +116,7 @@
 
   in rew end;
 
-val chtype = Proofterm.change_type o SOME;
+val chtypes = Proofterm.change_types o SOME;
 
 fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
 fun corr_name s vs = extr_name s vs ^ "_correctness";
@@ -731,10 +731,10 @@
                       (Abs ("x", T, rlz $ list_comb (Bound 0, args') $ prop));
 
                     val corr_prf' = mkabsp shyps
-                      (chtype [] Proofterm.equal_elim_axm %> lhs %> rhs %%
-                       (chtype [propT] Proofterm.symmetric_axm %> rhs %> lhs %%
-                         (chtype [T, propT] Proofterm.combination_axm %> f %> f %> c %> t' %%
-                           (chtype [T --> propT] Proofterm.reflexive_axm %> f) %%
+                      (chtypes [] Proofterm.equal_elim_axm %> lhs %> rhs %%
+                       (chtypes [propT] Proofterm.symmetric_axm %> rhs %> lhs %%
+                         (chtypes [T, propT] Proofterm.combination_axm %> f %> f %> c %> t' %%
+                           (chtypes [T --> propT] Proofterm.reflexive_axm %> f) %%
                            PAxm (Thm.def_name cname, eqn,
                              SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
                     val corr_prop = Reconstruct.prop_of corr_prf';
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Jul 26 14:27:46 2019 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Jul 26 14:43:56 2019 +0200
@@ -243,7 +243,7 @@
                 (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
                 map the ts);
             in
-              (Proofterm.change_type (SOME [fastype_of1 (Ts, rhs')])
+              (Proofterm.change_types (SOME [fastype_of1 (Ts, rhs')])
                 Proofterm.reflexive_axm %> rhs', true)
             end
           else (prf, false)
--- a/src/Pure/Proof/proof_syntax.ML	Fri Jul 26 14:27:46 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Jul 26 14:43:56 2019 +0200
@@ -91,7 +91,7 @@
 
     fun prf_of [] (Bound i) = PBound i
       | prf_of Ts (Const (s, Type ("Pure.proof", _))) =
-          Proofterm.change_type (if ty then SOME Ts else NONE)
+          Proofterm.change_types (if ty then SOME Ts else NONE)
             (case Long_Name.explode s of
                "axm" :: xs =>
                  let
@@ -111,7 +111,7 @@
       | prf_of Ts (Const ("Pure.OfClass", _) $ Const (c_class, _)) =
           (case try Logic.class_of_const c_class of
             SOME c =>
-              Proofterm.change_type (if ty then SOME Ts else NONE)
+              Proofterm.change_types (if ty then SOME Ts else NONE)
                 (OfClass (TVar ((Name.aT, 0), []), c))
           | NONE => error ("Bad class constant: " ^ quote c_class))
       | prf_of Ts (Const ("Pure.Hyp", _) $ prop) = Hyp prop
--- a/src/Pure/Proof/reconstruct.ML	Fri Jul 26 14:27:46 2019 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Fri Jul 26 14:43:56 2019 +0200
@@ -135,7 +135,7 @@
             val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
               (Proofterm.forall_intr_vfs prop) handle ListPair.UnequalLengths =>
                 error ("Wrong number of type arguments for " ^ quote (Proofterm.guess_name prf))
-          in (prop', Proofterm.change_type (SOME Ts) prf, [], env', vTs) end;
+          in (prop', Proofterm.change_types (SOME Ts) prf, [], env', vTs) end;
 
     fun head_norm (prop, prf, cnstrts, env, vTs) =
       (Envir.head_norm env prop, prf, cnstrts, env, vTs);
--- a/src/Pure/proofterm.ML	Fri Jul 26 14:27:46 2019 +0200
+++ b/src/Pure/proofterm.ML	Fri Jul 26 14:43:56 2019 +0200
@@ -81,7 +81,7 @@
   val fold_proof_terms: (term -> 'a -> 'a) -> (typ -> 'a -> 'a) -> proof -> 'a -> 'a
   val maxidx_proof: proof -> int -> int
   val size_of_proof: proof -> int
-  val change_type: typ list option -> proof -> proof
+  val change_types: typ list option -> proof -> proof
   val prf_abstract_over: term -> proof -> proof
   val prf_incr_bv: int -> int -> int -> int -> proof -> proof
   val incr_pboundvars: int -> int -> proof -> proof
@@ -487,12 +487,12 @@
   | size_of_proof (prf1 %% prf2) = size_of_proof prf1 + size_of_proof prf2
   | size_of_proof _ = 1;
 
-fun change_type opTs (PAxm (name, prop, _)) = PAxm (name, prop, opTs)
-  | change_type (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
-  | change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs)
-  | change_type opTs (PThm (i, ((name, prop, _, open_proof), body))) =
-      PThm (i, ((name, prop, opTs, open_proof), body))
-  | change_type _ prf = prf;
+fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types)
+  | change_types (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
+  | change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types)
+  | change_types types (PThm (i, ((name, prop, _, open_proof), body))) =
+      PThm (i, ((name, prop, types, open_proof), body))
+  | change_types _ prf = prf;
 
 
 (* utilities *)