# HG changeset patch
# User wenzelm
# Date 1447942215 -3600
#      Thu Nov 19 15:10:15 2015 +0100
# Node ID c42a363746a571f498ffafbacc5dfe627dfc56cf
# Parent  aa96ef3c08ec968ed1cdaacf18757fb25db26fa1
more robust subgoal addressing of tactics;
prefer canonical PARALLEL_ALLGOALS;

diff -r aa96ef3c08ec -r c42a363746a5 thys/ConcurrentGC/Handshakes.thy
--- a/thys/ConcurrentGC/Handshakes.thy	Wed Nov 18 15:22:17 2015 +0000
+++ b/thys/ConcurrentGC/Handshakes.thy	Thu Nov 19 15:10:15 2015 +0100
@@ -256,14 +256,14 @@
 lemma (in mut_m') handshake_invL[intro]:
   "\<lbrace> handshake_invL \<rbrace> mutator m'"
 apply vcg_nihe
-apply vcg_ni
+apply vcg_ni+
 done
 
 lemma (in gc) mut_handshake_invL[intro]:
   notes mut_m.handshake_invL_def[inv]
   shows "\<lbrace> handshake_invL and mut_m.handshake_invL m \<rbrace> gc \<lbrace> mut_m.handshake_invL m \<rbrace>"
 apply vcg_nihe
-apply vcg_ni
+apply vcg_ni+
 done
 
 lemma (in sys) mut_handshake_invL[intro]:
@@ -275,7 +275,7 @@
   notes gc.handshake_invL_def[inv]
   shows "\<lbrace> handshake_invL and gc.handshake_invL \<rbrace> mutator m \<lbrace> gc.handshake_invL \<rbrace>"
 apply vcg_nihe
-apply vcg_ni
+apply vcg_ni+
 done
 
 lemma (in mut_m) handshake_phase_inv[intro]:
diff -r aa96ef3c08ec -r c42a363746a5 thys/ConcurrentGC/MarkObject.thy
--- a/thys/ConcurrentGC/MarkObject.thy	Wed Nov 18 15:22:17 2015 +0000
+++ b/thys/ConcurrentGC/MarkObject.thy	Thu Nov 19 15:10:15 2015 +0100
@@ -1019,6 +1019,7 @@
   apply (erule greyI)
  apply (clarsimp split: obj_at_splits)
 apply (clarsimp simp: obj_at_field_on_heap_def split: option.splits)
+apply vcg_ni+
 done
 
 lemma (in mut_m) gc_mark_mark_object_invL[intro]:
diff -r aa96ef3c08ec -r c42a363746a5 thys/ConcurrentGC/StrongTricolour.thy
--- a/thys/ConcurrentGC/StrongTricolour.thy	Wed Nov 18 15:22:17 2015 +0000
+++ b/thys/ConcurrentGC/StrongTricolour.thy	Thu Nov 19 15:10:15 2015 +0100
@@ -1932,9 +1932,9 @@
 apply(tactic {*
 let val ctxt = @{context} in
 
-  TRY o vcg_clarsimp_tac ctxt
-THEN'
-  PARALLEL_GOALS o (
+  TRY (HEADGOAL (vcg_clarsimp_tac ctxt))
+THEN
+  PARALLEL_ALLGOALS (
                vcg_sem_tac ctxt
          THEN' (SELECT_GOAL (Local_Defs.unfold_tac ctxt (Inv.get ctxt)))
          THEN' (TRY o REPEAT_ALL_NEW (Tactic.match_tac ctxt @{thms conjI})) (* expose the location predicates, do not split the consequents *)
@@ -1946,11 +1946,9 @@
   THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Tactic.ematch_tac ctxt @{thms thin_locs} THEN' REPEAT1 o assume_tac ctxt))
   THEN_ALL_NEW asm_full_simp_tac (ss_only (@{thms loc_simps} @ Loc.get ctxt) ctxt)
   THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Rule_Insts.thin_tac ctxt "True" []))
-  THEN_ALL_NEW clarsimp_tac ctxt
-
-)
-
-end 1
+  THEN_ALL_NEW clarsimp_tac ctxt)
+
+end
 *})
 
 (* hs_noop_done *)
