src/ZF/UNITY/Constrains.thy
author wenzelm
Sat Dec 14 17:28:05 2013 +0100 (2013-12-14)
changeset 54742 7a86358a3c0b
parent 51717 9e7d1c139569
child 57945 cacb00a569e0
permissions -rw-r--r--
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;
     1 (*  Title:      ZF/UNITY/Constrains.thy
     2     Author:     Sidi O Ehmety, Computer Laboratory
     3     Copyright   2001  University of Cambridge
     4 *)
     5 
     6 header{*Weak Safety Properties*}
     7 
     8 theory Constrains
     9 imports UNITY
    10 begin
    11 
    12 consts traces :: "[i, i] => i"
    13   (* Initial states and program => (final state, reversed trace to it)... 
    14       the domain may also be state*list(state) *)
    15 inductive 
    16   domains 
    17      "traces(init, acts)" <=
    18          "(init \<union> (\<Union>act\<in>acts. field(act)))*list(\<Union>act\<in>acts. field(act))"
    19   intros 
    20          (*Initial trace is empty*)
    21     Init: "s: init ==> <s,[]> \<in> traces(init,acts)"
    22 
    23     Acts: "[| act:acts;  <s,evs> \<in> traces(init,acts);  <s,s'>: act |]
    24            ==> <s', Cons(s,evs)> \<in> traces(init, acts)"
    25   
    26   type_intros list.intros UnI1 UnI2 UN_I fieldI2 fieldI1
    27 
    28 
    29 consts reachable :: "i=>i"
    30 inductive
    31   domains
    32   "reachable(F)" \<subseteq> "Init(F) \<union> (\<Union>act\<in>Acts(F). field(act))"
    33   intros 
    34     Init: "s:Init(F) ==> s:reachable(F)"
    35 
    36     Acts: "[| act: Acts(F);  s:reachable(F);  <s,s'>: act |]
    37            ==> s':reachable(F)"
    38 
    39   type_intros UnI1 UnI2 fieldI2 UN_I
    40 
    41   
    42 definition
    43   Constrains :: "[i,i] => i"  (infixl "Co" 60)  where
    44   "A Co B == {F:program. F:(reachable(F) \<inter> A) co B}"
    45 
    46 definition
    47   op_Unless  :: "[i, i] => i"  (infixl "Unless" 60)  where
    48   "A Unless B == (A-B) Co (A \<union> B)"
    49 
    50 definition
    51   Stable     :: "i => i"  where
    52   "Stable(A) == A Co A"
    53 
    54 definition
    55   (*Always is the weak form of "invariant"*)
    56   Always :: "i => i"  where
    57   "Always(A) == initially(A) \<inter> Stable(A)"
    58 
    59 
    60 (*** traces and reachable ***)
    61 
    62 lemma reachable_type: "reachable(F) \<subseteq> state"
    63 apply (cut_tac F = F in Init_type)
    64 apply (cut_tac F = F in Acts_type)
    65 apply (cut_tac F = F in reachable.dom_subset, blast)
    66 done
    67 
    68 lemma st_set_reachable: "st_set(reachable(F))"
    69 apply (unfold st_set_def)
    70 apply (rule reachable_type)
    71 done
    72 declare st_set_reachable [iff]
    73 
    74 lemma reachable_Int_state: "reachable(F) \<inter> state = reachable(F)"
    75 by (cut_tac reachable_type, auto)
    76 declare reachable_Int_state [iff]
    77 
    78 lemma state_Int_reachable: "state \<inter> reachable(F) = reachable(F)"
    79 by (cut_tac reachable_type, auto)
    80 declare state_Int_reachable [iff]
    81 
    82 lemma reachable_equiv_traces: 
    83 "F \<in> program ==> reachable(F)={s \<in> state. \<exists>evs. <s,evs>:traces(Init(F), Acts(F))}"
    84 apply (rule equalityI, safe)
    85 apply (blast dest: reachable_type [THEN subsetD])
    86 apply (erule_tac [2] traces.induct)
    87 apply (erule reachable.induct)
    88 apply (blast intro: reachable.intros traces.intros)+
    89 done
    90 
    91 lemma Init_into_reachable: "Init(F) \<subseteq> reachable(F)"
    92 by (blast intro: reachable.intros)
    93 
    94 lemma stable_reachable: "[| F \<in> program; G \<in> program;  
    95     Acts(G) \<subseteq> Acts(F)  |] ==> G \<in> stable(reachable(F))"
    96 apply (blast intro: stableI constrainsI st_setI
    97              reachable_type [THEN subsetD] reachable.intros)
    98 done
    99 
   100 declare stable_reachable [intro!]
   101 declare stable_reachable [simp]
   102 
   103 (*The set of all reachable states is an invariant...*)
   104 lemma invariant_reachable: 
   105    "F \<in> program ==> F \<in> invariant(reachable(F))"
   106 apply (unfold invariant_def initially_def)
   107 apply (blast intro: reachable_type [THEN subsetD] reachable.intros)
   108 done
   109 
   110 (*...in fact the strongest invariant!*)
   111 lemma invariant_includes_reachable: "F \<in> invariant(A) ==> reachable(F) \<subseteq> A"
   112 apply (cut_tac F = F in Acts_type)
   113 apply (cut_tac F = F in Init_type)
   114 apply (cut_tac F = F in reachable_type)
   115 apply (simp (no_asm_use) add: stable_def constrains_def invariant_def initially_def)
   116 apply (rule subsetI)
   117 apply (erule reachable.induct)
   118 apply (blast intro: reachable.intros)+
   119 done
   120 
   121 (*** Co ***)
   122 
   123 lemma constrains_reachable_Int: "F \<in> B co B'==>F:(reachable(F) \<inter> B) co (reachable(F) \<inter> B')"
   124 apply (frule constrains_type [THEN subsetD])
   125 apply (frule stable_reachable [OF _ _ subset_refl])
   126 apply (simp_all add: stable_def constrains_Int)
   127 done
   128 
   129 (*Resembles the previous definition of Constrains*)
   130 lemma Constrains_eq_constrains: 
   131 "A Co B = {F \<in> program. F:(reachable(F) \<inter> A) co (reachable(F)  \<inter>  B)}"
   132 apply (unfold Constrains_def)
   133 apply (blast dest: constrains_reachable_Int constrains_type [THEN subsetD]
   134              intro: constrains_weaken)
   135 done
   136 
   137 lemmas Constrains_def2 = Constrains_eq_constrains [THEN eq_reflection]
   138 
   139 lemma constrains_imp_Constrains: "F \<in> A co A' ==> F \<in> A Co A'"
   140 apply (unfold Constrains_def)
   141 apply (blast intro: constrains_weaken_L dest: constrainsD2)
   142 done
   143 
   144 lemma ConstrainsI: 
   145     "[|!!act s s'. [| act \<in> Acts(F); <s,s'>:act; s \<in> A |] ==> s':A'; 
   146        F \<in> program|]
   147      ==> F \<in> A Co A'"
   148 apply (auto simp add: Constrains_def constrains_def st_set_def)
   149 apply (blast dest: reachable_type [THEN subsetD])
   150 done
   151 
   152 lemma Constrains_type: 
   153  "A Co B \<subseteq> program"
   154 apply (unfold Constrains_def, blast)
   155 done
   156 
   157 lemma Constrains_empty: "F \<in> 0 Co B \<longleftrightarrow> F \<in> program"
   158 by (auto dest: Constrains_type [THEN subsetD]
   159             intro: constrains_imp_Constrains)
   160 declare Constrains_empty [iff]
   161 
   162 lemma Constrains_state: "F \<in> A Co state \<longleftrightarrow> F \<in> program"
   163 apply (unfold Constrains_def)
   164 apply (auto dest: Constrains_type [THEN subsetD] intro: constrains_imp_Constrains)
   165 done
   166 declare Constrains_state [iff]
   167 
   168 lemma Constrains_weaken_R: 
   169         "[| F \<in> A Co A'; A'<=B' |] ==> F \<in> A Co B'"
   170 apply (unfold Constrains_def2)
   171 apply (blast intro: constrains_weaken_R)
   172 done
   173 
   174 lemma Constrains_weaken_L: 
   175     "[| F \<in> A Co A'; B<=A |] ==> F \<in> B Co A'"
   176 apply (unfold Constrains_def2)
   177 apply (blast intro: constrains_weaken_L st_set_subset)
   178 done
   179 
   180 lemma Constrains_weaken: 
   181    "[| F \<in> A Co A'; B<=A; A'<=B' |] ==> F \<in> B Co B'"
   182 apply (unfold Constrains_def2)
   183 apply (blast intro: constrains_weaken st_set_subset)
   184 done
   185 
   186 (** Union **)
   187 lemma Constrains_Un: 
   188     "[| F \<in> A Co A'; F \<in> B Co B' |] ==> F \<in> (A \<union> B) Co (A' \<union> B')"
   189 apply (unfold Constrains_def2, auto)
   190 apply (simp add: Int_Un_distrib)
   191 apply (blast intro: constrains_Un)
   192 done
   193 
   194 lemma Constrains_UN: 
   195     "[|(!!i. i \<in> I==>F \<in> A(i) Co A'(i)); F \<in> program|] 
   196      ==> F:(\<Union>i \<in> I. A(i)) Co (\<Union>i \<in> I. A'(i))"
   197 by (auto intro: constrains_UN simp del: UN_simps 
   198          simp add: Constrains_def2 Int_UN_distrib)
   199 
   200 
   201 (** Intersection **)
   202 
   203 lemma Constrains_Int: 
   204     "[| F \<in> A Co A'; F \<in> B Co B'|]==> F:(A \<inter> B) Co (A' \<inter> B')"
   205 apply (unfold Constrains_def)
   206 apply (subgoal_tac "reachable (F) \<inter> (A \<inter> B) = (reachable (F) \<inter> A) \<inter> (reachable (F) \<inter> B) ")
   207 apply (auto intro: constrains_Int)
   208 done
   209 
   210 lemma Constrains_INT: 
   211     "[| (!!i. i \<in> I ==>F \<in> A(i) Co A'(i)); F \<in> program  |]  
   212      ==> F:(\<Inter>i \<in> I. A(i)) Co (\<Inter>i \<in> I. A'(i))"
   213 apply (simp (no_asm_simp) del: INT_simps add: Constrains_def INT_extend_simps)
   214 apply (rule constrains_INT)
   215 apply (auto simp add: Constrains_def)
   216 done
   217 
   218 lemma Constrains_imp_subset: "F \<in> A Co A' ==> reachable(F) \<inter> A \<subseteq> A'"
   219 apply (unfold Constrains_def)
   220 apply (blast dest: constrains_imp_subset)
   221 done
   222 
   223 lemma Constrains_trans: 
   224  "[| F \<in> A Co B; F \<in> B Co C |] ==> F \<in> A Co C"
   225 apply (unfold Constrains_def2)
   226 apply (blast intro: constrains_trans constrains_weaken)
   227 done
   228 
   229 lemma Constrains_cancel: 
   230 "[| F \<in> A Co (A' \<union> B); F \<in> B Co B' |] ==> F \<in> A Co (A' \<union> B')"
   231 apply (unfold Constrains_def2)
   232 apply (simp (no_asm_use) add: Int_Un_distrib)
   233 apply (blast intro: constrains_cancel)
   234 done
   235 
   236 (*** Stable ***)
   237 (* Useful because there's no Stable_weaken.  [Tanja Vos] *)
   238 
   239 lemma stable_imp_Stable: 
   240 "F \<in> stable(A) ==> F \<in> Stable(A)"
   241 
   242 apply (unfold stable_def Stable_def)
   243 apply (erule constrains_imp_Constrains)
   244 done
   245 
   246 lemma Stable_eq: "[| F \<in> Stable(A); A = B |] ==> F \<in> Stable(B)"
   247 by blast
   248 
   249 lemma Stable_eq_stable: 
   250 "F \<in> Stable(A) \<longleftrightarrow>  (F \<in> stable(reachable(F) \<inter> A))"
   251 apply (auto dest: constrainsD2 simp add: Stable_def stable_def Constrains_def2)
   252 done
   253 
   254 lemma StableI: "F \<in> A Co A ==> F \<in> Stable(A)"
   255 by (unfold Stable_def, assumption)
   256 
   257 lemma StableD: "F \<in> Stable(A) ==> F \<in> A Co A"
   258 by (unfold Stable_def, assumption)
   259 
   260 lemma Stable_Un: 
   261     "[| F \<in> Stable(A); F \<in> Stable(A') |] ==> F \<in> Stable(A \<union> A')"
   262 apply (unfold Stable_def)
   263 apply (blast intro: Constrains_Un)
   264 done
   265 
   266 lemma Stable_Int: 
   267     "[| F \<in> Stable(A); F \<in> Stable(A') |] ==> F \<in> Stable (A \<inter> A')"
   268 apply (unfold Stable_def)
   269 apply (blast intro: Constrains_Int)
   270 done
   271 
   272 lemma Stable_Constrains_Un: 
   273     "[| F \<in> Stable(C); F \<in> A Co (C \<union> A') |]    
   274      ==> F \<in> (C \<union> A) Co (C \<union> A')"
   275 apply (unfold Stable_def)
   276 apply (blast intro: Constrains_Un [THEN Constrains_weaken_R])
   277 done
   278 
   279 lemma Stable_Constrains_Int: 
   280     "[| F \<in> Stable(C); F \<in> (C \<inter> A) Co A' |]    
   281      ==> F \<in> (C \<inter> A) Co (C \<inter> A')"
   282 apply (unfold Stable_def)
   283 apply (blast intro: Constrains_Int [THEN Constrains_weaken])
   284 done
   285 
   286 lemma Stable_UN: 
   287     "[| (!!i. i \<in> I ==> F \<in> Stable(A(i))); F \<in> program |]
   288      ==> F \<in> Stable (\<Union>i \<in> I. A(i))"
   289 apply (simp add: Stable_def)
   290 apply (blast intro: Constrains_UN)
   291 done
   292 
   293 lemma Stable_INT: 
   294     "[|(!!i. i \<in> I ==> F \<in> Stable(A(i))); F \<in> program |]
   295      ==> F \<in> Stable (\<Inter>i \<in> I. A(i))"
   296 apply (simp add: Stable_def)
   297 apply (blast intro: Constrains_INT)
   298 done
   299 
   300 lemma Stable_reachable: "F \<in> program ==>F \<in> Stable (reachable(F))"
   301 apply (simp (no_asm_simp) add: Stable_eq_stable Int_absorb)
   302 done
   303 
   304 lemma Stable_type: "Stable(A) \<subseteq> program"
   305 apply (unfold Stable_def)
   306 apply (rule Constrains_type)
   307 done
   308 
   309 (*** The Elimination Theorem.  The "free" m has become universally quantified!
   310      Should the premise be !!m instead of \<forall>m ?  Would make it harder to use
   311      in forward proof. ***)
   312 
   313 lemma Elimination: 
   314     "[| \<forall>m \<in> M. F \<in> ({s \<in> A. x(s) = m}) Co (B(m)); F \<in> program |]  
   315      ==> F \<in> ({s \<in> A. x(s):M}) Co (\<Union>m \<in> M. B(m))"
   316 apply (unfold Constrains_def, auto)
   317 apply (rule_tac A1 = "reachable (F) \<inter> A" 
   318         in UNITY.elimination [THEN constrains_weaken_L])
   319 apply (auto intro: constrains_weaken_L)
   320 done
   321 
   322 (* As above, but for the special case of A=state *)
   323 lemma Elimination2: 
   324  "[| \<forall>m \<in> M. F \<in> {s \<in> state. x(s) = m} Co B(m); F \<in> program |]  
   325      ==> F \<in> {s \<in> state. x(s):M} Co (\<Union>m \<in> M. B(m))"
   326 apply (blast intro: Elimination)
   327 done
   328 
   329 (** Unless **)
   330 
   331 lemma Unless_type: "A Unless B <=program"
   332 apply (unfold op_Unless_def)
   333 apply (rule Constrains_type)
   334 done
   335 
   336 (*** Specialized laws for handling Always ***)
   337 
   338 (** Natural deduction rules for "Always A" **)
   339 
   340 lemma AlwaysI: 
   341 "[| Init(F)<=A;  F \<in> Stable(A) |] ==> F \<in> Always(A)"
   342 
   343 apply (unfold Always_def initially_def)
   344 apply (frule Stable_type [THEN subsetD], auto)
   345 done
   346 
   347 lemma AlwaysD: "F \<in> Always(A) ==> Init(F)<=A & F \<in> Stable(A)"
   348 by (simp add: Always_def initially_def)
   349 
   350 lemmas AlwaysE = AlwaysD [THEN conjE]
   351 lemmas Always_imp_Stable = AlwaysD [THEN conjunct2]
   352 
   353 (*The set of all reachable states is Always*)
   354 lemma Always_includes_reachable: "F \<in> Always(A) ==> reachable(F) \<subseteq> A"
   355 apply (simp (no_asm_use) add: Stable_def Constrains_def constrains_def Always_def initially_def)
   356 apply (rule subsetI)
   357 apply (erule reachable.induct)
   358 apply (blast intro: reachable.intros)+
   359 done
   360 
   361 lemma invariant_imp_Always: 
   362      "F \<in> invariant(A) ==> F \<in> Always(A)"
   363 apply (unfold Always_def invariant_def Stable_def stable_def)
   364 apply (blast intro: constrains_imp_Constrains)
   365 done
   366 
   367 lemmas Always_reachable = invariant_reachable [THEN invariant_imp_Always]
   368 
   369 lemma Always_eq_invariant_reachable: "Always(A) = {F \<in> program. F \<in> invariant(reachable(F) \<inter> A)}"
   370 apply (simp (no_asm) add: Always_def invariant_def Stable_def Constrains_def2 stable_def initially_def)
   371 apply (rule equalityI, auto) 
   372 apply (blast intro: reachable.intros reachable_type)
   373 done
   374 
   375 (*the RHS is the traditional definition of the "always" operator*)
   376 lemma Always_eq_includes_reachable: "Always(A) = {F \<in> program. reachable(F) \<subseteq> A}"
   377 apply (rule equalityI, safe)
   378 apply (auto dest: invariant_includes_reachable 
   379    simp add: subset_Int_iff invariant_reachable Always_eq_invariant_reachable)
   380 done
   381 
   382 lemma Always_type: "Always(A) \<subseteq> program"
   383 by (unfold Always_def initially_def, auto)
   384 
   385 lemma Always_state_eq: "Always(state) = program"
   386 apply (rule equalityI)
   387 apply (auto dest: Always_type [THEN subsetD] reachable_type [THEN subsetD]
   388             simp add: Always_eq_includes_reachable)
   389 done
   390 declare Always_state_eq [simp]
   391 
   392 lemma state_AlwaysI: "F \<in> program ==> F \<in> Always(state)"
   393 by (auto dest: reachable_type [THEN subsetD]
   394             simp add: Always_eq_includes_reachable)
   395 
   396 lemma Always_eq_UN_invariant: "st_set(A) ==> Always(A) = (\<Union>I \<in> Pow(A). invariant(I))"
   397 apply (simp (no_asm) add: Always_eq_includes_reachable)
   398 apply (rule equalityI, auto) 
   399 apply (blast intro: invariantI rev_subsetD [OF _ Init_into_reachable] 
   400                     rev_subsetD [OF _ invariant_includes_reachable]  
   401              dest: invariant_type [THEN subsetD])+
   402 done
   403 
   404 lemma Always_weaken: "[| F \<in> Always(A); A \<subseteq> B |] ==> F \<in> Always(B)"
   405 by (auto simp add: Always_eq_includes_reachable)
   406 
   407 
   408 (*** "Co" rules involving Always ***)
   409 lemmas Int_absorb2 = subset_Int_iff [unfolded iff_def, THEN conjunct1, THEN mp]
   410 
   411 lemma Always_Constrains_pre: "F \<in> Always(I) ==> (F:(I \<inter> A) Co A') \<longleftrightarrow> (F \<in> A Co A')"
   412 apply (simp (no_asm_simp) add: Always_includes_reachable [THEN Int_absorb2] Constrains_def Int_assoc [symmetric])
   413 done
   414 
   415 lemma Always_Constrains_post: "F \<in> Always(I) ==> (F \<in> A Co (I \<inter> A')) \<longleftrightarrow>(F \<in> A Co A')"
   416 apply (simp (no_asm_simp) add: Always_includes_reachable [THEN Int_absorb2] Constrains_eq_constrains Int_assoc [symmetric])
   417 done
   418 
   419 lemma Always_ConstrainsI: "[| F \<in> Always(I);  F \<in> (I \<inter> A) Co A' |] ==> F \<in> A Co A'"
   420 by (blast intro: Always_Constrains_pre [THEN iffD1])
   421 
   422 (* [| F \<in> Always(I);  F \<in> A Co A' |] ==> F \<in> A Co (I \<inter> A') *)
   423 lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2]
   424 
   425 (*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
   426 lemma Always_Constrains_weaken: 
   427 "[|F \<in> Always(C); F \<in> A Co A'; C \<inter> B<=A; C \<inter> A'<=B'|]==>F \<in> B Co B'"
   428 apply (rule Always_ConstrainsI)
   429 apply (drule_tac [2] Always_ConstrainsD, simp_all) 
   430 apply (blast intro: Constrains_weaken)
   431 done
   432 
   433 (** Conjoining Always properties **)
   434 lemma Always_Int_distrib: "Always(A \<inter> B) = Always(A) \<inter> Always(B)"
   435 by (auto simp add: Always_eq_includes_reachable)
   436 
   437 (* the premise i \<in> I is need since \<Inter>is formally not defined for I=0 *)
   438 lemma Always_INT_distrib: "i \<in> I==>Always(\<Inter>i \<in> I. A(i)) = (\<Inter>i \<in> I. Always(A(i)))"
   439 apply (rule equalityI)
   440 apply (auto simp add: Inter_iff Always_eq_includes_reachable)
   441 done
   442 
   443 
   444 lemma Always_Int_I: "[| F \<in> Always(A);  F \<in> Always(B) |] ==> F \<in> Always(A \<inter> B)"
   445 apply (simp (no_asm_simp) add: Always_Int_distrib)
   446 done
   447 
   448 (*Allows a kind of "implication introduction"*)
   449 lemma Always_Diff_Un_eq: "[| F \<in> Always(A) |] ==> (F \<in> Always(C-A \<union> B)) \<longleftrightarrow> (F \<in> Always(B))"
   450 by (auto simp add: Always_eq_includes_reachable)
   451 
   452 (*Delete the nearest invariance assumption (which will be the second one
   453   used by Always_Int_I) *)
   454 lemmas Always_thin = thin_rl [of "F \<in> Always(A)"]
   455 
   456 ML
   457 {*
   458 (*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
   459 val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin};
   460 
   461 (*Combines a list of invariance THEOREMS into one.*)
   462 val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I});
   463 
   464 (*To allow expansion of the program's definition when appropriate*)
   465 structure Program_Defs = Named_Thms
   466 (
   467   val name = @{binding program}
   468   val description = "program definitions"
   469 );
   470 
   471 (*proves "co" properties when the program is specified*)
   472 
   473 fun constrains_tac ctxt =
   474    SELECT_GOAL
   475       (EVERY [REPEAT (Always_Int_tac 1),
   476               REPEAT (etac @{thm Always_ConstrainsI} 1
   477                       ORELSE
   478                       resolve_tac [@{thm StableI}, @{thm stableI},
   479                                    @{thm constrains_imp_Constrains}] 1),
   480               rtac @{thm constrainsI} 1,
   481               (* Three subgoals *)
   482               rewrite_goal_tac ctxt [@{thm st_set_def}] 3,
   483               REPEAT (force_tac ctxt 2),
   484               full_simp_tac (ctxt addsimps (Program_Defs.get ctxt)) 1,
   485               ALLGOALS (clarify_tac ctxt),
   486               REPEAT (FIRSTGOAL (etac @{thm disjE})),
   487               ALLGOALS (clarify_tac ctxt),
   488               REPEAT (FIRSTGOAL (etac @{thm disjE})),
   489               ALLGOALS (clarify_tac ctxt),
   490               ALLGOALS (asm_full_simp_tac ctxt),
   491               ALLGOALS (clarify_tac ctxt)]);
   492 
   493 (*For proving invariants*)
   494 fun always_tac ctxt i =
   495     rtac @{thm AlwaysI} i THEN force_tac ctxt i THEN constrains_tac ctxt i;
   496 *}
   497 
   498 setup Program_Defs.setup
   499 
   500 method_setup safety = {*
   501   Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
   502   "for proving safety properties"
   503 
   504 method_setup always = {*
   505   Scan.succeed (SIMPLE_METHOD' o always_tac) *}
   506   "for proving invariants"
   507 
   508 end