# HG changeset patch
# User paulson
# Date 950884628 -3600
# Node ID 6ba8fa2b063893c1e4b7931d8a0c8c752722feae
# Parent  38f96394c099af1226208077419a4e0e00008c80
Rename: theory for applying a bijection over states to a UNITY program

diff -r 38f96394c099 -r 6ba8fa2b0638 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Feb 18 15:35:29 2000 +0100
+++ b/src/HOL/IsaMakefile	Fri Feb 18 15:37:08 2000 +0100
@@ -249,6 +249,7 @@
   UNITY/Lift_prog.ML UNITY/Lift_prog.thy UNITY/ListOrder.thy\
   UNITY/Mutex.ML UNITY/Mutex.thy\
   UNITY/Network.ML UNITY/Network.thy UNITY/Reach.ML UNITY/Reach.thy\
+  UNITY/Rename.ML UNITY/Rename.thy\
   UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/Token.ML UNITY/Token.thy\
   UNITY/UNITY.ML UNITY/UNITY.thy\
   UNITY/WFair.ML UNITY/WFair.thy UNITY/Lift.ML UNITY/Lift.thy\
diff -r 38f96394c099 -r 6ba8fa2b0638 src/HOL/UNITY/Rename.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Rename.ML	Fri Feb 18 15:37:08 2000 +0100
@@ -0,0 +1,268 @@
+(*  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];
+
+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 "bij h ==> h``{s. P s} = {s. P (inv h s)}";
+by (auto_tac (claset() addSIs [exI],
+	      simpset() addsimps [bij_is_inj, bij_is_surj RS surj_f_inv_f]));
+qed "rename_set_eq_Collect";
+
+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";
+
+Goalw [rename_def, rename_act_def]
+     "bij h ==> Acts (rename h F) = (rename_act h `` Acts F)";
+by (asm_simp_tac (simpset() addsimps [export Acts_extend]) 1);
+qed "Acts_rename";
+
+Addsimps [Init_rename, Acts_rename];
+
+Goalw [rename_act_def, extend_act_def]
+     "(s,s') : act ==> (h s, h s') : rename_act h act";
+by Auto_tac;
+qed "rename_actI";
+
+Goalw [rename_act_def]
+     "bij h ==> ((s,s') : rename_act h act) = ((inv h s, inv h s') : act)";
+by (rtac trans 1);
+by (etac (bij_export mem_extend_act_iff) 2);
+by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 1);
+qed "mem_rename_act_iff";
+
+Goalw [rename_act_def] "Domain (rename_act h act) = h``(Domain act)";
+by (asm_simp_tac (simpset() addsimps [export Domain_extend_act]) 1);
+qed "Domain_rename_act"; 
+
+(*** 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). inv h x) = project_act (%(x,u::'c). 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 "extend_act_inv";
+
+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, extend_act_inv]) 2);
+by (asm_simp_tac (simpset() addsimps [extend_set_inv]) 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";
+
+
+(*** 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 ==> inj (rename h)";
+by (asm_simp_tac (simpset() addsimps [export inj_extend]) 1);
+qed "inj_rename";
+
+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];
+
+(*** 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";
+
+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";
+
+
+(*** 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[v o inv h] \
+\                             (rename h `` Y)) = \
+\               (F : X guarantees[v] 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[v] Y) = \
+\               (F : (rename (inv h) `` X) guarantees[v o h] \
+\                    (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";
+
+
+(** junk
+
+
+Goalw [extend_act_def, project_act_def, surj_def]
+ "surj h ==> extend_act (%(x,u). h x) (project_act (%(x,u). h x) act) = act";
+by Auto_tac;
+by (forw_inst_tac [("x", "a")] spec 1);
+by (dres_inst_tac [("x", "b")] spec 1);
+by Auto_tac;
+qed "project_act_inverse";
+
+Goal "bij h ==> rename h (rename (inv h) F) = F";
+by (rtac program_equalityI 1);
+by (Asm_simp_tac 1);
+by (asm_simp_tac
+    (simpset() addsimps [rename_def, inverse_def, export Acts_extend,
+			 image_eq_UN, export extend_act_Id,
+			 bij_is_surj RS project_act_inverse]) 1);
+qed "rename_rename_inv";
+Addsimps [rename_rename_inv];
+
+
+
+Goalw [bij_def]
+     "bij h \
+\     ==> extend_set (%(x,u::'c). inv h x) = inv (extend_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";
+
+
+***)
diff -r 38f96394c099 -r 6ba8fa2b0638 src/HOL/UNITY/Rename.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Rename.thy	Fri Feb 18 15:37:08 2000 +0100
@@ -0,0 +1,23 @@
+(*  Title:      HOL/UNITY/Rename.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2000  University of Cambridge
+
+Renaming of state sets
+*)
+
+Rename = Extend +
+
+constdefs
+  rename_act :: "['a => 'b, ('a*'a) set] => ('b*'b) set"
+    "rename_act h == extend_act (%(x,u::unit). h x)"
+
+(**OR
+      "rename_act h == %act. UN (s,s'): act.  {(h s, h s')}"
+      "rename_act h == %act. (prod_fun h h) `` act"
+**)
+  
+  rename :: "['a => 'b, 'a program] => 'b program"
+    "rename h == extend (%(x,u::unit). h x)"
+
+end