Up to index of Isabelle/HOLCF/IOA
theory Deadlock(* 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)