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.76    by (simp add: zero_enat_def)
    1.77  
    1.78 -lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>"
    1.79 +lemma i0_ne_Infty [simp]: "0 \<noteq> (\<infinity>::enat)"
    1.80    by (simp add: zero_enat_def)
    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.89    by (simp add: one_enat_def)
    1.90  
    1.91 -lemma i1_ne_Infty [simp]: "1 \<noteq> \<infinity>"
    1.92 +lemma i1_ne_Infty [simp]: "1 \<noteq> (\<infinity>::enat)"
    1.93    by (simp add: one_enat_def)
    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.97    by (simp add: number_of_enat_def)
    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.101    by (simp add: number_of_enat_def)
   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.129  by(simp add: diff_enat_def)
   1.130  
   1.131 -lemma idiff_Infty[simp,code]: "\<infinity> - n = \<infinity>"
   1.132 +lemma idiff_Infty[simp,code]: "\<infinity> - n = (\<infinity>::enat)"
   1.133  by(simp add: diff_enat_def)
   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.143  instantiation enat :: linordered_ab_semigroup_add
   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.188    by (simp_all add: max_def)
   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)
   1.208        apply (simp add: P_Fin)