src/HOL/UNITY/Constrains.thy
author paulson
Thu Jan 30 18:08:09 2003 +0100 (2003-01-30)
changeset 13797 baefae13ad37
parent 6823 97babc436a41
child 13798 4c1a53627500
permissions -rw-r--r--
conversion of UNITY theories to new-style
paulson@5313
     1
(*  Title:      HOL/UNITY/Constrains
paulson@5313
     2
    ID:         $Id$
paulson@5313
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5313
     4
    Copyright   1998  University of Cambridge
paulson@5313
     5
paulson@13797
     6
Weak safety relations: restricted to the set of reachable states.
paulson@5313
     7
*)
paulson@5313
     8
paulson@13797
     9
theory Constrains = UNITY:
paulson@6535
    10
paulson@6535
    11
consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
paulson@6535
    12
paulson@6535
    13
  (*Initial states and program => (final state, reversed trace to it)...
paulson@6535
    14
    Arguments MUST be curried in an inductive definition*)
paulson@6535
    15
paulson@6535
    16
inductive "traces init acts"  
paulson@13797
    17
  intros 
paulson@6535
    18
         (*Initial trace is empty*)
paulson@13797
    19
    Init:  "s: init ==> (s,[]) : traces init acts"
paulson@6535
    20
paulson@13797
    21
    Acts:  "[| act: acts;  (s,evs) : traces init acts;  (s,s'): act |]
