1open HolKernel Parse boolLib bossLib; 2 3open pred_setTheory listTheory pairTheory prop_logicTheory containerTheory 4 tuerk_tacticsLib set_lemmataTheory temporal_deep_mixedTheory; 5 6open Sanity; 7 8val _ = hide "S"; 9val _ = hide "I"; 10 11val _ = new_theory "xprop_logic"; 12val _ = ParseExtras.temp_loose_equality() 13 14Datatype : 15 xprop_logic = XP_PROP 'a (* atomic proposition *) 16 | XP_NEXT_PROP 'a (* X atomic proposition *) 17 | XP_TRUE (* true *) 18 | XP_NOT xprop_logic (* negation *) 19 | XP_AND (xprop_logic # xprop_logic) (* conjunction *) 20End 21 22Theorem xprop_logic_induct = Q.GEN `P` 23 (MATCH_MP 24 (DECIDE ``(A ==> (B1 /\ B2)) ==> (A ==> B1)``) 25 (SIMP_RULE std_ss 26 [pairTheory.FORALL_PROD, 27 PROVE[]``(!x y. P x ==> Q(x,y)) = !x. P x ==> !y. Q(x,y)``, 28 PROVE[]``(!x y. P y ==> Q(x,y)) = !y. P y ==> !x. Q(x,y)``] 29 (Q.SPECL 30 [`P`,`\(f1,f2). P f1 /\ P f2`] 31 (TypeBase.induction_of ``:'a xprop_logic``)))); 32 33val XP_USED_CURRENT_VARS_def = Define 34 `(XP_USED_CURRENT_VARS (XP_TRUE) = EMPTY) /\ 35 (XP_USED_CURRENT_VARS (XP_PROP p) = {p}) /\ 36 (XP_USED_CURRENT_VARS (XP_NEXT_PROP p) = EMPTY) /\ 37 (XP_USED_CURRENT_VARS (XP_NOT b) = XP_USED_CURRENT_VARS b) /\ 38 (XP_USED_CURRENT_VARS (XP_AND(b1,b2)) = 39 (XP_USED_CURRENT_VARS b1) UNION (XP_USED_CURRENT_VARS b2))`; 40 41val XP_USED_X_VARS_def = Define 42 `(XP_USED_X_VARS (XP_TRUE) = EMPTY) /\ 43 (XP_USED_X_VARS (XP_PROP p) = EMPTY) /\ 44 (XP_USED_X_VARS (XP_NEXT_PROP p) = {p}) /\ 45 (XP_USED_X_VARS (XP_NOT b) = XP_USED_X_VARS b) /\ 46 (XP_USED_X_VARS (XP_AND(b1,b2)) = (XP_USED_X_VARS b1) UNION (XP_USED_X_VARS b2))`; 47 48val XP_USED_VARS_def = Define 49 `XP_USED_VARS b = (XP_USED_CURRENT_VARS b) UNION (XP_USED_X_VARS b)`; 50 51val XP_VAR_RENAMING_def = Define 52 `(XP_VAR_RENAMING (f:'a->'b) (XP_TRUE) = XP_TRUE) /\ 53 (XP_VAR_RENAMING f (XP_PROP p) = (XP_PROP (f p))) /\ 54 (XP_VAR_RENAMING f (XP_NEXT_PROP p) = (XP_NEXT_PROP (f p))) /\ 55 (XP_VAR_RENAMING f (XP_NOT b) = XP_NOT (XP_VAR_RENAMING f b)) /\ 56 (XP_VAR_RENAMING f (XP_AND(b1,b2)) = XP_AND(XP_VAR_RENAMING f b1, XP_VAR_RENAMING f b2))`; 57 58(*============================================================================= 59= Semantic 60=============================================================================*) 61 62val XP_SEM_def = 63 Define 64 `(XP_SEM (XP_TRUE) (s1:'a set, s2:'a set) = T) /\ 65 (XP_SEM (XP_PROP p) (s1, s2) = (p IN s1)) /\ 66 (XP_SEM (XP_NEXT_PROP p) (s1, s2) = (p IN s2)) /\ 67 (XP_SEM (XP_NOT b) (s1, s2) = ~(XP_SEM b (s1, s2))) /\ 68 (XP_SEM (XP_AND (b1,b2)) (s1, s2) = ((XP_SEM b1 (s1, s2)) /\ (XP_SEM b2 (s1, s2))))`; 69 70(*============================================================================= 71= Syntactic Sugar and elementary lemmata 72=============================================================================*) 73 74(****************************************************************************** 75* Propositional logic with X 76******************************************************************************) 77val XP_FALSE_def = Define 78 `XP_FALSE = XP_NOT(XP_TRUE)`; 79 80val XP_OR_def = Define 81 `XP_OR(b1, b2) = XP_NOT(XP_AND(XP_NOT b1, XP_NOT b2))`; 82 83val XP_IMPL_def = Define 84 `XP_IMPL(b1, b2) = XP_OR(XP_NOT b1, b2)`; 85 86val XP_COND_def = Define 87 `XP_COND(c, f1, f2) = XP_AND(XP_IMPL(c, f1), XP_IMPL(XP_NOT c, f2))`; 88 89val XP_EQUIV_def = Define 90 `XP_EQUIV(b1, b2) = XP_AND(XP_IMPL(b1, b2),XP_IMPL(b2, b1))`; 91 92val XPROP_LOGIC_EQUIVALENT_def = Define 93 `XPROP_LOGIC_EQUIVALENT b1 b2 = !s1 s2. (XP_SEM b1 (s1, s2)) = (XP_SEM b2 (s1, s2))`; 94 95(* conversion from prop_logic to xprop_logic (next version) *) 96val XP_NEXT_def = Define 97 `(XP_NEXT (P_TRUE) = XP_TRUE) /\ 98 (XP_NEXT (P_PROP p) = XP_NEXT_PROP p) /\ 99 (XP_NEXT (P_NOT b) = XP_NOT (XP_NEXT b)) /\ 100 (XP_NEXT (P_AND(b1,b2)) = (XP_AND((XP_NEXT b1),(XP_NEXT b2))))`; 101 102(* conversion from prop_logic to xprop_logic (current version) *) 103val XP_CURRENT_def = Define 104 `(XP_CURRENT (P_TRUE) = XP_TRUE) /\ 105 (XP_CURRENT (P_PROP p) = XP_PROP p) /\ 106 (XP_CURRENT (P_NOT b) = XP_NOT (XP_CURRENT b)) /\ 107 (XP_CURRENT (P_AND(b1,b2)) = (XP_AND((XP_CURRENT b1),(XP_CURRENT b2))))`; 108 109val XP_BIGOR_def = Define 110 `(XP_BIGOR [] = XP_FALSE) /\ 111 (XP_BIGOR (s::S) = XP_OR (s, XP_BIGOR S))`; 112 113val XP_BIGAND_def = Define 114 `(XP_BIGAND [] = XP_TRUE) /\ 115 (XP_BIGAND (s::l) = XP_AND (s, XP_BIGAND l))`; 116 117val XP_BIGCOND_def = Define 118 `(XP_BIGCOND [] = XP_FALSE) /\ 119 (XP_BIGCOND ((c,b)::l) = XP_COND (c, b, XP_BIGCOND l))`; 120 121val XP_PROP_SET_MODEL_def = Define 122 `XP_PROP_SET_MODEL S1 S2 S' = 123 (XP_AND(XP_CURRENT(P_PROP_SET_MODEL S1 S'), 124 XP_NEXT(P_PROP_SET_MODEL S2 S')))`; 125 126 127val XP_PROP_SET_MODEL_CURRENT_def = Define 128 `XP_PROP_SET_MODEL_CURRENT f S' = 129 XP_BIGOR (SET_TO_LIST (IMAGE (\S. 130 (XP_AND(XP_NEXT(P_PROP_SET_MODEL S S'), 131 XP_CURRENT(P_PROP_SET_MODEL (f (S INTER S')) S')))) 132 (POW S')))`; 133 134val XP_PROP_SET_MODEL_NEXT_def = Define 135 `XP_PROP_SET_MODEL_NEXT f S' = 136 XP_BIGOR (SET_TO_LIST (IMAGE (\S. 137 (XP_AND(XP_CURRENT(P_PROP_SET_MODEL S S'), 138 XP_NEXT(P_PROP_SET_MODEL (f (S INTER S')) S')))) 139 (POW S')))`; 140 141 142val XP_NEXT_THM = 143 store_thm ( 144 "XP_NEXT_THM", 145 146 ``((XP_NEXT P_TRUE) = XP_TRUE) /\ 147 ((XP_NEXT P_FALSE) = XP_FALSE) /\ 148 ((XP_NEXT (P_PROP p)) = XP_NEXT_PROP p) /\ 149 ((XP_NEXT (P_NOT b)) = XP_NOT (XP_NEXT b)) /\ 150 ((XP_NEXT (P_AND(b1, b2))) = XP_AND (XP_NEXT b1, XP_NEXT b2)) /\ 151 ((XP_NEXT (P_OR(b1, b2))) = XP_OR (XP_NEXT b1, XP_NEXT b2)) /\ 152 ((XP_NEXT (P_IMPL(b1, b2))) = XP_IMPL (XP_NEXT b1, XP_NEXT b2)) /\ 153 ((XP_NEXT (P_EQUIV(b1, b2))) = XP_EQUIV (XP_NEXT b1, XP_NEXT b2)) /\ 154 ((XP_NEXT (P_BIGAND l)) = XP_BIGAND (MAP XP_NEXT l)) /\ 155 ((XP_NEXT (P_BIGOR l)) = XP_BIGOR (MAP XP_NEXT l))``, 156 157 SIMP_TAC std_ss [XP_NEXT_def, XP_FALSE_def, P_FALSE_def, P_OR_def, XP_OR_def, 158 P_IMPL_def, XP_IMPL_def, XP_EQUIV_def, P_EQUIV_def] THEN 159 Induct_on `l` THENL [ 160 SIMP_TAC list_ss [P_BIGAND_def, XP_BIGAND_def, XP_NEXT_def, XP_BIGOR_def, P_BIGOR_def, P_FALSE_def, XP_FALSE_def], 161 ASM_SIMP_TAC list_ss [P_BIGAND_def, XP_BIGAND_def, XP_NEXT_def, P_BIGOR_def, XP_BIGOR_def, XP_OR_def, P_OR_def] 162 ]); 163 164 165val XP_CURRENT_THM = 166 store_thm ( 167 "XP_CURRENT_THM", 168 169 ``((XP_CURRENT P_TRUE) = XP_TRUE) /\ 170 ((XP_CURRENT P_FALSE) = XP_FALSE) /\ 171 ((XP_CURRENT (P_PROP p)) = XP_PROP p) /\ 172 ((XP_CURRENT (P_NOT b)) = XP_NOT (XP_CURRENT b)) /\ 173 ((XP_CURRENT (P_AND(b1, b2))) = XP_AND (XP_CURRENT b1, XP_CURRENT b2)) /\ 174 ((XP_CURRENT (P_OR(b1, b2))) = XP_OR (XP_CURRENT b1, XP_CURRENT b2)) /\ 175 ((XP_CURRENT (P_IMPL(b1, b2))) = XP_IMPL (XP_CURRENT b1, XP_CURRENT b2)) /\ 176 ((XP_CURRENT (P_EQUIV(b1, b2))) = XP_EQUIV (XP_CURRENT b1, XP_CURRENT b2)) /\ 177 ((XP_CURRENT (P_BIGAND l)) = XP_BIGAND (MAP XP_CURRENT l)) /\ 178 ((XP_CURRENT (P_BIGOR l)) = XP_BIGOR (MAP XP_CURRENT l))``, 179 180 SIMP_TAC std_ss [XP_CURRENT_def, XP_FALSE_def, P_FALSE_def, P_OR_def, XP_OR_def, 181 P_IMPL_def, XP_IMPL_def, XP_EQUIV_def, P_EQUIV_def] THEN 182 Induct_on `l` THENL [ 183 SIMP_TAC list_ss [P_BIGAND_def, XP_BIGAND_def, XP_CURRENT_def, XP_BIGOR_def, P_BIGOR_def, P_FALSE_def, XP_FALSE_def], 184 ASM_SIMP_TAC list_ss [P_BIGAND_def, XP_BIGAND_def, XP_CURRENT_def, P_BIGOR_def, XP_BIGOR_def, XP_OR_def, P_OR_def] 185 ]); 186 187 188 189val XP_SEM_THM = 190 store_thm 191 ("XP_SEM_THM", 192 ``!s1 s2 b1 b2 b c p. 193 (XP_SEM XP_TRUE (s1,s2)) /\ 194 ~(XP_SEM XP_FALSE (s1,s2)) /\ 195 (XP_SEM (XP_PROP p) (s1,s2) = p IN s1) /\ 196 (XP_SEM (XP_NEXT_PROP p) (s1,s2) = p IN s2) /\ 197 (XP_SEM (XP_NOT b) (s1,s2) = ~XP_SEM b (s1,s2)) /\ 198 (XP_SEM (XP_AND (b1,b2)) (s1,s2) = 199 (XP_SEM b1 (s1,s2) /\ XP_SEM b2 (s1,s2))) /\ 200 (XP_SEM (XP_OR (b1,b2)) (s1,s2) = XP_SEM b1 (s1,s2) \/ XP_SEM b2 (s1,s2)) /\ 201 (XP_SEM (XP_IMPL (b1,b2)) (s1,s2) = (~XP_SEM b1 (s1,s2) \/ XP_SEM b2 (s1,s2))) /\ 202 (XP_SEM (XP_EQUIV (b1,b2)) (s1,s2) = (XP_SEM b1 (s1,s2) = XP_SEM b2 (s1,s2))) /\ 203 (XP_SEM (XP_COND (c, b1, b2)) (s1,s2) = (XP_SEM (XP_AND(c, b1)) (s1,s2) \/ XP_SEM (XP_AND(XP_NOT c, b2)) (s1,s2)))``, 204 205 SIMP_TAC std_ss [XP_FALSE_def, XP_OR_def, XP_IMPL_def, XP_EQUIV_def, XP_SEM_def, XP_COND_def] THEN 206 REPEAT STRIP_TAC THEN PROVE_TAC[] 207); 208 209 210 211val XP_USED_VARS___DIRECT_DEF = 212 store_thm 213 ("XP_USED_VARS___DIRECT_DEF", 214 ``!p b b1 b2. 215 (XP_USED_VARS (XP_TRUE) = EMPTY) /\ 216 (XP_USED_VARS (XP_PROP p) = {p}) /\ 217 (XP_USED_VARS (XP_NEXT_PROP p) = {p}) /\ 218 (XP_USED_VARS (XP_NOT b) = XP_USED_VARS b) /\ 219 (XP_USED_VARS (XP_AND(b1,b2)) = ((XP_USED_VARS b1) UNION (XP_USED_VARS b2)))``, 220 221 SIMP_TAC std_ss [XP_USED_VARS_def, XP_USED_CURRENT_VARS_def, XP_USED_X_VARS_def, 222 UNION_EMPTY, EXTENSION, IN_UNION] THEN 223 PROVE_TAC[]); 224 225 226val XP_BIGAND___XP_USED_VARS = 227 store_thm 228 ("XP_BIGAND___XP_USED_VARS", 229 230 ``(!l:'a xprop_logic list. (XP_USED_X_VARS (XP_BIGAND l) = 231 LIST_BIGUNION (MAP (\xp. XP_USED_X_VARS xp) l))) /\ 232 (!l:'a xprop_logic list. (XP_USED_CURRENT_VARS (XP_BIGAND l) = 233 LIST_BIGUNION (MAP (\xp. XP_USED_CURRENT_VARS xp) l))) /\ 234 (!l:'a xprop_logic list. (XP_USED_VARS (XP_BIGAND l) = 235 LIST_BIGUNION (MAP (\xp. XP_USED_VARS xp) l)))``, 236 237 SIMP_TAC std_ss [GSYM FORALL_AND_THM] THEN 238 Induct_on `l` THENL [ 239 SIMP_TAC list_ss [XP_BIGAND_def, XP_USED_X_VARS_def, 240 XP_USED_CURRENT_VARS_def, 241 XP_USED_VARS_def, 242 LIST_BIGUNION_def, 243 UNION_EMPTY], 244 245 SIMP_ALL_TAC list_ss [XP_BIGAND_def, XP_USED_X_VARS_def, 246 XP_USED_CURRENT_VARS_def, 247 XP_USED_VARS_def, 248 LIST_BIGUNION_def, 249 UNION_EMPTY, EXTENSION, IN_UNION] THEN 250 ASM_SIMP_TAC std_ss [] THEN 251 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN 252 PROVE_TAC[] 253 ]); 254 255 256val XP_NEXT___XP_USED_VARS= 257 store_thm 258 ("XP_NEXT___XP_USED_VARS", 259 ``!p. (XP_USED_VARS (XP_NEXT p) = (P_USED_VARS p)) /\ 260 (XP_USED_X_VARS (XP_NEXT p) = (P_USED_VARS p)) /\ 261 (XP_USED_CURRENT_VARS (XP_NEXT p) = EMPTY)``, 262 263 INDUCT_THEN prop_logic_induct STRIP_ASSUME_TAC THEN 264 ASM_REWRITE_TAC[XP_NEXT_def, 265 XP_USED_CURRENT_VARS_def, 266 XP_USED_VARS_def, 267 XP_USED_X_VARS_def, 268 UNION_EMPTY, 269 P_USED_VARS_def] THEN 270 METIS_TAC[]); 271 272 273val XP_CURRENT___XP_USED_VARS= 274 store_thm 275 ("XP_CURRENT___XP_USED_VARS", 276 ``!p. (XP_USED_VARS (XP_CURRENT p) = (P_USED_VARS p)) /\ 277 (XP_USED_X_VARS (XP_CURRENT p) = EMPTY) /\ 278 (XP_USED_CURRENT_VARS (XP_CURRENT p) = (P_USED_VARS p))``, 279 280 INDUCT_THEN prop_logic_induct STRIP_ASSUME_TAC THEN 281 ASM_REWRITE_TAC[XP_CURRENT_def, 282 XP_USED_CURRENT_VARS_def, 283 XP_USED_VARS_def, 284 XP_USED_X_VARS_def, 285 UNION_EMPTY, 286 P_USED_VARS_def] THEN 287 METIS_TAC[]); 288 289 290 291val XP_USED_VARS_EVAL = 292 store_thm 293 ("XP_USED_VARS_EVAL", 294 ``!p c b b1 b2 P. ( 295 (XP_USED_VARS (XP_TRUE) = {}) /\ 296 (XP_USED_VARS (XP_FALSE) = {}) /\ 297 (XP_USED_VARS (XP_PROP p) = {p}) /\ 298 (XP_USED_VARS (XP_NEXT_PROP p) = {p}) /\ 299 (XP_USED_VARS (XP_CURRENT P) = P_USED_VARS P) /\ 300 (XP_USED_VARS (XP_NEXT P) = P_USED_VARS P) /\ 301 (XP_USED_VARS (XP_NOT b) = XP_USED_VARS b) /\ 302 (XP_USED_VARS (XP_AND(b1, b2)) = XP_USED_VARS b1 UNION XP_USED_VARS b2) /\ 303 (XP_USED_VARS (XP_OR(b1, b2)) = XP_USED_VARS b1 UNION XP_USED_VARS b2) /\ 304 (XP_USED_VARS (XP_COND(c, b1, b2)) = XP_USED_VARS c UNION XP_USED_VARS b1 UNION XP_USED_VARS b2) /\ 305 (XP_USED_VARS (XP_IMPL(b1, b2)) = XP_USED_VARS b1 UNION XP_USED_VARS b2) /\ 306 (XP_USED_VARS (XP_EQUIV(b1, b2)) = XP_USED_VARS b1 UNION XP_USED_VARS b2) /\ 307 (XP_USED_CURRENT_VARS (XP_TRUE) = {}) /\ 308 (XP_USED_CURRENT_VARS (XP_FALSE) = {}) /\ 309 (XP_USED_CURRENT_VARS (XP_PROP p) = {p}) /\ 310 (XP_USED_CURRENT_VARS (XP_NEXT_PROP p) = {}) /\ 311 (XP_USED_CURRENT_VARS (XP_CURRENT P) = P_USED_VARS P) /\ 312 (XP_USED_CURRENT_VARS (XP_NEXT P) = {}) /\ 313 (XP_USED_CURRENT_VARS (XP_NOT b) = XP_USED_CURRENT_VARS b) /\ 314 (XP_USED_CURRENT_VARS (XP_AND(b1, b2)) = XP_USED_CURRENT_VARS b1 UNION XP_USED_CURRENT_VARS b2) /\ 315 (XP_USED_CURRENT_VARS (XP_OR(b1, b2)) = XP_USED_CURRENT_VARS b1 UNION XP_USED_CURRENT_VARS b2) /\ 316 (XP_USED_CURRENT_VARS (XP_COND(c, b1, b2)) = XP_USED_CURRENT_VARS c UNION XP_USED_CURRENT_VARS b1 UNION XP_USED_CURRENT_VARS b2) /\ 317 (XP_USED_CURRENT_VARS (XP_IMPL(b1, b2)) = XP_USED_CURRENT_VARS b1 UNION XP_USED_CURRENT_VARS b2) /\ 318 (XP_USED_CURRENT_VARS (XP_EQUIV(b1, b2)) = XP_USED_CURRENT_VARS b1 UNION XP_USED_CURRENT_VARS b2) /\ 319 (XP_USED_X_VARS (XP_TRUE) = {}) /\ 320 (XP_USED_X_VARS (XP_FALSE) = {}) /\ 321 (XP_USED_X_VARS (XP_PROP p) = {}) /\ 322 (XP_USED_X_VARS (XP_NEXT_PROP p) = {p}) /\ 323 (XP_USED_X_VARS (XP_CURRENT P) = {}) /\ 324 (XP_USED_X_VARS (XP_NEXT P) = P_USED_VARS P) /\ 325 (XP_USED_X_VARS (XP_NOT b) = XP_USED_X_VARS b) /\ 326 (XP_USED_X_VARS (XP_AND(b1, b2)) = XP_USED_X_VARS b1 UNION XP_USED_X_VARS b2) /\ 327 (XP_USED_X_VARS (XP_OR(b1, b2)) = XP_USED_X_VARS b1 UNION XP_USED_X_VARS b2) /\ 328 (XP_USED_X_VARS (XP_COND(c, b1, b2)) = XP_USED_X_VARS c UNION XP_USED_X_VARS b1 UNION XP_USED_X_VARS b2) /\ 329 (XP_USED_X_VARS (XP_IMPL(b1, b2)) = XP_USED_X_VARS b1 UNION XP_USED_X_VARS b2) /\ 330 (XP_USED_X_VARS (XP_EQUIV(b1, b2)) = XP_USED_X_VARS b1 UNION XP_USED_X_VARS b2) 331 )``, 332 333 REWRITE_TAC[XP_USED_VARS_def, 334 XP_USED_X_VARS_def, XP_USED_CURRENT_VARS_def, UNION_EMPTY, 335 XP_FALSE_def, XP_OR_def, XP_IMPL_def, XP_EQUIV_def, 336 XP_NEXT___XP_USED_VARS, XP_CURRENT___XP_USED_VARS, 337 XP_COND_def] THEN 338 SIMP_TAC std_ss [EXTENSION, IN_UNION] THEN PROVE_TAC[]); 339 340 341 342val XP_SEM___XP_NEXT = 343 store_thm 344 ("XP_SEM___XP_NEXT", 345 346 ``!p s1 s2. (XP_SEM (XP_NEXT p) (s1, s2)) = (P_SEM s2 p)``, 347 348 INDUCT_THEN prop_logic_induct ASSUME_TAC THENL [ 349 REWRITE_TAC[XP_NEXT_def, XP_SEM_THM, P_SEM_THM], 350 351 REWRITE_TAC[XP_NEXT_def, XP_SEM_THM, P_SEM_THM], 352 353 REWRITE_TAC[XP_NEXT_def, XP_SEM_THM, P_SEM_THM] THEN 354 METIS_TAC[], 355 356 REWRITE_TAC[XP_NEXT_def, XP_SEM_THM, P_SEM_THM] THEN 357 METIS_TAC[] 358 ]); 359 360 361val XP_SEM___XP_CURRENT = 362 store_thm 363 ("XP_SEM___XP_CURRENT", 364 365 ``!p s1 s2. (XP_SEM (XP_CURRENT p) (s1, s2)) = (P_SEM s1 p)``, 366 367 INDUCT_THEN prop_logic_induct ASSUME_TAC THENL [ 368 REWRITE_TAC[XP_CURRENT_def, XP_SEM_THM, P_SEM_THM], 369 370 REWRITE_TAC[XP_CURRENT_def, XP_SEM_THM, P_SEM_THM], 371 372 REWRITE_TAC[XP_CURRENT_def, XP_SEM_THM, P_SEM_THM] THEN 373 METIS_TAC[], 374 375 REWRITE_TAC[XP_CURRENT_def, XP_SEM_THM, P_SEM_THM] THEN 376 METIS_TAC[] 377 ]); 378 379 380val XP_BIGAND_SEM = 381 store_thm 382 ("XP_BIGAND_SEM", 383 384 ``!l S1 S2. (XP_SEM (XP_BIGAND l) (S1,S2)) = (!e. (IS_EL e l) ==> XP_SEM e (S1,S2))``, 385 386 Induct_on `l` THEN 387 SIMP_TAC list_ss [XP_SEM_THM, XP_BIGAND_def] THEN 388 PROVE_TAC[]); 389 390 391val XP_BIGOR_SEM = 392 store_thm 393 ("XP_BIGOR_SEM", 394 395 ``!l S1 S2. (XP_SEM (XP_BIGOR l) (S1,S2)) = (?e. (IS_EL e l) /\ XP_SEM e (S1,S2))``, 396 397 Induct_on `l` THEN 398 SIMP_TAC list_ss [XP_SEM_THM, XP_BIGOR_def] THEN 399 PROVE_TAC[]); 400 401 402 403val IS_CURRENT_POSITIVE_NEGATIVE_PROP_FORMULA_SUBSET_def = 404Define 405`(IS_CURRENT_POSITIVE_PROP_FORMULA_SUBSET S XP_TRUE = T) /\ 406 (IS_CURRENT_POSITIVE_PROP_FORMULA_SUBSET S (XP_PROP a) = T) /\ 407 (IS_CURRENT_POSITIVE_PROP_FORMULA_SUBSET S (XP_NEXT_PROP a) = T) /\ 408 (IS_CURRENT_POSITIVE_PROP_FORMULA_SUBSET S (XP_NOT p') = IS_CURRENT_NEGATIVE_PROP_FORMULA_SUBSET S p') /\ 409 (IS_CURRENT_POSITIVE_PROP_FORMULA_SUBSET S (XP_AND(p', p'')) = ( 410 IS_CURRENT_POSITIVE_PROP_FORMULA_SUBSET S p' /\ 411 IS_CURRENT_POSITIVE_PROP_FORMULA_SUBSET S p'')) /\ 412 (IS_CURRENT_NEGATIVE_PROP_FORMULA_SUBSET S XP_TRUE = T) /\ 413 (IS_CURRENT_NEGATIVE_PROP_FORMULA_SUBSET S (XP_PROP a) = (~(a IN S))) /\ 414 (IS_CURRENT_NEGATIVE_PROP_FORMULA_SUBSET S (XP_NEXT_PROP a) = T) /\ 415 (IS_CURRENT_NEGATIVE_PROP_FORMULA_SUBSET S (XP_NOT p') = IS_CURRENT_POSITIVE_PROP_FORMULA_SUBSET S p') /\ 416 (IS_CURRENT_NEGATIVE_PROP_FORMULA_SUBSET S (XP_AND(p', p'')) = ( 417 IS_CURRENT_NEGATIVE_PROP_FORMULA_SUBSET S p' /\ 418 IS_CURRENT_NEGATIVE_PROP_FORMULA_SUBSET S p''))`; 419 420 421val IS_CURRENT_POSITIVE_PROP_FORMULA_def = 422Define 423`IS_CURRENT_POSITIVE_PROP_FORMULA p = 424 IS_CURRENT_POSITIVE_PROP_FORMULA_SUBSET UNIV p`; 425 426val IS_CURRENT_NEGATIVE_PROP_FORMULA_def = 427Define 428`IS_CURRENT_NEGATIVE_PROP_FORMULA p = 429 IS_CURRENT_NEGATIVE_PROP_FORMULA_SUBSET UNIV p`; 430 431 432 433val IS_NEXT_POSITIVE_NEGATIVE_PROP_FORMULA_SUBSET_def = 434Define 435`(IS_NEXT_POSITIVE_PROP_FORMULA_SUBSET S XP_TRUE = T) /\ 436 (IS_NEXT_POSITIVE_PROP_FORMULA_SUBSET S (XP_PROP a) = T) /\ 437 (IS_NEXT_POSITIVE_PROP_FORMULA_SUBSET S (XP_NEXT_PROP a) = T) /\ 438 (IS_NEXT_POSITIVE_PROP_FORMULA_SUBSET S (XP_NOT p') = IS_NEXT_NEGATIVE_PROP_FORMULA_SUBSET S p') /\ 439 (IS_NEXT_POSITIVE_PROP_FORMULA_SUBSET S (XP_AND(p', p'')) = ( 440 IS_NEXT_POSITIVE_PROP_FORMULA_SUBSET S p' /\ 441 IS_NEXT_POSITIVE_PROP_FORMULA_SUBSET S p'')) /\ 442 (IS_NEXT_NEGATIVE_PROP_FORMULA_SUBSET S XP_TRUE = T) /\ 443 (IS_NEXT_NEGATIVE_PROP_FORMULA_SUBSET S (XP_PROP a) = T) /\ 444 (IS_NEXT_NEGATIVE_PROP_FORMULA_SUBSET S (XP_NEXT_PROP a) = (~(a IN S))) /\ 445 (IS_NEXT_NEGATIVE_PROP_FORMULA_SUBSET S (XP_NOT p') = IS_NEXT_POSITIVE_PROP_FORMULA_SUBSET S p') /\ 446 (IS_NEXT_NEGATIVE_PROP_FORMULA_SUBSET S (XP_AND(p', p'')) = ( 447 IS_NEXT_NEGATIVE_PROP_FORMULA_SUBSET S p' /\ 448 IS_NEXT_NEGATIVE_PROP_FORMULA_SUBSET S p''))`; 449 450 451val IS_NEXT_POSITIVE_PROP_FORMULA_def = 452Define 453`IS_NEXT_POSITIVE_PROP_FORMULA p = 454 IS_NEXT_POSITIVE_PROP_FORMULA_SUBSET UNIV p`; 455 456val IS_NEXT_NEGATIVE_PROP_FORMULA_def = 457Define 458`IS_NEXT_NEGATIVE_PROP_FORMULA p = 459 IS_NEXT_NEGATIVE_PROP_FORMULA_SUBSET UNIV p`; 460 461 462 463val IS_CURRENT_POSITIVE_NEGATIVE_PROP_FORMULA_SUBSET_SEM = 464 store_thm 465 ("IS_CURRENT_POSITIVE_NEGATIVE_PROP_FORMULA_SUBSET_SEM", 466 ``!p V V' S S'. ((IS_CURRENT_POSITIVE_PROP_FORMULA_SUBSET V p /\ XP_SEM p (S, S') /\ V' SUBSET V) ==> 467 (XP_SEM p ((S UNION V'), S'))) /\ 468 ((IS_CURRENT_NEGATIVE_PROP_FORMULA_SUBSET V p /\ XP_SEM p ((S UNION V'), S') /\ V' SUBSET V) ==> 469 (XP_SEM p (S, S')))``, 470 471 INDUCT_THEN xprop_logic_induct ASSUME_TAC THEN 472 REWRITE_TAC[IS_CURRENT_POSITIVE_NEGATIVE_PROP_FORMULA_SUBSET_def, XP_SEM_def, IN_UNION] THENL [ 473 PROVE_TAC[SUBSET_DEF], 474 PROVE_TAC[], 475 PROVE_TAC[], 476 PROVE_TAC[] 477 ]); 478 479 480val IS_CURRENT_POSITIVE_NEGATIVE_PROP_FORMULA_SEM = 481 store_thm 482 ("IS_CURRENT_POSITIVE_NEGATIVE_PROP_FORMULA_SEM", 483 ``!p S S' S''. ((IS_CURRENT_POSITIVE_PROP_FORMULA p /\ XP_SEM p (S, S'') /\ S SUBSET S') ==> 484 (XP_SEM p (S', S''))) /\ 485 ((IS_CURRENT_NEGATIVE_PROP_FORMULA p /\ XP_SEM p (S', S'') /\ S SUBSET S') ==> 486 (XP_SEM p (S, S'')))``, 487 488 REWRITE_TAC[IS_CURRENT_POSITIVE_NEGATIVE_PROP_FORMULA_SUBSET_def, 489 IS_CURRENT_POSITIVE_PROP_FORMULA_def, 490 IS_CURRENT_NEGATIVE_PROP_FORMULA_def] THEN 491 REPEAT GEN_TAC THEN 492 Cases_on `S SUBSET S'` THEN ASM_REWRITE_TAC[] THEN 493 `?V'. V' = S' DIFF S` by PROVE_TAC[] THEN 494 `S' = S UNION V'` by (ASM_SIMP_TAC std_ss [UNION_DEF, DIFF_DEF, 495 GSPECIFICATION, EXTENSION] THEN PROVE_TAC[SUBSET_DEF]) THEN 496 PROVE_TAC[IS_CURRENT_POSITIVE_NEGATIVE_PROP_FORMULA_SUBSET_SEM, 497 SUBSET_UNIV]); 498 499 500 501 502val IS_NEXT_POSITIVE_NEGATIVE_PROP_FORMULA_SUBSET_SEM = 503 store_thm 504 ("IS_NEXT_POSITIVE_NEGATIVE_PROP_FORMULA_SUBSET_SEM", 505 ``!p V V' S S'. ((IS_NEXT_POSITIVE_PROP_FORMULA_SUBSET V p /\ XP_SEM p (S', S) /\ V' SUBSET V) ==> 506 (XP_SEM p (S', (S UNION V')))) /\ 507 ((IS_NEXT_NEGATIVE_PROP_FORMULA_SUBSET V p /\ XP_SEM p (S', (S UNION V')) /\ V' SUBSET V) ==> 508 (XP_SEM p (S', S)))``, 509 510 INDUCT_THEN xprop_logic_induct ASSUME_TAC THEN 511 REWRITE_TAC[IS_NEXT_POSITIVE_NEGATIVE_PROP_FORMULA_SUBSET_def, XP_SEM_def, IN_UNION] THENL [ 512 PROVE_TAC[], 513 PROVE_TAC[SUBSET_DEF], 514 PROVE_TAC[], 515 PROVE_TAC[] 516 ]); 517 518 519 520 521val IS_NEXT_POSITIVE_NEGATIVE_PROP_FORMULA_SEM = 522 store_thm 523 ("IS_NEXT_POSITIVE_NEGATIVE_PROP_FORMULA_SEM", 524 ``!p S S' S''. ((IS_NEXT_POSITIVE_PROP_FORMULA p /\ XP_SEM p (S'', S) /\ S SUBSET S') ==> 525 (XP_SEM p (S'', S'))) /\ 526 ((IS_NEXT_NEGATIVE_PROP_FORMULA p /\ XP_SEM p (S'', S') /\ S SUBSET S') ==> 527 (XP_SEM p (S'', S)))``, 528 529 REWRITE_TAC[IS_NEXT_POSITIVE_NEGATIVE_PROP_FORMULA_SUBSET_def, 530 IS_NEXT_POSITIVE_PROP_FORMULA_def, 531 IS_NEXT_NEGATIVE_PROP_FORMULA_def] THEN 532 REPEAT GEN_TAC THEN 533 Cases_on `S SUBSET S'` THEN ASM_REWRITE_TAC[] THEN 534 `?V'. V' = S' DIFF S` by PROVE_TAC[] THEN 535 `S' = S UNION V'` by (ASM_SIMP_TAC std_ss [UNION_DEF, DIFF_DEF, 536 GSPECIFICATION, EXTENSION] THEN PROVE_TAC[SUBSET_DEF]) THEN 537 PROVE_TAC[IS_NEXT_POSITIVE_NEGATIVE_PROP_FORMULA_SUBSET_SEM, 538 SUBSET_UNIV]); 539 540 541val XP_ASSIGN_TRUE_def = 542Define 543`(XP_ASSIGN_TRUE V V' (XP_PROP p) = (if p IN V then XP_TRUE else XP_PROP p)) /\ 544 (XP_ASSIGN_TRUE V V' (XP_NEXT_PROP p) = (if p IN V' then XP_TRUE else XP_NEXT_PROP p)) /\ 545 (XP_ASSIGN_TRUE V V' XP_TRUE = XP_TRUE) /\ 546 (XP_ASSIGN_TRUE V V' (XP_NOT b) = XP_NOT(XP_ASSIGN_TRUE V V' b)) /\ 547 (XP_ASSIGN_TRUE V V' (XP_AND(b1,b2)) = XP_AND ( 548 XP_ASSIGN_TRUE V V' b1, 549 XP_ASSIGN_TRUE V V' b2))`; 550 551val XP_ASSIGN_FALSE_def = 552Define 553`(XP_ASSIGN_FALSE V V' (XP_PROP p) = (if p IN V then XP_FALSE else XP_PROP p)) /\ 554 (XP_ASSIGN_FALSE V V' (XP_NEXT_PROP p) = (if p IN V' then XP_FALSE else XP_NEXT_PROP p)) /\ 555 (XP_ASSIGN_FALSE V V' XP_TRUE = XP_TRUE) /\ 556 (XP_ASSIGN_FALSE V V' (XP_NOT b) = XP_NOT(XP_ASSIGN_FALSE V V' b)) /\ 557 (XP_ASSIGN_FALSE V V' (XP_AND(b1,b2)) = XP_AND ( 558 XP_ASSIGN_FALSE V V' b1, 559 XP_ASSIGN_FALSE V V' b2))`; 560 561val XP_ASSIGN_TRUE_SEM = 562 store_thm 563 ("XP_ASSIGN_TRUE_SEM", 564 565 ``!p s s' V V'. XP_SEM (XP_ASSIGN_TRUE V V' p) (s, s') = 566 XP_SEM p ((s UNION V), (s' UNION V'))``, 567 568 INDUCT_THEN xprop_logic_induct ASSUME_TAC THEN 569 ASM_REWRITE_TAC[XP_ASSIGN_TRUE_def, XP_SEM_def] THEN 570 REWRITE_TAC[IN_UNION] THENL [ 571 Cases_on `a IN V`, 572 Cases_on `a IN V'` 573 ] THEN 574 REWRITE_TAC[XP_SEM_def] 575); 576 577 578val XP_ASSIGN_FALSE_SEM = 579 store_thm 580 ("XP_ASSIGN_FALSE_SEM", 581 582 ``!p s s' V V'. XP_SEM (XP_ASSIGN_FALSE V V' p) (s, s') = 583 XP_SEM p ((s DIFF V), (s' DIFF V'))``, 584 585 INDUCT_THEN xprop_logic_induct ASSUME_TAC THEN 586 ASM_REWRITE_TAC[XP_ASSIGN_FALSE_def, XP_SEM_def] THEN 587 REWRITE_TAC[IN_DIFF] THENL [ 588 Cases_on `a IN V`, 589 Cases_on `a IN V'` 590 ] THEN 591 REWRITE_TAC[XP_SEM_THM]); 592 593 594val XP_CURRENT_EXISTS_def = 595Define 596`(XP_CURRENT_EXISTS [] p = p) /\ 597 (XP_CURRENT_EXISTS (v::l) p = XP_CURRENT_EXISTS l (XP_OR(XP_ASSIGN_TRUE {v} {} p, XP_ASSIGN_FALSE {v} {} p)))`; 598 599val XP_NEXT_EXISTS_def = 600Define 601`(XP_NEXT_EXISTS [] p = p) /\ 602 (XP_NEXT_EXISTS (v::l) p = XP_NEXT_EXISTS l (XP_OR(XP_ASSIGN_TRUE {} {v} p, XP_ASSIGN_FALSE {} {v} p)))`; 603 604 605val XP_CURRENT_FORALL_def = 606Define 607`(XP_CURRENT_FORALL l p = XP_NOT (XP_CURRENT_EXISTS l (XP_NOT p)))`; 608 609 610val XP_NEXT_FORALL_def = 611Define 612`(XP_NEXT_FORALL l p = XP_NOT (XP_NEXT_EXISTS l (XP_NOT p)))`; 613 614 615val XP_CURRENT_EXISTS_SEM = 616 store_thm 617 ("XP_CURRENT_EXISTS_SEM", 618 619 ``!s s' l p. (XP_SEM (XP_CURRENT_EXISTS l p) (s, s') = 620 (?l'. (l' SUBSET (LIST_TO_SET l)) /\ (XP_SEM p (((s DIFF (LIST_TO_SET l)) UNION l'), s'))))``, 621 622 Induct_on `l` THENL [ 623 SIMP_TAC list_ss [LIST_TO_SET_THM, SUBSET_EMPTY, XP_CURRENT_EXISTS_def, UNION_EMPTY, 624 DIFF_EMPTY], 625 626 ASM_SIMP_TAC list_ss [XP_CURRENT_EXISTS_def, LIST_TO_SET_THM, XP_SEM_THM, XP_ASSIGN_TRUE_SEM, 627 XP_ASSIGN_FALSE_SEM] THEN 628 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 629 EXISTS_TAC ``h INSERT l'`` THEN 630 REPEAT STRIP_TAC THENL [ 631 FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_INSERT] THEN PROVE_TAC[], 632 633 `s DIFF (h INSERT LIST_TO_SET l) UNION (h INSERT l') = 634 s DIFF LIST_TO_SET l UNION l' UNION {h}` by 635 (SIMP_TAC std_ss [INSERT_DEF, UNION_DEF, DIFF_DEF, GSPECIFICATION, EXTENSION, 636 NOT_IN_EMPTY] THEN 637 PROVE_TAC[]) THEN 638 FULL_SIMP_TAC std_ss [UNION_EMPTY] 639 ], 640 641 EXISTS_TAC ``l' DELETE h`` THEN 642 REPEAT STRIP_TAC THENL [ 643 FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_DELETE, IN_INSERT], 644 645 `s DIFF (h INSERT LIST_TO_SET l) UNION (l' DELETE h) = 646 s DIFF LIST_TO_SET l UNION l' DIFF {h}` by 647 (SIMP_TAC std_ss [INSERT_DEF, UNION_DEF, DIFF_DEF, GSPECIFICATION, EXTENSION, 648 NOT_IN_EMPTY, DELETE_DEF] THEN 649 PROVE_TAC[]) THEN 650 FULL_SIMP_TAC std_ss [DIFF_EMPTY] 651 ], 652 653 EXISTS_TAC ``l' DELETE h`` THEN 654 REPEAT STRIP_TAC THENL [ 655 FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_INSERT, IN_DELETE] THEN PROVE_TAC[], 656 657 `(s DIFF LIST_TO_SET l UNION (l' DELETE h) UNION {h} = 658 s DIFF (h INSERT LIST_TO_SET l) UNION l') \/ 659 (s DIFF LIST_TO_SET l UNION (l' DELETE h) DIFF {h} = 660 s DIFF (h INSERT LIST_TO_SET l) UNION l')` by 661 (SIMP_TAC std_ss [INSERT_DEF, UNION_DEF, DIFF_DEF, GSPECIFICATION, EXTENSION, 662 NOT_IN_EMPTY, DELETE_DEF] THEN 663 METIS_TAC[]) THEN 664 FULL_SIMP_TAC std_ss [UNION_EMPTY, DIFF_EMPTY] 665 ] 666 ] 667 ]); 668 669 670val XP_NEXT_EXISTS_SEM = 671 store_thm 672 ("XP_NEXT_EXISTS_SEM", 673 674 ``!s s' l p. (XP_SEM (XP_NEXT_EXISTS l p) (s', s) = 675 (?l'. (l' SUBSET (LIST_TO_SET l)) /\ (XP_SEM p (s', ((s DIFF (LIST_TO_SET l)) UNION l')))))``, 676 677 Induct_on `l` THENL [ 678 SIMP_TAC list_ss [LIST_TO_SET_THM, SUBSET_EMPTY, XP_NEXT_EXISTS_def, UNION_EMPTY, 679 DIFF_EMPTY], 680 681 ASM_SIMP_TAC list_ss [XP_NEXT_EXISTS_def, LIST_TO_SET_THM, XP_SEM_THM, XP_ASSIGN_TRUE_SEM, 682 XP_ASSIGN_FALSE_SEM] THEN 683 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 684 EXISTS_TAC ``h INSERT l'`` THEN 685 REPEAT STRIP_TAC THENL [ 686 FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_INSERT] THEN PROVE_TAC[], 687 688 `s DIFF (h INSERT LIST_TO_SET l) UNION (h INSERT l') = 689 s DIFF LIST_TO_SET l UNION l' UNION {h}` by 690 (SIMP_TAC std_ss [INSERT_DEF, UNION_DEF, DIFF_DEF, GSPECIFICATION, EXTENSION, 691 NOT_IN_EMPTY] THEN 692 PROVE_TAC[]) THEN 693 FULL_SIMP_TAC std_ss [UNION_EMPTY] 694 ], 695 696 EXISTS_TAC ``l' DELETE h`` THEN 697 REPEAT STRIP_TAC THENL [ 698 FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_DELETE, IN_INSERT], 699 700 `s DIFF (h INSERT LIST_TO_SET l) UNION (l' DELETE h) = 701 s DIFF LIST_TO_SET l UNION l' DIFF {h}` by 702 (SIMP_TAC std_ss [INSERT_DEF, UNION_DEF, DIFF_DEF, GSPECIFICATION, EXTENSION, 703 NOT_IN_EMPTY, DELETE_DEF] THEN 704 PROVE_TAC[]) THEN 705 FULL_SIMP_TAC std_ss [DIFF_EMPTY] 706 ], 707 708 EXISTS_TAC ``l' DELETE h`` THEN 709 REPEAT STRIP_TAC THENL [ 710 FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_INSERT, IN_DELETE] THEN PROVE_TAC[], 711 712 `(s DIFF LIST_TO_SET l UNION (l' DELETE h) UNION {h} = 713 s DIFF (h INSERT LIST_TO_SET l) UNION l') \/ 714 (s DIFF LIST_TO_SET l UNION (l' DELETE h) DIFF {h} = 715 s DIFF (h INSERT LIST_TO_SET l) UNION l')` by 716 (SIMP_TAC std_ss [INSERT_DEF, UNION_DEF, DIFF_DEF, GSPECIFICATION, EXTENSION, 717 NOT_IN_EMPTY, DELETE_DEF] THEN 718 METIS_TAC[]) THEN 719 FULL_SIMP_TAC std_ss [UNION_EMPTY, DIFF_EMPTY] 720 ] 721 ] 722 ]); 723 724 725val XP_CURRENT_FORALL_SEM = 726 store_thm 727 ("XP_CURRENT_FORALL_SEM", 728 729 ``!s s' l p. (XP_SEM (XP_CURRENT_FORALL l p) (s, s')) = 730 (!l'. (l' SUBSET (LIST_TO_SET l)) ==> (XP_SEM p (((s DIFF (LIST_TO_SET l)) UNION l'), s')))``, 731 732 REWRITE_TAC[XP_CURRENT_FORALL_def, XP_SEM_THM, XP_CURRENT_EXISTS_SEM] THEN 733 PROVE_TAC[]); 734 735 736val XP_NEXT_FORALL_SEM = 737 store_thm 738 ("XP_NEXT_FORALL_SEM", 739 740 ``!s s' l p. (XP_SEM (XP_NEXT_FORALL l p) (s, s')) = 741 (!l'. (l' SUBSET (LIST_TO_SET l)) ==> (XP_SEM p (s, ((s' DIFF (LIST_TO_SET l)) UNION l'))))``, 742 743 REWRITE_TAC[XP_NEXT_FORALL_def, XP_SEM_THM, XP_NEXT_EXISTS_SEM] THEN 744 PROVE_TAC[]); 745 746 747 748(***************************************************************************** 749 * Variable renamings 750 *****************************************************************************) 751val FINITE___XP_USED_CURRENT_VARS = 752 store_thm 753 ("FINITE___XP_USED_CURRENT_VARS", 754 755 ``!p. FINITE(XP_USED_CURRENT_VARS p)``, 756 757 INDUCT_THEN xprop_logic_induct ASSUME_TAC THENL [ 758 REWRITE_TAC[XP_USED_CURRENT_VARS_def, FINITE_SING], 759 REWRITE_TAC[XP_USED_CURRENT_VARS_def, FINITE_EMPTY], 760 REWRITE_TAC[XP_USED_CURRENT_VARS_def, FINITE_EMPTY], 761 ASM_REWRITE_TAC[XP_USED_CURRENT_VARS_def], 762 ASM_REWRITE_TAC[XP_USED_CURRENT_VARS_def, FINITE_UNION] 763 ]); 764 765 766val FINITE___XP_USED_X_VARS = 767 store_thm 768 ("FINITE___XP_USED_X_VARS", 769 770 ``!p. FINITE(XP_USED_X_VARS p)``, 771 772 INDUCT_THEN xprop_logic_induct ASSUME_TAC THENL [ 773 REWRITE_TAC[XP_USED_X_VARS_def, FINITE_EMPTY], 774 REWRITE_TAC[XP_USED_X_VARS_def, FINITE_SING], 775 REWRITE_TAC[XP_USED_X_VARS_def, FINITE_EMPTY], 776 ASM_REWRITE_TAC[XP_USED_X_VARS_def], 777 ASM_REWRITE_TAC[XP_USED_X_VARS_def, FINITE_UNION] 778 ]); 779 780 781val FINITE___XP_USED_VARS = 782 store_thm 783 ("FINITE___XP_USED_VARS", 784 785 ``!p. FINITE(XP_USED_VARS p)``, 786 787 REWRITE_TAC[XP_USED_VARS_def, FINITE___XP_USED_X_VARS, FINITE___XP_USED_CURRENT_VARS, FINITE_UNION]); 788 789 790val XP_VAR_RENAMING___USED_CURRENT_VARS = 791 store_thm 792 ("XP_VAR_RENAMING___USED_CURRENT_VARS", 793 794 ``!a f. (XP_USED_CURRENT_VARS (XP_VAR_RENAMING f a) = 795 (IMAGE f (XP_USED_CURRENT_VARS a)))``, 796 797 INDUCT_THEN xprop_logic_induct ASSUME_TAC THENL [ 798 799 SIMP_TAC std_ss [XP_USED_CURRENT_VARS_def, 800 XP_VAR_RENAMING_def, 801 IMAGE_DEF, 802 EXTENSION, 803 GSPECIFICATION, 804 IN_SING, 805 EXISTS_PROD], 806 807 REWRITE_TAC [XP_USED_CURRENT_VARS_def, XP_VAR_RENAMING_def, IMAGE_EMPTY], REWRITE_TAC [XP_USED_CURRENT_VARS_def, XP_VAR_RENAMING_def, IMAGE_EMPTY], 808 ASM_REWRITE_TAC [XP_USED_CURRENT_VARS_def, XP_VAR_RENAMING_def], 809 ASM_REWRITE_TAC [XP_USED_CURRENT_VARS_def, XP_VAR_RENAMING_def, IMAGE_UNION] 810 ]); 811 812 813val XP_VAR_RENAMING___USED_X_VARS = 814 store_thm 815 ("XP_VAR_RENAMING___USED_X_VARS", 816 817 ``!a f. (XP_USED_X_VARS (XP_VAR_RENAMING f a) = 818 (IMAGE f (XP_USED_X_VARS a)))``, 819 820 INDUCT_THEN xprop_logic_induct ASSUME_TAC THENL [ 821 822 REWRITE_TAC [XP_USED_X_VARS_def, XP_VAR_RENAMING_def, IMAGE_EMPTY], 823 824 SIMP_TAC std_ss [XP_USED_X_VARS_def, 825 XP_VAR_RENAMING_def, 826 IMAGE_DEF, 827 EXTENSION, 828 GSPECIFICATION, 829 IN_SING], 830 831 REWRITE_TAC [XP_USED_X_VARS_def, XP_VAR_RENAMING_def, IMAGE_EMPTY], 832 ASM_REWRITE_TAC [XP_USED_X_VARS_def, XP_VAR_RENAMING_def], 833 ASM_REWRITE_TAC [XP_USED_X_VARS_def, XP_VAR_RENAMING_def, IMAGE_UNION] 834 ]); 835 836 837val XP_VAR_RENAMING___USED_VARS = 838 store_thm 839 ("XP_VAR_RENAMING___USED_VARS", 840 841 ``!a f. (XP_USED_VARS (XP_VAR_RENAMING f a) = 842 (IMAGE f (XP_USED_VARS a)))``, 843 844 REWRITE_TAC[XP_USED_VARS_def, IMAGE_UNION, 845 XP_VAR_RENAMING___USED_CURRENT_VARS, XP_VAR_RENAMING___USED_X_VARS]); 846 847 848 849val XP_USED_VARS_INTER_SUBSET_THM = 850 store_thm 851 ("XP_USED_VARS_INTER_SUBSET_THM", 852 ``!b S s1 s2. 853 (((XP_USED_X_VARS b) SUBSET S) ==> 854 ((XP_SEM b (s1, s2)) = (XP_SEM b (s1, s2 INTER S)))) /\ 855 856 (((XP_USED_CURRENT_VARS b) SUBSET S) ==> 857 ((XP_SEM b (s1, s2)) = (XP_SEM b (s1 INTER S, s2))))``, 858 859 INDUCT_THEN xprop_logic_induct ASSUME_TAC THENL [ 860 SIMP_TAC std_ss [XP_USED_X_VARS_def, XP_USED_CURRENT_VARS_def, EMPTY_SUBSET, XP_SEM_def, IN_INTER, 861 SUBSET_DEF, IN_SING], 862 863 SIMP_TAC std_ss [XP_USED_X_VARS_def, XP_USED_CURRENT_VARS_def, EMPTY_SUBSET, XP_SEM_def, IN_INTER, 864 SUBSET_DEF, IN_SING], 865 866 SIMP_TAC std_ss [XP_SEM_def], 867 ASM_SIMP_TAC std_ss [XP_SEM_def, XP_USED_X_VARS_def, XP_USED_CURRENT_VARS_def], 868 869 ASM_SIMP_TAC std_ss [XP_SEM_def, XP_USED_X_VARS_def, XP_USED_CURRENT_VARS_def, UNION_SUBSET] THEN 870 PROVE_TAC[] 871 ]); 872 873 874val XP_USED_VARS_INTER_THM = 875 store_thm 876 ("XP_USED_VARS_INTER_THM", 877 ``!b s1 s2. 878 ((XP_SEM b (s1, s2)) = (XP_SEM b (s1 INTER (XP_USED_CURRENT_VARS b), s2 INTER (XP_USED_X_VARS b))))``, 879 880 PROVE_TAC[XP_USED_VARS_INTER_SUBSET_THM, SUBSET_REFL]); 881 882 883val XP_USED_VARS_INTER_SUBSET_BOTH_THM = 884 store_thm 885 ("XP_USED_VARS_INTER_SUBSET_BOTH_THM", 886 ``!b S s1 s2. 887 ((XP_USED_VARS b) SUBSET S) ==> 888 ((XP_SEM b (s1, s2)) = (XP_SEM b (s1 INTER S, s2 INTER S)))``, 889 890 REWRITE_TAC[XP_USED_VARS_def, UNION_SUBSET] THEN 891 METIS_TAC[XP_USED_VARS_INTER_SUBSET_THM]); 892 893 894val XP_SEM___VAR_RENAMING___NOT_INJ = 895 store_thm ( 896 "XP_SEM___VAR_RENAMING___NOT_INJ", 897 ``!p f s1 s2. XP_SEM (XP_VAR_RENAMING f p) (s1, s2) = XP_SEM p 898 ((\x. f x IN s1), (\x. f x IN s2))``, 899 900 INDUCT_THEN xprop_logic_induct ASSUME_TAC THEN ( 901 ASM_SIMP_TAC std_ss [XP_VAR_RENAMING_def, XP_SEM_def, IN_ABS] 902 )); 903 904val XP_SEM___VAR_RENAMING = 905 store_thm 906 ("XP_SEM___VAR_RENAMING", 907 ``!p f s1 s2. (INJ f (s1 UNION s2 UNION XP_USED_VARS p) UNIV) ==> ((XP_SEM p (s1,s2)) = (XP_SEM (XP_VAR_RENAMING f p) (IMAGE f s1, IMAGE f s2)))``, 908 909 INDUCT_THEN xprop_logic_induct ASSUME_TAC THEN REPEAT STRIP_TAC THENL [ 910 SIMP_ALL_TAC std_ss [INJ_DEF, IMAGE_DEF, IN_UNIV, IN_UNION, XP_SEM_def, XP_VAR_RENAMING_def, GSPECIFICATION, 911 XP_USED_VARS_def, XP_USED_CURRENT_VARS_def, IN_SING] THEN 912 PROVE_TAC[], 913 914 SIMP_ALL_TAC std_ss [INJ_DEF, IMAGE_DEF, IN_UNIV, IN_UNION, XP_SEM_def, XP_VAR_RENAMING_def, GSPECIFICATION, 915 XP_USED_VARS_def, XP_USED_X_VARS_def, IN_SING] THEN 916 PROVE_TAC[], 917 918 SIMP_TAC std_ss [XP_SEM_def, XP_VAR_RENAMING_def], 919 920 FULL_SIMP_TAC std_ss [XP_SEM_def, XP_VAR_RENAMING_def, XP_USED_VARS_def, XP_USED_CURRENT_VARS_def, 921 XP_USED_X_VARS_def], 922 923 FULL_SIMP_TAC std_ss [XP_SEM_def, XP_VAR_RENAMING_def, XP_USED_VARS_def, XP_USED_CURRENT_VARS_def, 924 XP_USED_X_VARS_def] THEN 925 SUBGOAL_TAC `(s1 UNION s2 UNION (XP_USED_CURRENT_VARS p UNION XP_USED_X_VARS p)) SUBSET 926 (s1 UNION s2 UNION (XP_USED_CURRENT_VARS p UNION XP_USED_CURRENT_VARS p' UNION 927 (XP_USED_X_VARS p UNION XP_USED_X_VARS p'))) /\ 928 929 (s1 UNION s2 UNION (XP_USED_CURRENT_VARS p' UNION XP_USED_X_VARS p')) SUBSET 930 (s1 UNION s2 UNION (XP_USED_CURRENT_VARS p UNION XP_USED_CURRENT_VARS p' UNION 931 (XP_USED_X_VARS p UNION XP_USED_X_VARS p')))` THEN1 ( 932 933 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] THEN 934 PROVE_TAC[] 935 ) THEN 936 PROVE_TAC[INJ_SUBSET, SUBSET_REFL] 937 ]); 938 939 940val XP_VAR_RENAMING_EVAL = 941 store_thm 942 ("XP_VAR_RENAMING_EVAL", 943 ``!p f b b1 b2. ( 944 (XP_VAR_RENAMING f (XP_TRUE) = XP_TRUE) /\ 945 (XP_VAR_RENAMING f (XP_FALSE) = XP_FALSE) /\ 946 (XP_VAR_RENAMING f (XP_PROP p) = (XP_PROP (f p))) /\ 947 (XP_VAR_RENAMING f (XP_NEXT_PROP p) = (XP_NEXT_PROP (f p))) /\ 948 (XP_VAR_RENAMING f (XP_NOT b) = XP_NOT(XP_VAR_RENAMING f b)) /\ 949 (XP_VAR_RENAMING f (XP_AND(b1, b2)) = XP_AND(XP_VAR_RENAMING f b1, XP_VAR_RENAMING f b2)) /\ 950 (XP_VAR_RENAMING f (XP_OR(b1, b2)) = XP_OR(XP_VAR_RENAMING f b1, XP_VAR_RENAMING f b2)) /\ 951 (XP_VAR_RENAMING f (XP_IMPL(b1, b2)) = XP_IMPL(XP_VAR_RENAMING f b1, XP_VAR_RENAMING f b2)) /\ 952 (XP_VAR_RENAMING f (XP_EQUIV(b1, b2)) = XP_EQUIV(XP_VAR_RENAMING f b1, XP_VAR_RENAMING f b2)) 953 )``, 954 955 REWRITE_TAC[XP_VAR_RENAMING_def, XP_FALSE_def, XP_OR_def, XP_IMPL_def, XP_EQUIV_def]); 956 957 958val XP_PROP_SET_MODEL_SEM = 959 store_thm 960 ("XP_PROP_SET_MODEL_SEM", 961 ``!S1 S2 S' T1 T2. FINITE S' ==> ((XP_SEM (XP_PROP_SET_MODEL S1 S2 S') (T1,T2)) = ((T1 INTER S' = S1 INTER S') /\ (T2 INTER S' = S2 INTER S')))``, 962 963 REWRITE_TAC[XP_PROP_SET_MODEL_def, XP_SEM_THM, 964 XP_SEM___XP_CURRENT, XP_SEM___XP_NEXT] THEN 965 PROVE_TAC[P_PROP_SET_MODEL_SEM]); 966 967 968val XP_PROP_SET_MODEL_CURRENT_SEM = 969 store_thm 970 ("XP_PROP_SET_MODEL_CURRENT_SEM", 971 ``!f S' T1 T2. FINITE S' ==> ((XP_SEM (XP_PROP_SET_MODEL_CURRENT f S') (T1,T2)) = ((T1 INTER S') = (f (T2 INTER S') INTER S')))``, 972 973 REWRITE_TAC[XP_PROP_SET_MODEL_CURRENT_def, XP_SEM_THM, 974 XP_BIGOR_SEM] THEN 975 REPEAT STRIP_TAC THEN 976 ASM_SIMP_TAC std_ss [FINITE_POW_IFF, IMAGE_FINITE, 977 MEM_SET_TO_LIST, IN_IMAGE, GSYM LEFT_EXISTS_AND_THM, 978 XP_SEM_THM, XP_SEM___XP_CURRENT, XP_SEM___XP_NEXT, 979 P_PROP_SET_MODEL_SEM, IN_POW 980 ] THEN 981 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 982 ASM_REWRITE_TAC[], 983 984 EXISTS_TAC ``T2 INTER S'`` THEN 985 ASM_REWRITE_TAC[INTER_INTER_ABSORPTION, 986 INTER_SUBSET] 987 ]); 988 989 990val XP_PROP_SET_MODEL_NEXT_SEM = 991 store_thm 992 ("XP_PROP_SET_MODEL_NEXT_SEM", 993 ``!f S' T1 T2. FINITE S' ==> ((XP_SEM (XP_PROP_SET_MODEL_NEXT f S') (T1,T2)) = ((T2 INTER S') = (f (T1 INTER S') INTER S')))``, 994 995 REWRITE_TAC[XP_PROP_SET_MODEL_NEXT_def, XP_SEM_THM, 996 XP_BIGOR_SEM] THEN 997 REPEAT STRIP_TAC THEN 998 ASM_SIMP_TAC std_ss [FINITE_POW_IFF, IMAGE_FINITE, 999 MEM_SET_TO_LIST, IN_IMAGE, GSYM LEFT_EXISTS_AND_THM, 1000 XP_SEM_THM, XP_SEM___XP_CURRENT, XP_SEM___XP_NEXT, 1001 P_PROP_SET_MODEL_SEM, IN_POW 1002 ] THEN 1003 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1004 ASM_REWRITE_TAC[], 1005 1006 EXISTS_TAC ``T1 INTER S'`` THEN 1007 ASM_REWRITE_TAC[INTER_INTER_ABSORPTION, 1008 INTER_SUBSET] 1009 ]); 1010 1011 1012 1013 1014val XP_ASSIGN_TRUE_FALSE___XP_USED_VARS = 1015 store_thm ("XP_ASSIGN_TRUE_FALSE___XP_USED_VARS", 1016 ``!xp v1 v2. 1017 (XP_USED_CURRENT_VARS (XP_ASSIGN_TRUE v1 v2 xp) = 1018 XP_USED_CURRENT_VARS xp DIFF v1) /\ 1019 (XP_USED_X_VARS (XP_ASSIGN_TRUE v1 v2 xp) = 1020 XP_USED_X_VARS xp DIFF v2) /\ 1021 (XP_USED_CURRENT_VARS (XP_ASSIGN_FALSE v1 v2 xp) = 1022 XP_USED_CURRENT_VARS xp DIFF v1) /\ 1023 (XP_USED_X_VARS (XP_ASSIGN_FALSE v1 v2 xp) = 1024 XP_USED_X_VARS xp DIFF v2)``, 1025 1026 INDUCT_THEN xprop_logic_induct ASSUME_TAC THENL [ 1027 REWRITE_TAC [XP_ASSIGN_TRUE_def, XP_ASSIGN_FALSE_def] THEN 1028 REPEAT GEN_TAC THEN 1029 Cases_on `a IN v1` THEN ( 1030 ASM_SIMP_TAC std_ss [XP_USED_VARS_EVAL, EXTENSION, IN_DIFF, 1031 IN_SING, NOT_IN_EMPTY] THEN 1032 PROVE_TAC[] 1033 ), 1034 1035 1036 REWRITE_TAC [XP_ASSIGN_TRUE_def, XP_ASSIGN_FALSE_def] THEN 1037 REPEAT GEN_TAC THEN 1038 Cases_on `a IN v2` THEN ( 1039 ASM_SIMP_TAC std_ss [XP_USED_VARS_EVAL, EXTENSION, IN_DIFF, 1040 IN_SING, NOT_IN_EMPTY] THEN 1041 PROVE_TAC[] 1042 ), 1043 1044 SIMP_TAC std_ss [XP_ASSIGN_TRUE_def, XP_USED_VARS_EVAL, EMPTY_DIFF, 1045 XP_ASSIGN_FALSE_def], 1046 1047 ASM_SIMP_TAC std_ss [XP_ASSIGN_TRUE_def, XP_ASSIGN_FALSE_def, XP_USED_VARS_EVAL], 1048 1049 ASM_SIMP_TAC std_ss [XP_ASSIGN_TRUE_def, XP_ASSIGN_FALSE_def, XP_USED_VARS_EVAL, UNION_OVER_DIFF] 1050 ]); 1051 1052 1053val XP_ASSIGN_TRUE_FALSE___EVAL = 1054 store_thm ("XP_ASSIGN_TRUE_FALSE___EVAL", 1055 ``(XP_ASSIGN_TRUE V V' (XP_PROP p) = (if p IN V then XP_TRUE else XP_PROP p)) /\ 1056 (XP_ASSIGN_TRUE V V' (XP_NEXT_PROP p) = (if p IN V' then XP_TRUE else XP_NEXT_PROP p)) /\ 1057 (XP_ASSIGN_TRUE V V' XP_TRUE = XP_TRUE) /\ 1058 (XP_ASSIGN_TRUE V V' XP_FALSE = XP_FALSE) /\ 1059 (XP_ASSIGN_TRUE V V' (XP_NOT b) = XP_NOT(XP_ASSIGN_TRUE V V' b)) /\ 1060 (XP_ASSIGN_TRUE V V' (XP_AND(b1,b2)) = XP_AND (XP_ASSIGN_TRUE V V' b1, XP_ASSIGN_TRUE V V' b2)) /\ 1061 (XP_ASSIGN_TRUE V V' (XP_OR(b1,b2)) = XP_OR (XP_ASSIGN_TRUE V V' b1, XP_ASSIGN_TRUE V V' b2)) /\ 1062 (XP_ASSIGN_TRUE V V' (XP_IMPL(b1,b2)) = XP_IMPL (XP_ASSIGN_TRUE V V' b1, XP_ASSIGN_TRUE V V' b2)) /\ 1063 (XP_ASSIGN_TRUE V V' (XP_COND(c, b1,b2)) = XP_COND (XP_ASSIGN_TRUE V V' c, XP_ASSIGN_TRUE V V' b1, XP_ASSIGN_TRUE V V' b2)) /\ 1064 (XP_ASSIGN_TRUE V V' (XP_EQUIV (b1,b2)) = XP_EQUIV (XP_ASSIGN_TRUE V V' b1, XP_ASSIGN_TRUE V V' b2)) /\ 1065 1066 (XP_ASSIGN_FALSE V V' (XP_PROP p) = (if p IN V then XP_FALSE else XP_PROP p)) /\ 1067 (XP_ASSIGN_FALSE V V' (XP_NEXT_PROP p) = (if p IN V' then XP_FALSE else XP_NEXT_PROP p)) /\ 1068 (XP_ASSIGN_FALSE V V' XP_TRUE = XP_TRUE) /\ 1069 (XP_ASSIGN_FALSE V V' XP_FALSE = XP_FALSE) /\ 1070 (XP_ASSIGN_FALSE V V' (XP_NOT b) = XP_NOT(XP_ASSIGN_FALSE V V' b)) /\ 1071 (XP_ASSIGN_FALSE V V' (XP_AND(b1,b2)) = XP_AND (XP_ASSIGN_FALSE V V' b1, XP_ASSIGN_FALSE V V' b2)) /\ 1072 (XP_ASSIGN_FALSE V V' (XP_OR(b1,b2)) = XP_OR (XP_ASSIGN_FALSE V V' b1, XP_ASSIGN_FALSE V V' b2)) /\ 1073 (XP_ASSIGN_FALSE V V' (XP_IMPL(b1,b2)) = XP_IMPL (XP_ASSIGN_FALSE V V' b1, XP_ASSIGN_FALSE V V' b2)) /\ 1074 (XP_ASSIGN_FALSE V V' (XP_COND(c, b1,b2)) = XP_COND (XP_ASSIGN_FALSE V V' c, XP_ASSIGN_FALSE V V' b1, XP_ASSIGN_FALSE V V' b2)) /\ 1075 (XP_ASSIGN_FALSE V V' (XP_EQUIV(b1,b2)) = XP_EQUIV (XP_ASSIGN_FALSE V V' b1, XP_ASSIGN_FALSE V V' b2))``, 1076 1077 SIMP_TAC std_ss [XP_ASSIGN_TRUE_def, XP_ASSIGN_FALSE_def, XP_FALSE_def, XP_EQUIV_def, XP_IMPL_def, XP_OR_def, XP_COND_def]); 1078 1079 1080val XP_EXISTS___XP_USED_VARS = 1081 store_thm ("XP_EXISTS___XP_USED_VARS", 1082 ``!l p. 1083 (XP_USED_CURRENT_VARS (XP_CURRENT_EXISTS l p) = 1084 XP_USED_CURRENT_VARS p DIFF (LIST_TO_SET l)) /\ 1085 (XP_USED_X_VARS (XP_CURRENT_EXISTS l p) = 1086 XP_USED_X_VARS p) /\ 1087 (XP_USED_X_VARS (XP_NEXT_EXISTS l p) = 1088 XP_USED_X_VARS p DIFF (LIST_TO_SET l)) /\ 1089 (XP_USED_CURRENT_VARS (XP_NEXT_EXISTS l p) = 1090 XP_USED_CURRENT_VARS p)``, 1091 1092 Induct_on `l` THENL [ 1093 SIMP_TAC std_ss [XP_CURRENT_EXISTS_def, LIST_TO_SET_THM, DIFF_EMPTY, 1094 XP_NEXT_EXISTS_def], 1095 1096 ASM_SIMP_TAC std_ss [XP_CURRENT_EXISTS_def, XP_NEXT_EXISTS_def, 1097 LIST_TO_SET_THM, DIFF_EMPTY, 1098 XP_USED_VARS_EVAL, XP_ASSIGN_TRUE_FALSE___XP_USED_VARS] THEN 1099 SIMP_TAC std_ss [EXTENSION, IN_UNION, IN_DIFF, IN_SING, IN_INSERT] THEN 1100 PROVE_TAC[] 1101 ]) 1102 1103 1104val XP_FORALL___XP_USED_VARS = 1105 store_thm ("XP_FORALL___XP_USED_VARS", 1106 ``!l p. 1107 (XP_USED_CURRENT_VARS (XP_CURRENT_FORALL l p) = 1108 XP_USED_CURRENT_VARS p DIFF (LIST_TO_SET l)) /\ 1109 (XP_USED_X_VARS (XP_CURRENT_FORALL l p) = 1110 XP_USED_X_VARS p) /\ 1111 (XP_USED_X_VARS (XP_NEXT_FORALL l p) = 1112 XP_USED_X_VARS p DIFF (LIST_TO_SET l)) /\ 1113 (XP_USED_CURRENT_VARS (XP_NEXT_FORALL l p) = 1114 XP_USED_CURRENT_VARS p)``, 1115 1116 SIMP_TAC std_ss [XP_CURRENT_FORALL_def, XP_NEXT_FORALL_def, 1117 XP_USED_VARS_EVAL, XP_EXISTS___XP_USED_VARS]); 1118 1119 1120val XP_BIGOR___XP_USED_VARS = 1121 store_thm ("XP_BIGOR___XP_USED_VARS", 1122 ``!l. (XP_USED_CURRENT_VARS (XP_BIGOR l) = LIST_BIGUNION (MAP (\xp. XP_USED_CURRENT_VARS xp) l)) /\ 1123 (XP_USED_X_VARS (XP_BIGOR l) = LIST_BIGUNION (MAP (\xp. XP_USED_X_VARS xp) l)) /\ 1124 (XP_USED_VARS (XP_BIGOR l) = LIST_BIGUNION (MAP (\xp. XP_USED_VARS xp) l))``, 1125 1126 Induct_on `l` THENL [ 1127 SIMP_TAC list_ss [XP_BIGOR_def, XP_USED_VARS_EVAL, LIST_BIGUNION_def], 1128 ASM_SIMP_TAC list_ss [XP_BIGOR_def, XP_USED_VARS_EVAL, LIST_BIGUNION_def] 1129 ]); 1130 1131 1132val XP_CURRENT_NEXT___ASSIGN_TRUE_FALSE = 1133 store_thm ( 1134 "XP_CURRENT_NEXT___ASSIGN_TRUE_FALSE", 1135 ``!p V. 1136 (XP_CURRENT (P_ASSIGN_TRUE V p) = XP_ASSIGN_TRUE V EMPTY (XP_CURRENT p)) /\ 1137 (XP_NEXT (P_ASSIGN_TRUE V p) = XP_ASSIGN_TRUE EMPTY V (XP_NEXT p)) /\ 1138 1139 (XP_CURRENT (P_ASSIGN_FALSE V p) = XP_ASSIGN_FALSE V EMPTY (XP_CURRENT p)) /\ 1140 (XP_NEXT (P_ASSIGN_FALSE V p) = XP_ASSIGN_FALSE EMPTY V (XP_NEXT p))``, 1141 1142INDUCT_THEN prop_logic_induct ASSUME_TAC THEN ( 1143 ASM_SIMP_TAC std_ss [P_ASSIGN_TRUE_def, P_ASSIGN_FALSE_def, XP_ASSIGN_TRUE_def, 1144 XP_ASSIGN_FALSE_def, XP_CURRENT_THM, XP_NEXT_THM, COND_RATOR, COND_RAND] 1145)) 1146 1147 1148 1149val XP_CURRENT_NEXT___EXISTS = 1150 store_thm ( 1151 "XP_CURRENT_NEXT___EXISTS", 1152 ``!p l. 1153 (XP_CURRENT (P_EXISTS l p) = XP_CURRENT_EXISTS l (XP_CURRENT p)) /\ 1154 (XP_NEXT (P_EXISTS l p) = XP_NEXT_EXISTS l (XP_NEXT p))``, 1155 1156 Induct_on `l` THENL [ 1157 SIMP_TAC std_ss [P_EXISTS_def, XP_CURRENT_EXISTS_def, XP_NEXT_EXISTS_def], 1158 1159 ASM_SIMP_TAC std_ss [P_EXISTS_def, XP_CURRENT_EXISTS_def, XP_NEXT_EXISTS_def, 1160 XP_NEXT_THM, XP_CURRENT_NEXT___ASSIGN_TRUE_FALSE, 1161 XP_CURRENT_THM] 1162 ]); 1163 1164val XP_CURRENT_NEXT___FORALL = 1165 store_thm ( 1166 "XP_CURRENT_NEXT___FORALL", 1167 1168 ``!l p. 1169 (XP_CURRENT (P_FORALL l p) = XP_CURRENT_FORALL l (XP_CURRENT p)) /\ 1170 (XP_NEXT (P_FORALL l p) = XP_NEXT_FORALL l (XP_NEXT p))``, 1171 1172 SIMP_TAC std_ss [P_FORALL_def, XP_CURRENT_FORALL_def, XP_NEXT_FORALL_def, 1173 XP_CURRENT_NEXT___EXISTS, XP_NEXT_THM, XP_CURRENT_THM] 1174) 1175 1176 1177 1178 1179val _ = export_theory(); 1180