--- a/src/HOL/HOLCF/FOCUS/Fstreams.thy Tue Jul 19 14:38:29 2011 +0200
+++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy Tue Jul 19 14:38:48 2011 +0200
@@ -28,7 +28,7 @@
definition
jth :: "nat => 'a fstream => 'a" where
- "jth = (%n s. if Fin n < #s then THE a. i_th n s = Def a else undefined)"
+ "jth = (%n s. if enat n < #s then THE a. i_th n s = Def a else undefined)"
definition
first :: "'a fstream => 'a" where
@@ -36,7 +36,7 @@
definition
last :: "'a fstream => 'a" where
- "last = (%s. case #s of Fin n => (if n~=0 then jth (THE k. Suc k = n) s else undefined))"
+ "last = (%s. case #s of enat n => (if n~=0 then jth (THE k. Suc k = n) s else undefined))"
abbreviation
@@ -54,7 +54,7 @@
lemma ft_fsingleton[simp]: "ft$(<a>) = Def a"
by (simp add: fsingleton_def2)
-lemma slen_fsingleton[simp]: "#(<a>) = Fin 1"
+lemma slen_fsingleton[simp]: "#(<a>) = enat 1"
by (simp add: fsingleton_def2 enat_defs)
lemma slen_fstreams[simp]: "#(<a> ooo s) = iSuc (#s)"
@@ -62,17 +62,17 @@
lemma slen_fstreams2[simp]: "#(s ooo <a>) = iSuc (#s)"
apply (cases "#s")
-apply (auto simp add: iSuc_Fin)
+apply (auto simp add: iSuc_enat)
apply (insert slen_sconc [of _ s "Suc 0" "<a>"], auto)
by (simp add: sconc_def)
lemma j_th_0_fsingleton[simp]:"jth 0 (<a>) = a"
apply (simp add: fsingleton_def2 jth_def)
-by (simp add: i_th_def Fin_0)
+by (simp add: i_th_def enat_0)
lemma jth_0[simp]: "jth 0 (<a> ooo s) = a"
apply (simp add: fsingleton_def2 jth_def)
-by (simp add: i_th_def Fin_0)
+by (simp add: i_th_def enat_0)
lemma first_sconc[simp]: "first (<a> ooo s) = a"
by (simp add: first_def)
@@ -80,12 +80,12 @@
lemma first_fsingleton[simp]: "first (<a>) = a"
by (simp add: first_def)
-lemma jth_n[simp]: "Fin n = #s ==> jth n (s ooo <a>) = a"
+lemma jth_n[simp]: "enat n = #s ==> jth n (s ooo <a>) = a"
apply (simp add: jth_def, auto)
apply (simp add: i_th_def rt_sconc1)
by (simp add: enat_defs split: enat.splits)
-lemma last_sconc[simp]: "Fin n = #s ==> last (s ooo <a>) = a"
+lemma last_sconc[simp]: "enat n = #s ==> last (s ooo <a>) = a"
apply (simp add: last_def)
apply (simp add: enat_defs split:enat.splits)
by (drule sym, auto)
@@ -102,13 +102,13 @@
lemma last_infinite[simp]:"#s = \<infinity> ==> last s = undefined"
by (simp add: last_def)
-lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = undefined"
+lemma jth_slen_lemma1:"n <= k & enat n = #s ==> jth k s = undefined"
by (simp add: jth_def enat_defs split:enat.splits, auto)
lemma jth_UU[simp]:"jth n UU = undefined"
by (simp add: jth_def)
-lemma ext_last:"[|s ~= UU; Fin (Suc n) = #s|] ==> (stream_take n$s) ooo <(last s)> = s"
+lemma ext_last:"[|s ~= UU; enat (Suc n) = #s|] ==> (stream_take n$s) ooo <(last s)> = s"
apply (simp add: last_def)
apply (case_tac "#s", auto)
apply (simp add: fsingleton_def2)