author | paulson |
Fri, 12 May 2000 15:14:35 +0200 | |
changeset 8866 | 9ac6a18d363b |
parent 8703 | 816d8f6513be |
child 8948 | b797cfa3548d |
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"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
49 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
50 |
Goalw [lift_map_def] "inj (lift_map i)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
51 |
by (rtac injI 1); |
7688 | 52 |
by Auto_tac; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
53 |
qed "inj_lift_map"; |
7688 | 54 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
55 |
(*** Surjectiveness proof ***) |
7186 | 56 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
57 |
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
|
58 |
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
|
59 |
qed "lift_map_drop_map_eq"; |
7186 | 60 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
61 |
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
|
62 |
by (dres_inst_tac [("f", "lift_map i")] arg_cong 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
63 |
by (full_simp_tac (simpset() addsimps [lift_map_drop_map_eq]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
64 |
qed "drop_map_inject"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
65 |
AddSDs [drop_map_inject]; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
66 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
67 |
Goal "surj (lift_map i)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
68 |
by (rtac surjI 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
69 |
by (rtac lift_map_drop_map_eq 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
70 |
qed "surj_lift_map"; |
7186 | 71 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
72 |
Goal "bij (lift_map i)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
73 |
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
|
74 |
qed "bij_lift_map"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
75 |
AddIffs [bij_lift_map]; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
76 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
77 |
AddIffs [bij_lift_map RS mem_rename_act_iff]; |
7186 | 78 |
|
8251
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); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
81 |
by (rtac lift_map_drop_map_eq 2); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
82 |
by (rtac drop_map_lift_map_eq 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
83 |
qed "inv_lift_map_eq"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
84 |
Addsimps [inv_lift_map_eq]; |
7688 | 85 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
86 |
Goal "inv (drop_map i) = lift_map i"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
87 |
by (rtac inv_equality 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
88 |
by (rtac drop_map_lift_map_eq 2); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
89 |
by (rtac lift_map_drop_map_eq 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
90 |
qed "inv_drop_map_eq"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
91 |
Addsimps [inv_drop_map_eq]; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
92 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
93 |
Goal "bij (drop_map i)"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
94 |
by (simp_tac (simpset() delsimps [inv_lift_map_eq] |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
95 |
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
|
96 |
qed "bij_drop_map"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
97 |
AddIffs [bij_drop_map]; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
98 |
|
7688 | 99 |
(*** sub ***) |
100 |
||
7947 | 101 |
Goal "sub i f = f i"; |
102 |
by (simp_tac (simpset() addsimps [sub_def]) 1); |
|
103 |
qed "sub_apply"; |
|
104 |
Addsimps [sub_apply]; |
|
7688 | 105 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
106 |
Goal "lift_set i {s. P s} = {s. P (drop_map i s)}"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
107 |
by (rtac set_ext 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
108 |
by (asm_simp_tac (simpset() delsimps [image_Collect] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
109 |
addsimps [lift_set_def, rename_set_eq_Collect]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
110 |
qed "lift_set_eq_Collect"; |
7688 | 111 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
112 |
Goalw [lift_set_def] "lift_set i {} = {}"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
113 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
114 |
qed "lift_set_empty"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
115 |
Addsimps [lift_set_empty]; |
7688 | 116 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
117 |
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
|
118 |
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
|
119 |
qed "lift_set_iff"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
120 |
AddIffs [lift_set_iff]; |
7186 | 121 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
122 |
(*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
|
123 |
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
|
124 |
by (asm_simp_tac (simpset() addsimps [lift_set_def, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
125 |
mem_rename_set_iff, drop_map_def]) 1); |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
126 |
qed "lift_set_iff2"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
127 |
AddIffs [lift_set_iff2]; |
7525 | 128 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
129 |
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
|
130 |
by (etac image_mono 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
131 |
qed "lift_set_mono"; |
7525 | 132 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
133 |
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
|
134 |
by (asm_simp_tac (simpset() addsimps [image_Un]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
135 |
qed "lift_set_Un_distrib"; |
7525 | 136 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
137 |
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
|
138 |
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
|
139 |
qed "lift_set_Diff_distrib"; |
7525 | 140 |
|
141 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
142 |
(*** the lattice operations ***) |
7525 | 143 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
144 |
Goalw [lift_def] "lift i SKIP = SKIP"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
145 |
by (Asm_simp_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
146 |
qed "lift_SKIP"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
147 |
Addsimps [lift_SKIP]; |
7525 | 148 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
149 |
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
|
150 |
by (Asm_simp_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
151 |
qed "lift_Join"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
152 |
Addsimps [lift_Join]; |
7688 | 153 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
154 |
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
|
155 |
by (Asm_simp_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
156 |
qed "lift_JN"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
157 |
Addsimps [lift_JN]; |
7525 | 158 |
|
7186 | 159 |
(*** Safety: co, stable, invariant ***) |
160 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
161 |
Goalw [lift_def, lift_set_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
162 |
"(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
|
163 |
by (asm_simp_tac (simpset() addsimps [rename_constrains]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
164 |
qed "lift_constrains"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7688
diff
changeset
|
165 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
166 |
Goalw [lift_def, lift_set_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
167 |
"(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
|
168 |
by (asm_simp_tac (simpset() addsimps [rename_stable]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
169 |
qed "lift_stable"; |
7186 | 170 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
171 |
Goalw [lift_def, lift_set_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
172 |
"(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
|
173 |
by (asm_simp_tac (simpset() addsimps [rename_invariant]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
174 |
qed "lift_invariant"; |
7186 | 175 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
176 |
Goalw [lift_def, lift_set_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
177 |
"(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
|
178 |
by (asm_simp_tac (simpset() addsimps [rename_Constrains]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
179 |
qed "lift_Constrains"; |
7186 | 180 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
181 |
Goalw [lift_def, lift_set_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
182 |
"(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
|
183 |
by (asm_simp_tac (simpset() addsimps [rename_Stable]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
184 |
qed "lift_Stable"; |
7186 | 185 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
186 |
Goalw [lift_def, lift_set_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
187 |
"(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
|
188 |
by (asm_simp_tac (simpset() addsimps [rename_Always]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
189 |
qed "lift_Always"; |
7361 | 190 |
|
7525 | 191 |
(*** Progress: transient, ensures ***) |
192 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
193 |
Goalw [lift_def, lift_set_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
194 |
"(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
|
195 |
by (asm_simp_tac (simpset() addsimps [rename_transient]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
196 |
qed "lift_transient"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
197 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
198 |
Goalw [lift_def, lift_set_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
199 |
"(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
|
200 |
\ (F : A ensures B)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
201 |
by (asm_simp_tac (simpset() addsimps [rename_ensures]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
202 |
qed "lift_ensures"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
203 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
204 |
Goalw [lift_def, lift_set_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
205 |
"(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
|
206 |
\ (F : A leadsTo B)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
207 |
by (asm_simp_tac (simpset() addsimps [rename_leadsTo]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
208 |
qed "lift_leadsTo"; |
7525 | 209 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
210 |
Goalw [lift_def, lift_set_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
211 |
"(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
|
212 |
\ (F : A LeadsTo B)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
213 |
by (asm_simp_tac (simpset() addsimps [rename_LeadsTo]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
214 |
qed "lift_LeadsTo"; |
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 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
217 |
(** guarantees **) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
218 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
219 |
Goalw [lift_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
220 |
"(lift i F : (lift i `` X) guarantees[v o drop_map i] (lift i `` Y)) = \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
221 |
\ (F : X guarantees[v] Y)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
222 |
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
|
223 |
by (asm_simp_tac (simpset() addsimps [o_def]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
224 |
qed "lift_lift_guarantees_eq"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
225 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
226 |
Goal "(lift i F : X guarantees[v] Y) = \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
227 |
\ (F : (rename (drop_map i) `` X) guarantees[v o lift_map i] \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
228 |
\ (rename (drop_map i) `` Y))"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
229 |
by (asm_simp_tac |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
230 |
(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
|
231 |
lift_def]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
232 |
qed "lift_guarantees_eq_lift_inv"; |
7525 | 233 |
|
234 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
235 |
(*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
|
236 |
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
|
237 |
change function components other than i*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
238 |
Goal "F : preserves snd ==> lift i F : preserves snd"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
239 |
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
|
240 |
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
|
241 |
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
|
242 |
qed "lift_preserves_snd_I"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
243 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
244 |
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
|
245 |
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
|
246 |
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
|
247 |
by (etac exI 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
248 |
bind_thm ("delete_map_eqE", result() RS exE); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
249 |
AddSEs [delete_map_eqE]; |
7186 | 250 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
251 |
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
|
252 |
by (Force_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
253 |
qed "delete_map_neq_apply"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
254 |
|
8703 | 255 |
(*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
|
256 |
|
8703 | 257 |
Goal "(f o fst) -`` A = (f-``A) <*> UNIV"; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
258 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
259 |
qed "vimage_o_fst_eq"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
260 |
|
8703 | 261 |
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
|
262 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
263 |
qed "vimage_sub_eq_lift_set"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
264 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
265 |
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
|
266 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
267 |
Goal "[| F : preserves snd; i~=j |] \ |
8703 | 268 |
\ ==> lift j F : stable (lift_set i (A <*> UNIV))"; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
269 |
by (auto_tac (claset(), |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
270 |
simpset() addsimps [lift_def, lift_set_def, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
271 |
stable_def, constrains_def, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
272 |
mem_rename_act_iff, mem_rename_set_iff])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
273 |
by (auto_tac (claset() addSDs [preserves_imp_eq], |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
274 |
simpset() addsimps [lift_map_def, drop_map_def])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
275 |
by (dres_inst_tac [("x", "i")] fun_cong 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
276 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
277 |
qed "preserves_snd_lift_stable"; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
278 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
279 |
(*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
|
280 |
premise ensures A<=B.*) |
8703 | 281 |
Goal "[| F i : (A <*> UNIV) co (B <*> UNIV); \ |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
282 |
\ F j : preserves snd |] \ |
8703 | 283 |
\ ==> 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
|
284 |
by (case_tac "i=j" 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
285 |
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
|
286 |
rename_constrains]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
287 |
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
|
288 |
by (assume_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
289 |
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
|
290 |
qed "constrains_imp_lift_constrains"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
291 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
292 |
(** Lemmas for the transient theorem **) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
293 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
294 |
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
|
295 |
by (rtac ext 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
296 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
297 |
qed "insert_map_upd_same"; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
298 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
299 |
Goal "(insert_map j t f)(i := s) = \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
300 |
\ (if i=j then insert_map i s f \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
301 |
\ else if i<j then insert_map j t (f(i:=s)) \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
302 |
\ else insert_map j t (f(i-1:=s)))"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
303 |
by (rtac ext 1); |
8866 | 304 |
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
|
305 |
by (ALLGOALS arith_tac); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
306 |
qed "insert_map_upd"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
307 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
308 |
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
|
309 |
\ ==> 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
|
310 |
by (stac (insert_map_upd_same RS sym) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
311 |
by (etac ssubst 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
312 |
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
|
313 |
by (Blast_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
314 |
qed "insert_map_eq_diff"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
315 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
316 |
Goalw [lift_map_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
317 |
"[| 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
|
318 |
\ ==> 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
|
319 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
320 |
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
|
321 |
qed "lift_map_eq_diff"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
322 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
323 |
Goal "F : preserves snd \ |
8703 | 324 |
\ ==> (lift i F : transient (lift_set j (A <*> UNIV))) = \ |
325 |
\ (i=j & F : transient (A <*> UNIV) | A={})"; |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
326 |
by (case_tac "i=j" 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
327 |
by (auto_tac (claset(), simpset() addsimps [lift_transient])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
328 |
by (auto_tac (claset(), |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
329 |
simpset() addsimps [lift_def, transient_def, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
330 |
Domain_rename_act])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
331 |
by (dtac subsetD 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
332 |
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
|
333 |
by Auto_tac; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
334 |
ren "s f uu s' f' uu'" 1; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
335 |
by (subgoal_tac "f'=f & uu'=uu" 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
336 |
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
|
337 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
338 |
by (dtac sym 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
339 |
by (dtac subsetD 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
340 |
by (rtac ImageI 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
341 |
by (etac rename_actI 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
342 |
by (force_tac (claset(), simpset() addsimps [lift_set_def]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
343 |
by (etac (lift_map_eq_diff RS exE) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
344 |
by (assume_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
345 |
by (dtac ComplD 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
346 |
by (etac notE 1 THEN etac ssubst 1 THEN Fast_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
347 |
qed "lift_transient_eq_disj"; |
8041 | 348 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
349 |
(*USELESS??*) |
8703 | 350 |
Goal "lift_map i `` (A <*> UNIV) = \ |
351 |
\ (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
|
352 |
by (auto_tac (claset() addSIs [bexI, image_eqI], |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
353 |
simpset() addsimps [lift_map_def])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
354 |
by (rtac (split RS sym) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
355 |
qed "lift_map_image_Times"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
356 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
357 |
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
|
358 |
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
|
359 |
qed "lift_preserves_eq"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
360 |
|
8327 | 361 |
(*A useful rewrite. If o, sub have been rewritten out already then can also |
362 |
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
|
363 |
Goal "F : preserves snd \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
364 |
\ ==> 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
|
365 |
\ (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
|
366 |
by (dtac (impOfSubs subset_preserves_o) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
367 |
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
|
368 |
drop_map_lift_map_eq]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
369 |
by (asm_simp_tac (simpset() delcongs [if_weak_cong] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
370 |
addsimps [lift_map_def, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
371 |
eq_commute, split_def, o_def]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
372 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
373 |
qed "lift_preserves_sub"; |
7186 | 374 |
|
375 |
||
8314 | 376 |
(*** Lemmas to handle function composition (o) more consistently ***) |
7186 | 377 |
|
8314 | 378 |
(*Lets us prove one version of a theorem and store others*) |
379 |
Goal "f o g = h ==> f' o f o g = f' o h"; |
|
380 |
by (asm_full_simp_tac (simpset() addsimps [expand_fun_eq, o_def]) 1); |
|
381 |
qed "o_equiv_assoc"; |
|
7186 | 382 |
|
8314 | 383 |
Goal "f o g = h ==> ALL x. f(g x) = h x"; |
384 |
by (asm_full_simp_tac (simpset() addsimps [expand_fun_eq, o_def]) 1); |
|
385 |
qed "o_equiv_apply"; |
|
386 |
||
387 |
fun make_o_equivs th = |
|
388 |
[th, |
|
389 |
th RS o_equiv_assoc |> simplify (HOL_ss addsimps [o_assoc]), |
|
390 |
th RS o_equiv_apply |> simplify (HOL_ss addsimps [o_def, sub_def])]; |
|
7186 | 391 |
|
8314 | 392 |
Addsimps (make_o_equivs fst_o_funPair @ make_o_equivs snd_o_funPair); |
393 |
||
394 |
Goal "sub i o fst o lift_map i = fst"; |
|
395 |
by (rtac ext 1); |
|
396 |
by (auto_tac (claset(), simpset() addsimps [o_def, lift_map_def, sub_def])); |
|
397 |
qed "fst_o_lift_map"; |
|
7186 | 398 |
|
8314 | 399 |
Goal "snd o lift_map i = snd o snd"; |
400 |
by (rtac ext 1); |
|
401 |
by (auto_tac (claset(), simpset() addsimps [o_def, lift_map_def])); |
|
402 |
qed "snd_o_lift_map"; |
|
403 |
||
404 |
Addsimps (make_o_equivs fst_o_lift_map @ make_o_equivs snd_o_lift_map); |
|
405 |
||
406 |
||
407 |