# HG changeset patch
# User paulson
# Date 940256163 -7200
# Node ID 62fb24e28e5ed8515bc40fa8dc9af16ae715b5b1
# Parent  4547f0bd94545e1f62eadf32806b7efb7d80bc25
exchanged the first two args of "project" and "drop_prog"

diff -r 4547f0bd9454 -r 62fb24e28e5e src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Mon Oct 18 15:20:21 1999 +0200
+++ b/src/HOL/UNITY/Extend.ML	Mon Oct 18 16:16:03 1999 +0200
@@ -304,7 +304,7 @@
 by Auto_tac;
 qed "Init_extend";
 
-Goalw [project_def] "Init (project C h F) = project_set h (Init F)";
+Goalw [project_def] "Init (project h C F) = project_set h (Init F)";
 by Auto_tac;
 qed "Init_project";
 
@@ -313,7 +313,7 @@
 	      simpset() addsimps [extend_def, image_iff]));
 qed "Acts_extend";
 
-Goal "Acts (project C h F) = insert Id (project_act h `` Restrict C `` Acts F)";
+Goal "Acts (project h C F) = insert Id (project_act h `` Restrict C `` Acts F)";
 by (auto_tac (claset(), 
 	      simpset() addsimps [project_def, image_iff]));
 qed "Acts_project";
@@ -332,7 +332,7 @@
 
 (*ALL act: Acts F. Domain act is MUCH TOO STRONG since Domain Id = UNIV!*)
 Goal "UNIV <= project_set h C \
-\     ==> project C h (extend h F) = F";
+\     ==> 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, 
@@ -369,7 +369,7 @@
 by Auto_tac;
 qed "extend_mono";
 
-Goal "F <= G ==> project C h F <= project C h G";
+Goal "F <= G ==> project h C F <= project h C G";
 by (full_simp_tac
     (simpset() addsimps [component_eq_subset, project_set_def]) 1);
 by Auto_tac;
@@ -420,7 +420,7 @@
 (*Opposite inclusion fails; this inclusion's more general than that of
   Diff_extend_eq*)     
 Goal "Diff (project_set h C) G acts \
-\     <= project C h (Diff C (extend h G) (extend_act h `` acts))";
+\     <= project h C (Diff C (extend h G) (extend_act h `` acts))";
 by (simp_tac
     (simpset() addsimps [component_eq_subset, Diff_def,image_UN,
 			 image_image, image_Diff_image_eq,
diff -r 4547f0bd9454 -r 62fb24e28e5e src/HOL/UNITY/Extend.thy
--- a/src/HOL/UNITY/Extend.thy	Mon Oct 18 15:20:21 1999 +0200
+++ b/src/HOL/UNITY/Extend.thy	Mon Oct 18 16:16:03 1999 +0200
@@ -33,8 +33,8 @@
 			       extend_act h `` Acts F)"
 
   (*Argument C allows weak safety laws to be projected*)
-  project :: "['c set, 'a*'b => 'c, 'c program] => 'a program"
-    "project C h F == mk_program (project_set h (Init F),
+  project :: "['a*'b => 'c, 'c set, 'c program] => 'a program"
+    "project h C F == mk_program (project_set h (Init F),
 		  	          project_act h `` Restrict C `` Acts F)"
 
 locale Extend =
diff -r 4547f0bd9454 -r 62fb24e28e5e src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Mon Oct 18 15:20:21 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML	Mon Oct 18 16:16:03 1999 +0200
@@ -72,12 +72,12 @@
 qed "Acts_lift_prog";
 Addsimps [Acts_lift_prog];
 
-Goalw [drop_prog_def] "Init (drop_prog C i F) = drop_set i (Init F)";
+Goalw [drop_prog_def] "Init (drop_prog i C F) = drop_set i (Init F)";
 by Auto_tac;
 qed "Init_drop_prog";
 Addsimps [Init_drop_prog];
 
-Goal "Acts (drop_prog C i F) = insert Id (drop_act i `` Restrict C `` Acts F)";
+Goal "Acts (drop_prog i C F) = insert Id (drop_act i `` Restrict C `` Acts F)";
 by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], 
 	      simpset() addsimps [drop_prog_def]));
 qed "Acts_drop_prog";