diff -r aa96ef3c08ec -r c42a363746a5 thys/ConcurrentGC/Tactics.thy
--- a/thys/ConcurrentGC/Tactics.thy	Wed Nov 18 15:22:17 2015 +0000
+++ b/thys/ConcurrentGC/Tactics.thy	Thu Nov 19 15:10:15 2015 +0100
@@ -254,18 +254,19 @@
     (Method.sections clasimp_modifiers >> K (SIMPLE_METHOD' o vcg_sem_tac))
     "turn VCG goal into semantics and clarsimp")
 
-fun vcg_jackhammer_gen_tac terminal_method ctxt =
-  vcg_clarsimp_tac ctxt
-THEN'
-  PARALLEL_GOALS o (
-               vcg_sem_tac ctxt
-  THEN_ALL_NEW (full_simp_tac (Splitter.add_split @{thm lcond_split_asm} (ctxt addsimps Inv.get ctxt)))
-  THEN_ALL_NEW ( (TRY o REPEAT_ALL_NEW (Tactic.ematch_tac ctxt @{thms conjE}))
-           THEN' (TRY o REPEAT_ALL_NEW (Tactic.ematch_tac ctxt @{thms thin_locs} THEN' REPEAT1 o assume_tac ctxt))
-           THEN' asm_full_simp_tac (ss_only (@{thms loc_simps} @ Loc.get ctxt) ctxt)
-           THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Rule_Insts.thin_tac ctxt "True" [])) (* FIXME weird, must be a standard way to do this. Leaving them in can cause simp to diverge ?? *)
-           THEN_ALL_NEW clarsimp_tac (ctxt addsimps (Loc.get ctxt @ @{thms atS_simps})) (* FIXME smelly *)
-           THEN_ALL_NEW TRY o terminal_method ctxt))
+fun vcg_jackhammer_gen_tac terminal_tac ctxt =
+  SELECT_GOAL (
+    HEADGOAL (vcg_clarsimp_tac ctxt)
+  THEN
+    PARALLEL_ALLGOALS (
+                 vcg_sem_tac ctxt
+    THEN_ALL_NEW (full_simp_tac (Splitter.add_split @{thm lcond_split_asm} (ctxt addsimps Inv.get ctxt)))
+    THEN_ALL_NEW ( (TRY o REPEAT_ALL_NEW (Tactic.ematch_tac ctxt @{thms conjE}))
+             THEN' (TRY o REPEAT_ALL_NEW (Tactic.ematch_tac ctxt @{thms thin_locs} THEN' REPEAT1 o assume_tac ctxt))
+             THEN' asm_full_simp_tac (ss_only (@{thms loc_simps} @ Loc.get ctxt) ctxt)
+             THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Rule_Insts.thin_tac ctxt "True" [])) (* FIXME weird, must be a standard way to do this. Leaving them in can cause simp to diverge ?? *)
+             THEN_ALL_NEW clarsimp_tac (ctxt addsimps (Loc.get ctxt @ @{thms atS_simps})) (* FIXME smelly *)
+             THEN_ALL_NEW TRY o terminal_tac ctxt)))
 
 val _ =
   Theory.setup (Method.setup @{binding vcg_jackhammer}
@@ -278,28 +279,30 @@
     "VCG supertactic, fastforce the survivors")
 
 fun vcg_ni_tac ctxt =
-  TRY o vcg_clarsimp_tac ctxt
-THEN'
-  PARALLEL_GOALS o (
-               vcg_sem_tac ctxt
-         THEN' (TRY o SELECT_GOAL (Local_Defs.unfold_tac ctxt (Inv.get ctxt)))
-         THEN' (TRY o REPEAT_ALL_NEW (Tactic.match_tac ctxt @{thms conjI})) (* expose the location predicates, do not split the consequents *)
-  THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Tactic.match_tac ctxt @{thms impI}))
-                   (* Preserve the label sets in atS but normalise the label in at; turn s' into s *)
-  THEN_ALL_NEW asm_full_simp_tac ctxt (* FIXME diverges on some invariants *)
-  THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Tactic.ematch_tac ctxt @{thms conjE}))
-                   (* The effect of vcg_pre: should be cheap *)
-  THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Tactic.ematch_tac ctxt @{thms thin_locs} THEN' REPEAT1 o assume_tac ctxt))
-  THEN_ALL_NEW asm_full_simp_tac (ss_only (@{thms loc_simps} @ Loc.get ctxt) ctxt)
-  THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Rule_Insts.thin_tac ctxt "True" [])) (* FIXME weird, must be a standard way to do this. Leaving them in can cause simp to diverge ?? *)
-  THEN_ALL_NEW clarsimp_tac ctxt)
+  SELECT_GOAL (
+    HEADGOAL (TRY o vcg_clarsimp_tac ctxt)
+  THEN
+    PARALLEL_ALLGOALS (
+                   vcg_sem_tac ctxt
+             THEN' (TRY o SELECT_GOAL (Local_Defs.unfold_tac ctxt (Inv.get ctxt)))
+             THEN' (TRY o REPEAT_ALL_NEW (Tactic.match_tac ctxt @{thms conjI})) (* expose the location predicates, do not split the consequents *)
+      THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Tactic.match_tac ctxt @{thms impI}))
+                       (* Preserve the label sets in atS but normalise the label in at; turn s' into s *)
+      THEN_ALL_NEW asm_full_simp_tac ctxt (* FIXME diverges on some invariants *)
+      THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Tactic.ematch_tac ctxt @{thms conjE}))
+                       (* The effect of vcg_pre: should be cheap *)
+      THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Tactic.ematch_tac ctxt @{thms thin_locs} THEN' REPEAT1 o assume_tac ctxt))
+      THEN_ALL_NEW asm_full_simp_tac (ss_only (@{thms loc_simps} @ Loc.get ctxt) ctxt)
+      THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Rule_Insts.thin_tac ctxt "True" [])) (* FIXME weird, must be a standard way to do this. Leaving them in can cause simp to diverge ?? *)
+      THEN_ALL_NEW clarsimp_tac ctxt))
 
 fun vcg_nihe_tac ctxt =
-  vcg_clarsimp_tac ctxt
-THEN'
-  PARALLEL_GOALS o (
-        (vcg_sem_tac ctxt THEN_ALL_NEW (Tactic.ematch_tac ctxt (NIE.get ctxt) THEN_ALL_NEW clarsimp_tac ctxt THEN_ALL_NEW SELECT_GOAL no_tac))
-ORELSE' SELECT_GOAL all_tac) (* FIXME perhaps replace with vcg_ni? but less diagnosable then *)
+  SELECT_GOAL (
+    HEADGOAL (vcg_clarsimp_tac ctxt)
+  THEN
+    PARALLEL_ALLGOALS (
+      (vcg_sem_tac ctxt THEN_ALL_NEW (Tactic.ematch_tac ctxt (NIE.get ctxt) THEN_ALL_NEW clarsimp_tac ctxt THEN_ALL_NEW SELECT_GOAL no_tac))
+      ORELSE' SELECT_GOAL all_tac)) (* FIXME perhaps replace with vcg_ni? but less diagnosable then *)
 
 val _ =
   Theory.setup (Method.setup @{binding vcg_ni}