1(* 2app load 3["pairTheory", "pairLib", "pairTools", "pairSyntax", "pred_setTheory", "pred_setLib", 4 "stringLib", "listTheory", "rich_listTheory", "simpLib", "stringTheory", "sumTheory", 5 "ksTheory", "numLib", "setLemmasTheory", "muSyntaxTheory", "muTheory", "res_quanLib", 6 "envTheory", "ctlTheory", "metisLib", "res_quanLib"]; 7*) 8 9open HolKernel Parse boolLib bossLib 10 11val _ = new_theory "ctl2mu"; 12 13open pairTheory; 14open pairLib; 15open pairTools; 16open pairSyntax; 17open pred_setTheory; 18open pred_setLib; 19open stringLib; 20open listTheory; 21open rich_listTheory; 22open simpLib; 23open stringTheory; 24open sumTheory; 25open ksTheory; 26open numLib; 27open setLemmasTheory; 28open muSyntaxTheory 29open muTheory; 30open res_quanLib 31open envTheory 32open ctlTheory 33open metisLib 34open res_quanLib 35 36val _ = numLib.prefer_num(); 37 38fun tsimps ty = 39 let val {convs,rewrs} = TypeBase.simpls_of ty in rewrs end; 40 41val BEXP2MU_def = Define ` 42(BEXP2MU (B_TRUE: 'prop bexp) = (TR:'prop mu)) /\ 43(BEXP2MU (B_PROP (b:'prop)) = (AP (b:'prop))) /\ 44(BEXP2MU (B_NOT be) = ~(BEXP2MU be)) /\ 45(BEXP2MU (B_AND(be1,be2)) = (BEXP2MU be1) /\ (BEXP2MU be2))`; 46 47val CTL2MU_def = Define ` 48 (CTL2MU (C_BOOL b) = BEXP2MU b) /\ 49 (CTL2MU (C_NOT f) = ~(CTL2MU f)) /\ 50 (CTL2MU (C_AND(f,g)) = (CTL2MU f) /\ (CTL2MU g )) /\ 51 (CTL2MU (C_EX f) = <<".">> (CTL2MU f)) /\ 52 (CTL2MU (C_EG f) = nu "Q" .. ((CTL2MU f ) /\ <<".">> (RV "Q"))) /\ 53 (CTL2MU (C_EU(f,g)) = mu "Q" .. ((CTL2MU g) \/ ((CTL2MU f) /\ <<".">> (RV "Q"))))`; 54 55val ctl2muks_def = Define `ctl2muks (M : ('prop,'state) kripke_structure) = 56 <| S := M.S; 57 S0 := M.S0; 58 T := (\q. M.R); 59 ap := M.P; 60 L := M.L |>`; 61 62val REST_RESTN = save_thm("REST_RESTN",prove(``!p. REST p = RESTN p (1:num)``, 63Induct_on `p` THEN REWRITE_TAC [REST_def,RESTN_def,DECIDE ``1 = SUC 0``])); 64 65val ELEM_REST = save_thm("ELEM_REST",prove(``!(p:'state path) (n:num). ELEM (REST p) n = ELEM p (n+1)``, 66Induct_on `p` THEN Induct_on `n` THENL [ 67REWRITE_TAC [ELEM_def,RESTN_def,REST_def,DECIDE ``1 = SUC 0``, DECIDE ``0+1=SUC 0``], (* finite, 0 *) 68FULL_SIMP_TAC std_ss [ELEM_def,RESTN_def,REST_def,DECIDE ``SUC n + 1 = SUC (SUC n)``,DECIDE ``n+1 = SUC n``], (* finite, SUC n *) 69REWRITE_TAC [ELEM_def,RESTN_def,REST_def,DECIDE ``1 = SUC 0``, DECIDE ``0+1=SUC 0``], (* infinite, 0 *) 70FULL_SIMP_TAC std_ss [ELEM_def,RESTN_def,REST_def,DECIDE ``SUC n + 1 = SUC (SUC n)``,DECIDE ``n+1 = SUC n``] (* infinite, SUC n *) 71])); 72 73val PATH_REST = save_thm("PATH_REST",prove(``!(p:'state path) (M: ('prop,'state) kripke_structure) (s:'state). PATH M p s ==> PATH M (REST p) (ELEM p 1)``, 74Induct_on `p` THENL [ 75 SIMP_TAC std_ss [PATH_def,IS_INFINITE_def], 76 REWRITE_TAC [PATH_def] 77 THEN REWRITE_TAC [REST_INFINITE,IS_INFINITE_def] 78 THEN REPEAT STRIP_TAC THENL [ 79 SIMP_TAC arith_ss [ELEM_def,RESTN_INFINITE,HEAD_def], 80 FULL_SIMP_TAC arith_ss [ELEM_def,RESTN_INFINITE,HEAD_def] 81 THEN POP_ASSUM (fn t => ASSUME_TAC (SPEC ``(n:num)+1`` t)) 82 THEN FULL_SIMP_TAC arith_ss []]])); 83 84val EG_LEMMA = prove(``!(M :('prop,'state) kripke_structure) (f:'prop ctl) (s:'state). C_SEM M (C_EG f) s = C_SEM M (C_AND(f,C_EX (C_EG f))) s``, 85REPEAT GEN_TAC THEN EQ_TAC THENL [ 86REWRITE_TAC [C_SEM_def,IN_DEF] 87THEN BETA_TAC 88THEN REPEAT STRIP_TAC THENL [ 89 FULL_SIMP_TAC resq_ss [PATH_def,IN_DEF] 90 THEN Induct_on `p` THENL [ 91 SIMP_TAC std_ss [IS_INFINITE_def], 92 SIMP_TAC std_ss [PLENGTH_def,xnum_to_def,IS_INFINITE_def] 93 THEN SIMP_TAC arith_ss [] THEN GEN_TAC THEN PROVE_TAC []], (* ==>, f case *) 94 EXISTS_TAC ``p:'state path`` 95 THEN REPEAT STRIP_TAC THENL [ 96 ASM_REWRITE_TAC [], 97 EXISTS_TAC ``REST (p:'state path)`` 98 THEN REPEAT STRIP_TAC THENL [ 99 FULL_SIMP_TAC std_ss [PATH_def] 100 THEN REPEAT STRIP_TAC THENL [ 101 FULL_SIMP_TAC std_ss [IS_INFINITE_REST], 102 FULL_SIMP_TAC std_ss [ELEM_REST], 103 SIMP_TAC std_ss [ELEM_REST,DECIDE ``SUC n + 1 = n + 2``,DECIDE ``SUC n + 1 + 1 = n + 3``] 104 THEN ASSUM_LIST (fn t => PROVE_TAC ((DECIDE ``((n:num)+2)+1 = n + 3``)::t))], (* |- PATH M (REST p) (ELEM p 1) *) 105 REWRITE_TAC [ELEM_REST] 106 THEN Induct_on `p` THENL [ 107 REWRITE_TAC [PATH_def,IS_INFINITE_def], (* finite *) 108 REWRITE_TAC [PATH_def,IS_INFINITE_def] 109 THEN REWRITE_TAC [REST_INFINITE,PLENGTH_def] 110 THEN SIMP_TAC resq_ss [IN_DEF,xnum_to_def] 111 THEN SIMP_TAC arith_ss []]]]], (* ==> *) 112REWRITE_TAC [C_SEM_def,IN_DEF] 113THEN BETA_TAC 114THEN REPEAT STRIP_TAC 115THEN Induct_on `p` THEN Induct_on `p'` 116THEN REWRITE_TAC [PATH_def,IS_INFINITE_def] 117THEN REPEAT STRIP_TAC 118THEN EXISTS_TAC ``INFINITE (\n. if (n=0) then s else ((f':num->'state) (n-1)))`` 119THEN SIMP_TAC std_ss [IS_INFINITE_def] 120THEN FULL_SIMP_TAC resq_ss [IN_DEF,xnum_to_def,PLENGTH_def] 121THEN SIMP_TAC arith_ss [] 122THEN REPEAT STRIP_TAC THENL [ 123 REWRITE_TAC [ELEM_def,RESTN_INFINITE] 124 THEN SIMP_TAC arith_ss [] 125 THEN SIMP_TAC std_ss [HEAD_def], (* p0=s case *) 126 Induct_on `n` THENL [ 127 SIMP_TAC std_ss [ELEM_def,RESTN_INFINITE,HEAD_def] 128 THEN Q.PAT_ASSUM `ELEM (INFINITE f') 0 = ELEM (INFINITE f'') 1` 129 (fn t => ONCE_REWRITE_TAC [SIMP_RULE std_ss [ELEM_def,RESTN_INFINITE,HEAD_def] t]) 130 THEN Q.PAT_ASSUM `ELEM (INFINITE f'') 0 = s` (fn t => ONCE_REWRITE_TAC [SIMP_RULE std_ss [ELEM_def,RESTN_INFINITE,HEAD_def] (SYM t)]) 131 THEN Q.PAT_ASSUM `!n. M.R (ELEM (INFINITE f'') n,ELEM (INFINITE f'') (n + 1))` 132 (fn t => ONCE_REWRITE_TAC [SIMP_RULE std_ss [ELEM_def,RESTN_INFINITE,HEAD_def] (SPEC ``0:num`` t)]), (* 0 *) 133 SIMP_TAC std_ss [ELEM_def,RESTN_INFINITE,HEAD_def] 134 THEN SIMP_TAC arith_ss [] 135 THEN ONCE_REWRITE_TAC [DECIDE ``SUC n = n + 1``] 136 THEN Q.PAT_ASSUM `!n. M.R (ELEM (INFINITE f') n,ELEM (INFINITE f') (n + 1))` 137 (fn t=> ONCE_REWRITE_TAC [SIMP_RULE arith_ss [ELEM_def,RESTN_INFINITE,HEAD_def] (SPEC ``n:num`` t)])], (* SUC n, !n. R(p_n,p_(n+1) *) 138 Induct_on `j` THENL [ 139 SIMP_TAC arith_ss [ELEM_def,RESTN_INFINITE,HEAD_def] 140 THEN ASM_REWRITE_TAC [], (* 0 *) 141 ONCE_REWRITE_TAC [DECIDE ``SUC j = j + 1``] 142 THEN SIMP_TAC arith_ss [ELEM_def,RESTN_INFINITE,HEAD_def] 143 THEN FULL_SIMP_TAC arith_ss [] 144 THEN Q.PAT_ASSUM `!j'. C_SEM M f (ELEM (INFINITE f') j')` 145 (fn t => REWRITE_TAC [SIMP_RULE arith_ss [ELEM_def,RESTN_INFINITE,HEAD_def] (SPEC ``j:num`` t)])]]]); 146 147val Nf2 = Define `(Nf2 (R:'state # 'state -> bool) (s:'state) (0:num) = s) /\ (Nf2 R s (SUC n) = (@r. R(Nf2 R s n,r)))`; 148 149val unc = Define `unc R = \x y. R(x,y)`; (*FIXME: replace this with CURRY_DEF*) 150val unc_thm = save_thm("unc_thm",prove(``!P x y. P(x,y) = (unc P) x y``,PROVE_TAC [unc])); 151 152val EU_LEMMA = prove(``!(M :('prop,'state) kripke_structure) (f:'prop ctl) (g:'prop ctl) (s:'state). TOTAL M.R ==> 153 (C_SEM M (C_EU(f,g)) s = C_SEM M (C_NOT(C_AND(C_NOT g,C_NOT(C_AND(f,C_EX (C_EU(f,g))))))) s)``, 154REPEAT GEN_TAC THEN STRIP_TAC THEN EQ_TAC THENL [ 155REWRITE_TAC [C_SEM_def,PATH_def,IN_DEF] 156THEN BETA_TAC 157THEN SIMP_TAC std_ss [] 158THEN STRIP_TAC 159THEN Induct_on `p` THEN FULL_SIMP_TAC std_ss [IS_INFINITE_def] 160THEN SIMP_TAC resq_ss [IN_DEF,xnum_to_def,PLENGTH_def] 161THEN SIMP_TAC arith_ss [] 162THEN REPEAT STRIP_TAC 163THEN Cases_on `C_SEM M g s` 164THEN RW_TAC std_ss [] THENL [ (* 2 *) 165IMP_RES_TAC ( prove(``C_SEM M g (ELEM (INFINITE f') k) /\ ~C_SEM M g (ELEM (INFINITE f') 0) ==> ~(k=0)``,PROVE_TAC [])) 166THEN PAT_ASSUM ``!(j:num). (P:bool) ==> (Q:bool)`` (fn t => (ASSUME_TAC (SPEC ``0:num`` t))) 167THEN FULL_SIMP_TAC arith_ss [], 168EXISTS_TAC ``(INFINITE (f':num->'state))`` 169THEN FULL_SIMP_TAC std_ss [IS_INFINITE_def] 170THEN EXISTS_TAC ``REST (INFINITE (f':num -> 'state))`` 171THEN FULL_SIMP_TAC std_ss [REST_INFINITE,IS_INFINITE_def,ELEM_REST] 172THEN FULL_SIMP_TAC arith_ss [PLENGTH_def,xnum_to_def] 173THEN EXISTS_TAC ``(k-1):num`` 174THEN IMP_RES_TAC ( prove(``C_SEM M g (ELEM (INFINITE f') k) /\ ~C_SEM M g (ELEM (INFINITE f') 0) ==> ~(k=0)``,PROVE_TAC [])) 175THEN FULL_SIMP_TAC arith_ss []], (* ==> *) 176REWRITE_TAC [C_SEM_def,PATH_def,IN_DEF] 177THEN BETA_TAC 178THEN SIMP_TAC std_ss [] 179THEN STRIP_TAC THENL [ (* 2 *) 180EXISTS_TAC ``INFINITE (Nf2 (M :('prop,'state) kripke_structure).R (s :'state))`` 181THEN SIMP_TAC std_ss [Nf2,IS_INFINITE_def,ELEM_def,RESTN_INFINITE,HEAD_def] 182THEN FULL_SIMP_TAC arith_ss [TOTAL_def] 183THEN CONJ_TAC THENL [ 184 ONCE_REWRITE_TAC [DECIDE ``n+1=SUC n``] 185 THEN Induct_on `n` THENL [ 186 SIMP_TAC arith_ss [Nf2,ELEM_def,RESTN_def,REST_def,HEAD_def,listTheory.HD,listTheory.TL, 187 PLENGTH_def,GT_xnum_num_def,listTheory.LENGTH] 188 THEN PAT_ASSUM ``!(s:'state). ?(s':'state). M.R (s,s')`` (fn t => ASSUME_TAC (SPEC ``s:'state`` t)) 189 THEN FULL_SIMP_TAC std_ss [unc_thm] 190 THEN REWRITE_TAC [SELECT_THM] 191 THEN ASSUM_LIST PROVE_TAC, (* 0 *) 192 FULL_SIMP_TAC arith_ss [ELEM_def,RESTN_INFINITE,HEAD_def,TOTAL_def,Nf2] 193 THEN PAT_ASSUM ``!(s:'state). ?(s':'state). M.R (s,s')`` 194 (fn t => ASSUME_TAC (SPEC ``@(r:'state). (M :('prop,'state) kripke_structure).R (Nf2 M.R s n,r)`` t)) 195 THEN FULL_SIMP_TAC std_ss [unc_thm] 196 THEN REWRITE_TAC [SELECT_THM] 197 THEN ASSUM_LIST PROVE_TAC], (* SUC *) 198 SIMP_TAC resq_ss [IN_DEF,PLENGTH_def] 199 THEN SIMP_TAC arith_ss [xnum_to_def] 200 THEN EXISTS_TAC ``0:num`` 201 THEN FULL_SIMP_TAC arith_ss [Nf2]], (* g *) 202 EXISTS_TAC ``INFINITE (\n. if (n=0) then s else ELEM (p':'state path) (n-1))`` 203 THEN FULL_SIMP_TAC resq_ss [] 204 THEN SIMP_TAC std_ss [IS_INFINITE_def,IN_DEF,xnum_to_def,PLENGTH_def] 205 THEN SIMP_TAC arith_ss [] 206 THEN REPEAT CONJ_TAC THENL [ (* 3 *) 207 SIMP_TAC std_ss [ELEM_def,RESTN_INFINITE,HEAD_def], (* p_0 = s *) 208 Induct_on `n` THENL [ 209 SIMP_TAC arith_ss [ELEM_def,RESTN_INFINITE,HEAD_def] 210 THEN REWRITE_TAC [RESTN_def] 211 THEN Induct_on `p'` THEN REPEAT STRIP_TAC THENL [ 212 FULL_SIMP_TAC std_ss [IS_INFINITE_def], (* finite *) 213 REWRITE_TAC [HEAD_def] 214 THEN PAT_ASSUM ``ELEM (INFINITE (f':num -> 'state)) 0 = ELEM (p:'state path) 1`` (fn t => 215 REWRITE_TAC [(CONV_RULE (LHS_CONV (SIMP_CONV std_ss [ELEM_def,RESTN_INFINITE,HEAD_def]))) t]) 216 THEN PAT_ASSUM ``ELEM (p:'state path) 0 = s`` (fn t => REWRITE_TAC [SYM t]) 217 THEN ONCE_REWRITE_TAC [DECIDE ``(1:num) = 0 + 1``] 218 THEN PAT_ASSUM ``!n. (M :('prop,'state) kripke_structure).R (ELEM p n,ELEM p (n + 1))`` 219 (fn t => REWRITE_TAC [SPEC ``0:num`` t])], (* infinite,0 *) 220 ONCE_REWRITE_TAC [ELEM_def] 221 THEN ONCE_REWRITE_TAC [RESTN_INFINITE] 222 THEN ONCE_REWRITE_TAC [HEAD_def] 223 THEN SIMP_TAC arith_ss [] 224 THEN ONCE_REWRITE_TAC [DECIDE ``SUC n = n + 1``] 225 THEN PAT_ASSUM ``!n. (M :('prop,'state) kripke_structure).R (ELEM p' n,ELEM p' (n + 1))`` 226 (fn t => REWRITE_TAC [SPEC ``n:num`` t])], (* SUC, R(p_n,p_(n+1)) *) 227 EXISTS_TAC ``SUC k`` 228 THEN ONCE_REWRITE_TAC [ELEM_def] 229 THEN ONCE_REWRITE_TAC [RESTN_INFINITE] 230 THEN ONCE_REWRITE_TAC [HEAD_def] 231 THEN SIMP_TAC arith_ss [] 232 THEN ASM_REWRITE_TAC [] 233 THEN GEN_TAC 234 THEN Cases_on `j=0` THENL [ 235 FULL_SIMP_TAC std_ss [], 236 FULL_SIMP_TAC std_ss [] 237 THEN Induct_on `j` THENL [ 238 SIMP_TAC std_ss [], (* 0 *) 239 REWRITE_TAC [DECIDE ``!j. ~(SUC j = 0)``] 240 THEN REWRITE_TAC [DECIDE ``!j k. SUC j < SUC k = j < k``,DECIDE ``!j. SUC j - 1 = j``] 241 THEN ASSUM_LIST PROVE_TAC]]]]]); (* SUC, j!=0, conj_3, strip_2, <== *) 242 243val fol1 = prove(``!x y x' y' z z'. (((x=y)==>z) /\ ((x'=y')==>z')) ==> (((x=y)/\(x'=y'))==>(z/\z'))``,PROVE_TAC []); 244val fol2 = prove(``!x y x' y'. (x = y) /\ (x' = y') ==> (x/\x' = y /\ y')``,PROVE_TAC []); 245val fol4 = prove(``!x y z. ((x==>y)/\(x==>z))==>(x==>(y/\z))``,PROVE_TAC []); 246val fol5 = prove(``!a b c. (a = c) ==> (a /\ b = c /\ b)``,PROVE_TAC []); 247 248val IMF_CTL_LEM8a1 = prove( 249 ``!f Q Q'. ~(Q IN FV f) = ~(Q IN (FV (RVNEG Q' f)))``, 250 Induct_on `f` THEN 251 SIMP_TAC std_ss ([FV_def,UNION_DEF,DELETE_DEF,DIFF_DEF,SET_SPEC,IN_SING, 252 RVNEG_def]@ tsimps ``:'a mu``) 253 THENL [ (* 8 *) 254 FULL_SIMP_TAC std_ss [], 255 PROVE_TAC[], 256 PROVE_TAC[], 257 REPEAT GEN_TAC THEN CASE_TAC THENL [ (* 2 *) 258 EQ_TAC THEN SIMP_TAC std_ss [FV_def,IN_SING], 259 EQ_TAC THEN SIMP_TAC std_ss [FV_def,IN_SING] 260 ], 261 PROVE_TAC[], 262 PROVE_TAC[], 263 REPEAT GEN_TAC THEN CASE_TAC THENL [ (* 2 *) 264 FULL_SIMP_TAC std_ss [FV_def,DELETE_DEF,IN_SING,DIFF_DEF,SET_SPEC], 265 FULL_SIMP_TAC std_ss [FV_def,DELETE_DEF,IN_SING,DIFF_DEF,SET_SPEC] 266 THEN MATCH_MP_TAC fol5 267 THEN ASSUM_LIST PROVE_TAC 268 ], 269 REPEAT GEN_TAC THEN CASE_TAC THENL [ (* 2 *) 270 FULL_SIMP_TAC std_ss [FV_def,DELETE_DEF,IN_SING,DIFF_DEF,SET_SPEC], 271 FULL_SIMP_TAC std_ss [FV_def,DELETE_DEF,IN_SING,DIFF_DEF,SET_SPEC] 272 THEN MATCH_MP_TAC fol5 273 THEN ASSUM_LIST PROVE_TAC 274 ] 275 ]); 276 277val IMF_CTL_LEM8a = prove( 278 ``!f Q. ~(Q IN FV f) ==> IMF f ==> ~SUBFORMULA (~RV Q) (NNF f)``, 279 recInduct NNF_IND_def THEN 280 SIMP_TAC std_ss ([MU_SUB_def,IMF_def,FV_def,NNF_def,UNION_DEF,SET_SPEC, 281 DELETE_DEF,DIFF_DEF,RVNEG_def,IN_SING] @ 282 tsimps ``:'a mu``) THEN 283 REPEAT CONJ_TAC THENL [ (* 3 *) 284 NTAC 6 STRIP_TAC THENL [(* 2 *) 285 FULL_SIMP_TAC std_ss [], 286 FULL_SIMP_TAC std_ss [] 287 ], 288 NTAC 6 STRIP_TAC THENL [(* 2 *) 289 FULL_SIMP_TAC std_ss [], 290 FULL_SIMP_TAC std_ss [] 291 ], 292 NTAC 6 STRIP_TAC THENL [(* 2 *) 293 FULL_SIMP_TAC std_ss [IMF_INV_RVNEG] 294 THEN ASSUM_LIST (fn t => PROVE_TAC (IMF_CTL_LEM8a1::t)), 295 PROVE_TAC [STATES_MONO_LEM3,RVNEG_def] 296 ] 297 ]); 298 299val FV_BEXP2MU = save_thm("FV_BEXP2MU",prove(``!b. FV (BEXP2MU b) = {}``, 300recInduct (theorem "BEXP2MU_ind") 301THEN FULL_SIMP_TAC std_ss [BEXP2MU_def,STATES_def,FV_def] 302THEN PROVE_TAC [EMPTY_UNION])); 303 304val FV_CTL2MU = save_thm("FV_CTL2MU",prove(``!(f: 'prop ctl). FV (CTL2MU f) = {}``, 305recInduct (theorem "CTL2MU_ind") 306THEN FULL_SIMP_TAC std_ss [FV_BEXP2MU,CTL2MU_def,STATES_def,FV_def] 307THEN REPEAT STRIP_TAC THENL [ 308PROVE_TAC [EMPTY_UNION], 309SIMP_TAC std_ss [UNION_DEF,DELETE_DEF,DIFF_DEF,SET_SPEC,NOT_IN_EMPTY] 310THEN SIMP_TAC std_ss [EMPTY_DEF,SET_GSPEC], 311SIMP_TAC std_ss [UNION_DEF,DELETE_DEF,DIFF_DEF,SET_SPEC,NOT_IN_EMPTY] 312THEN SIMP_TAC std_ss [EMPTY_DEF,SET_GSPEC] 313] 314)); 315 316val IMF_CTL_LEM =save_thm("IMF_CTL_LEM",prove(``!f Q. IMF (CTL2MU f) ==> ~SUBFORMULA (~RV Q) (NNF (CTL2MU f))``, 317GEN_TAC THEN SIMP_TAC std_ss [IMF_CTL_LEM8a,FV_CTL2MU,NOT_IN_EMPTY])); 318 319val IMF_CTL = save_thm("IMF_CTL",prove(``!f. IMF (CTL2MU f)``, 320recInduct (theorem "CTL2MU_ind") THEN REPEAT CONJ_TAC THENL [ 321 REWRITE_TAC [CTL2MU_def] 322 THEN recInduct (theorem "BEXP2MU_ind") 323 THEN FULL_SIMP_TAC std_ss ([IMF_def,BEXP2MU_def,NNF_def,MU_SUB_def,RVNEG_def]@(tsimps ``:'a mu``)), (* C_BOOL *) 324 SIMP_TAC std_ss [CTL2MU_def,IMF_def], (* C_NOT *) 325 SIMP_TAC std_ss [CTL2MU_def,IMF_def], (* C_AND *) 326 SIMP_TAC std_ss [CTL2MU_def,IMF_def], (* C_EX *) 327 SIMP_TAC std_ss ([CTL2MU_def,IMF_def,NNF_def,MU_SUB_def,RVNEG_def,IMF_CTL_LEM]@(tsimps ``:'a mu``)), (* C_EG *) 328 SIMP_TAC std_ss ([CTL2MU_def,IMF_def,NNF_def,MU_SUB_def,RVNEG_def,IMF_CTL_LEM]@(tsimps ``:'a mu``)) (* C_EU *) 329])); 330 331val Nf = Define `(Nf (R:'state # 'state -> bool) (s:'state) (q:'state) (0:num) = s) /\ (Nf R s q (SUC n) = if (n=0) then q else (@r. R(Nf R s q n,r)))`; 332 333val STATES_FV_ENV_INV_SPEC = save_thm("STATES_FV_ENV_INV_SPEC",prove(``!(f: 'prop ctl) (M: ('prop,'state) kripke_structure) X. 334 (STATES (CTL2MU f) (ctl2muks M) EMPTY_ENV[[["Q"<--X]]] 335 = STATES (CTL2MU f) (ctl2muks M) EMPTY_ENV)``, 336recInduct (theorem "CTL2MU_ind") THEN SIMP_TAC std_ss [FV_CTL2MU,NOT_IN_EMPTY] THEN REPEAT CONJ_TAC THENL [ 337recInduct (theorem "BEXP2MU_ind") 338THEN FULL_SIMP_TAC std_ss [STATES_def,BEXP2MU_def,CTL2MU_def], 339FULL_SIMP_TAC std_ss [STATES_def,CTL2MU_def], (* ~ *) 340FULL_SIMP_TAC std_ss [STATES_def,CTL2MU_def], (* /\ *) 341FULL_SIMP_TAC std_ss [STATES_def,CTL2MU_def], (* EX *) 342FULL_SIMP_TAC std_ss [STATES_def,CTL2MU_def] 343THEN REPEAT STRIP_TAC 344THEN SIMP_TAC std_ss [EXTENSION,SET_SPEC] 345THEN SIMP_TAC std_ss [ENV_UPDATE], 346FULL_SIMP_TAC std_ss [STATES_def,CTL2MU_def] 347THEN REPEAT STRIP_TAC 348THEN SIMP_TAC std_ss [EXTENSION,SET_SPEC] 349THEN SIMP_TAC std_ss [ENV_UPDATE]])); 350 351val Nf3 = Define `(Nf3 (R:'state # 'state -> bool) (x:'state) (q:'state) (0:num) = x) 352 /\ (Nf3 R x q (SUC n) = if (n=0) then q else (@r. R(Nf3 R x q n,r)))`; 353 354val CTL2MU_AND_LEM = prove(``!(M: ('prop,'state) kripke_structure) f1 f2 . C_SEM M (C_AND(f1,f2)) = C_SEM M f1 INTER C_SEM M f2``, 355REPEAT GEN_TAC 356THEN REWRITE_TAC [FUN_EQ_THM] 357THEN REWRITE_TAC [INTER_DEF] 358THEN SIMP_TAC std_ss [SET_GSPEC] 359THEN SIMP_TAC std_ss [IN_DEF] 360THEN REWRITE_TAC [C_SEM_def]); 361 362val CTL2MU_OR_LEM = prove(``!(M: ('prop,'state) kripke_structure) f1 f2 . C_SEM M (C_NOT(C_AND(C_NOT f1,C_NOT f2))) = C_SEM M f1 UNION C_SEM M f2``, 363REPEAT GEN_TAC 364THEN REWRITE_TAC [FUN_EQ_THM] 365THEN REWRITE_TAC [UNION_DEF] 366THEN SIMP_TAC std_ss [SET_GSPEC] 367THEN SIMP_TAC std_ss [IN_DEF] 368THEN SIMP_TAC std_ss [C_SEM_def]); 369 370val CTL2MU_EG_LEM = prove(``!(M: ('prop,'state) kripke_structure) (f:'prop ctl). TOTAL M.R /\ wfKS (ctl2muks M) ==> 371 (STATES <<".">> (RV "Q") (ctl2muks M) EMPTY_ENV[[["Q"<--C_SEM M (C_EG f)]]] = C_SEM M (C_EX (C_EG f)))``, 372REPEAT STRIP_TAC 373THEN SIMP_TAC std_ss [EXTENSION] 374THEN GEN_TAC 375THEN REWRITE_TAC [STATES_def] 376THEN FULL_SIMP_TAC std_ss [SET_SPEC,wfKS_def,IN_UNIV] 377THEN REWRITE_TAC [IN_DEF] 378THEN SIMP_TAC std_ss [ENV_EVAL] 379THEN SIMP_TAC std_ss [C_SEM_def,IN_DEF] 380THEN SIMP_TAC std_ss [KS_TRANSITION_def,ctl2muks_def,KS_accfupds,combinTheory.K_DEF] THEN (CONV_TAC (DEPTH_CONV BETA_CONV)) 381THEN EQ_TAC THENL [ 382 STRIP_TAC 383 THEN EXISTS_TAC ``INFINITE (Nf3 (M: ('prop,'state) kripke_structure).R x q)`` 384 THEN CONJ_TAC THENL [ 385 FULL_SIMP_TAC std_ss [PATH_def,TOTAL_def] 386 THEN REPEAT CONJ_TAC THENL [ (* 3 *) 387 REWRITE_TAC [IS_INFINITE_def], 388 SIMP_TAC std_ss [ELEM_def,RESTN_INFINITE,HEAD_def,Nf3], 389 ONCE_REWRITE_TAC [DECIDE ``n+1=SUC n``] 390 THEN Induct_on `n` THENL [ 391 SIMP_TAC arith_ss [Nf3,ELEM_def,RESTN_INFINITE,HEAD_def] 392 THEN REWRITE_TAC [Nf3,DECIDE ``1=SUC 0``] 393 THEN ASM_REWRITE_TAC [], (* 0 *) 394 FULL_SIMP_TAC arith_ss [ELEM_def,RESTN_INFINITE,HEAD_def,TOTAL_def,Nf3] 395 THEN PAT_ASSUM ``!(s:'state). ?(s':'state). M.R (s,s')`` 396 (fn t => ASSUME_TAC (SPEC ``(if n = 0 then q else @(r:'state). (M: ('prop,'state) kripke_structure).R (Nf3 M.R x q n,r))`` t)) 397 THEN FULL_SIMP_TAC std_ss [unc_thm] 398 THEN REWRITE_TAC [SELECT_THM] 399 THEN ASSUM_LIST PROVE_TAC]], (* conj_3 *) 400 EXISTS_TAC ``p: 'state path`` 401 THEN (CONV_TAC (LAND_CONV (SIMP_CONV std_ss [ELEM_def,RESTN_INFINITE,HEAD_def]))) 402 THEN REWRITE_TAC [Nf3,DECIDE ``1=SUC 0``] 403 THEN ASM_REWRITE_TAC []], (* ==> *) 404 STRIP_TAC 405 THEN EXISTS_TAC ``ELEM (p:'state path) 1`` 406 THEN CONJ_TAC THENL [ 407 FULL_SIMP_TAC std_ss [PATH_def] 408 THEN PAT_ASSUM ``ELEM (p:'state path) 0 = x`` (fn t => ONCE_REWRITE_TAC [SYM t]) 409 THEN PAT_ASSUM `` !n. (M: ('prop,'state) kripke_structure).R (ELEM p n,ELEM p (n + 1))`` (fn t => ASSUME_TAC (SPEC ``0:num`` t)) 410 THEN FULL_SIMP_TAC arith_ss [], 411 EXISTS_TAC ``p' : 'state path`` 412 THEN ASM_REWRITE_TAC []]]); (* <== *) 413 414val CTL2MU_EU_LEM = prove(``!(M: ('prop,'state) kripke_structure) (f:'prop ctl) (g:'prop ctl). TOTAL M.R /\ wfKS (ctl2muks M) ==> 415 (STATES <<".">> (RV "Q") (ctl2muks M) EMPTY_ENV[[["Q"<--C_SEM M (C_EU(f,g))]]] = C_SEM M (C_EX (C_EU(f,g))))``, 416REPEAT STRIP_TAC 417THEN SIMP_TAC std_ss [EXTENSION] 418THEN GEN_TAC 419THEN REWRITE_TAC [STATES_def] 420THEN FULL_SIMP_TAC std_ss [SET_SPEC,wfKS_def,IN_UNIV] 421THEN REWRITE_TAC [IN_DEF] 422THEN SIMP_TAC std_ss [ENV_EVAL] 423THEN SIMP_TAC std_ss [C_SEM_def,IN_DEF] 424THEN SIMP_TAC std_ss [KS_TRANSITION_def,ctl2muks_def,KS_accfupds,combinTheory.K_DEF] THEN (CONV_TAC (DEPTH_CONV BETA_CONV)) 425THEN EQ_TAC THENL [ 426 STRIP_TAC 427 THEN EXISTS_TAC ``INFINITE (Nf3 (M: ('prop,'state) kripke_structure).R x q)`` 428 THEN CONJ_TAC THENL [ 429 FULL_SIMP_TAC std_ss [PATH_def,TOTAL_def] 430 THEN REPEAT CONJ_TAC THENL [ (* 3 *) 431 REWRITE_TAC [IS_INFINITE_def], 432 SIMP_TAC std_ss [ELEM_def,RESTN_INFINITE,HEAD_def,Nf3], 433 ONCE_REWRITE_TAC [DECIDE ``n+1=SUC n``] 434 THEN Induct_on `n` THENL [ 435 SIMP_TAC arith_ss [Nf3,ELEM_def,RESTN_INFINITE,HEAD_def] 436 THEN REWRITE_TAC [Nf3,DECIDE ``1=SUC 0``] 437 THEN ASM_REWRITE_TAC [], (* 0 *) 438 FULL_SIMP_TAC arith_ss [ELEM_def,RESTN_INFINITE,HEAD_def,TOTAL_def,Nf3] 439 THEN PAT_ASSUM ``!(s:'state). ?(s':'state). M.R (s,s')`` 440 (fn t => ASSUME_TAC (SPEC ``(if n = 0 then q else @(r:'state). (M: ('prop,'state) kripke_structure).R (Nf3 M.R x q n,r))`` t)) 441 THEN FULL_SIMP_TAC std_ss [unc_thm] 442 THEN REWRITE_TAC [SELECT_THM] 443 THEN ASSUM_LIST PROVE_TAC]], (* conj_3 *) 444 EXISTS_TAC ``p: 'state path`` 445 THEN (CONV_TAC (LAND_CONV (SIMP_CONV std_ss [ELEM_def,RESTN_INFINITE,HEAD_def]))) 446 THEN REWRITE_TAC [Nf3,DECIDE ``1=SUC 0``] 447 THEN ASM_REWRITE_TAC []], (* ==> *) 448 STRIP_TAC 449 THEN EXISTS_TAC ``ELEM (p:'state path) 1`` 450 THEN CONJ_TAC THENL [ 451 FULL_SIMP_TAC std_ss [PATH_def] 452 THEN PAT_ASSUM ``ELEM (p:'state path) 0 = x`` (fn t => ONCE_REWRITE_TAC [SYM t]) 453 THEN PAT_ASSUM `` !n. (M: ('prop,'state) kripke_structure).R (ELEM p n,ELEM p (n + 1))`` (fn t => ASSUME_TAC (SPEC ``0:num`` t)) 454 THEN FULL_SIMP_TAC arith_ss [], 455 EXISTS_TAC ``p' : 'state path`` 456 THEN ASM_REWRITE_TAC []]]); (* <== *) 457 458val GFP_def = Define ` 459(GFP (M: ('prop,'state) kripke_structure) (f: 'prop ctl) (0:num) = (UNIV:'state -> bool)) /\ 460(GFP M f (SUC n) = C_SEM M f INTER {s | ?s'. M.R(s,s') /\ s' IN GFP M f n})`; 461 462val CTL_GFP_EQ_CTL2MU_GFP = prove(``!(f: 'prop ctl) (s:'state) (M: ('prop,'state) kripke_structure). 463 ((C_SEM M f = MU_SAT (CTL2MU f) (ctl2muks M) EMPTY_ENV) /\ wfKS (ctl2muks M) ) 464 ==> (BIGINTER {P | ?i. P = GFP M f i} 465 = BIGINTER {P | ?i. P = FP ((CTL2MU f) /\ <<".">> (RV "Q")) "Q" (ctl2muks M) EMPTY_ENV[[["Q"<--(ctl2muks M).S]]] i})``, 466REPEAT STRIP_TAC 467THEN MATCH_MP_TAC BIGINTER_LEMMA1 468THEN Induct_on `n` THENL [ 469 FULL_SIMP_TAC std_ss [GFP_def,STATES_def,ENV_EVAL,wfKS_def,ctl2muks_def], (* 0 *) 470 REWRITE_TAC [GFP_def] 471 THEN ONCE_REWRITE_TAC [STATES_def] THEN ONCE_REWRITE_TAC [STATES_def] 472 THEN REWRITE_TAC [ STATES_FV_ENV_INV_SPEC,ENV_UPDATE] 473 THEN ONCE_REWRITE_TAC [STATES_def] THEN ONCE_REWRITE_TAC [STATES_def] 474 THEN FULL_SIMP_TAC std_ss [KS_TRANSITION_def,ctl2muks_def,wfKS_def] 475 THEN FULL_SIMP_TAC std_ss [KS_accfupds,KS_accessors,KS_fn_updates] 476 THEN FULL_SIMP_TAC std_ss [ENV_EVAL,IN_UNIV] 477 THEN REWRITE_TAC [SET_SPEC] 478 THEN SIMP_TAC std_ss [INTER_DEF,SET_SPEC] 479 THEN ONCE_REWRITE_TAC [EXTENSION] 480 THEN SIMP_TAC std_ss [SET_SPEC] 481 THEN SIMP_TAC std_ss [IN_DEF,MU_SAT_def]]); 482 483val CTL_GFP_CLOSURE = prove(``!(f: 'prop ctl) (s:'state) (M: ('prop,'state) kripke_structure). 484 ((C_SEM M f = MU_SAT (CTL2MU f) (ctl2muks M) EMPTY_ENV) /\ wfKS (ctl2muks M) /\ FINITE (ctl2muks M).S 485 /\ (!(f: 'prop ctl). IMF (CTL2MU f))) 486 ==> (s IN BIGINTER {P | ?i. P = GFP M f i} 487 = (C_SEM M f s /\ ?s'. M.R(s,s') /\ s' IN BIGINTER {P | ?i. P = GFP M f i}))``, 488REPEAT STRIP_TAC 489THEN IMP_RES_TAC CTL_GFP_EQ_CTL2MU_GFP 490THEN POP_ASSUM (fn t => REWRITE_TAC [t]) 491THEN POP_ASSUM (fn t => ASSUME_TAC (REWRITE_RULE [CTL2MU_def] (SPEC ``C_EG (f:'prop ctl)`` t))) 492THEN IMP_RES_TAC GEN_GFP_IDEM 493THEN POP_ASSUM (fn t => CONV_TAC (LHS_CONV (ONCE_REWRITE_CONV [SYM (SPEC ``EMPTY_ENV:string -> 'state -> bool`` t)]))) 494THEN ONCE_REWRITE_TAC [STATES_def] 495THEN REWRITE_TAC [ STATES_FV_ENV_INV_SPEC,ENV_UPDATE] 496THEN SIMP_TAC std_ss [INTER_DEF,SET_SPEC] 497THEN ONCE_REWRITE_TAC [STATES_def] THEN ONCE_REWRITE_TAC [STATES_def] 498THEN FULL_SIMP_TAC std_ss [KS_TRANSITION_def,ctl2muks_def,wfKS_def] 499THEN FULL_SIMP_TAC std_ss [ctl2muks_def,KS_accfupds,KS_accessors,KS_fn_updates] 500THEN FULL_SIMP_TAC std_ss [ENV_EVAL,IN_UNIV] 501THEN SIMP_TAC std_ss [SET_SPEC] 502THEN SIMP_TAC std_ss [MU_SAT_def,IN_DEF]); 503 504val Nf4_def = Define `(Nf4 (R:'state # 'state -> bool) (P:'state -> bool) (0:num) = (ARB:'state)) 505 /\ (Nf4 R P (SUC n) = @r. R(Nf4 R P n,r) /\ P r)`; 506 507 508val P1_def = Define `P1 P R s = R(ARB,s) /\ P s`; 509val P2_def = Define `P2 P R n s = R(Nf4 R P n,s) /\ P s`; 510val P3_def = Define `P3 P R n s = R((@r. P2 P R n r),s) /\ P s`; 511 512val GFP_CLOSURE_IMP_EG_LEM2 = prove(``!(P:'state ->bool) Q (R:'state # 'state -> bool). (!s. P s = Q s /\ ?s'. R(s,s') /\ P s') 513==> (?f. !n. P (f n) ==> Q(f n) /\ R(f n,f (SUC n)) /\ P (f (SUC n)))``, 514REPEAT STRIP_TAC 515THEN EXISTS_TAC ``Nf4 (R:'state # 'state -> bool) (P:'state ->bool)`` 516THEN Induct_on `n` THENL [ 517STRIP_TAC 518THEN CONJ_TAC THENL [ 519 ASSUM_LIST PROVE_TAC, 520 UNDISCH_TAC ``(P :'state -> bool) (Nf4 (R :'state # 'state -> bool) (P:'state -> bool) (0 :num))`` 521 THEN SIMP_TAC std_ss [Nf4_def] 522 THEN STRIP_TAC 523 THEN REWRITE_TAC [GSYM P1_def] 524 THEN REWRITE_TAC [SELECT_THM] 525 THEN REWRITE_TAC [P1_def] 526 THEN ASSUM_LIST PROVE_TAC], (* conj, 0 *) 527 REWRITE_TAC [Nf4_def] 528 THEN STRIP_TAC 529 THEN CONJ_TAC THENL [ 530 ASSUM_LIST PROVE_TAC, 531 REWRITE_TAC [GSYM P2_def] 532 THEN REWRITE_TAC [GSYM P3_def] 533 THEN REWRITE_TAC [SELECT_THM] 534 THEN REWRITE_TAC [P2_def,P3_def] 535 THEN ASSUM_LIST PROVE_TAC]]); (* conj, SUC *) 536 537val Nf5_def = Define `(Nf5 (R:'state # 'state -> bool) (P:'state -> bool) (s:'state) (0:num) = s) 538 /\ (Nf5 R P s (SUC n) = @r. R(Nf5 R P s n,r) /\ P r)`; 539 540val P4_def = Define `P4 R P s s' = R(s,s') /\ P s'`; 541val P5_def = Define `P5 R P s n s' = R(Nf5 R P s n,s') /\ P s'`; 542val P6_def = Define `P6 R P s n s' = R((@r. P5 R P s n r),s') /\ P s'`; 543 544val GFP_CLOSURE_IMP_EG_LEM1a = prove(``!(P:'state ->bool) Q (R:'state # 'state -> bool) s. (!s. P s = Q s /\ ?s'. R(s,s') /\ P s') /\ P s 545==> (!n. P (Nf5 R P s n) ==> Q(Nf5 R P s n) /\ R(Nf5 R P s n,Nf5 R P s (SUC n)) /\ P (Nf5 R P s (SUC n)))``, 546REPEAT GEN_TAC THEN STRIP_TAC 547THEN Induct_on `n` THENL [ 548STRIP_TAC 549THEN CONJ_TAC THENL [ 550 ASSUM_LIST PROVE_TAC, 551 UNDISCH_TAC ``(P :'state -> bool) (Nf5 (R :'state # 'state -> bool) (P:'state -> bool) (s:'state) (0 :num))`` 552 THEN SIMP_TAC std_ss [Nf5_def] 553 THEN STRIP_TAC 554 THEN REWRITE_TAC [GSYM P4_def] 555 THEN REWRITE_TAC [SELECT_THM] 556 THEN REWRITE_TAC [P4_def] 557 THEN ASSUM_LIST PROVE_TAC], (* conj, 0 *) 558 REWRITE_TAC [Nf5_def] 559 THEN STRIP_TAC 560 THEN CONJ_TAC THENL [ 561 ASSUM_LIST PROVE_TAC, 562 REWRITE_TAC [GSYM P5_def] 563 THEN REWRITE_TAC [GSYM P6_def] 564 THEN REWRITE_TAC [SELECT_THM] 565 THEN REWRITE_TAC [P5_def,P6_def] 566 THEN ASSUM_LIST PROVE_TAC]]); (* conj, SUC *) 567 568val GFP_CLOSURE_IMP_EG_LEM1 = prove(``!(P:'state ->bool) Q (R:'state # 'state -> bool) s. (!s. P s = Q s /\ ?s'.R(s,s') /\ P s') /\ P s 569 ==> ?(f:num->'state). (f(0) = s) /\ !n. R(f n,f (SUC n)) /\ P(f n)``, 570REPEAT STRIP_TAC 571THEN EXISTS_TAC ``Nf5 (R:'state # 'state -> bool) (P:'state ->bool) s`` 572THEN CONJ_TAC THENL [ 573 REWRITE_TAC [Nf5_def], 574 Induct_on `n` THENL [ 575 REWRITE_TAC [Nf5_def] 576 THEN CONJ_TAC THENL [ 577 MATCH_MP_TAC (DECIDE ``((R:'state # 'state -> bool) (s,@r. R (s,r) /\ (P:'state ->bool) r) /\ P(@r. R (s,r) /\ P r)) 578 ==> (R (s,@r. R (s,r) /\ P r))``) 579 THEN REWRITE_TAC [GSYM P4_def] 580 THEN REWRITE_TAC [SELECT_THM] 581 THEN REWRITE_TAC [P4_def] 582 THEN ASSUM_LIST PROVE_TAC, 583 POP_ASSUM (fn t => REWRITE_TAC [t])], (* conj, 0 *) 584 CONJ_TAC THENL [ 585 REWRITE_TAC [Nf5_def] 586 THEN REWRITE_TAC [GSYM P5_def] 587 THEN MATCH_MP_TAC (DECIDE ``((R:'state # 'state -> bool) ((@r. P5 R (P:'state ->bool) s n r),@r. R ((@r. P5 R P s n r),r) /\ P r) 588 /\ P (@r. R ((@r. P5 R P s n r),r) /\ P r)) 589 ==> (R((@r. P5 R P s n r),@r. R ((@r. P5 R P s n r),r) /\ P r))``) 590 THEN REWRITE_TAC [GSYM P6_def] 591 THEN REWRITE_TAC [SELECT_THM] 592 THEN REWRITE_TAC [P5_def,P6_def] 593 THEN REWRITE_TAC [GSYM (List.last(CONJUNCTS Nf5_def))] 594 THEN POP_ASSUM (fn t => `P (Nf5 (R:'state # 'state -> bool) (P:'state ->bool) s (SUC n))` 595 by PROVE_TAC [List.last(CONJUNCTS t),GFP_CLOSURE_IMP_EG_LEM1a]) 596 THEN ASSUM_LIST PROVE_TAC, 597 IMP_RES_TAC GFP_CLOSURE_IMP_EG_LEM1a 598 THEN ASSUM_LIST PROVE_TAC] (* conj *)] (* SUC *)] (* conj *)); 599 600val GFP_CLOSURE_IMP_EG_LEM3 = prove(``!(P:'state ->bool) Q (R:'state # 'state -> bool) s. (!s. P s = Q s /\ ?s'.R(s,s') /\ P s') /\ P s 601 ==> ?(f:num->'state). (f(0) = s) /\ !n. R(f n,f (SUC n)) /\ Q(f n)``, 602REPEAT STRIP_TAC 603THEN IMP_RES_TAC GFP_CLOSURE_IMP_EG_LEM1 604THEN ASSUM_LIST (fn t => PROVE_TAC ( GFP_CLOSURE_IMP_EG_LEM2::t))); 605 606val GFP_CLOSURE_IMP_EG_LEM = prove (``!(f: 'prop ctl) (s:'state) (M: ('prop,'state) kripke_structure). 607((C_SEM M f = MU_SAT (CTL2MU f) (ctl2muks M) EMPTY_ENV) /\ wfKS (ctl2muks M) /\ FINITE (ctl2muks M).S 608 /\ (!(f: 'prop ctl). IMF (CTL2MU f))) /\ 609(s IN BIGINTER {P | ?i. P = GFP M f i}) ==> ?p. PATH M p s /\ !n::0 to PLENGTH p. C_SEM M f (ELEM p n)``, 610REPEAT STRIP_TAC 611THEN `!(s :'state). s IN BIGINTER {(P :'state -> bool) | ?(i :num). P = GFP M f i} 612 = C_SEM M f s /\ ?(s' :'state). M.R (s,s') /\ s' IN BIGINTER {P | ?(i :num). P = GFP M f i}` 613 by (POP_ASSUM (fn t => ALL_TAC) THEN IMP_RES_TAC CTL_GFP_CLOSURE) 614THEN POP_ASSUM (fn t => ASSUME_TAC (SIMP_RULE std_ss [IN_DEF] t)) 615THEN `!(s :'state). BIGINTER {P | ?i. P = GFP M f i} s ==> 616 ?f'. (f' 0 = s) /\ !n. M.R (f' n,f' (SUC n)) /\ C_SEM M f (f' n)` by IMP_RES_TAC GFP_CLOSURE_IMP_EG_LEM3 617THEN PAT_ASSUM ``(s :'state) IN BIGINTER {P | ?i. P = GFP M f i}`` (fn t => POP_ASSUM (fn t' => 618 ASSUME_TAC (MATCH_MP t' (SIMP_RULE std_ss [IN_DEF] t)))) 619THEN POP_ASSUM (fn t => POP_ASSUM_LIST (fn t => ALL_TAC) THEN ASSUME_TAC t) 620THEN FULL_SIMP_TAC std_ss [] 621THEN EXISTS_TAC ``INFINITE (f':num->'state)`` 622THEN POP_ASSUM (fn t => ASSUME_TAC ((CONV_RULE unwindLib.FORALL_CONJ_CONV) t)) 623THEN FULL_SIMP_TAC resq_ss [PATH_def,PLENGTH_def,xnum_to_def,IN_DEF] 624THEN FULL_SIMP_TAC arith_ss [ELEM_def,RESTN_INFINITE,HEAD_def,IS_INFINITE_def,DECIDE ``SUC n = n + 1``]); 625 626val CTL_GFP_SUBSET_EG = prove(``!(f: 'prop ctl) (M: ('prop,'state) kripke_structure). 627((C_SEM M f = MU_SAT (CTL2MU f) (ctl2muks M) EMPTY_ENV) /\ wfKS (ctl2muks M) /\ FINITE (ctl2muks M).S 628 /\ (!(f: 'prop ctl). IMF (CTL2MU f))) 629==> BIGINTER {P | ?i. P = GFP M f i} SUBSET C_SEM M (C_EG f)``, 630REPEAT STRIP_TAC THEN REWRITE_TAC [SUBSET_DEF] 631THEN GEN_TAC THEN SPEC_TAC (``x:'state``,``s:'state``) THEN GEN_TAC 632THEN SIMP_TAC std_ss [IN_DEF,C_SEM_def] 633THEN IMP_RES_TAC GFP_CLOSURE_IMP_EG_LEM 634THEN FULL_SIMP_TAC std_ss [IN_DEF]); 635 636val CTL_LFP = Define ` 637(LFP (M: ('prop,'state) kripke_structure) (f: 'prop ctl) (g:'prop ctl) (0:num) = ({}:'state -> bool)) /\ 638(LFP M f g (SUC n) = C_SEM M g UNION (C_SEM M f INTER {s | ?s'. M.R(s,s') /\ s' IN LFP M f g n}))`; 639 640val CTL_LFP_EQ_CTL2MU_LFP = prove(``!(f: 'prop ctl) (g: 'prop ctl) (s:'state) (M: ('prop,'state) kripke_structure). 641 ((C_SEM M f = MU_SAT (CTL2MU f) (ctl2muks M) EMPTY_ENV) 642 /\ (C_SEM M g = MU_SAT (CTL2MU g) (ctl2muks M) EMPTY_ENV) /\ (wfKS (ctl2muks M))) 643 ==> (BIGUNION {P | ?i. P = LFP M f g i} 644 = BIGUNION {P | ?i. P = FP ((CTL2MU g) \/ ((CTL2MU f) /\ <<".">> (RV "Q"))) "Q" (ctl2muks M) EMPTY_ENV[[["Q"<--{}]]] i})``, 645REPEAT STRIP_TAC 646THEN MATCH_MP_TAC BIGUNION_LEMMA1 647THEN Induct_on `n` THENL [ 648 FULL_SIMP_TAC std_ss [CTL_LFP,STATES_def,ENV_EVAL,ctl2muks_def], (* 0 *) 649 REWRITE_TAC [CTL_LFP] 650 THEN ONCE_REWRITE_TAC [STATES_def] THEN ONCE_REWRITE_TAC [STATES_def] THEN ONCE_REWRITE_TAC [STATES_def] 651 THEN REWRITE_TAC [ STATES_FV_ENV_INV_SPEC,ENV_UPDATE] 652 THEN ONCE_REWRITE_TAC [STATES_def] THEN ONCE_REWRITE_TAC [STATES_def] 653 THEN FULL_SIMP_TAC std_ss [KS_TRANSITION_def,wfKS_def] 654 THEN FULL_SIMP_TAC std_ss [ctl2muks_def,KS_accfupds,KS_accessors,KS_fn_updates] 655 THEN FULL_SIMP_TAC std_ss [ENV_EVAL,IN_UNIV] 656 THEN REWRITE_TAC [SET_SPEC] 657 THEN SIMP_TAC std_ss [UNION_DEF,INTER_DEF,SET_SPEC] 658 THEN ONCE_REWRITE_TAC [EXTENSION] 659 THEN SIMP_TAC std_ss [SET_SPEC] 660 THEN SIMP_TAC std_ss [IN_DEF,MU_SAT_def]]); 661 662val FIN_PFX_def = Define ` 663(FIN_PFX l 0 = []) /\ 664(FIN_PFX l (SUC n) = (HD l)::(FIN_PFX (TL l) n))`; 665 666val INF_PFX_def = Define ` 667(INF_PFX f 0 = []) /\ 668(INF_PFX f (SUC n) = SNOC (f n) (INF_PFX f n))`; 669 670val PREFIX_def = Define ` 671(PREFIX (FINITE l) n = FIN_PFX l n) /\ 672(PREFIX (INFINITE f) n = INF_PFX f n)`; 673 674val INF_PREFIX_LENGTH = save_thm("INF_PREFIX_LENGTH",prove(``!f k. LENGTH (PREFIX (INFINITE f) k) = k``, 675REWRITE_TAC [PREFIX_def] 676THEN Induct_on `k` THENL [ 677REWRITE_TAC [INF_PFX_def,LENGTH,SNOC], 678REWRITE_TAC [INF_PFX_def] 679THEN FULL_SIMP_TAC arith_ss [LENGTH,SNOC,LENGTH_SNOC]])); 680 681val IDX_BIGUNION = save_thm("IDX_BIGUNION",prove(``!P s. s IN BIGUNION {p | ?i. p = P i} = ?i. s IN P i``, 682SIMP_TAC std_ss [BIGUNION,SET_SPEC] THEN PROVE_TAC [])); 683 684val CTL_LFP_LEM = prove(``!(f: 'prop ctl) (g: 'prop ctl) (s:'state) (M: ('prop,'state) kripke_structure). 685C_SEM M (C_EU(f,g)) s ==> s IN BIGUNION {P | ?(i:num). P = LFP M f g i}``, 686CONV_TAC (STRIP_QUANT_CONV (LAND_CONV (REWRITE_CONV [C_SEM_def,IN_DEF]))) THEN BETA_TAC THEN REPEAT STRIP_TAC 687THEN Induct_on `p` THENL [ 688 SIMP_TAC std_ss [PATH_def,IS_INFINITE_def], 689 GEN_TAC 690 THEN CONV_TAC (RAND_CONV (RATOR_CONV (SIMP_CONV resq_ss [IN_DEF,PLENGTH_def,xnum_to_def]))) 691 THEN SIMP_TAC arith_ss [] 692 THEN SPEC_TAC (``INFINITE (f':num->'state)``,``p:'state path``) 693 THEN REPEAT STRIP_TAC 694 THEN UNDISCH_TAC ``!(j :num). j < (k :num) ==> C_SEM (M :('prop,'state) kripke_structure) (f :'prop ctl) (ELEM (p :'state path) j)`` 695 THEN UNDISCH_TAC `` C_SEM (M :('prop,'state) kripke_structure) (g :'prop ctl) (ELEM (p :'state path) (k :num))`` 696 THEN UNDISCH_TAC ``PATH (M :('prop,'state) kripke_structure) (p :'state path) (s :'state)`` 697 THEN SPEC_TAC (``s:'state``,``s:'state``) 698 THEN Induct_on `LENGTH (PREFIX (p:'state path) (k:num))` THENL [ 699 REPEAT STRIP_TAC 700 THEN REWRITE_TAC [IDX_BIGUNION] 701 THEN EXISTS_TAC ``SUC 0`` 702 THEN FULL_SIMP_TAC std_ss [PATH_def,UNION_DEF,CTL_LFP,SET_SPEC] 703 THEN DISJ1_TAC 704 THEN Induct_on `p` THENL [ 705 FULL_SIMP_TAC std_ss [PATH_def,IS_INFINITE_def], 706 FULL_SIMP_TAC std_ss [INF_PREFIX_LENGTH]] 707 THEN ASSUM_LIST (fn t => PROVE_TAC (IN_DEF::t)), (* basis case *) 708 REPEAT STRIP_TAC 709 THEN PAT_ASSUM ``!p k. t`` (fn t => ASSUME_TAC ( SPECL [``REST (p: 'state path)``,``(k:num)-1``] t )) 710 THEN Cases_on `k=0` THENL [ 711 REPEAT STRIP_TAC 712 THEN REWRITE_TAC [IDX_BIGUNION] 713 THEN EXISTS_TAC ``SUC 0`` 714 THEN FULL_SIMP_TAC std_ss [PATH_def,UNION_DEF,CTL_LFP,SET_SPEC] 715 THEN DISJ1_TAC 716 THEN Induct_on `p` THENL [ 717 FULL_SIMP_TAC std_ss [PATH_def,IS_INFINITE_def], 718 FULL_SIMP_TAC std_ss [INF_PREFIX_LENGTH]] 719 THEN ASSUM_LIST (fn t => PROVE_TAC (IN_DEF::t)), (* k = 0 *) 720 Induct_on `p` THENL [ 721 SIMP_TAC std_ss [PATH_def,IS_INFINITE_def], 722 SIMP_TAC std_ss [INF_PREFIX_LENGTH,REST_INFINITE] 723 THEN REWRITE_TAC [GSYM REST_INFINITE] 724 THEN GEN_TAC 725 THEN SPEC_TAC (``INFINITE (f':num->'state)``,``p:'state path``) 726 THEN REPEAT STRIP_TAC 727 THEN IMP_RES_TAC (SIMP_RULE std_ss [] (ARITH_CONV ``~(k=0) /\ (SUC v = k) ==> (v = k - 1)``)) 728 THEN RES_TAC 729 THEN PAT_ASSUM ``((v:num)=k-1)==>t`` (fn t => ALL_TAC) 730 THEN PAT_ASSUM ``(v:num)= k - 1`` (fn t => PAT_ASSUM ``SUC v = k`` (fn t => ALL_TAC)) 731 THEN POP_ASSUM (fn t => ASSUME_TAC (SPEC ``ELEM (p:'state path) 1`` t)) 732 THEN FULL_SIMP_TAC std_ss [ELEM_REST] 733 THEN IMP_RES_TAC PATH_REST 734 THEN RES_TAC 735 THEN PAT_ASSUM ``PATH x y z ==> t`` (fn t => ALL_TAC) 736 THEN PAT_ASSUM ``PATH M (REST (p:'state path)) (ELEM p 1)`` (fn t => ALL_TAC) 737 THEN FULL_SIMP_TAC std_ss [DECIDE ``~((k:num)=0) = (k-1+1=k)``] 738 THEN PAT_ASSUM ``(k:num) - 1 + 1 = k`` (fn t => FULL_SIMP_TAC std_ss [t] THEN ASSUME_TAC t) 739 THEN FULL_SIMP_TAC std_ss [SYM (DECIDE ``~((k:num)=0) = (k-1+1=k)``)] 740 THEN RES_TAC 741 THEN PAT_ASSUM ``C_SEM x y z ==> t`` (fn t => ALL_TAC) 742 THEN SUBGOAL_THEN ``(!j. j < (k:num) - 1 743 ==> C_SEM (M: ('prop,'state) kripke_structure) f (ELEM (p:'state path) (j + 1)))`` ASSUME_TAC THENL [ 744 GEN_TAC 745 THEN IMP_RES_TAC (DECIDE ``~((k:num)=0) ==> (j<k-1 = j+1<k)``) 746 THEN POP_ASSUM (fn _ => POP_ASSUM (fn _ => POP_ASSUM (fn t => REWRITE_TAC [t]))) 747 THEN ASM_REWRITE_TAC [], (* subgoal *) 748 RES_TAC 749 THEN PAT_ASSUM ``x ==> y`` (fn t => ALL_TAC) 750 THEN PAT_ASSUM ``!(j:num). j < (k:num) - 1 ==> C_SEM M f (ELEM (p:'state path) (j + 1))`` (fn t => ALL_TAC) 751 THEN FULL_SIMP_TAC std_ss [PATH_def] 752 THEN PAT_ASSUM ``!(j:num). j < (k:num)==> C_SEM M f (ELEM (p:'state path) j)`` 753 (fn t => ASSUME_TAC (SPEC ``0:num`` t) THEN ASSUME_TAC t) 754 THEN PAT_ASSUM ``ELEM (p:'state path) 0 = s`` (fn t => PAT_ASSUM `` 0 < (k:num) ==> C_SEM M f (ELEM p 0)`` (fn t' => 755 ASSUME_TAC (REWRITE_RULE [t] t') THEN ASSUME_TAC t)) 756 THEN FULL_SIMP_TAC std_ss [DECIDE ``~((k:num)=0) = 0 < k``] 757 THEN RES_TAC 758 THEN FULL_SIMP_TAC std_ss [SYM (DECIDE ``~((k:num)=0) = 0 < k``)] 759 THEN PAT_ASSUM ``T`` (fn _ => POP_ASSUM (fn _ => ALL_TAC)) 760 THEN FULL_SIMP_TAC std_ss [IDX_BIGUNION] 761 THEN EXISTS_TAC ``SUC i`` 762 THEN FULL_SIMP_TAC std_ss [PATH_def,UNION_DEF,CTL_LFP,SET_SPEC,INTER_DEF] 763 THEN DISJ2_TAC 764 THEN CONJ_TAC THENL [ 765 FULL_SIMP_TAC std_ss [IN_DEF], 766 EXISTS_TAC ``ELEM (p:'state path) 1`` 767 THEN PAT_ASSUM ``ELEM (p:'state path) 0 = s`` (fn t => REWRITE_TAC [SYM t]) 768 THEN ASM_REWRITE_TAC [] 769 THEN ONCE_REWRITE_TAC [DECIDE ``(1:num) = 0+1``] 770 THEN ASSUM_LIST PROVE_TAC]]]]]]); 771 772val CTL2MU_LEM = prove(``!(f: 'prop ctl) (M: ('prop,'state) kripke_structure). 773 ((!(f: 'prop ctl). IMF (CTL2MU f)) /\ TOTAL M.R /\ wfKS (ctl2muks M) /\ FINITE (ctl2muks M).S) ==> 774 (C_SEM M f = MU_SAT (CTL2MU f) (ctl2muks M) EMPTY_ENV)``, 775REWRITE_TAC [FUN_EQ_THM] 776THEN CONV_TAC (STRIP_QUANT_CONV (RIGHT_IMP_FORALL_CONV)) 777THEN CONV_TAC (QUANT_CONV SWAP_VARS_CONV) 778THEN CONV_TAC SWAP_VARS_CONV 779THEN ONCE_REWRITE_TAC [GEN_ALPHA_CONV ``s:'state`` `` !(x :'state) (f :'prop ctl) (M :('prop,'state) kripke_structure). 780 (!(f :'prop ctl). IMF (CTL2MU f)) /\ (TOTAL :('state # 'state -> bool) -> bool) M.R /\ wfKS (ctl2muks M) /\ FINITE (ctl2muks M).S 781 ==> (C_SEM M f x = MU_SAT (CTL2MU f) (ctl2muks M) EMPTY_ENV x)``] 782THEN CONV_TAC SWAP_VARS_CONV 783THEN recInduct (theorem "CTL2MU_ind") THEN REPEAT CONJ_TAC THENL [ 784SIMP_TAC std_ss [MU_SAT_def,STATES_def,CTL2MU_def,BEXP2MU_def,C_SEM_def,B_SEM_def] 785THEN recInduct (theorem "BEXP2MU_ind") THEN REPEAT CONJ_TAC THENL [ 786FULL_SIMP_TAC std_ss [ctl2muks_def,KS_accfupds,KS_accessors,KS_fn_updates,B_SEM_def,BEXP2MU_def,STATES_def,wfKS_def,IN_UNIV,SET_SPEC], 787FULL_SIMP_TAC std_ss [ctl2muks_def,KS_accfupds,KS_accessors,KS_fn_updates] 788THEN FULL_SIMP_TAC std_ss [B_SEM_def,BEXP2MU_def,STATES_def,ctl2muks_def,wfKS_def] 789THEN FULL_SIMP_TAC std_ss [ctl2muks_def,KS_accfupds,KS_accessors,KS_fn_updates] 790THEN FULL_SIMP_TAC std_ss [SET_SPEC] 791THEN PROVE_TAC [IN_UNIV], 792FULL_SIMP_TAC std_ss [ctl2muks_def,KS_accfupds,KS_accessors,KS_fn_updates,B_SEM_def,BEXP2MU_def,STATES_def,wfKS_def,IN_UNIV,DIFF_DEF,SET_SPEC], 793FULL_SIMP_TAC std_ss [ctl2muks_def,KS_accfupds,KS_accessors,KS_fn_updates,B_SEM_def,BEXP2MU_def,STATES_def,wfKS_def,IN_UNIV,INTER_DEF,SET_SPEC]], (* C_BOOL *) 794FULL_SIMP_TAC std_ss [ctl2muks_def,KS_accfupds,KS_accessors,KS_fn_updates,B_SEM_def,BEXP2MU_def,STATES_def,wfKS_def,IN_UNIV,DIFF_DEF, 795 SET_SPEC,MU_SAT_def,STATES_def,CTL2MU_def,C_SEM_def,B_SEM_def], (* C_NOT *) 796FULL_SIMP_TAC std_ss [ctl2muks_def,KS_accfupds,KS_accessors,KS_fn_updates,B_SEM_def,BEXP2MU_def,STATES_def,wfKS_def,IN_UNIV,INTER_DEF, 797 SET_SPEC,MU_SAT_def,STATES_def,CTL2MU_def,C_SEM_def,B_SEM_def], (* C_AND *) 798FULL_SIMP_TAC std_ss [MU_SAT_def,STATES_def,CTL2MU_def,BEXP2MU_def,C_SEM_def,B_SEM_def] 799THEN CONV_TAC (STRIP_QUANT_CONV (RAND_CONV (STRIP_QUANT_CONV (RAND_CONV (LHS_CONV(STRIP_QUANT_CONV (RAND_CONV(RATOR_CONV (REWRITE_CONV [IN_DEF]))))))))) 800THEN BETA_TAC 801THEN REPEAT STRIP_TAC 802THEN FULL_SIMP_TAC std_ss [wfKS_def,KS_TRANSITION_def] 803THEN FULL_SIMP_TAC std_ss [ctl2muks_def,KS_accfupds,KS_accessors,KS_fn_updates] 804THEN FULL_SIMP_TAC std_ss [SET_SPEC,IN_UNIV] 805THEN FULL_SIMP_TAC std_ss [PATH_def] 806THEN EQ_TAC THENL [ 807 CONV_TAC LEFT_IMP_EXISTS_CONV 808 THEN GEN_TAC THEN 809 CONV_TAC RIGHT_IMP_EXISTS_CONV 810 THEN EXISTS_TAC ``ELEM (p:'state path) ((0:num)+1)`` 811 THEN REPEAT STRIP_TAC THENL [ 812 PAT_ASSUM ``ELEM (p:'state path) 0 = s`` (fn t => ONCE_REWRITE_TAC [SYM t]) 813 THEN PAT_ASSUM ``!n. (M: ('prop,'state) kripke_structure).R (ELEM (p:'state path) n,ELEM p (n + 1))`` 814 (fn t => ASSUME_TAC (SPEC ``0:num`` t)) 815 THEN FULL_SIMP_TAC arith_ss [], 816 FULL_SIMP_TAC std_ss []], (* ==> *) 817 CONV_TAC LEFT_IMP_EXISTS_CONV 818 THEN GEN_TAC THEN 819 CONV_TAC RIGHT_IMP_EXISTS_CONV 820 THEN EXISTS_TAC ``INFINITE (Nf (M: ('prop,'state) kripke_structure).R s q)`` 821 THEN REPEAT STRIP_TAC THENL [ 822 REWRITE_TAC [IS_INFINITE_def], (* INFINITE p *) 823 SIMP_TAC std_ss [ELEM_def,RESTN_def,REST_def,HEAD_def,listTheory.HD,Nf], (* ELEM p 0 = s *) 824 ONCE_REWRITE_TAC [DECIDE ``n+1=SUC n``] 825 THEN Induct_on `n` THENL [ 826 SIMP_TAC arith_ss [Nf,ELEM_def,RESTN_def,REST_def,HEAD_def,listTheory.HD,listTheory.TL, 827 PLENGTH_def,GT_xnum_num_def,listTheory.LENGTH] 828 THEN REWRITE_TAC [Nf,DECIDE ``1=SUC 0``] 829 THEN ASM_REWRITE_TAC [], (* 0 *) 830 FULL_SIMP_TAC arith_ss [ELEM_def,RESTN_INFINITE,HEAD_def,TOTAL_def,Nf] 831 THEN PAT_ASSUM ``!s. ?s'. (M: ('prop,'state) kripke_structure).R (s,s')`` 832 (fn t => ASSUME_TAC (SPEC ``(if n = 0 then q else @r. (M: ('prop,'state) kripke_structure).R (Nf M.R s q n,r))`` t)) 833 THEN FULL_SIMP_TAC std_ss [unc_thm] 834 THEN REWRITE_TAC [SELECT_THM] 835 THEN ASSUM_LIST PROVE_TAC], (* SUC n *) 836 REWRITE_TAC [ELEM_def] THEN ONCE_REWRITE_TAC [DECIDE ``1 = SUC 0``] 837 THEN REWRITE_TAC [Nf,ELEM_def,RESTN_def,REST_def,HEAD_def,listTheory.HD,listTheory.TL,DECIDE ``1 = SUC 0``] 838 THEN SIMP_TAC arith_ss [] THEN REWRITE_TAC [DECIDE ``1=SUC 0``] THEN REWRITE_TAC [Nf] 839 THEN ASM_REWRITE_TAC []]], (* <== *) (* C_EX *) 840REPEAT STRIP_TAC 841THEN EQ_TAC THENL [ 842 FULL_SIMP_TAC std_ss [MU_SAT_def,STATES_def,CTL2MU_def,BEXP2MU_def,SET_SPEC,IN_UNIV] 843 THEN CONV_TAC RIGHT_IMP_FORALL_CONV 844 THEN SPEC_TAC (``s:'state``,``s:'state``) 845 THEN CONV_TAC (SWAP_VARS_CONV) 846 THEN CONV_TAC (STRIP_QUANT_CONV (LAND_CONV (ONCE_REWRITE_CONV [GSYM (prove(``!x P. x IN P = P x``,PROVE_TAC [IN_DEF]))]))) 847 THEN REWRITE_TAC [GSYM SUBSET_DEF] 848 THEN Induct_on `n` THENL [ 849 FULL_SIMP_TAC std_ss [ctl2muks_def,KS_accfupds,KS_accessors,KS_fn_updates,STATES_def,ENV_EVAL,SUBSET_UNIV,wfKS_def,ctl2muks_def,SET_SPEC,IN_UNIV], (* 0 *) 850 PAT_ASSUM ``!(f:'prop ctl). IMF (CTL2MU f)`` (fn t => ASSUME_TAC (REWRITE_RULE [CTL2MU_def] (SPEC ``C_EG (f:'prop ctl)`` t))) 851 THEN IMP_RES_TAC (REWRITE_RULE [IMF_MU_IFF_IMF_NU] STATES_MONO_EQ) 852 THEN POP_ASSUM (fn t => ASSUME_TAC (ISPEC ``EMPTY_ENV:string -> 'state -> bool`` t)) 853 THEN ONCE_REWRITE_TAC [STATES_def] 854 THEN REWRITE_TAC [ENV_UPDATE] 855 THEN POP_ASSUM (fn t => ASSUME_TAC ((CONV_RULE (LAND_CONV (ONCE_REWRITE_CONV [STATES_def]))) t)) 856 THEN IMP_RES_TAC CTL2MU_EG_LEM 857 THEN POP_ASSUM (fn t=> FULL_SIMP_TAC std_ss [SPEC ``f: 'prop ctl`` t]) 858 THEN FULL_SIMP_TAC std_ss [STATES_FV_ENV_INV_SPEC] 859 THEN RES_TAC 860 THEN POP_ASSUM (fn t => ALL_TAC) 861 THEN POP_ASSUM (fn t => ALL_TAC) 862 THEN POP_ASSUM (fn t => ASSUME_TAC (REWRITE_RULE [GSYM FUN_EQ_THM] (SIMP_RULE std_ss [IN_DEF] t))) 863 THEN POP_ASSUM (fn t => FULL_SIMP_TAC std_ss [SYM t]) 864 THEN FULL_SIMP_TAC std_ss [GSYM CTL2MU_AND_LEM, 865 REWRITE_RULE [GSYM FUN_EQ_THM] 866 (GENL [``(M: ('prop,'state) kripke_structure)``,``f:'prop ctl``] EG_LEMMA)]], (* SUC,==>*) 867 RES_TAC 868 THEN POP_ASSUM (fn t => ALL_TAC) 869 THEN POP_ASSUM (fn t => ALL_TAC) 870 THEN POP_ASSUM (fn t => ASSUME_TAC (REWRITE_RULE [GSYM FUN_EQ_THM] (SIMP_RULE std_ss [IN_DEF] t))) 871 THEN REWRITE_TAC [MU_SAT_def] 872 THEN REWRITE_TAC [CTL2MU_def] 873 THEN IMP_RES_TAC NU_BIGINTER 874 THEN POP_ASSUM (fn t => REWRITE_TAC [t]) 875 THEN IMP_RES_TAC CTL_GFP_EQ_CTL2MU_GFP 876 THEN POP_ASSUM (fn t => REWRITE_TAC [SYM t]) 877 THEN IMP_RES_TAC CTL_GFP_SUBSET_EG 878 THEN POP_ASSUM (fn t => ASSUME_TAC (SIMP_RULE std_ss [SUBSET_DEF,IN_DEF] t)) 879 THEN FULL_SIMP_TAC std_ss [IN_DEF]], (* <==,EG *) 880REPEAT STRIP_TAC 881THEN EQ_TAC THENL [ 882 FULL_SIMP_TAC std_ss [MU_SAT_def,MU_BIGUNION,CTL2MU_def,BEXP2MU_def,SET_SPEC,IN_UNIV] 883 THEN RES_TAC 884 THEN PAT_ASSUM ``!s. t ==> t'`` (fn t => ALL_TAC) 885 THEN PAT_ASSUM ``!s. t ==> t'`` (fn t => ALL_TAC) 886 THEN PAT_ASSUM ``!s. t ==> t'`` (fn t => ALL_TAC) 887 THEN PAT_ASSUM ``!s. t ==> t'`` (fn t => ALL_TAC) 888 THEN PAT_ASSUM ``!s. C_SEM M g s = s IN STATES (CTL2MU g) (ctl2muks M) EMPTY_ENV`` 889 (fn t=> ASSUME_TAC (SIMP_RULE std_ss [GSYM MU_SAT_def] t)) 890 THEN POP_ASSUM (fn t=> ASSUME_TAC (REWRITE_RULE [GSYM FUN_EQ_THM] t)) 891 THEN PAT_ASSUM ``!s. C_SEM M f s = s IN STATES (CTL2MU f) (ctl2muks M) EMPTY_ENV`` 892 (fn t=> ASSUME_TAC (SIMP_RULE std_ss [GSYM MU_SAT_def] t)) 893 THEN POP_ASSUM (fn t=> ASSUME_TAC (REWRITE_RULE [GSYM FUN_EQ_THM] t)) 894 THEN `BIGUNION {P | ?i. P = LFP M f g i} 895 = BIGUNION {P | ?i. P = FP (CTL2MU g \/ CTL2MU f /\ <<".">> (RV "Q")) "Q" (ctl2muks M) EMPTY_ENV[[["Q"<--{}]]] i}` 896 by IMP_RES_TAC CTL_LFP_EQ_CTL2MU_LFP 897 THEN POP_ASSUM (fn t => REWRITE_TAC [SYM t]) 898 THEN REWRITE_TAC [CTL_LFP_LEM], (* ==> *) 899 FULL_SIMP_TAC std_ss [MU_SAT_def,STATES_def,CTL2MU_def,BEXP2MU_def,SET_SPEC,IN_UNIV] 900 THEN CONV_TAC LEFT_IMP_EXISTS_CONV 901 THEN SPEC_TAC (``s:'state``,``s:'state``) 902 THEN CONV_TAC (SWAP_VARS_CONV) 903 THEN CONV_TAC (STRIP_QUANT_CONV (RAND_CONV (ONCE_REWRITE_CONV [GSYM (prove(``!x P. x IN P = P x``,PROVE_TAC [IN_DEF]))]))) 904 THEN REWRITE_TAC [GSYM SUBSET_DEF] 905 THEN Induct_on `n` THENL [ 906 REWRITE_TAC [STATES_def,ENV_EVAL,EMPTY_SUBSET], (* 0 *) 907 PAT_ASSUM ``!(f:'prop ctl). IMF (CTL2MU f)`` (fn t => ASSUME_TAC (REWRITE_RULE [CTL2MU_def] (SPEC ``C_EU(f:'prop ctl,g:'prop ctl)`` t))) 908 THEN IMP_RES_TAC STATES_MONO_EQ 909 THEN POP_ASSUM (fn t => ASSUME_TAC (SPEC ``EMPTY_ENV:string -> 'state -> bool`` t)) 910 THEN ONCE_REWRITE_TAC [STATES_def] 911 THEN REWRITE_TAC [ENV_UPDATE] 912 THEN POP_ASSUM (fn t => ASSUME_TAC ((CONV_RULE(RAND_CONV ((ONCE_REWRITE_CONV [STATES_def]) THENC (ONCE_REWRITE_CONV [STATES_def])))) t)) 913 THEN IMP_RES_TAC CTL2MU_EU_LEM 914 THEN POP_ASSUM (fn t=> FULL_SIMP_TAC std_ss [SPECL [``f: 'prop ctl``,``g: 'prop ctl``] t]) 915 THEN FULL_SIMP_TAC std_ss [STATES_FV_ENV_INV_SPEC] 916 THEN RES_TAC 917 THEN POP_ASSUM (fn t => ALL_TAC) 918 THEN POP_ASSUM (fn t => ALL_TAC) 919 THEN PAT_ASSUM ``!s. C_SEM M g s ==> s IN STATES (CTL2MU g) (ctl2muks M) EMPTY_ENV`` (fn t => ALL_TAC) 920 THEN PAT_ASSUM ``!s. s IN STATES (CTL2MU g) (ctl2muks M) EMPTY_ENV ==> C_SEM M g s`` (fn t => ALL_TAC) 921 THEN PAT_ASSUM ``!s. C_SEM M f s = s IN STATES (CTL2MU f) (ctl2muks M) EMPTY_ENV`` 922 (fn t => ASSUME_TAC (REWRITE_RULE [GSYM FUN_EQ_THM] (SIMP_RULE std_ss [IN_DEF] t))) 923 THEN PAT_ASSUM ``!s. C_SEM M g s = s IN STATES (CTL2MU g) (ctl2muks M) EMPTY_ENV`` 924 (fn t => ASSUME_TAC (REWRITE_RULE [GSYM FUN_EQ_THM] (SIMP_RULE std_ss [IN_DEF] t))) 925 THEN POP_ASSUM (fn t => POP_ASSUM (fn t' => FULL_SIMP_TAC std_ss [SYM t,SYM t'])) 926 THEN FULL_SIMP_TAC std_ss [GSYM CTL2MU_AND_LEM,GSYM CTL2MU_OR_LEM, 927 (CONV_RULE (RAND_CONV(REWRITE_CONV [GSYM FUN_EQ_THM]))) 928 ((CONV_RULE FORALL_IMP_CONV) 929 (ISPECL [``(M: ('prop,'state) kripke_structure)``,``f:'prop ctl``,``g:'prop ctl``] 930 EU_LEMMA))]]]]); 931 932val CTL2MU = save_thm("CTL2MU",SIMP_RULE std_ss [IMF_CTL] CTL2MU_LEM); 933 934val CTL2MU_MODEL = save_thm("CTL2MU_MODEL",prove(``!(f: 'prop ctl) (M: ('prop,'state) kripke_structure). 935 (TOTAL M.R /\ wfKS (ctl2muks M) /\ FINITE (ctl2muks M).S) ==> 936 (CTL_MODEL_SAT M f = MU_MODEL_SAT (CTL2MU f) (ctl2muks M) EMPTY_ENV)``, 937REPEAT STRIP_TAC THEN REWRITE_TAC [MU_MODEL_SAT_def,CTL_MODEL_SAT_def] 938THEN CONV_TAC (RHS_CONV (QUANT_CONV (LAND_CONV (REWRITE_CONV[ctl2muks_def])))) 939THEN REWRITE_TAC [combinTheory.K_THM,KS_accfupds] 940THEN METIS_TAC [CTL2MU])) 941 942 943val _ = export_theory(); 944