# HG changeset patch
# User desharna
# Date 1400163344 -7200
# Node ID 8e9ca31e9b8efdb5731f4f43519d90d11f625669
# Parent  299b026cc5af80dd8dc96e4d6c7a6ad81dc2c6f9
generate 'disc_map_iff[simp]' theorem for (co)datatypes

diff -r 299b026cc5af -r 8e9ca31e9b8e src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon May 19 09:35:35 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu May 15 16:15:44 2014 +0200
@@ -98,6 +98,7 @@
 
 val EqN = "Eq_";
 val set_emptyN = "set_empty";
+val disc_map_iffN = "disc_map_iff";
 
 structure Data = Generic_Data
 (
@@ -1176,6 +1177,48 @@
                 end;
 
               val sets = map mk_set (sets_of_bnf fp_bnf);
+
+              val disc_map_iff_thms =
+                let
+                  val (((Ds, As), Bs), names_lthy) = lthy
+                    |> mk_TFrees (dead_of_bnf fp_bnf)
+                    ||>> mk_TFrees (live_of_bnf fp_bnf)
+                    ||>> mk_TFrees (live_of_bnf fp_bnf);
+                  val fTs = map2 (curry op -->) As Bs;
+                  val T1 = mk_T_of_bnf Ds As fp_bnf;
+                  val T2 = mk_T_of_bnf Ds Bs fp_bnf;
+                  val ((fs, t), names_lthy) = names_lthy
+                    |> mk_Frees "f" fTs
+                    ||>> yield_singleton (mk_Frees "a") T1;
+                  val map_term = mk_map_of_bnf Ds As Bs fp_bnf;
+                  fun mk_discs T = map (fn disc =>
+                    subst_nonatomic_types [(domain_type (fastype_of disc), T)] disc);
+                  val discs1 = mk_discs T1 discs;
+                  val discs2 = mk_discs T2 discs;
+                  val discs1_t = map (fn disc1 => Term.betapply (disc1, t)) discs1;
+                  fun mk_goal (disc1_t, disc2) =
+                    let
+                      val (head, tail) = Term.strip_comb disc1_t;
+                      val is_t_eq_t = head aconv HOLogic.eq_const T1 andalso
+                        forall (fn u => u = t) tail;
+                    in
+                      if head aconv @{const Not} orelse is_t_eq_t then NONE
+                      else
+                        SOME (mk_Trueprop_eq
+                          (betapply (disc2, (Term.list_comb (map_term, fs) $ t)), disc1_t))
+                    end;
+                  val goals = map_filter mk_goal (discs1_t ~~ discs2);
+                in
+                  if null goals then []
+                  else
+                    Goal.prove_sorry names_lthy [] [] (Logic.mk_conjunction_balanced goals)
+                      (fn {context = ctxt, prems = _} =>
+                        mk_disc_map_iff_tac ctxt (certify ctxt t) exhaust (flat disc_thmss)
+                          map_thms)
+                      |> Conjunction.elim_balanced (length goals)
+                      |> Proof_Context.export names_lthy lthy
+                end;
+
               val ctr_argT_namess = map ((fn Ts => fold Term.add_tfree_namesT Ts []) o
                 binder_types o fastype_of) ctrs;
               val setTs = map (HOLogic.dest_setT o range_type o fastype_of) sets;
@@ -1238,7 +1281,8 @@
                 |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
 
               val notes =
-                [(mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs),
+                [(disc_map_iffN, disc_map_iff_thms, simp_attrs),
+                 (mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs),
                  (rel_distinctN, rel_distinct_thms, simp_attrs),
                  (rel_injectN, rel_inject_thms, simp_attrs),
                  (setN, set_thms, code_nitpicksimp_attrs @ simp_attrs),
diff -r 299b026cc5af -r 8e9ca31e9b8e src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon May 19 09:35:35 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu May 15 16:15:44 2014 +0200
@@ -18,6 +18,7 @@
   val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
     tactic
   val mk_disc_corec_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
+  val mk_disc_map_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
   val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
   val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic
   val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list ->
@@ -31,6 +32,7 @@
 structure BNF_FP_Def_Sugar_Tactics : BNF_FP_DEF_SUGAR_TACTICS =
 struct
 
+open Ctr_Sugar_Util
 open BNF_Tactics
 open BNF_Util
 open BNF_FP_Util
@@ -113,6 +115,15 @@
       (if is_refl disc then all_tac else HEADGOAL (rtac disc)))
     (map rtac case_splits' @ [K all_tac]) corecs discs);
 
+fun mk_disc_map_iff_tac ctxt ct exhaust discs maps =
+  TRYALL Goal.conjunction_tac THEN
+    ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+      REPEAT_DETERM o hyp_subst_tac ctxt) THEN
+    unfold_thms_tac ctxt maps THEN
+    unfold_thms_tac ctxt (map (fn thm => thm RS @{thm iffD2[OF eq_False]}
+      handle THM _ => thm RS @{thm iffD2[OF eq_True]}) discs) THEN
+    ALLGOALS (rtac refl ORELSE' rtac TrueI);
+
 fun solve_prem_prem_tac ctxt =
   REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
     hyp_subst_tac ctxt ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
@@ -194,10 +205,10 @@
 
 fun mk_set_empty_tac ctxt ct exhaust sets discs =
   TRYALL Goal.conjunction_tac THEN
-  ALLGOALS(rtac (Ctr_Sugar_Util.cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+  ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
     REPEAT_DETERM o hyp_subst_tac ctxt) THEN
   unfold_thms_tac ctxt (sets @ map_filter (fn thm =>
     SOME (thm RS @{thm iffD2[OF eq_False]}) handle THM _ => NONE) discs) THEN
-  ALLGOALS(rtac refl ORELSE' etac FalseE);
+  ALLGOALS (rtac refl ORELSE' etac FalseE);
 
 end;