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 +
    1.40  subsection \<open>Traditional theorem names\<close>
    1.41  
    1.42  lemmas enat_defs = zero_enat_def one_enat_def eSuc_def