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