src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
changeset 63659 abe0c3872d8a
parent 63627 6ddb43c6b711
child 63680 6e1e8b5abbfa
     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 10 18:57:20 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 10 18:57:20 2016 +0200
     1.3 @@ -1686,17 +1686,20 @@
     1.4    "lift_option f a' None = None"
     1.5    by (auto simp: lift_option_def)
     1.6  
     1.7 -lemma (in comm_monoid) comm_monoid_lift_option: "comm_monoid (lift_option op \<^bold>*) (Some \<^bold>1)"
     1.8 -  proof qed (auto simp: lift_option_def ac_simps split: bind_split)
     1.9 -
    1.10 -lemma (in comm_monoid) comm_monoid_set_lift_option: "comm_monoid_set (lift_option op \<^bold>*) (Some \<^bold>1)"
    1.11 -  proof qed (auto simp: lift_option_def ac_simps split: bind_split)
    1.12 -
    1.13 -lemma comm_monoid_and: "comm_monoid op \<and> True"
    1.14 -  proof qed auto
    1.15 -
    1.16 -lemma comm_monoid_set_and: "comm_monoid_set op \<and> True"
    1.17 -  proof qed auto
    1.18 +lemma comm_monoid_lift_option:
    1.19 +  assumes "comm_monoid f z"
    1.20 +  shows "comm_monoid (lift_option f) (Some z)"
    1.21 +proof -
    1.22 +  from assms interpret comm_monoid f z .
    1.23 +  show ?thesis
    1.24 +    by standard (auto simp: lift_option_def ac_simps split: bind_split)
    1.25 +qed
    1.26 +
    1.27 +lemma comm_monoid_and: "comm_monoid HOL.conj True"
    1.28 +  by standard auto
    1.29 +
    1.30 +lemma comm_monoid_set_and: "comm_monoid_set HOL.conj True"
    1.31 +  by (rule comm_monoid_set.intro) (fact comm_monoid_and)
    1.32  
    1.33  paragraph \<open>Operative\<close>
    1.34  
    1.35 @@ -3893,45 +3896,51 @@
    1.36  
    1.37  lemma operative_integral:
    1.38    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
    1.39 -  shows "comm_monoid.operative (lift_option op +) (Some 0) (\<lambda>i. if f integrable_on i then Some (integral i f) else None)"
    1.40 -  unfolding comm_monoid.operative_def[OF add.comm_monoid_lift_option]
    1.41 -proof safe
    1.42 -  fix a b c
    1.43 -  fix k :: 'a
    1.44 -  assume k: "k \<in> Basis"
    1.45 -  show "(if f integrable_on cbox a b then Some (integral (cbox a b) f) else None) =
    1.46 -        lift_option op + (if f integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c} then Some (integral (cbox a b \<inter> {x. x \<bullet> k \<le> c}) f) else None)
    1.47 -        (if f integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k} then Some (integral (cbox a b \<inter> {x. c \<le> x \<bullet> k}) f) else None)"
    1.48 -  proof (cases "f integrable_on cbox a b")
    1.49 -    case True
    1.50 -    with k show ?thesis
    1.51 -      apply (simp add: integrable_split)
    1.52 -      apply (rule integral_unique [OF has_integral_split[OF _ _ k]])
    1.53 -      apply (auto intro: integrable_integral)
    1.54 -      done
    1.55 -  next
    1.56 -    case False
    1.57 -    have "\<not> (f integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}) \<or> \<not> ( f integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k})"
    1.58 -    proof (rule ccontr)
    1.59 -      assume "\<not> ?thesis"
    1.60 -      then have "f integrable_on cbox a b"
    1.61 -        unfolding integrable_on_def
    1.62 -        apply (rule_tac x="integral (cbox a b \<inter> {x. x \<bullet> k \<le> c}) f + integral (cbox a b \<inter> {x. x \<bullet> k \<ge> c}) f" in exI)
    1.63 -        apply (rule has_integral_split[OF _ _ k])
    1.64 +  shows "comm_monoid.operative (lift_option op +) (Some 0)
    1.65 +    (\<lambda>i. if f integrable_on i then Some (integral i f) else None)"
    1.66 +proof -
    1.67 +  interpret comm_monoid "lift_option plus" "Some (0::'b)"
    1.68 +    by (rule comm_monoid_lift_option)
    1.69 +      (rule add.comm_monoid_axioms)
    1.70 +  show ?thesis
    1.71 +  proof (unfold operative_def, safe)
    1.72 +    fix a b c
    1.73 +    fix k :: 'a
    1.74 +    assume k: "k \<in> Basis"
    1.75 +    show "(if f integrable_on cbox a b then Some (integral (cbox a b) f) else None) =
    1.76 +          lift_option op + (if f integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c} then Some (integral (cbox a b \<inter> {x. x \<bullet> k \<le> c}) f) else None)
    1.77 +          (if f integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k} then Some (integral (cbox a b \<inter> {x. c \<le> x \<bullet> k}) f) else None)"
    1.78 +    proof (cases "f integrable_on cbox a b")
    1.79 +      case True
    1.80 +      with k show ?thesis
    1.81 +        apply (simp add: integrable_split)
    1.82 +        apply (rule integral_unique [OF has_integral_split[OF _ _ k]])
    1.83          apply (auto intro: integrable_integral)
    1.84          done
    1.85 -      then show False
    1.86 +    next
    1.87 +    case False
    1.88 +      have "\<not> (f integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}) \<or> \<not> ( f integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k})"
    1.89 +      proof (rule ccontr)
    1.90 +        assume "\<not> ?thesis"
    1.91 +        then have "f integrable_on cbox a b"
    1.92 +          unfolding integrable_on_def
    1.93 +          apply (rule_tac x="integral (cbox a b \<inter> {x. x \<bullet> k \<le> c}) f + integral (cbox a b \<inter> {x. x \<bullet> k \<ge> c}) f" in exI)
    1.94 +          apply (rule has_integral_split[OF _ _ k])
    1.95 +          apply (auto intro: integrable_integral)
    1.96 +          done
    1.97 +        then show False
    1.98 +          using False by auto
    1.99 +      qed
   1.100 +      then show ?thesis
   1.101          using False by auto
   1.102      qed
   1.103 -    then show ?thesis
   1.104 -      using False by auto
   1.105 -  qed
   1.106 -next
   1.107 -  fix a b :: 'a
   1.108 -  assume "content (cbox a b) = 0"
   1.109 -  then show "(if f integrable_on cbox a b then Some (integral (cbox a b) f) else None) = Some 0"
   1.110 -    using has_integral_null_eq
   1.111 -    by (auto simp: integrable_on_null)
   1.112 +  next
   1.113 +    fix a b :: 'a
   1.114 +    assume "content (cbox a b) = 0"
   1.115 +    then show "(if f integrable_on cbox a b then Some (integral (cbox a b) f) else None) = Some 0"
   1.116 +      using has_integral_null_eq
   1.117 +      by (auto simp: integrable_on_null)
   1.118 +  qed
   1.119  qed
   1.120  
   1.121  subsection \<open>Finally, the integral of a constant\<close>
   1.122 @@ -5902,9 +5911,13 @@
   1.123      and "(f has_integral (j::'a::banach)) {c .. b}"
   1.124    shows "(f has_integral (i + j)) {a .. b}"
   1.125  proof -
   1.126 -  note operative_integral[of f, unfolded comm_monoid.operative_1_le[OF add.comm_monoid_lift_option]]
   1.127 -  note conjunctD2[OF this,rule_format]
   1.128 -  note * = this(2)[OF conjI[OF assms(1-2)],unfolded if_P[OF assms(3)]]
   1.129 +  interpret comm_monoid "lift_option plus" "Some (0::'a)"
   1.130 +    by (rule comm_monoid_lift_option)
   1.131 +      (rule add.comm_monoid_axioms)
   1.132 +  note operative_integral [of f, unfolded operative_1_le]
   1.133 +  note conjunctD2 [OF this, rule_format]
   1.134 +  note * = this(2) [OF conjI [OF assms(1-2)],
   1.135 +    unfolded if_P [OF assms(3)]]
   1.136    then have "f integrable_on cbox a b"
   1.137      apply -
   1.138      apply (rule ccontr)
   1.139 @@ -7625,8 +7638,14 @@
   1.140      qed
   1.141    }
   1.142    assume "cbox c d \<noteq> {}"
   1.143 -  from partial_division_extend_1[OF assms(2) this] guess p . note p=this
   1.144 -  note operat = comm_monoid_set.operative_division[OF add.comm_monoid_set_lift_option operative_integral p(1), symmetric]
   1.145 +  from partial_division_extend_1 [OF assms(2) this] guess p . note p=this
   1.146 +  interpret comm_monoid_set "lift_option plus" "Some (0 :: 'b)"
   1.147 +    apply (rule comm_monoid_set.intro)
   1.148 +    apply (rule comm_monoid_lift_option)
   1.149 +    apply (rule add.comm_monoid_axioms)
   1.150 +    done
   1.151 +  note operat = operative_division
   1.152 +    [OF operative_integral p(1), symmetric]
   1.153    let ?P = "(if g integrable_on cbox a b then Some (integral (cbox a b) g) else None) = Some i"
   1.154    {
   1.155      presume "?P"
   1.156 @@ -7642,9 +7661,9 @@
   1.157        unfolding g_def
   1.158        by auto
   1.159    }
   1.160 -  let ?F = "comm_monoid_set.F (lift_option op +) (Some 0)"
   1.161 +  let ?F = F
   1.162    have iterate:"?F (\<lambda>i. if g integrable_on i then Some (integral i g) else None) (p - {cbox c d}) = Some 0"
   1.163 -  proof (intro comm_monoid_set.neutral[OF add.comm_monoid_set_lift_option] ballI)
   1.164 +  proof (intro neutral ballI)
   1.165      fix x
   1.166      assume x: "x \<in> p - {cbox c d}"
   1.167      then have "x \<in> p"
   1.168 @@ -7666,6 +7685,11 @@
   1.169  
   1.170    have *: "p = insert (cbox c d) (p - {cbox c d})"
   1.171      using p by auto
   1.172 +  interpret comm_monoid_set "lift_option plus" "Some (0 :: 'b)"
   1.173 +    apply (rule comm_monoid_set.intro)
   1.174 +    apply (rule comm_monoid_lift_option)
   1.175 +    apply (rule add.comm_monoid_axioms)
   1.176 +    done
   1.177    have **: "g integrable_on cbox c d"
   1.178      apply (rule integrable_spike_interior[where f=f])
   1.179      unfolding g_def  using assms(1)
   1.180 @@ -7684,7 +7708,7 @@
   1.181      unfolding operat
   1.182      using p
   1.183      apply (subst *)
   1.184 -    apply (subst comm_monoid_set.insert[OF add.comm_monoid_set_lift_option])
   1.185 +    apply (subst insert)
   1.186      apply (simp_all add: division_of_finite iterate)
   1.187      done
   1.188  qed