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