author noschinl Tue Dec 20 11:40:56 2011 +0100 (2011-12-20) changeset 45934 9321cd2572fe parent 45933 ee70da42e08a child 45935 32f769f94ea4
add simp rules for enat and ereal
```     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.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)
```