author | wenzelm |
Fri, 09 Nov 2001 00:09:47 +0100 | |
changeset 12114 | a8e860c86252 |
parent 11701 | 3d51fbf81c17 |
permissions | -rw-r--r-- |
7186 | 1 |
(* Title: HOL/UNITY/Lift_prog.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
7482 | 5 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
6 |
Arrays of processes. |
7186 | 7 |
*) |
8 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
9 |
Addsimps [insert_map_def, delete_map_def]; |
7186 | 10 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
11 |
Goal "delete_map i (insert_map i x f) = f"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
12 |
by (rtac ext 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
13 |
by (Simp_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
14 |
qed "insert_map_inverse"; |
7186 | 15 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
16 |
Goal "(insert_map i x (delete_map i g)) = g(i:=x)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
17 |
by (rtac ext 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
18 |
by (auto_tac (claset(), simpset() addsplits [nat_diff_split])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
19 |
qed "insert_map_delete_map_eq"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
20 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
21 |
(*** Injectiveness proof ***) |
7186 | 22 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
23 |
Goal "(insert_map i x f) = (insert_map i y g) ==> x=y"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
24 |
by (dres_inst_tac [("x","i")] fun_cong 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
25 |
by (Full_simp_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
26 |
qed "insert_map_inject1"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
27 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
28 |
Goal "(insert_map i x f) = (insert_map i y g) ==> f=g"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
29 |
by (dres_inst_tac [("f", "delete_map i")] arg_cong 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
30 |
by (full_simp_tac (simpset() addsimps [insert_map_inverse]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
31 |
qed "insert_map_inject2"; |
7186 | 32 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
33 |
Goal "(insert_map i x f) = (insert_map i y g) ==> x=y & f=g"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
34 |
by (blast_tac (claset() addDs [insert_map_inject1, insert_map_inject2]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
35 |
bind_thm ("insert_map_inject", result() RS conjE); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
36 |
AddSEs [insert_map_inject]; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
37 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
38 |
(*The general case: we don't assume i=i'*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
39 |
Goalw [lift_map_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
40 |
"(lift_map i (s,(f,uu)) = lift_map i' (s',(f',uu'))) \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
41 |
\ = (uu = uu' & insert_map i s f = insert_map i' s' f')"; |
7525 | 42 |
by Auto_tac; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
43 |
qed "lift_map_eq_iff"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
44 |
AddIffs [lift_map_eq_iff]; |
7186 | 45 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
46 |
Goalw [lift_map_def, drop_map_def] "!!s. drop_map i (lift_map i s) = s"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
47 |
by (force_tac (claset() addIs [insert_map_inverse], simpset()) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
48 |
qed "drop_map_lift_map_eq"; |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
49 |
Addsimps [drop_map_lift_map_eq]; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
50 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
51 |
Goalw [lift_map_def] "inj (lift_map i)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
52 |
by (rtac injI 1); |
7688 | 53 |
by Auto_tac; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
54 |
qed "inj_lift_map"; |
7688 | 55 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
56 |
(*** Surjectiveness proof ***) |
7186 | 57 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
58 |
Goalw [lift_map_def, drop_map_def] "!!s. lift_map i (drop_map i s) = s"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
59 |
by (force_tac (claset(), simpset() addsimps [insert_map_delete_map_eq]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
60 |
qed "lift_map_drop_map_eq"; |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
61 |
Addsimps [lift_map_drop_map_eq]; |
7186 | 62 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
63 |
Goal "(drop_map i s) = (drop_map i s') ==> s=s'"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
64 |
by (dres_inst_tac [("f", "lift_map i")] arg_cong 1); |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
65 |
by (Full_simp_tac 1); |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
66 |
qed "drop_map_inject"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
67 |
AddSDs [drop_map_inject]; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
68 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
69 |
Goal "surj (lift_map i)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
70 |
by (rtac surjI 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
71 |
by (rtac lift_map_drop_map_eq 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
72 |
qed "surj_lift_map"; |
7186 | 73 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
74 |
Goal "bij (lift_map i)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
75 |
by (simp_tac (simpset() addsimps [bij_def, inj_lift_map, surj_lift_map]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
76 |
qed "bij_lift_map"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
77 |
AddIffs [bij_lift_map]; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
78 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
79 |
Goal "inv (lift_map i) = drop_map i"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
80 |
by (rtac inv_equality 1); |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
81 |
by Auto_tac; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
82 |
qed "inv_lift_map_eq"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
83 |
Addsimps [inv_lift_map_eq]; |
7688 | 84 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
85 |
Goal "inv (drop_map i) = lift_map i"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
86 |
by (rtac inv_equality 1); |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
87 |
by Auto_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
88 |
qed "inv_drop_map_eq"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
89 |
Addsimps [inv_drop_map_eq]; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
90 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
91 |
Goal "bij (drop_map i)"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
92 |
by (simp_tac (simpset() delsimps [inv_lift_map_eq] |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
93 |
addsimps [inv_lift_map_eq RS sym, bij_imp_bij_inv]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
94 |
qed "bij_drop_map"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
95 |
AddIffs [bij_drop_map]; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
96 |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
97 |
(*sub's main property!*) |
7947 | 98 |
Goal "sub i f = f i"; |
99 |
by (simp_tac (simpset() addsimps [sub_def]) 1); |
|
100 |
qed "sub_apply"; |
|
101 |
Addsimps [sub_apply]; |
|
7688 | 102 |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
103 |
(*** lift_set ***) |
7688 | 104 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
105 |
Goalw [lift_set_def] "lift_set i {} = {}"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
106 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
107 |
qed "lift_set_empty"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
108 |
Addsimps [lift_set_empty]; |
7688 | 109 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
110 |
Goalw [lift_set_def] "(lift_map i x : lift_set i A) = (x : A)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
111 |
by (rtac (inj_lift_map RS inj_image_mem_iff) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
112 |
qed "lift_set_iff"; |
7186 | 113 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
114 |
(*Do we really need both this one and its predecessor?*) |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
115 |
Goal "((f,uu) : lift_set i A) = ((f i, (delete_map i f, uu)) : A)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
116 |
by (asm_simp_tac (simpset() addsimps [lift_set_def, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
117 |
mem_rename_set_iff, drop_map_def]) 1); |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
118 |
qed "lift_set_iff2"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
119 |
AddIffs [lift_set_iff2]; |
7525 | 120 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
121 |
Goalw [lift_set_def] "A<=B ==> lift_set i A <= lift_set i B"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
122 |
by (etac image_mono 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
123 |
qed "lift_set_mono"; |
7525 | 124 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
125 |
Goalw [lift_set_def] "lift_set i (A Un B) = lift_set i A Un lift_set i B"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
126 |
by (asm_simp_tac (simpset() addsimps [image_Un]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
127 |
qed "lift_set_Un_distrib"; |
7525 | 128 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
129 |
Goalw [lift_set_def] "lift_set i (A-B) = lift_set i A - lift_set i B"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
130 |
by (rtac (inj_lift_map RS image_set_diff) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
131 |
qed "lift_set_Diff_distrib"; |
7525 | 132 |
|
133 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
134 |
(*** the lattice operations ***) |
7525 | 135 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
136 |
Goal "bij (lift i)"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
137 |
by (simp_tac (simpset() addsimps [lift_def]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
138 |
qed "bij_lift"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
139 |
AddIffs [bij_lift]; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
140 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
141 |
Goalw [lift_def] "lift i SKIP = SKIP"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
142 |
by (Asm_simp_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
143 |
qed "lift_SKIP"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
144 |
Addsimps [lift_SKIP]; |
7525 | 145 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
146 |
Goalw [lift_def] "lift i (F Join G) = lift i F Join lift i G"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
147 |
by (Asm_simp_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
148 |
qed "lift_Join"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
149 |
Addsimps [lift_Join]; |
7688 | 150 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
151 |
Goalw [lift_def] "lift j (JOIN I F) = (JN i:I. lift j (F i))"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
152 |
by (Asm_simp_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
153 |
qed "lift_JN"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
154 |
Addsimps [lift_JN]; |
7525 | 155 |
|
7186 | 156 |
(*** Safety: co, stable, invariant ***) |
157 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
158 |
Goalw [lift_def, lift_set_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
159 |
"(lift i F : (lift_set i A) co (lift_set i B)) = (F : A co B)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
160 |
by (asm_simp_tac (simpset() addsimps [rename_constrains]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
161 |
qed "lift_constrains"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7688
diff
changeset
|
162 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
163 |
Goalw [lift_def, lift_set_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
164 |
"(lift i F : stable (lift_set i A)) = (F : stable A)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
165 |
by (asm_simp_tac (simpset() addsimps [rename_stable]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
166 |
qed "lift_stable"; |
7186 | 167 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
168 |
Goalw [lift_def, lift_set_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
169 |
"(lift i F : invariant (lift_set i A)) = (F : invariant A)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
170 |
by (asm_simp_tac (simpset() addsimps [rename_invariant]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
171 |
qed "lift_invariant"; |
7186 | 172 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
173 |
Goalw [lift_def, lift_set_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
174 |
"(lift i F : (lift_set i A) Co (lift_set i B)) = (F : A Co B)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
175 |
by (asm_simp_tac (simpset() addsimps [rename_Constrains]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
176 |
qed "lift_Constrains"; |
7186 | 177 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
178 |
Goalw [lift_def, lift_set_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
179 |
"(lift i F : Stable (lift_set i A)) = (F : Stable A)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
180 |
by (asm_simp_tac (simpset() addsimps [rename_Stable]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
181 |
qed "lift_Stable"; |
7186 | 182 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
183 |
Goalw [lift_def, lift_set_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
184 |
"(lift i F : Always (lift_set i A)) = (F : Always A)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
185 |
by (asm_simp_tac (simpset() addsimps [rename_Always]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
186 |
qed "lift_Always"; |
7361 | 187 |
|
7525 | 188 |
(*** Progress: transient, ensures ***) |
189 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
190 |
Goalw [lift_def, lift_set_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
191 |
"(lift i F : transient (lift_set i A)) = (F : transient A)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
192 |
by (asm_simp_tac (simpset() addsimps [rename_transient]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
193 |
qed "lift_transient"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
194 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
195 |
Goalw [lift_def, lift_set_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
196 |
"(lift i F : (lift_set i A) ensures (lift_set i B)) = \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
197 |
\ (F : A ensures B)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
198 |
by (asm_simp_tac (simpset() addsimps [rename_ensures]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
199 |
qed "lift_ensures"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
200 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
201 |
Goalw [lift_def, lift_set_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
202 |
"(lift i F : (lift_set i A) leadsTo (lift_set i B)) = \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
203 |
\ (F : A leadsTo B)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
204 |
by (asm_simp_tac (simpset() addsimps [rename_leadsTo]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
205 |
qed "lift_leadsTo"; |
7525 | 206 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
207 |
Goalw [lift_def, lift_set_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
208 |
"(lift i F : (lift_set i A) LeadsTo (lift_set i B)) = \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
209 |
\ (F : A LeadsTo B)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
210 |
by (asm_simp_tac (simpset() addsimps [rename_LeadsTo]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
211 |
qed "lift_LeadsTo"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
212 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
213 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
214 |
(** guarantees **) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
215 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
216 |
Goalw [lift_def] |
10834 | 217 |
"(lift i F : (lift i ` X) guarantees (lift i ` Y)) = \ |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
218 |
\ (F : X guarantees Y)"; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
219 |
by (stac (bij_lift_map RS rename_rename_guarantees_eq RS sym) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
220 |
by (asm_simp_tac (simpset() addsimps [o_def]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
221 |
qed "lift_lift_guarantees_eq"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
222 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
223 |
Goal "(lift i F : X guarantees Y) = \ |
10834 | 224 |
\ (F : (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))"; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
225 |
by (asm_simp_tac |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
226 |
(simpset() addsimps [bij_lift_map RS rename_guarantees_eq_rename_inv, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
227 |
lift_def]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
228 |
qed "lift_guarantees_eq_lift_inv"; |
7525 | 229 |
|
230 |
||
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
231 |
(*** We devote an ENORMOUS effort to proving lift_transient_eq_disj, |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
232 |
which is used only in TimerArray and perhaps isn't even essential |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
233 |
there! |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
234 |
***) |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
235 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
236 |
(*To preserve snd means that the second component is there just to allow |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
237 |
guarantees properties to be stated. Converse fails, for lift i F can |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
238 |
change function components other than i*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
239 |
Goal "F : preserves snd ==> lift i F : preserves snd"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
240 |
by (dres_inst_tac [("w1", "snd")] (impOfSubs subset_preserves_o) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
241 |
by (asm_simp_tac (simpset() addsimps [lift_def, rename_preserves]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
242 |
by (full_simp_tac (simpset() addsimps [lift_map_def, o_def, split_def]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
243 |
qed "lift_preserves_snd_I"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
244 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
245 |
Goal "(delete_map i g) = (delete_map i g') ==> EX x. g = g'(i:=x)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
246 |
by (dres_inst_tac [("f", "insert_map i (g i)")] arg_cong 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
247 |
by (full_simp_tac (simpset() addsimps [insert_map_delete_map_eq]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
248 |
by (etac exI 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
249 |
bind_thm ("delete_map_eqE", result() RS exE); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
250 |
AddSEs [delete_map_eqE]; |
7186 | 251 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
252 |
Goal "[| delete_map j g = delete_map j g'; i~=j |] ==> g i = g' i"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
253 |
by (Force_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
254 |
qed "delete_map_neq_apply"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
255 |
|
8703 | 256 |
(*A set of the form (A <*> UNIV) ignores the second (dummy) state component*) |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
257 |
|
10834 | 258 |
Goal "(f o fst) -` A = (f-`A) <*> UNIV"; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
259 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
260 |
qed "vimage_o_fst_eq"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
261 |
|
10834 | 262 |
Goal "(sub i -`A) <*> UNIV = lift_set i (A <*> UNIV)"; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
263 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
264 |
qed "vimage_sub_eq_lift_set"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
265 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
266 |
Addsimps [vimage_o_fst_eq, vimage_sub_eq_lift_set]; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
267 |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
268 |
Goalw [extend_act_def] |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
269 |
"((s,s') : extend_act (%(x,u::unit). lift_map i x) act) = \ |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
270 |
\ ((drop_map i s, drop_map i s') : act)"; |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
271 |
by Auto_tac; |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
272 |
by (rtac bexI 1); |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
273 |
by Auto_tac; |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
274 |
qed "mem_lift_act_iff"; |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
275 |
AddIffs [mem_lift_act_iff]; |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
276 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
277 |
Goal "[| F : preserves snd; i~=j |] \ |
8703 | 278 |
\ ==> lift j F : stable (lift_set i (A <*> UNIV))"; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
279 |
by (auto_tac (claset(), |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
280 |
simpset() addsimps [lift_def, lift_set_def, |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
281 |
stable_def, constrains_def, rename_def, |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
282 |
extend_def, mem_rename_set_iff])); |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
283 |
by (auto_tac (claset() addSDs [preserves_imp_eq], |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
284 |
simpset() addsimps [lift_map_def, drop_map_def])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
285 |
by (dres_inst_tac [("x", "i")] fun_cong 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
286 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
287 |
qed "preserves_snd_lift_stable"; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
288 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
289 |
(*If i~=j then lift j F does nothing to lift_set i, and the |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
290 |
premise ensures A<=B.*) |
8703 | 291 |
Goal "[| F i : (A <*> UNIV) co (B <*> UNIV); \ |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
292 |
\ F j : preserves snd |] \ |
8703 | 293 |
\ ==> lift j (F j) : (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
294 |
by (case_tac "i=j" 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
295 |
by (asm_full_simp_tac (simpset() addsimps [lift_def, lift_set_def, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
296 |
rename_constrains]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
297 |
by (etac (preserves_snd_lift_stable RS stableD RS constrains_weaken_R) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
298 |
by (assume_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
299 |
by (etac (constrains_imp_subset RS lift_set_mono) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
300 |
qed "constrains_imp_lift_constrains"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
301 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
302 |
(** Lemmas for the transient theorem **) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
303 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
304 |
Goal "(insert_map i t f)(i := s) = insert_map i s f"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
305 |
by (rtac ext 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
306 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
307 |
qed "insert_map_upd_same"; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
308 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
309 |
Goal "(insert_map j t f)(i := s) = \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
310 |
\ (if i=j then insert_map i s f \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
311 |
\ else if i<j then insert_map j t (f(i:=s)) \ |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11467
diff
changeset
|
312 |
\ else insert_map j t (f(i - Suc 0 := s)))"; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
313 |
by (rtac ext 1); |
8866 | 314 |
by (auto_tac (claset(), simpset() addsplits [nat_diff_split])); |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
315 |
by (ALLGOALS arith_tac); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
316 |
qed "insert_map_upd"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
317 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
318 |
Goal "[| insert_map i s f = insert_map j t g; i~=j |] \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
319 |
\ ==> EX g'. insert_map i s' f = insert_map j t g'"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
320 |
by (stac (insert_map_upd_same RS sym) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
321 |
by (etac ssubst 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
322 |
by (asm_simp_tac (HOL_ss addsimps [insert_map_upd]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
323 |
by (Blast_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
324 |
qed "insert_map_eq_diff"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
325 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
326 |
Goalw [lift_map_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
327 |
"[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv)); i~=j |] \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
328 |
\ ==> EX g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
329 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
330 |
by (blast_tac (claset() addDs [insert_map_eq_diff]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
331 |
qed "lift_map_eq_diff"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
332 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
333 |
Goal "F : preserves snd \ |
8703 | 334 |
\ ==> (lift i F : transient (lift_set j (A <*> UNIV))) = \ |
335 |
\ (i=j & F : transient (A <*> UNIV) | A={})"; |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
336 |
by (case_tac "i=j" 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
337 |
by (auto_tac (claset(), simpset() addsimps [lift_transient])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
338 |
by (auto_tac (claset(), |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
339 |
simpset() addsimps [lift_set_def, lift_def, transient_def, |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
340 |
rename_def, extend_def, Domain_extend_act])); |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
341 |
by (dtac subsetD 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
342 |
by (Blast_tac 1); |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8065
diff
changeset
|
343 |
by Auto_tac; |
11467 | 344 |
by (rename_tac "s f uu s' f' uu'" 1); |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
345 |
by (subgoal_tac "f'=f & uu'=uu" 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
346 |
by (force_tac (claset() addSDs [preserves_imp_eq], simpset()) 2); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
347 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
348 |
by (dtac sym 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
349 |
by (dtac subsetD 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
350 |
by (rtac ImageI 1); |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
351 |
by (etac |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
352 |
(bij_lift_map RS good_map_bij RS export (mem_extend_act_iff RS iffD2)) 1); |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
353 |
by (Force_tac 1); |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
354 |
by (etac (lift_map_eq_diff RS exE) 1); |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8948
diff
changeset
|
355 |
by Auto_tac; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
356 |
qed "lift_transient_eq_disj"; |
8041 | 357 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
358 |
(*USELESS??*) |
10834 | 359 |
Goal "lift_map i ` (A <*> UNIV) = \ |
8703 | 360 |
\ (UN s:A. UN f. {insert_map i s f}) <*> UNIV"; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
361 |
by (auto_tac (claset() addSIs [bexI, image_eqI], |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
362 |
simpset() addsimps [lift_map_def])); |
10918 | 363 |
by (rtac (split_conv RS sym) 1); |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
364 |
qed "lift_map_image_Times"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
365 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
366 |
Goal "(lift i F : preserves v) = (F : preserves (v o lift_map i))"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
367 |
by (simp_tac (simpset() addsimps [lift_def, rename_preserves]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
368 |
qed "lift_preserves_eq"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
369 |
|
8327 | 370 |
(*A useful rewrite. If o, sub have been rewritten out already then can also |
371 |
use it as rewrite_rule [sub_def, o_def] lift_preserves_sub*) |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
372 |
Goal "F : preserves snd \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
373 |
\ ==> lift i F : preserves (v o sub j o fst) = \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
374 |
\ (if i=j then F : preserves (v o fst) else True)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
375 |
by (dtac (impOfSubs subset_preserves_o) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
376 |
by (full_simp_tac (simpset() addsimps [lift_preserves_eq, o_def, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
377 |
drop_map_lift_map_eq]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
378 |
by (asm_simp_tac (simpset() delcongs [if_weak_cong] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
379 |
addsimps [lift_map_def, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
380 |
eq_commute, split_def, o_def]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
381 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
382 |
qed "lift_preserves_sub"; |
7186 | 383 |
|
384 |
||
8314 | 385 |
(*** Lemmas to handle function composition (o) more consistently ***) |
7186 | 386 |
|
8314 | 387 |
(*Lets us prove one version of a theorem and store others*) |
388 |
Goal "f o g = h ==> f' o f o g = f' o h"; |
|
389 |
by (asm_full_simp_tac (simpset() addsimps [expand_fun_eq, o_def]) 1); |
|
390 |
qed "o_equiv_assoc"; |
|
7186 | 391 |
|
8314 | 392 |
Goal "f o g = h ==> ALL x. f(g x) = h x"; |
393 |
by (asm_full_simp_tac (simpset() addsimps [expand_fun_eq, o_def]) 1); |
|
394 |
qed "o_equiv_apply"; |
|
395 |
||
396 |
fun make_o_equivs th = |
|
397 |
[th, |
|
398 |
th RS o_equiv_assoc |> simplify (HOL_ss addsimps [o_assoc]), |
|
399 |
th RS o_equiv_apply |> simplify (HOL_ss addsimps [o_def, sub_def])]; |
|
7186 | 400 |
|
8314 | 401 |
Addsimps (make_o_equivs fst_o_funPair @ make_o_equivs snd_o_funPair); |
402 |
||
403 |
Goal "sub i o fst o lift_map i = fst"; |
|
404 |
by (rtac ext 1); |
|
405 |
by (auto_tac (claset(), simpset() addsimps [o_def, lift_map_def, sub_def])); |
|
406 |
qed "fst_o_lift_map"; |
|
7186 | 407 |
|
8314 | 408 |
Goal "snd o lift_map i = snd o snd"; |
409 |
by (rtac ext 1); |
|
410 |
by (auto_tac (claset(), simpset() addsimps [o_def, lift_map_def])); |
|
411 |
qed "snd_o_lift_map"; |
|
412 |
||
413 |
Addsimps (make_o_equivs fst_o_lift_map @ make_o_equivs snd_o_lift_map); |
|
414 |
||
415 |
||
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
416 |
(*** More lemmas about extend and project |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
417 |
They could be moved to {Extend,Project}.ML, but DON'T need the locale ***) |
8314 | 418 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
419 |
Goal "extend_act h' (extend_act h act) = \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
420 |
\ extend_act (%(x,(y,y')). h'(h(x,y),y')) act"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
421 |
by (auto_tac (claset() addSEs [rev_bexI], |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
422 |
simpset() addsimps [extend_act_def])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
423 |
by (ALLGOALS Blast_tac); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
424 |
qed "extend_act_extend_act"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
425 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
426 |
Goal "project_act h (project_act h' act) = \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
427 |
\ project_act (%(x,(y,y')). h'(h(x,y),y')) act"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
428 |
by (auto_tac (claset() addSEs [rev_bexI], |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
429 |
simpset() addsimps [project_act_def])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
430 |
qed "project_act_project_act"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
431 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
432 |
Goal "project_act h (extend_act h' act) = \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
433 |
\ {(x,x'). EX s s' y y' z. (s,s') : act & \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
434 |
\ h(x,y) = h'(s,z) & h(x',y') = h'(s',z)}"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
435 |
by (simp_tac (simpset() addsimps [extend_act_def, project_act_def]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
436 |
by (Blast_tac 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
437 |
qed "project_act_extend_act"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
438 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
439 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
440 |
(*** OK and "lift" ***) |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
441 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
442 |
Goal "act <= {(x,x'). fst x = fst x'} ==> act : UNION (preserves fst) Acts"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
443 |
by (res_inst_tac [("a","mk_program(UNIV,{act},UNIV)")] UN_I 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
444 |
by (auto_tac (claset(), |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
445 |
simpset() addsimps [preserves_def,stable_def,constrains_def])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
446 |
qed "act_in_UNION_preserves_fst"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
447 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
448 |
Goal "[| ALL i:I. F i : preserves snd; \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
449 |
\ ALL i:I. UNION (preserves fst) Acts <= AllowedActs (F i) |] \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
450 |
\ ==> OK I (%i. lift i (F i))"; |
11170
015af2fc7026
simplified proofs for splitI and splitD, added splitD'
oheimb
parents:
10918
diff
changeset
|
451 |
by (auto_tac (claset(), |
015af2fc7026
simplified proofs for splitI and splitD, added splitD'
oheimb
parents:
10918
diff
changeset
|
452 |
simpset() addsimps [OK_def, lift_def, rename_def, export Acts_extend])); |
015af2fc7026
simplified proofs for splitI and splitD, added splitD'
oheimb
parents:
10918
diff
changeset
|
453 |
by (simp_tac ( |
015af2fc7026
simplified proofs for splitI and splitD, added splitD'
oheimb
parents:
10918
diff
changeset
|
454 |
simpset() addsimps [export AllowedActs_extend,project_act_extend_act]) 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
455 |
by (rename_tac "act" 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
456 |
by (subgoal_tac |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
457 |
"{(x, x'). EX s f u s' f' u'. \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
458 |
\ ((s, f, u), s', f', u') : act & \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
459 |
\ lift_map j x = lift_map i (s, f, u) & \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
460 |
\ lift_map j x' = lift_map i (s', f', u')} \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
461 |
\ <= {(x,x'). fst x = fst x'}" 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
462 |
by (blast_tac (claset() addIs [act_in_UNION_preserves_fst]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
463 |
by (Clarify_tac 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
464 |
by (REPEAT (dres_inst_tac [("x","j")] fun_cong 1) ); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
465 |
by (dres_inst_tac [("x","i")] bspec 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
466 |
by (assume_tac 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
467 |
by (ftac preserves_imp_eq 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
468 |
by Auto_tac; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
469 |
qed "UNION_OK_lift_I"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
470 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
471 |
Goal "[| ALL i:I. F i : preserves snd; \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
472 |
\ ALL i:I. preserves fst <= Allowed (F i) |] \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
473 |
\ ==> OK I (%i. lift i (F i))"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
474 |
by (asm_full_simp_tac |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
475 |
(simpset() addsimps [safety_prop_AllowedActs_iff_Allowed, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
476 |
UNION_OK_lift_I]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
477 |
qed "OK_lift_I"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
478 |
|
10834 | 479 |
Goal "Allowed (lift i F) = lift i ` (Allowed F)"; |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
480 |
by (simp_tac (simpset() addsimps [lift_def, Allowed_rename]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
481 |
qed "Allowed_lift"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
482 |
Addsimps [Allowed_lift]; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
483 |
|
10834 | 484 |
Goal "lift i ` preserves v = preserves (v o drop_map i)"; |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
485 |
by (simp_tac (simpset() addsimps [rename_image_preserves, lift_def, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
486 |
inv_lift_map_eq]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
487 |
qed "lift_image_preserves"; |