# HG changeset patch
# User wenzelm
# Date 1570712028 -7200
# Node ID 22e2f5acc0b4439835537b17beaa2fae56f34f09
# Parent  37062fe191758c7e3fd7f052a85359e948a06410
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;

diff -r 37062fe19175 -r 22e2f5acc0b4 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Oct 10 11:04:27 2019 +0200
+++ b/src/Pure/proofterm.ML	Thu Oct 10 14:53:48 2019 +0200
@@ -109,7 +109,7 @@
   val forall_intr_proof': term -> proof -> proof
   val varify_proof: term -> (string * sort) list -> proof -> proof
   val legacy_freezeT: term -> proof -> proof
-  val rotate_proof: term list -> term -> int -> proof -> proof
+  val rotate_proof: term list -> term -> (string * typ) list -> term list -> int -> proof -> proof
   val permute_prems_proof: term list -> int -> int -> proof -> proof
   val generalize: string list * string list -> int -> proof -> proof
   val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
@@ -117,7 +117,7 @@
   val lift_proof: term -> int -> term -> proof -> proof
   val incr_indexes: int -> proof -> proof
   val assumption_proof: term list -> term -> int -> proof -> proof
-  val bicompose_proof: bool -> term list -> term list -> term list -> term option ->
+  val bicompose_proof: bool -> term list -> term list -> term option -> term list ->
     int -> int -> proof -> proof -> proof
   val equality_axms: (string * term) list
   val reflexive_axm: proof
