diff -r ec2f0dad8b98 -r 7355fd313cf8 src/HOL/HOLCF/IOA/Deadlock.thy
--- 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