paulson@13797
    22
	    ==> (s', s#evs) : traces init acts"
paulson@6535
    23
paulson@6535
    24
paulson@6535
    25
consts reachable :: "'a program => 'a set"
paulson@6535
    26
paulson@6535
    27
inductive "reachable F"
paulson@13797
    28
  intros 
paulson@13797
    29
    Init:  "s: Init F ==> s : reachable F"
paulson@5313
    30
paulson@13797
    31
    Acts:  "[| act: Acts F;  s : reachable F;  (s,s'): act |]
paulson@13797
    32
	    ==> s' : reachable F"
paulson@6536
    33
paulson@13797
    34
constdefs
paulson@13797
    35
  Constrains :: "['a set, 'a set] => 'a program set"  (infixl "Co" 60)
paulson@6575
    36
    "A Co B == {F. F : (reachable F Int A)  co  B}"
paulson@6536
    37
paulson@13797
    38
  Unless  :: "['a set, 'a set] => 'a program set"     (infixl "Unless" 60)
paulson@6536
    39
    "A Unless B == (A-B) Co (A Un B)"
paulson@6536
    40
paulson@5648
    41
  Stable     :: "'a set => 'a program set"
paulson@6536
    42
    "Stable A == A Co A"
paulson@5313
    43
paulson@6570
    44
  (*Always is the weak form of "invariant"*)
paulson@6570
    45
  Always :: "'a set => 'a program set"
paulson@6570
    46
    "Always A == {F. Init F <= A} Int Stable A"
paulson@5313
    47
paulson@5784
    48
  (*Polymorphic in both states and the meaning of <= *)
paulson@6705
    49
  Increasing :: "['a => 'b::{order}] => 'a program set"
paulson@5784
    50
    "Increasing f == INT z. Stable {s. z <= f s}"
paulson@5784
    51
paulson@13797
    52
paulson@13797
    53
(*** traces and reachable ***)
paulson@13797
    54
paulson@13797
    55
lemma reachable_equiv_traces:
paulson@13797
    56
     "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}"
paulson@13797
    57
apply safe
paulson@13797
    58
apply (erule_tac [2] traces.induct)
paulson@13797
    59
apply (erule reachable.induct)
paulson@13797
    60
apply (blast intro: reachable.intros traces.intros)+
paulson@13797
    61
done
paulson@13797
    62
paulson@13797
    63
lemma Init_subset_reachable: "Init F <= reachable F"
paulson@13797
    64
by (blast intro: reachable.intros)
paulson@13797
    65
paulson@13797
    66
lemma stable_reachable [intro!,simp]:
paulson@13797
    67
     "Acts G <= Acts F ==> G : stable (reachable F)"
paulson@13797
    68
by (blast intro: stableI constrainsI reachable.intros)
paulson@13797
    69
paulson@13797
    70
(*The set of all reachable states is an invariant...*)
paulson@13797
    71
lemma invariant_reachable: "F : invariant (reachable F)"
paulson@13797
    72
apply (simp add: invariant_def)
paulson@13797
    73
apply (blast intro: reachable.intros)
paulson@13797
    74
done
paulson@13797
    75
paulson@13797
    76
(*...in fact the strongest invariant!*)
paulson@13797
    77
lemma invariant_includes_reachable: "F : invariant A ==> reachable F <= A"
paulson@13797
    78
apply (simp add: stable_def constrains_def invariant_def)
paulson@13797
    79
apply (rule subsetI)
paulson@13797
    80
apply (erule reachable.induct)
paulson@13797
    81
apply (blast intro: reachable.intros)+
paulson@13797
    82
done
paulson@13797
    83
paulson@13797
    84
paulson@13797
    85
(*** Co ***)
paulson@13797
    86
paulson@13797
    87
(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*)
paulson@13797
    88
lemmas constrains_reachable_Int =  
paulson@13797
    89
    subset_refl [THEN stable_reachable [unfolded stable_def], 
paulson@13797
    90
                 THEN constrains_Int, standard]
paulson@13797
    91
paulson@13797
    92
(*Resembles the previous definition of Constrains*)
paulson@13797
    93
lemma Constrains_eq_constrains: 
paulson@13797
    94
     "A Co B = {F. F : (reachable F  Int  A) co (reachable F  Int  B)}"
paulson@13797
    95
apply (unfold Constrains_def)
paulson@13797
    96
apply (blast dest: constrains_reachable_Int intro: constrains_weaken)
paulson@13797
    97
done
paulson@13797
    98
paulson@13797
    99
lemma constrains_imp_Constrains: "F : A co A' ==> F : A Co A'"
paulson@13797
   100
apply (unfold Constrains_def)
paulson@13797
   101
apply (blast intro: constrains_weaken_L)
paulson@13797
   102
done
paulson@13797
   103
paulson@13797
   104
lemma stable_imp_Stable: "F : stable A ==> F : Stable A"
paulson@13797
   105
apply (unfold stable_def Stable_def)
paulson@13797
   106
apply (erule constrains_imp_Constrains)
paulson@13797
   107
done
paulson@13797
   108
paulson@13797
   109
lemma ConstrainsI: 
paulson@13797
   110
    "(!!act s s'. [| act: Acts F;  (s,s') : act;  s: A |] ==> s': A')  
paulson@13797
   111
     ==> F : A Co A'"
paulson@13797
   112
apply (rule constrains_imp_Constrains)
paulson@13797
   113
apply (blast intro: constrainsI)
paulson@13797
   114
done
paulson@13797
   115
paulson@13797
   116
lemma Constrains_empty [iff]: "F : {} Co B"
paulson@13797
   117
by (unfold Constrains_def constrains_def, blast)
paulson@13797
   118
paulson@13797
   119
lemma Constrains_UNIV [iff]: "F : A Co UNIV"
paulson@13797
   120
by (blast intro: ConstrainsI)
paulson@13797
   121
paulson@13797
   122
lemma Constrains_weaken_R: 
paulson@13797
   123
    "[| F : A Co A'; A'<=B' |] ==> F : A Co B'"
paulson@13797
   124
apply (unfold Constrains_def)
paulson@13797
   125
apply (blast intro: constrains_weaken_R)
paulson@13797
   126
done
paulson@13797
   127
paulson@13797
   128
lemma Constrains_weaken_L: 
paulson@13797
   129
    "[| F : A Co A'; B<=A |] ==> F : B Co A'"
paulson@13797
   130
apply (unfold Constrains_def)
paulson@13797
   131
apply (blast intro: constrains_weaken_L)
paulson@13797
   132
done
paulson@13797
   133
paulson@13797
   134
lemma Constrains_weaken: 
paulson@13797
   135
   "[| F : A Co A'; B<=A; A'<=B' |] ==> F : B Co B'"
paulson@13797
   136
apply (unfold Constrains_def)
paulson@13797
   137
apply (blast intro: constrains_weaken)
paulson@13797
   138
done
paulson@13797
   139
paulson@13797
   140
(** Union **)
paulson@13797
   141
paulson@13797
   142
lemma Constrains_Un: 
paulson@13797
   143
    "[| F : A Co A'; F : B Co B' |] ==> F : (A Un B) Co (A' Un B')"
paulson@13797
   144
apply (unfold Constrains_def)
paulson@13797
   145
apply (blast intro: constrains_Un [THEN constrains_weaken])
paulson@13797
   146
done
paulson@13797
   147
paulson@13797
   148
lemma Constrains_UN: 
paulson@13797
   149
  assumes Co: "!!i. i:I ==> F : (A i) Co (A' i)"
paulson@13797
   150
  shows "F : (UN i:I. A i) Co (UN i:I. A' i)"
paulson@13797
   151
apply (unfold Constrains_def)
paulson@13797
   152
apply (rule CollectI)
paulson@13797
   153
apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_UN, 
paulson@13797
   154
                THEN constrains_weaken],   auto)
