generate 'map_cong_simp' for BNFs

--- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Aug 18 14:19:23 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Aug 18 15:03:22 2014 +0200
@@ -60,6 +60,7 @@
   val map_comp_of_bnf: bnf -> thm
   val map_cong0_of_bnf: bnf -> thm
   val map_cong_of_bnf: bnf -> thm
+  val map_cong_simp_of_bnf: bnf -> thm
   val map_def_of_bnf: bnf -> thm
   val map_id0_of_bnf: bnf -> thm
   val map_id_of_bnf: bnf -> thm
@@ -227,6 +228,7 @@
   inj_map_strong: thm lazy,
   map_comp: thm lazy,
   map_cong: thm lazy,
+  map_cong_simp: thm lazy,
   map_id: thm lazy,
   map_ident0: thm lazy,
   map_ident: thm lazy,
@@ -245,9 +247,9 @@
 };
 
 fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
-    inj_map inj_map_strong map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq
-    rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_mono_strong rel_Grp
-    rel_conversep rel_OO = {
+    inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0 map_ident
+    map_transfer rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_mono_strong
+    rel_Grp rel_conversep rel_OO = {
   bd_Card_order = bd_Card_order,
   bd_Cinfinite = bd_Cinfinite,
   bd_Cnotzero = bd_Cnotzero,
@@ -260,6 +262,7 @@
   inj_map_strong = inj_map_strong,
   map_comp = map_comp,
   map_cong = map_cong,
+  map_cong_simp = map_cong_simp,
   map_id = map_id,
   map_ident0 = map_ident0,
   map_ident = map_ident,
@@ -289,6 +292,7 @@
   inj_map_strong,
   map_comp,
   map_cong,
+  map_cong_simp,
   map_id,
   map_ident0,
   map_ident,
@@ -316,6 +320,7 @@
     inj_map_strong = Lazy.map f inj_map_strong,
     map_comp = Lazy.map f map_comp,
     map_cong = Lazy.map f map_cong,
+    map_cong_simp = Lazy.map f map_cong_simp,
     map_id = Lazy.map f map_id,
     map_ident0 = Lazy.map f map_ident0,
     map_ident = Lazy.map f map_ident,
@@ -446,6 +451,7 @@
 val map_comp_of_bnf = Lazy.force o #map_comp o #facts o rep_bnf;
 val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf;
 val map_cong_of_bnf = Lazy.force o #map_cong o #facts o rep_bnf;
+val map_cong_simp_of_bnf = Lazy.force o #map_cong_simp o #facts o rep_bnf;
 val map_transfer_of_bnf = Lazy.force o #map_transfer o #facts o rep_bnf;
 val le_rel_OO_of_bnf = #le_rel_OO o #axioms o rep_bnf;
 val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
@@ -619,6 +625,7 @@
 val map_compN = "map_comp";
 val map_cong0N = "map_cong0";
 val map_congN = "map_cong";
+val map_cong_simpN = "map_cong_simp";
 val map_transferN = "map_transfer";
 val rel_eqN = "rel_eq";
 val rel_flipN = "rel_flip";
@@ -689,6 +696,7 @@
            (map_compN, [Lazy.force (#map_comp facts)], []),
            (map_cong0N, [#map_cong0 axioms], []),
            (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
+           (map_cong_simpN, [Lazy.force (#map_cong_simp facts)], []),
            (map_idN, [Lazy.force (#map_id facts)], []),
            (map_id0N, [#map_id0 axioms], []),
            (map_identN, [Lazy.force (#map_ident facts)], []),
@@ -1011,13 +1019,13 @@
         fold_rev Logic.all (fs @ gs) (mk_Trueprop_eq (bnf_map_app_comp, comp_bnf_map_app))
       end;
 
-    fun mk_map_cong_prem x z set f f_copy =
-      Logic.all z (Logic.mk_implies
+    fun mk_map_cong_prem mk_implies x z set f f_copy =
+      Logic.all z (mk_implies
         (mk_Trueprop_mem (z, set $ x), mk_Trueprop_eq (f $ z, f_copy $ z)));
 
     val map_cong0_goal =
       let
-        val prems = map4 (mk_map_cong_prem x) zs bnf_sets_As fs fs_copy;
+        val prems = map4 (mk_map_cong_prem Logic.mk_implies x) zs bnf_sets_As fs fs_copy;
         val eq = mk_Trueprop_eq (Term.list_comb (bnf_map_AsBs, fs) $ x,
           Term.list_comb (bnf_map_AsBs, fs_copy) $ x);
       in
@@ -1147,20 +1155,23 @@
         val map_ident = Lazy.lazy (fn () => mk_map_ident lthy (Lazy.force map_id));
         val map_comp = Lazy.lazy (fn () => mk_map_comp (#map_comp0 axioms));
 
-        fun mk_map_cong () =
+        fun mk_map_cong mk_implies () =
           let
             val prem0 = mk_Trueprop_eq (x, x_copy);
-            val prems = map4 (mk_map_cong_prem x_copy) zs bnf_sets_As fs fs_copy;
+            val prems = map4 (mk_map_cong_prem mk_implies x_copy) zs bnf_sets_As fs fs_copy;
             val eq = mk_Trueprop_eq (Term.list_comb (bnf_map_AsBs, fs) $ x,
               Term.list_comb (bnf_map_AsBs, fs_copy) $ x_copy);
             val goal = fold_rev Logic.all (x :: x_copy :: fs @ fs_copy)
               (Logic.list_implies (prem0 :: prems, eq));
           in
-            Goal.prove_sorry lthy [] [] goal (fn _ => mk_map_cong_tac lthy (#map_cong0 axioms))
+            Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+              unfold_thms_tac lthy @{thms simp_implies_def} THEN
+              mk_map_cong_tac lthy (#map_cong0 axioms))
             |> Thm.close_derivation
           end;
 
-        val map_cong = Lazy.lazy mk_map_cong;
+        val map_cong = Lazy.lazy (mk_map_cong Logic.mk_implies);
+        val map_cong_simp = Lazy.lazy (mk_map_cong (fn (a, b) => @{term simp_implies} $ a $ b));
 
         fun mk_inj_map () =
           let
@@ -1416,8 +1427,8 @@
         val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def;
 
         val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
-          in_mono in_rel inj_map inj_map_strong map_comp map_cong map_id map_ident0 map_ident
-          map_transfer rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0
+          in_mono in_rel inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0
+          map_ident map_transfer rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0
           rel_mono_strong rel_Grp rel_conversep rel_OO;
 
         val wits = map2 mk_witness bnf_wits wit_thms;