# HG changeset patch # User wenzelm # Date 1701956938 -3600 # Node ID 04dfecb9343ac6a1683042c52df4f672c126be3d # Parent f91212703951090bf5aa6ace4fbe61f0b5704aec misc tuning and clarification, following Term.incr_bv / Term.incr_boundvars; diff -r f91212703951 -r 04dfecb9343a src/HOL/Tools/rewrite_hol_proof.ML --- 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); diff -r f91212703951 -r 04dfecb9343a src/Pure/Proof/extraction.ML --- 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 diff -r f91212703951 -r 04dfecb9343a src/Pure/Proof/proof_rewrite_rules.ML --- 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)) |> diff -r f91212703951 -r 04dfecb9343a src/Pure/Proof/proof_syntax.ML --- 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]))) = diff -r f91212703951 -r 04dfecb9343a src/Pure/proofterm.ML --- 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 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')