# HG changeset patch
# User wenzelm
# Date 1570654354 -7200
# Node ID a6644dfe8e260d70b6fe2b6074fa63a3595d353f
# Parent  83b7d1927fda0ce900cbf3ff7f6549d110581c52
misc tuning and clarification;

diff -r 83b7d1927fda -r a6644dfe8e26 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Oct 09 22:22:17 2019 +0200
+++ b/src/Pure/proofterm.ML	Wed Oct 09 22:52:34 2019 +0200
@@ -105,7 +105,7 @@
   (*proof terms for specific inference rules*)
   val implies_intr_proof: term -> proof -> proof
   val implies_intr_proof': term -> proof -> proof
-  val forall_intr_proof: term -> string -> proof -> proof
+  val forall_intr_proof: string * term -> typ option -> proof -> proof
   val forall_intr_proof': term -> proof -> proof
   val varify_proof: term -> (string * sort) list -> proof -> proof
   val legacy_freezeT: term -> proof -> proof
@@ -127,13 +127,13 @@
   val equal_elim_axm: proof
   val abstract_rule_axm: proof
   val combination_axm: proof
-  val reflexive: proof
-  val symmetric: proof -> proof
-  val transitive: term -> typ -> proof -> proof -> proof
-  val abstract_rule: term -> string -> proof -> proof
-  val combination: term -> term -> term -> term -> typ -> proof -> proof -> proof
-  val equal_intr: term -> term -> proof -> proof -> proof
-  val equal_elim: term -> term -> proof -> proof -> proof
+  val reflexive_proof: proof
+  val symmetric_proof: proof -> proof
+  val transitive_proof: typ -> term -> proof -> proof -> proof
+  val equal_intr_proof: term -> term -> proof -> proof -> proof
+  val equal_elim_proof: term -> term -> proof -> proof -> proof
+  val abstract_rule_proof: string * term -> proof -> proof
+  val combination_proof: typ -> term -> term -> term -> term -> proof -> proof -> proof
   val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list ->
     sort list -> proof -> proof
   val of_sort_proof: Sorts.algebra ->
@@ -868,11 +868,11 @@
 
 (* forall introduction *)
 
-fun forall_intr_proof x a prf = Abst (a, NONE, prf_abstract_over x prf);
+fun forall_intr_proof (a, v) opt_T prf = Abst (a, opt_T, prf_abstract_over v prf);
 
-fun forall_intr_proof' t prf =
-  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
-  in Abst (a, SOME T, prf_abstract_over t prf) end;
+fun forall_intr_proof' v prf =
+  let val (a, T) = (case v of Var ((a, _), T) => (a, T) | Free (a, T) => (a, T))
+  in forall_intr_proof (a, v) (SOME T) prf end;
 
 
 (* varify *)
@@ -1237,8 +1237,8 @@
   ("equal_elim", Logic.list_implies ([Logic.mk_equals (A, B), A], B)),
   ("abstract_rule",
     Logic.mk_implies
-      (Logic.all x
-        (Logic.mk_equals (f $ x, g $ x)), Logic.mk_equals (lambda x (f $ x), lambda x (g $ x)))),
+      (Logic.all x (Logic.mk_equals (f $ x, g $ x)),
+        Logic.mk_equals (lambda x (f $ x), lambda x (g $ x)))),
   ("combination", Logic.list_implies
     ([Logic.mk_equals (f, g), Logic.mk_equals (x, y)], Logic.mk_equals (f $ x, g $ y)))];
 
@@ -1246,19 +1246,28 @@
   equal_elim_axm, abstract_rule_axm, combination_axm] =
     map (fn (s, t) => PAxm ("Pure." ^ s, Logic.varify_global t, NONE)) equality_axms;
 
-val reflexive = reflexive_axm % NONE;
+val reflexive_proof = reflexive_axm % NONE;
+
+val is_reflexive_proof = fn PAxm ("Pure.reflexive", _, _) % _ => true | _ => false;
 
-fun symmetric (prf as PAxm ("Pure.reflexive", _, _) % _) = prf
-  | symmetric prf = symmetric_axm % NONE % NONE %% prf;
+fun symmetric_proof prf =
+  if is_reflexive_proof prf then prf
+  else symmetric_axm % NONE % NONE %% prf;
 
-fun transitive _ _ (PAxm ("Pure.reflexive", _, _) % _) prf2 = prf2
-  | transitive _ _ prf1 (PAxm ("Pure.reflexive", _, _) % _) = prf1
-  | transitive u (Type ("prop", [])) prf1 prf2 =
-      transitive_axm % NONE % SOME (remove_types u) % NONE %% prf1 %% prf2
-  | transitive _ _ prf1 prf2 = transitive_axm % NONE % NONE % NONE %% prf1 %% prf2;
+fun transitive_proof U u prf1 prf2 =
+  if is_reflexive_proof prf1 then prf2
+  else if is_reflexive_proof prf2 then prf1
+  else if U = propT then transitive_axm % NONE % SOME (remove_types u) % NONE %% prf1 %% prf2
+  else transitive_axm % NONE % NONE % NONE %% prf1 %% prf2;
 
-fun abstract_rule x a prf =
-  abstract_rule_axm % NONE % NONE %% forall_intr_proof x a prf;
+fun equal_intr_proof A B prf1 prf2 =
+  equal_intr_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
+
+fun equal_elim_proof A B prf1 prf2 =
+  equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
+
+fun abstract_rule_proof (a, x) prf =
+  abstract_rule_axm % NONE % NONE %% forall_intr_proof (a, x) NONE prf;
 
 fun check_comb (PAxm ("Pure.combination", _, _) % f % _ % _ % _ %% prf %% _) =
       is_some f orelse check_comb prf
