imports RefCorrectness CompoScheds
```(*  Title:      HOL/HOLCF/IOA/Deadlock.thy
Author:     Olaf MÃ¼ller
*)

section ‹Deadlock freedom of I/O Automata›

imports RefCorrectness CompoScheds
begin

text ‹Input actions may always be added to a schedule.›

lemma 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 ↝ nil ∈ schedules A"
apply (simp add: schedules_def has_schedule_def)
apply auto
apply (frule inp_is_act)
apply (simp add: executions_def)
apply (pair ex)
apply (rename_tac s ex)
apply (subgoal_tac "Finite ex")
prefer 2
apply (simp add: filter_act_def)
defer
apply (rule_tac [2] Map2Finite [THEN iffD1])
apply (rule_tac [2] t = "Map fst ⋅ ex" in subst)
prefer 2
apply assumption
apply (erule_tac [2] FiniteFilter)
text ‹subgoal 1›
apply (frule exists_laststate)
apply (erule allE)
apply (erule exE)
text ‹using input-enabledness›
apply (simp add: input_enabled_def)
apply (erule conjE)+
apply (erule_tac x = "a" in allE)
apply simp
apply (erule_tac x = "u" in allE)
apply (erule exE)
text ‹instantiate execution›
apply (rule_tac x = " (s, ex @@ (a, s2) ↝ nil) " in exI)
apply (simp add: filter_act_def MapConc)
apply (erule_tac t = "u" in lemma_2_1)
apply simp
apply (rule sym)
apply assumption
done

text ‹
Deadlock freedom: component B cannot block an out or int action of component
A in every schedule.

Needs compositionality on schedule level, input-enabledness, compatibility
and distributivity of ‹is_exec_frag› over ‹@@›.
›

assumes "a ∈ local A"
and "Finite sch"
and "sch ∈ schedules (A ∥ B)"
and "Filter (λx. x ∈ act A) ⋅ (sch @@ a ↝ nil) ∈ schedules A"
and "compatible A B"
and "input_enabled B"
shows "(sch @@ a ↝ nil) ∈ schedules (A ∥ B)"
supply if_split [split del]
apply (insert assms)
apply (simp add: compositionality_sch locals_def)
apply (rule conjI)
text ‹‹a ∈ act (A ∥ B)››
prefer 2
apply (simp add: actions_of_par)
apply (blast dest: int_is_act out_is_act)

text ‹‹Filter B (sch @@ [a]) ∈ schedules B››
apply (case_tac "a ∈ int A")
apply (drule intA_is_not_actB)
apply (assumption) (* ⟶ a ∉ act B *)
apply simp

text ‹case ‹a ∉ int A›, i.e. ‹a ∈ out A››
apply (case_tac "a ∉ act B")
apply simp
text ‹case ‹a ∈ act B››
apply simp
apply (subgoal_tac "a ∈ out A")
prefer 2
apply blast
apply (drule outAactB_is_inpB)
apply assumption
apply assumption
apply (rule scheds_input_enabled)
apply simp
apply assumption+
done

end
```