1 2(*****************************************************************************) 3(* Create "Clockedsugarsemanticstheory" containing clocked 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; 17map load 18 ["SyntaxTheory","UnclockedSemanticsTheory"]; 19open SyntaxTheory PSLPathTheory ModelTheory UnclockedSemanticsTheory; 20quietdec := false; 21*) 22 23(****************************************************************************** 24* Boilerplate needed for compilation 25******************************************************************************) 26open HolKernel Parse boolLib bossLib; 27 28(****************************************************************************** 29* Open theories of sequences and lists 30******************************************************************************) 31open SyntaxTheory PSLPathTheory ModelTheory UnclockedSemanticsTheory; 32 33(*****************************************************************************) 34(* END BOILERPLATE *) 35(*****************************************************************************) 36 37(****************************************************************************** 38* Start a new theory called ClockedSemantics 39******************************************************************************) 40val _ = new_theory "ClockedSemantics"; 41val _ = ParseExtras.temp_loose_equality() 42 43(****************************************************************************** 44* pureDefine doesn't export definitions to theCompset (for EVAL). 45******************************************************************************) 46val pureDefine = with_flag (computeLib.auto_import_definitions, false) Define; 47 48(****************************************************************************** 49* CLOCK_TICK v c formalises "v is a clock tick of c" 50******************************************************************************) 51val CLOCK_TICK_def = 52 Define 53 `CLOCK_TICK v c = 54 LENGTH v > 0 /\ 55 B_SEM (ELEM v (LENGTH v - 1)) c /\ 56 !i :: LESS(LENGTH v - 1). B_SEM (ELEM v i) (B_NOT c)`; 57 58(****************************************************************************** 59* Clocked semantics of SEREs. 60* S_SEM v r means "v is in the language of r" in the clocked semantics 61* where v is a finite word, i.e. a list of letters: v : ('a letter)list. 62* S_SEM_def is a simple structural recursion for easy definition 63* (see clause for ``S_SEM v (S_REPEAT r)``). 64* Theorem S_SEM gives LRM v1.1 version. 65******************************************************************************) 66val S_SEM_def = 67 pureDefine 68 `(S_SEM v c (S_BOOL b) = CLOCK_TICK v c /\ B_SEM (ELEM v (LENGTH v - 1)) b) 69 /\ 70 (S_SEM v c (S_CAT(r1,r2)) = 71 ?v1 v2. (v = v1 <> v2) /\ S_SEM v1 c r1 /\ S_SEM v2 c r2) 72 /\ 73 (S_SEM v c (S_FUSION(r1,r2)) = 74 ?v1 v2 l. (v = v1 <> [l] <> v2) /\ 75 S_SEM (v1<>[l]) c r1 /\ S_SEM ([l]<>v2) c r2) 76 /\ 77 (S_SEM v c (S_OR(r1,r2)) = 78 S_SEM v c r1 \/ S_SEM v c r2) 79 /\ 80 (S_SEM v c (S_AND(r1,r2)) = 81 S_SEM v c r1 /\ S_SEM v c r2) 82 /\ 83 (S_SEM v c S_EMPTY = 84 (v = [])) 85 /\ 86 (S_SEM v c (S_REPEAT r) = 87 ?vlist. (v = CONCAT vlist) /\ EVERY (\v. S_SEM v c r) vlist) 88 /\ 89 (S_SEM v c (S_CLOCK(r,c1)) = 90 S_SEM v c1 r)`; 91 92(* Lemma for deriving theorem S_SEM below *) 93val S_SEM_REPEAT = 94 store_thm 95 ("S_SEM_REPEAT", 96 ``S_SEM v c (S_REPEAT r) = 97 S_SEM v c S_EMPTY \/ 98 ?v1 v2. 99 ~(v=[]) /\ (v = v1 <> v2) /\ S_SEM v1 c r /\ S_SEM v2 c (S_REPEAT r)``, 100 Induct_on `v` 101 THEN RW_TAC std_ss [S_SEM_def] 102 THENL 103 [Q.EXISTS_TAC `[]` 104 THEN RW_TAC list_ss [FinitePSLPathTheory.CONCAT_def], 105 EQ_TAC 106 THEN RW_TAC list_ss [] 107 THENL 108 [Cases_on `vlist` 109 THEN FULL_SIMP_TAC list_ss [FinitePSLPathTheory.CONCAT_def] 110 THEN Q.EXISTS_TAC `h'` THEN Q.EXISTS_TAC `CONCAT t` 111 THEN PROVE_TAC[], 112 Q.EXISTS_TAC `v1::vlist` 113 THEN RW_TAC list_ss [FinitePSLPathTheory.CONCAT_def]]]); 114 115 116(****************************************************************************** 117* Clocked semantics of SEREs. 118* S_SEM v r means "v is in the language of r" in the clocked semantics: v |=c r 119* where v is a finite word, i.e. a list of letters: v : ('a letter)list. 120* S_SEM_def is a simple structural recursion for easy definition 121* (see clause for ``S_SEM v (S_REPEAT r)``). 122* Theorem S_SEM gives LRM v1.1 version. 123******************************************************************************) 124val S_SEM = 125 store_thm 126 ("S_SEM", 127 ``(S_SEM v c (S_BOOL b) = CLOCK_TICK v c /\ B_SEM (ELEM v (LENGTH v - 1)) b) 128 /\ 129 (S_SEM v c (S_CAT(r1,r2)) = 130 ?v1 v2. (v = v1 <> v2) /\ S_SEM v1 c r1 /\ S_SEM v2 c r2) 131 /\ 132 (S_SEM v c (S_FUSION(r1,r2)) = 133 ?v1 v2 l. (v = v1 <> [l] <> v2) /\ 134 S_SEM (v1<>[l]) c r1 /\ S_SEM ([l]<>v2) c r2) 135 /\ 136 (S_SEM v c (S_OR(r1,r2)) = 137 S_SEM v c r1 \/ S_SEM v c r2) 138 /\ 139 (S_SEM v c (S_AND(r1,r2)) = 140 S_SEM v c r1 /\ S_SEM v c r2) 141 /\ 142 (S_SEM v c S_EMPTY = 143 (v = [])) 144 /\ 145 (S_SEM v c (S_REPEAT r) = 146 S_SEM v c S_EMPTY \/ 147 ?v1 v2. 148 ~(v=[]) /\ (v = v1 <> v2) /\ S_SEM v1 c r /\ S_SEM v2 c (S_REPEAT r)) 149 /\ 150 (S_SEM v c (S_CLOCK(r,c1)) = 151 S_SEM v c1 r)``, 152 RW_TAC std_ss [S_SEM_def, GSYM S_SEM_REPEAT]); 153 154 155(****************************************************************************** 156* F_SEM v c f means "v |=c f" in the clocked semantics 157* where v is a finite or infinite word i.e. v : ('prop letter)path 158* F_SEM_def is unfolded version for easy definition. 159* Theorem F_SEM gives version corresponding to LRM v1.1 160******************************************************************************) 161val F_SEM_def = 162 Define 163 `(F_SEM v c (F_NOT f) = 164 ~(F_SEM (COMPLEMENT v) c f)) 165 /\ 166 (F_SEM v c (F_AND(f1,f2)) = 167 F_SEM v c f1 /\ F_SEM v c f2) 168 /\ 169 (F_SEM v c (F_STRONG_BOOL b) = 170 ?j :: LESS(LENGTH v). CLOCK_TICK (SEL v (0,j)) c /\ B_SEM (ELEM v j) b) 171 /\ 172 (F_SEM v c (F_WEAK_BOOL b) = 173 !j :: LESS(LENGTH v). 174 CLOCK_TICK (SEL (COMPLEMENT v) (0,j)) c ==> B_SEM (ELEM v j) b) 175 /\ 176 (F_SEM v c (F_STRONG_SERE r) = 177 ?j :: LESS(LENGTH v). S_SEM (SEL v (0,j)) c r) 178(* 179 /\ 180 (F_SEM v c (F_WEAK_SERE r) = 181 !j :: LESS(LENGTH v). 182 F_SEM (CAT(SEL v (0,j),TOP_OMEGA)) c (F_STRONG_SERE r)) 183*) 184 /\ 185 (F_SEM v c (F_WEAK_SERE r) = 186 !j :: LESS(LENGTH v). 187 ?k :: LESS(LENGTH(CAT(SEL v (0,j),TOP_OMEGA))). 188 S_SEM (SEL(CAT(SEL v (0,j),TOP_OMEGA)) (0,k)) c r) 189 /\ 190 (F_SEM v c (F_NEXT f) = 191 ?j k :: LESS(LENGTH v). 192 j < k /\ 193 CLOCK_TICK (SEL v (0,j)) c /\ 194 CLOCK_TICK (SEL v (j+1,k)) c /\ 195 F_SEM (RESTN v k) c f) 196 /\ 197 (F_SEM v c (F_UNTIL(f1,f2)) = 198 ?k :: LESS(LENGTH v). 199 B_SEM (ELEM v k) c /\ 200 F_SEM (RESTN v k) c f2 /\ 201 !j :: LESS k. B_SEM (ELEM (COMPLEMENT v) j) c ==> F_SEM (RESTN v j) c f1) 202 /\ 203(* Contains j=0 bug spoteed by Thomas Turk 204 (F_SEM v c (F_ABORT (f,b)) = 205 F_SEM v c f 206 \/ 207 ?j :: LESS(LENGTH v). 208 B_SEM (ELEM v j) b /\ F_SEM (CAT(SEL v (0,j-1),TOP_OMEGA)) c f) 209*) 210 (F_SEM v c (F_ABORT (f,b)) = 211 F_SEM v c f 212 \/ 213 ?j :: LESS(LENGTH v). 214 B_SEM (ELEM v j) b 215 /\ 216 if j=0 then F_SEM TOP_OMEGA c f 217 else F_SEM (CAT(SEL v (0,j-1),TOP_OMEGA)) c f) 218 /\ 219 (F_SEM v c (F_CLOCK(f,c1)) = 220 F_SEM v c1 f) 221 /\ 222 (F_SEM v c (F_SUFFIX_IMP(r,f)) = 223 !j :: LESS(LENGTH v). 224 S_SEM (SEL (COMPLEMENT v) (0,j)) c r ==> F_SEM (RESTN v j) c f)`; 225 226(****************************************************************************** 227* F_SEM v c f means "v |=c f" in the clocked semantics 228* where v is a finite or infinite word i.e. v : ('prop letter)path 229* F_SEM_def is unfolded version for easy definition. 230* Theorem F_SEM gives version corresponding to LRM v1.1 231******************************************************************************) 232val F_SEM = 233 store_thm 234 ("F_SEM", 235 ``(F_SEM v c (F_NOT f) = 236 ~(F_SEM (COMPLEMENT v) c f)) 237 /\ 238 (F_SEM v c (F_AND(f1,f2)) = 239 F_SEM v c f1 /\ F_SEM v c f2) 240 /\ 241 (F_SEM v c (F_STRONG_BOOL b) = 242 ?j :: LESS(LENGTH v). CLOCK_TICK (SEL v (0,j)) c /\ B_SEM (ELEM v j) b) 243 /\ 244 (F_SEM v c (F_WEAK_BOOL b) = 245 !j :: LESS(LENGTH v). 246 CLOCK_TICK (SEL (COMPLEMENT v) (0,j)) c ==> B_SEM (ELEM v j) b) 247 /\ 248 (F_SEM v c (F_STRONG_SERE r) = 249 ?j :: LESS(LENGTH v). S_SEM (SEL v (0,j)) c r) 250 /\ 251 (F_SEM v c (F_WEAK_SERE r) = 252 !j :: LESS(LENGTH v). 253 F_SEM (CAT(SEL v (0,j),TOP_OMEGA)) c (F_STRONG_SERE r)) 254(* 255 /\ 256 (F_SEM v c (F_WEAK_SERE r) = 257 !j :: LESS(LENGTH v). 258 ?k :: LESS(LENGTH(CAT(SEL v (0,j),TOP_OMEGA))). 259 S_SEM (SEL(CAT(SEL v (0,j),TOP_OMEGA)) (0,k)) c r) 260*) 261 /\ 262 (F_SEM v c (F_NEXT f) = 263 ?j k :: LESS(LENGTH v). 264 j < k /\ 265 CLOCK_TICK (SEL v (0,j)) c /\ 266 CLOCK_TICK (SEL v (j+1,k)) c /\ 267 F_SEM (RESTN v k) c f) 268 /\ 269 (F_SEM v c (F_UNTIL(f1,f2)) = 270 ?k :: LESS(LENGTH v). 271 B_SEM (ELEM v k) c /\ 272 F_SEM (RESTN v k) c f2 /\ 273 !j :: LESS k. B_SEM (ELEM (COMPLEMENT v) j) c ==> F_SEM (RESTN v j) c f1) 274 /\ 275(* Contains j=0 bug spoteed by Thomas Turk 276 (F_SEM v c (F_ABORT (f,b)) = 277 F_SEM v c f 278 \/ 279 ?j :: LESS(LENGTH v). 280 B_SEM (ELEM v j) b /\ F_SEM (CAT(SEL v (0,j-1),TOP_OMEGA)) c f) 281*) 282 (F_SEM v c (F_ABORT (f,b)) = 283 F_SEM v c f 284 \/ 285 ?j :: LESS(LENGTH v). 286 B_SEM (ELEM v j) b 287 /\ 288 if j=0 then F_SEM TOP_OMEGA c f 289 else F_SEM (CAT(SEL v (0,j-1),TOP_OMEGA)) c f) 290 /\ 291 (F_SEM v c (F_CLOCK(f,c1)) = 292 F_SEM v c1 f) 293 /\ 294 (F_SEM v c (F_SUFFIX_IMP(r,f)) = 295 !j :: LESS(LENGTH v). 296 S_SEM (SEL (COMPLEMENT v) (0,j)) c r ==> F_SEM (RESTN v j) c f)``, 297 RW_TAC std_ss [F_SEM_def]); 298 299val _ = export_theory(); 300