@@ -1267,7 +1276,7 @@
   | check_comb (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf) = check_comb prf
   | check_comb _ = false;
 
-fun combination f g t u (Type (_, [T, U])) prf1 prf2 =
+fun combination_proof A f g t u prf1 prf2 =
   let
     val f = Envir.beta_norm f;
     val g = Envir.beta_norm g;
@@ -1280,7 +1289,7 @@
             combination_axm %> remove_types f % NONE
         | _ => combination_axm %> remove_types f %> remove_types g)
   in
-    (case T of
+    (case A of
       Type ("fun", _) => prf %
         (case head_of f of
           Abs _ => SOME (remove_types t)
@@ -1293,12 +1302,6 @@
      | _ => prf % NONE % NONE %% prf1 %% prf2)
   end;
 
-fun equal_intr A B prf1 prf2 =
-  equal_intr_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
-
-fun equal_elim A B prf1 prf2 =
-  equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
-
 
 
 (** rewriting on proof terms **)
diff -r 83b7d1927fda -r a6644dfe8e26 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Oct 09 22:22:17 2019 +0200
+++ b/src/Pure/thm.ML	Wed Oct 09 22:52:34 2019 +0200
@@ -1157,7 +1157,7 @@
     (th as Thm (der, {maxidx = maxidx2, constraints, shyps, hyps, tpairs, prop, ...})) =
   let
     fun result a =
-      Thm (deriv_rule1 (Proofterm.forall_intr_proof x a) der,
+      Thm (deriv_rule1 (Proofterm.forall_intr_proof (a, x) NONE) der,
        {cert = join_certificate1 (ct, th),
         tags = [],
         maxidx = Int.max (maxidx1, maxidx2),
@@ -1208,7 +1208,7 @@
   t \<equiv> t
 *)
 fun reflexive (Cterm {cert, t, T = _, maxidx, sorts}) =
-  Thm (deriv_rule0 (fn () => Proofterm.reflexive),
+  Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof),
    {cert = cert,
     tags = [],
     maxidx = maxidx,
@@ -1226,7 +1226,7 @@
 fun symmetric (th as Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) =
   (case prop of
     (eq as Const ("Pure.eq", _)) $ t $ u =>
-      Thm (deriv_rule1 Proofterm.symmetric der,
+      Thm (deriv_rule1 Proofterm.symmetric_proof der,
        {cert = cert,
         tags = [],
         maxidx = maxidx,
@@ -1251,10 +1251,10 @@
     fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]);
   in
     case (prop1, prop2) of
-      ((eq as Const ("Pure.eq", Type (_, [T, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) =>
+      ((eq as Const ("Pure.eq", Type (_, [U, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) =>
         if not (u aconv u') then err "middle term"
         else
-          Thm (deriv_rule2 (Proofterm.transitive u T) der1 der2,
+          Thm (deriv_rule2 (Proofterm.transitive_proof U u) der1 der2,
            {cert = join_certificate2 (th1, th2),
             tags = [],
             maxidx = Int.max (maxidx1, maxidx2),
@@ -1277,7 +1277,7 @@
       (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt)
       | _ => raise THM ("beta_conversion: not a redex", 0, []));
   in
-    Thm (deriv_rule0 (fn () => Proofterm.reflexive),
+    Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof),
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -1289,7 +1289,7 @@
   end;
 
 fun eta_conversion (Cterm {cert, t, T = _, maxidx, sorts}) =
-  Thm (deriv_rule0 (fn () => Proofterm.reflexive),
+  Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof),
    {cert = cert,
     tags = [],
     maxidx = maxidx,
@@ -1300,7 +1300,7 @@
     prop = Logic.mk_equals (t, Envir.eta_contract t)});
 
 fun eta_long_conversion (Cterm {cert, t, T = _, maxidx, sorts}) =
-  Thm (deriv_rule0 (fn () => Proofterm.reflexive),
+  Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof),
    {cert = cert,
     tags = [],
     maxidx = maxidx,
@@ -1323,7 +1323,7 @@
     val (t, u) = Logic.dest_equals prop
       handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]);
     val result =
-      Thm (deriv_rule1 (Proofterm.abstract_rule x a) der,
+      Thm (deriv_rule1 (Proofterm.abstract_rule_proof (a, x)) der,
        {cert = cert,
         tags = [],
         maxidx = maxidx,
@@ -1367,7 +1367,7 @@
       (Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g,
        Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) =>
         (chktypes fT tT;
-          Thm (deriv_rule2 (Proofterm.combination f g t u fT) der1 der2,
+          Thm (deriv_rule2 (Proofterm.combination_proof (domain_type fT) f g t u) der1 der2,
            {cert = join_certificate2 (th1, th2),
             tags = [],
             maxidx = Int.max (maxidx1, maxidx2),
@@ -1395,7 +1395,7 @@
     (case (prop1, prop2) of
       (Const("Pure.imp", _) $ A $ B, Const("Pure.imp", _) $ B' $ A') =>
         if A aconv A' andalso B aconv B' then
-          Thm (deriv_rule2 (Proofterm.equal_intr A B) der1 der2,
+          Thm (deriv_rule2 (Proofterm.equal_intr_proof A B) der1 der2,
            {cert = join_certificate2 (th1, th2),
             tags = [],
             maxidx = Int.max (maxidx1, maxidx2),
@@ -1424,7 +1424,7 @@
     (case prop1 of
       Const ("Pure.eq", _) $ A $ B =>
         if prop2 aconv A then
-          Thm (deriv_rule2 (Proofterm.equal_elim A B) der1 der2,
+          Thm (deriv_rule2 (Proofterm.equal_elim_proof A B) der1 der2,
            {cert = join_certificate2 (th1, th2),
             tags = [],
             maxidx = Int.max (maxidx1, maxidx2),