paulson@13797
   155
done
paulson@13797
   156
paulson@13797
   157
(** Intersection **)
paulson@13797
   158
paulson@13797
   159
lemma Constrains_Int: 
paulson@13797
   160
    "[| F : A Co A'; F : B Co B' |] ==> F : (A Int B) Co (A' Int B')"
paulson@13797
   161
apply (unfold Constrains_def)
paulson@13797
   162
apply (blast intro: constrains_Int [THEN constrains_weaken])
paulson@13797
   163
done
paulson@13797
   164
paulson@13797
   165
lemma Constrains_INT: 
paulson@13797
   166
  assumes Co: "!!i. i:I ==> F : (A i) Co (A' i)"
paulson@13797
   167
  shows "F : (INT i:I. A i) Co (INT i:I. A' i)"
paulson@13797
   168
apply (unfold Constrains_def)
paulson@13797
   169
apply (rule CollectI)
paulson@13797
   170
apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_INT, 
paulson@13797
   171
                THEN constrains_weaken],   auto)
paulson@13797
   172
done
paulson@13797
   173
paulson@13797
   174
lemma Constrains_imp_subset: "F : A Co A' ==> reachable F Int A <= A'"
paulson@13797
   175
by (simp add: constrains_imp_subset Constrains_def)
paulson@13797
   176
paulson@13797
   177
lemma Constrains_trans: "[| F : A Co B; F : B Co C |] ==> F : A Co C"
paulson@13797
   178
apply (simp add: Constrains_eq_constrains)
paulson@13797
   179
apply (blast intro: constrains_trans constrains_weaken)
paulson@13797
   180
done
paulson@13797
   181
paulson@13797
   182
lemma Constrains_cancel:
paulson@13797
   183
     "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')"
paulson@13797
   184
by (simp add: Constrains_eq_constrains constrains_def, blast)
paulson@13797
   185
paulson@13797
   186
paulson@13797
   187
(*** Stable ***)
paulson@13797
   188
paulson@13797
   189
