|
1 (* Title: HOL/HOLCF/IOA/Deadlock.thy |
|
2 Author: Olaf Müller |
|
3 *) |
|
4 |
|
5 section \<open>Deadlock freedom of I/O Automata\<close> |
|
6 |
|
7 theory Deadlock |
|
8 imports RefCorrectness CompoScheds |
|
9 begin |
|
10 |
|
11 text \<open>input actions may always be added to a schedule\<close> |
|
12 |
|
13 lemma scheds_input_enabled: |
|
14 "[| Filter (%x. x:act A)$sch : schedules A; a:inp A; input_enabled A; Finite sch|] |
|
15 ==> Filter (%x. x:act A)$sch @@ a\<leadsto>nil : 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 (tactic \<open>pair_tac @{context} "ex" 1\<close>) |
|
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$ex" in subst) |
|
28 prefer 2 apply (assumption) |
|
29 apply (erule_tac [2] FiniteFilter) |
|
30 (* subgoal 1 *) |
|
31 apply (frule exists_laststate) |
|
32 apply (erule allE) |
|
33 apply (erule exE) |
|
34 (* using input-enabledness *) |
|
35 apply (simp add: input_enabled_def) |
|
36 apply (erule conjE)+ |
|
37 apply (erule_tac x = "a" in allE) |
|
38 apply simp |
|
39 apply (erule_tac x = "u" in allE) |
|
40 apply (erule exE) |
|
41 (* instantiate execution *) |
|
42 apply (rule_tac x = " (s,ex @@ (a,s2) \<leadsto>nil) " in exI) |
|
43 apply (simp add: filter_act_def MapConc) |
|
44 apply (erule_tac t = "u" in lemma_2_1) |
|
45 apply simp |
|
46 apply (rule sym) |
|
47 apply assumption |
|
48 done |
|
49 |
|
50 text \<open> |
|
51 Deadlock freedom: component B cannot block an out or int action |
|
52 of component A in every schedule. |
|
53 Needs compositionality on schedule level, input-enabledness, compatibility |
|
54 and distributivity of is_exec_frag over @@ |
|
55 \<close> |
|
56 |
|
57 declare split_if [split del] |
|
58 lemma IOA_deadlock_free: "[| a : local A; Finite sch; sch : schedules (A\<parallel>B); |
|
59 Filter (%x. x:act A)$(sch @@ a\<leadsto>nil) : schedules A; compatible A B; input_enabled B |] |
|
60 ==> (sch @@ a\<leadsto>nil) : schedules (A\<parallel>B)" |
|
61 apply (simp add: compositionality_sch locals_def) |
|
62 apply (rule conjI) |
|
63 (* a : act (A\<parallel>B) *) |
|
64 prefer 2 |
|
65 apply (simp add: actions_of_par) |
|
66 apply (blast dest: int_is_act out_is_act) |
|
67 |
|
68 (* Filter B (sch@@[a]) : schedules B *) |
|
69 |
|
70 apply (case_tac "a:int A") |
|
71 apply (drule intA_is_not_actB) |
|
72 apply (assumption) (* --> a~:act B *) |
|
73 apply simp |
|
74 |
|
75 (* case a~:int A , i.e. a:out A *) |
|
76 apply (case_tac "a~:act B") |
|
77 apply simp |
|
78 (* case a:act B *) |
|
79 apply simp |
|
80 apply (subgoal_tac "a:out A") |
|
81 prefer 2 apply (blast) |
|
82 apply (drule outAactB_is_inpB) |
|
83 apply assumption |
|
84 apply assumption |
|
85 apply (rule scheds_input_enabled) |
|
86 apply simp |
|
87 apply assumption+ |
|
88 done |
|
89 |
|
90 declare split_if [split] |
|
91 |
|
92 end |