changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
authorpaulson
Tue Aug 31 15:56:56 1999 +0200 (1999-08-31)
changeset 7399cf780c2bcccf
parent 7398 c68ecbf05eb6
child 7400 fbd5582761e6
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
src/HOL/UNITY/Alloc.ML
src/HOL/UNITY/Client.thy
src/HOL/UNITY/Comp.ML
src/HOL/UNITY/Comp.thy
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/PPROD.ML
     1.1 --- a/src/HOL/UNITY/Alloc.ML	Mon Aug 30 23:19:13 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Alloc.ML	Tue Aug 31 15:56:56 1999 +0200
     1.3 @@ -6,6 +6,18 @@
     1.4  Specification of Chandy and Charpentier's Allocator
     1.5  *)
     1.6  
     1.7 +
     1.8 +Goal "~ f #2 ==> ~ (!t::nat. (#0 <= t & t <= #10) --> f t)";
     1.9 +
    1.10 +(*Useful examples:  singletonI RS subst_elem,  subst_elem RSN (2,IntI) *)
    1.11 +Goal "[| b:A;  a=b |] ==> a:A";
    1.12 +by (etac ssubst 1);
    1.13 +by (assume_tac 1);
    1.14 +qed "subst_elem";
    1.15 +
    1.16 +
    1.17 +
    1.18 +
    1.19  (*Generalized version allowing different clients*)
    1.20  Goal "[| Alloc : alloc_spec;  \
    1.21  \        Client : (lessThan Nclients) funcset client_spec;  \
    1.22 @@ -32,6 +44,20 @@
    1.23  
    1.24  AddIffs [inj_sysOfAlloc, surj_sysOfAlloc];
    1.25  
    1.26 +val bij_sysOfAlloc = [inj_sysOfAlloc, surj_sysOfAlloc] MRS bijI;
    1.27 +
    1.28 +(*MUST BE AUTOMATED: even the statement of such results*)
    1.29 +Goal "!!s. inv sysOfAlloc s = \
    1.30 +\            ((| allocGiv = allocGiv s,   \
    1.31 +\                allocAsk = allocAsk s,   \
    1.32 +\                allocRel = allocRel s|), \
    1.33 +\             client s)";
    1.34 +by (rtac (inj_sysOfAlloc RS inv_f_eq) 1);
    1.35 +by (auto_tac (claset() addSWrapper record_split_wrapper, 
    1.36 +	      simpset() addsimps [sysOfAlloc_def]));
    1.37 +qed "inv_sysOfAlloc_eq";
    1.38 +
    1.39 +
    1.40  (**SHOULD NOT BE NECESSARY: The various injections into the system
    1.41     state need to be treated symmetrically or done automatically*)
    1.42  Goalw [sysOfClient_def] "inj sysOfClient";
    1.43 @@ -49,6 +75,7 @@
    1.44  
    1.45  AddIffs [inj_sysOfClient, surj_sysOfClient];
    1.46  
    1.47 +val bij_sysOfClient = [inj_sysOfClient, surj_sysOfClient] MRS bijI;
    1.48  
    1.49  (*MUST BE AUTOMATED: even the statement of such results*)
    1.50  Goal "!!s. inv sysOfClient s = \
    1.51 @@ -57,8 +84,8 @@
    1.52  \                allocAsk = allocAsk s, \
    1.53  \                allocRel = allocRel s|) )";
    1.54  by (rtac (inj_sysOfClient RS inv_f_eq) 1);
    1.55 -by (rewrite_goals_tac [sysOfAlloc_def, sysOfClient_def]);
    1.56 -by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
    1.57 +by (auto_tac (claset() addSWrapper record_split_wrapper, 
    1.58 +	      simpset() addsimps [sysOfAlloc_def, sysOfClient_def]));
    1.59  qed "inv_sysOfClient_eq";
    1.60  
    1.61  
    1.62 @@ -128,20 +155,21 @@
    1.63  
    1.64  (*Not sure what to say about the other components because they involve
    1.65    extend*)
    1.66 -Goalw [System_def] "Network component System";
    1.67 +Goalw [System_def] "Network <= System";
    1.68  by (blast_tac (claset() addIs [componentI]) 1);
    1.69  qed "Network_component_System";
    1.70  
    1.71 -AddIffs [Network_component_System];
    1.72 -
    1.73 +Goalw [System_def] "(extend sysOfAlloc Alloc) <= System";
    1.74 +by (blast_tac (claset() addIs [componentI]) 1);
    1.75 +qed "Alloc_component_System";
    1.76  
    1.77 -val project_guarantees' =
    1.78 -  [surj_sysOfClient, inj_sysOfClient] MRS export project_guarantees;
    1.79 +AddIffs [Network_component_System, Alloc_component_System];
    1.80 +
    1.81  
    1.82  (* F : UNIV guarantees Increasing func
    1.83     ==> extend sysOfClient F : UNIV guarantees Increasing (func o client) *)
    1.84 -val extend_guar_Increasing' =
    1.85 -  [surj_sysOfClient, inj_sysOfClient] MRS export extend_guar_Increasing
    1.86 +val extend_Client_guar_Increasing =
    1.87 +  bij_sysOfClient RS export extend_guar_Increasing
    1.88    |> simplify (simpset() addsimps [inv_sysOfClient_eq]);
    1.89  
    1.90  
    1.91 @@ -154,7 +182,7 @@
    1.92  	  MRS guaranteesD) 1);
    1.93  by (asm_simp_tac 
    1.94      (simpset() addsimps [guarantees_PLam_I, 
    1.95 -			 extend_guar_Increasing' RS guaranteesD,
    1.96 +			 extend_Client_guar_Increasing RS guaranteesD,
    1.97  			 lift_prog_guar_Increasing]) 1);
    1.98  qed "System_Increasing_rel";
    1.99  
   1.100 @@ -169,13 +197,81 @@
   1.101  			       System_Increasing_rel, Network]) 1);
   1.102  qed "System_Increasing_allocRel";
   1.103  
   1.104 -Goal "i < Nclients \
   1.105 -\ ==> System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
   1.106 -\                  <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
   1.107 -fr component_guaranteesD;
   1.108 +
   1.109 +(*NEED TO PROVE something like this (maybe without premise)*)
   1.110 +Goal "i < Nclients ==> System : (sub i o allocRel) localTo Network";
   1.111  
   1.112 -val extend_guar_Increasing'' =
   1.113 -  [surj_sysOfAlloc, inj_sysOfAlloc] MRS export extend_guar_Increasing
   1.114 +fun alloc_export th = bij_sysOfAlloc RS export th;
   1.115 +
   1.116 +val extend_Alloc_guar_Increasing =
   1.117 +  alloc_export extend_guar_Increasing
   1.118    |> simplify (simpset() addsimps [inv_sysOfAlloc_eq]);
   1.119  
   1.120 +Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
   1.121 +\                  <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
   1.122 +by (res_inst_tac 
   1.123 +    [("X", "(INT i : lessThan Nclients. (sub i o allocRel) localTo Network \
   1.124 +\                                       Int Increasing (sub i o allocRel))")] 
   1.125 +    component_guaranteesD 1);;
   1.126 +br Alloc_component_System 3;
   1.127 +br project_guarantees 1;
   1.128 +br Alloc_Safety 1;
   1.129 +by (dtac (alloc_export (project_extend_Join RSN (2, subst_elem RS project_Always_D))) 2 
   1.130 +     THEN
   1.131 +     full_simp_tac
   1.132 +     (simpset() addsimps [inv_sysOfAlloc_eq,
   1.133 +			  alloc_export Collect_eq_extend_set RS sym]) 2);
   1.134 +auto();
   1.135 +by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 3);
   1.136 +
   1.137 +bd bspec 1;
   1.138 +by (Blast_tac 1);
   1.139 +
   1.140 +
   1.141 +xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
   1.142 +
   1.143 +       [| i < Nclients;
   1.144 +          extend sysOfAlloc Alloc Join G
   1.145 +          : (sub i o allocRel) localTo Network &
   1.146 +          extend sysOfAlloc Alloc Join G : Increasing (sub i o allocRel) |]
   1.147 +       ==> Alloc Join project sysOfAlloc G : Increasing (sub i o allocRel)
   1.148 +
   1.149 +
   1.150 +       [| i < Nclients;
   1.151 +          H : (sub i o allocRel) localTo Network &
   1.152 +          H : Increasing (sub i o allocRel) |]
   1.153 +       ==> project sysOfAlloc H : Increasing (sub i o allocRel)
   1.154 +
   1.155 +Open_locale"Extend";
   1.156 +
   1.157 +Goal "(H : (func o f) localTo G) ==> (project h H : func localTo (project h G))";
   1.158 +by (asm_full_simp_tac 
   1.159 +    (simpset() addsimps [localTo_def, 
   1.160 +			 project_extend_Join RS sym,
   1.161 +			 Diff_project_stable,
   1.162 +			 Collect_eq_extend_set RS sym]) 1);
   1.163 +auto();
   1.164 +br Diff_project_stable 1;
   1.165 +PROBABLY FALSE;
   1.166 +
   1.167 +by (Clarify_tac 1);
   1.168 +by (dres_inst_tac [("x","z")] spec 1);
   1.169 +
   1.170 +br (alloc_export project_Always_D) 2;
   1.171 +
   1.172 +by (rtac (alloc_export extend_Always RS iffD2) 2);
   1.173 +
   1.174 +xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
   1.175 +
   1.176 +br guaranteesI 1;
   1.177 +
   1.178 +by (res_inst_tac 
   1.179 +    [("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")] 
   1.180 +    component_guaranteesD 1);;
   1.181 +
   1.182 +
   1.183  by (rtac (Alloc_Safety RS component_guaranteesD) 1);
   1.184 +
   1.185 +
   1.186 +br (alloc_export guarantees_imp_extend_guarantees RS guarantees_weaken) 1;
   1.187 +br Alloc_Safety 1;
     2.1 --- a/src/HOL/UNITY/Client.thy	Mon Aug 30 23:19:13 1999 +0200
     2.2 +++ b/src/HOL/UNITY/Client.thy	Tue Aug 31 15:56:56 1999 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  Distributed Resource Management System: the Client
     2.5  *)
     2.6  
     2.7 -Client = Comp + 
     2.8 +Client = Guar + 
     2.9  
    2.10  consts
    2.11    Max :: nat       (*Maximum number of tokens*)
     3.1 --- a/src/HOL/UNITY/Comp.ML	Mon Aug 30 23:19:13 1999 +0200
     3.2 +++ b/src/HOL/UNITY/Comp.ML	Tue Aug 31 15:56:56 1999 +0200
     3.3 @@ -11,7 +11,7 @@
     3.4  (*** component ***)
     3.5  
     3.6  Goalw [component_def]
     3.7 -     "H component F | H component G ==> H component (F Join G)";
     3.8 +     "H <= F | H <= G ==> H <= (F Join G)";
     3.9  by Auto_tac;
    3.10  by (res_inst_tac [("x", "G Join Ga")] exI 1);
    3.11  by (res_inst_tac [("x", "G Join F")] exI 2);
    3.12 @@ -19,349 +19,61 @@
    3.13  qed "componentI";
    3.14  
    3.15  Goalw [component_def]
    3.16 -     "(F component G) = (Init G <= Init F & Acts F <= Acts G)";
    3.17 +     "(F <= G) = (Init G <= Init F & Acts F <= Acts G)";
    3.18  by (force_tac (claset() addSIs [exI, program_equalityI], 
    3.19  	       simpset() addsimps [Acts_Join]) 1);
    3.20  qed "component_eq_subset";
    3.21  
    3.22 -Goalw [component_def] "SKIP component F";
    3.23 +Goalw [component_def] "SKIP <= F";
    3.24  by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1);
    3.25  qed "component_SKIP";
    3.26  
    3.27 -Goalw [component_def] "F component F";
    3.28 +Goalw [component_def] "F <= (F :: 'a program)";
    3.29  by (blast_tac (claset() addIs [Join_SKIP_right]) 1);
    3.30  qed "component_refl";
    3.31  
    3.32  AddIffs [component_SKIP, component_refl];
    3.33  
    3.34 -Goal "F component SKIP ==> F = SKIP";
    3.35 +Goal "F <= SKIP ==> F = SKIP";
    3.36  by (auto_tac (claset() addSIs [program_equalityI],
    3.37  	      simpset() addsimps [component_eq_subset]));
    3.38  qed "SKIP_minimal";
    3.39  
    3.40 -Goalw [component_def] "F component (F Join G)";
    3.41 +Goalw [component_def] "F <= (F Join G)";
    3.42  by (Blast_tac 1);
    3.43  qed "component_Join1";
    3.44  
    3.45 -Goalw [component_def] "G component (F Join G)";
    3.46 +Goalw [component_def] "G <= (F Join G)";
    3.47  by (simp_tac (simpset() addsimps [Join_commute]) 1);
    3.48  by (Blast_tac 1);
    3.49  qed "component_Join2";
    3.50  
    3.51 -Goalw [component_def] "i : I ==> (F i) component (JN i:I. (F i))";
    3.52 +Goalw [component_def] "i : I ==> (F i) <= (JN i:I. (F i))";
    3.53  by (blast_tac (claset() addIs [JN_absorb]) 1);
    3.54  qed "component_JN";
    3.55  
    3.56 -Goalw [component_def] "[| F component G; G component H |] ==> F component H";
    3.57 +Goalw [component_def] "[| F <= G; G <= H |] ==> F <= (H :: 'a program)";
    3.58  by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
    3.59  qed "component_trans";
    3.60  
    3.61 -Goal "[| F component G; G component F |] ==> F=G";
    3.62 +Goal "[| F <= G; G <= F |] ==> F = (G :: 'a program)";
    3.63  by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
    3.64  by (blast_tac (claset() addSIs [program_equalityI]) 1);
    3.65  qed "component_antisym";
    3.66  
    3.67  Goalw [component_def]
    3.68 -      "F component H = (EX G. F Join G = H & Disjoint F G)";
    3.69 +      "F <= H = (EX G. F Join G = H & Disjoint F G)";
    3.70  by (blast_tac (claset() addSIs [Diff_Disjoint, Join_Diff2]) 1);
    3.71  qed "component_eq";
    3.72  
    3.73 -Goal "((F Join G) component H) = (F component H & G component H)";
    3.74 +Goal "((F Join G) <= H) = (F <= H & G <= H)";
    3.75  by (simp_tac (simpset() addsimps [component_eq_subset, Acts_Join]) 1);
    3.76  by (Blast_tac 1);
    3.77  qed "Join_component_iff";
    3.78  
    3.79 -Goal "[| F component G; G : A co B |] ==> F : A co B";
    3.80 +Goal "[| F <= G; G : A co B |] ==> F : A co B";
    3.81  by (auto_tac (claset(), 
    3.82  	      simpset() addsimps [constrains_def, component_eq_subset]));
    3.83  qed "component_constrains";
    3.84  
    3.85 -(*** existential properties ***)
    3.86 -
    3.87 -Goalw [ex_prop_def]
    3.88 -     "[| ex_prop X; finite GG |] ==> GG Int X ~= {} --> (JN G:GG. G) : X";
    3.89 -by (etac finite_induct 1);
    3.90 -by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
    3.91 -qed_spec_mp "ex1";
    3.92 -
    3.93 -Goalw [ex_prop_def]
    3.94 -     "ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X ==> ex_prop X";
    3.95 -by (Clarify_tac 1);
    3.96 -by (dres_inst_tac [("x", "{F,G}")] spec 1);
    3.97 -by Auto_tac;
    3.98 -qed "ex2";
    3.99 -
   3.100 -(*Chandy & Sanders take this as a definition*)
   3.101 -Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X)";
   3.102 -by (blast_tac (claset() addIs [ex1,ex2]) 1);
   3.103 -qed "ex_prop_finite";
   3.104 -
   3.105 -(*Their "equivalent definition" given at the end of section 3*)
   3.106 -Goal "ex_prop X = (ALL G. G:X = (ALL H. G component H --> H: X))";
   3.107 -by Auto_tac;
   3.108 -by (rewrite_goals_tac [ex_prop_def, component_def]);
   3.109 -by (Blast_tac 1);
   3.110 -by Safe_tac;
   3.111 -by (stac Join_commute 2);
   3.112 -by (ALLGOALS Blast_tac);
   3.113 -qed "ex_prop_equiv";
   3.114 -
   3.115 -
   3.116 -(*** universal properties ***)
   3.117 -
   3.118 -Goalw [uv_prop_def]
   3.119 -     "[| uv_prop X; finite GG |] ==> GG <= X --> (JN G:GG. G) : X";
   3.120 -by (etac finite_induct 1);
   3.121 -by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
   3.122 -qed_spec_mp "uv1";
   3.123 -
   3.124 -Goalw [uv_prop_def]
   3.125 -     "ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X  ==> uv_prop X";
   3.126 -by (rtac conjI 1);
   3.127 -by (Clarify_tac 2);
   3.128 -by (dres_inst_tac [("x", "{F,G}")] spec 2);
   3.129 -by (dres_inst_tac [("x", "{}")] spec 1);
   3.130 -by Auto_tac;
   3.131 -qed "uv2";
   3.132 -
   3.133 -(*Chandy & Sanders take this as a definition*)
   3.134 -Goal "uv_prop X = (ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X)";
   3.135 -by (blast_tac (claset() addIs [uv1,uv2]) 1);
   3.136 -qed "uv_prop_finite";
   3.137 -
   3.138 -
   3.139 -(*** guarantees ***)
   3.140 -
   3.141 -val prems = Goal
   3.142 -     "(!!G. [| F Join G : X;  Disjoint F G |] ==> F Join G : Y) \
   3.143 -\     ==> F : X guarantees Y";
   3.144 -by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1);
   3.145 -by (blast_tac (claset() addIs prems) 1);
   3.146 -qed "guaranteesI";
   3.147 -
   3.148 -Goalw [guar_def, component_def]
   3.149 -     "[| F : X guarantees Y;  F Join G : X |] ==> F Join G : Y";
   3.150 -by (Blast_tac 1);
   3.151 -qed "guaranteesD";
   3.152 -
   3.153 -(*This version of guaranteesD matches more easily in the conclusion*)
   3.154 -Goalw [guar_def]
   3.155 -     "[| F : X guarantees Y;  H : X;  F component H |] ==> H : Y";
   3.156 -by (Blast_tac 1);
   3.157 -qed "component_guaranteesD";
   3.158 -
   3.159 -(*This equation is more intuitive than the official definition*)
   3.160 -Goal "(F : X guarantees Y) = \
   3.161 -\     (ALL G. F Join G : X & Disjoint F G --> F Join G : Y)";
   3.162 -by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1);
   3.163 -by (Blast_tac 1);
   3.164 -qed "guarantees_eq";
   3.165 -
   3.166 -Goalw [guar_def]
   3.167 -     "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'";
   3.168 -by (Blast_tac 1);
   3.169 -qed "guarantees_weaken";
   3.170 -
   3.171 -Goalw [guar_def]
   3.172 -     "[| F: X guarantees Y; F component F' |] ==> F': X guarantees Y";
   3.173 -by (blast_tac (claset() addIs [component_trans]) 1);
   3.174 -qed "guarantees_weaken_prog";
   3.175 -
   3.176 -Goalw [guar_def] "X <= Y ==> X guarantees Y = UNIV";
   3.177 -by (Blast_tac 1);
   3.178 -qed "subset_imp_guarantees_UNIV";
   3.179 -
   3.180 -(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
   3.181 -Goalw [guar_def] "X <= Y ==> F : X guarantees Y";
   3.182 -by (Blast_tac 1);
   3.183 -qed "subset_imp_guarantees";
   3.184 -
   3.185 -(*Remark at end of section 4.1*)
   3.186 -Goalw [guar_def] "ex_prop Y = (Y = UNIV guarantees Y)";
   3.187 -by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
   3.188 -by (blast_tac (claset() addEs [equalityE]) 1);
   3.189 -qed "ex_prop_equiv2";
   3.190 -
   3.191 -(** Distributive laws.  Re-orient to perform miniscoping **)
   3.192 -
   3.193 -Goalw [guar_def]
   3.194 -     "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)";
   3.195 -by (Blast_tac 1);
   3.196 -qed "guarantees_UN_left";
   3.197 -
   3.198 -Goalw [guar_def]
   3.199 -    "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)";
   3.200 -by (Blast_tac 1);
   3.201 -qed "guarantees_Un_left";
   3.202 -
   3.203 -Goalw [guar_def]
   3.204 -     "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)";
   3.205 -by (Blast_tac 1);
   3.206 -qed "guarantees_INT_right";
   3.207 -
   3.208 -Goalw [guar_def]
   3.209 -    "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)";
   3.210 -by (Blast_tac 1);
   3.211 -qed "guarantees_Int_right";
   3.212 -
   3.213 -Goalw [guar_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))";
   3.214 -by (Blast_tac 1);
   3.215 -qed "shunting";
   3.216 -
   3.217 -Goalw [guar_def] "(X guarantees Y) = -Y guarantees -X";
   3.218 -by (Blast_tac 1);
   3.219 -qed "contrapositive";
   3.220 -
   3.221 -(** The following two can be expressed using intersection and subset, which
   3.222 -    is more faithful to the text but looks cryptic.
   3.223 -**)
   3.224 -
   3.225 -Goalw [guar_def]
   3.226 -    "[| F : V guarantees X;  F : (X Int Y) guarantees Z |]\
   3.227 -\    ==> F : (V Int Y) guarantees Z";
   3.228 -by (Blast_tac 1);
   3.229 -qed "combining1";
   3.230 -
   3.231 -Goalw [guar_def]
   3.232 -    "[| F : V guarantees (X Un Y);  F : Y guarantees Z |]\
   3.233 -\    ==> F : V guarantees (X Un Z)";
   3.234 -by (Blast_tac 1);
   3.235 -qed "combining2";
   3.236 -
   3.237 -(** The following two follow Chandy-Sanders, but the use of object-quantifiers
   3.238 -    does not suit Isabelle... **)
   3.239 -
   3.240 -(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *)
   3.241 -Goalw [guar_def]
   3.242 -     "ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)";
   3.243 -by (Blast_tac 1);
   3.244 -qed "all_guarantees";
   3.245 -
   3.246 -(*Premises should be [| F: X guarantees Y i; i: I |] *)
   3.247 -Goalw [guar_def]
   3.248 -     "EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)";
   3.249 -by (Blast_tac 1);
   3.250 -qed "ex_guarantees";
   3.251 -
   3.252 -(*** Additional guarantees laws, by lcp ***)
   3.253 -
   3.254 -Goalw [guar_def]
   3.255 -    "[| F: U guarantees V;  G: X guarantees Y |] \
   3.256 -\    ==> F Join G: (U Int X) guarantees (V Int Y)";
   3.257 -by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
   3.258 -by (Blast_tac 1);
   3.259 -qed "guarantees_Join_Int";
   3.260 -
   3.261 -Goalw [guar_def]
   3.262 -    "[| F: U guarantees V;  G: X guarantees Y |]  \
   3.263 -\    ==> F Join G: (U Un X) guarantees (V Un Y)";
   3.264 -by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
   3.265 -by (Blast_tac 1);
   3.266 -qed "guarantees_Join_Un";
   3.267 -
   3.268 -Goal "((JOIN I F) component H) = (ALL i: I. F i component H)";
   3.269 -by (simp_tac (simpset() addsimps [component_eq_subset, Acts_JN]) 1);
   3.270 -by (Blast_tac 1);
   3.271 -qed "JN_component_iff";
   3.272 -
   3.273 -Goalw [guar_def]
   3.274 -    "[| ALL i:I. F i : X i guarantees Y i |] \
   3.275 -\    ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)";
   3.276 -by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
   3.277 -by (Blast_tac 1);
   3.278 -bind_thm ("guarantees_JN_INT", ballI RS result());
   3.279 -
   3.280 -Goalw [guar_def]
   3.281 -    "[| ALL i:I. F i : X i guarantees Y i |] \
   3.282 -\    ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)";
   3.283 -by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
   3.284 -by (Blast_tac 1);
   3.285 -bind_thm ("guarantees_JN_UN", ballI RS result());
   3.286 -
   3.287 -
   3.288 -(*** guarantees laws for breaking down the program, by lcp ***)
   3.289 -
   3.290 -Goalw [guar_def]
   3.291 -    "F: X guarantees Y | G: X guarantees Y ==> F Join G: X guarantees Y";
   3.292 -by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
   3.293 -by (Blast_tac 1);
   3.294 -qed "guarantees_Join_I";
   3.295 -
   3.296 -Goalw [guar_def]
   3.297 -     "[| i : I;  F i: X guarantees Y |] ==> (JN i:I. (F i)) : X guarantees Y";
   3.298 -by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
   3.299 -by (Blast_tac 1);
   3.300 -qed "guarantees_JN_I";
   3.301 -
   3.302 -
   3.303 -(*** well-definedness ***)
   3.304 -
   3.305 -Goalw [welldef_def] "F Join G: welldef ==> F: welldef";
   3.306 -by Auto_tac;
   3.307 -qed "Join_welldef_D1";
   3.308 -
   3.309 -Goalw [welldef_def] "F Join G: welldef ==> G: welldef";
   3.310 -by Auto_tac;
   3.311 -qed "Join_welldef_D2";
   3.312 -
   3.313 -(*** refinement ***)
   3.314 -
   3.315 -Goalw [refines_def] "F refines F wrt X";
   3.316 -by (Blast_tac 1);
   3.317 -qed "refines_refl";
   3.318 -
   3.319 -Goalw [refines_def]
   3.320 -     "[| H refines G wrt X;  G refines F wrt X |] ==> H refines F wrt X";
   3.321 -by Auto_tac;
   3.322 -qed "refines_trans";
   3.323 -
   3.324 -Goalw [strict_ex_prop_def]
   3.325 -     "strict_ex_prop X \
   3.326 -\     ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)";
   3.327 -by (Blast_tac 1);
   3.328 -qed "strict_ex_refine_lemma";
   3.329 -
   3.330 -Goalw [strict_ex_prop_def]
   3.331 -     "strict_ex_prop X \
   3.332 -\     ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \
   3.333 -\         (F: welldef Int X --> G:X)";
   3.334 -by Safe_tac;
   3.335 -by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
   3.336 -by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2], simpset()));
   3.337 -qed "strict_ex_refine_lemma_v";
   3.338 -
   3.339 -Goal "[| strict_ex_prop X;  \
   3.340 -\        ALL H. F Join H : welldef Int X --> G Join H : welldef |] \
   3.341 -\     ==> (G refines F wrt X) = (G iso_refines F wrt X)";
   3.342 -by (res_inst_tac [("x","SKIP")] allE 1
   3.343 -    THEN assume_tac 1);
   3.344 -by (asm_full_simp_tac
   3.345 -    (simpset() addsimps [refines_def, iso_refines_def,
   3.346 -			 strict_ex_refine_lemma_v]) 1);
   3.347 -qed "ex_refinement_thm";
   3.348 -
   3.349 -
   3.350 -Goalw [strict_uv_prop_def]
   3.351 -     "strict_uv_prop X \
   3.352 -\     ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)";
   3.353 -by (Blast_tac 1);
   3.354 -qed "strict_uv_refine_lemma";
   3.355 -
   3.356 -Goalw [strict_uv_prop_def]
   3.357 -     "strict_uv_prop X \
   3.358 -\     ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \
   3.359 -\         (F: welldef Int X --> G:X)";
   3.360 -by Safe_tac;
   3.361 -by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
   3.362 -by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2],
   3.363 -	      simpset()));
   3.364 -qed "strict_uv_refine_lemma_v";
   3.365 -
   3.366 -Goal "[| strict_uv_prop X;  \
   3.367 -\        ALL H. F Join H : welldef Int X --> G Join H : welldef |] \
   3.368 -\     ==> (G refines F wrt X) = (G iso_refines F wrt X)";
   3.369 -by (res_inst_tac [("x","SKIP")] allE 1
   3.370 -    THEN assume_tac 1);
   3.371 -by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def,
   3.372 -					   strict_uv_refine_lemma_v]) 1);
   3.373 -qed "uv_refinement_thm";
   3.374 +bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);
     4.1 --- a/src/HOL/UNITY/Comp.thy	Mon Aug 30 23:19:13 1999 +0200
     4.2 +++ b/src/HOL/UNITY/Comp.thy	Tue Aug 31 15:56:56 1999 +0200
     4.3 @@ -10,42 +10,13 @@
     4.4  
     4.5  Comp = Union +
     4.6  
     4.7 -constdefs
     4.8 -
     4.9 -  (*Existential and Universal properties.  I formalize the two-program
    4.10 -    case, proving equivalence with Chandy and Sanders's n-ary definitions*)
    4.11 -
    4.12 -  ex_prop  :: 'a program set => bool
    4.13 -   "ex_prop X == ALL F G. F:X | G: X --> (F Join G) : X"
    4.14 -
    4.15 -  strict_ex_prop  :: 'a program set => bool
    4.16 -   "strict_ex_prop X == ALL F G. (F:X | G: X) = (F Join G : X)"
    4.17 -
    4.18 -  uv_prop  :: 'a program set => bool
    4.19 -   "uv_prop X == SKIP : X & (ALL F G. F:X & G: X --> (F Join G) : X)"
    4.20 -
    4.21 -  strict_uv_prop  :: 'a program set => bool
    4.22 -   "strict_uv_prop X == SKIP : X & (ALL F G. (F:X & G: X) = (F Join G : X))"
    4.23 +instance
    4.24 +  program :: (term)ord
    4.25  
    4.26 -  (*Ill-defined programs can arise through "Join"*)
    4.27 -  welldef :: 'a program set  
    4.28 -   "welldef == {F. Init F ~= {}}"
    4.29 -
    4.30 -  component :: ['a program, 'a program] => bool     (infixl 50)
    4.31 -   "F component H == EX G. F Join G = H"
    4.32 +defs
    4.33  
    4.34 -  guar :: ['a program set, 'a program set] => 'a program set
    4.35 -   (infixl "guarantees" 55)    (*higher than membership, lower than Co*)
    4.36 -   "X guarantees Y == {F. ALL H. F component H --> H:X --> H:Y}"
    4.37 +  component_def   "F <= H == EX G. F Join G = H"
    4.38  
    4.39 -  refines :: ['a program, 'a program, 'a program set] => bool
    4.40 -			("(3_ refines _ wrt _)" [10,10,10] 10)
    4.41 -   "G refines F wrt X ==
    4.42 -      ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X"
    4.43 -
    4.44 -  iso_refines :: ['a program, 'a program, 'a program set] => bool
    4.45 -			("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
    4.46 -   "G iso_refines F wrt X ==
    4.47 -      F : welldef Int X --> G : welldef Int X"
    4.48 +  strict_component_def   "(F < (H::'a program)) == (F <= H & F ~= H)"
    4.49  
    4.50  end
     5.1 --- a/src/HOL/UNITY/Extend.ML	Mon Aug 30 23:19:13 1999 +0200
     5.2 +++ b/src/HOL/UNITY/Extend.ML	Tue Aug 31 15:56:56 1999 +0200
     5.3 @@ -300,8 +300,7 @@
     5.4  
     5.5  (*Opposite direction fails because Diff in the extended state may remove
     5.6    fewer actions, i.e. those that affect other state variables.*)
     5.7 -Goal "Diff (project h G) acts  component  \
     5.8 -\     project h (Diff G (extend_act h `` acts))";
     5.9 +Goal "Diff (project h G) acts <= project h (Diff G (extend_act h `` acts))";
    5.10  by (force_tac (claset(), 
    5.11  	       simpset() addsimps [component_eq_subset, Diff_def]) 1);
    5.12  qed "Diff_project_component_project_Diff";
     6.1 --- a/src/HOL/UNITY/Extend.thy	Mon Aug 30 23:19:13 1999 +0200
     6.2 +++ b/src/HOL/UNITY/Extend.thy	Tue Aug 31 15:56:56 1999 +0200
     6.3 @@ -8,7 +8,7 @@
     6.4    function g (forgotten) maps the extended state to the "extending part"
     6.5  *)
     6.6  
     6.7 -Extend = Union + Comp +
     6.8 +Extend = Guar +
     6.9  
    6.10  constdefs
    6.11  
     7.1 --- a/src/HOL/UNITY/Lift_prog.ML	Mon Aug 30 23:19:13 1999 +0200
     7.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Tue Aug 31 15:56:56 1999 +0200
     7.3 @@ -68,12 +68,12 @@
     7.4  
     7.5  (** These monotonicity results look natural but are UNUSED **)
     7.6  
     7.7 -Goal "F component G ==> lift_prog i F component lift_prog i G";
     7.8 +Goal "F <= G ==> lift_prog i F <= lift_prog i G";
     7.9  by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
    7.10  by Auto_tac;
    7.11  qed "lift_prog_mono";
    7.12  
    7.13 -Goal "F component G ==> drop_prog i F component drop_prog i G";
    7.14 +Goal "F <= G ==> drop_prog i F <= drop_prog i G";
    7.15  by (full_simp_tac (simpset() addsimps [component_eq_subset, drop_set_def]) 1);
    7.16  by Auto_tac;
    7.17  qed "drop_prog_mono";
    7.18 @@ -218,6 +218,8 @@
    7.19  
    7.20  (*** Diff, needed for localTo ***)
    7.21  
    7.22 +(** THESE PROOFS CAN BE GENERALIZED AS IN EXTEND.ML **)
    7.23 +
    7.24  Goal "Diff G (lift_act i `` Acts F) : (lift_set i A) co (lift_set i B)  \
    7.25  \     ==> Diff (drop_prog i G) (Acts F) : A co B";
    7.26  by (auto_tac (claset(), 
    7.27 @@ -382,7 +384,10 @@
    7.28  by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1);
    7.29  qed "lift_prog_guarantees";
    7.30  
    7.31 -(*Weak precondition and postcondition; this is the good one!*)
    7.32 +(*Weak precondition and postcondition; this is the good one!
    7.33 +CAN WEAKEN 2ND PREMISE TO  
    7.34 +      !!G. extend h F Join G : XX ==> F Join project h G : X; 
    7.35 +*)
    7.36  val [xguary,drop_prog,lift_prog] =
    7.37  Goal "[| F : X guarantees Y;  \
    7.38  \        !!H. H : XX ==> drop_prog i H : X;  \
     8.1 --- a/src/HOL/UNITY/Lift_prog.thy	Mon Aug 30 23:19:13 1999 +0200
     8.2 +++ b/src/HOL/UNITY/Lift_prog.thy	Tue Aug 31 15:56:56 1999 +0200
     8.3 @@ -6,7 +6,7 @@
     8.4  lift_prog, etc: replication of components
     8.5  *)
     8.6  
     8.7 -Lift_prog = Union + Comp +
     8.8 +Lift_prog = Guar +
     8.9  
    8.10  constdefs
    8.11  
     9.1 --- a/src/HOL/UNITY/PPROD.ML	Mon Aug 30 23:19:13 1999 +0200
     9.2 +++ b/src/HOL/UNITY/PPROD.ML	Tue Aug 31 15:56:56 1999 +0200
     9.3 @@ -40,7 +40,7 @@
     9.4  by Auto_tac;
     9.5  qed "PLam_insert";
     9.6  
     9.7 -Goalw [PLam_def] "i : I ==> (lift_prog i (F i)) component (PLam I F)";
     9.8 +Goalw [PLam_def] "i : I ==> lift_prog i (F i) <= (PLam I F)";
     9.9  (*blast_tac doesn't use HO unification*)
    9.10  by (fast_tac (claset() addIs [component_JN]) 1);
    9.11  qed "component_PLam";