# HG changeset patch # User wenzelm # Date 1467746601 -7200 # Node ID a528d24826c54e2b0f247b77fdb443ff21e66049 # Parent c22928719e198a58fd796f6b0aee6262119d9ed4# Parent ae07cd27ebf1886877b950315be77d1247613edd merged diff -r ae07cd27ebf1 -r a528d24826c5 NEWS --- 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 + #\# ~> \ + #\# ~> < + 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. diff -r ae07cd27ebf1 -r a528d24826c5 src/Doc/Locales/Examples3.thy --- 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 \ n" text \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.\ sublocale non_negative \ diff -r ae07cd27ebf1 -r a528d24826c5 src/HOL/Library/Multiset.thy --- 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 \ 'a multiset \ bool" (infix "#\#" 50) - where "M' #\# M \ (M', M) \ mult {(x', x). x' < x}" - -definition le_multiset :: "'a::order multiset \ 'a multiset \ bool" (infix "#\#" 50) - where "M' #\# M \ M' #\# M \ 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 \ 'a multiset \ bool" + where "M' < M \ (M', M) \ mult {(x', x). x' < x}" + +definition less_eq_multiset :: "'a multiset \ 'a multiset \ bool" + where "less_eq_multiset M' M \ M' < M \ M' = M" + +instance proof - - have irrefl: "\ M #\# M" for M :: "'a multiset" + have irrefl: "\ M < M" for M :: "'a multiset" proof - assume "M #\# M" + assume "M < M" then have MM: "(M, M) \ 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 #\# M \ M #\# N \ K #\# N" for K M N :: "'a multiset" + have trans: "K < M \ M < N \ 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 \ _) less_multiset" - by standard (auto simp add: le_multiset_def irrefl dest: trans) -qed \ \FIXME avoid junk stemming from type class interpretation\ - -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 \ \FIXME avoid junk stemming from type class interpretation\ + +lemma mset_le_irrefl [elim!]: fixes M :: "'a::order multiset" - shows "M #\# M \ R" + shows "M < M \ R" by simp @@ -2553,27 +2553,29 @@ apply (simp add: add.assoc) done -lemma union_less_mono2: "B #\# D \ C + B #\# C + (D::'a::order multiset)" +lemma union_le_mono2: "B < D \ 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 #\# D \ B + C #\# D + (C::'a::order multiset)" +lemma union_le_mono1: "B < D \ 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 #\# C \ B #\# D \ A + B #\# 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 \ B < D \ 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 \Termination proofs with multiset orders\ @@ -2767,17 +2769,17 @@ multiset_inter_assoc multiset_inter_left_commute -lemma mult_less_not_refl: "\ M #\# (M::'a::order multiset)" - by (fact multiset_order.less_irrefl) - -lemma mult_less_trans: "K #\# M \ M #\# N \ K #\# (N::'a::order multiset)" - by (fact multiset_order.less_trans) - -lemma mult_less_not_sym: "M #\# N \ \ N #\# (M::'a::order multiset)" - by (fact multiset_order.less_not_sym) - -lemma mult_less_asym: "M #\# N \ (\ P \ N #\# (M::'a::order multiset)) \ P" - by (fact multiset_order.less_asym) +lemma mset_le_not_refl: "\ M < (M::'a::order multiset)" + by (fact less_irrefl) + +lemma mset_le_trans: "K < M \ M < N \ K < (N::'a::order multiset)" + by (fact less_trans) + +lemma mset_le_not_sym: "M < N \ \ N < (M::'a::order multiset)" + by (fact less_not_sym) + +lemma mset_le_asym: "M < N \ (\ P \ N < (M::'a::order multiset)) \ P" + by (fact less_asym) declaration \ let @@ -2951,8 +2953,8 @@ qed text \ - 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 \"} + and @{term "op <"} (multiset order). \ text \Quickcheck generators\ diff -r ae07cd27ebf1 -r a528d24826c5 src/HOL/Library/Multiset_Order.thy --- 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: "\K M N :: 'a multiset. ?less K M \ ?less M N \ ?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 \The Dershowitz--Manna ordering:\ @@ -209,88 +209,88 @@ end lemma less_multiset_less_multiset\<^sub>H\<^sub>O: - "M #\# N \ less_multiset\<^sub>H\<^sub>O M N" + "M < N \ 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 #\# N \ (\y. count N y < count M y \ (\x. y < x \ count M x < count N x))" - by (auto simp: le_multiset_def less_multiset\<^sub>H\<^sub>O) + shows "M \ N \ (\y. count N y < count M y \ (\x. y < x \ 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 #\# 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 \ ('a :: order) multiset \ bool) - (less_multiset :: ('a :: order) multiset \ ('a :: order) multiset \ bool)" + (op \ :: ('a :: order) multiset \ ('a :: order) multiset \ bool) + (op < :: ('a :: order) multiset \ ('a :: order) multiset \ bool)" by unfold_locales lemma linorder_multiset: "class.linorder - (le_multiset :: ('a :: linorder) multiset \ ('a :: linorder) multiset \ bool) - (less_multiset :: ('a :: linorder) multiset \ ('a :: linorder) multiset \ bool)" - by unfold_locales (fastforce simp add: less_multiset\<^sub>H\<^sub>O le_multiset_def not_less_iff_gr_or_eq) + (op \ :: ('a :: linorder) multiset \ ('a :: linorder) multiset \ bool) + (op < :: ('a :: linorder) multiset \ ('a :: linorder) multiset \ 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 \ ('a :: linorder) multiset \ bool" - "less_multiset :: ('a :: linorder) multiset \ ('a :: linorder) multiset \ bool" + "op \ :: ('a :: linorder) multiset \ ('a :: linorder) multiset \ bool" + "op < :: ('a :: linorder) multiset \ ('a :: linorder) multiset \ bool" by (rule linorder_multiset) interpretation multiset_wellorder: wellorder - "le_multiset :: ('a :: wellorder) multiset \ ('a :: wellorder) multiset \ bool" - "less_multiset :: ('a :: wellorder) multiset \ ('a :: wellorder) multiset \ bool" + "op \ :: ('a :: wellorder) multiset \ ('a :: wellorder) multiset \ bool" + "op < :: ('a :: wellorder) multiset \ ('a :: wellorder) multiset \ 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 "\ M #\# N \ N #\# M" + shows "\ M \ N \ N \ 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 \# N \ M #\# N" - unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O + shows "M \# N \ M \ 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 #\# M + {#undefined#}" - unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O by simp + shows "{#} \ M" + by (simp add: subset_eq_imp_le_multiset) + +lemma less_eq_multiset_empty_right[simp]: + fixes M :: "('a :: linorder) multiset" + shows "M \ {#} \ \ M \ {#}" + by (metis less_eq_multiset_empty_left antisym) lemma le_multiset_empty_left[simp]: fixes M :: "('a :: linorder) multiset" - shows "{#} #\# M" - by (simp add: less_eq_imp_le_multiset) + shows "M \ {#} \ {#} < M" + by (simp add: less_multiset\<^sub>H\<^sub>O) lemma le_multiset_empty_right[simp]: fixes M :: "('a :: linorder) multiset" - shows "M \ {#} \ \ M #\# {#}" - by (metis le_multiset_empty_left multiset_order.antisym) - -lemma less_multiset_empty_left[simp]: - fixes M :: "('a :: linorder) multiset" - shows "M \ {#} \ {#} #\# M" - by (simp add: less_multiset\<^sub>H\<^sub>O) - -lemma less_multiset_empty_right[simp]: - fixes M :: "('a :: linorder) multiset" - shows "\ M #\# {#}" + shows "\ 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 #\# (M + N)" and - le_multiset_plus_right[simp]: "M #\# (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 \ (M + N)" and + less_eq_multiset_plus_right[simp]: "M \ (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 #\# M' + N \ M #\# M'" and - less_multiset_plus_plus_right_iff[simp]: "M + N #\# M + N' \ N #\# N'" + le_multiset_plus_plus_left_iff[simp]: "M + N < M' + N \ M < M'" and + le_multiset_plus_plus_right_iff[simp]: "M + N < M + N' \ N < N'" unfolding less_multiset\<^sub>H\<^sub>O by auto lemma add_eq_self_empty_iff: "M + N = M \ N = {#}" @@ -299,22 +299,22 @@ lemma fixes M N :: "('a :: linorder) multiset" shows - less_multiset_plus_left_nonempty[simp]: "M \ {#} \ N #\# M + N" and - less_multiset_plus_right_nonempty[simp]: "N \ {#} \ M #\# M + N" + le_multiset_plus_left_nonempty[simp]: "M \ {#} \ N < M + N" and + le_multiset_plus_right_nonempty[simp]: "N \ {#} \ 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: "(\y :: 'a :: linorder. y \# N \ (\x. x \# M \ x < y)) \ M #\# N" +lemma ex_gt_imp_less_multiset: "(\y :: 'a :: linorder. y \# N \ (\x. x \# M \ x < y)) \ 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: - "(\y :: 'a :: linorder. y \# M + N \ y \ x) \ count M x < count N x \ M #\# N" + +lemma ex_gt_count_imp_le_multiset: + "(\y :: 'a :: linorder. y \# M + N \ y \ x) \ count M x < count N x \ 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 \# M \ N #\# P \ M - P + N #\# M" - by (drule subset_mset.diff_add[symmetric]) (metis union_less_mono2) +lemma union_le_diff_plus: "P \# M \ N < P \ M - P + N < M" + by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2) end diff -r ae07cd27ebf1 -r a528d24826c5 src/HOL/Probability/Borel_Space.thy --- 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 "(\x. suminf (\i. f i x)) \ 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} \ 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 \ 'a::metric_space" + shows "Measurable.pred borel (isCont f)" +proof (subst measurable_cong) + let ?I = "\j. inverse(real (Suc j))" + show "isCont f x = (\i. \j. \y z. dist x y < ?I j \ dist x z < ?I j \ dist (f y) (f z) \ ?I i)" for x + unfolding continuous_at_eps_delta + proof safe + fix i assume "\e>0. \d>0. \y. dist y x < d \ dist (f y) (f x) < e" + moreover have "0 < ?I i / 2" + by simp + ultimately obtain d where d: "0 < d" "\y. dist x y < d \ 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 "\j. \y z. dist x y < ?I j \ dist x z < ?I j \ dist (f y) (f z) \ ?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) \ dist (f y) (f x) + dist (f z) (f x)" + by (rule dist_triangle2) + also have "\ < ?I i / 2 + ?I i / 2" + by (intro add_strict_mono d less_trans[OF _ j] *) + also have "\ \ ?I i" + by (simp add: field_simps of_nat_Suc) + finally show "dist (f y) (f z) \ ?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 "\i. \j. \y z. dist x y < ?I j \ dist x z < ?I j \ dist (f y) (f z) \ ?I i" + from this[THEN spec, of "Suc n"] + obtain j where j: "\y z. dist x y < ?I j \ dist x z < ?I j \ dist (f y) (f z) \ ?I (Suc n)" + by auto + + show "\d>0. \y. dist y x < d \ 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) \ ?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 \ 'a::metric_space" shows "{x. isCont f x} \ sets borel" -proof - - let ?I = "\j. inverse(real (Suc j))" - - { fix x - have "isCont f x = (\i. \j. \y z. dist x y < ?I j \ dist x z < ?I j \ dist (f y) (f z) \ ?I i)" - unfolding continuous_at_eps_delta - proof safe - fix i assume "\e>0. \d>0. \y. dist y x < d \ dist (f y) (f x) < e" - moreover have "0 < ?I i / 2" - by simp - ultimately obtain d where d: "0 < d" "\y. dist x y < d \ 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 "\j. \y z. dist x y < ?I j \ dist x z < ?I j \ dist (f y) (f z) \ ?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) \ dist (f y) (f x) + dist (f z) (f x)" - by (rule dist_triangle2) - also have "\ < ?I i / 2 + ?I i / 2" - by (intro add_strict_mono d less_trans[OF _ j] *) - also have "\ \ ?I i" - by (simp add: field_simps of_nat_Suc) - finally show "dist (f y) (f z) \ ?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 "\i. \j. \y z. dist x y < ?I j \ dist x z < ?I j \ dist (f y) (f z) \ ?I i" - from this[THEN spec, of "Suc n"] - obtain j where j: "\y z. dist x y < ?I j \ dist x z < ?I j \ dist (f y) (f z) \ ?I (Suc n)" - by auto - - show "\d>0. \y. dist y x < d \ 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) \ ?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 **: "\e y. open {x. dist x y < e}" - using open_ball by (simp_all add: ball_def dist_commute) - - have "{x\space borel. isCont f x} \ 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 \ '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" diff -r ae07cd27ebf1 -r a528d24826c5 src/HOL/Probability/Levy.thy --- 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 \ cdf M1 x) (at_right x)" - by (simp add: continuous_within) - from M2.cdf_is_right_cont [of x] have "(cdf M2 \ cdf M2 x) (at_right x)" - by (simp add: continuous_within) + let ?D = "\x. \cdf M1 x - cdf M2 x\" { fix \ :: real assume "\ > 0" - from \\ > 0\ \(cdf M1 \ 0) at_bot\ \(cdf M2 \ 0) at_bot\ - have "eventually (\y. \cdf M1 y\ < \ / 4 \ \cdf M2 y\ < \ / 4 \ y \ x) at_bot" - by (simp only: tendsto_iff dist_real_def diff_0_right eventually_conj eventually_le_at_bot) - then obtain M where "\y. y \ M \ \cdf M1 y\ < \ / 4" "\y. y \ M \ \cdf M2 y\ < \ / 4" "M \ x" + have "(?D \ 0) at_bot" + using \(cdf M1 \ 0) at_bot\ \(cdf M2 \ 0) at_bot\ by (intro tendsto_eq_intros) auto + then have "eventually (\y. ?D y < \ / 2 \ y \ x) at_bot" + using \\ > 0\ by (simp only: tendsto_iff dist_real_def diff_0_right eventually_conj eventually_le_at_bot abs_idempotent) + then obtain M where "\y. y \ M \ ?D y < \ / 2" "M \ 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 \ x" "\cdf M1 a\ < \ / 4" "\cdf M2 a\ < \ / 4" + "measure M1 {a} = 0" "measure M2 {a} = 0" "a < M" "a \ x" and 1: "?D a < \ / 2" by auto - from \\ > 0\ \(cdf M1 \ cdf M1 x) (at_right x)\ \(cdf M2 \ cdf M2 x) (at_right x)\ - have "eventually (\y. \cdf M1 y - cdf M1 x\ < \ / 4 \ \cdf M2 y - cdf M2 x\ < \ / 4 \ 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" "\y. x < y \ y < N \ \cdf M1 y - cdf M1 x\ < \ / 4" - "\y. x < y \ y < N \ \cdf M2 y - cdf M2 x\ < \ / 4" "\y. x < y \ y < N \ x < y" + have "(?D \ ?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 (\y. \?D y - ?D x\ < \ / 2) (at_right x)" + using \\ > 0\ by (simp only: tendsto_iff dist_real_def eventually_conj eventually_at_right_less) + then obtain N where "N > x" "\y. x < y \ y < N \ \?D y - ?D x\ < \ / 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" "\cdf M2 x - cdf M2 b\ < \ / 4" "\cdf M1 x - cdf M1 b\ < \ / 4" + "measure M1 {b} = 0" "measure M2 {b} = 0" and 2: "\?D b - ?D x\ < \ / 2" by (auto simp: abs_minus_commute) from \a \ x\ \x < b\ have "a < b" "a \ b" by auto from \char M1 = char M2\ - M1.Levy_Inversion [OF \a \ b\ \measure M1 {a} = 0\ \measure M1 {b} = 0\] + M1.Levy_Inversion [OF \a \ b\ \measure M1 {a} = 0\ \measure M1 {b} = 0\] M2.Levy_Inversion [OF \a \ b\ \measure M2 {a} = 0\ \measure M2 {b} = 0\] 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 \a < b\] M2.cdf_diff_eq [OF \a < b\] . - - 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 \a < b\, symmetric] M2.cdf_diff_eq [OF \a < b\, symmetric] by simp + then have "?D x = \(?D b - ?D x) - ?D a\" by simp - also have "\ \ abs (cdf M1 x - cdf M1 b) + abs (cdf M1 a)" - by (rule abs_triangle_ineq) - also have "\ \ \ / 4 + \ / 4" - by (intro add_mono less_imp_le \\cdf M1 a\ < \ / 4\ \\cdf M1 x - cdf M1 b\ < \ / 4\) - finally have 1: "abs (cdf M1 x - (cdf M1 b - cdf M1 a)) \ \ / 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 "\ \ abs (cdf M2 x - cdf M2 b) + abs (cdf M2 a)" - by (rule abs_triangle_ineq) - also have "\ \ \ / 4 + \ / 4" - by (intro add_mono less_imp_le \\cdf M2 x - cdf M2 b\ < \ / 4\ \\cdf M2 a\ < \ / 4\) - finally have 2: "abs (cdf M2 x - (cdf M2 b - cdf M2 a)) \ \ / 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 "\ \ 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 "\ \ \ / 2 + \ / 2" by (rule add_mono [OF 1 2]) - finally have "abs (cdf M1 x - cdf M2 x) \ \" by simp } + also have "\ \ \?D b - ?D x\ + \?D a\" + by (rule abs_triangle_ineq4) + also have "\ \ \ / 2 + \ / 2" + using 1 2 by (intro add_mono) auto + finally have "?D x \ \" by simp } then show "cdf M1 x = cdf M2 x" by (metis abs_le_zero_iff dense_ge eq_iff_diff_eq_0) qed diff -r ae07cd27ebf1 -r a528d24826c5 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- 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); diff -r ae07cd27ebf1 -r a528d24826c5 src/HOL/UNITY/Comp/AllocBase.thy --- 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 #\# 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) \ 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 **) diff -r ae07cd27ebf1 -r a528d24826c5 src/HOL/UNITY/Follows.thy --- 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\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::order multiset \ 'a multiset \ bool" where - "M' < M \ M' #\# M" - -definition less_eq_multiset :: "'a multiset \ 'a multiset \ bool" where - "(M'::'a multiset) \ M \ M' #\# 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 \ increasing f; F \ increasing g |] diff -r ae07cd27ebf1 -r a528d24826c5 src/Pure/Tools/ci_profile.scala --- 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")