author | paulson |
Thu, 13 Aug 1998 18:06:40 +0200 | |
changeset 5313 | 1861a564d7e2 |
parent 5277 | e4297d03e5d2 |
child 5340 | d75c03cf77b5 |
permissions | -rw-r--r-- |
4776 | 1 |
(* Title: HOL/UNITY/UNITY |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
The basic UNITY theory (revised version, based upon the "co" operator) |
|
7 |
||
8 |
From Misra, "A Logic for Concurrent Programming", 1994 |
|
9 |
*) |
|
10 |
||
11 |
set proof_timing; |
|
12 |
HOL_quantifiers := false; |
|
13 |
||
14 |
||
15 |
(*** constrains ***) |
|
16 |
||
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
17 |
val prems = Goalw [constrains_def] |
5253 | 18 |
"(!!act s s'. [| act: acts; (s,s') : act; s: A |] ==> s': A') \ |
19 |
\ ==> constrains acts A A'"; |
|
4776 | 20 |
by (blast_tac (claset() addIs prems) 1); |
21 |
qed "constrainsI"; |
|
22 |
||
5069 | 23 |
Goalw [constrains_def] |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
24 |
"[| constrains acts A A'; act: acts; (s,s'): act; s: A |] ==> s': A'"; |
4776 | 25 |
by (Blast_tac 1); |
26 |
qed "constrainsD"; |
|
27 |
||
5253 | 28 |
Goalw [constrains_def] "constrains acts {} B"; |
4776 | 29 |
by (Blast_tac 1); |
30 |
qed "constrains_empty"; |
|
31 |
||
5253 | 32 |
Goalw [constrains_def] "constrains acts A UNIV"; |
4776 | 33 |
by (Blast_tac 1); |
34 |
qed "constrains_UNIV"; |
|
35 |
AddIffs [constrains_empty, constrains_UNIV]; |
|
36 |
||
5069 | 37 |
Goalw [constrains_def] |
5253 | 38 |
"[| constrains acts A A'; A'<=B' |] ==> constrains acts A B'"; |
4776 | 39 |
by (Blast_tac 1); |
40 |
qed "constrains_weaken_R"; |
|
41 |
||
5069 | 42 |
Goalw [constrains_def] |
5253 | 43 |
"[| constrains acts A A'; B<=A |] ==> constrains acts B A'"; |
4776 | 44 |
by (Blast_tac 1); |
45 |
qed "constrains_weaken_L"; |
|
46 |
||
5069 | 47 |
Goalw [constrains_def] |
5253 | 48 |
"[| constrains acts A A'; B<=A; A'<=B' |] ==> constrains acts B B'"; |
4776 | 49 |
by (Blast_tac 1); |
50 |
qed "constrains_weaken"; |
|
51 |
||
52 |
(** Union **) |
|
53 |
||
5069 | 54 |
Goalw [constrains_def] |
5253 | 55 |
"[| constrains acts A A'; constrains acts B B' |] \ |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
56 |
\ ==> constrains acts (A Un B) (A' Un B')"; |
4776 | 57 |
by (Blast_tac 1); |
58 |
qed "constrains_Un"; |
|
59 |
||
5069 | 60 |
Goalw [constrains_def] |
5253 | 61 |
"ALL i:I. constrains acts (A i) (A' i) \ |
62 |
\ ==> constrains acts (UN i:I. A i) (UN i:I. A' i)"; |
|
4776 | 63 |
by (Blast_tac 1); |
64 |
qed "ball_constrains_UN"; |
|
65 |
||
5069 | 66 |
Goalw [constrains_def] |
5253 | 67 |
"[| ALL i. constrains acts (A i) (A' i) |] \ |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
68 |
\ ==> constrains acts (UN i. A i) (UN i. A' i)"; |
4776 | 69 |
by (Blast_tac 1); |
70 |
qed "all_constrains_UN"; |
|
71 |
||
72 |
(** Intersection **) |
|
73 |
||
5069 | 74 |
Goalw [constrains_def] |
5253 | 75 |
"[| constrains acts A A'; constrains acts B B' |] \ |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
76 |
\ ==> constrains acts (A Int B) (A' Int B')"; |
4776 | 77 |
by (Blast_tac 1); |
78 |
qed "constrains_Int"; |
|
79 |
||
5069 | 80 |
Goalw [constrains_def] |
5253 | 81 |
"ALL i:I. constrains acts (A i) (A' i) \ |
82 |
\ ==> constrains acts (INT i:I. A i) (INT i:I. A' i)"; |
|
4776 | 83 |
by (Blast_tac 1); |
84 |
qed "ball_constrains_INT"; |
|
85 |
||
5069 | 86 |
Goalw [constrains_def] |
5253 | 87 |
"[| ALL i. constrains acts (A i) (A' i) |] \ |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
88 |
\ ==> constrains acts (INT i. A i) (INT i. A' i)"; |
4776 | 89 |
by (Blast_tac 1); |
90 |
qed "all_constrains_INT"; |
|
91 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
92 |
Goalw [constrains_def] "[| constrains acts A A'; id: acts |] ==> A<=A'"; |
4776 | 93 |
by (Blast_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
94 |
qed "constrains_imp_subset"; |
4776 | 95 |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
96 |
Goalw [constrains_def] |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
97 |
"[| id: acts; constrains acts A B; constrains acts B C |] \ |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
98 |
\ ==> constrains acts A C"; |
4776 | 99 |
by (Blast_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
100 |
qed "constrains_trans"; |
4776 | 101 |
|
102 |
||
103 |
(*** stable ***) |
|
104 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
105 |
Goalw [stable_def] "constrains acts A A ==> stable acts A"; |
4776 | 106 |
by (assume_tac 1); |
107 |
qed "stableI"; |
|
108 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
109 |
Goalw [stable_def] "stable acts A ==> constrains acts A A"; |
4776 | 110 |
by (assume_tac 1); |
111 |
qed "stableD"; |
|
112 |
||
5069 | 113 |
Goalw [stable_def] |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
114 |
"[| stable acts A; stable acts A' |] ==> stable acts (A Un A')"; |
4776 | 115 |
by (blast_tac (claset() addIs [constrains_Un]) 1); |
116 |
qed "stable_Un"; |
|
117 |
||
5069 | 118 |
Goalw [stable_def] |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
119 |
"[| stable acts A; stable acts A' |] ==> stable acts (A Int A')"; |
4776 | 120 |
by (blast_tac (claset() addIs [constrains_Int]) 1); |
121 |
qed "stable_Int"; |
|
122 |
||
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
123 |
Goalw [stable_def, constrains_def] |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
124 |
"[| stable acts C; constrains acts A (C Un A') |] \ |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
125 |
\ ==> constrains acts (C Un A) (C Un A')"; |
4776 | 126 |
by (Blast_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
127 |
qed "stable_constrains_Un"; |
4776 | 128 |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
129 |
Goalw [stable_def, constrains_def] |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
130 |
"[| stable acts C; constrains acts (C Int A) A' |] \ |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
131 |
\ ==> constrains acts (C Int A) (C Int A')"; |
4776 | 132 |
by (Blast_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
133 |
qed "stable_constrains_Int"; |
4776 | 134 |
|
135 |
||
136 |
(*The Elimination Theorem. The "free" m has become universally quantified! |
|
137 |
Should the premise be !!m instead of ALL m ? Would make it harder to use |
|
138 |
in forward proof.*) |
|
5069 | 139 |
Goalw [constrains_def] |
5253 | 140 |
"[| ALL m. constrains acts {s. s x = m} (B m) |] \ |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
141 |
\ ==> constrains acts {s. s x : M} (UN m:M. B m)"; |
4776 | 142 |
by (Blast_tac 1); |
143 |
qed "elimination"; |
|
144 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
145 |
|
4776 | 146 |
(*As above, but for the trivial case of a one-variable state, in which the |
147 |
state is identified with its one variable.*) |
|
5069 | 148 |
Goalw [constrains_def] |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
149 |
"(ALL m. constrains acts {m} (B m)) ==> constrains acts M (UN m:M. B m)"; |
4776 | 150 |
by (Blast_tac 1); |
151 |
qed "elimination_sing"; |
|
152 |
||
153 |
||
5069 | 154 |
Goalw [constrains_def] |
5253 | 155 |
"[| constrains acts A (A' Un B); constrains acts B B'; id: acts |] \ |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
156 |
\ ==> constrains acts A (A' Un B')"; |
4776 | 157 |
by (Blast_tac 1); |
158 |
qed "constrains_cancel"; |
|
159 |
||
160 |
||
161 |
||
162 |
(*** Theoretical Results from Section 6 ***) |
|
163 |
||
5069 | 164 |
Goalw [constrains_def, strongest_rhs_def] |
5253 | 165 |
"constrains acts A (strongest_rhs acts A )"; |
4776 | 166 |
by (Blast_tac 1); |
167 |
qed "constrains_strongest_rhs"; |
|
168 |
||
5069 | 169 |
Goalw [constrains_def, strongest_rhs_def] |
5253 | 170 |
"constrains acts A B ==> strongest_rhs acts A <= B"; |
4776 | 171 |
by (Blast_tac 1); |
172 |
qed "strongest_rhs_is_strongest"; |