merged
authorwenzelm
Thu Jan 17 15:50:56 2013 +0100 (2013-01-17)
changeset 509478757e6aa50eb
parent 50944 03b11adf1f33
parent 50946 8ad3e376f63e
child 50948 8c742f9de9f5
child 50956 d58dae9079a6
merged
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu Jan 17 14:38:12 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Jan 17 15:50:56 2013 +0100
     1.3 @@ -89,7 +89,8 @@
     1.4        case True
     1.5        show ?thesis
     1.6          apply (rule assms[OF Suc(1)[OF True]])
     1.7 -        using `?r` apply auto
     1.8 +        using `?r`
     1.9 +        apply auto
    1.10          done
    1.11      next
    1.12        case False
    1.13 @@ -241,7 +242,8 @@
    1.14            thus ?thesis
    1.15              apply (rule_tac x=i in bexI, rule_tac x=x in exI, rule_tac x="min d e" in exI)
    1.16              unfolding ab
    1.17 -            using interval_open_subset_closed[of a b] and e apply fastforce+
    1.18 +            using interval_open_subset_closed[of a b] and e
    1.19 +            apply fastforce+
    1.20              done
    1.21          next
    1.22            case False
    1.23 @@ -285,8 +287,10 @@
    1.24                  done
    1.25                also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2"
    1.26                  apply (rule add_strict_left_mono)
    1.27 -                using as unfolding mem_ball dist_norm
    1.28 -                using e apply (auto simp add: field_simps)
    1.29 +                using as
    1.30 +                unfolding mem_ball dist_norm
    1.31 +                using e
    1.32 +                apply (auto simp add: field_simps)
    1.33                  done
    1.34                finally show "y\<in>ball x e"
    1.35                  unfolding mem_ball dist_norm using e by (auto simp add:field_simps)
    1.36 @@ -415,7 +419,8 @@
    1.37    assumes "{a..b}\<noteq>{}"
    1.38    shows "content {a..b} = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
    1.39    apply (rule content_closed_interval)
    1.40 -  using assms unfolding interval_ne_empty
    1.41 +  using assms
    1.42 +  unfolding interval_ne_empty
    1.43    apply assumption
    1.44    done
    1.45  
    1.46 @@ -533,10 +538,10 @@
    1.47      unfolding content_def
    1.48      unfolding interval_bounds[OF ab_ne] interval_bounds[OF cd_ne]
    1.49      unfolding if_not_P[OF False] if_not_P[OF `{c..d} \<noteq> {}`]
    1.50 -    apply(rule setprod_mono,rule)
    1.51 +    apply (rule setprod_mono, rule)
    1.52    proof
    1.53      fix i :: 'a
    1.54 -    assume i:"i\<in>Basis"
    1.55 +    assume i: "i\<in>Basis"
    1.56      show "0 \<le> b \<bullet> i - a \<bullet> i" using ab_ne[THEN bspec, OF i] i by auto
    1.57      show "b \<bullet> i - a \<bullet> i \<le> d \<bullet> i - c \<bullet> i"
    1.58        using assms[unfolded subset_eq mem_interval,rule_format,OF ab_ab(2),of i]
    1.59 @@ -620,7 +625,10 @@
    1.60      assume "s = {{a}}"
    1.61      moreover fix k assume "k\<in>s" 
    1.62      ultimately have"\<exists>x y. k = {x..y}"
    1.63 -      apply (rule_tac x=a in exI)+ unfolding interval_sing by auto
    1.64 +      apply (rule_tac x=a in exI)+
    1.65 +      unfolding interval_sing
    1.66 +      apply auto
    1.67 +      done
    1.68    }
    1.69    ultimately show ?l unfolding division_of_def interval_sing by auto
    1.70  next
    1.71 @@ -671,9 +679,9 @@
    1.72    assumes "content {a..b} = 0" "d division_of {a..b}"
    1.73    shows "\<forall>k\<in>d. content k = 0"
    1.74    unfolding forall_in_division[OF assms(2)]
    1.75 -  apply(rule,rule,rule)
    1.76 -  apply(drule division_ofD(2)[OF assms(2)])
    1.77 -  apply(drule content_subset) unfolding assms(1)
    1.78 +  apply (rule,rule,rule)
    1.79 +  apply (drule division_ofD(2)[OF assms(2)])
    1.80 +  apply (drule content_subset) unfolding assms(1)
    1.81  proof -
    1.82    case goal1
    1.83    thus ?case using content_pos_le[of a b] by auto
    1.84 @@ -748,7 +756,9 @@
    1.85  lemma elementary_inter:
    1.86    assumes "p1 division_of s" "p2 division_of (t::('a::ordered_euclidean_space) set)"
    1.87    shows "\<exists>p. p division_of (s \<inter> t)"
    1.88 -  by (rule, rule division_inter[OF assms])
    1.89 +  apply rule
    1.90 +  apply (rule division_inter[OF assms])
    1.91 +  done
    1.92  
    1.93  lemma elementary_inters:
    1.94    assumes "finite f" "f\<noteq>{}" "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::ordered_euclidean_space) set)"
    1.95 @@ -775,21 +785,41 @@
    1.96  
    1.97  lemma division_disjoint_union:
    1.98    assumes "p1 division_of s1" "p2 division_of s2" "interior s1 \<inter> interior s2 = {}"
    1.99 -  shows "(p1 \<union> p2) division_of (s1 \<union> s2)" proof(rule division_ofI) 
   1.100 +  shows "(p1 \<union> p2) division_of (s1 \<union> s2)"
   1.101 +proof (rule division_ofI)
   1.102    note d1 = division_ofD[OF assms(1)] and d2 = division_ofD[OF assms(2)]
   1.103    show "finite (p1 \<union> p2)" using d1(1) d2(1) by auto
   1.104    show "\<Union>(p1 \<union> p2) = s1 \<union> s2" using d1(6) d2(6) by auto
   1.105 -  { fix k1 k2 assume as:"k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2" moreover let ?g="interior k1 \<inter> interior k2 = {}"
   1.106 -  { assume as:"k1\<in>p1" "k2\<in>p2" have ?g using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]]
   1.107 -      using assms(3) by blast } moreover
   1.108 -  { assume as:"k1\<in>p2" "k2\<in>p1" have ?g using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]]
   1.109 -      using assms(3) by blast} ultimately
   1.110 -  show ?g using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto }
   1.111 -  fix k assume k:"k \<in> p1 \<union> p2"  show "k \<subseteq> s1 \<union> s2" using k d1(2) d2(2) by auto
   1.112 -  show "k \<noteq> {}" using k d1(3) d2(3) by auto show "\<exists>a b. k = {a..b}" using k d1(4) d2(4) by auto qed
   1.113 +  {
   1.114 +    fix k1 k2
   1.115 +    assume as: "k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2"
   1.116 +    moreover
   1.117 +    let ?g="interior k1 \<inter> interior k2 = {}"
   1.118 +    {
   1.119 +      assume as: "k1\<in>p1" "k2\<in>p2"
   1.120 +      have ?g
   1.121 +        using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]]
   1.122 +        using assms(3) by blast
   1.123 +    }
   1.124 +    moreover
   1.125 +    {
   1.126 +      assume as: "k1\<in>p2" "k2\<in>p1"
   1.127 +      have ?g
   1.128 +        using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]]
   1.129 +        using assms(3) by blast
   1.130 +    }
   1.131 +    ultimately show ?g using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto
   1.132 +  }
   1.133 +  fix k
   1.134 +  assume k: "k \<in> p1 \<union> p2"
   1.135 +  show "k \<subseteq> s1 \<union> s2" using k d1(2) d2(2) by auto
   1.136 +  show "k \<noteq> {}" using k d1(3) d2(3) by auto
   1.137 +  show "\<exists>a b. k = {a..b}" using k d1(4) d2(4) by auto
   1.138 +qed
   1.139  
   1.140  lemma partial_division_extend_1:
   1.141 -  assumes incl: "{c..d} \<subseteq> {a..b::'a::ordered_euclidean_space}" and nonempty: "{c..d} \<noteq> {}"
   1.142 +  assumes incl: "{c..d} \<subseteq> {a..b::'a::ordered_euclidean_space}"
   1.143 +    and nonempty: "{c..d} \<noteq> {}"
   1.144    obtains p where "p division_of {a..b}" "{c..d} \<in> p"
   1.145  proof
   1.146    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)}"
   1.147 @@ -800,52 +830,61 @@
   1.148      by (auto simp add: interval_eq_empty eucl_le[where 'a='a]
   1.149               intro!: image_eqI[where x="\<lambda>(i::'a)\<in>Basis. (c, d)"])
   1.150  
   1.151 -  {  fix i :: 'a assume "i \<in> Basis"
   1.152 +  {
   1.153 +    fix i :: 'a
   1.154 +    assume "i \<in> Basis"
   1.155      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"
   1.156 -      unfolding interval_eq_empty subset_interval by (auto simp: not_le) }
   1.157 +      unfolding interval_eq_empty subset_interval by (auto simp: not_le)
   1.158 +  }
   1.159    note ord = this
   1.160  
   1.161    show "p division_of {a..b}"
   1.162    proof (rule division_ofI)
   1.163 -    show "finite p"
   1.164 -      unfolding p_def by (auto intro!: finite_PiE)
   1.165 -    { fix k assume "k \<in> p"
   1.166 +    show "finite p" unfolding p_def by (auto intro!: finite_PiE)
   1.167 +    {
   1.168 +      fix k
   1.169 +      assume "k \<in> p"
   1.170        then obtain f where f: "f \<in> Basis \<rightarrow>\<^isub>E {(a, c), (c, d), (d, b)}" and k: "k = ?B f"
   1.171          by (auto simp: p_def)
   1.172        then show "\<exists>a b. k = {a..b}" by auto
   1.173        have "k \<subseteq> {a..b} \<and> k \<noteq> {}"
   1.174        proof (simp add: k interval_eq_empty subset_interval not_less, safe)
   1.175          fix i :: 'a assume i: "i \<in> Basis"
   1.176 -        moreover with f have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
   1.177 +        moreover
   1.178 +        with f have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
   1.179            by (auto simp: PiE_iff)
   1.180          moreover note ord[of i]
   1.181 -        ultimately 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"
   1.182 +        ultimately
   1.183 +        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"
   1.184            by (auto simp: subset_iff eucl_le[where 'a='a])
   1.185        qed
   1.186        then show "k \<noteq> {}" "k \<subseteq> {a .. b}" by auto
   1.187 -      { 
   1.188 -      fix l assume "l \<in> p"
   1.189 -      then obtain g where g: "g \<in> Basis \<rightarrow>\<^isub>E {(a, c), (c, d), (d, b)}" and l: "l = ?B g"
   1.190 -        by (auto simp: p_def)
   1.191 -      assume "l \<noteq> k"
   1.192 -      have "\<exists>i\<in>Basis. f i \<noteq> g i"
   1.193 -      proof (rule ccontr)
   1.194 -        assume "\<not> (\<exists>i\<in>Basis. f i \<noteq> g i)"
   1.195 -        with f g have "f = g"
   1.196 -          by (auto simp: PiE_iff extensional_def intro!: ext)
   1.197 -        with `l \<noteq> k` show False
   1.198 -          by (simp add: l k)
   1.199 -      qed
   1.200 -      then guess i ..
   1.201 -      moreover then have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
   1.202 -          "g i = (a, c) \<or> g i = (c, d) \<or> g i = (d, b)"
   1.203 -        using f g by (auto simp: PiE_iff)
   1.204 -      moreover note ord[of i]
   1.205 -      ultimately show "interior l \<inter> interior k = {}"
   1.206 -        by (auto simp add: l k interior_closed_interval disjoint_interval intro!: bexI[of _ i]) }
   1.207 -      note `k \<subseteq> { a.. b}` }
   1.208 +      {
   1.209 +        fix l assume "l \<in> p"
   1.210 +        then obtain g where g: "g \<in> Basis \<rightarrow>\<^isub>E {(a, c), (c, d), (d, b)}" and l: "l = ?B g"
   1.211 +          by (auto simp: p_def)
   1.212 +        assume "l \<noteq> k"
   1.213 +        have "\<exists>i\<in>Basis. f i \<noteq> g i"
   1.214 +        proof (rule ccontr)
   1.215 +          assume "\<not> (\<exists>i\<in>Basis. f i \<noteq> g i)"
   1.216 +          with f g have "f = g"
   1.217 +            by (auto simp: PiE_iff extensional_def intro!: ext)
   1.218 +          with `l \<noteq> k` show False
   1.219 +            by (simp add: l k)
   1.220 +        qed
   1.221 +        then guess i .. note * = this
   1.222 +        moreover from * have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
   1.223 +            "g i = (a, c) \<or> g i = (c, d) \<or> g i = (d, b)"
   1.224 +          using f g by (auto simp: PiE_iff)
   1.225 +        moreover note ord[of i]
   1.226 +        ultimately show "interior l \<inter> interior k = {}"
   1.227 +          by (auto simp add: l k interior_closed_interval disjoint_interval intro!: bexI[of _ i])
   1.228 +      }
   1.229 +      note `k \<subseteq> { a.. b}`
   1.230 +    }
   1.231      moreover
   1.232 -    { fix x assume x: "x \<in> {a .. b}"
   1.233 +    {
   1.234 +      fix x assume x: "x \<in> {a .. b}"
   1.235        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)}"
   1.236        proof
   1.237          fix i :: 'a assume "i \<in> Basis"
   1.238 @@ -868,61 +907,164 @@
   1.239    qed
   1.240  qed
   1.241  
   1.242 -lemma partial_division_extend_interval: assumes "p division_of (\<Union>p)" "(\<Union>p) \<subseteq> {a..b}"
   1.243 -  obtains q where "p \<subseteq> q" "q division_of {a..b::'a::ordered_euclidean_space}" proof(cases "p = {}")
   1.244 -  case True guess q apply(rule elementary_interval[of a b]) .
   1.245 -  thus ?thesis apply- apply(rule that[of q]) unfolding True by auto next
   1.246 -  case False note p = division_ofD[OF assms(1)]
   1.247 -  have *:"\<forall>k\<in>p. \<exists>q. q division_of {a..b} \<and> k\<in>q" proof case goal1
   1.248 -    guess c using p(4)[OF goal1] .. then guess d .. note "cd" = this
   1.249 -    have *:"{c..d} \<subseteq> {a..b}" "{c..d} \<noteq> {}" using p(2,3)[OF goal1, unfolded "cd"] using assms(2) by auto
   1.250 -    guess q apply(rule partial_division_extend_1[OF *]) . thus ?case unfolding "cd" by auto qed
   1.251 +lemma partial_division_extend_interval:
   1.252 +  assumes "p division_of (\<Union>p)" "(\<Union>p) \<subseteq> {a..b}"
   1.253 +  obtains q where "p \<subseteq> q" "q division_of {a..b::'a::ordered_euclidean_space}"
   1.254 +proof (cases "p = {}")
   1.255 +  case True
   1.256 +  guess q apply (rule elementary_interval[of a b]) .
   1.257 +  thus ?thesis
   1.258 +    apply -
   1.259 +    apply (rule that[of q])
   1.260 +    unfolding True
   1.261 +    apply auto
   1.262 +    done
   1.263 +next
   1.264 +  case False
   1.265 +  note p = division_ofD[OF assms(1)]
   1.266 +  have *: "\<forall>k\<in>p. \<exists>q. q division_of {a..b} \<and> k\<in>q"
   1.267 +  proof
   1.268 +    case goal1
   1.269 +    guess c using p(4)[OF goal1] ..
   1.270 +    then guess d .. note "cd" = this
   1.271 +    have *: "{c..d} \<subseteq> {a..b}" "{c..d} \<noteq> {}"
   1.272 +      using p(2,3)[OF goal1, unfolded "cd"] using assms(2) by auto
   1.273 +    guess q apply(rule partial_division_extend_1[OF *]) .
   1.274 +    thus ?case unfolding "cd" by auto
   1.275 +  qed
   1.276    guess q using bchoice[OF *] .. note q = conjunctD2[OF this[rule_format]]
   1.277 -  have "\<And>x. x\<in>p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})" apply(rule,rule_tac p="q x" in division_of_subset) proof-
   1.278 -    fix x assume x:"x\<in>p" show "q x division_of \<Union>q x" apply-apply(rule division_ofI)
   1.279 -      using division_ofD[OF q(1)[OF x]] by auto show "q x - {x} \<subseteq> q x" by auto qed
   1.280 -  hence "\<exists>d. d division_of \<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)" apply- apply(rule elementary_inters)
   1.281 -    apply(rule finite_imageI[OF p(1)]) unfolding image_is_empty apply(rule False) by auto
   1.282 +  have "\<And>x. x\<in>p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
   1.283 +    apply (rule, rule_tac p="q x" in division_of_subset)
   1.284 +  proof -
   1.285 +    fix x
   1.286 +    assume x: "x\<in>p"
   1.287 +    show "q x division_of \<Union>q x"
   1.288 +      apply -
   1.289 +      apply (rule division_ofI)
   1.290 +      using division_ofD[OF q(1)[OF x]]
   1.291 +      apply auto
   1.292 +      done
   1.293 +    show "q x - {x} \<subseteq> q x" by auto
   1.294 +  qed
   1.295 +  hence "\<exists>d. d division_of \<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)"
   1.296 +    apply -
   1.297 +    apply (rule elementary_inters)
   1.298 +    apply (rule finite_imageI[OF p(1)])
   1.299 +    unfolding image_is_empty
   1.300 +    apply (rule False)
   1.301 +    apply auto
   1.302 +    done
   1.303    then guess d .. note d = this
   1.304 -  show ?thesis apply(rule that[of "d \<union> p"]) proof-
   1.305 -    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
   1.306 -    have *:"{a..b} = \<Inter> (\<lambda>i. \<Union>(q i - {i})) ` p \<union> \<Union>p" apply(rule *[OF False]) proof fix i assume i:"i\<in>p"
   1.307 -      show "\<Union>(q i - {i}) \<union> i = {a..b}" using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto qed
   1.308 -    show "d \<union> p division_of {a..b}" unfolding * apply(rule division_disjoint_union[OF d assms(1)])
   1.309 -      apply(rule inter_interior_unions_intervals) apply(rule p open_interior ballI)+ proof(assumption,rule)
   1.310 -      fix k assume k:"k\<in>p" have *:"\<And>u t s. u \<subseteq> s \<Longrightarrow> s \<inter> t = {} \<Longrightarrow> u \<inter> t = {}" by auto
   1.311 -      show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<inter> interior k = {}" apply(rule *[of _ "interior (\<Union>(q k - {k}))"])
   1.312 -        defer apply(subst Int_commute) apply(rule inter_interior_unions_intervals) proof- note qk=division_ofD[OF q(1)[OF k]]
   1.313 -        show "finite (q k - {k})" "open (interior k)"  "\<forall>t\<in>q k - {k}. \<exists>a b. t = {a..b}" using qk by auto
   1.314 -        show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}" using qk(5) using q(2)[OF k] by auto
   1.315 -        have *:"\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x" by auto show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<subseteq> interior (\<Union>(q k - {k}))"
   1.316 -          apply(rule interior_mono *)+ using k by auto qed qed qed auto qed
   1.317 +  show ?thesis
   1.318 +    apply (rule that[of "d \<union> p"])
   1.319 +  proof -
   1.320 +    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
   1.321 +    have *: "{a..b} = \<Inter> (\<lambda>i. \<Union>(q i - {i})) ` p \<union> \<Union>p"
   1.322 +      apply (rule *[OF False])
   1.323 +    proof
   1.324 +      fix i
   1.325 +      assume i: "i\<in>p"
   1.326 +      show "\<Union>(q i - {i}) \<union> i = {a..b}"
   1.327 +        using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto
   1.328 +    qed
   1.329 +    show "d \<union> p division_of {a..b}"
   1.330 +      unfolding *
   1.331 +      apply (rule division_disjoint_union[OF d assms(1)])
   1.332 +      apply (rule inter_interior_unions_intervals)
   1.333 +      apply (rule p open_interior ballI)+
   1.334 +    proof (assumption, rule)
   1.335 +      fix k
   1.336 +      assume k: "k\<in>p"
   1.337 +      have *: "\<And>u t s. u \<subseteq> s \<Longrightarrow> s \<inter> t = {} \<Longrightarrow> u \<inter> t = {}" by auto
   1.338 +      show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<inter> interior k = {}"
   1.339 +        apply (rule *[of _ "interior (\<Union>(q k - {k}))"])
   1.340 +        defer
   1.341 +        apply (subst Int_commute)
   1.342 +        apply (rule inter_interior_unions_intervals)
   1.343 +      proof -
   1.344 +        note qk=division_ofD[OF q(1)[OF k]]
   1.345 +        show "finite (q k - {k})" "open (interior k)"
   1.346 +          "\<forall>t\<in>q k - {k}. \<exists>a b. t = {a..b}" using qk by auto
   1.347 +        show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}"
   1.348 +          using qk(5) using q(2)[OF k] by auto
   1.349 +        have *: "\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x" by auto
   1.350 +        show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<subseteq> interior (\<Union>(q k - {k}))"
   1.351 +          apply (rule interior_mono *)+
   1.352 +          using k by auto
   1.353 +      qed
   1.354 +    qed
   1.355 +  qed auto
   1.356 +qed
   1.357  
   1.358  lemma elementary_bounded[dest]: "p division_of s \<Longrightarrow> bounded (s::('a::ordered_euclidean_space) set)"
   1.359    unfolding division_of_def by(metis bounded_Union bounded_interval) 
   1.360  
   1.361  lemma elementary_subset_interval: "p division_of s \<Longrightarrow> \<exists>a b. s \<subseteq> {a..b::'a::ordered_euclidean_space}"
   1.362 -  by(meson elementary_bounded bounded_subset_closed_interval)
   1.363 -
   1.364 -lemma division_union_intervals_exists: assumes "{a..b::'a::ordered_euclidean_space} \<noteq> {}"
   1.365 -  obtains p where "(insert {a..b} p) division_of ({a..b} \<union> {c..d})" proof(cases "{c..d} = {}")
   1.366 -  case True show ?thesis apply(rule that[of "{}"]) unfolding True using assms by auto next
   1.367 -  case False note false=this show ?thesis proof(cases "{a..b} \<inter> {c..d} = {}")
   1.368 -  have *:"\<And>a b. {a,b} = {a} \<union> {b}" by auto
   1.369 -  case True show ?thesis apply(rule that[of "{{c..d}}"]) unfolding * apply(rule division_disjoint_union)
   1.370 -    using false True assms using interior_subset by auto next
   1.371 -  case False obtain u v where uv:"{a..b} \<inter> {c..d} = {u..v}" unfolding inter_interval by auto
   1.372 -  have *:"{u..v} \<subseteq> {c..d}" using uv by auto
   1.373 -  guess p apply(rule partial_division_extend_1[OF * False[unfolded uv]]) . note p=this division_ofD[OF this(1)]
   1.374 -  have *:"{a..b} \<union> {c..d} = {a..b} \<union> \<Union>(p - {{u..v}})" "\<And>x s. insert x s = {x} \<union> s" using p(8) unfolding uv[THEN sym] by auto
   1.375 -  show thesis apply(rule that[of "p - {{u..v}}"]) unfolding *(1) apply(subst *(2)) apply(rule division_disjoint_union)
   1.376 -    apply(rule,rule assms) apply(rule division_of_subset[of p]) apply(rule division_of_union_self[OF p(1)]) defer
   1.377 -    unfolding interior_inter[THEN sym] proof-
   1.378 -    have *:"\<And>cd p uv ab. p \<subseteq> cd \<Longrightarrow> ab \<inter> cd = uv \<Longrightarrow> ab \<inter> p = uv \<inter> p" by auto
   1.379 -    have "interior ({a..b} \<inter> \<Union>(p - {{u..v}})) = interior({u..v} \<inter> \<Union>(p - {{u..v}}))" 
   1.380 -      apply(rule arg_cong[of _ _ interior]) apply(rule *[OF _ uv]) using p(8) by auto
   1.381 -    also have "\<dots> = {}" unfolding interior_inter apply(rule inter_interior_unions_intervals) using p(6) p(7)[OF p(2)] p(3) by auto
   1.382 -    finally show "interior ({a..b} \<inter> \<Union>(p - {{u..v}})) = {}" by assumption qed auto qed qed
   1.383 +  by (meson elementary_bounded bounded_subset_closed_interval)
   1.384 +
   1.385 +lemma division_union_intervals_exists:
   1.386 +  assumes "{a..b::'a::ordered_euclidean_space} \<noteq> {}"
   1.387 +  obtains p where "(insert {a..b} p) division_of ({a..b} \<union> {c..d})"
   1.388 +proof (cases "{c..d} = {}")
   1.389 +  case True
   1.390 +  show ?thesis
   1.391 +    apply (rule that[of "{}"])
   1.392 +    unfolding True
   1.393 +    using assms
   1.394 +    apply auto
   1.395 +    done
   1.396 +next
   1.397 +  case False
   1.398 +  note false=this
   1.399 +  show ?thesis
   1.400 +  proof (cases "{a..b} \<inter> {c..d} = {}")
   1.401 +    case True
   1.402 +    have *:"\<And>a b. {a,b} = {a} \<union> {b}" by auto
   1.403 +    show ?thesis
   1.404 +      apply (rule that[of "{{c..d}}"])
   1.405 +      unfolding *
   1.406 +      apply (rule division_disjoint_union)
   1.407 +      using false True assms
   1.408 +      using interior_subset
   1.409 +      apply auto
   1.410 +      done
   1.411 +  next
   1.412 +    case False
   1.413 +    obtain u v where uv: "{a..b} \<inter> {c..d} = {u..v}"
   1.414 +      unfolding inter_interval by auto
   1.415 +    have *: "{u..v} \<subseteq> {c..d}" using uv by auto
   1.416 +    guess p apply (rule partial_division_extend_1[OF * False[unfolded uv]]) .
   1.417 +    note p=this division_ofD[OF this(1)]
   1.418 +    have *: "{a..b} \<union> {c..d} = {a..b} \<union> \<Union>(p - {{u..v}})" "\<And>x s. insert x s = {x} \<union> s"
   1.419 +      using p(8) unfolding uv[THEN sym] by auto
   1.420 +    show ?thesis
   1.421 +      apply (rule that[of "p - {{u..v}}"])
   1.422 +      unfolding *(1)
   1.423 +      apply (subst *(2))
   1.424 +      apply (rule division_disjoint_union)
   1.425 +      apply (rule, rule assms)
   1.426 +      apply (rule division_of_subset[of p])
   1.427 +      apply (rule division_of_union_self[OF p(1)])
   1.428 +      defer
   1.429 +      unfolding interior_inter[THEN sym]
   1.430 +    proof -
   1.431 +      have *: "\<And>cd p uv ab. p \<subseteq> cd \<Longrightarrow> ab \<inter> cd = uv \<Longrightarrow> ab \<inter> p = uv \<inter> p" by auto
   1.432 +      have "interior ({a..b} \<inter> \<Union>(p - {{u..v}})) = interior({u..v} \<inter> \<Union>(p - {{u..v}}))" 
   1.433 +        apply (rule arg_cong[of _ _ interior])
   1.434 +        apply (rule *[OF _ uv])
   1.435 +        using p(8)
   1.436 +        apply auto
   1.437 +        done
   1.438 +      also have "\<dots> = {}"
   1.439 +        unfolding interior_inter
   1.440 +        apply (rule inter_interior_unions_intervals)
   1.441 +        using p(6) p(7)[OF p(2)] p(3)
   1.442 +        apply auto
   1.443 +        done
   1.444 +      finally show "interior ({a..b} \<inter> \<Union>(p - {{u..v}})) = {}" .
   1.445 +    qed auto
   1.446 +  qed
   1.447 +qed
   1.448  
   1.449  lemma division_of_unions: assumes "finite f"  "\<And>p. p\<in>f \<Longrightarrow> p division_of (\<Union>p)"
   1.450    "\<And>k1 k2. \<lbrakk>k1 \<in> \<Union>f; k2 \<in> \<Union>f; k1 \<noteq> k2\<rbrakk> \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
     2.1 --- a/src/Pure/General/properties.scala	Thu Jan 17 14:38:12 2013 +0100
     2.2 +++ b/src/Pure/General/properties.scala	Thu Jan 17 15:50:56 2013 +0100
     2.3 @@ -102,33 +102,5 @@
     2.4          case Some((_, value)) => Value.Double.unapply(value)
     2.5        }
     2.6    }
     2.7 -
     2.8 -
     2.9 -  /* concrete syntax -- similar to ML */
    2.10 -
    2.11 -  private val syntax = Outer_Syntax.empty + "," + "(" + ")" + "[" + "]"
    2.12 -
    2.13 -  private object Parser extends Parse.Parser
    2.14 -  {
    2.15 -    def prop: Parser[Entry] =
    2.16 -      keyword("(") ~ string ~ keyword(",") ~ string ~ keyword(")") ^^
    2.17 -      { case _ ~ x ~ _ ~ y ~ _ => (x, y) }
    2.18 -    def props: Parser[T] =
    2.19 -      keyword("[") ~> repsep(prop, keyword(",")) <~ keyword("]")
    2.20 -  }
    2.21 -
    2.22 -  def parse(text: java.lang.String): Properties.T =
    2.23 -  {
    2.24 -    Parser.parse_all(Parser.props, Token.reader(syntax.scan(text))) match {
    2.25 -      case Parser.Success(result, _) => result
    2.26 -      case bad => error(bad.toString)
    2.27 -    }
    2.28 -  }
    2.29 -
    2.30 -  def parse_lines(prefix: java.lang.String, lines: List[java.lang.String]): List[T] =
    2.31 -    for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s)
    2.32 -
    2.33 -  def find_parse_line(prefix: java.lang.String, lines: List[java.lang.String]): Option[T] =
    2.34 -    lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length)))
    2.35  }
    2.36  
     3.1 --- a/src/Pure/Tools/build.scala	Thu Jan 17 14:38:12 2013 +0100
     3.2 +++ b/src/Pure/Tools/build.scala	Thu Jan 17 15:50:56 2013 +0100
     3.3 @@ -521,6 +521,37 @@
     3.4    }
     3.5  
     3.6  
     3.7 +  /* inlined properties -- syntax similar to ML */
     3.8 +
     3.9 +  object Props
    3.10 +  {
    3.11 +    private val syntax = Outer_Syntax.empty + "," + "(" + ")" + "[" + "]"
    3.12 +
    3.13 +    private object Parser extends Parse.Parser
    3.14 +    {
    3.15 +      def prop: Parser[Properties.Entry] =
    3.16 +        keyword("(") ~ string ~ keyword(",") ~ string ~ keyword(")") ^^
    3.17 +        { case _ ~ x ~ _ ~ y ~ _ => (x, y) }
    3.18 +      def props: Parser[Properties.T] =
    3.19 +        keyword("[") ~> repsep(prop, keyword(",")) <~ keyword("]")
    3.20 +    }
    3.21 +
    3.22 +    def parse(text: String): Properties.T =
    3.23 +    {
    3.24 +      Parser.parse_all(Parser.props, Token.reader(syntax.scan(text))) match {
    3.25 +        case Parser.Success(result, _) => result
    3.26 +        case bad => error(bad.toString)
    3.27 +      }
    3.28 +    }
    3.29 +
    3.30 +    def parse_lines(prefix: String, lines: List[String]): List[Properties.T] =
    3.31 +      for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s)
    3.32 +
    3.33 +    def find_parse_line(prefix: String, lines: List[String]): Option[Properties.T] =
    3.34 +      lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length)))
    3.35 +  }
    3.36 +
    3.37 +
    3.38    /* log files */
    3.39  
    3.40    private val LOG = Path.explode("log")
    3.41 @@ -529,13 +560,14 @@
    3.42  
    3.43    private val SESSION_PARENT_PATH = "\fSession.parent_path = "
    3.44  
    3.45 +
    3.46    sealed case class Log_Info(stats: List[Properties.T], timing: Properties.T)
    3.47  
    3.48    def parse_log(text: String): Log_Info =
    3.49    {
    3.50      val lines = split_lines(text)
    3.51 -    val stats = Properties.parse_lines("\fML_statistics = ", lines)
    3.52 -    val timing = Properties.find_parse_line("\fTiming = ", lines) getOrElse Nil
    3.53 +    val stats = Props.parse_lines("\fML_statistics = ", lines)
    3.54 +    val timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
    3.55      Log_Info(stats, timing)
    3.56    }
    3.57