4 Copyright 2000 University of Cambridge |
4 Copyright 2000 University of Cambridge |
5 |
5 |
6 Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo |
6 Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo |
7 *) |
7 *) |
8 |
8 |
9 Detects = WFair + Reach + |
9 theory Detects = FP + SubstAx: |
10 |
|
11 |
10 |
12 consts |
11 consts |
13 op_Detects :: "['a set, 'a set] => 'a program set" (infixl "Detects" 60) |
12 op_Detects :: "['a set, 'a set] => 'a program set" (infixl "Detects" 60) |
14 op_Equality :: "['a set, 'a set] => 'a set" (infixl "<==>" 60) |
13 op_Equality :: "['a set, 'a set] => 'a set" (infixl "<==>" 60) |
15 |
14 |
16 defs |
15 defs |
17 Detects_def "A Detects B == (Always (-A Un B)) Int (B LeadsTo A)" |
16 Detects_def: "A Detects B == (Always (-A Un B)) Int (B LeadsTo A)" |
18 Equality_def "A <==> B == (-A Un B) Int (A Un -B)" |
17 Equality_def: "A <==> B == (-A Un B) Int (A Un -B)" |
|
18 |
|
19 |
|
20 (* Corollary from Sectiom 3.6.4 *) |
|
21 |
|
22 lemma Always_at_FP: "F: A LeadsTo B ==> F : Always (-((FP F) Int A Int -B))" |
|
23 apply (rule LeadsTo_empty) |
|
24 apply (subgoal_tac "F : (FP F Int A Int - B) LeadsTo (B Int (FP F Int -B))") |
|
25 apply (subgoal_tac [2] " (FP F Int A Int - B) = (A Int (FP F Int -B))") |
|
26 apply (subgoal_tac "(B Int (FP F Int -B)) = {}") |
|
27 apply auto |
|
28 apply (blast intro: PSP_Stable stable_imp_Stable stable_FP_Int) |
|
29 done |
|
30 |
|
31 |
|
32 lemma Detects_Trans: |
|
33 "[| F : A Detects B; F : B Detects C |] ==> F : A Detects C" |
|
34 apply (unfold Detects_def Int_def) |
|
35 apply (simp (no_asm)) |
|
36 apply safe |
|
37 apply (rule_tac [2] LeadsTo_Trans) |
|
38 apply auto |
|
39 apply (subgoal_tac "F : Always ((-A Un B) Int (-B Un C))") |
|
40 apply (blast intro: Always_weaken) |
|
41 apply (simp add: Always_Int_distrib) |
|
42 done |
|
43 |
|
44 lemma Detects_refl: "F : A Detects A" |
|
45 apply (unfold Detects_def) |
|
46 apply (simp (no_asm) add: Un_commute Compl_partition subset_imp_LeadsTo) |
|
47 done |
|
48 |
|
49 lemma Detects_eq_Un: "(A<==>B) = (A Int B) Un (-A Int -B)" |
|
50 apply (unfold Equality_def) |
|
51 apply blast |
|
52 done |
|
53 |
|
54 (*Not quite antisymmetry: sets A and B agree in all reachable states *) |
|
55 lemma Detects_antisym: |
|
56 "[| F : A Detects B; F : B Detects A|] ==> F : Always (A <==> B)" |
|
57 apply (unfold Detects_def Equality_def) |
|
58 apply (simp add: Always_Int_I Un_commute) |
|
59 done |
|
60 |
|
61 |
|
62 (* Theorem from Section 3.8 *) |
|
63 |
|
64 lemma Detects_Always: |
|
65 "F : A Detects B ==> F : Always ((-(FP F)) Un (A <==> B))" |
|
66 apply (unfold Detects_def Equality_def) |
|
67 apply (simp (no_asm) add: Un_Int_distrib Always_Int_distrib) |
|
68 apply (blast dest: Always_at_FP intro: Always_weaken) |
|
69 done |
|
70 |
|
71 (* Theorem from exercise 11.1 Section 11.3.1 *) |
|
72 |
|
73 lemma Detects_Imp_LeadstoEQ: |
|
74 "F : A Detects B ==> F : UNIV LeadsTo (A <==> B)" |
|
75 apply (unfold Detects_def Equality_def) |
|
76 apply (rule_tac B = "B" in LeadsTo_Diff) |
|
77 prefer 2 apply (blast intro: Always_LeadsTo_weaken) |
|
78 apply (blast intro: Always_LeadsToI subset_imp_LeadsTo) |
|
79 done |
|
80 |
19 |
81 |
20 end |
82 end |
21 |
83 |