src/HOL/Library/Extended_Nat.thy

 begin
 
 class infinity =
   fixes infinity :: "'a"  ("\<infinity>")
 
-
 subsection \<open>Type definition\<close>
 
 text \<open>
   We extend the standard natural numbers by a special value indicating
   infinity.

 
 text \<open>TODO: introduce enat as coinductive datatype, enat is just @{const of_nat}\<close>
 
 definition enat :: "nat \<Rightarrow> enat" where
   "enat n = Abs_enat (Some n)"
- 
+
 instantiation enat :: infinity
 begin
 
 definition "\<infinity> = Abs_enat None"
 instance ..

 instance enat :: countable
 proof
   show "\<exists>to_nat::enat \<Rightarrow> nat. inj to_nat"
     by (rule exI[of _ "to_nat \<circ> Rep_enat"]) (simp add: inj_on_def Rep_enat_inject)
 qed
- 
+
 old_rep_datatype enat "\<infinity> :: enat"
 proof -
   fix P i assume "\<And>j. P (enat j)" "P \<infinity>"
   then show "P i"
   proof induct

 end
 
 lemma eSuc_plus_1:
   "eSuc n = n + 1"
   by (cases n) (simp_all add: eSuc_enat one_enat_def)
-  
+
 lemma plus_1_eSuc:
   "1 + q = eSuc q"
   "q + 1 = eSuc q"
   by (simp_all add: eSuc_plus_1 ac_simps)
 

 lemma i0_less [simp]: "(0::enat) < n \<longleftrightarrow> n \<noteq> 0"
   by (simp add: zero_enat_def less_enat_def split: enat.splits)
 
 lemma eSuc_ile_mono [simp]: "eSuc n \<le> eSuc m \<longleftrightarrow> n \<le> m"
   by (simp add: eSuc_def less_eq_enat_def split: enat.splits)
- 
+
 lemma eSuc_mono [simp]: "eSuc n < eSuc m \<longleftrightarrow> n < m"
   by (simp add: eSuc_def less_enat_def split: enat.splits)
 
 lemma ile_eSuc [simp]: "n \<le> eSuc n"
   by (simp add: eSuc_def less_eq_enat_def split: enat.splits)

 done
 
 lemma eSuc_max: "eSuc (max x y) = max (eSuc x) (eSuc y)"
   by (simp add: eSuc_def split: enat.split)
 
-lemma eSuc_Max: 
+lemma eSuc_Max:
   assumes "finite A" "A \<noteq> {}"
   shows "eSuc (Max A) = Max (eSuc ` A)"
 using assms proof induction
   case (insert x A)
   thus ?case by(cases "A = {}")(simp_all add: eSuc_max)