src/HOL/UNITY/UNITY.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 45694 4a8743618257
child 46577 e5438c5797ae
permissions -rw-r--r--
Quotient_Info stores only relation maps
wenzelm@32960
     1
(*  Title:      HOL/UNITY/UNITY.thy
paulson@4776
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     3
    Copyright   1998  University of Cambridge
paulson@4776
     4
wenzelm@32960
     5
The basic UNITY theory (revised version, based upon the "co"
wenzelm@32960
     6
operator).
paulson@4776
     7
wenzelm@32960
     8
From Misra, "A Logic for Concurrent Programming", 1994.
paulson@4776
     9
*)
paulson@4776
    10
paulson@13798
    11
header {*The Basic UNITY Theory*}
paulson@13798
    12
haftmann@16417
    13
theory UNITY imports Main begin
paulson@6535
    14
wenzelm@45694
    15
definition
wenzelm@45694
    16
  "Program =
wenzelm@45694
    17
    {(init:: 'a set, acts :: ('a * 'a)set set,
wenzelm@45694
    18
      allowed :: ('a * 'a)set set). Id \<in> acts & Id: allowed}"
wenzelm@45694
    19
wenzelm@45694
    20
typedef (open) 'a program = "Program :: ('a set * ('a * 'a) set set * ('a * 'a) set set) set"
wenzelm@45694
    21
  morphisms Rep_Program Abs_Program
wenzelm@45694
    22
  unfolding Program_def by blast
paulson@6536
    23
haftmann@35416
    24
definition Acts :: "'a program => ('a * 'a)set set" where
wenzelm@14653
    25
    "Acts F == (%(init, acts, allowed). acts) (Rep_Program F)"
wenzelm@14653
    26
haftmann@35416
    27
definition "constrains" :: "['a set, 'a set] => 'a program set"  (infixl "co"     60) where
paulson@13805
    28
    "A co B == {F. \<forall>act \<in> Acts F. act``A \<subseteq> B}"
paulson@13797
    29
haftmann@35416
    30
definition unless  :: "['a set, 'a set] => 'a program set"  (infixl "unless" 60)  where
paulson@13805
    31
    "A unless B == (A-B) co (A \<union> B)"
paulson@13797
    32
haftmann@35416
    33
definition mk_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
haftmann@35416
    34
                   => 'a program" where
paulson@10064
    35
    "mk_program == %(init, acts, allowed).
paulson@10064
    36
                      Abs_Program (init, insert Id acts, insert Id allowed)"
paulson@6535
    37
haftmann@35416
    38
definition Init :: "'a program => 'a set" where
paulson@10064
    39
    "Init F == (%(init, acts, allowed). init) (Rep_Program F)"
paulson@6535
    40
haftmann@35416
    41
definition AllowedActs :: "'a program => ('a * 'a)set set" where
paulson@10064
    42
    "AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)"
paulson@10064
    43
haftmann@35416
    44
definition Allowed :: "'a program => 'a program set" where
paulson@13805
    45
    "Allowed F == {G. Acts G \<subseteq> AllowedActs F}"
paulson@4776
    46
haftmann@35416
    47
definition stable     :: "'a set => 'a program set" where
paulson@6536
    48
    "stable A == A co A"
paulson@4776
    49
haftmann@35416
    50
definition strongest_rhs :: "['a program, 'a set] => 'a set" where
paulson@13805
    51
    "strongest_rhs F A == Inter {B. F \<in> A co B}"
paulson@4776
    52
haftmann@35416
    53
definition invariant :: "'a set => 'a program set" where
paulson@13805
    54
    "invariant A == {F. Init F \<subseteq> A} \<inter> stable A"
paulson@4776
    55
haftmann@35416
    56
definition increasing :: "['a => 'b::{order}] => 'a program set" where
paulson@13812
    57
    --{*Polymorphic in both states and the meaning of @{text "\<le>"}*}
paulson@13805
    58
    "increasing f == \<Inter>z. stable {s. z \<le> f s}"
paulson@4776
    59
paulson@6536
    60
wenzelm@24147
    61
