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"; 54val _ = ParseExtras.temp_loose_equality() 55 56(****************************************************************************** 57* pureDefine doesn't export definitions to theCompset (for EVAL). 58******************************************************************************) 59val pureDefine = with_flag (computeLib.auto_import_definitions, false) Define; 60 61(****************************************************************************** 62* B_SEM l b means "l |= b" where l is a letter, i.e. l : 'prop -> bool 63******************************************************************************) 64val B_SEM_def = 65 Define 66 `(B_SEM l (B_PROP(p:'prop)) = p IN l) 67 /\ 68 (B_SEM l (B_NOT b) = ~(B_SEM l b)) 69 /\ 70 (B_SEM l (B_AND(b1,b2)) = B_SEM l b1 /\ B_SEM l b2)`; 71 72val B_SEM = 73 store_thm 74 ("B_SEM", 75 ``(B_SEM l (B_PROP p) = p IN l) 76 /\ 77 (B_SEM l B_TRUE = T) 78 /\ 79 (B_SEM l B_FALSE = F) 80 /\ 81 (B_SEM l (B_NOT b) = ~(B_SEM l b)) 82 /\ 83 (B_SEM l (B_AND(b1,b2)) = B_SEM l b1 /\ B_SEM l b2) 84 /\ 85 (B_SEM l (B_OR(b1,b2)) = B_SEM l b1 \/ B_SEM l b2)``, 86 RW_TAC std_ss [B_SEM_def,B_OR_def,B_TRUE_def,B_FALSE_def] 87 THEN PROVE_TAC[]); 88 89(****************************************************************************** 90* Unclocked "SEM 1" semantics of SEREs. 91* US_SEM w r means "w is in the language of r" in the unclocked semantics 92* where w is a word, i.e. a list of letters: w : ('prop -> bool)list 93******************************************************************************) 94val US_SEM_def = 95 pureDefine 96 `(US_SEM w (S_BOOL b) = (LENGTH w = 1) /\ B_SEM (ELEM w 0) b) 97 /\ 98 (US_SEM w (S_CAT(r1,r2)) = 99 ?w1 w2. (w = w1 <> w2) /\ US_SEM w1 r1 /\ US_SEM w2 r2) 100 /\ 101 (US_SEM w (S_FUSION(r1,r2)) = 102 ?w1 w2 l. (w = w1 <> [l] <> w2) /\ 103 US_SEM (w1<>[l]) r1 /\ US_SEM ([l]<>w2) r2) 104 /\ 105 (US_SEM w (S_OR(r1,r2)) = 106 US_SEM w r1 \/ US_SEM w r2) 107 /\ 108 (US_SEM w (S_AND(r1,r2)) = 109 US_SEM w r1 /\ US_SEM w r2) 110 /\ 111 (US_SEM w (S_REPEAT r) = 112 ?wlist. (w = CONCAT wlist) /\ EVERY (\w. US_SEM w r) wlist)`; 113 114(****************************************************************************** 115* Original unclocked "SEM 1" semantics of Sugar formulas 116* UF_SEM w f means "w |= f" in the unclocked semantics 117* where w is a finite or infinite word i.e. w : ('prop -> bool)path 118******************************************************************************) 119val OLD_UF_SEM_def = 120 Define 121 `(OLD_UF_SEM w (F_BOOL b) = 122 B_SEM (ELEM w 0) b) 123 /\ 124 (OLD_UF_SEM w (F_NOT f) = 125 ~(OLD_UF_SEM w f)) 126 /\ 127 (OLD_UF_SEM w (F_AND(f1,f2)) = 128 OLD_UF_SEM w f1 /\ OLD_UF_SEM w f2) 129 /\ 130 (OLD_UF_SEM w (F_NEXT f) = 131 LENGTH w > 1 /\ OLD_UF_SEM (RESTN w 1) f) 132 /\ 133 (OLD_UF_SEM w (F_UNTIL(f1,f2)) = 134 ?k :: (0 to LENGTH w). 135 OLD_UF_SEM (RESTN w k) f2 /\ !j :: (0 to k). OLD_UF_SEM (RESTN w j) f1) 136 /\ 137 (OLD_UF_SEM w (F_SUFFIX_IMP(r,f)) = 138 !j :: (0 to LENGTH w). 139 US_SEM (SEL w (0,j)) r ==> OLD_UF_SEM (RESTN w j) f) 140 /\ 141 (OLD_UF_SEM w (F_STRONG_IMP(r1,r2)) = 142 !j :: (0 to LENGTH w). 143 US_SEM (SEL w (0,j)) r1 144 ==> 145 ?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2) 146 /\ 147 (OLD_UF_SEM w (F_WEAK_IMP(r1,r2)) = 148 !j :: (0 to LENGTH w). 149 US_SEM (SEL w (0,j)) r1 150 ==> 151 ((?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2) 152 \/ 153 (!k :: (j to LENGTH w). ?w'. US_SEM (SEL w (j,k) <> w') r2))) 154 /\ 155 (OLD_UF_SEM w (F_ABORT (f,b)) = 156 OLD_UF_SEM w f 157 \/ 158 OLD_UF_SEM w (F_BOOL b) 159 \/ 160 ?j :: (1 to LENGTH w). 161 ?w'. OLD_UF_SEM (RESTN w j) (F_BOOL b) 162 /\ 163 OLD_UF_SEM (CAT(SEL w (0,j-1),w')) f)`; 164 165(****************************************************************************** 166* Unclocked "SEM 1" semantics of Sugar formulas 167* with additional |w|>0 for boolean formulas 168* UF_SEM w f means "w |= f" in the unclocked semantics 169* where w is a finite or infinite word i.e. w : ('prop -> bool)path 170******************************************************************************) 171val UF_SEM_def = 172 Define 173 `(UF_SEM w (F_BOOL b) = 174 LENGTH w > 0 /\ B_SEM (ELEM w 0) b) 175 /\ 176 (UF_SEM w (F_NOT f) = 177 ~(UF_SEM w f)) 178 /\ 179 (UF_SEM w (F_AND(f1,f2)) = 180 UF_SEM w f1 /\ UF_SEM w f2) 181 /\ 182 (UF_SEM w (F_NEXT f) = 183 LENGTH w > 1 /\ UF_SEM (RESTN w 1) f) 184 /\ 185 (UF_SEM w (F_UNTIL(f1,f2)) = 186 ?k :: (0 to LENGTH w). 187 UF_SEM (RESTN w k) f2 /\ !j :: (0 to k). UF_SEM (RESTN w j) f1) 188 /\ 189 (UF_SEM w (F_SUFFIX_IMP(r,f)) = 190 !j :: (0 to LENGTH w). 191 US_SEM (SEL w (0,j)) r ==> UF_SEM (RESTN w j) f) 192 /\ 193 (UF_SEM w (F_STRONG_IMP(r1,r2)) = 194 !j :: (0 to LENGTH w). 195 US_SEM (SEL w (0,j)) r1 196 ==> 197 ?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2) 198 /\ 199 (UF_SEM w (F_WEAK_IMP(r1,r2)) = 200 !j :: (0 to LENGTH w). 201 US_SEM (SEL w (0,j)) r1 202 ==> 203 ((?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2) 204 \/ 205 (!k :: (j to LENGTH w). ?w'. US_SEM (SEL w (j,k) <> w') r2))) 206 /\ 207 (UF_SEM w (F_ABORT (f,b)) = 208 UF_SEM w f 209 \/ 210 UF_SEM w (F_BOOL b) 211 \/ 212 ?j :: (1 to LENGTH w). 213 ?w'. UF_SEM (RESTN w j) (F_BOOL b) 214 /\ 215 UF_SEM (CAT(SEL w (0,j-1),w')) f)`; 216 217(****************************************************************************** 218* PATH M p is true iff p is a path with respect to transition relation M.R 219******************************************************************************) 220val PATH_def = Define `PATH M p s = IS_INFINITE p /\ (ELEM p 0 = s) /\ (!n. M.R(ELEM p n, ELEM p (n+1)))`; 221 222(****************************************************************************** 223* O_SEM M s f means "M, s |= f" 224******************************************************************************) 225val O_SEM_def = 226 Define 227 `(O_SEM M (O_BOOL b) s = B_SEM (M.L s) b) 228 /\ 229 (O_SEM M (O_NOT f) s = ~(O_SEM M f s)) 230 /\ 231 (O_SEM M (O_AND(f1,f2)) s = O_SEM M f1 s /\ O_SEM M f2 s) 232 /\ 233 (O_SEM M (O_EX f) s = 234 ?p. PATH M p s /\ O_SEM M f (ELEM p 1)) 235 /\ 236 (O_SEM M (O_EU(f1,f2)) s = 237 ?p. PATH M p s /\ 238 ?k :: (0 to LENGTH p). O_SEM M f2 (ELEM p k) /\ !j. j < k ==> O_SEM M f1 (ELEM p j)) 239 /\ 240 (O_SEM M (O_EG f) s = 241 ?p. PATH M p s /\ !j :: (0 to LENGTH p). O_SEM M f (ELEM p j))`; 242 243val _ = export_theory(); 244