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