text{*Perhaps HOL shouldn't add this in the first place!*}
paulson@13797
    62
declare image_Collect [simp del]
paulson@13797
    63
paulson@16184
    64
subsubsection{*The abstract type of programs*}
paulson@13797
    65
paulson@13797
    66
lemmas program_typedef =
paulson@13797
    67
     Rep_Program Rep_Program_inverse Abs_Program_inverse 
paulson@13797
    68
     Program_def Init_def Acts_def AllowedActs_def mk_program_def
paulson@13797
    69
paulson@13805
    70
lemma Id_in_Acts [iff]: "Id \<in> Acts F"
paulson@13797
    71
apply (cut_tac x = F in Rep_Program)
paulson@13797
    72
apply (auto simp add: program_typedef) 
paulson@13797
    73
done
paulson@13797
    74
paulson@13797
    75
lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F"
paulson@13797
    76
by (simp add: insert_absorb Id_in_Acts)
paulson@13797
    77
paulson@13861
    78
lemma Acts_nonempty [simp]: "Acts F \<noteq> {}"
paulson@13861
    79
by auto
paulson@13861
    80
paulson@13805
    81
lemma Id_in_AllowedActs [iff]: "Id \<in> AllowedActs F"
paulson@13797
    82
apply (cut_tac x = F in Rep_Program)
paulson@13797
    83
apply (auto simp add: program_typedef) 
paulson@13797
    84
done
paulson@13797
    85
paulson@13797
    86
lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F"
paulson@13797
    87
by (simp add: insert_absorb Id_in_AllowedActs)
paulson@13797
    88
paulson@16184
    89
subsubsection{*Inspectors for type "program"*}
paulson@13797
    90
paulson@13797
    91
lemma Init_eq [simp]: "Init (mk_program (init,acts,allowed)) = init"
paulson@13812
    92
by (simp add: program_typedef)
paulson@13797
    93
paulson@13797
    94
lemma Acts_eq [simp]: "Acts (mk_program (init,acts,allowed)) = insert Id acts"
paulson@13812
    95
by (simp add: program_typedef)
paulson@13797
    96
paulson@13797
    97
lemma AllowedActs_eq [simp]:
paulson@13797
    98
     "AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed"
paulson@13812
    99
by (simp add: program_typedef)
paulson@13797
   100
paulson@16184
   101
subsubsection{*Equality for UNITY programs*}
paulson@13797
   102
paulson@13797
   103
lemma surjective_mk_program [simp]:
paulson@13797
   104
     "mk_program (Init F, Acts F, AllowedActs F) = F"
paulson@13797
   105
apply (cut_tac x = F in Rep_Program)
paulson@13797
   106
apply (auto simp add: program_typedef)
paulson@13797
   107
apply (drule_tac f = Abs_Program in arg_cong)+
paulson@13797
   108
apply (simp add: program_typedef insert_absorb)
paulson@13797
   109
done
paulson@13797
   110
paulson@13797
   111
lemma program_equalityI:
paulson@13797
   112
     "[| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |]  
paulson@13797
   113
      ==> F = G"
paulson@13797
   114
apply (rule_tac t = F in surjective_mk_program [THEN subst])
paulson@13797
   115
apply (rule_tac t = G in surjective_mk_program [THEN subst], simp)
paulson@13797
   116
done
paulson@13797
   117
paulson@13797
   118
lemma program_equalityE:
paulson@13797
   119
     "[| F = G;  
paulson@13797
   120
         [| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |] 
paulson@13797
   121
         ==> P |] ==> P"
paulson@13797
   122
by simp 
paulson@13797
   123
paulson@13797
   124
lemma program_equality_iff:
paulson@13797
   125
     "(F=G) =   
paulson@13797
   126
      (Init F = Init G & Acts F = Acts G &AllowedActs F = AllowedActs G)"
paulson@13797
   127
by (blast intro: program_equalityI program_equalityE)
paulson@13797
   128
paulson@13797
   129
paulson@16184
   130
subsubsection{*co*}
paulson@13797
   131
paulson@13797
   132
lemma constrainsI: 
paulson@13805
   133
    "(!!act s s'. [| act: Acts F;  (s,s') \<in> act;  s \<in> A |] ==> s': A')  
paulson@13805
   134
     ==> F \<in> A co A'"
paulson@13797
   135
by (simp add: constrains_def, blast)
paulson@13797
   136
paulson@13797
   137
lemma constrainsD: 
paulson@13805
   138
    "[| F \<in> A co A'; act: Acts F;  (s,s'): act;  s \<in> A |] ==> s': A'"
paulson@13797
   139
by (unfold constrains_def, blast)
paulson@13797
   140
