# HG changeset patch
# User berghofe
# Date 1002731872 -7200
# Node ID 592923615f77328878e419b61b6d9d51ddaf5b59
# Parent  bc0a84063a9c5382c4f8fe7667e003762e735f10
Tuned several functions to improve sharing of unchanged subproofs.

diff -r bc0a84063a9c -r 592923615f77 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Oct 09 18:11:07 2001 +0200
+++ b/src/Pure/proofterm.ML	Wed Oct 10 18:37:52 2001 +0200
@@ -110,6 +110,8 @@
 structure Proofterm : PROOFTERM =
 struct
 
+open Envir;
+
 datatype proof =
    PBound of int
  | Abst of string * typ option * proof
@@ -218,13 +220,31 @@
 val mk_Abst = foldr (fn ((s, T:typ), prf) => Abst (s, None, prf));
 fun mk_AbsP (i, prf) = funpow i (fn prf => AbsP ("H", None, prf)) prf;
 
-fun map_proof_terms f g (Abst (s, T, prf)) = Abst (s, apsome g T, map_proof_terms f g prf)
-  | map_proof_terms f g (AbsP (s, t, prf)) = AbsP (s, apsome f t, map_proof_terms f g prf)
-  | map_proof_terms f g (prf % t) = map_proof_terms f g prf % apsome f t
-  | map_proof_terms f g (prf1 %% prf2) = map_proof_terms f g prf1 %% map_proof_terms f g prf2
-  | map_proof_terms _ g (PThm (a, prf, prop, Some Ts)) = PThm (a, prf, prop, Some (map g Ts))
-  | map_proof_terms _ g (PAxm (a, prop, Some Ts)) = PAxm (a, prop, Some (map g Ts))
-  | map_proof_terms _ _ prf = prf;
+fun apsome' f None = raise SAME
+  | apsome' f (Some x) = Some (f x);
+
+fun same f x =
+  let val x' = f x
+  in if x = x' then raise SAME else x' end;
+
+fun map_proof_terms f g =
+  let
+    fun mapp (Abst (s, T, prf)) = (Abst (s, apsome' (same g) T, mapph prf)
+          handle SAME => Abst (s, T, mapp prf))
+      | mapp (AbsP (s, t, prf)) = (AbsP (s, apsome' (same f) t, mapph prf)
+          handle SAME => AbsP (s, t, mapp prf))
+      | mapp (prf % t) = (mapp prf % apsome f t
+          handle SAME => prf % apsome' (same f) t)
+      | mapp (prf1 %% prf2) = (mapp prf1 %% mapph prf2
+          handle SAME => prf1 %% mapp prf2)
+      | mapp (PThm (a, prf, prop, Some Ts)) =
+          PThm (a, prf, prop, Some (same (map g) Ts))
+      | mapp (PAxm (a, prop, Some Ts)) =
+          PAxm (a, prop, Some (same (map g) Ts))
+      | mapp _ = raise SAME
+    and mapph prf = (mapp prf handle SAME => prf)
+
+  in mapph end;
 
 fun fold_proof_terms f g (a, Abst (_, Some T, prf)) = fold_proof_terms f g (g (T, a), prf)
   | fold_proof_terms f g (a, Abst (_, None, prf)) = fold_proof_terms f g (a, prf)
@@ -257,15 +277,25 @@
 
 fun prf_abstract_over v =
   let
-    fun abst' Ts t = strip_abs Ts (abstract_over (v, mk_abs Ts t));
+    fun abst' lev u = if v aconv u then Bound lev else
+      (case u of
+         Abs (a, T, t) => Abs (a, T, abst' (lev + 1) t)
+       | f $ t => (abst' lev f $ absth' lev t handle SAME => f $ abst' lev t)
+       | _ => raise SAME)
+    and absth' lev t = (abst' lev t handle SAME => t);
 
-    fun abst Ts (AbsP (a, t, prf)) = AbsP (a, apsome (abst' Ts) t, abst Ts prf)
-      | abst Ts (Abst (a, T, prf)) = Abst (a, T, abst (dummyT::Ts) prf)
-      | abst Ts (prf1 %% prf2) = abst Ts prf1 %% abst Ts prf2
-      | abst Ts (prf % t) = abst Ts prf % apsome (abst' Ts) t
-      | abst _ prf = prf
+    fun abst lev (AbsP (a, t, prf)) =
+          (AbsP (a, apsome' (abst' lev) t, absth lev prf)
+           handle SAME => AbsP (a, t, abst lev prf))
+      | abst lev (Abst (a, T, prf)) = Abst (a, T, abst (lev + 1) prf)
+      | abst lev (prf1 %% prf2) = (abst lev prf1 %% absth lev prf2
+          handle SAME => prf1 %% abst lev prf2)
+      | abst lev (prf % t) = (abst lev prf % apsome (absth' lev) t
+          handle SAME => prf % apsome' (abst' lev) t)
+      | abst _ _ = raise SAME
+    and absth lev prf = (abst lev prf handle SAME => prf)
 
-  in abst [] end;
+  in absth 0 end;
 
 
 (*increments a proof term's non-local bound variables
@@ -275,16 +305,23 @@
 
 fun incr_bv' inct tlev t = incr_bv (inct, tlev, t);
 
-fun prf_incr_bv incP inct Plev tlev (u as PBound i) = if i>=Plev then PBound(i+incP) else u 
-  | prf_incr_bv incP inct Plev tlev (AbsP (a, t, body)) =
-      AbsP (a, apsome (incr_bv' inct tlev) t, prf_incr_bv incP inct (Plev+1) tlev body)
-  | prf_incr_bv incP inct Plev tlev (Abst (a, T, body)) =
-      Abst (a, T, prf_incr_bv incP inct Plev (tlev+1) body)
-  | prf_incr_bv incP inct Plev tlev (prf %% prf') = 
-      prf_incr_bv incP inct Plev tlev prf %% prf_incr_bv incP inct Plev tlev prf'
-  | prf_incr_bv incP inct Plev tlev (prf % t) = 
-      prf_incr_bv incP inct Plev tlev prf % apsome (incr_bv' inct tlev) t
-  | prf_incr_bv _ _ _ _ prf = prf;
+fun prf_incr_bv' incP inct Plev tlev (PBound i) =
+      if i >= Plev then PBound (i+incP) else raise SAME 
+  | prf_incr_bv' incP inct Plev tlev (AbsP (a, t, body)) =
+      (AbsP (a, apsome' (same (incr_bv' inct tlev)) t,
+         prf_incr_bv incP inct (Plev+1) tlev body) handle SAME =>
+           AbsP (a, t, prf_incr_bv' incP inct (Plev+1) tlev body))
+  | prf_incr_bv' incP inct Plev tlev (Abst (a, T, body)) =
+      Abst (a, T, prf_incr_bv' incP inct Plev (tlev+1) body)
+  | prf_incr_bv' incP inct Plev tlev (prf %% prf') = 
+      (prf_incr_bv' incP inct Plev tlev prf %% prf_incr_bv incP inct Plev tlev prf'
+       handle SAME => prf %% prf_incr_bv' incP inct Plev tlev prf')
+  | prf_incr_bv' incP inct Plev tlev (prf % t) = 
+      (prf_incr_bv' incP inct Plev tlev prf % apsome (incr_bv' inct tlev) t
+       handle SAME => prf % apsome' (same (incr_bv' inct tlev)) t)
+  | prf_incr_bv' _ _ _ _ _ = raise SAME
+and prf_incr_bv incP inct Plev tlev prf =
+      (prf_incr_bv' incP inct Plev tlev prf handle SAME => prf);
 
 fun incr_pboundvars  0 0 prf = prf
   | incr_pboundvars incP inct prf = prf_incr_bv incP inct 0 0 prf;
@@ -308,11 +345,6 @@
 
 (**** substitutions ****)
 
-local open Envir in
-
-fun apsome' f None = raise SAME
-  | apsome' f (Some x) = Some (f x);
-
 fun norm_proof env =
   let
     fun norm (Abst (s, T, prf)) = (Abst (s, apsome' (norm_type_same env) T, normh prf)
@@ -383,8 +415,6 @@
     and substh prf Plev tlev = (subst prf Plev tlev handle SAME => prf)
   in case args of [] => prf | _ => substh prf 0 0 end;
 
-end;
-
 
 (**** Freezing and thawing of variables in proof terms ****)
 
@@ -446,14 +476,16 @@
 
 fun implies_intr_proof h prf =
   let
-    fun abshyp i (Hyp t) = if h aconv t then PBound i else Hyp t
+    fun abshyp i (Hyp t) = if h aconv t then PBound i else raise SAME
       | abshyp i (Abst (s, T, prf)) = Abst (s, T, abshyp i prf)
       | abshyp i (AbsP (s, t, prf)) = AbsP (s, t, abshyp (i+1) prf)
       | abshyp i (prf % t) = abshyp i prf % t
-      | abshyp i (prf1 %% prf2) = abshyp i prf1 %% abshyp i prf2
-      | abshyp _ prf = prf;
+      | abshyp i (prf1 %% prf2) = (abshyp i prf1 %% abshyph i prf2
+          handle SAME => prf1 %% abshyp i prf2)
+      | abshyp _ _ = raise SAME
+    and abshyph i prf = (abshyp i prf handle SAME => prf)
   in
-    AbsP ("H", None (*h*), abshyp 0 prf)
+    AbsP ("H", None (*h*), abshyph 0 prf)
   end;
 
 
@@ -545,13 +577,22 @@
 
     fun lift'' Us Ts t = strip_abs Ts (Logic.incr_indexes (Us, inc) (mk_abs Ts t));
 
-    fun lift' Us Ts (Abst (s, T, prf)) = Abst (s, apsome (incr_tvar inc) T, lift' Us (dummyT::Ts) prf)
-      | lift' Us Ts (AbsP (s, t, prf)) = AbsP (s, apsome (lift'' Us Ts) t, lift' Us Ts prf)
-      | lift' Us Ts (prf % t) = lift' Us Ts prf % apsome (lift'' Us Ts) t
-      | lift' Us Ts (prf1 %% prf2) = lift' Us Ts prf1 %% lift' Us Ts prf2
-      | lift' _ _ (PThm (s, prf, prop, Ts)) = PThm (s, prf, prop, apsome (map (incr_tvar inc)) Ts)
-      | lift' _ _ (PAxm (s, prop, Ts)) = PAxm (s, prop, apsome (map (incr_tvar inc)) Ts)
-      | lift' _ _ prf = prf;
+    fun lift' Us Ts (Abst (s, T, prf)) =
+          (Abst (s, apsome' (same (incr_tvar inc)) T, lifth' Us (dummyT::Ts) prf)
+           handle SAME => Abst (s, T, lift' Us (dummyT::Ts) prf))
+      | lift' Us Ts (AbsP (s, t, prf)) =
+          (AbsP (s, apsome' (same (lift'' Us Ts)) t, lifth' Us Ts prf)
+           handle SAME => AbsP (s, t, lift' Us Ts prf))
+      | lift' Us Ts (prf % t) = (lift' Us Ts prf % apsome (lift'' Us Ts) t
+          handle SAME => prf % apsome' (same (lift'' Us Ts)) t)
+      | lift' Us Ts (prf1 %% prf2) = (lift' Us Ts prf1 %% lifth' Us Ts prf2
+          handle SAME => prf1 %% lift' Us Ts prf2)
+      | lift' _ _ (PThm (s, prf, prop, Ts)) =
+          PThm (s, prf, prop, apsome' (same (map (incr_tvar inc))) Ts)
+      | lift' _ _ (PAxm (s, prop, Ts)) =
+          PAxm (s, prop, apsome' (same (map (incr_tvar inc))) Ts)
+      | lift' _ _ _ = raise SAME
+    and lifth' Us Ts prf = (lift' Us Ts prf handle SAME => prf);
 
     val ps = map lift_all (Logic.strip_imp_prems (snd (Logic.strip_flexpairs prop)));
     val k = length ps;
@@ -563,7 +604,7 @@
 	    AbsP ("H", None (*A*), lift Us (true::bs) (i+1) j B)
       | lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) = 
 	    Abst (a, None (*T*), lift (T::Us) (false::bs) i (j+1) t)
-      | lift Us bs i j _ = proof_combP (lift' (rev Us) [] prf,
+      | lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf,
             map (fn k => (#3 (foldr mk_app (bs, (i-1, j-1, PBound k)))))
               (i + k - 1 downto i));
   in
@@ -945,7 +986,7 @@
 fun rewrite_proof tsig = rewrite_prf (fn (tab, f) =>
   Type.typ_match tsig (tab, f ()) handle Type.TYPE_MATCH => raise PMatch);
 
-fun rewrite_proof_notypes tsig = rewrite_prf fst tsig;
+fun rewrite_proof_notypes rews = rewrite_prf fst rews;
 
 (**** theory data ****)