# HG changeset patch
# User nipkow
# Date 1470840949 -7200
# Node ID f8e79d14d61fff02993951d1388bd92124710955
# Parent  e690d6f2185b3b7e1c34445fd7e9127b02198ce1# Parent  50cadecbe5bcbd98265fca089516f20d12846c80
merged

diff -r e690d6f2185b -r f8e79d14d61f NEWS
--- a/NEWS	Wed Aug 10 14:50:59 2016 +0200
+++ b/NEWS	Wed Aug 10 16:55:49 2016 +0200
@@ -49,6 +49,14 @@
 context. Unlike "context includes ... begin", the effect of 'unbundle'
 on the target context persists, until different declarations are given.
 
+* Splitter in simp, auto and friends:
+- The syntax "split add" has been discontinued, use plain "split".
+- For situations with many nested conditional or case expressions,
+there is an alternative splitting strategy that can be much faster.
+It is selected by writing "split!" instead of "split". It applies
+safe introduction and elimination rules after each split rule.
+As a result the subgoal may be split into several subgoals.
+
 * Proof method "blast" is more robust wrt. corner cases of Pure
 statements without object-logic judgment.
 
diff -r e690d6f2185b -r f8e79d14d61f src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Wed Aug 10 14:50:59 2016 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Wed Aug 10 16:55:49 2016 +0200
@@ -270,7 +270,7 @@
 
     opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
     ;
-    @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') |
+    @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | '!' | 'del') |
       'cong' (() | 'add' | 'del')) ':' @{syntax thms}
   \<close>}
 
@@ -300,6 +300,12 @@
   \secref{sec:simp-strategies} on the looper). This works only if the
   Simplifier method has been properly setup to include the Splitter (all major
   object logics such HOL, HOLCF, FOL, ZF do this already).
+  The \<open>!\<close> option causes the split rules to be used aggressively:
+  after each application of a split rule in the conclusion, the \<open>safe\<close>
+  tactic of the classical reasoner (see \secref{sec:classical:partial})
+  is applied to the new goal. The net effect is that the goal is split into
+  the different cases. This option can speed up simplification of goals
+  with many nested conditional or case expressions significantly.
 
   There is also a separate @{method_ref split} method available for
   single-step case splitting. The effect of repeatedly applying \<open>(split thms)\<close>
@@ -468,8 +474,8 @@
   \end{matharray}
 
   @{rail \<open>
-    (@@{attribute simp} | @@{attribute split} | @@{attribute cong})
-      (() | 'add' | 'del')
+    (@@{attribute simp} | @@{attribute cong}) (() | 'add' | 'del') |
+    @@{attribute split} (() | '!' | 'del')
     ;
     @@{command print_simpset} ('!'?)
   \<close>}
@@ -985,6 +991,9 @@
   -> Proof.context"} \\
   @{index_ML_op delloop: "Proof.context * string -> Proof.context"} \\
   @{index_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\
+  @{index_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\
+  @{index_ML Splitter.add_split_bang: "
+  thm -> Proof.context -> Proof.context"} \\
   @{index_ML Splitter.del_split: "thm -> Proof.context -> Proof.context"} \\
   \end{mldecls}
 
@@ -1007,8 +1016,14 @@
     \<^descr> \<open>ctxt delloop name\<close> deletes the looper tactic that was associated with
     \<open>name\<close> from \<open>ctxt\<close>.
 
-    \<^descr> @{ML Splitter.add_split}~\<open>thm ctxt\<close> adds split tactics for \<open>thm\<close> as
-    additional looper tactics of \<open>ctxt\<close>.
+    \<^descr> @{ML Splitter.add_split}~\<open>thm ctxt\<close> adds split tactic
+    for \<open>thm\<close> as additional looper tactic of \<open>ctxt\<close>
+    (overwriting previous split tactic for the same constant).
+
+    \<^descr> @{ML Splitter.add_split_bang}~\<open>thm ctxt\<close> adds aggressive
+    (see \S\ref{sec:simp-meth})
+    split tactic for \<open>thm\<close> as additional looper tactic of \<open>ctxt\<close>
+    (overwriting previous split tactic for the same constant).
 
     \<^descr> @{ML Splitter.del_split}~\<open>thm ctxt\<close> deletes the split tactic
     corresponding to \<open>thm\<close> from the looper tactics of \<open>ctxt\<close>.
@@ -1430,7 +1445,8 @@
       (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thms}
     ;
     @{syntax_def clasimpmod}: ('simp' (() | 'add' | 'del' | 'only') |
-      ('cong' | 'split') (() | 'add' | 'del') |
+      'cong' (() | 'add' | 'del') |
+      'split' (() | '!' | 'del') |
       'iff' (((() | 'add') '?'?) | 'del') |
       (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thms}
   \<close>}
@@ -1524,7 +1540,7 @@
 \<close>
 
 
-subsection \<open>Partially automated methods\<close>
+subsection \<open>Partially automated methods\label{sec:classical:partial}\<close>
 
 text \<open>These proof methods may help in situations when the
   fully-automated tools fail.  The result is a simpler subgoal that
diff -r e690d6f2185b -r f8e79d14d61f src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Wed Aug 10 14:50:59 2016 +0200
+++ b/src/Provers/splitter.ML	Wed Aug 10 16:55:49 2016 +0200
@@ -461,11 +461,10 @@
 fun split_add bang = Simplifier.attrib (gen_add_split bang);
 val split_del = Simplifier.attrib del_split;
 
-val opt_bang = Scan.optional (Args.bang >> K true) false;
-
-val add_del =
-  Scan.lift (Args.add |-- opt_bang >> split_add
-    || Args.del >> K split_del || opt_bang >> split_add);
+val add_del = Scan.lift
+  (Args.bang >> K (split_add true)
+   || Args.del >> K split_del
+   || Scan.succeed (split_add false));
 
 val _ = Theory.setup
   (Attrib.setup @{binding split} add_del "declare case split rule");
@@ -476,8 +475,6 @@
 val split_modifiers =
  [Args.$$$ splitN -- Args.colon >> K (Method.modifier (split_add false) @{here}),
   Args.$$$ splitN -- Args.bang_colon >> K (Method.modifier (split_add true) @{here}),
-  Args.$$$ splitN -- Args.add -- Args.colon >> K (Method.modifier (split_add false) @{here}),
-  Args.$$$ splitN -- Args.add -- Args.bang_colon >> K (Method.modifier (split_add true) @{here}),
   Args.$$$ splitN -- Args.del -- Args.colon >> K (Method.modifier split_del @{here})];
 
 val _ =