author | kleing |
Sun, 16 Dec 2001 00:20:17 +0100 | |
changeset 12521 | b1ebe0320d79 |
parent 11190 | 44e157622cb2 |
permissions | -rw-r--r-- |
5597 | 1 |
(* Title: HOL/UNITY/Comp.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Composition |
|
11190 | 7 |
From Chandy and Sanders, "Reasoning About Program Composition" |
5597 | 8 |
|
11190 | 9 |
Revised by Sidi Ehmety on January 2001 |
10 |
||
5597 | 11 |
*) |
11190 | 12 |
(*** component <= ***) |
6738
06189132c67b
component_eq_subset: a neat characterization of "component"
paulson
parents:
6703
diff
changeset
|
13 |
Goalw [component_def] |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7386
diff
changeset
|
14 |
"H <= F | H <= G ==> H <= (F Join G)"; |
7361 | 15 |
by Auto_tac; |
16 |
by (res_inst_tac [("x", "G Join Ga")] exI 1); |
|
17 |
by (res_inst_tac [("x", "G Join F")] exI 2); |
|
18 |
by (auto_tac (claset(), simpset() addsimps Join_ac)); |
|
19 |
qed "componentI"; |
|
20 |
||
21 |
Goalw [component_def] |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
22 |
"(F <= G) = \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
23 |
\ (Init G <= Init F & Acts F <= Acts G & AllowedActs G <= AllowedActs F)"; |
6738
06189132c67b
component_eq_subset: a neat characterization of "component"
paulson
parents:
6703
diff
changeset
|
24 |
by (force_tac (claset() addSIs [exI, program_equalityI], |
7537 | 25 |
simpset()) 1); |
6738
06189132c67b
component_eq_subset: a neat characterization of "component"
paulson
parents:
6703
diff
changeset
|
26 |
qed "component_eq_subset"; |
06189132c67b
component_eq_subset: a neat characterization of "component"
paulson
parents:
6703
diff
changeset
|
27 |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7386
diff
changeset
|
28 |
Goalw [component_def] "SKIP <= F"; |
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset
|
29 |
by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1); |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
30 |
qed "component_SKIP"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
31 |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7386
diff
changeset
|
32 |
Goalw [component_def] "F <= (F :: 'a program)"; |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
33 |
by (blast_tac (claset() addIs [Join_SKIP_right]) 1); |
5597 | 34 |
qed "component_refl"; |
35 |
||
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
36 |
AddIffs [component_SKIP, component_refl]; |
5597 | 37 |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7386
diff
changeset
|
38 |
Goal "F <= SKIP ==> F = SKIP"; |
6833 | 39 |
by (auto_tac (claset() addSIs [program_equalityI], |
40 |
simpset() addsimps [component_eq_subset])); |
|
41 |
qed "SKIP_minimal"; |
|
42 |
||
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7386
diff
changeset
|
43 |
Goalw [component_def] "F <= (F Join G)"; |
5968 | 44 |
by (Blast_tac 1); |
45 |
qed "component_Join1"; |
|
46 |
||
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7386
diff
changeset
|
47 |
Goalw [component_def] "G <= (F Join G)"; |
5968 | 48 |
by (simp_tac (simpset() addsimps [Join_commute]) 1); |
49 |
by (Blast_tac 1); |
|
50 |
qed "component_Join2"; |
|
51 |
||
7915
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7878
diff
changeset
|
52 |
Goal "F<=G ==> F Join G = G"; |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7878
diff
changeset
|
53 |
by (auto_tac (claset(), simpset() addsimps [component_def, Join_left_absorb])); |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7878
diff
changeset
|
54 |
qed "Join_absorb1"; |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7878
diff
changeset
|
55 |
|
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7878
diff
changeset
|
56 |
Goal "G<=F ==> F Join G = F"; |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7878
diff
changeset
|
57 |
by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def])); |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7878
diff
changeset
|
58 |
qed "Join_absorb2"; |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7878
diff
changeset
|
59 |
|
7947 | 60 |
Goal "((JOIN I F) <= H) = (ALL i: I. F i <= H)"; |
61 |
by (simp_tac (simpset() addsimps [component_eq_subset]) 1); |
|
62 |
by (Blast_tac 1); |
|
63 |
qed "JN_component_iff"; |
|
64 |
||
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7386
diff
changeset
|
65 |
Goalw [component_def] "i : I ==> (F i) <= (JN i:I. (F i))"; |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
66 |
by (blast_tac (claset() addIs [JN_absorb]) 1); |
5968 | 67 |
qed "component_JN"; |
68 |
||
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7386
diff
changeset
|
69 |
Goalw [component_def] "[| F <= G; G <= H |] ==> F <= (H :: 'a program)"; |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
70 |
by (blast_tac (claset() addIs [Join_assoc RS sym]) 1); |
5597 | 71 |
qed "component_trans"; |
72 |
||
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7386
diff
changeset
|
73 |
Goal "[| F <= G; G <= F |] ==> F = (G :: 'a program)"; |
6738
06189132c67b
component_eq_subset: a neat characterization of "component"
paulson
parents:
6703
diff
changeset
|
74 |
by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1); |
06189132c67b
component_eq_subset: a neat characterization of "component"
paulson
parents:
6703
diff
changeset
|
75 |
by (blast_tac (claset() addSIs [program_equalityI]) 1); |
6703 | 76 |
qed "component_antisym"; |
5597 | 77 |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7386
diff
changeset
|
78 |
Goal "((F Join G) <= H) = (F <= H & G <= H)"; |
7537 | 79 |
by (simp_tac (simpset() addsimps [component_eq_subset]) 1); |
6833 | 80 |
by (Blast_tac 1); |
81 |
qed "Join_component_iff"; |
|
82 |
||
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7386
diff
changeset
|
83 |
Goal "[| F <= G; G : A co B |] ==> F : A co B"; |
7386 | 84 |
by (auto_tac (claset(), |
85 |
simpset() addsimps [constrains_def, component_eq_subset])); |
|
86 |
qed "component_constrains"; |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
87 |
|
7947 | 88 |
(*Used in Guar.thy to show that programs are partially ordered*) |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7386
diff
changeset
|
89 |
bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq); |
7947 | 90 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
91 |
|
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
92 |
(*** preserves ***) |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
93 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
94 |
val prems = |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
95 |
Goalw [preserves_def] "(!!z. F : stable {s. v s = z}) ==> F : preserves v"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
96 |
by (blast_tac (claset() addIs prems) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
97 |
qed "preservesI"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
98 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
99 |
Goalw [preserves_def, stable_def, constrains_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
100 |
"[| F : preserves v; act : Acts F; (s,s') : act |] ==> v s = v s'"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
101 |
by (Force_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
102 |
qed "preserves_imp_eq"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
103 |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8251
diff
changeset
|
104 |
Goalw [preserves_def] |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8251
diff
changeset
|
105 |
"(F Join G : preserves v) = (F : preserves v & G : preserves v)"; |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8251
diff
changeset
|
106 |
by Auto_tac; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
107 |
qed "Join_preserves"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
108 |
|
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
109 |
Goal "(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
110 |
by (simp_tac (simpset() addsimps [JN_stable, preserves_def]) 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
111 |
by (Blast_tac 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
112 |
qed "JN_preserves"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
113 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
114 |
Goal "SKIP : preserves v"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
115 |
by (auto_tac (claset(), simpset() addsimps [preserves_def])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
116 |
qed "SKIP_preserves"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
117 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
118 |
AddIffs [Join_preserves, JN_preserves, SKIP_preserves]; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
119 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
120 |
Goalw [funPair_def] "(funPair f g) x = (f x, g x)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
121 |
by (Simp_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
122 |
qed "funPair_apply"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
123 |
Addsimps [funPair_apply]; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
124 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
125 |
Goal "preserves (funPair v w) = preserves v Int preserves w"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
126 |
by (auto_tac (claset(), |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
127 |
simpset() addsimps [preserves_def, stable_def, constrains_def])); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
128 |
by (Blast_tac 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
129 |
qed "preserves_funPair"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
130 |
|
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
131 |
(* (F : preserves (funPair v w)) = (F : preserves v Int preserves w) *) |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
132 |
AddIffs [preserves_funPair RS eqset_imp_iff]; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
133 |
|
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
134 |
|
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
135 |
Goal "(funPair f g) o h = funPair (f o h) (g o h)"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
136 |
by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
137 |
qed "funPair_o_distrib"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
138 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
139 |
Goal "fst o (funPair f g) = f"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
140 |
by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
141 |
qed "fst_o_funPair"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
142 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
143 |
Goal "snd o (funPair f g) = g"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
144 |
by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
145 |
qed "snd_o_funPair"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
146 |
Addsimps [fst_o_funPair, snd_o_funPair]; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
147 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
148 |
Goal "preserves v <= preserves (w o v)"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
149 |
by (force_tac (claset(), |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
150 |
simpset() addsimps [preserves_def, stable_def, constrains_def]) 1); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
151 |
qed "subset_preserves_o"; |
7947 | 152 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
153 |
Goal "preserves v <= stable {s. P (v s)}"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
154 |
by (auto_tac (claset(), |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
155 |
simpset() addsimps [preserves_def, stable_def, constrains_def])); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
156 |
by (rename_tac "s' s" 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
157 |
by (subgoal_tac "v s = v s'" 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
158 |
by (ALLGOALS Force_tac); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
159 |
qed "preserves_subset_stable"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
160 |
|
8216 | 161 |
Goal "preserves v <= increasing v"; |
162 |
by (auto_tac (claset(), |
|
163 |
simpset() addsimps [impOfSubs preserves_subset_stable, |
|
164 |
increasing_def])); |
|
165 |
qed "preserves_subset_increasing"; |
|
166 |
||
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
167 |
Goal "preserves id <= stable A"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
168 |
by (force_tac (claset(), |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
169 |
simpset() addsimps [preserves_def, stable_def, constrains_def]) 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
170 |
qed "preserves_id_subset_stable"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
171 |
|
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
172 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
173 |
(** For use with def_UNION_ok_iff **) |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
174 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
175 |
Goal "safety_prop (preserves v)"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
176 |
by (auto_tac (claset() addIs [safety_prop_INTER1], |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
177 |
simpset() addsimps [preserves_def])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
178 |
qed "safety_prop_preserves"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
179 |
AddIffs [safety_prop_preserves]; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
180 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
181 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
182 |
(** Some lemmas used only in Client.ML **) |
7947 | 183 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
184 |
Goal "[| F : stable {s. P (v s) (w s)}; \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
185 |
\ G : preserves v; G : preserves w |] \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
186 |
\ ==> F Join G : stable {s. P (v s) (w s)}"; |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8251
diff
changeset
|
187 |
by (Asm_simp_tac 1); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
188 |
by (subgoal_tac "G: preserves (funPair v w)" 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
189 |
by (Asm_simp_tac 2); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
190 |
by (dres_inst_tac [("P1", "split ?Q")] |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
191 |
(impOfSubs preserves_subset_stable) 1); |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
192 |
by Auto_tac; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
193 |
qed "stable_localTo_stable2"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
194 |
|
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
195 |
Goal "[| F : stable {s. v s <= w s}; G : preserves v; \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
196 |
\ F Join G : Increasing w |] \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
197 |
\ ==> F Join G : Stable {s. v s <= w s}"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
198 |
by (auto_tac (claset(), |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
199 |
simpset() addsimps [stable_def, Stable_def, Increasing_def, |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8251
diff
changeset
|
200 |
Constrains_def, all_conj_distrib])); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
201 |
by (blast_tac (claset() addIs [constrains_weaken]) 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
202 |
(*The G case remains*) |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
203 |
by (auto_tac (claset(), |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
204 |
simpset() addsimps [preserves_def, stable_def, constrains_def])); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
205 |
by (case_tac "act: Acts F" 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
206 |
by (Blast_tac 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
207 |
(*We have a G-action, so delete assumptions about F-actions*) |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
208 |
by (thin_tac "ALL act:Acts F. ?P act" 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
209 |
by (thin_tac "ALL z. ALL act:Acts F. ?P z act" 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
210 |
by (subgoal_tac "v x = v xa" 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
211 |
by (Blast_tac 2); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
212 |
by Auto_tac; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
213 |
by (etac order_trans 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
214 |
by (Blast_tac 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
215 |
qed "Increasing_preserves_Stable"; |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8065
diff
changeset
|
216 |
|
11190 | 217 |
(** component_of **) |
218 |
||
219 |
(* component_of is stronger than <= *) |
|
220 |
Goalw [component_def, component_of_def] |
|
221 |
"F component_of H ==> F <= H"; |
|
222 |
by (Blast_tac 1); |
|
223 |
qed "component_of_imp_component"; |
|
224 |
||
225 |
||
226 |
(* component_of satisfies many of the <='s properties *) |
|
227 |
Goalw [component_of_def] |
|
228 |
"F component_of F"; |
|
229 |
by (res_inst_tac [("x", "SKIP")] exI 1); |
|
230 |
by Auto_tac; |
|
231 |
qed "component_of_refl"; |
|
232 |
||
233 |
Goalw [component_of_def] |
|
234 |
"SKIP component_of F"; |
|
235 |
by Auto_tac; |
|
236 |
qed "component_of_SKIP"; |
|
237 |
||
238 |
Addsimps [component_of_refl, component_of_SKIP]; |
|
239 |
||
240 |
Goalw [component_of_def] |
|
241 |
"[| F component_of G; G component_of H |] ==> F component_of H"; |
|
242 |
by (blast_tac (claset() addIs [Join_assoc RS sym]) 1); |
|
243 |
qed "component_of_trans"; |
|
244 |
||
245 |
bind_thm ("strict_component_of_eq", strict_component_of_def RS meta_eq_to_obj_eq); |
|
246 |
||
247 |
(** localize **) |
|
248 |
Goalw [localize_def] |
|
249 |
"Init (localize v F) = Init F"; |
|
250 |
by (Simp_tac 1); |
|
251 |
qed "localize_Init_eq"; |
|
252 |
||
253 |
Goalw [localize_def] |
|
254 |
"Acts (localize v F) = Acts F"; |
|
255 |
by (Simp_tac 1); |
|
256 |
qed "localize_Acts_eq"; |
|
257 |
||
258 |
Goalw [localize_def] |
|
259 |
"AllowedActs (localize v F) = AllowedActs F Int (UN G:(preserves v). Acts G)"; |
|
260 |
by Auto_tac; |
|
261 |
qed "localize_AllowedActs_eq"; |
|
262 |
||
263 |
Addsimps [localize_Init_eq, localize_Acts_eq, localize_AllowedActs_eq]; |