merge

--- a/src/Doc/Datatypes/Datatypes.thy	Wed Jun 11 14:24:23 2014 +1000
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Jul 03 11:31:25 2014 +0200
@@ -877,6 +877,10 @@
 @{thm list.rel_inject(1)[no_vars]} \\
 @{thm list.rel_inject(2)[no_vars]}
 
+\item[@{text "t."}\hthm{rel\_intros}\rm:] ~ \\
+@{thm list.rel_intros(1)[no_vars]} \\
+@{thm list.rel_intros(2)[no_vars]}
+
 \item[@{text "t."}\hthm{rel\_distinct} @{text "[simp]"}\rm:] ~ \\
 @{thm list.rel_distinct(1)[no_vars]} \\
 @{thm list.rel_distinct(2)[no_vars]}

--- a/src/HOL/BNF_LFP.thy	Wed Jun 11 14:24:23 2014 +1000
+++ b/src/HOL/BNF_LFP.thy	Thu Jul 03 11:31:25 2014 +0200
@@ -195,5 +195,4 @@
 
 hide_fact (open) id_transfer
 
-
 end

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Jun 11 14:24:23 2014 +1000
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 03 11:31:25 2014 +0200
@@ -1503,6 +1503,15 @@
               fun mk_rel_inject_thm ((ctr_def', cxIn), (_, cyIn)) =
                 mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] cxIn cyIn;
 
+              fun mk_rel_intro_thm thm =
+                let
+                  fun impl thm = rotate_prems (~1) (impl (rotate_prems 1 (conjI RS thm)))
+                    handle THM _ => thm
+                in
+                  impl (thm RS iffD2)
+                  handle THM _ => thm
+                end;
+
               fun mk_half_rel_distinct_thm ((xctr_def', cxIn), (yctr_def', cyIn)) =
                 mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def']
                   cxIn cyIn;
@@ -1512,6 +1521,8 @@
                 RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2);
 
               val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos);
+              val rel_intro_thms = map mk_rel_intro_thm rel_inject_thms;
+
               val half_rel_distinct_thmss =
                 map (map mk_half_rel_distinct_thm) (mk_half_pairss rel_infos);
               val other_half_rel_distinct_thmss =
@@ -1534,6 +1545,7 @@
                  (mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs),
                  (rel_distinctN, rel_distinct_thms, simp_attrs),
                  (rel_injectN, rel_inject_thms, simp_attrs),
+                 (rel_introsN, rel_intro_thms, []),
                  (setN, set_thms, code_nitpicksimp_attrs @ simp_attrs),
                  (sel_mapN, sel_map_thms, []),
                  (sel_setN, sel_set_thms, []),

--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Jun 11 14:24:23 2014 +1000
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Jul 03 11:31:25 2014 +0200
@@ -127,6 +127,7 @@
   val rel_coinductN: string
   val rel_inductN: string
   val rel_injectN: string
+  val rel_introsN: string
   val rel_distinctN: string
   val rvN: string
   val sel_corecN: string
@@ -406,6 +407,7 @@
 val rel_distinctN = relN ^ "_" ^ distinctN
 val injectN = "inject"
 val rel_injectN = relN ^ "_" ^ injectN
+val rel_introsN = relN ^ "_intros"
 val rel_coinductN = relN ^ "_" ^ coinductN
 val dtor_rel_coinductN = dtorN ^ "_" ^ rel_coinductN
 val rel_inductN = relN ^ "_" ^ inductN