# HG changeset patch # User hoelzl # Date 1311079029 -7200 # Node ID e8511be08dddf25ecb46ba090655712e0490394c # Parent cedb5cb948fda84847a0344c872ffca4e9ff6ab7 Introduce infinity type class diff -r cedb5cb948fd -r e8511be08ddd src/HOL/HOLCF/FOCUS/Fstreams.thy --- a/src/HOL/HOLCF/FOCUS/Fstreams.thy Tue Jul 19 14:36:12 2011 +0200 +++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy Tue Jul 19 14:37:09 2011 +0200 @@ -99,7 +99,7 @@ lemma last_UU[simp]:"last UU = undefined" by (simp add: last_def jth_def enat_defs) -lemma last_infinite[simp]:"#s = Infty ==> last s = undefined" +lemma last_infinite[simp]:"#s = \ ==> last s = undefined" by (simp add: last_def) lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = undefined" diff -r cedb5cb948fd -r e8511be08ddd src/HOL/HOLCF/FOCUS/Stream_adm.thy --- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy Tue Jul 19 14:36:12 2011 +0200 +++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy Tue Jul 19 14:37:09 2011 +0200 @@ -87,7 +87,7 @@ done -(* context (theory "Nat_InFinity");*) +(* context (theory "Extended_Nat");*) lemma ile_lemma: "Fin (i + j) <= x ==> Fin i <= x" by (rule order_trans) auto diff -r cedb5cb948fd -r e8511be08ddd src/HOL/HOLCF/Library/Stream.thy --- a/src/HOL/HOLCF/Library/Stream.thy Tue Jul 19 14:36:12 2011 +0200 +++ b/src/HOL/HOLCF/Library/Stream.thy Tue Jul 19 14:37:09 2011 +0200 @@ -424,7 +424,7 @@ apply (simp add: stream.finite_def, auto) by (simp add: slen_take_lemma4) -lemma slen_infinite: "stream_finite x = (#x ~= Infty)" +lemma slen_infinite: "stream_finite x = (#x ~= \)" by (simp add: slen_def) lemma slen_mono_lemma: "stream_finite s ==> ALL t. s << t --> #s <= #t" @@ -849,16 +849,16 @@ (* ----------------------------------------------------------------------- *) lemma slen_sconc_finite1: - "[| #(x ooo y) = Infty; Fin n = #x |] ==> #y = Infty" -apply (case_tac "#y ~= Infty",auto) + "[| #(x ooo y) = \; Fin n = #x |] ==> #y = \" +apply (case_tac "#y ~= \",auto) apply (drule_tac y=y in rt_sconc1) apply (insert stream_finite_i_rt [of n "x ooo y"]) by (simp add: slen_infinite) -lemma slen_sconc_infinite1: "#x=Infty ==> #(x ooo y) = Infty" +lemma slen_sconc_infinite1: "#x=\ ==> #(x ooo y) = \" by (simp add: sconc_def) -lemma slen_sconc_infinite2: "#y=Infty ==> #(x ooo y) = Infty" +lemma slen_sconc_infinite2: "#y=\ ==> #(x ooo y) = \" apply (case_tac "#x") apply (simp add: sconc_def) apply (rule someI2_ex) @@ -868,7 +868,7 @@ apply (fastsimp simp add: slen_infinite,auto) by (simp add: sconc_def) -lemma sconc_finite: "(#x~=Infty & #y~=Infty) = (#(x ooo y)~=Infty)" +lemma sconc_finite: "(#x~=\ & #y~=\) = (#(x ooo y)~=\)" apply auto apply (metis not_Infty_eq slen_sconc_finite1) apply (metis not_Infty_eq slen_sconc_infinite1) @@ -934,7 +934,7 @@ lemma contlub_sconc_lemma: "chain Y ==> (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))" -apply (case_tac "#x=Infty") +apply (case_tac "#x=\") apply (simp add: sconc_def) apply (drule finite_lub_sconc,auto simp add: slen_infinite) done diff -r cedb5cb948fd -r e8511be08ddd src/HOL/Library/Extended_Nat.thy --- a/src/HOL/Library/Extended_Nat.thy Tue Jul 19 14:36:12 2011 +0200 +++ b/src/HOL/Library/Extended_Nat.thy Tue Jul 19 14:37:09 2011 +0200 @@ -9,6 +9,15 @@ imports Main begin +class infinity = + fixes infinity :: "'a" + +notation (xsymbols) + infinity ("\") + +notation (HTML output) + infinity ("\") + subsection {* Type definition *} text {* @@ -16,26 +25,39 @@ infinity. *} -datatype enat = Fin nat | Infty - -notation (xsymbols) - Infty ("\") +typedef (open) enat = "UNIV :: nat option set" .. + +definition Fin :: "nat \ enat" where + "Fin n = Abs_enat (Some n)" + +instantiation enat :: infinity +begin + definition "\ = Abs_enat None" + instance proof qed +end + +rep_datatype Fin "\ :: enat" +proof - + fix P i assume "\j. P (Fin j)" "P \" + then show "P i" + proof induct + case (Abs_enat y) then show ?case + by (cases y rule: option.exhaust) + (auto simp: Fin_def infinity_enat_def) + qed +qed (auto simp add: Fin_def infinity_enat_def Abs_enat_inject) -notation (HTML output) - Infty ("\") +declare [[coercion "Fin :: nat \ enat"]] - -lemma not_Infty_eq[iff]: "(x ~= Infty) = (EX i. x = Fin i)" +lemma not_Infty_eq[iff]: "(x \ \) = (EX i. x = Fin i)" by (cases x) auto -lemma not_Fin_eq [iff]: "(ALL y. x ~= Fin y) = (x = Infty)" +lemma not_Fin_eq [iff]: "(ALL y. x ~= Fin y) = (x = \)" by (cases x) auto - primrec the_Fin :: "enat \ nat" where "the_Fin (Fin n) = n" - subsection {* Constructors and numbers *} instantiation enat :: "{zero, one, number}" @@ -69,10 +91,10 @@ lemma one_iSuc: "1 = iSuc 0" by (simp add: zero_enat_def one_enat_def iSuc_def) -lemma Infty_ne_i0 [simp]: "\ \ 0" +lemma Infty_ne_i0 [simp]: "(\::enat) \ 0" by (simp add: zero_enat_def) -lemma i0_ne_Infty [simp]: "0 \ \" +lemma i0_ne_Infty [simp]: "0 \ (\::enat)" by (simp add: zero_enat_def) lemma zero_enat_eq [simp]: @@ -90,16 +112,16 @@ "\ 1 = (0\enat)" unfolding zero_enat_def one_enat_def by simp_all -lemma Infty_ne_i1 [simp]: "\ \ 1" +lemma Infty_ne_i1 [simp]: "(\::enat) \ 1" by (simp add: one_enat_def) -lemma i1_ne_Infty [simp]: "1 \ \" +lemma i1_ne_Infty [simp]: "1 \ (\::enat)" by (simp add: one_enat_def) -lemma Infty_ne_number [simp]: "\ \ number_of k" +lemma Infty_ne_number [simp]: "(\::enat) \ number_of k" by (simp add: number_of_enat_def) -lemma number_ne_Infty [simp]: "number_of k \ \" +lemma number_ne_Infty [simp]: "number_of k \ (\::enat)" by (simp add: number_of_enat_def) lemma iSuc_Fin: "iSuc (Fin n) = Fin (Suc n)" @@ -134,9 +156,10 @@ "m + n = (case m of \ \ \ | Fin m \ (case n of \ \ \ | Fin n \ Fin (m + n)))" lemma plus_enat_simps [simp, code]: - "Fin m + Fin n = Fin (m + n)" - "\ + q = \" - "q + \ = \" + fixes q :: enat + shows "Fin m + Fin n = Fin (m + n)" + and "\ + q = \" + and "q + \ = \" by (simp_all add: plus_enat_def split: enat.splits) instance proof @@ -195,7 +218,7 @@ lemma times_enat_simps [simp, code]: "Fin m * Fin n = Fin (m * n)" - "\ * \ = \" + "\ * \ = (\::enat)" "\ * Fin n = (if n = 0 then 0 else \)" "Fin m * \ = (if m = 0 then 0 else \)" unfolding times_enat_def zero_enat_def @@ -274,7 +297,7 @@ lemma idiff_Fin_Fin[simp,code]: "Fin a - Fin b = Fin (a - b)" by(simp add: diff_enat_def) -lemma idiff_Infty[simp,code]: "\ - n = \" +lemma idiff_Infty[simp,code]: "\ - n = (\::enat)" by(simp add: diff_enat_def) lemma idiff_Infty_right[simp,code]: "Fin a - \ = 0" @@ -301,7 +324,6 @@ (*lemmas idiff_self_eq_0_Fin = idiff_self_eq_0[unfolded zero_enat_def]*) - subsection {* Ordering *} instantiation enat :: linordered_ab_semigroup_add @@ -318,19 +340,19 @@ lemma enat_ord_simps [simp]: "Fin m \ Fin n \ m \ n" "Fin m < Fin n \ m < n" - "q \ \" - "q < \ \ q \ \" - "\ \ q \ q = \" - "\ < q \ False" + "q \ (\::enat)" + "q < (\::enat) \ q \ \" + "(\::enat) \ q \ q = \" + "(\::enat) < q \ False" by (simp_all add: less_eq_enat_def less_enat_def split: enat.splits) lemma enat_ord_code [code]: "Fin m \ Fin n \ m \ n" "Fin m < Fin n \ m < n" - "q \ \ \ True" + "q \ (\::enat) \ True" "Fin m < \ \ True" "\ \ Fin n \ False" - "\ < q \ False" + "(\::enat) < q \ False" by simp_all instance by default @@ -414,16 +436,16 @@ "min (Fin m) (Fin n) = Fin (min m n)" "min q 0 = 0" "min 0 q = 0" - "min q \ = q" - "min \ q = q" + "min q (\::enat) = q" + "min (\::enat) q = q" by (auto simp add: min_def) lemma max_enat_simps [simp]: "max (Fin m) (Fin n) = Fin (max m n)" "max q 0 = q" "max 0 q = q" - "max q \ = \" - "max \ q = \" + "max q \ = (\::enat)" + "max \ q = (\::enat)" by (simp_all add: max_def) lemma Fin_ile: "n \ Fin m \ \k. n = Fin k" @@ -479,7 +501,7 @@ by (induct n) auto lemma less_InftyE: - "[| n < Infty; !!k. n = Fin k ==> P |] ==> P" + "[| n < \; !!k. n = Fin k ==> P |] ==> P" by (induct n) auto lemma enat_less_induct: @@ -495,7 +517,7 @@ fix nat show "P (Fin nat)" by (rule P_Fin) next - show "P Infty" + show "P \" apply (rule prem, clarify) apply (erule less_InftyE) apply (simp add: P_Fin)