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