# HG changeset patch
# User wenzelm
# Date 1563876470 -7200
# Node ID 725438ceae7c5af32cc2332875704a2568ee5773
# Parent  f5bce5af361b4d9a00d9ce2ca06ff2cbd34b43ef
proof terms are always constructed sequentially;
discontinued unused Proofterm.Promise -- too complex;

diff -r f5bce5af361b -r 725438ceae7c src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Jul 22 21:55:02 2019 +0200
+++ b/src/HOL/ROOT	Tue Jul 23 12:07:50 2019 +0200
@@ -16,7 +16,7 @@
   description "
     HOL-Main with explicit proof terms.
   "
-  options [quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0, parallel_limit = 500]
+  options [quick_and_dirty = false, record_proofs = 2, parallel_limit = 500]
   sessions
     "HOL-Library"
   theories
@@ -434,7 +434,7 @@
   description "
     Examples for program extraction in Higher-Order Logic.
   "
-  options [parallel_proofs = 0, quick_and_dirty = false]
+  options [quick_and_dirty = false]
   sessions
     "HOL-Computational_Algebra"
   theories
@@ -455,8 +455,7 @@
     The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
     theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
   \<close>
-  options [print_mode = "no_brackets",
-    parallel_proofs = 0, quick_and_dirty = false]
+  options [print_mode = "no_brackets", quick_and_dirty = false]
   sessions
     "HOL-Library"
   theories
diff -r f5bce5af361b -r 725438ceae7c src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Jul 22 21:55:02 2019 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jul 23 12:07:50 2019 +0200
@@ -1293,7 +1293,10 @@
 local
 
 fun future_terminal_proof proof1 proof2 done state =
