src/HOL/Library/Extended_Nat.thy
changeset 47108 2a1953f0d20d
parent 45934 9321cd2572fe
child 49834 b27bbb021df1
     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