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