# HG changeset patch
# User wenzelm
# Date 1413921345 -7200
# Node ID e55fe82f3803ba8b64f7298a7c0d3b1a1a078149
# Parent  cb9d84d3e7f270c8541484cc248abfa08a9a0e8a# Parent  790ff9eb2578dd0077290540aab50147c945a018
merged

diff -r 790ff9eb2578 -r e55fe82f3803 NEWS
--- a/NEWS	Tue Oct 21 21:35:45 2014 +0200
+++ b/NEWS	Tue Oct 21 21:55:45 2014 +0200
@@ -55,10 +55,9 @@
   dvd_plus_eq_left ~> dvd_add_left_iff
 Minor INCOMPATIBILITY.
 
-* More foundational definition for predicate "even":
+* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _".
   even_def ~> even_iff_mod_2_eq_zero
-  even_iff_2_dvd ~> even_def
-Minor INCOMPATIBILITY.
+INCOMPATIBILITY.
 
 * Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1
 Minor INCOMPATIBILITY.
diff -r 790ff9eb2578 -r e55fe82f3803 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Oct 21 21:55:45 2014 +0200
@@ -1021,6 +1021,9 @@
 (The @{text "[code]"} attribute is set by the @{text code} plugin,
 Section~\ref{ssec:code-generator}.)
 
+\item[@{text "t."}\hthm{rec_o_map}\rm:] ~ \\
+@{thm list.rec_o_map[no_vars]}
+
 \item[@{text "t."}\hthm{rec_transfer}\rm:] ~ \\
 @{thm list.rec_transfer[no_vars]}
 
@@ -1078,7 +1081,7 @@
 \item \emph{The @{const size} function has a slightly different definition.}
 The new function returns @{text 1} instead of @{text 0} for some nonrecursive
 constructors. This departure from the old behavior made it possible to implement
-@{const size} in terms of the parameterized function @{text "t.size_t"}.
+@{const size} in terms of the generic function @{text "t.size_t"}.
 Moreover, the new function considers nested occurrences of a value, in the nested
 recursive case. The old behavior can be obtained by disabling the @{text size}
 plugin (Section~\ref{sec:controlling-plugins}) and instantiating the
@@ -1852,6 +1855,9 @@
 @{thm llist.corec_sel(1)[no_vars]} \\
 @{thm llist.corec_sel(2)[no_vars]}
 
+\item[@{text "t."}\hthm{map_o_corec}\rm:] ~ \\
+@{thm llist.map_o_corec[no_vars]}
+
 \item[@{text "t."}\hthm{corec_transfer}\rm:] ~ \\
 @{thm llist.corec_transfer[no_vars]}
 
@@ -2843,7 +2849,7 @@
   \label{ssec:size} *}
 
 text {*
-For each datatype, the \hthm{size} plugin generates a parameterized size
+For each datatype, the \hthm{size} plugin generates a generic size
 function @{text "t.size_t"} as well as a specific instance
 @{text "size \<Colon> t \<Rightarrow> bool"} belonging to the @{text size} type
 class. The \keyw{fun} command relies on @{const size} to prove termination of
@@ -2860,11 +2866,12 @@
 @{thm list.size(3)[no_vars]} \\
 @{thm list.size(4)[no_vars]}
 
-\item[@{text "t."}\hthm{rec_o_map}\rm:] ~ \\
-@{thm list.rec_o_map[no_vars]}
-
-\item[@{text "t."}\hthm{size_o_map}\rm:] ~ \\
-@{thm list.size_o_map[no_vars]}
+\item[@{text "t."}\hthm{size_gen}\rm:] ~ \\
+@{thm list.size_gen(1)[no_vars]} \\
+@{thm list.size_gen(2)[no_vars]}
+
+\item[@{text "t."}\hthm{size_gen_o_map}\rm:] ~ \\
+@{thm list.size_gen_o_map[no_vars]}
 
 \end{description}
 \end{indentblock}
diff -r 790ff9eb2578 -r e55fe82f3803 src/HOL/BNF_Fixpoint_Base.thy
--- a/src/HOL/BNF_Fixpoint_Base.thy	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/HOL/BNF_Fixpoint_Base.thy	Tue Oct 21 21:55:45 2014 +0200
@@ -186,6 +186,16 @@
 lemma inj_on_convol_ident: "inj_on (\<lambda>x. (x, f x)) X"
   unfolding inj_on_def by simp
 
+lemma map_sum_if_distrib_then:
+  "\<And>f g e x y. map_sum f g (if e then Inl x else y) = (if e then Inl (f x) else map_sum f g y)"
+  "\<And>f g e x y. map_sum f g (if e then Inr x else y) = (if e then Inr (g x) else map_sum f g y)"
+  by simp_all
+
+lemma map_sum_if_distrib_else:
+  "\<And>f g e x y. map_sum f g (if e then x else Inl y) = (if e then map_sum f g x else Inl (f y))"
+  "\<And>f g e x y. map_sum f g (if e then x else Inr y) = (if e then map_sum f g x else Inr (g y))"
+  by simp_all
+
 lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x"
   by (case_tac x) simp
 
@@ -199,6 +209,9 @@
 lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x"
   by (case_tac x) simp+
 
+lemma case_prod_o_map_prod: "case_prod f \<circ> map_prod g1 g2 = case_prod (\<lambda>l r. f (g1 l) (g2 r))"
+  unfolding comp_def by auto
+
 lemma case_prod_transfer:
   "(rel_fun (rel_fun A (rel_fun B C)) (rel_fun (rel_prod A B) C)) case_prod case_prod"
   unfolding rel_fun_def rel_prod_def by simp
diff -r 790ff9eb2578 -r e55fe82f3803 src/HOL/Codegenerator_Test/Candidates.thy
--- a/src/HOL/Codegenerator_Test/Candidates.thy	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Tue Oct 21 21:55:45 2014 +0200
@@ -12,11 +12,6 @@
   "~~/src/HOL/ex/Records"
 begin
 
-lemma [code]: -- {* Formal joining of hierarchy of implicit definitions in Scala *}
-  fixes a :: "'a :: semiring_div_parity"
-  shows "even a \<longleftrightarrow> a mod 2 = 0"
-  by (fact even_iff_mod_2_eq_zero)
-
 inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
 where
   empty: "sublist [] xs"
diff -r 790ff9eb2578 -r e55fe82f3803 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/HOL/Complex.thy	Tue Oct 21 21:55:45 2014 +0200
@@ -733,7 +733,7 @@
     moreover from cos have "sin d = 0" by (rule cos_one_sin_zero)
     ultimately have "d = 0"
       unfolding sin_zero_iff
-      by (auto simp add: numeral_2_eq_2 less_Suc_eq elim!: evenE)
+      by (auto elim!: evenE dest!: less_2_cases)
     thus "a = x" unfolding d_def by simp
   qed (simp add: assms del: Re_sgn Im_sgn)
   with `z \<noteq> 0` show "arg z = x"
diff -r 790ff9eb2578 -r e55fe82f3803 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/HOL/Deriv.thy	Tue Oct 21 21:55:45 2014 +0200
@@ -80,10 +80,10 @@
   using bounded_linear.linear[OF has_derivative_bounded_linear] .
 
 lemma has_derivative_ident[derivative_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
-  by (simp add: has_derivative_def tendsto_const)
+  by (simp add: has_derivative_def)
 
 lemma has_derivative_const[derivative_intros, simp]: "((\<lambda>x. c) has_derivative (\<lambda>x. 0)) F"
-  by (simp add: has_derivative_def tendsto_const)
+  by (simp add: has_derivative_def)
 
 lemma (in bounded_linear) bounded_linear: "bounded_linear f" ..
 
@@ -180,7 +180,7 @@
     show "(H ---> 0) (at x within s)" by fact
     show "eventually (\<lambda>n. norm (f n - f x - f' (n - x)) / norm (n - x) \<le> H n) (at x within s)"
       unfolding eventually_at using e sandwich by auto
-  qed (auto simp: le_divide_eq tendsto_const)
+  qed (auto simp: le_divide_eq)
 qed fact
 
 lemma has_derivative_subset: "(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_derivative f') (at x within t)"
@@ -1583,8 +1583,7 @@
   from \<zeta> have "eventually (\<lambda>x. norm (\<zeta> x) \<le> x) (at_right 0)"
     by eventually_elim auto
   then have "((\<lambda>x. norm (\<zeta> x)) ---> 0) (at_right 0)"
-    by (rule_tac real_tendsto_sandwich[where f="\<lambda>x. 0" and h="\<lambda>x. x"])
-       (auto intro: tendsto_const tendsto_ident_at)
+    by (rule_tac real_tendsto_sandwich[where f="\<lambda>x. 0" and h="\<lambda>x. x"]) auto
   then have "(\<zeta> ---> 0) (at_right 0)"
     by (rule tendsto_norm_zero_cancel)
   with \<zeta> have "filterlim \<zeta> (at_right 0) (at_right 0)"
diff -r 790ff9eb2578 -r e55fe82f3803 src/HOL/Library/Indicator_Function.thy
--- a/src/HOL/Library/Indicator_Function.thy	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/HOL/Library/Indicator_Function.thy	Tue Oct 21 21:55:45 2014 +0200
@@ -87,8 +87,8 @@
     "(indicator (\<Union> i. A i) x :: 'a) = 1"
     using incseqD[OF `incseq A`, of i "n + i" for n] `x \<in> A i` by (auto simp: indicator_def)
   then show ?thesis
-    by (rule_tac LIMSEQ_offset[of _ i]) (simp add: tendsto_const)
-qed (auto simp: indicator_def tendsto_const)
+    by (rule_tac LIMSEQ_offset[of _ i]) simp
+qed (auto simp: indicator_def)
 
 lemma LIMSEQ_indicator_UN:
   "(\<lambda>k. indicator (\<Union> i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x"
@@ -112,8 +112,8 @@
     "(indicator (\<Inter>i. A i) x :: 'a) = 0"
     using decseqD[OF `decseq A`, of i "n + i" for n] `x \<notin> A i` by (auto simp: indicator_def)
   then show ?thesis
-    by (rule_tac LIMSEQ_offset[of _ i]) (simp add: tendsto_const)
-qed (auto simp: indicator_def tendsto_const)
+    by (rule_tac LIMSEQ_offset[of _ i]) simp
+qed (auto simp: indicator_def)
 
 lemma LIMSEQ_indicator_INT:
   "(\<lambda>k. indicator (\<Inter>i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Inter>i. A i) x"
diff -r 790ff9eb2578 -r e55fe82f3803 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/HOL/Limits.thy	Tue Oct 21 21:55:45 2014 +0200
@@ -544,11 +544,8 @@
   shows "((\<lambda>x. \<Sum>i\<in>S. f i x) ---> (\<Sum>i\<in>S. a i)) F"
 proof (cases "finite S")
   assume "finite S" thus ?thesis using assms
-    by (induct, simp add: tendsto_const, simp add: tendsto_add)
-next
-  assume "\<not> finite S" thus ?thesis
-    by (simp add: tendsto_const)
-qed
+    by (induct, simp, simp add: tendsto_add)
+qed simp
 
 lemma continuous_setsum [continuous_intros]:
   fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
@@ -646,7 +643,7 @@
 lemma tendsto_power [tendsto_intros]:
   fixes f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
   shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) ---> a ^ n) F"
