# HG changeset patch
# User paulson
# Date 940610120 -7200
# Node ID c7fd7eb3b0efa0e8d34c87420f3d627c6f42de00
# Parent  5bfde29f1dbbbdb85ad3ecdab45ce3c4b886c9b1
ALMOST working version: LocalTo results commented out

diff -r 5bfde29f1dbb -r c7fd7eb3b0ef src/HOL/UNITY/Alloc.ML
--- a/src/HOL/UNITY/Alloc.ML	Fri Oct 22 18:33:39 1999 +0200
+++ b/src/HOL/UNITY/Alloc.ML	Fri Oct 22 18:35:20 1999 +0200
@@ -388,7 +388,7 @@
 
 (*A LOT of work just to lift "Client_Progress" to the array*)
 Goal "lift_prog i Client \
-\  : Increasing (giv o sub i) Int ((%z. z i) localTo[UNIV] (lift_prog i Client)) \
+\  : Increasing (giv o sub i) Int ((%z. z i) LocalTo (lift_prog i Client)) \
 \    guarantees \
 \    (INT h. {s. h <=  (giv o sub i) s & \
 \                       h pfixGe (ask o sub i) s}  \
diff -r 5bfde29f1dbb -r c7fd7eb3b0ef src/HOL/UNITY/Comp.ML
--- a/src/HOL/UNITY/Comp.ML	Fri Oct 22 18:33:39 1999 +0200
+++ b/src/HOL/UNITY/Comp.ML	Fri Oct 22 18:35:20 1999 +0200
@@ -48,6 +48,14 @@
 by (Blast_tac 1);
 qed "component_Join2";
 
+Goal "F<=G ==> F Join G = G";
+by (auto_tac (claset(), simpset() addsimps [component_def, Join_left_absorb]));
+qed "Join_absorb1";
+
+Goal "G<=F ==> F Join G = F";
+by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def]));
+qed "Join_absorb2";
+
 Goalw [component_def] "i : I ==> (F i) <= (JN i:I. (F i))";
 by (blast_tac (claset() addIs [JN_absorb]) 1);
 qed "component_JN";
diff -r 5bfde29f1dbb -r c7fd7eb3b0ef src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Fri Oct 22 18:33:39 1999 +0200
+++ b/src/HOL/UNITY/Extend.ML	Fri Oct 22 18:35:20 1999 +0200
@@ -8,17 +8,6 @@
   function g (forgotten) maps the extended state to the "extending part"
 *)
 
-
-
-		Goal "(A Int B = {}) = (ALL x:A. ALL y:B. x ~= y)";
-		by  (Blast_tac 1);
-		qed "disjoint_iff_not_equal";
-
-		Goal "ff -`` (ff `` A) = {y. EX x:A. ff x = ff y}";
-		by (blast_tac (claset() addIs [sym]) 1);
-		qed "vimage_image_eq";
-
-
 (** These we prove OUTSIDE the locale. **)
 
 (*Possibly easier than reasoning about "inv h"*)
@@ -277,7 +266,7 @@
 qed "project_act_Id";
 
 Goalw [project_set_def, project_act_def]
-  "Domain (project_act h (Restrict C act)) = project_set h (Domain act Int C)";
+  "Domain (project_act h act) = project_set h (Domain act)";
 by (force_tac (claset(), 
               simpset() addsimps [split_extended_all]) 1);
 qed "Domain_project_act";
@@ -330,14 +319,19 @@
 qed "project_set_UNIV";
 Addsimps [project_set_UNIV];
 
+Goal "project h C (extend h F) = \
+\     mk_program (Init F, Restrict (project_set h C) `` Acts F)";
+by (rtac program_equalityI 1);
+by (asm_simp_tac (simpset() addsimps [image_eq_UN, 
+                   project_act_extend_act_restrict]) 2);
+by (Simp_tac 1);
+qed "project_extend_eq";
+
 (*ALL act: Acts F. Domain act is MUCH TOO STRONG since Domain Id = UNIV!*)
 Goal "UNIV <= project_set h C \
 \     ==> project h C (extend h F) = F";
