1.1 --- a/src/HOL/Library/Extended_Nat.thy Sat Mar 24 16:27:04 2012 +0100
1.2 +++ b/src/HOL/Library/Extended_Nat.thy Sun Mar 25 20:15:39 2012 +0200
1.3 @@ -61,19 +61,17 @@
1.4 primrec the_enat :: "enat \<Rightarrow> nat"
1.5 where "the_enat (enat n) = n"
1.6
1.7 +
1.8 subsection {* Constructors and numbers *}
1.9
1.10 -instantiation enat :: "{zero, one, number}"
1.11 +instantiation enat :: "{zero, one}"
1.12 begin
1.13
1.14 definition
1.15 "0 = enat 0"
1.16
1.17 definition
1.18 - [code_unfold]: "1 = enat 1"
1.19 -
1.20 -definition
1.21 - [code_unfold, code del]: "number_of k = enat (number_of k)"
1.22 + "1 = enat 1"
1.23
1.24 instance ..
1.25
1.26 @@ -82,15 +80,12 @@
1.27 definition eSuc :: "enat \<Rightarrow> enat" where
1.28 "eSuc i = (case i of enat n \<Rightarrow> enat (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
1.29
1.30 -lemma enat_0: "enat 0 = 0"
1.31 +lemma enat_0 [code_post]: "enat 0 = 0"
1.32 by (simp add: zero_enat_def)
1.33
1.34 -lemma enat_1: "enat 1 = 1"
1.35 +lemma enat_1 [code_post]: "enat 1 = 1"
1.36 by (simp add: one_enat_def)
1.37
1.38 -lemma enat_number: "enat (number_of k) = number_of k"
1.39 - by (simp add: number_of_enat_def)
1.40 -
1.41 lemma one_eSuc: "1 = eSuc 0"
1.42 by (simp add: zero_enat_def one_enat_def eSuc_def)
1.43
1.44 @@ -100,16 +95,6 @@
1.45 lemma i0_ne_infinity [simp]: "0 \<noteq> (\<infinity>::enat)"
1.46 by (simp add: zero_enat_def)
1.47
1.48 -lemma zero_enat_eq [simp]:
1.49 - "number_of k = (0\<Colon>enat) \<longleftrightarrow> number_of k = (0\<Colon>nat)"
1.50 - "(0\<Colon>enat) = number_of k \<longleftrightarrow> number_of k = (0\<Colon>nat)"
1.51 - unfolding zero_enat_def number_of_enat_def by simp_all
1.52 -
1.53 -lemma one_enat_eq [simp]:
1.54 - "number_of k = (1\<Colon>enat) \<longleftrightarrow> number_of k = (1\<Colon>nat)"
1.55 - "(1\<Colon>enat) = number_of k \<longleftrightarrow> number_of k = (1\<Colon>nat)"
1.56 - unfolding one_enat_def number_of_enat_def by simp_all
1.57 -
1.58 lemma zero_one_enat_neq [simp]:
1.59 "\<not> 0 = (1\<Colon>enat)"
1.60 "\<not> 1 = (0\<Colon>enat)"
1.61 @@ -121,18 +106,9 @@
1.62 lemma i1_ne_infinity [simp]: "1 \<noteq> (\<infinity>::enat)"
1.63 by (simp add: one_enat_def)
1.64
1.65 -lemma infinity_ne_number [simp]: "(\<infinity>::enat) \<noteq> number_of k"
1.66 - by (simp add: number_of_enat_def)
1.67 -
1.68 -lemma number_ne_infinity [simp]: "number_of k \<noteq> (\<infinity>::enat)"
1.69 - by (simp add: number_of_enat_def)
1.70 -
1.71 lemma eSuc_enat: "eSuc (enat n) = enat (Suc n)"
1.72 by (simp add: eSuc_def)
1.73
1.74 -lemma eSuc_number_of: "eSuc (number_of k) = enat (Suc (number_of k))"
1.75 - by (simp add: eSuc_enat number_of_enat_def)
1.76 -
1.77 lemma eSuc_infinity [simp]: "eSuc \<infinity> = \<infinity>"
1.78 by (simp add: eSuc_def)
1.79
1.80 @@ -145,11 +121,6 @@
1.81 lemma eSuc_inject [simp]: "eSuc m = eSuc n \<longleftrightarrow> m = n"
1.82 by (simp add: eSuc_def split: enat.splits)
1.83
1.84 -lemma number_of_enat_inject [simp]:
1.85 - "(number_of k \<Colon> enat) = number_of l \<longleftrightarrow> (number_of k \<Colon> nat) = number_of l"
1.86 - by (simp add: number_of_enat_def)
1.87 -
1.88 -
1.89 subsection {* Addition *}
1.90
1.91 instantiation enat :: comm_monoid_add
1.92 @@ -177,16 +148,6 @@
1.93
1.94 end
1.95
1.96 -lemma plus_enat_number [simp]:
1.97 - "(number_of k \<Colon> enat) + number_of l = (if k < Int.Pls then number_of l
1.98 - else if l < Int.Pls then number_of k else number_of (k + l))"
1.99 - unfolding number_of_enat_def plus_enat_simps nat_arith(1) if_distrib [symmetric, of _ enat] ..
1.100 -
1.101 -lemma eSuc_number [simp]:
1.102 - "eSuc (number_of k) = (if neg (number_of k \<Colon> int) then 1 else number_of (Int.succ k))"
1.103 - unfolding eSuc_number_of
1.104 - unfolding one_enat_def number_of_enat_def Suc_nat_number_of if_distrib [symmetric] ..
1.105 -
1.106 lemma eSuc_plus_1:
1.107 "eSuc n = n + 1"
1.108 by (cases n) (simp_all add: eSuc_enat one_enat_def)
1.109 @@ -261,12 +222,6 @@
1.110 apply (simp add: plus_1_eSuc eSuc_enat)
1.111 done
1.112
1.113 -instance enat :: number_semiring
1.114 -proof
1.115 - fix n show "number_of (int n) = (of_nat n :: enat)"
1.116 - unfolding number_of_enat_def number_of_int of_nat_id of_nat_eq_enat ..
1.117 -qed
1.118 -
1.119 instance enat :: semiring_char_0 proof
1.120 have "inj enat" by (rule injI) simp
1.121 then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_enat)
1.122 @@ -279,6 +234,25 @@
1.123 by (auto simp add: times_enat_def zero_enat_def split: enat.split)
1.124
1.125
1.126 +subsection {* Numerals *}
1.127 +
1.128 +lemma numeral_eq_enat:
1.129 + "numeral k = enat (numeral k)"
1.130 + using of_nat_eq_enat [of "numeral k"] by simp
1.131 +
1.132 +lemma enat_numeral [code_abbrev]:
1.133 + "enat (numeral k) = numeral k"
1.134 + using numeral_eq_enat ..
1.135 +
1.136 +lemma infinity_ne_numeral [simp]: "(\<infinity>::enat) \<noteq> numeral k"
1.137 + by (simp add: numeral_eq_enat)
1.138 +
1.139 +lemma numeral_ne_infinity [simp]: "numeral k \<noteq> (\<infinity>::enat)"
1.140 + by (simp add: numeral_eq_enat)
1.141 +
1.142 +lemma eSuc_numeral [simp]: "eSuc (numeral k) = numeral (k + Num.One)"
1.143 + by (simp only: eSuc_plus_1 numeral_plus_one)
1.144 +
1.145 subsection {* Subtraction *}
1.146
1.147 instantiation enat :: minus
1.148 @@ -292,13 +266,13 @@
1.149
1.150 end
1.151
1.152 -lemma idiff_enat_enat [simp,code]: "enat a - enat b = enat (a - b)"
1.153 +lemma idiff_enat_enat [simp, code]: "enat a - enat b = enat (a - b)"
1.154 by (simp add: diff_enat_def)
1.155
1.156 -lemma idiff_infinity [simp,code]: "\<infinity> - n = (\<infinity>::enat)"
1.157 +lemma idiff_infinity [simp, code]: "\<infinity> - n = (\<infinity>::enat)"
1.158 by (simp add: diff_enat_def)
1.159
1.160 -lemma idiff_infinity_right [simp,code]: "enat a - \<infinity> = 0"
1.161 +lemma idiff_infinity_right [simp, code]: "enat a - \<infinity> = 0"
1.162 by (simp add: diff_enat_def)
1.163
1.164 lemma idiff_0 [simp]: "(0::enat) - n = 0"
1.165 @@ -344,13 +318,13 @@
1.166 "(\<infinity>::enat) < q \<longleftrightarrow> False"
1.167 by (simp_all add: less_eq_enat_def less_enat_def split: enat.splits)
1.168
1.169 -lemma number_of_le_enat_iff[simp]:
1.170 - shows "number_of m \<le> enat n \<longleftrightarrow> number_of m \<le> n"
1.171 -by (auto simp: number_of_enat_def)
1.172 +lemma numeral_le_enat_iff[simp]:
1.173 + shows "numeral m \<le> enat n \<longleftrightarrow> numeral m \<le> n"
1.174 +by (auto simp: numeral_eq_enat)
1.175
1.176 -lemma number_of_less_enat_iff[simp]:
1.177 - shows "number_of m < enat n \<longleftrightarrow> number_of m < n"
1.178 -by (auto simp: number_of_enat_def)
1.179 +lemma numeral_less_enat_iff[simp]:
1.180 + shows "numeral m < enat n \<longleftrightarrow> numeral m < n"
1.181 +by (auto simp: numeral_eq_enat)
1.182
1.183 lemma enat_ord_code [code]:
1.184 "enat m \<le> enat n \<longleftrightarrow> m \<le> n"
1.185 @@ -375,10 +349,15 @@
1.186 by (simp split: enat.splits)
1.187 qed
1.188
1.189 +(* BH: These equations are already proven generally for any type in
1.190 +class linordered_semidom. However, enat is not in that class because
1.191 +it does not have the cancellation property. Would it be worthwhile to
1.192 +a generalize linordered_semidom to a new class that includes enat? *)
1.193 +
1.194 lemma enat_ord_number [simp]:
1.195 - "(number_of m \<Colon> enat) \<le> number_of n \<longleftrightarrow> (number_of m \<Colon> nat) \<le> number_of n"
1.196 - "(number_of m \<Colon> enat) < number_of n \<longleftrightarrow> (number_of m \<Colon> nat) < number_of n"
1.197 - by (simp_all add: number_of_enat_def)
1.198 + "(numeral m \<Colon> enat) \<le> numeral n \<longleftrightarrow> (numeral m \<Colon> nat) \<le> numeral n"
1.199 + "(numeral m \<Colon> enat) < numeral n \<longleftrightarrow> (numeral m \<Colon> nat) < numeral n"
1.200 + by (simp_all add: numeral_eq_enat)
1.201
1.202 lemma i0_lb [simp]: "(0\<Colon>enat) \<le> n"
1.203 by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
1.204 @@ -525,10 +504,10 @@
1.205 val find_first = find_first_t []
1.206 val trans_tac = Numeral_Simprocs.trans_tac
1.207 val norm_ss = HOL_basic_ss addsimps
1.208 - @{thms add_ac semiring_numeral_0_eq_0 add_0_left add_0_right}
1.209 + @{thms add_ac add_0_left add_0_right}
1.210 fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
1.211 fun simplify_meta_eq ss cancel_th th =
1.212 - Arith_Data.simplify_meta_eq @{thms semiring_numeral_0_eq_0} ss
1.213 + Arith_Data.simplify_meta_eq [] ss
1.214 ([th, cancel_th] MRS trans)
1.215 fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
1.216 end
1.217 @@ -646,7 +625,7 @@
1.218
1.219 subsection {* Traditional theorem names *}
1.220
1.221 -lemmas enat_defs = zero_enat_def one_enat_def number_of_enat_def eSuc_def
1.222 +lemmas enat_defs = zero_enat_def one_enat_def eSuc_def
1.223 plus_enat_def less_eq_enat_def less_enat_def
1.224
1.225 end