Tuned several functions to improve sharing of unchanged subproofs.
authorberghofe
Wed Oct 10 18:37:52 2001 +0200 (2001-10-10)
changeset 11715592923615f77
parent 11714 bc0a84063a9c
child 11716 064833efb479
Tuned several functions to improve sharing of unchanged subproofs.
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/proofterm.ML	Tue Oct 09 18:11:07 2001 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Wed Oct 10 18:37:52 2001 +0200
     1.3 @@ -110,6 +110,8 @@
     1.4  structure Proofterm : PROOFTERM =
     1.5  struct
     1.6  
     1.7 +open Envir;
     1.8 +
     1.9  datatype proof =
    1.10     PBound of int
    1.11   | Abst of string * typ option * proof
    1.12 @@ -218,13 +220,31 @@
    1.13  val mk_Abst = foldr (fn ((s, T:typ), prf) => Abst (s, None, prf));
    1.14  fun mk_AbsP (i, prf) = funpow i (fn prf => AbsP ("H", None, prf)) prf;
    1.15  
    1.16 -fun map_proof_terms f g (Abst (s, T, prf)) = Abst (s, apsome g T, map_proof_terms f g prf)
    1.17 -  | map_proof_terms f g (AbsP (s, t, prf)) = AbsP (s, apsome f t, map_proof_terms f g prf)
    1.18 -  | map_proof_terms f g (prf % t) = map_proof_terms f g prf % apsome f t
    1.19 -  | map_proof_terms f g (prf1 %% prf2) = map_proof_terms f g prf1 %% map_proof_terms f g prf2
    1.20 -  | map_proof_terms _ g (PThm (a, prf, prop, Some Ts)) = PThm (a, prf, prop, Some (map g Ts))
    1.21 -  | map_proof_terms _ g (PAxm (a, prop, Some Ts)) = PAxm (a, prop, Some (map g Ts))
    1.22 -  | map_proof_terms _ _ prf = prf;
    1.23 +fun apsome' f None = raise SAME
    1.24 +  | apsome' f (Some x) = Some (f x);
    1.25 +
    1.26 +fun same f x =
    1.27 +  let val x' = f x
    1.28 +  in if x = x' then raise SAME else x' end;
    1.29 +
    1.30 +fun map_proof_terms f g =
    1.31 +  let
    1.32 +    fun mapp (Abst (s, T, prf)) = (Abst (s, apsome' (same g) T, mapph prf)
    1.33 +          handle SAME => Abst (s, T, mapp prf))
    1.34 +      | mapp (AbsP (s, t, prf)) = (AbsP (s, apsome' (same f) t, mapph prf)
    1.35 +          handle SAME => AbsP (s, t, mapp prf))
    1.36 +      | mapp (prf % t) = (mapp prf % apsome f t
    1.37 +          handle SAME => prf % apsome' (same f) t)
    1.38 +      | mapp (prf1 %% prf2) = (mapp prf1 %% mapph prf2
    1.39 +          handle SAME => prf1 %% mapp prf2)
    1.40 +      | mapp (PThm (a, prf, prop, Some Ts)) =
    1.41 +          PThm (a, prf, prop, Some (same (map g) Ts))
    1.42 +      | mapp (PAxm (a, prop, Some Ts)) =
    1.43 +          PAxm (a, prop, Some (same (map g) Ts))
    1.44 +      | mapp _ = raise SAME
    1.45 +    and mapph prf = (mapp prf handle SAME => prf)
    1.46 +
    1.47 +  in mapph end;
    1.48  
    1.49  fun fold_proof_terms f g (a, Abst (_, Some T, prf)) = fold_proof_terms f g (g (T, a), prf)
    1.50    | fold_proof_terms f g (a, Abst (_, None, prf)) = fold_proof_terms f g (a, prf)
    1.51 @@ -257,15 +277,25 @@
    1.52  
    1.53  fun prf_abstract_over v =
    1.54    let
    1.55 -    fun abst' Ts t = strip_abs Ts (abstract_over (v, mk_abs Ts t));
    1.56 +    fun abst' lev u = if v aconv u then Bound lev else
    1.57 +      (case u of
    1.58 +         Abs (a, T, t) => Abs (a, T, abst' (lev + 1) t)
    1.59 +       | f $ t => (abst' lev f $ absth' lev t handle SAME => f $ abst' lev t)
    1.60 +       | _ => raise SAME)
    1.61 +    and absth' lev t = (abst' lev t handle SAME => t);
    1.62  
    1.63 -    fun abst Ts (AbsP (a, t, prf)) = AbsP (a, apsome (abst' Ts) t, abst Ts prf)
    1.64 -      | abst Ts (Abst (a, T, prf)) = Abst (a, T, abst (dummyT::Ts) prf)
    1.65 -      | abst Ts (prf1 %% prf2) = abst Ts prf1 %% abst Ts prf2
    1.66 -      | abst Ts (prf % t) = abst Ts prf % apsome (abst' Ts) t
    1.67 -      | abst _ prf = prf
    1.68 +    fun abst lev (AbsP (a, t, prf)) =
    1.69 +          (AbsP (a, apsome' (abst' lev) t, absth lev prf)
    1.70 +           handle SAME => AbsP (a, t, abst lev prf))
    1.71 +      | abst lev (Abst (a, T, prf)) = Abst (a, T, abst (lev + 1) prf)
    1.72 +      | abst lev (prf1 %% prf2) = (abst lev prf1 %% absth lev prf2
    1.73 +          handle SAME => prf1 %% abst lev prf2)
    1.74 +      | abst lev (prf % t) = (abst lev prf % apsome (absth' lev) t
    1.75 +          handle SAME => prf % apsome' (abst' lev) t)
    1.76 +      | abst _ _ = raise SAME
    1.77 +    and absth lev prf = (abst lev prf handle SAME => prf)
    1.78  
    1.79 -  in abst [] end;
    1.80 +  in absth 0 end;
    1.81  
    1.82  
    1.83  (*increments a proof term's non-local bound variables
    1.84 @@ -275,16 +305,23 @@
    1.85  
    1.86  fun incr_bv' inct tlev t = incr_bv (inct, tlev, t);
    1.87  
    1.88 -fun prf_incr_bv incP inct Plev tlev (u as PBound i) = if i>=Plev then PBound(i+incP) else u 
    1.89 -  | prf_incr_bv incP inct Plev tlev (AbsP (a, t, body)) =
    1.90 -      AbsP (a, apsome (incr_bv' inct tlev) t, prf_incr_bv incP inct (Plev+1) tlev body)
    1.91 -  | prf_incr_bv incP inct Plev tlev (Abst (a, T, body)) =
    1.92 -      Abst (a, T, prf_incr_bv incP inct Plev (tlev+1) body)
    1.93 -  | prf_incr_bv incP inct Plev tlev (prf %% prf') = 
    1.94 -      prf_incr_bv incP inct Plev tlev prf %% prf_incr_bv incP inct Plev tlev prf'
    1.95 -  | prf_incr_bv incP inct Plev tlev (prf % t) = 
    1.96 -      prf_incr_bv incP inct Plev tlev prf % apsome (incr_bv' inct tlev) t
    1.97 -  | prf_incr_bv _ _ _ _ prf = prf;
    1.98 +fun prf_incr_bv' incP inct Plev tlev (PBound i) =
    1.99 +      if i >= Plev then PBound (i+incP) else raise SAME 
   1.100 +  | prf_incr_bv' incP inct Plev tlev (AbsP (a, t, body)) =
   1.101 +      (AbsP (a, apsome' (same (incr_bv' inct tlev)) t,
   1.102 +         prf_incr_bv incP inct (Plev+1) tlev body) handle SAME =>
   1.103 +           AbsP (a, t, prf_incr_bv' incP inct (Plev+1) tlev body))
   1.104 +  | prf_incr_bv' incP inct Plev tlev (Abst (a, T, body)) =
   1.105 +      Abst (a, T, prf_incr_bv' incP inct Plev (tlev+1) body)
   1.106 +  | prf_incr_bv' incP inct Plev tlev (prf %% prf') = 
   1.107 +      (prf_incr_bv' incP inct Plev tlev prf %% prf_incr_bv incP inct Plev tlev prf'
   1.108 +       handle SAME => prf %% prf_incr_bv' incP inct Plev tlev prf')
   1.109 +  | prf_incr_bv' incP inct Plev tlev (prf % t) = 
   1.110 +      (prf_incr_bv' incP inct Plev tlev prf % apsome (incr_bv' inct tlev) t
   1.111 +       handle SAME => prf % apsome' (same (incr_bv' inct tlev)) t)
   1.112 +  | prf_incr_bv' _ _ _ _ _ = raise SAME
   1.113 +and prf_incr_bv incP inct Plev tlev prf =
   1.114 +      (prf_incr_bv' incP inct Plev tlev prf handle SAME => prf);
   1.115  
   1.116  fun incr_pboundvars  0 0 prf = prf
   1.117    | incr_pboundvars incP inct prf = prf_incr_bv incP inct 0 0 prf;
   1.118 @@ -308,11 +345,6 @@
   1.119  
   1.120  (**** substitutions ****)
   1.121  
   1.122 -local open Envir in
   1.123 -
   1.124 -fun apsome' f None = raise SAME
   1.125 -  | apsome' f (Some x) = Some (f x);
   1.126 -
   1.127  fun norm_proof env =
   1.128    let
   1.129      fun norm (Abst (s, T, prf)) = (Abst (s, apsome' (norm_type_same env) T, normh prf)
   1.130 @@ -383,8 +415,6 @@
   1.131      and substh prf Plev tlev = (subst prf Plev tlev handle SAME => prf)
   1.132    in case args of [] => prf | _ => substh prf 0 0 end;
   1.133  
   1.134 -end;
   1.135 -
   1.136  
   1.137  (**** Freezing and thawing of variables in proof terms ****)
   1.138  
   1.139 @@ -446,14 +476,16 @@
   1.140  
   1.141  fun implies_intr_proof h prf =
   1.142    let
   1.143 -    fun abshyp i (Hyp t) = if h aconv t then PBound i else Hyp t
   1.144 +    fun abshyp i (Hyp t) = if h aconv t then PBound i else raise SAME
   1.145        | abshyp i (Abst (s, T, prf)) = Abst (s, T, abshyp i prf)
   1.146        | abshyp i (AbsP (s, t, prf)) = AbsP (s, t, abshyp (i+1) prf)
   1.147        | abshyp i (prf % t) = abshyp i prf % t
   1.148 -      | abshyp i (prf1 %% prf2) = abshyp i prf1 %% abshyp i prf2
   1.149 -      | abshyp _ prf = prf;
   1.150 +      | abshyp i (prf1 %% prf2) = (abshyp i prf1 %% abshyph i prf2
   1.151 +          handle SAME => prf1 %% abshyp i prf2)
   1.152 +      | abshyp _ _ = raise SAME
   1.153 +    and abshyph i prf = (abshyp i prf handle SAME => prf)
   1.154    in
   1.155 -    AbsP ("H", None (*h*), abshyp 0 prf)
   1.156 +    AbsP ("H", None (*h*), abshyph 0 prf)
   1.157    end;
   1.158  
   1.159  
   1.160 @@ -545,13 +577,22 @@
   1.161  
   1.162      fun lift'' Us Ts t = strip_abs Ts (Logic.incr_indexes (Us, inc) (mk_abs Ts t));
   1.163  
   1.164 -    fun lift' Us Ts (Abst (s, T, prf)) = Abst (s, apsome (incr_tvar inc) T, lift' Us (dummyT::Ts) prf)
   1.165 -      | lift' Us Ts (AbsP (s, t, prf)) = AbsP (s, apsome (lift'' Us Ts) t, lift' Us Ts prf)
   1.166 -      | lift' Us Ts (prf % t) = lift' Us Ts prf % apsome (lift'' Us Ts) t
   1.167 -      | lift' Us Ts (prf1 %% prf2) = lift' Us Ts prf1 %% lift' Us Ts prf2
   1.168 -      | lift' _ _ (PThm (s, prf, prop, Ts)) = PThm (s, prf, prop, apsome (map (incr_tvar inc)) Ts)
   1.169 -      | lift' _ _ (PAxm (s, prop, Ts)) = PAxm (s, prop, apsome (map (incr_tvar inc)) Ts)
   1.170 -      | lift' _ _ prf = prf;
   1.171 +    fun lift' Us Ts (Abst (s, T, prf)) =
   1.172 +          (Abst (s, apsome' (same (incr_tvar inc)) T, lifth' Us (dummyT::Ts) prf)
   1.173 +           handle SAME => Abst (s, T, lift' Us (dummyT::Ts) prf))
   1.174 +      | lift' Us Ts (AbsP (s, t, prf)) =
   1.175 +          (AbsP (s, apsome' (same (lift'' Us Ts)) t, lifth' Us Ts prf)
   1.176 +           handle SAME => AbsP (s, t, lift' Us Ts prf))
   1.177 +      | lift' Us Ts (prf % t) = (lift' Us Ts prf % apsome (lift'' Us Ts) t
   1.178 +          handle SAME => prf % apsome' (same (lift'' Us Ts)) t)
   1.179 +      | lift' Us Ts (prf1 %% prf2) = (lift' Us Ts prf1 %% lifth' Us Ts prf2
   1.180 +          handle SAME => prf1 %% lift' Us Ts prf2)
   1.181 +      | lift' _ _ (PThm (s, prf, prop, Ts)) =
   1.182 +          PThm (s, prf, prop, apsome' (same (map (incr_tvar inc))) Ts)
   1.183 +      | lift' _ _ (PAxm (s, prop, Ts)) =
   1.184 +          PAxm (s, prop, apsome' (same (map (incr_tvar inc))) Ts)
   1.185 +      | lift' _ _ _ = raise SAME
   1.186 +    and lifth' Us Ts prf = (lift' Us Ts prf handle SAME => prf);
   1.187  
   1.188      val ps = map lift_all (Logic.strip_imp_prems (snd (Logic.strip_flexpairs prop)));
   1.189      val k = length ps;
   1.190 @@ -563,7 +604,7 @@
   1.191  	    AbsP ("H", None (*A*), lift Us (true::bs) (i+1) j B)
   1.192        | lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) = 
   1.193  	    Abst (a, None (*T*), lift (T::Us) (false::bs) i (j+1) t)
   1.194 -      | lift Us bs i j _ = proof_combP (lift' (rev Us) [] prf,
   1.195 +      | lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf,
   1.196              map (fn k => (#3 (foldr mk_app (bs, (i-1, j-1, PBound k)))))
   1.197                (i + k - 1 downto i));
   1.198    in
   1.199 @@ -945,7 +986,7 @@
   1.200  fun rewrite_proof tsig = rewrite_prf (fn (tab, f) =>
   1.201    Type.typ_match tsig (tab, f ()) handle Type.TYPE_MATCH => raise PMatch);
   1.202  
   1.203 -fun rewrite_proof_notypes tsig = rewrite_prf fst tsig;
   1.204 +fun rewrite_proof_notypes rews = rewrite_prf fst rews;
   1.205  
   1.206  (**** theory data ****)
   1.207