-by (simp_tac (simpset() addsimps [extend_def, project_def]) 1);
-by (rtac program_equalityI 1);
-by (asm_simp_tac (simpset() addsimps [image_image_eq_UN, image_UN, 
-                   subset_UNIV RS subset_trans RS Restrict_triv]) 2);
-by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [project_extend_eq, image_eq_UN, 
+                   subset_UNIV RS subset_trans RS Restrict_triv]) 1);
 qed "extend_inverse";
 Addsimps [extend_inverse];
 
@@ -409,12 +403,14 @@
               simpset() addsimps [extend_act_def]));
 qed "Restrict_extend_set";
 
-Goal "(Diff (extend_set h C) (extend h G) (extend_act h `` acts)) = \
+Goalw [Diff_def]
+     "(Diff (extend_set h C) (extend h G) (extend_act h `` acts)) = \
 \     extend h (Diff C G acts)";
-by (auto_tac (claset() addSIs [program_equalityI],
-	      simpset() addsimps [Diff_def, image_image_eq_UN,
-				  Restrict_extend_set,
-				  inj_extend_act RS image_set_diff]));
+by (rtac program_equalityI 1);
+by (Simp_tac 1);
+by (simp_tac (simpset() addsimps [inj_extend_act RS image_set_diff]) 1);
+by (simp_tac (simpset() addsimps [image_eq_UN,
+				  Restrict_extend_set]) 1);
 qed "Diff_extend_eq";
 
 (*Opposite inclusion fails; this inclusion's more general than that of
diff -r 5bfde29f1dbb -r c7fd7eb3b0ef src/HOL/UNITY/LessThan.ML
--- a/src/HOL/UNITY/LessThan.ML	Fri Oct 22 18:33:39 1999 +0200
+++ b/src/HOL/UNITY/LessThan.ML	Fri Oct 22 18:35:20 1999 +0200
@@ -61,6 +61,17 @@
 by (Blast_tac 1);
 qed "image_Diff_image_eq";
 
+Goal "Domain (Restrict A r) = A Int Domain r";
+by (Blast_tac 1);
+qed "Domain_Restrict";
+
+Goal "(Restrict A r) ^^ B = r ^^ (A Int B)";
+by (Blast_tac 1);
+qed "Image_Restrict";
+
+Addsimps [Domain_Restrict, Image_Restrict];
+
+
 
 (*** lessThan ***)
 
diff -r 5bfde29f1dbb -r c7fd7eb3b0ef src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Fri Oct 22 18:33:39 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML	Fri Oct 22 18:35:20 1999 +0200
@@ -453,12 +453,14 @@
 by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
 qed "lift_prog_localTo_guar_increasing";
 
+(***
 Goal "F : (v LocalTo G) guarantees Increasing func  \
 \     ==> lift_prog i F : (v o sub i) LocalTo (lift_prog i G)  \
 \                         guarantees Increasing (func o sub i)";
 by (dtac (lift_export extend_LocalTo_guar_Increasing) 1);
 by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
 qed "lift_prog_LocalTo_guar_Increasing";
+***)
 
 Goal "F : Always A guarantees Always B \
 \ ==> lift_prog i F : Always(lift_set i A) guarantees Always (lift_set i B)";
diff -r 5bfde29f1dbb -r c7fd7eb3b0ef src/HOL/UNITY/Project.ML
--- a/src/HOL/UNITY/Project.ML	Fri Oct 22 18:33:39 1999 +0200
+++ b/src/HOL/UNITY/Project.ML	Fri Oct 22 18:35:20 1999 +0200
@@ -35,7 +35,7 @@
 Goal "UNIV <= project_set h C \
 \     ==> project h C ((extend h F) Join G) = F Join (project h C G)";
 by (rtac program_equalityI 1);
-by (asm_simp_tac (simpset() addsimps [image_Un, image_image_eq_UN, image_UN,
+by (asm_simp_tac (simpset() addsimps [image_eq_UN, UN_Un,
 			subset_UNIV RS subset_trans RS Restrict_triv]) 2);
 by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
 qed "project_extend_Join";
@@ -247,9 +247,9 @@
 \  <= project h C (Diff C G acts)";
 by (simp_tac 
     (simpset() addsimps [component_eq_subset, Diff_def,
-			 Restrict_project_act, project_act_Restrict_Id, 
-			 image_image_eq_UN, image_UN, Restrict_image_Diff]) 1);
-by (Force_tac 1);
+			 project_act_Restrict_Id, Restrict_image_Diff]) 1);
+by (force_tac (claset() delrules [equalityI], 
+	       simpset() addsimps [Restrict_project_act, image_eq_UN]) 1);
 qed "Diff_project_project_component_project_Diff";
 
 Goal "Diff (project_set h C) (project h C G) acts <= \
@@ -259,8 +259,7 @@
 by (simp_tac 
     (simpset() addsimps [component_eq_subset, Diff_def,
 			 Restrict_project_act, project_act_Restrict_Id, 
-			 image_image_eq_UN, image_UN, Restrict_image_Diff]) 1);
-by (Blast_tac 1);
+			 image_eq_UN, Restrict_image_Diff]) 1);
 qed "Diff_project_component_project_Diff";
 
 Goal "Diff C G (extend_act h `` acts) : (extend_set h A) co (extend_set h B) \
@@ -282,8 +281,8 @@
 Goal "Diff C (extend h G) (extend_act h `` acts) \
 \         : (extend_set h A) co (extend_set h B) \
 \     ==> Diff (project_set h C) G acts : A co B";
