# 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)