author | wenzelm |
Wed, 09 Jan 2002 17:48:40 +0100 | |
changeset 12691 | d21db58bcdc2 |
parent 10834 | a7897aebbffc |
child 13550 | 5a176b8dda84 |
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 |
||
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8216
diff
changeset
|
11 |
(*Perhaps equalities.ML shouldn't add this in the first place!*) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8216
diff
changeset
|
12 |
Delsimps [image_Collect]; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8216
diff
changeset
|
13 |
|
6535 | 14 |
(*** The abstract type of programs ***) |
15 |
||
16 |
val rep_ss = simpset() addsimps |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
17 |
[Init_def, Acts_def, AllowedActs_def, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
18 |
mk_program_def, Program_def, Rep_Program, |
6535 | 19 |
Rep_Program_inverse, Abs_Program_inverse]; |
20 |
||
21 |
||
22 |
Goal "Id : Acts F"; |
|
23 |
by (cut_inst_tac [("x", "F")] Rep_Program 1); |
|
24 |
by (auto_tac (claset(), rep_ss)); |
|
25 |
qed "Id_in_Acts"; |
|
26 |
AddIffs [Id_in_Acts]; |
|
27 |
||
28 |
Goal "insert Id (Acts F) = Acts F"; |
|
29 |
by (simp_tac (simpset() addsimps [insert_absorb, Id_in_Acts]) 1); |
|
30 |
qed "insert_Id_Acts"; |
|
31 |
AddIffs [insert_Id_Acts]; |
|
32 |
||
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
33 |
Goal "Id : AllowedActs F"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
34 |
by (cut_inst_tac [("x", "F")] Rep_Program 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
35 |
by (auto_tac (claset(), rep_ss)); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
36 |
qed "Id_in_AllowedActs"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
37 |
AddIffs [Id_in_AllowedActs]; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
38 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
39 |
Goal "insert Id (AllowedActs F) = AllowedActs F"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
40 |
by (simp_tac (simpset() addsimps [insert_absorb, Id_in_AllowedActs]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
41 |
qed "insert_Id_AllowedActs"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
42 |
AddIffs [insert_Id_AllowedActs]; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
43 |
|
6535 | 44 |
(** Inspectors for type "program" **) |
45 |
||
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
46 |
Goal "Init (mk_program (init,acts,allowed)) = init"; |
6535 | 47 |
by (auto_tac (claset(), rep_ss)); |
48 |
qed "Init_eq"; |
|
49 |
||
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
50 |
Goal "Acts (mk_program (init,acts,allowed)) = insert Id acts"; |
6535 | 51 |
by (auto_tac (claset(), rep_ss)); |
52 |
qed "Acts_eq"; |
|
53 |
||
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
54 |
Goal "AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
55 |
by (auto_tac (claset(), rep_ss)); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
56 |
qed "AllowedActs_eq"; |
6535 | 57 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
58 |
Addsimps [Init_eq, Acts_eq, AllowedActs_eq]; |
6535 | 59 |
|
8327 | 60 |
(** Equality for UNITY programs **) |
7915
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7826
diff
changeset
|
61 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
62 |
Goal "mk_program (Init F, Acts F, AllowedActs F) = F"; |
7915
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7826
diff
changeset
|
63 |
by (cut_inst_tac [("x", "F")] Rep_Program 1); |
6535 | 64 |
by (auto_tac (claset(), rep_ss)); |
65 |
by (REPEAT (dres_inst_tac [("f", "Abs_Program")] arg_cong 1)); |
|
7915
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7826
diff
changeset
|
66 |
by (asm_full_simp_tac (rep_ss addsimps [insert_absorb]) 1); |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7826
diff
changeset
|
67 |
qed "surjective_mk_program"; |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7826
diff
changeset
|
68 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
69 |
Goal "[| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |] \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
70 |
\ ==> F = G"; |
8988 | 71 |
by (res_inst_tac [("t", "F")] (surjective_mk_program RS subst) 1); |
72 |
by (res_inst_tac [("t", "G")] (surjective_mk_program RS subst) 1); |
|
73 |
by (Asm_simp_tac 1); |
|
6535 | 74 |
qed "program_equalityI"; |
75 |
||
76 |
val [major,minor] = |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
77 |
Goal "[| F = G; \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
78 |
\ [| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |]\ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
79 |
\ ==> P |] ==> P"; |
6535 | 80 |
by (rtac minor 1); |
81 |
by (auto_tac (claset(), simpset() addsimps [major])); |
|
82 |
qed "program_equalityE"; |
|
83 |
||
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
84 |
Goal "(F=G) = \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
85 |
\ (Init F = Init G & Acts F = Acts G &AllowedActs F = AllowedActs G)"; |
8327 | 86 |
by (blast_tac (claset() addIs [program_equalityI, program_equalityE]) 1); |
87 |
qed "program_equality_iff"; |
|
88 |
||
7915
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7826
diff
changeset
|
89 |
Addsimps [surjective_mk_program]; |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7826
diff
changeset
|
90 |
|
6535 | 91 |
|
92 |
(*** These rules allow "lazy" definition expansion |
|
93 |
They avoid expanding the full program, which is a large expression |
|
94 |
***) |
|
95 |
||
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
96 |
Goal "F == mk_program (init,acts,allowed) ==> Init F = init"; |
6535 | 97 |
by Auto_tac; |
98 |
qed "def_prg_Init"; |
|
99 |
||
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
100 |
Goal "F == mk_program (init,acts,allowed) ==> Acts F = insert Id acts"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
101 |
by Auto_tac; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
102 |
qed "def_prg_Acts"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
103 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
104 |
Goal "F == mk_program (init,acts,allowed) \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
105 |
\ ==> AllowedActs F = insert Id allowed"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
106 |
by Auto_tac; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
107 |
qed "def_prg_AllowedActs"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
108 |
|
6535 | 109 |
(*The program is not expanded, but its Init and Acts are*) |
110 |
val [rew] = goal thy |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9025
diff
changeset
|
111 |
"[| F == mk_program (init,acts,allowed) |] \ |
6535 | 112 |
\ ==> Init F = init & Acts F = insert Id acts"; |
113 |
by (rewtac rew); |
|
114 |
by Auto_tac; |
|
115 |
qed "def_prg_simps"; |
|
116 |
||
117 |
(*An action is expanded only if a pair of states is being tested against it*) |
|
118 |
Goal "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'"; |
|
119 |
by Auto_tac; |
|
120 |
qed "def_act_simp"; |
|
121 |
||
122 |
fun simp_of_act def = def RS def_act_simp; |
|
123 |
||
124 |
(*A set is expanded only if an element is being tested against it*) |
|
125 |
Goal "A == B ==> (x : A) = (x : B)"; |
|
126 |
by Auto_tac; |
|
127 |
qed "def_set_simp"; |
|
128 |
||
129 |
fun simp_of_set def = def RS def_set_simp; |
|
130 |
||
131 |
||
6536 | 132 |
(*** co ***) |
4776 | 133 |
|
7403 | 134 |
(*These operators are not overloaded, but their operands are sets, and |
135 |
ultimately there's a risk of reaching equality, which IS overloaded*) |
|
136 |
overload_1st_set "UNITY.constrains"; |
|
5648 | 137 |
overload_1st_set "UNITY.stable"; |
138 |
overload_1st_set "UNITY.unless"; |
|
5340 | 139 |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
140 |
val prems = Goalw [constrains_def] |
5648 | 141 |
"(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') \ |
6536 | 142 |
\ ==> F : A co A'"; |
4776 | 143 |
by (blast_tac (claset() addIs prems) 1); |
144 |
qed "constrainsI"; |
|
145 |
||
5069 | 146 |
Goalw [constrains_def] |
6536 | 147 |
"[| F : A co A'; act: Acts F; (s,s'): act; s: A |] ==> s': A'"; |
4776 | 148 |
by (Blast_tac 1); |
149 |
qed "constrainsD"; |
|
150 |
||
6536 | 151 |
Goalw [constrains_def] "F : {} co B"; |
4776 | 152 |
by (Blast_tac 1); |
153 |
qed "constrains_empty"; |
|
154 |
||
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
155 |
Goalw [constrains_def] "(F : A co {}) = (A={})"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
156 |
by (Blast_tac 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
157 |
qed "constrains_empty2"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
158 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
159 |
Goalw [constrains_def] "(F : UNIV co B) = (B = UNIV)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
160 |
by (Blast_tac 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
161 |
qed "constrains_UNIV"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
162 |
|
6536 | 163 |
Goalw [constrains_def] "F : A co UNIV"; |
4776 | 164 |
by (Blast_tac 1); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
165 |
qed "constrains_UNIV2"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
166 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
167 |
AddIffs [constrains_empty, constrains_empty2, |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
168 |
constrains_UNIV, constrains_UNIV2]; |
4776 | 169 |
|
5648 | 170 |
(*monotonic in 2nd argument*) |
5069 | 171 |
Goalw [constrains_def] |
6536 | 172 |
"[| F : A co A'; A'<=B' |] ==> F : A co B'"; |
4776 | 173 |
by (Blast_tac 1); |
174 |
qed "constrains_weaken_R"; |
|
175 |
||
5648 | 176 |
(*anti-monotonic in 1st argument*) |
5069 | 177 |
Goalw [constrains_def] |
6536 | 178 |
"[| F : A co A'; B<=A |] ==> F : B co A'"; |
4776 | 179 |
by (Blast_tac 1); |
180 |
qed "constrains_weaken_L"; |
|
181 |
||
5069 | 182 |
Goalw [constrains_def] |
6536 | 183 |
"[| F : A co A'; B<=A; A'<=B' |] ==> F : B co B'"; |
4776 | 184 |
by (Blast_tac 1); |
185 |
qed "constrains_weaken"; |
|
186 |
||
187 |
(** Union **) |
|
188 |
||
5069 | 189 |
Goalw [constrains_def] |
7345 | 190 |
"[| F : A co A'; F : B co B' |] ==> F : (A Un B) co (A' Un B')"; |
4776 | 191 |
by (Blast_tac 1); |
192 |
qed "constrains_Un"; |
|
193 |
||
5069 | 194 |
Goalw [constrains_def] |
7345 | 195 |
"ALL i:I. F : (A i) co (A' i) ==> F : (UN i:I. A i) co (UN i:I. A' i)"; |
4776 | 196 |
by (Blast_tac 1); |
8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8327
diff
changeset
|
197 |
bind_thm ("constrains_UN", ballI RS result()); |
4776 | 198 |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
199 |
Goalw [constrains_def] "(A Un B) co C = (A co C) Int (B co C)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
200 |
by (Blast_tac 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
201 |
qed "constrains_Un_distrib"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
202 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
203 |
Goalw [constrains_def] "(UN i:I. A i) co B = (INT i:I. A i co B)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
204 |
by (Blast_tac 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
205 |
qed "constrains_UN_distrib"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
206 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
207 |
Goalw [constrains_def] "C co (A Int B) = (C co A) Int (C co B)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
208 |
by (Blast_tac 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
209 |
qed "constrains_Int_distrib"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
210 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
211 |
Goalw [constrains_def] "A co (INT i:I. B i) = (INT i:I. A co B i)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
212 |
by (Blast_tac 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
213 |
qed "constrains_INT_distrib"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7630
diff
changeset
|
214 |
|
4776 | 215 |
(** Intersection **) |
216 |
||
5069 | 217 |
Goalw [constrains_def] |
7345 | 218 |
"[| F : A co A'; F : B co B' |] ==> F : (A Int B) co (A' Int B')"; |
4776 | 219 |
by (Blast_tac 1); |
220 |
qed "constrains_Int"; |
|
221 |
||
5069 | 222 |
Goalw [constrains_def] |
7345 | 223 |
"ALL i:I. F : (A i) co (A' i) ==> F : (INT i:I. A i) co (INT i:I. A' i)"; |
4776 | 224 |
by (Blast_tac 1); |
8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8327
diff
changeset
|
225 |
bind_thm ("constrains_INT", ballI RS result()); |
4776 | 226 |
|
6536 | 227 |
Goalw [constrains_def] "F : A co A' ==> A <= A'"; |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
228 |
by Auto_tac; |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
229 |
qed "constrains_imp_subset"; |
4776 | 230 |
|
6536 | 231 |
(*The reasoning is by subsets since "co" refers to single actions |
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
232 |
only. So this rule isn't that useful.*) |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
233 |
Goalw [constrains_def] |
6536 | 234 |
"[| F : A co B; F : B co C |] ==> F : A co C"; |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
235 |
by (Blast_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
236 |
qed "constrains_trans"; |
4776 | 237 |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
238 |
Goalw [constrains_def] |
7345 | 239 |
"[| F : A co (A' Un B); F : B co B' |] ==> F : A co (A' Un B')"; |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
240 |
by (Clarify_tac 1); |
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
241 |
by (Blast_tac 1); |
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
242 |
qed "constrains_cancel"; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
243 |
|
4776 | 244 |
|
7630 | 245 |
(*** unless ***) |
246 |
||
247 |
Goalw [unless_def] "F : (A-B) co (A Un B) ==> F : A unless B"; |
|
248 |
by (assume_tac 1); |
|
249 |
qed "unlessI"; |
|
250 |
||
251 |
Goalw [unless_def] "F : A unless B ==> F : (A-B) co (A Un B)"; |
|
252 |
by (assume_tac 1); |
|
253 |
qed "unlessD"; |
|
254 |
||
255 |
||
4776 | 256 |
(*** stable ***) |
257 |
||
6536 | 258 |
Goalw [stable_def] "F : A co A ==> F : stable A"; |
4776 | 259 |
by (assume_tac 1); |
260 |
qed "stableI"; |
|
261 |
||
6536 | 262 |
Goalw [stable_def] "F : stable A ==> F : A co A"; |
4776 | 263 |
by (assume_tac 1); |
264 |
qed "stableD"; |
|
265 |
||
7594
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7403
diff
changeset
|
266 |
Goalw [stable_def, constrains_def] "stable UNIV = UNIV"; |
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7403
diff
changeset
|
267 |
by Auto_tac; |
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7403
diff
changeset
|
268 |
qed "stable_UNIV"; |
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7403
diff
changeset
|
269 |
Addsimps [stable_UNIV]; |
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7403
diff
changeset
|
270 |
|
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
271 |
(** Union **) |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
272 |
|
5069 | 273 |
Goalw [stable_def] |
5648 | 274 |
"[| F : stable A; F : stable A' |] ==> F : stable (A Un A')"; |
4776 | 275 |
by (blast_tac (claset() addIs [constrains_Un]) 1); |
276 |
qed "stable_Un"; |
|
277 |
||
5069 | 278 |
Goalw [stable_def] |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
279 |
"ALL i:I. F : stable (A i) ==> F : stable (UN i:I. A i)"; |
8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8327
diff
changeset
|
280 |
by (blast_tac (claset() addIs [constrains_UN]) 1); |
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8327
diff
changeset
|
281 |
bind_thm ("stable_UN", ballI RS result()); |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
282 |
|
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
283 |
(** Intersection **) |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
284 |
|
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
285 |
Goalw [stable_def] |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
7915
diff
changeset
|
286 |
"[| F : stable A; F : stable A' |] ==> F : stable (A Int A')"; |
4776 | 287 |
by (blast_tac (claset() addIs [constrains_Int]) 1); |
288 |
qed "stable_Int"; |
|
289 |
||
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
290 |
Goalw [stable_def] |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
291 |
"ALL i:I. F : stable (A i) ==> F : stable (INT i:I. A i)"; |
8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8327
diff
changeset
|
292 |
by (blast_tac (claset() addIs [constrains_INT]) 1); |
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8327
diff
changeset
|
293 |
bind_thm ("stable_INT", ballI RS result()); |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
294 |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
295 |
Goalw [stable_def, constrains_def] |
7345 | 296 |
"[| F : stable C; F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')"; |
4776 | 297 |
by (Blast_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
298 |
qed "stable_constrains_Un"; |
4776 | 299 |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
300 |
Goalw [stable_def, constrains_def] |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
7915
diff
changeset
|
301 |
"[| F : stable C; F : (C Int A) co A' |] ==> F : (C Int A) co (C Int A')"; |
4776 | 302 |
by (Blast_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
303 |
qed "stable_constrains_Int"; |
4776 | 304 |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
7915
diff
changeset
|
305 |
(*[| F : stable C; F : (C Int A) co A |] ==> F : stable (C Int A) *) |
5648 | 306 |
bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI); |
307 |
||
308 |
||
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
309 |
(*** invariant ***) |
5648 | 310 |
|
311 |
Goal "[| Init F<=A; F: stable A |] ==> F : invariant A"; |
|
312 |
by (asm_simp_tac (simpset() addsimps [invariant_def]) 1); |
|
313 |
qed "invariantI"; |
|
314 |
||
315 |
(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*) |
|
316 |
Goal "[| F : invariant A; F : invariant B |] ==> F : invariant (A Int B)"; |
|
317 |
by (auto_tac (claset(), simpset() addsimps [invariant_def, stable_Int])); |
|
318 |
qed "invariant_Int"; |
|
319 |
||
320 |
||
321 |
(*** increasing ***) |
|
322 |
||
8216 | 323 |
Goalw [increasing_def] |
324 |
"F : increasing f ==> F : stable {s. z <= f s}"; |
|
325 |
by (Blast_tac 1); |
|
326 |
qed "increasingD"; |
|
327 |
||
9025 | 328 |
Goalw [increasing_def, stable_def] "F : increasing (%s. c)"; |
329 |
by Auto_tac; |
|
330 |
qed "increasing_constant"; |
|
331 |
AddIffs [increasing_constant]; |
|
332 |
||
5648 | 333 |
Goalw [increasing_def, stable_def, constrains_def] |
6712 | 334 |
"mono g ==> increasing f <= increasing (g o f)"; |
5648 | 335 |
by Auto_tac; |
6712 | 336 |
by (blast_tac (claset() addIs [monoD, order_trans]) 1); |
337 |
qed "mono_increasing_o"; |
|
5648 | 338 |
|
8216 | 339 |
(*Holds by the theorem (Suc m <= n) = (m < n) *) |
5648 | 340 |
Goalw [increasing_def] |
8216 | 341 |
"!!z::nat. F : increasing f ==> F: stable {s. z < f s}"; |
5648 | 342 |
by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1); |
343 |
by (Blast_tac 1); |
|
8216 | 344 |
qed "strict_increasingD"; |
5648 | 345 |
|
346 |
||
347 |
(** The Elimination Theorem. The "free" m has become universally quantified! |
|
348 |
Should the premise be !!m instead of ALL m ? Would make it harder to use |
|
349 |
in forward proof. **) |
|
350 |
||
5069 | 351 |
Goalw [constrains_def] |
6536 | 352 |
"[| ALL m:M. F : {s. s x = m} co (B m) |] \ |
353 |
\ ==> F : {s. s x : M} co (UN m:M. B m)"; |
|
4776 | 354 |
by (Blast_tac 1); |
355 |
qed "elimination"; |
|
356 |
||
357 |
(*As above, but for the trivial case of a one-variable state, in which the |
|
358 |
state is identified with its one variable.*) |
|
5069 | 359 |
Goalw [constrains_def] |
6536 | 360 |
"(ALL m:M. F : {m} co (B m)) ==> F : M co (UN m:M. B m)"; |
4776 | 361 |
by (Blast_tac 1); |
362 |
qed "elimination_sing"; |
|
363 |
||
364 |
||
365 |
||
366 |
(*** Theoretical Results from Section 6 ***) |
|
367 |
||
5069 | 368 |
Goalw [constrains_def, strongest_rhs_def] |
6536 | 369 |
"F : A co (strongest_rhs F A )"; |
4776 | 370 |
by (Blast_tac 1); |
371 |
qed "constrains_strongest_rhs"; |
|
372 |
||
5069 | 373 |
Goalw [constrains_def, strongest_rhs_def] |
6536 | 374 |
"F : A co B ==> strongest_rhs F A <= B"; |
4776 | 375 |
by (Blast_tac 1); |
376 |
qed "strongest_rhs_is_strongest"; |
|
8948
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
377 |
|
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
378 |
|
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
379 |
(** Ad-hoc set-theory rules **) |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
380 |
|
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
381 |
Goal "A Un B - (A - B) = B"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
382 |
by (Blast_tac 1); |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
383 |
qed "Un_Diff_Diff"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
384 |
Addsimps [Un_Diff_Diff]; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
385 |
|
10834 | 386 |
Goal "Union(B) Int A = Union((%C. C Int A)`B)"; |
8948
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
387 |
by (Blast_tac 1); |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
388 |
qed "Int_Union_Union"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
389 |
|
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
390 |
(** Needed for WF reasoning in WFair.ML **) |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
391 |
|
10834 | 392 |
Goal "less_than `` {k} = greaterThan k"; |
8948
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
393 |
by (Blast_tac 1); |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
394 |
qed "Image_less_than"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
395 |
|
10834 | 396 |
Goal "less_than^-1 `` {k} = lessThan k"; |
8948
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
397 |
by (Blast_tac 1); |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
398 |
qed "Image_inverse_less_than"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
399 |
|
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8703
diff
changeset
|
400 |
Addsimps [Image_less_than, Image_inverse_less_than]; |