--- a/NEWS Tue Jul 05 20:51:02 2016 +0200
+++ b/NEWS Tue Jul 05 21:23:21 2016 +0200
@@ -311,6 +311,43 @@
Some functions have been renamed:
ms_lesseq_impl -> subset_eq_mset_impl
+* Multisets are now ordered with the multiset ordering
+ #\<subseteq># ~> \<le>
+ #\<subset># ~> <
+ le_multiset ~> less_eq_multiset
+ less_multiset ~> le_multiset
+INCOMPATIBILITY
+
+* The prefix multiset_order has been discontinued: the theorems can be directly
+accessed.
+INCOMPATILBITY
+
+* Some theorems about the multiset ordering have been renamed:
+ le_multiset_def ~> less_eq_multiset_def
+ less_multiset_def ~> le_multiset_def
+ less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset
+ mult_less_not_refl ~> mset_le_not_refl
+ mult_less_trans ~> mset_le_trans
+ mult_less_not_sym ~> mset_le_not_sym
+ mult_less_asym ~> mset_le_asym
+ mult_less_irrefl ~> mset_le_irrefl
+ union_less_mono2{,1,2} ~> union_le_mono2{,1,2}
+
+ le_multiset\<^sub>H\<^sub>O ~> less_eq_multiset\<^sub>H\<^sub>O
+ le_multiset_total ~> less_eq_multiset_total
+ less_multiset_right_total ~> subset_eq_imp_le_multiset
+ le_multiset_empty_left ~> less_eq_multiset_empty_left
+ le_multiset_empty_right ~> less_eq_multiset_empty_right
+ less_multiset_empty_right ~> le_multiset_empty_left
+ less_multiset_empty_left ~> le_multiset_empty_right
+ union_less_diff_plus ~> union_le_diff_plus
+ ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset
+ less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty
+ le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty
+ less_multiset_plus_plus_left_iff ~> le_multiset_plus_plus_left_iff
+ less_multiset_plus_plus_right_iff ~> le_multiset_plus_plus_right_iff
+INCOMPATIBILITY
+
* Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
INCOMPATIBILITY.
--- a/src/Doc/Locales/Examples3.thy Tue Jul 05 20:51:02 2016 +0200
+++ b/src/Doc/Locales/Examples3.thy Tue Jul 05 21:23:21 2016 +0200
@@ -91,8 +91,8 @@
\begin{tabular}{l}
@{thm [source] int.less_def} from locale @{text partial_order}: \\
\quad @{thm int.less_def} \\
- @{thm [source] int.meet_left} from locale @{text lattice}: \\
- \quad @{thm int.meet_left} \\
+ @{thm [source] int.ex_sup} from locale @{text lattice}: \\
+ \quad @{thm int.ex_sup} \\
@{thm [source] int.join_distr} from locale @{text distrib_lattice}: \\
\quad @{thm int.join_distr} \\
@{thm [source] int.less_total} from locale @{text total_order}: \\
@@ -408,7 +408,7 @@
assumes non_neg: "0 \<le> n"
text \<open>It is again convenient to make the interpretation in an
- incremental fashion, first for order preserving maps, the for
+ incremental fashion, first for order preserving maps, then for
lattice endomorphisms.\<close>
sublocale non_negative \<subseteq>
--- a/src/HOL/Library/Multiset.thy Tue Jul 05 20:51:02 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Tue Jul 05 21:23:21 2016 +0200
@@ -2500,21 +2500,20 @@
ultimately show thesis by (auto intro: that)
qed
-definition less_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#\<subset>#" 50)
- where "M' #\<subset># M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
-
-definition le_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#\<subseteq>#" 50)
- where "M' #\<subseteq># M \<longleftrightarrow> M' #\<subset># M \<or> M' = M"
-
-notation (ASCII)
- less_multiset (infix "#<#" 50) and
- le_multiset (infix "#<=#" 50)
-
-interpretation multiset_order: order le_multiset less_multiset
+instantiation multiset :: (order) order
+begin
+
+definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
+ where "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
+
+definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
+ where "less_eq_multiset M' M \<longleftrightarrow> M' < M \<or> M' = M"
+
+instance
proof -
- have irrefl: "\<not> M #\<subset># M" for M :: "'a multiset"
+ have irrefl: "\<not> M < M" for M :: "'a multiset"
proof
- assume "M #\<subset># M"
+ assume "M < M"
then have MM: "(M, M) \<in> mult {(x, y). x < y}" by (simp add: less_multiset_def)
have "trans {(x'::'a, x). x' < x}"
by (rule transI) simp
@@ -2531,15 +2530,16 @@
by (induct rule: finite_induct) (auto intro: order_less_trans)
with * show False by simp
qed
- have trans: "K #\<subset># M \<Longrightarrow> M #\<subset># N \<Longrightarrow> K #\<subset># N" for K M N :: "'a multiset"
+ have trans: "K < M \<Longrightarrow> M < N \<Longrightarrow> K < N" for K M N :: "'a multiset"
unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
- show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset"
- by standard (auto simp add: le_multiset_def irrefl dest: trans)
-qed \<comment> \<open>FIXME avoid junk stemming from type class interpretation\<close>
-
-lemma mult_less_irrefl [elim!]:
+ show "OFCLASS('a multiset, order_class)"
+ by standard (auto simp add: less_eq_multiset_def irrefl dest: trans)
+qed
+end \<comment> \<open>FIXME avoid junk stemming from type class interpretation\<close>
+
+lemma mset_le_irrefl [elim!]:
fixes M :: "'a::order multiset"
- shows "M #\<subset># M \<Longrightarrow> R"
+ shows "M < M \<Longrightarrow> R"
by simp
@@ -2553,27 +2553,29 @@
apply (simp add: add.assoc)
done
-lemma union_less_mono2: "B #\<subset># D \<Longrightarrow> C + B #\<subset># C + (D::'a::order multiset)"
+lemma union_le_mono2: "B < D \<Longrightarrow> C + B < C + (D::'a::order multiset)"
apply (unfold less_multiset_def mult_def)
apply (erule trancl_induct)
apply (blast intro: mult1_union)
apply (blast intro: mult1_union trancl_trans)
done
-lemma union_less_mono1: "B #\<subset># D \<Longrightarrow> B + C #\<subset># D + (C::'a::order multiset)"
+lemma union_le_mono1: "B < D \<Longrightarrow> B + C < D + (C::'a::order multiset)"
apply (subst add.commute [of B C])
apply (subst add.commute [of D C])
-apply (erule union_less_mono2)
+apply (erule union_le_mono2)
done
lemma union_less_mono:
fixes A B C D :: "'a::order multiset"
- shows "A #\<subset># C \<Longrightarrow> B #\<subset># D \<Longrightarrow> A + B #\<subset># C + D"
- by (blast intro!: union_less_mono1 union_less_mono2 multiset_order.less_trans)
-
-interpretation multiset_order: ordered_ab_semigroup_add plus le_multiset less_multiset
- by standard (auto simp add: le_multiset_def intro: union_less_mono2)
-
+ shows "A < C \<Longrightarrow> B < D \<Longrightarrow> A + B < C + D"
+ by (blast intro!: union_le_mono1 union_le_mono2 less_trans)
+
+instantiation multiset :: (order) ordered_ab_semigroup_add
+begin
+instance
+ by standard (auto simp add: less_eq_multiset_def intro: union_le_mono2)
+end
subsubsection \<open>Termination proofs with multiset orders\<close>
@@ -2767,17 +2769,17 @@
multiset_inter_assoc
multiset_inter_left_commute
-lemma mult_less_not_refl: "\<not> M #\<subset># (M::'a::order multiset)"
- by (fact multiset_order.less_irrefl)
-
-lemma mult_less_trans: "K #\<subset># M \<Longrightarrow> M #\<subset># N \<Longrightarrow> K #\<subset># (N::'a::order multiset)"
- by (fact multiset_order.less_trans)
-
-lemma mult_less_not_sym: "M #\<subset># N \<Longrightarrow> \<not> N #\<subset># (M::'a::order multiset)"
- by (fact multiset_order.less_not_sym)
-
-lemma mult_less_asym: "M #\<subset># N \<Longrightarrow> (\<not> P \<Longrightarrow> N #\<subset># (M::'a::order multiset)) \<Longrightarrow> P"
- by (fact multiset_order.less_asym)
+lemma mset_le_not_refl: "\<not> M < (M::'a::order multiset)"
+ by (fact less_irrefl)
+
+lemma mset_le_trans: "K < M \<Longrightarrow> M < N \<Longrightarrow> K < (N::'a::order multiset)"
+ by (fact less_trans)
+
+lemma mset_le_not_sym: "M < N \<Longrightarrow> \<not> N < (M::'a::order multiset)"
+ by (fact less_not_sym)
+
+lemma mset_le_asym: "M < N \<Longrightarrow> (\<not> P \<Longrightarrow> N < (M::'a::order multiset)) \<Longrightarrow> P"
+ by (fact less_asym)
declaration \<open>
let
@@ -2951,8 +2953,8 @@
qed
text \<open>
- Exercise for the casual reader: add implementations for @{const le_multiset}
- and @{const less_multiset} (multiset order).
+ Exercise for the casual reader: add implementations for @{term "op \<le>"}
+ and @{term "op <"} (multiset order).
\<close>
text \<open>Quickcheck generators\<close>
--- a/src/HOL/Library/Multiset_Order.thy Tue Jul 05 20:51:02 2016 +0200
+++ b/src/HOL/Library/Multiset_Order.thy Tue Jul 05 21:23:21 2016 +0200
@@ -62,7 +62,7 @@
have trans: "\<And>K M N :: 'a multiset. ?less K M \<Longrightarrow> ?less M N \<Longrightarrow> ?less K N"
unfolding mult_def by (blast intro: trancl_trans)
show "class.order ?le ?less"
- by standard (auto simp add: le_multiset_def irrefl dest: trans)
+ by standard (auto simp add: less_eq_multiset_def irrefl dest: trans)
qed
text \<open>The Dershowitz--Manna ordering:\<close>
@@ -209,88 +209,88 @@
end
lemma less_multiset_less_multiset\<^sub>H\<^sub>O:
- "M #\<subset># N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
+ "M < N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def]
-lemma le_multiset\<^sub>H\<^sub>O:
+lemma less_eq_multiset\<^sub>H\<^sub>O:
fixes M N :: "('a :: linorder) multiset"
- shows "M #\<subseteq># N \<longleftrightarrow> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
- by (auto simp: le_multiset_def less_multiset\<^sub>H\<^sub>O)
+ shows "M \<le> N \<longleftrightarrow> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
+ by (auto simp: less_eq_multiset_def less_multiset\<^sub>H\<^sub>O)
-lemma wf_less_multiset: "wf {(M :: ('a :: wellorder) multiset, N). M #\<subset># N}"
+lemma wf_less_multiset: "wf {(M :: ('a :: wellorder) multiset, N). M < N}"
unfolding less_multiset_def by (auto intro: wf_mult wf)
lemma order_multiset: "class.order
- (le_multiset :: ('a :: order) multiset \<Rightarrow> ('a :: order) multiset \<Rightarrow> bool)
- (less_multiset :: ('a :: order) multiset \<Rightarrow> ('a :: order) multiset \<Rightarrow> bool)"
+ (op \<le> :: ('a :: order) multiset \<Rightarrow> ('a :: order) multiset \<Rightarrow> bool)
+ (op < :: ('a :: order) multiset \<Rightarrow> ('a :: order) multiset \<Rightarrow> bool)"
by unfold_locales
lemma linorder_multiset: "class.linorder
- (le_multiset :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool)
- (less_multiset :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool)"
- by unfold_locales (fastforce simp add: less_multiset\<^sub>H\<^sub>O le_multiset_def not_less_iff_gr_or_eq)
+ (op \<le> :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool)
+ (op < :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool)"
+ by unfold_locales (fastforce simp add: less_multiset\<^sub>H\<^sub>O less_eq_multiset_def not_less_iff_gr_or_eq)
interpretation multiset_linorder: linorder
- "le_multiset :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool"
- "less_multiset :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool"
+ "op \<le> :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool"
+ "op < :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool"
by (rule linorder_multiset)
interpretation multiset_wellorder: wellorder
- "le_multiset :: ('a :: wellorder) multiset \<Rightarrow> ('a :: wellorder) multiset \<Rightarrow> bool"
- "less_multiset :: ('a :: wellorder) multiset \<Rightarrow> ('a :: wellorder) multiset \<Rightarrow> bool"
+ "op \<le> :: ('a :: wellorder) multiset \<Rightarrow> ('a :: wellorder) multiset \<Rightarrow> bool"
+ "op < :: ('a :: wellorder) multiset \<Rightarrow> ('a :: wellorder) multiset \<Rightarrow> bool"
by unfold_locales (blast intro: wf_less_multiset [unfolded wf_def, simplified, rule_format])
-lemma le_multiset_total:
+lemma less_eq_multiset_total:
fixes M N :: "('a :: linorder) multiset"
- shows "\<not> M #\<subseteq># N \<Longrightarrow> N #\<subseteq># M"
+ shows "\<not> M \<le> N \<Longrightarrow> N \<le> M"
by (metis multiset_linorder.le_cases)
-lemma less_eq_imp_le_multiset:
+lemma subset_eq_imp_le_multiset:
fixes M N :: "('a :: linorder) multiset"
- shows "M \<le># N \<Longrightarrow> M #\<subseteq># N"
- unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O
+ shows "M \<le># N \<Longrightarrow> M \<le> N"
+ unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O
by (simp add: less_le_not_le subseteq_mset_def)
-lemma less_multiset_right_total:
+lemma le_multiset_right_total:
+ fixes M :: "('a :: linorder) multiset"
+ shows "M < M + {#undefined#}"
+ unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O by simp
+
+lemma less_eq_multiset_empty_left[simp]:
fixes M :: "('a :: linorder) multiset"
- shows "M #\<subset># M + {#undefined#}"
- unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O by simp
+ shows "{#} \<le> M"
+ by (simp add: subset_eq_imp_le_multiset)
+
+lemma less_eq_multiset_empty_right[simp]:
+ fixes M :: "('a :: linorder) multiset"
+ shows "M \<noteq> {#} \<Longrightarrow> \<not> M \<le> {#}"
+ by (metis less_eq_multiset_empty_left antisym)
lemma le_multiset_empty_left[simp]:
fixes M :: "('a :: linorder) multiset"
- shows "{#} #\<subseteq># M"
- by (simp add: less_eq_imp_le_multiset)
+ shows "M \<noteq> {#} \<Longrightarrow> {#} < M"
+ by (simp add: less_multiset\<^sub>H\<^sub>O)
lemma le_multiset_empty_right[simp]:
fixes M :: "('a :: linorder) multiset"
- shows "M \<noteq> {#} \<Longrightarrow> \<not> M #\<subseteq># {#}"
- by (metis le_multiset_empty_left multiset_order.antisym)
-
-lemma less_multiset_empty_left[simp]:
- fixes M :: "('a :: linorder) multiset"
- shows "M \<noteq> {#} \<Longrightarrow> {#} #\<subset># M"
- by (simp add: less_multiset\<^sub>H\<^sub>O)
-
-lemma less_multiset_empty_right[simp]:
- fixes M :: "('a :: linorder) multiset"
- shows "\<not> M #\<subset># {#}"
+ shows "\<not> M < {#}"
using subset_eq_empty less_multiset\<^sub>D\<^sub>M by blast
lemma
fixes M N :: "('a :: linorder) multiset"
shows
- le_multiset_plus_left[simp]: "N #\<subseteq># (M + N)" and
- le_multiset_plus_right[simp]: "M #\<subseteq># (M + N)"
- using [[metis_verbose = false]] by (metis less_eq_imp_le_multiset mset_subset_eq_add_left add.commute)+
+ less_eq_multiset_plus_left[simp]: "N \<le> (M + N)" and
+ less_eq_multiset_plus_right[simp]: "M \<le> (M + N)"
+ using [[metis_verbose = false]] by (metis subset_eq_imp_le_multiset mset_subset_eq_add_left add.commute)+
lemma
fixes M N :: "('a :: linorder) multiset"
shows
- less_multiset_plus_plus_left_iff[simp]: "M + N #\<subset># M' + N \<longleftrightarrow> M #\<subset># M'" and
- less_multiset_plus_plus_right_iff[simp]: "M + N #\<subset># M + N' \<longleftrightarrow> N #\<subset># N'"
+ le_multiset_plus_plus_left_iff[simp]: "M + N < M' + N \<longleftrightarrow> M < M'" and
+ le_multiset_plus_plus_right_iff[simp]: "M + N < M + N' \<longleftrightarrow> N < N'"
unfolding less_multiset\<^sub>H\<^sub>O by auto
lemma add_eq_self_empty_iff: "M + N = M \<longleftrightarrow> N = {#}"
@@ -299,22 +299,22 @@
lemma
fixes M N :: "('a :: linorder) multiset"
shows
- less_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N #\<subset># M + N" and
- less_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M #\<subset># M + N"
+ le_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N < M + N" and
+ le_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M < M + N"
using [[metis_verbose = false]]
- by (metis add.right_neutral less_multiset_empty_left less_multiset_plus_plus_right_iff
+ by (metis add.right_neutral le_multiset_empty_left le_multiset_plus_plus_right_iff
add.commute)+
-lemma ex_gt_imp_less_multiset: "(\<exists>y :: 'a :: linorder. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M #\<subset># N"
+lemma ex_gt_imp_less_multiset: "(\<exists>y :: 'a :: linorder. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M < N"
unfolding less_multiset\<^sub>H\<^sub>O
by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)
-
-lemma ex_gt_count_imp_less_multiset:
- "(\<forall>y :: 'a :: linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M #\<subset># N"
+
+lemma ex_gt_count_imp_le_multiset:
+ "(\<forall>y :: 'a :: linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M < N"
unfolding less_multiset\<^sub>H\<^sub>O
by (metis add_gr_0 count_union mem_Collect_eq not_gr0 not_le not_less_iff_gr_or_eq set_mset_def)
-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)
+lemma union_le_diff_plus: "P \<le># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
+ by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)
end
--- a/src/HOL/Probability/Borel_Space.thy Tue Jul 05 20:51:02 2016 +0200
+++ b/src/HOL/Probability/Borel_Space.thy Tue Jul 05 21:23:21 2016 +0200
@@ -1815,77 +1815,65 @@
shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M"
unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
+lemma Collect_closed_imp_pred_borel: "closed {x. P x} \<Longrightarrow> Measurable.pred borel P"
+ by (simp add: pred_def)
+
(* Proof by Jeremy Avigad and Luke Serafin *)
+lemma isCont_borel_pred[measurable]:
+ fixes f :: "'b::metric_space \<Rightarrow> 'a::metric_space"
+ shows "Measurable.pred borel (isCont f)"
+proof (subst measurable_cong)
+ let ?I = "\<lambda>j. inverse(real (Suc j))"
+ show "isCont f x = (\<forall>i. \<exists>j. \<forall>y z. dist x y < ?I j \<and> dist x z < ?I j \<longrightarrow> dist (f y) (f z) \<le> ?I i)" for x
+ unfolding continuous_at_eps_delta
+ proof safe
+ fix i assume "\<forall>e>0. \<exists>d>0. \<forall>y. dist y x < d \<longrightarrow> dist (f y) (f x) < e"
+ moreover have "0 < ?I i / 2"
+ by simp
+ ultimately obtain d where d: "0 < d" "\<And>y. dist x y < d \<Longrightarrow> dist (f y) (f x) < ?I i / 2"
+ by (metis dist_commute)
+ then obtain j where j: "?I j < d"
+ by (metis reals_Archimedean)
+
+ show "\<exists>j. \<forall>y z. dist x y < ?I j \<and> dist x z < ?I j \<longrightarrow> dist (f y) (f z) \<le> ?I i"
+ proof (safe intro!: exI[where x=j])
+ fix y z assume *: "dist x y < ?I j" "dist x z < ?I j"
+ have "dist (f y) (f z) \<le> dist (f y) (f x) + dist (f z) (f x)"
+ by (rule dist_triangle2)
+ also have "\<dots> < ?I i / 2 + ?I i / 2"
+ by (intro add_strict_mono d less_trans[OF _ j] *)
+ also have "\<dots> \<le> ?I i"
+ by (simp add: field_simps of_nat_Suc)
+ finally show "dist (f y) (f z) \<le> ?I i"
+ by simp
+ qed
+ next
+ fix e::real assume "0 < e"
+ then obtain n where n: "?I n < e"
+ by (metis reals_Archimedean)
+ assume "\<forall>i. \<exists>j. \<forall>y z. dist x y < ?I j \<and> dist x z < ?I j \<longrightarrow> dist (f y) (f z) \<le> ?I i"
+ from this[THEN spec, of "Suc n"]
+ obtain j where j: "\<And>y z. dist x y < ?I j \<Longrightarrow> dist x z < ?I j \<Longrightarrow> dist (f y) (f z) \<le> ?I (Suc n)"
+ by auto
+
+ show "\<exists>d>0. \<forall>y. dist y x < d \<longrightarrow> dist (f y) (f x) < e"
+ proof (safe intro!: exI[of _ "?I j"])
+ fix y assume "dist y x < ?I j"
+ then have "dist (f y) (f x) \<le> ?I (Suc n)"
+ by (intro j) (auto simp: dist_commute)
+ also have "?I (Suc n) < ?I n"
+ by simp
+ also note n
+ finally show "dist (f y) (f x) < e" .
+ qed simp
+ qed
+qed (intro pred_intros_countable closed_Collect_all closed_Collect_le open_Collect_less
+ Collect_closed_imp_pred_borel closed_Collect_imp open_Collect_conj continuous_intros)
+
lemma isCont_borel:
fixes f :: "'b::metric_space \<Rightarrow> 'a::metric_space"
shows "{x. isCont f x} \<in> sets borel"
-proof -
- let ?I = "\<lambda>j. inverse(real (Suc j))"
-
- { fix x
- have "isCont f x = (\<forall>i. \<exists>j. \<forall>y z. dist x y < ?I j \<and> dist x z < ?I j \<longrightarrow> dist (f y) (f z) \<le> ?I i)"
- unfolding continuous_at_eps_delta
- proof safe
- fix i assume "\<forall>e>0. \<exists>d>0. \<forall>y. dist y x < d \<longrightarrow> dist (f y) (f x) < e"
- moreover have "0 < ?I i / 2"
- by simp
- ultimately obtain d where d: "0 < d" "\<And>y. dist x y < d \<Longrightarrow> dist (f y) (f x) < ?I i / 2"
- by (metis dist_commute)
- then obtain j where j: "?I j < d"
- by (metis reals_Archimedean)
-
- show "\<exists>j. \<forall>y z. dist x y < ?I j \<and> dist x z < ?I j \<longrightarrow> dist (f y) (f z) \<le> ?I i"
- proof (safe intro!: exI[where x=j])
- fix y z assume *: "dist x y < ?I j" "dist x z < ?I j"
- have "dist (f y) (f z) \<le> dist (f y) (f x) + dist (f z) (f x)"
- by (rule dist_triangle2)
- also have "\<dots> < ?I i / 2 + ?I i / 2"
- by (intro add_strict_mono d less_trans[OF _ j] *)
- also have "\<dots> \<le> ?I i"
- by (simp add: field_simps of_nat_Suc)
- finally show "dist (f y) (f z) \<le> ?I i"
- by simp
- qed
- next
- fix e::real assume "0 < e"
- then obtain n where n: "?I n < e"
- by (metis reals_Archimedean)
- assume "\<forall>i. \<exists>j. \<forall>y z. dist x y < ?I j \<and> dist x z < ?I j \<longrightarrow> dist (f y) (f z) \<le> ?I i"
- from this[THEN spec, of "Suc n"]
- obtain j where j: "\<And>y z. dist x y < ?I j \<Longrightarrow> dist x z < ?I j \<Longrightarrow> dist (f y) (f z) \<le> ?I (Suc n)"
- by auto
-
- show "\<exists>d>0. \<forall>y. dist y x < d \<longrightarrow> dist (f y) (f x) < e"
- proof (safe intro!: exI[of _ "?I j"])
- fix y assume "dist y x < ?I j"
- then have "dist (f y) (f x) \<le> ?I (Suc n)"
- by (intro j) (auto simp: dist_commute)
- also have "?I (Suc n) < ?I n"
- by simp
- also note n
- finally show "dist (f y) (f x) < e" .
- qed simp
- qed }
- note * = this
-
- have **: "\<And>e y. open {x. dist x y < e}"
- using open_ball by (simp_all add: ball_def dist_commute)
-
- have "{x\<in>space borel. isCont f x} \<in> sets borel"
- unfolding *
- apply (intro sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex)
- apply (simp add: Collect_all_eq)
- apply (intro borel_closed closed_INT ballI closed_Collect_imp open_Collect_conj **)
- apply auto
- done
- then show ?thesis
- by simp
-qed
-
-lemma isCont_borel_pred[measurable]:
- fixes f :: "'b::metric_space \<Rightarrow> 'a::metric_space"
- shows "Measurable.pred borel (isCont f)"
- unfolding pred_def by (simp add: isCont_borel)
+ by simp
lemma is_real_interval:
assumes S: "is_interval S"
--- a/src/HOL/Probability/Levy.thy Tue Jul 05 20:51:02 2016 +0200
+++ b/src/HOL/Probability/Levy.thy Tue Jul 05 21:23:21 2016 +0200
@@ -219,64 +219,46 @@
have "cdf M1 = cdf M2"
proof (rule ext)
fix x
- from M1.cdf_is_right_cont [of x] have "(cdf M1 \<longlongrightarrow> cdf M1 x) (at_right x)"
- by (simp add: continuous_within)
- from M2.cdf_is_right_cont [of x] have "(cdf M2 \<longlongrightarrow> cdf M2 x) (at_right x)"
- by (simp add: continuous_within)
+ let ?D = "\<lambda>x. \<bar>cdf M1 x - cdf M2 x\<bar>"
{ fix \<epsilon> :: real
assume "\<epsilon> > 0"
- from \<open>\<epsilon> > 0\<close> \<open>(cdf M1 \<longlongrightarrow> 0) at_bot\<close> \<open>(cdf M2 \<longlongrightarrow> 0) at_bot\<close>
- have "eventually (\<lambda>y. \<bar>cdf M1 y\<bar> < \<epsilon> / 4 \<and> \<bar>cdf M2 y\<bar> < \<epsilon> / 4 \<and> y \<le> x) at_bot"
- by (simp only: tendsto_iff dist_real_def diff_0_right eventually_conj eventually_le_at_bot)
- then obtain M where "\<And>y. y \<le> M \<Longrightarrow> \<bar>cdf M1 y\<bar> < \<epsilon> / 4" "\<And>y. y \<le> M \<Longrightarrow> \<bar>cdf M2 y\<bar> < \<epsilon> / 4" "M \<le> x"
+ have "(?D \<longlongrightarrow> 0) at_bot"
+ using \<open>(cdf M1 \<longlongrightarrow> 0) at_bot\<close> \<open>(cdf M2 \<longlongrightarrow> 0) at_bot\<close> by (intro tendsto_eq_intros) auto
+ then have "eventually (\<lambda>y. ?D y < \<epsilon> / 2 \<and> y \<le> x) at_bot"
+ using \<open>\<epsilon> > 0\<close> by (simp only: tendsto_iff dist_real_def diff_0_right eventually_conj eventually_le_at_bot abs_idempotent)
+ then obtain M where "\<And>y. y \<le> M \<Longrightarrow> ?D y < \<epsilon> / 2" "M \<le> x"
unfolding eventually_at_bot_linorder by auto
with open_minus_countable[OF count, of "{..< M}"] obtain a where
- "measure M1 {a} = 0" "measure M2 {a} = 0" "a < M" "a \<le> x" "\<bar>cdf M1 a\<bar> < \<epsilon> / 4" "\<bar>cdf M2 a\<bar> < \<epsilon> / 4"
+ "measure M1 {a} = 0" "measure M2 {a} = 0" "a < M" "a \<le> x" and 1: "?D a < \<epsilon> / 2"
by auto
- from \<open>\<epsilon> > 0\<close> \<open>(cdf M1 \<longlongrightarrow> cdf M1 x) (at_right x)\<close> \<open>(cdf M2 \<longlongrightarrow> cdf M2 x) (at_right x)\<close>
- have "eventually (\<lambda>y. \<bar>cdf M1 y - cdf M1 x\<bar> < \<epsilon> / 4 \<and> \<bar>cdf M2 y - cdf M2 x\<bar> < \<epsilon> / 4 \<and> x < y) (at_right x)"
- by (simp only: tendsto_iff dist_real_def eventually_conj eventually_at_right_less)
- then obtain N where "N > x" "\<And>y. x < y \<Longrightarrow> y < N \<Longrightarrow> \<bar>cdf M1 y - cdf M1 x\<bar> < \<epsilon> / 4"
- "\<And>y. x < y \<Longrightarrow> y < N \<Longrightarrow> \<bar>cdf M2 y - cdf M2 x\<bar> < \<epsilon> / 4" "\<And>y. x < y \<Longrightarrow> y < N \<Longrightarrow> x < y"
+ have "(?D \<longlongrightarrow> ?D x) (at_right x)"
+ using M1.cdf_is_right_cont [of x] M2.cdf_is_right_cont [of x]
+ by (intro tendsto_intros) (auto simp add: continuous_within)
+ then have "eventually (\<lambda>y. \<bar>?D y - ?D x\<bar> < \<epsilon> / 2) (at_right x)"
+ using \<open>\<epsilon> > 0\<close> by (simp only: tendsto_iff dist_real_def eventually_conj eventually_at_right_less)
+ then obtain N where "N > x" "\<And>y. x < y \<Longrightarrow> y < N \<Longrightarrow> \<bar>?D y - ?D x\<bar> < \<epsilon> / 2"
by (auto simp add: eventually_at_right[OF less_add_one])
with open_minus_countable[OF count, of "{x <..< N}"] obtain b where "x < b" "b < N"
- "measure M1 {b} = 0" "measure M2 {b} = 0" "\<bar>cdf M2 x - cdf M2 b\<bar> < \<epsilon> / 4" "\<bar>cdf M1 x - cdf M1 b\<bar> < \<epsilon> / 4"
+ "measure M1 {b} = 0" "measure M2 {b} = 0" and 2: "\<bar>?D b - ?D x\<bar> < \<epsilon> / 2"
by (auto simp: abs_minus_commute)
from \<open>a \<le> x\<close> \<open>x < b\<close> have "a < b" "a \<le> b" by auto
from \<open>char M1 = char M2\<close>
- M1.Levy_Inversion [OF \<open>a \<le> b\<close> \<open>measure M1 {a} = 0\<close> \<open>measure M1 {b} = 0\<close>]
+ M1.Levy_Inversion [OF \<open>a \<le> b\<close> \<open>measure M1 {a} = 0\<close> \<open>measure M1 {b} = 0\<close>]
M2.Levy_Inversion [OF \<open>a \<le> b\<close> \<open>measure M2 {a} = 0\<close> \<open>measure M2 {b} = 0\<close>]
have "complex_of_real (measure M1 {a<..b}) = complex_of_real (measure M2 {a<..b})"
by (intro LIMSEQ_unique) auto
- then have "measure M1 {a<..b} = measure M2 {a<..b}" by auto
- then have *: "cdf M1 b - cdf M1 a = cdf M2 b - cdf M2 a"
- unfolding M1.cdf_diff_eq [OF \<open>a < b\<close>] M2.cdf_diff_eq [OF \<open>a < b\<close>] .
-
- have "abs (cdf M1 x - (cdf M1 b - cdf M1 a)) = abs (cdf M1 x - cdf M1 b + cdf M1 a)"
+ then have "?D a = ?D b"
+ unfolding of_real_eq_iff M1.cdf_diff_eq [OF \<open>a < b\<close>, symmetric] M2.cdf_diff_eq [OF \<open>a < b\<close>, symmetric] by simp
+ then have "?D x = \<bar>(?D b - ?D x) - ?D a\<bar>"
by simp
- also have "\<dots> \<le> abs (cdf M1 x - cdf M1 b) + abs (cdf M1 a)"
- by (rule abs_triangle_ineq)
- also have "\<dots> \<le> \<epsilon> / 4 + \<epsilon> / 4"
- by (intro add_mono less_imp_le \<open>\<bar>cdf M1 a\<bar> < \<epsilon> / 4\<close> \<open>\<bar>cdf M1 x - cdf M1 b\<bar> < \<epsilon> / 4\<close>)
- finally have 1: "abs (cdf M1 x - (cdf M1 b - cdf M1 a)) \<le> \<epsilon> / 2" by simp
-
- have "abs (cdf M2 x - (cdf M2 b - cdf M2 a)) = abs (cdf M2 x - cdf M2 b + cdf M2 a)"
- by simp
- also have "\<dots> \<le> abs (cdf M2 x - cdf M2 b) + abs (cdf M2 a)"
- by (rule abs_triangle_ineq)
- also have "\<dots> \<le> \<epsilon> / 4 + \<epsilon> / 4"
- by (intro add_mono less_imp_le \<open>\<bar>cdf M2 x - cdf M2 b\<bar> < \<epsilon> / 4\<close> \<open>\<bar>cdf M2 a\<bar> < \<epsilon> / 4\<close>)
- finally have 2: "abs (cdf M2 x - (cdf M2 b - cdf M2 a)) \<le> \<epsilon> / 2" by simp
-
- have "abs (cdf M1 x - cdf M2 x) = abs ((cdf M1 x - (cdf M1 b - cdf M1 a)) -
- (cdf M2 x - (cdf M2 b - cdf M2 a)))" by (subst *, simp)
- also have "\<dots> \<le> abs (cdf M1 x - (cdf M1 b - cdf M1 a)) +
- abs (cdf M2 x - (cdf M2 b - cdf M2 a))" by (rule abs_triangle_ineq4)
- also have "\<dots> \<le> \<epsilon> / 2 + \<epsilon> / 2" by (rule add_mono [OF 1 2])
- finally have "abs (cdf M1 x - cdf M2 x) \<le> \<epsilon>" by simp }
+ also have "\<dots> \<le> \<bar>?D b - ?D x\<bar> + \<bar>?D a\<bar>"
+ by (rule abs_triangle_ineq4)
+ also have "\<dots> \<le> \<epsilon> / 2 + \<epsilon> / 2"
+ using 1 2 by (intro add_mono) auto
+ finally have "?D x \<le> \<epsilon>" by simp }
then show "cdf M1 x = cdf M2 x"
by (metis abs_le_zero_iff dense_ge eq_iff_diff_eq_0)
qed
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Tue Jul 05 20:51:02 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Tue Jul 05 21:23:21 2016 +0200
@@ -1256,7 +1256,7 @@
let val T = fastype_of1 (bound_Ts, hd args) in
(case (Option.mapPartial (ctr_sugar_of lthy) (try (fst o dest_Type) T), T <> res_T) of
(SOME {selss, T = Type (_, Ts), ...}, true) =>
- (case const_of (fold (curry op @) selss []) fun_t of
+ (case const_of (flat selss) fun_t of
SOME sel =>
let
val args' = args |> map (typ_before explore params);
--- a/src/HOL/UNITY/Comp/AllocBase.thy Tue Jul 05 20:51:02 2016 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Tue Jul 05 21:23:21 2016 +0200
@@ -36,9 +36,9 @@
lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
by (fact mset_append)
-lemma subseteq_le_multiset: "A #\<subseteq># A + B"
-unfolding le_multiset_def apply (cases B; simp)
-apply (rule union_less_mono2[of "{#}" "_ + {#_#}" A, simplified])
+lemma subseteq_le_multiset: "(A :: 'a::order multiset) \<le> A + B"
+unfolding less_eq_multiset_def apply (cases B; simp)
+apply (rule union_le_mono2[of "{#}" "_ + {#_#}" A, simplified])
apply (simp add: less_multiset\<^sub>H\<^sub>O)
done
@@ -47,7 +47,7 @@
apply (unfold prefix_def)
apply (erule genPrefix.induct, simp_all add: add_right_mono)
apply (erule order_trans)
-apply (simp add: less_eq_multiset_def subseteq_le_multiset)
+apply (simp add: subseteq_le_multiset)
done
(** setsum **)
--- a/src/HOL/UNITY/Follows.thy Tue Jul 05 20:51:02 2016 +0200
+++ b/src/HOL/UNITY/Follows.thy Tue Jul 05 21:23:21 2016 +0200
@@ -175,19 +175,7 @@
subsection\<open>Multiset union properties (with the multiset ordering)\<close>
-(*TODO: remove when multiset is of sort ord again*)
-instantiation multiset :: (order) ordered_ab_semigroup_add
-begin
-definition less_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
- "M' < M \<longleftrightarrow> M' #\<subset># M"
-
-definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
- "(M'::'a multiset) \<le> M \<longleftrightarrow> M' #\<subseteq># M"
-
-instance
- by standard (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 |]
--- a/src/Pure/Tools/ci_profile.scala Tue Jul 05 20:51:02 2016 +0200
+++ b/src/Pure/Tools/ci_profile.scala Tue Jul 05 21:23:21 2016 +0200
@@ -19,10 +19,11 @@
println(name + "=" + Outer_Syntax.quote_string(value))
}
- private def build(options: Options): Build.Results =
+ private def build(options: Options): (Build.Results, Time) =
{
val progress = new Console_Progress(true)
- progress.interrupt_handler {
+ val start_time = Time.now()
+ val results = progress.interrupt_handler {
Build.build_selection(
options = options,
progress = progress,
@@ -34,6 +35,8 @@
system_mode = true,
selection = select_sessions _)
}
+ val end_time = Time.now()
+ (results, end_time - start_time)
}
private def load_properties(): JProperties =
@@ -85,14 +88,16 @@
println(s"Build for Isabelle id $isabelle_id")
pre_hook(args)
- val results = build(options)
+ val (results, elapsed_time) = build(options)
print_section("TIMING")
val groups = results.sessions.map(results.info).flatMap(_.groups)
for (group <- groups)
println(s"Group $group: " + compute_timing(results, Some(group)).message_resources)
- println("Overall: " + compute_timing(results, None).message_resources)
+
+ val total_timing = compute_timing(results, None).copy(elapsed = elapsed_time)
+ println("Overall: " + total_timing.message_resources)
if (!results.ok) {
print_section("FAILED SESSIONS")