generate 'set_empty' theorem for BNFs

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu May 08 12:54:33 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon May 12 17:42:54 2014 +0200
@@ -97,6 +97,7 @@
 open BNF_LFP_Size
 
 val EqN = "Eq_";
+val set_emptyN = "set_empty";
 
 structure Data = Generic_Data
 (
@@ -1115,7 +1116,8 @@
             free_constructors tacss ((wrap_opts, standard_binding), ctr_specs) lthy
           end;
 
-        fun derive_maps_sets_rels (ctr_sugar as {case_cong, ...} : ctr_sugar, lthy) =
+        fun derive_maps_sets_rels
+          (ctr_sugar as {case_cong, discs, ctrs, exhaust, disc_thmss, ...} : ctr_sugar, lthy) =
           if live = 0 then
             ((([], [], [], []), ctr_sugar), lthy)
           else
@@ -1164,6 +1166,36 @@
               val set_thmss = map mk_set_thms fp_set_thms;
               val set_thms = flat set_thmss;
 
+              fun mk_set t =
+                let
+                  val Type (_, Ts0) = domain_type (fastype_of t);
+                  val Type (_, Ts) = fpT;
+                in
+                  Term.subst_atomic_types (Ts0 ~~ Ts) t
+                end;
+
+              val sets = map mk_set (sets_of_bnf fp_bnf);
+              val ctr_argT_namess = map ((fn Ts => fold Term.add_tfree_namesT Ts []) o
+                binder_types o fastype_of) ctrs;
+              val setTs = map (HOLogic.dest_setT o range_type o fastype_of) sets;
+              val setT_names = map (fn T => the_single (Term.add_tfree_namesT T [])) setTs;
+              fun mk_set_empty_goal disc set T = Logic.mk_implies (HOLogic.mk_Trueprop (disc $ u),
+                mk_Trueprop_eq (set $ u, HOLogic.mk_set T []));
+              val goals = map_filter I (flat
+                (map2 (fn names => fn disc =>
+                  map3 (fn name => fn setT => fn set =>
+                    if member (op =) names name then NONE
+                    else SOME (mk_set_empty_goal disc set setT))
+                  setT_names setTs sets)
+                ctr_argT_namess discs));
+
+              val set_empty_thms = if null goals then []
+                else Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
+                  (fn {context = ctxt, prems = _} =>
+                    mk_set_empty_tac ctxt (certify ctxt u) exhaust set_thms (flat disc_thmss))
+                  |> Conjunction.elim_balanced (length goals)
+                  |> Proof_Context.export names_lthy lthy;
+
               val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns);
 
               fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
@@ -1208,7 +1240,8 @@
                 [(mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs),
                  (rel_distinctN, rel_distinct_thms, simp_attrs),
                  (rel_injectN, rel_inject_thms, simp_attrs),
-                 (setN, set_thms, code_nitpicksimp_attrs @ simp_attrs)]
+                 (setN, set_thms, code_nitpicksimp_attrs @ simp_attrs),
+                 (set_emptyN, set_empty_thms, [])]
                 |> massage_simple_notes fp_b_name;
             in
               (((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_sugar),

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu May 08 12:54:33 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon May 12 17:42:54 2014 +0200
@@ -25,6 +25,7 @@
   val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic
   val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
     tactic
+  val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
 end;
 
 structure BNF_FP_Def_Sugar_Tactics : BNF_FP_DEF_SUGAR_TACTICS =
@@ -191,4 +192,12 @@
       (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
       selsss));
 
+fun mk_set_empty_tac ctxt ct exhaust sets discs =
+  TRYALL Goal.conjunction_tac THEN
+  ALLGOALS(rtac (Ctr_Sugar_Util.cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+    hyp_subst_tac ctxt) THEN
+  Local_Defs.unfold_tac ctxt (sets @ map_filter (fn thm =>
+    SOME (thm RS @{thm iffD2[OF eq_False]}) handle THM _ => NONE) discs) THEN
+  ALLGOALS(rtac refl ORELSE' etac FalseE);
+
 end;