# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1497886948 -3600
# Node ID 571b698659c0b4ffd9817b18300d2118fd794aa4
# Parent  0e640e04fc567c83abc09884864c3c5dfd6a4c35
Repaired an inadvertent reordering of the premises of two theorems

diff -r 0e640e04fc56 -r 571b698659c0 src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Mon Jun 19 16:07:47 2017 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy	Mon Jun 19 16:42:28 2017 +0100
@@ -311,26 +311,26 @@
 where
   "s division_of i \<longleftrightarrow>
     finite s \<and>
-    (\<forall>k\<in>s. k \<subseteq> i \<and> k \<noteq> {} \<and> (\<exists>a b. k = cbox a b)) \<and>
-    (\<forall>k1\<in>s. \<forall>k2\<in>s. k1 \<noteq> k2 \<longrightarrow> interior(k1) \<inter> interior(k2) = {}) \<and>
+    (\<forall>K\<in>s. K \<subseteq> i \<and> K \<noteq> {} \<and> (\<exists>a b. K = cbox a b)) \<and>
+    (\<forall>K1\<in>s. \<forall>K2\<in>s. K1 \<noteq> K2 \<longrightarrow> interior(K1) \<inter> interior(K2) = {}) \<and>
     (\<Union>s = i)"
 
 lemma division_ofD[dest]:
   assumes "s division_of i"
   shows "finite s"
-    and "\<And>k. k \<in> s \<Longrightarrow> k \<subseteq> i"
-    and "\<And>k. k \<in> s \<Longrightarrow> k \<noteq> {}"
-    and "\<And>k. k \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
-    and "\<And>k1 k2. k1 \<in> s \<Longrightarrow> k2 \<in> s \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}"
+    and "\<And>K. K \<in> s \<Longrightarrow> K \<subseteq> i"
+    and "\<And>K. K \<in> s \<Longrightarrow> K \<noteq> {}"
+    and "\<And>K. K \<in> s \<Longrightarrow> \<exists>a b. K = cbox a b"
+    and "\<And>K1 K2. K1 \<in> s \<Longrightarrow> K2 \<in> s \<Longrightarrow> K1 \<noteq> K2 \<Longrightarrow> interior(K1) \<inter> interior(K2) = {}"
     and "\<Union>s = i"
   using assms unfolding division_of_def by auto
 
 lemma division_ofI:
   assumes "finite s"
-    and "\<And>k. k \<in> s \<Longrightarrow> k \<subseteq> i"
-    and "\<And>k. k \<in> s \<Longrightarrow> k \<noteq> {}"
-    and "\<And>k. k \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
-    and "\<And>k1 k2. k1 \<in> s \<Longrightarrow> k2 \<in> s \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
+    and "\<And>K. K \<in> s \<Longrightarrow> K \<subseteq> i"
+    and "\<And>K. K \<in> s \<Longrightarrow> K \<noteq> {}"
+    and "\<And>K. K \<in> s \<Longrightarrow> \<exists>a b. K = cbox a b"
+    and "\<And>K1 K2. K1 \<in> s \<Longrightarrow> K2 \<in> s \<Longrightarrow> K1 \<noteq> K2 \<Longrightarrow> interior K1 \<inter> interior K2 = {}"
     and "\<Union>s = i"
   shows "s division_of i"
   using assms unfolding division_of_def by auto
@@ -350,9 +350,9 @@
 proof
   assume ?r
   moreover