(*Useful because there's no Stable_weaken.  [Tanja Vos]*)
paulson@13797
   190
lemma Stable_eq: "[| F: Stable A; A = B |] ==> F : Stable B"
paulson@13797
   191
by blast
paulson@13797
   192
paulson@13797
   193
lemma Stable_eq_stable: "(F : Stable A) = (F : stable (reachable F Int A))"
paulson@13797
   194
by (simp add: Stable_def Constrains_eq_constrains stable_def)
paulson@13797
   195
paulson@13797
   196
lemma StableI: "F : A Co A ==> F : Stable A"
paulson@13797
   197
by (unfold Stable_def, assumption)
paulson@13797
   198
paulson@13797
   199
lemma StableD: "F : Stable A ==> F : A Co A"
paulson@13797
   200
by (unfold Stable_def, assumption)
paulson@13797
   201
paulson@13797
   202
lemma Stable_Un: 
paulson@13797
   203
    "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Un A')"
paulson@13797
   204
apply (unfold Stable_def)
paulson@13797
   205
apply (blast intro: Constrains_Un)
paulson@13797
   206
done
paulson@13797
   207
paulson@13797
   208
lemma Stable_Int: 
paulson@13797
   209
    "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Int A')"
paulson@13797
   210
apply (unfold Stable_def)
paulson@13797
   211
apply (blast intro: Constrains_Int)
paulson@13797
   212
done
paulson@13797
   213
paulson@13797
   214
lemma Stable_Constrains_Un: 
paulson@13797
   215
    "[| F : Stable C; F : A Co (C Un A') |]    
paulson@13797
   216
     ==> F : (C Un A) Co (C Un A')"
paulson@13797
   217
apply (unfold Stable_def)
paulson@13797
   218
apply (blast intro: Constrains_Un [THEN Constrains_weaken])
paulson@13797
   219
done
paulson@13797
   220
paulson@13797
   221
lemma Stable_Constrains_Int: 
paulson@13797
   222
    "[| F : Stable C; F : (C Int A) Co A' |]    
paulson@13797
   223
     ==> F : (C Int A) Co (C Int A')"
paulson@13797
   224
apply (unfold Stable_def)
paulson@13797
   225
apply (blast intro: Constrains_Int [THEN Constrains_weaken])
paulson@13797
   226
done
paulson@13797
   227
paulson@13797
   228
lemma Stable_UN: 
paulson@13797
   229
    "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (UN i:I. A i)"
paulson@13797
   230
by (simp add: Stable_def Constrains_UN) 
paulson@13797
   231
paulson@13797
   232
lemma Stable_INT: 
paulson@13797
   233
    "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (INT i:I. A i)"
paulson@13797
   234
by (simp add: Stable_def Constrains_INT) 
paulson@13797
   235
paulson@13797
   236
lemma Stable_reachable: "F : Stable (reachable F)"
paulson@13797
   237
by (simp add: Stable_eq_stable)
paulson@13797
   238
paulson@13797
   239
paulson@13797
   240
paulson@13797
   241
(*** Increasing ***)
paulson@13797
   242
paulson@13797
   243
lemma IncreasingD: 
paulson@13797
   244
     "F : Increasing f ==> F : Stable {s. x <= f s}"
paulson@13797
   245
by (unfold Increasing_def, blast)
paulson@13797
   246
paulson@13797
   247
lemma mono_Increasing_o: 
paulson@13797
   248
     "mono g ==> Increasing f <= Increasing (g o f)"
paulson@13797
   249
apply (simp add: Increasing_def Stable_def Constrains_def stable_def 
paulson@13797
   250
                 constrains_def)
paulson@13797
   251
apply (blast intro: monoD order_trans)
paulson@13797
   252
done
paulson@13797
   253
paulson@13797
   254
lemma strict_IncreasingD: 
paulson@13797
   255
     "!!z::nat. F : Increasing f ==> F: Stable {s. z < f s}"
paulson@13797
   256
by (simp add: Increasing_def Suc_le_eq [symmetric])
paulson@13797
   257
paulson@13797
   258
lemma increasing_imp_Increasing: 
paulson@13797
   259
     "F : increasing f ==> F : Increasing f"
paulson@13797
   260
apply (unfold increasing_def Increasing_def)
paulson@13797
   261
apply (blast intro: stable_imp_Stable)
paulson@13797
   262
done
paulson@13797
   263
paulson@13797
   264
lemmas Increasing_constant =  
paulson@13797
   265
    increasing_constant [THEN increasing_imp_Increasing, standard, iff]
paulson@13797
   266
paulson@13797
   267
paulson@13797
   268
(*** The Elimination Theorem.  The "free" m has become universally quantified!
paulson@13797
   269
     Should the premise be !!m instead of ALL m ?  Would make it harder to use
paulson@13797
   270
     in forward proof. ***)
paulson@13797
   271
paulson@13797
   272
lemma Elimination: 
paulson@13797
   273
    "[| ALL m. F : {s. s x = m} Co (B m) |]  
paulson@13797
   274
     ==> F : {s. s x : M} Co (UN m:M. B m)"
paulson@13797
   275
paulson@13797
   276
by (unfold Constrains_def constrains_def, blast)
paulson@13797
   277
paulson@13797
   278
(*As above, but for the trivial case of a one-variable state, in which the
paulson@13797
   279
  state is identified with its one variable.*)
paulson@13797
   280
lemma Elimination_sing: 
paulson@13797
   281
    "(ALL m. F : {m} Co (B m)) ==> F : M Co (UN m:M. B m)"
paulson@13797
   282
by (unfold Constrains_def constrains_def, blast)
paulson@13797
   283
paulson@13797
   284
paulson@13797
   285
(*** Specialized laws for handling Always ***)
paulson@13797
   286
paulson@13797
   287
(** Natural deduction rules for "Always A" **)
paulson@13797
   288
paulson@13797
   289
lemma AlwaysI: "[| Init F<=A;  F : Stable A |] ==> F : Always A"
paulson@13797
   290
by (simp add: Always_def)
paulson@13797
   291
paulson@13797
   292
lemma AlwaysD: "F : Always A ==> Init F<=A & F : Stable A"
paulson@13797
   293
by (simp add: Always_def)
paulson@13797
   294
paulson@13797
   295
lemmas AlwaysE = AlwaysD [THEN conjE, standard]
paulson@13797
   296
lemmas Always_imp_Stable = AlwaysD [THEN conjunct2, standard]
paulson@13797
   297
paulson@13797
   298
paulson@13797
   299
(*The set of all reachable states is Always*)
paulson@13797
   300
lemma Always_includes_reachable: "F : Always A ==> reachable F <= A"
paulson@13797
   301
apply (simp add: Stable_def Constrains_def constrains_def Always_def)
paulson@13797
   302
apply (rule subsetI)
paulson@13797
   303
apply (erule reachable.induct)
paulson@13797
   304
apply (blast intro: reachable.intros)+
paulson@13797
   305
done
paulson@13797
   306
paulson@13797
   307
lemma invariant_imp_Always: 
paulson@13797
   308
     "F : invariant A ==> F : Always A"
paulson@13797
   309
apply (unfold Always_def invariant_def Stable_def stable_def)
paulson@13797
   310
apply (blast intro: constrains_imp_Constrains)
paulson@13797
   311
done
paulson@13797
   312
paulson@13797
   313
lemmas Always_reachable =
paulson@13797
   314
    invariant_reachable [THEN invariant_imp_Always, standard]
paulson@13797
   315
paulson@13797
   316
lemma Always_eq_invariant_reachable:
paulson@13797
   317
     "Always A = {F. F : invariant (reachable F Int A)}"
paulson@13797
   318
apply (simp add: Always_def invariant_def Stable_def Constrains_eq_constrains
paulson@13797
   319
                 stable_def)
paulson@13797
   320
apply (blast intro: reachable.intros)
paulson@13797
   321
done
paulson@13797
   322
paulson@13797
   323
(*the RHS is the traditional definition of the "always" operator*)
paulson@13797
   324
lemma Always_eq_includes_reachable: "Always A = {F. reachable F <= A}"
paulson@13797
   325
by (auto dest: invariant_includes_reachable simp add: Int_absorb2 invariant_reachable Always_eq_invariant_reachable)
paulson@13797
   326
paulson@13797
   327
lemma Always_UNIV_eq [simp]: "Always UNIV = UNIV"
paulson@13797
   328
by (auto simp add: Always_eq_includes_reachable)
paulson@13797
   329
paulson@13797
   330
lemma UNIV_AlwaysI: "UNIV <= A ==> F : Always A"
paulson@13797
   331
by (auto simp add: Always_eq_includes_reachable)
paulson@13797
   332
paulson@13797
   333
lemma Always_eq_UN_invariant: "Always A = (UN I: Pow A. invariant I)"
paulson@13797
   334
apply (simp add: Always_eq_includes_reachable)
paulson@13797
   335
apply (blast intro: invariantI Init_subset_reachable [THEN subsetD] 
paulson@13797
   336
                    invariant_includes_reachable [THEN subsetD])
paulson@13797
   337
done
paulson@13797
   338
paulson@13797
   339
lemma Always_weaken: "[| F : Always A; A <= B |] ==> F : Always B"
paulson@13797
   340
by (auto simp add: Always_eq_includes_reachable)
paulson@13797
   341
paulson@13797
   342
paulson@13797
   343
(*** "Co" rules involving Always ***)
paulson@13797
   344
paulson@13797
   345
lemma Always_Constrains_pre:
paulson@13797
   346
     "F : Always INV ==> (F : (INV Int A) Co A') = (F : A Co A')"
paulson@13797
   347
by (simp add: Always_includes_reachable [THEN Int_absorb2] Constrains_def 
paulson@13797
   348
              Int_assoc [symmetric])
paulson@13797
   349
paulson@13797
   350
lemma Always_Constrains_post:
paulson@13797
   351
     "F : Always INV ==> (F : A Co (INV Int A')) = (F : A Co A')"
paulson@13797
   352
by (simp add: Always_includes_reachable [THEN Int_absorb2] 
paulson@13797
   353
              Constrains_eq_constrains Int_assoc [symmetric])
paulson@13797
   354
paulson@13797
   355
(* [| F : Always INV;  F : (INV Int A) Co A' |] ==> F : A Co A' *)
paulson@13797
   356
lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1, standard]
paulson@13797
   357
paulson@13797
   358
(* [| F : Always INV;  F : A Co A' |] ==> F : A Co (INV Int A') *)
paulson@13797
   359
lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2, standard]
paulson@13797
   360
paulson@13797
   361
(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
paulson@13797
   362
lemma Always_Constrains_weaken:
paulson@13797
   363
     "[| F : Always C;  F : A Co A';    
paulson@13797
   364
         C Int B <= A;   C Int A' <= B' |]  
paulson@13797
   365
      ==> F : B Co B'"
paulson@13797
   366
apply (rule Always_ConstrainsI, assumption)
paulson@13797
   367
apply (drule Always_ConstrainsD, assumption)
paulson@13797
   368
apply (blast intro: Constrains_weaken)
paulson@13797
   369
done
paulson@13797
   370
paulson@13797
   371
paulson@13797
   372
(** Conjoining Always properties **)
paulson@13797
   373
paulson@13797
   374
lemma Always_Int_distrib: "Always (A Int B) = Always A Int Always B"
paulson@13797
   375
by (auto simp add: Always_eq_includes_reachable)
paulson@13797
   376
paulson@13797
   377
lemma Always_INT_distrib: "Always (INTER I A) = (INT i:I. Always (A i))"
paulson@13797
   378
by (auto simp add: Always_eq_includes_reachable)
paulson@13797
   379
paulson@13797
   380
lemma Always_Int_I:
paulson@13797
   381
     "[| F : Always A;  F : Always B |] ==> F : Always (A Int B)"
paulson@13797
   382
by (simp add: Always_Int_distrib)
paulson@13797
   383
paulson@13797
   384
(*Allows a kind of "implication introduction"*)
paulson@13797
   385
lemma Always_Compl_Un_eq:
paulson@13797
   386
     "F : Always A ==> (F : Always (-A Un B)) = (F : Always B)"
paulson@13797
   387
by (auto simp add: Always_eq_includes_reachable)
paulson@13797
   388
paulson@13797
   389
(*Delete the nearest invariance assumption (which will be the second one
paulson@13797
   390
  used by Always_Int_I) *)
paulson@13797
   391
lemmas Always_thin = thin_rl [of "F : Always A", standard]
paulson@13797
   392
paulson@5313
   393
end