-  by (induct n) (simp_all add: tendsto_const tendsto_mult)
+  by (induct n) (simp_all add: tendsto_mult)
 
 lemma continuous_power [continuous_intros]:
   fixes f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}"
@@ -664,11 +661,8 @@
   shows "((\<lambda>x. \<Prod>i\<in>S. f i x) ---> (\<Prod>i\<in>S. L i)) F"
 proof (cases "finite S")
   assume "finite S" thus ?thesis using assms
-    by (induct, simp add: tendsto_const, simp add: tendsto_mult)
-next
-  assume "\<not> finite S" thus ?thesis
-    by (simp add: tendsto_const)
-qed
+    by (induct, simp, simp add: tendsto_mult)
+qed simp
 
 lemma continuous_setprod [continuous_intros]:
   fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
@@ -1480,7 +1474,7 @@
   hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0"
     by (rule LIMSEQ_inverse_realpow_zero)
   thus ?thesis by (simp add: power_inverse)
-qed (rule LIMSEQ_imp_Suc, simp add: tendsto_const)
+qed (rule LIMSEQ_imp_Suc, simp)
 
 lemma LIMSEQ_power_zero:
   fixes x :: "'a::{real_normed_algebra_1}"
diff -r 790ff9eb2578 -r e55fe82f3803 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Oct 21 21:55:45 2014 +0200
@@ -3691,7 +3691,7 @@
       then obtain r where "subseq r" and fr: "\<forall>n. f (r n) = f l"
         using infinite_enumerate by blast
       then have "subseq r \<and> (f \<circ> r) ----> f l"
-        by (simp add: fr tendsto_const o_def)
+        by (simp add: fr o_def)
       with f show "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) ----> l"
         by auto
     next
@@ -7529,8 +7529,6 @@
   ultimately show "\<exists>!x\<in>s. g x = x" using `a \<in> s` by blast
 qed
 
-declare tendsto_const [intro] (* FIXME: move *)
-
 no_notation
   eucl_less (infix "<e" 50)
 
diff -r 790ff9eb2578 -r e55fe82f3803 src/HOL/Old_Number_Theory/Primes.thy
--- a/src/HOL/Old_Number_Theory/Primes.thy	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Primes.thy	Tue Oct 21 21:55:45 2014 +0200
@@ -68,7 +68,7 @@
 proof-
   from e have np: "n > 0" by presburger
   from e have "2 dvd (n - 1)" by presburger
-  then obtain k where "n - 1 = 2*k" using dvd_def by auto
+  then obtain k where "n - 1 = 2 * k" ..
   hence k: "n = 2*k + 1"  using e by presburger 
   hence "n\<^sup>2 = 4* (k\<^sup>2 + k) + 1" by algebra   
   thus ?thesis by blast
@@ -588,7 +588,6 @@
 thus ?thesis by blast
 qed
 
-lemma even_dvd[simp]: "even (n::nat) \<longleftrightarrow> 2 dvd n" by presburger
 lemma prime_odd: "prime p \<Longrightarrow> p = 2 \<or> odd p" unfolding prime_def by auto
 
 
@@ -828,6 +827,5 @@
 done
 
 declare power_Suc0[simp del]
-declare even_dvd[simp del]
 
 end
diff -r 790ff9eb2578 -r e55fe82f3803 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/HOL/Parity.thy	Tue Oct 21 21:55:45 2014 +0200
@@ -189,47 +189,41 @@
 context semiring_parity
 begin
 
-definition even :: "'a \<Rightarrow> bool"
+abbreviation even :: "'a \<Rightarrow> bool"
 where
