# HG changeset patch
# User desharna
# Date 1411390887 -7200
# Node ID fa50722ad6cbe7ce46580c919c5dfeb831b9710d
# Parent  d94ec306b7a8cf081389e54767bbd00c6a13798b
make 'set_induct0' tactic more robust w.r.t multiple arguments constructors

diff -r d94ec306b7a8 -r fa50722ad6cb src/HOL/Datatype_Examples/Misc_Codatatype.thy
--- a/src/HOL/Datatype_Examples/Misc_Codatatype.thy	Mon Sep 22 10:55:51 2014 +0200
+++ b/src/HOL/Datatype_Examples/Misc_Codatatype.thy	Mon Sep 22 15:01:27 2014 +0200
@@ -26,6 +26,16 @@
 codatatype ('b, 'c :: ord, 'd, 'e) some_passive =
   SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
 
+codatatype 'a multi_live_direct1 = MultiLiveDirect1 'a
+codatatype 'a multi_live_direct2 = MultiLiveDirect2 'a 'a
+codatatype 'a multi_live_direct3 = MultiLiveDirect3 'a 'a 'a
+codatatype 'a multi_live_direct4 = MultiLiveDirect4 'a 'a 'a 'a
+codatatype 'a multi_live_direct5 = MultiLiveDirect5 'a 'a 'a 'a 'a
+codatatype 'a multi_live_direct6 = MultiLiveDirect6 'a 'a 'a 'a 'a 'a
+codatatype 'a multi_live_direct7 = MultiLiveDirect7 'a 'a 'a 'a 'a 'a 'a
+codatatype 'a multi_live_direct8 = MultiLiveDirect8 'a 'a 'a 'a 'a 'a 'a 'a
+codatatype 'a multi_live_direct9 = MultiLiveDirect9 'a 'a 'a 'a 'a 'a 'a 'a 'a
+
 codatatype lambda =
   Var string |
   App lambda lambda |
diff -r d94ec306b7a8 -r fa50722ad6cb src/HOL/Datatype_Examples/Misc_Datatype.thy
--- a/src/HOL/Datatype_Examples/Misc_Datatype.thy	Mon Sep 22 10:55:51 2014 +0200
+++ b/src/HOL/Datatype_Examples/Misc_Datatype.thy	Mon Sep 22 15:01:27 2014 +0200
@@ -24,6 +24,16 @@
 datatype (discs_sels) ('b, 'c :: ord, 'd, 'e) some_passive =
   SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
 
+datatype (discs_sels) 'a multi_live_direct1 = MultiLiveDirect1 'a
+datatype (discs_sels) 'a multi_live_direct2 = MultiLiveDirect2 'a 'a
+datatype (discs_sels) 'a multi_live_direct3 = MultiLiveDirect3 'a 'a 'a
+datatype (discs_sels) 'a multi_live_direct4 = MultiLiveDirect4 'a 'a 'a 'a
+datatype (discs_sels) 'a multi_live_direct5 = MultiLiveDirect5 'a 'a 'a 'a 'a
+datatype (discs_sels) 'a multi_live_direct6 = MultiLiveDirect6 'a 'a 'a 'a 'a 'a
+datatype (discs_sels) 'a multi_live_direct7 = MultiLiveDirect7 'a 'a 'a 'a 'a 'a 'a
+datatype (discs_sels) 'a multi_live_direct8 = MultiLiveDirect8 'a 'a 'a 'a 'a 'a 'a 'a
+datatype (discs_sels) 'a multi_live_direct9 = MultiLiveDirect9 'a 'a 'a 'a 'a 'a 'a 'a 'a
+
 datatype (discs_sels) hfset = HFset "hfset fset"
 
 datatype (discs_sels) lambda =
diff -r d94ec306b7a8 -r fa50722ad6cb src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Sep 22 10:55:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Sep 22 15:01:27 2014 +0200
@@ -365,7 +365,12 @@
 fun mk_set_induct0_tac ctxt cts assms dtor_set_inducts exhausts set_pre_defs ctor_defs dtor_ctors
     Abs_pre_inverses =
   let
-    val assms_ctor_defs = map (unfold_thms ctxt (@{thm id_bnf_def} :: ctor_defs)) assms;
+    val assms_tac =
+      let val assms' = map (unfold_thms ctxt (@{thm id_bnf_def} :: ctor_defs)) assms in
+        fold (curry (op ORELSE')) (map (fn thm =>
+            funpow (length (prems_of thm)) (fn tac => tac THEN' atac) (rtac thm)) assms')
+          (etac FalseE)
+      end;
     val exhausts' = map (fn thm => thm RS @{thm asm_rl[of "P x y" for P x y]}) exhausts
       |> map2 (fn ct => cterm_instantiate_pos [NONE, SOME ct]) cts;
   in
@@ -377,12 +382,8 @@
     unfold_thms_tac ctxt (Abs_pre_inverses @ dtor_ctors @ set_pre_defs @ ctor_defs @
       @{thms id_bnf_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert Un_empty_left
         Un_empty_right empty_iff singleton_iff}) THEN
-    REPEAT_DETERM (HEADGOAL
-      (TRY o etac UnE THEN' TRY o etac @{thm singletonE} THEN' TRY o hyp_subst_tac ctxt THEN'
-       REPEAT_DETERM o eresolve_tac @{thms UN_E UnE singletonE} THEN'
-       fold (curry (op ORELSE')) (map (fn thm =>
-         funpow (length (prems_of thm)) (fn tac => tac THEN' atac) (rtac thm)) assms_ctor_defs)
-         (etac FalseE)))
+    REPEAT (HEADGOAL (hyp_subst_tac ctxt ORELSE' eresolve_tac @{thms UN_E UnE singletonE} ORELSE'
+      assms_tac))
   end;
 
 end;