defer rew_proof on unnamed PThm node as open_proof operation: significant performance improvement;
misc tuning and clarification;
--- a/src/HOL/Tools/inductive_realizer.ML Thu Jul 25 14:01:06 2019 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Fri Jul 26 09:35:02 2019 +0200
@@ -14,7 +14,7 @@
struct
fun name_of_thm thm =
- (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
+ (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _, _), _)) => cons name | _ => I)
[Thm.proof_of thm] [] of
[name] => name
| _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
--- a/src/HOL/Tools/rewrite_hol_proof.ML Thu Jul 25 14:01:06 2019 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Fri Jul 26 09:35:02 2019 +0200
@@ -305,9 +305,9 @@
(** Replace congruence rules by substitution rules **)
-fun strip_cong ps (PThm (_, (("HOL.cong", _, _), _)) % _ % _ % SOME x % SOME y %%
+fun strip_cong ps (PThm (_, (("HOL.cong", _, _, _), _)) % _ % _ % SOME x % SOME y %%
prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1
- | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f %% _) = SOME (f, ps)
+ | strip_cong ps (PThm (_, (("HOL.refl", _, _, _), _)) % SOME f %% _) = SOME (f, ps)
| strip_cong _ _ = NONE;
val subst_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of subst))));
@@ -330,15 +330,15 @@
fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
-fun elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % _ % _ %% prf1 %% prf2) =
+fun elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _, _), _)) % _ % _ %% prf1 %% prf2) =
Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
- | elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) =
+ | elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _, _), _)) % P % _ %% prf) =
Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
(strip_cong [] (Proofterm.incr_pboundvars 1 0 prf))
- | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) =
+ | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _, _), _)) % _ % _ %% prf1 %% prf2) =
Option.map (make_subst Ts prf2 [] o
apsnd (map (make_sym Ts))) (strip_cong [] prf1)
- | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) =
+ | elim_cong_aux Ts (PThm (_, (("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))
| elim_cong_aux _ _ = NONE;
--- a/src/Pure/Proof/extraction.ML Thu Jul 25 14:01:06 2019 +0200
+++ b/src/Pure/Proof/extraction.ML Fri Jul 26 09:35:02 2019 +0200
@@ -596,9 +596,9 @@
(corr_prf1 % u %% corr_prf2, defs2)
end
- | corr d vs ts Ts hs cs _ (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ defs =
+ | corr d vs ts Ts hs cs _ (prf0 as PThm (_, ((name, prop, SOME Ts', open_proof), body))) _ defs =
let
- val prf = Proofterm.join_proof body;
+ val prf = Proofterm.join_proof body |> open_proof;
val (vs', tye) = find_inst prop Ts ts vs;
val shyps = mk_shyps tye;
val sprfs = mk_sprfs cs tye;
@@ -624,7 +624,7 @@
val corr_prf' =
Proofterm.proof_combP (Proofterm.proof_combt
(PThm (serial (),
- ((corr_name name vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
+ ((corr_name name vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev)), I),
Future.value (Proofterm.approximate_proof_body corr_prf))),
vfs_of corr_prop),
map PBound (length shyps - 1 downto 0)) |>
@@ -694,9 +694,9 @@
in (f $ t, defs'') end
end
- | extr d vs ts Ts hs (prf0 as PThm (_, ((s, prop, SOME Ts'), body))) defs =
+ | extr d vs ts Ts hs (prf0 as PThm (_, ((s, prop, SOME Ts', open_proof), body))) defs =
let
- val prf = Proofterm.join_proof body;
+ val prf = Proofterm.join_proof body |> open_proof;
val (vs', tye) = find_inst prop Ts ts vs;
val shyps = mk_shyps tye;
val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
@@ -741,7 +741,7 @@
val corr_prf'' =
Proofterm.proof_combP (Proofterm.proof_combt
(PThm (serial (),
- ((corr_name s vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
+ ((corr_name s vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev)), I),
Future.value (Proofterm.approximate_proof_body corr_prf'))),
vfs_of corr_prop),
map PBound (length shyps - 1 downto 0)) |>
--- a/src/Pure/Proof/proof_checker.ML Thu Jul 25 14:01:06 2019 +0200
+++ b/src/Pure/Proof/proof_checker.ML Fri Jul 26 09:35:02 2019 +0200
@@ -84,7 +84,7 @@
Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
end;
- fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
+ fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts, _), _))) =
let
val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
val prop = Thm.prop_of thm;
--- a/src/Pure/Proof/proof_rewrite_rules.ML Thu Jul 25 14:01:06 2019 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri Jul 26 09:35:02 2019 +0200
@@ -35,12 +35,12 @@
val equal_elim_axm = ax Proofterm.equal_elim_axm [];
val symmetric_axm = ax Proofterm.symmetric_axm [propT];
- fun rew' (PThm (_, (("Pure.protectD", _, _), _)) % _ %%
- (PThm (_, (("Pure.protectI", _, _), _)) % _ %% prf)) = SOME prf
- | rew' (PThm (_, (("Pure.conjunctionD1", _, _), _)) % _ % _ %%
- (PThm (_, (("Pure.conjunctionI", _, _), _)) % _ % _ %% prf %% _)) = SOME prf
- | rew' (PThm (_, (("Pure.conjunctionD2", _, _), _)) % _ % _ %%
- (PThm (_, (("Pure.conjunctionI", _, _), _)) % _ % _ %% _ %% prf)) = SOME prf
+ fun rew' (PThm (_, (("Pure.protectD", _, _, _), _)) % _ %%
+ (PThm (_, (("Pure.protectI", _, _, _), _)) % _ %% prf)) = SOME prf
+ | rew' (PThm (_, (("Pure.conjunctionD1", _, _, _), _)) % _ % _ %%
+ (PThm (_, (("Pure.conjunctionI", _, _, _), _)) % _ % _ %% prf %% _)) = SOME prf
+ | rew' (PThm (_, (("Pure.conjunctionD2", _, _, _), _)) % _ % _ %%
+ (PThm (_, (("Pure.conjunctionI", _, _, _), _)) % _ % _ %% _ %% prf)) = SOME prf
| rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
(PAxm ("Pure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
| rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %%
@@ -50,14 +50,14 @@
| rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
(PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
_ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %%
- ((tg as PThm (_, (("Pure.protectI", _, _), _))) % _ %% prf2)) =
+ ((tg as PThm (_, (("Pure.protectI", _, _, _), _))) % _ %% prf2)) =
SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
| rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
(PAxm ("Pure.symmetric", _, _) % _ % _ %%
(PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
_ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1)) %%
- ((tg as PThm (_, (("Pure.protectI", _, _), _))) % _ %% prf2)) =
+ ((tg as PThm (_, (("Pure.protectI", _, _, _), _))) % _ %% prf2)) =
SOME (tg %> B %% (equal_elim_axm %> A %> B %%
(symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
@@ -233,7 +233,7 @@
(AbsP (s, t, fst (insert_refl defs Ts prf)), false)
| insert_refl defs Ts prf =
(case Proofterm.strip_combt prf of
- (PThm (_, ((s, prop, SOME Ts), _)), ts) =>
+ (PThm (_, ((s, prop, SOME Ts, _), _)), ts) =>
if member (op =) defs s then
let
val vs = vars_of prop;
@@ -259,7 +259,7 @@
let
val cnames = map (fst o dest_Const o fst) defs';
val thms = Proofterm.fold_proof_atoms true
- (fn PThm (_, ((name, prop, _), _)) =>
+ (fn PThm (_, ((name, prop, _, _), _)) =>
if member (op =) defnames name orelse
not (exists_Const (member (op =) cnames o #1) prop)
then I
--- a/src/Pure/Proof/proof_syntax.ML Thu Jul 25 14:01:06 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Fri Jul 26 09:35:02 2019 +0200
@@ -167,7 +167,7 @@
fun proof_syntax prf =
let
val thm_names = Symtab.keys (Proofterm.fold_proof_atoms true
- (fn PThm (_, ((name, _, _), _)) => if name <> "" then Symtab.update (name, ()) else I
+ (fn PThm (_, ((name, _, _, _), _)) => if name <> "" then Symtab.update (name, ()) else I
| _ => I) [prf] Symtab.empty);
val axm_names = Symtab.keys (Proofterm.fold_proof_atoms true
(fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty);
@@ -184,7 +184,7 @@
val prf = Thm.proof_of thm;
val prf' =
(case Proofterm.strip_combt (fst (Proofterm.strip_combP prf)) of
- (PThm (_, ((_, prop', _), body)), _) =>
+ (PThm (_, ((_, prop', _, _), body)), _) =>
if prop = prop' then Proofterm.join_proof body else prf
| _ => prf)
in if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf' end;
--- a/src/Pure/Proof/reconstruct.ML Thu Jul 25 14:01:06 2019 +0200
+++ b/src/Pure/Proof/reconstruct.ML Fri Jul 26 09:35:02 2019 +0200
@@ -209,7 +209,7 @@
add_cnstrt Ts (v $ t) (prf % SOME t) cnstrts env3 vTs'
(u, Const ("Pure.all", (T --> propT) --> propT) $ v)
end)
- | mk_cnstrts env _ _ vTs (prf as PThm (_, ((_, prop, opTs), _))) =
+ | mk_cnstrts env _ _ vTs (prf as PThm (_, ((_, prop, opTs, _), _))) =
mk_cnstrts_atom env vTs prop opTs prf
| mk_cnstrts env _ _ vTs (prf as PAxm (_, prop, opTs)) =
mk_cnstrts_atom env vTs prop opTs prf
@@ -312,7 +312,7 @@
Const ("Pure.imp", _) $ P $ Q => Q
| _ => error "prop_of: ==> expected")
| prop_of0 Hs (Hyp t) = t
- | prop_of0 Hs (PThm (_, ((_, prop, SOME Ts), _))) = prop_of_atom prop Ts
+ | prop_of0 Hs (PThm (_, ((_, prop, SOME Ts, _), _))) = prop_of_atom prop Ts
| prop_of0 Hs (PAxm (_, prop, SOME Ts)) = prop_of_atom prop Ts
| prop_of0 Hs (OfClass (T, c)) = Logic.mk_of_class (T, c)
| prop_of0 Hs (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts
@@ -330,6 +330,8 @@
fun expand_proof ctxt thms prf =
let
+ val thy = Proof_Context.theory_of ctxt;
+
fun expand maxidx prfs (AbsP (s, t, prf)) =
let val (maxidx', prfs', prf') = expand maxidx prfs prf
in (maxidx', prfs', AbsP (s, t, prf')) end
@@ -344,7 +346,7 @@
| expand maxidx prfs (prf % t) =
let val (maxidx', prfs', prf') = expand maxidx prfs prf
in (maxidx', prfs', prf' % t) end
- | expand maxidx prfs (prf as PThm (_, ((a, prop, SOME Ts), body))) =
+ | expand maxidx prfs (prf as PThm (_, ((a, prop, SOME Ts, open_proof), body))) =
if not (exists
(fn (b, NONE) => a = b
| (b, SOME prop') => a = b andalso prop = prop') thms)
@@ -357,8 +359,11 @@
val _ =
message ctxt (fn () =>
"Reconstructing proof of " ^ a ^ "\n" ^ Syntax.string_of_term ctxt prop);
- val prf' = Proofterm.forall_intr_vfs_prf prop
- (reconstruct_proof ctxt prop (Proofterm.join_proof body));
+ val prf' =
+ Proofterm.join_proof body
+ |> open_proof
+ |> reconstruct_proof ctxt prop
+ |> Proofterm.forall_intr_vfs_prf prop;
val (maxidx', prfs', prf) = expand
(Proofterm.maxidx_proof prf' ~1) prfs prf'
in (maxidx' + maxidx + 1, Proofterm.incr_indexes (maxidx + 1) prf,
--- a/src/Pure/proofterm.ML Thu Jul 25 14:01:06 2019 +0200
+++ b/src/Pure/proofterm.ML Fri Jul 26 09:35:02 2019 +0200
@@ -20,7 +20,7 @@
| PAxm of string * term * typ list option
| OfClass of typ * class
| Oracle of string * term * typ list option
- | PThm of serial * ((string * term * typ list option) * proof_body future)
+ | PThm of serial * ((string * term * typ list option * (proof -> proof)) * proof_body future)
and proof_body = PBody of
{oracles: (string * term) Ord_List.T,
thms: (serial * thm_node) Ord_List.T,
@@ -178,7 +178,7 @@
| PAxm of string * term * typ list option
| OfClass of typ * class
| Oracle of string * term * typ list option
- | PThm of serial * ((string * term * typ list option) * proof_body future)
+ | PThm of serial * ((string * term * typ list option * (proof -> proof)) * proof_body future)
and proof_body = PBody of
{oracles: (string * term) Ord_List.T,
thms: (serial * thm_node) Ord_List.T,
@@ -295,7 +295,7 @@
let
val (oracles, thms) = fold_proof_atoms false
(fn Oracle (s, prop, _) => apfst (cons (s, prop))
- | PThm (i, ((name, prop, _), body)) => apsnd (cons (i, make_thm_node name prop body))
+ | PThm (i, ((name, prop, _, _), body)) => apsnd (cons (i, make_thm_node name prop body))
| _ => I) [prf] ([], []);
in
PBody
@@ -335,8 +335,9 @@
fn PAxm (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
fn OfClass (a, b) => ([b], typ a),
fn Oracle (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
- fn PThm (a, ((b, c, d), body)) =>
- ([int_atom a, b], triple term (option (list typ)) proof_body (c, d, Future.join body))]
+ fn PThm (a, ((b, c, d, open_proof), body)) =>
+ ([int_atom a, b], triple term (option (list typ)) proof_body
+ (c, d, map_proof_of open_proof (Future.join body)))]
and proof_body (PBody {oracles, thms, proof = prf}) =
triple (list (pair string term)) (list pthm) proof (oracles, thms, prf)
and pthm (a, thm_node) =
@@ -370,7 +371,7 @@
fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in Oracle (a, c, d) end,
fn ([a, b], c) =>
let val (d, e, f) = triple term (option (list typ)) proof_body c
- in PThm (int_atom a, ((b, d, e), Future.value f)) end]
+ in PThm (int_atom a, ((b, d, e, I), Future.value f)) end]
and proof_body x =
let val (a, b, c) = triple (list (pair string term)) (list pthm) proof x
in PBody {oracles = a, thms = b, proof = c} end
@@ -444,8 +445,8 @@
| proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
| proof (OfClass T_c) = ofclass T_c
| proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
- | proof (PThm (i, ((a, prop, SOME Ts), body))) =
- PThm (i, ((a, prop, SOME (typs Ts)), body))
+ | proof (PThm (i, ((a, prop, SOME Ts, open_proof), body))) =
+ PThm (i, ((a, prop, SOME (typs Ts), open_proof), body))
| proof _ = raise Same.SAME;
in proof end;
@@ -470,7 +471,7 @@
| fold_proof_terms _ g (PAxm (_, _, SOME Ts)) = fold g Ts
| fold_proof_terms _ g (OfClass (T, _)) = g T
| fold_proof_terms _ g (Oracle (_, _, SOME Ts)) = fold g Ts
- | fold_proof_terms _ g (PThm (_, ((_, _, SOME Ts), _))) = fold g Ts
+ | fold_proof_terms _ g (PThm (_, ((_, _, SOME Ts, _), _))) = fold g Ts
| fold_proof_terms _ _ _ = I;
fun maxidx_proof prf = fold_proof_terms Term.maxidx_term Term.maxidx_typ prf;
@@ -484,8 +485,8 @@
fun change_type opTs (PAxm (name, prop, _)) = PAxm (name, prop, opTs)
| change_type (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
| change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs)
- | change_type opTs (PThm (i, ((name, prop, _), body))) =
- PThm (i, ((name, prop, opTs), body))
+ | change_type opTs (PThm (i, ((name, prop, _, open_proof), body))) =
+ PThm (i, ((name, prop, opTs, open_proof), body))
| change_type _ prf = prf;
@@ -632,8 +633,8 @@
OfClass (htypeT Envir.norm_type_same T, c)
| norm (Oracle (s, prop, Ts)) =
Oracle (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts)
- | norm (PThm (i, ((s, t, Ts), body))) =
- PThm (i, ((s, t, Same.map_option (htypeTs Envir.norm_types_same) Ts), body))
+ | norm (PThm (i, ((s, t, Ts, open_proof), body))) =
+ PThm (i, ((s, t, Same.map_option (htypeTs Envir.norm_types_same) Ts, open_proof), body))
| norm _ = raise Same.SAME;
in Same.commit norm end;
@@ -776,7 +777,7 @@
let val U = Term.itselfT T --> propT
in Const ("Pure.OfClass", U --> proofT) $ Const (Logic.const_of_class c, U) end;
-fun term_of _ (PThm (_, ((name, _, Ts), _))) =
+fun term_of _ (PThm (_, ((name, _, Ts, _), _))) =
fold AppT (these Ts) (Const (Long_Name.append "thm" name, proofT))
| term_of _ (PAxm (name, _, Ts)) =
fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT))
@@ -949,8 +950,8 @@
OfClass (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 (i, ((s, prop, Ts), body))) =
- PThm (i, ((s, prop, (Same.map_option o Same.map) (Logic.incr_tvar inc) Ts), body))
+ | lift' _ _ (PThm (i, ((s, prop, Ts, open_proof), body))) =
+ PThm (i, ((s, prop, (Same.map_option o Same.map) (Logic.incr_tvar inc) Ts, open_proof), body))
| lift' _ _ _ = raise Same.SAME
and lifth' Us Ts prf = (lift' Us Ts prf handle Same.SAME => prf);
@@ -1287,7 +1288,7 @@
(case prf of
PAxm (_, prop, _) => prop
| Oracle (_, prop, _) => prop
- | PThm (_, ((_, prop, _), _)) => prop
+ | PThm (_, ((_, prop, _, _), _)) => prop
| _ => raise Fail "shrink: proof not in normal form");
val vs = vars_of prop;
val (ts', ts'') = chop (length vs) ts;
@@ -1376,7 +1377,8 @@
| mtch Ts i j inst (OfClass (T1, c1), OfClass (T2, c2)) =
if c1 = c2 then matchT inst (T1, T2)
else raise PMatch
- | mtch Ts i j inst (PThm (_, ((name1, prop1, opTs), _)), PThm (_, ((name2, prop2, opUs), _))) =
+ | mtch Ts i j inst
+ (PThm (_, ((name1, prop1, opTs, _), _)), PThm (_, ((name2, prop2, opUs, _), _))) =
if name1 = name2 andalso prop1 = prop2 then
optmatch matchTs inst (opTs, opUs)
else raise PMatch
@@ -1422,8 +1424,8 @@
| subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts)
| subst _ _ (OfClass (T, c)) = OfClass (substT T, c)
| subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts)
- | subst _ _ (PThm (i, ((id, prop, Ts), body))) =
- PThm (i, ((id, prop, Same.map_option substTs Ts), body))
+ | subst _ _ (PThm (i, ((id, prop, Ts, open_proof), body))) =
+ PThm (i, ((id, prop, Same.map_option substTs Ts, open_proof), body))
| subst _ _ _ = raise Same.SAME;
in fn t => subst 0 0 t handle Same.SAME => t end;
@@ -1447,7 +1449,7 @@
| (Hyp (Var _), _) => true
| (PAxm (a, _, _), PAxm (b, _, _)) => a = b andalso matchrands prf1 prf2
| (OfClass (_, c), OfClass (_, d)) => c = d andalso matchrands prf1 prf2
- | (PThm (_, ((a, propa, _), _)), PThm (_, ((b, propb, _), _))) =>
+ | (PThm (_, ((a, propa, _, _), _)), PThm (_, ((b, propb, _, _), _))) =>
a = b andalso propa = propb andalso matchrands prf1 prf2
| (PBound i, PBound j) => i = j andalso matchrands prf1 prf2
| (AbsP _, _) => true (*because of possible eta equality*)
@@ -1603,7 +1605,7 @@
| clean maxidx prfs (prf % t) =
let val (maxidx', prfs', prf') = clean maxidx prfs prf
in (maxidx', prfs', prf' % t) end
- | clean maxidx prfs (PThm (_, (("", prop, SOME Ts), body))) =
+ | clean maxidx prfs (PThm (_, (("", prop, SOME Ts, _), body))) =
let
val (maxidx', prf, prfs') =
(case AList.lookup (op =) prfs prop of
@@ -1707,47 +1709,39 @@
fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
val body0 =
- if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
- else
- let
- val rew = rew_proof thy;
- val prf0 = fold_rev implies_intr_proof hyps prf;
- in
- (singleton o Future.cond_forks)
- {name = "Proofterm.prepare_thm_proof", group = NONE,
- deps = [], pri = 1, interrupts = true}
- (fn () => make_body0 (rew prf0))
- end;
+ Future.value (make_body0
+ (if proofs_enabled () then fold_rev implies_intr_proof hyps prf else MinProof))
fun export i prf1 =
- if Options.default_bool "export_proofs" then
+ if Options.default_bool "export_proofs" then
Export.export thy (Path.binding0 (Path.make ["proofs", string_of_int i]))
- (Buffer.chunks
- (YXML.buffer_body (Term_XML.Encode.term (term_of_proof prf1)) Buffer.empty))
+ (Buffer.chunks (YXML.buffer_body (Term_XML.Encode.term (term_of_proof prf1)) Buffer.empty))
else ();
fun prune prf1 =
- if Options.default_bool "prune_proofs" then MinProof else shrink_proof prf1;
+ if Options.default_bool "prune_proofs" then MinProof
+ else shrink_proof prf1;
- fun publish i = tap (export i) #> prune;
+ fun publish i = clean_proof thy #> tap (export i) #> prune;
fun new_prf () =
let
val i = proof_serial ();
val postproc =
unconstrainT_body thy (atyp_map, constraints) #>
- name <> "" ? map_proof_of (clean_proof thy #> publish i);
+ name <> "" ? map_proof_of (publish i);
in (i, fulfill_proof_future thy promises postproc body0) end;
val (i, body') =
(*non-deterministic, depends on unknown promises*)
(case strip_combt (fst (strip_combP prf)) of
- (PThm (i, ((a, prop', NONE), body')), args') =>
+ (PThm (i, ((a, prop', NONE, _), body')), args') =>
if (a = "" orelse a = name) andalso prop1 = prop' andalso args = args'
then (i, body' |> (a = "" andalso name <> "") ? Future.map (map_proof_of (publish i)))
else new_prf ()
| _ => new_prf ());
- val head = PThm (i, ((name, prop1, NONE), body'));
+ val open_proof = if name = "" then clean_proof thy #> shrink_proof else I;
+ val head = PThm (i, ((name, prop1, NONE, open_proof), body'));
in ((i, make_thm_node name prop1 body'), head, args, argsP, args1) end;
fun thm_proof thy name shyps hyps concl promises body =
@@ -1762,11 +1756,11 @@
fun get_name shyps hyps prop prf =
let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in
(case strip_combt (fst (strip_combP prf)) of
- (PThm (_, ((name, prop', _), _)), _) => if prop = prop' then name else ""
+ (PThm (_, ((name, prop', _, _), _)), _) => if prop = prop' then name else ""
| _ => "")
end;
-fun guess_name (PThm (_, ((name, _, _), _))) = name
+fun guess_name (PThm (_, ((name, _, _, _), _))) = name
| guess_name (prf %% Hyp _) = guess_name prf
| guess_name (prf %% OfClass _) = guess_name prf
| guess_name (prf % NONE) = guess_name prf