author | paulson |
Thu, 06 Aug 1998 15:47:26 +0200 | |
changeset 5277 | e4297d03e5d2 |
parent 5253 | 82a5ca6290aa |
child 5313 | 1861a564d7e2 |
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] |
5253 | 24 |
"[| constrains acts A A'; act: acts; (s,s'): act; s: A |] \ |
4776 | 25 |
\ ==> s': A'"; |
26 |
by (Blast_tac 1); |
|
27 |
qed "constrainsD"; |
|
28 |
||
5253 | 29 |
Goalw [constrains_def] "constrains acts {} B"; |
4776 | 30 |
by (Blast_tac 1); |
31 |
qed "constrains_empty"; |
|
32 |
||
5253 | 33 |
Goalw [constrains_def] "constrains acts A UNIV"; |
4776 | 34 |
by (Blast_tac 1); |
35 |
qed "constrains_UNIV"; |
|
36 |
AddIffs [constrains_empty, constrains_UNIV]; |
|
37 |
||
5069 | 38 |
Goalw [constrains_def] |
5253 | 39 |
"[| constrains acts A A'; A'<=B' |] ==> constrains acts A B'"; |
4776 | 40 |
by (Blast_tac 1); |
41 |
qed "constrains_weaken_R"; |
|
42 |
||
5069 | 43 |
Goalw [constrains_def] |
5253 | 44 |
"[| constrains acts A A'; B<=A |] ==> constrains acts B A'"; |
4776 | 45 |
by (Blast_tac 1); |
46 |
qed "constrains_weaken_L"; |
|
47 |
||
5069 | 48 |
Goalw [constrains_def] |
5253 | 49 |
"[| constrains acts A A'; B<=A; A'<=B' |] ==> constrains acts B B'"; |
4776 | 50 |
by (Blast_tac 1); |
51 |
qed "constrains_weaken"; |
|
52 |
||
53 |
(** Union **) |
|
54 |
||
5069 | 55 |
Goalw [constrains_def] |
5253 | 56 |
"[| 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
|
57 |
\ ==> constrains acts (A Un B) (A' Un B')"; |
4776 | 58 |
by (Blast_tac 1); |
59 |
qed "constrains_Un"; |
|
60 |
||
5069 | 61 |
Goalw [constrains_def] |
5253 | 62 |
"ALL i:I. constrains acts (A i) (A' i) \ |
63 |
\ ==> constrains acts (UN i:I. A i) (UN i:I. A' i)"; |
|
4776 | 64 |
by (Blast_tac 1); |
65 |
qed "ball_constrains_UN"; |
|
66 |
||
5069 | 67 |
Goalw [constrains_def] |
5253 | 68 |
"[| 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
|
69 |
\ ==> constrains acts (UN i. A i) (UN i. A' i)"; |
4776 | 70 |
by (Blast_tac 1); |
71 |
qed "all_constrains_UN"; |
|
72 |
||
73 |
(** Intersection **) |
|
74 |
||
5069 | 75 |
Goalw [constrains_def] |
5253 | 76 |
"[| 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
|
77 |
\ ==> constrains acts (A Int B) (A' Int B')"; |
4776 | 78 |
by (Blast_tac 1); |
79 |
qed "constrains_Int"; |
|
80 |
||
5069 | 81 |
Goalw [constrains_def] |
5253 | 82 |
"ALL i:I. constrains acts (A i) (A' i) \ |
83 |
\ ==> constrains acts (INT i:I. A i) (INT i:I. A' i)"; |
|
4776 | 84 |
by (Blast_tac 1); |
85 |
qed "ball_constrains_INT"; |
|
86 |
||
5069 | 87 |
Goalw [constrains_def] |
5253 | 88 |
"[| 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
|
89 |
\ ==> constrains acts (INT i. A i) (INT i. A' i)"; |
4776 | 90 |
by (Blast_tac 1); |
91 |
qed "all_constrains_INT"; |
|
92 |
||
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
93 |
Goalw [constrains_def] |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
94 |
"[| constrains acts A A'; id: acts |] ==> A<=A'"; |
4776 | 95 |
by (Blast_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
96 |
qed "constrains_imp_subset"; |
4776 | 97 |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
98 |
Goalw [constrains_def] |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
99 |
"[| 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
|
100 |
\ ==> constrains acts A C"; |
4776 | 101 |
by (Blast_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
102 |
qed "constrains_trans"; |
4776 | 103 |
|
104 |
||
105 |
(*** stable ***) |
|
106 |
||
5069 | 107 |
Goalw [stable_def] |
5253 | 108 |
"constrains acts A A ==> stable acts A"; |
4776 | 109 |
by (assume_tac 1); |
110 |
qed "stableI"; |
|
111 |
||
5069 | 112 |
Goalw [stable_def] |
5253 | 113 |
"stable acts A ==> constrains acts A A"; |
4776 | 114 |
by (assume_tac 1); |
115 |
qed "stableD"; |
|
116 |
||
5069 | 117 |
Goalw [stable_def] |
5253 | 118 |
"[| stable acts A; stable acts A' |] \ |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
119 |
\ ==> stable acts (A Un A')"; |
4776 | 120 |
by (blast_tac (claset() addIs [constrains_Un]) 1); |
121 |
qed "stable_Un"; |
|
122 |
||
5069 | 123 |
Goalw [stable_def] |
5253 | 124 |
"[| stable acts A; stable acts A' |] \ |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
125 |
\ ==> stable acts (A Int A')"; |
4776 | 126 |
by (blast_tac (claset() addIs [constrains_Int]) 1); |
127 |
qed "stable_Int"; |
|
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 A (C Un A') |] \ |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
131 |
\ ==> constrains acts (C Un A) (C Un 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_Un"; |
4776 | 134 |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
135 |
Goalw [stable_def, constrains_def] |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
136 |
"[| 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
|
137 |
\ ==> constrains acts (C Int A) (C Int A')"; |
4776 | 138 |
by (Blast_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
139 |
qed "stable_constrains_Int"; |
4776 | 140 |
|
141 |
||
142 |
(*The Elimination Theorem. The "free" m has become universally quantified! |
|
143 |
Should the premise be !!m instead of ALL m ? Would make it harder to use |
|
144 |
in forward proof.*) |
|
5069 | 145 |
Goalw [constrains_def] |
5253 | 146 |
"[| ALL m. constrains acts {s. s x = m} (B m) |] \ |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
147 |
\ ==> constrains acts {s. P(s x)} (UN m. {s. P(m)} Int B m)"; |
4776 | 148 |
by (Blast_tac 1); |
149 |
qed "elimination"; |
|
150 |
||
151 |
(*As above, but for the trivial case of a one-variable state, in which the |
|
152 |
state is identified with its one variable.*) |
|
5069 | 153 |
Goalw [constrains_def] |
5253 | 154 |
"[| ALL m. constrains acts {m} (B m) |] \ |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
155 |
\ ==> constrains acts {s. P s} (UN m. {s. P(m)} Int B m)"; |
4776 | 156 |
by (Blast_tac 1); |
157 |
qed "elimination_sing"; |
|
158 |
||
159 |
||
5069 | 160 |
Goalw [constrains_def] |
5253 | 161 |
"[| 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
|
162 |
\ ==> constrains acts A (A' Un B')"; |
4776 | 163 |
by (Blast_tac 1); |
164 |
qed "constrains_cancel"; |
|
165 |
||
166 |
||
167 |
||
168 |
(*** Theoretical Results from Section 6 ***) |
|
169 |
||
5069 | 170 |
Goalw [constrains_def, strongest_rhs_def] |
5253 | 171 |
"constrains acts A (strongest_rhs acts A )"; |
4776 | 172 |
by (Blast_tac 1); |
173 |
qed "constrains_strongest_rhs"; |
|
174 |
||
5069 | 175 |
Goalw [constrains_def, strongest_rhs_def] |
5253 | 176 |
"constrains acts A B ==> strongest_rhs acts A <= B"; |
4776 | 177 |
by (Blast_tac 1); |
178 |
qed "strongest_rhs_is_strongest"; |