src/HOL/UNITY/UNITY.thy
author paulson
Thu Jan 30 18:08:09 2003 +0100 (2003-01-30)
changeset 13797 baefae13ad37
parent 10834 a7897aebbffc
child 13798 4c1a53627500
permissions -rw-r--r--
conversion of UNITY theories to new-style
paulson@4776
     1
(*  Title:      HOL/UNITY/UNITY
paulson@4776
     2
    ID:         $Id$
paulson@4776
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     4
    Copyright   1998  University of Cambridge
paulson@4776
     5
paulson@4776
     6
The basic UNITY theory (revised version, based upon the "co" operator)
paulson@4776
     7
paulson@4776
     8
From Misra, "A Logic for Concurrent Programming", 1994
paulson@4776
     9
*)
paulson@4776
    10
paulson@13797
    11
theory UNITY = Main:
paulson@6535
    12
paulson@6535
    13
typedef (Program)
paulson@10064
    14
  'a program = "{(init:: 'a set, acts :: ('a * 'a)set set,
paulson@13797
    15
		   allowed :: ('a * 'a)set set). Id:acts & Id: allowed}" 
paulson@13797
    16
  by blast
paulson@6536
    17
paulson@4776
    18
constdefs
paulson@13797
    19
  constrains :: "['a set, 'a set] => 'a program set"  (infixl "co"     60)
paulson@13797
    20
    "A co B == {F. ALL act: Acts F. act``A <= B}"
paulson@13797
    21
paulson@13797
    22
  unless  :: "['a set, 'a set] => 'a program set"  (infixl "unless" 60)
paulson@13797
    23
    "A unless B == (A-B) co (A Un B)"
paulson@13797
    24
paulson@13797
    25
  mk_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
paulson@10064
    26
		   => 'a program"
paulson@10064
    27
    "mk_program == %(init, acts, allowed).
paulson@10064
    28
                      Abs_Program (init, insert Id acts, insert Id allowed)"
paulson@6535
    29
paulson@6535
    30
  Init :: "'a program => 'a set"
paulson@10064
    31
    "Init F == (%(init, acts, allowed). init) (Rep_Program F)"
paulson@6535
    32
paulson@6535
    33
  Acts :: "'a program => ('a * 'a)set set"
paulson@10064
    34
    "Acts F == (%(init, acts, allowed). acts) (Rep_Program F)"
paulson@10064
    35
paulson@10064
    36
  AllowedActs :: "'a program => ('a * 'a)set set"
paulson@10064
    37
    "AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)"
paulson@10064
    38
paulson@10064
    39
  Allowed :: "'a program => 'a program set"
paulson@10064
    40
    "Allowed F == {G. Acts G <= AllowedActs F}"
paulson@4776
    41
paulson@5648
    42
  stable     :: "'a set => 'a program set"
paulson@6536
    43
    "stable A == A co A"
paulson@4776
    44
paulson@5648
    45
  strongest_rhs :: "['a program, 'a set] => 'a set"
paulson@6536
    46
    "strongest_rhs F A == Inter {B. F : A co B}"
paulson@4776
    47
paulson@5648
    48
  invariant :: "'a set => 'a program set"
paulson@5648
    49
    "invariant A == {F. Init F <= A} Int stable A"
paulson@4776
    50
paulson@5648
    51
  (*Polymorphic in both states and the meaning of <= *)
paulson@6713
    52
  increasing :: "['a => 'b::{order}] => 'a program set"
paulson@5648
    53
    "increasing f == INT z. stable {s. z <= f s}"
paulson@4776
    54
paulson@6536
    55
paulson@13797
    56
