8334
|
1 |
(* Title: HOL/UNITY/Detects
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tanja Vos, Cambridge University Computer Laboratory
|
|
4 |
Copyright 2000 University of Cambridge
|
|
5 |
|
|
6 |
Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
|
|
7 |
*)
|
|
8 |
|
|
9 |
(* Corollary from Sectiom 3.6.4 *)
|
|
10 |
|
|
11 |
Goal "F: A LeadsTo B ==> F : Always (-((FP F) Int A Int -B))";
|
|
12 |
by (rtac LeadsTo_empty 1);
|
|
13 |
by (subgoal_tac "F : (FP F Int A Int - B) LeadsTo (B Int (FP F Int -B))" 1);
|
|
14 |
by (subgoal_tac "(FP F Int A Int - B) = (A Int (FP F Int -B))" 2);
|
|
15 |
by (subgoal_tac "(B Int (FP F Int -B)) = {}" 1);
|
|
16 |
by Auto_tac;
|
|
17 |
by (blast_tac (claset() addIs [PSP_Stable, stable_imp_Stable,
|
|
18 |
stable_FP_Int]) 1);
|
|
19 |
qed "Always_at_FP";
|
|
20 |
|
|
21 |
|
|
22 |
Goalw [Detects_def, Int_def]
|
|
23 |
"[| F : A Detects B; F : B Detects C |] ==> F : A Detects C";
|
|
24 |
by (Simp_tac 1);
|
|
25 |
by Safe_tac;
|
|
26 |
by (rtac LeadsTo_Trans 2);
|
|
27 |
by Auto_tac;
|
|
28 |
by (subgoal_tac "F : Always ((-A Un B) Int (-B Un C))" 1);
|
|
29 |
by (simp_tac (simpset() addsimps [Always_Int_distrib]) 2);
|
|
30 |
by Auto_tac;
|
|
31 |
by (blast_tac (claset() addIs [Always_weaken]) 1);
|
|
32 |
qed "Detects_Trans";
|
|
33 |
|
|
34 |
|
|
35 |
Goalw [Detects_def] "F : A Detects A";
|
|
36 |
by (simp_tac (simpset() addsimps [Un_commute, Compl_partition,
|
|
37 |
subset_imp_LeadsTo]) 1);
|
|
38 |
qed "Detects_refl";
|
|
39 |
|
|
40 |
Goalw [Equality_def] "(A<==>B) = (A Int B) Un (-A Int -B)";
|
|
41 |
by (Blast_tac 1);
|
|
42 |
qed "Detects_eq_Un";
|
|
43 |
|
|
44 |
(*Not quite antisymmetry: sets A and B agree in all reachable states *)
|
|
45 |
Goalw [Detects_def, Equality_def]
|
|
46 |
"[| F : A Detects B; F : B Detects A|] ==> F : Always (A <==> B)";
|
|
47 |
by (asm_full_simp_tac (simpset() addsimps [Always_Int_I, Un_commute]) 1);
|
|
48 |
qed "Detects_antisym";
|
|
49 |
|
|
50 |
|
|
51 |
(* Theorem from Section 3.8 *)
|
|
52 |
|
|
53 |
Goalw [Detects_def, Equality_def]
|
|
54 |
"F : A Detects B ==> F : Always ((-(FP F)) Un (A <==> B))";
|
|
55 |
by (simp_tac (simpset() addsimps [Un_Int_distrib, Always_Int_distrib]) 1);
|
|
56 |
by (blast_tac (claset() addDs [Always_at_FP]
|
|
57 |
addIs [Always_weaken]) 1);
|
|
58 |
qed "Detects_Always";
|
|
59 |
|
|
60 |
(* Theorem from exercise 11.1 Section 11.3.1 *)
|
|
61 |
|
|
62 |
Goalw [Detects_def, Equality_def]
|
|
63 |
"F : A Detects B ==> F : UNIV LeadsTo (A <==> B)";
|
|
64 |
by (res_inst_tac [("B", "B")] LeadsTo_Diff 1);
|
|
65 |
by (blast_tac (claset() addIs [Always_LeadsTo_weaken]) 2);
|
|
66 |
by (blast_tac (claset() addIs [Always_LeadsToI, subset_imp_LeadsTo]) 1);
|
|
67 |
qed "Detects_Imp_LeadstoEQ";
|
|
68 |
|
|
69 |
|