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