(*Perhaps equalities.ML shouldn't add this in the first place!*)
paulson@13797
    57
declare image_Collect [simp del]
paulson@13797
    58
paulson@13797
    59
(*** The abstract type of programs ***)
paulson@13797
    60
paulson@13797
    61
lemmas program_typedef =
paulson@13797
    62
     Rep_Program Rep_Program_inverse Abs_Program_inverse 
paulson@13797
    63
     Program_def Init_def Acts_def AllowedActs_def mk_program_def
paulson@13797
    64
paulson@13797
    65
lemma Id_in_Acts [iff]: "Id : Acts F"
paulson@13797
    66
apply (cut_tac x = F in Rep_Program)
paulson@13797
    67
apply (auto simp add: program_typedef) 
paulson@13797
    68
done
paulson@13797
    69
paulson@13797
    70
lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F"
paulson@13797
    71
by (simp add: insert_absorb Id_in_Acts)
paulson@13797
    72
paulson@13797
    73
lemma Id_in_AllowedActs [iff]: "Id : AllowedActs F"
paulson@13797
    74
apply (cut_tac x = F in Rep_Program)
paulson@13797
    75
apply (auto simp add: program_typedef) 
paulson@13797
    76
done
paulson@13797
    77
paulson@13797
    78
lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F"
paulson@13797
    79
by (simp add: insert_absorb Id_in_AllowedActs)
paulson@13797
    80
paulson@13797
    81
(** Inspectors for type "program" **)
paulson@13797
    82
paulson@13797
    83
lemma Init_eq [simp]: "Init (mk_program (init,acts,allowed)) = init"
paulson@13797
    84
by (auto simp add: program_typedef)
paulson@13797
    85
paulson@13797
    86
lemma Acts_eq [simp]: "Acts (mk_program (init,acts,allowed)) = insert Id acts"
paulson@13797
    87
by (auto simp add: program_typedef)
paulson@13797
    88
paulson@13797
    89
lemma AllowedActs_eq [simp]:
paulson@13797
    90
     "AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed"
paulson@13797
    91
by (auto simp add: program_typedef)
paulson@13797
    92
paulson@13797
    93
(** Equality for UNITY programs **)
paulson@13797
    94
paulson@13797
    95
lemma surjective_mk_program [simp]:
paulson@13797
    96
     "mk_program (Init F, Acts F, AllowedActs F) = F"
paulson@13797
    97
apply (cut_tac x = F in Rep_Program)
paulson@13797
    98
apply (auto simp add: program_typedef)
paulson@13797
    99
apply (drule_tac f = Abs_Program in arg_cong)+
paulson@13797
   100
apply (simp add: program_typedef insert_absorb)
paulson@13797
   101
done
paulson@13797
   102
paulson@13797
   103
lemma program_equalityI:
paulson@13797
   104
     "[| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |]  
paulson@13797
   105
      ==> F = G"
paulson@13797
   106
apply (rule_tac t = F in surjective_mk_program [THEN subst])
paulson@13797
   107
apply (rule_tac t = G in surjective_mk_program [THEN subst], simp)
paulson@13797
   108
done
paulson@13797
   109
paulson@13797
   110
lemma program_equalityE:
paulson@13797
   111
     "[| F = G;  
paulson@13797
   112
         [| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |] 
paulson@13797
   113
         ==> P |] ==> P"
paulson@13797
   114
by simp 
paulson@13797
   115
paulson@13797
   116
lemma program_equality_iff:
paulson@13797
   117
     "(F=G) =   
paulson@13797
   118
      (Init F = Init G & Acts F = Acts G &AllowedActs F = AllowedActs G)"
paulson@13797
   119
by (blast intro: program_equalityI program_equalityE)
paulson@13797
   120
paulson@13797
   121
paulson@13797
   122
(*** These rules allow "lazy" definition expansion 
paulson@13797
   123
     They avoid expanding the full program, which is a large expression
paulson@13797
   124
***)
paulson@13797
   125
paulson@13797
   126
lemma def_prg_Init: "F == mk_program (init,acts,allowed) ==> Init F = init"
paulson@13797
   127
by auto
paulson@13797
   128
paulson@13797
   129
lemma def_prg_Acts:
paulson@13797
   130
     "F == mk_program (init,acts,allowed) ==> Acts F = insert Id acts"
paulson@13797
   131
by auto
paulson@13797
   132
paulson@13797
   133
lemma def_prg_AllowedActs:
paulson@13797
   134
     "F == mk_program (init,acts,allowed)  
paulson@13797
   135
      ==> AllowedActs F = insert Id allowed"
paulson@13797
   136
by auto
paulson@13797
   137
paulson@13797
   138
(*The program is not expanded, but its Init and Acts are*)
paulson@13797
   139
lemma def_prg_simps:
paulson@13797
   140
    "[| F == mk_program (init,acts,allowed) |]  
paulson@13797
   141
     ==> Init F = init & Acts F = insert Id acts"
paulson@13797
   142
by simp
paulson@13797
   143
paulson@13797
   144
(*An action is expanded only if a pair of states is being tested against it*)
paulson@13797
   145
lemma def_act_simp:
paulson@13797
   146
     "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'"
paulson@13797
   147
by auto
paulson@13797
   148
paulson@13797
   149
(*A set is expanded only if an element is being tested against it*)
paulson@13797
   150