-  [presburger, algebra]: "even a \<longleftrightarrow> 2 dvd a"
+  "even a \<equiv> 2 dvd a"
 
 abbreviation odd :: "'a \<Rightarrow> bool"
 where
-  "odd a \<equiv> \<not> even a"
+  "odd a \<equiv> \<not> 2 dvd a"
 
 lemma evenE [elim?]:
   assumes "even a"
   obtains b where "a = 2 * b"
-proof -
-  from assms have "2 dvd a" by (simp add: even_def)
-  then show thesis using that ..
-qed
+  using assms by (rule dvdE)
 
 lemma oddE [elim?]:
   assumes "odd a"
   obtains b where "a = 2 * b + 1"
-proof -
-  from assms have "\<not> 2 dvd a" by (simp add: even_def)
-  then show thesis using that by (rule not_two_dvdE)
-qed
+  using assms by (rule not_two_dvdE)
   
 lemma even_times_iff [simp, presburger, algebra]:
   "even (a * b) \<longleftrightarrow> even a \<or> even b"
-  by (auto simp add: even_def dest: two_is_prime)
+  by (auto simp add: dest: two_is_prime)
 
 lemma even_zero [simp]:
   "even 0"
-  by (simp add: even_def)
+  by simp
 
 lemma odd_one [simp]:
   "odd 1"
-  by (simp add: even_def)
+  by simp
 
 lemma even_numeral [simp]:
   "even (numeral (Num.Bit0 n))"
 proof -
   have "even (2 * numeral n)"
-    unfolding even_times_iff by (simp add: even_def)
+    unfolding even_times_iff by simp
   then have "even (numeral n + numeral n)"
     unfolding mult_2 .
   then show ?thesis
@@ -245,7 +239,7 @@
   then have "even (2 * numeral n + 1)"
     unfolding mult_2 .
   then have "2 dvd numeral n * 2 + 1"
-    unfolding even_def by (simp add: ac_simps)
+    by (simp add: ac_simps)
   with dvd_add_times_triv_left_iff [of 2 "numeral n" 1]
     have "2 dvd 1"
     by simp
@@ -254,7 +248,7 @@
 
 lemma even_add [simp]:
   "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
-  by (auto simp add: even_def dvd_add_right_iff dvd_add_left_iff not_dvd_not_dvd_dvd_add)
+  by (auto simp add: dvd_add_right_iff dvd_add_left_iff not_dvd_not_dvd_dvd_add)
 
 lemma odd_add [simp]:
   "odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))"
@@ -271,7 +265,7 @@
 
 lemma even_minus [simp, presburger, algebra]:
   "even (- a) \<longleftrightarrow> even a"
-  by (simp add: even_def)
+  by (fact dvd_minus_iff)
 
 lemma even_diff [simp]:
   "even (a - b) \<longleftrightarrow> even (a + b)"
@@ -300,7 +294,7 @@
 
 lemma even_iff_mod_2_eq_zero:
   "even a \<longleftrightarrow> a mod 2 = 0"
-  by (simp add: even_def dvd_eq_mod_eq_0)
+  by (fact dvd_eq_mod_eq_0)
 
 lemma even_succ_div_two [simp]:
   "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
@@ -312,7 +306,7 @@
 
 lemma even_two_times_div_two:
   "even a \<Longrightarrow> 2 * (a div 2) = a"
-  by (rule dvd_mult_div_cancel) (simp add: even_def)
+  by (fact dvd_mult_div_cancel)
 
 lemma odd_two_times_div_two_succ:
   "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
@@ -325,7 +319,7 @@
 
 lemma even_Suc [simp, presburger, algebra]:
   "even (Suc n) = odd n"
-  by (simp add: even_def two_dvd_Suc_iff)
+  by (fact two_dvd_Suc_iff)
 
 lemma odd_pos: 
   "odd (n :: nat) \<Longrightarrow> 0 < n"
@@ -334,11 +328,11 @@
 lemma even_diff_nat [simp]:
   fixes m n :: nat
   shows "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)"
-  by (simp add: even_def two_dvd_diff_nat_iff)
+  by (fact two_dvd_diff_nat_iff)
 
 lemma even_int_iff:
   "even (int n) \<longleftrightarrow> even n"
-  by (simp add: even_def dvd_int_iff)
+  by (simp add: dvd_int_iff)
 
 lemma even_nat_iff:
   "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
diff -r 790ff9eb2578 -r e55fe82f3803 src/HOL/Probability/Bochner_Integration.thy
--- a/src/HOL/Probability/Bochner_Integration.thy	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy	Tue Oct 21 21:55:45 2014 +0200
@@ -2335,7 +2335,7 @@
          (auto split: split_indicator simp: natceiling_le_eq) }
   from filterlim_cong[OF refl refl this]
   have "AE x in M. (\<lambda>i. f x * indicator {..real i} x) ----> f x"
-    by (simp add: tendsto_const)
+    by simp
   have "(\<lambda>i. \<integral> x. f x * indicator {..real i} x \<partial>M) ----> x"
     using conv filterlim_real_sequentially by (rule filterlim_compose)
   have M_measure[simp]: "borel_measurable M = borel_measurable borel"
@@ -2439,7 +2439,7 @@
     then 
     show "(\<lambda>i. f' i x) ----> integral\<^sup>L M (f x)"
       unfolding f'_def
-      by (cases "integrable M (f x)") (simp_all add: not_integrable_integral_eq tendsto_const)
+      by (cases "integrable M (f x)") (simp_all add: not_integrable_integral_eq)
   qed
 qed
 
diff -r 790ff9eb2578 -r e55fe82f3803 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Oct 21 21:55:45 2014 +0200
@@ -234,7 +234,7 @@
 end
 
 lemma embed_pmf_transfer:
-  "rel_fun (eq_onp (\<lambda>f::'a \<Rightarrow> real. (\<forall>x. 0 \<le> f x) \<and> (\<integral>\<^sup>+x. ereal (f x) \<partial>count_space UNIV) = 1)) pmf_as_measure.cr_pmf (\<lambda>f. density (count_space UNIV) (ereal \<circ> f)) embed_pmf"
+  "rel_fun (eq_onp (\<lambda>f. (\<forall>x. 0 \<le> f x) \<and> (\<integral>\<^sup>+x. ereal (f x) \<partial>count_space UNIV) = 1)) pmf_as_measure.cr_pmf (\<lambda>f. density (count_space UNIV) (ereal \<circ> f)) embed_pmf"
   by (auto simp: rel_fun_def eq_onp_def embed_pmf.transfer)
 
 lemma td_pmf_embed_pmf:
@@ -263,6 +263,13 @@
 
 setup_lifting td_pmf_embed_pmf
 
+lemma set_pmf_transfer[transfer_rule]: 
+  assumes "bi_total A"
+  shows "rel_fun (pcr_pmf A) (rel_set A) (\<lambda>f. {x. f x \<noteq> 0}) set_pmf"  
+  using `bi_total A`
+  by (auto simp: pcr_pmf_def cr_pmf_def rel_fun_def rel_set_def bi_total_def Bex_def set_pmf_iff)
+     metis+
+
 end 
 
 (*
diff -r 790ff9eb2578 -r e55fe82f3803 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/HOL/Series.thy	Tue Oct 21 21:55:45 2014 +0200
@@ -45,7 +45,7 @@
   by (simp add: suminf_def sums_def lim_def)
 
 lemma sums_zero[simp, intro]: "(\<lambda>n. 0) sums 0"
-  unfolding sums_def by (simp add: tendsto_const)
+  unfolding sums_def by simp
 
 lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)"
   by (rule sums_zero [THEN sums_summable])
