added compatibility relation: AllowedActs, Allowed, ok,
OK and changes to "guarantees", etc.
(* Title: HOL/UNITY/Rename.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2000 University of Cambridge
*)
Addsimps [image_inv_f_f, image_surj_f_inv_f];
Goal "bij h ==> good_map (%(x,u). h x)";
by (rtac good_mapI 1);
by (rewrite_goals_tac [bij_def, inj_on_def, surj_def]);
by Auto_tac;
qed "good_map_bij";
Addsimps [good_map_bij];
AddIs [good_map_bij];
fun bij_export th = good_map_bij RS export th |> simplify (simpset());
Goalw [bij_def, split_def] "bij h ==> fst (inv (%(x,u). h x) s) = inv h s";
by (Clarify_tac 1);
by (subgoal_tac "surj (%p. h (fst p))" 1);
by (asm_full_simp_tac (simpset() addsimps [surj_def]) 2);
by (etac injD 1);
by (asm_simp_tac (simpset() addsimps [surj_f_inv_f]) 1);
by (etac surj_f_inv_f 1);
qed "fst_o_inv_eq_inv";
Goal "bij h ==> z : h``A = (inv h z : A)";
by (auto_tac (claset() addSIs [image_eqI],
simpset() addsimps [bij_is_inj, bij_is_surj RS surj_f_inv_f]));
qed "mem_rename_set_iff";
Goal "extend_set (%(x,u). h x) A = h``A";
by (auto_tac (claset() addSIs [image_eqI],
simpset() addsimps [extend_set_def]));
qed "extend_set_eq_image";
Addsimps [extend_set_eq_image];
Goalw [rename_def] "Init (rename h F) = h``(Init F)";
by (Simp_tac 1);
qed "Init_rename";
Addsimps [Init_rename];
(*** inverse properties ***)
Goalw [bij_def]
"bij h \
\ ==> extend_set (%(x,u::'c). inv h x) = project_set (%(x,u::'c). h x)";
by (rtac ext 1);
by (auto_tac (claset() addSIs [image_eqI],
simpset() addsimps [extend_set_def, project_set_def,
surj_f_inv_f]));
qed "extend_set_inv";
(** for "rename" (programs) **)
Goal "bij h \
\ ==> extend_act (%(x,u::'c). h x) = project_act (%(x,u::'c). inv h x)";
by (rtac ext 1);
by (auto_tac (claset() addSIs [image_eqI],
simpset() addsimps [extend_act_def, project_act_def, bij_def,
surj_f_inv_f]));
qed "bij_extend_act_eq_project_act";
Goal "bij h ==> bij (extend_act (%(x,u::'c). h x))";
by (rtac bijI 1);
by (rtac (export inj_extend_act) 1);
by (auto_tac (claset(), simpset() addsimps [bij_extend_act_eq_project_act]));
by (blast_tac (claset() addIs [bij_imp_bij_inv, surjI,
export extend_act_inverse]) 1);
qed "bij_extend_act";
Goal "bij h ==> bij (project_act (%(x,u::'c). h x))";
by (ftac (bij_imp_bij_inv RS bij_extend_act) 1);
by (asm_full_simp_tac (simpset() addsimps [bij_extend_act_eq_project_act,
bij_imp_bij_inv, inv_inv_eq]) 1);
qed "bij_project_act";
Goal "bij h ==> inv (project_act (%(x,u::'c). inv h x)) = \
\ project_act (%(x,u::'c). h x)";
by (asm_simp_tac
(simpset() addsimps [bij_extend_act_eq_project_act RS sym]) 1);
by (rtac surj_imp_inv_eq 1);
by (blast_tac (claset() addIs [bij_extend_act, bij_is_surj]) 1);
by (asm_simp_tac (simpset() addsimps [export extend_act_inverse]) 1);
qed "bij_inv_project_act_eq";
Goal "bij h \
\ ==> extend (%(x,u::'c). inv h x) = project (%(x,u::'c). h x) UNIV";
by (ftac bij_imp_bij_inv 1);
by (rtac ext 1);
by (rtac program_equalityI 1);
by (asm_simp_tac
(simpset() addsimps [export project_act_Id, export Acts_extend,
insert_Id_image_Acts, bij_extend_act_eq_project_act,
inv_inv_eq]) 2);
by (asm_simp_tac (simpset() addsimps [extend_set_inv]) 1);
by (asm_simp_tac
(simpset() addsimps [export AllowedActs_extend,
export AllowedActs_project,
bij_project_act, bij_vimage_eq_inv_image,
bij_inv_project_act_eq]) 1);
qed "extend_inv";
Goal "bij h ==> rename (inv h) (rename h F) = F";
by (asm_simp_tac (simpset() addsimps [rename_def, extend_inv,
export extend_inverse]) 1);
qed "rename_inv_rename";
Addsimps [rename_inv_rename];
Goal "bij h ==> rename h (rename (inv h) F) = F";
by (ftac bij_imp_bij_inv 1);
by (etac (inv_inv_eq RS subst) 1 THEN etac rename_inv_rename 1);
qed "rename_rename_inv";
Addsimps [rename_rename_inv];
Goal "bij h ==> rename (inv h) = inv (rename h)";
by (rtac (inv_equality RS sym) 1);
by Auto_tac;
qed "rename_inv_eq";
(** (rename h) is bijective <=> h is bijective **)
Goal "bij h ==> bij (extend (%(x,u::'c). h x))";
by (rtac bijI 1);
by (blast_tac (claset() addIs [export inj_extend]) 1);
by (res_inst_tac [("f","extend (%(x,u). inv h x)")] surjI 1);
by (stac ((inst "f" "h" inv_inv_eq) RS sym) 1
THEN stac extend_inv 2 THEN stac (export extend_inverse) 3);
by (auto_tac (claset(), simpset() addsimps [bij_imp_bij_inv, inv_inv_eq]));
qed "bij_extend";
Goal "bij h ==> bij (project (%(x,u::'c). h x) UNIV)";
by (stac (extend_inv RS sym) 1);
by (auto_tac (claset(), simpset() addsimps [bij_imp_bij_inv, bij_extend]));
qed "bij_project";
Goal "bij h \
\ ==> inv (project (%(x,u::'c). h x) UNIV) = extend (%(x,u::'c). h x)";
by (rtac inj_imp_inv_eq 1);
by (etac (bij_project RS bij_is_inj) 1);
by (asm_simp_tac (simpset() addsimps [export extend_inverse]) 1);
qed "inv_project_eq";
Goal "bij h ==> Allowed (rename h F) = rename h `` Allowed F";
by (asm_simp_tac (simpset() addsimps [rename_def, export Allowed_extend]) 1);
by (stac bij_vimage_eq_inv_image 1);
by (rtac bij_project 1);
by (Blast_tac 1);
by (asm_simp_tac (simpset() addsimps [inv_project_eq]) 1);
qed "Allowed_rename";
Addsimps [Allowed_rename];
Goal "bij h ==> bij (rename h)";
by (asm_simp_tac (simpset() addsimps [rename_def, bij_extend]) 1);
qed "bij_rename";
bind_thm ("surj_rename", bij_rename RS bij_is_surj);
Goalw [inj_on_def] "inj (rename h) ==> inj h";
by Auto_tac;
by (dres_inst_tac [("x", "mk_program ({x}, {}, {})")] spec 1);
by (dres_inst_tac [("x", "mk_program ({y}, {}, {})")] spec 1);
by (auto_tac (claset(),
simpset() addsimps [program_equality_iff,
rename_def, extend_def]));
qed "inj_rename_imp_inj";
Goalw [surj_def] "surj (rename h) ==> surj h";
by Auto_tac;
by (dres_inst_tac [("x", "mk_program ({y}, {}, {})")] spec 1);
by (auto_tac (claset(),
simpset() addsimps [program_equality_iff,
rename_def, extend_def]));
qed "surj_rename_imp_surj";
Goalw [bij_def] "bij (rename h) ==> bij h";
by (asm_simp_tac
(simpset() addsimps [inj_rename_imp_inj, surj_rename_imp_surj]) 1);
qed "bij_rename_imp_bij";
Goal "bij (rename h) = bij h";
by (blast_tac (claset() addIs [bij_rename, bij_rename_imp_bij]) 1);
qed "bij_rename_iff";
AddIffs [bij_rename_iff];
(*** the lattice operations ***)
Goalw [rename_def] "bij h ==> rename h SKIP = SKIP";
by (Asm_simp_tac 1);
qed "rename_SKIP";
Addsimps [rename_SKIP];
Goalw [rename_def]
"bij h ==> rename h (F Join G) = rename h F Join rename h G";
by (asm_simp_tac (simpset() addsimps [export extend_Join]) 1);
qed "rename_Join";
Addsimps [rename_Join];
Goalw [rename_def] "bij h ==> rename h (JOIN I F) = (JN i:I. rename h (F i))";
by (asm_simp_tac (simpset() addsimps [export extend_JN]) 1);
qed "rename_JN";
Addsimps [rename_JN];
(*** Strong Safety: co, stable ***)
Goalw [rename_def]
"bij h ==> (rename h F : (h``A) co (h``B)) = (F : A co B)";
by (REPEAT (stac (extend_set_eq_image RS sym) 1));
by (etac (good_map_bij RS export extend_constrains) 1);
qed "rename_constrains";
Goalw [stable_def]
"bij h ==> (rename h F : stable (h``A)) = (F : stable A)";
by (asm_simp_tac (simpset() addsimps [rename_constrains]) 1);
qed "rename_stable";
Goal "bij h ==> (rename h F : invariant (h``A)) = (F : invariant A)";
by (asm_simp_tac (simpset() addsimps [invariant_def, rename_stable,
bij_is_inj RS inj_image_subset_iff]) 1);
qed "rename_invariant";
Goal "bij h ==> (rename h F : increasing func) = (F : increasing (func o h))";
by (asm_simp_tac
(simpset() addsimps [increasing_def, rename_stable RS sym,
bij_image_Collect_eq, bij_is_surj RS surj_f_inv_f]) 1);
qed "rename_increasing";
(*** Weak Safety: Co, Stable ***)
Goalw [rename_def]
"bij h ==> reachable (rename h F) = h `` (reachable F)";
by (asm_simp_tac (simpset() addsimps [export reachable_extend_eq]) 1);
qed "reachable_rename_eq";
Goal "bij h ==> (rename h F : (h``A) Co (h``B)) = (F : A Co B)";
by (asm_simp_tac
(simpset() addsimps [Constrains_def, reachable_rename_eq,
rename_constrains, bij_is_inj, image_Int RS sym]) 1);
qed "rename_Constrains";
Goalw [Stable_def]
"bij h ==> (rename h F : Stable (h``A)) = (F : Stable A)";
by (asm_simp_tac (simpset() addsimps [rename_Constrains]) 1);
qed "rename_Stable";
Goal "bij h ==> (rename h F : Always (h``A)) = (F : Always A)";
by (asm_simp_tac (simpset() addsimps [Always_def, rename_Stable,
bij_is_inj RS inj_image_subset_iff]) 1);
qed "rename_Always";
Goal "bij h ==> (rename h F : Increasing func) = (F : Increasing (func o h))";
by (asm_simp_tac
(simpset() addsimps [Increasing_def, rename_Stable RS sym,
bij_image_Collect_eq, bij_is_surj RS surj_f_inv_f]) 1);
qed "rename_Increasing";
(*** Progress: transient, ensures ***)
Goalw [rename_def]
"bij h ==> (rename h F : transient (h``A)) = (F : transient A)";
by (stac (extend_set_eq_image RS sym) 1);
by (etac (good_map_bij RS export extend_transient) 1);
qed "rename_transient";
Goalw [rename_def]
"bij h ==> (rename h F : (h``A) ensures (h``B)) = (F : A ensures B)";
by (REPEAT (stac (extend_set_eq_image RS sym) 1));
by (etac (good_map_bij RS export extend_ensures) 1);
qed "rename_ensures";
Goalw [rename_def]
"bij h ==> (rename h F : (h``A) leadsTo (h``B)) = (F : A leadsTo B)";
by (REPEAT (stac (extend_set_eq_image RS sym) 1));
by (etac (good_map_bij RS export extend_leadsTo) 1);
qed "rename_leadsTo";
Goalw [rename_def]
"bij h ==> (rename h F : (h``A) LeadsTo (h``B)) = (F : A LeadsTo B)";
by (REPEAT (stac (extend_set_eq_image RS sym) 1));
by (etac (good_map_bij RS export extend_LeadsTo) 1);
qed "rename_LeadsTo";
Goalw [rename_def]
"bij h ==> (rename h F : (rename h `` X) guarantees \
\ (rename h `` Y)) = \
\ (F : X guarantees Y)";
by (stac (good_map_bij RS export extend_guarantees_eq RS sym) 1);
by (assume_tac 1);
by (asm_simp_tac (simpset() addsimps [fst_o_inv_eq_inv, o_def]) 1);
qed "rename_rename_guarantees_eq";
Goal "bij h ==> (rename h F : X guarantees Y) = \
\ (F : (rename (inv h) `` X) guarantees \
\ (rename (inv h) `` Y))";
by (stac (rename_rename_guarantees_eq RS sym) 1);
by (assume_tac 1);
by (asm_simp_tac
(simpset() addsimps [image_eq_UN, o_def, bij_is_surj RS surj_f_inv_f]) 1);
qed "rename_guarantees_eq_rename_inv";
Goal "bij h ==> (rename h G : preserves v) = (G : preserves (v o h))";
by (stac (good_map_bij RS export extend_preserves RS sym) 1);
by (assume_tac 1);
by (asm_simp_tac (simpset() addsimps [o_def, fst_o_inv_eq_inv, rename_def,
bij_is_surj RS surj_f_inv_f]) 1);
qed "rename_preserves";
Goal "bij h ==> (rename h F ok rename h G) = (F ok G)";
by (asm_simp_tac (simpset() addsimps [export ok_extend_iff, rename_def]) 1);
qed "ok_rename_iff";
Addsimps [ok_rename_iff];
Goal "bij h ==> OK I (%i. rename h (F i)) = (OK I F)";
by (asm_simp_tac (simpset() addsimps [export OK_extend_iff, rename_def]) 1);
qed "OK_rename_iff";
Addsimps [OK_rename_iff];
(*** "image" versions of the rules, for lifting "guarantees" properties ***)
(*Tactic used in all the proofs. Better would have been to prove one
meta-theorem, but how can we handle the polymorphism? E.g. in
rename_constrains the two appearances of "co" have different types!*)
fun rename_image_tac ths =
EVERY [Auto_tac,
(rename_tac "F" 2),
(subgoal_tac "EX G. F = rename h G" 2),
(auto_tac (claset() addSIs [surj_rename RS surj_f_inv_f RS sym],
simpset() addsimps ths))];
Goal "bij h ==> rename h `` (A co B) = (h `` A) co (h``B)";
by (rename_image_tac [rename_constrains]);
qed "rename_image_constrains";
Goal "bij h ==> rename h `` stable A = stable (h `` A)";
by (rename_image_tac [rename_stable]);
qed "rename_image_stable";
Goal "bij h ==> rename h `` increasing func = increasing (func o inv h)";
by (rename_image_tac [rename_increasing, o_def, bij_is_inj]);
qed "rename_image_increasing";
Goal "bij h ==> rename h `` invariant A = invariant (h `` A)";
by (rename_image_tac [rename_invariant]);
qed "rename_image_invariant";
Goal "bij h ==> rename h `` (A Co B) = (h `` A) Co (h``B)";
by (rename_image_tac [rename_Constrains]);
qed "rename_image_Constrains";
Goal "bij h ==> rename h `` preserves v = preserves (v o inv h)";
by (asm_simp_tac (simpset() addsimps [o_def, rename_image_stable,
preserves_def, bij_image_INT, bij_image_Collect_eq]) 1);
qed "rename_image_preserves";
Goal "bij h ==> rename h `` Stable A = Stable (h `` A)";
by (rename_image_tac [rename_Stable]);
qed "rename_image_Stable";
Goal "bij h ==> rename h `` Increasing func = Increasing (func o inv h)";
by (rename_image_tac [rename_Increasing, o_def, bij_is_inj]);
qed "rename_image_Increasing";
Goal "bij h ==> rename h `` Always A = Always (h `` A)";
by (rename_image_tac [rename_Always]);
qed "rename_image_Always";
Goal "bij h ==> rename h `` (A leadsTo B) = (h `` A) leadsTo (h``B)";
by (rename_image_tac [rename_leadsTo]);
qed "rename_image_leadsTo";
Goal "bij h ==> rename h `` (A LeadsTo B) = (h `` A) LeadsTo (h``B)";
by (rename_image_tac [rename_LeadsTo]);
qed "rename_image_LeadsTo";