lemma def_set_simp: "A == B ==> (x : A) = (x : B)"
paulson@13797
   151
by auto
paulson@13797
   152
paulson@13797
   153
paulson@13797
   154
(*** co ***)
paulson@13797
   155
paulson@13797
   156
lemma constrainsI: 
paulson@13797
   157
    "(!!act s s'. [| act: Acts F;  (s,s') : act;  s: A |] ==> s': A')  
paulson@13797
   158
     ==> F : A co A'"
paulson@13797
   159
by (simp add: constrains_def, blast)
paulson@13797
   160
paulson@13797
   161
lemma constrainsD: 
paulson@13797
   162
    "[| F : A co A'; act: Acts F;  (s,s'): act;  s: A |] ==> s': A'"
paulson@13797
   163
by (unfold constrains_def, blast)
paulson@13797
   164
paulson@13797
   165
lemma constrains_empty [iff]: "F : {} co B"
paulson@13797
   166
by (unfold constrains_def, blast)
paulson@13797
   167
paulson@13797
   168
lemma constrains_empty2 [iff]: "(F : A co {}) = (A={})"
paulson@13797
   169
by (unfold constrains_def, blast)
paulson@13797
   170
paulson@13797
   171
lemma constrains_UNIV [iff]: "(F : UNIV co B) = (B = UNIV)"
paulson@13797
   172
by (unfold constrains_def, blast)
paulson@13797
   173
paulson@13797
   174
lemma constrains_UNIV2 [iff]: "F : A co UNIV"
paulson@13797
   175
by (unfold constrains_def, blast)
paulson@13797
   176
paulson@13797
   177
(*monotonic in 2nd argument*)
paulson@13797
   178
lemma constrains_weaken_R: 
paulson@13797
   179
    "[| F : A co A'; A'<=B' |] ==> F : A co B'"
paulson@13797
   180
by (unfold constrains_def, blast)
paulson@13797
   181
paulson@13797
   182
(*anti-monotonic in 1st argument*)
paulson@13797
   183
lemma constrains_weaken_L: 
paulson@13797
   184
    "[| F : A co A'; B<=A |] ==> F : B co A'"
paulson@13797
   185
by (unfold constrains_def, blast)
paulson@13797
   186
paulson@13797
   187
lemma constrains_weaken: 
paulson@13797
   188
   "[| F : A co A'; B<=A; A'<=B' |] ==> F : B co B'"
paulson@13797
   189
by (unfold constrains_def, blast)
paulson@13797
   190
paulson@13797
   191
(** Union **)
paulson@13797
   192
paulson@13797
   193
lemma constrains_Un: 
paulson@13797
   194
    "[| F : A co A'; F : B co B' |] ==> F : (A Un B) co (A' Un B')"
paulson@13797
   195
by (unfold constrains_def, blast)
paulson@13797
   196
paulson@13797
   197
lemma constrains_UN: 
paulson@13797
   198
    "(!!i. i:I ==> F : (A i) co (A' i)) 
