# HG changeset patch
# User blanchet
# Date 1366810920 -7200
# Node ID 219a3063ed29281213098540ff4e5fc5365b2980
# Parent  4c9f08836d878ea75027f36b07fc85e8cf7d5da0
derive "map_cong"

diff -r 4c9f08836d87 -r 219a3063ed29 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Wed Apr 24 14:15:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed Apr 24 15:42:00 2013 +0200
@@ -53,6 +53,7 @@
   val map_comp'_of_bnf: BNF -> thm
   val map_comp_of_bnf: BNF -> thm
   val map_cong0_of_bnf: BNF -> thm
+  val map_cong_of_bnf: BNF -> thm
   val map_def_of_bnf: BNF -> thm
   val map_id'_of_bnf: BNF -> thm
   val map_id_of_bnf: BNF -> thm
@@ -184,6 +185,7 @@
   in_mono: thm lazy,
   in_srel: thm lazy,
   map_comp': thm lazy,
+  map_cong: thm lazy,
   map_id': thm lazy,
   map_wppull: thm lazy,
   rel_eq: thm lazy,
@@ -199,7 +201,7 @@
 };
 
 fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong in_mono in_srel
-    map_comp' map_id' map_wppull rel_eq rel_flip rel_srel set_natural' srel_cong srel_mono
+    map_comp' map_cong map_id' map_wppull rel_eq rel_flip rel_srel set_natural' srel_cong srel_mono
     srel_Id srel_Gr srel_converse srel_O = {
   bd_Card_order = bd_Card_order,
   bd_Cinfinite = bd_Cinfinite,
@@ -209,6 +211,7 @@
   in_mono = in_mono,
   in_srel = in_srel,
   map_comp' = map_comp',
+  map_cong = map_cong,
   map_id' = map_id',
   map_wppull = map_wppull,
   rel_eq = rel_eq,
@@ -231,6 +234,7 @@
   in_mono,
   in_srel,
   map_comp',
+  map_cong,
   map_id',
   map_wppull,
   rel_eq,
@@ -251,6 +255,7 @@
     in_mono = Lazy.map f in_mono,
     in_srel = Lazy.map f in_srel,
     map_comp' = Lazy.map f map_comp',
+    map_cong = Lazy.map f map_cong,
     map_id' = Lazy.map f map_id',
     map_wppull = Lazy.map f map_wppull,
     rel_eq = Lazy.map f rel_eq,
@@ -372,6 +377,7 @@
 val map_comp_of_bnf = #map_comp o #axioms o rep_bnf;
 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_wppull_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf;
 val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf;
 val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
@@ -508,6 +514,7 @@
 val map_compN = "map_comp";
 val map_comp'N = "map_comp'";
 val map_cong0N = "map_cong0";
+val map_congN = "map_cong";
 val map_wpullN = "map_wpull";
 val rel_eqN = "rel_eq";
 val rel_flipN = "rel_flip";
@@ -699,11 +706,10 @@
     val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits;
 
     val pre_names_lthy = lthy;
-    val (((((((((((((((((((((((((fs, fs_copy), gs), hs), p), (x, x')), (y, y')), (z, z')), zs), As),
+    val ((((((((((((((((((((((((fs, gs), hs), p), (x, x')), (y, y')), (z, z')), zs), As),
       As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), (Rs, Rs')), Rs_copy), Ss),
       (Qs, Qs')), 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)
       ||>> yield_singleton (mk_Frees "p") CA'CB'
@@ -728,6 +734,9 @@
       ||>> mk_Frees "s" setRTsBsCs
       ||>> mk_Frees' "P" QTs;
 
+    val fs_copy = map2 (retype_free o fastype_of) fs gs;
+    val x_copy = retype_free CA' y;
+
     (*Gr (in R1 .. Rn) (map fst .. fst)^-1 O Gr (in R1 .. Rn) (map snd .. snd)*)
     val O_Gr =
       let
@@ -797,35 +806,31 @@
           (map (dest_Free o fst o Logic.dest_equals o prop_of) defs);
 
     val map_id_goal =
-      let
-        val bnf_map_app_id = Term.list_comb (bnf_map_AsAs, map HOLogic.id_const As');
-      in
-        HOLogic.mk_Trueprop
-          (HOLogic.mk_eq (bnf_map_app_id, HOLogic.id_const CA'))
+      let val bnf_map_app_id = Term.list_comb (bnf_map_AsAs, map HOLogic.id_const As') in
+        mk_Trueprop_eq (bnf_map_app_id, HOLogic.id_const CA')
       end;
 
     val map_comp_goal =
       let
         val bnf_map_app_comp = Term.list_comb (bnf_map_AsCs, map2 (curry HOLogic.mk_comp) gs fs);
         val comp_bnf_map_app = HOLogic.mk_comp
-          (Term.list_comb (bnf_map_BsCs, gs),
-           Term.list_comb (bnf_map_AsBs, fs));
+          (Term.list_comb (bnf_map_BsCs, gs), Term.list_comb (bnf_map_AsBs, fs));
       in
         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
+        (HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set $ x)),
+        mk_Trueprop_eq (f $ z, f_copy $ z)));
+
     val map_cong0_goal =
       let
-        fun mk_prem z set f f_copy =
-          Logic.all z (Logic.mk_implies
-            (HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set $ x)),
-            mk_Trueprop_eq (f $ z, f_copy $ z)));
-        val prems = map4 mk_prem zs bnf_sets_As fs fs_copy;
-        val eq = HOLogic.mk_eq (Term.list_comb (bnf_map_AsBs, fs) $ x,
+        val prems = map4 (mk_map_cong_prem 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
-        fold_rev Logic.all (x :: fs @ fs_copy)
-          (Logic.list_implies (prems, HOLogic.mk_Trueprop eq))
+        fold_rev Logic.all (x :: fs @ fs_copy) (Logic.list_implies (prems, eq))
       end;
 
     val set_naturals_goal =
@@ -955,11 +960,11 @@
 
         fun mk_in_cong () =
           let
-            val prems_cong = map2 (HOLogic.mk_Trueprop oo curry HOLogic.mk_eq) As As_copy;
+            val prems_cong = map2 (curry mk_Trueprop_eq) As As_copy;
             val in_cong_goal =
               fold_rev Logic.all (As @ As_copy)
-                (Logic.list_implies (prems_cong, HOLogic.mk_Trueprop
-                  (HOLogic.mk_eq (mk_in As bnf_sets_As CA', mk_in As_copy bnf_sets_As CA'))));
+                (Logic.list_implies (prems_cong,
+                  mk_Trueprop_eq (mk_in As bnf_sets_As CA', mk_in As_copy bnf_sets_As CA')));
           in
             Goal.prove_sorry lthy [] [] in_cong_goal (K ((TRY o hyp_subst_tac THEN' rtac refl) 1))
             |> Thm.close_derivation
@@ -967,8 +972,23 @@
 
         val in_cong = Lazy.lazy mk_in_cong;
 
-        val map_id' = Lazy.lazy (fn () => mk_id' (#map_id axioms));
-        val map_comp' = Lazy.lazy (fn () => mk_comp' (#map_comp axioms));
+        val map_id' = Lazy.lazy (fn () => mk_map_id' (#map_id axioms));
+        val map_comp' = Lazy.lazy (fn () => mk_map_comp' (#map_comp axioms));
+
+        fun mk_map_cong () =
+          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 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 (#map_cong0 axioms))
+            |> Thm.close_derivation
+          end;
+
+        val map_cong = Lazy.lazy mk_map_cong;
 
         val set_natural' =
           map (fn thm => Lazy.lazy (fn () => mk_set_natural' thm)) (#set_natural axioms);
@@ -1009,9 +1029,9 @@
             |> Thm.close_derivation
           end;
 
-        val srel_O_Grs = no_refl [#srel_O_Gr axioms];
+        val map_wppull = Lazy.lazy mk_map_wppull;
 
-        val map_wppull = Lazy.lazy mk_map_wppull;
+        val srel_O_Grs = no_refl [#srel_O_Gr axioms];
 
         fun mk_srel_Gr () =
           let
@@ -1059,8 +1079,7 @@
         fun mk_srel_Id () =
           let val srelAsAs = mk_bnf_srel self_setRTs CA' CA' in
             Goal.prove_sorry lthy [] []
-              (HOLogic.mk_Trueprop
-                (HOLogic.mk_eq (Term.list_comb (srelAsAs, map Id_const As'), Id_const CA')))
+              (mk_Trueprop_eq (Term.list_comb (srelAsAs, map Id_const As'), Id_const CA'))
               (mk_srel_Id_tac live (Lazy.force srel_Gr) (#map_id axioms))
             |> Thm.close_derivation
           end;
@@ -1156,8 +1175,8 @@
         val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def bnf_srel_def;
 
         val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong
-          in_mono in_srel map_comp' map_id' map_wppull rel_eq rel_flip rel_srel set_natural'
-          srel_cong srel_mono srel_Id srel_Gr srel_converse srel_O;
+          in_mono in_srel map_comp' map_cong map_id' map_wppull rel_eq rel_flip rel_srel
+          set_natural' srel_cong srel_mono srel_Id srel_Gr srel_converse srel_O;
 
         val wits = map2 mk_witness bnf_wits wit_thms;
 
@@ -1202,6 +1221,7 @@
                   val notes =
                     [(map_comp'N, [Lazy.force (#map_comp' facts)]),
                     (map_cong0N, [#map_cong0 axioms]),
+                    (map_congN, [Lazy.force (#map_cong facts)]),
                     (map_id'N, [Lazy.force (#map_id' facts)]),
                     (rel_eqN, [Lazy.force (#rel_eq facts)]),
                     (rel_flipN, [Lazy.force (#rel_flip facts)]),
diff -r 4c9f08836d87 -r 219a3063ed29 src/HOL/BNF/Tools/bnf_def_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Wed Apr 24 14:15:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Wed Apr 24 15:42:00 2013 +0200
@@ -9,8 +9,9 @@
 signature BNF_DEF_TACTICS =
 sig
   val mk_collect_set_natural_tac: thm list -> tactic
-  val mk_id': thm -> thm
-  val mk_comp': thm -> thm
+  val mk_map_id': thm -> thm
+  val mk_map_comp': thm -> thm
+  val mk_map_cong_tac: thm -> tactic
   val mk_in_mono_tac: int -> tactic
   val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
   val mk_set_natural': thm -> thm
@@ -33,8 +34,11 @@
 open BNF_Util
 open BNF_Tactics
 
-fun mk_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply};
-fun mk_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
+fun mk_map_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply};
+fun mk_map_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
+fun mk_map_cong_tac cong0 =
+  (hyp_subst_tac THEN' rtac cong0 THEN'
+   REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1;
 fun mk_set_natural' set_natural = set_natural RS @{thm pointfreeE};
 fun mk_in_mono_tac n = if n = 0 then rtac subset_UNIV 1
   else (rtac subsetI THEN'
diff -r 4c9f08836d87 -r 219a3063ed29 src/HOL/BNF/Tools/bnf_fp.ML
--- a/src/HOL/BNF/Tools/bnf_fp.ML	Wed Apr 24 14:15:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML	Wed Apr 24 15:42:00 2013 +0200
@@ -107,8 +107,6 @@
   val split_conj_thm: thm -> thm list
   val split_conj_prems: int -> thm -> thm
 
-  val retype_free: typ -> term -> term
-
   val mk_sumTN: typ list -> typ
   val mk_sumTN_balanced: typ list -> typ
 
@@ -264,8 +262,6 @@
 
 val mk_common_name = space_implode "_";
 
-fun retype_free T (Free (s, _)) = Free (s, T);
-
 fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T');
 
 fun dest_sumTN 1 T = [T]
diff -r 4c9f08836d87 -r 219a3063ed29 src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Wed Apr 24 14:15:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Wed Apr 24 15:42:00 2013 +0200
@@ -62,6 +62,7 @@
     (term list * (string * typ) list) * Proof.context
   val mk_Freess': string -> typ list list -> Proof.context ->
     (term list list * (string * typ) list list) * Proof.context
+  val retype_free: typ -> term -> term
   val nonzero_string_of_int: int -> string
 
   val strip_typeN: int -> typ -> typ list * typ
@@ -347,6 +348,8 @@
 fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts));
 fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
 
+fun retype_free T (Free (s, _)) = Free (s, T);
+
 
 (** Types **)