add simp rules for enat and ereal
authornoschinl
Tue Dec 20 11:40:56 2011 +0100 (2011-12-20)
changeset 459349321cd2572fe
parent 45933 ee70da42e08a
child 45935 32f769f94ea4
add simp rules for enat and ereal
src/HOL/Library/Extended_Nat.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Probability/Probability_Measure.thy
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Mon Dec 19 14:41:08 2011 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Tue Dec 20 11:40:56 2011 +0100
     1.3 @@ -49,6 +49,9 @@
     1.4  
     1.5  declare [[coercion "enat::nat\<Rightarrow>enat"]]
     1.6  
     1.7 +lemmas enat2_cases = enat.exhaust[case_product enat.exhaust]
     1.8 +lemmas enat3_cases = enat.exhaust[case_product enat.exhaust enat.exhaust]
     1.9 +
    1.10  lemma not_infinity_eq [iff]: "(x \<noteq> \<infinity>) = (EX i. x = enat i)"
    1.11    by (cases x) auto
    1.12  
    1.13 @@ -165,9 +168,9 @@
    1.14  instance proof
    1.15    fix n m q :: enat
    1.16    show "n + m + q = n + (m + q)"
    1.17 -    by (cases n, auto, cases m, auto, cases q, auto)
    1.18 +    by (cases n m q rule: enat3_cases) auto
    1.19    show "n + m = m + n"
    1.20 -    by (cases n, auto, cases m, auto)
    1.21 +    by (cases n m rule: enat2_cases) auto
    1.22    show "0 + n = n"
    1.23      by (cases n) (simp_all add: zero_enat_def)
    1.24  qed
    1.25 @@ -341,6 +344,14 @@
    1.26    "(\<infinity>::enat) < q \<longleftrightarrow> False"
    1.27    by (simp_all add: less_eq_enat_def less_enat_def split: enat.splits)
    1.28  
    1.29 +lemma number_of_le_enat_iff[simp]:
    1.30 +  shows "number_of m \<le> enat n \<longleftrightarrow> number_of m \<le> n"
    1.31 +by (auto simp: number_of_enat_def)
    1.32 +
    1.33 +lemma number_of_less_enat_iff[simp]:
    1.34 +  shows "number_of m < enat n \<longleftrightarrow> number_of m < n"
    1.35 +by (auto simp: number_of_enat_def)
    1.36 +
    1.37  lemma enat_ord_code [code]:
    1.38    "enat m \<le> enat n \<longleftrightarrow> m \<le> n"
    1.39    "enat m < enat n \<longleftrightarrow> m < n"
     2.1 --- a/src/HOL/Library/Extended_Real.thy	Mon Dec 19 14:41:08 2011 +0100
     2.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue Dec 20 11:40:56 2011 +0100
     2.3 @@ -55,11 +55,7 @@
     2.4    instance ..
     2.5  end
     2.6  
     2.7 -definition "ereal_of_enat n = (case n of enat n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
     2.8 -
     2.9  declare [[coercion "ereal :: real \<Rightarrow> ereal"]]
    2.10 -declare [[coercion "ereal_of_enat :: enat \<Rightarrow> ereal"]]
    2.11 -declare [[coercion "(\<lambda>n. ereal (real n)) :: nat \<Rightarrow> ereal"]]
    2.12  
    2.13  lemma ereal_uminus_uminus[simp]:
    2.14    fixes a :: ereal shows "- (- a) = a"
    2.15 @@ -1068,6 +1064,28 @@
    2.16    qed (insert y, simp_all)
    2.17  qed simp
    2.18  
    2.19 +lemma ereal_divide_right_mono[simp]:
    2.20 +  fixes x y z :: ereal
    2.21 +  assumes "x \<le> y" "0 < z" shows "x / z \<le> y / z"
    2.22 +using assms by (cases x y z rule: ereal3_cases) (auto intro: divide_right_mono)
    2.23 +
    2.24 +lemma ereal_divide_left_mono[simp]:
    2.25 +  fixes x y z :: ereal
    2.26 +  assumes "y \<le> x" "0 < z" "0 < x * y"
    2.27 +  shows "z / x \<le> z / y"
    2.28 +using assms by (cases x y z rule: ereal3_cases)
    2.29 +  (auto intro: divide_left_mono simp: field_simps sign_simps split: split_if_asm)
    2.30 +
    2.31 +lemma ereal_divide_zero_left[simp]:
    2.32 +  fixes a :: ereal
    2.33 +  shows "0 / a = 0"
    2.34 +  by (cases a) (auto simp: zero_ereal_def)
    2.35 +
    2.36 +lemma ereal_times_divide_eq_left[simp]:
    2.37 +  fixes a b c :: ereal
    2.38 +  shows "b / c * a = b * a / c"
    2.39 +  by (cases a b c rule: ereal3_cases) (auto simp: field_simps sign_simps)
    2.40 +
    2.41  subsection "Complete lattice"
    2.42  
    2.43  instantiation ereal :: lattice
    2.44 @@ -1683,6 +1701,54 @@
    2.45    finally show ?thesis .
    2.46  qed
    2.47  
    2.48 +subsection "Relation to @{typ enat}"
    2.49 +
    2.50 +definition "ereal_of_enat n = (case n of enat n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
    2.51 +
    2.52 +declare [[coercion "ereal_of_enat :: enat \<Rightarrow> ereal"]]
    2.53 +declare [[coercion "(\<lambda>n. ereal (real n)) :: nat \<Rightarrow> ereal"]]
    2.54 +
    2.55 +lemma ereal_of_enat_simps[simp]:
    2.56 +  "ereal_of_enat (enat n) = ereal n"
    2.57 +  "ereal_of_enat \<infinity> = \<infinity>"
    2.58 +  by (simp_all add: ereal_of_enat_def)
    2.59 +
    2.60 +lemma ereal_of_enat_le_iff[simp]:
    2.61 +  "ereal_of_enat m \<le> ereal_of_enat n \<longleftrightarrow> m \<le> n"
    2.62 +by (cases m n rule: enat2_cases) auto
    2.63 +
    2.64 +lemma number_of_le_ereal_of_enat_iff[simp]:
    2.65 +  shows "number_of m \<le> ereal_of_enat n \<longleftrightarrow> number_of m \<le> n"
    2.66 +by (cases n) (auto dest: natceiling_le intro: natceiling_le_eq[THEN iffD1])
    2.67 +
    2.68 +lemma ereal_of_enat_ge_zero_cancel_iff[simp]:
    2.69 +  "0 \<le> ereal_of_enat n \<longleftrightarrow> 0 \<le> n"
    2.70 +by (cases n) (auto simp: enat_0[symmetric])
    2.71 +
    2.72 +lemma ereal_of_enat_gt_zero_cancel_iff[simp]:
    2.73 +  "0 < ereal_of_enat n \<longleftrightarrow> 0 < n"
    2.74 +by (cases n) (auto simp: enat_0[symmetric])
    2.75 +
    2.76 +lemma ereal_of_enat_zero[simp]:
    2.77 +  "ereal_of_enat 0 = 0"
    2.78 +by (auto simp: enat_0[symmetric])
    2.79 +
    2.80 +lemma ereal_of_enat_add:
    2.81 +  "ereal_of_enat (m + n) = ereal_of_enat m + ereal_of_enat n"
    2.82 +by (cases m n rule: enat2_cases) auto
    2.83 +
    2.84 +lemma ereal_of_enat_sub:
    2.85 +  assumes "n \<le> m" shows "ereal_of_enat (m - n) = ereal_of_enat m - ereal_of_enat n "
    2.86 +using assms by (cases m n rule: enat2_cases) auto
    2.87 +
    2.88 +lemma ereal_of_enat_mult:
    2.89 +  "ereal_of_enat (m * n) = ereal_of_enat m * ereal_of_enat n"
    2.90 +by (cases m n rule: enat2_cases) auto
    2.91 +
    2.92 +lemmas ereal_of_enat_pushin = ereal_of_enat_add ereal_of_enat_sub ereal_of_enat_mult
    2.93 +lemmas ereal_of_enat_pushout = ereal_of_enat_pushin[symmetric]
    2.94 +
    2.95 +
    2.96  subsection "Limits on @{typ ereal}"
    2.97  
    2.98  subsubsection "Topological space"
     3.1 --- a/src/HOL/Probability/Probability_Measure.thy	Mon Dec 19 14:41:08 2011 +0100
     3.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Tue Dec 20 11:40:56 2011 +0100
     3.3 @@ -1028,7 +1028,6 @@
     3.4      proof
     3.5        show "positive ?P (measure ?P)"
     3.6        proof (simp add: positive_def, safe)
     3.7 -        show "0 / \<mu> A = 0" using `\<mu> A \<noteq> 0` by (cases "\<mu> A") (auto simp: zero_ereal_def)
     3.8          fix B assume "B \<in> events"
     3.9          with real_measure[of "A \<inter> B"] real_measure[OF `A \<in> events`] `A \<in> sets M`
    3.10          show "0 \<le> \<mu> (A \<inter> B) / \<mu> A" by (auto simp: Int)