--- a/src/HOL/HOLCF/IOA/Deadlock.thy Tue Jan 12 20:05:53 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Deadlock.thy Tue Jan 12 23:40:33 2016 +0100
@@ -8,85 +8,91 @@
imports RefCorrectness CompoScheds
begin
-text \<open>input actions may always be added to a schedule\<close>
+text \<open>Input actions may always be added to a schedule.\<close>
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\<leadsto>nil : schedules A"
-apply (simp add: schedules_def has_schedule_def)
-apply auto
-apply (frule inp_is_act)
-apply (simp add: executions_def)
-apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-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)
-(* subgoal 1 *)
-apply (frule exists_laststate)
-apply (erule allE)
-apply (erule exE)
-(* 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)
-(* instantiate execution *)
-apply (rule_tac x = " (s,ex @@ (a,s2) \<leadsto>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
+ "Filter (\<lambda>x. x \<in> act A) $ sch \<in> schedules A \<Longrightarrow> a \<in> inp A \<Longrightarrow> input_enabled A \<Longrightarrow> Finite sch
+ \<Longrightarrow> Filter (\<lambda>x. x \<in> act A) $ sch @@ a \<leadsto> nil \<in> schedules A"
+ apply (simp add: schedules_def has_schedule_def)
+ apply auto
+ apply (frule inp_is_act)
+ apply (simp add: executions_def)
+ apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+ 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 \<open>subgoal 1\<close>
+ apply (frule exists_laststate)
+ apply (erule allE)
+ apply (erule exE)
+ text \<open>using input-enabledness\<close>
+ 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 \<open>instantiate execution\<close>
+ apply (rule_tac x = " (s, ex @@ (a, s2) \<leadsto> 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 \<open>
- 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 @@
+ 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 \<open>is_exec_frag\<close> over \<open>@@\<close>.
\<close>
-declare split_if [split del]
-lemma IOA_deadlock_free: "[| a : local A; Finite sch; sch : schedules (A\<parallel>B);
- Filter (%x. x:act A)$(sch @@ a\<leadsto>nil) : schedules A; compatible A B; input_enabled B |]
- ==> (sch @@ a\<leadsto>nil) : schedules (A\<parallel>B)"
-apply (simp add: compositionality_sch locals_def)
-apply (rule conjI)
-(* a : act (A\<parallel>B) *)
-prefer 2
-apply (simp add: actions_of_par)
-apply (blast dest: int_is_act out_is_act)
-
-(* Filter B (sch@@[a]) : schedules B *)
+lemma IOA_deadlock_free:
+ assumes "a \<in> local A"
+ and "Finite sch"
+ and "sch \<in> schedules (A \<parallel> B)"
+ and "Filter (\<lambda>x. x \<in> act A) $ (sch @@ a \<leadsto> nil) \<in> schedules A"
+ and "compatible A B"
+ and "input_enabled B"
+ shows "(sch @@ a \<leadsto> nil) \<in> schedules (A \<parallel> B)"
+ supply split_if [split del]
+ apply (insert assms)
+ apply (simp add: compositionality_sch locals_def)
+ apply (rule conjI)
+ text \<open>\<open>a \<in> act (A \<parallel> B)\<close>\<close>
+ prefer 2
+ apply (simp add: actions_of_par)
+ apply (blast dest: int_is_act out_is_act)
-apply (case_tac "a:int A")
-apply (drule intA_is_not_actB)
-apply (assumption) (* --> a~:act B *)
-apply simp
+ text \<open>\<open>Filter B (sch @@ [a]) \<in> schedules B\<close>\<close>
+ apply (case_tac "a \<in> int A")
+ apply (drule intA_is_not_actB)
+ apply (assumption) (* \<longrightarrow> a \<notin> act B *)
+ apply simp
-(* case a~:int A , i.e. a:out A *)
-apply (case_tac "a~:act B")
-apply simp
-(* 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
-
-declare split_if [split]
+ text \<open>case \<open>a \<notin> int A\<close>, i.e. \<open>a \<in> out A\<close>\<close>
+ apply (case_tac "a \<notin> act B")
+ apply simp
+ text \<open>case \<open>a \<in> act B\<close>\<close>
+ apply simp
+ apply (subgoal_tac "a \<in> 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