Rename: theory for applying a bijection over states to a UNITY program
authorpaulson
Fri Feb 18 15:37:08 2000 +0100 (2000-02-18)
changeset 82566ba8fa2b0638
parent 8255 38f96394c099
child 8257 fe9bf28e8a58
Rename: theory for applying a bijection over states to a UNITY program
src/HOL/IsaMakefile
src/HOL/UNITY/Rename.ML
src/HOL/UNITY/Rename.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Feb 18 15:35:29 2000 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Feb 18 15:37:08 2000 +0100
     1.3 @@ -249,6 +249,7 @@
     1.4    UNITY/Lift_prog.ML UNITY/Lift_prog.thy UNITY/ListOrder.thy\
     1.5    UNITY/Mutex.ML UNITY/Mutex.thy\
     1.6    UNITY/Network.ML UNITY/Network.thy UNITY/Reach.ML UNITY/Reach.thy\
     1.7 +  UNITY/Rename.ML UNITY/Rename.thy\
     1.8    UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/Token.ML UNITY/Token.thy\
     1.9    UNITY/UNITY.ML UNITY/UNITY.thy\
    1.10    UNITY/WFair.ML UNITY/WFair.thy UNITY/Lift.ML UNITY/Lift.thy\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/UNITY/Rename.ML	Fri Feb 18 15:37:08 2000 +0100
     2.3 @@ -0,0 +1,268 @@
     2.4 +(*  Title:      HOL/UNITY/Rename.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   2000  University of Cambridge
     2.8 +
     2.9 +*)
    2.10 +
    2.11 +Addsimps [image_inv_f_f, image_surj_f_inv_f];
    2.12 +
    2.13 +Goal "bij h ==> good_map (%(x,u). h x)";
    2.14 +by (rtac good_mapI 1);
    2.15 +by (rewrite_goals_tac [bij_def, inj_on_def, surj_def]);
    2.16 +by Auto_tac;
    2.17 +qed "good_map_bij";
    2.18 +Addsimps [good_map_bij];
    2.19 +
    2.20 +fun bij_export th = good_map_bij RS export th |> simplify (simpset());
    2.21 +
    2.22 +Goalw [bij_def, split_def] "bij h ==> fst (inv (%(x,u). h x) s) = inv h s";
    2.23 +by (Clarify_tac 1);
    2.24 +by (subgoal_tac "surj (%p. h (fst p))" 1);
    2.25 +by (asm_full_simp_tac (simpset() addsimps [surj_def]) 2);
    2.26 +by (etac injD 1);
    2.27 +by (asm_simp_tac (simpset() addsimps [surj_f_inv_f]) 1);
    2.28 +by (etac surj_f_inv_f 1);
    2.29 +qed "fst_o_inv_eq_inv";
    2.30 +
    2.31 +Goal "bij h ==> z : h``A = (inv h z : A)";
    2.32 +by (auto_tac (claset() addSIs [image_eqI],
    2.33 +	      simpset() addsimps [bij_is_inj, bij_is_surj RS surj_f_inv_f]));
    2.34 +qed "mem_rename_set_iff";
    2.35 +
    2.36 +Goal "bij h ==> h``{s. P s} = {s. P (inv h s)}";
    2.37 +by (auto_tac (claset() addSIs [exI],
    2.38 +	      simpset() addsimps [bij_is_inj, bij_is_surj RS surj_f_inv_f]));
    2.39 +qed "rename_set_eq_Collect";
    2.40 +
    2.41 +Goal "extend_set (%(x,u). h x) A = h``A";
    2.42 +by (auto_tac (claset() addSIs [image_eqI],
    2.43 +	      simpset() addsimps [extend_set_def]));
    2.44 +qed "extend_set_eq_image";
    2.45 +Addsimps [extend_set_eq_image];
    2.46 +
    2.47 +Goalw [rename_def] "Init (rename h F) = h``(Init F)";
    2.48 +by (Simp_tac 1);
    2.49 +qed "Init_rename";
    2.50 +
    2.51 +Goalw [rename_def, rename_act_def]
    2.52 +     "bij h ==> Acts (rename h F) = (rename_act h `` Acts F)";
    2.53 +by (asm_simp_tac (simpset() addsimps [export Acts_extend]) 1);
    2.54 +qed "Acts_rename";
    2.55 +
    2.56 +Addsimps [Init_rename, Acts_rename];
    2.57 +
    2.58 +Goalw [rename_act_def, extend_act_def]
    2.59 +     "(s,s') : act ==> (h s, h s') : rename_act h act";
    2.60 +by Auto_tac;
    2.61 +qed "rename_actI";
    2.62 +
    2.63 +Goalw [rename_act_def]
    2.64 +     "bij h ==> ((s,s') : rename_act h act) = ((inv h s, inv h s') : act)";
    2.65 +by (rtac trans 1);
    2.66 +by (etac (bij_export mem_extend_act_iff) 2);
    2.67 +by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 1);
    2.68 +qed "mem_rename_act_iff";
    2.69 +
    2.70 +Goalw [rename_act_def] "Domain (rename_act h act) = h``(Domain act)";
    2.71 +by (asm_simp_tac (simpset() addsimps [export Domain_extend_act]) 1);
    2.72 +qed "Domain_rename_act"; 
    2.73 +
    2.74 +(*** inverse properties ***)
    2.75 +
    2.76 +Goalw [bij_def]
    2.77 +     "bij h \
    2.78 +\     ==> extend_set (%(x,u::'c). inv h x) = project_set (%(x,u::'c). h x)";
    2.79 +by (rtac ext 1);
    2.80 +by (auto_tac (claset() addSIs [image_eqI], 
    2.81 +	      simpset() addsimps [extend_set_def, project_set_def,
    2.82 +				  surj_f_inv_f]));
    2.83 +qed "extend_set_inv";
    2.84 +
    2.85 +(** for "rename" (programs) **)
    2.86 +
    2.87 +Goal "bij h \
    2.88 +\     ==> extend_act (%(x,u::'c). inv h x) = project_act (%(x,u::'c). h x)";
    2.89 +by (rtac ext 1);
    2.90 +by (auto_tac (claset() addSIs [image_eqI], 
    2.91 +	      simpset() addsimps [extend_act_def, project_act_def, bij_def,
    2.92 +				  surj_f_inv_f]));
    2.93 +qed "extend_act_inv";
    2.94 +
    2.95 +Goal "bij h  \
    2.96 +\     ==> extend (%(x,u::'c). inv h x) = project (%(x,u::'c). h x) UNIV";
    2.97 +by (ftac bij_imp_bij_inv 1);
    2.98 +by (rtac ext 1);
    2.99 +by (rtac program_equalityI 1);
   2.100 +by (asm_simp_tac
   2.101 +    (simpset() addsimps [export project_act_Id, export Acts_extend,
   2.102 +			 insert_Id_image_Acts, extend_act_inv]) 2);
   2.103 +by (asm_simp_tac (simpset() addsimps [extend_set_inv]) 1);
   2.104 +qed "extend_inv";
   2.105 +
   2.106 +Goal "bij h ==> rename (inv h) (rename h F) = F";
   2.107 +by (asm_simp_tac (simpset() addsimps [rename_def, extend_inv, 
   2.108 +				      export extend_inverse]) 1);
   2.109 +qed "rename_inv_rename";
   2.110 +Addsimps [rename_inv_rename];
   2.111 +
   2.112 +Goal "bij h ==> rename h (rename (inv h) F) = F";
   2.113 +by (ftac bij_imp_bij_inv 1);
   2.114 +by (etac (inv_inv_eq RS subst) 1 THEN etac rename_inv_rename 1);
   2.115 +qed "rename_rename_inv";
   2.116 +Addsimps [rename_rename_inv];
   2.117 +
   2.118 +Goal "bij h ==> rename (inv h) = inv (rename h)";
   2.119 +by (rtac (inv_equality RS sym) 1);
   2.120 +by Auto_tac;
   2.121 +qed "rename_inv_eq";
   2.122 +
   2.123 +
   2.124 +(*** the lattice operations ***)
   2.125 +
   2.126 +Goalw [rename_def] "bij h ==> rename h SKIP = SKIP";
   2.127 +by (Asm_simp_tac 1);
   2.128 +qed "rename_SKIP";
   2.129 +Addsimps [rename_SKIP];
   2.130 +
   2.131 +Goalw [rename_def] "bij h ==> inj (rename h)";
   2.132 +by (asm_simp_tac (simpset() addsimps [export inj_extend]) 1);
   2.133 +qed "inj_rename";
   2.134 +
   2.135 +Goalw [rename_def]
   2.136 +     "bij h ==> rename h (F Join G) = rename h F Join rename h G";
   2.137 +by (asm_simp_tac (simpset() addsimps [export extend_Join]) 1);
   2.138 +qed "rename_Join";
   2.139 +Addsimps [rename_Join];
   2.140 +
   2.141 +Goalw [rename_def] "bij h ==> rename h (JOIN I F) = (JN i:I. rename h (F i))";
   2.142 +by (asm_simp_tac (simpset() addsimps [export extend_JN]) 1);
   2.143 +qed "rename_JN";
   2.144 +Addsimps [rename_JN];
   2.145 +
   2.146 +(*** Safety: co, stable ***)
   2.147 +
   2.148 +Goalw [rename_def]
   2.149 +     "bij h ==> (rename h F : (h``A) co (h``B)) = (F : A co B)";
   2.150 +by (REPEAT (stac (extend_set_eq_image RS sym) 1));
   2.151 +by (etac (good_map_bij RS export extend_constrains) 1);
   2.152 +qed "rename_constrains";
   2.153 +
   2.154 +Goalw [stable_def]
   2.155 +     "bij h ==> (rename h F : stable (h``A)) = (F : stable A)";
   2.156 +by (asm_simp_tac (simpset() addsimps [rename_constrains]) 1);
   2.157 +qed "rename_stable";
   2.158 +
   2.159 +Goal "bij h ==> (rename h F : invariant (h``A)) = (F : invariant A)";
   2.160 +by (asm_simp_tac (simpset() addsimps [invariant_def, rename_stable,
   2.161 +				      bij_is_inj RS inj_image_subset_iff]) 1);
   2.162 +qed "rename_invariant";
   2.163 +
   2.164 +Goalw [rename_def]
   2.165 +     "bij h ==> reachable (rename h F) = h `` (reachable F)";
   2.166 +by (asm_simp_tac (simpset() addsimps [export reachable_extend_eq]) 1);
   2.167 +qed "reachable_rename_eq";
   2.168 +
   2.169 +Goal "bij h ==> (rename h F : (h``A) Co (h``B)) = (F : A Co B)";
   2.170 +by (asm_simp_tac
   2.171 +    (simpset() addsimps [Constrains_def, reachable_rename_eq, 
   2.172 +			 rename_constrains, bij_is_inj, image_Int RS sym]) 1);
   2.173 +qed "rename_Constrains";
   2.174 +
   2.175 +Goalw [Stable_def]
   2.176 +     "bij h ==> (rename h F : Stable (h``A)) = (F : Stable A)";
   2.177 +by (asm_simp_tac (simpset() addsimps [rename_Constrains]) 1);
   2.178 +qed "rename_Stable";
   2.179 +
   2.180 +Goal "bij h ==> (rename h F : Always (h``A)) = (F : Always A)";
   2.181 +by (asm_simp_tac (simpset() addsimps [Always_def, rename_Stable,
   2.182 +				      bij_is_inj RS inj_image_subset_iff]) 1);
   2.183 +qed "rename_Always";
   2.184 +
   2.185 +
   2.186 +(*** Progress: transient, ensures ***)
   2.187 +
   2.188 +Goalw [rename_def]
   2.189 +     "bij h ==> (rename h F : transient (h``A)) = (F : transient A)";
   2.190 +by (stac (extend_set_eq_image RS sym) 1);
   2.191 +by (etac (good_map_bij RS export extend_transient) 1);
   2.192 +qed "rename_transient";
   2.193 +
   2.194 +Goalw [rename_def]
   2.195 +     "bij h ==> (rename h F : (h``A) ensures (h``B)) = (F : A ensures B)";
   2.196 +by (REPEAT (stac (extend_set_eq_image RS sym) 1));
   2.197 +by (etac (good_map_bij RS export extend_ensures) 1);
   2.198 +qed "rename_ensures";
   2.199 +
   2.200 +Goalw [rename_def]
   2.201 +     "bij h ==> (rename h F : (h``A) leadsTo (h``B)) = (F : A leadsTo B)";
   2.202 +by (REPEAT (stac (extend_set_eq_image RS sym) 1));
   2.203 +by (etac (good_map_bij RS export extend_leadsTo) 1);
   2.204 +qed "rename_leadsTo";
   2.205 +
   2.206 +Goalw [rename_def]
   2.207 +     "bij h ==> (rename h F : (h``A) LeadsTo (h``B)) = (F : A LeadsTo B)";
   2.208 +by (REPEAT (stac (extend_set_eq_image RS sym) 1));
   2.209 +by (etac (good_map_bij RS export extend_LeadsTo) 1);
   2.210 +qed "rename_LeadsTo";
   2.211 +
   2.212 +Goalw [rename_def]
   2.213 +     "bij h ==> (rename h F : (rename h `` X) guarantees[v o inv h] \
   2.214 +\                             (rename h `` Y)) = \
   2.215 +\               (F : X guarantees[v] Y)";
   2.216 +by (stac (good_map_bij RS export extend_guarantees_eq RS sym) 1);
   2.217 +by (assume_tac 1);
   2.218 +by (asm_simp_tac (simpset() addsimps [fst_o_inv_eq_inv, o_def]) 1);
   2.219 +qed "rename_rename_guarantees_eq";
   2.220 +
   2.221 +Goal "bij h ==> (rename h F : X guarantees[v] Y) = \
   2.222 +\               (F : (rename (inv h) `` X) guarantees[v o h] \
   2.223 +\                    (rename (inv h) `` Y))";
   2.224 +by (stac (rename_rename_guarantees_eq RS sym) 1);
   2.225 +by (assume_tac 1);
   2.226 +by (asm_simp_tac
   2.227 +    (simpset() addsimps [image_eq_UN, o_def, bij_is_surj RS surj_f_inv_f]) 1);
   2.228 +qed "rename_guarantees_eq_rename_inv";
   2.229 +
   2.230 +Goal "bij h ==> (rename h G : preserves v) = (G : preserves (v o h))";
   2.231 +by (stac (good_map_bij RS export extend_preserves RS sym) 1);
   2.232 +by (assume_tac 1);
   2.233 +by (asm_simp_tac (simpset() addsimps [o_def, fst_o_inv_eq_inv, rename_def,
   2.234 +				      bij_is_surj RS surj_f_inv_f]) 1);
   2.235 +qed "rename_preserves";
   2.236 +
   2.237 +
   2.238 +(** junk
   2.239 +
   2.240 +
   2.241 +Goalw [extend_act_def, project_act_def, surj_def]
   2.242 + "surj h ==> extend_act (%(x,u). h x) (project_act (%(x,u). h x) act) = act";
   2.243 +by Auto_tac;
   2.244 +by (forw_inst_tac [("x", "a")] spec 1);
   2.245 +by (dres_inst_tac [("x", "b")] spec 1);
   2.246 +by Auto_tac;
   2.247 +qed "project_act_inverse";
   2.248 +
   2.249 +Goal "bij h ==> rename h (rename (inv h) F) = F";
   2.250 +by (rtac program_equalityI 1);
   2.251 +by (Asm_simp_tac 1);
   2.252 +by (asm_simp_tac
   2.253 +    (simpset() addsimps [rename_def, inverse_def, export Acts_extend,
   2.254 +			 image_eq_UN, export extend_act_Id,
   2.255 +			 bij_is_surj RS project_act_inverse]) 1);
   2.256 +qed "rename_rename_inv";
   2.257 +Addsimps [rename_rename_inv];
   2.258 +
   2.259 +
   2.260 +
   2.261 +Goalw [bij_def]
   2.262 +     "bij h \
   2.263 +\     ==> extend_set (%(x,u::'c). inv h x) = inv (extend_set (%(x,u::'c). h x))";
   2.264 +by (rtac ext 1);
   2.265 +by (auto_tac (claset() addSIs [image_eqI], 
   2.266 +	      simpset() addsimps [extend_set_def, project_set_def,
   2.267 +				  surj_f_inv_f]));
   2.268 +qed "extend_set_inv";
   2.269 +
   2.270 +
   2.271 +***)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/UNITY/Rename.thy	Fri Feb 18 15:37:08 2000 +0100
     3.3 @@ -0,0 +1,23 @@
     3.4 +(*  Title:      HOL/UNITY/Rename.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   2000  University of Cambridge
     3.8 +
     3.9 +Renaming of state sets
    3.10 +*)
    3.11 +
    3.12 +Rename = Extend +
    3.13 +
    3.14 +constdefs
    3.15 +  rename_act :: "['a => 'b, ('a*'a) set] => ('b*'b) set"
    3.16 +    "rename_act h == extend_act (%(x,u::unit). h x)"
    3.17 +
    3.18 +(**OR
    3.19 +      "rename_act h == %act. UN (s,s'): act.  {(h s, h s')}"
    3.20 +      "rename_act h == %act. (prod_fun h h) `` act"
    3.21 +**)
    3.22 +  
    3.23 +  rename :: "['a => 'b, 'a program] => 'b program"
    3.24 +    "rename h == extend (%(x,u::unit). h x)"
    3.25 +
    3.26 +end