-  { fix k
-    assume "s = {{a}}" "k\<in>s"
-    then have "\<exists>x y. k = cbox x y"
+  { fix K
+    assume "s = {{a}}" "K\<in>s"
+    then have "\<exists>x y. K = cbox x y"
       apply (rule_tac x=a in exI)+
       apply (force simp: cbox_sing)
       done
@@ -1106,22 +1106,22 @@
 definition tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40)
   where "s tagged_partial_division_of i \<longleftrightarrow>
     finite s \<and>
-    (\<forall>x k. (x, k) \<in> s \<longrightarrow> x \<in> k \<and> k \<subseteq> i \<and> (\<exists>a b. k = cbox a b)) \<and>
-    (\<forall>x1 k1 x2 k2. (x1, k1) \<in> s \<and> (x2, k2) \<in> s \<and> (x1, k1) \<noteq> (x2, k2) \<longrightarrow>
-      interior k1 \<inter> interior k2 = {})"
+    (\<forall>x K. (x, K) \<in> s \<longrightarrow> x \<in> K \<and> K \<subseteq> i \<and> (\<exists>a b. K = cbox a b)) \<and>
+    (\<forall>x1 K1 x2 K2. (x1, K1) \<in> s \<and> (x2, K2) \<in> s \<and> (x1, K1) \<noteq> (x2, K2) \<longrightarrow>
+      interior K1 \<inter> interior K2 = {})"
 
 lemma tagged_partial_division_ofD[dest]:
   assumes "s tagged_partial_division_of i"
   shows "finite s"
-    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k"
-    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"
-    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
-    and "\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow>
-      (x2, k2) \<in> s \<Longrightarrow> (x1, k1) \<noteq> (x2, k2) \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
+    and "\<And>x K. (x,K) \<in> s \<Longrightarrow> x \<in> K"
+    and "\<And>x K. (x,K) \<in> s \<Longrightarrow> K \<subseteq> i"
+    and "\<And>x K. (x,K) \<in> s \<Longrightarrow> \<exists>a b. K = cbox a b"
+    and "\<And>x1 K1 x2 K2. (x1,K1) \<in> s \<Longrightarrow>
+      (x2, K2) \<in> s \<Longrightarrow> (x1, K1) \<noteq> (x2, K2) \<Longrightarrow> interior K1 \<inter> interior K2 = {}"
   using assms unfolding tagged_partial_division_of_def by blast+
 
 definition tagged_division_of (infixr "tagged'_division'_of" 40)
-  where "s tagged_division_of i \<longleftrightarrow> s tagged_partial_division_of i \<and> (\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
+  where "s tagged_division_of i \<longleftrightarrow> s tagged_partial_division_of i \<and> (\<Union>{K. \<exists>x. (x,K) \<in> s} = i)"
 
 lemma tagged_division_of_finite: "s tagged_division_of i \<Longrightarrow> finite s"
   unfolding tagged_division_of_def tagged_partial_division_of_def by auto
@@ -1129,20 +1129,20 @@
 lemma tagged_division_of:
   "s tagged_division_of i \<longleftrightarrow>
     finite s \<and>
-    (\<forall>x k. (x, k) \<in> s \<longrightarrow> x \<in> k \<and> k \<subseteq> i \<and> (\<exists>a b. k = cbox a b)) \<and>
-    (\<forall>x1 k1 x2 k2. (x1, k1) \<in> s \<and> (x2, k2) \<in> s \<and> (x1, k1) \<noteq> (x2, k2) \<longrightarrow>
-      interior k1 \<inter> interior k2 = {}) \<and>
-    (\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
+    (\<forall>x K. (x, K) \<in> s \<longrightarrow> x \<in> K \<and> K \<subseteq> i \<and> (\<exists>a b. K = cbox a b)) \<and>
+    (\<forall>x1 K1 x2 K2. (x1, K1) \<in> s \<and> (x2, K2) \<in> s \<and> (x1, K1) \<noteq> (x2, K2) \<longrightarrow>
+      interior K1 \<inter> interior K2 = {}) \<and>
+    (\<Union>{K. \<exists>x. (x,K) \<in> s} = i)"
   unfolding tagged_division_of_def tagged_partial_division_of_def by auto
 
 lemma tagged_division_ofI:
   assumes "finite s"
-    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k"
-    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"
-    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
-    and "\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow> (x2, k2) \<in> s \<Longrightarrow> (x1, k1) \<noteq> (x2, k2) \<Longrightarrow>
-      interior k1 \<inter> interior k2 = {}"
-    and "(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
+    and "\<And>x K. (x,K) \<in> s \<Longrightarrow> x \<in> K"
+    and "\<And>x K. (x,K) \<in> s \<Longrightarrow> K \<subseteq> i"
+    and "\<And>x K. (x,K) \<in> s \<Longrightarrow> \<exists>a b. K = cbox a b"
+    and "\<And>x1 K1 x2 K2. (x1,K1) \<in> s \<Longrightarrow> (x2, K2) \<in> s \<Longrightarrow> (x1, K1) \<noteq> (x2, K2) \<Longrightarrow>
+      interior K1 \<inter> interior K2 = {}"
+    and "(\<Union>{K. \<exists>x. (x,K) \<in> s} = i)"
   shows "s tagged_division_of i"
   unfolding tagged_division_of
   using assms
@@ -1153,12 +1153,12 @@
 lemma tagged_division_ofD[dest]:  (*FIXME USE A LOCALE*)
   assumes "s tagged_division_of i"
   shows "finite s"
-    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k"
-    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"
-    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
-    and "\<And>x1 k1 x2 k2. (x1, k1) \<in> s \<Longrightarrow> (x2, k2) \<in> s \<Longrightarrow> (x1, k1) \<noteq> (x2, k2) \<Longrightarrow>
-      interior k1 \<inter> interior k2 = {}"
-    and "(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
+    and "\<And>x K. (x,K) \<in> s \<Longrightarrow> x \<in> K"
+    and "\<And>x K. (x,K) \<in> s \<Longrightarrow> K \<subseteq> i"
+    and "\<And>x K. (x,K) \<in> s \<Longrightarrow> \<exists>a b. K = cbox a b"
+    and "\<And>x1 K1 x2 K2. (x1, K1) \<in> s \<Longrightarrow> (x2, K2) \<in> s \<Longrightarrow> (x1, K1) \<noteq> (x2, K2) \<Longrightarrow>
+      interior K1 \<inter> interior K2 = {}"
+    and "(\<Union>{K. \<exists>x. (x,K) \<in> s} = i)"
   using assms unfolding tagged_division_of by blast+
 
 lemma division_of_tagged_division:
@@ -1899,28 +1899,28 @@
 
 lemma tagged_division_split_left_inj:
   assumes d: "d tagged_division_of i"
-  and "k1 \<noteq> k2"
-  and tags: "(x1, k1) \<in> d" "(x2, k2) \<in> d"
-  and eq: "k1 \<inter> {x. x \<bullet> k \<le> c} = k2 \<inter> {x. x \<bullet> k \<le> c}"
-    shows "interior (k1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
+  and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
+  and "K1 \<noteq> K2"
+  and eq: "K1 \<inter> {x. x \<bullet> k \<le> c} = K2 \<inter> {x. x \<bullet> k \<le> c}"
+    shows "interior (K1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
 proof -
-  have "interior (k1 \<inter> k2) = {} \<or> (x2, k2) = (x1, k1)"
+  have "interior (K1 \<inter> K2) = {} \<or> (x2, K2) = (x1, K1)"
     using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
   then show ?thesis
-    using eq \<open>k1 \<noteq> k2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
+    using eq \<open>K1 \<noteq> K2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
 qed
 
 lemma tagged_division_split_right_inj:
   assumes d: "d tagged_division_of i"
-  and "k1 \<noteq> k2"
-  and tags: "(x1, k1) \<in> d" "(x2, k2) \<in> d"
-  and eq: "k1 \<inter> {x. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}"
-    shows "interior (k1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
+  and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
+  and "K1 \<noteq> K2"
+  and eq: "K1 \<inter> {x. x\<bullet>k \<ge> c} = K2 \<inter> {x. x\<bullet>k \<ge> c}"
+    shows "interior (K1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
 proof -
-  have "interior (k1 \<inter> k2) = {} \<or> (x2, k2) = (x1, k1)"
+  have "interior (K1 \<inter> K2) = {} \<or> (x2, K2) = (x1, K1)"
     using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
   then show ?thesis
-    using eq \<open>k1 \<noteq> k2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
+    using eq \<open>K1 \<noteq> K2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
 qed
 
 subsection \<open>Special case of additivity we need for the FTC.\<close>