Theory Buffer_adm

Up to index of Isabelle/HOLCF/FOCUS

theory Buffer_adm
imports Buffer Stream_adm
uses [Buffer_adm.ML]
begin

(*  Title:      HOLCF/FOCUS/Buffer_adm.thy
    ID:         $Id: Buffer_adm.thy,v 1.4 2005/09/06 19:51:17 wenzelm Exp $
    Author:     David von Oheimb, TU Muenchen
*)

header {* One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility *}

theory Buffer_adm
imports Buffer Stream_adm
begin

end



theorem cont_BufAC_Asm_F:

  down_cont BufAC_Asm_F

theorem BufAC_Asm_F_stream_monoP:

  stream_monoP BufAC_Asm_F

theorem BufAC_Asm_F_stream_antiP:

  stream_antiP BufAC_Asm_F

theorem adm_non_BufAC_Asm:

  adm (%u. u ∉ BufAC_Asm)

theorem BufAC_Asm_cong:

  [| f ∈ BufEq; ff ∈ BufEq; s ∈ BufAC_Asm |] ==> f·s = ff·s

theorem BufAC_Asm_antiton:

  antitonP BufAC_Asm

theorem BufAC_Cmt_2stream_monoP:

  f ∈ BufEq
  ==> ∃l. ∀i x s.
             s ∈ BufAC_Asm -->
             x << s -->
             Fin (l i) < #x -->
             (x, f·x) ∈ down_iterate BufAC_Cmt_F i -->
             (s, f·s) ∈ down_iterate BufAC_Cmt_F i

theorem BufAC_Cmt_iterate_all:

  (x ∈ BufAC_Cmt) = (∀n. x ∈ down_iterate BufAC_Cmt_F n)

theorem adm_BufAC:

  f ∈ BufEq ==> adm (%s. s ∈ BufAC_Asm --> (s, f·s) ∈ BufAC_Cmt)

theorem Buf_Eq_imp_AC:

  BufEq ⊆ BufAC

theorem adm_BufAC_Asm:

  adm (%x. x ∈ BufAC_Asm)

theorem adm_non_BufAC_Asm':

  adm (%u. u ∉ BufAC_Asm)

theorem adm_BufAC':

  f ∈ BufEq ==> adm (%u. u ∈ BufAC_Asm --> (u, f·u) ∈ BufAC_Cmt)