src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 42151 4da4fc77664b
child 61999 89291b5d0ede
permissions -rw-r--r--
modernized header;
     1 (*  Title:      HOL/HOLCF/IOA/meta_theory/Deadlock.thy
     2     Author:     Olaf Müller
     3 *)
     4 
     5 section {* Deadlock freedom of I/O Automata *}
     6 
     7 theory Deadlock
     8 imports RefCorrectness CompoScheds
     9 begin
    10 
    11 text {* input actions may always be added to a schedule *}
    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>>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 {* pair_tac @{context} "ex" 1 *})
    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) >>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 {*
    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 *}
    56 
    57 declare split_if [split del]
    58 lemma IOA_deadlock_free: "[| a : local A; Finite sch; sch : schedules (A||B);  
    59              Filter (%x. x:act A)$(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |]  
    60            ==> (sch @@ a>>nil) : schedules (A||B)"
    61 apply (simp add: compositionality_sch locals_def)
    62 apply (rule conjI)
    63 (* a : act (A||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