exchanged the first two args of "project" and "drop_prog"
authorpaulson
Mon Oct 18 16:16:03 1999 +0200 (1999-10-18)
changeset 788062fb24e28e5e
parent 7879 4547f0bd9454
child 7881 1b1db39a110b
exchanged the first two args of "project" and "drop_prog"
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/Extend.thy
src/HOL/UNITY/Lift_prog.ML
src/HOL/UNITY/Lift_prog.thy
src/HOL/UNITY/Project.ML
src/HOL/UNITY/Project.thy
     1.1 --- a/src/HOL/UNITY/Extend.ML	Mon Oct 18 15:20:21 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Extend.ML	Mon Oct 18 16:16:03 1999 +0200
     1.3 @@ -304,7 +304,7 @@
     1.4  by Auto_tac;
     1.5  qed "Init_extend";
     1.6  
     1.7 -Goalw [project_def] "Init (project C h F) = project_set h (Init F)";
     1.8 +Goalw [project_def] "Init (project h C F) = project_set h (Init F)";
     1.9  by Auto_tac;
    1.10  qed "Init_project";
    1.11  
    1.12 @@ -313,7 +313,7 @@
    1.13  	      simpset() addsimps [extend_def, image_iff]));
    1.14  qed "Acts_extend";
    1.15  
    1.16 -Goal "Acts (project C h F) = insert Id (project_act h `` Restrict C `` Acts F)";
    1.17 +Goal "Acts (project h C F) = insert Id (project_act h `` Restrict C `` Acts F)";
    1.18  by (auto_tac (claset(), 
    1.19  	      simpset() addsimps [project_def, image_iff]));
    1.20  qed "Acts_project";
    1.21 @@ -332,7 +332,7 @@
    1.22  
    1.23  (*ALL act: Acts F. Domain act is MUCH TOO STRONG since Domain Id = UNIV!*)
    1.24  Goal "UNIV <= project_set h C \
    1.25 -\     ==> project C h (extend h F) = F";
    1.26 +\     ==> project h C (extend h F) = F";
    1.27  by (simp_tac (simpset() addsimps [extend_def, project_def]) 1);
    1.28  by (rtac program_equalityI 1);
    1.29  by (asm_simp_tac (simpset() addsimps [image_image_eq_UN, image_UN, 
    1.30 @@ -369,7 +369,7 @@
    1.31  by Auto_tac;
    1.32  qed "extend_mono";
    1.33  
    1.34 -Goal "F <= G ==> project C h F <= project C h G";
    1.35 +Goal "F <= G ==> project h C F <= project h C G";
    1.36  by (full_simp_tac
    1.37      (simpset() addsimps [component_eq_subset, project_set_def]) 1);
    1.38  by Auto_tac;
    1.39 @@ -420,7 +420,7 @@
    1.40  (*Opposite inclusion fails; this inclusion's more general than that of
    1.41    Diff_extend_eq*)     
    1.42  Goal "Diff (project_set h C) G acts \
    1.43 -\     <= project C h (Diff C (extend h G) (extend_act h `` acts))";
    1.44 +\     <= project h C (Diff C (extend h G) (extend_act h `` acts))";
    1.45  by (simp_tac
    1.46      (simpset() addsimps [component_eq_subset, Diff_def,image_UN,
    1.47  			 image_image, image_Diff_image_eq,
     2.1 --- a/src/HOL/UNITY/Extend.thy	Mon Oct 18 15:20:21 1999 +0200
     2.2 +++ b/src/HOL/UNITY/Extend.thy	Mon Oct 18 16:16:03 1999 +0200
     2.3 @@ -33,8 +33,8 @@
     2.4  			       extend_act h `` Acts F)"
     2.5  
     2.6    (*Argument C allows weak safety laws to be projected*)
     2.7 -  project :: "['c set, 'a*'b => 'c, 'c program] => 'a program"
     2.8 -    "project C h F == mk_program (project_set h (Init F),
     2.9 +  project :: "['a*'b => 'c, 'c set, 'c program] => 'a program"
    2.10 +    "project h C F == mk_program (project_set h (Init F),
    2.11  		  	          project_act h `` Restrict C `` Acts F)"
    2.12  
    2.13  locale Extend =
     3.1 --- a/src/HOL/UNITY/Lift_prog.ML	Mon Oct 18 15:20:21 1999 +0200
     3.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Mon Oct 18 16:16:03 1999 +0200
     3.3 @@ -72,12 +72,12 @@
     3.4  qed "Acts_lift_prog";
     3.5  Addsimps [Acts_lift_prog];
     3.6  
     3.7 -Goalw [drop_prog_def] "Init (drop_prog C i F) = drop_set i (Init F)";
     3.8 +Goalw [drop_prog_def] "Init (drop_prog i C F) = drop_set i (Init F)";
     3.9  by Auto_tac;
    3.10  qed "Init_drop_prog";
    3.11  Addsimps [Init_drop_prog];
    3.12  
    3.13 -Goal "Acts (drop_prog C i F) = insert Id (drop_act i `` Restrict C `` Acts F)";
    3.14 +Goal "Acts (drop_prog i C F) = insert Id (drop_act i `` Restrict C `` Acts F)";
    3.15  by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], 
    3.16  	      simpset() addsimps [drop_prog_def]));
    3.17  qed "Acts_drop_prog";
    3.18 @@ -181,7 +181,7 @@
    3.19  			lift_act_correct]) 1);
    3.20  qed "lift_prog_correct";
    3.21  
    3.22 -Goal "drop_prog C i = project C (lift_map i)";
    3.23 +Goal "drop_prog i C = project (lift_map i) C";
    3.24  by (rtac (program_equalityI RS ext) 1);
    3.25  by (simp_tac (simpset() addsimps [drop_set_correct]) 1);
    3.26  by (simp_tac (simpset() 
    3.27 @@ -234,7 +234,7 @@
    3.28  Addsimps [lift_act_inverse];
    3.29  *)
    3.30  
    3.31 -Goal "UNIV <= drop_set i C ==> drop_prog C i (lift_prog i F) = F";
    3.32 +Goal "UNIV <= drop_set i C ==> drop_prog i C (lift_prog i F) = F";
    3.33  by (asm_full_simp_tac
    3.34      (simpset() addsimps [drop_set_correct, drop_prog_correct, 
    3.35  			 lift_prog_correct, lift_export extend_inverse]) 1);
    3.36 @@ -297,14 +297,14 @@
    3.37  
    3.38  (** Safety and drop_prog **)
    3.39  
    3.40 -Goal "(drop_prog C i F : A co B)  =  \
    3.41 +Goal "(drop_prog i C F : A co B)  =  \
    3.42  \     (F : (C Int lift_set i A) co (lift_set i B) & A <= B)";
    3.43  by (simp_tac
    3.44      (simpset() addsimps [drop_prog_correct, 
    3.45  			 lift_set_correct, lift_export project_constrains]) 1);
    3.46  qed "drop_prog_constrains";
    3.47  
    3.48 -Goal "(drop_prog UNIV i F : stable A)  =  (F : stable (lift_set i A))";
    3.49 +Goal "(drop_prog i UNIV F : stable A)  =  (F : stable (lift_set i A))";
    3.50  by (simp_tac (simpset() addsimps [stable_def, drop_prog_constrains]) 1);
    3.51  qed "drop_prog_stable";
    3.52  
    3.53 @@ -312,7 +312,7 @@
    3.54  (*** Diff, needed for localTo ***)
    3.55  
    3.56  Goal "[| Diff C G (lift_act i `` acts) : (lift_set i A) co (lift_set i B) |] \
    3.57 -\     ==> Diff (drop_set i C) (drop_prog C i G) acts : A co B";
    3.58 +\     ==> Diff (drop_set i C) (drop_prog i C G) acts : A co B";
    3.59  by (asm_full_simp_tac
    3.60      (simpset() addsimps [drop_set_correct, drop_prog_correct, 
    3.61  			 lift_set_correct, lift_act_correct, 
    3.62 @@ -321,7 +321,7 @@
    3.63  
    3.64  Goalw [stable_def]
    3.65       "[| Diff C G (lift_act i `` acts) : stable (lift_set i A) |]  \
    3.66 -\     ==> Diff (drop_set i C) (drop_prog C i G) acts : stable A";
    3.67 +\     ==> Diff (drop_set i C) (drop_prog i C G) acts : stable A";
    3.68  by (blast_tac (claset() addIs [Diff_drop_prog_constrains]) 1);
    3.69  qed "Diff_drop_prog_stable";
    3.70  
    3.71 @@ -347,7 +347,7 @@
    3.72  qed "lift_prog_Stable";
    3.73  
    3.74  Goal "[| reachable (lift_prog i F Join G) <= C;    \
    3.75 -\        F Join drop_prog C i G : A Co B |] \
    3.76 +\        F Join drop_prog i C G : A Co B |] \
    3.77  \     ==> lift_prog i F Join G : (lift_set i A) Co (lift_set i B)";
    3.78  by (asm_full_simp_tac
    3.79      (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
    3.80 @@ -356,13 +356,13 @@
    3.81  
    3.82  Goalw [Stable_def]
    3.83       "[| reachable (lift_prog i F Join G) <= C;    \
    3.84 -\        F Join drop_prog C i G : Stable A |]  \
    3.85 +\        F Join drop_prog i C G : Stable A |]  \
    3.86  \     ==> lift_prog i F Join G : Stable (lift_set i A)";
    3.87  by (asm_simp_tac (simpset() addsimps [drop_prog_Constrains_D]) 1);
    3.88  qed "drop_prog_Stable_D";
    3.89  
    3.90  Goal "[| reachable (lift_prog i F Join G) <= C;  \
    3.91 -\        F Join drop_prog C i G : Always A |]   \
    3.92 +\        F Join drop_prog i C G : Always A |]   \
    3.93  \     ==> lift_prog i F Join G : Always (lift_set i A)";
    3.94  by (asm_full_simp_tac
    3.95      (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
    3.96 @@ -371,7 +371,7 @@
    3.97  
    3.98  Goalw [Increasing_def]
    3.99       "[| reachable (lift_prog i F Join G) <= C;  \
   3.100 -\        F Join drop_prog C i G : Increasing func |] \
   3.101 +\        F Join drop_prog i C G : Increasing func |] \
   3.102  \     ==> lift_prog i F Join G : Increasing (func o (sub i))";
   3.103  by Auto_tac;
   3.104  by (stac Collect_eq_lift_set 1);
   3.105 @@ -381,7 +381,7 @@
   3.106  
   3.107  (*UNUSED*)
   3.108  Goal "UNIV <= drop_set i C \
   3.109 -\     ==> drop_prog C i ((lift_prog i F) Join G) = F Join (drop_prog C i G)";
   3.110 +\     ==> drop_prog i C ((lift_prog i F) Join G) = F Join (drop_prog i C G)";
   3.111  by (asm_full_simp_tac
   3.112      (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
   3.113  		     drop_set_correct, lift_export project_extend_Join]) 1);
     4.1 --- a/src/HOL/UNITY/Lift_prog.thy	Mon Oct 18 15:20:21 1999 +0200
     4.2 +++ b/src/HOL/UNITY/Lift_prog.thy	Mon Oct 18 16:16:03 1999 +0200
     4.3 @@ -31,8 +31,8 @@
     4.4  		   lift_act i `` Acts F)"
     4.5  
     4.6    (*Argument C allows weak safety laws to be projected*)
     4.7 -  drop_prog :: "[('a=>'b) set, 'a, ('a=>'b) program] => 'b program"
     4.8 -    "drop_prog C i F ==
     4.9 +  drop_prog :: "['a, ('a=>'b) set, ('a=>'b) program] => 'b program"
    4.10 +    "drop_prog i C F ==
    4.11         mk_program (drop_set i (Init F),
    4.12  		   drop_act i `` Restrict C `` (Acts F))"
    4.13  
     5.1 --- a/src/HOL/UNITY/Project.ML	Mon Oct 18 15:20:21 1999 +0200
     5.2 +++ b/src/HOL/UNITY/Project.ML	Mon Oct 18 16:16:03 1999 +0200
     5.3 @@ -16,24 +16,24 @@
     5.4  by (auto_tac (claset(), simpset() addsimps [project_act_def]));
     5.5  qed "project_act_mono";
     5.6  
     5.7 -Goal "[| D <= C; project C h F : A co B |] ==> project D h F : A co B";
     5.8 +Goal "[| D <= C; project h C F : A co B |] ==> project h D F : A co B";
     5.9  by (auto_tac (claset(), simpset() addsimps [constrains_def]));
    5.10  by (dtac project_act_mono 1);
    5.11  by (Blast_tac 1);
    5.12  qed "project_constrains_mono";
    5.13  
    5.14 -Goal "[| D <= C;  project C h F : stable A |] ==> project D h F : stable A";
    5.15 +Goal "[| D <= C;  project h C F : stable A |] ==> project h D F : stable A";
    5.16  by (asm_full_simp_tac
    5.17      (simpset() addsimps [stable_def, project_constrains_mono]) 1);
    5.18  qed "project_stable_mono";
    5.19  
    5.20 -Goal "F : A co B ==> project C h (extend h F) : A co B";
    5.21 +Goal "F : A co B ==> project h C (extend h F) : A co B";
    5.22  by (auto_tac (claset(), 
    5.23        simpset() addsimps [extend_act_def, project_act_def, constrains_def]));
    5.24  qed "project_extend_constrains_I";
    5.25  
    5.26  Goal "UNIV <= project_set h C \
    5.27 -\     ==> project C h ((extend h F) Join G) = F Join (project C h G)";
    5.28 +\     ==> project h C ((extend h F) Join G) = F Join (project h C G)";
    5.29  by (rtac program_equalityI 1);
    5.30  by (asm_simp_tac (simpset() addsimps [image_Un, image_image_eq_UN, image_UN,
    5.31  			subset_UNIV RS subset_trans RS Restrict_triv]) 2);
    5.32 @@ -41,8 +41,8 @@
    5.33  qed "project_extend_Join";
    5.34  
    5.35  Goal "UNIV <= project_set h C \
    5.36 -\     ==> (extend h F) Join G = extend h H ==> H = F Join (project C h G)";
    5.37 -by (dres_inst_tac [("f", "project C h")] arg_cong 1);
    5.38 +\     ==> (extend h F) Join G = extend h H ==> H = F Join (project h C G)";
    5.39 +by (dres_inst_tac [("f", "project h C")] arg_cong 1);
    5.40  by (asm_full_simp_tac (simpset() addsimps [project_extend_Join]) 1);
    5.41  qed "extend_Join_eq_extend_D";
    5.42  
    5.43 @@ -50,7 +50,7 @@
    5.44  (** Safety **)
    5.45  
    5.46  Goalw [constrains_def]
    5.47 -     "(project C h F : A co B)  =  \
    5.48 +     "(project h C F : A co B)  =  \
    5.49  \     (F : (C Int extend_set h A) co (extend_set h B) & A <= B)";
    5.50  by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un]));
    5.51  by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1);
    5.52 @@ -60,17 +60,17 @@
    5.53  qed "project_constrains";
    5.54  
    5.55  Goalw [stable_def]
    5.56 -     "(project UNIV h F : stable A) = (F : stable (extend_set h A))";
    5.57 +     "(project h UNIV F : stable A) = (F : stable (extend_set h A))";
    5.58  by (simp_tac (simpset() addsimps [project_constrains]) 1);
    5.59  qed "project_stable";
    5.60  
    5.61 -Goal "F : stable (extend_set h A) ==> project C h F : stable A";
    5.62 +Goal "F : stable (extend_set h A) ==> project h C F : stable A";
    5.63  by (dtac (project_stable RS iffD2) 1);
    5.64  by (blast_tac (claset() addIs [project_stable_mono]) 1);
    5.65  qed "project_stable_I";
    5.66  
    5.67  (*used below to prove Join_project_ensures*)
    5.68 -Goal "[| G : stable C;  project C h G : A unless B |] \
    5.69 +Goal "[| G : stable C;  project h C G : A unless B |] \
    5.70  \     ==> G : (C Int extend_set h A) unless (extend_set h B)";
    5.71  by (asm_full_simp_tac
    5.72      (simpset() addsimps [unless_def, project_constrains]) 1);
    5.73 @@ -79,7 +79,7 @@
    5.74  qed_spec_mp "project_unless";
    5.75  
    5.76  (*This form's useful with guarantees reasoning*)
    5.77 -Goal "(F Join project C h G : A co B)  =  \
    5.78 +Goal "(F Join project h C G : A co B)  =  \
    5.79  \       (extend h F Join G : (C Int extend_set h A) co (extend_set h B) &  \
    5.80  \        F : A co B)";
    5.81  by (simp_tac (simpset() addsimps [Join_constrains, project_constrains]) 1);
    5.82 @@ -91,14 +91,14 @@
    5.83    could weaken it to G : (C Int extend_set h A) co C*)
    5.84  Goalw [stable_def]
    5.85       "extend h F Join G : stable C \
    5.86 -\     ==> (F Join project C h G : stable A)  =  \
    5.87 +\     ==> (F Join project h C G : stable A)  =  \
    5.88  \         (extend h F Join G : stable (C Int extend_set h A) &  \
    5.89  \          F : stable A)";
    5.90  by (simp_tac (simpset() addsimps [Join_project_constrains]) 1);
    5.91  by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1);
    5.92  qed "Join_project_stable";
    5.93  
    5.94 -Goal "(F Join project UNIV h G : increasing func)  =  \
    5.95 +Goal "(F Join project h UNIV G : increasing func)  =  \
    5.96  \     (extend h F Join G : increasing (func o f))";
    5.97  by (simp_tac (simpset() addsimps [increasing_def, Join_project_stable]) 1);
    5.98  by (auto_tac (claset(),
    5.99 @@ -108,7 +108,7 @@
   5.100  
   5.101  (*For using project_guarantees in particular cases*)
   5.102  Goal "extend h F Join G : extend_set h A co extend_set h B \
   5.103 -\     ==> F Join project C h G : A co B";
   5.104 +\     ==> F Join project h C G : A co B";
   5.105  by (asm_full_simp_tac
   5.106      (simpset() addsimps [project_constrains, Join_constrains, 
   5.107  			 extend_constrains]) 1);
   5.108 @@ -117,7 +117,7 @@
   5.109  qed "project_constrains_I";
   5.110  
   5.111  (*The UNIV argument is essential*)
   5.112 -Goal "F Join project UNIV h G : A co B \
   5.113 +Goal "F Join project h UNIV G : A co B \
   5.114  \     ==> extend h F Join G : extend_set h A co extend_set h B";
   5.115  by (asm_full_simp_tac
   5.116      (simpset() addsimps [project_constrains, Join_constrains, 
   5.117 @@ -243,8 +243,8 @@
   5.118  qed "project_act_Restrict_Id";
   5.119  
   5.120  Goal
   5.121 -  "Diff(project_set h C)(project C h G)(project_act h `` Restrict C `` acts) \
   5.122 -\  <= project C h (Diff C G acts)";
   5.123 +  "Diff(project_set h C)(project h C G)(project_act h `` Restrict C `` acts) \
   5.124 +\  <= project h C (Diff C G acts)";
   5.125  by (simp_tac 
   5.126      (simpset() addsimps [component_eq_subset, Diff_def,
   5.127  			 Restrict_project_act, project_act_Restrict_Id, 
   5.128 @@ -252,8 +252,8 @@
   5.129  by (Force_tac 1);
   5.130  qed "Diff_project_project_component_project_Diff";
   5.131  
   5.132 -Goal "Diff (project_set h C) (project C h G) acts <= \
   5.133 -\         project C h (Diff C G (extend_act h `` acts))";
   5.134 +Goal "Diff (project_set h C) (project h C G) acts <= \
   5.135 +\         project h C (Diff C G (extend_act h `` acts))";
   5.136  by (rtac component_trans 1);
   5.137  by (rtac Diff_project_project_component_project_Diff 2);
   5.138  by (simp_tac 
   5.139 @@ -264,7 +264,7 @@
   5.140  qed "Diff_project_component_project_Diff";
   5.141  
   5.142  Goal "Diff C G (extend_act h `` acts) : (extend_set h A) co (extend_set h B) \
   5.143 -\     ==> Diff (project_set h C) (project C h G) acts : A co B";
   5.144 +\     ==> Diff (project_set h C) (project h C G) acts : A co B";
   5.145  by (rtac (Diff_project_component_project_Diff RS component_constrains) 1);
   5.146  by (rtac (project_constrains RS iffD2) 1);
   5.147  by (ftac constrains_imp_subset 1);
   5.148 @@ -273,7 +273,7 @@
   5.149  
   5.150  Goalw [stable_def]
   5.151       "Diff C G (extend_act h `` acts) : stable (extend_set h A) \
   5.152 -\     ==> Diff (project_set h C) (project C h G) acts : stable A";
   5.153 +\     ==> Diff (project_set h C) (project h C G) acts : stable A";
   5.154  by (etac Diff_project_constrains 1);
   5.155  qed "Diff_project_stable";
   5.156  
   5.157 @@ -307,7 +307,7 @@
   5.158    simultaneously with other variables, and this action would not be 
   5.159    superseded by anything in (extend h G) *)
   5.160  Goal "H : (v o f) localTo[C] extend h G \
   5.161 -\     ==> project C h H : v localTo[project_set h C] G";
   5.162 +\     ==> project h C H : v localTo[project_set h C] G";
   5.163  by (asm_full_simp_tac 
   5.164      (simpset() addsimps [LOCALTO_def, 
   5.165  			 project_extend_Join RS sym,
   5.166 @@ -316,14 +316,14 @@
   5.167  qed "project_localTo_lemma";
   5.168  
   5.169  Goal "extend h F Join G : (v o f) localTo[C] extend h H \
   5.170 -\     ==> F Join project C h G : v localTo[project_set h C] H";
   5.171 +\     ==> F Join project h C G : v localTo[project_set h C] H";
   5.172  by (asm_full_simp_tac 
   5.173      (simpset() addsimps [Join_localTo, localTo_project_set_I,
   5.174  			 project_localTo_lemma]) 1);
   5.175  qed "gen_project_localTo_I";
   5.176  
   5.177  Goal "extend h F Join G : (v o f) localTo[UNIV] extend h H \
   5.178 -\     ==> F Join project UNIV h G : v localTo[UNIV] H";
   5.179 +\     ==> F Join project h UNIV G : v localTo[UNIV] H";
   5.180  bd gen_project_localTo_I 1;
   5.181  by (Asm_full_simp_tac 1);
   5.182  qed "project_localTo_I";
   5.183 @@ -339,7 +339,7 @@
   5.184  
   5.185  Goal "[| reachable (extend h F Join G) <= C;  \
   5.186  \        z : reachable (extend h F Join G) |] \
   5.187 -\     ==> f z : reachable (F Join project C h G)";
   5.188 +\     ==> f z : reachable (F Join project h C G)";
   5.189  by (etac reachable.induct 1);
   5.190  by (force_tac (claset() addIs [reachable.Init, project_set_I],
   5.191  	       simpset()) 1);
   5.192 @@ -355,7 +355,7 @@
   5.193    preconditions (localTo) and WEAK postconditions.*)
   5.194  Goalw [Constrains_def]
   5.195       "[| reachable (extend h F Join G) <= C;    \
   5.196 -\        F Join project C h G : A Co B |] \
   5.197 +\        F Join project h C G : A Co B |] \
   5.198  \     ==> extend h F Join G : (extend_set h A) Co (extend_set h B)";
   5.199  by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1);
   5.200  by (Clarify_tac 1);
   5.201 @@ -365,14 +365,14 @@
   5.202  
   5.203  Goalw [Stable_def]
   5.204       "[| reachable (extend h F Join G) <= C;  \
   5.205 -\        F Join project C h G : Stable A |]   \
   5.206 +\        F Join project h C G : Stable A |]   \
   5.207  \     ==> extend h F Join G : Stable (extend_set h A)";
   5.208  by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1);
   5.209  qed "project_Stable_D";
   5.210  
   5.211  Goalw [Always_def]
   5.212       "[| reachable (extend h F Join G) <= C;  \
   5.213 -\        F Join project C h G : Always A |]   \
   5.214 +\        F Join project h C G : Always A |]   \
   5.215  \     ==> extend h F Join G : Always (extend_set h A)";
   5.216  by (force_tac (claset() addIs [reachable.Init, project_set_I],
   5.217                 simpset() addsimps [project_Stable_D]) 1);
   5.218 @@ -380,7 +380,7 @@
   5.219  
   5.220  Goalw [Increasing_def]
   5.221       "[| reachable (extend h F Join G) <= C;  \
   5.222 -\        F Join project C h G : Increasing func |] \
   5.223 +\        F Join project h C G : Increasing func |] \
   5.224  \     ==> extend h F Join G : Increasing (func o f)";
   5.225  by Auto_tac;
   5.226  by (stac Collect_eq_extend_set 1);
   5.227 @@ -391,7 +391,7 @@
   5.228  (** Converse results for weak safety: benefits of the argument C *)
   5.229  
   5.230  Goal "[| C <= reachable(extend h F Join G);   \
   5.231 -\        x : reachable (F Join project C h G) |] \
   5.232 +\        x : reachable (F Join project h C G) |] \
   5.233  \     ==> EX y. h(x,y) : reachable (extend h F Join G)";
   5.234  by (etac reachable.induct 1);
   5.235  by (ALLGOALS Asm_full_simp_tac);
   5.236 @@ -405,7 +405,7 @@
   5.237  
   5.238  
   5.239  Goal "project_set h (reachable (extend h F Join G)) = \
   5.240 -\     reachable (F Join project (reachable (extend h F Join G)) h G)";
   5.241 +\     reachable (F Join project h (reachable (extend h F Join G)) G)";
   5.242  by (auto_tac (claset() addDs [subset_refl RS reachable_imp_reachable_project,
   5.243  			      subset_refl RS reachable_project_imp_reachable], 
   5.244  	      simpset() addsimps [project_set_def]));
   5.245 @@ -415,7 +415,7 @@
   5.246  Goalw [Constrains_def]
   5.247       "[| C <= reachable (extend h F Join G);  \
   5.248  \        extend h F Join G : (extend_set h A) Co (extend_set h B) |] \
   5.249 -\     ==> F Join project C h G : A Co B";
   5.250 +\     ==> F Join project h C G : A Co B";
   5.251  by (full_simp_tac (simpset() addsimps [Join_project_constrains, 
   5.252  				       extend_set_Int_distrib]) 1);
   5.253  by (rtac conjI 1);
   5.254 @@ -433,14 +433,14 @@
   5.255  Goalw [Stable_def]
   5.256       "[| C <= reachable (extend h F Join G);  \
   5.257  \        extend h F Join G : Stable (extend_set h A) |] \
   5.258 -\     ==> F Join project C h G : Stable A";
   5.259 +\     ==> F Join project h C G : Stable A";
   5.260  by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1);
   5.261  qed "project_Stable_I";
   5.262  
   5.263  Goalw [Always_def]
   5.264       "[| C <= reachable (extend h F Join G);  \
   5.265  \        extend h F Join G : Always (extend_set h A) |]   \
   5.266 -\     ==> F Join project C h G : Always A";
   5.267 +\     ==> F Join project h C G : Always A";
   5.268  by (auto_tac (claset(), simpset() addsimps [project_Stable_I]));
   5.269  by (rewrite_goals_tac [project_set_def, extend_set_def]);
   5.270  by (Blast_tac 1);
   5.271 @@ -449,32 +449,32 @@
   5.272  Goalw [Increasing_def]
   5.273       "[| C <= reachable (extend h F Join G);  \
   5.274  \        extend h F Join G : Increasing (func o f) |] \
   5.275 -\     ==> F Join project C h G : Increasing func";
   5.276 +\     ==> F Join project h C G : Increasing func";
   5.277  by Auto_tac;
   5.278  by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym,
   5.279  				      project_Stable_I]) 1); 
   5.280  qed "project_Increasing_I";
   5.281  
   5.282 -Goal "(F Join project (reachable (extend h F Join G)) h G : A Co B)  =  \
   5.283 +Goal "(F Join project h (reachable (extend h F Join G)) G : A Co B)  =  \
   5.284  \     (extend h F Join G : (extend_set h A) Co (extend_set h B))";
   5.285  by (blast_tac (claset() addIs [project_Constrains_I, project_Constrains_D]) 1);
   5.286  qed "project_Constrains";
   5.287  
   5.288  Goalw [Stable_def]
   5.289 -     "(F Join project (reachable (extend h F Join G)) h G : Stable A)  =  \
   5.290 +     "(F Join project h (reachable (extend h F Join G)) G : Stable A)  =  \
   5.291  \     (extend h F Join G : Stable (extend_set h A))";
   5.292  by (rtac project_Constrains 1);
   5.293  qed "project_Stable";
   5.294  
   5.295  Goal
   5.296 -   "(F Join project (reachable (extend h F Join G)) h G : Increasing func)  = \
   5.297 +   "(F Join project h (reachable (extend h F Join G)) G : Increasing func)  = \
   5.298  \   (extend h F Join G : Increasing (func o f))";
   5.299  by (asm_simp_tac (simpset() addsimps [Increasing_def, project_Stable,
   5.300  				      Collect_eq_extend_set RS sym]) 1);
   5.301  qed "project_Increasing";
   5.302  
   5.303  Goal "extend h F Join G : (v o f) LocalTo extend h H \
   5.304 -\     ==> F Join project (reachable (extend h F Join G)) h G : v LocalTo H";
   5.305 +\     ==> F Join project h (reachable (extend h F Join G)) G : v LocalTo H";
   5.306  by (asm_full_simp_tac 
   5.307      (simpset() addsimps [LocalTo_def, project_set_reachable_extend_eq RS sym,
   5.308  			 gen_project_localTo_I]) 1);
   5.309 @@ -542,7 +542,7 @@
   5.310  
   5.311  (** Progress includes safety in the definition of ensures **)
   5.312  
   5.313 -(*** Progress for (project C h F) ***)
   5.314 +(*** Progress for (project h C F) ***)
   5.315  
   5.316  (** transient **)
   5.317  
   5.318 @@ -552,7 +552,7 @@
   5.319       "[| ALL act: Acts F. act ^^ extend_set h A <= - extend_set h A --> \
   5.320  \                      Domain act <= C;    \
   5.321  \        F : transient (extend_set h A) |] \
   5.322 -\     ==> project C h F : transient A";
   5.323 +\     ==> project h C F : transient A";
   5.324  by (auto_tac (claset() delrules [ballE],
   5.325                simpset() addsimps [Domain_project_act, Int_absorb2]));
   5.326  by (REPEAT (ball_tac 1));
   5.327 @@ -567,7 +567,7 @@
   5.328    Converse of the above...it requires a strong assumption about actions
   5.329    being enabled for all possible values of the new variables.*)
   5.330  Goalw [transient_def]
   5.331 -     "[| project C h F : transient A;  \
   5.332 +     "[| project h C F : transient A;  \
   5.333  \        ALL act: Acts F. project_act h (Restrict C act) ^^ A <= - A --> \
   5.334  \                         Domain act <= C \
   5.335  \             & extend_set h (project_set h (Domain act)) <= Domain act |]  \
   5.336 @@ -594,7 +594,7 @@
   5.337  (*For simplicity, the complicated condition on C is eliminated
   5.338    NOT SURE THIS IS GOOD FOR ANYTHING: CAN'T PROVE LEADSTO THEOREM*)
   5.339  Goal "F : (extend_set h A) ensures (extend_set h B) \
   5.340 -\     ==> project UNIV h F : A ensures B";
   5.341 +\     ==> project h UNIV F : A ensures B";
   5.342  by (asm_full_simp_tac
   5.343      (simpset() addsimps [ensures_def, project_constrains, 
   5.344  			 transient_extend_set_imp_project_transient,
   5.345 @@ -604,9 +604,9 @@
   5.346  qed "ensures_extend_set_imp_project_ensures";
   5.347  
   5.348  (*A strong condition: F can do anything that project G can.*)
   5.349 -Goal "[| ALL D. project C h G : transient D --> F : transient D;  \
   5.350 +Goal "[| ALL D. project h C G : transient D --> F : transient D;  \
   5.351  \        extend h F Join G : stable C;  \
   5.352 -\        F Join project C h G : A ensures B |] \
   5.353 +\        F Join project h C G : A ensures B |] \
   5.354  \     ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
   5.355  by (case_tac "A <= B" 1);
   5.356  by (blast_tac (claset() addIs [subset_imp_ensures] addDs [extend_set_mono]) 1);
   5.357 @@ -620,9 +620,9 @@
   5.358  		       simpset()) 1));
   5.359  qed_spec_mp "Join_project_ensures";
   5.360  
   5.361 -Goal "[| ALL D. project C h G : transient D --> F : transient D;  \
   5.362 +Goal "[| ALL D. project h C G : transient D --> F : transient D;  \
   5.363  \        extend h F Join G : stable C;  \
   5.364 -\        F Join project C h G : A leadsTo B |] \
   5.365 +\        F Join project h C G : A leadsTo B |] \
   5.366  \     ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
   5.367  by (etac leadsTo_induct 1);
   5.368  by (asm_simp_tac (simpset() delsimps UN_simps
   5.369 @@ -633,8 +633,8 @@
   5.370  qed "project_leadsTo_lemma";
   5.371  
   5.372  (*Instance of the previous theorem for STRONG progress*)
   5.373 -Goal "[| ALL D. project UNIV h G : transient D --> F : transient D;  \
   5.374 -\        F Join project UNIV h G : A leadsTo B |] \
   5.375 +Goal "[| ALL D. project h UNIV G : transient D --> F : transient D;  \
   5.376 +\        F Join project h UNIV G : A leadsTo B |] \
   5.377  \     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
   5.378  by (dtac project_leadsTo_lemma 1);
   5.379  by Auto_tac;
   5.380 @@ -642,9 +642,9 @@
   5.381  
   5.382  (** Towards the analogous theorem for WEAK progress*)
   5.383  
   5.384 -Goal "[| ALL D. project C h G : transient D --> F : transient D;  \
   5.385 +Goal "[| ALL D. project h C G : transient D --> F : transient D;  \
   5.386  \        extend h F Join G : stable C;  \
   5.387 -\        F Join project C h G : (project_set h C Int A) leadsTo B |] \
   5.388 +\        F Join project h C G : (project_set h C Int A) leadsTo B |] \
   5.389  \     ==> extend h F Join G : C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)";
   5.390  by (etac leadsTo_induct 1);
   5.391  by (asm_simp_tac (simpset() delsimps UN_simps
   5.392 @@ -654,17 +654,17 @@
   5.393  by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
   5.394  val lemma = result();
   5.395  
   5.396 -Goal "[| ALL D. project C h G : transient D --> F : transient D;  \
   5.397 +Goal "[| ALL D. project h C G : transient D --> F : transient D;  \
   5.398  \        extend h F Join G : stable C;  \
   5.399 -\        F Join project C h G : (project_set h C Int A) leadsTo B |] \
   5.400 +\        F Join project h C G : (project_set h C Int A) leadsTo B |] \
   5.401  \     ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
   5.402  by (rtac (lemma RS leadsTo_weaken) 1);
   5.403  by (auto_tac (claset() addIs [project_set_I], simpset()));
   5.404  val lemma2 = result();
   5.405  
   5.406  Goal "[| C = (reachable (extend h F Join G)); \
   5.407 -\        ALL D. project C h G : transient D --> F : transient D;  \
   5.408 -\        F Join project C h G : A LeadsTo B |] \
   5.409 +\        ALL D. project h C G : transient D --> F : transient D;  \
   5.410 +\        F Join project h C G : A LeadsTo B |] \
   5.411  \     ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
   5.412  by (asm_full_simp_tac 
   5.413      (simpset() addsimps [LeadsTo_def, lemma2, stable_reachable, 
   5.414 @@ -776,7 +776,7 @@
   5.415  (** Guarantees with a leadsTo postcondition **)
   5.416  
   5.417  (*Bridges the gap between the "old" and "new" condition of the leadsTo rules*)
   5.418 -Goal "[| ALL x. project C h G ~: transient {x}; project C h G: transient D |] \
   5.419 +Goal "[| ALL x. project h C G ~: transient {x}; project h C G: transient D |] \
   5.420  \     ==> F : transient D";
   5.421  by (case_tac "D={}" 1);
   5.422  by (auto_tac (claset() addIs [transient_strengthen], simpset()));
   5.423 @@ -784,7 +784,7 @@
   5.424  
   5.425  
   5.426  (*Previously tried to prove
   5.427 -[| G : f localTo extend h F; project C h G : transient D |] ==> F : transient D
   5.428 +[| G : f localTo extend h F; project h C G : transient D |] ==> F : transient D
   5.429  but it can fail if C removes some parts of an action of G.*)
   5.430  
   5.431  
   5.432 @@ -796,7 +796,7 @@
   5.433  qed "localTo_imp_stable";
   5.434  
   5.435  Goal "[| G : f localTo[UNIV] extend h F; \
   5.436 -\        Disjoint UNIV (extend h F) G |] ==> project C h G : stable {x}";
   5.437 +\        Disjoint UNIV (extend h F) G |] ==> project h C G : stable {x}";
   5.438  by (asm_full_simp_tac
   5.439      (simpset() addsimps [localTo_imp_stable,
   5.440  			 extend_set_sing, project_stable_I]) 1);
   5.441 @@ -808,7 +808,7 @@
   5.442  				  stable_def, constrains_def]));
   5.443  qed "stable_sing_imp_not_transient";
   5.444  
   5.445 -Goal "[| F Join project UNIV h G : A leadsTo B;    \
   5.446 +Goal "[| F Join project h UNIV G : A leadsTo B;    \
   5.447  \        G : f localTo[UNIV] extend h F; \
   5.448  \        Disjoint UNIV (extend h F) G |]  \
   5.449  \     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
   5.450 @@ -820,7 +820,7 @@
   5.451  				  stable_sing_imp_not_transient]));
   5.452  qed "project_leadsTo_D";
   5.453  
   5.454 -Goal "[| F Join project (reachable (extend h F Join G)) h G : A LeadsTo B; \
   5.455 +Goal "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B; \
   5.456  \         G : f localTo[UNIV] extend h F; \
   5.457  \         Disjoint UNIV (extend h F) G |]  \
   5.458  \      ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
     6.1 --- a/src/HOL/UNITY/Project.thy	Mon Oct 18 15:20:21 1999 +0200
     6.2 +++ b/src/HOL/UNITY/Project.thy	Mon Oct 18 16:16:03 1999 +0200
     6.3 @@ -14,12 +14,12 @@
     6.4    projecting :: "['c program => 'c set, 'a*'b => 'c, 
     6.5  		  'a program, 'c program set, 'a program set] => bool"
     6.6    "projecting C h F X' X ==
     6.7 -     ALL G. extend h F Join G : X' --> F Join project (C G) h G : X"
     6.8 +     ALL G. extend h F Join G : X' --> F Join project h (C G) G : X"
     6.9  
    6.10    extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
    6.11  		 'c program set, 'c program set, 'a program set] => bool"
    6.12    "extending C h F X' Y' Y ==
    6.13 -     ALL G. F Join project (C G) h G : Y & extend h F Join G : X' &
    6.14 +     ALL G. F Join project h (C G) G : Y & extend h F Join G : X' &
    6.15              Disjoint UNIV (extend h F) G
    6.16              --> extend h F Join G : Y'"
    6.17