src/HOL/Library/Extended_Nat.thy
 changeset 60636 ee18efe9b246 parent 60500 903bb1495239 child 60679 ade12ef2773c
```     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Thu Jul 02 16:14:20 2015 +0200
1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Fri Jul 03 08:26:34 2015 +0200
1.3 @@ -6,7 +6,7 @@
1.4  section \<open>Extended natural numbers (i.e. with infinity)\<close>
1.5
1.6  theory Extended_Nat
1.7 -imports Main Countable
1.8 +imports Main Countable Order_Continuity
1.9  begin
1.10
1.11  class infinity =
1.12 @@ -472,6 +472,17 @@
1.13  apply (erule (1) le_less_trans)
1.14  done
1.15
1.16 +lemma eSuc_max: "eSuc (max x y) = max (eSuc x) (eSuc y)"
1.17 +  by (simp add: eSuc_def split: enat.split)
1.18 +
1.19 +lemma eSuc_Max:
1.20 +  assumes "finite A" "A \<noteq> {}"
1.21 +  shows "eSuc (Max A) = Max (eSuc ` A)"
1.22 +using assms proof induction
1.23 +  case (insert x A)
1.24 +  thus ?case by(cases "A = {}")(simp_all add: eSuc_max)
1.25 +qed simp
1.26 +
1.27  instantiation enat :: "{order_bot, order_top}"
1.28  begin
1.29
1.30 @@ -647,6 +658,12 @@
1.31
1.32  instance enat :: complete_linorder ..
1.33
1.34 +lemma eSuc_Sup: "A \<noteq> {} \<Longrightarrow> eSuc (Sup A) = Sup (eSuc ` A)"
1.35 +  by(auto simp add: Sup_enat_def eSuc_Max inj_on_def dest: finite_imageD)
1.36 +
1.37 +lemma sup_continuous_eSuc: "sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. eSuc (f x))"
1.38 +  using  eSuc_Sup[of "_ ` UNIV"] by (auto simp: sup_continuous_def)
1.39 +