src/HOLCF/FOCUS/Stream_adm.thy
author wenzelm
Tue Sep 06 21:51:17 2005 +0200 (2005-09-06)
changeset 17293 ecf182ccc3ca
parent 14981 e73f8140af78
child 18075 43000d7a017c
permissions -rw-r--r--
converted to Isar theory format;
wenzelm@17293
     1
(*  Title:      HOLCF/ex/Stream_adm.thy
wenzelm@11355
     2
    ID:         $Id$
wenzelm@17293
     3
    Author:     David von Oheimb, TU Muenchen
oheimb@11350
     4
*)
oheimb@11350
     5
wenzelm@17293
     6
header {* Admissibility for streams *}
oheimb@11350
     7
wenzelm@17293
     8
theory Stream_adm
wenzelm@17293
     9
imports Stream Continuity
wenzelm@17293
    10
begin
oheimb@11350
    11
oheimb@11350
    12
constdefs
wenzelm@17293
    13
wenzelm@17293
    14
  stream_monoP  :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool"
wenzelm@17293
    15
  "stream_monoP F \<equiv> \<exists>Q i. \<forall>P s. Fin i \<le> #s \<longrightarrow>
wenzelm@17293
    16
                    (s \<in> F P) = (stream_take i\<cdot>s \<in> Q \<and> iterate i rt s \<in> P)"
wenzelm@17293
    17
wenzelm@17293
    18
  stream_antiP  :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool"
wenzelm@17293
    19
  "stream_antiP F \<equiv> \<forall>P x. \<exists>Q i.
wenzelm@17293
    20
                (#x  < Fin i \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow> y \<in> F P \<longrightarrow> x \<in> F P)) \<and>
wenzelm@17293
    21
                (Fin i <= #x \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow>
wenzelm@17293
    22
                (y \<in> F P) = (stream_take i\<cdot>y \<in> Q \<and> iterate i rt y \<in> P)))"
wenzelm@17293
    23
oheimb@11350
    24
  antitonP :: "'a set => bool"
wenzelm@17293
    25
  "antitonP P \<equiv> \<forall>x y. x \<sqsubseteq> y \<longrightarrow> y\<in>P \<longrightarrow> x\<in>P"
wenzelm@17293
    26
wenzelm@17293
    27
ML {* use_legacy_bindings (the_context ()) *}
wenzelm@17293
    28
oheimb@11350
    29
end