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 Asch ∈ schedules A; a ∈ inp A; input_enabled A;
     Finite sch |]
  ==> Filter (%x. x ∈ act Asch @@ [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)