1(* Title: ZF/UNITY/UNITY.thy 2 Author: Sidi O Ehmety, Computer Laboratory 3 Copyright 2001 University of Cambridge 4*) 5 6section \<open>The Basic UNITY Theory\<close> 7 8theory UNITY imports State begin 9 10text\<open>The basic UNITY theory (revised version, based upon the "co" operator) 11From Misra, "A Logic for Concurrent Programming", 1994. 12 13This ZF theory was ported from its HOL equivalent.\<close> 14 15definition 16 program :: i where 17 "program == {<init, acts, allowed>: 18 Pow(state) * Pow(Pow(state*state)) * Pow(Pow(state*state)). 19 id(state) \<in> acts & id(state) \<in> allowed}" 20 21definition 22 mk_program :: "[i,i,i]=>i" where 23 \<comment> \<open>The definition yields a program thanks to the coercions 24 init \<inter> state, acts \<inter> Pow(state*state), etc.\<close> 25 "mk_program(init, acts, allowed) == 26 <init \<inter> state, cons(id(state), acts \<inter> Pow(state*state)), 27 cons(id(state), allowed \<inter> Pow(state*state))>" 28 29definition 30 SKIP :: i ("\<bottom>") where 31 "SKIP == mk_program(state, 0, Pow(state*state))" 32 33 (* Coercion from anything to program *) 34definition 35 programify :: "i=>i" where 36 "programify(F) == if F \<in> program then F else SKIP" 37 38definition 39 RawInit :: "i=>i" where 40 "RawInit(F) == fst(F)" 41 42definition 43 Init :: "i=>i" where 44 "Init(F) == RawInit(programify(F))" 45 46definition 47 RawActs :: "i=>i" where 48 "RawActs(F) == cons(id(state), fst(snd(F)))" 49 50definition 51 Acts :: "i=>i" where 52 "Acts(F) == RawActs(programify(F))" 53 54definition 55 RawAllowedActs :: "i=>i" where 56 "RawAllowedActs(F) == cons(id(state), snd(snd(F)))" 57 58definition 59 AllowedActs :: "i=>i" where 60 "AllowedActs(F) == RawAllowedActs(programify(F))" 61 62 63definition 64 Allowed :: "i =>i" where 65 "Allowed(F) == {G \<in> program. Acts(G) \<subseteq> AllowedActs(F)}" 66 67definition 68 initially :: "i=>i" where 69 "initially(A) == {F \<in> program. Init(F)\<subseteq>A}" 70 71definition "constrains" :: "[i, i] => i" (infixl "co" 60) where 72 "A co B == {F \<in> program. (\<forall>act \<in> Acts(F). act``A\<subseteq>B) & st_set(A)}" 73 \<comment> \<open>the condition @{term "st_set(A)"} makes the definition slightly 74 stronger than the HOL one\<close> 75 76definition unless :: "[i, i] => i" (infixl "unless" 60) where 77 "A unless B == (A - B) co (A \<union> B)" 78 79definition 80 stable :: "i=>i" where 81 "stable(A) == A co A" 82 83definition 84 strongest_rhs :: "[i, i] => i" where 85 "strongest_rhs(F, A) == \<Inter>({B \<in> Pow(state). F \<in> A co B})" 86 87definition 88 invariant :: "i => i" where 89 "invariant(A) == initially(A) \<inter> stable(A)" 90 91 (* meta-function composition *) 92definition 93 metacomp :: "[i=>i, i=>i] => (i=>i)" (infixl "comp" 65) where 94 "f comp g == %x. f(g(x))" 95 96definition 97 pg_compl :: "i=>i" where 98 "pg_compl(X)== program - X" 99 100text\<open>SKIP\<close> 101lemma SKIP_in_program [iff,TC]: "SKIP \<in> program" 102by (force simp add: SKIP_def program_def mk_program_def) 103 104 105subsection\<open>The function @{term programify}, the coercion from anything to 106 program\<close> 107 108lemma programify_program [simp]: "F \<in> program ==> programify(F)=F" 109by (force simp add: programify_def) 110 111lemma programify_in_program [iff,TC]: "programify(F) \<in> program" 112by (force simp add: programify_def) 113 114text\<open>Collapsing rules: to remove programify from expressions\<close> 115lemma programify_idem [simp]: "programify(programify(F))=programify(F)" 116by (force simp add: programify_def) 117 118lemma Init_programify [simp]: "Init(programify(F)) = Init(F)" 119by (simp add: Init_def) 120 121lemma Acts_programify [simp]: "Acts(programify(F)) = Acts(F)" 122by (simp add: Acts_def) 123 124lemma AllowedActs_programify [simp]: 125 "AllowedActs(programify(F)) = AllowedActs(F)" 126by (simp add: AllowedActs_def) 127 128subsection\<open>The Inspectors for Programs\<close> 129 130lemma id_in_RawActs: "F \<in> program ==>id(state) \<in> RawActs(F)" 131by (auto simp add: program_def RawActs_def) 132 133lemma id_in_Acts [iff,TC]: "id(state) \<in> Acts(F)" 134by (simp add: id_in_RawActs Acts_def) 135 136lemma id_in_RawAllowedActs: "F \<in> program ==>id(state) \<in> RawAllowedActs(F)" 137by (auto simp add: program_def RawAllowedActs_def) 138 139lemma id_in_AllowedActs [iff,TC]: "id(state) \<in> AllowedActs(F)" 140by (simp add: id_in_RawAllowedActs AllowedActs_def) 141 142lemma cons_id_Acts [simp]: "cons(id(state), Acts(F)) = Acts(F)" 143by (simp add: cons_absorb) 144 145lemma cons_id_AllowedActs [simp]: 146 "cons(id(state), AllowedActs(F)) = AllowedActs(F)" 147by (simp add: cons_absorb) 148 149 150subsection\<open>Types of the Inspectors\<close> 151 152lemma RawInit_type: "F \<in> program ==> RawInit(F)\<subseteq>state" 153by (auto simp add: program_def RawInit_def) 154 155lemma RawActs_type: "F \<in> program ==> RawActs(F)\<subseteq>Pow(state*state)" 156by (auto simp add: program_def RawActs_def) 157 158lemma RawAllowedActs_type: 159 "F \<in> program ==> RawAllowedActs(F)\<subseteq>Pow(state*state)" 160by (auto simp add: program_def RawAllowedActs_def) 161 162lemma Init_type: "Init(F)\<subseteq>state" 163by (simp add: RawInit_type Init_def) 164 165lemmas InitD = Init_type [THEN subsetD] 166 167lemma st_set_Init [iff]: "st_set(Init(F))" 168apply (unfold st_set_def) 169apply (rule Init_type) 170done 171 172lemma Acts_type: "Acts(F)\<subseteq>Pow(state*state)" 173by (simp add: RawActs_type Acts_def) 174 175lemma AllowedActs_type: "AllowedActs(F) \<subseteq> Pow(state*state)" 176by (simp add: RawAllowedActs_type AllowedActs_def) 177 178text\<open>Needed in Behaviors\<close> 179lemma ActsD: "[| act \<in> Acts(F); <s,s'> \<in> act |] ==> s \<in> state & s' \<in> state" 180by (blast dest: Acts_type [THEN subsetD]) 181 182lemma AllowedActsD: 183 "[| act \<in> AllowedActs(F); <s,s'> \<in> act |] ==> s \<in> state & s' \<in> state" 184by (blast dest: AllowedActs_type [THEN subsetD]) 185 186subsection\<open>Simplification rules involving @{term state}, @{term Init}, 187 @{term Acts}, and @{term AllowedActs}\<close> 188 189text\<open>But are they really needed?\<close> 190 191lemma state_subset_is_Init_iff [iff]: "state \<subseteq> Init(F) \<longleftrightarrow> Init(F)=state" 192by (cut_tac F = F in Init_type, auto) 193 194lemma Pow_state_times_state_is_subset_Acts_iff [iff]: 195 "Pow(state*state) \<subseteq> Acts(F) \<longleftrightarrow> Acts(F)=Pow(state*state)" 196by (cut_tac F = F in Acts_type, auto) 197 198lemma Pow_state_times_state_is_subset_AllowedActs_iff [iff]: 199 "Pow(state*state) \<subseteq> AllowedActs(F) \<longleftrightarrow> AllowedActs(F)=Pow(state*state)" 200by (cut_tac F = F in AllowedActs_type, auto) 201 202subsubsection\<open>Eliminating \<open>\<inter> state\<close> from expressions\<close> 203 204lemma Init_Int_state [simp]: "Init(F) \<inter> state = Init(F)" 205by (cut_tac F = F in Init_type, blast) 206 207lemma state_Int_Init [simp]: "state \<inter> Init(F) = Init(F)" 208by (cut_tac F = F in Init_type, blast) 209 210lemma Acts_Int_Pow_state_times_state [simp]: 211 "Acts(F) \<inter> Pow(state*state) = Acts(F)" 212by (cut_tac F = F in Acts_type, blast) 213 214lemma state_times_state_Int_Acts [simp]: 215 "Pow(state*state) \<inter> Acts(F) = Acts(F)" 216by (cut_tac F = F in Acts_type, blast) 217 218lemma AllowedActs_Int_Pow_state_times_state [simp]: 219 "AllowedActs(F) \<inter> Pow(state*state) = AllowedActs(F)" 220by (cut_tac F = F in AllowedActs_type, blast) 221 222lemma state_times_state_Int_AllowedActs [simp]: 223 "Pow(state*state) \<inter> AllowedActs(F) = AllowedActs(F)" 224by (cut_tac F = F in AllowedActs_type, blast) 225 226 227subsubsection\<open>The Operator @{term mk_program}\<close> 228 229lemma mk_program_in_program [iff,TC]: 230 "mk_program(init, acts, allowed) \<in> program" 231by (auto simp add: mk_program_def program_def) 232 233lemma RawInit_eq [simp]: 234 "RawInit(mk_program(init, acts, allowed)) = init \<inter> state" 235by (auto simp add: mk_program_def RawInit_def) 236 237lemma RawActs_eq [simp]: 238 "RawActs(mk_program(init, acts, allowed)) = 239 cons(id(state), acts \<inter> Pow(state*state))" 240by (auto simp add: mk_program_def RawActs_def) 241 242lemma RawAllowedActs_eq [simp]: 243 "RawAllowedActs(mk_program(init, acts, allowed)) = 244 cons(id(state), allowed \<inter> Pow(state*state))" 245by (auto simp add: mk_program_def RawAllowedActs_def) 246 247lemma Init_eq [simp]: "Init(mk_program(init, acts, allowed)) = init \<inter> state" 248by (simp add: Init_def) 249 250lemma Acts_eq [simp]: 251 "Acts(mk_program(init, acts, allowed)) = 252 cons(id(state), acts \<inter> Pow(state*state))" 253by (simp add: Acts_def) 254 255lemma AllowedActs_eq [simp]: 256 "AllowedActs(mk_program(init, acts, allowed))= 257 cons(id(state), allowed \<inter> Pow(state*state))" 258by (simp add: AllowedActs_def) 259 260text\<open>Init, Acts, and AlowedActs of SKIP\<close> 261 262lemma RawInit_SKIP [simp]: "RawInit(SKIP) = state" 263by (simp add: SKIP_def) 264 265lemma RawAllowedActs_SKIP [simp]: "RawAllowedActs(SKIP) = Pow(state*state)" 266by (force simp add: SKIP_def) 267 268lemma RawActs_SKIP [simp]: "RawActs(SKIP) = {id(state)}" 269by (force simp add: SKIP_def) 270 271lemma Init_SKIP [simp]: "Init(SKIP) = state" 272by (force simp add: SKIP_def) 273 274lemma Acts_SKIP [simp]: "Acts(SKIP) = {id(state)}" 275by (force simp add: SKIP_def) 276 277lemma AllowedActs_SKIP [simp]: "AllowedActs(SKIP) = Pow(state*state)" 278by (force simp add: SKIP_def) 279 280text\<open>Equality of UNITY programs\<close> 281 282lemma raw_surjective_mk_program: 283 "F \<in> program ==> mk_program(RawInit(F), RawActs(F), RawAllowedActs(F))=F" 284apply (auto simp add: program_def mk_program_def RawInit_def RawActs_def 285 RawAllowedActs_def, blast+) 286done 287 288lemma surjective_mk_program [simp]: 289 "mk_program(Init(F), Acts(F), AllowedActs(F)) = programify(F)" 290by (auto simp add: raw_surjective_mk_program Init_def Acts_def AllowedActs_def) 291 292lemma program_equalityI: 293 "[|Init(F) = Init(G); Acts(F) = Acts(G); 294 AllowedActs(F) = AllowedActs(G); F \<in> program; G \<in> program |] ==> F = G" 295apply (subgoal_tac "programify(F) = programify(G)") 296apply simp 297apply (simp only: surjective_mk_program [symmetric]) 298done 299 300lemma program_equalityE: 301 "[|F = G; 302 [|Init(F) = Init(G); Acts(F) = Acts(G); AllowedActs(F) = AllowedActs(G) |] 303 ==> P |] 304 ==> P" 305by force 306 307 308lemma program_equality_iff: 309 "[| F \<in> program; G \<in> program |] ==>(F=G) \<longleftrightarrow> 310 (Init(F) = Init(G) & Acts(F) = Acts(G) & AllowedActs(F) = AllowedActs(G))" 311by (blast intro: program_equalityI program_equalityE) 312 313subsection\<open>These rules allow "lazy" definition expansion\<close> 314 315lemma def_prg_Init: 316 "F == mk_program (init,acts,allowed) ==> Init(F) = init \<inter> state" 317by auto 318 319lemma def_prg_Acts: 320 "F == mk_program (init,acts,allowed) 321 ==> Acts(F) = cons(id(state), acts \<inter> Pow(state*state))" 322by auto 323 324lemma def_prg_AllowedActs: 325 "F == mk_program (init,acts,allowed) 326 ==> AllowedActs(F) = cons(id(state), allowed \<inter> Pow(state*state))" 327by auto 328 329lemma def_prg_simps: 330 "[| F == mk_program (init,acts,allowed) |] 331 ==> Init(F) = init \<inter> state & 332 Acts(F) = cons(id(state), acts \<inter> Pow(state*state)) & 333 AllowedActs(F) = cons(id(state), allowed \<inter> Pow(state*state))" 334by auto 335 336 337text\<open>An action is expanded only if a pair of states is being tested against it\<close> 338lemma def_act_simp: 339 "[| act == {<s,s'> \<in> A*B. P(s, s')} |] 340 ==> (<s,s'> \<in> act) \<longleftrightarrow> (<s,s'> \<in> A*B & P(s, s'))" 341by auto 342 343text\<open>A set is expanded only if an element is being tested against it\<close> 344lemma def_set_simp: "A == B ==> (x \<in> A) \<longleftrightarrow> (x \<in> B)" 345by auto 346 347 348subsection\<open>The Constrains Operator\<close> 349 350lemma constrains_type: "A co B \<subseteq> program" 351by (force simp add: constrains_def) 352 353lemma constrainsI: 354 "[|(!!act s s'. [| act: Acts(F); <s,s'> \<in> act; s \<in> A|] ==> s' \<in> A'); 355 F \<in> program; st_set(A) |] ==> F \<in> A co A'" 356by (force simp add: constrains_def) 357 358lemma constrainsD: 359 "F \<in> A co B ==> \<forall>act \<in> Acts(F). act``A\<subseteq>B" 360by (force simp add: constrains_def) 361 362lemma constrainsD2: "F \<in> A co B ==> F \<in> program & st_set(A)" 363by (force simp add: constrains_def) 364 365lemma constrains_empty [iff]: "F \<in> 0 co B \<longleftrightarrow> F \<in> program" 366by (force simp add: constrains_def st_set_def) 367 368lemma constrains_empty2 [iff]: "(F \<in> A co 0) \<longleftrightarrow> (A=0 & F \<in> program)" 369by (force simp add: constrains_def st_set_def) 370 371lemma constrains_state [iff]: "(F \<in> state co B) \<longleftrightarrow> (state\<subseteq>B & F \<in> program)" 372apply (cut_tac F = F in Acts_type) 373apply (force simp add: constrains_def st_set_def) 374done 375 376lemma constrains_state2 [iff]: "F \<in> A co state \<longleftrightarrow> (F \<in> program & st_set(A))" 377apply (cut_tac F = F in Acts_type) 378apply (force simp add: constrains_def st_set_def) 379done 380 381text\<open>monotonic in 2nd argument\<close> 382lemma constrains_weaken_R: 383 "[| F \<in> A co A'; A'\<subseteq>B' |] ==> F \<in> A co B'" 384apply (unfold constrains_def, blast) 385done 386 387text\<open>anti-monotonic in 1st argument\<close> 388lemma constrains_weaken_L: 389 "[| F \<in> A co A'; B\<subseteq>A |] ==> F \<in> B co A'" 390apply (unfold constrains_def st_set_def, blast) 391done 392 393lemma constrains_weaken: 394 "[| F \<in> A co A'; B\<subseteq>A; A'\<subseteq>B' |] ==> F \<in> B co B'" 395apply (drule constrains_weaken_R) 396apply (drule_tac [2] constrains_weaken_L, blast+) 397done 398 399 400subsection\<open>Constrains and Union\<close> 401 402lemma constrains_Un: 403 "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<union> B) co (A' \<union> B')" 404by (auto simp add: constrains_def st_set_def, force) 405 406lemma constrains_UN: 407 "[|!!i. i \<in> I ==> F \<in> A(i) co A'(i); F \<in> program |] 408 ==> F \<in> (\<Union>i \<in> I. A(i)) co (\<Union>i \<in> I. A'(i))" 409by (force simp add: constrains_def st_set_def) 410 411lemma constrains_Un_distrib: 412 "(A \<union> B) co C = (A co C) \<inter> (B co C)" 413by (force simp add: constrains_def st_set_def) 414 415lemma constrains_UN_distrib: 416 "i \<in> I ==> (\<Union>i \<in> I. A(i)) co B = (\<Inter>i \<in> I. A(i) co B)" 417by (force simp add: constrains_def st_set_def) 418 419 420subsection\<open>Constrains and Intersection\<close> 421 422lemma constrains_Int_distrib: "C co (A \<inter> B) = (C co A) \<inter> (C co B)" 423by (force simp add: constrains_def st_set_def) 424 425lemma constrains_INT_distrib: 426 "x \<in> I ==> A co (\<Inter>i \<in> I. B(i)) = (\<Inter>i \<in> I. A co B(i))" 427by (force simp add: constrains_def st_set_def) 428 429lemma constrains_Int: 430 "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<inter> B) co (A' \<inter> B')" 431by (force simp add: constrains_def st_set_def) 432 433lemma constrains_INT [rule_format]: 434 "[| \<forall>i \<in> I. F \<in> A(i) co A'(i); F \<in> program|] 435 ==> F \<in> (\<Inter>i \<in> I. A(i)) co (\<Inter>i \<in> I. A'(i))" 436apply (case_tac "I=0") 437 apply (simp add: Inter_def) 438apply (erule not_emptyE) 439apply (auto simp add: constrains_def st_set_def, blast) 440apply (drule bspec, assumption, force) 441done 442 443(* The rule below simulates the HOL's one for (\<Inter>z. A i) co (\<Inter>z. B i) *) 444lemma constrains_All: 445"[| \<forall>z. F:{s \<in> state. P(s, z)} co {s \<in> state. Q(s, z)}; F \<in> program |]==> 446 F:{s \<in> state. \<forall>z. P(s, z)} co {s \<in> state. \<forall>z. Q(s, z)}" 447by (unfold constrains_def, blast) 448 449lemma constrains_imp_subset: 450 "[| F \<in> A co A' |] ==> A \<subseteq> A'" 451by (unfold constrains_def st_set_def, force) 452 453text\<open>The reasoning is by subsets since "co" refers to single actions 454 only. So this rule isn't that useful.\<close> 455 456lemma constrains_trans: "[| F \<in> A co B; F \<in> B co C |] ==> F \<in> A co C" 457by (unfold constrains_def st_set_def, auto, blast) 458 459lemma constrains_cancel: 460"[| F \<in> A co (A' \<union> B); F \<in> B co B' |] ==> F \<in> A co (A' \<union> B')" 461apply (drule_tac A = B in constrains_imp_subset) 462apply (blast intro: constrains_weaken_R) 463done 464 465 466subsection\<open>The Unless Operator\<close> 467 468lemma unless_type: "A unless B \<subseteq> program" 469by (force simp add: unless_def constrains_def) 470 471lemma unlessI: "[| F \<in> (A-B) co (A \<union> B) |] ==> F \<in> A unless B" 472apply (unfold unless_def) 473apply (blast dest: constrainsD2) 474done 475 476lemma unlessD: "F :A unless B ==> F \<in> (A-B) co (A \<union> B)" 477by (unfold unless_def, auto) 478 479 480subsection\<open>The Operator @{term initially}\<close> 481 482lemma initially_type: "initially(A) \<subseteq> program" 483by (unfold initially_def, blast) 484 485lemma initiallyI: "[| F \<in> program; Init(F)\<subseteq>A |] ==> F \<in> initially(A)" 486by (unfold initially_def, blast) 487 488lemma initiallyD: "F \<in> initially(A) ==> Init(F)\<subseteq>A" 489by (unfold initially_def, blast) 490 491 492subsection\<open>The Operator @{term stable}\<close> 493 494lemma stable_type: "stable(A)\<subseteq>program" 495by (unfold stable_def constrains_def, blast) 496 497lemma stableI: "F \<in> A co A ==> F \<in> stable(A)" 498by (unfold stable_def, assumption) 499 500lemma stableD: "F \<in> stable(A) ==> F \<in> A co A" 501by (unfold stable_def, assumption) 502 503lemma stableD2: "F \<in> stable(A) ==> F \<in> program & st_set(A)" 504by (unfold stable_def constrains_def, auto) 505 506lemma stable_state [simp]: "stable(state) = program" 507by (auto simp add: stable_def constrains_def dest: Acts_type [THEN subsetD]) 508 509 510lemma stable_unless: "stable(A)= A unless 0" 511by (auto simp add: unless_def stable_def) 512 513 514subsection\<open>Union and Intersection with @{term stable}\<close> 515 516lemma stable_Un: 517 "[| F \<in> stable(A); F \<in> stable(A') |] ==> F \<in> stable(A \<union> A')" 518apply (unfold stable_def) 519apply (blast intro: constrains_Un) 520done 521 522lemma stable_UN: 523 "[|!!i. i\<in>I ==> F \<in> stable(A(i)); F \<in> program |] 524 ==> F \<in> stable (\<Union>i \<in> I. A(i))" 525apply (unfold stable_def) 526apply (blast intro: constrains_UN) 527done 528 529lemma stable_Int: 530 "[| F \<in> stable(A); F \<in> stable(A') |] ==> F \<in> stable (A \<inter> A')" 531apply (unfold stable_def) 532apply (blast intro: constrains_Int) 533done 534 535lemma stable_INT: 536 "[| !!i. i \<in> I ==> F \<in> stable(A(i)); F \<in> program |] 537 ==> F \<in> stable (\<Inter>i \<in> I. A(i))" 538apply (unfold stable_def) 539apply (blast intro: constrains_INT) 540done 541 542lemma stable_All: 543 "[|\<forall>z. F \<in> stable({s \<in> state. P(s, z)}); F \<in> program|] 544 ==> F \<in> stable({s \<in> state. \<forall>z. P(s, z)})" 545apply (unfold stable_def) 546apply (rule constrains_All, auto) 547done 548 549lemma stable_constrains_Un: 550 "[| F \<in> stable(C); F \<in> A co (C \<union> A') |] ==> F \<in> (C \<union> A) co (C \<union> A')" 551apply (unfold stable_def constrains_def st_set_def, auto) 552apply (blast dest!: bspec) 553done 554 555lemma stable_constrains_Int: 556 "[| F \<in> stable(C); F \<in> (C \<inter> A) co A' |] ==> F \<in> (C \<inter> A) co (C \<inter> A')" 557by (unfold stable_def constrains_def st_set_def, blast) 558 559(* [| F \<in> stable(C); F \<in> (C \<inter> A) co A |] ==> F \<in> stable(C \<inter> A) *) 560lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI] 561 562subsection\<open>The Operator @{term invariant}\<close> 563 564lemma invariant_type: "invariant(A) \<subseteq> program" 565apply (unfold invariant_def) 566apply (blast dest: stable_type [THEN subsetD]) 567done 568 569lemma invariantI: "[| Init(F)\<subseteq>A; F \<in> stable(A) |] ==> F \<in> invariant(A)" 570apply (unfold invariant_def initially_def) 571apply (frule stable_type [THEN subsetD], auto) 572done 573 574lemma invariantD: "F \<in> invariant(A) ==> Init(F)\<subseteq>A & F \<in> stable(A)" 575by (unfold invariant_def initially_def, auto) 576 577lemma invariantD2: "F \<in> invariant(A) ==> F \<in> program & st_set(A)" 578apply (unfold invariant_def) 579apply (blast dest: stableD2) 580done 581 582text\<open>Could also say 583 @{term "invariant(A) \<inter> invariant(B) \<subseteq> invariant (A \<inter> B)"}\<close> 584lemma invariant_Int: 585 "[| F \<in> invariant(A); F \<in> invariant(B) |] ==> F \<in> invariant(A \<inter> B)" 586apply (unfold invariant_def initially_def) 587apply (simp add: stable_Int, blast) 588done 589 590 591subsection\<open>The Elimination Theorem\<close> 592 593(** The "free" m has become universally quantified! 594 Should the premise be !!m instead of \<forall>m ? Would make it harder 595 to use in forward proof. **) 596 597text\<open>The general case is easier to prove than the special case!\<close> 598lemma "elimination": 599 "[| \<forall>m \<in> M. F \<in> {s \<in> A. x(s) = m} co B(m); F \<in> program |] 600 ==> F \<in> {s \<in> A. x(s) \<in> M} co (\<Union>m \<in> M. B(m))" 601by (auto simp add: constrains_def st_set_def, blast) 602 603text\<open>As above, but for the special case of A=state\<close> 604lemma elimination2: 605 "[| \<forall>m \<in> M. F \<in> {s \<in> state. x(s) = m} co B(m); F \<in> program |] 606 ==> F:{s \<in> state. x(s) \<in> M} co (\<Union>m \<in> M. B(m))" 607by (rule UNITY.elimination, auto) 608 609subsection\<open>The Operator @{term strongest_rhs}\<close> 610 611lemma constrains_strongest_rhs: 612 "[| F \<in> program; st_set(A) |] ==> F \<in> A co (strongest_rhs(F,A))" 613by (auto simp add: constrains_def strongest_rhs_def st_set_def 614 dest: Acts_type [THEN subsetD]) 615 616lemma strongest_rhs_is_strongest: 617 "[| F \<in> A co B; st_set(B) |] ==> strongest_rhs(F,A) \<subseteq> B" 618by (auto simp add: constrains_def strongest_rhs_def st_set_def) 619 620ML \<open> 621fun simp_of_act def = def RS @{thm def_act_simp}; 622fun simp_of_set def = def RS @{thm def_set_simp}; 623\<close> 624 625end 626