1(* app load ["envTheory","setLemmasTheory","res_quanLib","stringLib","pred_setLib","ksTheory"] *) 2 3open HolKernel Parse boolLib bossLib 4 5val _ = new_theory "ctl"; 6 7open pairTheory; 8open pairLib; 9open pairTools; 10open pairSyntax; 11open PairRules; 12open pred_setTheory; 13open pred_setLib; 14open stringLib; 15open listTheory; 16open simpLib; 17open stringTheory; 18open sumTheory; 19open ksTheory; 20open numLib; 21open setLemmasTheory; 22open res_quanLib 23open envTheory 24 25val _ = numLib.prefer_num(); 26 27(* Most of this is cannibalised from MJCG's old Sugar2 theories *) 28 29(****************************************************************************** 30* Boolean expressions 31******************************************************************************) 32val bexp_def = 33 Hol_datatype 34 `bexp = B_TRUE (* truth *) 35 | B_PROP of 'a (* atomic proposition *) 36 | B_NOT of bexp (* negation *) 37 | B_AND of bexp # bexp`; (* conjunction *) 38 39(****************************************************************************** 40* Definition of disjunction 41******************************************************************************) 42 43val B_OR_def = 44 Define `B_OR(b1,b2) = B_NOT(B_AND(B_NOT b1, B_NOT b2))`; 45 46(****************************************************************************** 47* Definition of falsity 48******************************************************************************) 49 50val B_FALSE_def = 51 Define `B_FALSE = B_NOT B_TRUE`; 52 53 54(****************************************************************************** 55* Formulas of Sugar Optional Branching Extension (CTL) 56******************************************************************************) 57val ctl_def = 58 Hol_datatype 59 `ctl = C_BOOL of 'a bexp (* boolean expression *) 60 | C_NOT of ctl (* \neg f *) 61 | C_AND of ctl # ctl (* f1 \wedge f2 *) 62 | C_EX of ctl (* EX f *) 63 | C_EU of ctl # ctl (* E[f1 U f2] *) 64 | C_EG of ctl`; (* EG f *) 65 66(****************************************************************************** 67* ``: ('prop,'state)kripke_structure`` 68******************************************************************************) 69val kripke_structure_def = 70 Hol_datatype 71 `kripke_structure = 72 <| S: 'state -> bool; 73 S0:'state -> bool; 74 R: 'state # 'state -> bool; 75 P: 'prop -> bool; 76 L: 'state -> ('prop -> bool) |>`; 77 78(****************************************************************************** 79* B_SEM l b means "l |= b" where l is a letter, i.e. l : 'prop -> bool 80******************************************************************************) 81val B_SEM_def = 82 Define 83 `(B_SEM l B_TRUE = T) 84 /\ 85 (B_SEM l (B_PROP(p:'prop)) = p IN l) 86 /\ 87 (B_SEM l (B_NOT b) = ~(B_SEM l b)) 88 /\ 89 (B_SEM l (B_AND(b1,b2)) = B_SEM l b1 /\ B_SEM l b2)`; 90 91(****************************************************************************** 92* A path is finite or infinite 93******************************************************************************) 94val path_def = 95 Hol_datatype 96 `path = FINITE of ('s list) 97 | INFINITE of (num -> 's)`; 98 99(****************************************************************************** 100* Tests 101******************************************************************************) 102val IS_FINITE_def = 103 Define `(IS_FINITE(FINITE p) = T) 104 /\ 105 (IS_FINITE(INFINITE f) = F)`; 106 107val IS_INFINITE_def = 108 Define `(IS_INFINITE(FINITE p) = F) 109 /\ 110 (IS_INFINITE(INFINITE f) = T)`; 111 112(****************************************************************************** 113* HEAD (p0 p1 p2 p3 ...) = p0 114******************************************************************************) 115val HEAD_def = 116 Define `(HEAD (FINITE p) = HD p) 117 /\ 118 (HEAD (INFINITE f) = f 0)`; 119 120(****************************************************************************** 121* REST (p0 p1 p2 p3 ...) = (p1 p2 p3 ...) 122******************************************************************************) 123val REST_def = 124 Define `(REST (FINITE p) = FINITE(TL p)) 125 /\ 126 (REST (INFINITE f) = INFINITE(\n. f(n+1)))`; 127 128(****************************************************************************** 129* RESTN (p0 p1 p2 p3 ...) n = (pn p(n+1) p(n+2) ...) 130******************************************************************************) 131val RESTN_def = 132 Define `(RESTN p 0 = p) /\ (RESTN p (SUC n) = RESTN (REST p) n)`; 133 134(****************************************************************************** 135* Simple properties 136******************************************************************************) 137val NOT_IS_INFINITE = 138 store_thm 139 ("NOT_IS_INFINITE", 140 ``IS_INFINITE p = ~(IS_FINITE p)``, 141 Cases_on `p` 142 THEN RW_TAC std_ss [IS_INFINITE_def,IS_FINITE_def]); 143 144val NOT_IS_FINITE = 145 store_thm 146 ("NOT_IS_FINITE", 147 ``IS_FINITE p = ~(IS_INFINITE p)``, 148 Cases_on `p` 149 THEN RW_TAC std_ss [IS_INFINITE_def,IS_FINITE_def]); 150 151val IS_INFINITE_REST = 152 store_thm 153 ("IS_INFINITE_REST", 154 ``!p. IS_INFINITE(REST p) = IS_INFINITE p``, 155 Induct 156 THEN RW_TAC list_ss [REST_def,IS_INFINITE_def,IS_FINITE_def]); 157 158val IS_INFINITE_RESTN = 159 store_thm 160 ("IS_INFINITE_RESTN", 161 ``!n p. IS_INFINITE(RESTN p n) = IS_INFINITE p``, 162 Induct 163 THEN RW_TAC list_ss [RESTN_def,IS_INFINITE_REST]); 164 165val IS_FINITE_REST = 166 store_thm 167 ("IS_FINITE_REST", 168 ``!p. IS_FINITE(REST p) = IS_FINITE p``, 169 Induct 170 THEN RW_TAC list_ss [REST_def,IS_INFINITE_def,IS_FINITE_def]); 171 172val IS_FINITE_RESTN = 173 store_thm 174 ("IS_FINITE_RESTN", 175 ``!n p. IS_FINITE(RESTN p n) = IS_FINITE p``, 176 Induct 177 THEN RW_TAC list_ss [RESTN_def,IS_FINITE_REST]); 178 179val FINITE_TL = 180 store_thm 181 ("FINITE_TL", 182 ``!l. 0 < LENGTH l ==> (FINITE(TL l) = REST(FINITE l))``, 183 Induct 184 THEN RW_TAC list_ss [REST_def]); 185 186(****************************************************************************** 187* LENGTH(FINITE l) = LENGTH l 188* LENGTH is not specified on infinite paths, but LEN (defined below) is. 189******************************************************************************) 190(*val LENGTH_def = 191 Define `LENGTH (FINITE l) = list$LENGTH l`;*) 192 193(****************************************************************************** 194* ELEM (p0 p1 p2 p3 ...) n = pn 195******************************************************************************) 196val ELEM_def = Define `ELEM p n = HEAD(RESTN p n)`; 197 198(****************************************************************************** 199* Extended numbers. 200******************************************************************************) 201val xnum_def = 202 Hol_datatype 203 `xnum = INFINITY (* length of an infinite path *) 204 | XNUM of num`; (* length of a finite path *) 205 206(****************************************************************************** 207* The constant ``to`` is a left associative infix with precedence 500. 208* It is overloaded so that 209* (m to n) i means m <= i /\ i < n (num_to_def) 210* (m to XNUM n) i means m <= i /\ i < n (xnum_to_def) 211* (m to INFINITY) i means m <= i (xnum_to_def) 212******************************************************************************) 213val num_to_def = 214 Define `$num_to m n i = m <= i /\ i < n`; 215 216val xnum_to_def = 217 Define 218 `($xnum_to m (XNUM n) i = m <= i /\ i < n) 219 /\ 220 ($xnum_to m INFINITY i = m <= i)`; 221 222val _ = overload_on("to", ``num_to``); 223val _ = overload_on("to", ``xnum_to``); 224 225val _ = set_fixity "to" (Infixl 500); 226 227(****************************************************************************** 228* Extend subtraction (-) to extended numbers 229******************************************************************************) 230val SUB_num_xnum_def = 231 Define 232 `$SUB_num_xnum (m:num) (XNUM (n:num)) = XNUM((m:num) - (n:num)) `; 233 234val SUB_xnum_num_def = 235 Define `$SUB_xnum_num (XNUM (m:num)) (n:num) = XNUM((m:num) - (n:num))`; 236 237val SUB_xnum_xnum_def = 238 Define 239 `($SUB_xnum_xnum (XNUM (m:num)) (XNUM (n:num)) = XNUM((m:num) - (n:num))) 240 /\ 241 ($SUB_xnum_xnum INFINITY (XNUM (n:num)) = INFINITY)`; 242 243val SUB = 244 save_thm 245 ("SUB", 246 LIST_CONJ(type_rws ``:xnum`` @ 247 [SUB_num_xnum_def,SUB_xnum_num_def,SUB_xnum_xnum_def])); 248 249val _ = overload_on("-", ``SUB_num_xnum``); 250val _ = overload_on("-", ``SUB_xnum_num``); 251val _ = overload_on("-", ``SUB_xnum_xnum``); 252 253(****************************************************************************** 254* Extend less-than predicate (<) to extended numbers 255******************************************************************************) 256val LS_num_xnum_def = 257 Define 258 `($LS_num_xnum (m:num) (XNUM (n:num)) = (m:num) < (n:num)) 259 /\ 260 ($LS_num_xnum (m:num) INFINITY = T)`; 261 262val LS_xnum_num_def = 263 Define 264 `($LS_xnum_num (XNUM (m:num)) (n:num) = (m:num) < (n:num)) 265 /\ 266 ($LS_xnum_num INFINITY (n:num) = F)`; 267 268val LS_xnum_xnum_def = 269 Define `$LS_xnum_xnum (XNUM (m:num)) (XNUM (n:num)) = (m:num) < (n:num)`; 270 271val LS = 272 save_thm("LS",LIST_CONJ[LS_num_xnum_def,LS_xnum_num_def,LS_xnum_xnum_def]); 273 274val _ = overload_on("<", ``LS_num_xnum``); 275val _ = overload_on("<", ``LS_xnum_num``); 276val _ = overload_on("<", ``LS_xnum_xnum``); 277 278(****************************************************************************** 279* Extend greater-than predicate (>) to extended numbers 280******************************************************************************) 281val GT_num_xnum_def = 282 Define `$GT_num_xnum (m:num) (XNUM (n:num)) = (m:num) > (n:num)`; 283 284val GT_num_xnum_def = 285 Define 286 `($GT_num_xnum (m:num) (XNUM (n:num)) = (m:num) > (n:num)) 287 /\ 288 ($GT_num_xnum (m:num) INFINITY = F)`; 289 290val GT_xnum_num_def = 291 Define 292 `($GT_xnum_num (XNUM (m:num)) (n:num) = (m:num) > (n:num)) 293 /\ 294 ($GT_xnum_num INFINITY (n:num) = T)`; 295 296val GT_xnum_xnum_def = 297 Define `$GT_xnum_xnum (XNUM (m:num)) (XNUM (n:num)) = (m:num) > (n:num)`; 298 299val GT = 300 save_thm("GT",LIST_CONJ[GT_num_xnum_def,GT_xnum_num_def,GT_xnum_xnum_def]); 301 302val _ = overload_on(">", ``GT_num_xnum``); 303val _ = overload_on(">", ``GT_xnum_num``); 304val _ = overload_on(">", ``GT_xnum_xnum``); 305 306(****************************************************************************** 307* PLENGTH(FINITE l) = XNUM(LENGTH l) 308* PLENGTH(INFINITE l) = INFINITY 309******************************************************************************) 310val PLENGTH_def = 311 Define `(PLENGTH(FINITE l) = XNUM(list$LENGTH l)) 312 /\ 313 (PLENGTH(INFINITE p) = INFINITY)`; 314 315(*val PATH_LENGTH = save_thm("PATH_LENGTH",LENGTH_def);*) 316 317val ALL_IN_INF = save_thm("ALL_IN_INF",prove(``!j. j IN 0 to INFINITY``, SIMP_TAC arith_ss [IN_DEF,xnum_to_def])); 318 319(****************************************************************************** 320* PATH M p is true iff p is a path with respect to transition relation M.R 321******************************************************************************) 322val PATH_def = Define `PATH M p s = IS_INFINITE p /\ (ELEM p 0 = s) /\ (!n. M.R(ELEM p n, ELEM p (n+1)))`; 323 324val PATH_INF = save_thm("PATH_INF",prove(``!M p s. PATH M p s ==> (PLENGTH p = INFINITY)``, 325Induct_on `p` THEN 326SIMP_TAC std_ss [IS_FINITE_def,PATH_def,IS_INFINITE_def,PLENGTH_def])); 327 328val ALL_IN_INF_PATH = save_thm("ALL_IN_INF_PATH",prove(``!M p s j. PATH M p s ==> j IN 0 to PLENGTH p``, 329Induct_on `p` 330THENL [ 331 SIMP_TAC arith_ss [PATH_def,IS_INFINITE_def], 332 SIMP_TAC std_ss [ALL_IN_INF,PLENGTH_def] 333])); 334 335(****************************************************************************** 336* C_SEM M s f means "M, s |= f" 337* The mutual recursion is not necessary here, but makes fCTL defs easier 338******************************************************************************) 339val csem_eqns as [CEG_def, CEU_def, CEX_def,C_SEM_def_aux] = 340 TotalDefn.multiDefine 341 `(C_SEM M (C_BOOL b) s = B_SEM (M.L s) b) /\ 342 (C_SEM M (C_NOT f) s = ~(C_SEM M f s)) /\ 343 (C_SEM M (C_AND(f1,f2)) s = C_SEM M f1 s /\ C_SEM M f2 s) /\ 344 (C_SEM M (C_EX f) s = CEX M (C_SEM M f) s) /\ 345 (C_SEM M (C_EU(f1,f2)) s = CEU M (C_SEM M f1, C_SEM M f2) s) /\ 346 (C_SEM M (C_EG f) s = CEG M (C_SEM M f) s) /\ 347 (CEX M X s = ?p. PATH M p s /\ (ELEM p 1) IN X) /\ 348 (CEU M (X1,X2) s = ?p. PATH M p s /\ ?k :: (0 to PLENGTH p). (ELEM p k) IN X2 /\ !j. j < k ==> (ELEM p j) IN X1) /\ 349 (CEG M X s = ?p. PATH M p s /\ !j :: (0 to PLENGTH p). (ELEM p j) IN X) 350`; 351 352val C_SEM_def = save_thm("C_SEM_def",LIST_CONJ csem_eqns); 353 354val CTL_MODEL_SAT_def = Define `CTL_MODEL_SAT M f = (!s. s IN M.S0 ==> C_SEM M f s)` 355 356val C_AX_def = Define `C_AX (f: 'prop ctl) = C_NOT (C_EX (C_NOT f))`; 357val C_EF_def = Define `C_EF (f: 'prop ctl) = C_EU(C_BOOL B_TRUE,f)`; 358val C_AF_def = Define `C_AF (f: 'prop ctl) = C_NOT(C_EG (C_NOT f))`; 359val C_AG_def = Define `C_AG (f: 'prop ctl) = C_NOT (C_EF (C_NOT f))`; 360val C_AU_def = Define `C_AU ((f1: 'prop ctl),(f2: 'prop ctl)) = C_AND(C_NOT(C_EU(C_NOT f2,C_AND(C_NOT f1,C_NOT f2))),C_NOT(C_EG(C_NOT f2)))`; 361val C_AR_def = Define `C_AR(f,g) = C_NOT (C_EU (C_NOT f,C_NOT g))`; 362val C_OR_def = Define `C_OR((f1: 'prop ctl),(f2: 'prop ctl)) = C_NOT(C_AND(C_NOT f1, C_NOT f2))`; 363val C_IMP_def = Define `C_IMP((f: 'prop ctl),(g: 'prop ctl)) = C_OR(C_NOT f,g)`; 364val C_IFF_def = Define `C_IFF (f: 'prop ctl) (g: 'prop ctl) = C_AND(C_IMP(f,g),C_IMP(g,f))`; 365val B_IMP_def = Define `B_IMP((f: 'a bexp),(g: 'a bexp)) = B_OR(B_NOT f,g)`; 366val B_IFF_def = Define `B_IFF (f: 'a bexp) (g: 'a bexp) = B_AND(B_IMP(f,g),B_IMP(g,f))`; 367val B_AND2_def = Define `B_AND2 (f: 'a bexp) (g: 'a bexp) = B_AND(f,g)`; 368val B_OR2_def = Define `B_OR2 (f: 'a bexp) (g: 'a bexp) = B_OR(f,g)`; 369val C_AND2_def = Define `C_AND2 (f: 'prop ctl) (g: 'prop ctl) = C_AND(f,g)`; 370val C_OR2_def = Define `C_OR2 (f: 'prop ctl) (g: 'prop ctl) = C_OR(f,g)`; 371val C_IMP2_def = Define `C_IMP2 (f: 'prop ctl) (g: 'prop ctl) = C_IMP(f,g)`; 372val B_IMP2_def = Define `B_IMP2 (f: 'a bexp) (g: 'a bexp) = B_IMP(f,g)`; 373 374val _ = overload_on ("~", mk_const("~",Type`:bool -> bool`)); 375val _ = overload_on ("~", (Term`C_NOT`)); 376val _ = overload_on ("~", (Term`B_NOT`)); 377val _ = overload_on ("~", mk_const("~",Type`:bool -> bool`)); 378fun prepOverload s = overload_on (s, mk_const(s,Type`:bool -> bool -> bool`)); 379val _ = app prepOverload ["/\\", "\\/","==>"]; 380val _ = overload_on ("/\\", (Term `C_AND2`)); val _ = prepOverload "/\\"; 381val _ = overload_on ("\\/", (Term `C_OR2`)); val _ = prepOverload "\\/"; 382val _ = overload_on ("/\\", (Term `B_AND2`)); val _ = prepOverload "/\\"; 383val _ = overload_on ("\\/", (Term `B_OR2`)); val _ = prepOverload "\\/"; 384val _ = overload_on ("==>", (Term `C_IMP2`)); val _ = prepOverload "==>"; 385val _ = overload_on ("==>", (Term `B_IMP2`)); val _ = prepOverload "==>"; 386val _ = overload_on ("=", (Term `C_IFF`)); val _ = prepOverload "="; 387val _ = overload_on ("=", (Term `B_IFF`)); val _ = prepOverload "="; 388val _ = overload_on ("T",Term`T:bool`); val _ = overload_on ("T",Term`B_TRUE`); val _ = overload_on ("T",Term`T:bool`); 389val _ = overload_on ("F",Term`F:bool`); val _ = overload_on ("F",Term`B_FALSE`); val _ = overload_on ("F",Term`F:bool`); 390 391(* FIXME: these NNF defs are not right because they do not move all negs inwards to atoms (because OR is defined in terms of AND, etc)*) 392val BEXP_NNF = Define ` 393(BEXP_NNF B_TRUE = B_TRUE) /\ 394(BEXP_NNF (B_PROP p) = B_PROP p) /\ 395(BEXP_NNF (B_AND(b1,b2)) = B_AND(BEXP_NNF b1,BEXP_NNF b2)) /\ 396(BEXP_NNF (B_NOT B_TRUE) = B_FALSE) /\ 397(BEXP_NNF (B_NOT (B_PROP p)) = B_NOT (B_PROP p)) /\ 398(BEXP_NNF (B_NOT (B_NOT b)) = BEXP_NNF b) /\ 399(BEXP_NNF (B_NOT (B_AND(b1,b2)))= B_OR(BEXP_NNF (B_NOT b1),BEXP_NNF (B_NOT b2)))` 400 401val CTL_NNF = Define ` 402(CTL_NNF (C_BOOL b) = C_BOOL b) /\ 403(CTL_NNF (C_AND(f,g)) = C_AND(CTL_NNF f,CTL_NNF g)) /\ 404(CTL_NNF (C_EX f) = C_EX (CTL_NNF f)) /\ 405(CTL_NNF (C_EG f) = C_EG (CTL_NNF f)) /\ 406(CTL_NNF (C_EU(f,g)) = C_EU (CTL_NNF f,CTL_NNF g)) /\ 407(CTL_NNF (C_NOT (C_BOOL b)) = (C_BOOL (BEXP_NNF (B_NOT b)))) /\ 408(CTL_NNF (C_NOT (C_AND(f,g))) = (C_OR(CTL_NNF(C_NOT f),CTL_NNF(C_NOT g)))) /\ 409(CTL_NNF (C_NOT (C_NOT f)) = CTL_NNF f) /\ 410(CTL_NNF (C_NOT (C_EX f)) = (C_AX (CTL_NNF (C_NOT f)))) /\ 411(CTL_NNF (C_NOT (C_EG f)) = (C_AF (CTL_NNF (C_NOT f)))) /\ 412(CTL_NNF (C_NOT (C_EU(f,g))) = (C_AR(CTL_NNF (C_NOT f),CTL_NNF (C_NOT g))))`; 413 414val ctl_size_def = snd (TypeBase.size_of ``:'a ctl``) 415val ctl_size2_def = Define `ctl_size2 (f: 'prop ctl) = ctl_size (\(a:('prop)).0) f` 416val bexp_size_def = snd (TypeBase.size_of ``:'a bexp``); 417val bexp_size2_def = Define `bexp_size2 (b: 'prop bexp) = bexp_size (\(a:('prop)).0) b` 418 419val bexp_pstv_size = Define ` 420(bexp_pstv_size B_TRUE = 0) /\ 421(bexp_pstv_size (B_PROP p) = 1) /\ 422(bexp_pstv_size (B_AND(b1,b2)) = 1+(bexp_pstv_size b1)+(bexp_pstv_size b2)) /\ 423(bexp_pstv_size (B_NOT b) = (bexp_pstv_size b))` 424 425val ctl_pstv_size = Define ` 426(ctl_pstv_size (C_BOOL b) = 1+(bexp_pstv_size b)) /\ 427(ctl_pstv_size (C_AND(f1,f2)) = 1+(ctl_pstv_size f1) + (ctl_pstv_size f2)) /\ 428(ctl_pstv_size (C_NOT f) = (ctl_pstv_size f)) /\ 429(ctl_pstv_size (C_EX f) = 1+(ctl_pstv_size f)) /\ 430(ctl_pstv_size (C_EG f) = 1+(ctl_pstv_size f)) /\ 431(ctl_pstv_size (C_EU(f1,f2)) =1+(ctl_pstv_size f1) + (ctl_pstv_size f2))` 432 433(*val cdefn = Defn.Hol_defn "CTL_NNF" ` 434(CTL_NNF (C_BOOL b) = C_BOOL b) /\ 435(CTL_NNF (C_AND(f,g)) = C_AND(CTL_NNF f,CTL_NNF g)) /\ 436(CTL_NNF (C_EX f) = C_EX (CTL_NNF f)) /\ 437(CTL_NNF (C_EG f) = C_EG (CTL_NNF f)) /\ 438(CTL_NNF (C_EU(f,g)) = C_EU (CTL_NNF f,CTL_NNF g)) /\ 439(CTL_NNF (C_NOT (C_BOOL b)) = (C_BOOL (BEXP_NNF (B_NOT b)))) /\ 440(CTL_NNF (C_NOT (C_AND(f,g))) = (C_OR(CTL_NNF(C_NOT f),CTL_NNF(C_NOT g)))) /\ 441(CTL_NNF (C_NOT (C_NOT f)) = CTL_NNF f) /\ 442(CTL_NNF (C_NOT (C_EX f)) = (C_AX (CTL_NNF (C_NOT f)))) /\ 443(CTL_NNF (C_NOT (C_EG f)) = (C_AF (CTL_NNF (C_NOT f)))) /\ 444(CTL_NNF (C_NOT (C_EU(f,g))) = (C_AR(CTL_NNF (C_NOT f),CTL_NNF (C_NOT g))))`; 445 446val (CTL_NNF_def,CTL_NNF_ind) = Defn.tprove(cdefn, 447 WF_REL_TAC `measure ctl_pstv_size` 448 THEN REPEAT (FIRST [Induct_on `f`,Induct_on `g`,Induct_on `b`]) 449 THEN FULL_SIMP_TAC arith_ss [ctl_pstv_size,bexp_pstv_size,C_AX_def,C_AR_def,C_AF_def,BEXP_NNF,B_OR_def,B_FALSE_def]*) 450 451val CTL_BOOL_SUB = Define ` 452(CTL_BOOL_SUB g (B_PROP (b:'prop)) = (g = B_PROP b)) /\ 453(CTL_BOOL_SUB g (B_NOT be1) = (CTL_BOOL_SUB g be1) \/ (g = B_NOT be1)) /\ 454(CTL_BOOL_SUB g (B_AND(be1,be2)) = (CTL_BOOL_SUB g be1) \/ (CTL_BOOL_SUB g be2) \/ (g = B_AND(be1,be2)))`; 455 456val CTL_SUB = Define ` 457(CTL_SUB g (C_BOOL b) = ?b'. (g = C_BOOL b') /\ CTL_BOOL_SUB b' b) /\ 458(CTL_SUB g (C_AND(f1,f2)) = (CTL_SUB g f1) \/ (CTL_SUB g f2) \/ (g = C_AND(f1,f2))) /\ 459(CTL_SUB g (C_NOT f) = (CTL_SUB g f) \/ (g=C_NOT f)) /\ 460(CTL_SUB g (C_EX f) = (CTL_SUB g f) \/ (g=C_EX f)) /\ 461(CTL_SUB g (C_EG f) = (CTL_SUB g f) \/ (g=C_EG f)) /\ 462(CTL_SUB g (C_EU(f1,f2)) = (CTL_SUB g f1) \/ (CTL_SUB g f2) \/ (g=C_EU(f1,f2)))`; 463 464val IS_ACTL = Define `IS_ACTL f = (!g. ~CTL_SUB (C_EX g) (CTL_NNF f)) /\ (!g. ~CTL_SUB (C_EG g) (CTL_NNF f)) /\ (!g1 g2. ~CTL_SUB (C_EU(g1,g2)) (CTL_NNF f))`; 465 466val CTL_NNF_ID = save_thm("CTL_NNF_ID",prove(``!f M. C_SEM M (CTL_NNF f) = C_SEM M f``, 467REWRITE_TAC [FUN_EQ_THM] 468THEN recInduct (theorem "CTL_NNF_ind") THEN REPEAT CONJ_TAC THEN SIMP_TAC std_ss [CTL_NNF] 469THEN REWRITE_TAC [FUN_EQ_THM,C_AR_def,C_AX_def,C_AF_def,C_OR_def] THEN SIMP_TAC std_ss [C_SEM_def] 470THEN recInduct (theorem "BEXP_NNF_ind") THEN REPEAT CONJ_TAC THEN SIMP_TAC std_ss [BEXP_NNF] 471THEN REWRITE_TAC [FUN_EQ_THM,B_FALSE_def,B_OR_def] THEN SIMP_TAC std_ss [B_SEM_def] 472)); 473 474(****************************************************************************** 475* REST(INFINITE f) = INFINITE(\n. f(n+1)) 476******************************************************************************) 477val REST_INFINITE = 478 store_thm 479 ("REST_INFINITE", 480 ``!f. REST (INFINITE f) = INFINITE(\n. f(n+1))``, 481 RW_TAC list_ss [REST_def]); 482 483(****************************************************************************** 484* RESTN (INFINITE f) i = INFINITE(\n. f(n+i)) 485******************************************************************************) 486val RESTN_INFINITE = 487 store_thm 488 ("RESTN_INFINITE", 489 ``!f i. RESTN (INFINITE f) i = INFINITE(\n. f(n+i))``, 490 Induct_on `i` 491 THEN RW_TAC list_ss 492 [REST_INFINITE,ETA_AX,RESTN_def, 493 DECIDE``i + (n + 1) = n + SUC i``]); 494 495val REST_FINITE = 496 store_thm 497 ("REST_FINITE", 498 ``!l. REST (FINITE l) = FINITE(TL l)``, 499 RW_TAC list_ss [REST_def]); 500 501val _ = export_theory() 502