src/HOL/Library/Extended_Nat.thy
 changeset 43921 e8511be08ddd parent 43919 a7e4fb1a0502 child 43922 c6f35921056e
```     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Tue Jul 19 14:36:12 2011 +0200
1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Tue Jul 19 14:37:09 2011 +0200
1.3 @@ -9,6 +9,15 @@
1.4  imports Main
1.5  begin
1.6
1.7 +class infinity =
1.8 +  fixes infinity :: "'a"
1.9 +
1.10 +notation (xsymbols)
1.11 +  infinity  ("\<infinity>")
1.12 +
1.13 +notation (HTML output)
1.14 +  infinity  ("\<infinity>")
1.15 +
1.16  subsection {* Type definition *}
1.17
1.18  text {*
1.19 @@ -16,26 +25,39 @@
1.20    infinity.
1.21  *}
1.22
1.23 -datatype enat = Fin nat | Infty
1.24 -
1.25 -notation (xsymbols)
1.26 -  Infty  ("\<infinity>")
1.27 +typedef (open) enat = "UNIV :: nat option set" ..
1.28 +
1.29 +definition Fin :: "nat \<Rightarrow> enat" where
1.30 +  "Fin n = Abs_enat (Some n)"
1.31 +
1.32 +instantiation enat :: infinity
1.33 +begin
1.34 +  definition "\<infinity> = Abs_enat None"
1.35 +  instance proof qed
1.36 +end
1.37 +
1.38 +rep_datatype Fin "\<infinity> :: enat"
1.39 +proof -
1.40 +  fix P i assume "\<And>j. P (Fin j)" "P \<infinity>"
1.41 +  then show "P i"
1.42 +  proof induct
1.43 +    case (Abs_enat y) then show ?case
1.44 +      by (cases y rule: option.exhaust)
1.45 +         (auto simp: Fin_def infinity_enat_def)
1.46 +  qed
1.47 +qed (auto simp add: Fin_def infinity_enat_def Abs_enat_inject)
1.48
1.49 -notation (HTML output)
1.50 -  Infty  ("\<infinity>")
1.51 +declare [[coercion "Fin :: nat \<Rightarrow> enat"]]
1.52
1.53 -
1.54 -lemma not_Infty_eq[iff]: "(x ~= Infty) = (EX i. x = Fin i)"
1.55 +lemma not_Infty_eq[iff]: "(x \<noteq> \<infinity>) = (EX i. x = Fin i)"
1.56  by (cases x) auto
1.57
1.58 -lemma not_Fin_eq [iff]: "(ALL y. x ~= Fin y) = (x = Infty)"
1.59 +lemma not_Fin_eq [iff]: "(ALL y. x ~= Fin y) = (x = \<infinity>)"
1.60  by (cases x) auto
1.61
1.62 -
1.63  primrec the_Fin :: "enat \<Rightarrow> nat"
1.64  where "the_Fin (Fin n) = n"
1.65
1.66 -
1.67  subsection {* Constructors and numbers *}
1.68
1.69  instantiation enat :: "{zero, one, number}"
1.70 @@ -69,10 +91,10 @@
1.71  lemma one_iSuc: "1 = iSuc 0"
1.72    by (simp add: zero_enat_def one_enat_def iSuc_def)
1.73
1.74 -lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0"
1.75 +lemma Infty_ne_i0 [simp]: "(\<infinity>::enat) \<noteq> 0"
1.77
1.78 -lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>"
1.79 +lemma i0_ne_Infty [simp]: "0 \<noteq> (\<infinity>::enat)"
1.81
1.82  lemma zero_enat_eq [simp]:
1.83 @@ -90,16 +112,16 @@
1.84    "\<not> 1 = (0\<Colon>enat)"
1.85    unfolding zero_enat_def one_enat_def by simp_all
1.86
1.87 -lemma Infty_ne_i1 [simp]: "\<infinity> \<noteq> 1"
1.88 +lemma Infty_ne_i1 [simp]: "(\<infinity>::enat) \<noteq> 1"
1.90
1.91 -lemma i1_ne_Infty [simp]: "1 \<noteq> \<infinity>"
1.92 +lemma i1_ne_Infty [simp]: "1 \<noteq> (\<infinity>::enat)"
1.94
1.95 -lemma Infty_ne_number [simp]: "\<infinity> \<noteq> number_of k"
1.96 +lemma Infty_ne_number [simp]: "(\<infinity>::enat) \<noteq> number_of k"
1.98
1.99 -lemma number_ne_Infty [simp]: "number_of k \<noteq> \<infinity>"
1.100 +lemma number_ne_Infty [simp]: "number_of k \<noteq> (\<infinity>::enat)"
1.102
1.103  lemma iSuc_Fin: "iSuc (Fin n) = Fin (Suc n)"
1.104 @@ -134,9 +156,10 @@
1.105    "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | Fin m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | Fin n \<Rightarrow> Fin (m + n)))"
1.106
1.107  lemma plus_enat_simps [simp, code]:
1.108 -  "Fin m + Fin n = Fin (m + n)"
1.109 -  "\<infinity> + q = \<infinity>"
1.110 -  "q + \<infinity> = \<infinity>"
1.111 +  fixes q :: enat
1.112 +  shows "Fin m + Fin n = Fin (m + n)"
1.113 +    and "\<infinity> + q = \<infinity>"
1.114 +    and "q + \<infinity> = \<infinity>"
1.115    by (simp_all add: plus_enat_def split: enat.splits)
1.116
1.117  instance proof
1.118 @@ -195,7 +218,7 @@
1.119
1.120  lemma times_enat_simps [simp, code]:
1.121    "Fin m * Fin n = Fin (m * n)"
1.122 -  "\<infinity> * \<infinity> = \<infinity>"
1.123 +  "\<infinity> * \<infinity> = (\<infinity>::enat)"
1.124    "\<infinity> * Fin n = (if n = 0 then 0 else \<infinity>)"
1.125    "Fin m * \<infinity> = (if m = 0 then 0 else \<infinity>)"
1.126    unfolding times_enat_def zero_enat_def
1.127 @@ -274,7 +297,7 @@
1.128  lemma idiff_Fin_Fin[simp,code]: "Fin a - Fin b = Fin (a - b)"
1.130
1.131 -lemma idiff_Infty[simp,code]: "\<infinity> - n = \<infinity>"
1.132 +lemma idiff_Infty[simp,code]: "\<infinity> - n = (\<infinity>::enat)"
1.134
1.135  lemma idiff_Infty_right[simp,code]: "Fin a - \<infinity> = 0"
1.136 @@ -301,7 +324,6 @@
1.137
1.138  (*lemmas idiff_self_eq_0_Fin = idiff_self_eq_0[unfolded zero_enat_def]*)
1.139
1.140 -
1.141  subsection {* Ordering *}
1.142
1.144 @@ -318,19 +340,19 @@
1.145  lemma enat_ord_simps [simp]:
1.146    "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
1.147    "Fin m < Fin n \<longleftrightarrow> m < n"
1.148 -  "q \<le> \<infinity>"
1.149 -  "q < \<infinity> \<longleftrightarrow> q \<noteq> \<infinity>"
1.150 -  "\<infinity> \<le> q \<longleftrightarrow> q = \<infinity>"
1.151 -  "\<infinity> < q \<longleftrightarrow> False"
1.152 +  "q \<le> (\<infinity>::enat)"
1.153 +  "q < (\<infinity>::enat) \<longleftrightarrow> q \<noteq> \<infinity>"
1.154 +  "(\<infinity>::enat) \<le> q \<longleftrightarrow> q = \<infinity>"
1.155 +  "(\<infinity>::enat) < q \<longleftrightarrow> False"
1.156    by (simp_all add: less_eq_enat_def less_enat_def split: enat.splits)
1.157
1.158  lemma enat_ord_code [code]:
1.159    "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
1.160    "Fin m < Fin n \<longleftrightarrow> m < n"
1.161 -  "q \<le> \<infinity> \<longleftrightarrow> True"
1.162 +  "q \<le> (\<infinity>::enat) \<longleftrightarrow> True"
1.163    "Fin m < \<infinity> \<longleftrightarrow> True"
1.164    "\<infinity> \<le> Fin n \<longleftrightarrow> False"
1.165 -  "\<infinity> < q \<longleftrightarrow> False"
1.166 +  "(\<infinity>::enat) < q \<longleftrightarrow> False"
1.167    by simp_all
1.168
1.169  instance by default
1.170 @@ -414,16 +436,16 @@
1.171    "min (Fin m) (Fin n) = Fin (min m n)"
1.172    "min q 0 = 0"
1.173    "min 0 q = 0"
1.174 -  "min q \<infinity> = q"
1.175 -  "min \<infinity> q = q"
1.176 +  "min q (\<infinity>::enat) = q"
1.177 +  "min (\<infinity>::enat) q = q"
1.178    by (auto simp add: min_def)
1.179
1.180  lemma max_enat_simps [simp]:
1.181    "max (Fin m) (Fin n) = Fin (max m n)"
1.182    "max q 0 = q"
1.183    "max 0 q = q"
1.184 -  "max q \<infinity> = \<infinity>"
1.185 -  "max \<infinity> q = \<infinity>"
1.186 +  "max q \<infinity> = (\<infinity>::enat)"
1.187 +  "max \<infinity> q = (\<infinity>::enat)"
1.189
1.190  lemma Fin_ile: "n \<le> Fin m \<Longrightarrow> \<exists>k. n = Fin k"
1.191 @@ -479,7 +501,7 @@
1.192  by (induct n) auto
1.193
1.194  lemma less_InftyE:
1.195 -  "[| n < Infty; !!k. n = Fin k ==> P |] ==> P"
1.196 +  "[| n < \<infinity>; !!k. n = Fin k ==> P |] ==> P"
1.197  by (induct n) auto
1.198
1.199  lemma enat_less_induct:
1.200 @@ -495,7 +517,7 @@
1.201      fix nat
1.202      show "P (Fin nat)" by (rule P_Fin)
1.203    next
1.204 -    show "P Infty"
1.205 +    show "P \<infinity>"
1.206        apply (rule prem, clarify)
1.207        apply (erule less_InftyE)