-  if Future.proofs_enabled 3 andalso not (is_relevant state) then
+  if Future.proofs_enabled 3 andalso
+    not (Proofterm.proofs_enabled ()) andalso
+    not (is_relevant state)
+  then
     state |> future_proof (fn state' =>
       let val pos = Position.thread_data () in
         Execution.fork {name = "Proof.future_terminal_proof", pos = pos, pri = ~1}
diff -r f5bce5af361b -r 725438ceae7c src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Jul 22 21:55:02 2019 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 23 12:07:50 2019 +0200
@@ -713,6 +713,7 @@
   (case try proof_of st of
     NONE => false
   | SOME state =>
+      not (Proofterm.proofs_enabled ()) andalso
       not (Proof.is_relevant state) andalso
        (if can (Proof.assert_bottom true) state
         then Future.proofs_enabled 1
diff -r f5bce5af361b -r 725438ceae7c src/Pure/ML/ml_pp.ML
--- a/src/Pure/ML/ml_pp.ML	Mon Jul 22 21:55:02 2019 +0200
+++ b/src/Pure/ML/ml_pp.ML	Tue Jul 23 12:07:50 2019 +0200
@@ -80,7 +80,6 @@
     | PAxm a => prt_app "PAxm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
     | OfClass a => prt_app "OfClass" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
     | Oracle a => prt_app "Oracle" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
-    | Promise a => prt_app "Promise" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
     | PThm a => prt_app "PThm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1))))
 
 and prt_proofs parens dp prf =
diff -r f5bce5af361b -r 725438ceae7c src/Pure/goal.ML
--- a/src/Pure/goal.ML	Mon Jul 22 21:55:02 2019 +0200
+++ b/src/Pure/goal.ML	Tue Jul 23 12:07:50 2019 +0200
@@ -165,7 +165,7 @@
 
     val schematic = exists is_schematic props;
     val immediate = is_none fork_pri;
-    val future = Future.proofs_enabled 1;
+    val future = Future.proofs_enabled 1 andalso not (Proofterm.proofs_enabled ());
     val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled ();
 
     val pos = Position.thread_data ();
diff -r f5bce5af361b -r 725438ceae7c src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Jul 22 21:55:02 2019 +0200
+++ b/src/Pure/proofterm.ML	Tue Jul 23 12:07:50 2019 +0200
@@ -20,7 +20,6 @@
    | PAxm of string * term * typ list option
    | OfClass of typ * class
    | Oracle of string * term * typ list option
-   | Promise of serial * term * typ list
    | PThm of serial * ((string * term * typ list option) * proof_body future)
   and proof_body = PBody of
     {oracles: (string * term) Ord_List.T,
@@ -150,7 +149,6 @@
     (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof
   val rew_proof: theory -> proof -> proof
 
-  val promise_proof: theory -> serial -> term -> proof
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
   val thm_proof: theory -> string -> sort list -> term list -> term ->
     (serial * proof_body future) list -> proof_body -> pthm * proof
@@ -176,7 +174,6 @@
  | PAxm of string * term * typ list option
  | OfClass of typ * class
  | Oracle of string * term * typ list option
- | Promise of serial * term * typ list
  | PThm of serial * ((string * term * typ list option) * proof_body future)
 and proof_body = PBody of
   {oracles: (string * term) Ord_List.T,
@@ -334,7 +331,6 @@
   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 Promise (a, b, c) => ([int_atom a], pair term (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))]
 and proof_body (PBody {oracles, thms, proof = prf}) =
@@ -368,7 +364,6 @@
   fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in PAxm (a, c, d) end,
   fn ([b], a) => OfClass (typ a, b),
   fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in Oracle (a, c, d) end,
-  fn ([a], b) => let val (c, d) = pair term (list typ) b in Promise (int_atom 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]
@@ -395,7 +390,6 @@
   | AbsP _ => false
   | op % _ => false
   | op %% _ => false
-  | Promise _ => false
   | _ => true);
 
 fun compact_proof (prf % _) = compact_proof prf
@@ -445,7 +439,6 @@
       | 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 (Promise (i, prop, Ts)) = Promise (i, prop, typs Ts)
       | proof (PThm (i, ((a, prop, SOME Ts), body))) =
           PThm (i, ((a, prop, SOME (typs Ts)), body))
       | proof _ = raise Same.SAME;
@@ -472,7 +465,6 @@
   | 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 (Promise (_, _, Ts)) = fold g Ts
   | fold_proof_terms _ g (PThm (_, ((_, _, SOME Ts), _))) = fold g Ts
   | fold_proof_terms _ _ _ = I;
 
@@ -487,7 +479,6 @@
 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 _ (Promise _) = raise Fail "change_type: unexpected promise"
   | change_type opTs (PThm (i, ((name, prop, _), body))) =
       PThm (i, ((name, prop, opTs), body))
   | change_type _ prf = prf;
@@ -636,8 +627,6 @@
           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 (Promise (i, prop, Ts)) =
-          Promise (i, prop, 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 _ = raise Same.SAME;
@@ -805,8 +794,7 @@
       in Const ("Pure.Appt", proofT --> T --> proofT) $ term_of Ts prf $ t end
   | term_of _ (Hyp t) = Hypt $ t
   | term_of _ (Oracle (_, t, _)) = Oraclet $ t
-  | term_of _ MinProof = MinProoft
-  | term_of _ (Promise (_, t, _)) = raise TERM ("Illegal proof promise", [t]);
+  | term_of _ MinProof = MinProoft;
 
 in
 
@@ -956,8 +944,6 @@
           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' _ _ (Promise (i, prop, Ts)) =
-          Promise (i, prop, 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' _ _ _ = raise Same.SAME
@@ -1296,7 +1282,6 @@
               (case prf of
                 PAxm (_, prop, _) => prop
               | Oracle (_, prop, _) => prop
-              | Promise (_, prop, _) => prop
               | PThm (_, ((_, prop, _), _)) => prop
               | _ => raise Fail "shrink: proof not in normal form");
             val vs = vars_of prop;
@@ -1431,7 +1416,6 @@
       | 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 _ _ (Promise (i, prop, Ts)) = Promise (i, prop, substTs Ts)
       | subst _ _ (PThm (i, ((id, prop, Ts), body))) =
           PThm (i, ((id, prop, Same.map_option substTs Ts), body))
       | subst _ _ _ = raise Same.SAME;
@@ -1587,16 +1571,6 @@
 
 (** promises **)
 
-fun promise_proof thy i prop =
-  let
-    val _ = prop |> Term.exists_subterm (fn t =>
-      (Term.is_Free t orelse Term.is_Var t) andalso
-        raise Fail ("promise_proof: illegal variable " ^ Syntax.string_of_term_global thy t));
-    val _ = prop |> Term.exists_type (Term.exists_subtype
-      (fn TFree (a, _) => raise Fail ("promise_proof: illegal type variable " ^ quote a)
-        | _ => false));
-  in Promise (i, prop, map TVar (Term.add_tvars prop [])) end;
-
 fun fulfill_norm_proof thy ps body0 =
   let
     val _ = consolidate (map #2 ps @ [body0]);
@@ -1606,15 +1580,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 proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
-
-    fun fill (Promise (i, prop, Ts)) =
-          (case Inttab.lookup proofs i of
-            NONE => NONE
-          | SOME prf => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) prf, normal_skel))
-      | fill _ = NONE;
-    val (rules, procs) = get_data thy;
-    val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0;
+    val proof = rew_proof thy proof0;
   in PBody {oracles = oracles, thms = thms, proof = proof} end;
 
 fun fulfill_proof_future thy promises (postproc: proof_body -> proof_body) body =
diff -r f5bce5af361b -r 725438ceae7c src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Jul 22 21:55:02 2019 +0200
+++ b/src/Pure/thm.ML	Tue Jul 23 12:07:50 2019 +0200
@@ -636,7 +636,7 @@
 fun make_deriv promises oracles thms proof =
   Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}};
 
-val empty_deriv = make_deriv [] [] [] Proofterm.MinProof;
+val empty_deriv = make_deriv [] [] [] MinProof;
 
 
 (* inference rules *)
@@ -720,12 +720,14 @@
   let
     val Cterm {cert = cert, t = prop, T, maxidx, sorts} = ct;
     val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
+    val _ =
+      if Proofterm.proofs_enabled ()
+      then raise CTERM ("future: proof terms enabled", [ct]) else ();
 
-    val thy = theory_of_cterm ct;
     val i = serial ();
     val future = future_thm |> Future.map (future_result i cert sorts prop);
   in
-    Thm (make_deriv [(i, future)] [] [] (Proofterm.promise_proof thy i prop),
+    Thm (make_deriv [(i, future)] [] [] MinProof,
      {cert = cert,
       tags = [],
       maxidx = maxidx,