# HG changeset patch
# User paulson
# Date 936004842 -7200
# Node ID 5e74c23063de58484a8e770d78fb251e3cd9a90d
# Parent  1048bc161c050f92eb561854219329ff432060a0
new results for localTo

diff -r 1048bc161c05 -r 5e74c23063de src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Mon Aug 30 11:20:23 1999 +0200
+++ b/src/HOL/UNITY/Extend.ML	Mon Aug 30 11:20:42 1999 +0200
@@ -246,6 +246,19 @@
 qed "extend_JN";
 Addsimps [extend_JN];
 
+Goal "project h ((extend h F) Join G) = F Join (project h G)";
+by (rtac program_equalityI 1);
+by (simp_tac (simpset() addsimps [Acts_Join, image_Un,
+				  image_compose RS sym, o_def]) 2);
+by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
+qed "project_extend_Join";
+
+Goal "(extend h F) Join G = extend h H ==> H = F Join (project h G)";
+by (dres_inst_tac [("f", "project h")] arg_cong 1);
+by (full_simp_tac (simpset() addsimps [project_extend_Join]) 1);
+by (etac sym 1);
+qed "extend_Join_eq_extend_D";
+
 
 (*** Safety: co, stable ***)
 
@@ -275,39 +288,65 @@
 by (simp_tac (simpset() addsimps [stable_def, project_constrains]) 1);
 qed "project_stable";
 
+Goal "(project h F : increasing func)  =  (F : increasing (func o f))";
+by (simp_tac (simpset() addsimps [increasing_def, project_stable,
+				  Collect_eq_extend_set RS sym]) 1);
+qed "project_increasing";
+
 
 (*** Diff, needed for localTo ***)
 
-Goal "Diff G (extend_act h `` Acts F) : (extend_set h A) co (extend_set h B)  \
-\     ==> Diff (project h G) (Acts F) : A co B";
-by (auto_tac (claset(), 
-	      simpset() addsimps [constrains_def, Diff_def]));
-by (dtac bspec 1);
-by (Force_tac 1);
-by (auto_tac (claset(), simpset() addsimps [project_act_def]));
-by (Force_tac 1);
+(** project versions **)
+
+(*Opposite direction fails because Diff in the extended state may remove
+  fewer actions, i.e. those that affect other state variables.*)
+Goal "Diff (project h G) acts  component  \
+\     project h (Diff G (extend_act h `` acts))";
+by (force_tac (claset(), 
+	       simpset() addsimps [component_eq_subset, Diff_def]) 1);
+qed "Diff_project_component_project_Diff";
+
+Goal "Diff G (extend_act h `` acts) : (extend_set h A) co (extend_set h B)  \
+\     ==> Diff (project h G) acts : A co B";
+br (Diff_project_component_project_Diff RS component_constrains) 1;
+be (project_constrains RS iffD2) 1;
 qed "Diff_project_co";
 
 Goalw [stable_def]
-     "Diff G (extend_act h `` Acts F) : stable (extend_set h A)  \
-\     ==> Diff (project h G) (Acts F) : stable A";
+     "Diff G (extend_act h `` acts) : stable (extend_set h A)  \
+\     ==> Diff (project h G) acts : stable A";
 by (etac Diff_project_co 1);
 qed "Diff_project_stable";
 
-Goal "Diff G (Acts F) : A co B  \
-\     ==> Diff (extend h G) (extend_act h `` Acts F) \
-\         : (extend_set h A) co (extend_set h B)";
-by (auto_tac (claset(), 
-	      simpset() addsimps [constrains_def, Diff_def]));
-by (blast_tac (claset() addDs [extend_act_D]) 1);
+(** extend versions **)
+
+Goal "(Diff (extend h G) (extend_act h `` acts)) = extend h (Diff G acts)";
+by (auto_tac (claset() addSIs [program_equalityI],
+	      simpset() addsimps [Diff_def,
+				  inj_extend_act RS image_set_diff RS sym,
+				  image_compose RS sym, o_def]));
+qed "Diff_extend_eq";
+
+Goal "(Diff (extend h G) (extend_act h `` acts) \
+\         : (extend_set h A) co (extend_set h B)) \
+\     = (Diff G acts : A co B)";
+by (simp_tac (simpset() addsimps [Diff_extend_eq, extend_constrains]) 1);
 qed "Diff_extend_co";
 
-Goalw [stable_def]
-   "Diff G (Acts F) : stable A  \
-\   ==> Diff (extend h G) (extend_act h `` Acts F) : stable (extend_set h A)";
-by (etac Diff_extend_co 1);
+Goal "(Diff (extend h G) (extend_act h `` acts) : stable (extend_set h A)) \
+\     = (Diff G acts : stable A)";
+by (simp_tac (simpset() addsimps [Diff_extend_co, stable_def]) 1);
 qed "Diff_extend_stable";
 
+(*Converse appears to fail*)
+Goal "(H : (func o f) localTo extend h G) ==> (project h H : func localTo G)";
+by (asm_full_simp_tac 
+    (simpset() addsimps [localTo_def, 
+			 project_extend_Join RS sym,
+			 Diff_project_stable,
+			 Collect_eq_extend_set RS sym]) 1);
+qed "project_localTo_I";
+
 
 (*** Weak safety primitives: Co, Stable ***)
 
@@ -388,19 +427,6 @@
 (*** Programs of the form  ((extend h F) Join G)
      in other words programs containing an extended component ***)
 