@@ -455,8 +455,8 @@
     PThm (_, Thm_Body {body = body', ...}) => Future.join body'
   | _ => body);
 
-val mk_Abst = fold_rev (fn (s, _: typ) => fn prf => Abst (s, NONE, prf));
-fun mk_AbsP (i, prf) = funpow i (fn prf => AbsP ("H", NONE, prf)) prf;
+val mk_Abst = fold_rev (fn (x, _: typ) => fn prf => Abst (x, NONE, prf));
+val mk_AbsP = fold_rev (fn _: term => fn prf => AbsP ("H", NONE, prf));
 
 fun map_proof_same term typ ofclass =
   let
@@ -921,26 +921,24 @@
 
 (* rotate assumptions *)
 
-fun rotate_proof Bs Bi m prf =
+fun rotate_proof Bs Bi' params asms m prf =
   let
-    val params = Term.strip_all_vars Bi;
-    val asms = Logic.strip_imp_prems (Term.strip_all_body Bi);
     val i = length asms;
     val j = length Bs;
   in
-    mk_AbsP (j+1, proof_combP (prf, map PBound
-      (j downto 1) @ [mk_Abst params (mk_AbsP (i,
-        proof_combP (proof_combt (PBound i, map Bound ((length params - 1) downto 0)),
+    mk_AbsP (Bs @ [Bi']) (proof_combP (prf, map PBound
+      (j downto 1) @ [mk_Abst params (mk_AbsP asms
+        (proof_combP (proof_combt (PBound i, map Bound ((length params - 1) downto 0)),
           map PBound (((i-m-1) downto 0) @ ((i-1) downto (i-m))))))]))
   end;
 
 
 (* permute premises *)
 
-fun permute_prems_proof prems j k prf =
-  let val n = length prems
-  in mk_AbsP (n, proof_combP (prf,
-    map PBound ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k))))
+fun permute_prems_proof prems' j k prf =
+  let val n = length prems' in
+    mk_AbsP prems'
+      (proof_combP (prf, map PBound ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k))))
   end;
 
 
@@ -1003,7 +1001,7 @@
             map (fn k => (#3 (fold_rev mk_app bs (i-1, j-1, PBound k))))
               (i + k - 1 downto i));
   in
-    mk_AbsP (k, lift [] [] 0 0 Bi)
+    mk_AbsP ps (lift [] [] 0 0 Bi)
   end;
 
 fun incr_indexes i =
@@ -1023,8 +1021,7 @@
   in all_prf t end;
 
 fun assumption_proof Bs Bi n prf =
-  mk_AbsP (length Bs, proof_combP (prf,
-    map PBound (length Bs - 1 downto 0) @ [mk_asm_prf Bi n ~1]));
+  mk_AbsP Bs (proof_combP (prf, map PBound (length Bs - 1 downto 0) @ [mk_asm_prf Bi n ~1]));
 
 
 (* composition of object rule with proof state *)
@@ -1036,12 +1033,12 @@
   | flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i),
       map Bound (j-1 downto 0)), map PBound (remove (op =) (i-n) (i-1 downto 0)));
 
-fun bicompose_proof flatten Bs oldAs newAs A n m rprf sprf =
+fun bicompose_proof flatten Bs As A oldAs n m rprf sprf =
   let
-    val la = length newAs;
     val lb = length Bs;
+    val la = length As;
   in
-    mk_AbsP (lb+la, proof_combP (sprf,
+    mk_AbsP (Bs @ As) (proof_combP (sprf,
       map PBound (lb + la - 1 downto la)) %%
         proof_combP (rprf, (if n>0 then [mk_asm_prf (the A) n m] else []) @
           map (if flatten then flatten_params_proof 0 0 n else PBound o snd)
diff -r 37062fe19175 -r 22e2f5acc0b4 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Oct 10 11:04:27 2019 +0200
+++ b/src/Pure/thm.ML	Thu Oct 10 14:53:48 2019 +0200
@@ -1828,23 +1828,24 @@
     val (context, cert') = make_context_certificate [state] opt_ctxt cert;
     val (tpairs, Bs, Bi, C) = dest_state (state, i);
     fun newth n (env, tpairs) =
-      Thm (deriv_rule1
-          ((if Envir.is_empty env then I else Proofterm.norm_proof' env) o
-            Proofterm.assumption_proof Bs Bi n) der,
-       {tags = [],
-        maxidx = Envir.maxidx_of env,
-        constraints = insert_constraints_env (Context.certificate_theory cert') env constraints,
-        shyps = Envir.insert_sorts env shyps,
-        hyps = hyps,
-        tpairs =
-          if Envir.is_empty env then tpairs
-          else map (apply2 (Envir.norm_term env)) tpairs,
-        prop =
-          if Envir.is_empty env then (*avoid wasted normalizations*)
-            Logic.list_implies (Bs, C)
-          else (*normalize the new rule fully*)
-            Envir.norm_term env (Logic.list_implies (Bs, C)),
-        cert = cert'});
+      let
+        val normt = Envir.norm_term env;
+        fun assumption_proof prf =
+          Proofterm.assumption_proof (map normt Bs) (normt Bi) n prf
+          |> not (Envir.is_empty env) ? Proofterm.norm_proof' env;
+      in
+        Thm (deriv_rule1 assumption_proof der,
+         {tags = [],
+          maxidx = Envir.maxidx_of env,
+          constraints = insert_constraints_env (Context.certificate_theory cert') env constraints,
+          shyps = Envir.insert_sorts env shyps,
+          hyps = hyps,
+          tpairs = if Envir.is_empty env then tpairs else map (apply2 normt) tpairs,
+          prop =
+            if Envir.is_empty env then Logic.list_implies (Bs, C) (*avoid wasted normalizations*)
+            else normt (Logic.list_implies (Bs, C)) (*normalize the new rule fully*),
+          cert = cert'})
+      end;
 
     val (close, asms, concl) = Logic.assum_problems (~1, Bi);
     val concl' = close concl;
@@ -1898,7 +1899,7 @@
         in Logic.list_all (params, Logic.list_implies (qs @ ps, concl)) end
       else raise THM ("rotate_rule", k, [state]);
   in
-    Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi m) der,
+    Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi' params asms m) der,
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -1923,14 +1924,16 @@
       handle General.Subscript => raise THM ("permute_prems: j", j, [rl]);
     val n_j = length moved_prems;
     val m = if k < 0 then n_j + k else k;
-    val prop' =
-      if 0 = m orelse m = n_j then prop
+    val (prems', prop') =
+      if 0 = m orelse m = n_j then (prems, prop)
       else if 0 < m andalso m < n_j then
-        let val (ps, qs) = chop m moved_prems
-        in Logic.list_implies (fixed_prems @ qs @ ps, concl) end
+        let
+          val (ps, qs) = chop m moved_prems;
+          val prems' = fixed_prems @ qs @ ps;
+        in (prems', Logic.list_implies (prems', concl)) end
       else raise THM ("permute_prems: k", k, [rl]);
   in
-    Thm (deriv_rule1 (Proofterm.permute_prems_proof prems j m) der,
+    Thm (deriv_rule1 (Proofterm.permute_prems_proof prems' j m) der,
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -2079,14 +2082,16 @@
            val constraints' =
              union_constraints constraints1 constraints2
              |> insert_constraints_env (Context.certificate_theory cert) env;
+           fun bicompose_proof prf1 prf2 =
+             Proofterm.bicompose_proof flatten (map normt Bs) (map normt As) A oldAs n (nlift+1)
+               prf1 prf2
            val th =
              Thm (deriv_rule2
                    ((if Envir.is_empty env then I
                      else if Envir.above env smax then
                        (fn f => fn der => f (Proofterm.norm_proof' env der))
                      else
-                       curry op oo (Proofterm.norm_proof' env))
-                    (Proofterm.bicompose_proof flatten Bs oldAs As A n (nlift+1))) rder' sder,
+                       curry op oo (Proofterm.norm_proof' env)) bicompose_proof) rder' sder,
                 {tags = [],
                  maxidx = Envir.maxidx_of env,
                  constraints = constraints',