--- a/Admin/components/components.sha1 Wed Aug 23 23:46:35 2017 +0100
+++ b/Admin/components/components.sha1 Thu Aug 24 12:45:46 2017 +0100
@@ -10,6 +10,7 @@
b01fdb93f2dc2b8bcfd41c6091d91b37d6e240f9 cvc4-1.5pre-3.tar.gz
76ff6103b8560f0e2778bbfbdb05f5fa18f850b7 cvc4-1.5pre-4.tar.gz
03aec2ec5757301c9df149f115d1f4f1d2cafd9e cvc4-1.5pre.tar.gz
+d70bfbe63590153c07709dea7084fbc39c669841 cvc4-1.5-1.tar.gz
3682476dc5e915cf260764fa5b86f1ebdab57507 cvc4-1.5.tar.gz
842d9526f37b928cf9e22f141884365129990d63 cygwin-20130110.tar.gz
cb3b0706d208f104b800267697204f6d82f7b48a cygwin-20130114.tar.gz
--- a/Admin/components/main Wed Aug 23 23:46:35 2017 +0100
+++ b/Admin/components/main Thu Aug 24 12:45:46 2017 +0100
@@ -1,7 +1,7 @@
#main components for everyday use, without big impact on overall build time
bash_process-1.2.1
csdp-6.x
-cvc4-1.5
+cvc4-1.5-1
e-2.0
isabelle_fonts-20160830
jdk-8u144
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Aug 23 23:46:35 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Aug 24 12:45:46 2017 +0100
@@ -188,15 +188,23 @@
finally show "(\<lambda>(x, k). content k *\<^sub>R f x) y = 0" .
qed
-lemma operative_content[intro]: "add.operative content"
- by (force simp add: add.operative_def content_split[symmetric] content_eq_0_interior)
+global_interpretation sum_content: operative plus 0 content
+ rewrites "comm_monoid_set.F plus 0 = sum"
+proof -
+ interpret operative plus 0 content
+ by standard (auto simp add: content_split [symmetric] content_eq_0_interior)
+ show "operative plus 0 content"
+ by standard
+ show "comm_monoid_set.F plus 0 = sum"
+ by (simp add: sum_def)
+qed
lemma additive_content_division: "d division_of (cbox a b) \<Longrightarrow> sum content d = content (cbox a b)"
- by (metis operative_content sum.operative_division)
+ by (fact sum_content.division)
lemma additive_content_tagged_division:
"d tagged_division_of (cbox a b) \<Longrightarrow> sum (\<lambda>(x,l). content l) d = content (cbox a b)"
- unfolding sum.operative_tagged_division[OF operative_content, symmetric] by blast
+ by (fact sum_content.tagged_division)
lemma subadditive_content_division:
assumes "\<D> division_of S" "S \<subseteq> cbox a b"
@@ -1404,16 +1412,16 @@
by (simp add: interval_split[OF k] integrable_Cauchy)
qed
-lemma operative_integral:
+lemma operative_integralI:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
- shows "comm_monoid.operative (lift_option op +) (Some 0)
+ shows "operative (lift_option op +) (Some 0)
(\<lambda>i. if f integrable_on i then Some (integral i f) else None)"
proof -
interpret comm_monoid "lift_option plus" "Some (0::'b)"
by (rule comm_monoid_lift_option)
(rule add.comm_monoid_axioms)
show ?thesis
- proof (unfold operative_def, safe)
+ proof
fix a b c
fix k :: 'a
assume k: "k \<in> Basis"
@@ -2457,45 +2465,49 @@
subsection \<open>Integrability of continuous functions.\<close>
-lemma operative_approximable:
+lemma operative_approximableI:
fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
assumes "0 \<le> e"
- shows "comm_monoid.operative op \<and> True (\<lambda>i. \<exists>g. (\<forall>x\<in>i. norm (f x - g (x::'b)) \<le> e) \<and> g integrable_on i)"
- unfolding comm_monoid.operative_def[OF comm_monoid_and]
-proof safe
- fix a b :: 'b
- show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
- if "box a b = {}" for a b
- apply (rule_tac x=f in exI)
- using assms that by (auto simp: content_eq_0_interior)
- {
- fix c g and k :: 'b
- assume fg: "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" and g: "g integrable_on cbox a b"
- assume k: "k \<in> Basis"
- show "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
- "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}"
- apply (rule_tac[!] x=g in exI)
- using fg integrable_split[OF g k] by auto
- }
- show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
- if fg1: "\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g1 x) \<le> e"
- and g1: "g1 integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
- and fg2: "\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g2 x) \<le> e"
- and g2: "g2 integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}"
- and k: "k \<in> Basis"
- for c k g1 g2
- proof -
- let ?g = "\<lambda>x. if x\<bullet>k = c then f x else if x\<bullet>k \<le> c then g1 x else g2 x"
+ shows "operative conj True (\<lambda>i. \<exists>g. (\<forall>x\<in>i. norm (f x - g (x::'b)) \<le> e) \<and> g integrable_on i)"
+proof -
+ interpret comm_monoid conj True
+ by standard auto
+ show ?thesis
+ proof (standard, safe)
+ fix a b :: 'b
show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
- proof (intro exI conjI ballI)
- show "norm (f x - ?g x) \<le> e" if "x \<in> cbox a b" for x
- by (auto simp: that assms fg1 fg2)
- show "?g integrable_on cbox a b"
- proof -
- have "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
- by(rule integrable_spike[OF negligible_standard_hyperplane[of k c]], use k g1 g2 in auto)+
- with has_integral_split[OF _ _ k] show ?thesis
- unfolding integrable_on_def by blast
+ if "box a b = {}" for a b
+ apply (rule_tac x=f in exI)
+ using assms that by (auto simp: content_eq_0_interior)
+ {
+ fix c g and k :: 'b
+ assume fg: "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" and g: "g integrable_on cbox a b"
+ assume k: "k \<in> Basis"
+ show "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
+ "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}"
+ apply (rule_tac[!] x=g in exI)
+ using fg integrable_split[OF g k] by auto
+ }
+ show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
+ if fg1: "\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g1 x) \<le> e"
+ and g1: "g1 integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
+ and fg2: "\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g2 x) \<le> e"
+ and g2: "g2 integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}"
+ and k: "k \<in> Basis"
+ for c k g1 g2
+ proof -
+ let ?g = "\<lambda>x. if x\<bullet>k = c then f x else if x\<bullet>k \<le> c then g1 x else g2 x"
+ show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
+ proof (intro exI conjI ballI)
+ show "norm (f x - ?g x) \<le> e" if "x \<in> cbox a b" for x
+ by (auto simp: that assms fg1 fg2)
+ show "?g integrable_on cbox a b"
+ proof -
+ have "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
+ by(rule integrable_spike[OF negligible_standard_hyperplane[of k c]], use k g1 g2 in auto)+
+ with has_integral_split[OF _ _ k] show ?thesis
+ unfolding integrable_on_def by blast
+ qed
qed
qed
qed
@@ -2516,11 +2528,9 @@
and f: "\<forall>i\<in>d. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i"
obtains g where "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" "g integrable_on cbox a b"
proof -
- note * = comm_monoid_set.operative_division
- [OF comm_monoid_set_and operative_approximable[OF \<open>0 \<le> e\<close>] d]
- have "finite d"
- by (rule division_of_finite[OF d])
- with f *[unfolded comm_monoid_set_F_and, of f] that show thesis
+ interpret operative conj True "\<lambda>i. \<exists>g. (\<forall>x\<in>i. norm (f x - g (x::'b)) \<le> e) \<and> g integrable_on i"
+ using \<open>0 \<le> e\<close> by (rule operative_approximableI)
+ from f local.division [OF d] that show thesis
by auto
qed
@@ -2999,31 +3009,43 @@
subsection \<open>Integrability on subintervals.\<close>
-lemma operative_integrable:
+lemma operative_integrableI:
fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
- shows "comm_monoid.operative op \<and> True (\<lambda>i. f integrable_on i)"
- unfolding comm_monoid.operative_def[OF comm_monoid_and]
- apply safe
- apply (subst integrable_on_def)
- apply rule
- apply (rule has_integral_null_eq[where i=0, THEN iffD2])
- apply (simp add: content_eq_0_interior)
- apply rule
- apply (rule, assumption, assumption)+
- unfolding integrable_on_def
- by (auto intro!: has_integral_split)
+ assumes "0 \<le> e"
+ shows "operative conj True (\<lambda>i. f integrable_on i)"
+proof -
+ interpret comm_monoid conj True
+ by standard auto
+ show ?thesis
+ apply standard
+ apply safe
+ apply (subst integrable_on_def)
+ apply rule
+ apply (rule has_integral_null_eq[where i=0, THEN iffD2])
+ apply (simp add: content_eq_0_interior)
+ apply rule
+ apply (rule, assumption, assumption)+
+ unfolding integrable_on_def
+ apply (auto intro!: has_integral_split)
+ done
+qed
lemma integrable_subinterval:
fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
assumes "f integrable_on cbox a b"
and "cbox c d \<subseteq> cbox a b"
shows "f integrable_on cbox c d"
- apply (cases "cbox c d = {}")
- defer
- apply (rule partial_division_extend_1[OF assms(2)],assumption)
- using comm_monoid_set.operative_division[OF comm_monoid_set_and operative_integrable,symmetric,of _ _ _ f] assms(1)
- apply (auto simp: comm_monoid_set_F_and)
- done
+proof -
+ interpret operative conj True "\<lambda>i. f integrable_on i"
+ using order_refl by (rule operative_integrableI)
+ show ?thesis
+ apply (cases "cbox c d = {}")
+ defer
+ apply (rule partial_division_extend_1[OF assms(2)],assumption)
+ using division [symmetric] assms(1)
+ apply (auto simp: comm_monoid_set_F_and)
+ done
+qed
lemma integrable_subinterval_real:
fixes f :: "real \<Rightarrow> 'a::banach"
@@ -3043,10 +3065,10 @@
and cb: "(f has_integral j) {c..b}"
shows "(f has_integral (i + j)) {a..b}"
proof -
- interpret comm_monoid "lift_option plus" "Some (0::'a)"
- by (rule comm_monoid_lift_option)
- (rule add.comm_monoid_axioms)
- from operative_integral [of f, unfolded operative_1_le] \<open>a \<le> c\<close> \<open>c \<le> b\<close>
+ interpret operative_real "lift_option plus" "Some 0"
+ "\<lambda>i. if f integrable_on i then Some (integral i f) else None"
+ using operative_integralI by (rule operative_realI)
+ from \<open>a \<le> c\<close> \<open>c \<le> b\<close> ac cb coalesce_less_eq
have *: "lift_option op +
(if f integrable_on {a..c} then Some (integral {a..c} f) else None)
(if f integrable_on {c..b} then Some (integral {c..b} f) else None) =
@@ -3097,6 +3119,8 @@
f integrable_on cbox u v"
shows "f integrable_on cbox a b"
proof -
+ interpret operative conj True "\<lambda>i. f integrable_on i"
+ using order_refl by (rule operative_integrableI)
have "\<forall>x. \<exists>d>0. x\<in>cbox a b \<longrightarrow> (\<forall>u v. x \<in> cbox u v \<and> cbox u v \<subseteq> ball x d \<and> cbox u v \<subseteq> cbox a b \<longrightarrow>
f integrable_on cbox u v)"
using assms by (metis zero_less_one)
@@ -3111,8 +3135,7 @@
have "f integrable_on k" if "(x, k) \<in> p" for x k
using tagged_division_ofD(2-4)[OF p(1) that] fineD[OF p(2) that] d[of x] by auto
then show ?thesis
- unfolding comm_monoid_set.operative_division[OF comm_monoid_set_and operative_integrable sndp, symmetric]
- comm_monoid_set_F_and
+ unfolding division [symmetric, OF sndp] comm_monoid_set_F_and
by auto
qed
@@ -4485,13 +4508,11 @@
}
assume "cbox c d \<noteq> {}"
from partial_division_extend_1 [OF assms(2) this] guess p . note p=this
- interpret comm_monoid_set "lift_option plus" "Some (0 :: 'b)"
- apply (rule comm_monoid_set.intro)
- apply (rule comm_monoid_lift_option)
- apply (rule add.comm_monoid_axioms)
- done
- note operat = operative_division
- [OF operative_integral p(1), symmetric]
+ interpret operative "lift_option plus" "Some (0 :: 'b)"
+ "\<lambda>i. if g integrable_on i then Some (integral i g) else None"
+ by (fact operative_integralI)
+ note operat = division
+ [OF p(1), symmetric]
let ?P = "(if g integrable_on cbox a b then Some (integral (cbox a b) g) else None) = Some i"
{
presume "?P"
@@ -6984,16 +7005,16 @@
apply (auto simp: has_integral_integral [symmetric])
done
-lemma integral_swap_operative:
+lemma integral_swap_operativeI:
fixes f :: "('a::euclidean_space * 'b::euclidean_space) \<Rightarrow> 'c::banach"
assumes f: "continuous_on s f" and e: "0 < e"
- shows "comm_monoid.operative (op \<and>) True
+ shows "operative conj True
(\<lambda>k. \<forall>a b c d.
cbox (a,c) (b,d) \<subseteq> k \<and> cbox (a,c) (b,d) \<subseteq> s
\<longrightarrow> norm(integral (cbox (a,c) (b,d)) f -
integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f((x,y)))))
\<le> e * content (cbox (a,c) (b,d)))"
-proof (auto simp: comm_monoid.operative_def[OF comm_monoid_and])
+proof (standard, auto)
fix a::'a and c::'b and b::'a and d::'b and u::'a and v::'a and w::'b and z::'b
assume *: "box (a, c) (b, d) = {}"
and cb1: "cbox (u, w) (v, z) \<subseteq> cbox (a, c) (b, d)"
@@ -7087,8 +7108,8 @@
lemma integral_prod_continuous:
fixes f :: "('a::euclidean_space * 'b::euclidean_space) \<Rightarrow> 'c::banach"
- assumes "continuous_on (cbox (a,c) (b,d)) f" (is "continuous_on ?CBOX f")
- shows "integral (cbox (a,c) (b,d)) f = integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f(x,y)))"
+ assumes "continuous_on (cbox (a, c) (b, d)) f" (is "continuous_on ?CBOX f")
+ shows "integral (cbox (a, c) (b, d)) f = integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x, y)))"
proof (cases "content ?CBOX = 0")
case True
then show ?thesis
@@ -7099,22 +7120,41 @@
using content_lt_nz by blast
have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) = 0"
proof (rule dense_eq0_I, simp)
- fix e::real assume "0 < e"
- with cbp have e': "0 < e/content ?CBOX"
+ fix e :: real
+ assume "0 < e"
+ with \<open>content ?CBOX > 0\<close> have "0 < e / content ?CBOX"
by simp
- have f_int_acbd: "f integrable_on cbox (a,c) (b,d)"
+ have f_int_acbd: "f integrable_on ?CBOX"
by (rule integrable_continuous [OF assms])
{ fix p
- assume p: "p division_of cbox (a,c) (b,d)"
- note opd1 = comm_monoid_set.operative_division [OF comm_monoid_set_and integral_swap_operative [OF assms e'], THEN iffD1,
- THEN spec, THEN spec, THEN spec, THEN spec, of p "(a,c)" "(b,d)" a c b d]
- have "(\<And>t u v w z.
- \<lbrakk>t \<in> p; cbox (u,w) (v,z) \<subseteq> t; cbox (u,w) (v,z) \<subseteq> cbox (a,c) (b,d)\<rbrakk> \<Longrightarrow>
- norm (integral (cbox (u,w) (v,z)) f - integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y))))
- \<le> e * content (cbox (u,w) (v,z)) / content?CBOX)
- \<Longrightarrow>
- norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) \<le> e"
- using opd1 [OF p] False by (simp add: comm_monoid_set_F_and)
+ assume p: "p division_of ?CBOX"
+ then have "finite p"
+ by blast
+ define e' where "e' = e / content ?CBOX"
+ with \<open>0 < e\<close> \<open>0 < e / content ?CBOX\<close>
+ have "0 < e'"
+ by simp
+ interpret operative conj True
+ "\<lambda>k. \<forall>a' b' c' d'.
+ cbox (a', c') (b', d') \<subseteq> k \<and> cbox (a', c') (b', d') \<subseteq> ?CBOX
+ \<longrightarrow> norm (integral (cbox (a', c') (b', d')) f -
+ integral (cbox a' b') (\<lambda>x. integral (cbox c' d') (\<lambda>y. f ((x, y)))))
+ \<le> e' * content (cbox (a', c') (b', d'))"
+ using assms \<open>0 < e'\<close> by (rule integral_swap_operativeI)
+ have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x, y))))
+ \<le> e' * content ?CBOX"
+ if "\<And>t u v w z. t \<in> p \<Longrightarrow> cbox (u, w) (v, z) \<subseteq> t \<Longrightarrow> cbox (u, w) (v, z) \<subseteq> ?CBOX
+ \<Longrightarrow> norm (integral (cbox (u, w) (v, z)) f -
+ integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))))
+ \<le> e' * content (cbox (u, w) (v, z))"
+ using that division [of p "(a, c)" "(b, d)"] p \<open>finite p\<close> by (auto simp add: comm_monoid_set_F_and)
+ with False have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x, y))))
+ \<le> e"
+ if "\<And>t u v w z. t \<in> p \<Longrightarrow> cbox (u, w) (v, z) \<subseteq> t \<Longrightarrow> cbox (u, w) (v, z) \<subseteq> ?CBOX
+ \<Longrightarrow> norm (integral (cbox (u, w) (v, z)) f -
+ integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))))
+ \<le> e * content (cbox (u, w) (v, z)) / content ?CBOX"
+ using that by (simp add: e'_def)
} note op_acbd = this
{ fix k::real and \<D> and u::'a and v w and z::'b and t1 t2 l
assume k: "0 < k"
@@ -7149,7 +7189,7 @@
\<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
apply (simp only: integral_diff [symmetric] f_int_uwvz integrable_const)
apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX / 2"]])
- using cbp e' nf'
+ using cbp \<open>0 < e / content ?CBOX\<close> nf'
apply (auto simp: integrable_diff f_int_uwvz integrable_const)
done
have int_integrable: "(\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))) integrable_on cbox u v"
@@ -7160,14 +7200,14 @@
\<le> e * content (cbox w z) / content (cbox (a, c) (b, d)) / 2"
apply (simp only: integral_diff [symmetric] f_int_uv integrable_const)
apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX / 2"]])
- using cbp e' nf'
+ using cbp \<open>0 < e / content ?CBOX\<close> nf'
apply (auto simp: integrable_diff f_int_uv integrable_const)
done
have "norm (integral (cbox u v)
(\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y)) - integral (cbox w z) (\<lambda>y. f (t1,t2))))
\<le> e * content (cbox w z) / content ?CBOX / 2 * content (cbox u v)"
apply (rule integrable_bound [OF _ _ normint_wz])
- using cbp e'
+ using cbp \<open>0 < e / content ?CBOX\<close>
apply (auto simp: divide_simps content_pos_le integrable_diff int_integrable integrable_const)
done
also have "... \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
--- a/src/HOL/Analysis/Tagged_Division.thy Wed Aug 23 23:46:35 2017 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy Thu Aug 24 12:45:46 2017 +0100
@@ -10,6 +10,8 @@
Topology_Euclidean_Space
begin
+term comm_monoid
+
lemma sum_Sigma_product:
assumes "finite S"
and "\<And>i. i \<in> S \<Longrightarrow> finite (T i)"
@@ -571,7 +573,7 @@
"g i = (a, c) \<or> g i = (c, d) \<or> g i = (d, b)"
using f g by (auto simp: PiE_iff)
with * ord[of i] show "interior l \<inter> interior k = {}"
- by (auto simp add: l k interior_cbox disjoint_interval intro!: bexI[of _ i])
+ by (auto simp add: l k disjoint_interval intro!: bexI[of _ i])
}
note \<open>k \<subseteq> cbox a b\<close>
}
@@ -1200,6 +1202,91 @@
apply auto
done
+lemma tagged_division_Un_interval:
+ fixes a :: "'a::euclidean_space"
+ assumes "p1 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<le> (c::real)})"
+ and "p2 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
+ and k: "k \<in> Basis"
+ shows "(p1 \<union> p2) tagged_division_of (cbox a b)"
+proof -
+ have *: "cbox a b = (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<union> (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
+ by auto
+ show ?thesis
+ apply (subst *)
+ apply (rule tagged_division_Un[OF assms(1-2)])
+ unfolding interval_split[OF k] interior_cbox
+ using k
+ apply (auto simp add: box_def elim!: ballE[where x=k])
+ done
+qed
+
+lemma tagged_division_Un_interval_real:
+ fixes a :: real
+ assumes "p1 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<le> (c::real)})"
+ and "p2 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<ge> c})"
+ and k: "k \<in> Basis"
+ shows "(p1 \<union> p2) tagged_division_of {a .. b}"
+ using assms
+ unfolding box_real[symmetric]
+ by (rule tagged_division_Un_interval)
+
+lemma tagged_division_split_left_inj:
+ assumes d: "d tagged_division_of i"
+ and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
+ and "K1 \<noteq> K2"
+ and eq: "K1 \<inter> {x. x \<bullet> k \<le> c} = K2 \<inter> {x. x \<bullet> k \<le> c}"
+ shows "interior (K1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
+proof -
+ have "interior (K1 \<inter> K2) = {} \<or> (x2, K2) = (x1, K1)"
+ using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
+ then show ?thesis
+ using eq \<open>K1 \<noteq> K2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
+qed
+
+lemma tagged_division_split_right_inj:
+ assumes d: "d tagged_division_of i"
+ and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
+ and "K1 \<noteq> K2"
+ and eq: "K1 \<inter> {x. x\<bullet>k \<ge> c} = K2 \<inter> {x. x\<bullet>k \<ge> c}"
+ shows "interior (K1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
+proof -
+ have "interior (K1 \<inter> K2) = {} \<or> (x2, K2) = (x1, K1)"
+ using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
+ then show ?thesis
+ using eq \<open>K1 \<noteq> K2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
+qed
+
+lemma (in comm_monoid_set) over_tagged_division_lemma:
+ assumes "p tagged_division_of i"
+ and "\<And>u v. box u v = {} \<Longrightarrow> d (cbox u v) = \<^bold>1"
+ shows "F (\<lambda>(_, k). d k) p = F d (snd ` p)"
+proof -
+ have *: "(\<lambda>(_ ,k). d k) = d \<circ> snd"
+ by (simp add: fun_eq_iff)
+ note assm = tagged_division_ofD[OF assms(1)]
+ show ?thesis
+ unfolding *
+ proof (rule reindex_nontrivial[symmetric])
+ show "finite p"
+ using assm by auto
+ fix x y
+ assume "x\<in>p" "y\<in>p" "x\<noteq>y" "snd x = snd y"
+ obtain a b where ab: "snd x = cbox a b"
+ using assm(4)[of "fst x" "snd x"] \<open>x\<in>p\<close> by auto
+ have "(fst x, snd y) \<in> p" "(fst x, snd y) \<noteq> y"
+ using \<open>x \<in> p\<close> \<open>x \<noteq> y\<close> \<open>snd x = snd y\<close> [symmetric] by auto
+ with \<open>x\<in>p\<close> \<open>y\<in>p\<close> have "interior (snd x) \<inter> interior (snd y) = {}"
+ by (intro assm(5)[of "fst x" _ "fst y"]) auto
+ then have "box a b = {}"
+ unfolding \<open>snd x = snd y\<close>[symmetric] ab by auto
+ then have "d (cbox a b) = \<^bold>1"
+ using assm(2)[of "fst x" "snd x"] \<open>x\<in>p\<close> ab[symmetric] by (intro assms(2)) auto
+ then show "d (snd x) = \<^bold>1"
+ unfolding ab by auto
+ qed
+qed
+
+
subsection \<open>Functions closed on boxes: morphisms from boxes to monoids\<close>
text \<open>This auxiliary structure is used to sum up over the elements of a division. Main theorem is
@@ -1233,29 +1320,21 @@
lemma comm_monoid_set_and: "comm_monoid_set HOL.conj True"
by (rule comm_monoid_set.intro) (fact comm_monoid_and)
-paragraph \<open>Operative\<close>
-definition (in comm_monoid) operative :: "('b::euclidean_space set \<Rightarrow> 'a) \<Rightarrow> bool"
- where "operative g \<longleftrightarrow>
- (\<forall>a b. box a b = {} \<longrightarrow> g (cbox a b) = \<^bold>1) \<and>
- (\<forall>a b c. \<forall>k\<in>Basis. g (cbox a b) = g (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. x\<bullet>k \<ge> c}))"
+paragraph \<open>Misc\<close>
-lemma (in comm_monoid) operativeD[dest]:
- assumes "operative g"
- shows "\<And>a b. box a b = {} \<Longrightarrow> g (cbox a b) = \<^bold>1"
- and "\<And>a b c k. k \<in> Basis \<Longrightarrow> g (cbox a b) = g (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
- using assms unfolding operative_def by auto
+lemma interval_real_split:
+ "{a .. b::real} \<inter> {x. x \<le> c} = {a .. min b c}"
+ "{a .. b} \<inter> {x. c \<le> x} = {max a c .. b}"
+ apply (metis Int_atLeastAtMostL1 atMost_def)
+ apply (metis Int_atLeastAtMostL2 atLeast_def)
+ done
-lemma (in comm_monoid) operative_empty:
- assumes g: "operative g" shows "g {} = \<^bold>1"
-proof -
- have *: "cbox One (-One) = ({}::'b set)"
- by (auto simp: box_eq_empty inner_sum_left inner_Basis sum.If_cases ex_in_conv)
- moreover have "box One (-One) = ({}::'b set)"
- using box_subset_cbox[of One "-One"] by (auto simp: *)
- ultimately show ?thesis
- using operativeD(1)[OF g, of One "-One"] by simp
-qed
+lemma bgauge_existence_lemma: "(\<forall>x\<in>s. \<exists>d::real. 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. x\<in>s \<longrightarrow> q d x)"
+ by (meson zero_less_one)
+
+
+paragraph \<open>Division points\<close>
definition "division_points (k::('a::euclidean_space) set) d =
{(j,x). j \<in> Basis \<and> (interval_lowerbound k)\<bullet>j < x \<and> x < (interval_upperbound k)\<bullet>j \<and>
@@ -1463,14 +1542,31 @@
by (simp add: interval_split k interval_doublesplit)
qed
-lemma (in comm_monoid_set) operative_division:
+paragraph \<open>Operative\<close>
+
+locale operative = comm_monoid_set +
fixes g :: "'b::euclidean_space set \<Rightarrow> 'a"
- assumes g: "operative g" and d: "d division_of (cbox a b)" shows "F g d = g (cbox a b)"
+ assumes box_empty_imp: "\<And>a b. box a b = {} \<Longrightarrow> g (cbox a b) = \<^bold>1"
+ and Basis_imp: "\<And>a b c k. k \<in> Basis \<Longrightarrow> g (cbox a b) = g (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
+begin
+
+lemma empty [simp]:
+ "g {} = \<^bold>1"
+proof -
+ have *: "cbox One (-One) = ({}::'b set)"
+ by (auto simp: box_eq_empty inner_sum_left inner_Basis sum.If_cases ex_in_conv)
+ moreover have "box One (-One) = ({}::'b set)"
+ using box_subset_cbox[of One "-One"] by (auto simp: *)
+ ultimately show ?thesis
+ using box_empty_imp [of One "-One"] by simp
+qed
+
+lemma division:
+ "F g d = g (cbox a b)" if "d division_of (cbox a b)"
proof -
define C where [abs_def]: "C = card (division_points (cbox a b) d)"
then show ?thesis
- using d
- proof (induction C arbitrary: a b d rule: less_induct)
+ using that proof (induction C arbitrary: a b d rule: less_induct)
case (less a b d)
show ?case
proof cases
@@ -1483,9 +1579,9 @@
then have "box a' b' \<subseteq> box a b"
unfolding subset_box by auto
then have "g k = \<^bold>1"
- using operativeD(1)[OF g, of a' b'] k by (simp add: \<open>box a b = {}\<close>) }
+ using box_empty_imp [of a' b'] k by (simp add: \<open>box a b = {}\<close>) }
then show "box a b = {} \<Longrightarrow> F g d = g (cbox a b)"
- by (auto intro!: neutral simp: operativeD(1)[OF g])
+ by (auto intro!: neutral simp: box_empty_imp)
next
assume "box a b \<noteq> {}"
then have ab: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i" and ab': "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
@@ -1560,7 +1656,7 @@
then have "box u v = {}"
using j unfolding box_eq_empty by (auto intro!: bexI[of _ j])
then show "g x = \<^bold>1"
- unfolding uv(1) by (rule operativeD(1)[OF g])
+ unfolding uv(1) by (rule box_empty_imp)
qed
then show "F g d = g (cbox a b)"
using division_ofD[OF less.prems]
@@ -1613,7 +1709,8 @@
have "interior (cbox u v \<inter> ?lec) = {}"
using that division_split_left_inj leq less.prems by blast
then show ?thesis
- unfolding leq interval_split[OF \<open>k \<in> Basis\<close>] using g by auto
+ unfolding leq interval_split [OF \<open>k \<in> Basis\<close>]
+ by (auto intro: box_empty_imp)
qed
have fxk_ge: "g (l \<inter> {x. x \<bullet> k \<ge> c}) = \<^bold>1"
if "l \<in> d" "y \<in> d" "l \<inter> ?gec = y \<inter> ?gec" "l \<noteq> y" for l y
@@ -1623,23 +1720,26 @@
have "interior (cbox u v \<inter> ?gec) = {}"
using that division_split_right_inj leq less.prems by blast
then show ?thesis
- unfolding leq interval_split[OF \<open>k \<in> Basis\<close>] using g by auto
+ unfolding leq interval_split[OF \<open>k \<in> Basis\<close>]
+ by (auto intro: box_empty_imp)
qed
have d1_alt: "d1 = (\<lambda>l. l \<inter> ?lec) ` {l \<in> d. l \<inter> ?lec \<noteq> {}}"
using d1_def by auto
have d2_alt: "d2 = (\<lambda>l. l \<inter> ?gec) ` {l \<in> d. l \<inter> ?gec \<noteq> {}}"
using d2_def by auto
have "g (cbox a b) = F g d1 \<^bold>* F g d2" (is "_ = ?prev")
- unfolding * using g \<open>k \<in> Basis\<close> by blast
+ unfolding * using \<open>k \<in> Basis\<close>
+ by (auto dest: Basis_imp)
also have "F g d1 = F (\<lambda>l. g (l \<inter> ?lec)) d"
unfolding d1_alt using division_of_finite[OF less.prems] fxk_le
- by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left simp: operative_empty[OF g])
+ by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left)
also have "F g d2 = F (\<lambda>l. g (l \<inter> ?gec)) d"
unfolding d2_alt using division_of_finite[OF less.prems] fxk_ge
- by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left simp: operative_empty[OF g])
+ by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left)
also have *: "\<forall>x\<in>d. g x = g (x \<inter> ?lec) \<^bold>* g (x \<inter> ?gec)"
unfolding forall_in_division[OF \<open>d division_of cbox a b\<close>]
- using g \<open>k \<in> Basis\<close> by blast
+ using \<open>k \<in> Basis\<close>
+ by (auto dest: Basis_imp)
have "F (\<lambda>l. g (l \<inter> ?lec)) d \<^bold>* F (\<lambda>l. g (l \<inter> ?gec)) d = F g d"
using * by (simp add: distrib)
finally show ?thesis by auto
@@ -1648,166 +1748,86 @@
qed
qed
-lemma (in comm_monoid_set) over_tagged_division_lemma:
- assumes "p tagged_division_of i"
- and "\<And>u v. cbox u v \<noteq> {} \<Longrightarrow> box u v = {} \<Longrightarrow> d (cbox u v) = \<^bold>1"
- shows "F (\<lambda>(x,k). d k) p = F d (snd ` p)"
+lemma tagged_division:
+ assumes "d tagged_division_of (cbox a b)"
+ shows "F (\<lambda>(_, l). g l) d = g (cbox a b)"
proof -
- have *: "(\<lambda>(x,k). d k) = d \<circ> snd"
- unfolding o_def by (rule ext) auto
- note assm = tagged_division_ofD[OF assms(1)]
- show ?thesis
- unfolding *
- proof (rule reindex_nontrivial[symmetric])
- show "finite p"
- using assm by auto
- fix x y
- assume "x\<in>p" "y\<in>p" "x\<noteq>y" "snd x = snd y"
- obtain a b where ab: "snd x = cbox a b"
- using assm(4)[of "fst x" "snd x"] \<open>x\<in>p\<close> by auto
- have "(fst x, snd y) \<in> p" "(fst x, snd y) \<noteq> y"
- by (metis prod.collapse \<open>x\<in>p\<close> \<open>snd x = snd y\<close> \<open>x \<noteq> y\<close>)+
- with \<open>x\<in>p\<close> \<open>y\<in>p\<close> have "interior (snd x) \<inter> interior (snd y) = {}"
- by (intro assm(5)[of "fst x" _ "fst y"]) auto
- then have "box a b = {}"
- unfolding \<open>snd x = snd y\<close>[symmetric] ab by auto
- then have "d (cbox a b) = \<^bold>1"
- using assm(2)[of "fst x" "snd x"] \<open>x\<in>p\<close> ab[symmetric] by (intro assms(2)) auto
- then show "d (snd x) = \<^bold>1"
- unfolding ab by auto
+ have "F (\<lambda>(_, k). g k) d = F g (snd ` d)"
+ using assms box_empty_imp by (rule over_tagged_division_lemma)
+ then show ?thesis
+ unfolding assms [THEN division_of_tagged_division, THEN division] .
qed
-qed
+
+end
-lemma (in comm_monoid_set) operative_tagged_division:
- assumes f: "operative g" and d: "d tagged_division_of (cbox a b)"
- shows "F (\<lambda>(x, l). g l) d = g (cbox a b)"
- unfolding d[THEN division_of_tagged_division, THEN operative_division[OF f], symmetric]
- by (simp add: f[THEN operativeD(1)] over_tagged_division_lemma[OF d])
-
-lemma interval_real_split:
- "{a .. b::real} \<inter> {x. x \<le> c} = {a .. min b c}"
- "{a .. b} \<inter> {x. c \<le> x} = {max a c .. b}"
- apply (metis Int_atLeastAtMostL1 atMost_def)
- apply (metis Int_atLeastAtMostL2 atLeast_def)
- done
+locale operative_real = comm_monoid_set +
+ fixes g :: "real set \<Rightarrow> 'a"
+ assumes neutral: "b \<le> a \<Longrightarrow> g {a..b} = \<^bold>1"
+ assumes coalesce_less: "a < c \<Longrightarrow> c < b \<Longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
+begin
-lemma (in comm_monoid) operative_1_lt:
- "operative (g :: real set \<Rightarrow> 'a) \<longleftrightarrow>
- ((\<forall>a b. b \<le> a \<longrightarrow> g {a .. b} = \<^bold>1) \<and> (\<forall>a b c. a < c \<and> c < b \<longrightarrow> g {a .. c} \<^bold>* g {c .. b} = g {a .. b}))"
- apply (simp add: operative_def atMost_def[symmetric] atLeast_def[symmetric])
-proof safe
- fix a b c :: real
- assume *: "\<forall>a b c. g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}"
- assume "a < c" "c < b"
- with *[rule_format, of a b c] show "g {a..c} \<^bold>* g {c..b} = g {a..b}"
- by (simp add: less_imp_le min.absorb2 max.absorb2)
-next
- fix a b c :: real
- assume as: "\<forall>a b. b \<le> a \<longrightarrow> g {a..b} = \<^bold>1"
- "\<forall>a b c. a < c \<and> c < b \<longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
- from as(1)[rule_format, of 0 1] as(1)[rule_format, of a a for a] as(2)
+sublocale operative where g = g
+ rewrites "box = (greaterThanLessThan :: real \<Rightarrow> _)"
+ and "cbox = (atLeastAtMost :: real \<Rightarrow> _)"
+ and "\<And>x::real. x \<in> Basis \<longleftrightarrow> x = 1"
+proof -
+ show "operative f z g"
+ proof
+ show "g (cbox a b) = \<^bold>1" if "box a b = {}" for a b
+ using that by (simp add: neutral)
+ show "g (cbox a b) = g (cbox a b \<inter> {x. x \<bullet> k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. c \<le> x \<bullet> k})"
+ if "k \<in> Basis" for a b c k
+ proof -
+ from that have [simp]: "k = 1"
+ by simp
+ from neutral [of 0 1] neutral [of a a for a] coalesce_less
have [simp]: "g {} = \<^bold>1" "\<And>a. g {a} = \<^bold>1"
"\<And>a b c. a < c \<Longrightarrow> c < b \<Longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
by auto
- show "g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}"
+ have "g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}"
by (auto simp: min_def max_def le_less)
+ then show "g (cbox a b) = g (cbox a b \<inter> {x. x \<bullet> k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. c \<le> x \<bullet> k})"
+ by (simp add: atMost_def [symmetric] atLeast_def [symmetric])
qed
-
-lemma (in comm_monoid) operative_1_le:
- "operative (g :: real set \<Rightarrow> 'a) \<longleftrightarrow>
- ((\<forall>a b. b \<le> a \<longrightarrow> g {a..b} = \<^bold>1) \<and> (\<forall>a b c. a \<le> c \<and> c \<le> b \<longrightarrow> g {a .. c} \<^bold>* g {c .. b} = g {a .. b}))"
- unfolding operative_1_lt
-proof safe
- fix a b c :: real
- assume as: "\<forall>a b c. a \<le> c \<and> c \<le> b \<longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}" "a < c" "c < b"
- show "g {a..c} \<^bold>* g {c..b} = g {a..b}"
- apply (rule as(1)[rule_format])
- using as(2-)
- apply auto
- done
-next
- fix a b c :: real
- assume eq1: "\<forall>a b. b \<le> a \<longrightarrow> g {a .. b} = \<^bold>1"
- and eqg: "\<forall>a b c. a < c \<and> c < b \<longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
- and "a \<le> c"
- and "c \<le> b"
- show "g {a..c} \<^bold>* g {c..b} = g {a..b}"
- proof (cases "c = a \<or> c = b")
- case False
- then show ?thesis
- using eqg \<open>a \<le> c\<close> \<open>c \<le> b\<close> by auto
- next
- case True
- then show ?thesis
- proof
- assume *: "c = a"
- then have "g {a .. c} = \<^bold>1"
- using eq1 by blast
- then show ?thesis
- unfolding * by auto
- next
- assume *: "c = b"
- then have "g {c .. b} = \<^bold>1"
- using eq1 by blast
- then show ?thesis
- unfolding * by auto
- qed
qed
+ show "box = (greaterThanLessThan :: real \<Rightarrow> _)"
+ and "cbox = (atLeastAtMost :: real \<Rightarrow> _)"
+ and "\<And>x::real. x \<in> Basis \<longleftrightarrow> x = 1"
+ by (simp_all add: fun_eq_iff)
qed
-lemma tagged_division_Un_interval:
- fixes a :: "'a::euclidean_space"
- assumes "p1 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<le> (c::real)})"
- and "p2 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
- and k: "k \<in> Basis"
- shows "(p1 \<union> p2) tagged_division_of (cbox a b)"
+lemma coalesce_less_eq:
+ "g {a..c} \<^bold>* g {c..b} = g {a..b}" if "a \<le> c" "c \<le> b"
+ proof (cases "c = a \<or> c = b")
+ case False
+ with that have "a < c" "c < b"
+ by auto
+ then show ?thesis
+ by (rule coalesce_less)
+ next
+ case True
+ with that box_empty_imp [of a a] box_empty_imp [of b b] show ?thesis
+ by safe simp_all
+ qed
+
+end
+
+lemma operative_realI:
+ "operative_real f z g" if "operative f z g"
proof -
- have *: "cbox a b = (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<union> (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
- by auto
+ interpret operative f z g
+ using that .
show ?thesis
- apply (subst *)
- apply (rule tagged_division_Un[OF assms(1-2)])
- unfolding interval_split[OF k] interior_cbox
- using k
- apply (auto simp add: box_def elim!: ballE[where x=k])
- done
+ proof
+ show "g {a..b} = z" if "b \<le> a" for a b
+ using that box_empty_imp by simp
+ show "f (g {a..c}) (g {c..b}) = g {a..b}" if "a < c" "c < b" for a b c
+ using that
+ using Basis_imp [of 1 a b c]
+ by (simp_all add: atMost_def [symmetric] atLeast_def [symmetric] max_def min_def)
+qed
qed
-lemma tagged_division_Un_interval_real:
- fixes a :: real
- assumes "p1 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<le> (c::real)})"
- and "p2 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<ge> c})"
- and k: "k \<in> Basis"
- shows "(p1 \<union> p2) tagged_division_of {a .. b}"
- using assms
- unfolding box_real[symmetric]
- by (rule tagged_division_Un_interval)
-
-lemma tagged_division_split_left_inj:
- assumes d: "d tagged_division_of i"
- and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
- and "K1 \<noteq> K2"
- and eq: "K1 \<inter> {x. x \<bullet> k \<le> c} = K2 \<inter> {x. x \<bullet> k \<le> c}"
- shows "interior (K1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
-proof -
- have "interior (K1 \<inter> K2) = {} \<or> (x2, K2) = (x1, K1)"
- using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
- then show ?thesis
- using eq \<open>K1 \<noteq> K2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
-qed
-
-lemma tagged_division_split_right_inj:
- assumes d: "d tagged_division_of i"
- and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
- and "K1 \<noteq> K2"
- and eq: "K1 \<inter> {x. x\<bullet>k \<ge> c} = K2 \<inter> {x. x\<bullet>k \<ge> c}"
- shows "interior (K1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
-proof -
- have "interior (K1 \<inter> K2) = {} \<or> (x2, K2) = (x1, K1)"
- using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
- then show ?thesis
- using eq \<open>K1 \<noteq> K2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
-qed
subsection \<open>Special case of additivity we need for the FTC.\<close>
@@ -1818,10 +1838,11 @@
shows "sum (\<lambda>(x,k). f(Sup k) - f(Inf k)) p = f b - f a"
proof -
let ?f = "(\<lambda>k::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))"
+ interpret operative_real plus 0 ?f
+ rewrites "comm_monoid_set.F op + 0 = sum"
+ by standard[1] (auto simp add: sum_def)
have p_td: "p tagged_division_of cbox a b"
using assms(2) box_real(2) by presburger
- have *: "add.operative ?f"
- unfolding add.operative_1_lt box_eq_empty by auto
have **: "cbox a b \<noteq> {}"
using assms(1) by auto
then have "f b - f a = (\<Sum>(x, l)\<in>p. if l = {} then 0 else f (interval_upperbound l) - f (interval_lowerbound l))"
@@ -1829,14 +1850,12 @@
have "(if cbox a b = {} then 0 else f (interval_upperbound (cbox a b)) - f (interval_lowerbound (cbox a b))) = f b - f a"
using assms by auto
then show ?thesis
- using p_td assms by (simp add: "*" sum.operative_tagged_division)
+ using p_td assms by (simp add: tagged_division)
qed
then show ?thesis
using assms by (auto intro!: sum.cong)
qed
-lemma bgauge_existence_lemma: "(\<forall>x\<in>s. \<exists>d::real. 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. x\<in>s \<longrightarrow> q d x)"
- by (meson zero_less_one)
subsection \<open>Fine-ness of a partition w.r.t. a gauge.\<close>
--- a/src/HOL/Library/Multiset.thy Wed Aug 23 23:46:35 2017 +0100
+++ b/src/HOL/Library/Multiset.thy Thu Aug 24 12:45:46 2017 +0100
@@ -1521,34 +1521,25 @@
lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
by (cases "B = {#}") (auto dest: multi_member_split)
-lemma multiset_partition: "M = {# x\<in>#M. P x #} + {# x\<in>#M. \<not> P x #}"
-apply (subst multiset_eq_iff)
-apply auto
-done
-
-lemma mset_subset_size: "(A::'a multiset) \<subset># B \<Longrightarrow> size A < size B"
+lemma multiset_partition: "M = {#x \<in># M. P x#} + {#x \<in># M. \<not> P x#}"
+ by (subst multiset_eq_iff) auto
+
+lemma mset_subset_size: "A \<subset># B \<Longrightarrow> size A < size B"
proof (induct A arbitrary: B)
- case (empty M)
- then have "M \<noteq> {#}" by (simp add: subset_mset.zero_less_iff_neq_zero)
- then obtain M' x where "M = add_mset x M'"
- by (blast dest: multi_nonempty_split)
- then show ?case by simp
+ case empty
+ then show ?case
+ using nonempty_has_size by auto
next
- case (add x S T)
- have IH: "\<And>B. S \<subset># B \<Longrightarrow> size S < size B" by fact
- have SxsubT: "add_mset x S \<subset># T" by fact
- then have "x \<in># T" and "S \<subset># T"
- by (auto dest: mset_subset_insertD)
- then obtain T' where T: "T = add_mset x T'"
- by (blast dest: multi_member_split)
- then have "S \<subset># T'" using SxsubT
- by simp
- then have "size S < size T'" using IH by simp
- then show ?case using T by simp
+ case (add x A)
+ have "add_mset x A \<subseteq># B"
+ by (meson add.prems subset_mset_def)
+ then show ?case
+ by (metis (no_types) add.prems add.right_neutral add_diff_cancel_left' leD nat_neq_iff
+ size_Diff_submset size_eq_0_iff_empty size_mset_mono subset_mset.le_iff_add subset_mset_def)
qed
lemma size_1_singleton_mset: "size M = 1 \<Longrightarrow> \<exists>a. M = {#a#}"
-by (cases M) auto
+ by (cases M) auto
subsubsection \<open>Strong induction and subset induction for multisets\<close>
@@ -1674,18 +1665,13 @@
"image_mset f = fold_mset (add_mset \<circ> f) {#}"
lemma comp_fun_commute_mset_image: "comp_fun_commute (add_mset \<circ> f)"
-proof
-qed (simp add: fun_eq_iff)
+ by unfold_locales (simp add: fun_eq_iff)
lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
by (simp add: image_mset_def)
lemma image_mset_single: "image_mset f {#x#} = {#f x#}"
-proof -
- interpret comp_fun_commute "add_mset \<circ> f"
- by (fact comp_fun_commute_mset_image)
- show ?thesis by (simp add: image_mset_def)
-qed
+ by (simp add: comp_fun_commute.fold_mset_add_mset comp_fun_commute_mset_image image_mset_def)
lemma image_mset_union [simp]: "image_mset f (M + N) = image_mset f M + image_mset f N"
proof -
@@ -1723,8 +1709,7 @@
finally show ?thesis by simp
qed
-lemma count_image_mset:
- "count (image_mset f A) x = (\<Sum>y\<in>f -` {x} \<inter> set_mset A. count A y)"
+lemma count_image_mset: "count (image_mset f A) x = (\<Sum>y\<in>f -` {x} \<inter> set_mset A. count A y)"
proof (induction A)
case empty
then show ?case by simp
@@ -1733,7 +1718,7 @@
moreover have *: "(if x = y then Suc n else n) = n + (if x = y then 1 else 0)" for n y
by simp
ultimately show ?case
- by (auto simp: sum.distrib sum.delta' intro!: sum.mono_neutral_left)
+ by (auto simp: sum.distrib intro!: sum.mono_neutral_left)
qed
lemma image_mset_subseteq_mono: "A \<subseteq># B \<Longrightarrow> image_mset f A \<subseteq># image_mset f B"
@@ -1765,7 +1750,7 @@
\<close>
lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_mset M"
-by (metis set_image_mset)
+ by simp
functor image_mset: image_mset
proof -
@@ -2065,24 +2050,20 @@
end
-lemma mset_sorted_list_of_multiset [simp]:
- "mset (sorted_list_of_multiset M) = M"
-by (induct M) simp_all
-
-lemma sorted_list_of_multiset_mset [simp]:
- "sorted_list_of_multiset (mset xs) = sort xs"
-by (induct xs) simp_all
-
-lemma finite_set_mset_mset_set[simp]:
- "finite A \<Longrightarrow> set_mset (mset_set A) = A"
-by (induct A rule: finite_induct) simp_all
+lemma mset_sorted_list_of_multiset[simp]: "mset (sorted_list_of_multiset M) = M"
+ by (induct M) simp_all
+
+lemma sorted_list_of_multiset_mset[simp]: "sorted_list_of_multiset (mset xs) = sort xs"
+ by (induct xs) simp_all
+
+lemma finite_set_mset_mset_set[simp]: "finite A \<Longrightarrow> set_mset (mset_set A) = A"
+ by auto
lemma mset_set_empty_iff: "mset_set A = {#} \<longleftrightarrow> A = {} \<or> infinite A"
using finite_set_mset_mset_set by fastforce
-lemma infinite_set_mset_mset_set:
- "\<not> finite A \<Longrightarrow> set_mset (mset_set A) = {}"
-by simp
+lemma infinite_set_mset_mset_set: "\<not> finite A \<Longrightarrow> set_mset (mset_set A) = {}"
+ by simp
lemma set_sorted_list_of_multiset [simp]:
"set (sorted_list_of_multiset M) = set_mset M"
@@ -2108,22 +2089,15 @@
finally show ?case by simp
qed simp_all
-lemma msubset_mset_set_iff [simp]:
- assumes "finite A" "finite B"
- shows "mset_set A \<subseteq># mset_set B \<longleftrightarrow> A \<subseteq> B"
- using subset_imp_msubset_mset_set[of A B]
- set_mset_mono[of "mset_set A" "mset_set B"] assms by auto
-
-lemma mset_set_eq_iff [simp]:
+lemma msubset_mset_set_iff[simp]:
assumes "finite A" "finite B"
- shows "mset_set A = mset_set B \<longleftrightarrow> A = B"
-proof -
- from assms have "mset_set A = mset_set B \<longleftrightarrow> set_mset (mset_set A) = set_mset (mset_set B)"
- by (intro iffI equalityI set_mset_mono) auto
- also from assms have "\<dots> \<longleftrightarrow> A = B" by simp
- finally show ?thesis .
-qed
-
+ shows "mset_set A \<subseteq># mset_set B \<longleftrightarrow> A \<subseteq> B"
+ using assms set_mset_mono subset_imp_msubset_mset_set by fastforce
+
+lemma mset_set_eq_iff[simp]:
+ assumes "finite A" "finite B"
+ shows "mset_set A = mset_set B \<longleftrightarrow> A = B"
+ using assms by (fastforce dest: finite_set_mset_mset_set)
(* Contributed by Lukas Bulwahn *)
lemma image_mset_mset_set:
@@ -2158,17 +2132,14 @@
lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
by (induct D) simp_all
-lemma replicate_count_mset_eq_filter_eq:
- "replicate (count (mset xs) k) k = filter (HOL.eq k) xs"
+lemma replicate_count_mset_eq_filter_eq: "replicate (count (mset xs) k) k = filter (HOL.eq k) xs"
by (induct xs) auto
-lemma replicate_mset_eq_empty_iff [simp]:
- "replicate_mset n a = {#} \<longleftrightarrow> n = 0"
+lemma replicate_mset_eq_empty_iff [simp]: "replicate_mset n a = {#} \<longleftrightarrow> n = 0"
by (induct n) simp_all
lemma replicate_mset_eq_iff:
- "replicate_mset m a = replicate_mset n b \<longleftrightarrow>
- m = 0 \<and> n = 0 \<or> m = n \<and> a = b"
+ "replicate_mset m a = replicate_mset n b \<longleftrightarrow> m = 0 \<and> n = 0 \<or> m = n \<and> a = b"
by (auto simp add: multiset_eq_iff)
lemma repeat_mset_cancel1: "repeat_mset a A = repeat_mset a B \<longleftrightarrow> A = B \<or> a = 0"
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Aug 23 23:46:35 2017 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Aug 24 12:45:46 2017 +0100
@@ -278,7 +278,8 @@
map2 (map o derive_overloaded_size_simp) overloaded_size_defs' size_simpss;
val overloaded_size_simps = flat overloaded_size_simpss;
val size_thmss = map2 append size_simpss overloaded_size_simpss;
- val size_gen_thmss = size_simpss
+ val size_gen_thmss = size_simpss;
+
fun rhs_is_zero thm =
let val Const (trueprop, _) $ (Const (eq, _) $ _ $ rhs) = Thm.prop_of thm in
trueprop = @{const_name Trueprop} andalso eq = @{const_name HOL.eq} andalso