@@ -181,7 +181,7 @@
 			lift_act_correct]) 1);
 qed "lift_prog_correct";
 
-Goal "drop_prog C i = project C (lift_map i)";
+Goal "drop_prog i C = project (lift_map i) C";
 by (rtac (program_equalityI RS ext) 1);
 by (simp_tac (simpset() addsimps [drop_set_correct]) 1);
 by (simp_tac (simpset() 
@@ -234,7 +234,7 @@
 Addsimps [lift_act_inverse];
 *)
 
-Goal "UNIV <= drop_set i C ==> drop_prog C i (lift_prog i F) = F";
+Goal "UNIV <= drop_set i C ==> drop_prog i C (lift_prog i F) = F";
 by (asm_full_simp_tac
     (simpset() addsimps [drop_set_correct, drop_prog_correct, 
 			 lift_prog_correct, lift_export extend_inverse]) 1);
@@ -297,14 +297,14 @@
 
 (** Safety and drop_prog **)
 
-Goal "(drop_prog C i F : A co B)  =  \
+Goal "(drop_prog i C F : A co B)  =  \
 \     (F : (C Int lift_set i A) co (lift_set i B) & A <= B)";
 by (simp_tac
     (simpset() addsimps [drop_prog_correct, 
 			 lift_set_correct, lift_export project_constrains]) 1);
 qed "drop_prog_constrains";
 
-Goal "(drop_prog UNIV i F : stable A)  =  (F : stable (lift_set i A))";
+Goal "(drop_prog i UNIV F : stable A)  =  (F : stable (lift_set i A))";
 by (simp_tac (simpset() addsimps [stable_def, drop_prog_constrains]) 1);
 qed "drop_prog_stable";
 
@@ -312,7 +312,7 @@
 (*** Diff, needed for localTo ***)
 
 Goal "[| Diff C G (lift_act i `` acts) : (lift_set i A) co (lift_set i B) |] \
-\     ==> Diff (drop_set i C) (drop_prog C i G) acts : A co B";
+\     ==> Diff (drop_set i C) (drop_prog i C G) acts : A co B";
 by (asm_full_simp_tac
     (simpset() addsimps [drop_set_correct, drop_prog_correct, 
 			 lift_set_correct, lift_act_correct, 
@@ -321,7 +321,7 @@
 
 Goalw [stable_def]
      "[| Diff C G (lift_act i `` acts) : stable (lift_set i A) |]  \
-\     ==> Diff (drop_set i C) (drop_prog C i G) acts : stable A";
+\     ==> Diff (drop_set i C) (drop_prog i C G) acts : stable A";
 by (blast_tac (claset() addIs [Diff_drop_prog_constrains]) 1);
 qed "Diff_drop_prog_stable";
 
@@ -347,7 +347,7 @@
 qed "lift_prog_Stable";
 
 Goal "[| reachable (lift_prog i F Join G) <= C;    \
-\        F Join drop_prog C i G : A Co B |] \
+\        F Join drop_prog i C G : A Co B |] \
 \     ==> lift_prog i F Join G : (lift_set i A) Co (lift_set i B)";
 by (asm_full_simp_tac
     (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
@@ -356,13 +356,13 @@
 
 Goalw [Stable_def]
      "[| reachable (lift_prog i F Join G) <= C;    \
-\        F Join drop_prog C i G : Stable A |]  \
+\        F Join drop_prog i C G : Stable A |]  \
 \     ==> lift_prog i F Join G : Stable (lift_set i A)";
 by (asm_simp_tac (simpset() addsimps [drop_prog_Constrains_D]) 1);
 qed "drop_prog_Stable_D";
 
 Goal "[| reachable (lift_prog i F Join G) <= C;  \
-\        F Join drop_prog C i G : Always A |]   \
+\        F Join drop_prog i C G : Always A |]   \
 \     ==> lift_prog i F Join G : Always (lift_set i A)";
 by (asm_full_simp_tac
     (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
@@ -371,7 +371,7 @@
 
 Goalw [Increasing_def]
      "[| reachable (lift_prog i F Join G) <= C;  \
-\        F Join drop_prog C i G : Increasing func |] \
+\        F Join drop_prog i C G : Increasing func |] \
 \     ==> lift_prog i F Join G : Increasing (func o (sub i))";
 by Auto_tac;
 by (stac Collect_eq_lift_set 1);
@@ -381,7 +381,7 @@
 
 (*UNUSED*)
 Goal "UNIV <= drop_set i C \
-\     ==> drop_prog C i ((lift_prog i F) Join G) = F Join (drop_prog C i G)";
+\     ==> drop_prog i C ((lift_prog i F) Join G) = F Join (drop_prog i C G)";
 by (asm_full_simp_tac
     (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
 		     drop_set_correct, lift_export project_extend_Join]) 1);
diff -r 4547f0bd9454 -r 62fb24e28e5e src/HOL/UNITY/Lift_prog.thy
--- a/src/HOL/UNITY/Lift_prog.thy	Mon Oct 18 15:20:21 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.thy	Mon Oct 18 16:16:03 1999 +0200
@@ -31,8 +31,8 @@
 		   lift_act i `` Acts F)"
 
   (*Argument C allows weak safety laws to be projected*)
-  drop_prog :: "[('a=>'b) set, 'a, ('a=>'b) program] => 'b program"
-    "drop_prog C i F ==
+  drop_prog :: "['a, ('a=>'b) set, ('a=>'b) program] => 'b program"
+    "drop_prog i C F ==
        mk_program (drop_set i (Init F),
 		   drop_act i `` Restrict C `` (Acts F))"
 
diff -r 4547f0bd9454 -r 62fb24e28e5e src/HOL/UNITY/Project.ML
--- a/src/HOL/UNITY/Project.ML	Mon Oct 18 15:20:21 1999 +0200
+++ b/src/HOL/UNITY/Project.ML	Mon Oct 18 16:16:03 1999 +0200
@@ -16,24 +16,24 @@
 by (auto_tac (claset(), simpset() addsimps [project_act_def]));
 qed "project_act_mono";
 
-Goal "[| D <= C; project C h F : A co B |] ==> project D h F : A co B";
+Goal "[| D <= C; project h C F : A co B |] ==> project h D F : A co B";
 by (auto_tac (claset(), simpset() addsimps [constrains_def]));
 by (dtac project_act_mono 1);
 by (Blast_tac 1);
 qed "project_constrains_mono";
 
-Goal "[| D <= C;  project C h F : stable A |] ==> project D h F : stable A";
+Goal "[| D <= C;  project h C F : stable A |] ==> project h D F : stable A";
 by (asm_full_simp_tac
     (simpset() addsimps [stable_def, project_constrains_mono]) 1);
 qed "project_stable_mono";
 
-Goal "F : A co B ==> project C h (extend h F) : A co B";
+Goal "F : A co B ==> project h C (extend h F) : A co B";
 by (auto_tac (claset(), 
       simpset() addsimps [extend_act_def, project_act_def, constrains_def]));
 qed "project_extend_constrains_I";
 
 Goal "UNIV <= project_set h C \
-\     ==> project C h ((extend h F) Join G) = F Join (project C h G)";
+\     ==> 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,
 			subset_UNIV RS subset_trans RS Restrict_triv]) 2);
@@ -41,8 +41,8 @@
 qed "project_extend_Join";
 
 Goal "UNIV <= project_set h C \
-\     ==> (extend h F) Join G = extend h H ==> H = F Join (project C h G)";
-by (dres_inst_tac [("f", "project C h")] arg_cong 1);
+\     ==> (extend h F) Join G = extend h H ==> H = F Join (project h C G)";
+by (dres_inst_tac [("f", "project h C")] arg_cong 1);
 by (asm_full_simp_tac (simpset() addsimps [project_extend_Join]) 1);
 qed "extend_Join_eq_extend_D";
 
@@ -50,7 +50,7 @@
 (** Safety **)
 
 Goalw [constrains_def]
-     "(project C h F : A co B)  =  \
+     "(project h C F : A co B)  =  \
 \     (F : (C Int extend_set h A) co (extend_set h B) & A <= B)";
 by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un]));
 by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1);
