src/HOL/HOLCF/Library/Stream.thy
changeset 43919 a7e4fb1a0502
parent 42151 4da4fc77664b
child 43921 e8511be08ddd
     1.1 --- a/src/HOL/HOLCF/Library/Stream.thy	Tue Jul 19 11:15:38 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/Library/Stream.thy	Tue Jul 19 14:35:44 2011 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* General Stream domain *}
     1.5  
     1.6  theory Stream
     1.7 -imports HOLCF "~~/src/HOL/Library/Nat_Infinity"
     1.8 +imports HOLCF "~~/src/HOL/Library/Extended_Nat"
     1.9  begin
    1.10  
    1.11  default_sort pcpo
    1.12 @@ -22,7 +22,7 @@
    1.13                                       If p\<cdot>x then x && h\<cdot>p\<cdot>xs else h\<cdot>p\<cdot>xs)"
    1.14  
    1.15  definition
    1.16 -  slen :: "'a stream \<Rightarrow> inat"  ("#_" [1000] 1000) where
    1.17 +  slen :: "'a stream \<Rightarrow> enat"  ("#_" [1000] 1000) where
    1.18    "#s = (if stream_finite s then Fin (LEAST n. stream_take n\<cdot>s = s) else \<infinity>)"
    1.19  
    1.20  
    1.21 @@ -327,7 +327,7 @@
    1.22  section "slen"
    1.23  
    1.24  lemma slen_empty [simp]: "#\<bottom> = 0"
    1.25 -by (simp add: slen_def stream.finite_def zero_inat_def Least_equality)
    1.26 +by (simp add: slen_def stream.finite_def zero_enat_def Least_equality)
    1.27  
    1.28  lemma slen_scons [simp]: "x ~= \<bottom> ==> #(x&&xs) = iSuc (#xs)"
    1.29  apply (case_tac "stream_finite (x && xs)")
    1.30 @@ -361,7 +361,7 @@
    1.31  
    1.32  lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y |  a = \<bottom> |  #y < Fin (Suc n))"
    1.33   apply (cases x, auto)
    1.34 -   apply (simp add: zero_inat_def)
    1.35 +   apply (simp add: zero_enat_def)
    1.36    apply (case_tac "#stream") apply (simp_all add: iSuc_Fin)
    1.37   apply (case_tac "#stream") apply (simp_all add: iSuc_Fin)
    1.38  done
    1.39 @@ -445,7 +445,7 @@
    1.40  
    1.41  lemma slen_rt_mult [rule_format]: "!x. Fin (i + j) <= #x --> Fin j <= #(iterate i$rt$x)"
    1.42  apply (induct i, auto)
    1.43 -apply (case_tac "x=UU", auto simp add: zero_inat_def)
    1.44 +apply (case_tac "x=UU", auto simp add: zero_enat_def)
    1.45  apply (drule stream_exhaust_eq [THEN iffD1], auto)
    1.46  apply (erule_tac x="y" in allE, auto)
    1.47  apply (simp add: not_le) apply (case_tac "#y") apply (simp_all add: iSuc_Fin)
    1.48 @@ -455,7 +455,7 @@
    1.49    "!(x::'a::flat stream) y. Fin n <= #x --> x << y --> stream_take n\<cdot>x = stream_take n\<cdot>y"
    1.50  apply (induct_tac n, auto)
    1.51  apply (case_tac "x=UU", auto)
    1.52 -apply (simp add: zero_inat_def)
    1.53 +apply (simp add: zero_enat_def)
    1.54  apply (simp add: Suc_ile_eq)
    1.55  apply (case_tac "y=UU", clarsimp)
    1.56  apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+
    1.57 @@ -566,11 +566,11 @@
    1.58   apply (subgoal_tac "#(i_rt n s)=0")
    1.59    apply (case_tac "stream_take n$s = s",simp+)
    1.60    apply (insert slen_take_eq [rule_format,of n s],simp)
    1.61 -  apply (cases "#s") apply (simp_all add: zero_inat_def)
    1.62 +  apply (cases "#s") apply (simp_all add: zero_enat_def)
    1.63    apply (simp add: slen_take_eq)
    1.64    apply (cases "#s")
    1.65    using i_rt_take_lemma1 [of n s]
    1.66 -  apply (simp_all add: zero_inat_def)
    1.67 +  apply (simp_all add: zero_enat_def)
    1.68    done
    1.69  
    1.70  lemma i_rt_lemma_slen: "#s=Fin n ==> i_rt n s = UU"
    1.71 @@ -585,20 +585,20 @@
    1.72                              #(stream_take n$x) = Fin t & #(i_rt n x)= Fin j
    1.73                                                --> Fin (j + t) = #x"
    1.74  apply (induct n, auto)
    1.75 - apply (simp add: zero_inat_def)
    1.76 + apply (simp add: zero_enat_def)
    1.77  apply (case_tac "x=UU",auto)
    1.78 - apply (simp add: zero_inat_def)
    1.79 + apply (simp add: zero_enat_def)
    1.80  apply (drule stream_exhaust_eq [THEN iffD1],clarsimp)
    1.81  apply (subgoal_tac "EX k. Fin k = #y",clarify)
    1.82   apply (erule_tac x="k" in allE)
    1.83   apply (erule_tac x="y" in allE,auto)
    1.84   apply (erule_tac x="THE p. Suc p = t" in allE,auto)
    1.85 -   apply (simp add: iSuc_def split: inat.splits)
    1.86 -  apply (simp add: iSuc_def split: inat.splits)
    1.87 +   apply (simp add: iSuc_def split: enat.splits)
    1.88 +  apply (simp add: iSuc_def split: enat.splits)
    1.89    apply (simp only: the_equality)
    1.90 - apply (simp add: iSuc_def split: inat.splits)
    1.91 + apply (simp add: iSuc_def split: enat.splits)
    1.92   apply force
    1.93 -apply (simp add: iSuc_def split: inat.splits)
    1.94 +apply (simp add: iSuc_def split: enat.splits)
    1.95  done
    1.96  
    1.97  lemma take_i_rt_len:
    1.98 @@ -690,13 +690,13 @@
    1.99  (* ----------------------------------------------------------------------- *)
   1.100  
   1.101  lemma UU_sconc [simp]: " UU ooo s = s "
   1.102 -by (simp add: sconc_def zero_inat_def)
   1.103 +by (simp add: sconc_def zero_enat_def)
   1.104  
   1.105  lemma scons_neq_UU: "a~=UU ==> a && s ~=UU"
   1.106  by auto
   1.107  
   1.108  lemma singleton_sconc [rule_format, simp]: "x~=UU --> (x && UU) ooo y = x && y"
   1.109 -apply (simp add: sconc_def zero_inat_def iSuc_def split: inat.splits, auto)
   1.110 +apply (simp add: sconc_def zero_enat_def iSuc_def split: enat.splits, auto)
   1.111  apply (rule someI2_ex,auto)
   1.112   apply (rule_tac x="x && y" in exI,auto)
   1.113  apply (simp add: i_rt_Suc_forw)
   1.114 @@ -709,12 +709,12 @@
   1.115   apply (rule stream_finite_ind [of x],auto)
   1.116    apply (simp add: stream.finite_def)
   1.117    apply (drule slen_take_lemma1,blast)
   1.118 - apply (simp_all add: zero_inat_def iSuc_def split: inat.splits)
   1.119 + apply (simp_all add: zero_enat_def iSuc_def split: enat.splits)
   1.120  apply (erule_tac x="y" in allE,auto)
   1.121  by (rule_tac x="a && w" in exI,auto)
   1.122  
   1.123  lemma rt_sconc1: "Fin n = #x ==> i_rt n (x ooo y) = y"
   1.124 -apply (simp add: sconc_def split: inat.splits, arith?,auto)
   1.125 +apply (simp add: sconc_def split: enat.splits, arith?,auto)
   1.126  apply (rule someI2_ex,auto)
   1.127  by (drule ex_sconc,simp)
   1.128  
   1.129 @@ -948,7 +948,7 @@
   1.130  (* ----------------------------------------------------------------------- *)
   1.131  
   1.132  lemma constr_sconc_UUs [simp]: "constr_sconc UU s = s"
   1.133 -by (simp add: constr_sconc_def zero_inat_def)
   1.134 +by (simp add: constr_sconc_def zero_enat_def)
   1.135  
   1.136  lemma "x ooo y = constr_sconc x y"
   1.137  apply (case_tac "#x")