# HG changeset patch
# User huffman
# Date 1272907699 25200
# Node ID f96aa31b739da4f98776e7bfc0d9d080c6882b58
# Parent  4c1f119fadb94165a49a1b059a9fe9532c53f493# Parent  25153c08655e2f2862841c86a83b7a91f5efaab6
merged

diff -r 25153c08655e -r f96aa31b739d src/HOL/Library/FrechetDeriv.thy
--- a/src/HOL/Library/FrechetDeriv.thy	Mon May 03 14:35:10 2010 +0200
+++ b/src/HOL/Library/FrechetDeriv.thy	Mon May 03 10:28:19 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]
 
diff -r 25153c08655e -r f96aa31b739d src/HOL/Library/Product_plus.thy
--- a/src/HOL/Library/Product_plus.thy	Mon May 03 14:35:10 2010 +0200
+++ b/src/HOL/Library/Product_plus.thy	Mon May 03 10:28:19 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
diff -r 25153c08655e -r f96aa31b739d src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon May 03 14:35:10 2010 +0200
+++ b/src/HOL/Limits.thy	Mon May 03 10:28:19 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)
 
 
diff -r 25153c08655e -r f96aa31b739d src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon May 03 14:35:10 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon May 03 10:28:19 2010 -0700
@@ -1931,14 +1931,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>
diff -r 25153c08655e -r f96aa31b739d src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Mon May 03 14:35:10 2010 +0200
+++ b/src/HOL/SEQ.thy	Mon May 03 10:28:19 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)"
diff -r 25153c08655e -r f96aa31b739d src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Mon May 03 14:35:10 2010 +0200
+++ b/src/HOLCF/Tools/fixrec.ML	Mon May 03 10:28:19 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