# HG changeset patch
# User desharna
# Date 1646993978 -3600
# Node ID 686a6d7d09915fa34e83cb81d5148aeb573e8a9d
# Parent  cdb9c7d41a419ac5ec3b6f1d107fcc38b0f8c925
generated lemma map_ident_strong for BNFs

diff -r cdb9c7d41a41 -r 686a6d7d0991 NEWS
--- a/NEWS	Fri Mar 11 09:23:05 2022 +0100
+++ b/NEWS	Fri Mar 11 11:19:38 2022 +0100
@@ -79,6 +79,8 @@
 * Meson
   - Added support for polymorphic "using" facts. Minor INCOMPATIBILITY.
 
+* (Co)datatype package:
+  - Lemma map_ident_strong is now generated for all BNFs.
 
 
 *** System ***
diff -r cdb9c7d41a41 -r 686a6d7d0991 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Mar 11 09:23:05 2022 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Mar 11 11:19:38 2022 +0100
@@ -982,6 +982,9 @@
 \item[\<open>t.\<close>\hthm{map_ident}\rm:] ~ \\
 @{thm list.map_ident[no_vars]}
 
+\item[\<open>t.\<close>\hthm{map_ident_strong}\rm:] ~ \\
+@{thm list.map_ident_strong[no_vars]}
+
 \item[\<open>t.\<close>\hthm{map_transfer} \<open>[transfer_rule]\<close>\rm:] ~ \\
 @{thm list.map_transfer[no_vars]} \\
 The \<open>[transfer_rule]\<close> attribute is set by the \<open>transfer\<close> plugin
diff -r cdb9c7d41a41 -r 686a6d7d0991 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Fri Mar 11 09:23:05 2022 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Mar 11 11:19:38 2022 +0100
@@ -275,6 +275,7 @@
   map_id: thm lazy,
   map_ident0: thm lazy,
   map_ident: thm lazy,
+  map_ident_strong: thm lazy,
   map_transfer: thm lazy,
   rel_eq: thm lazy,
   rel_flip: thm lazy,
@@ -311,8 +312,8 @@
 
 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_cong_simp map_cong_pred map_id map_ident0 map_ident
