# HG changeset patch
# User desharna
# Date 1399542764 -7200
# Node ID 69b6369a98fad54033829171b0be64587b4285a5
# Parent  f901a08c5653c05c4ae18195079343f6df63aff0
generate 'map_ident' theorem for BNFs

diff -r f901a08c5653 -r 69b6369a98fa src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Wed May 07 18:09:08 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu May 08 11:52:44 2014 +0200
@@ -61,6 +61,7 @@
   val map_def_of_bnf: bnf -> thm
   val map_id0_of_bnf: bnf -> thm
   val map_id_of_bnf: bnf -> thm
+  val map_ident_of_bnf: bnf -> thm
   val map_transfer_of_bnf: bnf -> thm
   val le_rel_OO_of_bnf: bnf -> thm
   val rel_def_of_bnf: bnf -> thm
@@ -222,6 +223,7 @@
   map_comp: thm lazy,
   map_cong: thm lazy,
   map_id: thm lazy,
+  map_ident: thm lazy,
   map_transfer: thm lazy,
   rel_eq: thm lazy,
   rel_flip: thm lazy,
@@ -235,8 +237,8 @@
 };
 
 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_transfer rel_eq rel_flip set_map rel_cong rel_mono
-    rel_mono_strong rel_Grp rel_conversep rel_OO = {
+    inj_map map_comp map_cong map_id map_ident map_transfer rel_eq rel_flip set_map rel_cong
+    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,
@@ -249,6 +251,7 @@
   map_comp = map_comp,
   map_cong = map_cong,
   map_id = map_id,
+  map_ident = map_ident,
   map_transfer = map_transfer,
   rel_eq = rel_eq,
   rel_flip = rel_flip,
@@ -273,6 +276,7 @@
   map_comp,
   map_cong,
   map_id,
+  map_ident,
   map_transfer,
   rel_eq,
   rel_flip,
@@ -295,6 +299,7 @@
     map_comp = Lazy.map f map_comp,
     map_cong = Lazy.map f map_cong,
     map_id = Lazy.map f map_id,
+    map_ident = Lazy.map f map_ident,
     map_transfer = Lazy.map f map_transfer,
     rel_eq = Lazy.map f rel_eq,
     rel_flip = Lazy.map f rel_flip,
@@ -413,6 +418,7 @@
 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;
+val map_ident_of_bnf = Lazy.force o #map_ident o #facts o rep_bnf;
 val map_comp0_of_bnf = #map_comp0 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;
@@ -581,6 +587,7 @@
 val inj_mapN = "inj_map";
 val map_id0N = "map_id0";
 val map_idN = "map_id";
+val map_identN = "map_ident";
 val map_comp0N = "map_comp0";
 val map_compN = "map_comp";
 val map_cong0N = "map_cong0";
@@ -654,6 +661,7 @@
             (map_cong0N, [#map_cong0 axioms], []),
             (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
             (map_idN, [Lazy.force (#map_id facts)], []),
+            (map_identN, [Lazy.force (#map_ident facts)], []),
             (rel_comppN, [Lazy.force (#rel_OO facts)], []),
             (rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []),
             (rel_conversepN, [Lazy.force (#rel_conversep facts)], []),
@@ -1094,6 +1102,7 @@
         val in_cong = Lazy.lazy mk_in_cong;
 
         val map_id = Lazy.lazy (fn () => mk_map_id (#map_id0 axioms));
+        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 () =
@@ -1310,8 +1319,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 map_comp map_cong map_id map_transfer rel_eq rel_flip set_map
-          rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
+          in_mono in_rel inj_map map_comp map_cong map_id map_ident map_transfer rel_eq rel_flip
+          set_map rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
 
         val wits = map2 mk_witness bnf_wits wit_thms;
 
@@ -1407,7 +1416,7 @@
       [Pretty.str (mk_setN (i + 1) ^ ":"), Pretty.brk 1,
           Pretty.quote (Syntax.pretty_term ctxt (nth sets i))];
 
-    fun pretty_bnf (key, BNF {name, T, map, sets, bd, live, lives, dead, deads, ...}) =
+    fun pretty_bnf (key, BNF {T, map, sets, bd, live, lives, dead, deads, ...}) =
       Pretty.big_list
         (Pretty.string_of (Pretty.block [Pretty.str key, Pretty.str ":", Pretty.brk 1,
           Pretty.quote (Syntax.pretty_typ ctxt T)]))
diff -r f901a08c5653 -r 69b6369a98fa src/HOL/Tools/BNF/bnf_def_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Wed May 07 18:09:08 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Thu May 08 11:52:44 2014 +0200
@@ -12,6 +12,7 @@
   val mk_in_mono_tac: int -> 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
   val mk_map_comp: thm -> thm
   val mk_map_cong_tac: Proof.context -> thm -> tactic
   val mk_set_map: thm -> thm
@@ -43,6 +44,7 @@
 val conversep_shift = @{thm conversep_le_swap} RS iffD1;
 
 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_comp comp = @{thm comp_eq_dest_lhs} OF [mk_sym comp];
 fun mk_map_cong_tac ctxt cong0 =
   (hyp_subst_tac ctxt THEN' rtac cong0 THEN'