# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1524145748 -3600
# Node ID a8a20be7053afcc19b86108dc45849e5d0617ed3
# Parent  0a2a1b6507c17b76786908356c451c7f93ca80a0
some simpler, cleaner proofs

diff -r 0a2a1b6507c1 -r a8a20be7053a src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Wed Apr 18 21:12:50 2018 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Thu Apr 19 14:49:08 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
diff -r 0a2a1b6507c1 -r a8a20be7053a src/HOL/Algebra/Order.thy
--- a/src/HOL/Algebra/Order.thy	Wed Apr 18 21:12:50 2018 +0100
+++ b/src/HOL/Algebra/Order.thy	Thu Apr 19 14:49:08 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)
 
diff -r 0a2a1b6507c1 -r a8a20be7053a src/HOL/Analysis/Fashoda_Theorem.thy
--- a/src/HOL/Analysis/Fashoda_Theorem.thy	Wed Apr 18 21:12:50 2018 +0100
+++ b/src/HOL/Analysis/Fashoda_Theorem.thy	Thu Apr 19 14:49:08 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