# HG changeset patch # User hoelzl # Date 1418138560 -3600 # Node ID f65ac77f7e07f112f88292c7b44a36c8b735996d # Parent 8281f83d286f12bb960c5f9d8882949534375553 move topology on enat to Extended_Real, otherwise Jinja_Threads fails diff -r 8281f83d286f -r f65ac77f7e07 src/HOL/Library/Extended_Nat.thy --- a/src/HOL/Library/Extended_Nat.thy Sat Nov 22 11:05:41 2014 +0100 +++ b/src/HOL/Library/Extended_Nat.thy Tue Dec 09 16:22:40 2014 +0100 @@ -6,7 +6,7 @@ section {* Extended natural numbers (i.e. with infinity) *} theory Extended_Nat -imports Complex_Main Countable +imports Main Countable begin class infinity = @@ -647,17 +647,6 @@ instance enat :: complete_linorder .. -instantiation enat :: linorder_topology -begin - -definition open_enat :: "enat set \ bool" where - "open_enat = generate_topology (range lessThan \ range greaterThan)" - -instance - proof qed (rule open_enat_def) - -end - subsection {* Traditional theorem names *} lemmas enat_defs = zero_enat_def one_enat_def eSuc_def diff -r 8281f83d286f -r f65ac77f7e07 src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Sat Nov 22 11:05:41 2014 +0100 +++ b/src/HOL/Library/Extended_Real.thy Tue Dec 09 16:22:40 2014 +0100 @@ -13,6 +13,90 @@ text {* +This should be part of @{theory Extended_Nat}, but then the AFP-entry @{text "Jinja_Thread"} fails, as it does +overload certain named from @{theory Complex_Main}. + +*} + +instantiation enat :: linorder_topology +begin + +definition open_enat :: "enat set \ bool" where + "open_enat = generate_topology (range lessThan \ range greaterThan)" + +instance + proof qed (rule open_enat_def) + +end + +lemma open_enat: "open {enat n}" +proof (cases n) + case 0 + then have "{enat n} = {..< eSuc 0}" + by (auto simp: enat_0) + then show ?thesis + by simp +next + case (Suc n') + then have "{enat n} = {enat n' <..< enat (Suc n)}" + apply auto + apply (case_tac x) + apply auto + done + then show ?thesis + by simp +qed + +lemma open_enat_iff: + fixes A :: "enat set" + shows "open A \ (\ \ A \ (\n::nat. {n <..} \ A))" +proof safe + assume "\ \ A" + then have "A = (\n\{n. enat n \ A}. {enat n})" + apply auto + apply (case_tac x) + apply auto + done + moreover have "open \" + by (auto intro: open_enat) + ultimately show "open A" + by simp +next + fix n assume "{enat n <..} \ A" + then have "A = (\n\{n. enat n \ A}. {enat n}) \ {enat n <..}" + apply auto + apply (case_tac x) + apply auto + done + moreover have "open \" + by (intro open_Un open_UN ballI open_enat open_greaterThan) + ultimately show "open A" + by simp +next + assume "open A" "\ \ A" + then have "generate_topology (range lessThan \ range greaterThan) A" "\ \ A" + unfolding open_enat_def by auto + then show "\n::nat. {n <..} \ A" + proof induction + case (Int A B) + then obtain n m where "{enat n<..} \ A" "{enat m<..} \ B" + by auto + then have "{enat (max n m) <..} \ A \ B" + by (auto simp add: subset_eq Ball_def max_def enat_ord_code(1)[symmetric] simp del: enat_ord_code(1)) + then show ?case + by auto + next + case (UN K) + then obtain k where "k \ K" "\ \ k" + by auto + with UN.IH[OF this] show ?case + by auto + qed auto +qed + + +text {* + For more lemmas about the extended real numbers go to @{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"}