# HG changeset patch
# User blanchet
# Date 1380155133 -7200
# Node ID 446076262e92003eac0027033afc613e688f4d0f
# Parent  27fd72593624ae91cb3da931b72e761e9ca5dc14
got rid of dependency on silly 'eq_ifI' theorem

diff -r 27fd72593624 -r 446076262e92 src/HOL/BNF/BNF_FP_Base.thy
--- a/src/HOL/BNF/BNF_FP_Base.thy	Thu Sep 26 02:09:52 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Base.thy	Thu Sep 26 02:25:33 2013 +0200
@@ -165,9 +165,6 @@
    (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
   unfolding Grp_def by rule auto
 
-lemma eq_ifI: "\<lbrakk>b \<Longrightarrow> t = x; \<not> b \<Longrightarrow> t = y\<rbrakk> \<Longrightarrow> t = (if b then x else y)"
-  by fastforce
-
 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 27fd72593624 -r 446076262e92 src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 26 02:09:52 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 26 02:25:33 2013 +0200
@@ -8,9 +8,9 @@
 signature BNF_FP_REC_SUGAR_TACTICS =
 sig
   val mk_primcorec_assumption_tac: Proof.context -> thm list -> tactic
-  val mk_primcorec_code_tac: thm list -> thm list -> thm -> thm list -> tactic
   val mk_primcorec_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
     thm list -> int list -> thm list -> tactic
+  val mk_primcorec_code_of_raw_tac: thm list -> thm list -> thm -> thm list -> tactic
   val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
   val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
     tactic
@@ -80,13 +80,14 @@
   unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl);
 
 fun mk_primcorec_split distincts discIs collapses splits split_asms =
-  HEADGOAL (SELECT_GOAL (HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' atac ORELSE'
-    eresolve_tac (@{thms not_TrueE FalseE} @ map (fn thm => thm RS trans) collapses) ORELSE'
-    resolve_tac split_connectI ORELSE'
-    Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
-    Splitter.split_tac (split_if :: splits) ORELSE'
-    eresolve_tac (map (fn thm => thm RS @{thm neq_eq_eq_contradict}) distincts) THEN' atac ORELSE'
-    (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac))));
+  HEADGOAL (SELECT_GOAL (HEADGOAL (REPEAT_DETERM o
+    (rtac refl ORELSE' atac ORELSE'
+     eresolve_tac (@{thms not_TrueE FalseE} @ map (fn thm => thm RS trans) collapses) ORELSE'
+     resolve_tac split_connectI ORELSE'
+     Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
+     Splitter.split_tac (split_if :: splits) ORELSE'
+     eresolve_tac (map (fn thm => thm RS @{thm neq_eq_eq_contradict}) distincts) THEN' atac ORELSE'
+     (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac))));
 
 fun mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs collapses splits split_asms m f_ctr =
   HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE' split_tac (split_if :: splits))) THEN
@@ -98,10 +99,13 @@
   EVERY (map2 (mk_primcorec_code_of_ctr_single_tac ctxt distincs discIs collapses splits split_asms)
     ms ctr_thms);
 
-fun mk_primcorec_code_tac eq_caseIs disc_excludes raw collapses =
-  HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' REPEAT o
-    (resolve_tac (maps (fn thm => [thm, thm RS sym]) (@{thm eq_ifI} :: eq_caseIs)) ORELSE'
-     rtac refl ORELSE' etac notE THEN' atac ORELSE'
+fun mk_primcorec_code_of_raw_tac splits disc_excludes raw collapses =
+  HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' REPEAT_DETERM o
+    (rtac refl ORELSE'
+     (TRY o rtac sym) THEN' atac ORELSE'
+     resolve_tac split_connectI ORELSE'
+     Splitter.split_tac (split_if :: splits) ORELSE'
+     etac notE THEN' atac ORELSE'
      dresolve_tac disc_excludes THEN' etac notE THEN' atac ORELSE'
      eresolve_tac (maps (fn thm => [thm, thm RS sym]) collapses)));