-br (Diff_project_set_component RS component_constrains) 1;
-by (forward_tac [constrains_imp_subset] 1);
+by (rtac (Diff_project_set_component RS component_constrains) 1);
+by (ftac constrains_imp_subset 1);
 by (asm_full_simp_tac
     (simpset() addsimps [project_constrains, extend_set_strict_mono]) 1);
 by (blast_tac (claset() addIs [constrains_weaken]) 1);
@@ -299,7 +298,7 @@
      "extend h F : (v o f) localTo[C] extend h H \
 \     ==> F : v localTo[project_set h C] H";
 by Auto_tac;
-br Diff_project_set_stable_I 1;
+by (rtac Diff_project_set_stable_I 1);
 by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym]) 1);
 qed "localTo_project_set_I";
 
@@ -324,7 +323,7 @@
 
 Goal "extend h F Join G : (v o f) localTo[UNIV] extend h H \
 \     ==> F Join project h UNIV G : v localTo[UNIV] H";
-bd gen_project_localTo_I 1;
+by (dtac gen_project_localTo_I 1);
 by (Asm_full_simp_tac 1);
 qed "project_localTo_I";
 
@@ -473,12 +472,16 @@
 				      Collect_eq_extend_set RS sym]) 1);
 qed "project_Increasing";
 
+(**
 Goal "extend h F Join G : (v o f) LocalTo extend h H \
 \     ==> F Join project h (reachable (extend h F Join G)) G : v LocalTo H";
 by (asm_full_simp_tac 
     (simpset() addsimps [LocalTo_def, project_set_reachable_extend_eq RS sym,
-			 gen_project_localTo_I]) 1);
+			 gen_project_localTo_I,
+			 Join_assoc RS sym]) 1);
+
 qed "project_LocalTo_I";
+**)
 
 (** A lot of redundant theorems: all are proved to facilitate reasoning
     about guarantees. **)
@@ -507,11 +510,13 @@
 by (blast_tac (claset() addIs [project_Increasing_I]) 1);
 qed "projecting_Increasing";
 
