src/HOL/UNITY/SubstAx.ML
changeset 4776 1f9362e769c1
child 5069 3ea049f7979d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/UNITY/SubstAx.ML	Fri Apr 03 12:34:33 1998 +0200
     1.3 @@ -0,0 +1,405 @@
     1.4 +(*  Title:      HOL/UNITY/SubstAx
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1998  University of Cambridge
     1.8 +
     1.9 +Weak Fairness versions of transient, ensures, LeadsTo.
    1.10 +
    1.11 +From Misra, "A Logic for Concurrent Programming", 1994
    1.12 +*)
    1.13 +
    1.14 +open SubstAx;
    1.15 +
    1.16 +(*constrains Acts B B' ==> constrains Acts (reachable Init Acts Int B)
    1.17 +                                           (reachable Init Acts Int B') *)
    1.18 +bind_thm ("constrains_reachable",
    1.19 +	  rewrite_rule [stable_def] stable_reachable RS constrains_Int);
    1.20 +
    1.21 +
    1.22 +(*** Introduction rules: Basis, Trans, Union ***)
    1.23 +
    1.24 +goalw thy [LeadsTo_def]
    1.25 +    "!!Acts. leadsTo Acts A B ==> LeadsTo Init Acts A B";
    1.26 +by (blast_tac (claset() addIs [PSP_stable2, stable_reachable]) 1);
    1.27 +qed "leadsTo_imp_LeadsTo";
    1.28 +
    1.29 +goalw thy [LeadsTo_def]
    1.30 +    "!!Acts. [| constrains Acts (reachable Init Acts Int (A - A'))   \
    1.31 +\                               (A Un A'); \
    1.32 +\               transient  Acts (reachable Init Acts Int (A-A')) |]   \
    1.33 +\           ==> LeadsTo Init Acts A A'";
    1.34 +by (rtac (stable_reachable RS stable_ensures_Int RS leadsTo_Basis) 1);
    1.35 +by (assume_tac 2);
    1.36 +by (asm_simp_tac 
    1.37 +    (simpset() addsimps [Int_Un_distrib RS sym, Diff_Int_distrib RS sym,
    1.38 +			 stable_constrains_Int]) 1);
    1.39 +qed "LeadsTo_Basis";
    1.40 +
    1.41 +goalw thy [LeadsTo_def]
    1.42 +    "!!Acts. [| LeadsTo Init Acts A B;  LeadsTo Init Acts B C |] \
    1.43 +\            ==> LeadsTo Init Acts A C";
    1.44 +by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
    1.45 +qed "LeadsTo_Trans";
    1.46 +
    1.47 +val prems = goalw thy [LeadsTo_def]
    1.48 + "(!!A. A : S ==> LeadsTo Init Acts A B) ==> LeadsTo Init Acts (Union S) B";
    1.49 +by (stac Int_Union 1);
    1.50 +by (blast_tac (claset() addIs (leadsTo_UN::prems)) 1);
    1.51 +qed "LeadsTo_Union";
    1.52 +
    1.53 +
    1.54 +(*** Derived rules ***)
    1.55 +
    1.56 +goal thy "!!Acts. id: Acts ==> LeadsTo Init Acts A UNIV";
    1.57 +by (asm_simp_tac (simpset() addsimps [LeadsTo_def, 
    1.58 +				      Int_lower1 RS subset_imp_leadsTo]) 1);
    1.59 +qed "LeadsTo_UNIV";
    1.60 +Addsimps [LeadsTo_UNIV];
    1.61 +
    1.62 +(*Useful with cancellation, disjunction*)
    1.63 +goal thy "!!Acts. LeadsTo Init Acts A (A' Un A') ==> LeadsTo Init Acts A A'";
    1.64 +by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
    1.65 +qed "LeadsTo_Un_duplicate";
    1.66 +
    1.67 +goal thy "!!Acts. LeadsTo Init Acts A (A' Un C Un C) ==> LeadsTo Init Acts A (A' Un C)";
    1.68 +by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
    1.69 +qed "LeadsTo_Un_duplicate2";
    1.70 +
    1.71 +val prems = goal thy
    1.72 +   "(!!i. i : I ==> LeadsTo Init Acts (A i) B) \
    1.73 +\   ==> LeadsTo Init Acts (UN i:I. A i) B";
    1.74 +by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
    1.75 +by (blast_tac (claset() addIs (LeadsTo_Union::prems)) 1);
    1.76 +qed "LeadsTo_UN";
    1.77 +
    1.78 +(*Binary union introduction rule*)
    1.79 +goal thy
    1.80 +  "!!C. [| LeadsTo Init Acts A C; LeadsTo Init Acts B C |] ==> LeadsTo Init Acts (A Un B) C";
    1.81 +by (stac Un_eq_Union 1);
    1.82 +by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
    1.83 +qed "LeadsTo_Un";
    1.84 +
    1.85 +
    1.86 +goalw thy [LeadsTo_def]
    1.87 +    "!!A B. [| reachable Init Acts Int A <= B;  id: Acts |] \
    1.88 +\           ==> LeadsTo Init Acts A B";
    1.89 +by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
    1.90 +qed "Int_subset_imp_LeadsTo";
    1.91 +
    1.92 +goalw thy [LeadsTo_def]
    1.93 +    "!!A B. [| A <= B;  id: Acts |] \
    1.94 +\           ==> LeadsTo Init Acts A B";
    1.95 +by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
    1.96 +qed "subset_imp_LeadsTo";
    1.97 +
    1.98 +bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo);
    1.99 +Addsimps [empty_LeadsTo];
   1.100 +
   1.101 +goal thy
   1.102 +    "!!A B. [| reachable Init Acts Int A = {};  id: Acts |] \
   1.103 +\           ==> LeadsTo Init Acts A B";
   1.104 +by (asm_simp_tac (simpset() addsimps [Int_subset_imp_LeadsTo]) 1);
   1.105 +qed "Int_empty_LeadsTo";
   1.106 +
   1.107 +
   1.108 +goalw thy [LeadsTo_def]
   1.109 +    "!!Acts. [| LeadsTo Init Acts A A';   \
   1.110 +\               reachable Init Acts Int A' <= B' |] \
   1.111 +\            ==> LeadsTo Init Acts A B'";
   1.112 +by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
   1.113 +qed_spec_mp "LeadsTo_weaken_R";
   1.114 +
   1.115 +
   1.116 +goalw thy [LeadsTo_def]
   1.117 +    "!!Acts. [| LeadsTo Init Acts A A'; \
   1.118 +     \               reachable Init Acts Int B <= A; id: Acts |]  \
   1.119 +\            ==> LeadsTo Init Acts B A'";
   1.120 +by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
   1.121 +qed_spec_mp "LeadsTo_weaken_L";
   1.122 +
   1.123 +
   1.124 +(*Distributes over binary unions*)
   1.125 +goal thy
   1.126 +  "!!C. id: Acts ==> \
   1.127 +\       LeadsTo Init Acts (A Un B) C  =  \
   1.128 +\       (LeadsTo Init Acts A C & LeadsTo Init Acts B C)";
   1.129 +by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
   1.130 +qed "LeadsTo_Un_distrib";
   1.131 +
   1.132 +goal thy
   1.133 +  "!!C. id: Acts ==> \
   1.134 +\       LeadsTo Init Acts (UN i:I. A i) B  =  \
   1.135 +\       (ALL i : I. LeadsTo Init Acts (A i) B)";
   1.136 +by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
   1.137 +qed "LeadsTo_UN_distrib";
   1.138 +
   1.139 +goal thy
   1.140 +  "!!C. id: Acts ==> \
   1.141 +\       LeadsTo Init Acts (Union S) B  =  \
   1.142 +\       (ALL A : S. LeadsTo Init Acts A B)";
   1.143 +by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
   1.144 +qed "LeadsTo_Union_distrib";
   1.145 +
   1.146 +
   1.147 +goal thy 
   1.148 +   "!!Acts. [| LeadsTo Init Acts A A'; id: Acts;   \
   1.149 +\               reachable Init Acts Int B  <= A;     \
   1.150 +\               reachable Init Acts Int A' <= B' |] \
   1.151 +\           ==> LeadsTo Init Acts B B'";
   1.152 +(*PROOF FAILED: why?*)
   1.153 +by (blast_tac (claset() addIs [LeadsTo_Trans, LeadsTo_weaken_R,
   1.154 +			       LeadsTo_weaken_L]) 1);
   1.155 +qed "LeadsTo_weaken";
   1.156 +
   1.157 +
   1.158 +(*Set difference: maybe combine with leadsTo_weaken_L??*)
   1.159 +goal thy
   1.160 +  "!!C. [| LeadsTo Init Acts (A-B) C; LeadsTo Init Acts B C; id: Acts |] \
   1.161 +\       ==> LeadsTo Init Acts A C";
   1.162 +by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
   1.163 +qed "LeadsTo_Diff";
   1.164 +
   1.165 +
   1.166 +(** Meta or object quantifier ???????????????????
   1.167 +    see ball_constrains_UN in UNITY.ML***)
   1.168 +
   1.169 +val prems = goal thy
   1.170 +   "(!! i. i:I ==> LeadsTo Init Acts (A i) (A' i)) \
   1.171 +\   ==> LeadsTo Init Acts (UN i:I. A i) (UN i:I. A' i)";
   1.172 +by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
   1.173 +by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_R] 
   1.174 +                        addIs prems) 1);
   1.175 +qed "LeadsTo_UN_UN";
   1.176 +
   1.177 +
   1.178 +(*Version with no index set*)
   1.179 +val prems = goal thy
   1.180 +   "(!! i. LeadsTo Init Acts (A i) (A' i)) \
   1.181 +\   ==> LeadsTo Init Acts (UN i. A i) (UN i. A' i)";
   1.182 +by (blast_tac (claset() addIs [LeadsTo_UN_UN] 
   1.183 +                        addIs prems) 1);
   1.184 +qed "LeadsTo_UN_UN_noindex";
   1.185 +
   1.186 +(*Version with no index set*)
   1.187 +goal thy
   1.188 +   "!!Acts. ALL i. LeadsTo Init Acts (A i) (A' i) \
   1.189 +\           ==> LeadsTo Init Acts (UN i. A i) (UN i. A' i)";
   1.190 +by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1);
   1.191 +qed "all_LeadsTo_UN_UN";
   1.192 +
   1.193 +
   1.194 +(*Binary union version*)
   1.195 +goal thy "!!Acts. [| LeadsTo Init Acts A A'; LeadsTo Init Acts B B' |] \
   1.196 +\                 ==> LeadsTo Init Acts (A Un B) (A' Un B')";
   1.197 +by (blast_tac (claset() addIs [LeadsTo_Un, 
   1.198 +			       LeadsTo_weaken_R]) 1);
   1.199 +qed "LeadsTo_Un_Un";
   1.200 +
   1.201 +
   1.202 +(** The cancellation law **)
   1.203 +
   1.204 +goal thy
   1.205 +   "!!Acts. [| LeadsTo Init Acts A (A' Un B); LeadsTo Init Acts B B'; \
   1.206 +\              id: Acts |]    \
   1.207 +\           ==> LeadsTo Init Acts A (A' Un B')";
   1.208 +by (blast_tac (claset() addIs [LeadsTo_Un_Un, 
   1.209 +			       subset_imp_LeadsTo, LeadsTo_Trans]) 1);
   1.210 +qed "LeadsTo_cancel2";
   1.211 +
   1.212 +goal thy
   1.213 +   "!!Acts. [| LeadsTo Init Acts A (A' Un B); LeadsTo Init Acts (B-A') B'; id: Acts |] \
   1.214 +\           ==> LeadsTo Init Acts A (A' Un B')";
   1.215 +by (rtac LeadsTo_cancel2 1);
   1.216 +by (assume_tac 2);
   1.217 +by (ALLGOALS Asm_simp_tac);
   1.218 +qed "LeadsTo_cancel_Diff2";
   1.219 +
   1.220 +goal thy
   1.221 +   "!!Acts. [| LeadsTo Init Acts A (B Un A'); LeadsTo Init Acts B B'; id: Acts |] \
   1.222 +\           ==> LeadsTo Init Acts A (B' Un A')";
   1.223 +by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
   1.224 +by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1);
   1.225 +qed "LeadsTo_cancel1";
   1.226 +
   1.227 +goal thy
   1.228 +   "!!Acts. [| LeadsTo Init Acts A (B Un A'); LeadsTo Init Acts (B-A') B'; id: Acts |] \
   1.229 +\           ==> LeadsTo Init Acts A (B' Un A')";
   1.230 +by (rtac LeadsTo_cancel1 1);
   1.231 +by (assume_tac 2);
   1.232 +by (ALLGOALS Asm_simp_tac);
   1.233 +qed "LeadsTo_cancel_Diff1";
   1.234 +
   1.235 +
   1.236 +
   1.237 +(** The impossibility law **)
   1.238 +
   1.239 +goalw thy [LeadsTo_def]
   1.240 +    "!!Acts. LeadsTo Init Acts A {} ==> reachable Init Acts Int A  = {}";
   1.241 +by (Full_simp_tac 1);
   1.242 +by (etac leadsTo_empty 1);
   1.243 +qed "LeadsTo_empty";
   1.244 +
   1.245 +
   1.246 +(** PSP: Progress-Safety-Progress **)
   1.247 +
   1.248 +(*Special case of PSP: Misra's "stable conjunction".  Doesn't need id:Acts. *)
   1.249 +goalw thy [LeadsTo_def]
   1.250 +   "!!Acts. [| LeadsTo Init Acts A A'; stable Acts B |] \
   1.251 +\           ==> LeadsTo Init Acts (A Int B) (A' Int B)";
   1.252 +by (asm_simp_tac (simpset() addsimps [Int_assoc RS sym, PSP_stable]) 1);
   1.253 +qed "R_PSP_stable";
   1.254 +
   1.255 +goal thy
   1.256 +   "!!Acts. [| LeadsTo Init Acts A A'; stable Acts B |] \
   1.257 +\           ==> LeadsTo Init Acts (B Int A) (B Int A')";
   1.258 +by (asm_simp_tac (simpset() addsimps (R_PSP_stable::Int_ac)) 1);
   1.259 +qed "R_PSP_stable2";
   1.260 +
   1.261 +
   1.262 +goalw thy [LeadsTo_def]
   1.263 +   "!!Acts. [| LeadsTo Init Acts A A'; constrains Acts B B'; id: Acts |] \
   1.264 +\           ==> LeadsTo Init Acts (A Int B) ((A' Int B) Un (B' - B))";
   1.265 +by (dtac PSP 1);
   1.266 +by (etac constrains_reachable 1);
   1.267 +by (etac leadsTo_weaken 2);
   1.268 +by (ALLGOALS Blast_tac);
   1.269 +qed "R_PSP";
   1.270 +
   1.271 +goal thy
   1.272 +   "!!Acts. [| LeadsTo Init Acts A A'; constrains Acts B B'; id: Acts |] \
   1.273 +\           ==> LeadsTo Init Acts (B Int A) ((B Int A') Un (B' - B))";
   1.274 +by (asm_simp_tac (simpset() addsimps (R_PSP::Int_ac)) 1);
   1.275 +qed "R_PSP2";
   1.276 +
   1.277 +goalw thy [unless_def]
   1.278 +   "!!Acts. [| LeadsTo Init Acts A A'; unless Acts B B'; id: Acts |] \
   1.279 +\           ==> LeadsTo Init Acts (A Int B) ((A' Int B) Un B')";
   1.280 +by (dtac R_PSP 1);
   1.281 +by (assume_tac 1);
   1.282 +by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2);
   1.283 +by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2);
   1.284 +by (etac LeadsTo_Diff 2);
   1.285 +by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 2);
   1.286 +by Auto_tac;
   1.287 +qed "R_PSP_unless";
   1.288 +
   1.289 +
   1.290 +(*** Induction rules ***)
   1.291 +
   1.292 +(** Meta or object quantifier ????? **)
   1.293 +goalw thy [LeadsTo_def]
   1.294 +   "!!Acts. [| wf r;     \
   1.295 +\              ALL m. LeadsTo Init Acts (A Int f-``{m})                     \
   1.296 +\                                       ((A Int f-``(r^-1 ^^ {m})) Un B);   \
   1.297 +\              id: Acts |] \
   1.298 +\           ==> LeadsTo Init Acts A B";
   1.299 +by (etac leadsTo_wf_induct 1);
   1.300 +by (assume_tac 2);
   1.301 +by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
   1.302 +qed "LeadsTo_wf_induct";
   1.303 +
   1.304 +
   1.305 +goal thy
   1.306 +   "!!Acts. [| wf r;     \
   1.307 +\              ALL m:I. LeadsTo Init Acts (A Int f-``{m})                   \
   1.308 +\                                  ((A Int f-``(r^-1 ^^ {m})) Un B);   \
   1.309 +\              id: Acts |] \
   1.310 +\           ==> LeadsTo Init Acts A ((A - (f-``I)) Un B)";
   1.311 +by (etac LeadsTo_wf_induct 1);
   1.312 +by Safe_tac;
   1.313 +by (case_tac "m:I" 1);
   1.314 +by (blast_tac (claset() addIs [LeadsTo_weaken]) 1);
   1.315 +by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 1);
   1.316 +qed "R_bounded_induct";
   1.317 +
   1.318 +
   1.319 +goal thy
   1.320 +   "!!Acts. [| ALL m. LeadsTo Init Acts (A Int f-``{m})                     \
   1.321 +\                                  ((A Int f-``(lessThan m)) Un B);   \
   1.322 +\              id: Acts |] \
   1.323 +\           ==> LeadsTo Init Acts A B";
   1.324 +by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
   1.325 +by (assume_tac 2);
   1.326 +by (Asm_simp_tac 1);
   1.327 +qed "R_lessThan_induct";
   1.328 +
   1.329 +goal thy
   1.330 +   "!!Acts. [| ALL m:(greaterThan l). LeadsTo Init Acts (A Int f-``{m})   \
   1.331 +\                                        ((A Int f-``(lessThan m)) Un B);   \
   1.332 +\              id: Acts |] \
   1.333 +\           ==> LeadsTo Init Acts A ((A Int (f-``(atMost l))) Un B)";
   1.334 +by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
   1.335 +by (rtac (wf_less_than RS R_bounded_induct) 1);
   1.336 +by (assume_tac 2);
   1.337 +by (Asm_simp_tac 1);
   1.338 +qed "R_lessThan_bounded_induct";
   1.339 +
   1.340 +goal thy
   1.341 +   "!!Acts. [| ALL m:(lessThan l). LeadsTo Init Acts (A Int f-``{m})   \
   1.342 +\                                    ((A Int f-``(greaterThan m)) Un B);   \
   1.343 +\              id: Acts |] \
   1.344 +\           ==> LeadsTo Init Acts A ((A Int (f-``(atLeast l))) Un B)";
   1.345 +by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
   1.346 +    (wf_less_than RS wf_inv_image RS LeadsTo_wf_induct) 1);
   1.347 +by (assume_tac 2);
   1.348 +by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
   1.349 +by (Clarify_tac 1);
   1.350 +by (case_tac "m<l" 1);
   1.351 +by (blast_tac (claset() addIs [not_leE, subset_imp_LeadsTo]) 2);
   1.352 +by (blast_tac (claset() addIs [LeadsTo_weaken_R, diff_less_mono2]) 1);
   1.353 +qed "R_greaterThan_bounded_induct";
   1.354 +
   1.355 +
   1.356 +
   1.357 +(*** Completion: Binary and General Finite versions ***)
   1.358 +
   1.359 +goalw thy [LeadsTo_def]
   1.360 +   "!!Acts. [| LeadsTo Init Acts A A';  stable Acts A';   \
   1.361 +\              LeadsTo Init Acts B B';  stable Acts B';  id: Acts |] \
   1.362 +\           ==> LeadsTo Init Acts (A Int B) (A' Int B')";
   1.363 +by (blast_tac (claset() addIs [stable_completion RS leadsTo_weaken] 
   1.364 +                        addSIs [stable_Int, stable_reachable]) 1);
   1.365 +qed "R_stable_completion";
   1.366 +
   1.367 +
   1.368 +goal thy
   1.369 +   "!!Acts. [| finite I;  id: Acts |]                     \
   1.370 +\           ==> (ALL i:I. LeadsTo Init Acts (A i) (A' i)) -->  \
   1.371 +\               (ALL i:I. stable Acts (A' i)) -->         \
   1.372 +\               LeadsTo Init Acts (INT i:I. A i) (INT i:I. A' i)";
   1.373 +by (etac finite_induct 1);
   1.374 +by (Asm_simp_tac 1);
   1.375 +by (asm_simp_tac 
   1.376 +    (simpset() addsimps [R_stable_completion, stable_def, 
   1.377 +			 ball_constrains_INT]) 1);
   1.378 +qed_spec_mp "R_finite_stable_completion";
   1.379 +
   1.380 +
   1.381 +goalw thy [LeadsTo_def]
   1.382 + "!!Acts. [| LeadsTo Init Acts A (A' Un C);  constrains Acts A' (A' Un C); \
   1.383 +\            LeadsTo Init Acts B (B' Un C);  constrains Acts B' (B' Un C); \
   1.384 +\            id: Acts |] \
   1.385 +\         ==> LeadsTo Init Acts (A Int B) ((A' Int B') Un C)";
   1.386 +
   1.387 +by (full_simp_tac (simpset() addsimps [Int_Un_distrib]) 1);
   1.388 +by (dtac completion 1);
   1.389 +by (assume_tac 2);
   1.390 +by (ALLGOALS 
   1.391 +    (asm_simp_tac 
   1.392 +     (simpset() addsimps [constrains_reachable, Int_Un_distrib RS sym])));
   1.393 +by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
   1.394 +qed "R_completion";
   1.395 +
   1.396 +
   1.397 +goal thy
   1.398 +   "!!Acts. [| finite I;  id: Acts |] \
   1.399 +\           ==> (ALL i:I. LeadsTo Init Acts (A i) (A' i Un C)) -->  \
   1.400 +\               (ALL i:I. constrains Acts (A' i) (A' i Un C)) --> \
   1.401 +\               LeadsTo Init Acts (INT i:I. A i) ((INT i:I. A' i) Un C)";
   1.402 +by (etac finite_induct 1);
   1.403 +by (ALLGOALS Asm_simp_tac);
   1.404 +by (Clarify_tac 1);
   1.405 +by (dtac ball_constrains_INT 1);
   1.406 +by (asm_full_simp_tac (simpset() addsimps [R_completion]) 1); 
   1.407 +qed "R_finite_completion";
   1.408 +