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