merged

--- a/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 13:19:04 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 14:19:23 2014 +0200
@@ -913,6 +913,12 @@
 \begin{indentblock}
 \begin{description}
 
+\item[@{text "t."}\hthm{inj_map}\rm:] ~ \\
+@{thm list.inj_map[no_vars]}
+
+\item[@{text "t."}\hthm{inj_map_strong}\rm:] ~ \\
+@{thm list.inj_map_strong[no_vars]}
+
 \item[@{text "t."}\hthm{set_map}\rm:] ~ \\
 @{thm list.set_map[no_vars]}
 

--- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Aug 18 13:19:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Aug 18 14:19:23 2014 +0200
@@ -55,6 +55,7 @@
   val in_mono_of_bnf: bnf -> thm
   val in_rel_of_bnf: bnf -> thm
   val inj_map_of_bnf: bnf -> thm
+  val inj_map_strong_of_bnf: bnf -> thm
   val map_comp0_of_bnf: bnf -> thm
   val map_comp_of_bnf: bnf -> thm
   val map_cong0_of_bnf: bnf -> thm
@@ -73,6 +74,7 @@
   val rel_cong_of_bnf: bnf -> thm
   val rel_conversep_of_bnf: bnf -> thm
   val rel_mono_of_bnf: bnf -> thm
+  val rel_mono_strong0_of_bnf: bnf -> thm
   val rel_mono_strong_of_bnf: bnf -> thm
   val rel_eq_of_bnf: bnf -> thm
   val rel_flip_of_bnf: bnf -> thm
@@ -222,6 +224,7 @@
   in_mono: thm lazy,
   in_rel: thm lazy,
   inj_map: thm lazy,
+  inj_map_strong: thm lazy,
   map_comp: thm lazy,
   map_cong: thm lazy,
   map_id: thm lazy,
@@ -234,6 +237,7 @@
   rel_cong: thm lazy,
   rel_map: thm list lazy,
   rel_mono: thm lazy,
+  rel_mono_strong0: thm lazy,
   rel_mono_strong: thm lazy,
   rel_Grp: thm lazy,
   rel_conversep: thm lazy,
