author | oheimb |
Thu, 30 Aug 2001 15:47:30 +0200 | |
changeset 11507 | 4b32a46ffd29 |
parent 10834 | a7897aebbffc |
child 13550 | 5a176b8dda84 |
permissions | -rw-r--r-- |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/UNITY/Rename.ML |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
4 |
Copyright 2000 University of Cambridge |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
5 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
6 |
*) |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
7 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
8 |
Addsimps [image_inv_f_f, image_surj_f_inv_f]; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
9 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
10 |
Goal "bij h ==> good_map (%(x,u). h x)"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
11 |
by (rtac good_mapI 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
12 |
by (rewrite_goals_tac [bij_def, inj_on_def, surj_def]); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
13 |
by Auto_tac; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
14 |
qed "good_map_bij"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
15 |
Addsimps [good_map_bij]; |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
16 |
AddIs [good_map_bij]; |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
17 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
18 |
fun bij_export th = good_map_bij RS export th |> simplify (simpset()); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
19 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
20 |
Goalw [bij_def, split_def] "bij h ==> fst (inv (%(x,u). h x) s) = inv h s"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
21 |
by (Clarify_tac 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
22 |
by (subgoal_tac "surj (%p. h (fst p))" 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
23 |
by (asm_full_simp_tac (simpset() addsimps [surj_def]) 2); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
24 |
by (etac injD 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
25 |
by (asm_simp_tac (simpset() addsimps [surj_f_inv_f]) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
26 |
by (etac surj_f_inv_f 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
27 |
qed "fst_o_inv_eq_inv"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
28 |
|
10834 | 29 |
Goal "bij h ==> z : h`A = (inv h z : A)"; |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
30 |
by (auto_tac (claset() addSIs [image_eqI], |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
31 |
simpset() addsimps [bij_is_inj, bij_is_surj RS surj_f_inv_f])); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
32 |
qed "mem_rename_set_iff"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
33 |
|
10834 | 34 |
Goal "extend_set (%(x,u). h x) A = h`A"; |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
35 |
by (auto_tac (claset() addSIs [image_eqI], |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
36 |
simpset() addsimps [extend_set_def])); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
37 |
qed "extend_set_eq_image"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
38 |
Addsimps [extend_set_eq_image]; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
39 |
|
10834 | 40 |
Goalw [rename_def] "Init (rename h F) = h`(Init F)"; |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
41 |
by (Simp_tac 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
42 |
qed "Init_rename"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
43 |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9190
diff
changeset
|
44 |
Addsimps [Init_rename]; |
8327 | 45 |
|
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
46 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
47 |
(*** inverse properties ***) |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
48 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
49 |
Goalw [bij_def] |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
50 |
"bij h \ |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
51 |
\ ==> extend_set (%(x,u::'c). inv h x) = project_set (%(x,u::'c). h x)"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
52 |
by (rtac ext 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
53 |
by (auto_tac (claset() addSIs [image_eqI], |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
54 |
simpset() addsimps [extend_set_def, project_set_def, |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
55 |
surj_f_inv_f])); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
56 |
qed "extend_set_inv"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
57 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
58 |
(** for "rename" (programs) **) |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
59 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
60 |
Goal "bij h \ |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
61 |
\ ==> extend_act (%(x,u::'c). h x) = project_act (%(x,u::'c). inv h x)"; |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
62 |
by (rtac ext 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
63 |
by (auto_tac (claset() addSIs [image_eqI], |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
64 |
simpset() addsimps [extend_act_def, project_act_def, bij_def, |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
65 |
surj_f_inv_f])); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
66 |
qed "bij_extend_act_eq_project_act"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
67 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
68 |
Goal "bij h ==> bij (extend_act (%(x,u::'c). h x))"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
69 |
by (rtac bijI 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
70 |
by (rtac (export inj_extend_act) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
71 |
by (auto_tac (claset(), simpset() addsimps [bij_extend_act_eq_project_act])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
72 |
by (blast_tac (claset() addIs [bij_imp_bij_inv, surjI, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
73 |
export extend_act_inverse]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
74 |
qed "bij_extend_act"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
75 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
76 |
Goal "bij h ==> bij (project_act (%(x,u::'c). h x))"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
77 |
by (ftac (bij_imp_bij_inv RS bij_extend_act) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
78 |
by (asm_full_simp_tac (simpset() addsimps [bij_extend_act_eq_project_act, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
79 |
bij_imp_bij_inv, inv_inv_eq]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
80 |
qed "bij_project_act"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
81 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
82 |
Goal "bij h ==> inv (project_act (%(x,u::'c). inv h x)) = \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
83 |
\ project_act (%(x,u::'c). h x)"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
84 |
by (asm_simp_tac |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
85 |
(simpset() addsimps [bij_extend_act_eq_project_act RS sym]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
86 |
by (rtac surj_imp_inv_eq 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
87 |
by (blast_tac (claset() addIs [bij_extend_act, bij_is_surj]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
88 |
by (asm_simp_tac (simpset() addsimps [export extend_act_inverse]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
89 |
qed "bij_inv_project_act_eq"; |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
90 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
91 |
Goal "bij h \ |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
92 |
\ ==> extend (%(x,u::'c). inv h x) = project (%(x,u::'c). h x) UNIV"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
93 |
by (ftac bij_imp_bij_inv 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
94 |
by (rtac ext 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
95 |
by (rtac program_equalityI 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
96 |
by (asm_simp_tac |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
97 |
(simpset() addsimps [export project_act_Id, export Acts_extend, |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
98 |
insert_Id_image_Acts, bij_extend_act_eq_project_act, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
99 |
inv_inv_eq]) 2); |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
100 |
by (asm_simp_tac (simpset() addsimps [extend_set_inv]) 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
101 |
by (asm_simp_tac |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
102 |
(simpset() addsimps [export AllowedActs_extend, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
103 |
export AllowedActs_project, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
104 |
bij_project_act, bij_vimage_eq_inv_image, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
105 |
bij_inv_project_act_eq]) 1); |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
106 |
qed "extend_inv"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
107 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
108 |
Goal "bij h ==> rename (inv h) (rename h F) = F"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
109 |
by (asm_simp_tac (simpset() addsimps [rename_def, extend_inv, |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
110 |
export extend_inverse]) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
111 |
qed "rename_inv_rename"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
112 |
Addsimps [rename_inv_rename]; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
113 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
114 |
Goal "bij h ==> rename h (rename (inv h) F) = F"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
115 |
by (ftac bij_imp_bij_inv 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
116 |
by (etac (inv_inv_eq RS subst) 1 THEN etac rename_inv_rename 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
117 |
qed "rename_rename_inv"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
118 |
Addsimps [rename_rename_inv]; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
119 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
120 |
Goal "bij h ==> rename (inv h) = inv (rename h)"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
121 |
by (rtac (inv_equality RS sym) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
122 |
by Auto_tac; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
123 |
qed "rename_inv_eq"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
124 |
|
8327 | 125 |
(** (rename h) is bijective <=> h is bijective **) |
126 |
||
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
127 |
Goal "bij h ==> bij (extend (%(x,u::'c). h x))"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
128 |
by (rtac bijI 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
129 |
by (blast_tac (claset() addIs [export inj_extend]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
130 |
by (res_inst_tac [("f","extend (%(x,u). inv h x)")] surjI 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
131 |
by (stac ((inst "f" "h" inv_inv_eq) RS sym) 1 |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
132 |
THEN stac extend_inv 2 THEN stac (export extend_inverse) 3); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
133 |
by (auto_tac (claset(), simpset() addsimps [bij_imp_bij_inv, inv_inv_eq])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
134 |
qed "bij_extend"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
135 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
136 |
Goal "bij h ==> bij (project (%(x,u::'c). h x) UNIV)"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
137 |
by (stac (extend_inv RS sym) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
138 |
by (auto_tac (claset(), simpset() addsimps [bij_imp_bij_inv, bij_extend])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
139 |
qed "bij_project"; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
140 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
141 |
Goal "bij h \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
142 |
\ ==> inv (project (%(x,u::'c). h x) UNIV) = extend (%(x,u::'c). h x)"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
143 |
by (rtac inj_imp_inv_eq 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
144 |
by (etac (bij_project RS bij_is_inj) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
145 |
by (asm_simp_tac (simpset() addsimps [export extend_inverse]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
146 |
qed "inv_project_eq"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
147 |
|
10834 | 148 |
Goal "bij h ==> Allowed (rename h F) = rename h ` Allowed F"; |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
149 |
by (asm_simp_tac (simpset() addsimps [rename_def, export Allowed_extend]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
150 |
by (stac bij_vimage_eq_inv_image 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
151 |
by (rtac bij_project 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
152 |
by (Blast_tac 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
153 |
by (asm_simp_tac (simpset() addsimps [inv_project_eq]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
154 |
qed "Allowed_rename"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
155 |
Addsimps [Allowed_rename]; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
156 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
157 |
Goal "bij h ==> bij (rename h)"; |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
158 |
by (asm_simp_tac (simpset() addsimps [rename_def, bij_extend]) 1); |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
159 |
qed "bij_rename"; |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
160 |
bind_thm ("surj_rename", bij_rename RS bij_is_surj); |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
161 |
|
8327 | 162 |
Goalw [inj_on_def] "inj (rename h) ==> inj h"; |
163 |
by Auto_tac; |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
164 |
by (dres_inst_tac [("x", "mk_program ({x}, {}, {})")] spec 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
165 |
by (dres_inst_tac [("x", "mk_program ({y}, {}, {})")] spec 1); |
8327 | 166 |
by (auto_tac (claset(), |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9190
diff
changeset
|
167 |
simpset() addsimps [program_equality_iff, |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9190
diff
changeset
|
168 |
rename_def, extend_def])); |
8327 | 169 |
qed "inj_rename_imp_inj"; |
170 |
||
171 |
Goalw [surj_def] "surj (rename h) ==> surj h"; |
|
172 |
by Auto_tac; |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
173 |
by (dres_inst_tac [("x", "mk_program ({y}, {}, {})")] spec 1); |
9190 | 174 |
by (auto_tac (claset(), |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9190
diff
changeset
|
175 |
simpset() addsimps [program_equality_iff, |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9190
diff
changeset
|
176 |
rename_def, extend_def])); |
8327 | 177 |
qed "surj_rename_imp_surj"; |
178 |
||
179 |
Goalw [bij_def] "bij (rename h) ==> bij h"; |
|
180 |
by (asm_simp_tac |
|
181 |
(simpset() addsimps [inj_rename_imp_inj, surj_rename_imp_surj]) 1); |
|
182 |
qed "bij_rename_imp_bij"; |
|
183 |
||
184 |
Goal "bij (rename h) = bij h"; |
|
185 |
by (blast_tac (claset() addIs [bij_rename, bij_rename_imp_bij]) 1); |
|
186 |
qed "bij_rename_iff"; |
|
187 |
AddIffs [bij_rename_iff]; |
|
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
188 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
189 |
|
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
190 |
(*** the lattice operations ***) |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
191 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
192 |
Goalw [rename_def] "bij h ==> rename h SKIP = SKIP"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
193 |
by (Asm_simp_tac 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
194 |
qed "rename_SKIP"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
195 |
Addsimps [rename_SKIP]; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
196 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
197 |
Goalw [rename_def] |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
198 |
"bij h ==> rename h (F Join G) = rename h F Join rename h G"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
199 |
by (asm_simp_tac (simpset() addsimps [export extend_Join]) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
200 |
qed "rename_Join"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
201 |
Addsimps [rename_Join]; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
202 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
203 |
Goalw [rename_def] "bij h ==> rename h (JOIN I F) = (JN i:I. rename h (F i))"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
204 |
by (asm_simp_tac (simpset() addsimps [export extend_JN]) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
205 |
qed "rename_JN"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
206 |
Addsimps [rename_JN]; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
207 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
208 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
209 |
(*** Strong Safety: co, stable ***) |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
210 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
211 |
Goalw [rename_def] |
10834 | 212 |
"bij h ==> (rename h F : (h`A) co (h`B)) = (F : A co B)"; |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
213 |
by (REPEAT (stac (extend_set_eq_image RS sym) 1)); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
214 |
by (etac (good_map_bij RS export extend_constrains) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
215 |
qed "rename_constrains"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
216 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
217 |
Goalw [stable_def] |
10834 | 218 |
"bij h ==> (rename h F : stable (h`A)) = (F : stable A)"; |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
219 |
by (asm_simp_tac (simpset() addsimps [rename_constrains]) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
220 |
qed "rename_stable"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
221 |
|
10834 | 222 |
Goal "bij h ==> (rename h F : invariant (h`A)) = (F : invariant A)"; |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
223 |
by (asm_simp_tac (simpset() addsimps [invariant_def, rename_stable, |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
224 |
bij_is_inj RS inj_image_subset_iff]) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
225 |
qed "rename_invariant"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
226 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
227 |
Goal "bij h ==> (rename h F : increasing func) = (F : increasing (func o h))"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
228 |
by (asm_simp_tac |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
229 |
(simpset() addsimps [increasing_def, rename_stable RS sym, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
230 |
bij_image_Collect_eq, bij_is_surj RS surj_f_inv_f]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
231 |
qed "rename_increasing"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
232 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
233 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
234 |
(*** Weak Safety: Co, Stable ***) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
235 |
|
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
236 |
Goalw [rename_def] |
10834 | 237 |
"bij h ==> reachable (rename h F) = h ` (reachable F)"; |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
238 |
by (asm_simp_tac (simpset() addsimps [export reachable_extend_eq]) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
239 |
qed "reachable_rename_eq"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
240 |
|
10834 | 241 |
Goal "bij h ==> (rename h F : (h`A) Co (h`B)) = (F : A Co B)"; |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
242 |
by (asm_simp_tac |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
243 |
(simpset() addsimps [Constrains_def, reachable_rename_eq, |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
244 |
rename_constrains, bij_is_inj, image_Int RS sym]) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
245 |
qed "rename_Constrains"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
246 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
247 |
Goalw [Stable_def] |
10834 | 248 |
"bij h ==> (rename h F : Stable (h`A)) = (F : Stable A)"; |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
249 |
by (asm_simp_tac (simpset() addsimps [rename_Constrains]) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
250 |
qed "rename_Stable"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
251 |
|
10834 | 252 |
Goal "bij h ==> (rename h F : Always (h`A)) = (F : Always A)"; |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
253 |
by (asm_simp_tac (simpset() addsimps [Always_def, rename_Stable, |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
254 |
bij_is_inj RS inj_image_subset_iff]) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
255 |
qed "rename_Always"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
256 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
257 |
Goal "bij h ==> (rename h F : Increasing func) = (F : Increasing (func o h))"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
258 |
by (asm_simp_tac |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
259 |
(simpset() addsimps [Increasing_def, rename_Stable RS sym, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
260 |
bij_image_Collect_eq, bij_is_surj RS surj_f_inv_f]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
261 |
qed "rename_Increasing"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8256
diff
changeset
|
262 |
|
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
263 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
264 |
(*** Progress: transient, ensures ***) |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
265 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
266 |
Goalw [rename_def] |
10834 | 267 |
"bij h ==> (rename h F : transient (h`A)) = (F : transient A)"; |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
268 |
by (stac (extend_set_eq_image RS sym) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
269 |
by (etac (good_map_bij RS export extend_transient) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
270 |
qed "rename_transient"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
271 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
272 |
Goalw [rename_def] |
10834 | 273 |
"bij h ==> (rename h F : (h`A) ensures (h`B)) = (F : A ensures B)"; |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
274 |
by (REPEAT (stac (extend_set_eq_image RS sym) 1)); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
275 |
by (etac (good_map_bij RS export extend_ensures) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
276 |
qed "rename_ensures"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
277 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
278 |
Goalw [rename_def] |
10834 | 279 |
"bij h ==> (rename h F : (h`A) leadsTo (h`B)) = (F : A leadsTo B)"; |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
280 |
by (REPEAT (stac (extend_set_eq_image RS sym) 1)); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
281 |
by (etac (good_map_bij RS export extend_leadsTo) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
282 |
qed "rename_leadsTo"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
283 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
284 |
Goalw [rename_def] |
10834 | 285 |
"bij h ==> (rename h F : (h`A) LeadsTo (h`B)) = (F : A LeadsTo B)"; |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
286 |
by (REPEAT (stac (extend_set_eq_image RS sym) 1)); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
287 |
by (etac (good_map_bij RS export extend_LeadsTo) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
288 |
qed "rename_LeadsTo"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
289 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
290 |
Goalw [rename_def] |
10834 | 291 |
"bij h ==> (rename h F : (rename h ` X) guarantees \ |
292 |
\ (rename h ` Y)) = \ |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
293 |
\ (F : X guarantees Y)"; |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
294 |
by (stac (good_map_bij RS export extend_guarantees_eq RS sym) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
295 |
by (assume_tac 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
296 |
by (asm_simp_tac (simpset() addsimps [fst_o_inv_eq_inv, o_def]) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
297 |
qed "rename_rename_guarantees_eq"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
298 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
299 |
Goal "bij h ==> (rename h F : X guarantees Y) = \ |
10834 | 300 |
\ (F : (rename (inv h) ` X) guarantees \ |
301 |
\ (rename (inv h) ` Y))"; |
|
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
302 |
by (stac (rename_rename_guarantees_eq RS sym) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
303 |
by (assume_tac 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
304 |
by (asm_simp_tac |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
305 |
(simpset() addsimps [image_eq_UN, o_def, bij_is_surj RS surj_f_inv_f]) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
306 |
qed "rename_guarantees_eq_rename_inv"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
307 |
|
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
308 |
Goal "bij h ==> (rename h G : preserves v) = (G : preserves (v o h))"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
309 |
by (stac (good_map_bij RS export extend_preserves RS sym) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
310 |
by (assume_tac 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
311 |
by (asm_simp_tac (simpset() addsimps [o_def, fst_o_inv_eq_inv, rename_def, |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
312 |
bij_is_surj RS surj_f_inv_f]) 1); |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
313 |
qed "rename_preserves"; |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
314 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
315 |
Goal "bij h ==> (rename h F ok rename h G) = (F ok G)"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
316 |
by (asm_simp_tac (simpset() addsimps [export ok_extend_iff, rename_def]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
317 |
qed "ok_rename_iff"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
318 |
Addsimps [ok_rename_iff]; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
319 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
320 |
Goal "bij h ==> OK I (%i. rename h (F i)) = (OK I F)"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
321 |
by (asm_simp_tac (simpset() addsimps [export OK_extend_iff, rename_def]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
322 |
qed "OK_rename_iff"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
323 |
Addsimps [OK_rename_iff]; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
324 |
|
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
325 |
|
8314 | 326 |
(*** "image" versions of the rules, for lifting "guarantees" properties ***) |
327 |
||
328 |
||
329 |
(*Tactic used in all the proofs. Better would have been to prove one |
|
330 |
meta-theorem, but how can we handle the polymorphism? E.g. in |
|
331 |
rename_constrains the two appearances of "co" have different types!*) |
|
332 |
fun rename_image_tac ths = |
|
333 |
EVERY [Auto_tac, |
|
334 |
(rename_tac "F" 2), |
|
335 |
(subgoal_tac "EX G. F = rename h G" 2), |
|
336 |
(auto_tac (claset() addSIs [surj_rename RS surj_f_inv_f RS sym], |
|
337 |
simpset() addsimps ths))]; |
|
338 |
||
10834 | 339 |
Goal "bij h ==> rename h ` (A co B) = (h ` A) co (h`B)"; |
8314 | 340 |
by (rename_image_tac [rename_constrains]); |
341 |
qed "rename_image_constrains"; |
|
342 |
||
10834 | 343 |
Goal "bij h ==> rename h ` stable A = stable (h ` A)"; |
8314 | 344 |
by (rename_image_tac [rename_stable]); |
345 |
qed "rename_image_stable"; |
|
346 |
||
10834 | 347 |
Goal "bij h ==> rename h ` increasing func = increasing (func o inv h)"; |
8314 | 348 |
by (rename_image_tac [rename_increasing, o_def, bij_is_inj]); |
349 |
qed "rename_image_increasing"; |
|
350 |
||
10834 | 351 |
Goal "bij h ==> rename h ` invariant A = invariant (h ` A)"; |
8314 | 352 |
by (rename_image_tac [rename_invariant]); |
353 |
qed "rename_image_invariant"; |
|
354 |
||
10834 | 355 |
Goal "bij h ==> rename h ` (A Co B) = (h ` A) Co (h`B)"; |
8314 | 356 |
by (rename_image_tac [rename_Constrains]); |
357 |
qed "rename_image_Constrains"; |
|
358 |
||
10834 | 359 |
Goal "bij h ==> rename h ` preserves v = preserves (v o inv h)"; |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
360 |
by (asm_simp_tac (simpset() addsimps [o_def, rename_image_stable, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
361 |
preserves_def, bij_image_INT, bij_image_Collect_eq]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
362 |
qed "rename_image_preserves"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
363 |
|
10834 | 364 |
Goal "bij h ==> rename h ` Stable A = Stable (h ` A)"; |
8314 | 365 |
by (rename_image_tac [rename_Stable]); |
366 |
qed "rename_image_Stable"; |
|
367 |
||
10834 | 368 |
Goal "bij h ==> rename h ` Increasing func = Increasing (func o inv h)"; |
8314 | 369 |
by (rename_image_tac [rename_Increasing, o_def, bij_is_inj]); |
370 |
qed "rename_image_Increasing"; |
|
371 |
||
10834 | 372 |
Goal "bij h ==> rename h ` Always A = Always (h ` A)"; |
8314 | 373 |
by (rename_image_tac [rename_Always]); |
374 |
qed "rename_image_Always"; |
|
375 |
||
10834 | 376 |
Goal "bij h ==> rename h ` (A leadsTo B) = (h ` A) leadsTo (h`B)"; |
8314 | 377 |
by (rename_image_tac [rename_leadsTo]); |
378 |
qed "rename_image_leadsTo"; |
|
379 |
||
10834 | 380 |
Goal "bij h ==> rename h ` (A LeadsTo B) = (h ` A) LeadsTo (h`B)"; |
8314 | 381 |
by (rename_image_tac [rename_LeadsTo]); |
382 |
qed "rename_image_LeadsTo"; |