-    map_transfer rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp rel_map rel_mono
-    rel_mono_strong0 rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO rel_refl
+    map_ident_strong map_transfer rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp rel_map
+    rel_mono rel_mono_strong0 rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO rel_refl
     rel_refl_strong rel_reflp rel_symp rel_transp rel_transfer rel_eq_onp pred_transfer pred_True
     pred_map pred_rel pred_mono_strong0 pred_mono_strong pred_mono pred_cong0 pred_cong
     pred_cong_simp = {
@@ -333,6 +334,7 @@
   map_id = map_id,
   map_ident0 = map_ident0,
   map_ident = map_ident,
+  map_ident_strong = map_ident_strong,
   map_transfer = map_transfer,
   rel_eq = rel_eq,
   rel_flip = rel_flip,
@@ -384,6 +386,7 @@
   map_id,
   map_ident0,
   map_ident,
+  map_ident_strong,
   map_transfer,
   rel_eq,
   rel_flip,
@@ -433,6 +436,7 @@
     map_id = Lazy.map f map_id,
     map_ident0 = Lazy.map f map_ident0,
     map_ident = Lazy.map f map_ident,
+    map_ident_strong = Lazy.map f map_ident_strong,
     map_transfer = Lazy.map f map_transfer,
     rel_eq = Lazy.map f rel_eq,
     rel_flip = Lazy.map f rel_flip,
@@ -591,6 +595,7 @@
 val map_id_of_bnf = Lazy.force o #map_id o #facts o rep_bnf;
 val map_ident0_of_bnf = Lazy.force o #map_ident0 o #facts o rep_bnf;
 val map_ident_of_bnf = Lazy.force o #map_ident o #facts o rep_bnf;
+val map_ident_strong_of_bnf = Lazy.force o #map_ident_strong o #facts o rep_bnf;
 val map_transfer_of_bnf = Lazy.force o #map_transfer o #facts o rep_bnf;
 val rel_eq_onp_of_bnf = Lazy.force o #rel_eq_onp o #facts o rep_bnf;
 val pred_def_of_bnf = #pred_def o #defs o rep_bnf;
@@ -845,6 +850,7 @@
 val map_id0N = "map_id0";
 val map_idN = "map_id";
 val map_identN = "map_ident";
+val map_ident_strongN = "map_ident_strong";
 val map_transferN = "map_transfer";
 val pred_mono_strong0N = "pred_mono_strong0";
 val pred_mono_strongN = "pred_mono_strong";
@@ -940,6 +946,7 @@
            (map_id0N, [#map_id0 axioms], []),
            (map_transferN, [Lazy.force (#map_transfer facts)], []),
            (map_identN, [Lazy.force (#map_ident facts)], []),
+           (map_ident_strongN, [Lazy.force (#map_ident_strong facts)], []),
            (pred_monoN, [Lazy.force (#pred_mono facts)], mono_attrs),
            (pred_mono_strongN, [Lazy.force (#pred_mono_strong facts)], []),
            (pred_congN, [Lazy.force (#pred_cong facts)], fundefcong_attrs),
@@ -1486,6 +1493,8 @@
         val map_id = Lazy.lazy (fn () => mk_map_id (#map_id0 axioms));
         val map_ident0 = Lazy.lazy (fn () => mk_map_ident lthy (#map_id0 axioms));
         val map_ident = Lazy.lazy (fn () => mk_map_ident lthy (Lazy.force map_id));
+        val map_ident_strong = Lazy.lazy (fn () =>
+          mk_map_ident_strong lthy (#map_cong0 axioms) (Lazy.force map_id));
         val map_comp = Lazy.lazy (fn () => mk_map_comp (#map_comp0 axioms));
 
         fun mk_map_cong mk_implies () =
@@ -2019,11 +2028,11 @@
 
         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_cong_simp map_cong_pred map_id
-          map_ident0 map_ident map_transfer rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp
-          rel_map rel_mono rel_mono_strong0 rel_mono_strong set_transfer rel_Grp rel_conversep
-          rel_OO rel_refl rel_refl_strong rel_reflp rel_symp rel_transp rel_transfer rel_eq_onp
-          pred_transfer pred_True pred_map pred_rel pred_mono_strong0 pred_mono_strong pred_mono
-          pred_cong0 pred_cong pred_cong_simp;
+          map_ident0 map_ident map_ident_strong map_transfer rel_eq rel_flip set_map rel_cong0
+          rel_cong rel_cong_simp rel_map rel_mono rel_mono_strong0 rel_mono_strong set_transfer
+          rel_Grp rel_conversep rel_OO rel_refl rel_refl_strong rel_reflp rel_symp rel_transp
+          rel_transfer rel_eq_onp pred_transfer pred_True pred_map pred_rel pred_mono_strong0
+          pred_mono_strong pred_mono pred_cong0 pred_cong pred_cong_simp;
 
         val wits = map2 mk_witness bnf_wits wit_thms;
 
diff -r cdb9c7d41a41 -r 686a6d7d0991 src/HOL/Tools/BNF/bnf_def_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Fri Mar 11 09:23:05 2022 +0100
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Fri Mar 11 11:19:38 2022 +0100
@@ -16,6 +16,7 @@
   val mk_inj_map_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic
   val mk_map_id: thm -> thm
   val mk_map_ident: Proof.context -> thm -> thm
+  val mk_map_ident_strong: Proof.context -> thm -> thm -> thm
   val mk_map_comp: thm -> thm
   val mk_map_cong_tac: Proof.context -> thm -> tactic
   val mk_set_map: thm -> thm
@@ -56,6 +57,9 @@
 
 fun mk_map_id id = mk_trans (fun_cong OF [id]) @{thm id_apply};
 fun mk_map_ident ctxt = unfold_thms ctxt @{thms id_def};
+fun mk_map_ident_strong ctxt map_cong0 map_id =
+  (trans OF [map_cong0, map_id])
+  |> unfold_thms ctxt @{thms id_apply}
 fun mk_map_comp comp = @{thm comp_eq_dest_lhs} OF [mk_sym comp];
 fun mk_map_cong_tac ctxt cong0 =
   (hyp_subst_tac ctxt THEN' rtac ctxt cong0 THEN'