# HG changeset patch
# User wenzelm
# Date 1565703286 -7200
# Node ID 9ddd66d53130ba12fbca711d05a69595dcd25c0a
# Parent  11d8517d9384d9fc8c9e7b5b7675d86ad8d9f754
added SUBPROOFS / "subproofs" method combinator, for more compact proofterms;

diff -r 11d8517d9384 -r 9ddd66d53130 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Aug 13 10:27:21 2019 +0200
+++ b/src/Pure/Isar/method.ML	Tue Aug 13 15:34:46 2019 +0200
@@ -770,6 +770,8 @@
       |> (fn SOME msg => Seq.single (Seq.Error msg)
            | NONE => goal_cases_tac (map Token.content_of names) (ctxt, st)))))
     "bind cases for goals" #>
+  setup \<^binding>\<open>subproofs\<close> (text_closure >> (Context_Tactic.SUBPROOFS ooo evaluate_runtime))
+    "apply proof method to subproofs with closed derivation" #>
   setup \<^binding>\<open>insert\<close> (Attrib.thms >> (K o insert))
     "insert theorems, ignoring facts" #>
   setup \<^binding>\<open>intro\<close> (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths))
diff -r 11d8517d9384 -r 9ddd66d53130 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Aug 13 10:27:21 2019 +0200
+++ b/src/Pure/ROOT.ML	Tue Aug 13 15:34:46 2019 +0200
@@ -243,8 +243,8 @@
 section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup";
 
 (*basic proof engine*)
+ML_file "par_tactical.ML";
 ML_file "context_tactic.ML";
-ML_file "par_tactical.ML";
 ML_file "Isar/proof_display.ML";
 ML_file "Isar/attrib.ML";
 ML_file "Isar/context_rules.ML";
diff -r 11d8517d9384 -r 9ddd66d53130 src/Pure/context_tactic.ML
--- a/src/Pure/context_tactic.ML	Tue Aug 13 10:27:21 2019 +0200
+++ b/src/Pure/context_tactic.ML	Tue Aug 13 15:34:46 2019 +0200
@@ -16,6 +16,7 @@
   val CONTEXT_CASES: Rule_Cases.cases -> tactic -> context_tactic
   val CONTEXT_SUBGOAL: (term * int -> context_tactic) -> int -> context_tactic
   val CONTEXT_THEN_ALL_NEW: (int -> context_tactic) * (int -> tactic) -> int -> context_tactic
+  val SUBPROOFS: context_tactic -> context_tactic
 end;
 
 signature CONTEXT_TACTIC =
@@ -26,6 +27,8 @@
 structure Context_Tactic: CONTEXT_TACTIC =
 struct
 
+(* type context_tactic *)
+
 type context_state = Proof.context * thm;
 type context_tactic = context_state -> context_state Seq.result Seq.seq;
 
@@ -52,6 +55,30 @@
     (ctxt, st) |> tac1 i |> Seq.maps_results (fn (ctxt', st') =>
       TACTIC_CONTEXT ctxt' ((Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)) st'));
 
+
+(* subproofs with closed derivation *)
+
+fun SUBPROOFS tac : context_tactic =
+  let
+    fun apply (g :: gs) (SOME (Seq.Result (results, ctxt))) =
+          (case Seq.pull (tac (ctxt, Goal.init g)) of
+            SOME (Seq.Result (ctxt', st'), _) =>
+              apply gs (SOME (Seq.Result (st' :: results, ctxt')))
+          | SOME (Seq.Error msg, _) => SOME (Seq.Error msg)
+          | NONE => NONE)
+      | apply _ x = x;
+  in
+    fn (ctxt, st) =>
+      (case Par_Tactical.strip_goals st of
+        SOME goals =>
+          (case apply goals (SOME (Seq.Result ([], ctxt))) of
+            SOME (Seq.Result (results, ctxt')) =>
+              TACTIC_CONTEXT ctxt' (Par_Tactical.retrofit_tac {close = true} results st)
+          | SOME (Seq.Error msg) => Seq.single (Seq.Error msg)
+          | NONE => Seq.empty)
+      | NONE => Seq.DETERM tac (ctxt, st))
+  end;
+
 end;
 
 structure Basic_Context_Tactic: BASIC_CONTEXT_TACTIC = Context_Tactic;
diff -r 11d8517d9384 -r 9ddd66d53130 src/Pure/par_tactical.ML
--- a/src/Pure/par_tactical.ML	Tue Aug 13 10:27:21 2019 +0200
+++ b/src/Pure/par_tactical.ML	Tue Aug 13 15:34:46 2019 +0200
@@ -14,6 +14,8 @@
 signature PAR_TACTICAL =
 sig
   include BASIC_PAR_TACTICAL
+  val strip_goals: thm -> cterm list option
+  val retrofit_tac: {close: bool} -> thm list -> tactic
 end;
 
 structure Par_Tactical: PAR_TACTICAL =
@@ -29,35 +31,43 @@
 
 (* parallel refinement of non-schematic goal by single results *)
 
-local
-
-exception FAILED of unit;
-
-fun retrofit st' =
-  rotate_prems ~1 #>
-  Thm.bicompose NONE {flatten = false, match = false, incremented = false}
-      (false, Goal.conclude st', Thm.nprems_of st') 1;
-
-in
-
-fun PARALLEL_GOALS tac st =
+fun strip_goals st =
   let
     val goals =
       Drule.strip_imp_prems (Thm.cprop_of st)
       |> map (Thm.adjust_maxidx_cterm ~1);
   in
-    if Future.relevant goals andalso forall (fn g => Thm.maxidx_of_cterm g = ~1) goals then
-      let
-        fun try_goal g =
-          (case SINGLE tac (Goal.init g) of
-            NONE => raise FAILED ()
-          | SOME st' => st');
-        val results = Par_List.map try_goal goals;
-      in EVERY (map retrofit (rev results)) st
-      end handle FAILED () => Seq.empty
-    else DETERM tac st
+    if not (null goals) andalso forall (fn g => Thm.maxidx_of_cterm g = ~1) goals
+    then SOME goals else NONE
   end;
 
+local
+
+exception FAILED of unit;
+
+fun retrofit {close} st' =
+  rotate_prems ~1 #>
+  Thm.bicompose NONE {flatten = false, match = false, incremented = false}
+      (false, Goal.conclude st' |> close ? Thm.close_derivation \<^here>, Thm.nprems_of st') 1;
+
+in
+
+fun retrofit_tac close = EVERY o map (retrofit close);
+
+fun PARALLEL_GOALS tac st =
+  (case strip_goals st of
+    SOME goals =>
+      if Future.relevant goals then
+        let
+          fun try_goal g =
+            (case SINGLE tac (Goal.init g) of
+              NONE => raise FAILED ()
+            | SOME st' => st');
+          val results = Par_List.map try_goal goals;
+        in retrofit_tac {close = false} (rev results) st end handle FAILED () => Seq.empty
+      else DETERM tac st
+  | NONE => DETERM tac st);
+
 end;
 
 val PARALLEL_ALLGOALS = PARALLEL_GOALS o ALLGOALS;