+(**
 Goalw [projecting_def]
      "projecting (%G. reachable (extend h F Join G)) h F \
-\         ((v o f) LocalTo extend h H)  (v LocalTo H)";
+\                ((v o f) LocalTo extend h H) (v LocalTo H)";
 by (blast_tac (claset() addIs [project_LocalTo_I]) 1);
 qed "projecting_LocalTo";
+**)
 
 Goalw [extending_def]
      "extending (%G. reachable (extend h F Join G)) h F X' \
@@ -554,7 +559,7 @@
 \        F : transient (extend_set h A) |] \
 \     ==> project h C F : transient A";
 by (auto_tac (claset() delrules [ballE],
-              simpset() addsimps [Domain_project_act, Int_absorb2]));
+              simpset() addsimps [Domain_project_act, Int_absorb1]));
 by (REPEAT (ball_tac 1));
 by (auto_tac (claset(),
               simpset() addsimps [extend_set_def, project_set_def, 
@@ -579,7 +584,7 @@
 by (assume_tac 2);
 by Auto_tac;
 by (eres_inst_tac [("P", "A <= ?B")] rev_mp 1);
-by (force_tac (claset(), simpset() addsimps [Int_absorb2]) 1);
+by (force_tac (claset(), simpset() addsimps [Int_absorb1]) 1);
 (*The Domain requirement's proved; must prove the Image requirement*)
 by (res_inst_tac [("y1", "x")] (surj_h RS surjD RS exE) 1);
 by (res_inst_tac [("y1", "xa")] (surj_h RS surjD RS exE) 1);
@@ -756,6 +761,7 @@
 by (rtac projecting_localTo 1);
 qed "extend_localTo_guar_increasing";
 
+(**
 Goal "F : (v LocalTo G) guarantees Increasing func  \
 \     ==> extend h F : (v o f) LocalTo (extend h G)  \
 \                      guarantees Increasing (func o f)";
@@ -764,6 +770,7 @@
 by (rtac projecting_LocalTo 1);
 by Auto_tac;
 qed "extend_LocalTo_guar_Increasing";
+**)
 
 Goal "F : Always A guarantees Always B \
 \ ==> extend h F : Always(extend_set h A) guarantees Always(extend_set h B)";
@@ -775,61 +782,45 @@
 
 (** Guarantees with a leadsTo postcondition **)
 
-(*Bridges the gap between the "old" and "new" condition of the leadsTo rules*)
-Goal "[| ALL x. project h C G ~: transient {x}; project h C G: transient D |] \
+Goalw [LOCALTO_def, transient_def, Diff_def]
+     "[| G : f localTo[C] extend h F;  project h C G : transient D |]    \
 \     ==> F : transient D";
+by Auto_tac;
+by (case_tac "Restrict C act : Restrict C ``extend_act h `` Acts F" 1);
+by Auto_tac; 
+by (rtac bexI 1);
+by (assume_tac 2);
+by (Blast_tac 1);
 by (case_tac "D={}" 1);
-by (auto_tac (claset() addIs [transient_strengthen], simpset()));
-qed "transient_lemma";
-
-
-(*Previously tried to prove
-[| G : f localTo extend h F; project h C G : transient D |] ==> F : transient D
-but it can fail if C removes some parts of an action of G.*)
-
-
-Goal "[| G : v localTo[UNIV] F;  Disjoint UNIV F G |] ==> G : stable {s. v s = z}";
-by (asm_full_simp_tac 
-    (simpset() addsimps [LOCALTO_def, Diff_def, Disjoint_def,
-			 stable_def, constrains_def]) 1);
 by (Blast_tac 1);
-qed "localTo_imp_stable";
-
-Goal "[| G : f localTo[UNIV] extend h F; \
-\        Disjoint UNIV (extend h F) G |] ==> project h C G : stable {x}";
-by (asm_full_simp_tac
-    (simpset() addsimps [localTo_imp_stable,
-			 extend_set_sing, project_stable_I]) 1);
-qed "localTo_imp_project_stable";
-
-Goal "F : stable{s} ==> F ~: transient {s}";
-by (auto_tac (claset(), 
-	      simpset() addsimps [FP_def, transient_def,
-				  stable_def, constrains_def]));
-qed "stable_sing_imp_not_transient";
+by (auto_tac (claset(),
+	      simpset() addsimps [stable_def, constrains_def]));
+by (subgoal_tac "ALL z. Restrict C act ^^ {s. f s = z} <= {s. f s = z}" 1);
+by (blast_tac (claset() addSDs [bspec]) 2);
+by (thin_tac "ALL z. ?P z" 1);
+by (subgoal_tac "project_act h (Restrict C act) ^^ D <= D" 1);
+by (Clarify_tac 2);
+by (asm_full_simp_tac (simpset() addsimps [project_act_def]) 2);
+by (force_tac (claset() addSDs [spec, ImageI RSN (2, subsetD)], simpset()) 2);
+by (blast_tac (claset() addSDs [subsetD]) 1);
+qed "localTo_project_transient_transient";
 
 Goal "[| F Join project h UNIV G : A leadsTo B;    \
-\        G : f localTo[UNIV] extend h F; \
-\        Disjoint UNIV (extend h F) G |]  \
+\        G : f localTo[UNIV] extend h F |]  \
 \     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
 by (rtac project_UNIV_leadsTo_lemma 1);
-by (Clarify_tac 1);
-by (rtac transient_lemma 1);
 by (auto_tac (claset(), 
-	      simpset() addsimps [localTo_imp_project_stable, 
-				  stable_sing_imp_not_transient]));
+         simpset() addsimps [impOfSubs (subset_UNIV RS localTo_anti_mono) RS
+			     localTo_project_transient_transient]));
 qed "project_leadsTo_D";
 
 Goal "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B; \
-\         G : f localTo[UNIV] extend h F; \
-\         Disjoint UNIV (extend h F) G |]  \
+\         G : f LocalTo extend h F |]  \
 \      ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
 by (rtac (refl RS Join_project_LeadsTo) 1);
-by (Clarify_tac 1);
-by (rtac transient_lemma 1);
 by (auto_tac (claset(), 
-	      simpset() addsimps [localTo_imp_project_stable, 
-				  stable_sing_imp_not_transient]));
+	      simpset() addsimps [LocalTo_def,
+				  localTo_project_transient_transient]));
 qed "project_LeadsTo_D";
 
 Goalw [extending_def]
