--- 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.
--- 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}
--- 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
--- 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"
--- 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"
--- 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)"
--- 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"
--- 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}"
--- 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)
--- 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
--- 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"
--- 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
--- 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
(*
--- 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
--- 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'
--- 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
--- 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,
--- 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 = [],
--- 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;
--- 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)"
--- 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
--- 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"