generate 'rel_map' theorem for BNFs

--- a/src/HOL/Tools/BNF/bnf_def.ML	Wed Aug 13 22:29:43 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Aug 14 13:20:54 2014 +0200
@@ -232,6 +232,7 @@
   rel_flip: thm lazy,
   set_map: thm lazy list,
   rel_cong: thm lazy,
+  rel_map: thm list lazy,
   rel_mono: thm lazy,
   rel_mono_strong: thm lazy,
   rel_Grp: thm lazy,
@@ -241,7 +242,7 @@
 
 fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
     inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq rel_flip set_map
-    rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO = {
+    rel_cong rel_map rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO = {
   bd_Card_order = bd_Card_order,
   bd_Cinfinite = bd_Cinfinite,
   bd_Cnotzero = bd_Cnotzero,
@@ -261,6 +262,7 @@
   rel_flip = rel_flip,
   set_map = set_map,
   rel_cong = rel_cong,
+  rel_map = rel_map,
   rel_mono = rel_mono,
   rel_mono_strong = rel_mono_strong,
   rel_Grp = rel_Grp,
@@ -287,6 +289,7 @@
   rel_flip,
   set_map,
   rel_cong,
+  rel_map,
   rel_mono,
   rel_mono_strong,
   rel_Grp,
@@ -311,6 +314,7 @@
     rel_flip = Lazy.map f rel_flip,
     set_map = map (Lazy.map f) set_map,
     rel_cong = Lazy.map f rel_cong,
+    rel_map = Lazy.map (map f) rel_map,
     rel_mono = Lazy.map f rel_mono,
     rel_mono_strong = Lazy.map f rel_mono_strong,
     rel_Grp = Lazy.map f rel_Grp,
@@ -609,6 +613,7 @@
 val set_bdN = "set_bd";
 val rel_GrpN = "rel_Grp";
 val rel_conversepN = "rel_conversep";
+val rel_mapN = "rel_map"
 val rel_monoN = "rel_mono"
 val rel_mono_strongN = "rel_mono_strong"
 val rel_comppN = "rel_compp";
@@ -676,6 +681,7 @@
            (rel_eqN, [Lazy.force (#rel_eq facts)], []),
            (rel_flipN, [Lazy.force (#rel_flip facts)], []),
            (rel_GrpN, [Lazy.force (#rel_Grp facts)], []),
+           (rel_mapN, Lazy.force (#rel_map facts), []),
            (rel_monoN, [Lazy.force (#rel_mono facts)], []),
            (set_mapN, map Lazy.force (#set_map facts), [])]
           |> filter_out (null o #2)
@@ -920,6 +926,7 @@
     val pred2RTs = map2 mk_pred2T As' Bs';
     val pred2RTsAsCs = map2 mk_pred2T As' Cs;
     val pred2RTsBsCs = map2 mk_pred2T Bs' Cs;
+    val pred2RTsCsBs = map2 mk_pred2T Cs Bs';
     val pred2RT's = map2 mk_pred2T Bs' As';
     val self_pred2RTs = map2 mk_pred2T As' As';
     val transfer_domRTs = map2 mk_pred2T As' B1Ts;
@@ -941,12 +948,13 @@
     fun mk_bnf_rel RTs CA CB = normalize_rel lthy RTs CA CB bnf_rel;
 
     val pre_names_lthy = lthy;
-    val (((((((((((((((fs, gs), hs), x), y), zs), ys), As),
-      As_copy), bs), Rs), Rs_copy), Ss),
+    val ((((((((((((((((((fs, gs), hs), is), x), y), zs), ys), As),
+      As_copy), bs), Rs), Rs_copy), Ss), S_AsCs), S_CsBs),
       transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy
       |> mk_Frees "f" (map2 (curry op -->) As' Bs')
       ||>> mk_Frees "g" (map2 (curry op -->) Bs' Cs)
       ||>> mk_Frees "h" (map2 (curry op -->) As' Ts)
+      ||>> mk_Frees "i" (map2 (curry op -->) As' Cs)
       ||>> yield_singleton (mk_Frees "x") CA'
       ||>> yield_singleton (mk_Frees "y") CB'
       ||>> mk_Frees "z" As'
@@ -957,6 +965,8 @@
       ||>> mk_Frees "R" pred2RTs
       ||>> mk_Frees "R" pred2RTs
       ||>> mk_Frees "S" pred2RTsBsCs
+      ||>> mk_Frees "S" pred2RTsAsCs
+      ||>> mk_Frees "S" pred2RTsCsBs
       ||>> mk_Frees "R" transfer_domRTs
       ||>> mk_Frees "S" transfer_ranRTs;
 
@@ -1022,6 +1032,7 @@
 
     val relAsCs = mk_bnf_rel pred2RTsAsCs CA' CC';
     val relBsCs = mk_bnf_rel pred2RTsBsCs CB' CC';
+    val relCsBs = mk_bnf_rel pred2RTsCsBs CC' CB';
     val rel_OO_lhs = Term.list_comb (relAsCs, map2 (curry mk_rel_compp) Rs Ss);
     val rel_OO_rhs = mk_rel_compp (Term.list_comb (rel, Rs), Term.list_comb (relBsCs, Ss));
     val le_rel_OO_goal =
@@ -1308,6 +1319,32 @@
 
         val rel_mono_strong = Lazy.lazy mk_rel_mono_strong;
 
+        fun mk_rel_map () =
+          let
+            fun mk_goal lhs rhs =
+              fold_rev Logic.all ([x, y] @ S_CsBs @ S_AsCs @ is @ gs) (mk_Trueprop_eq (lhs, rhs));
+
+            val lhss =
+              [Term.list_comb (relCsBs, S_CsBs) $ (Term.list_comb (bnf_map_AsCs, is) $ x) $ y,
+               Term.list_comb (relAsCs, S_AsCs) $ x $ (Term.list_comb (bnf_map_BsCs, gs) $ y)];
+            val rhss =
+              [Term.list_comb (rel, map3 (fn f => fn P => fn T =>
+                 mk_vimage2p f (HOLogic.id_const T) $ P) is S_CsBs Bs') $ x $ y,
+               Term.list_comb (rel, map3 (fn f => fn P => fn T =>
+                 mk_vimage2p (HOLogic.id_const T) f $ P) gs S_AsCs As') $ x $ y];
+            val goals = map2 mk_goal lhss rhss;
+          in
+            Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
+              (fn {context = ctxt, prems = _} =>
+                 mk_rel_map0_tac ctxt live (Lazy.force rel_OO) (Lazy.force rel_conversep)
+                  (Lazy.force rel_Grp) (Lazy.force map_id))
+            |> Conjunction.elim_balanced (length goals)
+            |> map (unfold_thms lthy @{thms vimage2p_def id_apply})
+            |> map Thm.close_derivation
+          end;
+
+        val rel_map = Lazy.lazy mk_rel_map;
+
         fun mk_map_transfer () =
           let
             val rels = map2 mk_rel_fun transfer_domRs transfer_ranRs;
@@ -1331,7 +1368,7 @@
 
         val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
           in_mono in_rel inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq
-          rel_flip set_map rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
+          rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
 
         val wits = map2 mk_witness bnf_wits wit_thms;
 

--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Wed Aug 13 22:29:43 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Thu Aug 14 13:20:54 2014 +0200
@@ -23,6 +23,7 @@
   val mk_rel_OO_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
   val mk_rel_conversep_tac: thm -> thm -> tactic
   val mk_rel_conversep_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
+  val mk_rel_map0_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic
   val mk_rel_mono_tac: thm list -> thm -> tactic
   val mk_rel_mono_strong_tac: Proof.context -> thm -> thm list -> tactic
 
@@ -118,6 +119,26 @@
     rtac @{thm equalityI}, rtac subset_UNIV, rtac subsetI, rtac CollectI,
     CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac map_id0])) 1;
 
+fun mk_rel_map0_tac ctxt live rel_compp rel_conversep rel_Grp map_id =
+  if live = 0 then
+    HEADGOAL (Goal.conjunction_tac) THEN
+    unfold_thms_tac ctxt @{thms id_apply} THEN
+    ALLGOALS (rtac refl)
+  else
+    let
+      val ks = 1 upto live;
+    in
+      Goal.conjunction_tac 1 THEN
+      unfold_thms_tac ctxt [rel_compp, rel_conversep, rel_Grp, @{thm vimage2p_Grp}] THEN
+      TRYALL (EVERY' [rtac iffI, rtac @{thm relcomppI}, rtac @{thm GrpI},
+        resolve_tac [map_id, refl], rtac CollectI,
+        CONJ_WRAP' (K (rtac @{thm subset_UNIV})) ks, rtac @{thm relcomppI}, atac,
+        rtac @{thm conversepI}, rtac @{thm GrpI}, resolve_tac [map_id, refl], rtac CollectI,
+        CONJ_WRAP' (K (rtac @{thm subset_UNIV})) ks,
+        REPEAT_DETERM o eresolve_tac @{thms relcomppE conversepE GrpE},
+        dtac (trans OF [sym, map_id]), hyp_subst_tac ctxt, atac])
+    end;
+
 fun mk_rel_mono_tac rel_OO_Grps in_mono =
   let
     val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Aug 13 22:29:43 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Aug 14 13:20:54 2014 +0200
@@ -471,7 +471,7 @@
   #>> map (fn thm => Thm.permute_prems 0 (~1) (thm RS prop))
   ##> (fn thm => Thm.permute_prems 0 (~nn)
     (if nn = 1 then thm RS prop
-     else funpow nn (fn thm => Local_Defs.unfold lthy @{thms conj_assoc} (thm RS prop_conj)) thm));
+     else funpow nn (fn thm => unfold_thms lthy @{thms conj_assoc} (thm RS prop_conj)) thm));
 
 fun mk_induct_attrs ctrss =
   let

--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Aug 13 22:29:43 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Aug 14 13:20:54 2014 +0200
@@ -1592,7 +1592,7 @@
     val (dtor_corec_unique_thms, dtor_corec_unique_thm) =
       `split_conj_thm (split_conj_prems n
         (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm)
-        |> Local_Defs.unfold lthy (@{thms o_case_sum comp_id id_comp comp_assoc[symmetric]
+        |> unfold_thms lthy (@{thms o_case_sum comp_id id_comp comp_assoc[symmetric]
            case_sum_o_inj(1)} @ map_id0s_o_id @ sym_map_comps)
         OF replicate n @{thm arg_cong2[of _ _ _ _ case_sum, OF refl]});
 

--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Wed Aug 13 22:29:43 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Aug 14 13:20:54 2014 +0200
@@ -1197,7 +1197,7 @@
     val (ctor_rec_unique_thms, ctor_rec_unique_thm) =
       `split_conj_thm (split_conj_prems n
         (mor_UNIV_thm RS iffD2 RS rec_unique_mor_thm)
-        |> Local_Defs.unfold lthy (@{thms convol_o comp_id id_comp comp_assoc fst_convol} @
+        |> unfold_thms lthy (@{thms convol_o comp_id id_comp comp_assoc fst_convol} @
            map_id0s @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]});
 
     val timer = time (timer "rec definitions & thms");