src/HOL/Multivariate_Analysis/Integration.thy
author haftmann
Sat, 25 May 2013 15:44:29 +0200
changeset 52141 eff000cab70f
parent 51642 400ec5ae7f8f
child 53015 a1119cf551e8
permissions -rw-r--r--
weaker precendence of syntax for big intersection and union on sets
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
     1
header {* Kurzweil-Henstock Gauge Integration in many dimensions. *}
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
     2
(*  Author:                     John Harrison
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
     3
    Translation from HOL light: Robert Himmelmann, TU Muenchen *)
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
     4
35292
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents: 35291
diff changeset
     5
theory Integration
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 40513
diff changeset
     6
imports
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 40513
diff changeset
     7
  Derivative
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 40513
diff changeset
     8
  "~~/src/HOL/Library/Indicator_Function"
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
     9
begin
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
    10
51518
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    11
lemma cSup_abs_le: (* TODO: is this really needed? *)
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    12
  fixes S :: "real set"
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    13
  shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    14
by (auto simp add: abs_le_interval_iff intro: cSup_least) (metis cSup_upper2) 
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    15
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    16
lemma cInf_abs_ge: (* TODO: is this really needed? *)
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    17
  fixes S :: "real set"
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    18
  shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    19
by (simp add: Inf_real_def) (rule cSup_abs_le, auto) 
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    20
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    21
lemma cSup_asclose: (* TODO: is this really needed? *)
51475
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    22
  fixes S :: "real set"
51518
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    23
  assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Sup S - l\<bar> \<le> e"
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    24
proof-
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    25
  have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    26
  thus ?thesis using S b cSup_bounds[of S "l - e" "l+e"] unfolding th
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    27
    by  (auto simp add: setge_def setle_def)
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    28
qed
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    29
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    30
lemma cInf_asclose: (* TODO: is this really needed? *)
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    31
  fixes S :: "real set"
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    32
  assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Inf S - l\<bar> \<le> e"
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    33
proof -
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    34
  have "\<bar>- Sup (uminus ` S) - l\<bar> =  \<bar>Sup (uminus ` S) - (-l)\<bar>"
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    35
    by auto
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    36
  also have "... \<le> e" 
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    37
    apply (rule cSup_asclose) 
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    38
    apply (auto simp add: S)
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    39
    apply (metis abs_minus_add_cancel b add_commute diff_minus)
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    40
    done
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    41
  finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    42
  thus ?thesis
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    43
    by (simp add: Inf_real_def)
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    44
qed
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    45
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    46
lemma cSup_finite_ge_iff: 
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    47
  fixes S :: "real set" shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Sup S \<longleftrightarrow> (\<exists>x\<in>S. a \<le> x)"
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    48
  by (metis cSup_eq_Max Max_ge_iff)
51475
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    49
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    50
lemma cSup_finite_le_iff: 
51518
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    51
  fixes S :: "real set" shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Sup S \<longleftrightarrow> (\<forall>x\<in>S. a \<ge> x)"
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    52
  by (metis cSup_eq_Max Max_le_iff)
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    53
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    54
lemma cInf_finite_ge_iff: 
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    55
  fixes S :: "real set" shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall>x\<in>S. a \<le> x)"
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    56
  by (metis cInf_eq_Min Min_ge_iff)
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    57
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    58
lemma cInf_finite_le_iff: 
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    59
  fixes S :: "real set" shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists>x\<in>S. a \<ge> x)"
6a56b7088a6a separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents: 51489
diff changeset
    60
  by (metis cInf_eq_Min Min_le_iff)
51475
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    61
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    62
lemma Inf: (* rename *)
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    63
  fixes S :: "real set"
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    64
  shows "S \<noteq> {} ==> (\<exists>b. b <=* S) ==> isGlb UNIV S (Inf S)"
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    65
by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def intro: cInf_lower cInf_greatest) 
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    66
 
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    67
lemma real_le_inf_subset:
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    68
  assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. b <=* s"
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    69
  shows "Inf s <= Inf (t::real set)"
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    70
  apply (rule isGlb_le_isLb)
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    71
  apply (rule Inf[OF assms(1)])
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    72
  apply (insert assms)
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    73
  apply (erule exE)
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    74
  apply (rule_tac x = b in exI)
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    75
  apply (auto simp: isLb_def setge_def intro: cInf_lower cInf_greatest)
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    76
  done
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    77
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    78
lemma real_ge_sup_subset:
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    79
  assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. s *<= b"
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    80
  shows "Sup s >= Sup (t::real set)"
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    81
  apply (rule isLub_le_isUb)
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    82
  apply (rule isLub_cSup[OF assms(1)])
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    83
  apply (insert assms)
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    84
  apply (erule exE)
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    85
  apply (rule_tac x = b in exI)
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    86
  apply (auto simp: isUb_def setle_def intro: cSup_upper cSup_least)
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    87
  done
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
    88
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
    89
(*declare not_less[simp] not_le[simp]*)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
    90
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
    91
lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
    92
  scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44176
diff changeset
    93
  scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
    94
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
    95
lemma real_arch_invD:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
    96
  "0 < (e::real) \<Longrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    97
  by (subst(asm) real_arch_inv)
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    98
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    99
36243
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   100
subsection {* Sundries *}
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   101
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   102
lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   103
lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   104
lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   105
lemma conjunctD5: assumes "a \<and> b \<and> c \<and> d \<and> e" shows a b c d e using assms by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   106
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
   107
declare norm_triangle_ineq4[intro] 
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   108
36243
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   109
lemma simple_image: "{f x |x . x \<in> s} = f ` s" by blast
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   110
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   111
lemma linear_simps:
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   112
  assumes "bounded_linear f"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   113
  shows
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   114
    "f (a + b) = f a + f b"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   115
    "f (a - b) = f a - f b"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   116
    "f 0 = 0"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   117
    "f (- a) = - f a"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   118
    "f (s *\<^sub>R v) = s *\<^sub>R (f v)"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   119
  apply (rule_tac[!] additive.add additive.minus additive.diff additive.zero bounded_linear.scaleR)
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   120
  using assms unfolding bounded_linear_def additive_def
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   121
  apply auto
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   122
  done
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   123
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   124
lemma bounded_linearI:
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   125
  assumes "\<And>x y. f (x + y) = f x + f y"
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   126
    and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x" "\<And>x. norm (f x) \<le> norm x * K"
36243
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   127
  shows "bounded_linear f"
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   128
  unfolding bounded_linear_def additive_def bounded_linear_axioms_def using assms by auto
51348
011c97ba3b3d move lemma Inf to usage point
hoelzl
parents: 50945
diff changeset
   129
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   130
lemma bounded_linear_component [intro]: "bounded_linear (\<lambda>x::'a::euclidean_space. x \<bullet> k)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   131
  by (rule bounded_linear_inner_left)
36243
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   132
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   133
lemma transitive_stepwise_lt_eq:
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   134
  assumes "(\<And>x y z::nat. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z)"
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   135
  shows "((\<forall>m. \<forall>n>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n)))" (is "?l = ?r")
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   136
proof (safe)
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   137
  assume ?r
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   138
  fix n m :: nat
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   139
  assume "m < n"
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   140
  then show "R m n"
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   141
  proof (induct n arbitrary: m)
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   142
    case (Suc n)
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   143
    show ?case 
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   144
    proof (cases "m < n")
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   145
      case True
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   146
      show ?thesis
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   147
        apply (rule assms[OF Suc(1)[OF True]])
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   148
        using `?r`
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   149
        apply auto
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   150
        done
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   151
    next
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   152
      case False
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   153
      then have "m = n" using Suc(2) by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   154
      then show ?thesis using `?r` by auto
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   155
    qed
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   156
  qed auto
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   157
qed auto
36243
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   158
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   159
lemma transitive_stepwise_gt:
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   160
  assumes "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n) "
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   161
  shows "\<forall>n>m. R m n"
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   162
proof -
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   163
  have "\<forall>m. \<forall>n>m. R m n"
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   164
    apply (subst transitive_stepwise_lt_eq)
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   165
    apply (rule assms)
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   166
    apply assumption
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   167
    apply assumption
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   168
    using assms(2) apply auto
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   169
    done
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   170
  then show ?thesis by auto
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   171
qed
36243
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   172
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   173
lemma transitive_stepwise_le_eq:
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   174
  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   175
  shows "(\<forall>m. \<forall>n\<ge>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n))" (is "?l = ?r")
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   176
proof safe
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   177
  assume ?r
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   178
  fix m n :: nat
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   179
  assume "m \<le> n"
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   180
  thus "R m n"
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   181
  proof (induct n arbitrary: m)
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   182
    case 0
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   183
    with assms show ?case by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   184
  next
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   185
    case (Suc n)
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   186
    show ?case
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   187
    proof (cases "m \<le> n")
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   188
      case True
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   189
      show ?thesis
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   190
        apply (rule assms(2))
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   191
        apply (rule Suc(1)[OF True])
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   192
        using `?r` apply auto
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   193
        done
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   194
    next
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   195
      case False
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   196
      hence "m = Suc n" using Suc(2) by auto
