1 2(*****************************************************************************) 3(* Create "UnclockedSugarSemanticsTheory" containing unclocked "SEM 1" *) 4(* semantics of the basic language. *) 5(* *) 6(* Created Wed Dec 25 23:02:12 GMT 2002 *) 7(*****************************************************************************) 8 9(*****************************************************************************) 10(* START BOILERPLATE *) 11(*****************************************************************************) 12 13(****************************************************************************** 14* Load theory of finite and infinite sequences and additional definitions of 15functions on lists (commented out for compilation) 16******************************************************************************) 17(* 18quietdec := true; 19map load 20 ["SyntaxTheory", "SyntacticSugarTheory", "PSLPathTheory", "KripkeTheory", 21 "rich_listTheory", "intLib"]; 22 23open SyntaxTheory SyntacticSugarTheory 24 PSLPathTheory KripkeTheory listTheory rich_listTheory intLib; 25 26val _ = intLib.deprecate_int(); 27quietdec := false; 28*) 29 30(****************************************************************************** 31* Boilerplate needed for compilation 32******************************************************************************) 33open HolKernel Parse boolLib bossLib; 34 35(****************************************************************************** 36* Open theories of sequences and lists 37******************************************************************************) 38open SyntaxTheory SyntacticSugarTheory PSLPathTheory KripkeTheory 39 listTheory rich_listTheory intLib; 40 41(****************************************************************************** 42* Set default parsing to natural numbers rather than integers 43******************************************************************************) 44val _ = intLib.deprecate_int(); 45 46(*****************************************************************************) 47(* END BOILERPLATE *) 48(*****************************************************************************) 49 50(****************************************************************************** 51* Start a new theory called UnclockedSugarSemantics 52******************************************************************************) 53val _ = new_theory "UnclockedSemantics"; 54 55(****************************************************************************** 56* pureDefine doesn't export definitions to theCompset (for EVAL). 57******************************************************************************) 58val pureDefine = with_flag (computeLib.auto_import_definitions, false) Define; 59 60(****************************************************************************** 61* B_SEM l b means "l |= b" where l is a letter, i.e. l : 'prop -> bool 62******************************************************************************) 63val B_SEM_def = 64 Define 65 `(B_SEM l (B_PROP(p:'prop)) = p IN l) 66 /\ 67 (B_SEM l (B_NOT b) = ~(B_SEM l b)) 68 /\ 69 (B_SEM l (B_AND(b1,b2)) = B_SEM l b1 /\ B_SEM l b2)`; 70 71val B_SEM = 72 store_thm 73 ("B_SEM", 74 ``(B_SEM l (B_PROP p) = p IN l) 75 /\ 76 (B_SEM l B_TRUE = T) 77 /\ 78 (B_SEM l B_FALSE = F) 79 /\ 80 (B_SEM l (B_NOT b) = ~(B_SEM l b)) 81 /\ 82 (B_SEM l (B_AND(b1,b2)) = B_SEM l b1 /\ B_SEM l b2) 83 /\ 84 (B_SEM l (B_OR(b1,b2)) = B_SEM l b1 \/ B_SEM l b2)``, 85 RW_TAC std_ss [B_SEM_def,B_OR_def,B_TRUE_def,B_FALSE_def] 86 THEN PROVE_TAC[]); 87 88(****************************************************************************** 89* Unclocked "SEM 1" semantics of SEREs. 90* US_SEM w r means "w is in the language of r" in the unclocked semantics 91* where w is a word, i.e. a list of letters: w : ('prop -> bool)list 92******************************************************************************) 93val US_SEM_def = 94 pureDefine 95 `(US_SEM w (S_BOOL b) = (LENGTH w = 1) /\ B_SEM (ELEM w 0) b) 96 /\ 97 (US_SEM w (S_CAT(r1,r2)) = 98 ?w1 w2. (w = w1 <> w2) /\ US_SEM w1 r1 /\ US_SEM w2 r2) 99 /\ 100 (US_SEM w (S_FUSION(r1,r2)) = 101 ?w1 w2 l. (w = w1 <> [l] <> w2) /\ 102 US_SEM (w1<>[l]) r1 /\ US_SEM ([l]<>w2) r2) 103 /\ 104 (US_SEM w (S_OR(r1,r2)) = 105 US_SEM w r1 \/ US_SEM w r2) 106 /\ 107 (US_SEM w (S_AND(r1,r2)) = 108 US_SEM w r1 /\ US_SEM w r2) 109 /\ 110 (US_SEM w (S_REPEAT r) = 111 ?wlist. (w = CONCAT wlist) /\ EVERY (\w. US_SEM w r) wlist)`; 112 113(****************************************************************************** 114* Original unclocked "SEM 1" semantics of Sugar formulas 115* UF_SEM w f means "w |= f" in the unclocked semantics 116* where w is a finite or infinite word i.e. w : ('prop -> bool)path 117******************************************************************************) 118val OLD_UF_SEM_def = 119 Define 120 `(OLD_UF_SEM w (F_BOOL b) = 121 B_SEM (ELEM w 0) b) 122 /\ 123 (OLD_UF_SEM w (F_NOT f) = 124 ~(OLD_UF_SEM w f)) 125 /\ 126 (OLD_UF_SEM w (F_AND(f1,f2)) = 127 OLD_UF_SEM w f1 /\ OLD_UF_SEM w f2) 128 /\ 129 (OLD_UF_SEM w (F_NEXT f) = 130 LENGTH w > 1 /\ OLD_UF_SEM (RESTN w 1) f) 131 /\ 132 (OLD_UF_SEM w (F_UNTIL(f1,f2)) = 133 ?k :: (0 to LENGTH w). 134 OLD_UF_SEM (RESTN w k) f2 /\ !j :: (0 to k). OLD_UF_SEM (RESTN w j) f1) 135 /\ 136 (OLD_UF_SEM w (F_SUFFIX_IMP(r,f)) = 137 !j :: (0 to LENGTH w). 138 US_SEM (SEL w (0,j)) r ==> OLD_UF_SEM (RESTN w j) f) 139 /\ 140 (OLD_UF_SEM w (F_STRONG_IMP(r1,r2)) = 141 !j :: (0 to LENGTH w). 142 US_SEM (SEL w (0,j)) r1 143 ==> 144 ?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2) 145 /\ 146 (OLD_UF_SEM w (F_WEAK_IMP(r1,r2)) = 147 !j :: (0 to LENGTH w). 148 US_SEM (SEL w (0,j)) r1 149 ==> 150 ((?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2) 151 \/ 152 (!k :: (j to LENGTH w). ?w'. US_SEM (SEL w (j,k) <> w') r2))) 153 /\ 154 (OLD_UF_SEM w (F_ABORT (f,b)) = 155 OLD_UF_SEM w f 156 \/ 157 OLD_UF_SEM w (F_BOOL b) 158 \/ 159 ?j :: (1 to LENGTH w). 160 ?w'. OLD_UF_SEM (RESTN w j) (F_BOOL b) 161 /\ 162 OLD_UF_SEM (CAT(SEL w (0,j-1),w')) f)`; 163 164(****************************************************************************** 165* Unclocked "SEM 1" semantics of Sugar formulas 166* with additional |w|>0 for boolean formulas 167* UF_SEM w f means "w |= f" in the unclocked semantics 168* where w is a finite or infinite word i.e. w : ('prop -> bool)path 169******************************************************************************) 170val UF_SEM_def = 171 Define 172 `(UF_SEM w (F_BOOL b) = 173 LENGTH w > 0 /\ B_SEM (ELEM w 0) b) 174 /\ 175 (UF_SEM w (F_NOT f) = 176 ~(UF_SEM w f)) 177 /\ 178 (UF_SEM w (F_AND(f1,f2)) = 179 UF_SEM w f1 /\ UF_SEM w f2) 180 /\ 181 (UF_SEM w (F_NEXT f) = 182 LENGTH w > 1 /\ UF_SEM (RESTN w 1) f) 183 /\ 184 (UF_SEM w (F_UNTIL(f1,f2)) = 185 ?k :: (0 to LENGTH w). 186 UF_SEM (RESTN w k) f2 /\ !j :: (0 to k). UF_SEM (RESTN w j) f1) 187 /\ 188 (UF_SEM w (F_SUFFIX_IMP(r,f)) = 189 !j :: (0 to LENGTH w). 190 US_SEM (SEL w (0,j)) r ==> UF_SEM (RESTN w j) f) 191 /\ 192 (UF_SEM w (F_STRONG_IMP(r1,r2)) = 193 !j :: (0 to LENGTH w). 194 US_SEM (SEL w (0,j)) r1 195 ==> 196 ?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2) 197 /\ 198 (UF_SEM w (F_WEAK_IMP(r1,r2)) = 199 !j :: (0 to LENGTH w). 200 US_SEM (SEL w (0,j)) r1 201 ==> 202 ((?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2) 203 \/ 204 (!k :: (j to LENGTH w). ?w'. US_SEM (SEL w (j,k) <> w') r2))) 205 /\ 206 (UF_SEM w (F_ABORT (f,b)) = 207 UF_SEM w f 208 \/ 209 UF_SEM w (F_BOOL b) 210 \/ 211 ?j :: (1 to LENGTH w). 212 ?w'. UF_SEM (RESTN w j) (F_BOOL b) 213 /\ 214 UF_SEM (CAT(SEL w (0,j-1),w')) f)`; 215 216(****************************************************************************** 217* PATH M p is true iff p is a path with respect to transition relation M.R 218******************************************************************************) 219val PATH_def = Define `PATH M p s = IS_INFINITE p /\ (ELEM p 0 = s) /\ (!n. M.R(ELEM p n, ELEM p (n+1)))`; 220 221(****************************************************************************** 222* O_SEM M s f means "M, s |= f" 223******************************************************************************) 224val O_SEM_def = 225 Define 226 `(O_SEM M (O_BOOL b) s = B_SEM (M.L s) b) 227 /\ 228 (O_SEM M (O_NOT f) s = ~(O_SEM M f s)) 229 /\ 230 (O_SEM M (O_AND(f1,f2)) s = O_SEM M f1 s /\ O_SEM M f2 s) 231 /\ 232 (O_SEM M (O_EX f) s = 233 ?p. PATH M p s /\ O_SEM M f (ELEM p 1)) 234 /\ 235 (O_SEM M (O_EU(f1,f2)) s = 236 ?p. PATH M p s /\ 237 ?k :: (0 to LENGTH p). O_SEM M f2 (ELEM p k) /\ !j. j < k ==> O_SEM M f1 (ELEM p j)) 238 /\ 239 (O_SEM M (O_EG f) s = 240 ?p. PATH M p s /\ !j :: (0 to LENGTH p). O_SEM M f (ELEM p j))`; 241 242val _ = export_theory(); 243 244