src/HOL/UNITY/Union.ML
changeset 5313 1861a564d7e2
parent 5259 86d80749453f
child 5426 566f47250bd0
     1.1 --- a/src/HOL/UNITY/Union.ML	Thu Aug 13 17:44:50 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Union.ML	Thu Aug 13 18:06:40 1998 +0200
     1.3 @@ -11,133 +11,35 @@
     1.4      Maybe Join instead of Un, and JOIN for UNION
     1.5  *)
     1.6  
     1.7 -(*** Safety: constrains, stable, FP ***)
     1.8 -
     1.9 -Goalw [constrains_def]
    1.10 -    "constrains (UN i:I. acts i) A B = (ALL i:I. constrains (acts i) A B)";
    1.11 -by (Blast_tac 1);
    1.12 -qed "constrains_UN";
    1.13 -
    1.14 -Goalw [constrains_def]
    1.15 -    "constrains (actsF Un actsG) A B =  \
    1.16 -\    (constrains actsF A B & constrains actsG A B)";
    1.17 -by (simp_tac (simpset() addsimps [ball_Un]) 1);
    1.18 -qed "constrains_Un";
    1.19 -
    1.20 -(*Provable by constrains_Un and constrains_weaken, but why bother?*)
    1.21 -Goalw [constrains_def]
    1.22 -     "[| constrains actsF A A';  constrains actsG B B' |] \
    1.23 -\     ==> constrains (actsF Un actsG) (A Int B) (A' Un B')";
    1.24 -by (Blast_tac 1);
    1.25 -qed "constrains_Un_weaken";
    1.26  
    1.27 -Goalw [stable_def] "stable (UN i:I. acts i) A = (ALL i:I. stable (acts i) A)";
    1.28 -by (simp_tac (simpset() addsimps [constrains_UN]) 1);
    1.29 -qed "stable_UN";
    1.30 -
    1.31 -Goalw [stable_def]
    1.32 -    "stable (actsF Un actsG) A = (stable actsF A & stable actsG A)";
    1.33 -by (simp_tac (simpset() addsimps [constrains_Un]) 1);
    1.34 -qed "stable_Un";
    1.35 +Goal "Init (Join prgF prgG) = Init prgF Int Init prgG";
    1.36 +by (simp_tac (simpset() addsimps [Join_def]) 1);
    1.37 +qed "Init_Join";
    1.38  
    1.39 -Goal "stable (Acts (Join prgF prgG)) A = \
    1.40 -\     (stable (Acts prgF) A & stable (Acts prgG) A)";
    1.41 -by (simp_tac (simpset() addsimps [Join_def, stable_Un]) 1);
    1.42 -qed "stable_Join";
    1.43 -
    1.44 -Goalw [FP_def] "FP (UN i:I. acts i) = (INT i:I. FP (acts i))";
    1.45 -by (simp_tac (simpset() addsimps [stable_UN, INTER_def]) 1);
    1.46 -qed "FP_UN";
    1.47 -
    1.48 -
    1.49 -(*** Progress: transient, ensures ***)
    1.50 -
    1.51 -Goalw [transient_def]
    1.52 -    "transient (UN i:I. acts i) A = (EX i:I. transient (acts i) A)";
    1.53 -by (Simp_tac 1);
    1.54 -qed "transient_UN";
    1.55 +Goal "Acts (Join prgF prgG) = Acts prgF Un Acts prgG";
    1.56 +by (simp_tac (simpset() addsimps [Join_def]) 1);
    1.57 +qed "Acts_Join";
    1.58  
    1.59 -Goalw [ensures_def,transient_def]
    1.60 -    "ensures (UN i:I. acts i) A B = \
    1.61 -\    ((ALL i:I. constrains (acts i) (A-B) (A Un B)) & \
    1.62 -\     (EX i:I. ensures (acts i) A B))";
    1.63 -by (simp_tac (simpset() addsimps [constrains_UN]) 1);
    1.64 -by Auto_tac;
    1.65 -qed "ensures_UN";
    1.66 -
    1.67 -(*Alternative proof: simplify using ensures_def,transient_def,constrains_Un*)
    1.68 -Goal "ensures (actsF Un actsG) A B =     \
    1.69 -\     (constrains actsF (A-B) (A Un B) & \
    1.70 -\      constrains actsG (A-B) (A Un B) & \
    1.71 -\      (ensures actsF A B | ensures actsG A B))";
    1.72 -by (simp_tac (simpset() addcongs [conj_cong]
    1.73 -			addsimps [ensures_UN, Un_eq_UN,
    1.74 -				  all_bool_eq, ex_bool_eq]) 1);
    1.75 -qed "ensures_Un";
    1.76 -
    1.77 -(*Or a longer proof via constrains_imp_subset*)
    1.78 -Goalw [stable_def, constrains_def]
    1.79 -     "[| stable actsF A;  constrains actsG A A';  id: actsG |] \
    1.80 -\     ==> constrains (actsF Un actsG) A A'";
    1.81 -by (asm_simp_tac (simpset() addsimps [ball_Un]) 1);
    1.82 -by (Blast_tac 1);
    1.83 -qed "stable_constrains_Un";
    1.84 +Goal "Init (JN i:I. prg i) = (INT i:I. Init (prg i))";
    1.85 +by (simp_tac (simpset() addsimps [JOIN_def]) 1);
    1.86 +qed "Init_JN";
    1.87  
    1.88 -Goalw [Join_def]
    1.89 -      "[| stable (Acts prgF) A;  invariant prgG A |]     \
    1.90 -\      ==> invariant (Join prgF prgG) A";
    1.91 -by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_Un]) 1);
    1.92 -by (Blast_tac 1);
    1.93 -qed "stable_Join_invariant";
    1.94 -
    1.95 -Goal "[| stable actsF A;  ensures actsG A B |]     \
    1.96 -\     ==> ensures (actsF Un actsG) A B";
    1.97 -by (asm_simp_tac (simpset() addsimps [ensures_Un]) 1);
    1.98 -by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
    1.99 -by (etac constrains_weaken 1);
   1.100 -by Auto_tac;
   1.101 -qed "ensures_stable_Un1";
   1.102 +Goal "Acts (JN i:I. prg i) = (UN i:I. Acts (prg i))";
   1.103 +by (simp_tac (simpset() addsimps [JOIN_def]) 1);
   1.104 +qed "Acts_JN";
   1.105  
   1.106 -Goal "[| stable (Acts prgF) A;  ensures (Acts prgG) A B |]     \
   1.107 -\     ==> ensures (Acts (Join prgF prgG)) A B";
   1.108 -by (asm_simp_tac (simpset() addsimps [Join_def, ensures_stable_Un1]) 1);
   1.109 -qed "ensures_stable_Join1";
   1.110 -
   1.111 -(*As above, but exchanging the roles of F and G*)
   1.112 -Goal "[| ensures actsF A B;  stable actsG A |]     \
   1.113 -\     ==> ensures (actsF Un actsG) A B";
   1.114 -by (stac Un_commute 1);
   1.115 -by (blast_tac (claset() addIs [ensures_stable_Un1]) 1);
   1.116 -qed "ensures_stable_Un2";
   1.117 -
   1.118 -Goal "[| ensures (Acts prgF) A B;  stable (Acts prgG) A |]     \
   1.119 -\     ==> ensures (Acts (Join prgF prgG)) A B";
   1.120 -by (asm_simp_tac (simpset() addsimps [Join_def, ensures_stable_Un2]) 1);
   1.121 -qed "ensures_stable_Join2";
   1.122 -
   1.123 +Addsimps [Init_Join, Init_JN];
   1.124  
   1.125  (** Theoretical issues **)
   1.126  
   1.127 -Goalw [Join_def] "Join prgF prgG = Join prgG prgF";
   1.128 -by (simp_tac (simpset() addsimps [Un_commute, Int_commute]) 1);
   1.129 +Goal "Join prgF prgG = Join prgG prgF";
   1.130 +by (simp_tac (simpset() addsimps [Join_def, Un_commute, Int_commute]) 1);
   1.131  qed "Join_commute";
   1.132  
   1.133 -Goalw [Join_def] "Join (Join prgF prgG) prgH = Join prgF (Join prgG prgH)";
   1.134 -by (simp_tac (simpset() addsimps [Un_assoc, Int_assoc]) 1);
   1.135 +Goal "Join (Join prgF prgG) prgH = Join prgF (Join prgG prgH)";
   1.136 +by (simp_tac (simpset() addsimps [Join_def, Un_assoc, Int_assoc]) 1);
   1.137  qed "Join_assoc";
   1.138  
   1.139 -(**NOT PROVABLE because no "surjective pairing" for records
   1.140 -Goalw [Join_def, Null_def] "id: Acts prgF ==> Join prgF Null = prgF";
   1.141 -by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
   1.142 -qed "Join_Null";
   1.143 -*)
   1.144 -
   1.145 -(**NOT PROVABLE because no "surjective pairing" for records
   1.146 -Goalw [Join_def] "Join prgF prgF = prgF";
   1.147 -auto();
   1.148 -qed "Join_absorb";
   1.149 -*)
   1.150 -
   1.151  
   1.152  (*
   1.153  val field_defs = thms"program.field_defs";
   1.154 @@ -149,3 +51,124 @@
   1.155  val update_convs = thms"program.update_convs";
   1.156  val simps = thms"program.simps";
   1.157  *)
   1.158 +
   1.159 +
   1.160 +(**NOT PROVABLE because no "surjective pairing" for records
   1.161 +Goalw [Join_def, Null_def] "id: Acts prgF ==> Join prgF Null = prgF";
   1.162 +by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
   1.163 +qed "Join_Null";
   1.164 +*)
   1.165 +
   1.166 +(**NOT PROVABLE because no "surjective pairing" for records
   1.167 +Goalw [Join_def] "Join prgF prgF = prgF";
   1.168 +by Auto_tac;
   1.169 +qed "Join_absorb";
   1.170 +*)
   1.171 +
   1.172 +
   1.173 +
   1.174 +(*** Safety: constrains, stable, FP ***)
   1.175 +
   1.176 +Goalw [constrains_def, JOIN_def]
   1.177 +    "constrains (Acts (JN i:I. prg i)) A B = \
   1.178 +\    (ALL i:I. constrains (Acts (prg i)) A B)";
   1.179 +by Auto_tac;
   1.180 +qed "constrains_JN";
   1.181 +
   1.182 +(**FAILS, I think; see 5.4.1, Substitution Axiom.
   1.183 +Goalw [Constrains_def]
   1.184 +    "Constrains (JN i:I. prg i) A B = (ALL i:I. Constrains (prg i) A B)";
   1.185 +by (simp_tac (simpset() addsimps [constrains_JN]) 1);
   1.186 +by (Blast_tac 1);
   1.187 +qed "Constrains_JN";
   1.188 +**)
   1.189 +
   1.190 +Goalw [constrains_def, Join_def]
   1.191 +    "constrains (Acts (Join prgF prgG)) A B =  \
   1.192 +\    (constrains (Acts prgF) A B & constrains (Acts prgG) A B)";
   1.193 +by (simp_tac (simpset() addsimps [ball_Un]) 1);
   1.194 +qed "constrains_Join";
   1.195 +
   1.196 +Goal "[| constrains (Acts prgF) A A';  constrains (Acts prgG) B B' |] \
   1.197 +\     ==> constrains (Acts (Join prgF prgG)) (A Int B) (A' Un B')";
   1.198 +by (simp_tac (simpset() addsimps [constrains_Join]) 1);
   1.199 +by (blast_tac (claset() addIs [constrains_weaken]) 1);
   1.200 +qed "constrains_Join_weaken";
   1.201 +
   1.202 +Goalw [stable_def] 
   1.203 +    "stable (Acts (JN i:I. prg i)) A = (ALL i:I. stable (Acts (prg i)) A)";
   1.204 +by (simp_tac (simpset() addsimps [constrains_JN]) 1);
   1.205 +qed "stable_JN";
   1.206 +
   1.207 +Goal "stable (Acts (Join prgF prgG)) A = \
   1.208 +\     (stable (Acts prgF) A & stable (Acts prgG) A)";
   1.209 +by (simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1);
   1.210 +qed "stable_Join";
   1.211 +
   1.212 +Goalw [FP_def] "FP (Acts (JN i:I. prg i)) = (INT i:I. FP (Acts (prg i)))";
   1.213 +by (simp_tac (simpset() addsimps [stable_JN, INTER_def]) 1);
   1.214 +qed "FP_JN";
   1.215 +
   1.216 +
   1.217 +(*** Progress: transient, ensures ***)
   1.218 +
   1.219 +Goalw [transient_def, JOIN_def]
   1.220 +   "transient (Acts (JN i:I. prg i)) A = (EX i:I. transient (Acts (prg i)) A)";
   1.221 +by (Simp_tac 1);
   1.222 +qed "transient_JN";
   1.223 +
   1.224 +Goalw [transient_def, Join_def]
   1.225 +   "transient (Acts (Join prgF prgG)) A = \
   1.226 +\   (transient (Acts prgF) A | transient (Acts prgG) A)";
   1.227 +by (simp_tac (simpset() addsimps [bex_Un]) 1);
   1.228 +qed "transient_Join";
   1.229 +
   1.230 +Goalw [ensures_def]
   1.231 +    "ensures (Acts (JN i:I. prg i)) A B = \
   1.232 +\    ((ALL i:I. constrains (Acts (prg i)) (A-B) (A Un B)) & \
   1.233 +\     (EX i:I. ensures (Acts (prg i)) A B))";
   1.234 +by (auto_tac (claset(),
   1.235 +	      simpset() addsimps [constrains_JN, transient_JN]));
   1.236 +qed "ensures_JN";
   1.237 +
   1.238 +Goalw [ensures_def]
   1.239 +     "ensures (Acts (Join prgF prgG)) A B =     \
   1.240 +\     (constrains (Acts prgF) (A-B) (A Un B) & \
   1.241 +\      constrains (Acts prgG) (A-B) (A Un B) & \
   1.242 +\      (ensures (Acts prgF) A B | ensures (Acts prgG) A B))";
   1.243 +by (auto_tac (claset(),
   1.244 +	      simpset() addsimps [constrains_Join, transient_Join]));
   1.245 +qed "ensures_Join";
   1.246 +
   1.247 +Goalw [stable_def, constrains_def, Join_def]
   1.248 +    "[| stable (Acts prgF) A;  constrains (Acts prgG) A A';  id: Acts prgG |] \
   1.249 +\    ==> constrains (Acts (Join prgF prgG)) A A'";
   1.250 +by (asm_simp_tac (simpset() addsimps [ball_Un]) 1);
   1.251 +by (Blast_tac 1);
   1.252 +qed "stable_constrains_Join";
   1.253 +
   1.254 +(*Premises cannot use Invariant because  Stable prgF A  is weaker than
   1.255 +  stable (Acts prgG) A *)
   1.256 +Goal  "[| stable (Acts prgF) A;  Init prgG <= A;  stable (Acts prgG) A |] \
   1.257 +\      ==> Invariant (Join prgF prgG) A";
   1.258 +by (simp_tac (simpset() addsimps [Invariant_def, Stable_eq_stable,
   1.259 +				  stable_Join]) 1);
   1.260 +by (force_tac(claset() addIs [stable_reachable, stable_Int],
   1.261 +	      simpset() addsimps [Acts_Join]) 1);
   1.262 +qed "stable_Join_Invariant";
   1.263 +
   1.264 +Goal "[| stable (Acts prgF) A;  ensures (Acts prgG) A B |]     \
   1.265 +\     ==> ensures (Acts (Join prgF prgG)) A B";
   1.266 +by (asm_simp_tac (simpset() addsimps [ensures_Join]) 1);
   1.267 +by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
   1.268 +by (etac constrains_weaken 1);
   1.269 +by Auto_tac;
   1.270 +qed "ensures_stable_Join1";
   1.271 +
   1.272 +(*As above, but exchanging the roles of F and G*)
   1.273 +Goal "[| ensures (Acts prgF) A B;  stable (Acts prgG) A |]     \
   1.274 +\     ==> ensures (Acts (Join prgF prgG)) A B";
   1.275 +by (stac Join_commute 1);
   1.276 +by (blast_tac (claset() addIs [ensures_stable_Join1]) 1);
   1.277 +qed "ensures_stable_Join2";
   1.278 +