36243
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   197
      thus ?thesis using assms(1) by auto
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   198
    qed
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   199
  qed
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   200
qed auto
36243
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   201
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   202
lemma transitive_stepwise_le:
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   203
  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n) "
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   204
  shows "\<forall>n\<ge>m. R m n"
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   205
proof -
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   206
  have "\<forall>m. \<forall>n\<ge>m. R m n"
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   207
    apply (subst transitive_stepwise_le_eq)
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   208
    apply (rule assms)
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   209
    apply (rule assms,assumption,assumption)
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   210
    using assms(3) apply auto
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   211
    done
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   212
  then show ?thesis by auto
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   213
qed
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   214
36243
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   215
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   216
subsection {* Some useful lemmas about intervals. *}
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   217
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   218
abbreviation One where "One \<equiv> ((\<Sum>Basis)::_::euclidean_space)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   219
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   220
lemma empty_as_interval: "{} = {One..(0::'a::ordered_euclidean_space)}"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   221
  by (auto simp: set_eq_iff eucl_le[where 'a='a] intro!: bexI[OF _ SOME_Basis])
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   222
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   223
lemma interior_subset_union_intervals: 
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   224
  assumes "i = {a..b::'a::ordered_euclidean_space}" "j = {c..d}"
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   225
    "interior j \<noteq> {}" "i \<subseteq> j \<union> s" "interior(i) \<inter> interior(j) = {}"
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   226
  shows "interior i \<subseteq> interior s"
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   227
proof -
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   228
  have "{a<..<b} \<inter> {c..d} = {}"
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   229
    using inter_interval_mixed_eq_empty[of c d a b] and assms(3,5)
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   230
    unfolding assms(1,2) interior_closed_interval by auto
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   231
  moreover
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   232
  have "{a<..<b} \<subseteq> {c..d} \<union> s"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   233
    apply (rule order_trans,rule interval_open_subset_closed)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   234
    using assms(4) unfolding assms(1,2)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   235
    apply auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   236
    done
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   237
  ultimately
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   238
  show ?thesis
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   239
    apply -
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   240
    apply (rule interior_maximal)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   241
    defer
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   242
    apply (rule open_interior)
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   243
    unfolding assms(1,2) interior_closed_interval
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   244
    apply auto
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   245
    done
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   246
qed
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   247
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   248
lemma inter_interior_unions_intervals:
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   249
  fixes f::"('a::ordered_euclidean_space) set set"
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   250
  assumes "finite f" "open s" "\<forall>t\<in>f. \<exists>a b. t = {a..b}" "\<forall>t\<in>f. s \<inter> (interior t) = {}"
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   251
  shows "s \<inter> interior(\<Union>f) = {}"
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   252
proof (rule ccontr, unfold ex_in_conv[THEN sym])
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   253
  case goal1
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   254
  have lem1: "\<And>x e s U. ball x e \<subseteq> s \<inter> interior U \<longleftrightarrow> ball x e \<subseteq> s \<inter> U"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   255
    apply rule
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   256
    defer
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   257
    apply (rule_tac Int_greatest)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   258
    unfolding open_subset_interior[OF open_ball]
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   259
    using interior_subset
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   260
    apply auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   261
    done
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   262
  have lem2: "\<And>x s P. \<exists>x\<in>s. P x \<Longrightarrow> \<exists>x\<in>insert x s. P x" by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   263
  have "\<And>f. finite f \<Longrightarrow> (\<forall>t\<in>f. \<exists>a b. t = {a..b}) \<Longrightarrow>
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   264
    (\<exists>x. x \<in> s \<inter> interior (\<Union>f)) \<Longrightarrow> (\<exists>t\<in>f. \<exists>x. \<exists>e>0. ball x e \<subseteq> s \<inter> t)"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   265
  proof -
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   266
    case goal1
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   267
    then show ?case
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   268
    proof (induct rule: finite_induct)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   269
      case empty from this(2) guess x ..
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   270
      hence False unfolding Union_empty interior_empty by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   271
      thus ?case by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   272
    next
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   273
      case (insert i f) guess x using insert(5) .. note x = this
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   274
      then guess e unfolding open_contains_ball_eq[OF open_Int[OF assms(2) open_interior],rule_format] .. note e=this
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   275
      guess a using insert(4)[rule_format,OF insertI1] ..
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   276
      then guess b .. note ab = this
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   277
      show ?case
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   278
      proof (cases "x\<in>i")
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   279
        case False
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   280
        hence "x \<in> UNIV - {a..b}" unfolding ab by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   281
        then guess d unfolding open_contains_ball_eq[OF open_Diff[OF open_UNIV closed_interval],rule_format] ..
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   282
        hence "0 < d" "ball x (min d e) \<subseteq> UNIV - i" unfolding ab ball_min_Int by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   283
        hence "ball x (min d e) \<subseteq> s \<inter> interior (\<Union>f)"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   284
          using e unfolding lem1 unfolding  ball_min_Int by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   285
        hence "x \<in> s \<inter> interior (\<Union>f)" using `d>0` e by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   286
        hence "\<exists>t\<in>f. \<exists>x e. 0 < e \<and> ball x e \<subseteq> s \<inter> t"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   287
          apply -
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   288
          apply (rule insert(3))
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   289
          using insert(4)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   290
          apply auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   291
          done
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   292
        thus ?thesis by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   293
      next
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   294
        case True show ?thesis
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   295
        proof (cases "x\<in>{a<..<b}")
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   296
          case True
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   297
          then guess d unfolding open_contains_ball_eq[OF open_interval,rule_format] ..
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   298
          thus ?thesis
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   299
            apply (rule_tac x=i in bexI, rule_tac x=x in exI, rule_tac x="min d e" in exI)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   300
            unfolding ab
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   301
            using interval_open_subset_closed[of a b] and e
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   302
            apply fastforce+
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   303
            done
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   304
        next
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   305
          case False
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   306
          then obtain k where "x\<bullet>k \<le> a\<bullet>k \<or> x\<bullet>k \<ge> b\<bullet>k" and k:"k\<in>Basis"
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   307
            unfolding mem_interval by (auto simp add: not_less)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   308
          hence "x\<bullet>k = a\<bullet>k \<or> x\<bullet>k = b\<bullet>k"
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   309
            using True unfolding ab and mem_interval
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   310
              apply (erule_tac x = k in ballE)
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   311
              apply auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   312
              done
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   313
          hence "\<exists>x. ball x (e/2) \<subseteq> s \<inter> (\<Union>f)"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   314
          proof (erule_tac disjE)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   315
            let ?z = "x - (e/2) *\<^sub>R k"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   316
            assume as: "x\<bullet>k = a\<bullet>k"
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   317
            have "ball ?z (e / 2) \<inter> i = {}"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   318
              apply (rule ccontr)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   319
              unfolding ex_in_conv[THEN sym]
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   320
            proof (erule exE)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   321
              fix y
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   322
              assume "y \<in> ball ?z (e / 2) \<inter> i"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   323
              hence "dist ?z y < e/2" and yi:"y\<in>i" by auto
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   324
              hence "\<bar>(?z - y) \<bullet> k\<bar> < e/2"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   325
                using Basis_le_norm[OF k, of "?z - y"] unfolding dist_norm by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   326
              hence "y\<bullet>k < a\<bullet>k"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   327
                using e[THEN conjunct1] k by (auto simp add: field_simps as inner_Basis inner_simps)
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   328
              hence "y \<notin> i"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   329
                unfolding ab mem_interval by (auto intro!: bexI[OF _ k])
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   330
              thus False using yi by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   331
            qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   332
            moreover
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   333
            have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   334
              apply(rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]])
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   335
            proof
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   336
              fix y
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   337
              assume as: "y\<in> ball ?z (e/2)"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   338
              have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y - (e / 2) *\<^sub>R k)"
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   339
                apply -
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   340
                apply (rule order_trans,rule norm_triangle_sub[of "x - y" "(e/2) *\<^sub>R k"])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   341
                unfolding norm_scaleR norm_Basis[OF k]
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   342
                apply auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   343
                done
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   344
              also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   345
                apply (rule add_strict_left_mono)
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   346
                using as
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   347
                unfolding mem_ball dist_norm
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   348
                using e
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   349
                apply (auto simp add: field_simps)
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   350
                done
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   351
              finally show "y\<in>ball x e"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   352
                unfolding mem_ball dist_norm using e by (auto simp add:field_simps)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   353
            qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   354
            ultimately show ?thesis
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   355
              apply (rule_tac x="?z" in exI)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   356
              unfolding Union_insert
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   357
              apply auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   358
              done
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   359
          next
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   360
            let ?z = "x + (e/2) *\<^sub>R k"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   361
            assume as: "x\<bullet>k = b\<bullet>k"
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   362
            have "ball ?z (e / 2) \<inter> i = {}"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   363
              apply (rule ccontr)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   364
              unfolding ex_in_conv[THEN sym]
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   365
            proof(erule exE)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   366
              fix y
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   367
              assume "y \<in> ball ?z (e / 2) \<inter> i"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   368
              hence "dist ?z y < e/2" and yi:"y\<in>i" by auto
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   369
              hence "\<bar>(?z - y) \<bullet> k\<bar> < e/2"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   370
                using Basis_le_norm[OF k, of "?z - y"] unfolding dist_norm by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   371
              hence "y\<bullet>k > b\<bullet>k"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   372
                using e[THEN conjunct1] k by(auto simp add:field_simps inner_simps inner_Basis as)
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   373
              hence "y \<notin> i"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   374
                unfolding ab mem_interval by (auto intro!: bexI[OF _ k])
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   375
              thus False using yi by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   376
            qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   377
            moreover
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   378
            have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   379
              apply (rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]])
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   380
            proof
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   381
              fix y
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   382
              assume as: "y\<in> ball ?z (e/2)"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   383
              have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y + (e / 2) *\<^sub>R k)"
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   384
                apply -
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   385
                apply(rule order_trans,rule norm_triangle_sub[of "x - y" "- (e/2) *\<^sub>R k"])
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   386
                unfolding norm_scaleR
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   387
                apply (auto simp: k)
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   388
                done
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   389
              also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   390
                apply (rule add_strict_left_mono)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   391
                using as unfolding mem_ball dist_norm
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   392
                using e apply (auto simp add: field_simps)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   393
                done
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   394
              finally show "y\<in>ball x e"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   395
                unfolding mem_ball dist_norm using e by(auto simp add:field_simps)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   396
            qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   397
            ultimately show ?thesis
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   398
              apply (rule_tac x="?z" in exI)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   399
              unfolding Union_insert
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   400
              apply auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   401
              done
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   402
          qed 
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   403
          then guess x ..
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   404
          hence "x \<in> s \<inter> interior (\<Union>f)"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   405
            unfolding lem1[where U="\<Union>f",THEN sym]
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   406
            using centre_in_ball e[THEN conjunct1] by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   407
          thus ?thesis
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   408
            apply -
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   409
            apply (rule lem2, rule insert(3))
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   410
            using insert(4) apply auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   411
            done
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   412
        qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   413
      qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   414
    qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   415
  qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   416
  note * = this
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   417
  guess t using *[OF assms(1,3) goal1] ..
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   418
  from this(2) guess x ..
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   419
  then guess e ..
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   420
  hence "x \<in> s" "x\<in>interior t"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   421
    defer
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   422
    using open_subset_interior[OF open_ball, of x e t] apply auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   423
    done
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   424
  thus False using `t\<in>f` assms(4) by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   425
qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   426
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
   427
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   428
subsection {* Bounds on intervals where they exist. *}
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   429
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   430
definition interval_upperbound :: "('a::ordered_euclidean_space) set \<Rightarrow> 'a" where
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   431
  "interval_upperbound s = (\<Sum>i\<in>Basis. Sup {a. \<exists>x\<in>s. x\<bullet>i = a} *\<^sub>R i)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   432
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   433
definition interval_lowerbound :: "('a::ordered_euclidean_space) set \<Rightarrow> 'a" where
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   434
  "interval_lowerbound s = (\<Sum>i\<in>Basis. Inf {a. \<exists>x\<in>s. x\<bullet>i = a} *\<^sub>R i)"
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   435
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   436
lemma interval_upperbound[simp]:
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   437
  "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   438
    interval_upperbound {a..b} = (b::'a::ordered_euclidean_space)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   439
  unfolding interval_upperbound_def euclidean_representation_setsum
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   440
  by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] setle_def
51475
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
   441
           intro!: cSup_unique)
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   442
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   443
lemma interval_lowerbound[simp]:
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   444
  "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   445
    interval_lowerbound {a..b} = (a::'a::ordered_euclidean_space)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   446
  unfolding interval_lowerbound_def euclidean_representation_setsum
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   447
  by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] setge_def
51475
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 51348
diff changeset
   448
           intro!: cInf_unique)
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   449
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   450
lemmas interval_bounds = interval_upperbound interval_lowerbound
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   451
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   452
lemma interval_bounds'[simp]:
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   453
  assumes "{a..b}\<noteq>{}"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   454
  shows "interval_upperbound {a..b} = b" "interval_lowerbound {a..b} = a"
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   455
  using assms unfolding interval_ne_empty by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   456
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   457
subsection {* Content (length, area, volume...) of an interval. *}
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   458
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
   459
definition "content (s::('a::ordered_euclidean_space) set) =
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   460
  (if s = {} then 0 else (\<Prod>i\<in>Basis. (interval_upperbound s)\<bullet>i - (interval_lowerbound s)\<bullet>i))"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   461
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   462
lemma interval_not_empty:"\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> {a..b::'a::ordered_euclidean_space} \<noteq> {}"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
   463
  unfolding interval_eq_empty unfolding not_ex not_less by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
   464
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   465
lemma content_closed_interval:
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   466
  fixes a::"'a::ordered_euclidean_space"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   467
  assumes "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   468
  shows "content {a..b} = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   469
  using interval_not_empty[OF assms]
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   470
  unfolding content_def interval_upperbound[OF assms] interval_lowerbound[OF assms]
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   471
  by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   472
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   473
lemma content_closed_interval':
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   474
  fixes a::"'a::ordered_euclidean_space"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   475
  assumes "{a..b}\<noteq>{}"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   476
  shows "content {a..b} = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   477
  apply (rule content_closed_interval)
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   478
  using assms
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   479
  unfolding interval_ne_empty
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   480
  apply assumption
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   481
  done
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   482
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   483
lemma content_real:
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   484
  assumes "a\<le>b"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   485
  shows "content {a..b} = b-a"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   486
proof -
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   487
  have *: "{..<Suc 0} = {0}" by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   488
  show ?thesis unfolding content_def using assms by (auto simp: *)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
   489
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
   490
50104
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49996
diff changeset
   491
lemma content_singleton[simp]: "content {a} = 0"
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49996
diff changeset
   492
proof -
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49996
diff changeset
   493
  have "content {a .. a} = 0"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   494
    by (subst content_closed_interval) (auto simp: ex_in_conv)
50104
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49996
diff changeset
   495
  then show ?thesis by simp
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49996
diff changeset
   496
qed
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49996
diff changeset
   497
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   498
lemma content_unit[intro]: "content{0..One::'a::ordered_euclidean_space} = 1"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   499
proof -
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   500
  have *: "\<forall>i\<in>Basis. (0::'a)\<bullet>i \<le> (One::'a)\<bullet>i" by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
   501
  have "0 \<in> {0..One::'a}" unfolding mem_interval by auto
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   502
  thus ?thesis unfolding content_def interval_bounds[OF *] using setprod_1 by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   503
qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   504
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   505
lemma content_pos_le[intro]:
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   506
  fixes a::"'a::ordered_euclidean_space"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   507
  shows "0 \<le> content {a..b}"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   508
