# HG changeset patch # User wenzelm # Date 1564126502 -7200 # Node ID 64ead6de6212643f14a46d8e14e8dc5c66e16054 # Parent c533bec6e92d4ae56204ede744334ae0d8563844 defer rew_proof on unnamed PThm node as open_proof operation: significant performance improvement; misc tuning and clarification; diff -r c533bec6e92d -r 64ead6de6212 src/HOL/Tools/inductive_realizer.ML --- 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])); diff -r c533bec6e92d -r 64ead6de6212 src/HOL/Tools/rewrite_hol_proof.ML --- 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; diff -r c533bec6e92d -r 64ead6de6212 src/Pure/Proof/extraction.ML --- 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)) |> diff -r c533bec6e92d -r 64ead6de6212 src/Pure/Proof/proof_checker.ML --- 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; diff -r c533bec6e92d -r 64ead6de6212 src/Pure/Proof/proof_rewrite_rules.ML --- 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 diff -r c533bec6e92d -r 64ead6de6212 src/Pure/Proof/proof_syntax.ML --- 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; diff -r c533bec6e92d -r 64ead6de6212 src/Pure/Proof/reconstruct.ML --- 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, diff -r c533bec6e92d -r 64ead6de6212 src/Pure/proofterm.ML --- 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