Up to index of Isabelle/HOLCF/FOCUS
theory Fstream(* Title: HOLCF/FOCUS/Fstream.thy ID: $Id: Fstream.thy,v 1.8 2005/09/06 19:51:17 wenzelm Exp $ Author: David von Oheimb, TU Muenchen FOCUS streams (with lifted elements) ###TODO: integrate Fstreams.thy *) header {* FOCUS flat streams *} theory Fstream imports Stream begin defaultsort type types 'a fstream = "'a lift stream" consts fscons :: "'a => 'a fstream -> 'a fstream" fsfilter :: "'a set => 'a fstream -> 'a fstream" syntax "@emptystream":: "'a fstream" ("<>") "@fscons" :: "'a => 'a fstream => 'a fstream" ("(_~>_)" [66,65] 65) "@fsfilter" :: "'a set => 'a fstream => 'a fstream" ("(_'(C')_)" [64,63] 63) syntax (xsymbols) "@fscons" :: "'a => 'a fstream => 'a fstream" ("(_\<leadsto>_)" [66,65] 65) "@fsfilter" :: "'a set => 'a fstream => 'a fstream" ("(_©_)" [64,63] 63) translations "<>" => "⊥" "a~>s" == "fscons a·s" "A(C)s" == "fsfilter A·s" defs fscons_def: "fscons a ≡ Λ s. Def a && s" fsfilter_def: "fsfilter A ≡ sfilter·(flift2 (λx. x∈A))" ML {* use_legacy_bindings (the_context ()) *} end
theorem Def_maximal:
[| a = Def d; a << b |] ==> b = Def d
theorem fscons_def2:
a~>s = Def a && s
theorem fstream_exhaust:
x = UU ∨ (∃a y. x = a~>y)
theorem fstream_cases:
[| x = UU ==> P; !!a y. x = a~>y ==> P |] ==> P
theorem fstream_exhaust_eq:
(x ≠ UU) = (∃a y. x = a~>y)
theorem fscons_not_empty:
a~>s ≠ UU
theorem fscons_inject:
(a~>s = b~>t) = (a = b ∧ s = t)
theorem fstream_prefix:
a~>s << t ==> ∃tt. t = a~>tt ∧ s << tt
theorem fstream_prefix':
x << a~>z = (x = UU ∨ (∃y. x = a~>y ∧ y << z))
theorem ft_empty:
ft·UU = UU
theorem ft_fscons:
ft·(m~>s) = Def m
theorem rt_empty:
rt·UU = UU
theorem rt_fscons:
rt·(m~>s) = s
theorem ft_eq:
(ft·s = Def a) = (∃t. s = a~>t)
theorem surjective_fscons_lemma:
(d~>y = x) = (ft·x = Def d ∧ rt·x = y)
theorem surjective_fscons:
ft·x = Def d ==> d~>rt·x = x
theorem fstream_take_Suc:
stream_take (Suc n)·(a~>s) = a~>stream_take n·s
theorem slen_fscons:
#(m~>s) = iSuc #s
theorem slen_fscons_eq:
(Fin (Suc n) < #x) = (∃a y. x = a~>y ∧ Fin n < #y)
theorem slen_fscons_eq_rev:
(#x < Fin (Suc (Suc n))) = (∀a y. x ≠ a~>y ∨ #y < Fin (Suc n))
theorem slen_fscons_less_eq:
(#(a~>y) < Fin (Suc (Suc n))) = (#y < Fin (Suc n))
theorem fstream_ind:
[| adm P; P UU; !!a s. P s ==> P (a~>s) |] ==> P x
theorem fstream_ind2:
[| adm P; P UU; !!a. P (a~>UU); !!a b s. P s ==> P (a~>b~>s) |] ==> P x
theorem fsfilter_empty:
A(C)UU = UU
theorem fsfilter_fscons:
A(C)x~>xs = (if x ∈ A then x~>(A(C)xs) else A(C)xs)
theorem fsfilter_emptys:
{}(C)x = UU
theorem fsfilter_insert:
insert a A(C)a~>x = a~>(insert a A(C)x)
theorem fsfilter_single_in:
{a}(C)a~>x = a~>({a}(C)x)
theorem fsfilter_single_out:
b ≠ a ==> {a}(C)b~>x = {a}(C)x
theorem fstream_lub_lemma1:
[| chain Y; lub (range Y) = a~>s |] ==> ∃j t. Y j = a~>t
theorem fstream_lub_lemma:
[| chain Y; lub (range Y) = a~>s |] ==> (∃j t. Y j = a~>t) ∧ (∃X. chain X ∧ (∀i. ∃j. Y j = a~>X i) ∧ lub (range X) = s)