@@ -60,17 +60,17 @@
 qed "project_constrains";
 
 Goalw [stable_def]
-     "(project UNIV h F : stable A) = (F : stable (extend_set h A))";
+     "(project h UNIV F : stable A) = (F : stable (extend_set h A))";
 by (simp_tac (simpset() addsimps [project_constrains]) 1);
 qed "project_stable";
 
-Goal "F : stable (extend_set h A) ==> project C h F : stable A";
+Goal "F : stable (extend_set h A) ==> project h C F : stable A";
 by (dtac (project_stable RS iffD2) 1);
 by (blast_tac (claset() addIs [project_stable_mono]) 1);
 qed "project_stable_I";
 
 (*used below to prove Join_project_ensures*)
-Goal "[| G : stable C;  project C h G : A unless B |] \
+Goal "[| G : stable C;  project h C G : A unless B |] \
 \     ==> G : (C Int extend_set h A) unless (extend_set h B)";
 by (asm_full_simp_tac
     (simpset() addsimps [unless_def, project_constrains]) 1);
@@ -79,7 +79,7 @@
 qed_spec_mp "project_unless";
 
 (*This form's useful with guarantees reasoning*)
-Goal "(F Join project C h G : A co B)  =  \
+Goal "(F Join project h C G : A co B)  =  \
 \       (extend h F Join G : (C Int extend_set h A) co (extend_set h B) &  \
 \        F : A co B)";
 by (simp_tac (simpset() addsimps [Join_constrains, project_constrains]) 1);
@@ -91,14 +91,14 @@
   could weaken it to G : (C Int extend_set h A) co C*)
 Goalw [stable_def]
      "extend h F Join G : stable C \
-\     ==> (F Join project C h G : stable A)  =  \
+\     ==> (F Join project h C G : stable A)  =  \
 \         (extend h F Join G : stable (C Int extend_set h A) &  \
 \          F : stable A)";
 by (simp_tac (simpset() addsimps [Join_project_constrains]) 1);
 by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1);
 qed "Join_project_stable";
 
