author | nipkow |
Fri, 02 Oct 1998 14:28:39 +0200 | |
changeset 5608 | a82a038a3e7a |
parent 5596 | b29d18d8c4d2 |
child 5611 | 6957f124ca97 |
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 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
12 |
Goal "Init (Join prgF prgG) = Init prgF Int Init prgG"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
13 |
by (simp_tac (simpset() addsimps [Join_def]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
14 |
qed "Init_Join"; |
5252 | 15 |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
16 |
Goal "Acts (Join prgF prgG) = Acts prgF Un Acts prgG"; |
5596 | 17 |
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
|
18 |
qed "Acts_Join"; |
5252 | 19 |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
20 |
Goal "Init (JN i:I. prg i) = (INT i:I. Init (prg i))"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
21 |
by (simp_tac (simpset() addsimps [JOIN_def]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
22 |
qed "Init_JN"; |
5252 | 23 |
|
5608 | 24 |
Goal "Acts (JN i:I. prg i) = insert Id (UN i:I. Acts (prg i))"; |
5596 | 25 |
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
|
26 |
qed "Acts_JN"; |
5252 | 27 |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
28 |
Addsimps [Init_Join, Init_JN]; |
5259 | 29 |
|
5584 | 30 |
Goal "(JN x:insert a A. B x) = Join (B a) (JN x:A. B x)"; |
5596 | 31 |
br program_equalityI 1; |
32 |
by (ALLGOALS (simp_tac (simpset() addsimps [JOIN_def, Join_def]))); |
|
5584 | 33 |
qed "JN_insert"; |
34 |
Addsimps[JN_insert]; |
|
35 |
||
36 |
||
5259 | 37 |
(** Theoretical issues **) |
38 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
39 |
Goal "Join prgF prgG = Join prgG prgF"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
40 |
by (simp_tac (simpset() addsimps [Join_def, Un_commute, Int_commute]) 1); |
5259 | 41 |
qed "Join_commute"; |
42 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
43 |
Goal "Join (Join prgF prgG) prgH = Join prgF (Join prgG prgH)"; |
5596 | 44 |
by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc]) 1); |
5259 | 45 |
qed "Join_assoc"; |
5596 | 46 |
|
5584 | 47 |
Goalw [Join_def, SKIP_def] "Join prgF SKIP = prgF"; |
5596 | 48 |
br program_equalityI 1; |
49 |
by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb]))); |
|
5584 | 50 |
qed "Join_SKIP"; |
51 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
52 |
Goalw [Join_def] "Join prgF prgF = prgF"; |
5596 | 53 |
br program_equalityI 1; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
54 |
by Auto_tac; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
55 |
qed "Join_absorb"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
56 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
57 |
|
5584 | 58 |
Goal "(JN G:{}. G) = SKIP"; |
59 |
by (simp_tac (simpset() addsimps [JOIN_def, SKIP_def]) 1); |
|
60 |
qed "JN_empty"; |
|
61 |
Addsimps [JN_empty]; |
|
62 |
||
63 |
||
64 |
||
65 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
66 |
(*** Safety: constrains, stable, FP ***) |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
67 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
68 |
Goalw [constrains_def, JOIN_def] |
5584 | 69 |
"I ~= {} ==> \ |
70 |
\ constrains (Acts (JN i:I. prg i)) A B = \ |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
71 |
\ (ALL i:I. constrains (Acts (prg i)) A B)"; |
5596 | 72 |
by (Simp_tac 1); |
73 |
by (Blast_tac 1); |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
74 |
qed "constrains_JN"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
75 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
76 |
(**FAILS, I think; see 5.4.1, Substitution Axiom. |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
77 |
Goalw [Constrains_def] |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
78 |
"Constrains (JN i:I. prg i) A B = (ALL i:I. Constrains (prg i) A B)"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
79 |
by (simp_tac (simpset() addsimps [constrains_JN]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
80 |
by (Blast_tac 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
81 |
qed "Constrains_JN"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
82 |
**) |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
83 |
|
5584 | 84 |
Goal "constrains (Acts (Join prgF prgG)) A B = \ |
85 |
\ (constrains (Acts prgF) A B & constrains (Acts prgG) A B)"; |
|
86 |
by (auto_tac |
|
87 |
(claset(), |
|
5596 | 88 |
simpset() addsimps [constrains_def, Join_def, ball_Un])); |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
89 |
qed "constrains_Join"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
90 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
91 |
Goal "[| constrains (Acts prgF) A A'; constrains (Acts prgG) B B' |] \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
92 |
\ ==> constrains (Acts (Join prgF prgG)) (A Int B) (A' Un B')"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
93 |
by (simp_tac (simpset() addsimps [constrains_Join]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
94 |
by (blast_tac (claset() addIs [constrains_weaken]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
95 |
qed "constrains_Join_weaken"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
96 |
|
5584 | 97 |
Goal "I ~= {} ==> \ |
98 |
\ stable (Acts (JN i:I. prg i)) A = (ALL i:I. stable (Acts (prg i)) A)"; |
|
99 |
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
|
100 |
qed "stable_JN"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
101 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
102 |
Goal "stable (Acts (Join prgF prgG)) A = \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
103 |
\ (stable (Acts prgF) A & stable (Acts prgG) A)"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
104 |
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
|
105 |
qed "stable_Join"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
106 |
|
5584 | 107 |
Goal "I ~= {} ==> FP (Acts (JN i:I. prg i)) = (INT i:I. FP (Acts (prg i)))"; |
108 |
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
|
109 |
qed "FP_JN"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
110 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
111 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
112 |
(*** Progress: transient, ensures ***) |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
113 |
|
5584 | 114 |
Goal "I ~= {} ==> \ |
115 |
\ transient (Acts (JN i:I. prg i)) A = (EX i:I. transient (Acts (prg i)) A)"; |
|
116 |
by (auto_tac (claset(), |
|
117 |
simpset() addsimps [transient_def, JOIN_def])); |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
118 |
qed "transient_JN"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
119 |
|
5584 | 120 |
Goal "transient (Acts (Join prgF prgG)) A = \ |
121 |
\ (transient (Acts prgF) A | transient (Acts prgG) A)"; |
|
122 |
by (auto_tac (claset(), |
|
5596 | 123 |
simpset() addsimps [bex_Un, transient_def, |
5584 | 124 |
Join_def])); |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
125 |
qed "transient_Join"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
126 |
|
5584 | 127 |
Goal "I ~= {} ==> \ |
128 |
\ ensures (Acts (JN i:I. prg i)) A B = \ |
|
129 |
\ ((ALL i:I. constrains (Acts (prg i)) (A-B) (A Un B)) & \ |
|
130 |
\ (EX i:I. ensures (Acts (prg i)) A B))"; |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
131 |
by (auto_tac (claset(), |
5584 | 132 |
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
|
133 |
qed "ensures_JN"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
134 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
135 |
Goalw [ensures_def] |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
136 |
"ensures (Acts (Join prgF prgG)) A B = \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
137 |
\ (constrains (Acts prgF) (A-B) (A Un B) & \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
138 |
\ constrains (Acts prgG) (A-B) (A Un B) & \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
139 |
\ (ensures (Acts prgF) A B | ensures (Acts prgG) A B))"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
140 |
by (auto_tac (claset(), |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
141 |
simpset() addsimps [constrains_Join, transient_Join])); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
142 |
qed "ensures_Join"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
143 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
144 |
Goalw [stable_def, constrains_def, Join_def] |
5608 | 145 |
"[| stable (Acts prgF) A; constrains (Acts prgG) A A'; Id: Acts prgG |] \ |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
146 |
\ ==> constrains (Acts (Join prgF prgG)) A A'"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
147 |
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
|
148 |
by (Blast_tac 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
149 |
qed "stable_constrains_Join"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
150 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
151 |
(*Premises cannot use Invariant because Stable prgF A is weaker than |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
152 |
stable (Acts prgG) A *) |
5584 | 153 |
Goal "[| stable (Acts prgF) A; Init prgG <= A; stable (Acts prgG) A |] \ |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
154 |
\ ==> Invariant (Join prgF prgG) A"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
155 |
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
|
156 |
stable_Join]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
157 |
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
|
158 |
simpset() addsimps [Acts_Join]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
159 |
qed "stable_Join_Invariant"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
160 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
161 |
Goal "[| stable (Acts prgF) A; ensures (Acts prgG) A B |] \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
162 |
\ ==> ensures (Acts (Join prgF prgG)) A B"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
163 |
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
|
164 |
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
|
165 |
by (etac constrains_weaken 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
166 |
by Auto_tac; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
167 |
qed "ensures_stable_Join1"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
168 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
169 |
(*As above, but exchanging the roles of F and G*) |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
170 |
Goal "[| ensures (Acts prgF) A B; stable (Acts prgG) A |] \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
171 |
\ ==> ensures (Acts (Join prgF prgG)) A B"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
172 |
by (stac Join_commute 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
173 |
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
|
174 |
qed "ensures_stable_Join2"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
175 |