@@ -84,7 +84,7 @@
   note eq = this
   show ?thesis unfolding sums_def
     by (rule LIMSEQ_offset[of _ "Suc (Max N)"])
-       (simp add: eq atLeast0LessThan tendsto_const del: add_Suc_right)
+       (simp add: eq atLeast0LessThan del: add_Suc_right)
 qed
 
 lemma summable_finite: "finite N \<Longrightarrow> (\<And>n. n \<notin> N \<Longrightarrow> f n = 0) \<Longrightarrow> summable f"
@@ -232,7 +232,7 @@
     with tendsto_add[OF this tendsto_const, of "- f 0"]
     show "(\<lambda>i. f (Suc i)) sums s"
       by (simp add: sums_def)
-  qed (auto intro: tendsto_add tendsto_const simp: sums_def)
+  qed (auto intro: tendsto_add simp: sums_def)
   finally show ?thesis ..
 qed
 
diff -r 790ff9eb2578 -r e55fe82f3803 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Oct 21 21:55:45 2014 +0200
@@ -42,6 +42,7 @@
      co_rec_selss: thm list list,
      co_rec_codes: thm list,
      co_rec_transfers: thm list,
+     co_rec_o_maps: thm list,
      common_rel_co_inducts: thm list,
      rel_co_inducts: thm list,
      common_set_inducts: thm list,
@@ -175,7 +176,9 @@
 val corec_codeN = "corec_code";
 val corec_transferN = "corec_transfer";
 val map_disc_iffN = "map_disc_iff";
+val map_o_corecN = "map_o_corec";
 val map_selN = "map_sel";
+val rec_o_mapN = "rec_o_map";
 val rec_transferN = "rec_transfer";
 val set_casesN = "set_cases";
 val set_introsN = "set_intros";
@@ -216,6 +219,7 @@
    co_rec_selss: thm list list,
    co_rec_codes: thm list,
    co_rec_transfers: thm list,
+   co_rec_o_maps: thm list,
    common_rel_co_inducts: thm list,
    rel_co_inducts: thm list,
    common_set_inducts: thm list,
@@ -254,7 +258,7 @@
    set_cases = map (Morphism.thm phi) set_cases};
 
 fun morph_fp_co_induct_sugar phi ({co_rec, common_co_inducts, co_inducts, co_rec_def, co_rec_thms,
-    co_rec_discs, co_rec_disc_iffs, co_rec_selss, co_rec_codes, co_rec_transfers,
+    co_rec_discs, co_rec_disc_iffs, co_rec_selss, co_rec_codes, co_rec_transfers, co_rec_o_maps,
     common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts} : fp_co_induct_sugar) =
   {co_rec = Morphism.term phi co_rec,
    common_co_inducts = map (Morphism.thm phi) common_co_inducts,
@@ -266,6 +270,7 @@
    co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss,
    co_rec_codes = map (Morphism.thm phi) co_rec_codes,
    co_rec_transfers = map (Morphism.thm phi) co_rec_transfers,
+   co_rec_o_maps = map (Morphism.thm phi) co_rec_o_maps,
    common_rel_co_inducts = map (Morphism.thm phi) common_rel_co_inducts,
    rel_co_inducts = map (Morphism.thm phi) rel_co_inducts,
    common_set_inducts = map (Morphism.thm phi) common_set_inducts,
@@ -348,7 +353,7 @@
     rel_distinctss map_disc_iffss map_selsss rel_selss rel_intross rel_casess set_thmss set_selsssss
     set_introsssss set_casess ctr_transferss case_transferss disc_transferss co_rec_disc_iffss
     co_rec_codess co_rec_transferss common_rel_co_inducts rel_co_inductss common_set_inducts
-    set_inductss sel_transferss noted =
+    set_inductss sel_transferss co_rec_o_mapss noted =
   let
     val fp_sugars =
       map_index (fn (kk, T) =>
@@ -388,6 +393,7 @@
             co_rec_selss = nth co_rec_selsss kk,
             co_rec_codes = nth co_rec_codess kk,
             co_rec_transfers = nth co_rec_transferss kk,
+            co_rec_o_maps = nth co_rec_o_mapss kk,
             common_rel_co_inducts = common_rel_co_inducts,
             rel_co_inducts = nth rel_co_inductss kk,
             common_set_inducts = common_set_inducts,
@@ -1959,6 +1965,36 @@
     val ctrXs_Tsss = map (map (map freeze_fp)) fake_ctr_Tsss;
     val ctrXs_repTs = map mk_sumprodT_balanced ctrXs_Tsss;
 
+    val _ =
+      let
+        fun mk_edges Xs ctrXs_Tsss =
+          let
+            fun add_edges i =
+              fold (fn T => fold_index (fn (j, X) =>
+                exists_subtype (curry (op =) X) T ? cons (i, j)) Xs);
+          in
+            fold_index (uncurry (fold o add_edges)) ctrXs_Tsss []
+          end;
+
+        fun mk_graph nn edges =
+          Int_Graph.empty
+          |> fold (fn kk => Int_Graph.new_node (kk, ())) (0 upto nn - 1)
+          |> fold Int_Graph.add_edge edges;
+
+        val str_of_scc = curry (op ^) (co_prefix fp ^ "datatype ") o
+          space_implode " and " o map (suffix " = \<dots>" o Long_Name.base_name);
+
+        fun warn [_] = ()
+          | warn sccs =
+            warning ("Defined types not fully mutually " ^ co_prefix fp ^ "recursive\n\
+              \Alternative specification:\n" ^
+              cat_lines (map (prefix "  " o str_of_scc o map (nth fp_b_names)) sccs));
+
+        val edges = mk_edges Xs ctrXs_Tsss;
+        val G = mk_graph nn edges;
+        val sccs = rev (map (sort int_ord) (Int_Graph.strong_conn G));
+      in warn sccs end;
+
     val fp_eqs = map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_repTs;
 
     val killed_As =
@@ -1969,7 +2005,7 @@
              dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
              ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_setss, xtor_rels,
              xtor_co_rec_thms, xtor_rel_co_induct, dtor_set_inducts,
-             xtor_co_rec_transfers, ...},
+             xtor_co_rec_transfers, xtor_co_rec_o_maps, ...},
            lthy)) =
       fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
         (map dest_TFree killed_As) fp_eqs no_defs_lthy
@@ -2018,6 +2054,7 @@
     val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
     val fp_nesting_set_maps = maps set_map_of_bnf fp_nesting_bnfs;
     val live_nesting_map_id0s = map map_id0_of_bnf live_nesting_bnfs;
+    val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs;
     val live_nesting_set_maps = maps set_map_of_bnf live_nesting_bnfs;
     val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs;
 
@@ -2034,6 +2071,7 @@
         (liveness_of_fp_bnf num_As any_fp_bnf) As Bs0;
 
     val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
+    val live_AsBs = filter (op <>) (As ~~ Bs);
 
     val ctors = map (mk_ctor As) ctors0;
     val dtors = map (mk_dtor As) dtors0;
@@ -2178,11 +2216,10 @@
 
     fun mk_co_rec_transfer_goals lthy co_recs =
       let
