# Theory Deadlock

Up to index of Isabelle/HOLCF/IOA

theory Deadlock
imports RefCorrectness CompoScheds
uses [Deadlock.ML]
begin

    (*  Title:      HOLCF/IOA/meta_theory/Deadlock.thy
        ID:         $Id: Deadlock.thy,v 1.5 2005/09/02 15:24:01 wenzelm Exp $
        Author:     Olaf Müller
    *)

    header {* Deadlock freedom of I/O Automata *}

    theory Deadlock
    imports RefCorrectness CompoScheds
    begin

    end

theorem scheds_input_enabled:

      [| Filter (%x. x ∈ act A)·sch ∈ schedules A; a ∈ inp A; input_enabled A;
         Finite sch |]
      ==> Filter (%x. x ∈ act A)·sch @@ [a!] ∈ schedules A

theorem IOA_deadlock_free:

      [| a ∈ local A; Finite sch; sch ∈ schedules (A || B);
         Filter (%x. x ∈ act A)·(sch @@ [a!]) ∈ schedules A; compatible A B;
         input_enabled B |]
      ==> sch @@ [a!] ∈ schedules (A || B)