--- a/src/Pure/Proof/extraction.ML Thu Dec 14 12:21:09 2023 +0100
+++ b/src/Pure/Proof/extraction.ML Thu Dec 14 17:33:45 2023 +0100
@@ -184,7 +184,7 @@
PBody
{oracles = Ord_List.make Proofterm.oracle_ord oracles,
thms = Ord_List.make Proofterm.thm_ord thms,
- zboxes = Proofterm.empty_zboxes,
+ zboxes = ZTerm.empty_zboxes,
zproof = ZDummy,
proof = prf};
in Proofterm.thm_body body end;
--- a/src/Pure/proofterm.ML Thu Dec 14 12:21:09 2023 +0100
+++ b/src/Pure/proofterm.ML Thu Dec 14 17:33:45 2023 +0100
@@ -13,7 +13,6 @@
prop: term, types: typ list option}
type thm_body
type thm_node
- type zboxes = (zterm * zproof future) Inttab.table
datatype proof =
MinProof
| PBound of int
@@ -29,7 +28,7 @@
and proof_body = PBody of
{oracles: ((string * Position.T) * term option) Ord_List.T,
thms: (serial * thm_node) Ord_List.T,
- zboxes: zboxes,
+ zboxes: ZTerm.zboxes,
zproof: zproof,
proof: proof}
type oracle = (string * Position.T) * term option
@@ -61,8 +60,6 @@
val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T
val union_thms: thm Ord_List.T -> thm Ord_List.T -> thm Ord_List.T
val unions_thms: thm Ord_List.T list -> thm Ord_List.T
- val empty_zboxes: zboxes
- val union_zboxes: zboxes -> zboxes -> zboxes
val no_proof_body: zproof -> proof -> proof_body
val no_thm_names: proof -> proof
val no_thm_proofs: proof -> proof
@@ -217,8 +214,6 @@
{serial: serial, pos: Position.T list, theory_name: string, name: string,
prop: term, types: typ list option};
-type zboxes = (zterm * zproof future) Inttab.table;
-
datatype proof =
MinProof
| PBound of int
@@ -234,7 +229,7 @@
and proof_body = PBody of
{oracles: ((string * Position.T) * term option) Ord_List.T,
thms: (serial * thm_node) Ord_List.T,
- zboxes: zboxes,
+ zboxes: ZTerm.zboxes,
zproof: zproof,
proof: proof}
and thm_body =
@@ -343,11 +338,8 @@
val union_thms = Ord_List.union thm_ord;
val unions_thms = Ord_List.unions thm_ord;
-val empty_zboxes: zboxes = Inttab.empty;
-val union_zboxes = curry (Inttab.merge (fn (_: (zterm * zproof future), _) => true));
-
fun no_proof_body zproof proof =
- PBody {oracles = [], thms = [], zboxes = empty_zboxes, zproof = zproof, proof = proof};
+ PBody {oracles = [], thms = [], zboxes = ZTerm.empty_zboxes, zproof = zproof, proof = proof};
val no_thm_body = thm_body (no_proof_body ZDummy MinProof);
fun no_thm_names (Abst (x, T, prf)) = Abst (x, T, no_thm_names prf)
@@ -471,7 +463,7 @@
val (a, b, c) =
triple (list (pair (pair string (Position.of_properties o properties))
(option (term consts)))) (list (thm consts)) (proof consts) x;
- in PBody {oracles = a, thms = b, zboxes = empty_zboxes, zproof = ZDummy, proof = c} end
+ in PBody {oracles = a, thms = b, zboxes = ZTerm.empty_zboxes, zproof = ZDummy, proof = c} end
and thm consts x =
let
val (a, (b, (c, (d, e)))) =
@@ -1990,7 +1982,7 @@
(fold (fn (_, PBody {oracles, ...}) => not (null oracles) ? cons oracles) ps [oracles0]);
val thms =
unions_thms (fold (fn (_, PBody {thms, ...}) => not (null thms) ? cons thms) ps [thms0]);
- val zboxes = fold (fn (_, PBody {zboxes, ...}) => union_zboxes zboxes) ps zboxes0;
+ val zboxes = fold (fn (_, PBody {zboxes, ...}) => ZTerm.union_zboxes zboxes) ps zboxes0;
val proof = rew_proof thy proof0;
in
PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = proof}
@@ -2260,7 +2252,7 @@
val zproof = ZTerm.todo_proof ();
val proof_body =
- PBody {oracles = [], thms = [thm], zboxes = empty_zboxes, zproof = zproof, proof = proof};
+ PBody {oracles = [], thms = [thm], zboxes = ZTerm.empty_zboxes, zproof = zproof, proof = proof};
in (thm, proof_body) end;
in
--- a/src/Pure/thm.ML Thu Dec 14 12:21:09 2023 +0100
+++ b/src/Pure/thm.ML Thu Dec 14 17:33:45 2023 +0100
@@ -750,7 +750,7 @@
make_deriv0 promises
(PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = proof});
-val empty_deriv = make_deriv [] [] [] Proofterm.empty_zboxes ZDummy MinProof;
+val empty_deriv = make_deriv [] [] [] ZTerm.empty_zboxes ZDummy MinProof;
(* inference rules *)
@@ -768,7 +768,7 @@
val oracles' = Proofterm.union_oracles oracles1 oracles2;
val thms' = Proofterm.union_thms thms1 thms2;
- val zboxes' = Proofterm.union_zboxes zboxes1 zboxes2;
+ val zboxes' = ZTerm.union_zboxes zboxes1 zboxes2;
val proofs = Proofterm.get_proofs_level ();
val zproof' = if Proofterm.zproof_enabled proofs then zproof zprf1 zprf2 else ZDummy;
@@ -780,7 +780,7 @@
fun deriv_rule0 zproof proof =
let val proofs = Proofterm.get_proofs_level () in
if Proofterm.proof_enabled proofs orelse Proofterm.zproof_enabled proofs then
- deriv_rule1 I I (make_deriv [] [] [] Proofterm.empty_zboxes
+ deriv_rule1 I I (make_deriv [] [] [] ZTerm.empty_zboxes
(if Proofterm.zproof_enabled proofs then zproof () else ZDummy)
(if Proofterm.proof_enabled proofs then proof () else MinProof))
else empty_deriv
@@ -844,7 +844,7 @@
val i = serial ();
val future = future_thm |> Future.map (future_result i cert sorts prop);
in
- Thm (make_deriv [(i, future)] [] [] Proofterm.empty_zboxes ZDummy MinProof,
+ Thm (make_deriv [(i, future)] [] [] ZTerm.empty_zboxes ZDummy MinProof,
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -985,12 +985,12 @@
local
-val empty_digest = ([], [], Proofterm.empty_zboxes);
+val empty_digest = ([], [], ZTerm.empty_zboxes);
fun union_digest (oracles1, thms1, zboxes1) (oracles2, thms2, zboxes2) =
(Proofterm.union_oracles oracles1 oracles2,
Proofterm.union_thms thms1 thms2,
- Proofterm.union_zboxes zboxes1 zboxes2);
+ ZTerm.union_zboxes zboxes1 zboxes2);
fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, zboxes, ...}, ...}, _)) =
(oracles, thms, zboxes);
@@ -1171,7 +1171,7 @@
then ZTerm.oracle_proof (Context.certificate_theory cert) name prop
else ZDummy;
in
- Thm (make_deriv [] [oracle] [] Proofterm.empty_zboxes zproof proof,
+ Thm (make_deriv [] [oracle] [] ZTerm.empty_zboxes zproof proof,
{cert = cert,
tags = [],
maxidx = maxidx,
--- a/src/Pure/zterm.ML Thu Dec 14 12:21:09 2023 +0100
+++ b/src/Pure/zterm.ML Thu Dec 14 17:33:45 2023 +0100
@@ -153,6 +153,10 @@
datatype ztyp = datatype ztyp
datatype zterm = datatype zterm
datatype zproof = datatype zproof
+ type zproof_const = zproof_name * zterm * ztyp ZTVars.table * zterm ZVars.table
+ type zboxes = (zterm * zproof future) Inttab.table
+ val empty_zboxes: zboxes
+ val union_zboxes: zboxes -> zboxes -> zboxes
val fold_tvars: (indexname * sort -> 'a -> 'a) -> ztyp -> 'a -> 'a
val fold_aterms: (zterm -> 'a -> 'a) -> zterm -> 'a -> 'a
val fold_types: (ztyp -> 'a -> 'a) -> zterm -> 'a -> 'a
@@ -525,38 +529,44 @@
val todo_proof = dummy_proof;
+(* boxes *)
+
+type zboxes = (zterm * zproof future) Inttab.table;
+
+val empty_zboxes: zboxes = Inttab.empty;
+val union_zboxes: zboxes -> zboxes -> zboxes = curry (Inttab.merge (K true));
+
+
(* constants *)
-fun const_proof thy a A =
+type zproof_const = zproof_name * zterm * ztyp ZTVars.table * zterm ZVars.table;
+
+fun zproof_const a A : zproof_const =
let
- val t = zterm_of thy A;
val instT =
- ZTVars.build (t |> (fold_types o fold_tvars) (fn v => fn tab =>
+ ZTVars.build (A |> (fold_types o fold_tvars) (fn v => fn tab =>
if ZTVars.defined tab v then tab else ZTVars.update (v, ZTVar v) tab));
val inst =
- ZVars.build (t |> fold_aterms (fn a => fn tab =>
- (case a of
- ZVar v => if ZVars.defined tab v then tab else ZVars.update (v, a) tab
+ ZVars.build (A |> fold_aterms (fn t => fn tab =>
+ (case t of
+ ZVar v => if ZVars.defined tab v then tab else ZVars.update (v, t) tab
| _ => tab)));
- in ZConstp (a, t, instT, inst) end;
+ in (a, A, instT, inst) end;
-fun map_const_proof (f, g) prf =
- (case prf of
- 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
- | _ => prf);
+fun make_const_proof (f, g) ((a, A, instT, inst): zproof_const) =
+ 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;
(* basic logic *)
-fun axiom_proof thy name =
- const_proof thy (ZAxiom name);
+fun axiom_proof thy name A =
+ ZConstp (zproof_const (ZAxiom name) (zterm_of thy A));
-fun oracle_proof thy name =
- const_proof thy (ZOracle name);
+fun oracle_proof thy name A =
+ ZConstp (zproof_const (ZOracle name) (zterm_of thy A));
fun assume_proof thy A =
ZHyp (zterm_of thy A);
@@ -627,7 +637,8 @@
val [reflexive_axiom, symmetric_axiom, transitive_axiom, equal_intr_axiom, equal_elim_axiom,
abstract_rule_axiom, combination_axiom] =
- Theory.equality_axioms |> map (fn (b, t) => axiom_proof thy0 (Sign.full_name thy0 b) t);
+ Theory.equality_axioms |> map (fn (b, t) =>
+ let val ZConstp c = axiom_proof thy0 (Sign.full_name thy0 b) t in c end);
in
@@ -639,7 +650,7 @@
val {ztyp, zterm} = zterm_cache thy;
val A = ztyp T;
val x = zterm t;
- in map_const_proof (fn "'a" => A, fn "x" => x) reflexive_axiom end;
+ in make_const_proof (fn "'a" => A, fn "x" => x) reflexive_axiom end;
fun symmetric_proof thy T t u prf =
if is_reflexive_proof prf then prf
@@ -649,7 +660,7 @@
val A = ztyp T;
val x = zterm t;
val y = zterm u;
- val ax = map_const_proof (fn "'a" => A, fn "x" => x | "y" => y) symmetric_axiom;
+ val ax = make_const_proof (fn "'a" => A, fn "x" => x | "y" => y) symmetric_axiom;
in ZAppp (ax, prf) end;
fun transitive_proof thy T t u v prf1 prf2 =
@@ -662,7 +673,7 @@
val x = zterm t;
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;
+ val ax = make_const_proof (fn "'a" => A, fn "x" => x | "y" => y | "z" => z) transitive_axiom;
in ZAppp (ZAppp (ax, prf1), prf2) end;
fun equal_intr_proof thy t u prf1 prf2 =
@@ -670,7 +681,7 @@
val {zterm, ...} = zterm_cache thy;
val A = zterm t;
val B = zterm u;
- val ax = map_const_proof (undefined, fn "A" => A | "B" => B) equal_intr_axiom;
+ val ax = make_const_proof (undefined, fn "A" => A | "B" => B) equal_intr_axiom;
in ZAppp (ZAppp (ax, prf1), prf2) end;
fun equal_elim_proof thy t u prf1 prf2 =
@@ -678,7 +689,7 @@
val {zterm, ...} = zterm_cache thy;
val A = zterm t;
val B = zterm u;
- val ax = map_const_proof (undefined, fn "A" => A | "B" => B) equal_elim_axiom;
+ val ax = make_const_proof (undefined, fn "A" => A | "B" => B) equal_elim_axiom;
in ZAppp (ZAppp (ax, prf1), prf2) end;
fun abstract_rule_proof thy T U x t u prf =
@@ -689,7 +700,7 @@
val f = zterm t;
val g = zterm u;
val ax =
- map_const_proof (fn "'a" => A | "'b" => B, fn "f" => f | "g" => g)
+ make_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;
@@ -703,7 +714,7 @@
val x = zterm t;
val y = zterm u;
val ax =
- map_const_proof (fn "'a" => A | "'b" => B, fn "f" => f' | "g" => g' | "x" => x | "y" => y)
+ make_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;