-        val liveAsBs = filter (op <>) (As ~~ Bs);
-        val B_ify = Term.subst_atomic_types (liveAsBs @ (Cs ~~ Es));
+        val B_ify = Term.subst_atomic_types (live_AsBs @ (Cs ~~ Es));
 
         val ((Rs, Ss), names_lthy) = lthy
-          |> mk_Frees "R" (map (uncurry mk_pred2T) liveAsBs)
+          |> mk_Frees "R" (map (uncurry mk_pred2T) live_AsBs)
           ||>> mk_Frees "S" (map2 mk_pred2T Cs Es);
 
         val co_recBs = map B_ify co_recs;
@@ -2201,6 +2238,73 @@
         |> map Thm.close_derivation
       end;
 
+    fun derive_rec_o_map_thmss lthy recs rec_defs =
+      if live = 0 then replicate nn []
+      else
+        let
+          fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy);
+
+          val maps0 = map map_of_bnf fp_bnfs;
+          val ABs = As ~~ Bs
+          val liveness = map (op <>) ABs;
+          val f_names = variant_names num_As "f";
+          val fs = map2 (curry Free) f_names (map (op -->) ABs);
+          val live_gs = AList.find (op =) (fs ~~ liveness) true;
+
+          val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0;
+
+          val rec_Ts as rec_T1 :: _ = map fastype_of recs;
+          val rec_arg_Ts = binder_fun_types rec_T1;
+
+          val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
+
+          val num_rec_args = length rec_arg_Ts;
+          val g_Ts = map B_ify_T rec_arg_Ts;
+          val g_names = variant_names num_rec_args "g";
+          val gs = map2 (curry Free) g_names g_Ts;
+          val grecs = map (fn recx => Term.list_comb (Term.map_types B_ify_T recx, gs)) recs;
+
+          val rec_o_map_lhss = map2 (curry HOLogic.mk_comp) grecs gmaps;
+
+          val ABfs = ABs ~~ fs;
+
+          fun mk_rec_arg_arg (x as Free (_, T)) =
+            let val U = B_ify_T T in
+              if T = U then x else build_map lthy [] (the o AList.lookup (op =) ABfs) (T, U) $ x
+            end;
+
+          fun mk_rec_o_map_arg rec_arg_T h =
+            let
+              val x_Ts = binder_types rec_arg_T;
+              val m = length x_Ts;
+              val x_names = variant_names m "x";
+              val xs = map2 (curry Free) x_names x_Ts;
+              val xs' = map mk_rec_arg_arg xs;
+            in
+              fold_rev Term.lambda xs (Term.list_comb (h, xs'))
+            end;
+
+          fun mk_rec_o_map_rhs recx =
+            let val args = map2 mk_rec_o_map_arg rec_arg_Ts gs in
+              Term.list_comb (recx, args)
+            end;
+
+          val rec_o_map_rhss = map mk_rec_o_map_rhs recs;
+
+          val rec_o_map_goals =
+            map2 (fold_rev (fold_rev Logic.all) [fs, gs] o HOLogic.mk_Trueprop oo
+              curry HOLogic.mk_eq) rec_o_map_lhss rec_o_map_rhss;
+          val rec_o_map_thms =
+            @{map 3} (fn goal => fn rec_def => fn ctor_rec_o_map =>
+                Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
+                  mk_co_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s
+                    abs_inverses ctor_rec_o_map)
+                |> Thm.close_derivation)
+              rec_o_map_goals rec_defs xtor_co_rec_o_maps;
+        in
+          map single rec_o_map_thms
+        end;
+
     fun derive_note_induct_recs_thms_for_types
         ((((map_thmss, map_disc_iffss, map_selsss, rel_injectss, rel_distinctss, rel_selss,
             rel_intross, rel_casess, set_thmss, set_selsssss, set_introsssss,
@@ -2235,6 +2339,8 @@
                (rel_induct_attrs, rel_induct_attrs))
             end;
 
+        val rec_o_map_thmss = derive_rec_o_map_thmss lthy recs rec_defs;
+
         val simp_thmss =
           @{map 6} mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss set_thmss;
 
@@ -2249,6 +2355,7 @@
         val notes =
           [(inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]),
            (recN, rec_thmss, K rec_attrs),
+           (rec_o_mapN, rec_o_map_thmss, K []),
            (rec_transferN, rec_transfer_thmss, K []),
            (rel_inductN, rel_induct_thmss, K (rel_induct_attrs @ [induct_pred_attr ""])),
            (simpsN, simp_thmss, K [])]
@@ -2267,6 +2374,7 @@
           rel_intross rel_casess set_thmss set_selsssss set_introsssss set_casess ctr_transferss
           case_transferss disc_transferss (replicate nn []) (replicate nn []) rec_transfer_thmss
           common_rel_induct_thms rel_induct_thmss [] (replicate nn []) sel_transferss
+          rec_o_map_thmss
       end;
 
     fun derive_corec_transfer_thms lthy corecs corec_defs =
@@ -2284,6 +2392,66 @@
         |> map Thm.close_derivation
       end;
 
+    fun derive_map_o_corec_thmss lthy0 lthy2 corecs corec_defs =
+      if live = 0 then replicate nn []
+      else
+        let
+          fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy0);
+          val maps0 = map map_of_bnf fp_bnfs;
+          val ABs = As ~~ Bs
+          val liveness = map (op <>) ABs;
+          val f_names = variant_names num_As "f";
+          val fs = map2 (curry Free) f_names (map (op -->) ABs);
+          val live_fs = AList.find (op =) (fs ~~ liveness) true;
+
+          val fmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_fs)) maps0;
+
+          val corec_Ts as corec_T1 :: _ = map fastype_of corecs;
+          val corec_arg_Ts = binder_fun_types corec_T1;
+
+          val B_ify = Term.subst_atomic_types (As ~~ Bs);
+          val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
+
+          val num_rec_args = length corec_arg_Ts;
+          val g_names = variant_names num_rec_args "g";
+          val gs = map2 (curry Free) g_names corec_arg_Ts;
+          val gcorecs = map (fn corecx => Term.list_comb (corecx, gs)) corecs;
+
+          val map_o_corec_lhss = map2 (curry HOLogic.mk_comp) fmaps gcorecs;
+
+          val ABgs = ABs ~~ fs;
+
+          fun mk_map_o_corec_arg corec_argB_T g =
+            let
+              val T = range_type (fastype_of g);
+              val U = range_type corec_argB_T;
+            in
+              if T = U then g
+              else HOLogic.mk_comp (build_map lthy2 [] (the o AList.lookup (op =) ABgs) (T, U), g)
+            end;
+
+          fun mk_map_o_corec_rhs corecx =
+            let val args = map2 (mk_map_o_corec_arg o B_ify_T) corec_arg_Ts gs in
+              Term.list_comb (B_ify corecx, args)
+            end;
+
+          val map_o_corec_rhss = map mk_map_o_corec_rhs corecs;
+
+          val map_o_corec_goals =
+            map2 (fold_rev (fold_rev Logic.all) [fs, gs] o HOLogic.mk_Trueprop oo
+              curry HOLogic.mk_eq) map_o_corec_lhss map_o_corec_rhss;
+
+          val map_o_corec_thms =
+            @{map 3} (fn goal => fn corec_def => fn dtor_map_o_corec =>
+                Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
+                  mk_co_rec_o_map_tac ctxt corec_def pre_map_defs live_nesting_map_ident0s
+                    abs_inverses dtor_map_o_corec)
+                |> Thm.close_derivation)
+              map_o_corec_goals corec_defs xtor_co_rec_o_maps;
+        in
+          map single map_o_corec_thms
+        end;
+
     fun derive_note_coinduct_corecs_thms_for_types
         ((((map_thmss, map_disc_iffss, map_selsss, rel_injectss, rel_distinctss, rel_selss,
             rel_intross, rel_casess, set_thmss, set_selsssss, set_introsssss, set_casess,
@@ -2339,6 +2507,8 @@
                (rel_coinduct_attrs, common_rel_coinduct_attrs))
             end;
 
+        val map_o_corec_thmss = derive_map_o_corec_thmss lthy lthy corecs corec_defs;
+
         val (set_induct_thms, set_induct_attrss) =
           derive_set_induct_thms_for_types lthy nn fpTs (map #ctrs ctr_sugars)
             (map (map (mk_set As)) (map sets_of_bnf fp_bnfs)) dtor_set_inducts
@@ -2370,6 +2540,7 @@
            (corec_disc_iffN, corec_disc_iff_thmss, K corec_disc_iff_attrs),
            (corec_selN, corec_sel_thmss, K corec_sel_attrs),
            (corec_transferN, corec_transfer_thmss, K []),
+           (map_o_corecN, map_o_corec_thmss, K []),
            (rel_coinductN, rel_coinduct_thmss, K (rel_coinduct_attrs @ [coinduct_pred_attr ""])),
            (simpsN, simp_thmss, K [])]
           |> massage_multi_notes fp_b_names fpTs;
@@ -2386,7 +2557,7 @@
           rel_intross rel_casess set_thmss set_selsssss set_introsssss set_casess ctr_transferss
           case_transferss disc_transferss corec_disc_iff_thmss (map single corec_code_thms)
           corec_transfer_thmss common_rel_coinduct_thms rel_coinduct_thmss set_induct_thms
-          (replicate nn (if nn = 1 then set_induct_thms else [])) sel_transferss
+          (replicate nn (if nn = 1 then set_induct_thms else [])) sel_transferss map_o_corec_thmss
       end;
 
     val lthy'' = lthy'
diff -r 790ff9eb2578 -r e55fe82f3803 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Oct 21 21:55:45 2014 +0200
@@ -19,6 +19,8 @@
     thm list list list -> tactic
   val mk_corec_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic
   val mk_corec_disc_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
+  val mk_co_rec_o_map_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> thm -> thm ->
+    thm Seq.seq
   val mk_corec_transfer_tac: Proof.context -> cterm list -> cterm list -> thm list -> thm list ->
     thm list -> thm list -> thm list -> ''a list -> ''a list list -> ''a list list list list ->
     ''a list list list list -> tactic
@@ -161,6 +163,19 @@
   @{thms comp_def convol_def fst_conv id_def case_prod_Pair_iden snd_conv split_conv
       case_unit_Unity} @ sumprod_thms_map;
 
+fun mk_co_rec_o_map_tac ctxt co_rec_def pre_map_defs map_ident0s abs_inverses xtor_co_rec_o_map =
+  let
+    val rec_o_map_simps = @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum map_sum.simps
+      case_prod_map_prod id_bnf_def map_prod_simp map_sum_if_distrib_then map_sum_if_distrib_else
+      if_distrib[THEN sym]};
+  in
+    HEADGOAL (subst_tac @{context} (SOME [1, 2]) [co_rec_def] THEN'
+      rtac (xtor_co_rec_o_map RS trans) THEN'
+      CONVERSION Thm.eta_long_conversion THEN'
+      asm_simp_tac (ss_only (pre_map_defs @ distinct Thm.eq_thm_prop (map_ident0s @ abs_inverses) @
+        rec_o_map_simps) ctxt))
+  end;
+
 fun mk_rec_tac pre_map_defs map_ident0s rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt =
   HEADGOAL ((if is_def_looping ctr_def then subst_tac ctxt NONE
     else SELECT_GOAL o unfold_thms_tac ctxt) [ctr_def]) THEN
diff -r 790ff9eb2578 -r e55fe82f3803 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Oct 21 21:55:45 2014 +0200
@@ -297,7 +297,8 @@
               fp_bnf_sugar = {map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels,
                 rel_intros, rel_cases, set_thms, set_selssss, set_introssss, set_cases, ...},
               fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers,
-                common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts, ...},
+                co_rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts,
+                set_inducts, ...},
               ...} : fp_sugar) =
           {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk,
            pre_bnf = pre_bnf, fp_bnf = nth (#bnfs fp_res) kk, absT_info = absT_info,
@@ -334,6 +335,7 @@
               co_rec_selss = co_rec_sel_thmss,
               co_rec_codes = co_rec_codes,
               co_rec_transfers = co_rec_transfers,
+              co_rec_o_maps = co_rec_o_maps,
               common_rel_co_inducts = common_rel_co_inducts,
               rel_co_inducts = rel_co_inducts,
               common_set_inducts = common_set_inducts,
diff -r 790ff9eb2578 -r e55fe82f3803 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Tue Oct 21 21:55:45 2014 +0200
@@ -109,6 +109,7 @@
         co_rec_selss = [],
         co_rec_codes = [],
         co_rec_transfers = [],
+        co_rec_o_maps = @{thms case_sum_o_map_sum},
         common_rel_co_inducts = [],
         rel_co_inducts = [],
         common_set_inducts = [],
@@ -174,6 +175,7 @@
         co_rec_selss = [],
         co_rec_codes = [],
         co_rec_transfers = [],
+        co_rec_o_maps = @{thms case_prod_o_map_prod},
         common_rel_co_inducts = [],
         rel_co_inducts = [],
         common_set_inducts = [],
diff -r 790ff9eb2578 -r e55fe82f3803 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Oct 21 21:55:45 2014 +0200
@@ -22,10 +22,9 @@
 open BNF_FP_Def_Sugar
 
 val size_N = "size_";
-
-val rec_o_mapN = "rec_o_map";
 val sizeN = "size";
-val size_o_mapN = "size_o_map";
+val size_genN = "size_gen";
+val size_gen_o_mapN = "size_gen_o_map";
 
 val nitpicksimp_attrs = @{attributes [nitpick_simp]};
 val simp_attrs = @{attributes [simp]};
@@ -38,11 +37,11 @@
   fun merge data = Symtab.merge (K true) data;
 );
 
-fun register_size T_name size_name size_simps size_o_maps =
-  Context.proof_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_o_maps)))));
+fun register_size T_name size_name size_simps size_gen_o_maps =
+  Context.proof_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_gen_o_maps)))));
 
