src/HOL/Multivariate_Analysis/Integration.thy
changeset 50348 4b4fe0d5ee22
parent 50252 4aa34bd43228
child 50526 899c9c4e4a4c
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Dec 04 18:00:37 2012 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Dec 04 18:00:40 2012 +0100
     1.3 @@ -8,10 +8,6 @@
     1.4    "~~/src/HOL/Library/Indicator_Function"
     1.5  begin
     1.6  
     1.7 -declare [[smt_certificates = "Integration.certs"]]
     1.8 -declare [[smt_read_only_certificates = true]]
     1.9 -declare [[smt_oracle = false]]
    1.10 -
    1.11  (*declare not_less[simp] not_le[simp]*)
    1.12  
    1.13  lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
    1.14 @@ -2770,16 +2766,21 @@
    1.15  lemma has_integral_component_le: fixes f g::"'a::ordered_euclidean_space \<Rightarrow> 'b::euclidean_space"
    1.16    assumes "(f has_integral i) s" "(g has_integral j) s"  "\<forall>x\<in>s. (f x)$$k \<le> (g x)$$k"
    1.17    shows "i$$k \<le> j$$k"
    1.18 -proof- have lem:"\<And>a b i (j::'b). \<And>g f::'a \<Rightarrow> 'b. (f has_integral i) ({a..b}) \<Longrightarrow> 
    1.19 +proof -
    1.20 +  have lem:"\<And>a b i (j::'b). \<And>g f::'a \<Rightarrow> 'b. (f has_integral i) ({a..b}) \<Longrightarrow> 
    1.21      (g has_integral j) ({a..b}) \<Longrightarrow> \<forall>x\<in>{a..b}. (f x)$$k \<le> (g x)$$k \<Longrightarrow> i$$k \<le> j$$k"
    1.22 -  proof(rule ccontr) case goal1 hence *:"0 < (i$$k - j$$k) / 3" by auto
    1.23 +  proof (rule ccontr)
    1.24 +    case goal1
    1.25 +    then have *: "0 < (i$$k - j$$k) / 3" by auto
    1.26      guess d1 using goal1(1)[unfolded has_integral,rule_format,OF *] apply-by(erule exE conjE)+ note d1=this[rule_format]
    1.27      guess d2 using goal1(2)[unfolded has_integral,rule_format,OF *] apply-by(erule exE conjE)+ note d2=this[rule_format]
    1.28      guess p using fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] unfolding fine_inter .
    1.29      note p = this(1) conjunctD2[OF this(2)]  note le_less_trans[OF component_le_norm, of _ _ k] term g
    1.30      note this[OF d1(2)[OF conjI[OF p(1,2)]]] this[OF d2(2)[OF conjI[OF p(1,3)]]]
    1.31 -    thus False unfolding euclidean_simps using rsum_component_le[OF p(1) goal1(3)] apply simp
    1.32 -      using [[z3_with_extensions]] by smt
    1.33 +    thus False
    1.34 +      unfolding euclidean_simps
    1.35 +      using rsum_component_le[OF p(1) goal1(3)]
    1.36 +      by (simp add: abs_real_def split: split_if_asm)
    1.37    qed let ?P = "\<exists>a b. s = {a..b}"
    1.38    { presume "\<not> ?P \<Longrightarrow> ?thesis" thus ?thesis proof(cases ?P)
    1.39        case True then guess a b apply-by(erule exE)+ note s=this
    1.40 @@ -2793,7 +2794,8 @@
    1.41    note ab = conjunctD2[OF this[unfolded Un_subset_iff]]
    1.42    guess w1 using B(2)[OF ab(1)] .. note w1=conjunctD2[OF this]
    1.43    guess w2 using B(4)[OF ab(2)] .. note w2=conjunctD2[OF this]
    1.44 -  have *:"\<And>w1 w2 j i::real .\<bar>w1 - i\<bar> < (i - j) / 3 \<Longrightarrow> \<bar>w2 - j\<bar> < (i - j) / 3 \<Longrightarrow> w1 \<le> w2 \<Longrightarrow> False" using [[z3_with_extensions]] by smt
    1.45 +  have *:"\<And>w1 w2 j i::real .\<bar>w1 - i\<bar> < (i - j) / 3 \<Longrightarrow> \<bar>w2 - j\<bar> < (i - j) / 3 \<Longrightarrow> w1 \<le> w2 \<Longrightarrow> False"
    1.46 +    by (simp add: abs_real_def split: split_if_asm)
    1.47    note le_less_trans[OF component_le_norm[of _ k]] note this[OF w1(2)] this[OF w2(2)] moreover
    1.48    have "w1$$k \<le> w2$$k" apply(rule lem[OF w1(1) w2(1)]) using assms by auto ultimately
    1.49    show False unfolding euclidean_simps by(rule *) qed
    1.50 @@ -3022,7 +3024,8 @@
    1.51        also have "... < e" apply(subst setsum_over_tagged_division_lemma[OF p[THEN conjunct1]])
    1.52        proof- case goal1 have "content ({u..v} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) \<le> content {u..v}"
    1.53            unfolding interval_doublesplit[OF k] apply(rule content_subset) unfolding interval_doublesplit[THEN sym,OF k] by auto
    1.54 -        thus ?case unfolding goal1 unfolding interval_doublesplit[OF k] using content_pos_le by smt
    1.55 +        thus ?case unfolding goal1 unfolding interval_doublesplit[OF k]
    1.56 +          by (blast intro: antisym)
    1.57        next have *:"setsum content {l \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d} |l. l \<in> snd ` p \<and> l \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d} \<noteq> {}} \<ge> 0"
    1.58            apply(rule setsum_nonneg,rule) unfolding mem_Collect_eq image_iff apply(erule exE bexE conjE)+ unfolding split_paired_all 
    1.59          proof- fix x l a b assume as:"x = l \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}" "(a, b) \<in> p" "l = snd (a, b)"
    1.60 @@ -3516,7 +3519,7 @@
    1.61    proof safe fix x and e::real assume as:"x\<in>k" "e>0"
    1.62      from k(2)[unfolded k content_eq_0] guess i .. 
    1.63      hence i:"c$$i = d$$i" "i<DIM('a)" using s(3)[OF k(1),unfolded k] unfolding interval_ne_empty by auto
    1.64 -    hence xi:"x$$i = d$$i" using as unfolding k mem_interval by smt
    1.65 +    hence xi:"x$$i = d$$i" using as unfolding k mem_interval by (metis antisym)
    1.66      def y \<equiv> "(\<chi>\<chi> j. if j = i then if c$$i \<le> (a$$i + b$$i) / 2 then c$$i +
    1.67        min e (b$$i - c$$i) / 2 else c$$i - min e (c$$i - a$$i) / 2 else x$$j)::'a"
    1.68      show "\<exists>x'\<in>\<Union>(s - {k}). x' \<noteq> x \<and> dist x' x < e" apply(rule_tac x=y in bexI) 
    1.69 @@ -3524,7 +3527,8 @@
    1.70        hence "d \<in> {a..b}" using s(2)[OF k(1)] unfolding k by auto note di = this[unfolded mem_interval,THEN spec[where x=i]]
    1.71        hence xyi:"y$$i \<noteq> x$$i" unfolding y_def unfolding i xi euclidean_lambda_beta'[OF i(2)] if_P[OF refl]
    1.72          apply(cases) apply(subst if_P,assumption) unfolding if_not_P not_le using as(2)
    1.73 -        using assms(2)[unfolded content_eq_0] using i(2) using [[z3_with_extensions]] by smt+
    1.74 +        using assms(2)[unfolded content_eq_0] using i(2)
    1.75 +        by (auto simp add: not_le min_def)
    1.76        thus "y \<noteq> x" unfolding euclidean_eq[where 'a='a] using i by auto
    1.77        have *:"{..<DIM('a)} = insert i ({..<DIM('a)} - {i})" using i by auto
    1.78        have "norm (y - x) < e + setsum (\<lambda>i. 0) {..<DIM('a)}" apply(rule le_less_trans[OF norm_le_l1])
    1.79 @@ -4710,7 +4714,8 @@
    1.80      proof- fix a b c d::"'n::ordered_euclidean_space" assume as:"ball 0 (max B1 B2) \<subseteq> {a..b}" "ball 0 (max B1 B2) \<subseteq> {c..d}"
    1.81        have **:"ball 0 B1 \<subseteq> ball (0::'n::ordered_euclidean_space) (max B1 B2)" "ball 0 B2 \<subseteq> ball (0::'n::ordered_euclidean_space) (max B1 B2)" by auto
    1.82        have *:"\<And>ga gc ha hc fa fc::real. abs(ga - i) < e / 3 \<and> abs(gc - i) < e / 3 \<and> abs(ha - j) < e / 3 \<and>
    1.83 -        abs(hc - j) < e / 3 \<and> abs(i - j) < e / 3 \<and> ga \<le> fa \<and> fa \<le> ha \<and> gc \<le> fc \<and> fc \<le> hc\<Longrightarrow> abs(fa - fc) < e" using [[z3_with_extensions]] by smt
    1.84 +        abs(hc - j) < e / 3 \<and> abs(i - j) < e / 3 \<and> ga \<le> fa \<and> fa \<le> ha \<and> gc \<le> fc \<and> fc \<le> hc\<Longrightarrow> abs(fa - fc) < e"
    1.85 +        by (simp add: abs_real_def split: split_if_asm)
    1.86        show "norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - integral {c..d} (\<lambda>x. if x \<in> s then f x else 0)) < e"
    1.87          unfolding real_norm_def apply(rule *, safe) unfolding real_norm_def[THEN sym]
    1.88          apply(rule B1(2),rule order_trans,rule **,rule as(1)) 
    1.89 @@ -6057,7 +6062,4 @@
    1.90              using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto
    1.91          qed qed(insert n,auto) qed qed qed
    1.92  
    1.93 -declare [[smt_certificates = ""]]
    1.94 -declare [[smt_read_only_certificates = false]]
    1.95 -
    1.96  end