--- a/NEWS Wed Jun 10 18:48:48 2015 +0200
+++ b/NEWS Wed Jun 10 18:57:31 2015 +0200
@@ -73,6 +73,30 @@
separate constants, and infix syntax is usually not available during
instantiation.
+* Library/Multiset:
+ - Renamed multiset inclusion operators:
+ < ~> <#
+ \<subset> ~> \<subset>#
+ <= ~> <=#
+ \<le> ~> \<le>#
+ \<subseteq> ~> \<subseteq>#
+ INCOMPATIBILITY.
+ - "'a multiset" is no longer an instance of the "order",
+ "ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff",
+ "semilattice_inf", and "semilattice_sup" type classes. The theorems
+ previously provided by these type classes (directly or indirectly)
+ are now available through the "subset_mset" interpretation
+ (e.g. add_mono ~> subset_mset.add_mono).
+ INCOMPATIBILITY.
+ - Renamed lemmas:
+ mset_le_def ~> subseteq_mset_def
+ mset_less_def ~> subset_mset_def
+ less_eq_multiset.rep_eq ~> subseteq_mset_def
+ INCOMPATIBILITY
+ - Removed lemmas generated by lift_definition:
+ less_eq_multiset.abs_eq, less_eq_multiset.rsp less_eq_multiset.transfer
+ less_eq_multiset_def
+ INCOMPATIBILITY
New in Isabelle2015 (May 2015)
------------------------------
--- a/src/HOL/Algebra/Divisibility.thy Wed Jun 10 18:48:48 2015 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Wed Jun 10 18:57:31 2015 +0200
@@ -2137,7 +2137,7 @@
assumes ab: "a divides b"
and afs: "wfactors G as a" and bfs: "wfactors G bs b"
and carr: "a \<in> carrier G" "b \<in> carrier G" "set as \<subseteq> carrier G" "set bs \<subseteq> carrier G"
- shows "fmset G as \<le> fmset G bs"
+ shows "fmset G as \<le># fmset G bs"
using ab
proof (elim dividesE)
fix c
@@ -2157,7 +2157,7 @@
qed
lemma (in comm_monoid_cancel) fmsubset_divides:
- assumes msubset: "fmset G as \<le> fmset G bs"
+ assumes msubset: "fmset G as \<le># fmset G bs"
and afs: "wfactors G as a" and bfs: "wfactors G bs b"
and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"
@@ -2193,7 +2193,7 @@
from csmset msubset
have "fmset G bs = fmset G as + fmset G cs"
- by (simp add: multiset_eq_iff mset_le_def)
+ by (simp add: multiset_eq_iff subseteq_mset_def)
hence basc: "b \<sim> a \<otimes> c"
by (rule fmset_wfactors_mult) fact+
@@ -2210,7 +2210,7 @@
assumes "wfactors G as a" and "wfactors G bs b"
and "a \<in> carrier G" and "b \<in> carrier G"
and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
- shows "a divides b = (fmset G as \<le> fmset G bs)"
+ shows "a divides b = (fmset G as \<le># fmset G bs)"
using assms
by (blast intro: divides_fmsubset fmsubset_divides)
@@ -2218,7 +2218,7 @@
text {* Proper factors on multisets *}
lemma (in factorial_monoid) fmset_properfactor:
- assumes asubb: "fmset G as \<le> fmset G bs"
+ assumes asubb: "fmset G as \<le># fmset G bs"
and anb: "fmset G as \<noteq> fmset G bs"
and "wfactors G as a" and "wfactors G bs b"
and "a \<in> carrier G" and "b \<in> carrier G"
@@ -2228,10 +2228,10 @@
apply (rule fmsubset_divides[of as bs], fact+)
proof
assume "b divides a"
- hence "fmset G bs \<le> fmset G as"
+ hence "fmset G bs \<le># fmset G as"
by (rule divides_fmsubset) fact+
with asubb
- have "fmset G as = fmset G bs" by (rule order_antisym)
+ have "fmset G as = fmset G bs" by (rule subset_mset.antisym)
with anb
show "False" ..
qed
@@ -2241,7 +2241,7 @@
and "wfactors G as a" and "wfactors G bs b"
and "a \<in> carrier G" and "b \<in> carrier G"
and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
- shows "fmset G as \<le> fmset G bs \<and> fmset G as \<noteq> fmset G bs"
+ shows "fmset G as \<le># fmset G bs \<and> fmset G as \<noteq> fmset G bs"
using pf
apply (elim properfactorE)
apply rule
@@ -2619,13 +2619,13 @@
have "c gcdof a b"
proof (simp add: isgcd_def, safe)
from csmset
- have "fmset G cs \<le> fmset G as"
- by (simp add: multiset_inter_def mset_le_def)
+ have "fmset G cs \<le># fmset G as"
+ by (simp add: multiset_inter_def subset_mset_def)
thus "c divides a" by (rule fmsubset_divides) fact+
next
from csmset
- have "fmset G cs \<le> fmset G bs"
- by (simp add: multiset_inter_def mset_le_def, force)
+ have "fmset G cs \<le># fmset G bs"
+ by (simp add: multiset_inter_def subseteq_mset_def, force)
thus "c divides b" by (rule fmsubset_divides) fact+
next
fix y
@@ -2637,13 +2637,13 @@
by auto
assume "y divides a"
- hence ya: "fmset G ys \<le> fmset G as" by (rule divides_fmsubset) fact+
+ hence ya: "fmset G ys \<le># fmset G as" by (rule divides_fmsubset) fact+
assume "y divides b"
- hence yb: "fmset G ys \<le> fmset G bs" by (rule divides_fmsubset) fact+
+ hence yb: "fmset G ys \<le># fmset G bs" by (rule divides_fmsubset) fact+
from ya yb csmset
- have "fmset G ys \<le> fmset G cs" by (simp add: mset_le_def)
+ have "fmset G ys \<le># fmset G cs" by (simp add: subset_mset_def)
thus "y divides c" by (rule fmsubset_divides) fact+
qed
@@ -2718,10 +2718,10 @@
have "c lcmof a b"
proof (simp add: islcm_def, safe)
- from csmset have "fmset G as \<le> fmset G cs" by (simp add: mset_le_def, force)
+ from csmset have "fmset G as \<le># fmset G cs" by (simp add: subseteq_mset_def, force)
thus "a divides c" by (rule fmsubset_divides) fact+
next
- from csmset have "fmset G bs \<le> fmset G cs" by (simp add: mset_le_def)
+ from csmset have "fmset G bs \<le># fmset G cs" by (simp add: subset_mset_def)
thus "b divides c" by (rule fmsubset_divides) fact+
next
fix y
@@ -2733,14 +2733,14 @@
by auto
assume "a divides y"
- hence ya: "fmset G as \<le> fmset G ys" by (rule divides_fmsubset) fact+
+ hence ya: "fmset G as \<le># fmset G ys" by (rule divides_fmsubset) fact+
assume "b divides y"
- hence yb: "fmset G bs \<le> fmset G ys" by (rule divides_fmsubset) fact+
+ hence yb: "fmset G bs \<le># fmset G ys" by (rule divides_fmsubset) fact+
from ya yb csmset
- have "fmset G cs \<le> fmset G ys"
- apply (simp add: mset_le_def, clarify)
+ have "fmset G cs \<le># fmset G ys"
+ apply (simp add: subseteq_mset_def, clarify)
apply (case_tac "count (fmset G as) a < count (fmset G bs) a")
apply simp
apply simp
--- a/src/HOL/Library/DAList_Multiset.thy Wed Jun 10 18:48:48 2015 +0200
+++ b/src/HOL/Library/DAList_Multiset.thy Wed Jun 10 18:57:31 2015 +0200
@@ -18,9 +18,9 @@
lemma [code, code del]: "minus = (minus :: 'a multiset \<Rightarrow> _)" ..
-lemma [code, code del]: "inf = (inf :: 'a multiset \<Rightarrow> _)" ..
+lemma [code, code del]: "inf_subset_mset = (inf_subset_mset :: 'a multiset \<Rightarrow> _)" ..
-lemma [code, code del]: "sup = (sup :: 'a multiset \<Rightarrow> _)" ..
+lemma [code, code del]: "sup_subset_mset = (sup_subset_mset :: 'a multiset \<Rightarrow> _)" ..
lemma [code, code del]: "image_mset = image_mset" ..
@@ -38,9 +38,9 @@
lemma [code, code del]: "sorted_list_of_multiset = sorted_list_of_multiset" ..
-lemma [code, code del]: "ord_multiset_inst.less_eq_multiset = ord_multiset_inst.less_eq_multiset" ..
+lemma [code, code del]: "subset_mset = subset_mset" ..
-lemma [code, code del]: "ord_multiset_inst.less_multiset = ord_multiset_inst.less_multiset" ..
+lemma [code, code del]: "subseteq_mset = subseteq_mset" ..
lemma [code, code del]: "equal_multiset_inst.equal_multiset = equal_multiset_inst.equal_multiset" ..
@@ -203,21 +203,21 @@
by (rule multiset_eqI) (simp add: count_of_filter DAList.filter.rep_eq)
-lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<le> m2 \<and> m2 \<le> m1"
- by (metis equal_multiset_def eq_iff)
+lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<le># m2 \<and> m2 \<le># m1"
+ by (metis equal_multiset_def subset_mset.eq_iff)
text \<open>By default the code for @{text "<"} is @{prop"xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> xs = ys"}.
With equality implemented by @{text"\<le>"}, this leads to three calls of @{text"\<le>"}.
Here is a more efficient version:\<close>
-lemma mset_less[code]: "xs < (ys :: 'a multiset) \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
- by (rule less_le_not_le)
+lemma mset_less[code]: "xs <# (ys :: 'a multiset) \<longleftrightarrow> xs \<le># ys \<and> \<not> ys \<le># xs"
+ by (rule subset_mset.less_le_not_le)
lemma mset_less_eq_Bag0:
- "Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)"
+ "Bag xs \<le># A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
assume ?lhs
- then show ?rhs by (auto simp add: mset_le_def)
+ then show ?rhs by (auto simp add: subseteq_mset_def)
next
assume ?rhs
show ?lhs
@@ -225,12 +225,12 @@
fix x
from \<open>?rhs\<close> have "count_of (DAList.impl_of xs) x \<le> count A x"
by (cases "x \<in> fst ` set (DAList.impl_of xs)") (auto simp add: count_of_empty)
- then show "count (Bag xs) x \<le> count A x" by (simp add: mset_le_def)
+ then show "count (Bag xs) x \<le> count A x" by (simp add: subset_mset_def)
qed
qed
lemma mset_less_eq_Bag [code]:
- "Bag xs \<le> (A :: 'a multiset) \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). n \<le> count A x)"
+ "Bag xs \<le># (A :: 'a multiset) \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). n \<le> count A x)"
proof -
{
fix x n
@@ -266,7 +266,7 @@
qed
declare multiset_inter_def [code]
-declare sup_multiset_def [code]
+declare sup_subset_mset_def [code]
declare multiset_of.simps [code]
--- a/src/HOL/Library/Multiset.thy Wed Jun 10 18:48:48 2015 +0200
+++ b/src/HOL/Library/Multiset.thy Wed Jun 10 18:57:31 2015 +0200
@@ -280,157 +280,137 @@
subsubsection {* Pointwise ordering induced by count *}
-instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le
-begin
-
-lift_definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" is "\<lambda> A B. (\<forall>a. A a \<le> B a)" .
-
-lemmas mset_le_def = less_eq_multiset_def
-
-definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
- mset_less_def: "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
-
-instance
- by default (auto simp add: mset_le_def mset_less_def multiset_eq_iff intro: order_trans antisym)
-
-end
-
-abbreviation less_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
- "A <# B \<equiv> A < B"
-abbreviation (xsymbols) subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50) where
- "A \<subset># B \<equiv> A < B"
-
-abbreviation less_eq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
- "A <=# B \<equiv> A \<le> B"
-abbreviation (xsymbols) leq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<le>#" 50) where
- "A \<le># B \<equiv> A \<le> B"
-abbreviation (xsymbols) subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subseteq>#" 50) where
- "A \<subseteq># B \<equiv> A \<le> B"
+definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
+"subseteq_mset A B = (\<forall>a. count A a \<le> count B a)"
+
+definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
+"subset_mset A B = (A <=# B \<and> A \<noteq> B)"
+
+notation subseteq_mset (infix "\<le>#" 50)
+notation (xsymbols) subseteq_mset (infix "\<subseteq>#" 50)
+
+notation (xsymbols) subset_mset (infix "\<subset>#" 50)
+
+interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op <=#" "op <#"
+ by default (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
lemma mset_less_eqI:
- "(\<And>x. count A x \<le> count B x) \<Longrightarrow> A \<le> B"
- by (simp add: mset_le_def)
+ "(\<And>x. count A x \<le> count B x) \<Longrightarrow> A \<le># B"
+ by (simp add: subseteq_mset_def)
lemma mset_le_exists_conv:
- "(A::'a multiset) \<le> B \<longleftrightarrow> (\<exists>C. B = A + C)"
-apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI)
+ "(A::'a multiset) \<le># B \<longleftrightarrow> (\<exists>C. B = A + C)"
+apply (unfold subseteq_mset_def, rule iffI, rule_tac x = "B - A" in exI)
apply (auto intro: multiset_eq_iff [THEN iffD2])
done
-instance multiset :: (type) ordered_cancel_comm_monoid_diff
+interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" "op -" 0 "op \<le>#" "op <#"
by default (simp, fact mset_le_exists_conv)
lemma mset_le_mono_add_right_cancel [simp]:
- "(A::'a multiset) + C \<le> B + C \<longleftrightarrow> A \<le> B"
- by (fact add_le_cancel_right)
+ "(A::'a multiset) + C \<le># B + C \<longleftrightarrow> A \<le># B"
+ by (fact subset_mset.add_le_cancel_right)
lemma mset_le_mono_add_left_cancel [simp]:
- "C + (A::'a multiset) \<le> C + B \<longleftrightarrow> A \<le> B"
- by (fact add_le_cancel_left)
+ "C + (A::'a multiset) \<le># C + B \<longleftrightarrow> A \<le># B"
+ by (fact subset_mset.add_le_cancel_left)
lemma mset_le_mono_add:
- "(A::'a multiset) \<le> B \<Longrightarrow> C \<le> D \<Longrightarrow> A + C \<le> B + D"
- by (fact add_mono)
+ "(A::'a multiset) \<le># B \<Longrightarrow> C \<le># D \<Longrightarrow> A + C \<le># B + D"
+ by (fact subset_mset.add_mono)
lemma mset_le_add_left [simp]:
- "(A::'a multiset) \<le> A + B"
- unfolding mset_le_def by auto
+ "(A::'a multiset) \<le># A + B"
+ unfolding subseteq_mset_def by auto
lemma mset_le_add_right [simp]:
- "B \<le> (A::'a multiset) + B"
- unfolding mset_le_def by auto
+ "B \<le># (A::'a multiset) + B"
+ unfolding subseteq_mset_def by auto
lemma mset_le_single:
- "a :# B \<Longrightarrow> {#a#} \<le> B"
- by (simp add: mset_le_def)
+ "a :# B \<Longrightarrow> {#a#} \<le># B"
+ by (simp add: subseteq_mset_def)
lemma multiset_diff_union_assoc:
- "C \<le> B \<Longrightarrow> (A::'a multiset) + B - C = A + (B - C)"
- by (simp add: multiset_eq_iff mset_le_def)
+ "C \<le># B \<Longrightarrow> (A::'a multiset) + B - C = A + (B - C)"
+ by (simp add: subset_mset.diff_add_assoc)
lemma mset_le_multiset_union_diff_commute:
- "B \<le> A \<Longrightarrow> (A::'a multiset) - B + C = A + C - B"
-by (simp add: multiset_eq_iff mset_le_def)
-
-lemma diff_le_self[simp]: "(M::'a multiset) - N \<le> M"
-by(simp add: mset_le_def)
-
-lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
-apply (clarsimp simp: mset_le_def mset_less_def)
+ "B \<le># A \<Longrightarrow> (A::'a multiset) - B + C = A + C - B"
+by (simp add: subset_mset.add_diff_assoc2)
+
+lemma diff_le_self[simp]: "(M::'a multiset) - N \<le># M"
+by(simp add: subseteq_mset_def)
+
+lemma mset_lessD: "A <# B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
+apply (clarsimp simp: subset_mset_def subseteq_mset_def)
apply (erule_tac x=x in allE)
apply auto
done
-lemma mset_leD: "A \<le> B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
-apply (clarsimp simp: mset_le_def mset_less_def)
+lemma mset_leD: "A \<le># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
+apply (clarsimp simp: subset_mset_def subseteq_mset_def)
apply (erule_tac x = x in allE)
apply auto
done
-lemma mset_less_insertD: "(A + {#x#} < B) \<Longrightarrow> (x \<in># B \<and> A < B)"
+lemma mset_less_insertD: "(A + {#x#} <# B) \<Longrightarrow> (x \<in># B \<and> A <# B)"
apply (rule conjI)
apply (simp add: mset_lessD)
-apply (clarsimp simp: mset_le_def mset_less_def)
+apply (clarsimp simp: subset_mset_def subseteq_mset_def)
apply safe
apply (erule_tac x = a in allE)
apply (auto split: split_if_asm)
done
-lemma mset_le_insertD: "(A + {#x#} \<le> B) \<Longrightarrow> (x \<in># B \<and> A \<le> B)"
+lemma mset_le_insertD: "(A + {#x#} \<le># B) \<Longrightarrow> (x \<in># B \<and> A \<le># B)"
apply (rule conjI)
apply (simp add: mset_leD)
-apply (force simp: mset_le_def mset_less_def split: split_if_asm)
+apply (force simp: subset_mset_def subseteq_mset_def split: split_if_asm)
done
-lemma mset_less_of_empty[simp]: "A < {#} \<longleftrightarrow> False"
- by (auto simp add: mset_less_def mset_le_def multiset_eq_iff)
-
-lemma empty_le[simp]: "{#} \<le> A"
+lemma mset_less_of_empty[simp]: "A <# {#} \<longleftrightarrow> False"
+ by (auto simp add: subseteq_mset_def subset_mset_def multiset_eq_iff)
+
+lemma empty_le[simp]: "{#} \<le># A"
unfolding mset_le_exists_conv by auto
-lemma le_empty[simp]: "(M \<le> {#}) = (M = {#})"
+lemma le_empty[simp]: "(M \<le># {#}) = (M = {#})"
unfolding mset_le_exists_conv by auto
-lemma multi_psub_of_add_self[simp]: "A < A + {#x#}"
- by (auto simp: mset_le_def mset_less_def)
-
-lemma multi_psub_self[simp]: "(A::'a multiset) < A = False"
+lemma multi_psub_of_add_self[simp]: "A <# A + {#x#}"
+ by (auto simp: subset_mset_def subseteq_mset_def)
+
+lemma multi_psub_self[simp]: "(A::'a multiset) <# A = False"
by simp
-lemma mset_less_add_bothsides: "N + {#x#} < M + {#x#} \<Longrightarrow> N < M"
- by (fact add_less_imp_less_right)
+lemma mset_less_add_bothsides: "N + {#x#} <# M + {#x#} \<Longrightarrow> N <# M"
+ by (fact subset_mset.add_less_imp_less_right)
lemma mset_less_empty_nonempty:
- "{#} < S \<longleftrightarrow> S \<noteq> {#}"
- by (auto simp: mset_le_def mset_less_def)
+ "{#} <# S \<longleftrightarrow> S \<noteq> {#}"
+ by (auto simp: subset_mset_def subseteq_mset_def)
lemma mset_less_diff_self:
- "c \<in># B \<Longrightarrow> B - {#c#} < B"
- by (auto simp: mset_le_def mset_less_def multiset_eq_iff)
+ "c \<in># B \<Longrightarrow> B - {#c#} <# B"
+ by (auto simp: subset_mset_def subseteq_mset_def multiset_eq_iff)
subsubsection {* Intersection *}
-instantiation multiset :: (type) semilattice_inf
-begin
-
-definition inf_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
- multiset_inter_def: "inf_multiset A B = A - (A - B)"
-
-instance
+definition inf_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where
+ multiset_inter_def: "inf_subset_mset A B = A - (A - B)"
+
+interpretation subset_mset: semilattice_inf inf_subset_mset "op \<le>#" "op <#"
proof -
- have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" by arith
- show "OFCLASS('a multiset, semilattice_inf_class)"
- by default (auto simp add: multiset_inter_def mset_le_def aux)
+ have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" by arith
+ show "class.semilattice_inf op #\<inter> op \<le># op <#"
+ by default (auto simp add: multiset_inter_def subseteq_mset_def aux)
qed
-end
-
-abbreviation multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where
- "multiset_inter \<equiv> inf"
lemma multiset_inter_count [simp]:
- "count (A #\<inter> B) x = min (count A x) (count B x)"
+ "count ((A::'a multiset) #\<inter> B) x = min (count A x) (count B x)"
by (simp add: multiset_inter_def)
lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
@@ -475,28 +455,19 @@
subsubsection {* Bounded union *}
-
-instantiation multiset :: (type) semilattice_sup
-begin
-
-definition sup_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
- "sup_multiset A B = A + (B - A)"
-
-instance
+definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "#\<union>" 70) where
+ "sup_subset_mset A B = A + (B - A)"
+
+interpretation subset_mset: semilattice_sup sup_subset_mset "op \<le>#" "op <#"
proof -
have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" by arith
- show "OFCLASS('a multiset, semilattice_sup_class)"
- by default (auto simp add: sup_multiset_def mset_le_def aux)
+ show "class.semilattice_sup op #\<union> op \<le># op <#"
+ by default (auto simp add: sup_subset_mset_def subseteq_mset_def aux)
qed
-end
-
-abbreviation sup_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<union>" 70) where
- "sup_multiset \<equiv> sup"
-
-lemma sup_multiset_count [simp]:
+lemma sup_subset_mset_count [simp]:
"count (A #\<union> B) x = max (count A x) (count B x)"
- by (simp add: sup_multiset_def)
+ by (simp add: sup_subset_mset_def)
lemma empty_sup [simp]:
"{#} #\<union> M = M"
@@ -522,6 +493,8 @@
"x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = ((N - {#x#}) #\<union> M) + {#x#}"
by (simp add: multiset_eq_iff)
+subsubsection {*Subset is an order*}
+interpretation subset_mset: order "op \<le>#" "op <#" by unfold_locales auto
subsubsection {* Filter (with comprehension syntax) *}
@@ -555,11 +528,11 @@
"filter_mset P (M #\<inter> N) = filter_mset P M #\<inter> filter_mset P N"
by (rule multiset_eqI) simp
-lemma multiset_filter_subset[simp]: "filter_mset f M \<le> M"
- unfolding less_eq_multiset.rep_eq by auto
-
-lemma multiset_filter_mono: assumes "A \<le> B"
- shows "filter_mset f A \<le> filter_mset f B"
+lemma multiset_filter_subset[simp]: "filter_mset f M \<le># M"
+ by (simp add: mset_less_eqI)
+
+lemma multiset_filter_mono: assumes "A \<le># B"
+ shows "filter_mset f A \<le># filter_mset f B"
proof -
from assms[unfolded mset_le_exists_conv]
obtain C where B: "B = A + C" by auto
@@ -603,7 +576,7 @@
lemma finite_Collect_mem [iff]: "finite {x. x :# M}"
unfolding set_of_def[symmetric] by simp
-lemma set_of_mono: "A \<le> B \<Longrightarrow> set_of A \<subseteq> set_of B"
+lemma set_of_mono: "A \<le># B \<Longrightarrow> set_of A \<subseteq> set_of B"
by (metis mset_leD subsetI mem_set_of_iff)
lemma ball_set_of_iff: "(\<forall>x \<in> set_of M. P x) \<longleftrightarrow> (\<forall>x. x \<in># M \<longrightarrow> P x)"
@@ -685,7 +658,7 @@
then show ?thesis by blast
qed
-lemma size_mset_mono: assumes "A \<le> B"
+lemma size_mset_mono: assumes "A \<le># B"
shows "size A \<le> size(B::_ multiset)"
proof -
from assms[unfolded mset_le_exists_conv]
@@ -697,7 +670,7 @@
by (rule size_mset_mono[OF multiset_filter_subset])
lemma size_Diff_submset:
- "M \<le> M' \<Longrightarrow> size (M' - M) = size M' - size(M::'a multiset)"
+ "M \<le># M' \<Longrightarrow> size (M' - M) = size M' - size(M::'a multiset)"
by (metis add_diff_cancel_left' size_union mset_le_exists_conv)
subsection {* Induction and case splits *}
@@ -732,7 +705,7 @@
apply auto
done
-lemma mset_less_size: "(A::'a multiset) < B \<Longrightarrow> size A < size B"
+lemma mset_less_size: "(A::'a multiset) <# B \<Longrightarrow> size A < size B"
proof (induct A arbitrary: B)
case (empty M)
then have "M \<noteq> {#}" by (simp add: mset_less_empty_nonempty)
@@ -741,12 +714,12 @@
then show ?case by simp
next
case (add S x T)
- have IH: "\<And>B. S < B \<Longrightarrow> size S < size B" by fact
- have SxsubT: "S + {#x#} < T" by fact
- then have "x \<in># T" and "S < T" by (auto dest: mset_less_insertD)
+ have IH: "\<And>B. S <# B \<Longrightarrow> size S < size B" by fact
+ have SxsubT: "S + {#x#} <# T" by fact
+ then have "x \<in># T" and "S <# T" by (auto dest: mset_less_insertD)
then obtain T' where T: "T = T' + {#x#}"
by (blast dest: multi_member_split)
- then have "S < T'" using SxsubT
+ then have "S <# T'" using SxsubT
by (blast intro: mset_less_add_bothsides)
then have "size S < size T'" using IH by simp
then show ?case using T by simp
@@ -760,35 +733,35 @@
text {* Well-foundedness of strict subset relation *}
-lemma wf_less_mset_rel: "wf {(M, N :: 'a multiset). M < N}"
+lemma wf_less_mset_rel: "wf {(M, N :: 'a multiset). M <# N}"
apply (rule wf_measure [THEN wf_subset, where f1=size])
apply (clarsimp simp: measure_def inv_image_def mset_less_size)
done
lemma full_multiset_induct [case_names less]:
-assumes ih: "\<And>B. \<forall>(A::'a multiset). A < B \<longrightarrow> P A \<Longrightarrow> P B"
+assumes ih: "\<And>B. \<forall>(A::'a multiset). A <# B \<longrightarrow> P A \<Longrightarrow> P B"
shows "P B"
apply (rule wf_less_mset_rel [THEN wf_induct])
apply (rule ih, auto)
done
lemma multi_subset_induct [consumes 2, case_names empty add]:
-assumes "F \<le> A"
+assumes "F \<le># A"
and empty: "P {#}"
and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})"
shows "P F"
proof -
- from `F \<le> A`
+ from `F \<le># A`
show ?thesis
proof (induct F)
show "P {#}" by fact
next
fix x F
- assume P: "F \<le> A \<Longrightarrow> P F" and i: "F + {#x#} \<le> A"
+ assume P: "F \<le># A \<Longrightarrow> P F" and i: "F + {#x#} \<le># A"
show "P (F + {#x#})"
proof (rule insert)
from i show "x \<in># A" by (auto dest: mset_le_insertD)
- from i have "F \<le> A" by (auto dest: mset_le_insertD)
+ from i have "F \<le># A" by (auto dest: mset_le_insertD)
with P show "P F" .
qed
qed
@@ -1280,8 +1253,8 @@
lemma msetsum_diff:
fixes M N :: "('a \<Colon> ordered_cancel_comm_monoid_diff) multiset"
- shows "N \<le> M \<Longrightarrow> msetsum (M - N) = msetsum M - msetsum N"
- by (metis add_diff_cancel_left' msetsum.union ordered_cancel_comm_monoid_diff_class.add_diff_inverse)
+ shows "N \<le># M \<Longrightarrow> msetsum (M - N) = msetsum M - msetsum N"
+ by (metis add_diff_cancel_right' msetsum.union subset_mset.diff_add)
lemma size_eq_msetsum: "size M = msetsum (image_mset (\<lambda>_. 1) M)"
proof (induct M)
@@ -1404,8 +1377,9 @@
lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n"
by (induct n, simp_all)
-lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<le> M"
- by (auto simp add: assms mset_less_eqI) (metis count_replicate_mset less_eq_multiset.rep_eq)
+lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<le># M"
+ by (auto simp add: assms mset_less_eqI) (metis count_replicate_mset subseteq_mset_def)
+
lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
by (induct D) simp_all
@@ -1555,8 +1529,8 @@
hide_const (open) part
-lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le> multiset_of xs"
- by (induct xs) (auto intro: order_trans)
+lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le># multiset_of xs"
+ by (induct xs) (auto intro: subset_mset.order_trans)
lemma multiset_of_update:
"i < length ls \<Longrightarrow> multiset_of (ls[i := v]) = multiset_of ls - {#ls ! i#} + {#v#}"
@@ -2037,17 +2011,17 @@
lemma multi_union_self_other_eq: "(A::'a multiset) + X = A + Y \<Longrightarrow> X = Y"
by (fact add_left_imp_eq)
-lemma mset_less_trans: "(M::'a multiset) < K \<Longrightarrow> K < N \<Longrightarrow> M < N"
- by (fact order_less_trans)
+lemma mset_less_trans: "(M::'a multiset) <# K \<Longrightarrow> K <# N \<Longrightarrow> M <# N"
+ by (fact subset_mset.less_trans)
lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
- by (fact inf.commute)
+ by (fact subset_mset.inf.commute)
lemma multiset_inter_assoc: "A #\<inter> (B #\<inter> C) = A #\<inter> B #\<inter> C"
- by (fact inf.assoc [symmetric])
+ by (fact subset_mset.inf.assoc [symmetric])
lemma multiset_inter_left_commute: "A #\<inter> (B #\<inter> C) = B #\<inter> (A #\<inter> C)"
- by (fact inf.left_commute)
+ by (fact subset_mset.inf.left_commute)
lemmas multiset_inter_ac =
multiset_inter_commute
@@ -2182,8 +2156,8 @@
None \<Rightarrow> None
| Some (ys1,_,ys2) \<Rightarrow> ms_lesseq_impl xs (ys1 @ ys2))"
-lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \<longleftrightarrow> \<not> multiset_of xs \<le> multiset_of ys) \<and>
- (ms_lesseq_impl xs ys = Some True \<longleftrightarrow> multiset_of xs < multiset_of ys) \<and>
+lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \<longleftrightarrow> \<not> multiset_of xs \<le># multiset_of ys) \<and>
+ (ms_lesseq_impl xs ys = Some True \<longleftrightarrow> multiset_of xs <# multiset_of ys) \<and>
(ms_lesseq_impl xs ys = Some False \<longrightarrow> multiset_of xs = multiset_of ys)"
proof (induct xs arbitrary: ys)
case (Nil ys)
@@ -2195,13 +2169,13 @@
case None
hence x: "x \<notin> set ys" by (simp add: extract_None_iff)
{
- assume "multiset_of (x # xs) \<le> multiset_of ys"
+ assume "multiset_of (x # xs) \<le># multiset_of ys"
from set_of_mono[OF this] x have False by simp
} note nle = this
moreover
{
- assume "multiset_of (x # xs) < multiset_of ys"
- hence "multiset_of (x # xs) \<le> multiset_of ys" by auto
+ assume "multiset_of (x # xs) <# multiset_of ys"
+ hence "multiset_of (x # xs) \<le># multiset_of ys" by auto
from nle[OF this] have False .
}
ultimately show ?thesis using None by auto
@@ -2216,14 +2190,14 @@
unfolding Some option.simps split
unfolding id
using Cons[of "ys1 @ ys2"]
- unfolding mset_le_def mset_less_def by auto
+ unfolding subset_mset_def subseteq_mset_def by auto
qed
qed
-lemma [code]: "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys \<noteq> None"
+lemma [code]: "multiset_of xs \<le># multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys \<noteq> None"
using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
-lemma [code]: "multiset_of xs < multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys = Some True"
+lemma [code]: "multiset_of xs <# multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys = Some True"
using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
instantiation multiset :: (equal) equal
--- a/src/HOL/Library/Multiset_Order.thy Wed Jun 10 18:48:48 2015 +0200
+++ b/src/HOL/Library/Multiset_Order.thy Wed Jun 10 18:57:31 2015 +0200
@@ -69,7 +69,7 @@
definition less_multiset\<^sub>D\<^sub>M where
"less_multiset\<^sub>D\<^sub>M M N \<longleftrightarrow>
- (\<exists>X Y. X \<noteq> {#} \<and> X \<le> N \<and> M = (N - X) + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)))"
+ (\<exists>X Y. X \<noteq> {#} \<and> X \<le># N \<and> M = (N - X) + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)))"
text {* The Huet--Oppen ordering: *}
@@ -134,12 +134,12 @@
proof -
assume "less_multiset\<^sub>D\<^sub>M M N"
then obtain X Y where
- "X \<noteq> {#}" and "X \<le> N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
+ "X \<noteq> {#}" and "X \<le># N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
unfolding less_multiset\<^sub>D\<^sub>M_def by blast
then have "(N - X + Y, N - X + X) \<in> mult {(x, y). x < y}"
by (intro one_step_implies_mult) (auto simp: Bex_def trans_def)
- with `M = N - X + Y` `X \<le> N` show "(M, N) \<in> mult {(x, y). x < y}"
- by (metis ordered_cancel_comm_monoid_diff_class.diff_add)
+ with `M = N - X + Y` `X \<le># N` show "(M, N) \<in> mult {(x, y). x < y}"
+ by (metis subset_mset.diff_add)
qed
lemma less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M: "less_multiset\<^sub>H\<^sub>O M N \<Longrightarrow> less_multiset\<^sub>D\<^sub>M M N"
@@ -151,7 +151,7 @@
def X \<equiv> "N - M"
def Y \<equiv> "M - N"
from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
- from z show "X \<le> N" unfolding X_def by auto
+ from z show "X \<le># N" unfolding X_def by auto
show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
proof (intro allI impI)
@@ -239,9 +239,9 @@
lemma less_eq_imp_le_multiset:
fixes M N :: "('a \<Colon> linorder) multiset"
- shows "M \<le> N \<Longrightarrow> M #\<subseteq># N"
+ shows "M \<le># N \<Longrightarrow> M #\<subseteq># N"
unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O
- by (auto dest: leD simp add: less_eq_multiset.rep_eq)
+ by (simp add: less_le_not_le subseteq_mset_def)
lemma less_multiset_right_total:
fixes M :: "('a \<Colon> linorder) multiset"
@@ -302,7 +302,7 @@
unfolding less_multiset\<^sub>H\<^sub>O by (metis add.left_neutral add_lessD1 dual_order.strict_iff_order
less_not_sym mset_leD mset_le_add_left)
-lemma union_less_diff_plus: "P \<le> M \<Longrightarrow> N #\<subset># P \<Longrightarrow> M - P + N #\<subset># M"
- by (drule ordered_cancel_comm_monoid_diff_class.diff_add[symmetric]) (metis union_less_mono2)
+lemma union_less_diff_plus: "P \<le># M \<Longrightarrow> N #\<subset># P \<Longrightarrow> M - P + N #\<subset># M"
+ by (drule subset_mset.diff_add[symmetric]) (metis union_less_mono2)
end
--- a/src/HOL/Library/Permutation.thy Wed Jun 10 18:48:48 2015 +0200
+++ b/src/HOL/Library/Permutation.thy Wed Jun 10 18:57:31 2015 +0200
@@ -140,7 +140,7 @@
apply simp
done
-lemma multiset_of_le_perm_append: "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
+lemma multiset_of_le_perm_append: "multiset_of xs \<le># multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
apply (insert surj_multiset_of)
apply (drule surjD)
--- a/src/HOL/Multivariate_Analysis/Integration.thy Wed Jun 10 18:48:48 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Jun 10 18:57:31 2015 +0200
@@ -241,8 +241,9 @@
and "\<forall>t\<in>f. \<exists>a b. t = cbox a b"
and "\<forall>t\<in>f. s \<inter> (interior t) = {}"
shows "s \<inter> interior (\<Union>f) = {}"
-proof (rule ccontr, unfold ex_in_conv[symmetric])
- case goal1
+proof (clarsimp simp only: all_not_in_conv [symmetric])
+ fix x
+ assume x: "x \<in> s" "x \<in> interior (\<Union>f)"
have lem1: "\<And>x e s U. ball x e \<subseteq> s \<inter> interior U \<longleftrightarrow> ball x e \<subseteq> s \<inter> U"
using interior_subset
by auto (meson Topology_Euclidean_Space.open_ball contra_subsetD interior_maximal mem_ball)
@@ -308,17 +309,14 @@
let ?z = "x - (e/2) *\<^sub>R k"
assume as: "x\<bullet>k = a\<bullet>k"
have "ball ?z (e / 2) \<inter> i = {}"
- apply (rule ccontr)
- unfolding ex_in_conv[symmetric]
- apply (erule exE)
- proof -
+ proof (clarsimp simp only: all_not_in_conv [symmetric])
fix y
- assume "y \<in> ball ?z (e / 2) \<inter> i"
- then have "dist ?z y < e/2" and yi:"y\<in>i" by auto
+ assume "y \<in> ball ?z (e / 2)" and yi: "y \<in> i"
+ then have "dist ?z y < e/2" by auto
then have "\<bar>(?z - y) \<bullet> k\<bar> < e/2"
using Basis_le_norm[OF k, of "?z - y"] unfolding dist_norm by auto
then have "y\<bullet>k < a\<bullet>k"
- using e[THEN conjunct1] k
+ using e k
by (auto simp add: field_simps abs_less_iff as inner_simps)
then have "y \<notin> i"
unfolding ab mem_box by (auto intro!: bexI[OF _ k])
@@ -337,10 +335,8 @@
done
also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2"
apply (rule add_strict_left_mono)
- using as
- unfolding mem_ball dist_norm
- using e
- apply (auto simp add: field_simps)
+ using as e
+ apply (auto simp add: field_simps dist_norm)
done
finally show "y \<in> ball x e"
unfolding mem_ball dist_norm using e by (auto simp add:field_simps)
@@ -354,19 +350,16 @@
let ?z = "x + (e/2) *\<^sub>R k"
assume as: "x\<bullet>k = b\<bullet>k"
have "ball ?z (e / 2) \<inter> i = {}"
- apply (rule ccontr)
- unfolding ex_in_conv[symmetric]
- apply (erule exE)
- proof -
+ proof (clarsimp simp only: all_not_in_conv [symmetric])
fix y
- assume "y \<in> ball ?z (e / 2) \<inter> i"
- then have "dist ?z y < e/2" and yi: "y \<in> i"
+ assume "y \<in> ball ?z (e / 2)" and yi: "y \<in> i"
+ then have "dist ?z y < e/2"
by auto
then have "\<bar>(?z - y) \<bullet> k\<bar> < e/2"
using Basis_le_norm[OF k, of "?z - y"]
unfolding dist_norm by auto
then have "y\<bullet>k > b\<bullet>k"
- using e[THEN conjunct1] k
+ using e k
by (auto simp add:field_simps inner_simps inner_Basis as)
then have "y \<notin> i"
unfolding ab mem_box by (auto intro!: bexI[OF _ k])
@@ -400,14 +393,14 @@
then obtain x where "ball x (e / 2) \<subseteq> s \<inter> \<Union>f" ..
then have "x \<in> s \<inter> interior (\<Union>f)"
unfolding lem1[where U="\<Union>f", symmetric]
- using centre_in_ball e[THEN conjunct1] by auto
+ using centre_in_ball e by auto
then show ?thesis
using insert.hyps(3) insert.prems(1) by blast
qed
qed
qed
qed
- from this[OF assms(1,3) goal1]
+ from this[OF assms(1,3)] x
obtain t x e where "t \<in> f" "0 < e" "ball x e \<subseteq> s \<inter> t"
by blast
then have "x \<in> s" "x \<in> interior t"
@@ -564,14 +557,15 @@
lemma content_pos_lt_eq:
"0 < content (cbox a (b::'a::euclidean_space)) \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
- apply rule
- defer
- apply (rule content_pos_lt, assumption)
-proof -
+proof (rule iffI)
assume "0 < content (cbox a b)"
then have "content (cbox a b) \<noteq> 0" by auto
then show "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
unfolding content_eq_0 not_ex not_le by fastforce
+next
+ assume "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
+ then show "0 < content (cbox a b)"
+ by (metis content_pos_lt)
qed
lemma content_empty [simp]: "content {} = 0"
@@ -593,22 +587,16 @@
have "cbox c d \<noteq> {}" using assms False by auto
then have cd_ne: "\<forall>i\<in>Basis. c \<bullet> i \<le> d \<bullet> i"
using assms unfolding box_ne_empty by auto
- show ?thesis
- unfolding content_def
- unfolding interval_bounds[OF ab_ne] interval_bounds[OF cd_ne]
- unfolding if_not_P[OF False] if_not_P[OF `cbox c d \<noteq> {}`]
- apply (rule setprod_mono)
- apply rule
- proof
- fix i :: 'a
- assume i: "i \<in> Basis"
- show "0 \<le> b \<bullet> i - a \<bullet> i"
- using ab_ne[THEN bspec, OF i] i by auto
- show "b \<bullet> i - a \<bullet> i \<le> d \<bullet> i - c \<bullet> i"
- using assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(2),of i]
- using assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(1),of i]
- using i by auto
- qed
+ have "\<And>i. i \<in> Basis \<Longrightarrow> 0 \<le> b \<bullet> i - a \<bullet> i"
+ using ab_ne by (metis diff_le_iff(1))
+ moreover
+ have "\<And>i. i \<in> Basis \<Longrightarrow> b \<bullet> i - a \<bullet> i \<le> d \<bullet> i - c \<bullet> i"
+ using assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(2)]
+ assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(1)]
+ by (metis diff_mono)
+ ultimately show ?thesis
+ unfolding content_def interval_bounds[OF ab_ne] interval_bounds[OF cd_ne]
+ by (simp add: setprod_mono if_not_P[OF False] if_not_P[OF `cbox c d \<noteq> {}`])
qed
lemma content_lt_nz: "0 < content (cbox a b) \<longleftrightarrow> content (cbox a b) \<noteq> 0"
@@ -1069,36 +1057,26 @@
qed
obtain q where q: "\<And>x. x \<in> p \<Longrightarrow> q x division_of cbox a b" "\<And>x. x \<in> p \<Longrightarrow> x \<in> q x"
using bchoice[OF *] by blast
- have "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
- apply rule
- apply (rule_tac p="q x" in division_of_subset)
- proof -
- fix x
+ { fix x
assume x: "x \<in> p"
- show "q x division_of \<Union>q x"
+ have "q x division_of \<Union>q x"
apply (rule division_ofI)
using division_ofD[OF q(1)[OF x]]
apply auto
- done
- show "q x - {x} \<subseteq> q x"
- by auto
- qed
+ done }
+ then have "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
+ by (meson Diff_subset division_of_subset)
then have "\<exists>d. d division_of \<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)"
apply -
- apply (rule elementary_inters)
- apply (rule finite_imageI[OF p(1)])
- unfolding image_is_empty
- apply (rule False)
- apply auto
+ apply (rule elementary_inters [OF finite_imageI[OF p(1)]])
+ apply (auto simp: False elementary_inters [OF finite_imageI[OF p(1)]])
done
then obtain d where d: "d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)" ..
- show ?thesis
- apply (rule that[of "d \<union> p"])
+ have "d \<union> p division_of cbox a b"
proof -
- 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
+ have te: "\<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
have *: "cbox a b = \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p) \<union> \<Union>p"
- apply (rule *[OF False])
- proof
+ proof (rule te[OF False], clarify)
fix i
assume i: "i \<in> p"
show "\<Union>(q i - {i}) \<union> i = cbox a b"
@@ -1135,7 +1113,9 @@
done
qed
qed
- qed auto
+ qed
+ then show ?thesis
+ by (meson Un_upper2 that)
qed
lemma elementary_bounded[dest]:
@@ -1938,11 +1918,7 @@
show "P s"
unfolding s
apply (rule as[rule_format])
- proof -
- case goal1
- then show ?case
- using s(2)[of i] using ab[OF `i \<in> Basis`] by auto
- qed
+ using ab s(2) by force
show "\<exists>a b. s = cbox a b"
unfolding s by auto
fix t
@@ -1959,17 +1935,8 @@
then obtain i where "c\<bullet>i \<noteq> e\<bullet>i \<or> d\<bullet>i \<noteq> f\<bullet>i" and i': "i \<in> Basis"
unfolding euclidean_eq_iff[where 'a='a] by auto
then have i: "c\<bullet>i \<noteq> e\<bullet>i" "d\<bullet>i \<noteq> f\<bullet>i"
- apply -
- apply(erule_tac[!] disjE)
- proof -
- assume "c\<bullet>i \<noteq> e\<bullet>i"
- then show "d\<bullet>i \<noteq> f\<bullet>i"
- using s(2)[OF i'] t(2)[OF i'] by fastforce
- next
- assume "d\<bullet>i \<noteq> f\<bullet>i"
- then show "c\<bullet>i \<noteq> e\<bullet>i"
- using s(2)[OF i'] t(2)[OF i'] by fastforce
- qed
+ using s(2) t(2) apply fastforce
+ using t(2)[OF i'] `c \<bullet> i \<noteq> e \<bullet> i \<or> d \<bullet> i \<noteq> f \<bullet> i` i' s(2) t(2) by fastforce
have *: "\<And>s t. (\<And>a. a \<in> s \<Longrightarrow> a \<in> t \<Longrightarrow> False) \<Longrightarrow> s \<inter> t = {}"
by auto
show "interior s \<inter> interior t = {}"
@@ -1979,16 +1946,9 @@
assume "x \<in> box c d" "x \<in> box e f"
then have x: "c\<bullet>i < d\<bullet>i" "e\<bullet>i < f\<bullet>i" "c\<bullet>i < f\<bullet>i" "e\<bullet>i < d\<bullet>i"
unfolding mem_box using i'
- apply -
- apply (erule_tac[!] x=i in ballE)+
- apply auto
- done
- show False
- using s(2)[OF i']
- apply -
- apply (erule_tac disjE)
- apply (erule_tac[!] conjE)
- proof -
+ by force+
+ show False using s(2)[OF i']
+ proof safe
assume as: "c \<bullet> i = a \<bullet> i" "d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2"
show False
using t(2)[OF i'] and i x unfolding as by (fastforce simp add:field_simps)
@@ -2007,7 +1967,8 @@
"x \<in> cbox c d"
"\<And>i. i \<in> Basis \<Longrightarrow>
c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
- c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i" by blast
+ c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i"
+ by blast
show "x\<in>cbox a b"
unfolding mem_box
proof safe
@@ -2056,7 +2017,7 @@
2 * (snd y\<bullet>i - fst y\<bullet>i) \<le> snd x\<bullet>i - fst x\<bullet>i))"
proof
case goal1
- then show ?case
+ show ?case
proof -
presume "\<not> P (cbox (fst x) (snd x)) \<Longrightarrow> ?thesis"
then show ?thesis by (cases "P (cbox (fst x) (snd x))") auto
@@ -2128,10 +2089,7 @@
obtain n where n: "(\<Sum>i\<in>Basis. b \<bullet> i - a \<bullet> i) / e < 2 ^ n"
using real_arch_pow2[of "(setsum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis) / e"] ..
show ?case
- apply (rule_tac x=n in exI)
- apply rule
- apply rule
- proof -
+ proof (rule exI [where x=n], clarify)
fix x y
assume xy: "x\<in>cbox (A n) (B n)" "y\<in>cbox (A n) (B n)"
have "dist x y \<le> setsum (\<lambda>i. abs((x - y)\<bullet>i)) Basis"
@@ -2189,25 +2147,20 @@
assume "e > 0"
from interv[OF this] obtain n
where n: "\<forall>x\<in>cbox (A n) (B n). \<forall>y\<in>cbox (A n) (B n). dist x y < e" ..
- show "\<exists>c d. x0 \<in> cbox c d \<and> cbox c d \<subseteq> ball x0 e \<and> cbox c d \<subseteq> cbox a b \<and> \<not> P (cbox c d)"
+ have "\<not> P (cbox (A n) (B n))"
+ apply (cases "0 < n")
+ using AB(3)[of "n - 1"] assms(3) AB(1-2)
+ apply auto
+ done
+ moreover have "cbox (A n) (B n) \<subseteq> ball x0 e"
+ using n using x0[of n] by auto
+ moreover have "cbox (A n) (B n) \<subseteq> cbox a b"
+ unfolding AB(1-2)[symmetric] by (rule ABsubset) auto
+ ultimately show "\<exists>c d. x0 \<in> cbox c d \<and> cbox c d \<subseteq> ball x0 e \<and> cbox c d \<subseteq> cbox a b \<and> \<not> P (cbox c d)"
apply (rule_tac x="A n" in exI)
apply (rule_tac x="B n" in exI)
- apply rule
- apply (rule x0)
- apply rule
- defer
- apply rule
- proof -
- show "\<not> P (cbox (A n) (B n))"
- apply (cases "0 < n")
- using AB(3)[of "n - 1"] assms(3) AB(1-2)
- apply auto
- done
- show "cbox (A n) (B n) \<subseteq> ball x0 e"
- using n using x0[of n] by auto
- show "cbox (A n) (B n) \<subseteq> cbox a b"
- unfolding AB(1-2)[symmetric] by (rule ABsubset) auto
- qed
+ apply (auto simp: x0)
+ done
qed
qed
@@ -2244,22 +2197,17 @@
assume "p tagged_division_of s" "g fine p" "p' tagged_division_of t" "g fine p'"
"interior s \<inter> interior t = {}"
then show "\<exists>p. p tagged_division_of s \<union> t \<and> g fine p"
- apply -
apply (rule_tac x="p \<union> p'" in exI)
- apply rule
- apply (rule tagged_division_union)
- prefer 4
- apply (rule fine_union)
- apply auto
+ apply (simp add: tagged_division_union fine_union)
done
qed blast
obtain e where e: "e > 0" "ball x e \<subseteq> g x"
using gaugeD[OF assms, of x] unfolding open_contains_ball by auto
- from x(2)[OF e(1)] obtain c d where c_d:
- "x \<in> cbox c d"
- "cbox c d \<subseteq> ball x e"
- "cbox c d \<subseteq> cbox a b"
- "\<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
+ from x(2)[OF e(1)]
+ obtain c d where c_d: "x \<in> cbox c d"
+ "cbox c d \<subseteq> ball x e"
+ "cbox c d \<subseteq> cbox a b"
+ "\<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
by blast
have "g fine {(x, cbox c d)}"
unfolding fine_def using e using c_d(2) by auto
@@ -2320,11 +2268,7 @@
{
presume "\<not> (\<exists>a b. i = cbox a b) \<Longrightarrow> False"
then show False
- apply -
- apply (cases "\<exists>a b. i = cbox a b")
- using assms
- apply (auto simp add:has_integral intro:lem[OF _ _ as])
- done
+ using as assms lem by blast
}
assume as: "\<not> (\<exists>a b. i = cbox a b)"
obtain B1 where B1:
@@ -2378,23 +2322,11 @@
have lem: "\<And>a b. \<And>f::'n \<Rightarrow> 'a.
(\<forall>x\<in>cbox a b. f(x) = 0) \<Longrightarrow> (f has_integral 0) (cbox a b)"
unfolding has_integral
- apply rule
- apply rule
- proof -
+ proof clarify
fix a b e
fix f :: "'n \<Rightarrow> 'a"
assume as: "\<forall>x\<in>cbox a b. f x = 0" "0 < (e::real)"
- show "\<exists>d. gauge d \<and>
- (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e)"
- apply (rule_tac x="\<lambda>x. ball x 1" in exI)
- apply rule
- apply (rule gaugeI)
- unfolding centre_in_ball
- defer
- apply (rule open_ball)
- apply rule
- apply rule
- apply (erule conjE)
+ have "\<And>p. p tagged_division_of cbox a b \<Longrightarrow> (\<lambda>x. ball x 1) fine p \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e"
proof -
case goal1
have "(\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) = 0"
@@ -2411,16 +2343,15 @@
qed
then show ?case
using as by auto
- qed auto
+ qed
+ then show "\<exists>d. gauge d \<and>
+ (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e)"
+ by auto
qed
{
presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis"
- then show ?thesis
- apply -
- apply (cases "\<exists>a b. s = cbox a b")
- using assms
- apply (auto simp add:has_integral intro: lem)
- done
+ with assms lem show ?thesis
+ by blast
}
have *: "(\<lambda>x. if x \<in> s then f x else 0) = (\<lambda>x. 0)"
apply (rule ext)
@@ -2429,26 +2360,8 @@
done
assume "\<not> (\<exists>a b. s = cbox a b)"
then show ?thesis
- apply (subst has_integral_alt)
- unfolding if_not_P *
- apply rule
- apply rule
- apply (rule_tac x=1 in exI)
- apply rule
- defer
- apply rule
- apply rule
- apply rule
- proof -
- fix e :: real
- fix a b
- assume "e > 0"
- then show "\<exists>z. ((\<lambda>x::'n. 0::'a) has_integral z) (cbox a b) \<and> norm (z - 0) < e"
- apply (rule_tac x=0 in exI)
- apply(rule,rule lem)
- apply auto
- done
- qed auto
+ using lem
+ by (subst has_integral_alt) (force simp add: *)
qed
lemma has_integral_0[simp]: "((\<lambda>x::'n::euclidean_space. 0) has_integral 0) s"
@@ -2469,20 +2382,17 @@
by blast
have lem: "\<And>(f :: 'n \<Rightarrow> 'a) y a b.
(f has_integral y) (cbox a b) \<Longrightarrow> ((h o f) has_integral h y) (cbox a b)"
- apply (subst has_integral)
- apply rule
- apply rule
- proof -
+ unfolding has_integral
+ proof clarify
case goal1
from pos_bounded
obtain B where B: "0 < B" "\<And>x. norm (h x) \<le> norm x * B"
by blast
have *: "e / B > 0" using goal1(2) B by simp
- obtain g where g:
- "gauge g"
- "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> g fine p \<Longrightarrow>
- norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - y) < e / B"
- by (rule has_integralD[OF goal1(1) *]) blast
+ obtain g where g: "gauge g"
+ "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> g fine p \<Longrightarrow>
+ norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - y) < e / B"
+ using "*" goal1(1) by auto
show ?case
apply (rule_tac x=g in exI)
apply rule
@@ -2511,19 +2421,11 @@
{
presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis"
then show ?thesis
- apply -
- apply (cases "\<exists>a b. s = cbox a b")
- using assms
- apply (auto simp add:has_integral intro!:lem)
- done
+ using assms(1) lem by blast
}
assume as: "\<not> (\<exists>a b. s = cbox a b)"
then show ?thesis
- apply (subst has_integral_alt)
- unfolding if_not_P
- apply rule
- apply rule
- proof -
+ proof (subst has_integral_alt, clarsimp)
fix e :: real
assume e: "e > 0"
have *: "0 < e/B" using e B(1) by simp
@@ -2534,34 +2436,18 @@
using has_integral_altD[OF assms(1) as *] by blast
show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
(\<exists>z. ((\<lambda>x. if x \<in> s then (h \<circ> f) x else 0) has_integral z) (cbox a b) \<and> norm (z - h y) < e)"
- apply (rule_tac x=M in exI)
- apply rule
- apply (rule M(1))
- apply rule
- apply rule
- apply rule
- proof -
+ proof (rule_tac x=M in exI, clarsimp simp add: M)
case goal1
obtain z where z:
"((\<lambda>x. if x \<in> s then f x else 0) has_integral z) (cbox a b)"
"norm (z - y) < e / B"
using M(2)[OF goal1(1)] by blast
have *: "(\<lambda>x. if x \<in> s then (h \<circ> f) x else 0) = h \<circ> (\<lambda>x. if x \<in> s then f x else 0)"
- unfolding o_def
- apply (rule ext)
- using zero
- apply auto
- done
+ using zero by auto
show ?case
apply (rule_tac x="h z" in exI)
- apply rule
- unfolding *
- apply (rule lem[OF z(1)])
- unfolding diff[symmetric]
- apply (rule le_less_trans[OF B(2)])
- using B(1) z(2)
- apply (auto simp add: field_simps)
- done
+ apply (simp add: "*" lem z(1))
+ by (metis B diff le_less_trans pos_less_divide_eq z(2))
qed
qed
qed
@@ -2577,9 +2463,7 @@
lemma has_integral_cmul: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s"
unfolding o_def[symmetric]
- apply (rule has_integral_linear,assumption)
- apply (rule bounded_linear_scaleR_right)
- done
+ by (metis has_integral_linear bounded_linear_scaleR_right)
lemma has_integral_cmult_real:
fixes c :: real
@@ -2595,9 +2479,7 @@
qed
lemma has_integral_neg: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral (-k)) s"
- apply (drule_tac c="-1" in has_integral_cmul)
- apply auto
- done
+ by (drule_tac c="-1" in has_integral_cmul) auto
lemma has_integral_add:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
@@ -2613,9 +2495,7 @@
case goal1
show ?case
unfolding has_integral
- apply rule
- apply rule
- proof -
+ proof clarify
fix e :: real
assume e: "e > 0"
then have *: "e/2 > 0"
@@ -2631,30 +2511,23 @@
norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - l) < e / 2"
using has_integralD[OF goal1(2) *] by blast
show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
- norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) < e)"
- apply (rule_tac x="\<lambda>x. (d1 x) \<inter> (d2 x)" in exI)
- apply rule
- apply (rule gauge_inter[OF d1(1) d2(1)])
- apply (rule,rule,erule conjE)
- proof -
+ norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) < e)"
+ proof (rule exI [where x="\<lambda>x. (d1 x) \<inter> (d2 x)"], clarsimp simp add: gauge_inter[OF d1(1) d2(1)])
fix p
assume as: "p tagged_division_of (cbox a b)" "(\<lambda>x. d1 x \<inter> d2 x) fine p"
have *: "(\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) =
(\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p. content k *\<^sub>R g x)"
unfolding scaleR_right_distrib setsum.distrib[of "\<lambda>(x,k). content k *\<^sub>R f x" "\<lambda>(x,k). content k *\<^sub>R g x" p,symmetric]
by (rule setsum.cong) auto
+ from as have fine: "d1 fine p" "d2 fine p"
+ unfolding fine_inter by auto
have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) =
- norm (((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k) + ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - l))"
+ norm (((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k) + ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - l))"
unfolding * by (auto simp add: algebra_simps)
- also
- let ?res = "\<dots>"
- from as have *: "d1 fine p" "d2 fine p"
- unfolding fine_inter by auto
- have "?res < e/2 + e/2"
+ also have "\<dots> < e/2 + e/2"
apply (rule le_less_trans[OF norm_triangle_ineq])
- apply (rule add_strict_mono)
- using d1(2)[OF as(1) *(1)] and d2(2)[OF as(1) *(2)]
- apply auto
+ using as d1 d2 fine
+ apply (blast intro: add_strict_mono)
done
finally show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) < e"
by auto
@@ -2664,19 +2537,11 @@
{
presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis"
then show ?thesis
- apply -
- apply (cases "\<exists>a b. s = cbox a b")
- using assms
- apply (auto simp add:has_integral intro!:lem)
- done
+ using assms lem by force
}
assume as: "\<not> (\<exists>a b. s = cbox a b)"
then show ?thesis
- apply (subst has_integral_alt)
- unfolding if_not_P
- apply rule
- apply rule
- proof -
+ proof (subst has_integral_alt, clarsimp)
case goal1
then have *: "e/2 > 0"
by auto
@@ -2693,14 +2558,7 @@
\<exists>z. ((\<lambda>x. if x \<in> s then g x else 0) has_integral z) (cbox a b) \<and> norm (z - l) < e / 2"
by blast
show ?case
- apply (rule_tac x="max B1 B2" in exI)
- apply rule
- apply (rule max.strict_coboundedI1)
- apply (rule B1)
- apply rule
- apply rule
- apply rule
- proof -
+ proof (rule_tac x="max B1 B2" in exI, clarsimp simp add: max.strict_coboundedI1 B1)
fix a b
assume "ball 0 (max B1 B2) \<subseteq> cbox a (b::'n)"
then have *: "ball 0 B1 \<subseteq> cbox a (b::'n)" "ball 0 B2 \<subseteq> cbox a (b::'n)"
@@ -2718,8 +2576,7 @@
by auto
show "\<exists>z. ((\<lambda>x. if x \<in> s then f x + g x else 0) has_integral z) (cbox a b) \<and> norm (z - (k + l)) < e"
apply (rule_tac x="w + z" in exI)
- apply rule
- apply (rule lem[OF w(1) z(1), unfolded *[symmetric]])
+ apply (simp add: lem[OF w(1) z(1), unfolded *[symmetric]])
using norm_triangle_ineq[of "w - k" "z - l"] w(2) z(2)
apply (auto simp add: field_simps)
done
@@ -2740,33 +2597,17 @@
lemma integral_add: "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow>
integral s (\<lambda>x. f x + g x) = integral s f + integral s g"
- apply (rule integral_unique)
- apply (drule integrable_integral)+
- apply (rule has_integral_add)
- apply assumption+
- done
+ by (rule integral_unique) (metis integrable_integral has_integral_add)
lemma integral_cmul: "f integrable_on s \<Longrightarrow> integral s (\<lambda>x. c *\<^sub>R f x) = c *\<^sub>R integral s f"
- apply (rule integral_unique)
- apply (drule integrable_integral)+
- apply (rule has_integral_cmul)
- apply assumption+
- done
+ by (rule integral_unique) (metis integrable_integral has_integral_cmul)
lemma integral_neg: "f integrable_on s \<Longrightarrow> integral s (\<lambda>x. - f x) = - integral s f"
- apply (rule integral_unique)
- apply (drule integrable_integral)+
- apply (rule has_integral_neg)
- apply assumption+
- done
+ by (rule integral_unique) (metis integrable_integral has_integral_neg)
lemma integral_sub: "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow>
integral s (\<lambda>x. f x - g x) = integral s f - integral s g"
- apply (rule integral_unique)
- apply (drule integrable_integral)+
- apply (rule has_integral_sub)
- apply assumption+
- done
+ by (rule integral_unique) (metis integrable_integral has_integral_sub)
lemma integrable_0: "(\<lambda>x. 0) integrable_on s"
unfolding integrable_on_def using has_integral_0 by auto
@@ -2797,13 +2638,8 @@
lemma integral_linear:
"f integrable_on s \<Longrightarrow> bounded_linear h \<Longrightarrow> integral s (h \<circ> f) = h (integral s f)"
- apply (rule has_integral_unique)
- defer
- unfolding has_integral_integral
- apply (drule (2) has_integral_linear)
- unfolding has_integral_integral[symmetric]
- apply (rule integrable_linear)
- apply assumption+
+ apply (rule has_integral_unique [where i=s and f = "h \<circ> f"])
+ apply (simp_all add: integrable_integral integrable_linear has_integral_linear )
done
lemma integral_component_eq[simp]:
@@ -2822,24 +2658,17 @@
then show ?case by auto
next
case (insert x F)
- show ?case
- unfolding setsum.insert[OF insert(1,3)]
- apply (rule has_integral_add)
- using insert assms
- apply auto
- done
-qed
-
-lemma integral_setsum: "finite t \<Longrightarrow> \<forall>a\<in>t. (f a) integrable_on s \<Longrightarrow>
- integral s (\<lambda>x. setsum (\<lambda>a. f a x) t) = setsum (\<lambda>a. integral s (f a)) t"
- apply (rule integral_unique)
- apply (rule has_integral_setsum)
- using integrable_integral
- apply auto
- done
+ with assms show ?case
+ by (simp add: has_integral_add)
+qed
+
+lemma integral_setsum:
+ "\<lbrakk>finite t; \<forall>a\<in>t. (f a) integrable_on s\<rbrakk> \<Longrightarrow>
+ integral s (\<lambda>x. setsum (\<lambda>a. f a x) t) = setsum (\<lambda>a. integral s (f a)) t"
+ by (auto intro: has_integral_setsum integrable_integral)
lemma integrable_setsum:
- "finite t \<Longrightarrow> \<forall>a \<in> t. (f a) integrable_on s \<Longrightarrow> (\<lambda>x. setsum (\<lambda>a. f a x) t) integrable_on s"
+ "\<lbrakk>finite t; \<forall>a\<in>t. (f a) integrable_on s\<rbrakk> \<Longrightarrow> (\<lambda>x. setsum (\<lambda>a. f a x) t) integrable_on s"
unfolding integrable_on_def
apply (drule bchoice)
using has_integral_setsum[of t]
@@ -2896,19 +2725,10 @@
by (metis assms box_real(2) has_integral_null)
lemma has_integral_null_eq[simp]: "content (cbox a b) = 0 \<Longrightarrow> (f has_integral i) (cbox a b) \<longleftrightarrow> i = 0"
- apply rule
- apply (rule has_integral_unique)
- apply assumption
- apply (drule (1) has_integral_null)
- apply (drule has_integral_null)
- apply auto
- done
+ by (auto simp add: has_integral_null dest!: integral_unique)
lemma integral_null[dest]: "content (cbox a b) = 0 \<Longrightarrow> integral (cbox a b) f = 0"
- apply (rule integral_unique)
- apply (drule has_integral_null)
- apply assumption
- done
+ by (metis has_integral_null integral_unique)
lemma integrable_on_null[dest]: "content (cbox a b) = 0 \<Longrightarrow> f integrable_on (cbox a b)"
unfolding integrable_on_def
@@ -2917,19 +2737,10 @@
done
lemma has_integral_empty[intro]: "(f has_integral 0) {}"
- unfolding empty_as_interval
- apply (rule has_integral_null)
- using content_empty
- unfolding empty_as_interval
- apply assumption
- done
+ by (simp add: has_integral_is_0)
lemma has_integral_empty_eq[simp]: "(f has_integral i) {} \<longleftrightarrow> i = 0"
- apply rule
- apply (rule has_integral_unique)
- apply assumption
- apply auto
- done
+ by (auto simp add: has_integral_empty has_integral_unique)
lemma integrable_on_empty[intro]: "f integrable_on {}"
unfolding integrable_on_def by auto
@@ -2993,17 +2804,10 @@
done
note d=this[rule_format]
show ?case
- apply (rule_tac x=d in exI)
- apply rule
- apply (rule d)
- apply rule
- apply rule
- apply rule
- apply (erule conjE)+
- proof -
+ proof (rule_tac x=d in exI, clarsimp simp: d)
fix p1 p2
assume as: "p1 tagged_division_of (cbox a b)" "d fine p1"
- "p2 tagged_division_of (cbox a b)" "d fine p2"
+ "p2 tagged_division_of (cbox a b)" "d fine p2"
show "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)) < e"
apply (rule dist_triangle_half_l[where y=y,unfolded dist_norm])
using d(2)[OF conjI[OF as(1-2)]] d(2)[OF conjI[OF as(3-4)]] .
--- a/src/HOL/UNITY/Comp/AllocBase.thy Wed Jun 10 18:48:48 2015 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Wed Jun 10 18:57:31 2015 +0200
@@ -5,7 +5,7 @@
section{*Common Declarations for Chandy and Charpentier's Allocator*}
-theory AllocBase imports "../UNITY_Main" begin
+theory AllocBase imports "../UNITY_Main" "~~/src/HOL/Library/Multiset_Order" begin
consts Nclients :: nat (*Number of clients*)
@@ -41,12 +41,19 @@
lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
by (induct l) (simp_all add: ac_simps)
+lemma subseteq_le_multiset: "A #<=# A + B"
+unfolding le_multiset_def apply (cases B; simp)
+apply (rule HOL.disjI1)
+apply (rule union_less_mono2[of "{#}" "_ + {#_#}" A, simplified])
+apply (simp add: less_multiset\<^sub>H\<^sub>O)
+done
+
lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"
apply (rule monoI)
apply (unfold prefix_def)
-apply (erule genPrefix.induct, auto)
+apply (erule genPrefix.induct, simp_all add: add_right_mono)
apply (erule order_trans)
-apply simp
+apply (simp add: less_eq_multiset_def subseteq_le_multiset)
done
(** setsum **)
--- a/src/HOL/UNITY/Follows.thy Wed Jun 10 18:48:48 2015 +0200
+++ b/src/HOL/UNITY/Follows.thy Wed Jun 10 18:57:31 2015 +0200
@@ -168,6 +168,19 @@
subsection{*Multiset union properties (with the multiset ordering)*}
+(*TODO: remove when multiset is of sort ord again*)
+instantiation multiset :: (order) ordered_ab_semigroup_add
+begin
+
+definition less_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+ "M' < M \<longleftrightarrow> M' #<# M"
+
+definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+ "(M'::'a multiset) \<le> M \<longleftrightarrow> M' #<=# M"
+
+instance
+ by default (auto simp add: less_eq_multiset_def less_multiset_def multiset_order.less_le_not_le add.commute multiset_order.add_right_mono)
+end
lemma increasing_union:
"[| F \<in> increasing f; F \<in> increasing g |]