Theory Stream_adm

Up to index of Isabelle/HOLCF/FOCUS

theory Stream_adm
imports Stream Continuity
uses [Stream_adm.ML]
begin

(*  Title:      HOLCF/ex/Stream_adm.thy
    ID:         $Id: Stream_adm.thy,v 1.5 2005/09/06 19:51:18 wenzelm Exp $
    Author:     David von Oheimb, TU Muenchen
*)

header {* Admissibility for streams *}

theory Stream_adm
imports Stream Continuity
begin

constdefs

  stream_monoP  :: "(('a stream) set => ('a stream) set) => bool"
  "stream_monoP F ≡ ∃Q i. ∀P s. Fin i ≤ #s -->
                    (s ∈ F P) = (stream_take i·s ∈ Q ∧ iterate i rt s ∈ P)"

  stream_antiP  :: "(('a stream) set => ('a stream) set) => bool"
  "stream_antiP F ≡ ∀P x. ∃Q i.
                (#x  < Fin i --> (∀y. x \<sqsubseteq> y --> y ∈ F P --> x ∈ F P)) ∧
                (Fin i <= #x --> (∀y. x \<sqsubseteq> y -->
                (y ∈ F P) = (stream_take i·y ∈ Q ∧ iterate i rt y ∈ P)))"

  antitonP :: "'a set => bool"
  "antitonP P ≡ ∀x y. x \<sqsubseteq> y --> y∈P --> x∈P"

ML {* use_legacy_bindings (the_context ()) *}

end

admissibility

theorem flatstream_adm_lemma:

  [| chain Y; ∀i. P (Y i);
     !!Y. [| chain Y; ∀i. P (Y i); ∀k. ∃j. Fin k < #(Y j) |]
          ==> P (lub (range Y)) |]
  ==> P (lub (range Y))

theorem flatstream_admI:

  (!!Y. [| chain Y; ∀i. P (Y i); ∀k. ∃j. Fin k < #(Y j) |] ==> P (lub (range Y)))
  ==> adm P

theorem ile_lemma:

  Fin (i + j) ≤ x ==> Fin ix

theorem stream_monoP2I:

  stream_monoP F
  ==> ∀i. ∃l. ∀x y. Fin l ≤ #x -->
                    x << y --> x ∈ down_iterate F i --> y ∈ down_iterate F i

theorem stream_monoP2_gfp_admI:

  [| ∀i. ∃l. ∀x y. Fin l ≤ #x -->
                   x << y --> x ∈ down_iterate F i --> y ∈ down_iterate F i;
     down_cont F |]
  ==> adm (%x. x ∈ gfp F)

theorem fstream_gfp_admI:

  [| stream_monoP F; down_cont F |] ==> adm (%x. x ∈ gfp F)

theorem stream_antiP2I:

  stream_antiP F
  ==> ∀i x y. x << y --> y ∈ down_iterate F i --> x ∈ down_iterate F i

theorem stream_antiP2_non_gfp_admI:

  [| ∀i x y. x << y --> y ∈ down_iterate F i --> x ∈ down_iterate F i;
     down_cont F |]
  ==> adm (%u. u ∉ gfp F)

theorem fstream_non_gfp_admI:

  [| stream_antiP F; down_cont F |] ==> adm (%u. u ∉ gfp F)

antitonP

theorem antitonPD:

  [| antitonP P; yP; x << y |] ==> xP

theorem antitonPI:

x y. yP --> x << y --> xP ==> antitonP P

theorem antitonP_adm_non_P:

  antitonP P ==> adm (%u. uP)

theorem def_gfp_adm_nonP:

  [| P == gfp F; {y. ∃x. y << xxP} ⊆ F {y. ∃x. y << xxP} |]
  ==> adm (%u. uP)

theorem adm_set:

  {lub (range Y) |Y. chain Y ∧ (∀i. Y iP)} ⊆ P ==> adm (%x. xP)

theorem def_gfp_admI:

  [| P == gfp F;
     {lub (range Y) |Y. chain Y ∧ (∀i. Y iP)}
     ⊆ F {lub (range Y) |Y. chain Y ∧ (∀i. Y iP)} |]
  ==> adm (%x. xP)