--- a/NEWS Wed Nov 11 15:41:01 2015 +0100
+++ b/NEWS Wed Nov 11 16:39:23 2015 +0100
@@ -462,6 +462,10 @@
than the former separate constants, hence infix syntax (_ / _) is usually
not available during instantiation.
+* New cancellation simprocs for boolean algebras to cancel
+complementary terms for sup and inf. For example, "sup x (sup y (- x))"
+simplifies to "top". INCOMPATIBILITY.
+
* Library/Multiset:
- Renamed multiset inclusion operators:
< ~> <#
--- a/src/HOL/Algebra/Coset.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/Algebra/Coset.thy Wed Nov 11 16:39:23 2015 +0100
@@ -759,6 +759,9 @@
order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
where "order S = card (carrier S)"
+lemma (in monoid) order_gt_0_iff_finite: "0 < order G \<longleftrightarrow> finite (carrier G)"
+by(auto simp add: order_def card_gt_0_iff)
+
lemma (in group) rcosets_part_G:
assumes "subgroup H G"
shows "\<Union>(rcosets H) = carrier G"
--- a/src/HOL/Algebra/Group.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/Algebra/Group.thy Wed Nov 11 16:39:23 2015 +0100
@@ -44,6 +44,9 @@
in if z < 0 then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
end
+lemma int_pow_int: "x (^)\<^bsub>G\<^esub> (int n) = x (^)\<^bsub>G\<^esub> n"
+by(simp add: int_pow_def nat_pow_def)
+
locale monoid =
fixes G (structure)
assumes m_closed [intro, simp]:
@@ -187,6 +190,9 @@
with G show ?thesis by (simp del: r_one add: m_assoc Units_closed)
qed
+lemma (in monoid) carrier_not_empty: "carrier G \<noteq> {}"
+by auto
+
text \<open>Power\<close>
lemma (in monoid) nat_pow_closed [intro, simp]:
@@ -434,7 +440,16 @@
by (auto simp add: int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult )
qed
-
+lemma (in group) int_pow_diff:
+ "x \<in> carrier G \<Longrightarrow> x (^) (n - m :: int) = x (^) n \<otimes> inv (x (^) m)"
+by(simp only: diff_conv_add_uminus int_pow_mult int_pow_neg)
+
+lemma (in group) inj_on_multc: "c \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. x \<otimes> c) (carrier G)"
+by(simp add: inj_on_def)
+
+lemma (in group) inj_on_cmult: "c \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. c \<otimes> x) (carrier G)"
+by(simp add: inj_on_def)
+
subsection \<open>Subgroups\<close>
locale subgroup =
--- a/src/HOL/Complete_Lattices.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/Complete_Lattices.thy Wed Nov 11 16:39:23 2015 +0100
@@ -1346,6 +1346,8 @@
lemma Union_disjoint: "(\<Union>C \<inter> A = {}) \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = {})"
by (fact Sup_inf_eq_bot_iff)
+lemma SUP_UNION: "(SUP x:(UN y:A. g y). f x) = (SUP y:A. SUP x:g y. f x :: _ :: complete_lattice)"
+by(rule order_antisym)(blast intro: SUP_least SUP_upper2)+
subsection \<open>Injections and bijections\<close>
--- a/src/HOL/Fun.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/Fun.thy Wed Nov 11 16:39:23 2015 +0100
@@ -663,6 +663,8 @@
lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
by auto
+lemma fun_upd_eqD: "f(x := y) = g(x := z) \<Longrightarrow> y = z"
+by(simp add: fun_eq_iff split: split_if_asm)
subsection \<open>@{text override_on}\<close>
--- a/src/HOL/Lattices.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/Lattices.thy Wed Nov 11 16:39:23 2015 +0100
@@ -707,8 +707,44 @@
then show ?thesis by simp
qed
+lemma sup_cancel_left1: "sup (sup x a) (sup (- x) b) = top"
+by(simp add: inf_sup_aci sup_compl_top)
+
+lemma sup_cancel_left2: "sup (sup (- x) a) (sup x b) = top"
+by(simp add: inf_sup_aci sup_compl_top)
+
+lemma inf_cancel_left1: "inf (inf x a) (inf (- x) b) = bot"
+by(simp add: inf_sup_aci inf_compl_bot)
+
+lemma inf_cancel_left2: "inf (inf (- x) a) (inf x b) = bot"
+by(simp add: inf_sup_aci inf_compl_bot)
+
+declare inf_compl_bot [simp] sup_compl_top [simp]
+
+lemma sup_compl_top_left1 [simp]: "sup (- x) (sup x y) = top"
+by(simp add: sup_assoc[symmetric])
+
+lemma sup_compl_top_left2 [simp]: "sup x (sup (- x) y) = top"
+using sup_compl_top_left1[of "- x" y] by simp
+
+lemma inf_compl_bot_left1 [simp]: "inf (- x) (inf x y) = bot"
+by(simp add: inf_assoc[symmetric])
+
+lemma inf_compl_bot_left2 [simp]: "inf x (inf (- x) y) = bot"
+using inf_compl_bot_left1[of "- x" y] by simp
+
+lemma inf_compl_bot_right [simp]: "inf x (inf y (- x)) = bot"
+by(subst inf_left_commute) simp
+
end
+ML_file "Tools/boolean_algebra_cancel.ML"
+
+simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") =
+ {* fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_sup_conv *}
+
+simproc_setup boolean_algebra_cancel_inf ("inf a b::'a::boolean_algebra") =
+ {* fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_inf_conv *}
subsection \<open>@{text "min/max"} as special case of lattice\<close>
--- a/src/HOL/Library/Extended_Nat.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/Library/Extended_Nat.thy Wed Nov 11 16:39:23 2015 +0100
@@ -459,6 +459,10 @@
lemma enat_iless: "n < enat m \<Longrightarrow> \<exists>k. n = enat k"
by (cases n) simp_all
+lemma iadd_le_enat_iff:
+ "x + y \<le> enat n \<longleftrightarrow> (\<exists>y' x'. x = enat x' \<and> y = enat y' \<and> x' + y' \<le> n)"
+by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all
+
lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. enat k < Y j"
apply (induct_tac k)
apply (simp (no_asm) only: enat_0)
--- a/src/HOL/Library/Extended_Real.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/Library/Extended_Real.thy Wed Nov 11 16:39:23 2015 +0100
@@ -311,7 +311,6 @@
shows "a \<noteq> \<infinity> \<Longrightarrow> a \<noteq> -\<infinity> \<Longrightarrow> \<bar>a\<bar> \<noteq> \<infinity>"
by auto
-
subsubsection "Addition"
instantiation ereal :: "{one,comm_monoid_add,zero_neq_one}"
@@ -593,6 +592,11 @@
lemma abs_ereal_pos[simp]: "0 \<le> \<bar>x :: ereal\<bar>"
by (cases x) auto
+lemma ereal_abs_leI:
+ fixes x y :: ereal
+ shows "\<lbrakk> x \<le> y; -x \<le> y \<rbrakk> \<Longrightarrow> \<bar>x\<bar> \<le> y"
+by(cases x y rule: ereal2_cases)(simp_all)
+
lemma real_of_ereal_le_0[simp]: "real_of_ereal (x :: ereal) \<le> 0 \<longleftrightarrow> x \<le> 0 \<or> x = \<infinity>"
by (cases x) auto
@@ -877,6 +881,11 @@
end
+lemma [simp]:
+ shows ereal_1_times: "ereal 1 * x = x"
+ and times_ereal_1: "x * ereal 1 = x"
+by(simp_all add: one_ereal_def[symmetric])
+
lemma one_not_le_zero_ereal[simp]: "\<not> (1 \<le> (0::ereal))"
by (simp add: one_ereal_def zero_ereal_def)
@@ -1045,6 +1054,10 @@
apply (simp only: numeral_inc ereal_plus_1)
done
+lemma distrib_left_ereal_nn:
+ "c \<ge> 0 \<Longrightarrow> (x + y) * ereal c = x * ereal c + y * ereal c"
+by(cases x y rule: ereal2_cases)(simp_all add: ring_distribs)
+
lemma setsum_ereal_right_distrib:
fixes f :: "'a \<Rightarrow> ereal"
shows "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> r * setsum f A = (\<Sum>n\<in>A. r * f n)"
@@ -1054,6 +1067,10 @@
"(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> setsum f A * r = (\<Sum>n\<in>A. f n * r :: ereal)"
using setsum_ereal_right_distrib[of A f r] by (simp add: mult_ac)
+lemma setsum_left_distrib_ereal:
+ "c \<ge> 0 \<Longrightarrow> setsum f A * ereal c = (\<Sum>x\<in>A. f x * c :: ereal)"
+by(subst setsum_comp_morphism[where h="\<lambda>x. x * ereal c", symmetric])(simp_all add: distrib_left_ereal_nn)
+
lemma ereal_le_epsilon:
fixes x y :: ereal
assumes "\<forall>e. 0 < e \<longrightarrow> x \<le> y + e"
@@ -1384,6 +1401,26 @@
shows "x - y = \<infinity> \<longleftrightarrow> y = -\<infinity> \<or> x = \<infinity>"
by (cases x y rule: ereal2_cases) simp_all
+lemma ereal_diff_add_eq_diff_diff_swap:
+ fixes x y z :: ereal
+ shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x - (y + z) = x - y - z"
+by(cases x y z rule: ereal3_cases) simp_all
+
+lemma ereal_diff_add_assoc2:
+ fixes x y z :: ereal
+ shows "x + y - z = x - z + y"
+by(cases x y z rule: ereal3_cases) simp_all
+
+lemma ereal_add_uminus_conv_diff: fixes x y z :: ereal shows "- x + y = y - x"
+by(cases x y rule: ereal2_cases) simp_all
+
+lemma ereal_minus_diff_eq:
+ fixes x y :: ereal
+ shows "\<lbrakk> x = \<infinity> \<longrightarrow> y \<noteq> \<infinity>; x = -\<infinity> \<longrightarrow> y \<noteq> - \<infinity> \<rbrakk> \<Longrightarrow> - (x - y) = y - x"
+by(cases x y rule: ereal2_cases) simp_all
+
+lemma ediff_le_self [simp]: "x - y \<le> (x :: enat)"
+by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all
subsubsection \<open>Division\<close>
@@ -1451,6 +1488,9 @@
lemma ereal_inverse_nonneg_iff: "0 \<le> inverse (x :: ereal) \<longleftrightarrow> 0 \<le> x \<or> x = -\<infinity>"
by (cases x) auto
+lemma inverse_ereal_ge0I: "0 \<le> (x :: ereal) \<Longrightarrow> 0 \<le> inverse x"
+by(cases x) simp_all
+
lemma zero_le_divide_ereal[simp]:
fixes a :: ereal
assumes "0 \<le> a"
@@ -2191,6 +2231,9 @@
lemmas ereal_of_enat_pushin = ereal_of_enat_add ereal_of_enat_sub ereal_of_enat_mult
lemmas ereal_of_enat_pushout = ereal_of_enat_pushin[symmetric]
+lemma ereal_of_enat_nonneg: "ereal_of_enat n \<ge> 0"
+by(cases n) simp_all
+
lemma ereal_of_enat_Sup:
assumes "A \<noteq> {}" shows "ereal_of_enat (Sup A) = (SUP a : A. ereal_of_enat a)"
proof (intro antisym mono_Sup)
@@ -2808,6 +2851,10 @@
qed
qed
+lemma Sup_ereal_mult_left':
+ "\<lbrakk> Y \<noteq> {}; x \<ge> 0 \<rbrakk> \<Longrightarrow> ereal x * (SUP i:Y. f i) = (SUP i:Y. ereal x * f i)"
+by(subst (1 2) mult.commute)(rule Sup_ereal_mult_right')
+
lemma sup_continuous_add[order_continuous_intros]:
fixes f g :: "'a::complete_lattice \<Rightarrow> ereal"
assumes nn: "\<And>x. 0 \<le> f x" "\<And>x. 0 \<le> g x" and cont: "sup_continuous f" "sup_continuous g"
--- a/src/HOL/Library/Indicator_Function.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/Library/Indicator_Function.thy Wed Nov 11 16:39:23 2015 +0100
@@ -60,6 +60,9 @@
lemma indicator_image: "inj f \<Longrightarrow> indicator (f ` X) (f x) = (indicator X x::_::zero_neq_one)"
by (auto simp: indicator_def inj_on_def)
+lemma indicator_vimage: "indicator (f -` A) x = indicator A (f x)"
+by(auto split: split_indicator)
+
lemma
fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A"
shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)"
--- a/src/HOL/Lifting.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/Lifting.thy Wed Nov 11 16:39:23 2015 +0100
@@ -570,6 +570,12 @@
ML_file "Tools/Lifting/lifting_setup.ML"
ML_file "Tools/Lifting/lifting_def_code_dt.ML"
+lemma pred_prod_beta: "pred_prod P Q xy \<longleftrightarrow> P (fst xy) \<and> Q (snd xy)"
+by(cases xy) simp
+
+lemma pred_prod_split: "P (pred_prod Q R xy) \<longleftrightarrow> (\<forall>x y. xy = (x, y) \<longrightarrow> P (Q x \<and> R y))"
+by(cases xy) simp
+
hide_const (open) POS NEG
end
--- a/src/HOL/List.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/List.thy Wed Nov 11 16:39:23 2015 +0100
@@ -795,6 +795,8 @@
lemma inj_split_Cons: "inj_on (\<lambda>(xs, n). n#xs) X"
by (auto intro!: inj_onI)
+lemma inj_on_Cons1 [simp]: "inj_on (op # x) A"
+by(simp add: inj_on_def)
subsubsection \<open>@{const length}\<close>
@@ -2501,6 +2503,9 @@
apply (case_tac j, auto)
done
+lemma zip_replicate1: "zip (replicate n x) ys = map (Pair x) (take n ys)"
+by(induction ys arbitrary: n)(case_tac [2] n, simp_all)
+
lemma take_zip:
"take n (zip xs ys) = zip (take n xs) (take n ys)"
apply (induct n arbitrary: xs ys)
@@ -2718,6 +2723,20 @@
lemma list_all2_same: "list_all2 P xs xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x x)"
by(auto simp add: list_all2_conv_all_nth set_conv_nth)
+lemma zip_assoc:
+ "zip xs (zip ys zs) = map (\<lambda>((x, y), z). (x, y, z)) (zip (zip xs ys) zs)"
+by(rule list_all2_all_nthI[where P="op =", unfolded list.rel_eq]) simp_all
+
+lemma zip_commute: "zip xs ys = map (\<lambda>(x, y). (y, x)) (zip ys xs)"
+by(rule list_all2_all_nthI[where P="op =", unfolded list.rel_eq]) simp_all
+
+lemma zip_left_commute:
+ "zip xs (zip ys zs) = map (\<lambda>(y, (x, z)). (x, y, z)) (zip ys (zip xs zs))"
+by(rule list_all2_all_nthI[where P="op =", unfolded list.rel_eq]) simp_all
+
+lemma zip_replicate2: "zip xs (replicate n y) = map (\<lambda>x. (x, y)) (take n xs)"
+by(subst zip_commute)(simp add: zip_replicate1)
+
subsubsection \<open>@{const List.product} and @{const product_lists}\<close>
lemma set_product[simp]: "set (List.product xs ys) = set xs \<times> set ys"
--- a/src/HOL/Num.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/Num.thy Wed Nov 11 16:39:23 2015 +0100
@@ -174,6 +174,9 @@
using nat_of_num_pos [of n] nat_of_num_pos [of m]
by (auto simp add: less_eq_num_def less_num_def)
+lemma le_num_One_iff: "x \<le> num.One \<longleftrightarrow> x = num.One"
+by (simp add: antisym_conv)
+
text \<open>Rules using @{text One} and @{text inc} as constructors\<close>
lemma add_One: "x + One = inc x"
@@ -646,6 +649,26 @@
zero_less_numeral
not_numeral_less_zero
+lemma min_0_1 [simp]:
+ fixes min' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" defines "min' \<equiv> min" shows
+ "min' 0 1 = 0"
+ "min' 1 0 = 0"
+ "min' 0 (numeral x) = 0"
+ "min' (numeral x) 0 = 0"
+ "min' 1 (numeral x) = 1"
+ "min' (numeral x) 1 = 1"
+by(simp_all add: min'_def min_def le_num_One_iff)
+
+lemma max_0_1 [simp]:
+ fixes max' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" defines "max' \<equiv> max" shows
+ "max' 0 1 = 1"
+ "max' 1 0 = 1"
+ "max' 0 (numeral x) = numeral x"
+ "max' (numeral x) 0 = numeral x"
+ "max' 1 (numeral x) = numeral x"
+ "max' (numeral x) 1 = numeral x"
+by(simp_all add: max'_def max_def le_num_One_iff)
+
end
subsubsection \<open>
--- a/src/HOL/Option.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/Option.thy Wed Nov 11 16:39:23 2015 +0100
@@ -65,6 +65,12 @@
lemma rel_option_None2 [simp]: "rel_option P x None \<longleftrightarrow> x = None"
by (cases x) simp_all
+lemma option_rel_Some1: "rel_option A (Some x) y \<longleftrightarrow> (\<exists>y'. y = Some y' \<and> A x y')" (* Option *)
+by(cases y) simp_all
+
+lemma option_rel_Some2: "rel_option A x (Some y) \<longleftrightarrow> (\<exists>x'. x = Some x' \<and> A x' y)" (* Option *)
+by(cases x) simp_all
+
lemma rel_option_inf: "inf (rel_option A) (rel_option B) = rel_option (inf A B)"
(is "?lhs = ?rhs")
proof (rule antisym)
@@ -96,6 +102,9 @@
lemma map_option_is_None [iff]: "(map_option f opt = None) = (opt = None)"
by (simp add: map_option_case split add: option.split)
+lemma None_eq_map_option_iff [iff]: "None = map_option f x \<longleftrightarrow> x = None"
+by(cases x) simp_all
+
lemma map_option_eq_Some [iff]: "(map_option f xo = Some y) = (\<exists>z. xo = Some z \<and> f z = y)"
by (simp add: map_option_case split add: option.split)
@@ -106,19 +115,27 @@
lemma map_option_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> map_option f x = map_option g y"
by (cases x) auto
+lemma map_option_idI: "(\<And>y. y \<in> set_option x \<Longrightarrow> f y = y) \<Longrightarrow> map_option f x = x"
+by(cases x)(simp_all)
+
functor map_option: map_option
by (simp_all add: option.map_comp fun_eq_iff option.map_id)
lemma case_map_option [simp]: "case_option g h (map_option f x) = case_option g (h \<circ> f) x"
by (cases x) simp_all
+lemma None_notin_image_Some [simp]: "None \<notin> Some ` A"
+by auto
+
+lemma notin_range_Some: "x \<notin> range Some \<longleftrightarrow> x = None"
+by(cases x) auto
+
lemma rel_option_iff:
"rel_option R x y = (case (x, y) of (None, None) \<Rightarrow> True
| (Some x, Some y) \<Rightarrow> R x y
| _ \<Rightarrow> False)"
by (auto split: prod.split option.split)
-
context
begin
@@ -183,6 +200,9 @@
lemma bind_eq_Some_conv: "bind f g = Some x \<longleftrightarrow> (\<exists>y. f = Some y \<and> g y = Some x)"
by (cases f) simp_all
+lemma bind_eq_None_conv: "Option.bind a f = None \<longleftrightarrow> a = None \<or> f (the a) = None"
+by(cases a) simp_all
+
lemma map_option_bind: "map_option f (bind x g) = bind x (map_option f \<circ> g)"
by (cases x) simp_all
@@ -197,6 +217,15 @@
lemma bind_option_cong_code: "x = y \<Longrightarrow> bind x f = bind y f"
by simp
+lemma bind_map_option: "bind (map_option f x) g = bind x (g \<circ> f)"
+by(cases x) simp_all
+
+lemma set_bind_option [simp]: "set_option (bind x f) = UNION (set_option x) (set_option \<circ> f)"
+by(cases x) auto
+
+lemma map_conv_bind_option: "map_option f x = Option.bind x (Some \<circ> f)"
+by(cases x) simp_all
+
end
setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm bind_option_cong_code})\<close>
--- a/src/HOL/Orderings.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/Orderings.thy Wed Nov 11 16:39:23 2015 +0100
@@ -256,7 +256,6 @@
unfolding Least_def by (rule theI2)
(blast intro: assms antisym)+
-
text \<open>Dual order\<close>
lemma dual_order:
@@ -1171,6 +1170,10 @@
lemma max_absorb1: "(y::'a::order) \<le> x \<Longrightarrow> max x y = x"
by (simp add: max_def)
+lemma max_min_same [simp]:
+ fixes x y :: "'a :: linorder"
+ shows "max x (min x y) = x" "max (min x y) x = x" "max (min x y) y = y" "max y (min x y) = y"
+by(auto simp add: max_def min_def)
subsection \<open>(Unique) top and bottom elements\<close>
--- a/src/HOL/Probability/Giry_Monad.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy Wed Nov 11 16:39:23 2015 +0100
@@ -1567,4 +1567,8 @@
by (rule measure_eqI)
(auto simp: indicator_inter_arith_ereal emeasure_density split: split_indicator)
+lemma null_measure_in_space_subprob_algebra [simp]:
+ "null_measure M \<in> space (subprob_algebra M) \<longleftrightarrow> space M \<noteq> {}"
+by(simp add: space_subprob_algebra subprob_space_null_measure_iff)
+
end
--- a/src/HOL/Probability/Measure_Space.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/Probability/Measure_Space.thy Wed Nov 11 16:39:23 2015 +0100
@@ -1421,6 +1421,9 @@
using emeasure_nonneg[of M A]
by (cases "emeasure M A") (auto simp: measure_def)
+lemma max_0_ereal_measure [simp]: "max 0 (ereal (measure M X)) = ereal (measure M X)"
+by(simp add: max_def measure_nonneg)
+
lemma measure_Union:
assumes finite: "emeasure M A \<noteq> \<infinity>" "emeasure M B \<noteq> \<infinity>"
and measurable: "A \<in> sets M" "B \<in> sets M" "A \<inter> B = {}"
@@ -2100,6 +2103,59 @@
lemma measure_null_measure[simp]: "measure (null_measure M) X = 0"
by (simp add: measure_def)
+lemma null_measure_idem [simp]: "null_measure (null_measure M) = null_measure M"
+by(rule measure_eqI) simp_all
+
+subsection \<open>Scaling a measure\<close>
+
+definition scale_measure :: "real \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
+where "scale_measure r M = measure_of (space M) (sets M) (\<lambda>A. (max 0 r) * emeasure M A)"
+
+lemma space_scale_measure: "space (scale_measure r M) = space M"
+by(simp add: scale_measure_def)
+
+lemma sets_scale_measure [simp, measurable_cong]: "sets (scale_measure r M) = sets M"
+by(simp add: scale_measure_def)
+
+lemma emeasure_scale_measure [simp]:
+ "emeasure (scale_measure r M) A = max 0 r * emeasure M A"
+ (is "_ = ?\<mu> A")
+proof(cases "A \<in> sets M")
+ case True
+ show ?thesis unfolding scale_measure_def
+ proof(rule emeasure_measure_of_sigma)
+ show "sigma_algebra (space M) (sets M)" ..
+ show "positive (sets M) ?\<mu>" by(simp add: positive_def emeasure_nonneg)
+ show "countably_additive (sets M) ?\<mu>"
+ proof (rule countably_additiveI)
+ fix A :: "nat \<Rightarrow> _" assume *: "range A \<subseteq> sets M" "disjoint_family A"
+ have "(\<Sum>i. ?\<mu> (A i)) = max 0 (ereal r) * (\<Sum>i. emeasure M (A i))"
+ by(rule suminf_cmult_ereal)(simp_all add: emeasure_nonneg)
+ also have "\<dots> = ?\<mu> (\<Union>i. A i)" using * by(simp add: suminf_emeasure)
+ finally show "(\<Sum>i. ?\<mu> (A i)) = ?\<mu> (\<Union>i. A i)" .
+ qed
+ qed(fact True)
+qed(simp add: emeasure_notin_sets)
+
+lemma measure_scale_measure [simp]: "measure (scale_measure r M) A = max 0 r * measure M A"
+by(simp add: measure_def max_def)
+
+lemma scale_measure_1 [simp]: "scale_measure 1 M = M"
+by(rule measure_eqI)(simp_all add: max_def)
+
+lemma scale_measure_le_0: "r \<le> 0 \<Longrightarrow> scale_measure r M = null_measure M"
+by(rule measure_eqI)(simp_all add: max_def)
+
+lemma scale_measure_0 [simp]: "scale_measure 0 M = null_measure M"
+by(simp add: scale_measure_le_0)
+
+lemma scale_scale_measure [simp]:
+ "scale_measure r (scale_measure r' M) = scale_measure (max 0 r * max 0 r') M"
+by(rule measure_eqI)(simp_all add: max_def mult.assoc times_ereal.simps(1)[symmetric] del: times_ereal.simps(1))
+
+lemma scale_null_measure [simp]: "scale_measure r (null_measure M) = null_measure M"
+by(rule measure_eqI) simp_all
+
subsection \<open>Measures form a chain-complete partial order\<close>
instantiation measure :: (type) order_bot
@@ -2270,4 +2326,16 @@
qed
end
+lemma
+ assumes A: "Complete_Partial_Order.chain op \<le> (f ` A)" and a: "a \<in> A" "f a \<noteq> bot"
+ shows space_SUP: "space (SUP M:A. f M) = space (f a)"
+ and sets_SUP: "sets (SUP M:A. f M) = sets (f a)"
+unfolding SUP_def by(rule space_Sup[OF A a(2) imageI[OF a(1)]] sets_Sup[OF A a(2) imageI[OF a(1)]])+
+
+lemma emeasure_SUP:
+ assumes A: "Complete_Partial_Order.chain op \<le> (f ` A)" "A \<noteq> {}"
+ assumes "X \<in> sets (SUP M:A. f M)"
+ shows "emeasure (SUP M:A. f M) X = (SUP M:A. emeasure (f M)) X"
+using \<open>X \<in> _\<close> unfolding SUP_def by(subst emeasure_Sup[OF A(1)]; simp add: A)
+
end
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Wed Nov 11 16:39:23 2015 +0100
@@ -1161,13 +1161,8 @@
unfolding mult.commute[of _ c] nn_integral_cmult[OF assms] by simp
lemma nn_integral_divide:
- "0 < c \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> (\<integral>\<^sup>+x. f x / c \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M) / c"
- unfolding divide_ereal_def
- apply (rule nn_integral_multc)
- apply assumption
- apply (cases c)
- apply auto
- done
+ "\<lbrakk> 0 \<le> c; f \<in> borel_measurable M \<rbrakk> \<Longrightarrow> (\<integral>\<^sup>+ x. f x / c \<partial>M) = (\<integral>\<^sup>+ x. f x \<partial>M) / c"
+by(simp add: divide_ereal_def nn_integral_multc inverse_ereal_ge0I)
lemma nn_integral_indicator[simp]:
"A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+ x. indicator A x\<partial>M) = (emeasure M) A"
@@ -2715,4 +2710,41 @@
"finite A \<Longrightarrow> X \<subseteq> A \<Longrightarrow> measure (uniform_count_measure A) X = card X / card A"
by (simp add: emeasure_point_measure_finite uniform_count_measure_def measure_def)
+lemma space_uniform_count_measure_empty_iff [simp]:
+ "space (uniform_count_measure X) = {} \<longleftrightarrow> X = {}"
+by(simp add: space_uniform_count_measure)
+
+lemma sets_uniform_count_measure_eq_UNIV [simp]:
+ "sets (uniform_count_measure UNIV) = UNIV \<longleftrightarrow> True"
+ "UNIV = sets (uniform_count_measure UNIV) \<longleftrightarrow> True"
+by(simp_all add: sets_uniform_count_measure)
+
+subsubsection \<open>Scaled measure\<close>
+
+lemma nn_integral_scale_measure':
+ assumes f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x"
+ shows "nn_integral (scale_measure r M) f = max 0 r * nn_integral M f"
+ using f
+proof induction
+ case (cong f g)
+ thus ?case
+ by(simp add: cong.hyps space_scale_measure cong: nn_integral_cong_simp)
+next
+ case (mult f c)
+ thus ?case
+ by(simp add: nn_integral_cmult max_def mult.assoc mult.left_commute)
+next
+ case (add f g)
+ thus ?case
+ by(simp add: nn_integral_add ereal_right_distrib nn_integral_nonneg)
+next
+ case (seq U)
+ thus ?case
+ by(simp add: nn_integral_monotone_convergence_SUP SUP_ereal_mult_left nn_integral_nonneg)
+qed simp
+
+lemma nn_integral_scale_measure:
+ "f \<in> borel_measurable M \<Longrightarrow> nn_integral (scale_measure r M) f = max 0 r * nn_integral M f"
+by(subst (1 2) nn_integral_max_0[symmetric])(rule nn_integral_scale_measure', simp_all)
+
end
--- a/src/HOL/Probability/Probability_Mass_Function.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Wed Nov 11 16:39:23 2015 +0100
@@ -144,6 +144,9 @@
lemma space_measure_pmf[simp]: "space (measure_pmf p) = UNIV"
using sets_eq_imp_space_eq[of "measure_pmf p" "count_space UNIV"] by simp
+lemma measure_pmf_UNIV [simp]: "measure (measure_pmf p) UNIV = 1"
+using measure_pmf.prob_space[of p] by simp
+
lemma measure_pmf_in_subprob_algebra[measurable (raw)]: "measure_pmf x \<in> space (subprob_algebra (count_space UNIV))"
by (simp add: space_subprob_algebra subprob_space_measure_pmf)
@@ -198,6 +201,9 @@
using AE_measure_singleton[of M] AE_measure_pmf[of M]
by (auto simp: set_pmf.rep_eq)
+lemma AE_pmfI: "(\<And>y. y \<in> set_pmf M \<Longrightarrow> P y) \<Longrightarrow> almost_everywhere (measure_pmf M) P"
+by(simp add: AE_measure_pmf_iff)
+
lemma countable_set_pmf [simp]: "countable (set_pmf p)"
by transfer (metis prob_space.finite_measure finite_measure.countable_support)
@@ -487,6 +493,9 @@
lemma emeasure_map_pmf[simp]: "emeasure (map_pmf f M) X = emeasure M (f -` X)"
unfolding map_pmf_rep_eq by (subst emeasure_distr) auto
+lemma measure_map_pmf[simp]: "measure (map_pmf f M) X = measure M (f -` X)"
+using emeasure_map_pmf[of f M X] by(simp add: measure_pmf.emeasure_eq_measure)
+
lemma nn_integral_map_pmf[simp]: "(\<integral>\<^sup>+x. f x \<partial>map_pmf g M) = (\<integral>\<^sup>+x. f (g x) \<partial>M)"
unfolding map_pmf_rep_eq by (intro nn_integral_distr) auto
@@ -810,6 +819,67 @@
end
+lemma pair_return_pmf1: "pair_pmf (return_pmf x) y = map_pmf (Pair x) y"
+by(simp add: pair_pmf_def bind_return_pmf map_pmf_def)
+
+lemma pair_return_pmf2: "pair_pmf x (return_pmf y) = map_pmf (\<lambda>x. (x, y)) x"
+by(simp add: pair_pmf_def bind_return_pmf map_pmf_def)
+
+lemma pair_pair_pmf: "pair_pmf (pair_pmf u v) w = map_pmf (\<lambda>(x, (y, z)). ((x, y), z)) (pair_pmf u (pair_pmf v w))"
+by(simp add: pair_pmf_def bind_return_pmf map_pmf_def bind_assoc_pmf)
+
+lemma pair_commute_pmf: "pair_pmf x y = map_pmf (\<lambda>(x, y). (y, x)) (pair_pmf y x)"
+unfolding pair_pmf_def by(subst bind_commute_pmf)(simp add: map_pmf_def bind_assoc_pmf bind_return_pmf)
+
+lemma set_pmf_subset_singleton: "set_pmf p \<subseteq> {x} \<longleftrightarrow> p = return_pmf x"
+proof(intro iffI pmf_eqI)
+ fix i
+ assume x: "set_pmf p \<subseteq> {x}"
+ hence *: "set_pmf p = {x}" using set_pmf_not_empty[of p] by auto
+ have "ereal (pmf p x) = \<integral>\<^sup>+ i. indicator {x} i \<partial>p" by(simp add: emeasure_pmf_single)
+ also have "\<dots> = \<integral>\<^sup>+ i. 1 \<partial>p" by(rule nn_integral_cong_AE)(simp add: AE_measure_pmf_iff * )
+ also have "\<dots> = 1" by simp
+ finally show "pmf p i = pmf (return_pmf x) i" using x
+ by(auto split: split_indicator simp add: pmf_eq_0_set_pmf)
+qed auto
+
+lemma bind_eq_return_pmf:
+ "bind_pmf p f = return_pmf x \<longleftrightarrow> (\<forall>y\<in>set_pmf p. f y = return_pmf x)"
+ (is "?lhs \<longleftrightarrow> ?rhs")
+proof(intro iffI strip)
+ fix y
+ assume y: "y \<in> set_pmf p"
+ assume "?lhs"
+ hence "set_pmf (bind_pmf p f) = {x}" by simp
+ hence "(\<Union>y\<in>set_pmf p. set_pmf (f y)) = {x}" by simp
+ hence "set_pmf (f y) \<subseteq> {x}" using y by auto
+ thus "f y = return_pmf x" by(simp add: set_pmf_subset_singleton)
+next
+ assume *: ?rhs
+ show ?lhs
+ proof(rule pmf_eqI)
+ fix i
+ have "ereal (pmf (bind_pmf p f) i) = \<integral>\<^sup>+ y. ereal (pmf (f y) i) \<partial>p" by(simp add: ereal_pmf_bind)
+ also have "\<dots> = \<integral>\<^sup>+ y. ereal (pmf (return_pmf x) i) \<partial>p"
+ by(rule nn_integral_cong_AE)(simp add: AE_measure_pmf_iff * )
+ also have "\<dots> = ereal (pmf (return_pmf x) i)" by simp
+ finally show "pmf (bind_pmf p f) i = pmf (return_pmf x) i" by simp
+ qed
+qed
+
+lemma pmf_False_conv_True: "pmf p False = 1 - pmf p True"
+proof -
+ have "pmf p False + pmf p True = measure p {False} + measure p {True}"
+ by(simp add: measure_pmf_single)
+ also have "\<dots> = measure p ({False} \<union> {True})"
+ by(subst measure_pmf.finite_measure_Union) simp_all
+ also have "{False} \<union> {True} = space p" by auto
+ finally show ?thesis by simp
+qed
+
+lemma pmf_True_conv_False: "pmf p True = 1 - pmf p False"
+by(simp add: pmf_False_conv_True)
+
subsection \<open> Conditional Probabilities \<close>
lemma measure_pmf_zero_iff: "measure (measure_pmf p) s = 0 \<longleftrightarrow> set_pmf p \<inter> s = {}"
@@ -946,6 +1016,22 @@
finally show "measure p {x. R x y} = measure q {y. R x y}" .
qed
+lemma rel_pmf_measureD:
+ assumes "rel_pmf R p q"
+ shows "measure (measure_pmf p) A \<le> measure (measure_pmf q) {y. \<exists>x\<in>A. R x y}" (is "?lhs \<le> ?rhs")
+using assms
+proof cases
+ fix pq
+ assume R: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y"
+ and p[symmetric]: "map_pmf fst pq = p"
+ and q[symmetric]: "map_pmf snd pq = q"
+ have "?lhs = measure (measure_pmf pq) (fst -` A)" by(simp add: p)
+ also have "\<dots> \<le> measure (measure_pmf pq) {y. \<exists>x\<in>A. R x (snd y)}"
+ by(rule measure_pmf.finite_measure_mono_AE)(auto 4 3 simp add: AE_measure_pmf_iff dest: R)
+ also have "\<dots> = ?rhs" by(simp add: q)
+ finally show ?thesis .
+qed
+
lemma rel_pmf_iff_measure:
assumes "symp R" "transp R"
shows "rel_pmf R p q \<longleftrightarrow>
@@ -1092,6 +1178,9 @@
qed
qed (fact natLeq_card_order natLeq_cinfinite)+
+lemma map_pmf_idI: "(\<And>x. x \<in> set_pmf p \<Longrightarrow> f x = x) \<Longrightarrow> map_pmf f p = p"
+by(simp cong: pmf.map_cong)
+
lemma rel_pmf_conj[simp]:
"rel_pmf (\<lambda>x y. P \<and> Q x y) x y \<longleftrightarrow> P \<and> rel_pmf Q x y"
"rel_pmf (\<lambda>x y. Q x y \<and> P) x y \<longleftrightarrow> P \<and> rel_pmf Q x y"
@@ -1190,6 +1279,31 @@
by (rule rel_pmf.intros[where pq="map_pmf (\<lambda>x. (x, x)) p"])
(auto simp add: pmf.map_comp o_def assms)
+lemma rel_pmf_bij_betw:
+ assumes f: "bij_betw f (set_pmf p) (set_pmf q)"
+ and eq: "\<And>x. x \<in> set_pmf p \<Longrightarrow> pmf p x = pmf q (f x)"
+ shows "rel_pmf (\<lambda>x y. f x = y) p q"
+proof(rule rel_pmf.intros)
+ let ?pq = "map_pmf (\<lambda>x. (x, f x)) p"
+ show "map_pmf fst ?pq = p" by(simp add: pmf.map_comp o_def)
+
+ have "map_pmf f p = q"
+ proof(rule pmf_eqI)
+ fix i
+ show "pmf (map_pmf f p) i = pmf q i"
+ proof(cases "i \<in> set_pmf q")
+ case True
+ with f obtain j where "i = f j" "j \<in> set_pmf p"
+ by(auto simp add: bij_betw_def image_iff)
+ thus ?thesis using f by(simp add: bij_betw_def pmf_map_inj eq)
+ next
+ case False thus ?thesis
+ by(subst pmf_map_outside)(auto simp add: set_pmf_iff eq[symmetric])
+ qed
+ qed
+ then show "map_pmf snd ?pq = q" by(simp add: pmf.map_comp o_def)
+qed auto
+
context
begin
@@ -1442,7 +1556,7 @@
lemma set_pmf_of_set[simp]: "set_pmf pmf_of_set = S"
using S_finite S_not_empty by (auto simp: set_pmf_iff)
-lemma emeasure_pmf_of_set[simp]: "emeasure pmf_of_set S = 1"
+lemma emeasure_pmf_of_set_space[simp]: "emeasure pmf_of_set S = 1"
by (rule measure_pmf.emeasure_eq_1_AE) (auto simp: AE_measure_pmf_iff)
lemma nn_integral_pmf_of_set':
@@ -1471,6 +1585,13 @@
apply(rule setsum.cong; simp_all)
done
+lemma emeasure_pmf_of_set:
+ "emeasure (measure_pmf pmf_of_set) A = card (S \<inter> A) / card S"
+apply(subst nn_integral_indicator[symmetric], simp)
+apply(subst nn_integral_pmf_of_set)
+apply(simp add: o_def max_def ereal_indicator[symmetric] S_not_empty S_finite real_of_nat_indicator[symmetric] of_nat_setsum[symmetric] setsum_indicator_eq_card del: of_nat_setsum)
+done
+
end
lemma pmf_of_set_singleton: "pmf_of_set {x} = return_pmf x"
@@ -1498,6 +1619,14 @@
lemma bernoulli_pmf_half_conv_pmf_of_set: "bernoulli_pmf (1 / 2) = pmf_of_set UNIV"
by(rule pmf_eqI) simp_all
+
+
+lemma measure_pmf_of_set:
+ assumes "S \<noteq> {}" "finite S"
+ shows "measure (measure_pmf (pmf_of_set S)) A = card (S \<inter> A) / card S"
+using emeasure_pmf_of_set[OF assms, of A]
+unfolding measure_pmf.emeasure_eq_measure by simp
+
subsubsection \<open> Poisson Distribution \<close>
context
@@ -1564,4 +1693,15 @@
lemma set_pmf_binomial[simp]: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (binomial_pmf n p) = {..n}"
by (simp add: set_pmf_binomial_eq)
+context begin interpretation lifting_syntax .
+
+lemma bind_pmf_parametric [transfer_rule]:
+ "(rel_pmf A ===> (A ===> rel_pmf B) ===> rel_pmf B) bind_pmf bind_pmf"
+by(blast intro: rel_pmf_bindI dest: rel_funD)
+
+lemma return_pmf_parametric [transfer_rule]: "(A ===> rel_pmf A) return_pmf return_pmf"
+by(rule rel_funI) simp
+
end
+
+end
--- a/src/HOL/Probability/Sigma_Algebra.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Wed Nov 11 16:39:23 2015 +0100
@@ -298,6 +298,10 @@
finally show ?thesis .
qed
+lemma (in sigma_algebra) countable_UN'':
+ "\<lbrakk> countable X; \<And>x y. x \<in> X \<Longrightarrow> A x \<in> M \<rbrakk> \<Longrightarrow> (\<Union>x\<in>X. A x) \<in> M"
+by(erule countable_UN')(auto)
+
lemma (in sigma_algebra) countable_INT [intro]:
fixes A :: "'i::countable \<Rightarrow> 'a set"
assumes A: "A`X \<subseteq> M" "X \<noteq> {}"
--- a/src/HOL/Product_Type.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/Product_Type.thy Wed Nov 11 16:39:23 2015 +0100
@@ -1144,6 +1144,9 @@
"Sigma (\<Union>X) B = (\<Union>A\<in>X. Sigma A B)"
by blast
+lemma Pair_vimage_Sigma: "Pair x -` Sigma A f = (if x \<in> A then f x else {})"
+ by auto
+
text \<open>
Non-dependent versions are needed to avoid the need for higher-order
matching, especially when the rules are re-oriented.
--- a/src/HOL/Relation.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/Relation.thy Wed Nov 11 16:39:23 2015 +0100
@@ -219,6 +219,9 @@
lemma reflp_equality [simp]: "reflp op ="
by(simp add: reflp_def)
+lemma reflp_mono: "\<lbrakk> reflp R; \<And>x y. R x y \<longrightarrow> Q x y \<rbrakk> \<Longrightarrow> reflp Q"
+by(auto intro: reflpI dest: reflpD)
+
subsubsection \<open>Irreflexivity\<close>
definition irrefl :: "'a rel \<Rightarrow> bool"
@@ -676,6 +679,8 @@
lemma eq_OO: "op= OO R = R"
by blast
+lemma OO_eq: "R OO op = = R"
+by blast
subsubsection \<open>Converse\<close>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/boolean_algebra_cancel.ML Wed Nov 11 16:39:23 2015 +0100
@@ -0,0 +1,81 @@
+(* Title: boolean_algebra_cancel.ML
+ Author: Andreas Lochbihler, ETH Zurich
+
+Simplification procedures for boolean algebras:
+- Cancel complementary terms sup and inf.
+*)
+
+signature BOOLEAN_ALGEBRA_CANCEL =
+sig
+ val cancel_sup_conv: conv
+ val cancel_inf_conv: conv
+end
+
+structure Boolean_Algebra_Cancel: BOOLEAN_ALGEBRA_CANCEL =
+struct
+val sup1 = @{lemma "(A::'a::semilattice_sup) == sup k a ==> sup A b == sup k (sup a b)"
+ by (simp only: ac_simps)}
+val sup2 = @{lemma "(B::'a::semilattice_sup) == sup k b ==> sup a B == sup k (sup a b)"
+ by (simp only: ac_simps)}
+val sup0 = @{lemma "(a::'a::bounded_semilattice_sup_bot) == sup a bot" by (simp)}
+
+val inf1 = @{lemma "(A::'a::semilattice_inf) == inf k a ==> inf A b == inf k (inf a b)"
+ by (simp only: ac_simps)}
+val inf2 = @{lemma "(B::'a::semilattice_inf) == inf k b ==> inf a B == inf k (inf a b)"
+ by (simp only: ac_simps)}
+val inf0 = @{lemma "(a::'a::bounded_semilattice_inf_top) == inf a top" by (simp)}
+
+fun move_to_front rule path = Conv.rewr_conv (Library.foldl (op RS) (rule, path))
+
+fun add_atoms sup pos path (t as Const (@{const_name Lattices.sup}, _) $ x $ y) =
+ if sup then
+ add_atoms sup pos (sup1::path) x #> add_atoms sup pos (sup2::path) y
+ else cons ((pos, t), path)
+ | add_atoms sup pos path (t as Const (@{const_name Lattices.inf}, _) $ x $ y) =
+ if not sup then
+ add_atoms sup pos (inf1::path) x #> add_atoms sup pos (inf2::path) y
+ else cons ((pos, t), path)
+ | add_atoms _ _ _ (Const (@{const_name Orderings.bot}, _)) = I
+ | add_atoms _ _ _ (Const (@{const_name Orderings.top}, _)) = I
+ | add_atoms _ pos path (Const (@{const_name Groups.uminus}, _) $ x) = cons ((not pos, x), path)
+ | add_atoms _ pos path x = cons ((pos, x), path);
+
+fun atoms sup pos t = add_atoms sup pos [] t []
+
+val coeff_ord = prod_ord bool_ord Term_Ord.term_ord
+
+fun find_common ord xs ys =
+ let
+ fun find (xs as (x, px)::xs') (ys as (y, py)::ys') =
+ (case ord (x, y) of
+ EQUAL => SOME (fst x, px, py)
+ | LESS => find xs' ys
+ | GREATER => find xs ys')
+ | find _ _ = NONE
+ fun ord' ((x, _), (y, _)) = ord (x, y)
+ in
+ find (sort ord' xs) (sort ord' ys)
+ end
+
+fun cancel_conv sup rule ct =
+ let
+ val rule0 = if sup then sup0 else inf0
+ fun cancel1_conv (pos, lpath, rpath) =
+ let
+ val lconv = move_to_front rule0 lpath
+ val rconv = move_to_front rule0 rpath
+ val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
+ in
+ conv1 then_conv Conv.rewr_conv (rule pos)
+ end
+ val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct)
+ val common = find_common coeff_ord (atoms sup true lhs) (atoms sup false rhs)
+ val conv =
+ case common of NONE => Conv.no_conv
+ | SOME x => cancel1_conv x
+ in conv ct end
+
+val cancel_sup_conv = cancel_conv true (fn pos => if pos then mk_meta_eq @{thm sup_cancel_left1} else mk_meta_eq @{thm sup_cancel_left2})
+val cancel_inf_conv = cancel_conv false (fn pos => if pos then mk_meta_eq @{thm inf_cancel_left1} else mk_meta_eq @{thm inf_cancel_left2})
+
+end
\ No newline at end of file
--- a/src/HOL/Transfer.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/Transfer.thy Wed Nov 11 16:39:23 2015 +0100
@@ -620,6 +620,10 @@
shows "((A ===> B ===> op =) ===> op =) right_unique right_unique"
unfolding right_unique_def[abs_def] by transfer_prover
+lemma map_fun_parametric [transfer_rule]:
+ "((A ===> B) ===> (C ===> D) ===> (B ===> C) ===> A ===> D) map_fun map_fun"
+unfolding map_fun_def[abs_def] by transfer_prover
+
end
end
--- a/src/HOL/UNITY/Detects.thy Wed Nov 11 15:41:01 2015 +0100
+++ b/src/HOL/UNITY/Detects.thy Wed Nov 11 16:39:23 2015 +0100
@@ -20,6 +20,7 @@
lemma Always_at_FP:
"[|F \<in> A LeadsTo B; all_total F|] ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
+supply [[simproc del: boolean_algebra_cancel_inf]] inf_compl_bot_right[simp del]
apply (rule LeadsTo_empty)
apply (subgoal_tac "F \<in> (FP F \<inter> A \<inter> - B) LeadsTo (B \<inter> (FP F \<inter> -B))")
apply (subgoal_tac [2] " (FP F \<inter> A \<inter> - B) = (A \<inter> (FP F \<inter> -B))")