paulson@13805
   141
lemma constrains_empty [iff]: "F \<in> {} co B"
paulson@13797
   142
by (unfold constrains_def, blast)
paulson@13797
   143
paulson@13805
   144
lemma constrains_empty2 [iff]: "(F \<in> A co {}) = (A={})"
paulson@13797
   145
by (unfold constrains_def, blast)
paulson@13797
   146
paulson@13805
   147
lemma constrains_UNIV [iff]: "(F \<in> UNIV co B) = (B = UNIV)"
paulson@13797
   148
by (unfold constrains_def, blast)
paulson@13797
   149
paulson@13805
   150
lemma constrains_UNIV2 [iff]: "F \<in> A co UNIV"
paulson@13797
   151
by (unfold constrains_def, blast)
paulson@13797
   152
paulson@13812
   153
text{*monotonic in 2nd argument*}
paulson@13797
   154
lemma constrains_weaken_R: 
paulson@13805
   155
    "[| F \<in> A co A'; A'<=B' |] ==> F \<in> A co B'"
paulson@13797
   156
by (unfold constrains_def, blast)
paulson@13797
   157
paulson@13812
   158
text{*anti-monotonic in 1st argument*}
paulson@13797
   159
lemma constrains_weaken_L: 
paulson@13805
   160
    "[| F \<in> A co A'; B \<subseteq> A |] ==> F \<in> B co A'"
paulson@13797
   161
by (unfold constrains_def, blast)
paulson@13797
   162
paulson@13797
   163
lemma constrains_weaken: 
paulson@13805
   164
   "[| F \<in> A co A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B co B'"
paulson@13797
   165
by (unfold constrains_def, blast)
paulson@13797
   166
paulson@16184
   167
subsubsection{*Union*}
paulson@13797
   168
paulson@13797
   169
lemma constrains_Un: 
paulson@13805
   170
    "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<union> B) co (A' \<union> B')"
paulson@13797
   171
by (unfold constrains_def, blast)
paulson@13797
   172
paulson@13797
   173
lemma constrains_UN: 
paulson@13805
   174
    "(!!i. i \<in> I ==> F \<in> (A i) co (A' i)) 
