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