proof (cases "{a..b} = {}")
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   509
  case False
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   510
  hence *: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i" unfolding interval_ne_empty .
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   511
  have "(\<Prod>i\<in>Basis. interval_upperbound {a..b} \<bullet> i - interval_lowerbound {a..b} \<bullet> i) \<ge> 0"
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   512
    apply (rule setprod_nonneg)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   513
    unfolding interval_bounds[OF *]
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   514
    using *
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   515
    apply (erule_tac x=x in ballE)
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   516
    apply auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   517
    done
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   518
  thus ?thesis unfolding content_def by (auto simp del:interval_bounds')
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   519
qed (unfold content_def, auto)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   520
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   521
lemma content_pos_lt:
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   522
  fixes a::"'a::ordered_euclidean_space"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   523
  assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   524
  shows "0 < content {a..b}"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   525
proof -
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   526
  have help_lemma1: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i \<Longrightarrow> \<forall>i\<in>Basis. a\<bullet>i \<le> ((b\<bullet>i)::real)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   527
    apply (rule, erule_tac x=i in ballE)
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   528
    apply auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   529
    done
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   530
  show ?thesis unfolding content_closed_interval[OF help_lemma1[OF assms]]
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   531
    apply(rule setprod_pos)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   532
    using assms apply (erule_tac x=x in ballE)
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   533
    apply auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   534
    done
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   535
qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   536
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   537
lemma content_eq_0: "content{a..b::'a::ordered_euclidean_space} = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)"
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   538
proof (cases "{a..b} = {}")
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   539
  case True
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   540
  thus ?thesis
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   541
    unfolding content_def if_P[OF True]
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   542
    unfolding interval_eq_empty
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   543
    apply -
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   544
    apply (rule, erule bexE)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   545
    apply (rule_tac x = i in bexI)
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   546
    apply auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   547
    done
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   548
next
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   549
  case False
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   550
  from this[unfolded interval_eq_empty not_ex not_less]
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   551
  have as: "\<forall>i\<in>Basis. b \<bullet> i \<ge> a \<bullet> i" by fastforce
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   552
  show ?thesis
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   553
    unfolding content_def if_not_P[OF False] setprod_zero_iff[OF finite_Basis]
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   554
    using as
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   555
    by (auto intro!: bexI)
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   556
qed
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   557
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   558
lemma cond_cases:"(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)" by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   559
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   560
lemma content_closed_interval_cases:
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   561
  "content {a..b::'a::ordered_euclidean_space} =
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   562
    (if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis else 0)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   563
  by (auto simp: not_le content_eq_0 intro: less_imp_le content_closed_interval)
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   564
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   565
lemma content_eq_0_interior: "content {a..b} = 0 \<longleftrightarrow> interior({a..b}) = {}"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   566
  unfolding content_eq_0 interior_closed_interval interval_eq_empty by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   567
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   568
lemma content_pos_lt_eq: "0 < content {a..b::'a::ordered_euclidean_space} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   569
  apply rule
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   570
  defer
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   571
  apply (rule content_pos_lt, assumption)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   572
proof -
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   573
  assume "0 < content {a..b}"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   574
  hence "content {a..b} \<noteq> 0" by auto
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   575
  thus "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   576
    unfolding content_eq_0 not_ex not_le by fastforce
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   577
qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   578
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   579
lemma content_empty [simp]: "content {} = 0" unfolding content_def by auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   580
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   581
lemma content_subset:
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   582
  assumes "{a..b} \<subseteq> {c..d}"
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   583
  shows "content {a..b::'a::ordered_euclidean_space} \<le> content {c..d}"
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   584
proof (cases "{a..b} = {}")
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   585
  case True
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   586
  thus ?thesis using content_pos_le[of c d] by auto
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   587
next
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   588
  case False
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   589
  hence ab_ne:"\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i" unfolding interval_ne_empty by auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   590
  hence ab_ab:"a\<in>{a..b}" "b\<in>{a..b}" unfolding mem_interval by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   591
  have "{c..d} \<noteq> {}" using assms False by auto
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   592
  hence cd_ne:"\<forall>i\<in>Basis. c \<bullet> i \<le> d \<bullet> i" using assms unfolding interval_ne_empty by auto
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   593
  show ?thesis
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   594
    unfolding content_def
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   595
    unfolding interval_bounds[OF ab_ne] interval_bounds[OF cd_ne]
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   596
    unfolding if_not_P[OF False] if_not_P[OF `{c..d} \<noteq> {}`]
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   597
    apply (rule setprod_mono, rule)
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   598
  proof
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   599
    fix i :: 'a
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   600
    assume i: "i\<in>Basis"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   601
    show "0 \<le> b \<bullet> i - a \<bullet> i" using ab_ne[THEN bspec, OF i] i by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   602
    show "b \<bullet> i - a \<bullet> i \<le> d \<bullet> i - c \<bullet> i"
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   603
      using assms[unfolded subset_eq mem_interval,rule_format,OF ab_ab(2),of i]
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   604
      using assms[unfolded subset_eq mem_interval,rule_format,OF ab_ab(1),of i]
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   605
      using i by auto
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   606
  qed
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   607
qed
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   608
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   609
lemma content_lt_nz: "0 < content {a..b} \<longleftrightarrow> content {a..b} \<noteq> 0"
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44522
diff changeset
   610
  unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   611
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   612
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   613
subsection {* The notion of a gauge --- simply an open set containing the point. *}
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   614
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   615
definition gauge where "gauge d \<longleftrightarrow> (\<forall>x. x\<in>(d x) \<and> open(d x))"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   616
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   617
lemma gaugeI: assumes "\<And>x. x\<in>g x" "\<And>x. open (g x)" shows "gauge g"
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   618
  using assms unfolding gauge_def by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   619
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   620
lemma gaugeD[dest]: assumes "gauge d" shows "x\<in>d x" "open (d x)"
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   621
  using assms unfolding gauge_def by auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   622
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   623
lemma gauge_ball_dependent: "\<forall>x. 0 < e x \<Longrightarrow> gauge (\<lambda>x. ball x (e x))"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   624
  unfolding gauge_def by auto 
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   625
35751
f7f8d59b60b9 added lemmas
himmelma
parents: 35540
diff changeset
   626
lemma gauge_ball[intro]: "0 < e \<Longrightarrow> gauge (\<lambda>x. ball x e)" unfolding gauge_def by auto 
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   627
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   628
lemma gauge_trivial[intro]: "gauge (\<lambda>x. ball x 1)"
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   629
  by (rule gauge_ball) auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   630
35751
f7f8d59b60b9 added lemmas
himmelma
parents: 35540
diff changeset
   631
lemma gauge_inter[intro]: "gauge d1 \<Longrightarrow> gauge d2 \<Longrightarrow> gauge (\<lambda>x. (d1 x) \<inter> (d2 x))"
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   632
  unfolding gauge_def by auto 
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   633
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   634
lemma gauge_inters:
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   635
  assumes "finite s" "\<forall>d\<in>s. gauge (f d)"
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   636
  shows "gauge(\<lambda>x. \<Inter> {f d x | d. d \<in> s})"
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   637
proof -
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   638
  have *:"\<And>x. {f d x |d. d \<in> s} = (\<lambda>d. f d x) ` s" by auto
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   639
  show ?thesis
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   640
    unfolding gauge_def unfolding * 
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   641
    using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   642
qed
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   643
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   644
lemma gauge_existence_lemma: "(\<forall>x. \<exists>d::real. p x \<longrightarrow> 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. p x \<longrightarrow> q d x)"
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   645
  by(meson zero_less_one)
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   646
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   647
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   648
subsection {* Divisions. *}
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   649
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   650
definition division_of (infixl "division'_of" 40) where
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   651
  "s division_of i \<equiv>
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   652
        finite s \<and>
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   653
        (\<forall>k\<in>s. k \<subseteq> i \<and> k \<noteq> {} \<and> (\<exists>a b. k = {a..b})) \<and>
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   654
        (\<forall>k1\<in>s. \<forall>k2\<in>s. k1 \<noteq> k2 \<longrightarrow> interior(k1) \<inter> interior(k2) = {}) \<and>
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   655
        (\<Union>s = i)"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   656
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   657
lemma division_ofD[dest]:
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   658
  assumes "s division_of i"
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   659
  shows "finite s" "\<And>k. k\<in>s \<Longrightarrow> k \<subseteq> i" "\<And>k. k\<in>s \<Longrightarrow>  k \<noteq> {}" "\<And>k. k\<in>s \<Longrightarrow> (\<exists>a b. k = {a..b})"
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   660
    "\<And>k1 k2. \<lbrakk>k1\<in>s; k2\<in>s; k1 \<noteq> k2\<rbrakk> \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}" "\<Union>s = i"
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   661
  using assms unfolding division_of_def by auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   662
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   663
lemma division_ofI:
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   664
  assumes "finite s" "\<And>k. k\<in>s \<Longrightarrow> k \<subseteq> i" "\<And>k. k\<in>s \<Longrightarrow>  k \<noteq> {}" "\<And>k. k\<in>s \<Longrightarrow> (\<exists>a b. k = {a..b})"
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   665
    "\<And>k1 k2. \<lbrakk>k1\<in>s; k2\<in>s; k1 \<noteq> k2\<rbrakk> \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}" "\<Union>s = i"
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   666
  shows "s division_of i" using assms unfolding division_of_def by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   667
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   668
lemma division_of_finite: "s division_of i \<Longrightarrow> finite s"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   669
  unfolding division_of_def by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   670
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   671
lemma division_of_self[intro]: "{a..b} \<noteq> {} \<Longrightarrow> {{a..b}} division_of {a..b}"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   672
  unfolding division_of_def by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   673
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   674
lemma division_of_trivial[simp]: "s division_of {} \<longleftrightarrow> s = {}" unfolding division_of_def by auto 
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   675
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   676
lemma division_of_sing[simp]:
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   677
  "s division_of {a..a::'a::ordered_euclidean_space} \<longleftrightarrow> s = {{a..a}}" (is "?l = ?r")
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   678
proof
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   679
  assume ?r
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   680
  moreover {
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   681
    assume "s = {{a}}"
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   682
    moreover fix k assume "k\<in>s" 
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   683
    ultimately have"\<exists>x y. k = {x..y}"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   684
      apply (rule_tac x=a in exI)+
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   685
      unfolding interval_sing
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   686
      apply auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   687
      done
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   688
  }
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   689
  ultimately show ?l unfolding division_of_def interval_sing by auto
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   690
next
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   691
  assume ?l
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   692
  note as=conjunctD4[OF this[unfolded division_of_def interval_sing]]
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   693
  { fix x assume x:"x\<in>s" have "x={a}" using as(2)[rule_format,OF x] by auto }
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   694
  moreover have "s \<noteq> {}" using as(4) by auto
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   695
  ultimately show ?r unfolding interval_sing by auto
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   696
qed
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   697
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   698
lemma elementary_empty: obtains p where "p division_of {}"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   699
  unfolding division_of_trivial by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   700
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   701
lemma elementary_interval: obtains p where "p division_of {a..b}"
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   702
  by (metis division_of_trivial division_of_self)
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   703
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   704
lemma division_contains: "s division_of i \<Longrightarrow> \<forall>x\<in>i. \<exists>k\<in>s. x \<in> k"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   705
  unfolding division_of_def by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   706
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   707
lemma forall_in_division:
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   708
 "d division_of i \<Longrightarrow> ((\<forall>x\<in>d. P x) \<longleftrightarrow> (\<forall>a b. {a..b} \<in> d \<longrightarrow> P {a..b}))"
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44522
diff changeset
   709
  unfolding division_of_def by fastforce
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   710
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   711
lemma division_of_subset: assumes "p division_of (\<Union>p)" "q \<subseteq> p" shows "q division_of (\<Union>q)"
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   712
  apply (rule division_ofI)
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   713
proof -
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   714
  note as=division_ofD[OF assms(1)]
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   715
  show "finite q"
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   716
    apply (rule finite_subset)
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   717
    using as(1) assms(2) apply auto
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   718
    done
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   719
  { fix k
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   720
    assume "k \<in> q"
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   721
    hence kp:"k\<in>p" using assms(2) by auto
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   722
    show "k\<subseteq>\<Union>q" using `k \<in> q` by auto
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   723
    show "\<exists>a b. k = {a..b}" using as(4)[OF kp]
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   724
      by auto show "k \<noteq> {}" using as(3)[OF kp] by auto }
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   725
  fix k1 k2
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   726
  assume "k1 \<in> q" "k2 \<in> q" "k1 \<noteq> k2"
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   727
  hence *: "k1\<in>p" "k2\<in>p" "k1\<noteq>k2" using assms(2) by auto
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   728
  show "interior k1 \<inter> interior k2 = {}" using as(5)[OF *] by auto
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   729
qed auto
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   730
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   731
lemma division_of_union_self[intro]: "p division_of s \<Longrightarrow> p division_of (\<Union>p)"
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   732
  unfolding division_of_def by auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   733
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   734
lemma division_of_content_0:
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   735
  assumes "content {a..b} = 0" "d division_of {a..b}"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   736
  shows "\<forall>k\<in>d. content k = 0"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   737
  unfolding forall_in_division[OF assms(2)]
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   738
  apply (rule,rule,rule)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   739
  apply (drule division_ofD(2)[OF assms(2)])
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   740
  apply (drule content_subset) unfolding assms(1)
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   741
proof -
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   742
  case goal1
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   743
  thus ?case using content_pos_le[of a b] by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   744
qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   745
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   746
lemma division_inter:
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   747
  assumes "p1 division_of s1" "p2 division_of (s2::('a::ordered_euclidean_space) set)"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   748
  shows "{k1 \<inter> k2 | k1 k2 .k1 \<in> p1 \<and> k2 \<in> p2 \<and> k1 \<inter> k2 \<noteq> {}} division_of (s1 \<inter> s2)"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   749
  (is "?A' division_of _")
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   750
proof -
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   751
  let ?A = "{s. s \<in>  (\<lambda>(k1,k2). k1 \<inter> k2) ` (p1 \<times> p2) \<and> s \<noteq> {}}"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   752
  have *:"?A' = ?A" by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   753
  show ?thesis unfolding *
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   754
  proof (rule division_ofI)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   755
    have "?A \<subseteq> (\<lambda>(x, y). x \<inter> y) ` (p1 \<times> p2)" by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   756
    moreover have "finite (p1 \<times> p2)" using assms unfolding division_of_def by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   757
    ultimately show "finite ?A" by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   758
    have *:"\<And>s. \<Union>{x\<in>s. x \<noteq> {}} = \<Union>s" by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   759
    show "\<Union>?A = s1 \<inter> s2"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   760
      apply (rule set_eqI)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   761
      unfolding * and Union_image_eq UN_iff
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   762
      using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)]
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   763
      apply auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   764
      done
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   765
    { fix k
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   766
      assume "k\<in>?A"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   767
      then obtain k1 k2 where k: "k = k1 \<inter> k2" "k1\<in>p1" "k2\<in>p2" "k\<noteq>{}" by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   768
      thus "k \<noteq> {}" by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   769
      show "k \<subseteq> s1 \<inter> s2"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   770
        using division_ofD(2)[OF assms(1) k(2)] and division_ofD(2)[OF assms(2) k(3)]
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   771
        unfolding k by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   772
      guess a1 using division_ofD(4)[OF assms(1) k(2)] ..
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   773
      then guess b1 .. note ab1=this
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   774
      guess a2 using division_ofD(4)[OF assms(2) k(3)] ..
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   775
      then guess b2 .. note ab2=this
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   776
      show "\<exists>a b. k = {a..b}"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   777
        unfolding k ab1 ab2 unfolding inter_interval by auto }
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   778
    fix k1 k2
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   779
    assume "k1\<in>?A"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   780
    then obtain x1 y1 where k1:"k1 = x1 \<inter> y1" "x1\<in>p1" "y1\<in>p2" "k1\<noteq>{}" by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   781
    assume "k2\<in>?A"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   782
    then obtain x2 y2 where k2:"k2 = x2 \<inter> y2" "x2\<in>p1" "y2\<in>p2" "k2\<noteq>{}" by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   783
    assume "k1 \<noteq> k2"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   784
    hence th:"x1\<noteq>x2 \<or> y1\<noteq>y2" unfolding k1 k2 by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   785
    have *:"(interior x1 \<inter> interior x2 = {} \<or> interior y1 \<inter> interior y2 = {}) \<Longrightarrow>
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   786
      interior(x1 \<inter> y1) \<subseteq> interior(x1) \<Longrightarrow> interior(x1 \<inter> y1) \<subseteq> interior(y1) \<Longrightarrow>
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   787
      interior(x2 \<inter> y2) \<subseteq> interior(x2) \<Longrightarrow> interior(x2 \<inter> y2) \<subseteq> interior(y2)
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   788
      \<Longrightarrow> interior(x1 \<inter> y1) \<inter> interior(x2 \<inter> y2) = {}" by auto
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   789
    show "interior k1 \<inter> interior k2 = {}"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   790
      unfolding k1 k2
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   791
      apply (rule *)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   792
      defer
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   793
      apply (rule_tac[1-4] interior_mono)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   794
      using division_ofD(5)[OF assms(1) k1(2) k2(2)]
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   795
      using division_ofD(5)[OF assms(2) k1(3) k2(3)]
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   796
      using th apply auto done
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   797
  qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   798
qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   799
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   800
lemma division_inter_1:
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   801
  assumes "d division_of i" "{a..b::'a::ordered_euclidean_space} \<subseteq> i"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   802
  shows "{ {a..b} \<inter> k |k. k \<in> d \<and> {a..b} \<inter> k \<noteq> {} } division_of {a..b}"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   803
proof (cases "{a..b} = {}")
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   804
  case True
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   805
  show ?thesis unfolding True and division_of_trivial by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   806
next
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   807
  case False
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   808
  have *: "{a..b} \<inter> i = {a..b}" using assms(2) by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   809
  show ?thesis using division_inter[OF division_of_self[OF False] assms(1)] unfolding * by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   810
qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   811
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   812
lemma elementary_inter:
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   813
  assumes "p1 division_of s" "p2 division_of (t::('a::ordered_euclidean_space) set)"
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   814
  shows "\<exists>p. p division_of (s \<inter> t)"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   815
  apply rule
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   816
  apply (rule division_inter[OF assms])
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   817
  done
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   818
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   819
lemma elementary_inters:
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   820
  assumes "finite f" "f\<noteq>{}" "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::ordered_euclidean_space) set)"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   821
  shows "\<exists>p. p division_of (\<Inter> f)"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   822
  using assms
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   823
proof (induct f rule: finite_induct)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   824
  case (insert x f)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   825
  show ?case
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   826
  proof (cases "f = {}")
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   827
    case True
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   828
    thus ?thesis unfolding True using insert by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   829
  next
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   830
    case False
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   831
    guess p using insert(3)[OF False insert(5)[unfolded ball_simps,THEN conjunct2]] ..
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   832
    moreover guess px using insert(5)[rule_format,OF insertI1] ..
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   833
    ultimately show ?thesis
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   834
      unfolding Inter_insert
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   835
      apply (rule_tac elementary_inter)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   836
      apply assumption
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   837
      apply assumption
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   838
      done
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   839
  qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   840