-Goal "(F Join project UNIV h G : increasing func)  =  \
+Goal "(F Join project h UNIV G : increasing func)  =  \
 \     (extend h F Join G : increasing (func o f))";
 by (simp_tac (simpset() addsimps [increasing_def, Join_project_stable]) 1);
 by (auto_tac (claset(),
@@ -108,7 +108,7 @@
 
 (*For using project_guarantees in particular cases*)
 Goal "extend h F Join G : extend_set h A co extend_set h B \
-\     ==> F Join project C h G : A co B";
+\     ==> F Join project h C G : A co B";
 by (asm_full_simp_tac
     (simpset() addsimps [project_constrains, Join_constrains, 
 			 extend_constrains]) 1);
@@ -117,7 +117,7 @@
 qed "project_constrains_I";
 
 (*The UNIV argument is essential*)
-Goal "F Join project UNIV h G : A co B \
+Goal "F Join project h UNIV G : A co B \
 \     ==> extend h F Join G : extend_set h A co extend_set h B";
 by (asm_full_simp_tac
     (simpset() addsimps [project_constrains, Join_constrains, 
@@ -243,8 +243,8 @@
 qed "project_act_Restrict_Id";
 
 Goal
-  "Diff(project_set h C)(project C h G)(project_act h `` Restrict C `` acts) \
-\  <= project C h (Diff C G acts)";
+  "Diff(project_set h C)(project h C G)(project_act h `` Restrict C `` acts) \
+\  <= project h C (Diff C G acts)";
 by (simp_tac 
     (simpset() addsimps [component_eq_subset, Diff_def,
 			 Restrict_project_act, project_act_Restrict_Id, 
@@ -252,8 +252,8 @@
 by (Force_tac 1);
 qed "Diff_project_project_component_project_Diff";
 
-Goal "Diff (project_set h C) (project C h G) acts <= \
-\         project C h (Diff C G (extend_act h `` acts))";
+Goal "Diff (project_set h C) (project h C G) acts <= \
+\         project h C (Diff C G (extend_act h `` acts))";
 by (rtac component_trans 1);
 by (rtac Diff_project_project_component_project_Diff 2);
 by (simp_tac 
@@ -264,7 +264,7 @@
 qed "Diff_project_component_project_Diff";
 
 Goal "Diff C G (extend_act h `` acts) : (extend_set h A) co (extend_set h B) \
-\     ==> Diff (project_set h C) (project C h G) acts : A co B";
+\     ==> Diff (project_set h C) (project h C G) acts : A co B";
 by (rtac (Diff_project_component_project_Diff RS component_constrains) 1);
 by (rtac (project_constrains RS iffD2) 1);
 by (ftac constrains_imp_subset 1);
@@ -273,7 +273,7 @@
 
 Goalw [stable_def]
      "Diff C G (extend_act h `` acts) : stable (extend_set h A) \
-\     ==> Diff (project_set h C) (project C h G) acts : stable A";
+\     ==> Diff (project_set h C) (project h C G) acts : stable A";
 by (etac Diff_project_constrains 1);
 qed "Diff_project_stable";
 
@@ -307,7 +307,7 @@
   simultaneously with other variables, and this action would not be 
   superseded by anything in (extend h G) *)
 Goal "H : (v o f) localTo[C] extend h G \
-\     ==> project C h H : v localTo[project_set h C] G";
+\     ==> project h C H : v localTo[project_set h C] G";
 by (asm_full_simp_tac 
     (simpset() addsimps [LOCALTO_def, 
 			 project_extend_Join RS sym,
@@ -316,14 +316,14 @@
 qed "project_localTo_lemma";
 
 Goal "extend h F Join G : (v o f) localTo[C] extend h H \
-\     ==> F Join project C h G : v localTo[project_set h C] H";
+\     ==> F Join project h C G : v localTo[project_set h C] H";
 by (asm_full_simp_tac 
     (simpset() addsimps [Join_localTo, localTo_project_set_I,
 			 project_localTo_lemma]) 1);
 qed "gen_project_localTo_I";
 
 Goal "extend h F Join G : (v o f) localTo[UNIV] extend h H \
-\     ==> F Join project UNIV h G : v localTo[UNIV] H";
+\     ==> F Join project h UNIV G : v localTo[UNIV] H";
 bd gen_project_localTo_I 1;
 by (Asm_full_simp_tac 1);
 qed "project_localTo_I";
@@ -339,7 +339,7 @@
 
 Goal "[| reachable (extend h F Join G) <= C;  \
 \        z : reachable (extend h F Join G) |] \
-\     ==> f z : reachable (F Join project C h G)";
+\     ==> f z : reachable (F Join project h C G)";
 by (etac reachable.induct 1);
 by (force_tac (claset() addIs [reachable.Init, project_set_I],
 	       simpset()) 1);
@@ -355,7 +355,7 @@
   preconditions (localTo) and WEAK postconditions.*)
 Goalw [Constrains_def]
      "[| reachable (extend h F Join G) <= C;    \
-\        F Join project C h G : A Co B |] \
+\        F Join project h C G : A Co B |] \
 \     ==> extend h F Join G : (extend_set h A) Co (extend_set h B)";
 by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1);
 by (Clarify_tac 1);
@@ -365,14 +365,14 @@
 
 Goalw [Stable_def]
      "[| reachable (extend h F Join G) <= C;  \
-\        F Join project C h G : Stable A |]   \
+\        F Join project h C G : Stable A |]   \
 \     ==> extend h F Join G : Stable (extend_set h A)";
 by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1);
 qed "project_Stable_D";
 
 Goalw [Always_def]
      "[| reachable (extend h F Join G) <= C;  \
-\        F Join project C h G : Always A |]   \
+\        F Join project h C G : Always A |]   \
 \     ==> extend h F Join G : Always (extend_set h A)";
 by (force_tac (claset() addIs [reachable.Init, project_set_I],
                simpset() addsimps [project_Stable_D]) 1);
@@ -380,7 +380,7 @@
 
 Goalw [Increasing_def]
      "[| reachable (extend h F Join G) <= C;  \
-\        F Join project C h G : Increasing func |] \
+\        F Join project h C G : Increasing func |] \
 \     ==> extend h F Join G : Increasing (func o f)";
 by Auto_tac;
 by (stac Collect_eq_extend_set 1);
@@ -391,7 +391,7 @@
 (** Converse results for weak safety: benefits of the argument C *)
 
 Goal "[| C <= reachable(extend h F Join G);   \
-\        x : reachable (F Join project C h G) |] \
+\        x : reachable (F Join project h C G) |] \
 \     ==> EX y. h(x,y) : reachable (extend h F Join G)";
 by (etac reachable.induct 1);
 by (ALLGOALS Asm_full_simp_tac);
@@ -405,7 +405,7 @@
 
 
 Goal "project_set h (reachable (extend h F Join G)) = \
-\     reachable (F Join project (reachable (extend h F Join G)) h G)";
+\     reachable (F Join project h (reachable (extend h F Join G)) G)";
 by (auto_tac (claset() addDs [subset_refl RS reachable_imp_reachable_project,
 			      subset_refl RS reachable_project_imp_reachable], 
 	      simpset() addsimps [project_set_def]));
@@ -415,7 +415,7 @@
 Goalw [Constrains_def]
      "[| C <= reachable (extend h F Join G);  \
 \        extend h F Join G : (extend_set h A) Co (extend_set h B) |] \
-\     ==> F Join project C h G : A Co B";
+\     ==> F Join project h C G : A Co B";
 by (full_simp_tac (simpset() addsimps [Join_project_constrains, 
 				       extend_set_Int_distrib]) 1);
 by (rtac conjI 1);
@@ -433,14 +433,14 @@
 Goalw [Stable_def]
      "[| C <= reachable (extend h F Join G);  \
 \        extend h F Join G : Stable (extend_set h A) |] \
-\     ==> F Join project C h G : Stable A";
+\     ==> F Join project h C G : Stable A";
 by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1);
 qed "project_Stable_I";
 
 Goalw [Always_def]
      "[| C <= reachable (extend h F Join G);  \
 \        extend h F Join G : Always (extend_set h A) |]   \
-\     ==> F Join project C h G : Always A";
+\     ==> F Join project h C G : Always A";
 by (auto_tac (claset(), simpset() addsimps [project_Stable_I]));
 by (rewrite_goals_tac [project_set_def, extend_set_def]);
 by (Blast_tac 1);
@@ -449,32 +449,32 @@
 Goalw [Increasing_def]
      "[| C <= reachable (extend h F Join G);  \
 \        extend h F Join G : Increasing (func o f) |] \
-\     ==> F Join project C h G : Increasing func";
+\     ==> F Join project h C G : Increasing func";
 by Auto_tac;
 by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym,
 				      project_Stable_I]) 1); 
 qed "project_Increasing_I";
 
-Goal "(F Join project (reachable (extend h F Join G)) h G : A Co B)  =  \
+Goal "(F Join project h (reachable (extend h F Join G)) G : A Co B)  =  \
 \     (extend h F Join G : (extend_set h A) Co (extend_set h B))";
 by (blast_tac (claset() addIs [project_Constrains_I, project_Constrains_D]) 1);
 qed "project_Constrains";
 
 Goalw [Stable_def]
-     "(F Join project (reachable (extend h F Join G)) h G : Stable A)  =  \
+     "(F Join project h (reachable (extend h F Join G)) G : Stable A)  =  \
 \     (extend h F Join G : Stable (extend_set h A))";
 by (rtac project_Constrains 1);
 qed "project_Stable";
 
 Goal
-   "(F Join project (reachable (extend h F Join G)) h G : Increasing func)  = \
+   "(F Join project h (reachable (extend h F Join G)) G : Increasing func)  = \
 \   (extend h F Join G : Increasing (func o f))";
 by (asm_simp_tac (simpset() addsimps [Increasing_def, project_Stable,
 				      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 (reachable (extend h F Join G)) h G : v LocalTo 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);
@@ -542,7 +542,7 @@
 
 (** Progress includes safety in the definition of ensures **)
 
-(*** Progress for (project C h F) ***)
+(*** Progress for (project h C F) ***)
 
 (** transient **)
 
@@ -552,7 +552,7 @@
      "[| ALL act: Acts F. act ^^ extend_set h A <= - extend_set h A --> \
 \                      Domain act <= C;    \
 \        F : transient (extend_set h A) |] \
-\     ==> project C h F : transient A";
+\     ==> project h C F : transient A";
 by (auto_tac (claset() delrules [ballE],
               simpset() addsimps [Domain_project_act, Int_absorb2]));
 by (REPEAT (ball_tac 1));
@@ -567,7 +567,7 @@
   Converse of the above...it requires a strong assumption about actions
   being enabled for all possible values of the new variables.*)
 Goalw [transient_def]
-     "[| project C h F : transient A;  \
+     "[| project h C F : transient A;  \
 \        ALL act: Acts F. project_act h (Restrict C act) ^^ A <= - A --> \
 \                         Domain act <= C \
 \             & extend_set h (project_set h (Domain act)) <= Domain act |]  \
@@ -594,7 +594,7 @@
 (*For simplicity, the complicated condition on C is eliminated
   NOT SURE THIS IS GOOD FOR ANYTHING: CAN'T PROVE LEADSTO THEOREM*)
 Goal "F : (extend_set h A) ensures (extend_set h B) \
-\     ==> project UNIV h F : A ensures B";
+\     ==> project h UNIV F : A ensures B";
 by (asm_full_simp_tac
     (simpset() addsimps [ensures_def, project_constrains, 
 			 transient_extend_set_imp_project_transient,
@@ -604,9 +604,9 @@
 qed "ensures_extend_set_imp_project_ensures";
 
 (*A strong condition: F can do anything that project G can.*)
-Goal "[| ALL D. project C h G : transient D --> F : transient D;  \
+Goal "[| ALL D. project h C G : transient D --> F : transient D;  \
 \        extend h F Join G : stable C;  \
-\        F Join project C h G : A ensures B |] \
+\        F Join project h C G : A ensures B |] \
 \     ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
 by (case_tac "A <= B" 1);
 by (blast_tac (claset() addIs [subset_imp_ensures] addDs [extend_set_mono]) 1);
@@ -620,9 +620,9 @@
 		       simpset()) 1));
 qed_spec_mp "Join_project_ensures";
 
-Goal "[| ALL D. project C h G : transient D --> F : transient D;  \
+Goal "[| ALL D. project h C G : transient D --> F : transient D;  \
 \        extend h F Join G : stable C;  \
-\        F Join project C h G : A leadsTo B |] \
+\        F Join project h C G : A leadsTo B |] \
 \     ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
 by (etac leadsTo_induct 1);
 by (asm_simp_tac (simpset() delsimps UN_simps
@@ -633,8 +633,8 @@
 qed "project_leadsTo_lemma";
 
 (*Instance of the previous theorem for STRONG progress*)
-Goal "[| ALL D. project UNIV h G : transient D --> F : transient D;  \
-\        F Join project UNIV h G : A leadsTo B |] \
+Goal "[| ALL D. project h UNIV G : transient D --> F : transient D;  \
+\        F Join project h UNIV G : A leadsTo B |] \
 \     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
 by (dtac project_leadsTo_lemma 1);
 by Auto_tac;
@@ -642,9 +642,9 @@
 
 (** Towards the analogous theorem for WEAK progress*)
 
-Goal "[| ALL D. project C h G : transient D --> F : transient D;  \
+Goal "[| ALL D. project h C G : transient D --> F : transient D;  \
 \        extend h F Join G : stable C;  \
-\        F Join project C h G : (project_set h C Int A) leadsTo B |] \
+\        F Join project h C G : (project_set h C Int A) leadsTo B |] \
 \     ==> extend h F Join G : C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)";
 by (etac leadsTo_induct 1);
 by (asm_simp_tac (simpset() delsimps UN_simps
@@ -654,17 +654,17 @@
 by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
 val lemma = result();
 
-Goal "[| ALL D. project C h G : transient D --> F : transient D;  \
+Goal "[| ALL D. project h C G : transient D --> F : transient D;  \
 \        extend h F Join G : stable C;  \
-\        F Join project C h G : (project_set h C Int A) leadsTo B |] \
+\        F Join project h C G : (project_set h C Int A) leadsTo B |] \
 \     ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
 by (rtac (lemma RS leadsTo_weaken) 1);
 by (auto_tac (claset() addIs [project_set_I], simpset()));
 val lemma2 = result();
 
 Goal "[| C = (reachable (extend h F Join G)); \
-\        ALL D. project C h G : transient D --> F : transient D;  \
-\        F Join project C h G : A LeadsTo B |] \
+\        ALL D. project h C G : transient D --> F : transient D;  \
+\        F Join project h C G : A LeadsTo B |] \
 \     ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
 by (asm_full_simp_tac 
     (simpset() addsimps [LeadsTo_def, lemma2, stable_reachable, 
@@ -776,7 +776,7 @@
 (** Guarantees with a leadsTo postcondition **)
 
 (*Bridges the gap between the "old" and "new" condition of the leadsTo rules*)
-Goal "[| ALL x. project C h G ~: transient {x}; project C h G: transient D |] \
+Goal "[| ALL x. project h C G ~: transient {x}; project h C G: transient D |] \
 \     ==> F : transient D";
 by (case_tac "D={}" 1);
 by (auto_tac (claset() addIs [transient_strengthen], simpset()));
@@ -784,7 +784,7 @@
 
 
 (*Previously tried to prove
-[| G : f localTo extend h F; project C h G : transient D |] ==> F : transient D
+[| 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.*)
 
 
@@ -796,7 +796,7 @@
 qed "localTo_imp_stable";
 
 Goal "[| G : f localTo[UNIV] extend h F; \
-\        Disjoint UNIV (extend h F) G |] ==> project C h G : stable {x}";
+\        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);
@@ -808,7 +808,7 @@
 				  stable_def, constrains_def]));
 qed "stable_sing_imp_not_transient";
 
-Goal "[| F Join project UNIV h G : A leadsTo B;    \
+Goal "[| F Join project h UNIV G : A leadsTo B;    \
 \        G : f localTo[UNIV] extend h F; \
 \        Disjoint UNIV (extend h F) G |]  \
 \     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
@@ -820,7 +820,7 @@
 				  stable_sing_imp_not_transient]));
 qed "project_leadsTo_D";
 
-Goal "[| F Join project (reachable (extend h F Join G)) h G : A LeadsTo B; \
+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 |]  \
 \      ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
diff -r 4547f0bd9454 -r 62fb24e28e5e src/HOL/UNITY/Project.thy
--- a/src/HOL/UNITY/Project.thy	Mon Oct 18 15:20:21 1999 +0200
+++ b/src/HOL/UNITY/Project.thy	Mon Oct 18 16:16:03 1999 +0200
@@ -14,12 +14,12 @@
   projecting :: "['c program => 'c set, 'a*'b => 'c, 
 		  'a program, 'c program set, 'a program set] => bool"
   "projecting C h F X' X ==
-     ALL G. extend h F Join G : X' --> F Join project (C G) h G : X"
+     ALL G. extend h F Join G : X' --> F Join project h (C G) G : X"
 
   extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
 		 'c program set, 'c program set, 'a program set] => bool"
   "extending C h F X' Y' Y ==
-     ALL G. F Join project (C G) h G : Y & extend h F Join G : X' &
+     ALL G. F Join project h (C G) G : Y & extend h F Join G : X' &
             Disjoint UNIV (extend h F) G
             --> extend h F Join G : Y'"