--- a/src/HOL/Library/BigO.thy Tue Apr 29 21:54:26 2014 +0200
+++ b/src/HOL/Library/BigO.thy Tue Apr 29 22:50:55 2014 +0200
@@ -390,7 +390,7 @@
also have "\<dots> \<subseteq> O(g) + O(g)"
proof -
from a have "O(f) \<subseteq> O(g)" by (auto del: subsetI)
- thus ?thesis by (auto del: subsetI)
+ then show ?thesis by (auto del: subsetI)
qed
also have "\<dots> \<subseteq> O(g)" by simp
finally show ?thesis .
--- a/src/HOL/Library/ContNotDenum.thy Tue Apr 29 21:54:26 2014 +0200
+++ b/src/HOL/Library/ContNotDenum.thy Tue Apr 29 22:50:55 2014 +0200
@@ -1,5 +1,5 @@
-(* Title : HOL/ContNonDenum
- Author : Benjamin Porter, Monash University, NICTA, 2005
+(* Title: HOL/Library/ContNonDenum.thy
+ Author: Benjamin Porter, Monash University, NICTA, 2005
*)
header {* Non-denumerability of the Continuum. *}
@@ -15,7 +15,7 @@
system.
{\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
-words, there does not exist a function f:@{text "\<nat>\<Rightarrow>\<real>"} such that f is
+words, there does not exist a function @{text "f: \<nat> \<Rightarrow> \<real>"} such that f is
surjective.
{\em Outline:} An elegant informal proof of this result uses Cantor's
@@ -25,41 +25,50 @@
completeness of the Real numbers and is the foundation for our
argument. Informally it states that an intersection of countable
closed intervals (where each successive interval is a subset of the
-last) is non-empty. We then assume a surjective function f:@{text
-"\<nat>\<Rightarrow>\<real>"} exists and find a real x such that x is not in the range of f
+last) is non-empty. We then assume a surjective function @{text
+"f: \<nat> \<Rightarrow> \<real>"} exists and find a real x such that x is not in the range of f
by generating a sequence of closed intervals then using the NIP. *}
+
subsection {* Closed Intervals *}
subsection {* Nested Interval Property *}
theorem NIP:
- fixes f::"nat \<Rightarrow> real set"
+ fixes f :: "nat \<Rightarrow> real set"
assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
- and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
+ and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
shows "(\<Inter>n. f n) \<noteq> {}"
proof -
let ?I = "\<lambda>n. {Inf (f n) .. Sup (f n)}"
- { fix n
+ {
+ fix n
from closed[rule_format, of n] obtain a b where "f n = {a .. b}" "a \<le> b"
by auto
then have "f n = {Inf (f n) .. Sup (f n)}" and "Inf (f n) \<le> Sup (f n)"
- by auto }
+ by auto
+ }
note f_eq = this
- { fix n m :: nat assume "n \<le> m" then have "f m \<subseteq> f n"
- by (induct rule: dec_induct) (metis order_refl, metis order_trans subset) }
+ {
+ fix n m :: nat
+ assume "n \<le> m"
+ then have "f m \<subseteq> f n"
+ by (induct rule: dec_induct) (metis order_refl, metis order_trans subset)
+ }
note subset' = this
have "compact (f 0)"
by (subst f_eq) (rule compact_Icc)
then have "f 0 \<inter> (\<Inter>i. f i) \<noteq> {}"
proof (rule compact_imp_fip_image)
- fix I :: "nat set" assume I: "finite I"
+ fix I :: "nat set"
+ assume I: "finite I"
have "{} \<subset> f (Max (insert 0 I))"
using f_eq[of "Max (insert 0 I)"] by auto
also have "\<dots> \<subseteq> (\<Inter>i\<in>insert 0 I. f i)"
proof (rule INF_greatest)
- fix i assume "i \<in> insert 0 I"
+ fix i
+ assume "i \<in> insert 0 I"
with I show "f (Max (insert 0 I)) \<subseteq> f i"
by (intro subset') auto
qed
@@ -70,6 +79,7 @@
by auto
qed
+
subsection {* Generating the intervals *}
subsubsection {* Existence of non-singleton closed intervals *}
@@ -80,7 +90,7 @@
non-singleton itself. *}
lemma closed_subset_ex:
- fixes c::real
+ fixes c :: real
assumes "a < b"
shows "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}"
proof (cases "c < b")
@@ -90,39 +100,45 @@
case True
with `a < b` `c < b` have "c \<notin> {a..b}"
by auto
- with `a < b` show ?thesis by auto
+ with `a < b` show ?thesis
+ by auto
next
case False
then have "a \<le> c" by simp
def ka \<equiv> "(c + b)/2"
-
- from ka_def `c < b` have kalb: "ka < b" by auto
- moreover from ka_def `c < b` have kagc: "ka > c" by simp
- ultimately have "c\<notin>{ka..b}" by auto
- moreover from `a \<le> c` kagc have "ka \<ge> a" by simp
- hence "{ka..b} \<subseteq> {a..b}" by auto
- ultimately have
- "ka < b \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
- using kalb by auto
+ from ka_def `c < b` have "ka < b"
+ by auto
+ moreover from ka_def `c < b` have "ka > c"
+ by simp
+ ultimately have "c \<notin> {ka..b}"
+ by auto
+ moreover from `a \<le> c` `ka > c` have "ka \<ge> a"
+ by simp
+ then have "{ka..b} \<subseteq> {a..b}"
+ by auto
+ ultimately have "ka < b \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
+ using `ka < b` by auto
then show ?thesis
by auto
qed
next
case False
then have "c \<ge> b" by simp
-
def kb \<equiv> "(a + b)/2"
with `a < b` have "kb < b" by auto
- with kb_def `c \<ge> b` have "a < kb" "kb < c" by auto
+ with kb_def `c \<ge> b` have "a < kb" "kb < c"
+ by auto
from `kb < c` have c: "c \<notin> {a..kb}"
by auto
with `kb < b` have "{a..kb} \<subseteq> {a..b}"
by auto
with `a < kb` c have "a < kb \<and> {a..kb} \<subseteq> {a..b} \<and> c \<notin> {a..kb}"
by simp
- then show ?thesis by auto
+ then show ?thesis
+ by auto
qed
+
subsection {* newInt: Interval generation *}
text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
@@ -130,17 +146,19 @@
does not contain @{text "f (Suc n)"}. With the base case defined such
that @{text "(f 0)\<notin>newInt 0 f"}. *}
+
subsubsection {* Definition *}
-primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
+primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)"
+where
"newInt 0 f = {f 0 + 1..f 0 + 2}"
- | "newInt (Suc n) f =
- (SOME e. (\<exists>e1 e2.
- e1 < e2 \<and>
- e = {e1..e2} \<and>
- e \<subseteq> newInt n f \<and>
- f (Suc n) \<notin> e)
- )"
+| "newInt (Suc n) f =
+ (SOME e.
+ (\<exists>e1 e2.
+ e1 < e2 \<and>
+ e = {e1..e2} \<and>
+ e \<subseteq> newInt n f \<and>
+ f (Suc n) \<notin> e))"
subsubsection {* Properties *}
@@ -150,81 +168,76 @@
lemma newInt_ex:
"\<exists>a b. a < b \<and>
- newInt (Suc n) f = {a..b} \<and>
- newInt (Suc n) f \<subseteq> newInt n f \<and>
- f (Suc n) \<notin> newInt (Suc n) f"
+ newInt (Suc n) f = {a..b} \<and>
+ newInt (Suc n) f \<subseteq> newInt n f \<and>
+ f (Suc n) \<notin> newInt (Suc n) f"
proof (induct n)
case 0
-
let ?e = "SOME e. \<exists>e1 e2.
- e1 < e2 \<and>
- e = {e1..e2} \<and>
- e \<subseteq> {f 0 + 1..f 0 + 2} \<and>
- f (Suc 0) \<notin> e"
+ e1 < e2 \<and>
+ e = {e1..e2} \<and>
+ e \<subseteq> {f 0 + 1..f 0 + 2} \<and>
+ f (Suc 0) \<notin> e"
have "newInt (Suc 0) f = ?e" by auto
moreover
have "f 0 + 1 < f 0 + 2" by simp
- with closed_subset_ex have
- "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and>
- f (Suc 0) \<notin> {ka..kb}" .
- hence
- "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
- e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> e" by simp
- hence
- "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> ?e"
+ with closed_subset_ex
+ have "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> {ka..kb}" .
+ then have "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and> e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> e"
+ by simp
+ then have "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> ?e"
by (rule someI_ex)
ultimately have "\<exists>e1 e2. e1 < e2 \<and>
- newInt (Suc 0) f = {e1..e2} \<and>
- newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
- f (Suc 0) \<notin> newInt (Suc 0) f" by simp
- thus
- "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>
- newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
+ newInt (Suc 0) f = {e1..e2} \<and>
+ newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
+ f (Suc 0) \<notin> newInt (Suc 0) f"
+ by simp
+ then show "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>
+ newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
by simp
next
case (Suc n)
- hence "\<exists>a b.
- a < b \<and>
- newInt (Suc n) f = {a..b} \<and>
- newInt (Suc n) f \<subseteq> newInt n f \<and>
- f (Suc n) \<notin> newInt (Suc n) f" by simp
+ then have "\<exists>a b.
+ a < b \<and>
+ newInt (Suc n) f = {a..b} \<and>
+ newInt (Suc n) f \<subseteq> newInt n f \<and>
+ f (Suc n) \<notin> newInt (Suc n) f"
+ by simp
then obtain a and b where ab: "a < b \<and>
- newInt (Suc n) f = {a..b} \<and>
- newInt (Suc n) f \<subseteq> newInt n f \<and>
- f (Suc n) \<notin> newInt (Suc n) f" by auto
- hence cab: "{a..b} = newInt (Suc n) f" by simp
+ newInt (Suc n) f = {a..b} \<and>
+ newInt (Suc n) f \<subseteq> newInt n f \<and>
+ f (Suc n) \<notin> newInt (Suc n) f"
+ by auto
+ then have cab: "{a..b} = newInt (Suc n) f"
+ by simp
let ?e = "SOME e. \<exists>e1 e2.
- e1 < e2 \<and>
- e = {e1..e2} \<and>
- e \<subseteq> {a..b} \<and>
- f (Suc (Suc n)) \<notin> e"
- from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
+ e1 < e2 \<and>
+ e = {e1..e2} \<and>
+ e \<subseteq> {a..b} \<and>
+ f (Suc (Suc n)) \<notin> e"
+ from cab have ni: "newInt (Suc (Suc n)) f = ?e"
+ by auto
from ab have "a < b" by simp
- with closed_subset_ex have
- "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>
- f (Suc (Suc n)) \<notin> {ka..kb}" .
- hence
- "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
- {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
+ with closed_subset_ex have "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>
+ f (Suc (Suc n)) \<notin> {ka..kb}" .
+ then have "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
+ {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
+ by simp
+ then have "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and> e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> e"
by simp
- hence
- "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
- e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> e" by simp
- hence
- "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and>
- ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
- with ab ni show
- "\<exists>ka kb. ka < kb \<and>
- newInt (Suc (Suc n)) f = {ka..kb} \<and>
- newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
- f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
+ then have "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e"
+ by (rule someI_ex)
+ with ab ni show "\<exists>ka kb. ka < kb \<and>
+ newInt (Suc (Suc n)) f = {ka..kb} \<and>
+ newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
+ f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f"
+ by auto
qed
-lemma newInt_subset:
- "newInt (Suc n) f \<subseteq> newInt n f"
+lemma newInt_subset: "newInt (Suc n) f \<subseteq> newInt n f"
using newInt_ex by auto
@@ -232,34 +245,27 @@
of f is in the intersection of all closed intervals generated by
newInt. *}
-lemma newInt_inter:
- "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
+lemma newInt_inter: "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
proof
- fix n::nat
- {
- assume n0: "n = 0"
- moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}" by simp
- ultimately have "f n \<notin> newInt n f" by simp
- }
- moreover
- {
- assume "\<not> n = 0"
- hence "n > 0" by simp
- then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
-
- from newInt_ex have
- "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
- newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
- then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
- with ndef have "f n \<notin> newInt n f" by simp
- }
- ultimately have "f n \<notin> newInt n f" by (rule case_split)
- thus "f n \<notin> (\<Inter>n. newInt n f)" by auto
+ fix n :: nat
+ have "f n \<notin> newInt n f"
+ proof (cases n)
+ case 0
+ moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}"
+ by simp
+ ultimately show ?thesis by simp
+ next
+ case (Suc m)
+ from newInt_ex have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
+ newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
+ then have "f (Suc m) \<notin> newInt (Suc m) f"
+ by auto
+ with Suc show ?thesis by simp
+ qed
+ then show "f n \<notin> (\<Inter>n. newInt n f)" by auto
qed
-
-lemma newInt_notempty:
- "(\<Inter>n. newInt n f) \<noteq> {}"
+lemma newInt_notempty: "(\<Inter>n. newInt n f) \<noteq> {}"
proof -
let ?g = "\<lambda>n. newInt n f"
have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
@@ -269,30 +275,26 @@
qed
moreover have "\<forall>n. \<exists>a b. ?g n = {a..b} \<and> a \<le> b"
proof
- fix n::nat
- {
- assume "n = 0"
- then have
- "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
+ fix n :: nat
+ show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b"
+ proof (cases n)
+ case 0
+ then have "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
by simp
- hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
- }
- moreover
- {
- assume "\<not> n = 0"
- then have "n > 0" by simp
- then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
-
- have
- "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
+ then show ?thesis
+ by blast
+ next
+ case (Suc m)
+ have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
(newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
by (rule newInt_ex)
- then obtain a and b where
- "a < b \<and> (newInt (Suc m) f) = {a..b}" by auto
- with nd have "?g n = {a..b} \<and> a \<le> b" by auto
- hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
- }
- ultimately show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by (rule case_split)
+ then obtain a and b where "a < b \<and> (newInt (Suc m) f) = {a..b}"
+ by auto
+ with Suc have "?g n = {a..b} \<and> a \<le> b"
+ by auto
+ then show ?thesis
+ by blast
+ qed
qed
ultimately show ?thesis by (rule NIP)
qed
@@ -300,17 +302,22 @@
subsection {* Final Theorem *}
-theorem real_non_denum:
- shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
-proof -- "by contradiction"
- assume "\<exists>f::nat\<Rightarrow>real. surj f"
- then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto
- -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
- have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
- moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
- ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast
- moreover from rangeF have "x \<in> range f" by simp
- ultimately show False by blast
+theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
+proof
+ assume "\<exists>f :: nat \<Rightarrow> real. surj f"
+ then obtain f :: "nat \<Rightarrow> real" where "surj f"
+ by auto
+ txt "We now produce a real number x that is not in the range of f, using the properties of newInt."
+ have "\<exists>x. x \<in> (\<Inter>n. newInt n f)"
+ using newInt_notempty by blast
+ moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
+ by (rule newInt_inter)
+ ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x"
+ by blast
+ moreover from `surj f` have "x \<in> range f"
+ by simp
+ ultimately show False
+ by blast
qed
end
--- a/src/HOL/Library/Convex.thy Tue Apr 29 21:54:26 2014 +0200
+++ b/src/HOL/Library/Convex.thy Tue Apr 29 22:50:55 2014 +0200
@@ -29,11 +29,18 @@
(is "_ \<longleftrightarrow> ?alt")
proof
assume alt[rule_format]: ?alt
- { fix x y and u v :: real assume mem: "x \<in> s" "y \<in> s"
+ {
+ fix x y and u v :: real
+ assume mem: "x \<in> s" "y \<in> s"
assume "0 \<le> u" "0 \<le> v"
- moreover assume "u + v = 1" then have "u = 1 - v" by auto
- ultimately have "u *\<^sub>R x + v *\<^sub>R y \<in> s" using alt[OF mem] by auto }
- then show "convex s" unfolding convex_def by auto
+ moreover
+ assume "u + v = 1"
+ then have "u = 1 - v" by auto
+ ultimately have "u *\<^sub>R x + v *\<^sub>R y \<in> s"
+ using alt[OF mem] by auto
+ }
+ then show "convex s"
+ unfolding convex_def by auto
qed (auto simp: convex_def)
lemma mem_convex:
@@ -50,7 +57,7 @@
lemma convex_UNIV[intro]: "convex UNIV"
unfolding convex_def by auto
-lemma convex_Inter: "(\<forall>s\<in>f. convex s) ==> convex(\<Inter> f)"
+lemma convex_Inter: "(\<forall>s\<in>f. convex s) \<Longrightarrow> convex(\<Inter> f)"
unfolding convex_def by auto
lemma convex_Int: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<inter> t)"
@@ -68,13 +75,16 @@
lemma convex_halfspace_ge: "convex {x. inner a x \<ge> b}"
proof -
- have *: "{x. inner a x \<ge> b} = {x. inner (-a) x \<le> -b}" by auto
- show ?thesis unfolding * using convex_halfspace_le[of "-a" "-b"] by auto
+ have *: "{x. inner a x \<ge> b} = {x. inner (-a) x \<le> -b}"
+ by auto
+ show ?thesis
+ unfolding * using convex_halfspace_le[of "-a" "-b"] by auto
qed
lemma convex_hyperplane: "convex {x. inner a x = b}"
proof -
- have *: "{x. inner a x = b} = {x. inner a x \<le> b} \<inter> {x. inner a x \<ge> b}" by auto
+ have *: "{x. inner a x = b} = {x. inner a x \<le> b} \<inter> {x. inner a x \<ge> b}"
+ by auto
show ?thesis using convex_halfspace_le convex_halfspace_ge
by (auto intro!: convex_Int simp: *)
qed
@@ -115,8 +125,11 @@
lemma convex_setsum:
fixes C :: "'a::real_vector set"
- assumes "finite s" and "convex C" and "(\<Sum> i \<in> s. a i) = 1"
- assumes "\<And>i. i \<in> s \<Longrightarrow> a i \<ge> 0" and "\<And>i. i \<in> s \<Longrightarrow> y i \<in> C"
+ assumes "finite s"
+ and "convex C"
+ and "(\<Sum> i \<in> s. a i) = 1"
+ assumes "\<And>i. i \<in> s \<Longrightarrow> a i \<ge> 0"
+ and "\<And>i. i \<in> s \<Longrightarrow> y i \<in> C"
shows "(\<Sum> j \<in> s. a j *\<^sub>R y j) \<in> C"
using assms(1,3,4,5)
proof (induct arbitrary: a set: finite)
@@ -124,18 +137,27 @@
then show ?case by simp
next
case (insert i s) note IH = this(3)
- have "a i + setsum a s = 1" and "0 \<le> a i" and "\<forall>j\<in>s. 0 \<le> a j" and "y i \<in> C" and "\<forall>j\<in>s. y j \<in> C"
+ have "a i + setsum a s = 1"
+ and "0 \<le> a i"
+ and "\<forall>j\<in>s. 0 \<le> a j"
+ and "y i \<in> C"
+ and "\<forall>j\<in>s. y j \<in> C"
using insert.hyps(1,2) insert.prems by simp_all
- then have "0 \<le> setsum a s" by (simp add: setsum_nonneg)
+ then have "0 \<le> setsum a s"
+ by (simp add: setsum_nonneg)
have "a i *\<^sub>R y i + (\<Sum>j\<in>s. a j *\<^sub>R y j) \<in> C"
proof (cases)
assume z: "setsum a s = 0"
- with `a i + setsum a s = 1` have "a i = 1" by simp
- from setsum_nonneg_0 [OF `finite s` _ z] `\<forall>j\<in>s. 0 \<le> a j` have "\<forall>j\<in>s. a j = 0" by simp
- show ?thesis using `a i = 1` and `\<forall>j\<in>s. a j = 0` and `y i \<in> C` by simp
+ with `a i + setsum a s = 1` have "a i = 1"
+ by simp
+ from setsum_nonneg_0 [OF `finite s` _ z] `\<forall>j\<in>s. 0 \<le> a j` have "\<forall>j\<in>s. a j = 0"
+ by simp
+ show ?thesis using `a i = 1` and `\<forall>j\<in>s. a j = 0` and `y i \<in> C`
+ by simp
next
assume nz: "setsum a s \<noteq> 0"
- with `0 \<le> setsum a s` have "0 < setsum a s" by simp
+ with `0 \<le> setsum a s` have "0 < setsum a s"
+ by simp
then have "(\<Sum>j\<in>s. (a j / setsum a s) *\<^sub>R y j) \<in> C"
using `\<forall>j\<in>s. 0 \<le> a j` and `\<forall>j\<in>s. y j \<in> C`
by (simp add: IH setsum_divide_distrib [symmetric])
@@ -143,9 +165,11 @@
and `0 \<le> setsum a s` and `a i + setsum a s = 1`
have "a i *\<^sub>R y i + setsum a s *\<^sub>R (\<Sum>j\<in>s. (a j / setsum a s) *\<^sub>R y j) \<in> C"
by (rule convexD)
- then show ?thesis by (simp add: scaleR_setsum_right nz)
+ then show ?thesis
+ by (simp add: scaleR_setsum_right nz)
qed
- then show ?case using `finite s` and `i \<notin> s` by simp
+ then show ?case using `finite s` and `i \<notin> s`
+ by simp
qed
lemma convex:
@@ -159,18 +183,22 @@
"\<forall>i. 1 \<le> i \<and> i \<le> k \<longrightarrow> 0 \<le> u i \<and> x i \<in> s"
"setsum u {1..k} = 1"
from this convex_setsum[of "{1 .. k}" s]
- show "(\<Sum>j\<in>{1 .. k}. u j *\<^sub>R x j) \<in> s" by auto
+ show "(\<Sum>j\<in>{1 .. k}. u j *\<^sub>R x j) \<in> s"
+ by auto
next
assume asm: "\<forall>k u x. (\<forall> i :: nat. 1 \<le> i \<and> i \<le> k \<longrightarrow> 0 \<le> u i \<and> x i \<in> s) \<and> setsum u {1..k} = 1
\<longrightarrow> (\<Sum>i = 1..k. u i *\<^sub>R (x i :: 'a)) \<in> s"
- { fix \<mu> :: real
+ {
+ fix \<mu> :: real
fix x y :: 'a
assume xy: "x \<in> s" "y \<in> s"
assume mu: "\<mu> \<ge> 0" "\<mu> \<le> 1"
let ?u = "\<lambda>i. if (i :: nat) = 1 then \<mu> else 1 - \<mu>"
let ?x = "\<lambda>i. if (i :: nat) = 1 then x else y"
- have "{1 :: nat .. 2} \<inter> - {x. x = 1} = {2}" by auto
- then have card: "card ({1 :: nat .. 2} \<inter> - {x. x = 1}) = 1" by simp
+ have "{1 :: nat .. 2} \<inter> - {x. x = 1} = {2}"
+ by auto
+ then have card: "card ({1 :: nat .. 2} \<inter> - {x. x = 1}) = 1"
+ by simp
then have "setsum ?u {1 .. 2} = 1"
using setsum_cases[of "{(1 :: nat) .. 2}" "\<lambda> x. x = 1" "\<lambda> x. \<mu>" "\<lambda> x. 1 - \<mu>"]
by auto
@@ -179,10 +207,13 @@
have grarr: "(\<Sum>j \<in> {Suc (Suc 0)..2}. ?u j *\<^sub>R ?x j) = (1 - \<mu>) *\<^sub>R y"
using setsum_head_Suc[of "Suc (Suc 0)" 2 "\<lambda> j. (1 - \<mu>) *\<^sub>R y"] by auto
from setsum_head_Suc[of "Suc 0" 2 "\<lambda> j. ?u j *\<^sub>R ?x j", simplified this]
- have "(\<Sum>j \<in> {1..2}. ?u j *\<^sub>R ?x j) = \<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y" by auto
- then have "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x \<in> s" using s by (auto simp:add_commute)
+ have "(\<Sum>j \<in> {1..2}. ?u j *\<^sub>R ?x j) = \<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y"
+ by auto
+ then have "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x \<in> s"
+ using s by (auto simp:add_commute)
}
- then show "convex s" unfolding convex_alt by auto
+ then show "convex s"
+ unfolding convex_alt by auto
qed
@@ -193,42 +224,48 @@
proof safe
fix t
fix u :: "'a \<Rightarrow> real"
- assume "convex s" "finite t"
- "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1"
+ assume "convex s"
+ and "finite t"
+ and "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1"
then show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
using convex_setsum[of t s u "\<lambda> x. x"] by auto
next
- assume asm0: "\<forall>t. \<forall> u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x)
- \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
+ assume asm0: "\<forall>t. \<forall> u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and>
+ setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
show "convex s"
unfolding convex_alt
proof safe
fix x y
fix \<mu> :: real
assume asm: "x \<in> s" "y \<in> s" "0 \<le> \<mu>" "\<mu> \<le> 1"
- { assume "x \<noteq> y"
+ {
+ assume "x \<noteq> y"
then have "(1 - \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s"
using asm0[rule_format, of "{x, y}" "\<lambda> z. if z = x then 1 - \<mu> else \<mu>"]
- asm by auto }
+ asm by auto
+ }
moreover
- { assume "x = y"
+ {
+ assume "x = y"
then have "(1 - \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s"
using asm0[rule_format, of "{x, y}" "\<lambda> z. 1"]
- asm by (auto simp:field_simps real_vector.scale_left_diff_distrib) }
- ultimately show "(1 - \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s" by blast
+ asm by (auto simp: field_simps real_vector.scale_left_diff_distrib)
+ }
+ ultimately show "(1 - \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s"
+ by blast
qed
qed
lemma convex_finite:
assumes "finite s"
- shows "convex s \<longleftrightarrow> (\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1
- \<longrightarrow> setsum (\<lambda>x. u x *\<^sub>R x) s \<in> s)"
+ shows "convex s \<longleftrightarrow> (\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<longrightarrow> setsum (\<lambda>x. u x *\<^sub>R x) s \<in> s)"
unfolding convex_explicit
proof safe
fix t u
assume sum: "\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> s"
and as: "finite t" "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = (1::real)"
- have *: "s \<inter> t = t" using as(2) by auto
+ have *: "s \<inter> t = t"
+ using as(2) by auto
have if_distrib_arg: "\<And>P f g x. (if P then f else g) x = (if P then f x else g x)"
by simp
show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
@@ -236,6 +273,7 @@
by (auto simp: assms setsum_cases if_distrib if_distrib_arg)
qed (erule_tac x=s in allE, erule_tac x=u in allE, auto)
+
subsection {* Functions that are convex on a set *}
definition convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
@@ -246,11 +284,13 @@
unfolding convex_on_def by auto
lemma convex_on_add [intro]:
- assumes "convex_on s f" "convex_on s g"
+ assumes "convex_on s f"
+ and "convex_on s g"
shows "convex_on s (\<lambda>x. f x + g x)"
proof -
- { fix x y
- assume "x\<in>s" "y\<in>s"
+ {
+ fix x y
+ assume "x \<in> s" "y \<in> s"
moreover
fix u v :: real
assume "0 \<le> u" "0 \<le> v" "u + v = 1"
@@ -260,13 +300,16 @@
then have "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \<le> u * (f x + g x) + v * (f y + g y)"
by (simp add: field_simps)
}
- then show ?thesis unfolding convex_on_def by auto
+ then show ?thesis
+ unfolding convex_on_def by auto
qed
lemma convex_on_cmul [intro]:
- assumes "0 \<le> (c::real)" "convex_on s f"
+ fixes c :: real
+ assumes "0 \<le> c"
+ and "convex_on s f"
shows "convex_on s (\<lambda>x. c * f x)"
-proof-
+proof -
have *: "\<And>u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)"
by (simp add: field_simps)
show ?thesis using assms(2) and mult_left_mono [OF _ assms(1)]
@@ -274,13 +317,19 @@
qed
lemma convex_lower:
- assumes "convex_on s f" "x\<in>s" "y \<in> s" "0 \<le> u" "0 \<le> v" "u + v = 1"
+ assumes "convex_on s f"
+ and "x \<in> s"
+ and "y \<in> s"
+ and "0 \<le> u"
+ and "0 \<le> v"
+ and "u + v = 1"
shows "f (u *\<^sub>R x + v *\<^sub>R y) \<le> max (f x) (f y)"
-proof-
+proof -
let ?m = "max (f x) (f y)"
have "u * f x + v * f y \<le> u * max (f x) (f y) + v * max (f x) (f y)"
using assms(4,5) by (auto simp add: mult_left_mono add_mono)
- also have "\<dots> = max (f x) (f y)" using assms(6) unfolding distrib[symmetric] by auto
+ also have "\<dots> = max (f x) (f y)"
+ using assms(6) unfolding distrib[symmetric] by auto
finally show ?thesis
using assms unfolding convex_on_def by fastforce
qed
@@ -290,11 +339,13 @@
shows "convex_on s (\<lambda>x. dist a x)"
proof (auto simp add: convex_on_def dist_norm)
fix x y
- assume "x\<in>s" "y\<in>s"
+ assume "x \<in> s" "y \<in> s"
fix u v :: real
- assume "0 \<le> u" "0 \<le> v" "u + v = 1"
+ assume "0 \<le> u"
+ assume "0 \<le> v"
+ assume "u + v = 1"
have "a = u *\<^sub>R a + v *\<^sub>R a"
- unfolding scaleR_left_distrib[symmetric] and `u+v=1` by simp
+ unfolding scaleR_left_distrib[symmetric] and `u + v = 1` by simp
then have *: "a - (u *\<^sub>R x + v *\<^sub>R y) = (u *\<^sub>R (a - x)) + (v *\<^sub>R (a - y))"
by (auto simp add: algebra_simps)
show "norm (a - (u *\<^sub>R x + v *\<^sub>R y)) \<le> u * norm (a - x) + v * norm (a - y)"
@@ -306,7 +357,9 @@
subsection {* Arithmetic operations on sets preserve convexity. *}
lemma convex_linear_image:
- assumes "linear f" and "convex s" shows "convex (f ` s)"
+ assumes "linear f"
+ and "convex s"
+ shows "convex (f ` s)"
proof -
interpret f: linear f by fact
from `convex s` show "convex (f ` s)"
@@ -314,7 +367,9 @@
qed
lemma convex_linear_vimage:
- assumes "linear f" and "convex s" shows "convex (f -` s)"
+ assumes "linear f"
+ and "convex s"
+ shows "convex (f -` s)"
proof -
interpret f: linear f by fact
from `convex s` show "convex (f -` s)"
@@ -322,21 +377,28 @@
qed
lemma convex_scaling:
- assumes "convex s" shows "convex ((\<lambda>x. c *\<^sub>R x) ` s)"
+ assumes "convex s"
+ shows "convex ((\<lambda>x. c *\<^sub>R x) ` s)"
proof -
- have "linear (\<lambda>x. c *\<^sub>R x)" by (simp add: linearI scaleR_add_right)
- then show ?thesis using `convex s` by (rule convex_linear_image)
+ have "linear (\<lambda>x. c *\<^sub>R x)"
+ by (simp add: linearI scaleR_add_right)
+ then show ?thesis
+ using `convex s` by (rule convex_linear_image)
qed
lemma convex_negations:
- assumes "convex s" shows "convex ((\<lambda>x. - x) ` s)"
+ assumes "convex s"
+ shows "convex ((\<lambda>x. - x) ` s)"
proof -
- have "linear (\<lambda>x. - x)" by (simp add: linearI)
- then show ?thesis using `convex s` by (rule convex_linear_image)
+ have "linear (\<lambda>x. - x)"
+ by (simp add: linearI)
+ then show ?thesis
+ using `convex s` by (rule convex_linear_image)
qed
lemma convex_sums:
- assumes "convex s" and "convex t"
+ assumes "convex s"
+ and "convex t"
shows "convex {x + y| x y. x \<in> s \<and> y \<in> t}"
proof -
have "linear (\<lambda>(x, y). x + y)"
@@ -362,7 +424,8 @@
assumes "convex s"
shows "convex ((\<lambda>x. a + x) ` s)"
proof -
- have "{a + y |y. y \<in> s} = (\<lambda>x. a + x) ` s" by auto
+ have "{a + y |y. y \<in> s} = (\<lambda>x. a + x) ` s"
+ by auto
then show ?thesis
using convex_sums[OF convex_singleton[of a] assms] by auto
qed
@@ -371,7 +434,8 @@
assumes "convex s"
shows "convex ((\<lambda>x. a + c *\<^sub>R x) ` s)"
proof -
- have "(\<lambda>x. a + c *\<^sub>R x) ` s = op + a ` op *\<^sub>R c ` s" by auto
+ have "(\<lambda>x. a + c *\<^sub>R x) ` s = op + a ` op *\<^sub>R c ` s"
+ by auto
then show ?thesis
using convex_translation[OF convex_scaling[OF assms], of a c] by auto
qed
@@ -381,18 +445,25 @@
proof safe
fix y x \<mu> :: real
assume asms: "y > 0" "x > 0" "\<mu> \<ge> 0" "\<mu> \<le> 1"
- { assume "\<mu> = 0"
+ {
+ assume "\<mu> = 0"
then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y = y" by simp
- then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms by simp }
+ then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms by simp
+ }
moreover
- { assume "\<mu> = 1"
- then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms by simp }
+ {
+ assume "\<mu> = 1"
+ then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms by simp
+ }
moreover
- { assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
+ {
+ assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
then have "\<mu> > 0" "(1 - \<mu>) > 0" using asms by auto
then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms
- by (auto simp add: add_pos_pos) }
- ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0" using assms by fastforce
+ by (auto simp add: add_pos_pos)
+ }
+ ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0"
+ using assms by fastforce
qed
lemma convex_on_setsum:
@@ -415,25 +486,32 @@
case (insert i s) note asms = this
then have "convex_on C f" by simp
from this[unfolded convex_on_def, rule_format]
- have conv: "\<And>x y \<mu>. x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> 0 \<le> \<mu> \<Longrightarrow> \<mu> \<le> 1
- \<Longrightarrow> f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
+ have conv: "\<And>x y \<mu>. x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> 0 \<le> \<mu> \<Longrightarrow> \<mu> \<le> 1 \<Longrightarrow>
+ f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
by simp
- { assume "a i = 1"
+ {
+ assume "a i = 1"
then have "(\<Sum> j \<in> s. a j) = 0"
using asms by auto
then have "\<And>j. j \<in> s \<Longrightarrow> a j = 0"
using setsum_nonneg_0[where 'b=real] asms by fastforce
- then have ?case using asms by auto }
+ then have ?case using asms by auto
+ }
moreover
- { assume asm: "a i \<noteq> 1"
+ {
+ assume asm: "a i \<noteq> 1"
from asms have yai: "y i \<in> C" "a i \<ge> 0" by auto
have fis: "finite (insert i s)" using asms by auto
then have ai1: "a i \<le> 1" using setsum_nonneg_leq_bound[of "insert i s" a] asms by simp
then have "a i < 1" using asm by auto
then have i0: "1 - a i > 0" by auto
let ?a = "\<lambda>j. a j / (1 - a i)"
- { fix j assume "j \<in> s" with i0 asms have "?a j \<ge> 0"
- by fastforce }
+ {
+ fix j
+ assume "j \<in> s"
+ with i0 asms have "?a j \<ge> 0"
+ by fastforce
+ }
note a_nonneg = this
have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
then have "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastforce
@@ -466,51 +544,66 @@
also have "\<dots> = (\<Sum> j \<in> s. a j * f (y j)) + a i * f (y i)" using i0 by auto
also have "\<dots> = (\<Sum> j \<in> insert i s. a j * f (y j))" using asms by auto
finally have "f (\<Sum> j \<in> insert i s. a j *\<^sub>R y j) \<le> (\<Sum> j \<in> insert i s. a j * f (y j))"
- by simp }
+ by simp
+ }
ultimately show ?case by auto
qed
lemma convex_on_alt:
fixes C :: "'a::real_vector set"
assumes "convex C"
- shows "convex_on C f =
- (\<forall> x \<in> C. \<forall> y \<in> C. \<forall> \<mu> :: real. \<mu> \<ge> 0 \<and> \<mu> \<le> 1
- \<longrightarrow> f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y)"
+ shows "convex_on C f \<longleftrightarrow>
+ (\<forall>x \<in> C. \<forall> y \<in> C. \<forall> \<mu> :: real. \<mu> \<ge> 0 \<and> \<mu> \<le> 1 \<longrightarrow>
+ f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y)"
proof safe
fix x y
fix \<mu> :: real
assume asms: "convex_on C f" "x \<in> C" "y \<in> C" "0 \<le> \<mu>" "\<mu> \<le> 1"
from this[unfolded convex_on_def, rule_format]
- have "\<And>u v. \<lbrakk>0 \<le> u; 0 \<le> v; u + v = 1\<rbrakk> \<Longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y" by auto
+ have "\<And>u v. 0 \<le> u \<Longrightarrow> 0 \<le> v \<Longrightarrow> u + v = 1 \<Longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y"
+ by auto
from this[of "\<mu>" "1 - \<mu>", simplified] asms
- show "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y" by auto
+ show "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
+ by auto
next
- assume asm: "\<forall>x\<in>C. \<forall>y\<in>C. \<forall>\<mu>. 0 \<le> \<mu> \<and> \<mu> \<le> 1 \<longrightarrow> f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
- { fix x y
+ assume asm: "\<forall>x\<in>C. \<forall>y\<in>C. \<forall>\<mu>. 0 \<le> \<mu> \<and> \<mu> \<le> 1 \<longrightarrow>
+ f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
+ {
+ fix x y
fix u v :: real
assume lasm: "x \<in> C" "y \<in> C" "u \<ge> 0" "v \<ge> 0" "u + v = 1"
then have[simp]: "1 - u = v" by auto
from asm[rule_format, of x y u]
- have "f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y" using lasm by auto
+ have "f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y"
+ using lasm by auto
}
- then show "convex_on C f" unfolding convex_on_def by auto
+ then show "convex_on C f"
+ unfolding convex_on_def by auto
qed
lemma convex_on_diff:
fixes f :: "real \<Rightarrow> real"
- assumes f: "convex_on I f" and I: "x\<in>I" "y\<in>I" and t: "x < t" "t < y"
+ assumes f: "convex_on I f"
+ and I: "x \<in> I" "y \<in> I"
+ and t: "x < t" "t < y"
shows "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
- "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
+ and "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
proof -
def a \<equiv> "(t - y) / (x - y)"
- with t have "0 \<le> a" "0 \<le> 1 - a" by (auto simp: field_simps)
+ with t have "0 \<le> a" "0 \<le> 1 - a"
+ by (auto simp: field_simps)
with f `x \<in> I` `y \<in> I` have cvx: "f (a * x + (1 - a) * y) \<le> a * f x + (1 - a) * f y"
by (auto simp: convex_on_def)
- have "a * x + (1 - a) * y = a * (x - y) + y" by (simp add: field_simps)
- also have "\<dots> = t" unfolding a_def using `x < t` `t < y` by simp
- finally have "f t \<le> a * f x + (1 - a) * f y" using cvx by simp
- also have "\<dots> = a * (f x - f y) + f y" by (simp add: field_simps)
- finally have "f t - f y \<le> a * (f x - f y)" by simp
+ have "a * x + (1 - a) * y = a * (x - y) + y"
+ by (simp add: field_simps)
+ also have "\<dots> = t"
+ unfolding a_def using `x < t` `t < y` by simp
+ finally have "f t \<le> a * f x + (1 - a) * f y"
+ using cvx by simp
+ also have "\<dots> = a * (f x - f y) + f y"
+ by (simp add: field_simps)
+ finally have "f t - f y \<le> a * (f x - f y)"
+ by simp
with t show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
by (simp add: le_divide_eq divide_le_eq field_simps a_def)
with t show "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
@@ -520,7 +613,7 @@
lemma pos_convex_function:
fixes f :: "real \<Rightarrow> real"
assumes "convex C"
- and leq: "\<And>x y. \<lbrakk>x \<in> C ; y \<in> C\<rbrakk> \<Longrightarrow> f' x * (y - x) \<le> f y - f x"
+ and leq: "\<And>x y. x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> f' x * (y - x) \<le> f y - f x"
shows "convex_on C f"
unfolding convex_on_alt[OF assms(1)]
using assms
@@ -529,11 +622,13 @@
let ?x = "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y"
assume asm: "convex C" "x \<in> C" "y \<in> C" "\<mu> \<ge> 0" "\<mu> \<le> 1"
then have "1 - \<mu> \<ge> 0" by auto
- then have xpos: "?x \<in> C" using asm unfolding convex_alt by fastforce
- have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x)
- \<ge> \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
+ then have xpos: "?x \<in> C"
+ using asm unfolding convex_alt by fastforce
+ have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x) \<ge>
+ \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
using add_mono[OF mult_left_mono[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
- mult_left_mono[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto
+ mult_left_mono[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]]
+ by auto
then have "\<mu> * f x + (1 - \<mu>) * f y - f ?x \<ge> 0"
by (auto simp add: field_simps)
then show "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
@@ -547,9 +642,11 @@
shows "{x .. y} \<subseteq> C"
proof safe
fix z assume zasm: "z \<in> {x .. y}"
- { assume asm: "x < z" "z < y"
+ {
+ assume asm: "x < z" "z < y"
let ?\<mu> = "(y - z) / (y - x)"
- have "0 \<le> ?\<mu>" "?\<mu> \<le> 1" using assms asm by (auto simp add: field_simps)
+ have "0 \<le> ?\<mu>" "?\<mu> \<le> 1"
+ using assms asm by (auto simp add: field_simps)
then have comb: "?\<mu> * x + (1 - ?\<mu>) * y \<in> C"
using assms iffD1[OF convex_alt, rule_format, of C y x ?\<mu>]
by (simp add: algebra_simps)
@@ -560,7 +657,8 @@
also have "\<dots> = z"
using assms by (auto simp: field_simps)
finally have "z \<in> C"
- using comb by auto }
+ using comb by auto
+ }
note less = this
show "z \<in> C" using zasm less assms
unfolding atLeastAtMost_iff le_less by auto
@@ -576,7 +674,8 @@
shows "f' x * (y - x) \<le> f y - f x"
using assms
proof -
- { fix x y :: real
+ {
+ fix x y :: real
assume asm: "x \<in> C" "y \<in> C" "y > x"
then have ge: "y - x > 0" "y - x \<ge> 0" by auto
from asm have le: "x - y < 0" "x - y \<le> 0" by auto
@@ -627,14 +726,18 @@
then have "f y - f x - f' x * (y - x) \<ge> 0" using ge by auto
then have "f y - f x \<ge> f' x * (y - x)" "f' y * (x - y) \<le> f x - f y"
using res by auto } note less_imp = this
- { fix x y :: real
+ {
+ fix x y :: real
assume "x \<in> C" "y \<in> C" "x \<noteq> y"
then have"f y - f x \<ge> f' x * (y - x)"
- unfolding neq_iff using less_imp by auto } note neq_imp = this
+ unfolding neq_iff using less_imp by auto
+ }
moreover
- { fix x y :: real
+ {
+ fix x y :: real
assume asm: "x \<in> C" "y \<in> C" "x = y"
- then have "f y - f x \<ge> f' x * (y - x)" by auto }
+ then have "f y - f x \<ge> f' x * (y - x)" by auto
+ }
ultimately show ?thesis using assms by blast
qed
@@ -645,14 +748,16 @@
and f'': "\<And>x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
and pos: "\<And>x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
shows "convex_on C f"
-using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function by fastforce
+ using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function
+ by fastforce
lemma minus_log_convex:
fixes b :: real
assumes "b > 1"
shows "convex_on {0 <..} (\<lambda> x. - log b x)"
proof -
- have "\<And>z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)" using DERIV_log by auto
+ have "\<And>z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)"
+ using DERIV_log by auto
then have f': "\<And>z. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - log b z) z :> - 1 / (ln b * z)"
by (auto simp: DERIV_minus)
have "\<And>z :: real. z > 0 \<Longrightarrow> DERIV inverse z :> - (inverse z ^ Suc (Suc 0))"
@@ -661,9 +766,10 @@
have "\<And>z :: real. z > 0 \<Longrightarrow>
DERIV (\<lambda> z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))"
by auto
- then have f''0: "\<And>z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
+ then have f''0: "\<And>z::real. z > 0 \<Longrightarrow>
+ DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
unfolding inverse_eq_divide by (auto simp add: mult_assoc)
- have f''_ge0: "\<And>z :: real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
+ have f''_ge0: "\<And>z::real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
using `b > 1` by (auto intro!:less_imp_le)
from f''_ge0_imp_convex[OF pos_is_convex,
unfolded greaterThan_iff, OF f' f''0 f''_ge0]
--- a/src/HOL/Library/Finite_Lattice.thy Tue Apr 29 21:54:26 2014 +0200
+++ b/src/HOL/Library/Finite_Lattice.thy Tue Apr 29 22:50:55 2014 +0200
@@ -1,4 +1,6 @@
-(* Author: Alessandro Coglio *)
+(* Title: HOL/Library/Finite_Lattice.thy
+ Author: Alessandro Coglio
+*)
theory Finite_Lattice
imports Product_Order
@@ -16,29 +18,27 @@
The resulting class is a subclass of @{class complete_lattice}. *}
class finite_lattice_complete = finite + lattice + bot + top + Inf + Sup +
-assumes bot_def: "bot = Inf_fin UNIV"
-assumes top_def: "top = Sup_fin UNIV"
-assumes Inf_def: "Inf A = Finite_Set.fold inf top A"
-assumes Sup_def: "Sup A = Finite_Set.fold sup bot A"
+ assumes bot_def: "bot = Inf_fin UNIV"
+ assumes top_def: "top = Sup_fin UNIV"
+ assumes Inf_def: "Inf A = Finite_Set.fold inf top A"
+ assumes Sup_def: "Sup A = Finite_Set.fold sup bot A"
text {* The definitional assumptions
on the operators @{const bot} and @{const top}
of class @{class finite_lattice_complete}
ensure that they yield bottom and top. *}
-lemma finite_lattice_complete_bot_least:
-"(bot::'a::finite_lattice_complete) \<le> x"
-by (auto simp: bot_def intro: Inf_fin.coboundedI)
+lemma finite_lattice_complete_bot_least: "(bot::'a::finite_lattice_complete) \<le> x"
+ by (auto simp: bot_def intro: Inf_fin.coboundedI)
instance finite_lattice_complete \<subseteq> order_bot
-proof qed (auto simp: finite_lattice_complete_bot_least)
+ by default (auto simp: finite_lattice_complete_bot_least)
-lemma finite_lattice_complete_top_greatest:
-"(top::'a::finite_lattice_complete) \<ge> x"
-by (auto simp: top_def Sup_fin.coboundedI)
+lemma finite_lattice_complete_top_greatest: "(top::'a::finite_lattice_complete) \<ge> x"
+ by (auto simp: top_def Sup_fin.coboundedI)
instance finite_lattice_complete \<subseteq> order_top
-proof qed (auto simp: finite_lattice_complete_top_greatest)
+ by default (auto simp: finite_lattice_complete_top_greatest)
instance finite_lattice_complete \<subseteq> bounded_lattice ..
@@ -47,19 +47,18 @@
of class @{class finite_lattice_complete}
ensure that they yield infimum and supremum. *}
-lemma finite_lattice_complete_Inf_empty:
- "Inf {} = (top :: 'a::finite_lattice_complete)"
+lemma finite_lattice_complete_Inf_empty: "Inf {} = (top :: 'a::finite_lattice_complete)"
by (simp add: Inf_def)
-lemma finite_lattice_complete_Sup_empty:
- "Sup {} = (bot :: 'a::finite_lattice_complete)"
+lemma finite_lattice_complete_Sup_empty: "Sup {} = (bot :: 'a::finite_lattice_complete)"
by (simp add: Sup_def)
lemma finite_lattice_complete_Inf_insert:
fixes A :: "'a::finite_lattice_complete set"
shows "Inf (insert x A) = inf x (Inf A)"
proof -
- interpret comp_fun_idem "inf :: 'a \<Rightarrow> _" by (fact comp_fun_idem_inf)
+ interpret comp_fun_idem "inf :: 'a \<Rightarrow> _"
+ by (fact comp_fun_idem_inf)
show ?thesis by (simp add: Inf_def)
qed
@@ -67,87 +66,87 @@
fixes A :: "'a::finite_lattice_complete set"
shows "Sup (insert x A) = sup x (Sup A)"
proof -
- interpret comp_fun_idem "sup :: 'a \<Rightarrow> _" by (fact comp_fun_idem_sup)
+ interpret comp_fun_idem "sup :: 'a \<Rightarrow> _"
+ by (fact comp_fun_idem_sup)
show ?thesis by (simp add: Sup_def)
qed
lemma finite_lattice_complete_Inf_lower:
"(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Inf A \<le> x"
- using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_insert intro: le_infI2)
+ using finite [of A]
+ by (induct A) (auto simp add: finite_lattice_complete_Inf_insert intro: le_infI2)
lemma finite_lattice_complete_Inf_greatest:
"\<forall>x::'a::finite_lattice_complete \<in> A. z \<le> x \<Longrightarrow> z \<le> Inf A"
- using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_empty finite_lattice_complete_Inf_insert)
+ using finite [of A]
+ by (induct A) (auto simp add: finite_lattice_complete_Inf_empty finite_lattice_complete_Inf_insert)
lemma finite_lattice_complete_Sup_upper:
"(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Sup A \<ge> x"
- using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Sup_insert intro: le_supI2)
+ using finite [of A]
+ by (induct A) (auto simp add: finite_lattice_complete_Sup_insert intro: le_supI2)
lemma finite_lattice_complete_Sup_least:
"\<forall>x::'a::finite_lattice_complete \<in> A. z \<ge> x \<Longrightarrow> z \<ge> Sup A"
- using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Sup_empty finite_lattice_complete_Sup_insert)
+ using finite [of A]
+ by (induct A) (auto simp add: finite_lattice_complete_Sup_empty finite_lattice_complete_Sup_insert)
instance finite_lattice_complete \<subseteq> complete_lattice
proof
qed (auto simp:
- finite_lattice_complete_Inf_lower
- finite_lattice_complete_Inf_greatest
- finite_lattice_complete_Sup_upper
- finite_lattice_complete_Sup_least
- finite_lattice_complete_Inf_empty
- finite_lattice_complete_Sup_empty)
+ finite_lattice_complete_Inf_lower
+ finite_lattice_complete_Inf_greatest
+ finite_lattice_complete_Sup_upper
+ finite_lattice_complete_Sup_least
+ finite_lattice_complete_Inf_empty
+ finite_lattice_complete_Sup_empty)
text {* The product of two finite lattices is already a finite lattice. *}
lemma finite_bot_prod:
"(bot :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) =
- Inf_fin UNIV"
-by (metis Inf_fin.coboundedI UNIV_I bot.extremum_uniqueI finite_UNIV)
+ Inf_fin UNIV"
+ by (metis Inf_fin.coboundedI UNIV_I bot.extremum_uniqueI finite_UNIV)
lemma finite_top_prod:
"(top :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) =
- Sup_fin UNIV"
-by (metis Sup_fin.coboundedI UNIV_I top.extremum_uniqueI finite_UNIV)
+ Sup_fin UNIV"
+ by (metis Sup_fin.coboundedI UNIV_I top.extremum_uniqueI finite_UNIV)
lemma finite_Inf_prod:
"Inf(A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
- Finite_Set.fold inf top A"
-by (metis Inf_fold_inf finite_code)
+ Finite_Set.fold inf top A"
+ by (metis Inf_fold_inf finite_code)
lemma finite_Sup_prod:
"Sup (A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
- Finite_Set.fold sup bot A"
-by (metis Sup_fold_sup finite_code)
+ Finite_Set.fold sup bot A"
+ by (metis Sup_fold_sup finite_code)
-instance prod ::
- (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
-proof
-qed (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
+instance prod :: (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
+ by default (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
text {* Functions with a finite domain and with a finite lattice as codomain
already form a finite lattice. *}
-lemma finite_bot_fun:
- "(bot :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Inf_fin UNIV"
-by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite_code)
+lemma finite_bot_fun: "(bot :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Inf_fin UNIV"
+ by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite_code)
-lemma finite_top_fun:
- "(top :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Sup_fin UNIV"
-by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite_code)
+lemma finite_top_fun: "(top :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Sup_fin UNIV"
+ by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite_code)
lemma finite_Inf_fun:
"Inf (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
- Finite_Set.fold inf top A"
-by (metis Inf_fold_inf finite_code)
+ Finite_Set.fold inf top A"
+ by (metis Inf_fold_inf finite_code)
lemma finite_Sup_fun:
"Sup (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
- Finite_Set.fold sup bot A"
-by (metis Sup_fold_sup finite_code)
+ Finite_Set.fold sup bot A"
+ by (metis Sup_fold_sup finite_code)
instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
-proof
-qed (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
+ by default (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
subsection {* Finite Distributive Lattices *}
@@ -161,22 +160,22 @@
lemma finite_distrib_lattice_complete_sup_Inf:
"sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y:A. sup x y)"
- using finite by (induct A rule: finite_induct)
- (simp_all add: sup_inf_distrib1)
+ using finite
+ by (induct A rule: finite_induct) (simp_all add: sup_inf_distrib1)
lemma finite_distrib_lattice_complete_inf_Sup:
"inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)"
-apply (rule finite_induct)
-apply (metis finite_code)
-apply (metis SUP_empty Sup_empty inf_bot_right)
-apply (metis SUP_insert Sup_insert inf_sup_distrib1)
-done
+ apply (rule finite_induct)
+ apply (metis finite_code)
+ apply (metis SUP_empty Sup_empty inf_bot_right)
+ apply (metis SUP_insert Sup_insert inf_sup_distrib1)
+ done
instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice
proof
qed (auto simp:
- finite_distrib_lattice_complete_sup_Inf
- finite_distrib_lattice_complete_inf_Sup)
+ finite_distrib_lattice_complete_sup_Inf
+ finite_distrib_lattice_complete_inf_Sup)
text {* The product of two finite distributive lattices
is already a finite distributive lattice. *}
@@ -184,7 +183,7 @@
instance prod ::
(finite_distrib_lattice_complete, finite_distrib_lattice_complete)
finite_distrib_lattice_complete
-..
+ ..
text {* Functions with a finite domain
and with a finite distributive lattice as codomain
@@ -192,7 +191,7 @@
instance "fun" ::
(finite, finite_distrib_lattice_complete) finite_distrib_lattice_complete
-..
+ ..
subsection {* Linear Orders *}
@@ -206,8 +205,8 @@
The resulting class is a subclass of @{class distrib_lattice}. *}
class linorder_lattice = linorder + inf + sup +
-assumes inf_def: "inf x y = (if x \<le> y then x else y)"
-assumes sup_def: "sup x y = (if x \<ge> y then x else y)"
+ assumes inf_def: "inf x y = (if x \<le> y then x else y)"
+ assumes sup_def: "sup x y = (if x \<ge> y then x else y)"
text {* The definitional assumptions
on the operators @{const inf} and @{const sup}
@@ -216,39 +215,39 @@
and that they distribute over each other. *}
lemma linorder_lattice_inf_le1: "inf (x::'a::linorder_lattice) y \<le> x"
-unfolding inf_def by (metis (full_types) linorder_linear)
+ unfolding inf_def by (metis (full_types) linorder_linear)
lemma linorder_lattice_inf_le2: "inf (x::'a::linorder_lattice) y \<le> y"
-unfolding inf_def by (metis (full_types) linorder_linear)
+ unfolding inf_def by (metis (full_types) linorder_linear)
lemma linorder_lattice_inf_greatest:
"(x::'a::linorder_lattice) \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> inf y z"
-unfolding inf_def by (metis (full_types))
+ unfolding inf_def by (metis (full_types))
lemma linorder_lattice_sup_ge1: "sup (x::'a::linorder_lattice) y \<ge> x"
-unfolding sup_def by (metis (full_types) linorder_linear)
+ unfolding sup_def by (metis (full_types) linorder_linear)
lemma linorder_lattice_sup_ge2: "sup (x::'a::linorder_lattice) y \<ge> y"
-unfolding sup_def by (metis (full_types) linorder_linear)
+ unfolding sup_def by (metis (full_types) linorder_linear)
lemma linorder_lattice_sup_least:
"(x::'a::linorder_lattice) \<ge> y \<Longrightarrow> x \<ge> z \<Longrightarrow> x \<ge> sup y z"
-by (auto simp: sup_def)
+ by (auto simp: sup_def)
lemma linorder_lattice_sup_inf_distrib1:
"sup (x::'a::linorder_lattice) (inf y z) = inf (sup x y) (sup x z)"
-by (auto simp: inf_def sup_def)
-
+ by (auto simp: inf_def sup_def)
+
instance linorder_lattice \<subseteq> distrib_lattice
-proof
+proof
qed (auto simp:
- linorder_lattice_inf_le1
- linorder_lattice_inf_le2
- linorder_lattice_inf_greatest
- linorder_lattice_sup_ge1
- linorder_lattice_sup_ge2
- linorder_lattice_sup_least
- linorder_lattice_sup_inf_distrib1)
+ linorder_lattice_inf_le1
+ linorder_lattice_inf_le2
+ linorder_lattice_inf_greatest
+ linorder_lattice_sup_ge1
+ linorder_lattice_sup_ge2
+ linorder_lattice_sup_least
+ linorder_lattice_sup_inf_distrib1)
subsection {* Finite Linear Orders *}
@@ -265,6 +264,5 @@
instance finite_linorder_complete \<subseteq> finite_distrib_lattice_complete ..
-
end
--- a/src/HOL/Library/Permutation.thy Tue Apr 29 21:54:26 2014 +0200
+++ b/src/HOL/Library/Permutation.thy Tue Apr 29 22:50:55 2014 +0200
@@ -22,12 +22,10 @@
subsection {* Some examples of rule induction on permutations *}
lemma xperm_empty_imp: "[] <~~> ys \<Longrightarrow> ys = []"
- by (induct xs == "[]::'a list" ys pred: perm) simp_all
+ by (induct xs == "[] :: 'a list" ys pred: perm) simp_all
-text {*
- \medskip This more general theorem is easier to understand!
- *}
+text {* \medskip This more general theorem is easier to understand! *}
lemma perm_length: "xs <~~> ys \<Longrightarrow> length xs = length ys"
by (induct pred: perm) simp_all
@@ -41,9 +39,7 @@
subsection {* Ways of making new permutations *}
-text {*
- We can insert the head anywhere in the list.
-*}
+text {* We can insert the head anywhere in the list. *}
lemma perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys"
by (induct xs) auto
@@ -72,10 +68,10 @@
subsection {* Further results *}
-lemma perm_empty [iff]: "([] <~~> xs) = (xs = [])"
+lemma perm_empty [iff]: "[] <~~> xs \<longleftrightarrow> xs = []"
by (blast intro: perm_empty_imp)
-lemma perm_empty2 [iff]: "(xs <~~> []) = (xs = [])"
+lemma perm_empty2 [iff]: "xs <~~> [] \<longleftrightarrow> xs = []"
apply auto
apply (erule perm_sym [THEN perm_empty_imp])
done
@@ -83,10 +79,10 @@
lemma perm_sing_imp: "ys <~~> xs \<Longrightarrow> xs = [y] \<Longrightarrow> ys = [y]"
by (induct pred: perm) auto
-lemma perm_sing_eq [iff]: "(ys <~~> [y]) = (ys = [y])"
+lemma perm_sing_eq [iff]: "ys <~~> [y] \<longleftrightarrow> ys = [y]"
by (blast intro: perm_sing_imp)
-lemma perm_sing_eq2 [iff]: "([y] <~~> ys) = (ys = [y])"
+lemma perm_sing_eq2 [iff]: "[y] <~~> ys \<longleftrightarrow> ys = [y]"
by (blast dest: perm_sym)
@@ -107,16 +103,16 @@
lemma cons_perm_imp_perm: "z # xs <~~> z # ys \<Longrightarrow> xs <~~> ys"
by (drule_tac z = z in perm_remove_perm) auto
-lemma cons_perm_eq [iff]: "(z#xs <~~> z#ys) = (xs <~~> ys)"
+lemma cons_perm_eq [iff]: "z#xs <~~> z#ys \<longleftrightarrow> xs <~~> ys"
by (blast intro: cons_perm_imp_perm)
lemma append_perm_imp_perm: "zs @ xs <~~> zs @ ys \<Longrightarrow> xs <~~> ys"
by (induct zs arbitrary: xs ys rule: rev_induct) auto
-lemma perm_append1_eq [iff]: "(zs @ xs <~~> zs @ ys) = (xs <~~> ys)"
+lemma perm_append1_eq [iff]: "zs @ xs <~~> zs @ ys \<longleftrightarrow> xs <~~> ys"
by (blast intro: append_perm_imp_perm perm_append1)
-lemma perm_append2_eq [iff]: "(xs @ zs <~~> ys @ zs) = (xs <~~> ys)"
+lemma perm_append2_eq [iff]: "xs @ zs <~~> ys @ zs \<longleftrightarrow> xs <~~> ys"
apply (safe intro!: perm_append2)
apply (rule append_perm_imp_perm)
apply (rule perm_append_swap [THEN perm.trans])
@@ -124,21 +120,30 @@
apply (blast intro: perm_append_swap)
done
-lemma multiset_of_eq_perm: "(multiset_of xs = multiset_of ys) = (xs <~~> ys) "
+lemma multiset_of_eq_perm: "multiset_of xs = multiset_of ys \<longleftrightarrow> xs <~~> ys"
apply (rule iffI)
- apply (erule_tac [2] perm.induct, simp_all add: union_ac)
- apply (erule rev_mp, rule_tac x=ys in spec)
- apply (induct_tac xs, auto)
- apply (erule_tac x = "remove1 a x" in allE, drule sym, simp)
+ apply (erule_tac [2] perm.induct)
+ apply (simp_all add: union_ac)
+ apply (erule rev_mp)
+ apply (rule_tac x=ys in spec)
+ apply (induct_tac xs)
+ apply auto
+ apply (erule_tac x = "remove1 a x" in allE)
+ apply (drule sym)
+ apply simp
apply (subgoal_tac "a \<in> set x")
apply (drule_tac z = a in perm.Cons)
- apply (erule perm.trans, rule perm_sym, erule perm_remove)
- apply (drule_tac f=set_of in arg_cong, simp)
+ apply (erule perm.trans)
+ apply (rule perm_sym)
+ apply (erule perm_remove)
+ apply (drule_tac f=set_of in arg_cong)
+ apply simp
done
lemma multiset_of_le_perm_append: "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
- apply (insert surj_multiset_of, drule surjD)
+ apply (insert surj_multiset_of)
+ apply (drule surjD)
apply (blast intro: sym)+
done
@@ -158,15 +163,16 @@
apply simp_all
apply (subgoal_tac "a \<in> set (remdups ys)")
prefer 2 apply (metis set_simps(2) insert_iff set_remdups)
- apply (drule split_list) apply(elim exE conjE)
- apply (drule_tac x=list in spec) apply(erule impE) prefer 2
- apply (drule_tac x="ysa@zs" in spec) apply(erule impE) prefer 2
+ apply (drule split_list) apply (elim exE conjE)
+ apply (drule_tac x = list in spec) apply (erule impE) prefer 2
+ apply (drule_tac x = "ysa @ zs" in spec) apply (erule impE) prefer 2
apply simp
apply (subgoal_tac "a # list <~~> a # ysa @ zs")
apply (metis Cons_eq_appendI perm_append_Cons trans)
apply (metis Cons Cons_eq_appendI distinct.simps(2)
distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
- apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
+ apply (subgoal_tac "set (a # list) =
+ set (ysa @ a # zs) \<and> distinct (a # list) \<and> distinct (ysa @ a # zs)")
apply (fastforce simp add: insert_ident)
apply (metis distinct_remdups set_remdups)
apply (subgoal_tac "length (remdups xs) < Suc (length xs)")
@@ -176,15 +182,17 @@
apply (rule length_remdups_leq)
done
-lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y \<longleftrightarrow> (set x = set y)"
+lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y \<longleftrightarrow> set x = set y"
by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
lemma permutation_Ex_bij:
assumes "xs <~~> ys"
shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))"
-using assms proof induct
+ using assms
+proof induct
case Nil
- then show ?case unfolding bij_betw_def by simp
+ then show ?case
+ unfolding bij_betw_def by simp
next
case (swap y x l)
show ?case
@@ -192,14 +200,15 @@
show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}"
by (auto simp: bij_betw_def)
fix i
- assume "i < length(y#x#l)"
+ assume "i < length (y # x # l)"
show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i"
by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc)
qed
next
case (Cons xs ys z)
- then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}" and
- perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" by blast
+ then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}"
+ and perm: "\<forall>i<length xs. xs ! i = ys ! (f i)"
+ by blast
let ?f = "\<lambda>i. case i of Suc n \<Rightarrow> Suc (f n) | 0 \<Rightarrow> 0"
show ?case
proof (intro exI[of _ ?f] allI conjI impI)
@@ -214,21 +223,24 @@
by (auto intro!: inj_onI imageI dest: inj_onD simp: image_comp comp_def)
qed (auto simp: bij_betw_def)
fix i
- assume "i < length (z#xs)"
+ assume "i < length (z # xs)"
then show "(z # xs) ! i = (z # ys) ! (?f i)"
using perm by (cases i) auto
qed
next
case (trans xs ys zs)
- then obtain f g where
- bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}" and
- perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" "\<forall>i<length ys. ys ! i = zs ! (g i)" by blast
+ then obtain f g
+ where bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}"
+ and perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" "\<forall>i<length ys. ys ! i = zs ! (g i)"
+ by blast
show ?case
proof (intro exI[of _ "g \<circ> f"] conjI allI impI)
show "bij_betw (g \<circ> f) {..<length xs} {..<length zs}"
using bij by (rule bij_betw_trans)
- fix i assume "i < length xs"
- with bij have "f i < length ys" unfolding bij_betw_def by force
+ fix i
+ assume "i < length xs"
+ with bij have "f i < length ys"
+ unfolding bij_betw_def by force
with `i < length xs` show "xs ! i = zs ! (g \<circ> f) i"
using trans(1,3)[THEN perm_length] perm by auto
qed