--- a/src/HOL/Tools/datatype_realizer.ML Fri Dec 08 19:36:27 2023 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML Fri Dec 08 20:56:21 2023 +0100
@@ -141,7 +141,7 @@
(case head_of (strip_abs_body f) of
Free (s, T) =>
let val T' = Logic.varifyT_global T in
- Abst (s, SOME T', Proofterm.prf_abstract_over
+ Abst (s, SOME T', Proofterm.abstract_over
(Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
end
| _ => AbsP ("H", SOME p, prf)))
--- a/src/Pure/envir.ML Fri Dec 08 19:36:27 2023 +0100
+++ b/src/Pure/envir.ML Fri Dec 08 20:56:21 2023 +0100
@@ -206,24 +206,23 @@
in
-fun norm_type_same tyenv T =
- if Vartab.is_empty tyenv then raise Same.SAME
- else norm_type0 tyenv T;
+fun norm_type_same tyenv =
+ if Vartab.is_empty tyenv then Same.same
+ else norm_type0 tyenv;
-fun norm_types_same tyenv Ts =
- if Vartab.is_empty tyenv then raise Same.SAME
- else Same.map (norm_type0 tyenv) Ts;
+fun norm_types_same tyenv =
+ if Vartab.is_empty tyenv then Same.same
+ else Same.map (norm_type0 tyenv);
fun norm_type tyenv = Same.commit (norm_type_same tyenv);
-fun norm_term_same (envir as Envir {tenv, tyenv, ...}) =
- if Vartab.is_empty tyenv then norm_term1 tenv
- else norm_term2 envir;
+fun norm_term_same (envir as Envir {tenv, tyenv, ...}) t =
+ if is_empty envir andalso not (Term.could_beta_contract t) then raise Same.SAME
+ else if Vartab.is_empty tyenv then norm_term1 tenv t else norm_term2 envir t;
fun norm_term envir = Same.commit (norm_term_same envir);
-fun beta_norm t =
- if Term.could_beta_contract t then norm_term init t else t;
+val beta_norm = norm_term init;
end;
@@ -376,13 +375,13 @@
in
-fun subst_type_same tyenv T =
- if Vartab.is_empty tyenv then raise Same.SAME
- else subst_type0 tyenv T;
+fun subst_type_same tyenv =
+ if Vartab.is_empty tyenv then Same.same
+ else subst_type0 tyenv;
-fun subst_term_types_same tyenv t =
- if Vartab.is_empty tyenv then raise Same.SAME
- else Term_Subst.map_types_same (subst_type0 tyenv) t;
+fun subst_term_types_same tyenv =
+ if Vartab.is_empty tyenv then Same.same
+ else Term_Subst.map_types_same (subst_type0 tyenv);
fun subst_term_same (tyenv, tenv) =
if Vartab.is_empty tenv then subst_term_types_same tyenv
--- a/src/Pure/logic.ML Fri Dec 08 19:36:27 2023 +0100
+++ b/src/Pure/logic.ML Fri Dec 08 20:56:21 2023 +0100
@@ -450,7 +450,7 @@
(fn TVar ((a, i), S) => TVar ((a, i + k), S)
| _ => raise Same.SAME);
-fun incr_tvar k T = incr_tvar_same k T handle Same.SAME => T;
+fun incr_tvar k = Same.commit (incr_tvar_same k);
(*For all variables in the term, increment indexnames and lift over the Us
result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
@@ -476,7 +476,7 @@
| incr _ (Bound _) = raise Same.SAME;
in incr 0 end;
-fun incr_indexes arg t = incr_indexes_same arg t handle Same.SAME => t;
+fun incr_indexes arg = Same.commit (incr_indexes_same arg);
(* Lifting functions from subgoal and increment:
--- a/src/Pure/proofterm.ML Fri Dec 08 19:36:27 2023 +0100
+++ b/src/Pure/proofterm.ML Fri Dec 08 20:56:21 2023 +0100
@@ -103,7 +103,7 @@
val maxidx_proof: proof -> int -> int
val size_of_proof: proof -> int
val change_types: typ list option -> proof -> proof
- val prf_abstract_over: term -> proof -> proof
+ val abstract_over: term -> 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
@@ -616,27 +616,30 @@
which must contain no loose bound variables.
The resulting proof term is ready to become the body of an Abst.*)
-fun prf_abstract_over v =
+fun abstract_over v =
let
- 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.SAME => f $ abst' lev t)
- | _ => raise Same.SAME)
- and absth' lev t = (abst' lev t handle Same.SAME => t);
+ fun term lev u =
+ if v aconv u then Bound lev
+ else
+ (case u of
+ Abs (a, T, t) => Abs (a, T, term (lev + 1) t)
+ | t $ u =>
+ (term lev t $ Same.commit (term lev) u
+ handle Same.SAME => t $ term lev u)
+ | _ => raise Same.SAME);
- fun abst lev (AbsP (a, t, prf)) =
- (AbsP (a, Same.map_option (abst' lev) t, absth lev prf)
- handle Same.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.SAME => prf1 %% abst lev prf2)
- | abst lev (prf % t) = (abst lev prf % Option.map (absth' lev) t
- handle Same.SAME => prf % Same.map_option (abst' lev) t)
- | abst _ _ = raise Same.SAME
- and absth lev prf = (abst lev prf handle Same.SAME => prf);
+ fun proof lev (AbsP (a, t, p)) =
+ (AbsP (a, Same.map_option (term lev) t, Same.commit (proof lev) p)
+ handle Same.SAME => AbsP (a, t, proof lev p))
+ | proof lev (Abst (a, T, p)) = Abst (a, T, proof (lev + 1) p)
+ | proof lev (p %% q) = (proof lev p %% Same.commit (proof lev) q
+ handle Same.SAME => p %% proof lev q)
+ | proof lev (p % t) =
+ (proof lev p % Option.map (Same.commit (term lev)) t
+ handle Same.SAME => p % Same.map_option (term lev) t)
+ | proof _ _ = raise Same.SAME;
- in absth 0 end;
+ in Same.commit (proof 0) end;
(*increments a proof term's non-local bound variables
@@ -739,35 +742,35 @@
in
-fun norm_proof env =
+fun norm_proof envir =
let
- val envT = Envir.type_env env;
+ val tyenv = Envir.type_env envir;
fun msg s = warning ("type conflict in norm_proof:\n" ^ s);
- fun norm_term_same t = Envir.norm_term_same env t handle TYPE (s, _, _) =>
- (msg s; Envir.norm_term_same env (del_conflicting_vars env t));
- fun norm_type_same T = Envir.norm_type_same envT T handle TYPE (s, _, _) =>
- (msg s; Envir.norm_type_same envT (del_conflicting_tvars envT T));
- fun norm_types_same Ts = Envir.norm_types_same envT Ts handle TYPE (s, _, _) =>
- (msg s; Envir.norm_types_same envT (map (del_conflicting_tvars envT) Ts));
+ fun norm_term_same t = Envir.norm_term_same envir t handle TYPE (s, _, _) =>
+ (msg s; Envir.norm_term_same envir (del_conflicting_vars envir t));
+ fun norm_type_same T = Envir.norm_type_same tyenv T handle TYPE (s, _, _) =>
+ (msg s; Envir.norm_type_same tyenv (del_conflicting_tvars tyenv T));
+ fun norm_types_same Ts = Envir.norm_types_same tyenv Ts handle TYPE (s, _, _) =>
+ (msg s; Envir.norm_types_same tyenv (map (del_conflicting_tvars tyenv) Ts));
- fun norm (Abst (s, T, prf)) =
- (Abst (s, Same.map_option norm_type_same T, Same.commit norm prf)
- handle Same.SAME => Abst (s, T, norm prf))
- | norm (AbsP (s, t, prf)) =
- (AbsP (s, Same.map_option norm_term_same t, Same.commit norm prf)
- handle Same.SAME => AbsP (s, t, norm prf))
- | norm (prf % t) =
- (norm prf % Option.map (Same.commit norm_term_same) t
- handle Same.SAME => prf % Same.map_option norm_term_same t)
- | norm (prf1 %% prf2) =
- (norm prf1 %% Same.commit norm prf2
- handle Same.SAME => prf1 %% norm prf2)
- | norm (PAxm (s, prop, Ts)) =
- PAxm (s, prop, Same.map_option norm_types_same Ts)
+ fun norm (Abst (a, T, p)) =
+ (Abst (a, Same.map_option norm_type_same T, Same.commit norm p)
+ handle Same.SAME => Abst (a, T, norm p))
+ | norm (AbsP (a, t, p)) =
+ (AbsP (a, Same.map_option norm_term_same t, Same.commit norm p)
+ handle Same.SAME => AbsP (a, t, norm p))
+ | norm (p % t) =
+ (norm p % Option.map (Same.commit norm_term_same) t
+ handle Same.SAME => p % Same.map_option norm_term_same t)
+ | norm (p %% q) =
+ (norm p %% Same.commit norm q
+ handle Same.SAME => p %% norm q)
+ | norm (PAxm (a, prop, Ts)) =
+ PAxm (a, prop, Same.map_option norm_types_same Ts)
| norm (PClass (T, c)) =
PClass (norm_type_same T, c)
- | norm (Oracle (s, prop, Ts)) =
- Oracle (s, prop, Same.map_option norm_types_same Ts)
+ | norm (Oracle (a, prop, Ts)) =
+ Oracle (a, prop, Same.map_option norm_types_same Ts)
| norm (PThm ({serial = i, pos = p, theory_name, name = a, prop = t, types = Ts}, thm_body)) =
PThm (thm_header i p theory_name a t
(Same.map_option norm_types_same Ts), thm_body)
@@ -793,27 +796,21 @@
(* substitution of bound variables *)
fun subst_bounds args prf =
- let
- val n = length args;
- fun term lev (Bound i) =
- (if i < lev then raise Same.SAME (*var is locally bound*)
- else if i - lev < n then Term.incr_boundvars lev (nth args (i - lev))
- else 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
- handle Same.SAME => t $ term lev u)
- | term _ _ = raise Same.SAME;
+ if null args then prf
+ else
+ let
+ val term = Term.subst_bounds_same args;
- fun proof lev (AbsP (a, t, p)) =
- (AbsP (a, Same.map_option (term lev) t, Same.commit (proof lev) p)
- handle Same.SAME => AbsP (a, t, proof lev p))
- | proof lev (Abst (a, T, p)) = Abst (a, T, proof (lev + 1) p)
- | proof lev (p %% q) = (proof lev p %% Same.commit (proof lev) q
- handle Same.SAME => p %% proof lev q)
- | proof lev (p % t) = (proof lev p % Option.map (Same.commit (term lev)) t
- handle Same.SAME => p % Same.map_option (term lev) t)
- | proof _ _ = raise Same.SAME;
- in if null args then prf else Same.commit (proof 0) prf end;
+ fun proof lev (AbsP (a, t, p)) =
+ (AbsP (a, Same.map_option (term lev) t, Same.commit (proof lev) p)
+ handle Same.SAME => AbsP (a, t, proof lev p))
+ | proof lev (Abst (a, T, p)) = Abst (a, T, proof (lev + 1) p)
+ | proof lev (p %% q) = (proof lev p %% Same.commit (proof lev) q
+ handle Same.SAME => p %% proof lev q)
+ | proof lev (p % t) = (proof lev p % Option.map (Same.commit (term lev)) t
+ handle Same.SAME => p % Same.map_option (term lev) t)
+ | proof _ _ = raise Same.SAME;
+ in Same.commit (proof 0) prf end;
fun subst_pbounds args prf =
let
@@ -923,7 +920,7 @@
(* forall introduction *)
-fun forall_intr_proof (a, v) opt_T prf = Abst (a, opt_T, prf_abstract_over v prf);
+fun forall_intr_proof (a, v) opt_T prf = Abst (a, opt_T, abstract_over v prf);
fun forall_intr_proof' v prf =
let val (a, T) = (case v of Var ((a, _), T) => (a, T) | Free (a, T) => (a, T))
@@ -1011,47 +1008,45 @@
fun lift_proof Bi inc prop prf =
let
- fun lift'' Us Ts t =
- strip_abs Ts (Logic.incr_indexes ([], Us, inc) (mk_abs Ts t));
+ val typ = Logic.incr_tvar_same inc;
+ val typs = Same.map_option (Same.map typ);
+
+ fun term Us Ts t =
+ strip_abs Ts (Logic.incr_indexes_same ([], Us, inc) (mk_abs Ts t));
- fun lift' Us Ts (Abst (s, T, prf)) =
- (Abst (s, Same.map_option (Logic.incr_tvar_same inc) T, lifth' Us (dummyT::Ts) prf)
- handle Same.SAME => Abst (s, T, lift' Us (dummyT::Ts) prf))
- | lift' Us Ts (AbsP (s, t, prf)) =
- (AbsP (s, Same.map_option (same (op =) (lift'' Us Ts)) t, lifth' Us Ts prf)
- handle Same.SAME => AbsP (s, t, lift' Us Ts prf))
- | lift' Us Ts (prf % t) = (lift' Us Ts prf % Option.map (lift'' Us Ts) t
- handle Same.SAME => prf % Same.map_option (same (op =) (lift'' Us Ts)) t)
- | lift' Us Ts (prf1 %% prf2) = (lift' Us Ts prf1 %% lifth' Us Ts prf2
- handle Same.SAME => prf1 %% lift' Us Ts prf2)
- | lift' _ _ (PAxm (s, prop, Ts)) =
- PAxm (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts)
- | lift' _ _ (PClass (T, c)) =
- PClass (Logic.incr_tvar_same inc T, c)
- | lift' _ _ (Oracle (s, prop, Ts)) =
- Oracle (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts)
- | lift' _ _ (PThm ({serial = i, pos = p, theory_name, name = s, prop, types = Ts}, thm_body)) =
- PThm (thm_header i p theory_name s prop
- ((Same.map_option o Same.map) (Logic.incr_tvar inc) Ts), thm_body)
- | lift' _ _ _ = raise Same.SAME
- and lifth' Us Ts prf = (lift' Us Ts prf handle Same.SAME => prf);
+ fun proof Us Ts (Abst (a, T, p)) =
+ (Abst (a, Same.map_option typ T, Same.commit (proof Us (dummyT :: Ts)) p)
+ handle Same.SAME => Abst (a, T, proof Us (dummyT :: Ts) p))
+ | proof Us Ts (AbsP (a, t, p)) =
+ (AbsP (a, Same.map_option (term Us Ts) t, Same.commit (proof Us Ts) p)
+ handle Same.SAME => AbsP (a, t, proof Us Ts p))
+ | proof Us Ts (p % t) =
+ (proof Us Ts p % Option.map (Same.commit (term Us Ts)) t
+ handle Same.SAME => p % Same.map_option (term Us Ts) t)
+ | proof Us Ts (p %% q) =
+ (proof Us Ts p %% Same.commit (proof Us Ts) q
+ handle Same.SAME => p %% proof Us Ts q)
+ | proof _ _ (PAxm (a, prop, Ts)) = PAxm (a, prop, typs Ts)
+ | proof _ _ (PClass (T, c)) = PClass (typ T, c)
+ | proof _ _ (Oracle (a, prop, Ts)) = Oracle (a, prop, typs Ts)
+ | proof _ _ (PThm ({serial, pos, theory_name, name, prop, types}, thm_body)) =
+ PThm (thm_header serial pos theory_name name prop (typs types), thm_body)
+ | proof _ _ _ = raise Same.SAME;
val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop);
val k = length ps;
fun mk_app b (i, j, prf) =
- if b then (i-1, j, prf %% PBound i) else (i, j-1, prf %> Bound j);
+ if b then (i - 1, j, prf %% PBound i) else (i, j - 1, prf %> Bound j);
fun lift Us bs i j (Const ("Pure.imp", _) $ A $ B) =
- AbsP ("H", NONE (*A*), lift Us (true::bs) (i+1) j B)
+ AbsP ("H", NONE (*A*), lift Us (true::bs) (i + 1) j B)
| lift Us bs i j (Const ("Pure.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 (lifth' (rev Us) [] prf,
- map (fn k => (#3 (fold_rev mk_app bs (i-1, j-1, PBound k))))
- (i + k - 1 downto i));
- in
- mk_AbsP ps (lift [] [] 0 0 Bi)
- end;
+ Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j + 1) t)
+ | lift Us bs i j _ =
+ proof_combP (Same.commit (proof (rev Us) []) prf,
+ map (fn k => (#3 (fold_rev mk_app bs (i - 1, j - 1, PBound k)))) (i + k - 1 downto i));
+ in mk_AbsP ps (lift [] [] 0 0 Bi) end;
fun incr_indexes i =
Same.commit (map_proof_terms_same
@@ -1060,14 +1055,14 @@
(* proof by assumption *)
-fun mk_asm_prf t i m =
+fun mk_asm_prf C i m =
let
fun imp_prf _ i 0 = PBound i
| imp_prf (Const ("Pure.imp", _) $ A $ B) i m = AbsP ("H", NONE (*A*), imp_prf B (i+1) (m-1))
| imp_prf _ i _ = PBound i;
fun all_prf (Const ("Pure.all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), all_prf t)
| all_prf t = imp_prf t (~i) m
- in all_prf t end;
+ in all_prf C end;
fun assumption_proof Bs Bi n prf =
mk_AbsP Bs (proof_combP (prf, map PBound (length Bs - 1 downto 0) @ [mk_asm_prf Bi n ~1]));
--- a/src/Pure/term.ML Fri Dec 08 19:36:27 2023 +0100
+++ b/src/Pure/term.ML Fri Dec 08 20:56:21 2023 +0100
@@ -90,6 +90,7 @@
val loose_bnos: term -> int list
val loose_bvar: term * int -> bool
val loose_bvar1: term * int -> bool
+ val subst_bounds_same: term list -> int -> term Same.operation
val subst_bounds: term list * term -> term
val subst_bound: term * term -> term
val betapply: term * term -> term
@@ -704,22 +705,27 @@
Loose bound variables >=n are reduced by "n" to
compensate for the disappearance of lambdas.
*)
-fun subst_bounds (args: term list, tm) : term =
- let
- val n = length args;
- fun term lev (Bound i) =
- (if i < lev then raise Same.SAME (*var is locally bound*)
- else if i - lev < n then incr_boundvars lev (nth args (i - lev))
- else 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
- handle Same.SAME => t $ term lev u)
- | term _ _ = raise Same.SAME;
- in if null args then tm else Same.commit (term 0) tm end;
+fun subst_bounds_same args =
+ if null args then fn _ => Same.same
+ else
+ let
+ val n = length args;
+ fun term lev (Bound i) =
+ (if i < lev then raise Same.SAME (*var is locally bound*)
+ else if i - lev < n then incr_boundvars lev (nth args (i - lev))
+ else 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
+ handle Same.SAME => t $ term lev u)
+ | term _ _ = raise Same.SAME;
+ in term end;
+
+fun subst_bounds (args: term list, body) : term =
+ if null args then body else Same.commit (subst_bounds_same args 0) body;
(*Special case: one argument*)
-fun subst_bound (arg, tm) : term =
+fun subst_bound (arg, body) : term =
let
fun term lev (Bound i) =
if i < lev then raise Same.SAME (*var is locally bound*)
@@ -730,7 +736,7 @@
(term lev t $ Same.commit (term lev) u
handle Same.SAME => t $ term lev u)
| term _ _ = raise Same.SAME;
- in term 0 tm handle Same.SAME => tm end;
+ in Same.commit (term 0) body end;
(*beta-reduce if possible, else form application*)
fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
@@ -780,16 +786,16 @@
The resulting term is ready to become the body of an Abs.*)
fun abstract_over (v, body) =
let
- fun abs lev tm =
+ fun term lev tm =
if v aconv tm then Bound lev
else
(case tm of
- Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
+ Abs (a, T, t) => Abs (a, T, term (lev + 1) t)
| t $ u =>
- (abs lev t $ (abs lev u handle Same.SAME => u)
- handle Same.SAME => t $ abs lev u)
+ (term lev t $ Same.commit (term lev) u
+ handle Same.SAME => t $ term lev u)
| _ => raise Same.SAME);
- in abs 0 body handle Same.SAME => body end;
+ in Same.commit (term 0) body end;
fun term_name (Const (x, _)) = Long_Name.base_name x
| term_name (Free (x, _)) = x
--- a/src/Pure/term_items.ML Fri Dec 08 19:36:27 2023 +0100
+++ b/src/Pure/term_items.ML Fri Dec 08 20:56:21 2023 +0100
@@ -33,6 +33,7 @@
val make2: key * 'a -> key * 'a -> 'a table
val make3: key * 'a -> key * 'a -> key * 'a -> 'a table
val make_strict: (key * 'a) list -> 'a table
+ val unsynchronized_cache: (key -> 'a) -> key -> 'a
type set = int table
val add_set: key -> set -> set
val make_set: key list -> set
@@ -84,6 +85,8 @@
fun make_strict es = Table (Table.make es);
+val unsynchronized_cache = Table.unsynchronized_cache;
+
(* set with order of addition *)
--- a/src/Pure/thm.ML Fri Dec 08 19:36:27 2023 +0100
+++ b/src/Pure/thm.ML Fri Dec 08 20:56:21 2023 +0100
@@ -1280,7 +1280,7 @@
(case prop of
Const ("Pure.imp", _) $ A $ B =>
if A aconv propA then
- Thm (deriv_rule2 (curry Proofterm.%%, curry ZAppP) der derA,
+ Thm (deriv_rule2 (curry Proofterm.%%, curry ZAppp) der derA,
{cert = join_certificate2 (thAB, thA),
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
@@ -1660,16 +1660,22 @@
val tpairs' = tpairs |> map (apply2 (Envir.norm_term env))
(*remove trivial tpairs, of the form t \<equiv> t*)
|> filter_out (op aconv);
- val der' = deriv_rule1 (Proofterm.norm_proof_remove_types env, ZTerm.todo_proof) der;
+ val prop' = Envir.norm_term env prop;
val thy' = Context.certificate_theory cert' handle ERROR msg =>
raise CONTEXT (msg, [], [], [th], Option.map Context.Proof opt_ctxt);
- val constraints' = insert_constraints_env thy' env constraints;
- val prop' = Envir.norm_term env prop;
- val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop');
- val shyps = Envir.insert_sorts env shyps;
+
+ fun prf p = Proofterm.norm_proof_remove_types env p;
+ fun zprf p = ZTerm.norm_proof thy' env p;
in
- Thm (der', {cert = cert', tags = [], maxidx = maxidx, constraints = constraints',
- shyps = shyps, hyps = hyps, tpairs = tpairs', prop = prop'})
+ Thm (deriv_rule1 (prf, zprf) der,
+ {cert = cert',
+ tags = [],
+ maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'),
+ constraints = insert_constraints_env thy' env constraints,
+ shyps = Envir.insert_sorts env shyps,
+ hyps = hyps,
+ tpairs = tpairs',
+ prop = prop'})
end)
end);
@@ -2043,15 +2049,15 @@
val (tpairs, Bs, Bi, C) = dest_state (state, i);
fun newth n (env, tpairs) =
let
- val normt = Envir.norm_term env;
- fun assumption_proof prf =
- Proofterm.assumption_proof (map normt Bs) (normt Bi) n prf;
val thy' = Context.certificate_theory cert' handle ERROR msg =>
raise CONTEXT (msg, [], [], [state], Option.map Context.Proof opt_ctxt);
+ val normt = Envir.norm_term env;
+ fun prf p =
+ Proofterm.assumption_proof (map normt Bs) (normt Bi) n p
+ |> not (Envir.is_empty env) ? Proofterm.norm_proof_remove_types env;
+ fun zprf p = ZTerm.assumption_proof thy' env Bs Bi n p;
in
- Thm (deriv_rule1
- (assumption_proof #> not (Envir.is_empty env) ? Proofterm.norm_proof_remove_types env,
- ZTerm.todo_proof) der,
+ Thm (deriv_rule1 (prf, zprf) der,
{tags = [],
maxidx = Envir.maxidx_of env,
constraints = insert_constraints_env thy' env constraints,
@@ -2059,7 +2065,8 @@
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*)
+ 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;
@@ -2086,15 +2093,21 @@
(case find_index (fn asm => Envir.aeconv (asm, concl)) asms of
~1 => raise THM ("eq_assumption", 0, [state])
| n =>
- Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1), ZTerm.todo_proof) der,
- {cert = cert,
- tags = [],
- maxidx = maxidx,
- constraints = constraints,
- shyps = shyps,
- hyps = hyps,
- tpairs = tpairs,
- prop = Logic.list_implies (Bs, C)}))
+ let
+ fun prf p = Proofterm.assumption_proof Bs Bi (n + 1) p;
+ fun zprf p =
+ ZTerm.assumption_proof (Context.certificate_theory cert) Envir.init Bs Bi (n + 1) p;
+ in
+ Thm (deriv_rule1 (prf, zprf) der,
+ {cert = cert,
+ tags = [],
+ maxidx = maxidx,
+ constraints = constraints,
+ shyps = shyps,
+ hyps = hyps,
+ tpairs = tpairs,
+ prop = Logic.list_implies (Bs, C)})
+ end)
end;
--- a/src/Pure/zterm.ML Fri Dec 08 19:36:27 2023 +0100
+++ b/src/Pure/zterm.ML Fri Dec 08 20:56:21 2023 +0100
@@ -135,14 +135,14 @@
datatype zproof =
ZDummy (*dummy proof*)
- | ZConstP of zproof_name * zterm * ztyp ZTVars.table * zterm ZVars.table
- | ZBoundP of int
+ | ZConstp of zproof_name * zterm * ztyp ZTVars.table * zterm ZVars.table
+ | ZBoundp of int
| ZHyp of zterm
| ZAbst of string * ztyp * zproof
- | ZAbsP of string * zterm * zproof
+ | ZAbsp of string * zterm * zproof
| ZAppt of zproof * zterm
- | ZAppP of zproof * zproof
- | ZClassP of ztyp * class; (*OFCLASS proof from sorts algebra*)
+ | ZAppp of zproof * zproof
+ | ZClassp of ztyp * class; (*OFCLASS proof from sorts algebra*)
@@ -158,6 +158,15 @@
val fold_types: (ztyp -> 'a -> 'a) -> zterm -> 'a -> 'a
val ztyp_ord: ztyp * ztyp -> order
val aconv_zterm: zterm * zterm -> bool
+ val ZAbsts: (string * ztyp) list -> zproof -> zproof
+ val ZAbsps: zterm list -> zproof -> zproof
+ val ZAppts: zproof * zterm list -> zproof
+ val ZAppps: zproof * zproof list -> zproof
+ val fold_proof_terms: (zterm -> 'a -> 'a) -> zproof -> 'a -> 'a
+ val exists_proof_terms: (zterm -> bool) -> zproof -> bool
+ val incr_bv_same: int -> int -> zterm Same.operation
+ val incr_bv: int -> int -> zterm -> zterm
+ val incr_boundvars: int -> zterm -> zterm
val ztyp_of: typ -> ztyp
val zterm_cache_consts: Consts.T -> {zterm: term -> zterm, ztyp: typ -> ztyp}
val zterm_cache: theory -> {zterm: term -> zterm, ztyp: typ -> ztyp}
@@ -165,6 +174,10 @@
val typ_of: ztyp -> typ
val term_of_consts: Consts.T -> zterm -> term
val term_of: theory -> zterm -> term
+ val could_beta_contract: zterm -> bool
+ val norm_type: Type.tyenv -> ztyp -> ztyp
+ val norm_term: theory -> Envir.env -> zterm -> zterm
+ val norm_proof: theory -> Envir.env -> zproof -> zproof
val dummy_proof: 'a -> zproof
val todo_proof: 'a -> zproof
val axiom_proof: theory -> string -> term -> zproof
@@ -192,6 +205,7 @@
val rotate_proof: theory -> term list -> term -> (string * typ) list ->
term list -> int -> zproof -> zproof
val permute_prems_proof: theory -> term list -> int -> int -> zproof -> zproof
+ val assumption_proof: theory -> Envir.env -> term list -> term -> int -> zproof -> zproof
end;
structure ZTerm: ZTERM =
@@ -213,14 +227,68 @@
(* derived operations *)
-val mk_ZAbst = fold_rev (fn (x, T) => fn prf => ZAbst (x, T, prf));
-val mk_ZAbsP = fold_rev (fn t => fn prf => ZAbsP ("H", t, prf));
+val ZAbsts = fold_rev (fn (x, T) => fn prf => ZAbst (x, T, prf));
+val ZAbsps = fold_rev (fn t => fn prf => ZAbsp ("H", t, prf));
+
+val ZAppts = Library.foldl ZAppt;
+val ZAppps = Library.foldl ZAppp;
+
+
+(* fold *)
-val mk_ZAppt = Library.foldl ZAppt;
-val mk_ZAppP = Library.foldl ZAppP;
+fun fold_proof_terms f =
+ let
+ fun proof (ZConstp (_, _, _, inst)) = ZVars.fold (f o #2) inst
+ | proof (ZHyp t) = f t
+ | proof (ZAbst (_, _, p)) = proof p
+ | proof (ZAbsp (_, t, p)) = f t #> proof p
+ | proof (ZAppt (p, t)) = proof p #> f t
+ | proof (ZAppp (p, q)) = proof p #> proof q
+ | proof _ = I;
+ in proof end;
+
+local exception Found in
+
+fun exists_proof_terms P prf =
+ (fold_proof_terms (fn t => fn () => if P t then raise Found else ()) prf (); true)
+ handle Found => true;
+
+end;
-(* map structure *)
+(* substitution of bound variables *)
+
+fun incr_bv_same inc =
+ if inc = 0 then fn _ => Same.same
+ else
+ let
+ fun term lev (ZBound i) = if i >= lev then ZBound (i + inc) else raise Same.SAME
+ | term lev (ZAbs (a, T, t)) = ZAbs (a, T, term (lev + 1) t)
+ | term lev (ZApp (t, u)) =
+ (ZApp (term lev t, Same.commit (term lev) u) handle Same.SAME =>
+ ZApp (t, term lev u))
+ | term _ _ = raise Same.SAME;
+ in term end;
+
+fun incr_bv inc lev = Same.commit (incr_bv_same inc lev);
+
+fun incr_boundvars inc = incr_bv inc 0;
+
+fun subst_bound arg body =
+ let
+ fun term lev (ZBound i) =
+ if i < lev then raise Same.SAME (*var is locally bound*)
+ else if i = lev then incr_boundvars lev arg
+ else ZBound (i - 1) (*loose: change it*)
+ | term lev (ZAbs (a, T, t)) = ZAbs (a, T, term (lev + 1) t)
+ | term lev (ZApp (t, u)) =
+ (ZApp (term lev t, Same.commit (term lev) u)
+ handle Same.SAME => ZApp (t, term lev u))
+ | term _ _ = raise Same.SAME;
+ in Same.commit (term 0) body end;
+
+
+(* direct substitution *)
fun subst_type_same tvar =
let
@@ -287,20 +355,20 @@
fun map_proof_same typ term =
let
fun proof ZDummy = raise Same.SAME
- | proof (ZConstP (a, A, instT, inst)) =
+ | proof (ZConstp (a, A, instT, inst)) =
let val (instT', inst') = map_insts_same typ term (instT, inst)
- in ZConstP (a, A, instT', inst') end
- | proof (ZBoundP _) = raise Same.SAME
+ in ZConstp (a, A, instT', inst') end
+ | proof (ZBoundp _) = raise Same.SAME
| proof (ZHyp h) = ZHyp (term h)
| proof (ZAbst (a, T, p)) =
(ZAbst (a, typ T, Same.commit proof p) handle Same.SAME => ZAbst (a, T, proof p))
- | proof (ZAbsP (a, t, p)) =
- (ZAbsP (a, term t, Same.commit proof p) handle Same.SAME => ZAbsP (a, t, proof p))
+ | proof (ZAbsp (a, t, p)) =
+ (ZAbsp (a, term t, Same.commit proof p) handle Same.SAME => ZAbsp (a, t, proof p))
| proof (ZAppt (p, t)) =
(ZAppt (proof p, Same.commit term t) handle Same.SAME => ZAppt (p, term t))
- | proof (ZAppP (p, q)) =
- (ZAppP (proof p, Same.commit proof q) handle Same.SAME => ZAppP (p, proof q))
- | proof (ZClassP (T, c)) = ZClassP (typ T, c);
+ | proof (ZAppp (p, q)) =
+ (ZAppp (proof p, Same.commit proof q) handle Same.SAME => ZAppp (p, proof q))
+ | proof (ZClassp (T, c)) = ZClassp (typ T, c);
in proof end;
fun map_proof_types_same typ =
@@ -352,6 +420,8 @@
| typ_of (ZType1 (c, T)) = Type (c, [typ_of T])
| typ_of (ZType (c, Ts)) = Type (c, map typ_of Ts);
+fun typ_cache () = ZTypes.unsynchronized_cache typ_of;
+
fun term_of_consts consts =
let
val instance = Consts.instance consts;
@@ -370,6 +440,77 @@
val term_of = term_of_consts o Sign.consts_of;
+(* beta normalization wrt. environment *)
+
+fun could_beta_contract (ZApp (ZAbs _, _)) = true
+ | could_beta_contract (ZApp (t, u)) = could_beta_contract t orelse could_beta_contract u
+ | could_beta_contract (ZAbs (_, _, b)) = could_beta_contract b
+ | could_beta_contract _ = false;
+
+fun norm_type_same ztyp tyenv =
+ if Vartab.is_empty tyenv then Same.same
+ else
+ let
+ fun norm (ZTVar v) =
+ (case Type.lookup tyenv v of
+ SOME U => Same.commit norm (ztyp U)
+ | NONE => raise Same.SAME)
+ | norm (ZFun (T, U)) =
+ (ZFun (norm T, Same.commit norm U)
+ handle Same.SAME => ZFun (T, norm U))
+ | norm ZProp = raise Same.SAME
+ | norm (ZItself T) = ZItself (norm T)
+ | norm (ZType0 _) = raise Same.SAME
+ | norm (ZType1 (a, T)) = ZType1 (a, norm T)
+ | norm (ZType (a, Ts)) = ZType (a, Same.map norm Ts);
+ in norm end;
+
+fun norm_term_same {ztyp, zterm, typ} (envir as Envir.Envir {tyenv, tenv, ...}) tm =
+ if Envir.is_empty envir andalso not (could_beta_contract tm) then raise Same.SAME
+ else
+ let
+ val lookup =
+ if Vartab.is_empty tenv then K NONE
+ else ZVars.unsynchronized_cache (apsnd typ #> Envir.lookup envir #> Option.map zterm);
+
+ val normT = norm_type_same ztyp tyenv;
+
+ fun norm (ZVar (xi, T)) =
+ (case lookup (xi, T) of
+ SOME u => Same.commit norm u
+ | NONE => ZVar (xi, normT T))
+ | norm (ZBound _) = raise Same.SAME
+ | norm (ZConst0 _) = raise Same.SAME
+ | norm (ZConst1 (a, T)) = ZConst1 (a, normT T)
+ | norm (ZConst (a, Ts)) = ZConst (a, Same.map normT Ts)
+ | norm (ZAbs (a, T, t)) =
+ (ZAbs (a, normT T, Same.commit norm t)
+ handle Same.SAME => ZAbs (a, T, norm t))
+ | norm (ZApp (ZAbs (_, _, body), t)) = Same.commit norm (subst_bound t body)
+ | norm (ZApp (f, t)) =
+ ((case norm f of
+ ZAbs (_, _, body) => Same.commit norm (subst_bound t body)
+ | nf => ZApp (nf, Same.commit norm t))
+ handle Same.SAME => ZApp (f, norm t))
+ | norm _ = raise Same.SAME;
+ in norm tm end;
+
+fun norm_proof_same (cache as {ztyp, ...}) (envir as Envir.Envir {tyenv, ...}) prf =
+ if Envir.is_empty envir andalso not (exists_proof_terms could_beta_contract prf) then
+ raise Same.SAME
+ else map_proof_same (norm_type_same ztyp tyenv) (norm_term_same cache envir) prf;
+
+fun norm_cache thy =
+ let
+ val {ztyp, zterm} = zterm_cache_consts (Sign.consts_of thy);
+ val typ = typ_cache ();
+ in {ztyp = ztyp, zterm = zterm, typ = typ} end;
+
+fun norm_type tyenv = Same.commit (norm_type_same (ztyp_cache ()) tyenv);
+fun norm_term thy envir = Same.commit (norm_term_same (norm_cache thy) envir);
+fun norm_proof thy envir = Same.commit (norm_proof_same (norm_cache thy) envir);
+
+
(** proof construction **)
@@ -390,15 +531,15 @@
(case a of
ZVar v => if ZVars.defined tab v then tab else ZVars.update (v, a) tab
| _ => tab)));
- in ZConstP (a, t, instT, inst) end;
+ in ZConstp (a, t, instT, inst) end;
fun map_const_proof (f, g) prf =
(case prf of
- ZConstP (a, A, instT, inst) =>
+ ZConstp (a, A, instT, inst) =>
let
val instT' = ZTVars.map (fn ((x, _), _) => fn y => the_default y (try f x)) instT;
val inst' = ZVars.map (fn ((x, _), _) => fn y => the_default y (try g x)) inst;
- in ZConstP (a, A, instT', inst') end
+ in ZConstp (a, A, instT', inst') end
| _ => prf);
@@ -414,20 +555,20 @@
ZHyp (zterm_of thy A);
fun trivial_proof thy A =
- ZAbsP ("H", zterm_of thy A, ZBoundP 0);
+ ZAbsp ("H", zterm_of thy A, ZBoundp 0);
fun implies_intr_proof thy A prf =
let
val h = zterm_of thy A;
- fun proof i (ZHyp t) = if aconv_zterm (h, t) then ZBoundP i else raise Same.SAME
+ fun proof i (ZHyp t) = if aconv_zterm (h, t) then ZBoundp i else raise Same.SAME
| proof i (ZAbst (x, T, p)) = ZAbst (x, T, proof i p)
- | proof i (ZAbsP (x, t, p)) = ZAbsP (x, t, proof (i + 1) p)
+ | proof i (ZAbsp (x, t, p)) = ZAbsp (x, t, proof (i + 1) p)
| proof i (ZAppt (p, t)) = ZAppt (proof i p, t)
- | proof i (ZAppP (p, q)) =
- (ZAppP (proof i p, Same.commit (proof i) q) handle Same.SAME =>
- ZAppP (p, proof i q))
+ | proof i (ZAppp (p, q)) =
+ (ZAppp (proof i p, Same.commit (proof i) q) handle Same.SAME =>
+ ZAppp (p, proof i q))
| proof _ _ = raise Same.SAME;
- in ZAbsP ("H", h, Same.commit (proof 0) prf) end;
+ in ZAbsp ("H", h, Same.commit (proof 0) prf) end;
fun forall_intr_proof thy T (a, x) prf =
let
@@ -446,22 +587,22 @@
| _ => raise Same.SAME);
fun proof i (ZAbst (x, T, prf)) = ZAbst (x, T, proof (i + 1) prf)
- | proof i (ZAbsP (x, t, prf)) =
- (ZAbsP (x, term i t, Same.commit (proof i) prf) handle Same.SAME =>
- ZAbsP (x, t, proof i prf))
+ | proof i (ZAbsp (x, t, prf)) =
+ (ZAbsp (x, term i t, Same.commit (proof i) prf) handle Same.SAME =>
+ ZAbsp (x, t, proof i prf))
| proof i (ZAppt (p, t)) =
(ZAppt (proof i p, Same.commit (term i) t) handle Same.SAME =>
ZAppt (p, term i t))
- | proof i (ZAppP (p, q)) =
- (ZAppP (proof i p, Same.commit (proof i) q) handle Same.SAME =>
- ZAppP (p, proof i q))
+ | proof i (ZAppp (p, q)) =
+ (ZAppp (proof i p, Same.commit (proof i) q) handle Same.SAME =>
+ ZAppp (p, proof i q))
| proof _ _ = raise Same.SAME;
in ZAbst (a, Z, Same.commit (proof 0) prf) end;
fun forall_elim_proof thy t p = ZAppt (p, zterm_of thy t);
-fun of_class_proof (T, c) = ZClassP (ztyp_of T, c);
+fun of_class_proof (T, c) = ZClassp (ztyp_of T, c);
(* equality *)
@@ -484,7 +625,7 @@
in
val is_reflexive_proof =
- fn ZConstP (ZAxiom "Pure.reflexive", _, _, _) => true | _ => false;
+ fn ZConstp (ZAxiom "Pure.reflexive", _, _, _) => true | _ => false;
fun reflexive_proof thy T t =
let
@@ -502,7 +643,7 @@
val x = zterm t;
val y = zterm u;
val ax = map_const_proof (fn "'a" => A, fn "x" => x | "y" => y) symmetric_axiom;
- in ZAppP (ax, prf) end;
+ in ZAppp (ax, prf) end;
fun transitive_proof thy T t u v prf1 prf2 =
if is_reflexive_proof prf1 then prf2
@@ -515,7 +656,7 @@
val y = zterm u;
val z = zterm v;
val ax = map_const_proof (fn "'a" => A, fn "x" => x | "y" => y | "z" => z) transitive_axiom;
- in ZAppP (ZAppP (ax, prf1), prf2) end;
+ in ZAppp (ZAppp (ax, prf1), prf2) end;
fun equal_intr_proof thy t u prf1 prf2 =
let
@@ -523,7 +664,7 @@
val A = zterm t;
val B = zterm u;
val ax = map_const_proof (undefined, fn "A" => A | "B" => B) equal_intr_axiom;
- in ZAppP (ZAppP (ax, prf1), prf2) end;
+ in ZAppp (ZAppp (ax, prf1), prf2) end;
fun equal_elim_proof thy t u prf1 prf2 =
let
@@ -531,7 +672,7 @@
val A = zterm t;
val B = zterm u;
val ax = map_const_proof (undefined, fn "A" => A | "B" => B) equal_elim_axiom;
- in ZAppP (ZAppP (ax, prf1), prf2) end;
+ in ZAppp (ZAppp (ax, prf1), prf2) end;
fun abstract_rule_proof thy T U x t u prf =
let
@@ -543,7 +684,7 @@
val ax =
map_const_proof (fn "'a" => A | "'b" => B, fn "f" => f | "g" => g)
abstract_rule_axiom;
- in ZAppP (ax, forall_intr_proof thy T x prf) end;
+ in ZAppp (ax, forall_intr_proof thy T x prf) end;
fun combination_proof thy T U f g t u prf1 prf2 =
let
@@ -557,7 +698,7 @@
val ax =
map_const_proof (fn "'a" => A | "'b" => B, fn "f" => f' | "g" => g' | "x" => x | "y" => y)
combination_axiom;
- in ZAppP (ZAppP (ax, prf1), prf2) end;
+ in ZAppp (ZAppp (ax, prf1), prf2) end;
end;
@@ -627,10 +768,10 @@
val i = length asms;
val j = length Bs;
in
- mk_ZAbsP (map zterm Bs @ [zterm Bi']) (mk_ZAppP (prf, map ZBoundP
- (j downto 1) @ [mk_ZAbst (map (apsnd ztyp) params) (mk_ZAbsP (map zterm asms)
- (mk_ZAppP (mk_ZAppt (ZBoundP i, map ZBound ((length params - 1) downto 0)),
- map ZBoundP (((i-m-1) downto 0) @ ((i-1) downto (i-m))))))]))
+ ZAbsps (map zterm Bs @ [zterm Bi']) (ZAppps (prf, map ZBoundp
+ (j downto 1) @ [ZAbsts (map (apsnd ztyp) params) (ZAbsps (map zterm asms)
+ (ZAppps (ZAppts (ZBoundp i, map ZBound ((length params - 1) downto 0)),
+ map ZBoundp (((i-m-1) downto 0) @ ((i-1) downto (i-m))))))]))
end;
fun permute_prems_proof thy prems' j k prf =
@@ -638,8 +779,30 @@
val {zterm, ...} = zterm_cache thy;
val n = length prems';
in
- mk_ZAbsP (map zterm prems')
- (mk_ZAppP (prf, map ZBoundP ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k))))
+ ZAbsps (map zterm prems')
+ (ZAppps (prf, map ZBoundp ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k))))
+ end;
+
+
+(* higher-order resolution *)
+
+fun mk_asm_prf C i m =
+ let
+ fun imp _ i 0 = ZBoundp i
+ | imp (ZApp (ZApp (ZConst0 "Pure.imp", A), B)) i m = ZAbsp ("H", A, imp B (i + 1) (m - 1))
+ | imp _ i _ = ZBoundp i;
+ fun all (ZApp (ZConst1 ("Pure.all", _), ZAbs (a, T, t))) = ZAbst (a, T, all t)
+ | all t = imp t (~ i) m
+ in all C end;
+
+fun assumption_proof thy envir Bs Bi n prf =
+ let
+ val cache as {zterm, ...} = norm_cache thy;
+ val normt = zterm #> Same.commit (norm_term_same cache envir);
+ in
+ ZAbsps (map normt Bs)
+ (ZAppps (prf, map ZBoundp (length Bs - 1 downto 0) @ [mk_asm_prf (normt Bi) n ~1]))
+ |> Same.commit (norm_proof_same cache envir)
end;
end;