author | paulson |
Tue, 13 Oct 1998 10:55:33 +0200 | |
changeset 5639 | 29d8e53a4920 |
parent 5620 | 3ac11c4af76a |
child 5648 | fe887910e32e |
permissions | -rw-r--r-- |
5252 | 1 |
(* Title: HOL/UNITY/Union.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Unions of programs |
|
7 |
||
8 |
From Misra's Chapter 5: Asynchronous Compositions of Programs |
|
9 |
*) |
|
10 |
||
11 |
||
5611 | 12 |
Goal "Init (F Join G) = Init F Int Init G"; |
13 |
by (simp_tac (simpset() addsimps [Join_def]) 1); |
|
14 |
qed "Init_SKIP"; |
|
15 |
||
16 |
Goal "Init (F Join G) = Init F Int Init G"; |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
17 |
by (simp_tac (simpset() addsimps [Join_def]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
18 |
qed "Init_Join"; |
5252 | 19 |
|
5611 | 20 |
Goal "Acts (F Join G) = Acts F Un Acts G"; |
5596 | 21 |
by (auto_tac (claset(), simpset() addsimps [Join_def])); |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
22 |
qed "Acts_Join"; |
5252 | 23 |
|
5611 | 24 |
Goal "Init (JN i:I. F i) = (INT i:I. Init (F i))"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
25 |
by (simp_tac (simpset() addsimps [JOIN_def]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
26 |
qed "Init_JN"; |
5252 | 27 |
|
5611 | 28 |
Goal "Acts (JN i:I. F i) = insert Id (UN i:I. Acts (F i))"; |
5596 | 29 |
by (auto_tac (claset(), simpset() addsimps [JOIN_def])); |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
30 |
qed "Acts_JN"; |
5252 | 31 |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
32 |
Addsimps [Init_Join, Init_JN]; |
5259 | 33 |
|
5611 | 34 |
Goal "(JN x:insert a A. B x) = (B a) Join (JN x:A. B x)"; |
35 |
by (rtac program_equalityI 1); |
|
5596 | 36 |
by (ALLGOALS (simp_tac (simpset() addsimps [JOIN_def, Join_def]))); |
5584 | 37 |
qed "JN_insert"; |
38 |
Addsimps[JN_insert]; |
|
39 |
||
40 |
||
5611 | 41 |
(** Algebraic laws **) |
5259 | 42 |
|
5611 | 43 |
Goal "F Join G = G Join F"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
44 |
by (simp_tac (simpset() addsimps [Join_def, Un_commute, Int_commute]) 1); |
5259 | 45 |
qed "Join_commute"; |
46 |
||
5611 | 47 |
Goal "(F Join G) Join H = F Join (G Join H)"; |
5596 | 48 |
by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc]) 1); |
5259 | 49 |
qed "Join_assoc"; |
5596 | 50 |
|
5611 | 51 |
Goalw [Join_def, SKIP_def] "SKIP Join F = F"; |
52 |
by (rtac program_equalityI 1); |
|
5596 | 53 |
by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb]))); |
5611 | 54 |
qed "Join_SKIP_left"; |
5584 | 55 |
|
5611 | 56 |
Goalw [Join_def, SKIP_def] "F Join SKIP = F"; |
57 |
by (rtac program_equalityI 1); |
|
58 |
by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb]))); |
|
59 |
qed "Join_SKIP_right"; |
|
60 |
||
61 |
Addsimps [Join_SKIP_left, Join_SKIP_right]; |
|
62 |
||
63 |
Goalw [Join_def] "F Join F = F"; |
|
64 |
by (rtac program_equalityI 1); |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
65 |
by Auto_tac; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
66 |
qed "Join_absorb"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
67 |
|
5611 | 68 |
Addsimps [Join_absorb]; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
69 |
|
5584 | 70 |
Goal "(JN G:{}. G) = SKIP"; |
71 |
by (simp_tac (simpset() addsimps [JOIN_def, SKIP_def]) 1); |
|
72 |
qed "JN_empty"; |
|
73 |
Addsimps [JN_empty]; |
|
74 |
||
75 |
||
76 |
||
77 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
78 |
(*** Safety: constrains, stable, FP ***) |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
79 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
80 |
Goalw [constrains_def, JOIN_def] |
5584 | 81 |
"I ~= {} ==> \ |
5611 | 82 |
\ constrains (Acts (JN i:I. F i)) A B = \ |
83 |
\ (ALL i:I. constrains (Acts (F i)) A B)"; |
|
5596 | 84 |
by (Simp_tac 1); |
85 |
by (Blast_tac 1); |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
86 |
qed "constrains_JN"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
87 |
|
5620 | 88 |
Goal "constrains (Acts (F Join G)) A B = \ |
89 |
\ (constrains (Acts F) A B & constrains (Acts G) A B)"; |
|
90 |
by (auto_tac |
|
91 |
(claset(), |
|
92 |
simpset() addsimps [constrains_def, Join_def])); |
|
93 |
qed "constrains_Join"; |
|
94 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
95 |
(**FAILS, I think; see 5.4.1, Substitution Axiom. |
5620 | 96 |
The problem is to relate reachable (F Join G) with |
97 |
reachable F and reachable G |
|
98 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
99 |
Goalw [Constrains_def] |
5611 | 100 |
"Constrains (JN i:I. F i) A B = (ALL i:I. Constrains (F i) A B)"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
101 |
by (simp_tac (simpset() addsimps [constrains_JN]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
102 |
by (Blast_tac 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
103 |
qed "Constrains_JN"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
104 |
|
5620 | 105 |
Goal "Constrains (F Join G) A B = (Constrains F A B & Constrains G A B)"; |
5584 | 106 |
by (auto_tac |
107 |
(claset(), |
|
5620 | 108 |
simpset() addsimps [Constrains_def, constrains_Join])); |
109 |
qed "Constrains_Join"; |
|
110 |
**) |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
111 |
|
5611 | 112 |
Goal "[| constrains (Acts F) A A'; constrains (Acts G) B B' |] \ |
113 |
\ ==> constrains (Acts (F Join G)) (A Int B) (A' Un B')"; |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
114 |
by (simp_tac (simpset() addsimps [constrains_Join]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
115 |
by (blast_tac (claset() addIs [constrains_weaken]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
116 |
qed "constrains_Join_weaken"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
117 |
|
5584 | 118 |
Goal "I ~= {} ==> \ |
5611 | 119 |
\ stable (Acts (JN i:I. F i)) A = (ALL i:I. stable (Acts (F i)) A)"; |
5584 | 120 |
by (asm_simp_tac (simpset() addsimps [stable_def, constrains_JN]) 1); |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
121 |
qed "stable_JN"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
122 |
|
5611 | 123 |
Goal "stable (Acts (F Join G)) A = \ |
124 |
\ (stable (Acts F) A & stable (Acts G) A)"; |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
125 |
by (simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
126 |
qed "stable_Join"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
127 |
|
5611 | 128 |
Goal "I ~= {} ==> FP (Acts (JN i:I. F i)) = (INT i:I. FP (Acts (F i)))"; |
5584 | 129 |
by (asm_simp_tac (simpset() addsimps [FP_def, stable_JN, INTER_def]) 1); |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
130 |
qed "FP_JN"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
131 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
132 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
133 |
(*** Progress: transient, ensures ***) |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
134 |
|
5584 | 135 |
Goal "I ~= {} ==> \ |
5611 | 136 |
\ transient (Acts (JN i:I. F i)) A = (EX i:I. transient (Acts (F i)) A)"; |
5584 | 137 |
by (auto_tac (claset(), |
138 |
simpset() addsimps [transient_def, JOIN_def])); |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
139 |
qed "transient_JN"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
140 |
|
5611 | 141 |
Goal "transient (Acts (F Join G)) A = \ |
142 |
\ (transient (Acts F) A | transient (Acts G) A)"; |
|
5584 | 143 |
by (auto_tac (claset(), |
5596 | 144 |
simpset() addsimps [bex_Un, transient_def, |
5584 | 145 |
Join_def])); |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
146 |
qed "transient_Join"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
147 |
|
5584 | 148 |
Goal "I ~= {} ==> \ |
5611 | 149 |
\ ensures (Acts (JN i:I. F i)) A B = \ |
150 |
\ ((ALL i:I. constrains (Acts (F i)) (A-B) (A Un B)) & \ |
|
151 |
\ (EX i:I. ensures (Acts (F i)) A B))"; |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
152 |
by (auto_tac (claset(), |
5584 | 153 |
simpset() addsimps [ensures_def, constrains_JN, transient_JN])); |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
154 |
qed "ensures_JN"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
155 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
156 |
Goalw [ensures_def] |
5611 | 157 |
"ensures (Acts (F Join G)) A B = \ |
158 |
\ (constrains (Acts F) (A-B) (A Un B) & \ |
|
159 |
\ constrains (Acts G) (A-B) (A Un B) & \ |
|
160 |
\ (ensures (Acts F) A B | ensures (Acts G) A B))"; |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
161 |
by (auto_tac (claset(), |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
162 |
simpset() addsimps [constrains_Join, transient_Join])); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
163 |
qed "ensures_Join"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
164 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
165 |
Goalw [stable_def, constrains_def, Join_def] |
5639 | 166 |
"[| stable (Acts F) A; constrains (Acts G) A A' |] \ |
5611 | 167 |
\ ==> constrains (Acts (F Join G)) A A'"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
168 |
by (asm_simp_tac (simpset() addsimps [ball_Un]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
169 |
by (Blast_tac 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
170 |
qed "stable_constrains_Join"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
171 |
|
5611 | 172 |
(*Premises cannot use Invariant because Stable F A is weaker than |
173 |
stable (Acts G) A *) |
|
174 |
Goal "[| stable (Acts F) A; Init G <= A; stable (Acts G) A |] \ |
|
5639 | 175 |
\ ==> Invariant (F Join G) A"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
176 |
by (simp_tac (simpset() addsimps [Invariant_def, Stable_eq_stable, |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
177 |
stable_Join]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
178 |
by (force_tac(claset() addIs [stable_reachable, stable_Int], |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
179 |
simpset() addsimps [Acts_Join]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
180 |
qed "stable_Join_Invariant"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
181 |
|
5611 | 182 |
Goal "[| stable (Acts F) A; ensures (Acts G) A B |] \ |
183 |
\ ==> ensures (Acts (F Join G)) A B"; |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
184 |
by (asm_simp_tac (simpset() addsimps [ensures_Join]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
185 |
by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
186 |
by (etac constrains_weaken 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
187 |
by Auto_tac; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
188 |
qed "ensures_stable_Join1"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
189 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
190 |
(*As above, but exchanging the roles of F and G*) |
5611 | 191 |
Goal "[| ensures (Acts F) A B; stable (Acts G) A |] \ |
192 |
\ ==> ensures (Acts (F Join G)) A B"; |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
193 |
by (stac Join_commute 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
194 |
by (blast_tac (claset() addIs [ensures_stable_Join1]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
195 |
qed "ensures_stable_Join2"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
196 |