src/HOL/Library/Extended_Nat.thy
changeset 62374 cb27a55d868a
parent 61631 4f7ef088c4ed
child 62376 85f38d5f8807
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Thu Feb 18 13:54:44 2016 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Fri Feb 19 12:25:57 2016 +0100
     1.3 @@ -12,7 +12,6 @@
     1.4  class infinity =
     1.5    fixes infinity :: "'a"  ("\<infinity>")
     1.6  
     1.7 -
     1.8  subsection \<open>Type definition\<close>
     1.9  
    1.10  text \<open>
    1.11 @@ -26,7 +25,7 @@
    1.12  
    1.13  definition enat :: "nat \<Rightarrow> enat" where
    1.14    "enat n = Abs_enat (Some n)"
    1.15 - 
    1.16 +
    1.17  instantiation enat :: infinity
    1.18  begin
    1.19  
    1.20 @@ -40,7 +39,7 @@
    1.21    show "\<exists>to_nat::enat \<Rightarrow> nat. inj to_nat"
    1.22      by (rule exI[of _ "to_nat \<circ> Rep_enat"]) (simp add: inj_on_def Rep_enat_inject)
    1.23  qed
    1.24 - 
    1.25 +
    1.26  old_rep_datatype enat "\<infinity> :: enat"
    1.27  proof -
    1.28    fix P i assume "\<And>j. P (enat j)" "P \<infinity>"
    1.29 @@ -169,7 +168,7 @@
    1.30  lemma eSuc_plus_1:
    1.31    "eSuc n = n + 1"
    1.32    by (cases n) (simp_all add: eSuc_enat one_enat_def)
    1.33 -  
    1.34 +
    1.35  lemma plus_1_eSuc:
    1.36    "1 + q = eSuc q"
    1.37    "q + 1 = eSuc q"
    1.38 @@ -399,7 +398,7 @@
    1.39  
    1.40  lemma eSuc_ile_mono [simp]: "eSuc n \<le> eSuc m \<longleftrightarrow> n \<le> m"
    1.41    by (simp add: eSuc_def less_eq_enat_def split: enat.splits)
    1.42 - 
    1.43 +
    1.44  lemma eSuc_mono [simp]: "eSuc n < eSuc m \<longleftrightarrow> n < m"
    1.45    by (simp add: eSuc_def less_enat_def split: enat.splits)
    1.46  
    1.47 @@ -479,7 +478,7 @@
    1.48  lemma eSuc_max: "eSuc (max x y) = max (eSuc x) (eSuc y)"
    1.49    by (simp add: eSuc_def split: enat.split)
    1.50  
    1.51 -lemma eSuc_Max: 
    1.52 +lemma eSuc_Max:
    1.53    assumes "finite A" "A \<noteq> {}"
    1.54    shows "eSuc (Max A) = Max (eSuc ` A)"
    1.55  using assms proof induction