1 2(*****************************************************************************) 3(* Create "UnclockedSemanticsTheory" containing unclocked semantics *) 4(* of PSL Version 1.1. *) 5(*****************************************************************************) 6 7(*****************************************************************************) 8(* START BOILERPLATE *) 9(*****************************************************************************) 10 11(****************************************************************************** 12* Load theory of syntax, paths and models 13* (commented out for compilation) 14******************************************************************************) 15(* 16quietdec := true; 17loadPath (* Add path to loadPath *) 18 := 19 "../../path" :: !loadPath; 20map load 21 ["SyntaxTheory","PSLPathTheory","ModelTheory"]; 22quietdec := false; 23*) 24 25(****************************************************************************** 26* Boilerplate needed for compilation 27******************************************************************************) 28open HolKernel Parse boolLib bossLib; 29 30(****************************************************************************** 31* Open theories of sequences and lists 32******************************************************************************) 33open SyntaxTheory PSLPathTheory ModelTheory; 34 35(*****************************************************************************) 36(* END BOILERPLATE *) 37(*****************************************************************************) 38 39(****************************************************************************** 40* Start a new theory called UnclockedSemantics 41******************************************************************************) 42val _ = new_theory "UnclockedSemantics"; 43val _ = ParseExtras.temp_loose_equality() 44 45(****************************************************************************** 46* pureDefine doesn't export definitions to theCompset (for EVAL). 47******************************************************************************) 48val pureDefine = with_flag (computeLib.auto_import_definitions, false) Define; 49 50(* Moved to ModelScript.sml 51(****************************************************************************** 52* A letter is either TOP, or BOTTOM 53* or a set of atomic propositions repersenting a state 54******************************************************************************) 55val letter_def = 56 Hol_datatype 57 `letter = TOP | BOTTOM | STATE of ('prop -> bool)`; 58*) 59 60(****************************************************************************** 61* B_SEM l b means "l ||= b" where l is a letter 62******************************************************************************) 63val B_SEM_def = 64 Define 65 `(B_SEM TOP b = T) 66 /\ 67 (B_SEM BOTTOM b = F) 68 /\ 69 (B_SEM (STATE s) (B_PROP(p:'prop)) = p IN s) 70 /\ 71 (B_SEM (STATE s) B_TRUE = T) 72 /\ 73 (B_SEM (STATE s) B_FALSE = F) 74 /\ 75 (B_SEM (STATE s) (B_NOT b) = ~(B_SEM (STATE s) b)) 76 /\ 77 (B_SEM (STATE s) (B_AND(b1,b2)) = B_SEM (STATE s) b1 /\ B_SEM (STATE s) b2)`; 78 79(****************************************************************************** 80* Unclocked semantics of SEREs. 81* US_SEM v r means "v is in the language of r" in the unclocked semantics 82* where v is a finite word, i.e. a list of letters: v : ('a letter)list. 83* US_SEM_def is a simple structural recursion for easy definition 84* (see clause for ``US_SEM v (S_REPEAT r)``). 85* Theorem US_SEM gives version corresponding to LRM Version 1.1. 86******************************************************************************) 87val US_SEM_def = 88 pureDefine 89 `(US_SEM v (S_BOOL b) = (LENGTH v = 1) /\ B_SEM (ELEM v 0) b) 90 /\ 91 (US_SEM v (S_CAT(r1,r2)) = 92 ?v1 v2. (v = v1 <> v2) /\ US_SEM v1 r1 /\ US_SEM v2 r2) 93 /\ 94 (US_SEM v (S_FUSION(r1,r2)) = 95 ?v1 v2 l. (v = v1 <> [l] <> v2) /\ 96 US_SEM (v1<>[l]) r1 /\ US_SEM ([l]<>v2) r2) 97 /\ 98 (US_SEM v (S_OR(r1,r2)) = 99 US_SEM v r1 \/ US_SEM v r2) 100 /\ 101 (US_SEM v (S_AND(r1,r2)) = 102 US_SEM v r1 /\ US_SEM v r2) 103 /\ 104 (US_SEM v S_EMPTY = 105 (v = [])) 106 /\ 107 (US_SEM v (S_REPEAT r) = 108 ?vlist. (v = CONCAT vlist) /\ EVERY (\v. US_SEM v r) vlist)`; 109 110(* Lemma for deriving theorem US_SEM below *) 111val US_SEM_REPEAT = 112 store_thm 113 ("US_SEM_REPEAT", 114 ``US_SEM v (S_REPEAT r) = 115 US_SEM v S_EMPTY \/ 116 ?v1 v2. 117 ~(v=[]) /\ (v = v1 <> v2) /\ US_SEM v1 r /\ US_SEM v2 (S_REPEAT r)``, 118 Induct_on `v` 119 THEN RW_TAC std_ss [US_SEM_def] 120 THENL 121 [Q.EXISTS_TAC `[]` 122 THEN RW_TAC list_ss [FinitePSLPathTheory.CONCAT_def], 123 EQ_TAC 124 THEN RW_TAC list_ss [] 125 THENL 126 [Cases_on `vlist` 127 THEN FULL_SIMP_TAC list_ss [FinitePSLPathTheory.CONCAT_def] 128 THEN Q.EXISTS_TAC `h'` THEN Q.EXISTS_TAC `CONCAT t` 129 THEN PROVE_TAC[], 130 Q.EXISTS_TAC `v1::vlist` 131 THEN RW_TAC list_ss [FinitePSLPathTheory.CONCAT_def]]]); 132 133(****************************************************************************** 134* Unclocked semantics of SEREs. 135* US_SEM v r means "v is in the language of r" in the unclocked semantics 136* where v is a finite word, i.e. a list of letters: v : ('a letter)list. 137* US_SEM_def is a simple structural recursion for easy definition 138* (see clause for ``US_SEM v (S_REPEAT r)``). 139* Theorem US_SEM gives version corresponding to LRM Version 1.1. 140******************************************************************************) 141val US_SEM = 142 store_thm 143 ("US_SEM", 144 ``(US_SEM v (S_BOOL b) = (LENGTH v = 1) /\ B_SEM (ELEM v 0) b) 145 /\ 146 (US_SEM v (S_CAT(r1,r2)) = 147 ?v1 v2. (v = v1 <> v2) /\ US_SEM v1 r1 /\ US_SEM v2 r2) 148 /\ 149 (US_SEM v (S_FUSION(r1,r2)) = 150 ?v1 v2 l. (v = v1 <> [l] <> v2) /\ 151 US_SEM (v1<>[l]) r1 /\ US_SEM ([l]<>v2) r2) 152 /\ 153 (US_SEM v (S_OR(r1,r2)) = 154 US_SEM v r1 \/ US_SEM v r2) 155 /\ 156 (US_SEM v (S_AND(r1,r2)) = 157 US_SEM v r1 /\ US_SEM v r2) 158 /\ 159 (US_SEM v S_EMPTY = 160 (v = [])) 161 /\ 162 (US_SEM v (S_REPEAT r) = 163 US_SEM v S_EMPTY \/ 164 ?v1 v2. 165 ~(v=[]) /\ (v = v1 <> v2) /\ US_SEM v1 r /\ US_SEM v2 (S_REPEAT r))``, 166 RW_TAC std_ss [US_SEM_def, GSYM US_SEM_REPEAT]); 167 168(****************************************************************************** 169* Complement a path 170******************************************************************************) 171val COMPLEMENT_LETTER_def = 172 Define 173 `(COMPLEMENT_LETTER TOP = BOTTOM) /\ 174 (COMPLEMENT_LETTER BOTTOM = TOP) /\ 175 (COMPLEMENT_LETTER(STATE s) = STATE s)`; 176 177(****************************************************************************** 178* Complement a path 179******************************************************************************) 180val COMPLEMENT_def = 181 Define 182 `(COMPLEMENT(FINITE p) = FINITE(MAP COMPLEMENT_LETTER p)) /\ 183 (COMPLEMENT(INFINITE f) = INFINITE(COMPLEMENT_LETTER o f))`; 184 185(****************************************************************************** 186* \top^\omega 187******************************************************************************) 188val TOP_OMEGA_def = 189 Define `TOP_OMEGA = INFINITE(\n. TOP)`; 190 191(****************************************************************************** 192* LESS m is predicate to test if a number is less than m 193* LESS : num -> num -> bool 194* LESSX m is predicate to test if a number is less than extended number m 195* LESSX : xnum -> num -> bool 196* Now defined in PSLPathTheory 197******************************************************************************) 198 199(****************************************************************************** 200* UF_SEM v f means "v |= f" in the unclocked semantics 201* where v is a finite or infinite word i.e. v : ('prop -> bool)path 202* UF_SEM_def is unfolded version for easy definition. 203* Theorem UF_SEM gives version corresponding to LRM v1.1 204******************************************************************************) 205val UF_SEM_def = 206 Define 207 `(UF_SEM v (F_NOT f) = 208 ~(UF_SEM (COMPLEMENT v) f)) 209 /\ 210 (UF_SEM v (F_AND(f1,f2)) = 211 UF_SEM v f1 /\ UF_SEM v f2) 212 /\ 213 (UF_SEM v (F_STRONG_BOOL b) = 214 (LENGTH v > 0) /\ B_SEM (ELEM v 0) b) 215 /\ 216 (UF_SEM v (F_WEAK_BOOL b) = 217 (LENGTH v = XNUM 0) \/ B_SEM (ELEM v 0) b) 218 /\ 219 (UF_SEM v (F_STRONG_SERE r) = 220 ?j :: (LESS(LENGTH v)). US_SEM (SEL v (0,j)) r) 221(* 222 /\ 223 (UF_SEM v (F_WEAK_SERE r) = 224 !j :: (LESS(LENGTH v)). 225 UF_SEM (CAT(SEL v (0,j),TOP_OMEGA)) (F_STRONG_SERE r)) 226*) 227 /\ 228 (UF_SEM v (F_WEAK_SERE r) = 229 !j :: (LESS(LENGTH v)). 230 ?k :: (LESS(LENGTH(CAT(SEL v (0,j),TOP_OMEGA)))). 231 US_SEM (SEL(CAT(SEL v (0,j),TOP_OMEGA)) (0,k)) r) 232 /\ 233 (UF_SEM v (F_NEXT f) = 234 LENGTH v > 1 /\ UF_SEM (RESTN v 1) f) 235 /\ 236 (UF_SEM v (F_UNTIL(f1,f2)) = 237 ?k :: (LESS(LENGTH v)). 238 UF_SEM (RESTN v k) f2 /\ !j :: (LESS k). UF_SEM (RESTN v j) f1) 239 /\ 240(* Contains j=0 bug spotted by Thomas Turk 241 (UF_SEM v (F_ABORT (f,b)) = 242 UF_SEM v f 243 \/ 244 ?j :: (LESS(LENGTH v)). 245 B_SEM (ELEM v j) b /\ UF_SEM (CAT(SEL v (0,j-1),TOP_OMEGA)) f) 246*) 247 (UF_SEM v (F_ABORT (f,b)) = 248 UF_SEM v f 249 \/ 250 ?j :: (LESS(LENGTH v)). 251 B_SEM (ELEM v j) b 252 /\ 253 if j=0 then UF_SEM TOP_OMEGA f 254 else UF_SEM (CAT(SEL v (0,j-1),TOP_OMEGA)) f) 255 /\ 256 (UF_SEM v (F_SUFFIX_IMP(r,f)) = 257 !j :: (LESS(LENGTH v)). 258 US_SEM (SEL (COMPLEMENT v) (0,j)) r ==> UF_SEM (RESTN v j) f)`; 259 260(****************************************************************************** 261* UF_SEM v f means "v |= f" in the unclocked semantics 262* where v is a finite or infinite word i.e. v : ('prop -> bool)path 263* UF_SEM_def is unfolded version for easy definition. 264* Theorem UF_SEM gives version corresponding to LRM v1.1 265******************************************************************************) 266val UF_SEM = 267 store_thm 268 ("UF_SEM", 269 ``(UF_SEM v (F_NOT f) = 270 ~(UF_SEM (COMPLEMENT v) f)) 271 /\ 272 (UF_SEM v (F_AND(f1,f2)) = 273 UF_SEM v f1 /\ UF_SEM v f2) 274 /\ 275 (UF_SEM v (F_STRONG_BOOL b) = 276 (LENGTH v > 0) /\ B_SEM (ELEM v 0) b) 277 /\ 278 (UF_SEM v (F_WEAK_BOOL b) = 279 (LENGTH v = XNUM 0) \/ B_SEM (ELEM v 0) b) 280 /\ 281 (UF_SEM v (F_STRONG_SERE r) = 282 ?j :: (LESS(LENGTH v)). US_SEM (SEL v (0,j)) r) 283 /\ 284 (UF_SEM v (F_WEAK_SERE r) = 285 !j :: (LESS(LENGTH v)). 286 UF_SEM (CAT(SEL v (0,j),TOP_OMEGA)) (F_STRONG_SERE r)) 287(* 288 /\ 289 (UF_SEM v (F_WEAK_SERE r) = 290 !j :: (LESS(LENGTH v)). 291 ?k :: (LESS(LENGTH(CAT(SEL v (0,j),TOP_OMEGA)))). 292 US_SEM (SEL(CAT(SEL v (0,j),TOP_OMEGA)) (0,k)) r) 293*) 294 /\ 295 (UF_SEM v (F_NEXT f) = 296 LENGTH v > 1 /\ UF_SEM (RESTN v 1) f) 297 /\ 298 (UF_SEM v (F_UNTIL(f1,f2)) = 299 ?k :: (LESS(LENGTH v)). 300 UF_SEM (RESTN v k) f2 /\ !j :: (LESS k). UF_SEM (RESTN v j) f1) 301 /\ 302(* Contains j=0 bug spotted by Thomas Turk 303 (UF_SEM v (F_ABORT (f,b)) = 304 UF_SEM v f 305 \/ 306 ?j :: (LESS(LENGTH v)). 307 B_SEM (ELEM v j) b /\ UF_SEM (CAT(SEL v (0,j-1),TOP_OMEGA)) f) 308*) 309 (UF_SEM v (F_ABORT (f,b)) = 310 UF_SEM v f 311 \/ 312 ?j :: (LESS(LENGTH v)). 313 B_SEM (ELEM v j) b 314 /\ 315 if j=0 then UF_SEM TOP_OMEGA f 316 else UF_SEM (CAT(SEL v (0,j-1),TOP_OMEGA)) f) 317 /\ 318 (UF_SEM v (F_SUFFIX_IMP(r,f)) = 319 !j :: (LESS(LENGTH v)). 320 US_SEM (SEL (COMPLEMENT v) (0,j)) r ==> UF_SEM (RESTN v j) f)``, 321 RW_TAC std_ss [UF_SEM_def]); 322 323(*****************************************************************************) 324(* Map a function over a path (used to define Lhat -- see LRM B.2.2) *) 325(*****************************************************************************) 326val MAP_PATH_def = 327 Define 328 `(MAP_PATH g (FINITE l) = FINITE(MAP g l)) 329 /\ 330 (MAP_PATH g (INFINITE f) = INFINITE(\n. g(f n)))`; 331 332(****************************************************************************** 333* UF_VALID M f means "Lhat(pi) |= f" for all computations pi of M 334******************************************************************************) 335val UF_VALID_def = (* from UnclockedSemanticsScript.sml *) 336 Define 337 `UF_VALID M f = 338 !v::(COMPUTATION M). UF_SEM (MAP_PATH (\s. STATE(M.L s)) v) f`; 339 340(****************************************************************************** 341* PATH M s is true of p iff p is a computation path of M 342* (now defined in ModelTheory) 343******************************************************************************) 344 345(****************************************************************************** 346* O_SEM M s f means "M, s |= f" 347******************************************************************************) 348val O_SEM_def = 349 Define 350 `(O_SEM M (O_BOOL b) s = B_SEM (STATE(M.L s)) b) 351 /\ 352 (O_SEM M (O_NOT f) s = ~(O_SEM M f s)) 353 /\ 354 (O_SEM M (O_AND(f1,f2)) s = O_SEM M f1 s /\ O_SEM M f2 s) 355 /\ 356 (O_SEM M (O_EX f) s = 357 ?p :: PATH M s. 358 (LENGTH p > 1) /\ (ELEM p 0 = s) /\ O_SEM M f (ELEM p 1)) 359 /\ 360 (O_SEM M (O_EU(f1,f2)) s = 361 ?p :: PATH M s. 362 ?k :: (LESS(LENGTH p)). 363 (ELEM p 0 = s) /\ 364 O_SEM M f2 (ELEM p k) /\ 365 !j. j < k ==> O_SEM M f1 (ELEM p j)) 366 /\ 367 (O_SEM M (O_EG f) s = 368 ?p :: PATH M s. 369 (ELEM p 0 = s) /\ !j :: (LESS(LENGTH p)). O_SEM M f (ELEM p j))`; 370 371(****************************************************************************** 372* O_VALID M f means "M, s |= f" for all initial states s 373******************************************************************************) 374val O_VALID_def = 375 Define 376 `O_VALID M f = !s::(M.S0). O_SEM M f s`; 377 378val _ = export_theory(); 379