--- a/src/HOL/Library/FrechetDeriv.thy Sat May 01 20:49:39 2010 +0200
+++ b/src/HOL/Library/FrechetDeriv.thy Sat May 01 16:13:24 2010 -0700
@@ -54,11 +54,6 @@
subsection {* Addition *}
-lemma add_diff_add:
- fixes a b c d :: "'a::ab_group_add"
- shows "(a + c) - (b + d) = (a - b) + (c - d)"
-by simp
-
lemma bounded_linear_add:
assumes "bounded_linear f"
assumes "bounded_linear g"
@@ -402,11 +397,6 @@
subsection {* Inverse *}
-lemma inverse_diff_inverse:
- "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
- \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
-by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
-
lemmas bounded_linear_mult_const =
mult.bounded_linear_left [THEN bounded_linear_compose]
--- a/src/HOL/Library/Product_plus.thy Sat May 01 20:49:39 2010 +0200
+++ b/src/HOL/Library/Product_plus.thy Sat May 01 16:13:24 2010 -0700
@@ -112,4 +112,10 @@
instance "*" :: (ab_group_add, ab_group_add) ab_group_add
by default (simp_all add: expand_prod_eq)
+lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
+by (cases "finite A", induct set: finite, simp_all)
+
+lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
+by (cases "finite A", induct set: finite, simp_all)
+
end
--- a/src/HOL/Limits.thy Sat May 01 20:49:39 2010 +0200
+++ b/src/HOL/Limits.thy Sat May 01 16:13:24 2010 -0700
@@ -11,7 +11,7 @@
subsection {* Nets *}
text {*
- A net is now defined simply as a filter.
+ A net is now defined simply as a filter on a set.
The definition also allows non-proper filters.
*}
@@ -53,6 +53,12 @@
unfolding eventually_def
by (rule is_filter.True [OF is_filter_Rep_net])
+lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P net"
+proof -
+ assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext)
+ thus "eventually P net" by simp
+qed
+
lemma eventually_mono:
"(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P net \<Longrightarrow> eventually Q net"
unfolding eventually_def
@@ -101,15 +107,15 @@
subsection {* Finer-than relation *}
-text {* @{term "net \<le> net'"} means that @{term net'} is finer than
-@{term net}. *}
+text {* @{term "net \<le> net'"} means that @{term net} is finer than
+@{term net'}. *}
-instantiation net :: (type) "{order,top}"
+instantiation net :: (type) complete_lattice
begin
definition
le_net_def [code del]:
- "net \<le> net' \<longleftrightarrow> (\<forall>P. eventually P net \<longrightarrow> eventually P net')"
+ "net \<le> net' \<longleftrightarrow> (\<forall>P. eventually P net' \<longrightarrow> eventually P net)"
definition
less_net_def [code del]:
@@ -117,12 +123,64 @@
definition
top_net_def [code del]:
- "top = Abs_net (\<lambda>P. True)"
+ "top = Abs_net (\<lambda>P. \<forall>x. P x)"
+
+definition
+ bot_net_def [code del]:
+ "bot = Abs_net (\<lambda>P. True)"
+
+definition
+ sup_net_def [code del]:
+ "sup net net' = Abs_net (\<lambda>P. eventually P net \<and> eventually P net')"
+
+definition
+ inf_net_def [code del]:
+ "inf a b = Abs_net
+ (\<lambda>P. \<exists>Q R. eventually Q a \<and> eventually R b \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
+
+definition
+ Sup_net_def [code del]:
+ "Sup A = Abs_net (\<lambda>P. \<forall>net\<in>A. eventually P net)"
+
+definition
+ Inf_net_def [code del]:
+ "Inf A = Sup {x::'a net. \<forall>y\<in>A. x \<le> y}"
+
+lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"
+unfolding top_net_def
+by (rule eventually_Abs_net, rule is_filter.intro, auto)
-lemma eventually_top [simp]: "eventually P top"
-unfolding top_net_def
+lemma eventually_bot [simp]: "eventually P bot"
+unfolding bot_net_def
by (subst eventually_Abs_net, rule is_filter.intro, auto)
+lemma eventually_sup:
+ "eventually P (sup net net') \<longleftrightarrow> eventually P net \<and> eventually P net'"
+unfolding sup_net_def
+by (rule eventually_Abs_net, rule is_filter.intro)
+ (auto elim!: eventually_rev_mp)
+
+lemma eventually_inf:
+ "eventually P (inf a b) \<longleftrightarrow>
+ (\<exists>Q R. eventually Q a \<and> eventually R b \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
+unfolding inf_net_def
+apply (rule eventually_Abs_net, rule is_filter.intro)
+apply (fast intro: eventually_True)
+apply clarify
+apply (intro exI conjI)
+apply (erule (1) eventually_conj)
+apply (erule (1) eventually_conj)
+apply simp
+apply auto
+done
+
+lemma eventually_Sup:
+ "eventually P (Sup A) \<longleftrightarrow> (\<forall>net\<in>A. eventually P net)"
+unfolding Sup_net_def
+apply (rule eventually_Abs_net, rule is_filter.intro)
+apply (auto intro: eventually_conj elim!: eventually_rev_mp)
+done
+
instance proof
fix x y :: "'a net" show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
by (rule less_net_def)
@@ -137,21 +195,49 @@
unfolding le_net_def expand_net_eq by fast
next
fix x :: "'a net" show "x \<le> top"
+ unfolding le_net_def eventually_top by (simp add: always_eventually)
+next
+ fix x :: "'a net" show "bot \<le> x"
unfolding le_net_def by simp
+next
+ fix x y :: "'a net" show "x \<le> sup x y" and "y \<le> sup x y"
+ unfolding le_net_def eventually_sup by simp_all
+next
+ fix x y z :: "'a net" assume "x \<le> z" and "y \<le> z" thus "sup x y \<le> z"
+ unfolding le_net_def eventually_sup by simp
+next
+ fix x y :: "'a net" show "inf x y \<le> x" and "inf x y \<le> y"
+ unfolding le_net_def eventually_inf by (auto intro: eventually_True)
+next
+ fix x y z :: "'a net" assume "x \<le> y" and "x \<le> z" thus "x \<le> inf y z"
+ unfolding le_net_def eventually_inf
+ by (auto elim!: eventually_mono intro: eventually_conj)
+next
+ fix x :: "'a net" and A assume "x \<in> A" thus "x \<le> Sup A"
+ unfolding le_net_def eventually_Sup by simp
+next
+ fix A and y :: "'a net" assume "\<And>x. x \<in> A \<Longrightarrow> x \<le> y" thus "Sup A \<le> y"
+ unfolding le_net_def eventually_Sup by simp
+next
+ fix z :: "'a net" and A assume "z \<in> A" thus "Inf A \<le> z"
+ unfolding le_net_def Inf_net_def eventually_Sup Ball_def by simp
+next
+ fix A and x :: "'a net" assume "\<And>y. y \<in> A \<Longrightarrow> x \<le> y" thus "x \<le> Inf A"
+ unfolding le_net_def Inf_net_def eventually_Sup Ball_def by simp
qed
end
lemma net_leD:
- "net \<le> net' \<Longrightarrow> eventually P net \<Longrightarrow> eventually P net'"
+ "net \<le> net' \<Longrightarrow> eventually P net' \<Longrightarrow> eventually P net"
unfolding le_net_def by simp
lemma net_leI:
- "(\<And>P. eventually P net \<Longrightarrow> eventually P net') \<Longrightarrow> net \<le> net'"
+ "(\<And>P. eventually P net' \<Longrightarrow> eventually P net) \<Longrightarrow> net \<le> net'"
unfolding le_net_def by simp
lemma eventually_False:
- "eventually (\<lambda>x. False) net \<longleftrightarrow> net = top"
+ "eventually (\<lambda>x. False) net \<longleftrightarrow> net = bot"
unfolding expand_net_eq by (auto elim: eventually_rev_mp)
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sat May 01 20:49:39 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sat May 01 16:13:24 2010 -0700
@@ -2205,14 +2205,6 @@
subsection {* Use this to derive general bound property of convex function. *}
-(* TODO: move *)
-lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
-by (cases "finite A", induct set: finite, simp_all)
-
-(* TODO: move *)
-lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
-by (cases "finite A", induct set: finite, simp_all)
-
lemma convex_on:
assumes "convex s"
shows "convex_on s f \<longleftrightarrow> (\<forall>k u x. (\<forall>i\<in>{1..k::nat}. 0 \<le> u i \<and> x i \<in> s) \<and> setsum u {1..k} = 1 \<longrightarrow>
--- a/src/HOL/SEQ.thy Sat May 01 20:49:39 2010 +0200
+++ b/src/HOL/SEQ.thy Sat May 01 16:13:24 2010 -0700
@@ -532,6 +532,33 @@
lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)"
by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def)
+lemma convergent_const: "convergent (\<lambda>n. c)"
+by (rule convergentI, rule LIMSEQ_const)
+
+lemma convergent_add:
+ fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector"
+ assumes "convergent (\<lambda>n. X n)"
+ assumes "convergent (\<lambda>n. Y n)"
+ shows "convergent (\<lambda>n. X n + Y n)"
+using assms unfolding convergent_def by (fast intro: LIMSEQ_add)
+
+lemma convergent_setsum:
+ fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector"
+ assumes "finite A" and "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
+ shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
+using assms
+by (induct A set: finite, simp_all add: convergent_const convergent_add)
+
+lemma (in bounded_linear) convergent:
+ assumes "convergent (\<lambda>n. X n)"
+ shows "convergent (\<lambda>n. f (X n))"
+using assms unfolding convergent_def by (fast intro: LIMSEQ)
+
+lemma (in bounded_bilinear) convergent:
+ assumes "convergent (\<lambda>n. X n)" and "convergent (\<lambda>n. Y n)"
+ shows "convergent (\<lambda>n. X n ** Y n)"
+using assms unfolding convergent_def by (fast intro: LIMSEQ)
+
lemma convergent_minus_iff:
fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
shows "convergent X \<longleftrightarrow> convergent (\<lambda>n. - X n)"
--- a/src/HOLCF/Tools/fixrec.ML Sat May 01 20:49:39 2010 +0200
+++ b/src/HOLCF/Tools/fixrec.ML Sat May 01 16:13:24 2010 -0700
@@ -337,10 +337,10 @@
(* proves a block of pattern matching equations as theorems, using unfold *)
fun make_simps ctxt (unfold_thm, eqns : (Attrib.binding * term) list) =
let
- val tacs =
- [rtac (unfold_thm RS @{thm ssubst_lhs}) 1,
- asm_simp_tac (simpset_of ctxt) 1];
- fun prove_term t = Goal.prove ctxt [] [] t (K (EVERY tacs));
+ val ss = Simplifier.context ctxt (FixrecSimpData.get (Context.Proof ctxt));
+ val rule = unfold_thm RS @{thm ssubst_lhs};
+ val tac = rtac rule 1 THEN asm_simp_tac ss 1;
+ fun prove_term t = Goal.prove ctxt [] [] t (K tac);
fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t);
in
map prove_eqn eqns