paulson@13797
   199
     ==> F : (UN i:I. A i) co (UN i:I. A' i)"
paulson@13797
   200
by (unfold constrains_def, blast)
paulson@13797
   201
paulson@13797
   202
lemma constrains_Un_distrib: "(A Un B) co C = (A co C) Int (B co C)"
paulson@13797
   203
by (unfold constrains_def, blast)
paulson@13797
   204
paulson@13797
   205
lemma constrains_UN_distrib: "(UN i:I. A i) co B = (INT i:I. A i co B)"
paulson@13797
   206
by (unfold constrains_def, blast)
paulson@13797
   207
paulson@13797
   208
lemma constrains_Int_distrib: "C co (A Int B) = (C co A) Int (C co B)"
paulson@13797
   209
by (unfold constrains_def, blast)
paulson@13797
   210
paulson@13797
   211
lemma constrains_INT_distrib: "A co (INT i:I. B i) = (INT i:I. A co B i)"
paulson@13797
   212
by (unfold constrains_def, blast)
paulson@13797
   213
paulson@13797
   214
(** Intersection **)
paulson@6536
   215
paulson@13797
   216
lemma constrains_Int: 
paulson@13797
   217
    "[| F : A co A'; F : B co B' |] ==> F : (A Int B) co (A' Int B')"
paulson@13797
   218
by (unfold constrains_def, blast)
paulson@13797
   219
paulson@13797
   220
lemma constrains_INT: 
paulson@13797
   221
    "(!!i. i:I ==> F : (A i) co (A' i)) 
paulson@13797
   222
     ==> F : (INT i:I. A i) co (INT i:I. A' i)"
paulson@13797
   223
by (unfold constrains_def, blast)
paulson@13797
   224
paulson@13797
   225
lemma constrains_imp_subset: "F : A co A' ==> A <= A'"
paulson@13797
   226
by (unfold constrains_def, auto)
paulson@13797
   227
paulson@13797
   228
(*The reasoning is by subsets since "co" refers to single actions
paulson@13797
   229
  only.  So this rule isn't that useful.*)
paulson@13797
   230
lemma constrains_trans: 
paulson@13797
   231
    "[| F : A co B; F : B co C |] ==> F : A co C"
paulson@13797
   232
by (unfold constrains_def, blast)
paulson@13797
   233
paulson@13797
   234
lemma constrains_cancel: 
paulson@13797
   235
   "[| F : A co (A' Un B); F : B co B' |] ==> F : A co (A' Un B')"
paulson@13797
   236
by (unfold constrains_def, clarify, blast)
paulson@13797
   237
paulson@13797
   238
paulson@13797
   239
(*** unless ***)
paulson@13797
   240
paulson@13797
   241
lemma unlessI: "F : (A-B) co (A Un B) ==> F : A unless B"
paulson@13797
   242
by (unfold unless_def, assumption)
paulson@13797
   243
paulson@13797
   244
lemma unlessD: "F : A unless B ==> F : (A-B) co (A Un B)"
paulson@13797
   245
by (unfold unless_def, assumption)
paulson@13797
   246
paulson@13797
   247
paulson@13797
   248
(*** stable ***)
paulson@13797
   249
paulson@13797
   250
lemma stableI: "F : A co A ==> F : stable A"
paulson@13797
   251
by (unfold stable_def, assumption)
paulson@13797
   252
paulson@13797
   253
lemma stableD: "F : stable A ==> F : A co A"
paulson@13797
   254
by (unfold stable_def, assumption)
paulson@13797
   255
paulson@13797
   256
lemma stable_UNIV [simp]: "stable UNIV = UNIV"
paulson@13797
   257
by (unfold stable_def constrains_def, auto)
paulson@13797
   258
paulson@13797
   259
(** Union **)
paulson@13797
   260
paulson@13797
   261
lemma stable_Un: 
paulson@13797
   262
    "[| F : stable A; F : stable A' |] ==> F : stable (A Un A')"
paulson@13797
   263
paulson@13797
   264
apply (unfold stable_def)
paulson@13797
   265
apply (blast intro: constrains_Un)
paulson@13797
   266
done
paulson@13797
   267
paulson@13797
   268
lemma stable_UN: 
paulson@13797
   269
    "(!!i. i:I ==> F : stable (A i)) ==> F : stable (UN i:I. A i)"
paulson@13797
   270
apply (unfold stable_def)
paulson@13797
   271
apply (blast intro: constrains_UN)
paulson@13797
   272
done
paulson@13797
   273
paulson@13797
   274
(** Intersection **)
paulson@13797
   275
paulson@13797
   276
lemma stable_Int: 
paulson@13797
   277
    "[| F : stable A;  F : stable A' |] ==> F : stable (A Int A')"
paulson@13797
   278
apply (unfold stable_def)
paulson@13797
   279
apply (blast intro: constrains_Int)
paulson@13797
   280
done
paulson@13797
   281
paulson@13797
   282
lemma stable_INT: 
paulson@13797
   283
    "(!!i. i:I ==> F : stable (A i)) ==> F : stable (INT i:I. A i)"
paulson@13797
   284
apply (unfold stable_def)
paulson@13797
   285
apply (blast intro: constrains_INT)
paulson@13797
   286
done
paulson@13797
   287
paulson@13797
   288
lemma stable_constrains_Un: 
paulson@13797
   289
    "[| F : stable C; F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')"
paulson@13797
   290
by (unfold stable_def constrains_def, blast)
paulson@13797
   291
paulson@13797
   292
lemma stable_constrains_Int: 
paulson@13797
   293
  "[| F : stable C; F :  (C Int A) co A' |] ==> F : (C Int A) co (C Int A')"
paulson@13797
   294
by (unfold stable_def constrains_def, blast)
paulson@13797
   295
paulson@13797
   296
(*[| F : stable C; F :  (C Int A) co A |] ==> F : stable (C Int A) *)
paulson@13797
   297
lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI, standard]
paulson@13797
   298
paulson@13797
   299
paulson@13797
   300
(*** invariant ***)
paulson@13797
   301
paulson@13797
   302
lemma invariantI: "[| Init F<=A;  F: stable A |] ==> F : invariant A"
paulson@13797
   303
by (simp add: invariant_def)
paulson@13797
   304
paulson@13797
   305
(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*)
paulson@13797
   306
lemma invariant_Int:
paulson@13797
   307
     "[| F : invariant A;  F : invariant B |] ==> F : invariant (A Int B)"
paulson@13797
   308
by (auto simp add: invariant_def stable_Int)
paulson@13797
   309
paulson@13797
   310
paulson@13797
   311
(*** increasing ***)
paulson@13797
   312
paulson@13797
   313
lemma increasingD: 
paulson@13797
   314
     "F : increasing f ==> F : stable {s. z <= f s}"
paulson@13797
   315
paulson@13797
   316
by (unfold increasing_def, blast)
paulson@13797
   317
paulson@13797
   318
lemma increasing_constant [iff]: "F : increasing (%s. c)"
paulson@13797
   319
by (unfold increasing_def stable_def, auto)
paulson@13797
   320
paulson@13797
   321
lemma mono_increasing_o: 
paulson@13797
   322
     "mono g ==> increasing f <= increasing (g o f)"
paulson@13797
   323
apply (unfold increasing_def stable_def constrains_def, auto)
paulson@13797
   324
apply (blast intro: monoD order_trans)
paulson@13797
   325
done
paulson@13797
   326
paulson@13797
   327
(*Holds by the theorem (Suc m <= n) = (m < n) *)
paulson@13797
   328
lemma strict_increasingD: 
paulson@13797
   329
     "!!z::nat. F : increasing f ==> F: stable {s. z < f s}"
paulson@13797
   330
by (simp add: increasing_def Suc_le_eq [symmetric])
paulson@13797
   331
paulson@13797
   332
paulson@13797
   333
(** The Elimination Theorem.  The "free" m has become universally quantified!
paulson@13797
   334
    Should the premise be !!m instead of ALL m ?  Would make it harder to use
paulson@13797
   335
    in forward proof. **)
paulson@13797
   336
paulson@13797
   337
lemma elimination: 
paulson@13797
   338
    "[| ALL m:M. F : {s. s x = m} co (B m) |]  
paulson@13797
   339
     ==> F : {s. s x : M} co (UN m:M. B m)"
paulson@13797
   340
by (unfold constrains_def, blast)
paulson@13797
   341
paulson@13797
   342
(*As above, but for the trivial case of a one-variable state, in which the
paulson@13797
   343
  state is identified with its one variable.*)
paulson@13797
   344
lemma elimination_sing: 
paulson@13797
   345
    "(ALL m:M. F : {m} co (B m)) ==> F : M co (UN m:M. B m)"
paulson@13797
   346
by (unfold constrains_def, blast)
paulson@13797
   347
paulson@13797
   348
paulson@13797
   349
paulson@13797
   350
(*** Theoretical Results from Section 6 ***)
paulson@13797
   351
paulson@13797
   352
lemma constrains_strongest_rhs: 
paulson@13797
   353
    "F : A co (strongest_rhs F A )"
paulson@13797
   354
by (unfold constrains_def strongest_rhs_def, blast)
paulson@13797
   355
paulson@13797
   356
lemma strongest_rhs_is_strongest: 
paulson@13797
   357
    "F : A co B ==> strongest_rhs F A <= B"
paulson@13797
   358
by (unfold constrains_def strongest_rhs_def, blast)
paulson@13797
   359
paulson@13797
   360
paulson@13797
   361
(** Ad-hoc set-theory rules **)
paulson@13797
   362
paulson@13797
   363
lemma Un_Diff_Diff [simp]: "A Un B - (A - B) = B"
paulson@13797
   364
by blast
paulson@13797
   365
paulson@13797
   366
lemma Int_Union_Union: "Union(B) Int A = Union((%C. C Int A)`B)"
paulson@13797
   367
by blast
paulson@13797
   368
paulson@13797
   369
(** Needed for WF reasoning in WFair.ML **)
paulson@13797
   370
paulson@13797
   371
lemma Image_less_than [simp]: "less_than `` {k} = greaterThan k"
paulson@13797
   372
by blast
paulson@13797
   373
paulson@13797
   374
lemma Image_inverse_less_than [simp]: "less_than^-1 `` {k} = lessThan k"
paulson@13797
   375
by blast
paulson@6536
   376
paulson@4776
   377
end