-Goal "project h ((extend h F) Join G) = F Join (project h G)";
-by (rtac program_equalityI 1);
-by (simp_tac (simpset() addsimps [Acts_Join, image_Un,
-				  image_compose RS sym, o_def]) 2);
-by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
-qed "project_extend_Join";
-
-Goal "(extend h F) Join G = extend h H ==> H = F Join (project h G)";
-by (dres_inst_tac [("f", "project h")] arg_cong 1);
-by (full_simp_tac (simpset() addsimps [project_extend_Join]) 1);
-by (etac sym 1);
-qed "extend_Join_eq_extend_D";
-
 Goal "z : reachable (extend h F Join G)  \
 \     ==> f z : reachable (F Join project h G)";
 by (etac reachable.induct 1);
@@ -549,25 +575,6 @@
 qed "f_act_extend_act";
 Addsimps [f_act_extend_act];
 
-Goalw [extend_set_def]
-     "f `` (extend_set h A Int B) = (f `` extend_set h A) Int (f``B)";
-by (force_tac (claset() addIs  [h_f_g_eq RS sym], simpset()) 1);
-qed "image_extend_set_Int_eq";
-
-Goal "(extend h F) Join G = extend h H ==> EX J. H = F Join J";
-by (etac program_equalityE 1);
-by (auto_tac (claset(), simpset() addsimps [Acts_Join]));
-by (res_inst_tac [("x", "mk_program(f``(Init G), f_act``Acts G)")] exI 1);
-by (rtac program_equalityI 1);
-(*Init*)
-by (REPEAT (dres_inst_tac [("f", "op `` f")] arg_cong 1));
-by (asm_full_simp_tac (simpset() addsimps [image_extend_set_Int_eq]) 1);
-(*Now for the Actions*)
-by (dres_inst_tac [("f", "op `` f_act")] arg_cong 1);
-by (asm_full_simp_tac 
-    (simpset() addsimps [Acts_Join, image_Un, image_compose RS sym, o_def]) 1);
-qed "extend_Join_eq_extend_D";
-
 (** Strong precondition and postcondition; doesn't seem very useful. **)
 
 Goal "F : X guarantees Y ==> \
@@ -610,58 +617,44 @@
 
 (*** guarantees corollaries ***)
 
-Goalw [increasing_def]
-     "F : UNIV guarantees increasing func \
+Goal "F : UNIV guarantees increasing func \
 \     ==> extend h F : UNIV guarantees increasing (func o f)";
 by (etac project_guarantees 1);
+by (asm_simp_tac
+    (simpset() addsimps [project_extend_Join, project_increasing RS sym]) 2);
 by Auto_tac;
-by (stac Collect_eq_extend_set 1); 
-by (asm_full_simp_tac
-    (simpset() addsimps [extend_stable, project_stable, 
-			 stable_Join]) 1);
 qed "extend_guar_increasing";
 
-Goalw [Increasing_def]
-     "F : UNIV guarantees Increasing func \
+Goal "F : UNIV guarantees Increasing func \
 \     ==> extend h F : UNIV guarantees Increasing (func o f)";
 by (etac project_guarantees 1);
+by (asm_simp_tac
+    (simpset() addsimps [project_extend_Join, project_Increasing_D]) 2);
 by Auto_tac;
-by (stac Collect_eq_extend_set 1); 
-by (asm_simp_tac (simpset() addsimps [extend_Join_Stable]) 1);
 qed "extend_guar_Increasing";
 
-Goalw [localTo_def, increasing_def]
-     "F : (func localTo F) guarantees increasing func  \
-\     ==> extend h F : (func o f) localTo (extend h F)  \
-\                         guarantees increasing (func o f)";
+Goal "F : (func localTo G) guarantees increasing func  \
+\     ==> extend h F : (func o f) localTo (extend h G)  \
+\                      guarantees increasing (func o f)";
 by (etac project_guarantees 1);
-by Auto_tac;
-by (stac Collect_eq_extend_set 2); 
 (*the "increasing" guarantee*)
-by (asm_full_simp_tac
-    (simpset() addsimps [extend_stable, project_stable, 
-			 stable_Join]) 2);
+by (asm_simp_tac
+    (simpset() addsimps [project_extend_Join, project_increasing RS sym]) 2);
 (*the "localTo" requirement*)
-by (asm_simp_tac
-    (simpset() addsimps [project_extend_Join RS sym,
-			 Diff_project_stable, 
-			 Collect_eq_extend_set RS sym]) 1); 
+by (asm_simp_tac 
+    (simpset() addsimps [project_localTo_I, project_extend_Join RS sym]) 1);
 qed "extend_localTo_guar_increasing";
 
-Goalw [localTo_def, Increasing_def]
-     "F : (func localTo F) guarantees Increasing func  \
-\     ==> extend h F : (func o f) localTo (extend h F)  \
-\                         guarantees Increasing (func o f)";
+Goal "F : (func localTo G) guarantees Increasing func  \
+\     ==> extend h F : (func o f) localTo (extend h G)  \
+\                      guarantees Increasing (func o f)";
 by (etac project_guarantees 1);
-by Auto_tac;
-by (stac Collect_eq_extend_set 2); 
 (*the "Increasing" guarantee*)
-by (asm_simp_tac (simpset() addsimps [extend_Join_Stable]) 2);
+by (asm_simp_tac
+    (simpset() addsimps [project_extend_Join, project_Increasing_D]) 2);
 (*the "localTo" requirement*)
-by (asm_simp_tac
-    (simpset() addsimps [project_extend_Join RS sym,
-			 Diff_project_stable, 
-			 Collect_eq_extend_set RS sym]) 1); 
+by (asm_simp_tac 
+    (simpset() addsimps [project_localTo_I, project_extend_Join RS sym]) 1);
 qed "extend_localTo_guar_Increasing";
 
 Close_locale "Extend";