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