# HG changeset patch
# User blanchet
# Date 1380150306 -7200
# Node ID 527ece7edc51b06d45a8a2944d2615a1ef12dea1
# Parent  e55b634ff9fbfffa25c3cb269ed433ed600d328a
made tactic more flexible w.r.t. case expressions and such

diff -r e55b634ff9fb -r 527ece7edc51 src/HOL/BNF/BNF_FP_Base.thy
--- a/src/HOL/BNF/BNF_FP_Base.thy	Wed Sep 25 21:25:53 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Base.thy	Thu Sep 26 01:05:06 2013 +0200
@@ -13,6 +13,9 @@
 imports BNF_Comp BNF_Ctr_Sugar
 begin
 
+lemma not_TrueE: "\<not> True \<Longrightarrow> P"
+by (erule notE, rule TrueI)
+
 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
 by auto
 
@@ -162,16 +165,6 @@
 lemma eq_ifI: "\<lbrakk>b \<Longrightarrow> t = x; \<not> b \<Longrightarrow> t = y\<rbrakk> \<Longrightarrow> t = (if b then x else y)"
   by fastforce
 
-lemma if_if_True:
-  "(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) =
-   (if b then x else if b' then x' else f y')"
-  by simp
-
-lemma if_if_False:
-  "(if (if b then False else b') then (if b then x else x') else f (if b then y else y')) =
-   (if b then f y else if b' then x' else f y')"
-  by simp
-
 ML_file "Tools/bnf_fp_util.ML"
 ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
 ML_file "Tools/bnf_fp_def_sugar.ML"
diff -r e55b634ff9fb -r 527ece7edc51 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Sep 25 21:25:53 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 26 01:05:06 2013 +0200
@@ -802,7 +802,7 @@
               |> curry Logic.list_all (map dest_Free fun_args);
           in
             mk_primcorec_ctr_or_sel_tac lthy def_thms sel_corec k m exclsss
-              nested_maps nested_map_idents nested_map_comps
+              nested_maps nested_map_idents nested_map_comps [] []
             |> K |> Goal.prove lthy [] [] t
             |> pair sel
           end;
diff -r e55b634ff9fb -r 527ece7edc51 src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Wed Sep 25 21:25:53 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 26 01:05:06 2013 +0200
@@ -12,7 +12,7 @@
   val mk_primcorec_code_of_ctr_tac: Proof.context -> thm list -> int list -> thm list -> tactic
   val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
   val mk_primcorec_ctr_or_sel_tac: Proof.context -> thm list -> thm -> int -> int ->
-    thm list list list -> thm list -> thm list -> thm list -> tactic
+    thm list list list -> thm list -> thm list -> thm list -> thm list -> thm list ->tactic
   val mk_primcorec_disc_of_ctr_tac: thm -> thm -> tactic;
   val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
     tactic
@@ -56,12 +56,17 @@
 fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss =
   mk_primcorec_prelude ctxt defs disc_corec THEN mk_primcorec_cases_tac ctxt k m exclsss;
 
-fun mk_primcorec_ctr_or_sel_tac ctxt defs f_eq k m exclsss maps map_idents map_comps =
+fun mk_primcorec_ctr_or_sel_tac ctxt defs f_eq k m exclsss maps map_idents map_comps splits
+    split_asms =
   mk_primcorec_prelude ctxt defs (f_eq RS trans) THEN
   mk_primcorec_cases_tac ctxt k m exclsss THEN
-  unfold_thms_tac ctxt (@{thms if_if_True if_if_False if_True if_False if_cancel[of _ True]
-    if_cancel[of _ False] o_def split_def sum.cases} @ maps @ map_comps @ map_idents) THEN
-  HEADGOAL (rtac refl);
+  unfold_thms_tac ctxt (@{thms o_def split_def sum.cases} @ maps @ map_comps @ map_idents) THEN
+  HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE'
+    eresolve_tac @{thms not_TrueE FalseE} ORELSE'
+    resolve_tac @{thms allI impI conjI} ORELSE'
+    Splitter.split_asm_tac (@{thm split_if_asm} :: split_asms) ORELSE'
+    Splitter.split_tac (@{thm split_if} :: splits) ORELSE'
+    etac notE THEN' atac));
 
 fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs =
   HEADGOAL (rtac ((if null sel_fs then collapse else collapse RS sym) RS trans) THEN'