move topology on enat to Extended_Real, otherwise Jinja_Threads fails
authorhoelzl
Tue Dec 09 16:22:40 2014 +0100 (2014-12-09)
changeset 59115f65ac77f7e07
parent 59114 8281f83d286f
child 59130 f4b6e2626cf8
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
src/HOL/Library/Extended_Nat.thy
src/HOL/Library/Extended_Real.thy
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Sat Nov 22 11:05:41 2014 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Tue Dec 09 16:22:40 2014 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  section {* Extended natural numbers (i.e. with infinity) *}
     1.5  
     1.6  theory Extended_Nat
     1.7 -imports Complex_Main Countable
     1.8 +imports Main Countable
     1.9  begin
    1.10  
    1.11  class infinity =
    1.12 @@ -647,17 +647,6 @@
    1.13  
    1.14  instance enat :: complete_linorder ..
    1.15  
    1.16 -instantiation enat :: linorder_topology
    1.17 -begin
    1.18 -
    1.19 -definition open_enat :: "enat set \<Rightarrow> bool" where
    1.20 -  "open_enat = generate_topology (range lessThan \<union> range greaterThan)"
    1.21 -
    1.22 -instance
    1.23 -  proof qed (rule open_enat_def)
    1.24 -
    1.25 -end
    1.26 -
    1.27  subsection {* Traditional theorem names *}
    1.28  
    1.29  lemmas enat_defs = zero_enat_def one_enat_def eSuc_def
     2.1 --- a/src/HOL/Library/Extended_Real.thy	Sat Nov 22 11:05:41 2014 +0100
     2.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue Dec 09 16:22:40 2014 +0100
     2.3 @@ -13,6 +13,90 @@
     2.4  
     2.5  text {*
     2.6  
     2.7 +This should be part of @{theory Extended_Nat}, but then the AFP-entry @{text "Jinja_Thread"} fails, as it does
     2.8 +overload certain named from @{theory Complex_Main}.
     2.9 +
    2.10 +*}
    2.11 +
    2.12 +instantiation enat :: linorder_topology
    2.13 +begin
    2.14 +
    2.15 +definition open_enat :: "enat set \<Rightarrow> bool" where
    2.16 +  "open_enat = generate_topology (range lessThan \<union> range greaterThan)"
    2.17 +
    2.18 +instance
    2.19 +  proof qed (rule open_enat_def)
    2.20 +
    2.21 +end
    2.22 +
    2.23 +lemma open_enat: "open {enat n}"
    2.24 +proof (cases n)
    2.25 +  case 0
    2.26 +  then have "{enat n} = {..< eSuc 0}"
    2.27 +    by (auto simp: enat_0)
    2.28 +  then show ?thesis
    2.29 +    by simp
    2.30 +next
    2.31 +  case (Suc n')
    2.32 +  then have "{enat n} = {enat n' <..< enat (Suc n)}"
    2.33 +    apply auto
    2.34 +    apply (case_tac x)
    2.35 +    apply auto
    2.36 +    done
    2.37 +  then show ?thesis
    2.38 +    by simp
    2.39 +qed
    2.40 +
    2.41 +lemma open_enat_iff:
    2.42 +  fixes A :: "enat set"
    2.43 +  shows "open A \<longleftrightarrow> (\<infinity> \<in> A \<longrightarrow> (\<exists>n::nat. {n <..} \<subseteq> A))"
    2.44 +proof safe
    2.45 +  assume "\<infinity> \<notin> A"
    2.46 +  then have "A = (\<Union>n\<in>{n. enat n \<in> A}. {enat n})"
    2.47 +    apply auto
    2.48 +    apply (case_tac x)
    2.49 +    apply auto
    2.50 +    done
    2.51 +  moreover have "open \<dots>"
    2.52 +    by (auto intro: open_enat)
    2.53 +  ultimately show "open A"
    2.54 +    by simp
    2.55 +next
    2.56 +  fix n assume "{enat n <..} \<subseteq> A"
    2.57 +  then have "A = (\<Union>n\<in>{n. enat n \<in> A}. {enat n}) \<union> {enat n <..}"
    2.58 +    apply auto
    2.59 +    apply (case_tac x)
    2.60 +    apply auto
    2.61 +    done
    2.62 +  moreover have "open \<dots>"
    2.63 +    by (intro open_Un open_UN ballI open_enat open_greaterThan)
    2.64 +  ultimately show "open A"
    2.65 +    by simp
    2.66 +next
    2.67 +  assume "open A" "\<infinity> \<in> A"
    2.68 +  then have "generate_topology (range lessThan \<union> range greaterThan) A" "\<infinity> \<in> A"
    2.69 +    unfolding open_enat_def by auto
    2.70 +  then show "\<exists>n::nat. {n <..} \<subseteq> A"
    2.71 +  proof induction
    2.72 +    case (Int A B)
    2.73 +    then obtain n m where "{enat n<..} \<subseteq> A" "{enat m<..} \<subseteq> B"
    2.74 +      by auto
    2.75 +    then have "{enat (max n m) <..} \<subseteq> A \<inter> B"
    2.76 +      by (auto simp add: subset_eq Ball_def max_def enat_ord_code(1)[symmetric] simp del: enat_ord_code(1))
    2.77 +    then show ?case
    2.78 +      by auto
    2.79 +  next
    2.80 +    case (UN K)
    2.81 +    then obtain k where "k \<in> K" "\<infinity> \<in> k"
    2.82 +      by auto
    2.83 +    with UN.IH[OF this] show ?case
    2.84 +      by auto
    2.85 +  qed auto
    2.86 +qed
    2.87 +
    2.88 +
    2.89 +text {*
    2.90 +
    2.91  For more lemmas about the extended real numbers go to
    2.92    @{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"}
    2.93