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