@@ -842,10 +833,11 @@
 
 Goalw [extending_def]
      "extending (%G. reachable (extend h F Join G)) h F \
-\               (f localTo[UNIV] extend h F) \
+\               (f LocalTo extend h F) \
 \               (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)";
-by (blast_tac (claset() addSDs [Join_localTo RS iffD1]
-			addIs [project_LeadsTo_D]) 1);
+by (force_tac (claset() addIs [project_LeadsTo_D],
+	       simpset()addsimps [LocalTo_def, Join_assoc RS sym, 
+				  Join_localTo]) 1);
 qed "extending_LeadsTo";
 
 (*STRONG precondition and postcondition*)
@@ -862,7 +854,7 @@
 (*WEAK precondition and postcondition*)
 Goal "F : (A Co A') guarantees (B LeadsTo B')  \
 \ ==> extend h F : ((extend_set h A) Co (extend_set h A'))  \
-\                   Int (f localTo[UNIV] (extend h F)) \
+\                   Int (f LocalTo (extend h F)) \
 \                  guarantees ((extend_set h B) LeadsTo (extend_set h B'))";
 by (etac project_guarantees 1);
 by (rtac (extending_LeadsTo RS extending_weaken) 2);
diff -r 5bfde29f1dbb -r c7fd7eb3b0ef src/HOL/UNITY/UNITY.ML
--- a/src/HOL/UNITY/UNITY.ML	Fri Oct 22 18:33:39 1999 +0200
+++ b/src/HOL/UNITY/UNITY.ML	Fri Oct 22 18:35:20 1999 +0200
@@ -62,14 +62,17 @@
 
 (** The notation of equality for type "program" **)
 
-Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G";
-by (subgoals_tac ["EX x. Rep_Program F = x",
-		  "EX x. Rep_Program G = x"] 1);
-by (REPEAT (Blast_tac 2));
-by (Clarify_tac 1);
+
+Goal "mk_program (Init F, Acts F) = F";
+by (cut_inst_tac [("x", "F")] Rep_Program 1);
 by (auto_tac (claset(), rep_ss));
 by (REPEAT (dres_inst_tac [("f", "Abs_Program")] arg_cong 1));
-by (asm_full_simp_tac rep_ss 1);
+by (asm_full_simp_tac (rep_ss addsimps [insert_absorb]) 1);
+qed "surjective_mk_program";
+
+Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G";
+by (stac (surjective_mk_program RS sym) 1);
+by (stac (surjective_mk_program RS sym) 1 THEN Force_tac 1);
 qed "program_equalityI";
 
 val [major,minor] =
@@ -78,6 +81,8 @@
 by (auto_tac (claset(), simpset() addsimps [major]));
 qed "program_equalityE";
 
+Addsimps [surjective_mk_program];
+
 
 (*** These rules allow "lazy" definition expansion 
      They avoid expanding the full program, which is a large expression
diff -r 5bfde29f1dbb -r c7fd7eb3b0ef src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Fri Oct 22 18:33:39 1999 +0200
+++ b/src/HOL/UNITY/Union.ML	Fri Oct 22 18:35:20 1999 +0200
@@ -126,7 +126,7 @@
 
 Addsimps [Join_absorb];
 
-Goalw [Join_def] "A Join (A Join B) = A Join B";
+Goalw [Join_def] "F Join (F Join G) = F Join G";
 by (rtac program_equalityI 1);
 by Auto_tac;
 qed "Join_left_absorb";
@@ -336,15 +336,16 @@
 by (force_tac (claset() addSEs [allE, ballE], simpset()) 1);
 qed "localTo_imp_o_localTo";
 
+(*NOT USED*)
 Goalw [LOCALTO_def, stable_def, constrains_def]
      "(%s. x) localTo[C] F = UNIV";
 by (Blast_tac 1);
 qed "triv_localTo_eq_UNIV";
 
-Goal "(F Join G : v localTo[C] H) = (F : v localTo[C] H  &  G : v localTo[C] H)";
-by (asm_full_simp_tac 
-    (simpset() addsimps [LOCALTO_def, Diff_Join_distrib,
-			 stable_def, Join_constrains]) 1);
+Goal "(F Join G : v localTo[C] H) = \
+\     (F : v localTo[C] H  &  G : v localTo[C] H)";
+by (simp_tac (simpset() addsimps [LOCALTO_def, Diff_Join_distrib,
+				  stable_def, Join_constrains]) 1);
 by (Blast_tac 1);
 qed "Join_localTo";
 
diff -r 5bfde29f1dbb -r c7fd7eb3b0ef src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Fri Oct 22 18:33:39 1999 +0200
+++ b/src/HOL/UNITY/Union.thy	Fri Oct 22 18:35:20 1999 +0200
@@ -33,7 +33,7 @@
 
   (*The weak version of localTo, considering only G's reachable states*)
   LocalTo :: ['a => 'b, 'a program] => 'a program set  (infixl 80)
-    "v LocalTo F == {G. G : v localTo[reachable G] F}"
+    "v LocalTo F == {G. G : v localTo[reachable (F Join G)] F}"
 
   (*Two programs with disjoint actions, except for identity actions.
     It's a weak property but still useful.*)