@@ -241,8 +245,9 @@
 };
 
 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_map rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO = {
+    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 = {
   bd_Card_order = bd_Card_order,
   bd_Cinfinite = bd_Cinfinite,
   bd_Cnotzero = bd_Cnotzero,
@@ -252,6 +257,7 @@
   in_mono = in_mono,
   in_rel = in_rel,
   inj_map = inj_map,
+  inj_map_strong = inj_map_strong,
   map_comp = map_comp,
   map_cong = map_cong,
   map_id = map_id,
@@ -264,6 +270,7 @@
   rel_cong = rel_cong,
   rel_map = rel_map,
   rel_mono = rel_mono,
+  rel_mono_strong0 = rel_mono_strong0,
   rel_mono_strong = rel_mono_strong,
   rel_Grp = rel_Grp,
   rel_conversep = rel_conversep,
@@ -279,6 +286,7 @@
   in_mono,
   in_rel,
   inj_map,
+  inj_map_strong,
   map_comp,
   map_cong,
   map_id,
@@ -291,6 +299,7 @@
   rel_cong,
   rel_map,
   rel_mono,
+  rel_mono_strong0,
   rel_mono_strong,
   rel_Grp,
   rel_conversep,
@@ -304,6 +313,7 @@
     in_mono = Lazy.map f in_mono,
     in_rel = Lazy.map f in_rel,
     inj_map = Lazy.map f inj_map,
+    inj_map_strong = Lazy.map f inj_map_strong,
     map_comp = Lazy.map f map_comp,
     map_cong = Lazy.map f map_cong,
     map_id = Lazy.map f map_id,
@@ -316,6 +326,7 @@
     rel_cong = Lazy.map f rel_cong,
     rel_map = Lazy.map (map f) rel_map,
     rel_mono = Lazy.map f rel_mono,
+    rel_mono_strong0 = Lazy.map f rel_mono_strong0,
     rel_mono_strong = Lazy.map f rel_mono_strong,
     rel_Grp = Lazy.map f rel_Grp,
     rel_conversep = Lazy.map f rel_conversep,
@@ -425,6 +436,7 @@
 val in_mono_of_bnf = Lazy.force o #in_mono o #facts o rep_bnf;
 val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf;
 val inj_map_of_bnf = Lazy.force o #inj_map o #facts o rep_bnf;
+val inj_map_strong_of_bnf = Lazy.force o #inj_map_strong o #facts o rep_bnf;
 val map_def_of_bnf = #map_def o #defs o rep_bnf;
 val map_id0_of_bnf = #map_id0 o #axioms o rep_bnf;
 val map_id_of_bnf = Lazy.force o #map_id o #facts o rep_bnf;
@@ -445,6 +457,7 @@
 val set_map_of_bnf = map Lazy.force o #set_map o #facts o rep_bnf;
 val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf;
 val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf;
+val rel_mono_strong0_of_bnf = Lazy.force o #rel_mono_strong0 o #facts o rep_bnf;
 val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf;
 val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
 val rel_conversep_of_bnf = Lazy.force o #rel_conversep o #facts o rep_bnf;
@@ -598,6 +611,7 @@
 val in_monoN = "in_mono";
 val in_relN = "in_rel";
 val inj_mapN = "inj_map";
+val inj_map_strongN = "inj_map_strong";
 val map_id0N = "map_id0";
 val map_idN = "map_id";
 val map_identN = "map_ident";
@@ -615,6 +629,7 @@
 val rel_conversepN = "rel_conversep";
 val rel_mapN = "rel_map"
 val rel_monoN = "rel_mono"
+val rel_mono_strong0N = "rel_mono_strong0"
 val rel_mono_strongN = "rel_mono_strong"
 val rel_comppN = "rel_compp";
 val rel_compp_GrpN = "rel_compp_Grp";
@@ -652,9 +667,9 @@
            (in_bdN, [Lazy.force (#in_bd facts)]),
            (in_monoN, [Lazy.force (#in_mono facts)]),
            (in_relN, [Lazy.force (#in_rel facts)]),
-           (inj_mapN, [Lazy.force (#inj_map facts)]),
            (map_comp0N, [#map_comp0 axioms]),
            (map_transferN, [Lazy.force (#map_transfer facts)]),
+           (rel_mono_strong0N, [Lazy.force (#rel_mono_strong0 facts)]),
            (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
            (set_map0N, #set_map0 axioms),
            (set_bdN, #set_bd axioms)] @
@@ -669,7 +684,9 @@
     fun note_unless_dont_note (noted0, lthy0) =
       let
         val notes =
-          [(map_compN, [Lazy.force (#map_comp facts)], []),
+          [(inj_mapN, [Lazy.force (#inj_map facts)], []),
+           (inj_map_strongN, [Lazy.force (#inj_map_strong facts)], []),
+           (map_compN, [Lazy.force (#map_comp facts)], []),
            (map_cong0N, [#map_cong0 axioms], []),
            (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
            (map_idN, [Lazy.force (#map_id facts)], []),
@@ -948,16 +965,19 @@
     fun mk_bnf_rel RTs CA CB = normalize_rel lthy RTs CA CB bnf_rel;
 
     val pre_names_lthy = lthy;
-    val ((((((((((((((((((fs, gs), hs), is), x), y), zs), ys), As),
+    val (((((((((((((((((((((fs, fs'), gs), hs), is), x), x'), y), zs), 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 "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 "x") CA'
       ||>> yield_singleton (mk_Frees "y") CB'
       ||>> mk_Frees "z" As'
+      ||>> mk_Frees "z" As'
       ||>> mk_Frees "y" Bs'
       ||>> mk_Frees "A" (map HOLogic.mk_setT As')
       ||>> mk_Frees "A" (map HOLogic.mk_setT As')
@@ -1299,7 +1319,7 @@
 
         val rel_flip = Lazy.lazy mk_rel_flip;
 
-        fun mk_rel_mono_strong () =
+        fun mk_rel_mono_strong0 () =
           let
             fun mk_prem setA setB R S a b =
               HOLogic.mk_Trueprop
@@ -1312,11 +1332,15 @@
           in
             Goal.prove_sorry lthy [] []
               (fold_rev Logic.all (x :: y :: Rs @ Rs_copy) (Logic.list_implies (prems, concl)))
-              (fn {context = ctxt, prems = _} => mk_rel_mono_strong_tac ctxt (Lazy.force in_rel)
+              (fn {context = ctxt, prems = _} => mk_rel_mono_strong0_tac ctxt (Lazy.force in_rel)
                 (map Lazy.force set_map))
             |> Thm.close_derivation
           end;
 
+        val rel_mono_strong0 = Lazy.lazy mk_rel_mono_strong0;
+
+        fun mk_rel_mono_strong () = Object_Logic.rulify lthy (Lazy.force rel_mono_strong0)
+
         val rel_mono_strong = Lazy.lazy mk_rel_mono_strong;
 
         fun mk_rel_map () =
@@ -1334,12 +1358,13 @@
                  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)
+            goals
+            |> map (fn goal => Goal.prove_sorry lthy [] [] goal
               (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})
+                  (Lazy.force rel_Grp) (Lazy.force map_id)))
+            |> map (unfold_thms lthy @{thms vimage2p_def[of id, unfolded id_apply]
+                 vimage2p_def[of _ id, unfolded id_apply]})
             |> map Thm.close_derivation
           end;
 
@@ -1364,11 +1389,36 @@
 
         val map_transfer = Lazy.lazy mk_map_transfer;
 
+        fun mk_inj_map_strong () =
+          let
+            val assms = map5 (fn setA => fn z => fn f => fn z' => fn f' =>
+              fold_rev Logic.all [z, z']
+                (Logic.mk_implies (mk_Trueprop_mem (z, setA $ x),
+                   Logic.mk_implies (mk_Trueprop_mem (z', setA $ x'),
+                     Logic.mk_implies (mk_Trueprop_eq (f $ z, f' $ z'),
+                       mk_Trueprop_eq (z, z')))))) bnf_sets_As zs fs zs' fs';
+            val concl = Logic.mk_implies
+              (mk_Trueprop_eq
+                 (Term.list_comb (bnf_map_AsBs, fs) $ x,
+                  Term.list_comb (bnf_map_AsBs, fs') $ x'),
+               mk_Trueprop_eq (x, x'));
+            val goal = fold_rev Logic.all (x :: x' :: fs @ fs')
+              (fold_rev (curry Logic.mk_implies) assms concl);
+          in
+            Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+              mk_inj_map_strong_tac ctxt (Lazy.force rel_eq) (Lazy.force rel_map)
+                (Lazy.force rel_mono_strong))
+            |> Thm.close_derivation
+          end;
+
+        val inj_map_strong = Lazy.lazy mk_inj_map_strong;
+
         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 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_strong rel_Grp rel_conversep rel_OO;
+          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;
 
         val wits = map2 mk_witness bnf_wits wit_thms;
 

--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Mon Aug 18 13:19:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Mon Aug 18 14:19:23 2014 +0200
@@ -11,6 +11,7 @@
 sig
   val mk_collect_set_map_tac: thm list -> tactic
   val mk_in_mono_tac: int -> tactic
+  val mk_inj_map_strong_tac: Proof.context -> thm -> thm list -> thm -> tactic
   val mk_inj_map_tac: int -> thm -> thm -> thm -> thm -> tactic
   val mk_map_id: thm -> thm
   val mk_map_ident: Proof.context -> thm -> thm
@@ -25,7 +26,7 @@
   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
+  val mk_rel_mono_strong0_tac: Proof.context -> thm -> thm list -> tactic
 
   val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic
 
@@ -70,6 +71,17 @@
         REPEAT_DETERM_N n o atac))
   end;
 
+fun mk_inj_map_strong_tac ctxt rel_eq rel_maps rel_mono_strong =
+  let
+    val rel_eq' = rel_eq RS @{thm predicate2_eqD};
+    val rel_maps' = map (fn thm => thm RS iffD1) rel_maps;
+  in
+    HEADGOAL (dtac (rel_eq' RS iffD2) THEN' rtac (rel_eq' RS iffD1)) THEN
+    EVERY (map (HEADGOAL o dtac) rel_maps') THEN
+    HEADGOAL (etac rel_mono_strong) THEN
+    TRYALL (Goal.assume_rule_tac ctxt)
+  end;
+
 fun mk_collect_set_map_tac set_map0s =
   (rtac (@{thm collect_comp} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN'
   EVERY' (map (fn set_map0 =>
@@ -197,7 +209,7 @@
         REPEAT_DETERM_N n o rtac @{thm fst_fstOp},
         in_tac @{thm fstOp_in},
         rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0,
-        REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, 
+        REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply,
           rtac ballE, rtac subst,
           rtac @{thm csquare_def}, rtac @{thm csquare_fstOp_sndOp}, atac, etac notE,
           etac set_mp, atac],
@@ -211,7 +223,7 @@
         in_tac @{thm sndOp_in}] 1
   end;
 
-fun mk_rel_mono_strong_tac ctxt in_rel set_maps =
+fun mk_rel_mono_strong0_tac ctxt in_rel set_maps =
   if null set_maps then atac 1
   else
     unfold_tac ctxt [in_rel] THEN
@@ -252,10 +264,10 @@
     let
       val bd'_Cinfinite = bd_Cinfinite RS @{thm Cinfinite_csum1};
       val inserts =
-        map (fn set_bd => 
+        map (fn set_bd =>
           iffD2 OF [@{thm card_of_ordLeq}, @{thm ordLeq_ordIso_trans} OF
             [set_bd, bd_Card_order RS @{thm card_of_Field_ordIso} RS @{thm ordIso_symmetric}]])
-        set_bds;        
+        set_bds;
     in
       EVERY' [rtac (Drule.rotate_prems 1 ctrans), rtac @{thm cprod_cinfinite_bound},
         rtac (ctrans OF @{thms ordLeq_csum2 ordLeq_cexp2}), rtac @{thm card_of_Card_order},

--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Aug 18 13:19:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Aug 18 14:19:23 2014 +0200
@@ -167,7 +167,7 @@
     val map_id0s = map map_id0_of_bnf bnfs;
     val map_ids = map map_id_of_bnf bnfs;
     val set_mapss = map set_map_of_bnf bnfs;
-    val rel_mono_strongs = map rel_mono_strong_of_bnf bnfs;
+    val rel_mono_strong0s = map rel_mono_strong0_of_bnf bnfs;
     val le_rel_OOs = map le_rel_OO_of_bnf bnfs;
 
     val timer = time (timer "Extracted terms & thms");
@@ -1691,7 +1691,7 @@
           in
             Goal.prove_sorry lthy [] [] goal
               (fn {context = ctxt, prems = _} => mk_le_rel_OO_tac ctxt m induct ctor_nchotomy_thms
-                ctor_Irel_thms rel_mono_strongs le_rel_OOs)
+                ctor_Irel_thms rel_mono_strong0s le_rel_OOs)
             |> Thm.close_derivation
             |> singleton (Proof_Context.export names_lthy lthy)
           end;
@@ -1762,7 +1762,7 @@
     val Irel_induct_thm =
       mk_rel_xtor_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's
         (fn {context = ctxt, prems = IHs} => mk_rel_induct_tac ctxt IHs m ctor_induct2_thm ks
-           ctor_Irel_thms rel_mono_strongs) lthy;
+           ctor_Irel_thms rel_mono_strong0s) lthy;
 
     val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
     val ctor_fold_transfer_thms =

--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Mon Aug 18 13:19:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Mon Aug 18 14:19:23 2014 +0200
@@ -582,7 +582,7 @@
     (induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1
   end;
 
-fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strongs le_rel_OOs =
+fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs =
   EVERY' (rtac induct ::
   map4 (fn nchotomy => fn Irel => fn rel_mono => fn le_rel_OO =>
     EVERY' [rtac impI, etac (nchotomy RS @{thm nchotomy_relcomppE}),
@@ -592,7 +592,7 @@
       REPEAT_DETERM_N m o EVERY' [rtac ballI, rtac ballI, rtac impI, atac],
       REPEAT_DETERM_N (length le_rel_OOs) o
         EVERY' [rtac ballI, rtac ballI, Goal.assume_rule_tac ctxt]])
-  ctor_nchotomys ctor_Irels rel_mono_strongs le_rel_OOs) 1;
+  ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs) 1;
 
 (* BNF tactics *)
 
@@ -701,19 +701,19 @@
     EVERY' [rtac iffI, if_tac, only_if_tac] 1
   end;
 
-fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strongs =
+fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strong0s =
   let val n = length ks;
   in
     unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
     EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2,
-      EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong =>
+      EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong0 =>
         EVERY' [rtac impI, dtac (ctor_rel RS iffD1), rtac (IH RS @{thm spec2} RS mp),
-          etac rel_mono_strong,
+          etac rel_mono_strong0,
           REPEAT_DETERM_N m o rtac @{thm ballI[OF ballI[OF imp_refl]]},
           EVERY' (map (fn j =>
             EVERY' [select_prem_tac n (dtac asm_rl) j, rtac @{thm ballI[OF ballI]},
               Goal.assume_rule_tac ctxt]) ks)])
-      IHs ctor_rels rel_mono_strongs)] 1
+      IHs ctor_rels rel_mono_strong0s)] 1
   end;
 
 fun mk_fold_transfer_tac ctxt m ctor_rel_induct map_transfers folds =