src/HOL/HOLCF/FOCUS/Fstreams.thy
changeset 43919 a7e4fb1a0502
parent 42151 4da4fc77664b
child 43921 e8511be08ddd
     1.1 --- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Jul 19 11:15:38 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Jul 19 14:35:44 2011 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4  by (simp add: fsingleton_def2)
     1.5  
     1.6  lemma slen_fsingleton[simp]: "#(<a>) = Fin 1"
     1.7 -by (simp add: fsingleton_def2 inat_defs)
     1.8 +by (simp add: fsingleton_def2 enat_defs)
     1.9  
    1.10  lemma slen_fstreams[simp]: "#(<a> ooo s) = iSuc (#s)"
    1.11  by (simp add: fsingleton_def2)
    1.12 @@ -83,11 +83,11 @@
    1.13  lemma jth_n[simp]: "Fin n = #s ==> jth n (s ooo <a>) = a"
    1.14  apply (simp add: jth_def, auto)
    1.15  apply (simp add: i_th_def rt_sconc1)
    1.16 -by (simp add: inat_defs split: inat.splits)
    1.17 +by (simp add: enat_defs split: enat.splits)
    1.18  
    1.19  lemma last_sconc[simp]: "Fin n = #s ==> last (s ooo <a>) = a"
    1.20  apply (simp add: last_def)
    1.21 -apply (simp add: inat_defs split:inat.splits)
    1.22 +apply (simp add: enat_defs split:enat.splits)
    1.23  by (drule sym, auto)
    1.24  
    1.25  lemma last_fsingleton[simp]: "last (<a>) = a"
    1.26 @@ -97,13 +97,13 @@
    1.27  by (simp add: first_def jth_def)
    1.28  
    1.29  lemma last_UU[simp]:"last UU = undefined"
    1.30 -by (simp add: last_def jth_def inat_defs)
    1.31 +by (simp add: last_def jth_def enat_defs)
    1.32  
    1.33  lemma last_infinite[simp]:"#s = Infty ==> last s = undefined"
    1.34  by (simp add: last_def)
    1.35  
    1.36  lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = undefined"
    1.37 -by (simp add: jth_def inat_defs split:inat.splits, auto)
    1.38 +by (simp add: jth_def enat_defs split:enat.splits, auto)
    1.39  
    1.40  lemma jth_UU[simp]:"jth n UU = undefined" 
    1.41  by (simp add: jth_def)