# HG changeset patch
# User blanchet
# Date 1430669651 -7200
# Node ID 98754695b421f328baa4276c29b1dfd0bd0cd6c9
# Parent  baf2c8fddaa4ee55ddd60f1dd2cb4200ccfba093
made split-rule tactic go beyond constructors with 20 arguments

diff -r baf2c8fddaa4 -r 98754695b421 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Sun May 03 20:21:25 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Sun May 03 18:14:11 2015 +0200
@@ -37,6 +37,8 @@
 val split_connectI = @{thms allI impI conjI};
 val unfold_lets = @{thms Let_def[abs_def] split_beta}
 
+fun clean_blast_tac ctxt = blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt);
+
 fun exhaust_inst_as_projs ctxt frees thm =
   let
     val num_frees = length frees;
diff -r baf2c8fddaa4 -r 98754695b421 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sun May 03 20:21:25 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sun May 03 18:14:11 2015 +0200
@@ -751,7 +751,7 @@
 
         fun prove_split selss goal =
           Goal.prove_sorry lthy [] [] goal (fn _ =>
-            mk_split_tac lthy uexhaust_thm case_thms selss inject_thmss distinct_thmsss)
+            mk_split_tac lthy ms uexhaust_thm case_thms selss inject_thmss distinct_thmsss)
           |> singleton (Proof_Context.export names_lthy lthy)
           |> Thm.close_derivation;
 
diff -r baf2c8fddaa4 -r 98754695b421 src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sun May 03 20:21:25 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sun May 03 18:14:11 2015 +0200
@@ -7,7 +7,6 @@
 
 signature CTR_SUGAR_GENERAL_TACTICS =
 sig
-  val clean_blast_tac: Proof.context -> int -> tactic
   val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
   val unfold_thms_tac: Proof.context -> thm list -> tactic
 end;
@@ -32,8 +31,8 @@
   val mk_half_distinct_disc_tac: Proof.context -> int -> thm -> thm -> tactic
   val mk_nchotomy_tac: int -> thm -> tactic
   val mk_other_half_distinct_disc_tac: thm -> tactic
-  val mk_split_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list ->
-    thm list list list -> tactic
+  val mk_split_tac: Proof.context -> int list -> thm -> thm list -> thm list list ->
+    thm list list -> thm list list list -> tactic
   val mk_split_asm_tac: Proof.context -> thm -> tactic
   val mk_unique_disc_def_tac: int -> thm -> tactic
 end;
@@ -45,7 +44,8 @@
 
 val meta_mp = @{thm meta_mp};
 
-fun clean_blast_tac ctxt = blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt);
+fun clean_blast_depth_tac ctxt depth =
+  depth_tac (put_claset (claset_of @{theory_context HOL}) ctxt) depth;
 
 fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl,
   tac, REPEAT_DETERM_N (n - k) o etac thin_rl]);
@@ -170,12 +170,14 @@
           rtac casex])
       cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss));
 
-fun mk_split_tac ctxt uexhaust cases selss injectss distinctsss =
-  HEADGOAL (rtac uexhaust) THEN
-  ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
-     simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @
-       flat (nth distinctsss (k - 1))) ctxt)) k) THEN
-  ALLGOALS (clean_blast_tac ctxt);
+fun mk_split_tac ctxt ms uexhaust cases selss injectss distinctsss =
+  let val depth = fold Integer.max ms 0 in
+    HEADGOAL (rtac uexhaust) THEN
+    ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
+       simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @
+         flat (nth distinctsss (k - 1))) ctxt)) k) THEN
+    ALLGOALS (clean_blast_depth_tac ctxt depth)
+  end;
 
 val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};