qed auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   841
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   842
lemma division_disjoint_union:
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   843
  assumes "p1 division_of s1" "p2 division_of s2" "interior s1 \<inter> interior s2 = {}"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   844
  shows "(p1 \<union> p2) division_of (s1 \<union> s2)"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   845
proof (rule division_ofI)
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   846
  note d1 = division_ofD[OF assms(1)] and d2 = division_ofD[OF assms(2)]
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   847
  show "finite (p1 \<union> p2)" using d1(1) d2(1) by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   848
  show "\<Union>(p1 \<union> p2) = s1 \<union> s2" using d1(6) d2(6) by auto
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   849
  {
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   850
    fix k1 k2
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   851
    assume as: "k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   852
    moreover
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   853
    let ?g="interior k1 \<inter> interior k2 = {}"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   854
    {
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   855
      assume as: "k1\<in>p1" "k2\<in>p2"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   856
      have ?g
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   857
        using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]]
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   858
        using assms(3) by blast
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   859
    }
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   860
    moreover
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   861
    {
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   862
      assume as: "k1\<in>p2" "k2\<in>p1"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   863
      have ?g
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   864
        using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]]
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   865
        using assms(3) by blast
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   866
    }
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   867
    ultimately show ?g using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   868
  }
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   869
  fix k
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   870
  assume k: "k \<in> p1 \<union> p2"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   871
  show "k \<subseteq> s1 \<union> s2" using k d1(2) d2(2) by auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   872
  show "k \<noteq> {}" using k d1(3) d2(3) by auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   873
  show "\<exists>a b. k = {a..b}" using k d1(4) d2(4) by auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   874
qed
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   875
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   876
lemma partial_division_extend_1:
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   877
  assumes incl: "{c..d} \<subseteq> {a..b::'a::ordered_euclidean_space}"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   878
    and nonempty: "{c..d} \<noteq> {}"
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   879
  obtains p where "p division_of {a..b}" "{c..d} \<in> p"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   880
