1(*  Title:      HOL/HOLCF/IOA/Deadlock.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>Deadlock freedom of I/O Automata\<close>
6
7theory Deadlock
8imports RefCorrectness CompoScheds
9begin
10
11text \<open>Input actions may always be added to a schedule.\<close>
12
13lemma scheds_input_enabled:
14  "Filter (\<lambda>x. x \<in> act A) \<cdot> sch \<in> schedules A \<Longrightarrow> a \<in> inp A \<Longrightarrow> input_enabled A \<Longrightarrow> Finite sch
15    \<Longrightarrow> Filter (\<lambda>x. x \<in> act A) \<cdot> sch @@ a \<leadsto> nil \<in> schedules A"
16  apply (simp add: schedules_def has_schedule_def)
17  apply auto
18  apply (frule inp_is_act)
19  apply (simp add: executions_def)
20  apply (pair ex)
21  apply (rename_tac s ex)
22  apply (subgoal_tac "Finite ex")
23  prefer 2
24  apply (simp add: filter_act_def)
25  defer
26  apply (rule_tac [2] Map2Finite [THEN iffD1])
27  apply (rule_tac [2] t = "Map fst \<cdot> ex" in subst)
28  prefer 2
29  apply assumption
30  apply (erule_tac [2] FiniteFilter)
31  text \<open>subgoal 1\<close>
32  apply (frule exists_laststate)
33  apply (erule allE)
34  apply (erule exE)
35  text \<open>using input-enabledness\<close>
36  apply (simp add: input_enabled_def)
37  apply (erule conjE)+
38  apply (erule_tac x = "a" in allE)
39  apply simp
40  apply (erule_tac x = "u" in allE)
41  apply (erule exE)
42  text \<open>instantiate execution\<close>
43  apply (rule_tac x = " (s, ex @@ (a, s2) \<leadsto> nil) " in exI)
44  apply (simp add: filter_act_def MapConc)
45  apply (erule_tac t = "u" in lemma_2_1)
46  apply simp
47  apply (rule sym)
48  apply assumption
49  done
50
51text \<open>
52  Deadlock freedom: component B cannot block an out or int action of component
53  A in every schedule.
54
55  Needs compositionality on schedule level, input-enabledness, compatibility
56  and distributivity of \<open>is_exec_frag\<close> over \<open>@@\<close>.
57\<close>
58
59lemma IOA_deadlock_free:
60  assumes "a \<in> local A"
61    and "Finite sch"
62    and "sch \<in> schedules (A \<parallel> B)"
63    and "Filter (\<lambda>x. x \<in> act A) \<cdot> (sch @@ a \<leadsto> nil) \<in> schedules A"
64    and "compatible A B"
65    and "input_enabled B"
66  shows "(sch @@ a \<leadsto> nil) \<in> schedules (A \<parallel> B)"
67  supply if_split [split del]
68  apply (insert assms)
69  apply (simp add: compositionality_sch locals_def)
70  apply (rule conjI)
71  text \<open>\<open>a \<in> act (A \<parallel> B)\<close>\<close>
72  prefer 2
73  apply (simp add: actions_of_par)
74  apply (blast dest: int_is_act out_is_act)
75
76  text \<open>\<open>Filter B (sch @@ [a]) \<in> schedules B\<close>\<close>
77  apply (case_tac "a \<in> int A")
78  apply (drule intA_is_not_actB)
79  apply (assumption) (* \<longrightarrow> a \<notin> act B *)
80  apply simp
81
82  text \<open>case \<open>a \<notin> int A\<close>, i.e. \<open>a \<in> out A\<close>\<close>
83  apply (case_tac "a \<notin> act B")
84  apply simp
85  text \<open>case \<open>a \<in> act B\<close>\<close>
86  apply simp
87  apply (subgoal_tac "a \<in> out A")
88  prefer 2
89  apply blast
90  apply (drule outAactB_is_inpB)
91  apply assumption
92  apply assumption
93  apply (rule scheds_input_enabled)
94  apply simp
95  apply assumption+
96  done
97
98end
99