# HG changeset patch
# User blanchet
# Date 1346768242 -7200
# Node ID 1bbd7a37fc2955dd18adbc32bedccd1c6c11828b
# Parent  5fc5211cf1041174c4baa6c3f421522e8cca9d21
implemented "mk_inject_tac"

diff -r 5fc5211cf104 -r 1bbd7a37fc29 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 15:51:32 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 16:17:22 2012 +0200
@@ -107,21 +107,22 @@
 
     val eqs = map dest_TFree Bs ~~ sum_prod_TsBs;
 
-    val ((raw_flds, raw_unfs, fld_unfs, unf_flds), lthy') = fp_bnf construct bs eqs lthy;
+    val ((raw_unfs, raw_flds, unf_flds, fld_unfs, fld_injects), lthy') =
+      fp_bnf construct bs eqs lthy;
 
-    fun mk_fld_or_unf get_foldedT Ts t =
+    fun mk_unf_or_fld get_foldedT Ts t =
       let val Type (_, Ts0) = get_foldedT (fastype_of t) in
         Term.subst_atomic_types (Ts0 ~~ Ts) t
       end;
 
-    val mk_fld = mk_fld_or_unf range_type;
-    val mk_unf = mk_fld_or_unf domain_type;
+    val mk_unf = mk_unf_or_fld domain_type;
+    val mk_fld = mk_unf_or_fld range_type;
 
+    val unfs = map (mk_unf As) raw_unfs;
     val flds = map (mk_fld As) raw_flds;
-    val unfs = map (mk_unf As) raw_unfs;
 
-    fun wrap_type ((((((((T, fld), unf), fld_unf), unf_fld), ctr_names), ctr_Tss), disc_names),
-        sel_namess) no_defs_lthy =
+    fun wrap_type (((((((((T, fld), unf), fld_unf), unf_fld), fld_inject), ctr_names), ctr_Tss),
+        disc_names), sel_namess) no_defs_lthy =
       let
         val n = length ctr_names;
         val ks = 1 upto n;
@@ -178,11 +179,15 @@
         fun exhaust_tac {context = ctxt, ...} =
           mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf_thm sumEN_thm';
 
-        (* ### *)
+        val inject_tacss =
+          map2 (fn 0 => K []
+                 | _ => fn ctr_def => [fn {context = ctxt, ...} =>
+                     mk_inject_tac ctxt ctr_def fld_inject])
+            ms ctr_defs;
+
+        (*###*)
         fun cheat_tac {context = ctxt, ...} = Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt);
 
-        val inject_tacss = map (fn 0 => [] | _ => [cheat_tac]) ms;
-
         val half_distinct_tacss = map (map (K cheat_tac)) (mk_half_pairss ks);
 
         val case_tacs = map (K cheat_tac) ks;
@@ -193,8 +198,8 @@
       end;
   in
     lthy'
-    |> fold wrap_type (Ts ~~ flds ~~ unfs ~~ fld_unfs ~~ unf_flds ~~ ctr_namess ~~ ctr_Tsss ~~
-      disc_namess ~~ sel_namesss)
+    |> fold wrap_type (Ts ~~ flds ~~ unfs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ctr_namess ~~
+      ctr_Tsss ~~ disc_namess ~~ sel_namesss)
   end;
 
 fun data_cmd info specs lthy =
diff -r 5fc5211cf104 -r 1bbd7a37fc29 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 04 15:51:32 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 04 16:17:22 2012 +0200
@@ -10,6 +10,7 @@
   val mk_exhaust_tac: Proof.context -> int -> int list -> thm list -> thm -> thm -> tactic
   val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
     -> tactic
+  val mk_inject_tac: Proof.context -> thm -> thm -> tactic
 end;
 
 structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS =
@@ -33,4 +34,10 @@
      SELECT_GOAL (Local_Defs.unfold_tac ctxt [th]) THEN'
      atac) [rev cTs, cTs] [cunf, cfld] [unf_fld, fld_unf])) 1;
 
+fun mk_inject_tac ctxt ctr_def fld_inject =
+  Local_Defs.unfold_tac ctxt [ctr_def] THEN
+  rtac (fld_inject RS ssubst) 1 THEN
+  Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN
+  rtac refl 1;
+
 end;
diff -r 5fc5211cf104 -r 1bbd7a37fc29 src/HOL/Codatatype/Tools/bnf_gfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 15:51:32 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 16:17:22 2012 +0200
@@ -10,7 +10,7 @@
 signature BNF_GFP =
 sig
   val bnf_gfp: binding list -> typ list list -> BNF_Def.BNF list -> local_theory ->
-    (term list * term list * thm list * thm list) * local_theory
+    (term list * term list * thm list * thm list * thm list) * local_theory
 end;
 
 structure BNF_GFP : BNF_GFP =
@@ -2989,7 +2989,7 @@
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
           bs thmss)
   in
-    ((flds, unfs, fld_unf_thms, unf_fld_thms),
+    ((unfs, flds, unf_fld_thms, fld_unf_thms, fld_inject_thms),
       lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;
 
diff -r 5fc5211cf104 -r 1bbd7a37fc29 src/HOL/Codatatype/Tools/bnf_lfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 04 15:51:32 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 04 16:17:22 2012 +0200
@@ -9,7 +9,7 @@
 signature BNF_LFP =
 sig
   val bnf_lfp: binding list -> typ list list -> BNF_Def.BNF list -> local_theory ->
-    (term list * term list * thm list * thm list) * local_theory
+    (term list * term list * thm list * thm list * thm list) * local_theory
 end;
 
 structure BNF_LFP : BNF_LFP =
@@ -1812,7 +1812,7 @@
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
           bs thmss)
   in
-    ((flds, unfs, fld_unf_thms, unf_fld_thms),
+    ((unfs, flds, unf_fld_thms, fld_unf_thms, fld_inject_thms),
       lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;