src/HOLCF/IOA/meta_theory/Deadlock.ML
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 7499 23e090051cb8
child 12218 6597093b77e7
permissions -rw-r--r--
` -> $
     1 (*  Title:      HOLCF/IOA/meta_theory/Deadlock.ML
     2     ID:         $Id$
     3     Author:     Olaf Mueller
     4     Copyright   1997 TU Muenchen
     5 
     6 Deadlock freedom of I/O Automata
     7 *)   
     8 
     9 (********************************************************************************
    10                input actions may always be added to a schedule
    11 **********************************************************************************)
    12 
    13 Goal "[| Filter (%x. x:act A)$sch : schedules A; a:inp A; input_enabled A; Finite sch|] \
    14 \         ==> Filter (%x. x:act A)$sch @@ a>>nil : schedules A";
    15 by (asm_full_simp_tac (simpset() addsimps [schedules_def,has_schedule_def]) 1);
    16 by (safe_tac set_cs);
    17 by (ftac inp_is_act 1);
    18 by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
    19 by (pair_tac "ex" 1);
    20 ren "s ex" 1;
    21 by (subgoal_tac "Finite ex" 1);
    22 by (asm_full_simp_tac (simpset() addsimps [filter_act_def]) 2);
    23 by (rtac (Map2Finite RS iffD1) 2);
    24 by (res_inst_tac [("t","Map fst$ex")] subst 2);
    25 by (assume_tac 2);
    26 by (etac FiniteFilter 2);
    27 (* subgoal 1 *)
    28 by (ftac exists_laststate 1);
    29 by (etac allE 1);
    30 by (etac exE 1);
    31 (* using input-enabledness *)
    32 by (asm_full_simp_tac (simpset() addsimps [input_enabled_def]) 1);
    33 by (REPEAT (etac conjE 1));
    34 by (eres_inst_tac [("x","a")] allE 1);
    35 by (Asm_full_simp_tac 1);
    36 by (eres_inst_tac [("x","u")] allE 1);
    37 by (etac exE 1);
    38 (* instantiate execution *)
    39 by (res_inst_tac [("x","(s,ex @@ (a,s2)>>nil)")] exI 1);
    40 by (asm_full_simp_tac (simpset() addsimps [filter_act_def,MapConc]) 1);
    41 by (eres_inst_tac [("t","u")] lemma_2_1 1);
    42 by (Asm_full_simp_tac 1);
    43 by (rtac sym 1);
    44 by (assume_tac 1);
    45 qed"scheds_input_enabled";
    46 
    47 (********************************************************************************
    48                Deadlock freedom: component B cannot block an out or int action
    49                                  of component A in every schedule.
    50     Needs compositionality on schedule level, input-enabledness, compatibility
    51                     and distributivity of is_exec_frag over @@
    52 **********************************************************************************)
    53 Delsplits [split_if];
    54 Goal "[| a : local A; Finite sch; sch : schedules (A||B); \
    55 \            Filter (%x. x:act A)$(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
    56 \          ==> (sch @@ a>>nil) : schedules (A||B)";
    57 
    58 by (asm_full_simp_tac (simpset() addsimps [compositionality_sch,locals_def]) 1);
    59 by (rtac conjI 1);
    60 (* a : act (A||B) *)
    61 by (asm_full_simp_tac (simpset() addsimps [actions_of_par]) 2);
    62 by (blast_tac (claset() addDs [int_is_act,out_is_act]) 2);
    63 
    64 (* Filter B (sch@@[a]) : schedules B *)
    65 
    66 by (case_tac "a:int A" 1);
    67 by (dtac intA_is_not_actB 1);
    68 by (assume_tac 1);  (* --> a~:act B *)
    69 by (Asm_full_simp_tac 1);
    70 
    71 (* case a~:int A , i.e. a:out A *)
    72 by (case_tac "a~:act B" 1);
    73 by (Asm_full_simp_tac 1);
    74 (* case a:act B *)
    75 by (Asm_full_simp_tac 1);
    76 by (subgoal_tac "a:out A" 1);
    77 by (Blast_tac 2);
    78 by (dtac outAactB_is_inpB 1);
    79 by (assume_tac 1);
    80 by (assume_tac 1);
    81 by (rtac scheds_input_enabled 1);
    82 by (Asm_full_simp_tac 1);
    83 by (REPEAT (atac 1));
    84 qed"IOA_deadlock_free";
    85 
    86 Addsplits [split_if];
    87 
    88 
    89 
    90