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