-fun register_size_global T_name size_name size_simps size_o_maps =
-  Context.theory_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_o_maps)))));
+fun register_size_global T_name size_name size_simps size_gen_o_maps =
+  Context.theory_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_gen_o_maps)))));
 
 val size_of = Symtab.lookup o Data.get o Context.Proof;
 val size_of_global = Symtab.lookup o Data.get o Context.Theory;
@@ -62,20 +61,12 @@
 val rec_o_map_simps =
   @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod id_bnf_def};
 
-fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
-    ctor_rec_o_map =
-  HEADGOAL (subst_tac @{context} (SOME [1, 2]) [rec_def] THEN' rtac (ctor_rec_o_map RS trans) THEN'
-    CONVERSION Thm.eta_long_conversion THEN'
-    asm_simp_tac (ss_only (pre_map_defs @
-        distinct Thm.eq_thm_prop (live_nesting_map_ident0s @ abs_inverses) @ rec_o_map_simps)
-      ctxt));
+val size_gen_o_map_simps = @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
 
-val size_o_map_simps = @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
-
-fun mk_size_o_map_tac ctxt size_def rec_o_map inj_maps size_maps =
+fun mk_size_gen_o_map_tac ctxt size_def rec_o_map inj_maps size_maps =
   unfold_thms_tac ctxt [size_def] THEN
   HEADGOAL (rtac (rec_o_map RS trans) THEN'
-    asm_simp_tac (ss_only (inj_maps @ size_maps @ size_o_map_simps) ctxt)) THEN
+    asm_simp_tac (ss_only (inj_maps @ size_maps @ size_gen_o_map_simps) ctxt)) THEN
   IF_UNSOLVED (unfold_thms_tac ctxt @{thms o_def} THEN HEADGOAL (rtac refl));
 
 fun generate_datatype_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP,
