Theory Fstream

Up to index of Isabelle/HOLCF/FOCUS

theory Fstream
imports Stream
uses [Fstream.ML]
begin

(*  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

fscons

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 = bs = t)

theorem fstream_prefix:

  a~>s << t ==> ∃tt. t = a~>tts << tt

theorem fstream_prefix':

  x << a~>z = (x = UU ∨ (∃y. x = a~>yy << z))

ft & rt

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

take

theorem fstream_take_Suc:

  stream_take (Suc n)·(a~>s) = a~>stream_take n·s

slen

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. xa~>y ∨ #y < Fin (Suc n))

theorem slen_fscons_less_eq:

  (#(a~>y) < Fin (Suc (Suc n))) = (#y < Fin (Suc n))

induction

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

fsfilter

theorem fsfilter_empty:

  A(C)UU = UU

theorem fsfilter_fscons:

  A(C)x~>xs = (if xA 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:

  ba ==> {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)