Introduce infinity type class
authorhoelzl
Tue Jul 19 14:37:09 2011 +0200 (2011-07-19)
changeset 43921e8511be08ddd
parent 43920 cedb5cb948fd
child 43922 c6f35921056e
Introduce infinity type class
src/HOL/HOLCF/FOCUS/Fstreams.thy
src/HOL/HOLCF/FOCUS/Stream_adm.thy
src/HOL/HOLCF/Library/Stream.thy
src/HOL/Library/Extended_Nat.thy
     1.1 --- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Jul 19 14:36:12 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Jul 19 14:37:09 2011 +0200
     1.3 @@ -99,7 +99,7 @@
     1.4  lemma last_UU[simp]:"last UU = undefined"
     1.5  by (simp add: last_def jth_def enat_defs)
     1.6  
     1.7 -lemma last_infinite[simp]:"#s = Infty ==> last s = undefined"
     1.8 +lemma last_infinite[simp]:"#s = \<infinity> ==> last s = undefined"
     1.9  by (simp add: last_def)
    1.10  
    1.11  lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = undefined"
     2.1 --- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Tue Jul 19 14:36:12 2011 +0200
     2.2 +++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Tue Jul 19 14:37:09 2011 +0200
     2.3 @@ -87,7 +87,7 @@
     2.4  done
     2.5  
     2.6  
     2.7 -(* context (theory "Nat_InFinity");*)
     2.8 +(* context (theory "Extended_Nat");*)
     2.9  lemma ile_lemma: "Fin (i + j) <= x ==> Fin i <= x"
    2.10    by (rule order_trans) auto
    2.11  
     3.1 --- a/src/HOL/HOLCF/Library/Stream.thy	Tue Jul 19 14:36:12 2011 +0200
     3.2 +++ b/src/HOL/HOLCF/Library/Stream.thy	Tue Jul 19 14:37:09 2011 +0200
     3.3 @@ -424,7 +424,7 @@
     3.4  apply (simp add: stream.finite_def, auto)
     3.5  by (simp add: slen_take_lemma4)
     3.6  
     3.7 -lemma slen_infinite: "stream_finite x = (#x ~= Infty)"
     3.8 +lemma slen_infinite: "stream_finite x = (#x ~= \<infinity>)"
     3.9  by (simp add: slen_def)
    3.10  
    3.11  lemma slen_mono_lemma: "stream_finite s ==> ALL t. s << t --> #s <= #t"
    3.12 @@ -849,16 +849,16 @@
    3.13  (* ----------------------------------------------------------------------- *)
    3.14  
    3.15  lemma slen_sconc_finite1:
    3.16 -  "[| #(x ooo y) = Infty; Fin n = #x |] ==> #y = Infty"
    3.17 -apply (case_tac "#y ~= Infty",auto)
    3.18 +  "[| #(x ooo y) = \<infinity>; Fin n = #x |] ==> #y = \<infinity>"
    3.19 +apply (case_tac "#y ~= \<infinity>",auto)
    3.20  apply (drule_tac y=y in rt_sconc1)
    3.21  apply (insert stream_finite_i_rt [of n "x ooo y"])
    3.22  by (simp add: slen_infinite)
    3.23  
    3.24 -lemma slen_sconc_infinite1: "#x=Infty ==> #(x ooo y) = Infty"
    3.25 +lemma slen_sconc_infinite1: "#x=\<infinity> ==> #(x ooo y) = \<infinity>"
    3.26  by (simp add: sconc_def)
    3.27  
    3.28 -lemma slen_sconc_infinite2: "#y=Infty ==> #(x ooo y) = Infty"
    3.29 +lemma slen_sconc_infinite2: "#y=\<infinity> ==> #(x ooo y) = \<infinity>"
    3.30  apply (case_tac "#x")
    3.31   apply (simp add: sconc_def)
    3.32   apply (rule someI2_ex)
    3.33 @@ -868,7 +868,7 @@
    3.34   apply (fastsimp simp add: slen_infinite,auto)
    3.35  by (simp add: sconc_def)
    3.36  
    3.37 -lemma sconc_finite: "(#x~=Infty & #y~=Infty) = (#(x ooo y)~=Infty)"
    3.38 +lemma sconc_finite: "(#x~=\<infinity> & #y~=\<infinity>) = (#(x ooo y)~=\<infinity>)"
    3.39  apply auto
    3.40    apply (metis not_Infty_eq slen_sconc_finite1)
    3.41   apply (metis not_Infty_eq slen_sconc_infinite1)
    3.42 @@ -934,7 +934,7 @@
    3.43  
    3.44  lemma contlub_sconc_lemma:
    3.45    "chain Y ==> (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"
    3.46 -apply (case_tac "#x=Infty")
    3.47 +apply (case_tac "#x=\<infinity>")
    3.48   apply (simp add: sconc_def)
    3.49  apply (drule finite_lub_sconc,auto simp add: slen_infinite)
    3.50  done
     4.1 --- a/src/HOL/Library/Extended_Nat.thy	Tue Jul 19 14:36:12 2011 +0200
     4.2 +++ b/src/HOL/Library/Extended_Nat.thy	Tue Jul 19 14:37:09 2011 +0200
     4.3 @@ -9,6 +9,15 @@
     4.4  imports Main
     4.5  begin
     4.6  
     4.7 +class infinity =
     4.8 +  fixes infinity :: "'a"
     4.9 +
    4.10 +notation (xsymbols)
    4.11 +  infinity  ("\<infinity>")
    4.12 +
    4.13 +notation (HTML output)
    4.14 +  infinity  ("\<infinity>")
    4.15 +
    4.16  subsection {* Type definition *}
    4.17  
    4.18  text {*
    4.19 @@ -16,26 +25,39 @@
    4.20    infinity.
    4.21  *}
    4.22  
    4.23 -datatype enat = Fin nat | Infty
    4.24 -
    4.25 -notation (xsymbols)
    4.26 -  Infty  ("\<infinity>")
    4.27 +typedef (open) enat = "UNIV :: nat option set" ..
    4.28 + 
    4.29 +definition Fin :: "nat \<Rightarrow> enat" where
    4.30 +  "Fin n = Abs_enat (Some n)"
    4.31 + 
    4.32 +instantiation enat :: infinity
    4.33 +begin
    4.34 +  definition "\<infinity> = Abs_enat None"
    4.35 +  instance proof qed
    4.36 +end
    4.37 + 
    4.38 +rep_datatype Fin "\<infinity> :: enat"
    4.39 +proof -
    4.40 +  fix P i assume "\<And>j. P (Fin j)" "P \<infinity>"
    4.41 +  then show "P i"
    4.42 +  proof induct
    4.43 +    case (Abs_enat y) then show ?case
    4.44 +      by (cases y rule: option.exhaust)
    4.45 +         (auto simp: Fin_def infinity_enat_def)
    4.46 +  qed
    4.47 +qed (auto simp add: Fin_def infinity_enat_def Abs_enat_inject)
    4.48  
    4.49 -notation (HTML output)
    4.50 -  Infty  ("\<infinity>")
    4.51 +declare [[coercion "Fin :: nat \<Rightarrow> enat"]]
    4.52  
    4.53 -
    4.54 -lemma not_Infty_eq[iff]: "(x ~= Infty) = (EX i. x = Fin i)"
    4.55 +lemma not_Infty_eq[iff]: "(x \<noteq> \<infinity>) = (EX i. x = Fin i)"
    4.56  by (cases x) auto
    4.57  
    4.58 -lemma not_Fin_eq [iff]: "(ALL y. x ~= Fin y) = (x = Infty)"
    4.59 +lemma not_Fin_eq [iff]: "(ALL y. x ~= Fin y) = (x = \<infinity>)"
    4.60  by (cases x) auto
    4.61  
    4.62 -
    4.63  primrec the_Fin :: "enat \<Rightarrow> nat"
    4.64  where "the_Fin (Fin n) = n"
    4.65  
    4.66 -
    4.67  subsection {* Constructors and numbers *}
    4.68  
    4.69  instantiation enat :: "{zero, one, number}"
    4.70 @@ -69,10 +91,10 @@
    4.71  lemma one_iSuc: "1 = iSuc 0"
    4.72    by (simp add: zero_enat_def one_enat_def iSuc_def)
    4.73  
    4.74 -lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0"
    4.75 +lemma Infty_ne_i0 [simp]: "(\<infinity>::enat) \<noteq> 0"
    4.76    by (simp add: zero_enat_def)
    4.77  
    4.78 -lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>"
    4.79 +lemma i0_ne_Infty [simp]: "0 \<noteq> (\<infinity>::enat)"
    4.80    by (simp add: zero_enat_def)
    4.81  
    4.82  lemma zero_enat_eq [simp]:
    4.83 @@ -90,16 +112,16 @@
    4.84    "\<not> 1 = (0\<Colon>enat)"
    4.85    unfolding zero_enat_def one_enat_def by simp_all
    4.86  
    4.87 -lemma Infty_ne_i1 [simp]: "\<infinity> \<noteq> 1"
    4.88 +lemma Infty_ne_i1 [simp]: "(\<infinity>::enat) \<noteq> 1"
    4.89    by (simp add: one_enat_def)
    4.90  
    4.91 -lemma i1_ne_Infty [simp]: "1 \<noteq> \<infinity>"
    4.92 +lemma i1_ne_Infty [simp]: "1 \<noteq> (\<infinity>::enat)"
    4.93    by (simp add: one_enat_def)
    4.94  
    4.95 -lemma Infty_ne_number [simp]: "\<infinity> \<noteq> number_of k"
    4.96 +lemma Infty_ne_number [simp]: "(\<infinity>::enat) \<noteq> number_of k"
    4.97    by (simp add: number_of_enat_def)
    4.98  
    4.99 -lemma number_ne_Infty [simp]: "number_of k \<noteq> \<infinity>"
   4.100 +lemma number_ne_Infty [simp]: "number_of k \<noteq> (\<infinity>::enat)"
   4.101    by (simp add: number_of_enat_def)
   4.102  
   4.103  lemma iSuc_Fin: "iSuc (Fin n) = Fin (Suc n)"
   4.104 @@ -134,9 +156,10 @@
   4.105    "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | Fin m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | Fin n \<Rightarrow> Fin (m + n)))"
   4.106  
   4.107  lemma plus_enat_simps [simp, code]:
   4.108 -  "Fin m + Fin n = Fin (m + n)"
   4.109 -  "\<infinity> + q = \<infinity>"
   4.110 -  "q + \<infinity> = \<infinity>"
   4.111 +  fixes q :: enat
   4.112 +  shows "Fin m + Fin n = Fin (m + n)"
   4.113 +    and "\<infinity> + q = \<infinity>"
   4.114 +    and "q + \<infinity> = \<infinity>"
   4.115    by (simp_all add: plus_enat_def split: enat.splits)
   4.116  
   4.117  instance proof
   4.118 @@ -195,7 +218,7 @@
   4.119  
   4.120  lemma times_enat_simps [simp, code]:
   4.121    "Fin m * Fin n = Fin (m * n)"
   4.122 -  "\<infinity> * \<infinity> = \<infinity>"
   4.123 +  "\<infinity> * \<infinity> = (\<infinity>::enat)"
   4.124    "\<infinity> * Fin n = (if n = 0 then 0 else \<infinity>)"
   4.125    "Fin m * \<infinity> = (if m = 0 then 0 else \<infinity>)"
   4.126    unfolding times_enat_def zero_enat_def
   4.127 @@ -274,7 +297,7 @@
   4.128  lemma idiff_Fin_Fin[simp,code]: "Fin a - Fin b = Fin (a - b)"
   4.129  by(simp add: diff_enat_def)
   4.130  
   4.131 -lemma idiff_Infty[simp,code]: "\<infinity> - n = \<infinity>"
   4.132 +lemma idiff_Infty[simp,code]: "\<infinity> - n = (\<infinity>::enat)"
   4.133  by(simp add: diff_enat_def)
   4.134  
   4.135  lemma idiff_Infty_right[simp,code]: "Fin a - \<infinity> = 0"
   4.136 @@ -301,7 +324,6 @@
   4.137  
   4.138  (*lemmas idiff_self_eq_0_Fin = idiff_self_eq_0[unfolded zero_enat_def]*)
   4.139  
   4.140 -
   4.141  subsection {* Ordering *}
   4.142  
   4.143  instantiation enat :: linordered_ab_semigroup_add
   4.144 @@ -318,19 +340,19 @@
   4.145  lemma enat_ord_simps [simp]:
   4.146    "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
   4.147    "Fin m < Fin n \<longleftrightarrow> m < n"
   4.148 -  "q \<le> \<infinity>"
   4.149 -  "q < \<infinity> \<longleftrightarrow> q \<noteq> \<infinity>"
   4.150 -  "\<infinity> \<le> q \<longleftrightarrow> q = \<infinity>"
   4.151 -  "\<infinity> < q \<longleftrightarrow> False"
   4.152 +  "q \<le> (\<infinity>::enat)"
   4.153 +  "q < (\<infinity>::enat) \<longleftrightarrow> q \<noteq> \<infinity>"
   4.154 +  "(\<infinity>::enat) \<le> q \<longleftrightarrow> q = \<infinity>"
   4.155 +  "(\<infinity>::enat) < q \<longleftrightarrow> False"
   4.156    by (simp_all add: less_eq_enat_def less_enat_def split: enat.splits)
   4.157  
   4.158  lemma enat_ord_code [code]:
   4.159    "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
   4.160    "Fin m < Fin n \<longleftrightarrow> m < n"
   4.161 -  "q \<le> \<infinity> \<longleftrightarrow> True"
   4.162 +  "q \<le> (\<infinity>::enat) \<longleftrightarrow> True"
   4.163    "Fin m < \<infinity> \<longleftrightarrow> True"
   4.164    "\<infinity> \<le> Fin n \<longleftrightarrow> False"
   4.165 -  "\<infinity> < q \<longleftrightarrow> False"
   4.166 +  "(\<infinity>::enat) < q \<longleftrightarrow> False"
   4.167    by simp_all
   4.168  
   4.169  instance by default
   4.170 @@ -414,16 +436,16 @@
   4.171    "min (Fin m) (Fin n) = Fin (min m n)"
   4.172    "min q 0 = 0"
   4.173    "min 0 q = 0"
   4.174 -  "min q \<infinity> = q"
   4.175 -  "min \<infinity> q = q"
   4.176 +  "min q (\<infinity>::enat) = q"
   4.177 +  "min (\<infinity>::enat) q = q"
   4.178    by (auto simp add: min_def)
   4.179  
   4.180  lemma max_enat_simps [simp]:
   4.181    "max (Fin m) (Fin n) = Fin (max m n)"
   4.182    "max q 0 = q"
   4.183    "max 0 q = q"
   4.184 -  "max q \<infinity> = \<infinity>"
   4.185 -  "max \<infinity> q = \<infinity>"
   4.186 +  "max q \<infinity> = (\<infinity>::enat)"
   4.187 +  "max \<infinity> q = (\<infinity>::enat)"
   4.188    by (simp_all add: max_def)
   4.189  
   4.190  lemma Fin_ile: "n \<le> Fin m \<Longrightarrow> \<exists>k. n = Fin k"
   4.191 @@ -479,7 +501,7 @@
   4.192  by (induct n) auto
   4.193  
   4.194  lemma less_InftyE:
   4.195 -  "[| n < Infty; !!k. n = Fin k ==> P |] ==> P"
   4.196 +  "[| n < \<infinity>; !!k. n = Fin k ==> P |] ==> P"
   4.197  by (induct n) auto
   4.198  
   4.199  lemma enat_less_induct:
   4.200 @@ -495,7 +517,7 @@
   4.201      fix nat
   4.202      show "P (Fin nat)" by (rule P_Fin)
   4.203    next
   4.204 -    show "P Infty"
   4.205 +    show "P \<infinity>"
   4.206        apply (rule prem, clarify)
   4.207        apply (erule less_InftyE)
   4.208        apply (simp add: P_Fin)