--- a/src/HOL/Algebra/Divisibility.thy Thu Apr 19 12:34:52 2018 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Thu Apr 19 14:49:19 2018 +0100
@@ -2491,11 +2491,7 @@
have "a' \<in> carrier G \<and> a' gcdof b c"
apply (simp add: gcdof_greatestLower carr')
apply (subst greatest_Lower_cong_l[of _ a])
- apply (simp add: a'a)
- apply (simp add: carr)
- apply (simp add: carr)
- apply (simp add: carr)
- apply (simp add: gcdof_greatestLower[symmetric] agcd carr)
+ apply (simp_all add: a'a carr gcdof_greatestLower[symmetric] agcd)
done
then show ?thesis ..
qed
--- a/src/HOL/Algebra/Order.thy Thu Apr 19 12:34:52 2018 +0200
+++ b/src/HOL/Algebra/Order.thy Thu Apr 19 14:49:19 2018 +0100
@@ -31,34 +31,33 @@
locale weak_partial_order = equivalence L for L (structure) +
assumes le_refl [intro, simp]:
- "x \<in> carrier L ==> x \<sqsubseteq> x"
+ "x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> x"
and weak_le_antisym [intro]:
- "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y"
+ "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L\<rbrakk> \<Longrightarrow> x .= y"
and le_trans [trans]:
- "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
+ "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
and le_cong:
- "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow>
+ "\<lbrakk>x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L\<rbrakk> \<Longrightarrow>
x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
definition
lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
where "x \<sqsubset>\<^bsub>L\<^esub> y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> y \<and> x .\<noteq>\<^bsub>L\<^esub> y"
-
subsubsection \<open>The order relation\<close>
context weak_partial_order
begin
lemma le_cong_l [intro, trans]:
- "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
+ "\<lbrakk>x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
by (auto intro: le_cong [THEN iffD2])
lemma le_cong_r [intro, trans]:
- "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
+ "\<lbrakk>x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
by (auto intro: le_cong [THEN iffD1])
-lemma weak_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
+lemma weak_refl [intro, simp]: "\<lbrakk>x .= y; x \<in> carrier L; y \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
by (simp add: le_cong_l)
end
@@ -143,93 +142,86 @@
Lower :: "[_, 'a set] => 'a set"
where "Lower L A = {l. (\<forall>x. x \<in> A \<inter> carrier L \<longrightarrow> l \<sqsubseteq>\<^bsub>L\<^esub> x)} \<inter> carrier L"
-lemma Upper_closed [intro!, simp]:
+lemma Lower_dual [simp]:
+ "Lower (inv_gorder L) A = Upper L A"
+ by (simp add:Upper_def Lower_def)
+
+lemma Upper_dual [simp]:
+ "Upper (inv_gorder L) A = Lower L A"
+ by (simp add:Upper_def Lower_def)
+
+lemma (in weak_partial_order) equivalence_dual: "equivalence (inv_gorder L)"
+ by (rule equivalence.intro) (auto simp: intro: sym trans)
+
+lemma (in weak_partial_order) dual_weak_order: "weak_partial_order (inv_gorder L)"
+ by intro_locales (auto simp add: weak_partial_order_axioms_def le_cong intro: equivalence_dual le_trans)
+
+lemma (in weak_partial_order) dual_eq_iff [simp]: "A {.=}\<^bsub>inv_gorder L\<^esub> A' \<longleftrightarrow> A {.=} A'"
+ by (auto simp: set_eq_def elem_def)
+
+lemma dual_weak_order_iff:
+ "weak_partial_order (inv_gorder A) \<longleftrightarrow> weak_partial_order A"
+proof
+ assume "weak_partial_order (inv_gorder A)"
+ then interpret dpo: weak_partial_order "inv_gorder A"
+ rewrites "carrier (inv_gorder A) = carrier A"
+ and "le (inv_gorder A) = (\<lambda> x y. le A y x)"
+ and "eq (inv_gorder A) = eq A"
+ by (simp_all)
+ show "weak_partial_order A"
+ by (unfold_locales, auto intro: dpo.sym dpo.trans dpo.le_trans)
+next
+ assume "weak_partial_order A"
+ thus "weak_partial_order (inv_gorder A)"
+ by (metis weak_partial_order.dual_weak_order)
+qed
+
+lemma Upper_closed [iff]:
"Upper L A \<subseteq> carrier L"
by (unfold Upper_def) clarify
lemma Upper_memD [dest]:
fixes L (structure)
- shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u \<and> u \<in> carrier L"
+ shows "\<lbrakk>u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u \<and> u \<in> carrier L"
by (unfold Upper_def) blast
lemma (in weak_partial_order) Upper_elemD [dest]:
- "[| u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
+ "\<lbrakk>u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u"
unfolding Upper_def elem_def
by (blast dest: sym)
lemma Upper_memI:
fixes L (structure)
- shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
+ shows "\<lbrakk>!! y. y \<in> A \<Longrightarrow> y \<sqsubseteq> x; x \<in> carrier L\<rbrakk> \<Longrightarrow> x \<in> Upper L A"
by (unfold Upper_def) blast
lemma (in weak_partial_order) Upper_elemI:
- "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x .\<in> Upper L A"
+ "\<lbrakk>!! y. y \<in> A \<Longrightarrow> y \<sqsubseteq> x; x \<in> carrier L\<rbrakk> \<Longrightarrow> x .\<in> Upper L A"
unfolding Upper_def by blast
lemma Upper_antimono:
- "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
+ "A \<subseteq> B \<Longrightarrow> Upper L B \<subseteq> Upper L A"
by (unfold Upper_def) blast
lemma (in weak_partial_order) Upper_is_closed [simp]:
- "A \<subseteq> carrier L ==> is_closed (Upper L A)"
+ "A \<subseteq> carrier L \<Longrightarrow> is_closed (Upper L A)"
by (rule is_closedI) (blast intro: Upper_memI)+
lemma (in weak_partial_order) Upper_mem_cong:
- assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
- and aa': "a .= a'"
- and aelem: "a \<in> Upper L A"
+ assumes "a' \<in> carrier L" "A \<subseteq> carrier L" "a .= a'" "a \<in> Upper L A"
shows "a' \<in> Upper L A"
-proof (rule Upper_memI[OF _ a'carr])
- fix y
- assume yA: "y \<in> A"
- hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr)
- also note aa'
- finally
- show "y \<sqsubseteq> a'"
- by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem])
-qed
+ by (metis assms Upper_closed Upper_is_closed closure_of_eq complete_classes)
+
+lemma (in weak_partial_order) Upper_semi_cong:
+ assumes "A \<subseteq> carrier L" "A {.=} A'"
+ shows "Upper L A \<subseteq> Upper L A'"
+ unfolding Upper_def
+ by clarsimp (meson assms equivalence.refl equivalence_axioms le_cong set_eqD2 subset_eq)
lemma (in weak_partial_order) Upper_cong:
- assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
- and AA': "A {.=} A'"
+ assumes "A \<subseteq> carrier L" "A' \<subseteq> carrier L" "A {.=} A'"
shows "Upper L A = Upper L A'"
-unfolding Upper_def
-apply rule
- apply (rule, clarsimp) defer 1
- apply (rule, clarsimp) defer 1
-proof -
- fix x a'
- assume carr: "x \<in> carrier L" "a' \<in> carrier L"
- and a'A': "a' \<in> A'"
- assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x"
-
- from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
- from this obtain a
- where aA: "a \<in> A"
- and a'a: "a' .= a"
- by auto
- note [simp] = subsetD[OF Acarr aA] carr
-
- note a'a
- also have "a \<sqsubseteq> x" by (simp add: aLxCond aA)
- finally show "a' \<sqsubseteq> x" by simp
-next
- fix x a
- assume carr: "x \<in> carrier L" "a \<in> carrier L"
- and aA: "a \<in> A"
- assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x"
-
- from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
- from this obtain a'
- where a'A': "a' \<in> A'"
- and aa': "a .= a'"
- by auto
- note [simp] = subsetD[OF A'carr a'A'] carr
-
- note aa'
- also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A')
- finally show "a \<sqsubseteq> x" by simp
-qed
+ using assms by (simp add: Upper_semi_cong set_eq_sym subset_antisym)
lemma Lower_closed [intro!, simp]:
"Lower L A \<subseteq> carrier L"
@@ -237,16 +229,16 @@
lemma Lower_memD [dest]:
fixes L (structure)
- shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x \<and> l \<in> carrier L"
+ shows "\<lbrakk>l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L\<rbrakk> \<Longrightarrow> l \<sqsubseteq> x \<and> l \<in> carrier L"
by (unfold Lower_def) blast
lemma Lower_memI:
fixes L (structure)
- shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
+ shows "\<lbrakk>!! y. y \<in> A \<Longrightarrow> x \<sqsubseteq> y; x \<in> carrier L\<rbrakk> \<Longrightarrow> x \<in> Lower L A"
by (unfold Lower_def) blast
lemma Lower_antimono:
- "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
+ "A \<subseteq> B \<Longrightarrow> Lower L B \<subseteq> Lower L A"
by (unfold Lower_def) blast
lemma (in weak_partial_order) Lower_is_closed [simp]:
@@ -254,56 +246,15 @@
by (rule is_closedI) (blast intro: Lower_memI dest: sym)+
lemma (in weak_partial_order) Lower_mem_cong:
- assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
- and aa': "a .= a'"
- and aelem: "a \<in> Lower L A"
+ assumes "a' \<in> carrier L" "A \<subseteq> carrier L" "a .= a'" "a \<in> Lower L A"
shows "a' \<in> Lower L A"
-using assms Lower_closed[of L A]
-by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]])
+ by (meson assms Lower_closed Lower_is_closed is_closed_eq subsetCE)
lemma (in weak_partial_order) Lower_cong:
- assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
- and AA': "A {.=} A'"
+ assumes "A \<subseteq> carrier L" "A' \<subseteq> carrier L" "A {.=} A'"
shows "Lower L A = Lower L A'"
-unfolding Lower_def
-apply rule
- apply clarsimp defer 1
- apply clarsimp defer 1
-proof -
- fix x a'
- assume carr: "x \<in> carrier L" "a' \<in> carrier L"
- and a'A': "a' \<in> A'"
- assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a"
- hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast
-
- from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
- from this obtain a
- where aA: "a \<in> A"
- and a'a: "a' .= a"
- by auto
-
- from aA and subsetD[OF Acarr aA]
- have "x \<sqsubseteq> a" by (rule aLxCond)
- also note a'a[symmetric]
- finally
- show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA])
-next
- fix x a
- assume carr: "x \<in> carrier L" "a \<in> carrier L"
- and aA: "a \<in> A"
- assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'"
- hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+
-
- from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
- from this obtain a'
- where a'A': "a' \<in> A'"
- and aa': "a .= a'"
- by auto
- from a'A' and subsetD[OF A'carr a'A']
- have "x \<sqsubseteq> a'" by (rule a'LxCond)
- also note aa'[symmetric]
- finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A'])
-qed
+ unfolding Upper_dual [symmetric]
+ by (rule weak_partial_order.Upper_cong [OF dual_weak_order]) (simp_all add: assms)
text \<open>Jacobson: Theorem 8.1\<close>
@@ -326,29 +277,37 @@
greatest :: "[_, 'a, 'a set] => bool"
where "greatest L g A \<longleftrightarrow> A \<subseteq> carrier L \<and> g \<in> A \<and> (\<forall>x\<in>A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
-text (in weak_partial_order) \<open>Could weaken these to @{term "l \<in> carrier L \<and> l
- .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}.\<close>
+text (in weak_partial_order) \<open>Could weaken these to @{term "l \<in> carrier L \<and> l .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}.\<close>
+
+lemma least_dual [simp]:
+ "least (inv_gorder L) x A = greatest L x A"
+ by (simp add:least_def greatest_def)
+
+lemma greatest_dual [simp]:
+ "greatest (inv_gorder L) x A = least L x A"
+ by (simp add:least_def greatest_def)
lemma least_closed [intro, simp]:
- "least L l A ==> l \<in> carrier L"
+ "least L l A \<Longrightarrow> l \<in> carrier L"
by (unfold least_def) fast
lemma least_mem:
- "least L l A ==> l \<in> A"
+ "least L l A \<Longrightarrow> l \<in> A"
by (unfold least_def) fast
lemma (in weak_partial_order) weak_least_unique:
- "[| least L x A; least L y A |] ==> x .= y"
+ "\<lbrakk>least L x A; least L y A\<rbrakk> \<Longrightarrow> x .= y"
by (unfold least_def) blast
lemma least_le:
fixes L (structure)
- shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"
+ shows "\<lbrakk>least L x A; a \<in> A\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a"
by (unfold least_def) fast
lemma (in weak_partial_order) least_cong:
- "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"
- by (unfold least_def) (auto dest: sym)
+ "\<lbrakk>x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A\<rbrakk> \<Longrightarrow> least L x A = least L x' A"
+ unfolding least_def
+ by (meson is_closed_eq is_closed_eq_rev le_cong local.refl subset_iff)
abbreviation is_lub :: "[_, 'a, 'a set] => bool"
where "is_lub L x A \<equiv> least L x (Upper L A)"
@@ -364,16 +323,14 @@
apply (rule least_cong) using assms by auto
lemma (in weak_partial_order) least_Upper_cong_r:
- assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *)
- and AA': "A {.=} A'"
+ assumes "A \<subseteq> carrier L" "A' \<subseteq> carrier L" "A {.=} A'"
shows "least L x (Upper L A) = least L x (Upper L A')"
-apply (subgoal_tac "Upper L A = Upper L A'", simp)
-by (rule Upper_cong) fact+
+ using Upper_cong assms by auto
lemma least_UpperI:
fixes L (structure)
- assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
- and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
+ assumes above: "!! x. x \<in> A \<Longrightarrow> x \<sqsubseteq> s"
+ and below: "!! y. y \<in> Upper L A \<Longrightarrow> s \<sqsubseteq> y"
and L: "A \<subseteq> carrier L" "s \<in> carrier L"
shows "least L s (Upper L A)"
proof -
@@ -385,30 +342,31 @@
lemma least_Upper_above:
fixes L (structure)
- shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
+ shows "\<lbrakk>least L s (Upper L A); x \<in> A; A \<subseteq> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> s"
by (unfold least_def) blast
lemma greatest_closed [intro, simp]:
- "greatest L l A ==> l \<in> carrier L"
+ "greatest L l A \<Longrightarrow> l \<in> carrier L"
by (unfold greatest_def) fast
lemma greatest_mem:
- "greatest L l A ==> l \<in> A"
+ "greatest L l A \<Longrightarrow> l \<in> A"
by (unfold greatest_def) fast
lemma (in weak_partial_order) weak_greatest_unique:
- "[| greatest L x A; greatest L y A |] ==> x .= y"
+ "\<lbrakk>greatest L x A; greatest L y A\<rbrakk> \<Longrightarrow> x .= y"
by (unfold greatest_def) blast
lemma greatest_le:
fixes L (structure)
- shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
+ shows "\<lbrakk>greatest L x A; a \<in> A\<rbrakk> \<Longrightarrow> a \<sqsubseteq> x"
by (unfold greatest_def) fast
lemma (in weak_partial_order) greatest_cong:
- "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==>
+ "\<lbrakk>x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A\<rbrakk> \<Longrightarrow>
greatest L x A = greatest L x' A"
- by (unfold greatest_def) (auto dest: sym)
+ unfolding greatest_def
+ by (meson is_closed_eq_rev le_cong_r local.sym subset_eq)
abbreviation is_glb :: "[_, 'a, 'a set] => bool"
where "is_glb L x A \<equiv> greatest L x (Lower L A)"
@@ -419,21 +377,23 @@
lemma (in weak_partial_order) greatest_Lower_cong_l:
assumes "x .= x'"
and "x \<in> carrier L" "x' \<in> carrier L"
- and "A \<subseteq> carrier L" (* unneccessary with current Lower *)
shows "greatest L x (Lower L A) = greatest L x' (Lower L A)"
- apply (rule greatest_cong) using assms by auto
+proof -
+ have "\<forall>A. is_closed (Lower L (A \<inter> carrier L))"
+ by simp
+ then show ?thesis
+ by (simp add: Lower_def assms greatest_cong)
+qed
lemma (in weak_partial_order) greatest_Lower_cong_r:
- assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L"
- and AA': "A {.=} A'"
+ assumes "A \<subseteq> carrier L" "A' \<subseteq> carrier L" "A {.=} A'"
shows "greatest L x (Lower L A) = greatest L x (Lower L A')"
-apply (subgoal_tac "Lower L A = Lower L A'", simp)
-by (rule Lower_cong) fact+
+ using Lower_cong assms by auto
lemma greatest_LowerI:
fixes L (structure)
- assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
- and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
+ assumes below: "!! x. x \<in> A \<Longrightarrow> i \<sqsubseteq> x"
+ and above: "!! y. y \<in> Lower L A \<Longrightarrow> y \<sqsubseteq> i"
and L: "A \<subseteq> carrier L" "i \<in> carrier L"
shows "greatest L i (Lower L A)"
proof -
@@ -445,53 +405,9 @@
lemma greatest_Lower_below:
fixes L (structure)
- shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
+ shows "\<lbrakk>greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L\<rbrakk> \<Longrightarrow> i \<sqsubseteq> x"
by (unfold greatest_def) blast
-lemma Lower_dual [simp]:
- "Lower (inv_gorder L) A = Upper L A"
- by (simp add:Upper_def Lower_def)
-
-lemma Upper_dual [simp]:
- "Upper (inv_gorder L) A = Lower L A"
- by (simp add:Upper_def Lower_def)
-
-lemma least_dual [simp]:
- "least (inv_gorder L) x A = greatest L x A"
- by (simp add:least_def greatest_def)
-
-lemma greatest_dual [simp]:
- "greatest (inv_gorder L) x A = least L x A"
- by (simp add:least_def greatest_def)
-
-lemma (in weak_partial_order) dual_weak_order:
- "weak_partial_order (inv_gorder L)"
- apply (unfold_locales)
- apply (simp_all)
- apply (metis sym)
- apply (metis trans)
- apply (metis weak_le_antisym)
- apply (metis le_trans)
- apply (metis le_cong_l le_cong_r sym)
-done
-
-lemma dual_weak_order_iff:
- "weak_partial_order (inv_gorder A) \<longleftrightarrow> weak_partial_order A"
-proof
- assume "weak_partial_order (inv_gorder A)"
- then interpret dpo: weak_partial_order "inv_gorder A"
- rewrites "carrier (inv_gorder A) = carrier A"
- and "le (inv_gorder A) = (\<lambda> x y. le A y x)"
- and "eq (inv_gorder A) = eq A"
- by (simp_all)
- show "weak_partial_order A"
- by (unfold_locales, auto intro: dpo.sym dpo.trans dpo.le_trans)
-next
- assume "weak_partial_order A"
- thus "weak_partial_order (inv_gorder A)"
- by (metis weak_partial_order.dual_weak_order)
-qed
-
subsubsection \<open>Intervals\<close>
@@ -514,7 +430,7 @@
by (auto simp add: at_least_at_most_def)
lemma at_least_at_most_member [intro]:
- "\<lbrakk> x \<in> carrier L; a \<sqsubseteq> x; x \<sqsubseteq> b \<rbrakk> \<Longrightarrow> x \<in> \<lbrace>a..b\<rbrace>"
+ "\<lbrakk>x \<in> carrier L; a \<sqsubseteq> x; x \<sqsubseteq> b\<rbrakk> \<Longrightarrow> x \<in> \<lbrace>a..b\<rbrace>"
by (simp add: at_least_at_most_def)
end
@@ -532,7 +448,7 @@
fixes f :: "'a \<Rightarrow> 'b"
assumes "weak_partial_order L1"
"weak_partial_order L2"
- "(\<And>x y. \<lbrakk> x \<in> carrier L1; y \<in> carrier L1; x \<sqsubseteq>\<^bsub>L1\<^esub> y \<rbrakk>
+ "(\<And>x y. \<lbrakk>x \<in> carrier L1; y \<in> carrier L1; x \<sqsubseteq>\<^bsub>L1\<^esub> y\<rbrakk>
\<Longrightarrow> f x \<sqsubseteq>\<^bsub>L2\<^esub> f y)"
shows "isotone L1 L2 f"
using assms by (auto simp add:isotone_def)
@@ -567,7 +483,7 @@
"idempotent L f \<equiv> \<forall>x\<in>carrier L. f (f x) .=\<^bsub>L\<^esub> f x"
lemma (in weak_partial_order) idempotent:
- "\<lbrakk> Idem f; x \<in> carrier L \<rbrakk> \<Longrightarrow> f (f x) .= f x"
+ "\<lbrakk>Idem f; x \<in> carrier L\<rbrakk> \<Longrightarrow> f (f x) .= f x"
by (auto simp add: idempotent_def)
@@ -597,7 +513,7 @@
declare weak_le_antisym [rule del]
lemma le_antisym [intro]:
- "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
+ "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L\<rbrakk> \<Longrightarrow> x = y"
using weak_le_antisym unfolding eq_is_equal .
lemma lless_eq:
@@ -628,8 +544,8 @@
and "eq (inv_gorder A) = eq A"
by (simp_all)
show "partial_order A"
- apply (unfold_locales, simp_all)
- apply (metis po.sym, metis po.trans)
+ apply (unfold_locales, simp_all add: po.sym)
+ apply (metis po.trans)
apply (metis po.weak_le_antisym, metis po.le_trans)
apply (metis (full_types) po.eq_is_equal, metis po.eq_is_equal)
done
@@ -642,11 +558,11 @@
text \<open>Least and greatest, as predicate\<close>
lemma (in partial_order) least_unique:
- "[| least L x A; least L y A |] ==> x = y"
+ "\<lbrakk>least L x A; least L y A\<rbrakk> \<Longrightarrow> x = y"
using weak_least_unique unfolding eq_is_equal .
lemma (in partial_order) greatest_unique:
- "[| greatest L x A; greatest L y A |] ==> x = y"
+ "\<lbrakk>greatest L x A; greatest L y A\<rbrakk> \<Longrightarrow> x = y"
using weak_greatest_unique unfolding eq_is_equal .
@@ -710,12 +626,12 @@
subsection \<open>Total Orders\<close>
locale weak_total_order = weak_partial_order +
- assumes total: "\<lbrakk> x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
+ assumes total: "\<lbrakk>x \<in> carrier L; y \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
text \<open>Introduction rule: the usual definition of total order\<close>
lemma (in weak_partial_order) weak_total_orderI:
- assumes total: "!!x y. \<lbrakk> x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
+ assumes total: "!!x y. \<lbrakk>x \<in> carrier L; y \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
shows "weak_total_order L"
by unfold_locales (rule total)
@@ -723,7 +639,7 @@
subsection \<open>Total orders where \<open>eq\<close> is the Equality\<close>
locale total_order = partial_order +
- assumes total_order_total: "\<lbrakk> x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
+ assumes total_order_total: "\<lbrakk>x \<in> carrier L; y \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
sublocale total_order < weak?: weak_total_order
by unfold_locales (rule total_order_total)
@@ -731,7 +647,7 @@
text \<open>Introduction rule: the usual definition of total order\<close>
lemma (in partial_order) total_orderI:
- assumes total: "!!x y. \<lbrakk> x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
+ assumes total: "!!x y. \<lbrakk>x \<in> carrier L; y \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
shows "total_order L"
by unfold_locales (rule total)
--- a/src/HOL/Analysis/Fashoda_Theorem.thy Thu Apr 19 12:34:52 2018 +0200
+++ b/src/HOL/Analysis/Fashoda_Theorem.thy Thu Apr 19 14:49:19 2018 +0100
@@ -890,237 +890,4 @@
qed
qed
-(** The Following still needs to be translated. Maybe I will do that later.
-
-(* ------------------------------------------------------------------------- *)
-(* Complement in dimension N >= 2 of set homeomorphic to any interval in *)
-(* any dimension is (path-)connected. This naively generalizes the argument *)
-(* in Ryuji Maehara's paper "The Jordan curve theorem via the Brouwer *)
-(* fixed point theorem", American Mathematical Monthly 1984. *)
-(* ------------------------------------------------------------------------- *)
-
-let RETRACTION_INJECTIVE_IMAGE_INTERVAL = prove
- (`!p:real^M->real^N a b.
- ~(interval[a,b] = {}) /\
- p continuous_on interval[a,b] /\
- (!x y. x IN interval[a,b] /\ y IN interval[a,b] /\ p x = p y ==> x = y)
- ==> ?f. f continuous_on (:real^N) /\
- IMAGE f (:real^N) SUBSET (IMAGE p (interval[a,b])) /\
- (!x. x IN (IMAGE p (interval[a,b])) ==> f x = x)`,
- REPEAT STRIP_TAC THEN
- FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INJECTIVE_ON_LEFT_INVERSE]) THEN
- DISCH_THEN(X_CHOOSE_TAC `q:real^N->real^M`) THEN
- SUBGOAL_THEN `(q:real^N->real^M) continuous_on
- (IMAGE p (interval[a:real^M,b]))`
- ASSUME_TAC THENL
- [MATCH_MP_TAC CONTINUOUS_ON_INVERSE THEN ASM_REWRITE_TAC[COMPACT_INTERVAL];
- ALL_TAC] THEN
- MP_TAC(ISPECL [`q:real^N->real^M`;
- `IMAGE (p:real^M->real^N)
- (interval[a,b])`;
- `a:real^M`; `b:real^M`]
- TIETZE_CLOSED_INTERVAL) THEN
- ASM_SIMP_TAC[COMPACT_INTERVAL; COMPACT_CONTINUOUS_IMAGE;
- COMPACT_IMP_CLOSED] THEN
- ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
- DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^M` STRIP_ASSUME_TAC) THEN
- EXISTS_TAC `(p:real^M->real^N) o (r:real^N->real^M)` THEN
- REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; o_THM; IN_UNIV] THEN
- CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
- MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN ASM_REWRITE_TAC[] THEN
- FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP(REWRITE_RULE[IMP_CONJ]
- CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[]);;
-
-let UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove
- (`!s:real^N->bool a b:real^M.
- s homeomorphic (interval[a,b])
- ==> !x. ~(x IN s) ==> ~bounded(path_component((:real^N) DIFF s) x)`,
- REPEAT GEN_TAC THEN REWRITE_TAC[homeomorphic; homeomorphism] THEN
- REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
- MAP_EVERY X_GEN_TAC [`p':real^N->real^M`; `p:real^M->real^N`] THEN
- DISCH_TAC THEN
- SUBGOAL_THEN
- `!x y. x IN interval[a,b] /\ y IN interval[a,b] /\
- (p:real^M->real^N) x = p y ==> x = y`
- ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
- FIRST_X_ASSUM(MP_TAC o funpow 4 CONJUNCT2) THEN
- DISCH_THEN(CONJUNCTS_THEN2 (SUBST1_TAC o SYM) ASSUME_TAC) THEN
- ASM_CASES_TAC `interval[a:real^M,b] = {}` THEN
- ASM_REWRITE_TAC[IMAGE_CLAUSES; DIFF_EMPTY; PATH_COMPONENT_UNIV;
- NOT_BOUNDED_UNIV] THEN
- ABBREV_TAC `s = (:real^N) DIFF (IMAGE p (interval[a:real^M,b]))` THEN
- X_GEN_TAC `c:real^N` THEN REPEAT STRIP_TAC THEN
- SUBGOAL_THEN `(c:real^N) IN s` ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
- SUBGOAL_THEN `bounded((path_component s c) UNION
- (IMAGE (p:real^M->real^N) (interval[a,b])))`
- MP_TAC THENL
- [ASM_SIMP_TAC[BOUNDED_UNION; COMPACT_IMP_BOUNDED; COMPACT_IMP_BOUNDED;
- COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
- ALL_TAC] THEN
- DISCH_THEN(MP_TAC o SPEC `c:real^N` o MATCH_MP BOUNDED_SUBSET_BALL) THEN
- REWRITE_TAC[UNION_SUBSET] THEN
- DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
- MP_TAC(ISPECL [`p:real^M->real^N`; `a:real^M`; `b:real^M`]
- RETRACTION_INJECTIVE_IMAGE_INTERVAL) THEN
- ASM_REWRITE_TAC[SUBSET; IN_UNIV] THEN
- DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^N` MP_TAC) THEN
- DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
- (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
- REWRITE_TAC[FORALL_IN_IMAGE; IN_UNIV] THEN DISCH_TAC THEN
- ABBREV_TAC `q = \z:real^N. if z IN path_component s c then r(z) else z` THEN
- SUBGOAL_THEN
- `(q:real^N->real^N) continuous_on
- (closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)))`
- MP_TAC THENL
- [EXPAND_TAC "q" THEN MATCH_MP_TAC CONTINUOUS_ON_CASES THEN
- REWRITE_TAC[CLOSED_CLOSURE; CONTINUOUS_ON_ID; GSYM OPEN_CLOSED] THEN
- REPEAT CONJ_TAC THENL
- [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN
- ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED;
- COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
- ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV];
- ALL_TAC] THEN
- X_GEN_TAC `z:real^N` THEN
- REWRITE_TAC[SET_RULE `~(z IN (s DIFF t) /\ z IN t)`] THEN
- STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
- MP_TAC(ISPECL
- [`path_component s (z:real^N)`; `path_component s (c:real^N)`]
- OPEN_INTER_CLOSURE_EQ_EMPTY) THEN
- ASM_REWRITE_TAC[GSYM DISJOINT; PATH_COMPONENT_DISJOINT] THEN ANTS_TAC THENL
- [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN
- ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED;
- COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
- REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
- DISCH_THEN(MP_TAC o SPEC `z:real^N`) THEN ASM_REWRITE_TAC[] THEN
- GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [IN] THEN
- REWRITE_TAC[PATH_COMPONENT_REFL_EQ] THEN ASM SET_TAC[]];
- ALL_TAC] THEN
- SUBGOAL_THEN
- `closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)) =
- (:real^N)`
- SUBST1_TAC THENL
- [MATCH_MP_TAC(SET_RULE `s SUBSET t ==> t UNION (UNIV DIFF s) = UNIV`) THEN
- REWRITE_TAC[CLOSURE_SUBSET];
- DISCH_TAC] THEN
- MP_TAC(ISPECL
- [`(\x. &2 % c - x) o
- (\x. c + B / norm(x - c) % (x - c)) o (q:real^N->real^N)`;
- `cball(c:real^N,B)`]
- BROUWER) THEN
- REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC; COMPACT_CBALL; CONVEX_CBALL] THEN
- ASM_SIMP_TAC[CBALL_EQ_EMPTY; REAL_LT_IMP_LE; REAL_NOT_LT] THEN
- SUBGOAL_THEN `!x. ~((q:real^N->real^N) x = c)` ASSUME_TAC THENL
- [X_GEN_TAC `x:real^N` THEN EXPAND_TAC "q" THEN
- REWRITE_TAC[NORM_EQ_0; VECTOR_SUB_EQ] THEN COND_CASES_TAC THEN
- ASM SET_TAC[PATH_COMPONENT_REFL_EQ];
- ALL_TAC] THEN
- REPEAT CONJ_TAC THENL
- [MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
- SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN
- MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN CONJ_TAC THENL
- [ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV]; ALL_TAC] THEN
- MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST] THEN
- MATCH_MP_TAC CONTINUOUS_ON_MUL THEN
- SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN
- REWRITE_TAC[o_DEF; real_div; LIFT_CMUL] THEN
- MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN
- MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_INV) THEN
- ASM_REWRITE_TAC[FORALL_IN_IMAGE; NORM_EQ_0; VECTOR_SUB_EQ] THEN
- SUBGOAL_THEN
- `(\x:real^N. lift(norm(x - c))) = (lift o norm) o (\x. x - c)`
- SUBST1_TAC THENL [REWRITE_TAC[o_DEF]; ALL_TAC] THEN
- MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
- ASM_SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST;
- CONTINUOUS_ON_LIFT_NORM];
- REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_CBALL; o_THM; dist] THEN
- X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
- REWRITE_TAC[VECTOR_ARITH `c - (&2 % c - (c + x)) = x`] THEN
- REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
- ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
- ASM_REAL_ARITH_TAC;
- REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(c /\ b) <=> c ==> ~b`] THEN
- REWRITE_TAC[IN_CBALL; o_THM; dist] THEN
- X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
- REWRITE_TAC[VECTOR_ARITH `&2 % c - (c + x') = x <=> --x' = x - c`] THEN
- ASM_CASES_TAC `(x:real^N) IN path_component s c` THENL
- [MATCH_MP_TAC(NORM_ARITH `norm(y) < B /\ norm(x) = B ==> ~(--x = y)`) THEN
- REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
- ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
- ASM_SIMP_TAC[REAL_ARITH `&0 < B ==> abs B = B`] THEN
- UNDISCH_TAC `path_component s c SUBSET ball(c:real^N,B)` THEN
- REWRITE_TAC[SUBSET; IN_BALL] THEN ASM_MESON_TAC[dist; NORM_SUB];
- EXPAND_TAC "q" THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[] THEN
- REWRITE_TAC[VECTOR_ARITH `--(c % x) = x <=> (&1 + c) % x = vec 0`] THEN
- ASM_REWRITE_TAC[DE_MORGAN_THM; VECTOR_SUB_EQ; VECTOR_MUL_EQ_0] THEN
- SUBGOAL_THEN `~(x:real^N = c)` ASSUME_TAC THENL
- [ASM_MESON_TAC[PATH_COMPONENT_REFL; IN]; ALL_TAC] THEN
- ASM_REWRITE_TAC[] THEN
- MATCH_MP_TAC(REAL_ARITH `&0 < x ==> ~(&1 + x = &0)`) THEN
- ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ]]]);;
-
-let PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove
- (`!s:real^N->bool a b:real^M.
- 2 <= dimindex(:N) /\ s homeomorphic interval[a,b]
- ==> path_connected((:real^N) DIFF s)`,
- REPEAT STRIP_TAC THEN REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
- FIRST_ASSUM(MP_TAC o MATCH_MP
- UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN
- ASM_REWRITE_TAC[SET_RULE `~(x IN s) <=> x IN (UNIV DIFF s)`] THEN
- ABBREV_TAC `t = (:real^N) DIFF s` THEN
- DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN
- STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP HOMEOMORPHIC_COMPACTNESS) THEN
- REWRITE_TAC[COMPACT_INTERVAL] THEN
- DISCH_THEN(MP_TAC o MATCH_MP COMPACT_IMP_BOUNDED) THEN
- REWRITE_TAC[BOUNDED_POS; LEFT_IMP_EXISTS_THM] THEN
- X_GEN_TAC `B:real` THEN STRIP_TAC THEN
- SUBGOAL_THEN `(?u:real^N. u IN path_component t x /\ B < norm(u)) /\
- (?v:real^N. v IN path_component t y /\ B < norm(v))`
- STRIP_ASSUME_TAC THENL
- [ASM_MESON_TAC[BOUNDED_POS; REAL_NOT_LE]; ALL_TAC] THEN
- MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `u:real^N` THEN
- CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
- MATCH_MP_TAC PATH_COMPONENT_SYM THEN
- MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `v:real^N` THEN
- CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
- MATCH_MP_TAC PATH_COMPONENT_OF_SUBSET THEN
- EXISTS_TAC `(:real^N) DIFF cball(vec 0,B)` THEN CONJ_TAC THENL
- [EXPAND_TAC "t" THEN MATCH_MP_TAC(SET_RULE
- `s SUBSET t ==> (u DIFF t) SUBSET (u DIFF s)`) THEN
- ASM_REWRITE_TAC[SUBSET; IN_CBALL_0];
- MP_TAC(ISPEC `cball(vec 0:real^N,B)`
- PATH_CONNECTED_COMPLEMENT_BOUNDED_CONVEX) THEN
- ASM_REWRITE_TAC[BOUNDED_CBALL; CONVEX_CBALL] THEN
- REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
- DISCH_THEN MATCH_MP_TAC THEN
- ASM_REWRITE_TAC[IN_DIFF; IN_UNIV; IN_CBALL_0; REAL_NOT_LE]]);;
-
-(* ------------------------------------------------------------------------- *)
-(* In particular, apply all these to the special case of an arc. *)
-(* ------------------------------------------------------------------------- *)
-
-let RETRACTION_ARC = prove
- (`!p. arc p
- ==> ?f. f continuous_on (:real^N) /\
- IMAGE f (:real^N) SUBSET path_image p /\
- (!x. x IN path_image p ==> f x = x)`,
- REWRITE_TAC[arc; path; path_image] THEN REPEAT STRIP_TAC THEN
- MATCH_MP_TAC RETRACTION_INJECTIVE_IMAGE_INTERVAL THEN
- ASM_REWRITE_TAC[INTERVAL_EQ_EMPTY_CART_1; DROP_VEC; REAL_NOT_LT; REAL_POS]);;
-
-let PATH_CONNECTED_ARC_COMPLEMENT = prove
- (`!p. 2 <= dimindex(:N) /\ arc p
- ==> path_connected((:real^N) DIFF path_image p)`,
- REWRITE_TAC[arc; path] THEN REPEAT STRIP_TAC THEN SIMP_TAC[path_image] THEN
- MP_TAC(ISPECL [`path_image p:real^N->bool`; `vec 0:real^1`; `vec 1:real^1`]
- PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN
- ASM_REWRITE_TAC[path_image] THEN DISCH_THEN MATCH_MP_TAC THEN
- ONCE_REWRITE_TAC[HOMEOMORPHIC_SYM] THEN
- MATCH_MP_TAC HOMEOMORPHIC_COMPACT THEN
- EXISTS_TAC `p:real^1->real^N` THEN ASM_REWRITE_TAC[COMPACT_INTERVAL]);;
-
-let CONNECTED_ARC_COMPLEMENT = prove
- (`!p. 2 <= dimindex(:N) /\ arc p
- ==> connected((:real^N) DIFF path_image p)`,
- SIMP_TAC[PATH_CONNECTED_ARC_COMPLEMENT; PATH_CONNECTED_IMP_CONNECTED]);; *)
-
end