paulson@13805
   175
     ==> F \<in> (\<Union>i \<in> I. A i) co (\<Union>i \<in> I. A' i)"
paulson@13797
   176
by (unfold constrains_def, blast)
paulson@13797
   177
paulson@13805
   178
lemma constrains_Un_distrib: "(A \<union> B) co C = (A co C) \<inter> (B co C)"
paulson@13797
   179
by (unfold constrains_def, blast)
paulson@13797
   180
paulson@13805
   181
lemma constrains_UN_distrib: "(\<Union>i \<in> I. A i) co B = (\<Inter>i \<in> I. A i co B)"
paulson@13797
   182
by (unfold constrains_def, blast)
paulson@13797
   183
paulson@13805
   184
lemma constrains_Int_distrib: "C co (A \<inter> B) = (C co A) \<inter> (C co B)"
paulson@13797
   185
by (unfold constrains_def, blast)
paulson@13797
   186
paulson@13805
   187
lemma constrains_INT_distrib: "A co (\<Inter>i \<in> I. B i) = (\<Inter>i \<in> I. A co B i)"
paulson@13797
   188
by (unfold constrains_def, blast)
paulson@13797
   189
paulson@16184
   190
subsubsection{*Intersection*}
paulson@6536
   191
paulson@13797
   192
lemma constrains_Int: 
paulson@13805
   193
    "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<inter> B) co (A' \<inter> B')"
paulson@13797
   194
by (unfold constrains_def, blast)
paulson@13797
   195
paulson@13797
   196
lemma constrains_INT: 
paulson@13805
   197
    "(!!i. i \<in> I ==> F \<in> (A i) co (A' i)) 
paulson@13805
   198
     ==> F \<in> (\<Inter>i \<in> I. A i) co (\<Inter>i \<in> I. A' i)"
paulson@13797
   199
by (unfold constrains_def, blast)
paulson@13797
   200
paulson@13805
   201
lemma constrains_imp_subset: "F \<in> A co A' ==> A \<subseteq> A'"
paulson@13797
   202
by (unfold constrains_def, auto)
paulson@13797
   203
paulson@13812
   204
text{*The reasoning is by subsets since "co" refers to single actions
paulson@13812
   205
  only.  So this rule isn't that useful.*}
paulson@13797
   206
lemma constrains_trans: 
paulson@13805
   207
    "[| F \<in> A co B; F \<in> B co C |] ==> F \<in> A co C"
paulson@13797
   208
by (unfold constrains_def, blast)
paulson@13797
   209
paulson@13797
   210
lemma constrains_cancel: 
paulson@13805
   211
   "[| F \<in> A co (A' \<union> B); F \<in> B co B' |] ==> F \<in> A co (A' \<union> B')"
paulson@13797
   212
by (unfold constrains_def, clarify, blast)
paulson@13797
   213
paulson@13797
   214
paulson@16184
   215
subsubsection{*unless*}
paulson@13797
   216
paulson@13805
   217
lemma unlessI: "F \<in> (A-B) co (A \<union> B) ==> F \<in> A unless B"
paulson@13797
   218
by (unfold unless_def, assumption)
paulson@13797
   219
paulson@13805
   220
lemma unlessD: "F \<in> A unless B ==> F \<in> (A-B) co (A \<union> B)"
paulson@13797
   221
by (unfold unless_def, assumption)
paulson@13797
   222
paulson@13797
   223
paulson@16184
   224
subsubsection{*stable*}
paulson@13797
   225
paulson@13805
   226
lemma stableI: "F \<in> A co A ==> F \<in> stable A"
paulson@13797
   227
by (unfold stable_def, assumption)
paulson@13797
   228
paulson@13805
   229
lemma stableD: "F \<in> stable A ==> F \<in> A co A"
paulson@13797
   230
by (unfold stable_def, assumption)
paulson@13797
   231
paulson@13797
   232
lemma stable_UNIV [simp]: "stable UNIV = UNIV"
paulson@13797
   233
by (unfold stable_def constrains_def, auto)
paulson@13797
   234
paulson@16184
   235
subsubsection{*Union*}
paulson@13797
   236
paulson@13797
   237
lemma stable_Un: 
paulson@13805
   238
    "[| F \<in> stable A; F \<in> stable A' |] ==> F \<in> stable (A \<union> A')"
paulson@13797
   239
paulson@13797
   240
apply (unfold stable_def)
paulson@13797
   241
apply (blast intro: constrains_Un)
paulson@13797
   242
done
paulson@13797
   243
paulson@13797
   244
lemma stable_UN: 
paulson@13805
   245
    "(!!i. i \<in> I ==> F \<in> stable (A i)) ==> F \<in> stable (\<Union>i \<in> I. A i)"
paulson@13797
   246
apply (unfold stable_def)
paulson@13797
   247
apply (blast intro: constrains_UN)
paulson@13797
   248
done
paulson@13797
   249
paulson@13870
   250
lemma stable_Union: 
paulson@13870
   251
    "(!!A. A \<in> X ==> F \<in> stable A) ==> F \<in> stable (\<Union>X)"
paulson@13870
   252
by (unfold stable_def constrains_def, blast)
paulson@13870
   253
paulson@16184
   254
subsubsection{*Intersection*}
paulson@13797
   255
paulson@13797
   256
lemma stable_Int: 
paulson@13805
   257
    "[| F \<in> stable A;  F \<in> stable A' |] ==> F \<in> stable (A \<inter> A')"
paulson@13797
   258
apply (unfold stable_def)
paulson@13797
   259
apply (blast intro: constrains_Int)
paulson@13797
   260
done
paulson@13797
   261
paulson@13797
   262
lemma stable_INT: 
paulson@13805
   263
    "(!!i. i \<in> I ==> F \<in> stable (A i)) ==> F \<in> stable (\<Inter>i \<in> I. A i)"
paulson@13797
   264
apply (unfold stable_def)
paulson@13797
   265
apply (blast intro: constrains_INT)
paulson@13797
   266
done
paulson@13797
   267
paulson@13870
   268
lemma stable_Inter: 
paulson@13870
   269
    "(!!A. A \<in> X ==> F \<in> stable A) ==> F \<in> stable (\<Inter>X)"
paulson@13870
   270
by (unfold stable_def constrains_def, blast)
paulson@13870
   271
paulson@13797
   272
lemma stable_constrains_Un: 
paulson@13805
   273
    "[| F \<in> stable C; F \<in> A co (C \<union> A') |] ==> F \<in> (C \<union> A) co (C \<union> A')"
paulson@13797
   274
by (unfold stable_def constrains_def, blast)
paulson@13797
   275
paulson@13797
   276
lemma stable_constrains_Int: 
paulson@13805
   277
  "[| F \<in> stable C; F \<in>  (C \<inter> A) co A' |] ==> F \<in> (C \<inter> A) co (C \<inter> A')"
paulson@13797
   278
by (unfold stable_def constrains_def, blast)
paulson@13797
   279
paulson@13805
   280
(*[| F \<in> stable C; F \<in>  (C \<inter> A) co A |] ==> F \<in> stable (C \<inter> A) *)
wenzelm@45605
   281
lemmas stable_constrains_stable = stable_constrains_Int[THEN stableI]
paulson@13797
   282
paulson@13797
   283
paulson@16184
   284
subsubsection{*invariant*}
paulson@13797
   285
paulson@13805
   286
lemma invariantI: "[| Init F \<subseteq> A;  F \<in> stable A |] ==> F \<in> invariant A"
paulson@13797
   287
by (simp add: invariant_def)
paulson@13797
   288
paulson@14150
   289
text{*Could also say @{term "invariant A \<inter> invariant B \<subseteq> invariant(A \<inter> B)"}*}
paulson@13797
   290
lemma invariant_Int:
paulson@13805
   291
     "[| F \<in> invariant A;  F \<in> invariant B |] ==> F \<in> invariant (A \<inter> B)"
paulson@13797
   292
by (auto simp add: invariant_def stable_Int)
paulson@13797
   293
paulson@13797
   294
paulson@16184
   295
subsubsection{*increasing*}
paulson@13797
   296
paulson@13797
   297
lemma increasingD: 
paulson@13805
   298
     "F \<in> increasing f ==> F \<in> stable {s. z \<subseteq> f s}"
paulson@13797
   299
by (unfold increasing_def, blast)
paulson@13797
   300
paulson@13805
   301
lemma increasing_constant [iff]: "F \<in> increasing (%s. c)"
paulson@13797
   302
by (unfold increasing_def stable_def, auto)
paulson@13797
   303
paulson@13797
   304
lemma mono_increasing_o: 
paulson@13805
   305
     "mono g ==> increasing f \<subseteq> increasing (g o f)"
paulson@13797
   306
apply (unfold increasing_def stable_def constrains_def, auto)
paulson@13797
   307
apply (blast intro: monoD order_trans)
paulson@13797
   308
done
paulson@13797
   309
paulson@13805
   310
(*Holds by the theorem (Suc m \<subseteq> n) = (m < n) *)
paulson@13797
   311
lemma strict_increasingD: 
paulson@13805
   312
     "!!z::nat. F \<in> increasing f ==> F \<in> stable {s. z < f s}"
paulson@13797
   313
by (simp add: increasing_def Suc_le_eq [symmetric])
paulson@13797
   314
paulson@13797
   315
paulson@13797
   316
(** The Elimination Theorem.  The "free" m has become universally quantified!
paulson@13805
   317
    Should the premise be !!m instead of \<forall>m ?  Would make it harder to use
paulson@13797
   318
    in forward proof. **)
paulson@13797
   319
paulson@13797
   320
lemma elimination: 
paulson@13805
   321
    "[| \<forall>m \<in> M. F \<in> {s. s x = m} co (B m) |]  
paulson@13805
   322
     ==> F \<in> {s. s x \<in> M} co (\<Union>m \<in> M. B m)"
paulson@13797
   323
by (unfold constrains_def, blast)
paulson@13797
   324
paulson@13812
   325
text{*As above, but for the trivial case of a one-variable state, in which the
paulson@13812
   326
  state is identified with its one variable.*}
paulson@13797
   327
lemma elimination_sing: 
paulson@13805
   328
    "(\<forall>m \<in> M. F \<in> {m} co (B m)) ==> F \<in> M co (\<Union>m \<in> M. B m)"
paulson@13797
   329
by (unfold constrains_def, blast)
paulson@13797
   330
paulson@13797
   331
paulson@13797
   332
paulson@16184
   333
subsubsection{*Theoretical Results from Section 6*}
paulson@13797
   334
paulson@13797
   335
lemma constrains_strongest_rhs: 
paulson@13805
   336
    "F \<in> A co (strongest_rhs F A )"
paulson@13797
   337
by (unfold constrains_def strongest_rhs_def, blast)
paulson@13797
   338
paulson@13797
   339
lemma strongest_rhs_is_strongest: 
paulson@13805
   340
    "F \<in> A co B ==> strongest_rhs F A \<subseteq> B"
paulson@13797
   341
by (unfold constrains_def strongest_rhs_def, blast)
paulson@13797
   342
paulson@13797
   343
paulson@16184
   344
subsubsection{*Ad-hoc set-theory rules*}
paulson@13797
   345
paulson@13805
   346
lemma Un_Diff_Diff [simp]: "A \<union> B - (A - B) = B"
paulson@13797
   347
by blast
paulson@13797
   348
paulson@13805
   349
lemma Int_Union_Union: "Union(B) \<inter> A = Union((%C. C \<inter> A)`B)"
paulson@13797
   350
by blast
paulson@13797
   351
wenzelm@24147
   352
text{*Needed for WF reasoning in WFair.thy*}
paulson@13797
   353
paulson@13797
   354
lemma Image_less_than [simp]: "less_than `` {k} = greaterThan k"
paulson@13797
   355
by blast
paulson@13797
   356
paulson@13797
   357
lemma Image_inverse_less_than [simp]: "less_than^-1 `` {k} = lessThan k"
paulson@13797
   358
by blast
paulson@6536
   359
paulson@13812
   360
paulson@13812
   361
subsection{*Partial versus Total Transitions*}
paulson@13812
   362
haftmann@35416
   363
definition totalize_act :: "('a * 'a)set => ('a * 'a)set" where
nipkow@30198
   364
    "totalize_act act == act \<union> Id_on (-(Domain act))"
paulson@13812
   365
haftmann@35416
   366
definition totalize :: "'a program => 'a program" where
paulson@13812
   367
    "totalize F == mk_program (Init F,
wenzelm@32960
   368
                               totalize_act ` Acts F,
wenzelm@32960
   369
                               AllowedActs F)"
paulson@13812
   370
haftmann@35416
   371
definition mk_total_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
haftmann@35416
   372
                   => 'a program" where
paulson@13812
   373
    "mk_total_program args == totalize (mk_program args)"
paulson@13812
   374
haftmann@35416
   375
definition all_total :: "'a program => bool" where
paulson@13812
   376
    "all_total F == \<forall>act \<in> Acts F. Domain act = UNIV"
paulson@13812
   377
  
paulson@13812
   378
lemma insert_Id_image_Acts: "f Id = Id ==> insert Id (f`Acts F) = f ` Acts F"
paulson@13812
   379
by (blast intro: sym [THEN image_eqI])
paulson@13812
   380
paulson@13812
   381
paulson@16184
   382
subsubsection{*Basic properties*}
paulson@13812
   383
paulson@13812
   384
lemma totalize_act_Id [simp]: "totalize_act Id = Id"
paulson@13812
   385
by (simp add: totalize_act_def) 
paulson@13812
   386
paulson@13812
   387
lemma Domain_totalize_act [simp]: "Domain (totalize_act act) = UNIV"
paulson@13812
   388
by (auto simp add: totalize_act_def)
paulson@13812
   389
paulson@13812
   390
lemma Init_totalize [simp]: "Init (totalize F) = Init F"
paulson@13812
   391
by (unfold totalize_def, auto)
paulson@13812
   392
paulson@13812
   393
lemma Acts_totalize [simp]: "Acts (totalize F) = (totalize_act ` Acts F)"
paulson@13812
   394
by (simp add: totalize_def insert_Id_image_Acts) 
paulson@13812
   395
paulson@13812
   396
lemma AllowedActs_totalize [simp]: "AllowedActs (totalize F) = AllowedActs F"
paulson@13812
   397
by (simp add: totalize_def)
paulson@13812
   398
paulson@13812
   399
lemma totalize_constrains_iff [simp]: "(totalize F \<in> A co B) = (F \<in> A co B)"
paulson@13812
   400
by (simp add: totalize_def totalize_act_def constrains_def, blast)
paulson@13812
   401
paulson@13812
   402
lemma totalize_stable_iff [simp]: "(totalize F \<in> stable A) = (F \<in> stable A)"
paulson@13812
   403
by (simp add: stable_def)
paulson@13812
   404
paulson@13812
   405
lemma totalize_invariant_iff [simp]:
paulson@13812
   406
     "(totalize F \<in> invariant A) = (F \<in> invariant A)"
paulson@13812
   407
by (simp add: invariant_def)
paulson@13812
   408
paulson@13812
   409
lemma all_total_totalize: "all_total (totalize F)"
paulson@13812
   410
by (simp add: totalize_def all_total_def)
paulson@13812
   411
paulson@13812
   412
lemma Domain_iff_totalize_act: "(Domain act = UNIV) = (totalize_act act = act)"
paulson@13812
   413
by (force simp add: totalize_act_def)
paulson@13812
   414
paulson@13812
   415
lemma all_total_imp_totalize: "all_total F ==> (totalize F = F)"
paulson@13812
   416
apply (simp add: all_total_def totalize_def) 
paulson@13812
   417
apply (rule program_equalityI)
paulson@13812
   418
  apply (simp_all add: Domain_iff_totalize_act image_def)
paulson@13812
   419
done
paulson@13812
   420
paulson@13812
   421
lemma all_total_iff_totalize: "all_total F = (totalize F = F)"
paulson@13812
   422
apply (rule iffI) 
paulson@13812
   423
 apply (erule all_total_imp_totalize) 
paulson@13812
   424
apply (erule subst) 
paulson@13812
   425
apply (rule all_total_totalize) 
paulson@13812
   426
done
paulson@13812
   427
paulson@13812
   428
lemma mk_total_program_constrains_iff [simp]:
paulson@13812
   429
     "(mk_total_program args \<in> A co B) = (mk_program args \<in> A co B)"
paulson@13812
   430
by (simp add: mk_total_program_def)
paulson@13812
   431
paulson@13812
   432
paulson@13812
   433
subsection{*Rules for Lazy Definition Expansion*}
paulson@13812
   434
paulson@13812
   435
text{*They avoid expanding the full program, which is a large expression*}
paulson@13812
   436
paulson@13812
   437
lemma def_prg_Init:
wenzelm@36866
   438
     "F = mk_total_program (init,acts,allowed) ==> Init F = init"
paulson@13812
   439
by (simp add: mk_total_program_def)
paulson@13812
   440
paulson@13812
   441
lemma def_prg_Acts:
wenzelm@36866
   442
     "F = mk_total_program (init,acts,allowed) 
paulson@13812
   443
      ==> Acts F = insert Id (totalize_act ` acts)"
paulson@13812
   444
by (simp add: mk_total_program_def)
paulson@13812
   445
paulson@13812
   446
lemma def_prg_AllowedActs:
wenzelm@36866
   447
     "F = mk_total_program (init,acts,allowed)  
paulson@13812
   448
      ==> AllowedActs F = insert Id allowed"
paulson@13812
   449
by (simp add: mk_total_program_def)
paulson@13812
   450
paulson@13812
   451
text{*An action is expanded if a pair of states is being tested against it*}
paulson@13812
   452
lemma def_act_simp:
wenzelm@36866
   453
     "act = {(s,s'). P s s'} ==> ((s,s') \<in> act) = P s s'"
paulson@13812
   454
by (simp add: mk_total_program_def)
paulson@13812
   455
paulson@13812
   456
text{*A set is expanded only if an element is being tested against it*}
wenzelm@36866
   457
lemma def_set_simp: "A = B ==> (x \<in> A) = (x \<in> B)"
paulson@13812
   458
by (simp add: mk_total_program_def)
paulson@13812
   459
paulson@16184
   460
subsubsection{*Inspectors for type "program"*}
paulson@13812
   461
paulson@13812
   462
lemma Init_total_eq [simp]:
paulson@13812
   463
     "Init (mk_total_program (init,acts,allowed)) = init"
paulson@13812
   464
by (simp add: mk_total_program_def)
paulson@13812
   465
paulson@13812
   466
lemma Acts_total_eq [simp]:
paulson@13812
   467
    "Acts(mk_total_program(init,acts,allowed)) = insert Id (totalize_act`acts)"
paulson@13812
   468
by (simp add: mk_total_program_def)
paulson@13812
   469
paulson@13812
   470
lemma AllowedActs_total_eq [simp]:
paulson@13812
   471
     "AllowedActs (mk_total_program (init,acts,allowed)) = insert Id allowed"
paulson@13812
   472
by (auto simp add: mk_total_program_def)
paulson@13812
   473
paulson@4776
   474
end