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