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