--- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Thu Dec 15 15:05:35 2016 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Fri Dec 16 19:50:46 2016 +0100
@@ -167,7 +167,7 @@
assms
|> map (apsnd (rewrite ctxt eqs'))
|> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
- |> Old_Z3_Proof_Tools.thm_net_of snd
+ |> Old_Z3_Proof_Tools.thm_net_of snd
fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion
@@ -183,14 +183,14 @@
if exact then (Thm.implies_elim thm1 th, ctxt)
else assume thm1 ctxt
val thms' = if exact then thms else th :: thms
- in
+ in
((insert (op =) i is, thms'),
(ctxt', Inttab.update (idx, Thm thm) ptab))
end
fun add (idx, ct) (cx as ((is, thms), (ctxt, ptab))) =
let
- val thm1 =
+ val thm1 =
Thm.trivial ct
|> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))
val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1
@@ -218,7 +218,7 @@
val mp_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm mp}
in
fun mp (MetaEq thm) p = Thm (Thm.implies_elim (comp meta_iffD1_c thm) p)
- | mp p_q p =
+ | mp p_q p =
let
val pq = thm_of p_q
val thm = comp iffD1_c pq handle THM _ => comp mp_c pq
@@ -509,7 +509,7 @@
(case lookup (Logic.mk_equals (apply2 Thm.term_of cp)) of
SOME eq => eq
| NONE => if exn then raise MONO else prove_refl cp)
-
+
val prove_exn = prove_eq true
and prove_safe = prove_eq false
@@ -752,7 +752,9 @@
fun check_after idx r ps ct (p, (ctxt, _)) =
if not (Config.get ctxt Old_SMT_Config.trace) then ()
else
- let val thm = thm_of p |> tap (Thm.join_proofs o single)
+ let
+ val thm = thm_of p
+ val _ = Thm.consolidate thm
in
if (Thm.cprop_of thm) aconvc ct then ()
else
@@ -852,7 +854,7 @@
fun discharge_assms_tac ctxt rules =
REPEAT (HEADGOAL (resolve_tac ctxt rules ORELSE' SOLVED' (discharge_sk_tac ctxt)))
-
+
fun discharge_assms ctxt rules thm =
if Thm.nprems_of thm = 0 then Goal.norm_result ctxt thm
else
@@ -881,7 +883,7 @@
if Config.get ctxt2 Old_SMT_Config.filter_only_facts then (is, @{thm TrueI})
else
(Thm @{thm TrueI}, cxp)
- |> fold (prove simpset vars) steps
+ |> fold (prove simpset vars) steps
|> discharge rules outer_ctxt
|> pair []
end
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Thu Dec 15 15:05:35 2016 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Fri Dec 16 19:50:46 2016 +0100
@@ -165,15 +165,17 @@
fun fold_body_thms f =
let
- fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) =>
+ fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) =>
fn (x, seen) =>
if Inttab.defined seen i then (x, seen)
else
let
- val body' = Future.join body
- val (x', seen') = app (n + (if name = "" then 0 else 1)) body'
+ val name = Proofterm.thm_node_name thm_node
+ val prop = Proofterm.thm_node_prop thm_node
+ val body = Future.join (Proofterm.thm_node_body thm_node)
+ val (x', seen') = app (n + (if name = "" then 0 else 1)) body
(x, Inttab.update (i, ()) seen)
- in (x' |> n = 0 ? f (name, prop, body'), seen') end)
+ in (x' |> n = 0 ? f (name, prop, body), seen') end)
in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end
in
--- a/src/HOL/Proofs/ex/Proof_Terms.thy Thu Dec 15 15:05:35 2016 +0100
+++ b/src/HOL/Proofs/ex/Proof_Terms.thy Fri Dec 16 19:50:46 2016 +0100
@@ -30,7 +30,7 @@
(*all theorems used in the graph of nested proofs*)
val all_thms =
Proofterm.fold_body_thms
- (fn (name, _, _) => insert (op =) name) [body] [];
+ (fn {name, ...} => insert (op =) name) [body] [];
\<close>
text \<open>
--- a/src/HOL/ROOT Thu Dec 15 15:05:35 2016 +0100
+++ b/src/HOL/ROOT Fri Dec 16 19:50:46 2016 +0100
@@ -18,10 +18,9 @@
description {*
HOL-Main with explicit proof terms.
*}
- options [document = false, quick_and_dirty = false]
+ options [document = false, quick_and_dirty = false, parallel_proofs = 0]
theories Proofs (*sequential change of global flag!*)
- theories List
- theories [checkpoint] "~~/src/HOL/Library/Old_Datatype"
+ theories "~~/src/HOL/Library/Old_Datatype"
files
"Tools/Quickcheck/Narrowing_Engine.hs"
"Tools/Quickcheck/PNF_Narrowing_Engine.hs"
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Thu Dec 15 15:05:35 2016 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Fri Dec 16 19:50:46 2016 +0100
@@ -293,7 +293,7 @@
| SOME _ => error ("Cannot associate a type with " ^ s ^
"\nsince it is no record or enumeration type");
-fun check_enum [] [] = NONE
+fun check_enum [] [] = NONE
| check_enum els [] = SOME ("has no element(s) " ^ commas els)
| check_enum [] cs = SOME ("has extra element(s) " ^
commas (map (Long_Name.base_name o fst) cs))
@@ -305,7 +305,7 @@
fun invert_map [] = I
| invert_map cmap =
map (apfst (the o AList.lookup (op =) (map swap cmap)));
-
+
fun add_type_def prfx (s, Basic_Type ty) (ids, thy) =
(check_no_assoc thy prfx s;
(ids,
@@ -677,7 +677,7 @@
"+", "-", "*", "/", "div", "mod", "**"]);
fun complex_expr (Number _) = false
- | complex_expr (Ident _) = false
+ | complex_expr (Ident _) = false
| complex_expr (Funct (s, es)) =
not (Symtab.defined builtin s) orelse exists complex_expr es
| complex_expr (Quantifier (_, _, _, e)) = complex_expr e
@@ -959,7 +959,7 @@
| SOME {vcs, path, ...} =>
let
val (proved, unproved) = partition_vcs vcs;
- val _ = Thm.join_proofs (maps (#2 o snd) proved);
+ val _ = List.app Thm.consolidate (maps (#2 o snd) proved);
val (proved', proved'') =
List.partition (fn (_, (_, thms, _, _)) =>
exists (#oracle o Thm.peek_status) thms) proved;
@@ -1117,7 +1117,7 @@
[(term_of_rule thy' prfx types pfuns ids rl, [])]))
other_rules),
Element.Notes ("", [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])]
-
+
in
set_env ctxt defs' types funs ids vcs' path prfx thy'
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Dec 15 15:05:35 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Dec 16 19:50:46 2016 +0100
@@ -84,8 +84,10 @@
be missing over there; or maybe the two code portions are not doing the same? *)
fun fold_body_thm max_thms outer_name (map_plain_name, map_inclass_name) body =
let
- fun app_thm map_name (_, (name, _, body)) (accum as (num_thms, names)) =
+ fun app_thm map_name (_, thm_node) (accum as (num_thms, names)) =
let
+ val name = Proofterm.thm_node_name thm_node
+ val body = Proofterm.thm_node_body thm_node
val (anonymous, enter_class) =
(* The "name = outer_name" case caters for the uncommon case where the proved theorem
occurs in its own proof (e.g., "Transitive_Closure.trancl_into_trancl"). *)
--- a/src/Pure/Concurrent/multithreading.ML Thu Dec 15 15:05:35 2016 +0100
+++ b/src/Pure/Concurrent/multithreading.ML Fri Dec 16 19:50:46 2016 +0100
@@ -61,7 +61,7 @@
val trace = ref 0;
fun tracing level msg =
- if level > ! trace then ()
+ if ! trace < level then ()
else Thread_Attributes.uninterruptible (fn _ => fn () =>
(TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
handle _ (*sic*) => ()) ();
@@ -79,20 +79,27 @@
fun synchronized name lock e =
Exn.release (Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
- let
- val immediate =
- if Mutex.trylock lock then true
- else
- let
- val _ = tracing 5 (fn () => name ^ ": locking ...");
- val timer = Timer.startRealTimer ();
- val _ = Mutex.lock lock;
- val time = Timer.checkRealTimer timer;
- val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
- in false end;
- val result = Exn.capture (restore_attributes e) ();
- val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
- val _ = Mutex.unlock lock;
- in result end) ());
+ if ! trace > 0 then
+ let
+ val immediate =
+ if Mutex.trylock lock then true
+ else
+ let
+ val _ = tracing 5 (fn () => name ^ ": locking ...");
+ val timer = Timer.startRealTimer ();
+ val _ = Mutex.lock lock;
+ val time = Timer.checkRealTimer timer;
+ val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
+ in false end;
+ val result = Exn.capture (restore_attributes e) ();
+ val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
+ val _ = Mutex.unlock lock;
+ in result end
+ else
+ let
+ val _ = Mutex.lock lock;
+ val result = Exn.capture (restore_attributes e) ();
+ val _ = Mutex.unlock lock;
+ in result end) ());
end;
--- a/src/Pure/Concurrent/thread_attributes.ML Thu Dec 15 15:05:35 2016 +0100
+++ b/src/Pure/Concurrent/thread_attributes.ML Fri Dec 16 19:50:46 2016 +0100
@@ -88,14 +88,20 @@
val w'' = Word.andb (w, Word.notb interrupt_state);
in Attributes (if w' = interrupt_asynch then Word.orb (w'', interrupt_asynch_once) else w) end;
-end;
-
fun with_attributes new_atts e =
let
- val orig_atts = safe_interrupts (get_attributes ());
- val result = Exn.capture (fn () => (set_attributes (safe_interrupts new_atts); e orig_atts)) ();
- val _ = set_attributes orig_atts;
- in Exn.release result end;
+ val atts1 = safe_interrupts (get_attributes ());
+ val atts2 = safe_interrupts new_atts;
+ in
+ if atts1 = atts2 then e atts1
+ else
+ let
+ val result = Exn.capture (fn () => (set_attributes atts2; e atts1)) ();
+ val _ = set_attributes atts1;
+ in Exn.release result end
+ end;
+
+end;
fun uninterruptible f x =
with_attributes no_interrupts (fn atts =>
--- a/src/Pure/General/source.ML Thu Dec 15 15:05:35 2016 +0100
+++ b/src/Pure/General/source.ML Fri Dec 16 19:50:46 2016 +0100
@@ -14,9 +14,8 @@
val map_filter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source
val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source
val of_list: 'a list -> ('a, 'a list) source
+ val of_string: string -> (string, string list) source
val exhausted: ('a, 'b) source -> ('a, 'a list) source
- val of_string: string -> (string, string list) source
- val of_string_limited: int -> string -> (string, substring) source
val source': 'a -> 'b Scan.stopper -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
val source: 'a Scan.stopper -> ('a list -> 'b list * 'a list) ->
@@ -84,20 +83,9 @@
fun of_list xs = make_source [] xs (fn xs => (xs, []));
-fun exhausted src = of_list (exhaust src);
-
-
-(* string source *)
-
val of_string = of_list o raw_explode;
-fun of_string_limited limit str =
- make_source [] (Substring.full str)
- (fn s =>
- let
- val (s1, s2) = Substring.splitAt (s, Int.min (Substring.size s, limit));
- val cs = map String.str (Substring.explode s1);
- in (cs, s2) end);
+fun exhausted src = of_list (exhaust src);
--- a/src/Pure/Isar/proof.ML Thu Dec 15 15:05:35 2016 +0100
+++ b/src/Pure/Isar/proof.ML Fri Dec 16 19:50:46 2016 +0100
@@ -522,8 +522,7 @@
fun err_lost () = error ("Lost goal structure:\n" ^ Thm.string_of_thm ctxt goal);
val th =
- (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal)
- handle THM _ => err_lost ())
+ (Goal.conclude (Thm.close_derivation goal) handle THM _ => err_lost ())
|> Drule.flexflex_unique (SOME ctxt)
|> Thm.check_shyps ctxt
|> Thm.check_hyps (Context.Proof ctxt);
--- a/src/Pure/Thy/thy_info.ML Thu Dec 15 15:05:35 2016 +0100
+++ b/src/Pure/Thy/thy_info.ML Fri Dec 16 19:50:46 2016 +0100
@@ -159,7 +159,7 @@
(*toplevel proofs and diags*)
val _ = Future.join_tasks (maps Future.group_snapshot (Execution.peek exec_id));
(*fully nested proofs*)
- val res = Exn.capture Thm.join_theory_proofs theory;
+ val res = Exn.capture Thm.consolidate_theory theory;
in res :: map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id)) end;
datatype task =
--- a/src/Pure/Tools/thm_deps.ML Thu Dec 15 15:05:35 2016 +0100
+++ b/src/Pure/Tools/thm_deps.ML Fri Dec 16 19:50:46 2016 +0100
@@ -20,8 +20,8 @@
fun make_node name directory =
Graph_Display.session_node
{name = Long_Name.base_name name, directory = directory, unfold = false, path = ""};
- fun add_dep ("", _, _) = I
- | add_dep (name, _, PBody {thms = thms', ...}) =
+ fun add_dep {name = "", ...} = I
+ | add_dep {name = name, body = PBody {thms = thms', ...}, ...} =
let
val prefix = #1 (split_last (Long_Name.explode name));
val session =
@@ -35,7 +35,7 @@
| NONE => [])
| _ => ["global"]);
val node = make_node name (space_implode "/" (session @ prefix));
- val deps = filter_out (fn s => s = "") (map (#1 o #2) thms');
+ val deps = filter_out (fn s => s = "") (map (Proofterm.thm_node_name o #2) thms');
in Symtab.update (name, (node, deps)) end;
val entries0 = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) Symtab.empty;
val entries1 =
@@ -73,7 +73,7 @@
val used =
Proofterm.fold_body_thms
- (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
+ (fn {name = a, ...} => a <> "" ? Symtab.update (a, ()))
(map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
Symtab.empty;
--- a/src/Pure/goal.ML Thu Dec 15 15:05:35 2016 +0100
+++ b/src/Pure/goal.ML Fri Dec 16 19:50:46 2016 +0100
@@ -232,7 +232,7 @@
(Thm.term_of stmt);
in
res
- |> length props > 1 ? Thm.close_derivation
+ |> Thm.close_derivation
|> Conjunction.elim_balanced (length props)
|> map (Assumption.export false ctxt' ctxt)
|> Variable.export ctxt' ctxt
--- a/src/Pure/more_thm.ML Thu Dec 15 15:05:35 2016 +0100
+++ b/src/Pure/more_thm.ML Fri Dec 16 19:50:46 2016 +0100
@@ -111,7 +111,7 @@
val untag: string -> attribute
val kind: string -> attribute
val register_proofs: thm list -> theory -> theory
- val join_theory_proofs: theory -> unit
+ val consolidate_theory: theory -> unit
val show_consts_raw: Config.raw
val show_consts: bool Config.T
val show_hyps_raw: Config.raw
@@ -452,8 +452,7 @@
(* close_derivation *)
fun close_derivation thm =
- if Thm.derivation_name thm = "" then Thm.name_derivation "" thm
- else thm;
+ if Thm.derivation_closed thm then thm else Thm.name_derivation "" thm;
(* user renaming of parameters in a subgoal *)
@@ -645,8 +644,8 @@
fun register_proofs more_thms =
Proofs.map (fold (cons o Thm.trim_context) more_thms);
-fun join_theory_proofs thy =
- Thm.join_proofs (map (Thm.transfer thy) (rev (Proofs.get thy)));
+fun consolidate_theory thy =
+ List.app (Thm.consolidate o Thm.transfer thy) (rev (Proofs.get thy));
--- a/src/Pure/proofterm.ML Thu Dec 15 15:05:35 2016 +0100
+++ b/src/Pure/proofterm.ML Fri Dec 16 19:50:46 2016 +0100
@@ -10,6 +10,7 @@
sig
val proofs: int Unsynchronized.ref
+ type thm_node
datatype proof =
MinProof
| PBound of int
@@ -25,7 +26,7 @@
| PThm of serial * ((string * term * typ list option) * proof_body future)
and proof_body = PBody of
{oracles: (string * term) Ord_List.T,
- thms: (serial * (string * term * proof_body future)) Ord_List.T,
+ thms: (serial * thm_node) Ord_List.T,
proof: proof}
val %> : proof * term -> proof
@@ -35,13 +36,17 @@
sig
include BASIC_PROOFTERM
+ type pthm = serial * thm_node
type oracle = string * term
- type pthm = serial * (string * term * proof_body future)
val proof_of: proof_body -> proof
+ val thm_node_name: thm_node -> string
+ val thm_node_prop: thm_node -> term
+ val thm_node_body: thm_node -> proof_body future
val join_proof: proof_body future -> proof
val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
- val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
- val join_bodies: proof_body list -> unit
+ val fold_body_thms: ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
+ proof_body list -> 'a -> 'a
+ val consolidate: proof_body -> unit
val peek_status: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
val oracle_ord: oracle * oracle -> order
@@ -60,6 +65,8 @@
(** primitive operations **)
val proofs_enabled: unit -> bool
+ val atomic_proof: proof -> bool
+ val compact_proof: proof -> bool
val proof_combt: proof * term list -> proof
val proof_combt': proof * term option list -> proof
val proof_combP: proof * proof list -> proof
@@ -173,16 +180,35 @@
| PThm of serial * ((string * term * typ list option) * proof_body future)
and proof_body = PBody of
{oracles: (string * term) Ord_List.T,
- thms: (serial * (string * term * proof_body future)) Ord_List.T,
- proof: proof};
+ thms: (serial * thm_node) Ord_List.T,
+ proof: proof}
+and thm_node =
+ Thm_Node of {name: string, prop: term, body: proof_body future, consolidate: unit lazy};
type oracle = string * term;
-type pthm = serial * (string * term * proof_body future);
+type pthm = serial * thm_node;
fun proof_of (PBody {proof, ...}) = proof;
val join_proof = Future.join #> proof_of;
-fun join_thms (thms: pthm list) = ignore (Future.joins (map (#3 o #2) thms));
+fun rep_thm_node (Thm_Node args) = args;
+val thm_node_name = #name o rep_thm_node;
+val thm_node_prop = #prop o rep_thm_node;
+val thm_node_body = #body o rep_thm_node;
+val thm_node_consolidate = #consolidate o rep_thm_node;
+
+fun join_thms (thms: pthm list) =
+ Future.joins (map (thm_node_body o #2) thms);
+
+fun consolidate (PBody {thms, ...}) =
+ List.app (Lazy.force o thm_node_consolidate o #2) thms;
+
+fun make_thm_node name prop body =
+ Thm_Node {name = name, prop = prop, body = body,
+ consolidate =
+ Lazy.lazy (fn () =>
+ let val PBody {thms, ...} = Future.join body
+ in List.app consolidate (join_thms thms) end)};
(***** proof atoms *****)
@@ -205,27 +231,27 @@
fun fold_body_thms f =
let
fun app (PBody {thms, ...}) =
- tap join_thms thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
+ tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) =>
if Inttab.defined seen i then (x, seen)
else
let
- val body' = Future.join body;
- val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
- in (f (name, prop, body') x', seen') end);
+ val name = thm_node_name thm_node;
+ val prop = thm_node_prop thm_node;
+ val body = Future.join (thm_node_body thm_node);
+ val (x', seen') = app body (x, Inttab.update (i, ()) seen);
+ in (f {serial = i, name = name, prop = prop, body = body} x', seen') end);
in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
-fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
-
fun peek_status bodies =
let
fun status (PBody {oracles, thms, ...}) x =
let
val ((oracle, unfinished, failed), seen) =
- (thms, x) |-> fold (fn (i, (_, _, body)) => fn (st, seen) =>
+ (thms, x) |-> fold (fn (i, thm_node) => fn (st, seen) =>
if Inttab.defined seen i then (st, seen)
else
let val seen' = Inttab.update (i, ()) seen in
- (case Future.peek body of
+ (case Future.peek (thm_node_body thm_node) of
SOME (Exn.Res body') => status body' (st, seen')
| SOME (Exn.Exn _) =>
let val (oracle, unfinished, _) = st
@@ -243,7 +269,7 @@
(* proof body *)
val oracle_ord = prod_ord fast_string_ord Term_Ord.fast_term_ord;
-fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
+fun thm_ord ((i, _): pthm, (j, _): pthm) = int_ord (j, i);
val unions_oracles = Ord_List.unions oracle_ord;
val unions_thms = Ord_List.unions thm_ord;
@@ -251,12 +277,12 @@
val all_oracles_of =
let
fun collect (PBody {oracles, thms, ...}) =
- tap join_thms thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
+ tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) =>
if Inttab.defined seen i then (x, seen)
else
let
- val body' = Future.join body;
- val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
+ val body = Future.join (thm_node_body thm_node);
+ val (x', seen') = collect body (x, Inttab.update (i, ()) seen);
in (if null oracles then x' else oracles :: x', seen') end);
in fn body => unions_oracles (#1 (collect body ([], Inttab.empty))) end;
@@ -264,7 +290,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, (name, prop, body)))
+ | PThm (i, ((name, prop, _), body)) => apsnd (cons (i, make_thm_node name prop body))
| _ => I) [prf] ([], []);
in
PBody
@@ -308,8 +334,9 @@
([int_atom a, b], triple term (option (list typ)) proof_body (c, d, 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, (b, c, body)) =
- pair int (triple string term proof_body) (a, (b, c, Future.join body));
+and pthm (a, thm_node) =
+ pair int (triple string term proof_body)
+ (a, (thm_node_name thm_node, thm_node_prop thm_node, Future.join (thm_node_body thm_node)));
in
@@ -345,7 +372,7 @@
in PBody {oracles = a, thms = b, proof = c} end
and pthm x =
let val (a, (b, c, d)) = pair int (triple string term proof_body) x
- in (a, (b, c, Future.value d)) end;
+ in (a, make_thm_node b c (Future.value d)) end;
in
@@ -357,6 +384,19 @@
(***** proof objects with different levels of detail *****)
+fun atomic_proof prf =
+ (case prf of
+ Abst _ => false
+ | AbsP _ => false
+ | op % _ => false
+ | op %% _ => false
+ | Promise _ => false
+ | _ => true);
+
+fun compact_proof (prf % _) = compact_proof prf
+ | compact_proof (prf1 %% prf2) = atomic_proof prf2 andalso compact_proof prf1
+ | compact_proof prf = atomic_proof prf;
+
fun (prf %> t) = prf % SOME t;
val proof_combt = Library.foldl (op %>);
@@ -533,11 +573,13 @@
prf_add_loose_bnos plev tlev prf2
(prf_add_loose_bnos plev tlev prf1 p)
| prf_add_loose_bnos plev tlev (prf % opt) (is, js) =
- prf_add_loose_bnos plev tlev prf (case opt of
+ prf_add_loose_bnos plev tlev prf
+ (case opt of
NONE => (is, insert (op =) ~1 js)
| SOME t => (is, add_loose_bnos (t, tlev, js)))
| prf_add_loose_bnos plev tlev (AbsP (_, opt, prf)) (is, js) =
- prf_add_loose_bnos (plev+1) tlev prf (case opt of
+ prf_add_loose_bnos (plev+1) tlev prf
+ (case opt of
NONE => (is, insert (op =) ~1 js)
| SOME t => (is, add_loose_bnos (t, tlev, js)))
| prf_add_loose_bnos plev tlev (Abst (_, _, prf)) p =
@@ -635,7 +677,7 @@
handle Same.SAME => prf % Same.map_option (subst' lev) t)
| subst _ _ = raise Same.SAME
and substh lev prf = (subst lev prf handle Same.SAME => prf);
- in case args of [] => prf | _ => substh 0 prf end;
+ in (case args of [] => prf | _ => substh 0 prf) end;
fun prf_subst_pbounds args prf =
let
@@ -651,7 +693,7 @@
| subst (prf % t) Plev tlev = subst prf Plev tlev % t
| subst _ _ _ = raise Same.SAME
and substh prf Plev tlev = (subst prf Plev tlev handle Same.SAME => prf)
- in case args of [] => prf | _ => substh prf 0 0 end;
+ in (case args of [] => prf | _ => substh prf 0 0) end;
(**** Freezing and thawing of variables in proof terms ****)
@@ -992,7 +1034,7 @@
| Var _ => SOME (remove_types t)
| _ => NONE) %
(case head_of g of
- Abs _ => SOME (remove_types u)
+ Abs _ => SOME (remove_types u)
| Var _ => SOME (remove_types u)
| _ => NONE) %% prf1 %% prf2
| _ => prf % NONE % NONE %% prf1 %% prf2)
@@ -1105,7 +1147,8 @@
add_npvars q p Ts (vs, if p andalso q then betapply (t, Var (("",0), T)) else t)
| add_npvars q p Ts (vs, Abs (_, T, t)) = add_npvars q p (T::Ts) (vs, t)
| add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t)
-and add_npvars' Ts (vs, t) = (case strip_comb t of
+and add_npvars' Ts (vs, t) =
+ (case strip_comb t of
(Var (ixn, _), ts) => if test_args [] ts then vs
else Library.foldl (add_npvars' Ts)
(AList.update (op =) (ixn,
@@ -1115,19 +1158,20 @@
fun prop_vars (Const ("Pure.imp", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q)
| prop_vars (Const ("Pure.all", _) $ Abs (_, _, t)) = prop_vars t
- | prop_vars t = (case strip_comb t of
- (Var (ixn, _), _) => [ixn] | _ => []);
+ | prop_vars t = (case strip_comb t of (Var (ixn, _), _) => [ixn] | _ => []);
fun is_proj t =
let
- fun is_p i t = (case strip_comb t of
+ fun is_p i t =
+ (case strip_comb t of
(Bound _, []) => false
| (Bound j, ts) => j >= i orelse exists (is_p i) ts
| (Abs (_, _, u), _) => is_p (i+1) u
| (_, ts) => exists (is_p i) ts)
- in (case strip_abs_body t of
- Bound _ => true
- | t' => is_p 0 t')
+ in
+ (case strip_abs_body t of
+ Bound _ => true
+ | t' => is_p 0 t')
end;
fun needed_vars prop =
@@ -1196,7 +1240,8 @@
val (ts', ts'') = chop (length vs) ts;
val insts = take (length ts') (map (fst o dest_Var) vs) ~~ ts';
val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
- insert (op =) ixn (case AList.lookup (op =) insts ixn of
+ insert (op =) ixn
+ (case AList.lookup (op =) insts ixn of
SOME (SOME t) => if is_proj t then union (op =) ixns ixns' else ixns'
| _ => union (op =) ixns ixns'))
(needed prop ts'' prfs, add_npvars false true [] ([], prop));
@@ -1250,12 +1295,12 @@
fun mtch Ts i j (pinst, tinst) (Hyp (Var (ixn, _)), prf) =
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
+ else
+ (case apfst (flt i) (apsnd (flt j) (prf_add_loose_bnos 0 0 prf ([], []))) of
([], []) => ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst)
- | ([], _) => if j = 0 then
- ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst)
- else raise PMatch
+ | ([], _) =>
+ if j = 0 then ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst)
+ else raise PMatch
| _ => raise PMatch)
| mtch Ts i j inst (prf1 % opt1, prf2 % opt2) =
optmatch (matcht Ts j) (mtch Ts i j inst (prf1, prf2)) (opt1, opt2)
@@ -1389,45 +1434,57 @@
| rew0 Ts hs prf = rew Ts hs prf;
fun rew1 _ _ (Hyp (Var _)) _ = NONE
- | rew1 Ts hs skel prf = (case rew2 Ts hs skel prf of
- SOME prf1 => (case rew0 Ts hs prf1 of
- SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts hs skel' prf2))
- | NONE => SOME prf1)
- | NONE => (case rew0 Ts hs prf of
- SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts hs skel' prf1))
- | NONE => NONE))
+ | rew1 Ts hs skel prf =
+ (case rew2 Ts hs skel prf of
+ SOME prf1 =>
+ (case rew0 Ts hs prf1 of
+ SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts hs skel' prf2))
+ | NONE => SOME prf1)
+ | NONE =>
+ (case rew0 Ts hs prf of
+ SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts hs skel' prf1))
+ | NONE => NONE))
- and rew2 Ts hs skel (prf % SOME t) = (case prf of
+ and rew2 Ts hs skel (prf % SOME t) =
+ (case prf of
Abst (_, _, body) =>
let val prf' = prf_subst_bounds [t] body
in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end
- | _ => (case rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf of
- SOME prf' => SOME (prf' % SOME t)
- | NONE => NONE))
+ | _ =>
+ (case rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf of
+ SOME prf' => SOME (prf' % SOME t)
+ | NONE => NONE))
| rew2 Ts hs skel (prf % NONE) = Option.map (fn prf' => prf' % NONE)
(rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf)
- | rew2 Ts hs skel (prf1 %% prf2) = (case prf1 of
+ | rew2 Ts hs skel (prf1 %% prf2) =
+ (case prf1 of
AbsP (_, _, body) =>
let val prf' = prf_subst_pbounds [prf2] body
in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end
| _ =>
- let val (skel1, skel2) = (case skel of
- skel1 %% skel2 => (skel1, skel2)
- | _ => (no_skel, no_skel))
- in case rew1 Ts hs skel1 prf1 of
- SOME prf1' => (case rew1 Ts hs skel2 prf2 of
+ let
+ val (skel1, skel2) =
+ (case skel of
+ skel1 %% skel2 => (skel1, skel2)
+ | _ => (no_skel, no_skel))
+ in
+ (case rew1 Ts hs skel1 prf1 of
+ SOME prf1' =>
+ (case rew1 Ts hs skel2 prf2 of
SOME prf2' => SOME (prf1' %% prf2')
| NONE => SOME (prf1' %% prf2))
- | NONE => (case rew1 Ts hs skel2 prf2 of
+ | NONE =>
+ (case rew1 Ts hs skel2 prf2 of
SOME prf2' => SOME (prf1 %% prf2')
- | NONE => NONE)
+ | NONE => NONE))
end)
- | rew2 Ts hs skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts) hs
+ | rew2 Ts hs skel (Abst (s, T, prf)) =
+ (case rew1 (the_default dummyT T :: Ts) hs
(case skel of Abst (_, _, skel') => skel' | _ => no_skel) prf of
SOME prf' => SOME (Abst (s, T, prf'))
| NONE => NONE)
- | rew2 Ts hs skel (AbsP (s, t, prf)) = (case rew1 Ts (t :: hs)
- (case skel of AbsP (_, _, skel') => skel' | _ => no_skel) prf of
+ | rew2 Ts hs skel (AbsP (s, t, prf)) =
+ (case rew1 Ts (t :: hs) (case skel of AbsP (_, _, skel') => skel' | _ => no_skel) prf of
SOME prf' => SOME (AbsP (s, t, prf'))
| NONE => NONE)
| rew2 _ _ _ _ = NONE;
@@ -1476,6 +1533,8 @@
fun fulfill_norm_proof thy ps body0 =
let
+ val _ = List.app (consolidate o #2) ps;
+ val _ = consolidate body0;
val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
val oracles =
unions_oracles
@@ -1573,15 +1632,14 @@
else new_prf ()
| _ => new_prf ());
val head = PThm (i, ((name, prop1, NONE), body'));
- in ((i, (name, prop1, body')), head, args, argsP, args1) end;
+ in ((i, make_thm_node name prop1 body'), head, args, argsP, args1) end;
fun thm_proof thy name shyps hyps concl promises body =
let val (pthm, head, args, argsP, _) = prepare_thm_proof thy name shyps hyps concl promises body
in (pthm, proof_combP (proof_combt' (head, args), argsP)) end;
fun unconstrain_thm_proof thy shyps concl promises body =
- let
- val (pthm, head, _, _, args) = prepare_thm_proof thy "" shyps [] concl promises body
+ let val (pthm, head, _, _, args) = prepare_thm_proof thy "" shyps [] concl promises body
in (pthm, proof_combt' (head, args)) end;
--- a/src/Pure/thm.ML Thu Dec 15 15:05:35 2016 +0100
+++ b/src/Pure/thm.ML Fri Dec 16 19:50:46 2016 +0100
@@ -86,9 +86,10 @@
val proof_bodies_of: thm list -> proof_body list
val proof_body_of: thm -> proof_body
val proof_of: thm -> proof
- val join_proofs: thm list -> unit
+ val consolidate: thm -> unit
val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool}
val future: thm future -> cterm -> thm
+ val derivation_closed: thm -> bool
val derivation_name: thm -> string
val name_derivation: string -> thm -> thm
val axiom: theory -> string -> thm
@@ -584,21 +585,14 @@
and join_promises_of thms = join_promises (Ord_List.make promise_ord (maps raw_promises_of thms));
fun fulfill_body (th as Thm (Deriv {promises, body}, _)) =
- Proofterm.fulfill_norm_proof (theory_of_thm th) (fulfill_promises promises) body
-and fulfill_promises promises =
- map fst promises ~~ map fulfill_body (Future.joins (map snd promises));
+ let val fulfilled_promises = map #1 promises ~~ map fulfill_body (Future.joins (map #2 promises))
+ in Proofterm.fulfill_norm_proof (theory_of_thm th) fulfilled_promises body end;
-fun proof_bodies_of thms =
- let
- val _ = join_promises_of thms;
- val bodies = map fulfill_body thms;
- val _ = Proofterm.join_bodies bodies;
- in bodies end;
-
+fun proof_bodies_of thms = (join_promises_of thms; map fulfill_body thms);
val proof_body_of = singleton proof_bodies_of;
val proof_of = Proofterm.proof_of o proof_body_of;
-val join_proofs = ignore o proof_bodies_of;
+val consolidate = ignore o proof_bodies_of o single;
(* derivation status *)
@@ -655,6 +649,10 @@
(* closed derivations with official name *)
(*non-deterministic, depends on unknown promises*)
+fun derivation_closed (Thm (Deriv {body, ...}, _)) =
+ Proofterm.compact_proof (Proofterm.proof_of body);
+
+(*non-deterministic, depends on unknown promises*)
fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
Proofterm.get_name shyps hyps prop (Proofterm.proof_of body);
@@ -1305,9 +1303,9 @@
val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees);
val ps = map (apsnd (Future.map fulfill_body)) promises;
- val (pthm as (_, (_, prop', _)), proof) =
- Proofterm.unconstrain_thm_proof thy shyps prop ps body;
+ val (pthm, proof) = Proofterm.unconstrain_thm_proof thy shyps prop ps body;
val der' = make_deriv [] [] [pthm] proof;
+ val prop' = Proofterm.thm_node_prop (#2 pthm);
in
Thm (der',
{cert = cert,