--- a/src/HOL/Tools/rewrite_hol_proof.ML Thu Dec 07 13:05:34 2023 +0100
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Thu Dec 07 14:48:58 2023 +0100
@@ -334,13 +334,13 @@
Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
| elim_cong_aux Ts (PThm ({name = "HOL.iffD1", ...}, _) % P % _ %% prf) =
Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
- (strip_cong [] (Proofterm.incr_pboundvars 1 0 prf))
+ (strip_cong [] (Proofterm.incr_boundvars 1 0 prf))
| elim_cong_aux Ts (PThm ({name = "HOL.iffD2", ...}, _) % _ % _ %% prf1 %% prf2) =
Option.map (make_subst Ts prf2 [] o
apsnd (map (make_sym Ts))) (strip_cong [] prf1)
| elim_cong_aux Ts (PThm ({name = "HOL.iffD2", ...}, _) % _ % P %% prf) =
Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
- apsnd (map (make_sym Ts))) (strip_cong [] (Proofterm.incr_pboundvars 1 0 prf))
+ apsnd (map (make_sym Ts))) (strip_cong [] (Proofterm.incr_boundvars 1 0 prf))
| elim_cong_aux _ _ = NONE;
fun elim_cong Ts hs prf = Option.map (rpair Proofterm.no_skel) (elim_cong_aux Ts prf);
--- a/src/Pure/Proof/extraction.ML Thu Dec 07 13:05:34 2023 +0100
+++ b/src/Pure/Proof/extraction.ML Thu Dec 07 14:48:58 2023 +0100
@@ -550,7 +550,7 @@
| corr d vs ts Ts hs cs t (Abst (s, SOME T, prf)) (Abst (_, _, prf')) defs =
let val (corr_prf, defs') = corr d vs [] (T :: Ts)
(dummyt :: hs) cs (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE)
- prf (Proofterm.incr_pboundvars 1 0 prf') defs
+ prf (Proofterm.incr_boundvars 1 0 prf') defs
in (Abst (s, SOME T, corr_prf), defs') end
| corr d vs ts Ts hs cs t (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) defs =
@@ -561,8 +561,8 @@
else (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE);
val (corr_prf, defs') =
corr d vs [] (T :: Ts) (prop :: hs)
- (prop :: cs) u (Proofterm.incr_pboundvars 0 1 prf)
- (Proofterm.incr_pboundvars 0 1 prf') defs;
+ (prop :: cs) u (Proofterm.incr_boundvars 0 1 prf)
+ (Proofterm.incr_boundvars 0 1 prf') defs;
val rlz = Const ("realizes", T --> propT --> propT)
in (
if T = nullT then AbsP ("R",
@@ -684,14 +684,14 @@
| extr d vs ts Ts hs (Abst (s, SOME T, prf)) defs =
let val (t, defs') = extr d vs []
- (T :: Ts) (dummyt :: hs) (Proofterm.incr_pboundvars 1 0 prf) defs
+ (T :: Ts) (dummyt :: hs) (Proofterm.incr_boundvars 1 0 prf) defs
in (Abs (s, T, t), defs') end
| extr d vs ts Ts hs (AbsP (s, SOME t, prf)) defs =
let
val T = etype_of thy' vs Ts t;
val (t, defs') =
- extr d vs [] (T :: Ts) (t :: hs) (Proofterm.incr_pboundvars 0 1 prf) defs
+ extr d vs [] (T :: Ts) (t :: hs) (Proofterm.incr_boundvars 0 1 prf) defs
in
(if T = nullT then subst_bound (nullt, t) else Abs (s, T, t), defs')
end
--- a/src/Pure/Proof/proof_rewrite_rules.ML Thu Dec 07 13:05:34 2023 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Thu Dec 07 14:48:58 2023 +0100
@@ -73,9 +73,9 @@
val _ $ A $ C = Envir.beta_norm X;
val _ $ B $ D = Envir.beta_norm Y
in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? B,
- Proofterm.equal_elim_axm %> C %> D %% Proofterm.incr_pboundvars 2 0 prf2 %%
+ Proofterm.equal_elim_axm %> C %> D %% Proofterm.incr_boundvars 2 0 prf2 %%
(PBound 1 %% (equal_elim_axm %> B %> A %%
- (Proofterm.symmetric_axm % ?? A % ?? B %% Proofterm.incr_pboundvars 2 0 prf1) %%
+ (Proofterm.symmetric_axm % ?? A % ?? B %% Proofterm.incr_boundvars 2 0 prf1) %%
PBound 0)))))
end
@@ -89,9 +89,9 @@
val _ $ B $ D = Envir.beta_norm X
in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? A,
equal_elim_axm %> D %> C %%
- (symmetric_axm % ?? C % ?? D %% Proofterm.incr_pboundvars 2 0 prf2) %%
+ (symmetric_axm % ?? C % ?? D %% Proofterm.incr_boundvars 2 0 prf2) %%
(PBound 1 %%
- (equal_elim_axm %> A %> B %% Proofterm.incr_pboundvars 2 0 prf1 %% PBound 0)))))
+ (equal_elim_axm %> A %> B %% Proofterm.incr_boundvars 2 0 prf1 %% PBound 0)))))
end
| rew' (PAxm ("Pure.combination", _, _) %
@@ -111,7 +111,7 @@
val _ $ Q = Envir.beta_norm Y;
in SOME (AbsP ("H", ?? X, Abst ("x", ty T,
equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
- (Proofterm.incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
+ (Proofterm.incr_boundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
end
| rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
@@ -126,7 +126,7 @@
val u = incr_boundvars 1 Q $ Bound 0
in SOME (AbsP ("H", ?? X, Abst ("x", ty T,
equal_elim_axm %> t %> u %%
- (symmetric_axm % ?? u % ?? t %% (Proofterm.incr_pboundvars 1 1 prf %> Bound 0))
+ (symmetric_axm % ?? u % ?? t %% (Proofterm.incr_boundvars 1 1 prf %> Bound 0))
%% (PBound 0 %> Bound 0))))
end
@@ -327,7 +327,7 @@
mk_prf (i - 1) j Hs Hs' P (prf %% un_hhf_proof H' H (PBound i))
| mk_prf _ _ _ _ _ prf = prf
in
- prf |> Proofterm.incr_pboundvars k l |> mk_prf (k - 1) (l - 1) Hs Hs' P |>
+ prf |> Proofterm.incr_boundvars k l |> mk_prf (k - 1) (l - 1) Hs Hs' P |>
fold_rev (fn P => fn prf => AbsP ("H", SOME P, prf)) Hs' |>
fold_rev (fn (s, T) => fn prf => Abst (s, SOME T, prf)) params
end
@@ -344,7 +344,7 @@
AbsP ("H", SOME P, mk_prf Q prf)
| mk_prf _ prf = prf
in
- prf |> Proofterm.incr_pboundvars k l |>
+ prf |> Proofterm.incr_boundvars k l |>
fold (fn i => fn prf => prf %> Bound i) (l - 1 downto 0) |>
fold (fn ((H, H'), i) => fn prf => prf %% hhf_proof H' H (PBound i))
(Hs ~~ Hs' ~~ (k - 1 downto 0)) |>
--- a/src/Pure/Proof/proof_syntax.ML Thu Dec 07 13:05:34 2023 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Thu Dec 07 14:48:58 2023 +0100
@@ -114,11 +114,11 @@
| term_of Ts (Abst (s, opT, prf)) =
let val T = the_default dummyT opT in
Const ("Pure.Abst", (T --> proofT) --> proofT) $
- Abs (s, T, term_of (T::Ts) (Proofterm.incr_pboundvars 1 0 prf))
+ Abs (s, T, term_of (T::Ts) (Proofterm.incr_boundvars 1 0 prf))
end
| term_of Ts (AbsP (s, t, prf)) =
AbsPt $ the_default Term.dummy_prop t $
- Abs (s, proofT, term_of (proofT::Ts) (Proofterm.incr_pboundvars 0 1 prf))
+ Abs (s, proofT, term_of (proofT::Ts) (Proofterm.incr_boundvars 0 1 prf))
| term_of Ts (prf1 %% prf2) =
AppPt $ term_of Ts prf1 $ term_of Ts prf2
| term_of Ts (prf % opt) =
@@ -178,13 +178,13 @@
if T = proofT then
error ("Term variable abstraction may not bind proof variable " ^ quote s)
else Abst (s, if ty then SOME T else NONE,
- Proofterm.incr_pboundvars (~1) 0 (prf_of [] prf))
+ Proofterm.incr_boundvars (~1) 0 (prf_of [] prf))
| prf_of [] (Const ("Pure.AbsP", _) $ t $ Abs (s, _, prf)) =
AbsP (s, case t of
Const ("Pure.dummy_pattern", _) => NONE
| _ $ Const ("Pure.dummy_pattern", _) => NONE
| _ => SOME (mk_term t),
- Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf))
+ Proofterm.incr_boundvars 0 (~1) (prf_of [] prf))
| prf_of [] (Const ("Pure.AppP", _) $ prf1 $ prf2) =
prf_of [] prf1 %% prf_of [] prf2
| prf_of Ts (Const ("Pure.Appt", _) $ prf $ Const ("Pure.type", Type ("itself", [T]))) =
--- a/src/Pure/proofterm.ML Thu Dec 07 13:05:34 2023 +0100
+++ b/src/Pure/proofterm.ML Thu Dec 07 14:48:58 2023 +0100
@@ -104,8 +104,9 @@
val size_of_proof: proof -> int
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
+ val incr_bv_same: int -> int -> int -> int -> proof Same.operation
+ val incr_bv: int -> int -> int -> int -> proof -> proof
+ val incr_boundvars: int -> int -> proof -> proof
val prf_loose_bvar1: proof -> int -> bool
val prf_loose_Pbvar1: proof -> int -> bool
val prf_add_loose_bnos: int -> int -> proof -> int list * int list -> int list * int list
@@ -643,26 +644,30 @@
inc is increment for bound variables
lev is level at which a bound variable is considered 'loose'*)
-fun prf_incr_bv' incP _ Plev _ (PBound i) =
- if i >= Plev then PBound (i+incP) else raise Same.SAME
- | prf_incr_bv' incP inct Plev tlev (AbsP (a, t, body)) =
- (AbsP (a, Same.map_option (incr_bv_same inct tlev) t,
- prf_incr_bv incP inct (Plev+1) tlev body) handle Same.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.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 % Option.map (incr_bv inct tlev) t
- handle Same.SAME => prf % Same.map_option (incr_bv_same inct tlev) t)
- | prf_incr_bv' _ _ _ _ _ = raise Same.SAME
-and prf_incr_bv incP inct Plev tlev prf =
- (prf_incr_bv' incP inct Plev tlev prf handle Same.SAME => prf);
+fun incr_bv_same incP inct =
+ if incP = 0 andalso inct = 0 then fn _ => fn _ => Same.same
+ else
+ let
+ fun proof Plev _ (PBound i) =
+ if i >= Plev then PBound (i + incP) else raise Same.SAME
+ | proof Plev tlev (AbsP (a, t, p)) =
+ (AbsP (a, Same.map_option (Term.incr_bv_same inct tlev) t,
+ Same.commit (proof (Plev + 1) tlev) p) handle Same.SAME =>
+ AbsP (a, t, proof (Plev + 1) tlev p))
+ | proof Plev tlev (Abst (a, T, body)) =
+ Abst (a, T, proof Plev (tlev + 1) body)
+ | proof Plev tlev (p %% q) =
+ (proof Plev tlev p %% Same.commit (proof Plev tlev) q
+ handle Same.SAME => p %% proof Plev tlev q)
+ | proof Plev tlev (p % t) =
+ (proof Plev tlev p % Option.map (Term.incr_bv inct tlev) t
+ handle Same.SAME => p % Same.map_option (Term.incr_bv_same inct tlev) t)
+ | proof _ _ _ = raise Same.SAME;
+ in proof end;
-fun incr_pboundvars 0 0 prf = prf
- | incr_pboundvars incP inct prf = prf_incr_bv incP inct 0 0 prf;
+fun incr_bv incP inct Plev tlev = Same.commit (incr_bv_same incP inct Plev tlev);
+
+fun incr_boundvars incP inct = incr_bv incP inct 0 0;
fun prf_loose_bvar1 (prf1 %% prf2) k = prf_loose_bvar1 prf1 k orelse prf_loose_bvar1 prf2 k
@@ -792,7 +797,7 @@
val n = length args;
fun term lev (Bound i) =
(if i<lev then raise Same.SAME (*var is locally bound*)
- else incr_boundvars lev (nth args (i - lev))
+ else Term.incr_boundvars lev (nth args (i - lev))
handle General.Subscript => Bound (i - n)) (*loose: change it*)
| term lev (Abs (a, T, t)) = Abs (a, T, term (lev + 1) t)
| term lev (t $ u) = (term lev t $ Same.commit (term lev) u
@@ -815,7 +820,7 @@
val n = length args;
fun proof Plev tlev (PBound i) =
(if i < Plev then raise Same.SAME (*var is locally bound*)
- else incr_pboundvars Plev tlev (nth args (i - Plev))
+ else incr_boundvars Plev tlev (nth args (i - Plev))
handle General.Subscript => PBound (i - n) (*loose: change it*))
| proof Plev tlev (AbsP (a, t, p)) = AbsP (a, t, proof (Plev + 1) tlev p)
| proof Plev tlev (Abst (a, T, p)) = Abst (a, T, proof Plev (tlev + 1) p)
@@ -1363,9 +1368,9 @@
if i = 0 andalso j = 0 then ((ixn, prf) :: pinst, tinst)
else
(case apfst (flt i) (apsnd (flt j) (prf_add_loose_bnos 0 0 prf ([], []))) of
- ([], []) => ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst)
+ ([], []) => ((ixn, incr_boundvars (~i) (~j) prf) :: pinst, tinst)
| ([], _) =>
- if j = 0 then ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst)
+ if j = 0 then ((ixn, incr_boundvars (~i) (~j) prf) :: pinst, tinst)
else raise PMatch
| _ => raise PMatch)
| mtch Ts i j inst (prf1 % opt1, prf2 % opt2) =
@@ -1377,11 +1382,11 @@
(optmatch matchT inst (opT, opU)) (prf1, prf2)
| mtch Ts i j inst (prf1, Abst (_, opU, prf2)) =
mtch (the_default dummyT opU :: Ts) i (j+1) inst
- (incr_pboundvars 0 1 prf1 %> Bound 0, prf2)
+ (incr_boundvars 0 1 prf1 %> Bound 0, prf2)
| mtch Ts i j inst (AbsP (_, opt, prf1), AbsP (_, opu, prf2)) =
mtch Ts (i+1) j (optmatch (matcht Ts j) inst (opt, opu)) (prf1, prf2)
| mtch Ts i j inst (prf1, AbsP (_, _, prf2)) =
- mtch Ts (i+1) j inst (incr_pboundvars 1 0 prf1 %% PBound 0, prf2)
+ mtch Ts (i+1) j inst (incr_boundvars 1 0 prf1 %% PBound 0, prf2)
| mtch Ts i j inst (PAxm (s1, _, opTs), PAxm (s2, _, opUs)) =
if s1 = s2 then optmatch matchTs inst (opTs, opUs)
else raise PMatch
@@ -1406,7 +1411,7 @@
fun subst' lev (Var (xi, _)) =
(case AList.lookup (op =) insts xi of
NONE => raise Same.SAME
- | SOME u => incr_boundvars lev u)
+ | SOME u => Term.incr_boundvars lev u)
| subst' _ (Const (s, T)) = Const (s, substT T)
| subst' _ (Free (s, T)) = Free (s, substT T)
| subst' lev (Abs (a, T, body)) =
@@ -1432,7 +1437,7 @@
| subst plev tlev (Hyp (Var (xi, _))) =
(case AList.lookup (op =) pinst xi of
NONE => raise Same.SAME
- | SOME prf' => incr_pboundvars plev tlev prf')
+ | SOME prf' => incr_boundvars plev tlev prf')
| subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts)
| subst _ _ (PClass (T, c)) = PClass (substT T, c)
| subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts)
@@ -1491,12 +1496,12 @@
fun rew0 Ts hs (prf as AbsP (_, _, prf' %% PBound 0)) =
if prf_loose_Pbvar1 prf' 0 then rew Ts hs prf
else
- let val prf'' = incr_pboundvars (~1) 0 prf'
+ let val prf'' = incr_boundvars (~1) 0 prf'
in SOME (the_default (prf'', no_skel) (rew Ts hs prf'')) end
| rew0 Ts hs (prf as Abst (_, _, prf' % SOME (Bound 0))) =
if prf_loose_bvar1 prf' 0 then rew Ts hs prf
else
- let val prf'' = incr_pboundvars 0 (~1) prf'
+ let val prf'' = incr_boundvars 0 (~1) prf'
in SOME (the_default (prf'', no_skel) (rew Ts hs prf'')) end
| rew0 Ts hs prf = rew Ts hs prf;
@@ -1699,9 +1704,9 @@
| ((Abs (_, T, t), []), (Abs (_, U, u), [])) =>
decompose thy (T::Ts) (t, u) (unifyT thy env T U)
| ((Abs (_, T, t), []), _) =>
- decompose thy (T::Ts) (t, incr_boundvars 1 u $ Bound 0) env
+ decompose thy (T::Ts) (t, Term.incr_boundvars 1 u $ Bound 0) env
| (_, (Abs (_, T, u), [])) =>
- decompose thy (T::Ts) (incr_boundvars 1 t $ Bound 0, u) env
+ decompose thy (T::Ts) (Term.incr_boundvars 1 t $ Bound 0, u) env
| _ => ([(mk_abs Ts t, mk_abs Ts u)], env)
end;
@@ -1743,7 +1748,7 @@
NONE => mk_tvar [] env
| SOME T => (T, env));
val (t, prf, cnstrts, env'', vTs') =
- mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf;
+ mk_cnstrts env' (T::Ts) (map (Term.incr_boundvars 1) Hs) vTs cprf;
in
(Const ("Pure.all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf),
cnstrts, env'', vTs')