proof
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   881
  let ?B = "\<lambda>f::'a\<Rightarrow>'a \<times> 'a. {(\<Sum>i\<in>Basis. (fst (f i) \<bullet> i) *\<^sub>R i) .. (\<Sum>i\<in>Basis. (snd (f i) \<bullet> i) *\<^sub>R i)}"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   882
  def p \<equiv> "?B ` (Basis \<rightarrow>\<^isub>E {(a, c), (c, d), (d, b)})"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   883
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   884
  show "{c .. d} \<in> p"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   885
    unfolding p_def
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   886
    by (auto simp add: interval_eq_empty eucl_le[where 'a='a]
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   887
             intro!: image_eqI[where x="\<lambda>(i::'a)\<in>Basis. (c, d)"])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   888
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   889
  {
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   890
    fix i :: 'a
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   891
    assume "i \<in> Basis"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   892
    with incl nonempty have "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> d \<bullet> i" "d \<bullet> i \<le> b \<bullet> i"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   893
      unfolding interval_eq_empty subset_interval by (auto simp: not_le)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   894
  }
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   895
  note ord = this
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   896
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   897
  show "p division_of {a..b}"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   898
  proof (rule division_ofI)
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   899
    show "finite p" unfolding p_def by (auto intro!: finite_PiE)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   900
    {
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   901
      fix k
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   902
      assume "k \<in> p"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   903
      then obtain f where f: "f \<in> Basis \<rightarrow>\<^isub>E {(a, c), (c, d), (d, b)}" and k: "k = ?B f"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   904
        by (auto simp: p_def)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   905
      then show "\<exists>a b. k = {a..b}" by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   906
      have "k \<subseteq> {a..b} \<and> k \<noteq> {}"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   907
      proof (simp add: k interval_eq_empty subset_interval not_less, safe)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   908
        fix i :: 'a assume i: "i \<in> Basis"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   909
        moreover
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   910
        with f have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   911
          by (auto simp: PiE_iff)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   912
        moreover note ord[of i]
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   913
        ultimately
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   914
        show "a \<bullet> i \<le> fst (f i) \<bullet> i" "snd (f i) \<bullet> i \<le> b \<bullet> i" "fst (f i) \<bullet> i \<le> snd (f i) \<bullet> i"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   915
          by (auto simp: subset_iff eucl_le[where 'a='a])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   916
      qed
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   917
      then show "k \<noteq> {}" "k \<subseteq> {a .. b}" by auto
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   918
      {
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   919
        fix l assume "l \<in> p"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   920
        then obtain g where g: "g \<in> Basis \<rightarrow>\<^isub>E {(a, c), (c, d), (d, b)}" and l: "l = ?B g"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   921
          by (auto simp: p_def)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   922
        assume "l \<noteq> k"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   923
        have "\<exists>i\<in>Basis. f i \<noteq> g i"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   924
        proof (rule ccontr)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   925
          assume "\<not> (\<exists>i\<in>Basis. f i \<noteq> g i)"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   926
          with f g have "f = g"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   927
            by (auto simp: PiE_iff extensional_def intro!: ext)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   928
          with `l \<noteq> k` show False
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   929
            by (simp add: l k)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   930
        qed
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   931
        then guess i .. note * = this
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   932
        moreover from * have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   933
            "g i = (a, c) \<or> g i = (c, d) \<or> g i = (d, b)"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   934
          using f g by (auto simp: PiE_iff)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   935
        moreover note ord[of i]
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   936
        ultimately show "interior l \<inter> interior k = {}"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   937
          by (auto simp add: l k interior_closed_interval disjoint_interval intro!: bexI[of _ i])
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   938
      }
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   939
      note `k \<subseteq> { a.. b}`
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   940
    }
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   941
    moreover
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   942
    {
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   943
      fix x assume x: "x \<in> {a .. b}"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   944
      have "\<forall>i\<in>Basis. \<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   945
      proof
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   946
        fix i :: 'a assume "i \<in> Basis"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   947
        with x ord[of i] 
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   948
        have "(a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> c \<bullet> i) \<or> (c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i) \<or>
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   949
            (d \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   950
          by (auto simp: eucl_le[where 'a='a])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   951
        then show "\<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   952
          by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   953
      qed
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   954
      then guess f unfolding bchoice_iff .. note f = this
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   955
      moreover then have "restrict f Basis \<in> Basis \<rightarrow>\<^isub>E {(a, c), (c, d), (d, b)}"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   956
        by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   957
      moreover from f have "x \<in> ?B (restrict f Basis)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   958
        by (auto simp: mem_interval eucl_le[where 'a='a])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   959
      ultimately have "\<exists>k\<in>p. x \<in> k"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   960
        unfolding p_def by blast }
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   961
    ultimately show "\<Union>p = {a..b}"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   962
      by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   963
  qed
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   964
qed
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   965
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   966
lemma partial_division_extend_interval:
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   967
  assumes "p division_of (\<Union>p)" "(\<Union>p) \<subseteq> {a..b}"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   968
  obtains q where "p \<subseteq> q" "q division_of {a..b::'a::ordered_euclidean_space}"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   969
proof (cases "p = {}")
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   970
  case True
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   971
  guess q apply (rule elementary_interval[of a b]) .
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   972
  thus ?thesis
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   973
    apply -
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   974
    apply (rule that[of q])
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   975
    unfolding True
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   976
    apply auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   977
    done
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   978
next
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   979
  case False
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   980
  note p = division_ofD[OF assms(1)]
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   981
  have *: "\<forall>k\<in>p. \<exists>q. q division_of {a..b} \<and> k\<in>q"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   982
  proof
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   983
    case goal1
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   984
    guess c using p(4)[OF goal1] ..
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   985
    then guess d .. note "cd" = this
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   986
    have *: "{c..d} \<subseteq> {a..b}" "{c..d} \<noteq> {}"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   987
      using p(2,3)[OF goal1, unfolded "cd"] using assms(2) by auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   988
    guess q apply(rule partial_division_extend_1[OF *]) .
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   989
    thus ?case unfolding "cd" by auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   990
  qed
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   991
  guess q using bchoice[OF *] .. note q = conjunctD2[OF this[rule_format]]
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   992
  have "\<And>x. x\<in>p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   993
    apply (rule, rule_tac p="q x" in division_of_subset)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   994
  proof -
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   995
    fix x
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   996
    assume x: "x\<in>p"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   997
    show "q x division_of \<Union>q x"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   998
      apply -
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   999
      apply (rule division_ofI)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1000
      using division_ofD[OF q(1)[OF x]]
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1001
      apply auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1002
      done
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1003
    show "q x - {x} \<subseteq> q x" by auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1004
  qed
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1005
  hence "\<exists>d. d division_of \<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1006
    apply -
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1007
    apply (rule elementary_inters)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1008
    apply (rule finite_imageI[OF p(1)])
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1009
    unfolding image_is_empty
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1010
    apply (rule False)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1011
    apply auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1012
    done
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1013
  then guess d .. note d = this
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1014
  show ?thesis
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1015
    apply (rule that[of "d \<union> p"])
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1016
  proof -
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1017
    have *: "\<And>s f t. s \<noteq> {} \<Longrightarrow> (\<forall>i\<in>s. f i \<union> i = t) \<Longrightarrow> t = \<Inter> (f ` s) \<union> (\<Union>s)" by auto
52141
eff000cab70f weaker precendence of syntax for big intersection and union on sets
haftmann
parents: 51642
diff changeset
  1018
    have *: "{a..b} = \<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p) \<union> \<Union>p"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1019
      apply (rule *[OF False])
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1020
    proof
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1021
      fix i
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1022
      assume i: "i\<in>p"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1023
      show "\<Union>(q i - {i}) \<union> i = {a..b}"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1024
        using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1025
    qed
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1026
    show "d \<union> p division_of {a..b}"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1027
      unfolding *
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1028
      apply (rule division_disjoint_union[OF d assms(1)])
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1029
      apply (rule inter_interior_unions_intervals)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1030
      apply (rule p open_interior ballI)+
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1031
    proof (assumption, rule)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1032
      fix k
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1033
      assume k: "k\<in>p"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1034
      have *: "\<And>u t s. u \<subseteq> s \<Longrightarrow> s \<inter> t = {} \<Longrightarrow> u \<inter> t = {}" by auto
52141
eff000cab70f weaker precendence of syntax for big intersection and union on sets
haftmann
parents: 51642
diff changeset
  1035
      show "interior (\<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)) \<inter> interior k = {}"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1036
        apply (rule *[of _ "interior (\<Union>(q k - {k}))"])
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1037
        defer
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1038
        apply (subst Int_commute)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1039
        apply (rule inter_interior_unions_intervals)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1040
      proof -
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1041
        note qk=division_ofD[OF q(1)[OF k]]
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1042
        show "finite (q k - {k})" "open (interior k)"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1043
          "\<forall>t\<in>q k - {k}. \<exists>a b. t = {a..b}" using qk by auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1044
        show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1045
          using qk(5) using q(2)[OF k] by auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1046
        have *: "\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x" by auto
52141
eff000cab70f weaker precendence of syntax for big intersection and union on sets
haftmann
parents: 51642
diff changeset
  1047
        show "interior (\<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)) \<subseteq> interior (\<Union>(q k - {k}))"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1048
          apply (rule interior_mono *)+
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1049
          using k by auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1050
      qed
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1051
    qed
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1052
  qed auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1053
qed
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1054
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
  1055
lemma elementary_bounded[dest]: "p division_of s \<Longrightarrow> bounded (s::('a::ordered_euclidean_space) set)"
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1056
  unfolding division_of_def by(metis bounded_Union bounded_interval) 
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1057
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
  1058
lemma elementary_subset_interval: "p division_of s \<Longrightarrow> \<exists>a b. s \<subseteq> {a..b::'a::ordered_euclidean_space}"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1059
  by (meson elementary_bounded bounded_subset_closed_interval)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1060
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1061
lemma division_union_intervals_exists:
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1062
  assumes "{a..b::'a::ordered_euclidean_space} \<noteq> {}"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1063
  obtains p where "(insert {a..b} p) division_of ({a..b} \<union> {c..d})"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1064
proof (cases "{c..d} = {}")
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1065
  case True
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1066
  show ?thesis
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1067
    apply (rule that[of "{}"])
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1068
    unfolding True
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1069
    using assms
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1070
    apply auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1071
    done
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1072
next
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1073
  case False
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1074
  note false=this
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1075
  show ?thesis
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1076
  proof (cases "{a..b} \<inter> {c..d} = {}")
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1077
    case True
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1078
    have *:"\<And>a b. {a,b} = {a} \<union> {b}" by auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1079
    show ?thesis
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1080
      apply (rule that[of "{{c..d}}"])
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1081
      unfolding *
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1082
      apply (rule division_disjoint_union)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1083
      using false True assms
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1084
      using interior_subset
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1085
      apply auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1086
      done
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1087
  next
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1088
    case False
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1089
    obtain u v where uv: "{a..b} \<inter> {c..d} = {u..v}"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1090
      unfolding inter_interval by auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1091
    have *: "{u..v} \<subseteq> {c..d}" using uv by auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1092
    guess p apply (rule partial_division_extend_1[OF * False[unfolded uv]]) .
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1093
    note p=this division_ofD[OF this(1)]
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1094
    have *: "{a..b} \<union> {c..d} = {a..b} \<union> \<Union>(p - {{u..v}})" "\<And>x s. insert x s = {x} \<union> s"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1095
      using p(8) unfolding uv[THEN sym] by auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1096
    show ?thesis
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1097
      apply (rule that[of "p - {{u..v}}"])
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1098
      unfolding *(1)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1099
      apply (subst *(2))
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1100
      apply (rule division_disjoint_union)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1101
      apply (rule, rule assms)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1102
      apply (rule division_of_subset[of p])
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1103
      apply (rule division_of_union_self[OF p(1)])
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1104
      defer
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1105
      unfolding interior_inter[THEN sym]
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1106
    proof -
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1107
      have *: "\<And>cd p uv ab. p \<subseteq> cd \<Longrightarrow> ab \<inter> cd = uv \<Longrightarrow> ab \<inter> p = uv \<inter> p" by auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1108
      have "interior ({a..b} \<inter> \<Union>(p - {{u..v}})) = interior({u..v} \<inter> \<Union>(p - {{u..v}}))" 
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1109
        apply (rule arg_cong[of _ _ interior])
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1110
        apply (rule *[OF _ uv])
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1111
        using p(8)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1112
        apply auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1113
        done
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1114
      also have "\<dots> = {}"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1115
        unfolding interior_inter
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1116
        apply (rule inter_interior_unions_intervals)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1117
        using p(6) p(7)[OF p(2)] p(3)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1118
        apply auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1119
        done
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1120
      finally show "interior ({a..b} \<inter> \<Union>(p - {{u..v}})) = {}" .
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1121
    qed auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1122
  qed
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1123
qed
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1124
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1125
lemma division_of_unions: assumes "finite f"  "\<And>p. p\<in>f \<Longrightarrow> p division_of (\<Union>p)"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1126
  "\<And>k1 k2. \<lbrakk>k1 \<in> \<Union>f; k2 \<in> \<Union>f; k1 \<noteq> k2\<rbrakk> \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1127
  shows "\<Union>f division_of \<Union>\<Union>f" apply(rule division_ofI) prefer 5 apply(rule assms(3)|assumption)+
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1128
  apply(rule finite_Union assms(1))+ prefer 3 apply(erule UnionE) apply(rule_tac s=X in division_ofD(3)[OF assms(2)])
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1129
  using division_ofD[OF assms(2)] by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1130
  
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1131
lemma elementary_union_interval: assumes "p division_of \<Union>p"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
  1132
  obtains q where "q division_of ({a..b::'a::ordered_euclidean_space} \<union> \<Union>p)" proof-
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1133
  note assm=division_ofD[OF assms]
52141
eff000cab70f weaker precendence of syntax for big intersection and union on sets
haftmann
parents: 51642
diff changeset
  1134
  have lem1:"\<And>f s. \<Union>\<Union> (f ` s) = \<Union>((\<lambda>x.\<Union>(f x)) ` s)" by auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1135
  have lem2:"\<And>f s. f \<noteq> {} \<Longrightarrow> \<Union>{s \<union> t |t. t \<in> f} = s \<union> \<Union>f" by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1136
{ presume "p={} \<Longrightarrow> thesis" "{a..b} = {} \<Longrightarrow> thesis" "{a..b} \<noteq> {} \<Longrightarrow> interior {a..b} = {} \<Longrightarrow> thesis"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1137
    "p\<noteq>{} \<Longrightarrow> interior {a..b}\<noteq>{} \<Longrightarrow> {a..b} \<noteq> {} \<Longrightarrow> thesis"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1138
  thus thesis by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1139
next assume as:"p={}" guess p apply(rule elementary_interval[of a b]) .
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1140
  thus thesis apply(rule_tac that[of p]) unfolding as by auto 
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1141
next assume as:"{a..b}={}" show thesis apply(rule that) unfolding as using assms by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1142
next assume as:"interior {a..b} = {}" "{a..b} \<noteq> {}"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1143
  show thesis apply(rule that[of "insert {a..b} p"],rule division_ofI)
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1144
    unfolding finite_insert apply(rule assm(1)) unfolding Union_insert  
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44522
diff changeset
  1145
    using assm(2-4) as apply- by(fastforce dest: assm(5))+
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1146
next assume as:"p \<noteq> {}" "interior {a..b} \<noteq> {}" "{a..b}\<noteq>{}"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1147
  have "\<forall>k\<in>p. \<exists>q. (insert {a..b} q) division_of ({a..b} \<union> k)" proof case goal1
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1148
    from assm(4)[OF this] guess c .. then guess d ..
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1149
    thus ?case apply-apply(rule division_union_intervals_exists[OF as(3),of c d]) by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1150
  qed from bchoice[OF this] guess q .. note q=division_ofD[OF this[rule_format]]
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1151
  let ?D = "\<Union>{insert {a..b} (q k) | k. k \<in> p}"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1152
  show thesis apply(rule that[of "?D"]) proof(rule division_ofI)
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1153
    have *:"{insert {a..b} (q k) |k. k \<in> p} = (\<lambda>k. insert {a..b} (q k)) ` p" by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1154
    show "finite ?D" apply(rule finite_Union) unfolding * apply(rule finite_imageI) using assm(1) q(1) by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1155
    show "\<Union>?D = {a..b} \<union> \<Union>p" unfolding * lem1 unfolding lem2[OF as(1), of "{a..b}",THEN sym]
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1156
      using q(6) by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1157
    fix k assume k:"k\<in>?D" thus " k \<subseteq> {a..b} \<union> \<Union>p" using q(2) by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1158
    show "k \<noteq> {}" using q(3) k by auto show "\<exists>a b. k = {a..b}" using q(4) k by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1159
    fix k' assume k':"k'\<in>?D" "k\<noteq>k'"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1160
    obtain x  where x: "k \<in>insert {a..b} (q x)"  "x\<in>p"  using k  by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1161
    obtain x' where x':"k'\<in>insert {a..b} (q x')" "x'\<in>p" using k' by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1162
    show "interior k \<inter> interior k' = {}" proof(cases "x=x'")
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1163
      case True show ?thesis apply(rule q(5)) using x x' k' unfolding True by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1164
    next case False 
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1165
      { presume "k = {a..b} \<Longrightarrow> ?thesis" "k' = {a..b} \<Longrightarrow> ?thesis" 
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1166
        "k \<noteq> {a..b} \<Longrightarrow> k' \<noteq> {a..b} \<Longrightarrow> ?thesis"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1167
        thus ?thesis by auto }
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1168
      { assume as':"k  = {a..b}" show ?thesis apply(rule q(5)) using x' k'(2) unfolding as' by auto }
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1169
      { assume as':"k' = {a..b}" show ?thesis apply(rule q(5)) using x  k'(2) unfolding as' by auto }
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1170
      assume as':"k \<noteq> {a..b}" "k' \<noteq> {a..b}"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1171
      guess c using q(4)[OF x(2,1)] .. then guess d .. note c_d=this
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1172
      have "interior k  \<inter> interior {a..b} = {}" apply(rule q(5)) using x  k'(2) using as' by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1173
      hence "interior k \<subseteq> interior x" apply-
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1174
        apply(rule interior_subset_union_intervals[OF c_d _ as(2) q(2)[OF x(2,1)]]) by auto moreover
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1175
      guess c using q(4)[OF x'(2,1)] .. then guess d .. note c_d=this
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1176
      have "interior k' \<inter> interior {a..b} = {}" apply(rule q(5)) using x' k'(2) using as' by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1177
      hence "interior k' \<subseteq> interior x'" apply-
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1178
        apply(rule interior_subset_union_intervals[OF c_d _ as(2) q(2)[OF x'(2,1)]]) by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1179
      ultimately show ?thesis using assm(5)[OF x(2) x'(2) False] by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1180
    qed qed } qed
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1181
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1182
lemma elementary_unions_intervals:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
  1183
  assumes "finite f" "\<And>s. s \<in> f \<Longrightarrow> \<exists>a b. s = {a..b::'a::ordered_euclidean_space}"
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1184
  obtains p where "p division_of (\<Union>f)" proof-
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1185
  have "\<exists>p. p division_of (\<Union>f)" proof(induct_tac f rule:finite_subset_induct) 
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1186
    show "\<exists>p. p division_of \<Union>{}" using elementary_empty by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1187
    fix x F assume as:"finite F" "x \<notin> F" "\<exists>p. p division_of \<Union>F" "x\<in>f"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1188
    from this(3) guess p .. note p=this
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1189
    from assms(2)[OF as(4)] guess a .. then guess b .. note ab=this
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1190
    have *:"\<Union>F = \<Union>p" using division_ofD[OF p] by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1191
    show "\<exists>p. p division_of \<Union>insert x F" using elementary_union_interval[OF p[unfolded *], of a b]
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1192
      unfolding Union_insert ab * by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1193
  qed(insert assms,auto) thus ?thesis apply-apply(erule exE,rule that) by auto qed
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1194
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
  1195
lemma elementary_union: assumes "ps division_of s" "pt division_of (t::('a::ordered_euclidean_space) set)"
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1196
  obtains p where "p division_of (s \<union> t)"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1197
proof- have "s \<union> t = \<Union>ps \<union> \<Union>pt" using assms unfolding division_of_def by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1198
  hence *:"\<Union>(ps \<union> pt) = s \<union> t" by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1199
  show ?thesis apply-apply(rule elementary_unions_intervals[of "ps\<union>pt"])
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1200
    unfolding * prefer 3 apply(rule_tac p=p in that)
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1201
    using assms[unfolded division_of_def] by auto qed
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1202
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
  1203
lemma partial_division_extend: fixes t::"('a::ordered_euclidean_space) set"
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1204
  assumes "p division_of s" "q division_of t" "s \<subseteq> t"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1205
  obtains r where "p \<subseteq> r" "r division_of t" proof-
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1206
  note divp = division_ofD[OF assms(1)] and divq = division_ofD[OF assms(2)]
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1207
  obtain a b where ab:"t\<subseteq>{a..b}" using elementary_subset_interval[OF assms(2)] by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1208
  guess r1 apply(rule partial_division_extend_interval) apply(rule assms(1)[unfolded divp(6)[THEN sym]])
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1209
    apply(rule subset_trans) by(rule ab assms[unfolded divp(6)[THEN sym]])+  note r1 = this division_ofD[OF this(2)]
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1210
  guess p' apply(rule elementary_unions_intervals[of "r1 - p"]) using r1(3,6) by auto 
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1211
  then obtain r2 where r2:"r2 division_of (\<Union>(r1 - p)) \<inter> (\<Union>q)" 
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1212
    apply- apply(drule elementary_inter[OF _ assms(2)[unfolded divq(6)[THEN sym]]]) by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1213
  { fix x assume x:"x\<in>t" "x\<notin>s"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1214
    hence "x\<in>\<Union>r1" unfolding r1 using ab by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1215
    then guess r unfolding Union_iff .. note r=this moreover
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1216
    have "r \<notin> p" proof assume "r\<in>p" hence "x\<in>s" using divp(2) r by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1217
      thus False using x by auto qed
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1218
    ultimately have "x\<in>\<Union>(r1 - p)" by auto }