@@ -125,12 +116,12 @@
             pair (snd_const T)
           else if exists (exists_subtype_in (As @ Cs)) Ts then
             (case Symtab.lookup data s of
-              SOME (size_name, (_, size_o_maps)) =>
+              SOME (size_name, (_, size_gen_o_maps)) =>
               let
-                val (args, size_o_mapss') = fold_map mk_size_of_typ Ts [];
+                val (args, size_gen_o_mapss') = fold_map mk_size_of_typ Ts [];
                 val size_const = Const (size_name, map fastype_of args ---> mk_to_natT T);
               in
-                append (size_o_maps :: size_o_mapss')
+                append (size_gen_o_maps :: size_gen_o_mapss')
                 #> pair (Term.list_comb (size_const, args))
               end
             | _ => pair (mk_abs_zero_nat T))
@@ -164,14 +155,14 @@
           val m = length x_Ts;
           val x_names = variant_names m "x";
           val xs = map2 (curry Free) x_names x_Ts;
-          val (summands, size_o_mapss) =
+          val (summands, size_gen_o_mapss) =
             fold_map mk_size_of_arg xs []
             |>> remove (op =) HOLogic.zero;
           val sum =
             if null summands then base_case
             else foldl1 mk_plus_nat (summands @ [HOLogic.Suc_zero]);
         in
-          append size_o_mapss
+          append size_gen_o_mapss
           #> pair (fold_rev Term.lambda (map substCnatT xs) sum)
         end;
 
@@ -182,11 +173,11 @@
       val maybe_conceal_def_binding = Thm.def_binding
         #> not (Config.get lthy0 bnf_note_all) ? Binding.conceal;
 
-      val (size_rhss, nested_size_o_mapss) = fold_map mk_size_rhs recs [];
+      val (size_rhss, nested_size_gen_o_mapss) = fold_map mk_size_rhs recs [];
       val size_Ts = map fastype_of size_rhss;
 
-      val nested_size_o_maps_complete = forall (not o null) nested_size_o_mapss;
-      val nested_size_o_maps = fold (union Thm.eq_thm_prop) nested_size_o_mapss [];
+      val nested_size_gen_o_maps_complete = forall (not o null) nested_size_gen_o_mapss;
+      val nested_size_gen_o_maps = fold (union Thm.eq_thm_prop) nested_size_gen_o_mapss [];
 
       val ((raw_size_consts, raw_size_defs), (lthy1', lthy1)) = lthy0
         |> apfst split_list o @{fold_map 2} (fn b => fn rhs =>
@@ -240,7 +231,7 @@
         (Spec_Rules.retrieve lthy0 @{const size ('a)}
          |> map_filter (try (fn (Spec_Rules.Equational, (_, [thm])) => thm)));
 
-      val nested_size_maps = map (mk_pointfull lthy2) nested_size_o_maps @ nested_size_o_maps;
+      val nested_size_maps = map (mk_pointfull lthy2) nested_size_gen_o_maps @ nested_size_gen_o_maps;
       val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ fp_nesting_bnfs @ live_nesting_bnfs)
         |> distinct Thm.eq_thm_prop;
 
@@ -260,6 +251,7 @@
       val overloaded_size_simpss =
         map2 (map o derive_overloaded_size_simp) overloaded_size_defs' size_simpss;
       val size_thmss = map2 append size_simpss overloaded_size_simpss;
+      val size_gen_thmss = size_simpss
 
       val ABs = As ~~ Bs;
       val g_names = variant_names num_As "g";
@@ -271,93 +263,45 @@
 
       val maps0 = map map_of_bnf fp_bnfs;
 
-      val (rec_o_map_thmss, size_o_map_thmss) =
-        if live = 0 then
-          `I (replicate nn [])
+      val size_gen_o_map_thmss =
+        if live = 0 then replicate nn []
         else
           let
-            val pre_bnfs = map #pre_bnf fp_sugars;
-            val pre_map_defs = map map_def_of_bnf pre_bnfs;
-            val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs;
-            val abs_inverses = map (#abs_inverse o #absT_info) fp_sugars;
-            val rec_defs = map (#co_rec_def o #fp_co_induct_sugar) fp_sugars;
-
             val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0;
 
-            val num_rec_args = length rec_arg_Ts;
-            val h_Ts = map B_ify rec_arg_Ts;
-            val h_names = variant_names num_rec_args "h";
-            val hs = map2 (curry Free) h_names h_Ts;
-            val hrecs = map (fn recx => Term.list_comb (Term.map_types B_ify recx, hs)) recs;
-
-            val rec_o_map_lhss = map2 (curry HOLogic.mk_comp) hrecs gmaps;
-
-            val ABgs = ABs ~~ gs;
-
-            fun mk_rec_arg_arg (x as Free (_, T)) =
-              let val U = B_ify T in
-                if T = U then x else build_map lthy2 [] (the o AList.lookup (op =) ABgs) (T, U) $ x
-              end;
-
-            fun mk_rec_o_map_arg rec_arg_T h =
-              let
-                val x_Ts = binder_types rec_arg_T;
-                val m = length x_Ts;
-                val x_names = variant_names m "x";
-                val xs = map2 (curry Free) x_names x_Ts;
-                val xs' = map mk_rec_arg_arg xs;
-              in
-                fold_rev Term.lambda xs (Term.list_comb (h, xs'))
-              end;
-
-            fun mk_rec_o_map_rhs recx =
-              let val args = map2 mk_rec_o_map_arg rec_arg_Ts hs in
-                Term.list_comb (recx, args)
-              end;
-
-            val rec_o_map_rhss = map mk_rec_o_map_rhs recs;
-
-            val rec_o_map_goals =
-              map2 (fold_rev (fold_rev Logic.all) [gs, hs] o HOLogic.mk_Trueprop oo
-                curry HOLogic.mk_eq) rec_o_map_lhss rec_o_map_rhss;
-            val rec_o_map_thms =
-              @{map 3} (fn goal => fn rec_def => fn ctor_rec_o_map =>
-                  Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
-                    mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
-                      ctor_rec_o_map)
-                  |> Thm.close_derivation)
-                rec_o_map_goals rec_defs ctor_rec_o_maps;
-
-            val size_o_map_conds =
-              if exists (can Logic.dest_implies o Thm.prop_of) nested_size_o_maps then
+            val size_gen_o_map_conds =
+              if exists (can Logic.dest_implies o Thm.prop_of) nested_size_gen_o_maps then
                 map (HOLogic.mk_Trueprop o mk_inj) live_gs
               else
                 [];
 
             val fsizes = map (fn size_constB => Term.list_comb (size_constB, fsB)) size_constsB;
-            val size_o_map_lhss = map2 (curry HOLogic.mk_comp) fsizes gmaps;
+            val size_gen_o_map_lhss = map2 (curry HOLogic.mk_comp) fsizes gmaps;
 
             val fgs = map2 (fn fB => fn g as Free (_, Type (_, [A, B])) =>
               if A = B then fB else HOLogic.mk_comp (fB, g)) fsB gs;
-            val size_o_map_rhss = map (fn c => Term.list_comb (c, fgs)) size_consts;
+            val size_gen_o_map_rhss = map (fn c => Term.list_comb (c, fgs)) size_consts;
 
-            val size_o_map_goals =
+            val size_gen_o_map_goals =
               map2 (fold_rev (fold_rev Logic.all) [fsB, gs] o
-                curry Logic.list_implies size_o_map_conds o HOLogic.mk_Trueprop oo
-                curry HOLogic.mk_eq) size_o_map_lhss size_o_map_rhss;
+                curry Logic.list_implies size_gen_o_map_conds o HOLogic.mk_Trueprop oo
+                curry HOLogic.mk_eq) size_gen_o_map_lhss size_gen_o_map_rhss;
 
-            val size_o_map_thmss =
-              if nested_size_o_maps_complete then
+            val rec_o_maps =
+              fold_rev (curry (op @) o (#co_rec_o_maps o #fp_co_induct_sugar)) fp_sugars [];
+
+            val size_gen_o_map_thmss =
+              if nested_size_gen_o_maps_complete then
                 @{map 3} (fn goal => fn size_def => fn rec_o_map =>
                     Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
-                      mk_size_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps)
+                      mk_size_gen_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps)
                     |> Thm.close_derivation
                     |> single)
-                  size_o_map_goals size_defs rec_o_map_thms
+                  size_gen_o_map_goals size_defs rec_o_maps
               else
                 replicate nn [];
           in
-            (map single rec_o_map_thms, size_o_map_thmss)
+            size_gen_o_map_thmss
           end;
 
       (* Ideally, the "[code]" attribute would be generated only if the "code" plugin is enabled. *)
@@ -372,9 +316,9 @@
         #> filter_out (null o fst o hd o snd);
 
       val notes =
-        [(rec_o_mapN, rec_o_map_thmss, []),
-         (sizeN, size_thmss, code_attrs :: nitpicksimp_attrs @ simp_attrs),
-         (size_o_mapN, size_o_map_thmss, [])]
+        [(sizeN, size_thmss, code_attrs :: nitpicksimp_attrs @ simp_attrs),
+         (size_genN, size_gen_thmss, []),
+         (size_gen_o_mapN, size_gen_o_map_thmss, [])]
         |> massage_multi_notes;
 
       val (noted, lthy3) =
@@ -388,7 +332,7 @@
       |> Local_Theory.declaration {syntax = false, pervasive = true}
         (fn phi => Data.map (fold2 (fn T_name => fn Const (size_name, _) =>
              Symtab.update (T_name, (size_name,
-               pairself (map (Morphism.thm (phi0 $> phi))) (size_simps, flat size_o_map_thmss))))
+               pairself (map (Morphism.thm (phi0 $> phi))) (size_simps, flat size_gen_o_map_thmss))))
            T_names size_consts))
     end
   | generate_datatype_size _ lthy = lthy;
diff -r 790ff9eb2578 -r e55fe82f3803 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/HOL/Topological_Spaces.thy	Tue Oct 21 21:55:45 2014 +0200
@@ -1171,10 +1171,10 @@
     by (auto simp: min_less_iff_disj elim: eventually_elim1)
 qed
 
-lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a within s)"
+lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\<lambda>x. x) ---> a) (at a within s)"
   unfolding tendsto_def eventually_at_topological by auto
 
-lemma (in topological_space) tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) F"
+lemma (in topological_space) tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) ---> k) F"
   by (simp add: tendsto_def)
 
 lemma (in t2_space) tendsto_unique:
@@ -1202,7 +1202,7 @@
 
 lemma (in t2_space) tendsto_const_iff:
   assumes "\<not> trivial_limit F" shows "((\<lambda>x. a :: 'a) ---> b) F \<longleftrightarrow> a = b"
-  by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const])
+  by (auto intro!: tendsto_unique [OF assms tendsto_const])
 
 lemma increasing_tendsto:
   fixes f :: "_ \<Rightarrow> 'a::order_topology"
@@ -1689,7 +1689,7 @@
 
 lemma LIMSEQ_le_const2:
   "\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
-  by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) (auto simp: tendsto_const)
+  by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) auto
 
 lemma convergentD: "convergent X ==> \<exists>L. (X ----> L)"
 by (simp add: convergent_def)
@@ -2117,10 +2117,10 @@
 qed
 
 lemma continuous_on_id[continuous_intros]: "continuous_on s (\<lambda>x. x)"
-  unfolding continuous_on_def by (fast intro: tendsto_ident_at)
+  unfolding continuous_on_def by fast
 
 lemma continuous_on_const[continuous_intros]: "continuous_on s (\<lambda>x. c)"
-  unfolding continuous_on_def by (auto intro: tendsto_const)
+  unfolding continuous_on_def by auto
 
 lemma continuous_on_compose[continuous_intros]:
   "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
diff -r 790ff9eb2578 -r e55fe82f3803 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/HOL/Transcendental.thy	Tue Oct 21 21:55:45 2014 +0200
@@ -1347,7 +1347,7 @@
     unfolding isCont_def
     by (subst filterlim_cong[OF _ refl, of _ "nhds (ln 0)" _ "\<lambda>_. ln 0"])
        (auto simp: ln_neg_is_const not_less eventually_at dist_real_def
-                intro!: tendsto_const exI[of _ "\<bar>x\<bar>"])
+                intro!: exI[of _ "\<bar>x\<bar>"])
 qed
 
 lemma tendsto_ln [tendsto_intros]:
@@ -2214,7 +2214,7 @@
       unfolding eventually_at_right[OF zero_less_one]
       using `x \<noteq> 0` by (intro exI[of _ "1 / \<bar>x\<bar>"]) (auto simp: field_simps powr_def)
   qed (simp_all add: at_eq_sup_left_right)
-qed (simp add: tendsto_const)
+qed simp
 
 lemma tendsto_exp_limit_at_top:
   fixes x :: real
@@ -3598,7 +3598,7 @@
 qed
 
 lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
-  by (simp add: cos_double mult.assoc power_add [symmetric] numeral_2_eq_2)
+  by (cases "even n") (simp_all add: cos_double mult.assoc)
 
 lemma cos_3over2_pi [simp]: "cos (3 / 2 * pi) = 0"
   apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
@@ -3733,7 +3733,7 @@
 proof (cases "x = 0")
   case True
   thus ?thesis
-    unfolding One_nat_def by (auto simp add: tendsto_const)
+    unfolding One_nat_def by auto
 next
   case False
   have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
diff -r 790ff9eb2578 -r e55fe82f3803 src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Tue Oct 21 21:35:45 2014 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy	Tue Oct 21 21:55:45 2014 +0200
@@ -25,7 +25,7 @@
 lemma emep1:
   fixes n d :: int
   shows "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
-  by (auto simp add: pos_zmod_mult_2 add.commute even_def dvd_def)
+  by (auto simp add: pos_zmod_mult_2 add.commute dvd_def)
 
 lemma int_mod_ge:
   "a < n \<Longrightarrow> 0 < (n :: int) \<Longrightarrow> a \<le> a mod n"