1open HolKernel Parse boolLib bossLib 2 3val _ = new_theory("muSyntax") 4 5 6open bossLib 7open pairTheory 8open pairLib 9open pairTools 10open pairSyntax 11open pred_setTheory 12open pred_setLib 13open listTheory 14open stringTheory 15open sumTheory 16open simpLib 17open stringLib 18open numLib 19open metisLib 20open ksTheory 21open setLemmasTheory 22open reachTheory 23 24infix && infix 8 by 25 26fun tsimps ty = let val {convs,rewrs} = TypeBase.simpls_of ty in rewrs end 27 28 29(* ======================propositional mu calculus: types,syntax,semantics etc =======================*) 30 31(* note to self: using string rather than mu (in RV,<>,[]) because the terms denoted are not themselves mu-calc formulae *) 32(* even though this approach clutters up the syntax with double quotes, it is the right way to do things *) 33(* however, using strings for bound vars of mu an nu is a hack because it is a pain getting general support for binders *) 34 35val _ = bossLib.Hol_datatype ` 36 mu = TR 37 | FL 38 | Not of mu 39 | And of mu => mu 40 | Or of mu => mu 41 | RV of string (* relational var *) 42 | AP of 'prop (* atomic proposition *) 43 | DIAMOND of string => mu (* diamond *) 44 | BOX of string => mu (* box *) 45 | mu of string => mu (* lfp *) 46 | nu of string => mu` (* mfp *) 47 48val tsimps_mu = tsimps ``:'prop mu``; 49 50 51val mu_size_def = snd (TypeBase.size_of ``:'prop mu``) 52val mu_size2_def = Define `mu_size2 (f: 'prop mu) = mu_size (\(a:('prop)).0) f` 53 54val _ = add_rule 55 {term_name = "AP", fixity = Prefix 950, (* 950 is tighter than ~ *) 56 pp_elements = [TOK "AP", HardSpace 1], 57 paren_style = OnlyIfNecessary, 58 block_style = (AroundSamePrec, (PP.INCONSISTENT, 0))} 59 60(* overload ~,/\,\/,T and F give priority to the boolean versions *) 61 62val _ = overload_on ("~", mk_const("~",``:bool -> bool``)) 63val _ = overload_on ("~", (``$Not``)) 64val _ = overload_on ("~", mk_const("~",``:bool -> bool``)) 65fun prepOverload s = overload_on (s, mk_const(s,``:bool -> bool -> bool``)) 66val _ = app prepOverload ["/\\", "\\/"] 67val _ = overload_on ("/\\", (``$And``)) val _ = prepOverload "/\\" 68val _ = overload_on ("\\/", (``$Or``)) val _ = prepOverload "\\/" 69val _ = overload_on ("T",T) val _ = overload_on ("T",``TR``) val _ = overload_on ("T",T) 70val _ = overload_on ("F",F) val _ = overload_on ("F",``FL``) val _ = overload_on ("F",F) 71 72(* make syntax for DIAMOND, BOX, lfp and mfp (somewhat) resemble standard notation *) 73(* Need to use << and >> because of precedence conflicts with < and > *) 74 75(* prec 2501 is higher fixity than any thing in default term grammar WIP: does this make sense...not really, should be lower *) 76val _ = add_rule {term_name = "DIAMOND", fixity = Prefix 2501, 77 pp_elements = [TOK "<<", TM, TOK ">>", HardSpace 1], 78 paren_style = OnlyIfNecessary, 79 block_style = (AroundSamePrec, (PP.INCONSISTENT, 0))} 80(* Could actually use [ and ] here by declaring CloseFix fixity. But this is for consistency with lfp *) 81val _ = add_rule {term_name = "BOX", fixity = Prefix 2501, 82 pp_elements = [TOK "[[", TM, TOK "]]",HardSpace 1], 83 paren_style = OnlyIfNecessary, 84 block_style = (AroundSamePrec, (PP.INCONSISTENT, 0))} 85val _ = add_rule {term_name = "mu", fixity = Prefix 2, 86 pp_elements = [TOK "mu",HardSpace 1, TM, TOK "..",HardSpace 1], 87 paren_style = OnlyIfNecessary, 88 block_style = (AroundSamePrec, (PP.INCONSISTENT, 0))} 89val _ = add_rule {term_name = "nu", fixity = Prefix 2, 90 pp_elements = [TOK "nu", HardSpace 1, TM, TOK "..",HardSpace 1], 91 paren_style = OnlyIfNecessary, 92 block_style = (AroundSamePrec, (PP.INCONSISTENT, 0))} 93 94(* defns for checking well-formedness of a mu-formula (bound vars must occur +vely within its scope) *) 95 96(* RVNEG(f,Q) == in f, all free ocurrances of Q are negated *) 97val RVNEG_def = save_thm("RVNEG_def",Define` 98(RVNEG rv (T:'prop mu) = (T:'prop mu)) /\ 99(RVNEG rv F = F) /\ 100(RVNEG rv (f /\ g) = (RVNEG rv f) /\ (RVNEG rv g)) /\ 101(RVNEG rv (f \/ g) = (RVNEG rv f) \/ (RVNEG rv g)) /\ 102(RVNEG rv (AP p) = AP p) /\ 103(RVNEG rv (RV Q) = if (rv=Q) then (~(RV Q)) else (RV Q)) /\ 104(RVNEG rv (<<a>> f) = <<a>> (RVNEG rv f)) /\ 105(RVNEG rv ([[a]] f) = [[a]] (RVNEG rv f)) /\ 106(RVNEG rv (mu Q .. f) = if (rv=Q) then (mu Q .. f) else (mu Q .. (RVNEG rv f))) /\ 107(RVNEG rv (nu Q .. f) = if (rv=Q) then (nu Q .. f) else (nu Q .. (RVNEG rv f))) /\ 108(RVNEG rv (~f) = ~(RVNEG rv f))`) 109 110val mu_pnf = Hol_defn "NNF" ` 111(NNF (T:'prop mu) = (T:'prop mu)) /\ 112(NNF F = F) /\ 113(NNF (f /\ g) = NNF f /\ NNF g) /\ 114(NNF (f \/ g) = NNF f \/ NNF g) /\ 115(NNF (AP p) = AP p) /\ 116(NNF (RV Q) = RV Q) /\ 117(NNF (<<a>> f) = <<a>> (NNF f)) /\ 118(NNF ([[a]] f) = [[a]] (NNF f)) /\ 119(NNF (mu Q .. f) = mu Q .. (NNF f)) /\ 120(NNF (nu Q .. f) = nu Q .. (NNF f)) /\ 121(NNF (~T) = F) /\ 122(NNF (~F) = T) /\ 123(NNF (~(f /\ g)) = ((NNF ~f)) \/ ((NNF ~g))) /\ 124(NNF (~(f \/ g)) = ((NNF ~f)) /\ ((NNF ~g))) /\ 125(NNF (~(AP p)) = ~(AP p)) /\ 126(NNF (~(RV Q)) = ~(RV Q)) /\ 127(NNF (~(<<a>> f)) = [[a]] (NNF ~f)) /\ 128(NNF (~([[a]] f)) = <<a>> (NNF ~f)) /\ 129(NNF (~~f) = NNF f) /\ 130(NNF (~(mu Q.. f)) = nu Q.. (NNF(RVNEG Q (~f)))) /\ 131(NNF (~(nu Q.. f)) = mu Q.. (NNF(RVNEG Q (~f))))` 132 133val mu_pstv_size_def = Define` 134(mu_pstv_size (T:'prop mu) = mu_size2 (T: 'prop mu)) /\ 135(mu_pstv_size (F:'prop mu) = mu_size2 (F: 'prop mu)) /\ 136(mu_pstv_size (f /\ g) = 1+ (mu_pstv_size f + mu_pstv_size g)) /\ 137(mu_pstv_size (f \/ g) = 1+ (mu_pstv_size f + mu_pstv_size g)) /\ 138(mu_pstv_size ((AP (p:'prop)):'prop mu) = mu_size2 ((AP (p:'prop)):'prop mu)) /\ 139(mu_pstv_size ((RV (Q:string)):'prop mu) = mu_size2 ((RV (Q:string)):'prop mu)) /\ 140(mu_pstv_size (<<(a:string)>> f) = 1 + (mu_pstv_size f)) /\ 141(mu_pstv_size ([[(a:string)]] f) = 1+ (mu_pstv_size f)) /\ 142(mu_pstv_size (mu (Q:string) .. f) = 1+ (STRLEN Q + mu_pstv_size f)) /\ 143(mu_pstv_size (nu (Q:string) .. f) = 1+ (STRLEN Q + mu_pstv_size f)) /\ 144(mu_pstv_size (~f) = mu_pstv_size f)` 145 146val mu_pstv_size_lemma1 = prove(``!f Q. mu_pstv_size (RVNEG Q f) = mu_pstv_size f``, 147 Induct_on `f` THEN RW_TAC std_ss [mu_pstv_size_def,RVNEG_def] THEN RW_TAC arith_ss [mu_pstv_size_def,RVNEG_def]) 148 149val mu_pstv_size_lemma2 = prove(``!f Q. mu_pstv_size (RVNEG Q (~f)) = mu_pstv_size f``, 150 Induct_on `f` THEN RW_TAC std_ss [mu_pstv_size_def,RVNEG_def] 151 THEN RW_TAC arith_ss [mu_pstv_size_def,RVNEG_def,mu_pstv_size_lemma1]) 152 153val (NNF_def,NNF_IND_def) = Defn.tprove(mu_pnf,WF_REL_TAC `inv_image ($< LEX $<) (\f. (mu_pstv_size f,mu_size2 f))` THEN RW_TAC std_ss [mu_size_def,mu_size2_def,mu_pstv_size_def] THEN RW_TAC arith_ss [mu_pstv_size_lemma2]) 154val _ = save_thm("NNF_def",NNF_def) 155val _ = save_thm("NNF_IND_def",NNF_IND_def) 156 157val MU_SUB_def = save_thm("MU_SUB_def",Define ` 158(SUBFORMULA (g:'prop mu) (T:'prop mu) = (g = T)) /\ 159(SUBFORMULA g F = (g = F)) /\ 160(SUBFORMULA g (~f) = (SUBFORMULA g f) \/ (g=~f)) /\ 161(SUBFORMULA g (f1 /\ f2) = (SUBFORMULA g f1) \/ (SUBFORMULA g f2) \/ (g = f1 /\ f2)) /\ 162(SUBFORMULA g (f1 \/ f2) = (SUBFORMULA g f1) \/ (SUBFORMULA g f2) \/ (g = f1 \/ f2)) /\ 163(SUBFORMULA g (RV Q) = (g = RV Q)) /\ 164(SUBFORMULA g (AP p) = (g = AP p)) /\ 165(SUBFORMULA g (<<a>> f) = (SUBFORMULA g f) \/ (g = <<a>> f)) /\ 166(SUBFORMULA g ([[a]] f) = (SUBFORMULA g f) \/ (g = [[a]] f)) /\ 167(SUBFORMULA g (mu Q.. f) = (SUBFORMULA g f) \/ (g = mu Q.. f)) /\ 168(SUBFORMULA g (nu Q.. f) = (SUBFORMULA g f) \/ (g = nu Q.. f))`) 169 170val _ = add_rule 171 {term_name = "SUBFORMULA", fixity = Infix (NONASSOC,450), 172 pp_elements = [HardSpace 1,TOK "SUBF",HardSpace 1], 173 paren_style = OnlyIfNecessary, 174 block_style = (AroundSamePrec, (PP.INCONSISTENT, 0))} 175 176val IMF_def = save_thm("IMF_def",Define ` 177(IMF (T:'prop mu) = T) /\ 178(IMF F = T) /\ 179(IMF (~f) = IMF f) /\ 180(IMF (f1 /\ f2) = (IMF f1) /\ (IMF f2)) /\ 181(IMF (f1 \/ f2) = (IMF f1) /\ (IMF f2)) /\ 182(IMF (RV Q) = T) /\ 183(IMF (AP p) = T) /\ 184(IMF (<<a>> f) = IMF f) /\ 185(IMF ([[a]] f) = IMF f) /\ 186(IMF (mu Q.. f) = ~(SUBFORMULA (~RV Q) (NNF f)) /\ (IMF f)) /\ 187(IMF (nu Q.. f) = ~(SUBFORMULA (~RV Q) (NNF f)) /\ (IMF f))`) 188 189val FV_def = save_thm("FV_def",Define ` 190(FV (T:'prop mu) = {}) /\ 191(FV F = {}) /\ 192(FV (~f) = FV f) /\ 193(FV (f1 /\ f2) = (FV f1) UNION (FV f2)) /\ 194(FV (f1 \/ f2) = (FV f1) UNION (FV f2)) /\ 195(FV (RV Q) = {Q}) /\ 196(FV (AP p) = {}) /\ 197(FV (<<a>> f) = FV f) /\ 198(FV ([[a]] f) = FV f) /\ 199(FV (mu Q.. f) = (FV f) DELETE Q) /\ 200(FV (nu Q.. f) = (FV f) DELETE Q)`) 201 202val ALLV_def = save_thm("ALLV_def",Define ` 203(ALLV (T:'prop mu) = {}) /\ 204(ALLV F = {}) /\ 205(ALLV (~f) = ALLV f) /\ 206(ALLV (f1 /\ f2) = (ALLV f1) UNION (ALLV f2)) /\ 207(ALLV (f1 \/ f2) = (ALLV f1) UNION (ALLV f2)) /\ 208(ALLV (RV Q) = {Q}) /\ 209(ALLV (AP p) = {}) /\ 210(ALLV (<<a>> f) = ALLV f) /\ 211(ALLV ([[a]] f) = ALLV f) /\ 212(ALLV (mu Q.. f) = (ALLV f)) /\ 213(ALLV (nu Q.. f) = (ALLV f))`) 214 215val CLOSED_def = save_thm("CLOSED_def",Define `CLOSED (f:'prop mu) = (FV f = {})`) 216 217val IS_PROP_def = Define ` 218(IS_PROP (T:'prop mu) = T) /\ 219(IS_PROP F = T) /\ 220(IS_PROP (~f) = IS_PROP f) /\ 221(IS_PROP (f1 /\ f2) = (IS_PROP f1) /\ (IS_PROP f2)) /\ 222(IS_PROP (f1 \/ f2) = (IS_PROP f1) /\ (IS_PROP f2)) /\ 223(IS_PROP (RV Q) = F) /\ 224(IS_PROP (AP p) = T) /\ 225(IS_PROP (<<a>> f) = F) /\ 226(IS_PROP ([[a]] f) = F) /\ 227(IS_PROP (mu Q.. f) = F) /\ 228(IS_PROP (nu Q.. f) = F)` 229 230val AP_SUBST_def = Define ` 231(AP_SUBST g ap (T:'prop mu) = (T:'prop mu)) /\ 232(AP_SUBST g ap F = F) /\ 233(AP_SUBST g ap (~f) = ~(AP_SUBST g ap f)) /\ 234(AP_SUBST g ap (f1 /\ f2) = (AP_SUBST g ap f1) /\ (AP_SUBST g ap f2)) /\ 235(AP_SUBST g ap (f1 \/ f2) = (AP_SUBST g ap f1) \/ (AP_SUBST g ap f2)) /\ 236(AP_SUBST g ap (RV Q) = (RV Q)) /\ 237(AP_SUBST g ap (AP p) = if (p=ap) then g else AP p) /\ 238(AP_SUBST g ap (<<a>> f) = <<a>> (AP_SUBST g ap f)) /\ 239(AP_SUBST g ap ([[a]] f) = [[a]] (AP_SUBST g ap f)) /\ 240(AP_SUBST g ap (mu Q.. f) = (mu Q.. (AP_SUBST g ap f))) /\ 241(AP_SUBST g ap (nu Q.. f) = (nu Q.. (AP_SUBST g ap f)))` 242 243val RVNEG_SYM = store_thm("RVNEG_SYM", 244 ``!Q Q' (f:'prop mu). RVNEG Q (RVNEG Q' f) = RVNEG Q' (RVNEG Q f)``, 245 246REPEAT GEN_TAC 247THEN Induct_on `f` THEN SIMP_TAC std_ss (RVNEG_def::tsimps ``:'prop mu``) THEN 248FULL_SIMP_TAC std_ss [] THENL [ 249 PROVE_TAC [], 250 PROVE_TAC [], 251 Q.X_GEN_TAC `s` 252 THEN Cases_on `Q=Q'` THEN 253 REPEAT (Cases_on `Q'=s` THEN 254 REPEAT (Cases_on `Q=s` THEN FULL_SIMP_TAC std_ss [RVNEG_def])),(*RV*) 255 256 Q.X_GEN_TAC `s` 257 THEN Cases_on `Q=Q'` THENL [ 258 Cases_on `Q'=s` THEN REPEAT (Cases_on `Q=s` THEN 259 (FULL_SIMP_TAC std_ss [RVNEG_def] ORELSE 260 PROVE_TAC [])), 261 Cases_on `Q'=s` THENL [ 262 Cases_on `Q=s` THENL [ 263 FULL_SIMP_TAC std_ss [RVNEG_def], 264 FULL_SIMP_TAC std_ss [RVNEG_def] 265 ], 266 Cases_on `Q=s` THENL [ 267 FULL_SIMP_TAC std_ss [RVNEG_def], 268 FULL_SIMP_TAC std_ss [RVNEG_def] THEN PROVE_TAC [] 269 ] 270 ] 271 ], (* mu *) 272 273 (* nu *) 274 Q.X_GEN_TAC `s` 275 THEN Cases_on `Q=Q'` THENL [ 276 Cases_on `Q'=s` THEN 277 REPEAT (Cases_on `Q=s` THEN 278 (FULL_SIMP_TAC std_ss [RVNEG_def] ORELSE ASSUM_LIST PROVE_TAC)), 279 Cases_on `Q'=s` THENL [ 280 Cases_on `Q=s` THENL [ 281 FULL_SIMP_TAC std_ss [RVNEG_def], 282 FULL_SIMP_TAC std_ss [RVNEG_def] 283 ], 284 Cases_on `Q=s` THENL [ 285 FULL_SIMP_TAC std_ss [RVNEG_def], 286 FULL_SIMP_TAC std_ss [RVNEG_def] 287 THEN ASSUM_LIST PROVE_TAC 288 ] 289 ] 290 ] 291]) 292 293val IMF_NEG_NEG_LEM1 = save_thm("IMF_NEG_NEG_LEM1",prove(``!(f:'prop mu) Q Q'. ~(Q'=Q) ==> (~SUBFORMULA (~RV Q) (NNF (RVNEG Q' f)) = ~SUBFORMULA (~RV Q) (NNF f))``, 294recInduct NNF_IND_def THEN REPEAT CONJ_TAC THEN BETA_TAC THEN SIMP_TAC std_ss ([NNF_def,RVNEG_def,IMF_def,MU_SUB_def]@tsimps_mu) THENL [ 295REPEAT GEN_TAC THEN DISCH_TAC 296THEN FULL_SIMP_TAC std_ss ([NNF_def,RVNEG_def,IMF_def,MU_SUB_def]@tsimps_mu) 297THEN Cases_on `Q''=Q` THENL [ 298FULL_SIMP_TAC std_ss ([NNF_def,RVNEG_def,IMF_def,MU_SUB_def]@tsimps_mu), 299FULL_SIMP_TAC std_ss ([NNF_def,RVNEG_def,IMF_def,MU_SUB_def]@tsimps_mu)], 300REPEAT STRIP_TAC THEN Cases_on `Q''=Q` THENL [ 301FULL_SIMP_TAC std_ss ([NNF_def,RVNEG_def,IMF_def,MU_SUB_def]@tsimps_mu), 302FULL_SIMP_TAC std_ss ([NNF_def,RVNEG_def,IMF_def,MU_SUB_def]@tsimps_mu)], 303REPEAT STRIP_TAC THEN Cases_on `Q''=Q` THENL [ 304FULL_SIMP_TAC std_ss ([NNF_def,RVNEG_def,IMF_def,MU_SUB_def]@tsimps_mu), 305FULL_SIMP_TAC std_ss ([NNF_def,RVNEG_def,IMF_def,MU_SUB_def]@tsimps_mu)], 306REPEAT GEN_TAC THEN DISCH_TAC 307THEN FULL_SIMP_TAC std_ss ([NNF_def,RVNEG_def,IMF_def,MU_SUB_def]@tsimps_mu) 308THEN Cases_on `Q''=Q` THENL [ 309FULL_SIMP_TAC std_ss ([NNF_def,RVNEG_def,IMF_def,MU_SUB_def]@tsimps_mu), 310FULL_SIMP_TAC std_ss ([NNF_def,RVNEG_def,IMF_def,MU_SUB_def]@tsimps_mu)], 311REPEAT STRIP_TAC THEN Cases_on `Q''=Q` THENL [ 312FULL_SIMP_TAC std_ss ([NNF_def,RVNEG_def,IMF_def,MU_SUB_def]@tsimps_mu), 313FULL_SIMP_TAC std_ss ([NNF_def,RVNEG_def,IMF_def,MU_SUB_def]@tsimps_mu) 314THEN FULL_SIMP_TAC std_ss [RVNEG_SYM]], (* mu *) 315REPEAT STRIP_TAC THEN Cases_on `Q''=Q` THENL [ 316FULL_SIMP_TAC std_ss ([NNF_def,RVNEG_def,IMF_def,MU_SUB_def]@tsimps_mu), 317FULL_SIMP_TAC std_ss ([NNF_def,RVNEG_def,IMF_def,MU_SUB_def]@tsimps_mu) 318THEN FULL_SIMP_TAC std_ss [RVNEG_SYM]]])) (* nu *) 319 320val IMF_INV_RVNEG = store_thm( 321 "IMF_INV_RVNEG", 322 ``!(f: 'prop mu) Q. IMF (RVNEG Q f) = IMF f``, 323 Induct_on `f` THEN 324 FULL_SIMP_TAC std_ss ([IMF_def,MU_SUB_def,RVNEG_def]@tsimps_mu) THENL [ 325 (* RV *) 326 SRW_TAC [][IMF_def], 327 328 (* mu *) 329 MAP_EVERY Q.X_GEN_TAC [`s`, `Q`] THEN Cases_on `Q=s` THEN 330 FULL_SIMP_TAC std_ss [IMF_def,MU_SUB_def] THEN 331 FULL_SIMP_TAC std_ss [IMF_NEG_NEG_LEM1], 332 333 (* nu *) 334 MAP_EVERY Q.X_GEN_TAC [`s`, `Q`] THEN Cases_on `Q=s` THEN 335 FULL_SIMP_TAC std_ss [IMF_def,MU_SUB_def] THEN 336 FULL_SIMP_TAC std_ss [IMF_NEG_NEG_LEM1] 337 ]) 338 339val IMF_INV_NEG_RVNEG = save_thm("IMF_INV_NEG_RVNEG",prove (``!f Q. IMF (f:'prop mu) = IMF (RVNEG Q ~f)``, 340SIMP_TAC std_ss [RVNEG_def,GSYM IMF_INV_RVNEG,IMF_def])) 341 342val STATES_MONO_NEG_MU_LEM1 = save_thm("STATES_MONO_NEG_MU_LEM1",prove(``!Q' Q (f:'prop mu) . SUBFORMULA (~RV Q') (NNF ~mu Q.. f) = SUBFORMULA (~RV Q') (NNF (RVNEG Q ~f))``,SIMP_TAC std_ss ([NNF_def,MU_SUB_def]@tsimps_mu))) 343 344val STATES_MONO_LEM2 = save_thm("STATES_MONO_LEM2",prove (``!(f:'prop mu) Q Q'. ~(Q'=Q) ==> (SUBFORMULA (~RV Q') (NNF f) = SUBFORMULA (~RV Q') (NNF (RVNEG Q f)))``, 345recInduct NNF_IND_def THEN REPEAT CONJ_TAC THEN BETA_TAC THEN (SIMP_TAC std_ss ([NNF_def,MU_SUB_def,RVNEG_def]@tsimps_mu)) THENL [ 346PROVE_TAC [], (* /\ *) 347PROVE_TAC [], (* \/ *) 348REPEAT GEN_TAC THEN DISCH_TAC THEN Cases_on `Q'=Q` THENL [ 349 FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def]@tsimps_mu), 350 FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def]@tsimps_mu)], (* RV *) 351REPEAT STRIP_TAC THEN Cases_on `Q'=Q` THENL [ 352 FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def]@tsimps_mu), 353 FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def]@tsimps_mu)], (* mu *) 354REPEAT STRIP_TAC THEN Cases_on `Q'=Q` THENL [ 355 FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def]@tsimps_mu), 356 FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def]@tsimps_mu)], (* nu *) 357PROVE_TAC [], (* ~/\ *) 358PROVE_TAC [], (* ~\/ *) 359REPEAT GEN_TAC THEN DISCH_TAC THEN Cases_on `Q'=Q` THENL [ 360 FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def]@tsimps_mu), 361 FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def]@tsimps_mu)], (* ~RV *) 362REPEAT STRIP_TAC THEN Cases_on `Q'=Q` THENL [ 363 FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def]@tsimps_mu), 364 FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def]@tsimps_mu) 365 THEN FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def,RVNEG_SYM]@tsimps_mu)], (* ~ mu *) 366REPEAT STRIP_TAC THEN Cases_on `Q'=Q` THENL [ 367 FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def]@tsimps_mu), 368 FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def]@tsimps_mu) 369 THEN FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def,RVNEG_SYM]@tsimps_mu)]])) (* ~ nu *) 370 371val NNF_RVNEG_DUALITY = save_thm("NNF_RVNEG_DUALITY",prove(``!(f:'prop mu) Q. NNF (RVNEG Q (RVNEG Q f)) = NNF f``, 372recInduct NNF_IND_def THEN REPEAT CONJ_TAC THEN BETA_TAC THEN FULL_SIMP_TAC std_ss (NNF_def::MU_SUB_def::RVNEG_def::tsimps_mu) THENL [ 373REPEAT GEN_TAC THEN Cases_on `Q'=Q` THENL [ 374 FULL_SIMP_TAC std_ss (RVNEG_def::NNF_def::tsimps_mu), 375 FULL_SIMP_TAC std_ss (RVNEG_def::NNF_def::tsimps_mu)], (* RV *) 376REPEAT STRIP_TAC THEN Cases_on `Q'=Q` THENL [ 377 FULL_SIMP_TAC std_ss (RVNEG_def::NNF_def::tsimps_mu), 378 FULL_SIMP_TAC std_ss (RVNEG_def::NNF_def::tsimps_mu)], (* mu *) 379REPEAT STRIP_TAC THEN Cases_on `Q'=Q` THENL [ 380 FULL_SIMP_TAC std_ss (RVNEG_def::NNF_def::tsimps_mu), 381 FULL_SIMP_TAC std_ss (RVNEG_def::NNF_def::tsimps_mu)], (* nu *) 382REPEAT GEN_TAC THEN Cases_on `Q'=Q` THENL [ 383 FULL_SIMP_TAC std_ss (RVNEG_def::NNF_def::tsimps_mu), 384 FULL_SIMP_TAC std_ss (RVNEG_def::NNF_def::tsimps_mu)], (* ~RV *) 385REPEAT STRIP_TAC THEN Cases_on `Q'=Q` THENL [ 386 FULL_SIMP_TAC std_ss (RVNEG_def::NNF_def::tsimps_mu), 387 FULL_SIMP_TAC std_ss (RVNEG_SYM::RVNEG_def::NNF_def::tsimps_mu)], (* ~mu *) 388REPEAT STRIP_TAC THEN Cases_on `Q'=Q` THENL [ 389 FULL_SIMP_TAC std_ss (RVNEG_def::NNF_def::tsimps_mu), 390 FULL_SIMP_TAC std_ss (RVNEG_SYM::RVNEG_def::NNF_def::tsimps_mu)]])) (* ~nu *) 391 392val IMF_MU_IFF_IMF_NU=save_thm("IMF_MU_IFF_IMF_NU",prove(``!(f:'prop mu) Q. IMF (mu Q..f) = IMF (nu Q..f)``,SIMP_TAC std_ss [IMF_def])) 393 394val ALLV_RVNEG = prove(``!f Q. ALLV f = ALLV (RVNEG Q f)``, 395Induct_on `f` THEN FULL_SIMP_TAC std_ss ([UNION_DEF,SET_SPEC,RVNEG_def,ALLV_def]@tsimps_mu) THENL [ 396 ONCE_REWRITE_TAC [EXTENSION] 397 THEN FULL_SIMP_TAC std_ss [SET_SPEC] 398 THEN METIS_TAC [], 399 ONCE_REWRITE_TAC [EXTENSION] 400 THEN FULL_SIMP_TAC std_ss [SET_SPEC] 401 THEN METIS_TAC [], 402 SRW_TAC [][ALLV_def], 403 SRW_TAC [][ALLV_def], 404 SRW_TAC [][ALLV_def] 405]) 406 407val ALLV_NNF = prove(``!f. ALLV f = ALLV (NNF f)``, 408recInduct NNF_IND_def THEN REPEAT CONJ_TAC THEN BETA_TAC 409THEN FULL_SIMP_TAC std_ss ([GSYM ALLV_RVNEG,NNF_def,RVNEG_def,NOT_IN_EMPTY,MU_SUB_def,ALLV_def]@tsimps_mu)) 410 411val ALLV_SUBF = prove(``!f Q. (RV Q) SUBF f = Q IN ALLV f``, 412Induct_on `f` THEN FULL_SIMP_TAC std_ss ([IN_SING,UNION_DEF,SET_SPEC,NOT_IN_EMPTY,MU_SUB_def,ALLV_def]@tsimps_mu)) 413 414val ALLV_FINITE = prove(``!f. FINITE (ALLV f)``, 415Induct_on `f` THEN FULL_SIMP_TAC std_ss [FINITE_EMPTY,FINITE_UNION,ALLV_def,FINITE_SING]) 416 417val CLOSED_NEG = save_thm("CLOSED_NEG",prove(``!f. CLOSED (~f) = CLOSED f``,Induct_on `f` THEN FULL_SIMP_TAC std_ss ([CLOSED_def,FV_def]@tsimps_mu))) 418 419val CLOSED_AND = save_thm("CLOSED_AND",prove(``!f g. CLOSED (f /\ g) = CLOSED f /\ CLOSED g``,Induct_on `f` THEN FULL_SIMP_TAC std_ss ([CLOSED_def,FV_def,UNION_EMPTY,EMPTY_UNION]@tsimps_mu))) 420 421val CLOSED_OR = save_thm("CLOSED_OR",prove(``!f g. CLOSED (f \/ g) = CLOSED f /\ CLOSED g``,Induct_on `f` THEN FULL_SIMP_TAC std_ss ([CLOSED_def,FV_def,UNION_EMPTY,EMPTY_UNION]@tsimps_mu))) 422 423val CLOSED_AP = save_thm("CLOSED_AP",prove(``!p. CLOSED (AP p)``,FULL_SIMP_TAC std_ss ([CLOSED_def,FV_def,UNION_EMPTY,EMPTY_UNION]@tsimps_mu))) 424 425val CLOSED_BOX = save_thm("CLOSED_BOX",prove(``!f a. CLOSED ([[a]] f) = CLOSED f``,Induct_on `f` THEN FULL_SIMP_TAC std_ss ([CLOSED_def,FV_def,UNION_EMPTY,EMPTY_UNION]@tsimps_mu))) 426 427val CLOSED_DMD = save_thm("CLOSED_DMD",prove(``!f a. CLOSED (<<a>> f) = CLOSED f``,Induct_on `f` THEN FULL_SIMP_TAC std_ss ([CLOSED_def,FV_def,UNION_EMPTY,EMPTY_UNION]@tsimps_mu))) 428 429(* thms about subformulas *) 430 431val SUBF_REFL = save_thm("SUBF_REFL",prove(``!f. f SUBF f``,Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 432 433val SUBF_NEG = prove(``!f g. ~(g SUBF f) ==> ~(~g SUBF f)``, 434Induct_on `f` THEN Induct_on `g` THEN FULL_SIMP_TAC std_ss ([MU_SUB_def]@tsimps_mu) 435THEN TRY (METIS_TAC (MU_SUB_def::tsimps_mu))) 436 437val SUBF_NEG2 = prove(``!f g. (~g SUBF f) ==> (g SUBF f)``, PROVE_TAC [SUBF_NEG]) 438 439val SUBF_CONJ = save_thm("SUBF_CONJ",prove(``!f g h. (f /\ g) SUBF h ==> f SUBF h /\ g SUBF h``, 440Induct_on `h` THEN REPEAT CONJ_TAC THEN FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def]@tsimps_mu) 441THEN REPEAT STRIP_TAC THEN (FIRST_PROVE [DISJ1_TAC THEN RES_TAC,DISJ2_TAC THEN RES_TAC, DISJ2_TAC THEN DISJ1_TAC THEN RES_TAC] ORELSE ASM_REWRITE_TAC [SUBF_REFL]))) 442 443val SUBF_DISJ = save_thm("SUBF_DISJ",prove(``!f g h. (f \/ g) SUBF h ==> f SUBF h /\ g SUBF h``, 444Induct_on `h` THEN REPEAT CONJ_TAC THEN FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def]@tsimps_mu) 445THEN REPEAT STRIP_TAC THEN (FIRST_PROVE [DISJ1_TAC THEN RES_TAC,DISJ2_TAC THEN RES_TAC, DISJ2_TAC THEN DISJ1_TAC THEN RES_TAC] ORELSE ASM_REWRITE_TAC [SUBF_REFL]))) 446 447val SUBF_DMD = save_thm("SUBF_DMD",prove(``!a f h. <<a>> f SUBF h ==> f SUBF h``, 448Induct_on `h` THEN REPEAT CONJ_TAC THEN FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def]@tsimps_mu) 449THEN REPEAT STRIP_TAC THEN (FIRST_PROVE [DISJ1_TAC THEN RES_TAC,DISJ2_TAC THEN RES_TAC, DISJ2_TAC THEN DISJ1_TAC THEN RES_TAC] ORELSE ASM_REWRITE_TAC [SUBF_REFL]))) 450 451val SUBF_BOX = save_thm("SUBF_BOX",prove(``!a f h. [[a]] f SUBF h ==> f SUBF h``, 452Induct_on `h` THEN REPEAT CONJ_TAC THEN FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def]@tsimps_mu) 453THEN REPEAT STRIP_TAC THEN (FIRST_PROVE [DISJ1_TAC THEN RES_TAC,DISJ2_TAC THEN RES_TAC, DISJ2_TAC THEN DISJ1_TAC THEN RES_TAC] ORELSE ASM_REWRITE_TAC [SUBF_REFL]))) 454 455val SUBF_MU = save_thm("SUBF_MU",prove(``!Q f h. (mu Q .. f) SUBF h ==> f SUBF h``, 456Induct_on `h` THEN REPEAT CONJ_TAC THEN FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def]@tsimps_mu) 457THEN REPEAT STRIP_TAC THEN (FIRST_PROVE [DISJ1_TAC THEN RES_TAC,DISJ2_TAC THEN RES_TAC, DISJ2_TAC THEN DISJ1_TAC THEN RES_TAC] ORELSE ASM_REWRITE_TAC [SUBF_REFL]))) 458 459val SUBF_NU = save_thm("SUBF_NU",prove(``!Q f h. (nu Q .. f) SUBF h ==> f SUBF h``, 460Induct_on `h` THEN REPEAT CONJ_TAC THEN FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def]@tsimps_mu) 461THEN REPEAT STRIP_TAC THEN (FIRST_PROVE [DISJ1_TAC THEN RES_TAC,DISJ2_TAC THEN RES_TAC, DISJ2_TAC THEN DISJ1_TAC THEN RES_TAC] ORELSE ASM_REWRITE_TAC [SUBF_REFL]))) 462 463val SUB_RV_BOX = save_thm("SUB_RV_BOX",prove(``!f a Q. ~SUBFORMULA (~RV Q) ([[a]] f) = ~SUBFORMULA (~RV Q) f``, 464Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))); 465 466val SUB_RV_MU = save_thm("SUB_RV_MU",prove(``!f Q Q'. ~SUBFORMULA (~RV Q') (mu Q .. f) = ~SUBFORMULA (~RV Q') f``, 467Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))); 468 469val SUB_RV_NU = save_thm("SUB_RV_NU",prove(``!f Q Q'. ~SUBFORMULA (~RV Q') (nu Q .. f) = ~SUBFORMULA (~RV Q') f``, 470Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))); 471 472val SUB_AP_RVNEG = save_thm("SUB_AP_RVNEG",prove(``!f p Q . SUBFORMULA (AP p) f = SUBFORMULA (AP p) (RVNEG Q ~f)``, 473Induct_on `f` THEN FULL_SIMP_TAC std_ss (RVNEG_def::MU_SUB_def::tsimps_mu) 474THEN REPEAT GEN_TAC THEN (TRY EQ_TAC) THEN RW_TAC std_ss [] 475THEN FULL_SIMP_TAC std_ss (RVNEG_def::MU_SUB_def::tsimps_mu) THEN ASSUM_LIST PROVE_TAC)); 476 477val SUB_AP_NEG_MU = save_thm("SUB_AP_NEG_MU",prove(``!f p Q . SUBFORMULA (AP p) ~(mu Q.. f) = SUBFORMULA (AP p) (RVNEG Q ~f)``, 478Induct_on `f` THEN FULL_SIMP_TAC std_ss ([SUB_AP_RVNEG,NNF_def,RVNEG_def,MU_SUB_def]@tsimps_mu) 479THEN REPEAT GEN_TAC THEN (TRY EQ_TAC) THEN RW_TAC std_ss [] 480THEN FULL_SIMP_TAC std_ss (RVNEG_def::MU_SUB_def::tsimps_mu) THEN ASSUM_LIST PROVE_TAC 481)); 482 483val SUB_AP_NEG_NU = save_thm("SUB_AP_NEG_NU",prove(``!f p Q . SUBFORMULA (AP p) ~(nu Q.. f) = SUBFORMULA (AP p) (RVNEG Q ~f)``, 484Induct_on `f` THEN FULL_SIMP_TAC std_ss ([SUB_AP_RVNEG,NNF_def,RVNEG_def,MU_SUB_def]@tsimps_mu) 485THEN REPEAT GEN_TAC THEN (TRY EQ_TAC) THEN RW_TAC std_ss [] 486THEN FULL_SIMP_TAC std_ss (RVNEG_def::MU_SUB_def::tsimps_mu) THEN ASSUM_LIST PROVE_TAC 487)); 488 489val SUB_AP_NEG = save_thm("SUB_AP_NEG",prove(``!f p. SUBFORMULA (AP p) (~f) = SUBFORMULA (AP p) f``, 490Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 491 492val SUB_AP_CONJ = save_thm("SUB_AP_CONJ",prove(``!f g p. SUBFORMULA (AP p) (f /\ g) = SUBFORMULA (AP p) f \/ SUBFORMULA (AP p) g``, 493Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 494 495val SUB_AP_DISJ = save_thm("SUB_AP_DISJ",prove(``!f g p. SUBFORMULA (AP p) (f \/ g) = SUBFORMULA (AP p) f \/ SUBFORMULA (AP p) g``, 496Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 497 498val SUB_AP_BOX = save_thm("SUB_AP_BOX",prove(``!f p a. SUBFORMULA (AP p) ([[a]]f) = SUBFORMULA (AP p) f``, 499Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 500 501val SUB_AP_DMD = save_thm("SUB_AP_DMD",prove(``!f p a. SUBFORMULA (AP p) (<<a>>f) = SUBFORMULA (AP p) f``, 502Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 503 504val SUB_AP_MU = save_thm("SUB_AP_MU",prove(``!f p Q. SUBFORMULA (AP p) (mu Q .. f) = SUBFORMULA (AP p) f``, 505Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 506 507val SUB_AP_NU = save_thm("SUB_AP_NU",prove(``!f p Q. SUBFORMULA (AP p) (nu Q .. f) = SUBFORMULA (AP p) f``, 508Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 509 510val NNF_NEG = save_thm("NNF_NEG",prove (``!f. IMF f ==> !g. SUBFORMULA (~g) (NNF f) ==> (?p. (g = AP p) \/ ?Q. (g = RV Q))``, 511recInduct NNF_IND_def THEN REPEAT CONJ_TAC THEN BETA_TAC 512THEN REPEAT (RW_TAC std_ss ([IMF_def,MU_SUB_def,NNF_def,RVNEG_def,IMF_INV_RVNEG]@tsimps_mu)))) 513 514val SUB_DMD_NEG = save_thm("SUB_DMD_NEG",prove(``!f g a. ~SUBFORMULA (<<a>> g) (~f) = ~SUBFORMULA (<<a>> g) f``, 515Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 516 517val SUB_DMD_CONJ = save_thm("SUB_DMD_CONJ",prove(``!f f1 g a. ~SUBFORMULA (<<a>> g) (f /\ f1) = (~SUBFORMULA (<<a>> g) f) /\ (~SUBFORMULA (<<a>> g) f1)``, 518Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 519 520val SUB_DMD_DISJ = save_thm("SUB_DMD_DISJ",prove(``!f f1 g a. ~SUBFORMULA (<<a>> g) (f \/ f1) = (~SUBFORMULA (<<a>> g) f) /\ (~SUBFORMULA (<<a>> g) f1)``, 521Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 522 523val SUB_DMD_DMD = save_thm("SUB_DMD_DMD",prove (``!f a. ~(!a' g . ~SUBFORMULA <<a'>> g <<a>> f)``,SIMP_TAC std_ss [] THEN REPEAT GEN_TAC THEN MAP_EVERY Q.EXISTS_TAC [`a`,`f`] THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 524 525val SUB_DMD_BOX = save_thm("SUB_DMD_BOX",prove(``!f g a a'. ~SUBFORMULA (<<a>> g) ([[a']]f) = ~SUBFORMULA (<<a>> g) f``, 526Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 527 528val SUB_DMD_MU = save_thm("SUB_DMD_MU",prove(``!f g a Q. ~SUBFORMULA (<<a>> g) (mu Q .. f) = ~SUBFORMULA (<<a>> g) f``, 529Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 530 531val SUB_DMD_NU = save_thm("SUB_DMD_NU",prove(``!f g a Q. ~SUBFORMULA (<<a>> g) (nu Q .. f) = ~SUBFORMULA (<<a>> g) f``, 532Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 533 534val SUB_AP_NEG_CONJ = save_thm("SUB_AP_NEG_CONJ",prove(``!f g p. SUBFORMULA (AP p) ~(f /\ g) = SUBFORMULA (AP p) ~f \/ SUBFORMULA (AP p) ~g``, 535Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 536 537val SUB_AP_NEG_DISJ = save_thm("SUB_AP_NEG_DISJ",prove(``!f g p. SUBFORMULA (AP p) ~(f \/ g) = SUBFORMULA (AP p) ~f \/ SUBFORMULA (AP p) ~g``, 538Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 539 540val SUB_AP_NEG_DMD = save_thm("SUB_AP_NEG_DMD",prove(``!f p a. SUBFORMULA (AP p) ~(<<a>>f) = SUBFORMULA (AP p) ~f``, 541Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 542 543val SUB_AP_NEG_NEG = save_thm("SUB_AP_NEG_NEG",prove(``!f p. SUBFORMULA (AP p) (~~f) = SUBFORMULA (AP p) f``, 544Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 545 546val SUB_DMD_NEG_CONJ = save_thm("SUB_DMD_NEG_CONJ",prove(``!f f1 g a. ~SUBFORMULA (<<a>> g) ~(f /\ f1) = (~SUBFORMULA (<<a>> g) ~f) /\ (~SUBFORMULA (<<a>> g) ~f1)``,Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 547 548val SUB_DMD_NEG_DISJ = save_thm("SUB_DMD_NEG_DISJ",prove(``!f f1 g a. ~SUBFORMULA (<<a>> g) ~(f \/ f1) = (~SUBFORMULA (<<a>> g) ~f) /\ (~SUBFORMULA (<<a>> g) ~f1)``,Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 549 550val SUB_DMD_NEG_DMD = save_thm("SUB_DMD_NEG_DMD",prove(``!f a. (!a' g. ~SUBFORMULA (<<a'>> g) ~(<<a>>f)) ==> !a' g. ~SUBFORMULA (<<a'>> g) ~f``, 551Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 552 553val SUB_DMD_NEG_NEG = save_thm("SUB_DMD_NEG_NEG",prove(``!f g a. ~SUBFORMULA (<<a>> g) (~~f) = ~SUBFORMULA (<<a>> g) f``, 554Induct_on `f` THEN SIMP_TAC std_ss (MU_SUB_def::tsimps_mu))) 555 556 557val STATES_MONO_LEM3 = save_thm("STATES_MONO_LEM3",prove(``!(f:'prop mu) Q. ~SUBFORMULA (~RV Q) (NNF f) = ~SUBFORMULA (~RV Q) (NNF (RVNEG Q ~f))``, 558recInduct NNF_IND_def THEN REPEAT CONJ_TAC THEN BETA_TAC THEN SIMP_TAC std_ss ([NNF_def,MU_SUB_def,RVNEG_def]@tsimps_mu) THENL [ 559REPEAT GEN_TAC THEN Cases_on `Q'=Q` THENL [ 560 FULL_SIMP_TAC std_ss [MU_SUB_def,NNF_def] 561 THEN FULL_SIMP_TAC std_ss tsimps_mu, 562 FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def]@ tsimps_mu)], (* RV *) 563REPEAT STRIP_TAC THEN Cases_on `Q'=Q` THENL [ 564 FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def]@ tsimps_mu), 565 FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def]@ tsimps_mu) 566 THEN FULL_SIMP_TAC std_ss [SIMP_RULE std_ss [RVNEG_def] (SPECL[``~RVNEG Q' (f:'prop mu)``,``Q:string``,``Q':string``] 567 STATES_MONO_LEM2)]], (* mu *) 568REPEAT STRIP_TAC THEN Cases_on `Q'=Q` THENL [ 569 FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def]@ tsimps_mu), 570 FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def]@ tsimps_mu) 571 THEN FULL_SIMP_TAC std_ss [SIMP_RULE std_ss [RVNEG_def] (SPECL[``~RVNEG Q' (f:'prop mu)``,``Q:string``,``Q':string``] 572 STATES_MONO_LEM2)]], (* nu *) 573REPEAT GEN_TAC THEN Cases_on `Q'=Q` THENL [ 574 FULL_SIMP_TAC std_ss [MU_SUB_def,NNF_def] 575 THEN FULL_SIMP_TAC std_ss tsimps_mu, 576 FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def]@ tsimps_mu)], (* ~RV *) 577REPEAT STRIP_TAC THEN Cases_on `Q'=Q` THENL [ 578 FULL_SIMP_TAC std_ss ([NNF_RVNEG_DUALITY,MU_SUB_def,NNF_def,RVNEG_def]@ tsimps_mu), 579 FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def]@ tsimps_mu) 580 THEN SIMP_TAC std_ss [RVNEG_SYM] 581 THEN PROVE_TAC [SIMP_RULE std_ss [RVNEG_def] (SPECL[``RVNEG Q' (f:'prop mu)``,``Q:string``,``Q':string``] 582 STATES_MONO_LEM2)]], (* ~mu *) 583REPEAT STRIP_TAC THEN Cases_on `Q'=Q` THENL [ 584 FULL_SIMP_TAC std_ss ([NNF_RVNEG_DUALITY,MU_SUB_def,NNF_def,RVNEG_def]@ tsimps_mu), 585 FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def]@ tsimps_mu) 586 THEN SIMP_TAC std_ss [RVNEG_SYM] 587 THEN PROVE_TAC [SIMP_RULE std_ss [RVNEG_def] (SPECL[``RVNEG Q' (f:'prop mu)``,``Q:string``,``Q':string``] 588 STATES_MONO_LEM2)]]])) (* ~nu *) 589 590val STATES_MONO_LEM6 = save_thm("STATES_MONO_LEM6",prove (``!Q Q' (f:'prop mu). SUBFORMULA (~RV Q') (NNF mu Q.. f) = SUBFORMULA (~RV Q') (NNF f)``,FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def]@ tsimps_mu))) 591 592val STATES_MONO_LEM11 = save_thm("STATES_MONO_LEM11",prove(``!Q Q' (f:'prop mu). SUBFORMULA (~RV Q') (NNF nu Q.. f) = SUBFORMULA (~RV Q') (NNF f)``,FULL_SIMP_TAC std_ss ([MU_SUB_def,NNF_def]@ tsimps_mu))) 593 594 595val STATES_MONO_LEM8 = save_thm("STATES_MONO_LEM8",prove(``!Q. ~SUBFORMULA (~RV Q) (NNF (RV:(string -> 'prop mu) Q))``,SIMP_TAC std_ss ([MU_SUB_def,NNF_def]@tsimps_mu))) 596 597val STATES_MONO_LEM9 = save_thm("STATES_MONO_LEM9",prove(``!Q. SUBFORMULA (~RV Q) (NNF (~(RV:(string -> 'prop mu)) Q))``,SIMP_TAC std_ss ([MU_SUB_def,NNF_def]@tsimps_mu))) 598 599(* thms about IMF *) 600 601val NNF_IDEM = save_thm("NNF_IDEM",prove(``!f. NNF (NNF f) = NNF f``,recInduct NNF_IND_def THEN REPEAT CONJ_TAC THEN SIMP_TAC std_ss (NNF_def::MU_SUB_def::tsimps_mu) THEN ASSUM_LIST (fn l => TRY (PROVE_TAC l)))) 602 603val IMF_NNF = save_thm("IMF_NNF",prove(``!f. IMF f = IMF (NNF f)``, 604recInduct NNF_IND_def THEN REPEAT CONJ_TAC THEN SIMP_TAC std_ss (NNF_IDEM::IMF_def::MU_SUB_def::NNF_def::tsimps_mu) THEN 605RW_TAC std_ss [] THEN PROVE_TAC [STATES_MONO_LEM3,IMF_INV_NEG_RVNEG])) 606 607val IMF_MU_NNF = save_thm("IMF_MU_NNF",prove(``!f Q. IMF (mu Q .. f) = IMF (mu Q .. NNF f)``, 608REWRITE_TAC [IMF_def] THEN PROVE_TAC [NNF_IDEM,IMF_NNF])) 609 610 611val IMF_MU_CONJ = save_thm("IMF_MU_CONJ",prove(``!f g Q. IMF (mu Q.. f /\ g) = IMF (mu Q .. f) /\ IMF (mu Q .. g)``,SIMP_TAC std_ss [IMF_def] THEN Induct_on `f` THEN SIMP_TAC std_ss (IMF_def::MU_SUB_def::NNF_def::tsimps_mu) THEN ASSUM_LIST PROVE_TAC)) 612 613val IMF_MU_NEG_CONJ = save_thm("IMF_MU_NEG_CONJ",prove(``!f g Q. IMF (mu Q.. ~(f /\ g)) = IMF (mu Q .. ~f) /\ IMF (mu Q .. ~g)``,SIMP_TAC std_ss [IMF_def] THEN Induct_on `f` THEN SIMP_TAC std_ss (IMF_def::MU_SUB_def::NNF_def::tsimps_mu) THEN ASSUM_LIST PROVE_TAC)) 614 615val IMF_MU_DISJ = save_thm("IMF_MU_DISJ",prove(``!f g Q. IMF (mu Q.. f \/ g) = IMF (mu Q .. f) /\ IMF (mu Q .. g)``,SIMP_TAC std_ss [IMF_def] THEN Induct_on `f` THEN SIMP_TAC std_ss (IMF_def::MU_SUB_def::NNF_def::tsimps_mu) THEN ASSUM_LIST PROVE_TAC)) 616 617val IMF_MU_NEG_DISJ = save_thm("IMF_MU_NEG_DISJ",prove(``!f g Q. IMF (mu Q.. ~(f \/ g)) = IMF (mu Q .. ~f) /\ IMF (mu Q .. ~g)``,SIMP_TAC std_ss [IMF_def] THEN Induct_on `f` THEN SIMP_TAC std_ss (IMF_def::MU_SUB_def::NNF_def::tsimps_mu) THEN ASSUM_LIST PROVE_TAC)) 618 619val IMF_MU_DMD = save_thm("IMF_MU_DMD",prove(``!f a Q. IMF (mu Q.. <<a>> f ) = IMF (mu Q .. f)``,SIMP_TAC std_ss [IMF_def] THEN Induct_on `f` THEN SIMP_TAC std_ss (IMF_def::MU_SUB_def::NNF_def::tsimps_mu) THEN ASSUM_LIST PROVE_TAC)) 620 621val IMF_MU_NEG_DMD = save_thm("IMF_MU_NEG_DMD",prove(``!f a Q. IMF (mu Q.. ~<<a>> f ) = IMF (mu Q .. ~f)``,SIMP_TAC std_ss [IMF_def] THEN Induct_on `f` THEN SIMP_TAC std_ss (IMF_def::MU_SUB_def::NNF_def::tsimps_mu) THEN ASSUM_LIST PROVE_TAC)) 622 623val IMF_MU_BOX = save_thm("IMF_MU_BOX",prove(``!f a Q. IMF (mu Q.. [[a]] f) = IMF (mu Q .. f)``,SIMP_TAC std_ss [IMF_def] THEN Induct_on `f` THEN SIMP_TAC std_ss (IMF_def::MU_SUB_def::NNF_def::tsimps_mu) THEN ASSUM_LIST PROVE_TAC)) 624 625val IMF_MU_NEG_BOX = save_thm("IMF_MU_NEG_BOX",prove(``!f a Q. IMF (mu Q.. ~[[a]] f) = IMF (mu Q .. ~f)``,SIMP_TAC std_ss [IMF_def] THEN Induct_on `f` THEN SIMP_TAC std_ss (IMF_def::MU_SUB_def::NNF_def::tsimps_mu) THEN ASSUM_LIST PROVE_TAC)) 626 627val IMF_MU_MU = save_thm("IMF_MU_MU",prove(``!f Q Q'. IMF (mu Q.. mu Q' .. f) ==> IMF (mu Q' .. f)``,SIMP_TAC std_ss [IMF_def] THEN recInduct NNF_IND_def THEN REPEAT CONJ_TAC THEN SIMP_TAC std_ss (IMF_def::MU_SUB_def::NNF_def::tsimps_mu) THEN ASSUM_LIST (fn l => TRY (PROVE_TAC l)))) 628 629val IMF_MU_NEG_MU = save_thm("IMF_MU_NEG_MU",prove(``!f Q Q'. IMF (mu Q.. ~mu Q' .. f) ==> IMF (mu Q' .. f)``,SIMP_TAC std_ss [IMF_def] THEN recInduct NNF_IND_def THEN REPEAT CONJ_TAC THEN SIMP_TAC std_ss (IMF_def::MU_SUB_def::NNF_def::tsimps_mu) THEN ASSUM_LIST (fn l => TRY (PROVE_TAC l)))) 630 631val IMF_MU_NU = save_thm("IMF_MU_NU",prove(``!f Q Q'. IMF (mu Q.. nu Q' .. f) ==> IMF (mu Q' .. f)``,SIMP_TAC std_ss [IMF_def] THEN recInduct NNF_IND_def THEN REPEAT CONJ_TAC THEN SIMP_TAC std_ss (IMF_def::MU_SUB_def::NNF_def::tsimps_mu) THEN ASSUM_LIST (fn l => TRY (PROVE_TAC l)))) 632 633val IMF_MU_NEG_NU = save_thm("IMF_MU_NEG_NU",prove(``!f Q Q'. IMF (mu Q.. ~nu Q' .. f) ==> IMF (mu Q' .. f)``,SIMP_TAC std_ss [IMF_def] THEN recInduct NNF_IND_def THEN REPEAT CONJ_TAC THEN SIMP_TAC std_ss (IMF_def::MU_SUB_def::NNF_def::tsimps_mu) THEN ASSUM_LIST (fn l => TRY (PROVE_TAC l)))) 634 635val IMF_MU_NEG_NEG = save_thm("IMF_MU_NEG_NEG",prove(``!f a Q. IMF (mu Q.. ~~f) = IMF (mu Q .. f)``,SIMP_TAC std_ss [IMF_def] THEN Induct_on `f` THEN SIMP_TAC std_ss (IMF_def::MU_SUB_def::NNF_def::tsimps_mu) THEN ASSUM_LIST PROVE_TAC)) 636 637val IMF_MU_INV_RVNEG = save_thm("IMF_MU_INV_RVNEG",prove(``!f Q. IMF (mu Q.. f) = IMF mu Q.. RVNEG Q ~f``, REWRITE_TAC [IMF_def] THEN PROVE_TAC[STATES_MONO_LEM3,IMF_INV_NEG_RVNEG])) 638 639val IMF_MU_EXT = save_thm("IMF_MU_EXT",prove(``!f. IMF f ==> ?Q. IMF (mu Q..f)``, 640REPEAT STRIP_TAC 641THEN FULL_SIMP_TAC std_ss [IMF_def] 642THEN Q.EXISTS_TAC `@Q. ~(Q IN ALLV (NNF f))` 643THEN SELECT_ELIM_TAC 644THEN CONJ_TAC THENL [ 645 POP_ASSUM (K ALL_TAC) 646 THEN REWRITE_TAC [GSYM ALLV_NNF] 647 THEN METIS_TAC [NOT_IN_FIN_STRING_SET,ALLV_FINITE], 648 REPEAT STRIP_TAC 649 THEN IMP_RES_TAC SUBF_NEG2 650 THEN METIS_TAC [ALLV_SUBF,ALLV_NNF] 651])) 652 653val _ = export_theory() 654