# HG changeset patch
# User blanchet
# Date 1389361177 -3600
# Node ID 0ac0b6576d21a5b695a608d653295844d991ac56
# Parent  baa2baf29eff676f4da27ce0253d19112090eb71
generate 'disc_iff' for all discriminators

diff -r baa2baf29eff -r 0ac0b6576d21 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 14:39:37 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 14:39:37 2014 +0100
@@ -1237,7 +1237,7 @@
         fun prove_disc_iff ({ctr_specs, ...} : corec_spec) exhaust_thms disc_thmss'
             (({fun_args = exhaust_fun_args, ...} : coeqn_data_disc) :: _) disc_thms
             ({fun_name, fun_T, fun_args, ctr_no, prems, eqn_pos, ...} : coeqn_data_disc) =
-          if null disc_thms orelse null exhaust_thms then
+          if null exhaust_thms then
             []
           else
             let
@@ -1247,17 +1247,14 @@
                   mk_conjs prems)
                 |> curry Logic.list_all (map dest_Free fun_args);
             in
-              if prems = [@{term False}] then
-                []
-              else
-                mk_primcorec_disc_iff_tac lthy (map (fst o dest_Free) exhaust_fun_args)
-                  (the_single exhaust_thms) (the_single disc_thms) disc_thmss' (flat disc_excludess)
-                |> K |> Goal.prove_sorry lthy [] [] goal
-                |> Thm.close_derivation
-                |> fold (fn rule => perhaps (try (fn thm => thm RS rule)))
-                  @{thms eqTrueE eq_False[THEN iffD1] notnotD}
-                |> pair eqn_pos
-                |> single
+              mk_primcorec_disc_iff_tac lthy (map (fst o dest_Free) exhaust_fun_args)
+                (the_single exhaust_thms) disc_thms disc_thmss' (flat disc_excludess)
+              |> K |> Goal.prove_sorry lthy [] [] goal
+              |> Thm.close_derivation
+              |> fold (fn rule => perhaps (try (fn thm => thm RS rule)))
+                @{thms eqTrueE eq_False[THEN iffD1] notnotD}
+              |> pair eqn_pos
+              |> single
             end;
 
         val disc_iff_thmss = map6 (flat ooo map2 oooo prove_disc_iff) corec_specs exhaust_thmss
diff -r baa2baf29eff -r 0ac0b6576d21 src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Fri Jan 10 14:39:37 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Fri Jan 10 14:39:37 2014 +0100
@@ -12,7 +12,7 @@
   val mk_primcorec_ctr_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
-  val mk_primcorec_disc_iff_tac: Proof.context -> string list -> thm -> thm -> thm list list ->
+  val mk_primcorec_disc_iff_tac: Proof.context -> string list -> thm -> thm list -> thm list list ->
     thm list -> tactic
   val mk_primcorec_exhaust_tac: Proof.context -> string list -> int -> thm -> tactic
   val mk_primcorec_nchotomy_tac: Proof.context -> thm list -> tactic
@@ -108,19 +108,20 @@
 fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss =
   prelude_tac ctxt defs disc_corec THEN cases_tac ctxt k m exclsss;
 
-fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_disc fun_discss disc_excludes =
+fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_discs fun_discss
+    disc_excludes =
   HEADGOAL (rtac iffI THEN'
     rtac fun_exhaust THEN'
     K (exhaust_inst_as_projs_tac ctxt fun_exhaust_frees) THEN'
     EVERY' (map (fn [] => etac FalseE
-        | [fun_disc'] =>
-          if Thm.eq_thm (fun_disc', fun_disc) then
+        | fun_discs' as [fun_disc'] =>
+          if eq_list Thm.eq_thm (fun_discs', fun_discs) then
             REPEAT_DETERM o etac conjI THEN' (atac ORELSE' rtac TrueI)
           else
             rtac FalseE THEN' rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac THEN'
             dresolve_tac disc_excludes THEN' etac notE THEN' atac)
       fun_discss) THEN'
-    rtac (unfold_thms ctxt [atomize_conjL] fun_disc) THEN_MAYBE' atac);
+    resolve_tac (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' atac);
 
 fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_idents map_comps fun_sel k
     m exclsss =