1open HolKernel Parse boolLib bossLib 2 3val _ = new_theory("cear"); 4 5open envTheory 6open pred_setTheory 7open setLemmasTheory 8open muSyntaxTheory 9open muTheory 10open ksTheory 11open reachTheory 12 13infix &&; infix 8 by; 14val _ = intLib.deprecate_int(); 15fun tsimps ty = let val {convs,rewrs} = TypeBase.simpls_of ty in rewrs end; 16 17val Next_def = Define `Next R s s' = R(s,s')`; 18 19val Prev_def = Define `Prev R s s' = R(s',s)`; 20 21val ReachFromRec_def = Define ` 22 (ReachFromRec R s 0 = {s}) /\ 23 (ReachFromRec R s (SUC n) = {s' | s' IN ReachFromRec R s n \/ ?s''. Next R s'' s' /\ s'' IN ReachFromRec R s n})`; 24 25val ReachFrom_def = Define `ReachFrom R s = BIGUNION {P | ?n. P = ReachFromRec R s n}`; 26 27val ReachToRec_def = Define ` 28 (ReachToRec R s 0 = {s}) /\ 29 (ReachToRec R s (SUC n) = {s' | s' IN ReachToRec R s n \/ ?s''. Prev R s'' s' /\ s'' IN ReachToRec R s n})`; 30 31val ReachTo_def = Define `ReachTo R s = BIGUNION {P | ?n. P = ReachToRec R s n}`; 32 33val ReachFromChain = prove(``!R s n. ReachFromRec R s n SUBSET ReachFromRec R s (SUC n)``, 34Induct_on `n` THENL [ 35SIMP_TAC std_ss [ReachFromRec_def,Next_def,SUBSET_DEF,IN_SING,SET_SPEC], 36FULL_SIMP_TAC std_ss [ReachFromRec_def,Next_def,SUBSET_DEF,SET_SPEC] 37]); 38 39val ReachFromStable =prove(``!R s (n:num). (ReachFromRec R s n = ReachFromRec R s (SUC n)) ==> 40 !m. m >= n ==> (ReachFromRec R s m = ReachFromRec R s n)``, 41REWRITE_TAC [DECIDE ``((m:num)>=n) = ((m=n) \/ (m>n))``] 42THEN REPEAT STRIP_TAC THENL [ 43ASM_REWRITE_TAC [], 44Induct_on `m` THENL [ 45 SIMP_TAC arith_ss [], (* 0 *) 46 REWRITE_TAC [DECIDE ``(SUC m > n)=(m>=n)``] 47 THEN REWRITE_TAC [DECIDE ``(m>=n) = ((m=n) \/ (m>n))``] 48 THEN REPEAT STRIP_TAC THENL [ 49 50 FULL_SIMP_TAC std_ss [], (* m=n *) 51 FULL_SIMP_TAC std_ss [] 52 THEN SIMP_TAC std_ss [ReachFromRec_def,Next_def,SET_SPEC] 53 THEN ASM_REWRITE_TAC []]]]); 54 55val ReachFromChainUnion = prove(``!R s n'. BIGUNION {P | ?n. n <= n' /\ (P = ReachFromRec R s n)} = ReachFromRec R s n'``, 56REPEAT STRIP_TAC 57THEN Induct_on `n'` THENL [ 58 REWRITE_TAC [DECIDE ``!n. n<=0 = (n=0)``] 59 THEN REWRITE_TAC [BIGUNION] 60 THEN SIMP_TAC std_ss [SET_SPEC] 61 THEN SIMP_TAC std_ss [SET_SPEC,EXTENSION], (* 0 *) 62 REWRITE_TAC [DECIDE ``!n n'. n<=(SUC n') = (n<=n' \/ (n=SUC n'))``] 63 THEN REWRITE_TAC [DECIDE ``!a b c.((a\/b)/\c)=((a/\c)\/(b/\c))``] 64 THEN SIMP_TAC std_ss [EXISTS_OR_THM] 65 THEN SIMP_TAC std_ss [GSYM (SIMP_RULE std_ss [IN_DEF] UNION_DEF)] 66 THEN SIMP_TAC std_ss [BIGUNION_UNION] 67 THEN FULL_SIMP_TAC std_ss [SET_GSPEC] 68 THEN SIMP_TAC std_ss [BIGUNION,IN_DEF] 69 THEN SIMP_TAC std_ss [SET_GSPEC, ETA_CONV `` (\x. ReachFromRec R s (SUC n') x)``] 70 THEN PROVE_TAC [ReachFromChain,SUBSET_UNION_ABSORPTION]]); 71 72val ReachFromStableSubset = prove(``!R s n'. (ReachFromRec R s n' = ReachFromRec R s (SUC n')) ==> (BIGUNION {P | ?n. n >= n' /\ (P = ReachFromRec R s n)} SUBSET ReachFromRec R s n')``, 73REPEAT STRIP_TAC 74THEN ASSUME_TAC (SPECL [``(R :'a # 'a -> bool)``,``(s :'a)``,``(n' :num)``] ReachFromStable) 75THEN UNDISCH_TAC ``ReachFromRec R s n' = ReachFromRec R s (SUC n')`` 76THEN UNDISCH_TAC ``(ReachFromRec R s n' = ReachFromRec R s (SUC n')) ==> 77 !m. m >= n' ==> (ReachFromRec R s m = ReachFromRec R s n')`` 78THEN SPEC_TAC (``ReachFromRec (R :'a # 'a -> bool) (s :'a)``,``P:num->'a->bool``) 79THEN REPEAT STRIP_TAC 80THEN SIMP_TAC std_ss [BIGUNION,SUBSET_DEF] 81THEN SIMP_TAC std_ss [SET_SPEC] 82THEN ASSUM_LIST PROVE_TAC); 83 84val ReachFromLem1 = prove(``!R s n'. (ReachFromRec R s n' = ReachFromRec R s (SUC n')) ==> 85 (ReachFromRec R s n' UNION BIGUNION {P | ?n. n >= n' /\ (P =ReachFromRec R s n)} = ReachFromRec R s n')``, 86REPEAT GEN_TAC 87THEN ASSUME_TAC (SPEC_ALL ReachFromStableSubset) 88THEN UNDISCH_TAC ``(ReachFromRec R s n' = ReachFromRec R s (SUC n')) ==> 89 BIGUNION {P | ?n. n >= n' /\ (P = ReachFromRec R s n)} SUBSET 90 ReachFromRec R s n'`` 91THEN SPEC_TAC (``ReachFromRec R s``,``P:num -> 'a -> bool``) 92THEN REPEAT STRIP_TAC 93THEN ONCE_REWRITE_TAC [UNION_COMM] 94THEN ASSUM_LIST (fn t => PROVE_TAC (SUBSET_UNION_ABSORPTION::t))); 95 96val ReachFromLem2 = prove(``!R s n'. (ReachFromRec R s n' = ReachFromRec R s (SUC n')) ==> 97 (BIGUNION {P | ?n. n <= n' /\ (P = ReachFromRec R s n)} UNION 98 BIGUNION {P | ?n. n >= n' /\ (P = ReachFromRec R s n)} = 99 ReachFromRec R s n')``, 100REPEAT STRIP_TAC 101THEN ASSUM_LIST (fn t => SIMP_TAC std_ss (ReachFromChainUnion::(tl t))) 102THEN ASSUME_TAC (SPEC_ALL ReachFromLem1) 103THEN UNDISCH_TAC ``ReachFromRec R s n' = ReachFromRec R s (SUC n')`` 104THEN UNDISCH_TAC ``(ReachFromRec R s n' = ReachFromRec R s (SUC n')) ==> 105 (ReachFromRec R s n' UNION 106 BIGUNION {P | ?n. n >= n' /\ (P = ReachFromRec R s n)} = 107 ReachFromRec R s n')`` 108THEN SPEC_TAC (``ReachFromRec R s``,``P:num -> 'a -> bool``) 109THEN ASSUM_LIST PROVE_TAC); 110 111val ReachFromFP = save_thm("ReachFromFP",prove(``!R s n'. (ReachFromRec R s n' = ReachFromRec R s (SUC n')) ==> (ReachFrom R s = ReachFromRec R s n')``, 112REPEAT STRIP_TAC 113THEN ASSUME_TAC (SPEC_ALL ReachFromLem2) 114THEN UNDISCH_TAC ``ReachFromRec R s n' = ReachFromRec R s (SUC n')`` 115THEN UNDISCH_TAC ``(ReachFromRec R s n' = ReachFromRec R s (SUC n')) ==> 116 (BIGUNION {P | ?n. n <= n' /\ (P = ReachFromRec R s n)} UNION 117 BIGUNION {P | ?n. n >= n' /\ (P = ReachFromRec R s n)} = 118 ReachFromRec R s n')`` 119THEN REWRITE_TAC [ReachFrom_def] 120THEN SPEC_TAC (``ReachFromRec R s``,``P:num -> 'a -> bool``) 121THEN REWRITE_TAC [GSYM BIGUNION_SPLIT] 122THEN ASSUM_LIST PROVE_TAC)); 123 124val ReachToChain = prove(``!R s n. ReachToRec R s n SUBSET ReachToRec R s (SUC n)``, 125Induct_on `n` THENL [ 126SIMP_TAC std_ss [ReachToRec_def,Next_def,SUBSET_DEF,IN_SING,SET_SPEC], 127FULL_SIMP_TAC std_ss [ReachToRec_def,Next_def,SUBSET_DEF,SET_SPEC] 128]); 129 130val ReachToStable =prove(``!R s n. (ReachToRec R s n = ReachToRec R s (SUC n)) ==> 131 !m. m >= n ==> (ReachToRec R s m = ReachToRec R s n)``, 132REWRITE_TAC [DECIDE ``(m>=n) = ((m=n) \/ (m>n))``] 133THEN REPEAT STRIP_TAC THENL [ 134ASM_REWRITE_TAC [], 135Induct_on `m` THENL [ 136 SIMP_TAC arith_ss [], (* 0 *) 137 REWRITE_TAC [DECIDE ``(SUC m > n)=(m>=n)``] 138 THEN REWRITE_TAC [DECIDE ``(m>=n) = ((m=n) \/ (m>n))``] 139 THEN REPEAT STRIP_TAC THENL [ 140 FULL_SIMP_TAC std_ss [], (* m=n *) 141 FULL_SIMP_TAC std_ss [] 142 THEN SIMP_TAC std_ss [ReachToRec_def,Prev_def,SET_SPEC] 143 THEN ASM_REWRITE_TAC []]]]); 144 145val ReachToChainUnion = prove(``!R s n'. BIGUNION {P | ?n. n <= n' /\ (P = ReachToRec R s n)} = ReachToRec R s n'``, 146REPEAT STRIP_TAC 147THEN Induct_on `n'` THENL [ 148 REWRITE_TAC [DECIDE ``!n. n<=0 = (n=0)``] 149 THEN REWRITE_TAC [BIGUNION] 150 THEN SIMP_TAC std_ss [SET_SPEC] 151 THEN SIMP_TAC std_ss [SET_SPEC,EXTENSION], (* 0 *) 152 REWRITE_TAC [DECIDE ``!n n'. n<=(SUC n') = (n<=n' \/ (n=SUC n'))``] 153 THEN REWRITE_TAC [DECIDE ``!a b c.((a\/b)/\c)=((a/\c)\/(b/\c))``] 154 THEN SIMP_TAC std_ss [EXISTS_OR_THM] 155 THEN SIMP_TAC std_ss [GSYM (SIMP_RULE std_ss [IN_DEF] UNION_DEF)] 156 THEN SIMP_TAC std_ss [BIGUNION_UNION] 157 THEN FULL_SIMP_TAC std_ss [SET_GSPEC] 158 THEN SIMP_TAC std_ss [BIGUNION,IN_DEF] 159 THEN SIMP_TAC std_ss [SET_GSPEC, ETA_CONV `` (\x. ReachToRec R s (SUC n') x)``] 160 THEN PROVE_TAC [ReachToChain,SUBSET_UNION_ABSORPTION]]); 161 162val ReachToStableSubset = prove(``!R s n'. (ReachToRec R s n' = ReachToRec R s (SUC n')) ==> (BIGUNION {P | ?n. n >= n' /\ (P = ReachToRec R s n)} SUBSET ReachToRec R s n')``, 163REPEAT STRIP_TAC 164THEN ASSUME_TAC (SPECL [``(R :'a # 'a -> bool)``,``(s :'a)``,``(n' :num)``] ReachToStable) 165THEN UNDISCH_TAC ``ReachToRec R s n' = ReachToRec R s (SUC n')`` 166THEN UNDISCH_TAC ``(ReachToRec R s n' = ReachToRec R s (SUC n')) ==> 167 !m. m >= n' ==> (ReachToRec R s m = ReachToRec R s n')`` 168THEN SPEC_TAC (``ReachToRec (R :'a # 'a -> bool) (s :'a)``,``P:num->'a->bool``) 169THEN REPEAT STRIP_TAC 170THEN SIMP_TAC std_ss [BIGUNION,SUBSET_DEF] 171THEN SIMP_TAC std_ss [SET_SPEC] 172THEN ASSUM_LIST PROVE_TAC); 173 174val ReachToLem1 = prove(``!R s n'. (ReachToRec R s n' = ReachToRec R s (SUC n')) ==> 175 (ReachToRec R s n' UNION BIGUNION {P | ?n. n >= n' /\ (P =ReachToRec R s n)} = ReachToRec R s n')``, 176REPEAT GEN_TAC 177THEN ASSUME_TAC (SPEC_ALL ReachToStableSubset) 178THEN UNDISCH_TAC ``(ReachToRec R s n' = ReachToRec R s (SUC n')) ==> 179 BIGUNION {P | ?n. n >= n' /\ (P = ReachToRec R s n)} SUBSET 180 ReachToRec R s n'`` 181THEN SPEC_TAC (``ReachToRec R s``,``P:num -> 'a -> bool``) 182THEN REPEAT STRIP_TAC 183THEN ONCE_REWRITE_TAC [UNION_COMM] 184THEN ASSUM_LIST (fn t => PROVE_TAC (SUBSET_UNION_ABSORPTION::t))); 185 186val ReachToLem2 = prove(``!R s n'. (ReachToRec R s n' = ReachToRec R s (SUC n')) ==> 187 (BIGUNION {P | ?n. n <= n' /\ (P = ReachToRec R s n)} UNION 188 BIGUNION {P | ?n. n >= n' /\ (P = ReachToRec R s n)} = 189 ReachToRec R s n')``, 190REPEAT STRIP_TAC 191THEN ASSUM_LIST (fn t => SIMP_TAC std_ss (ReachToChainUnion::(tl t))) 192THEN ASSUME_TAC (SPEC_ALL ReachToLem1) 193THEN UNDISCH_TAC ``ReachToRec R s n' = ReachToRec R s (SUC n')`` 194THEN UNDISCH_TAC ``(ReachToRec R s n' = ReachToRec R s (SUC n')) ==> 195 (ReachToRec R s n' UNION 196 BIGUNION {P | ?n. n >= n' /\ (P = ReachToRec R s n)} = 197 ReachToRec R s n')`` 198THEN SPEC_TAC (``ReachToRec R s``,``P:num -> 'a -> bool``) 199THEN ASSUM_LIST PROVE_TAC); 200 201val ReachToFP = save_thm("ReachToFP",prove(``!R s n'. (ReachToRec R s n' = ReachToRec R s (SUC n')) ==> (ReachTo R s = ReachToRec R s n')``, 202REPEAT STRIP_TAC 203THEN ASSUME_TAC (SPEC_ALL ReachToLem2) 204THEN UNDISCH_TAC ``ReachToRec R s n' = ReachToRec R s (SUC n')`` 205THEN UNDISCH_TAC ``(ReachToRec R s n' = ReachToRec R s (SUC n')) ==> 206 (BIGUNION {P | ?n. n <= n' /\ (P = ReachToRec R s n)} UNION 207 BIGUNION {P | ?n. n >= n' /\ (P = ReachToRec R s n)} = 208 ReachToRec R s n')`` 209THEN REWRITE_TAC [ReachTo_def] 210THEN SPEC_TAC (``ReachToRec R s``,``P:num -> 'a -> bool``) 211THEN REWRITE_TAC [GSYM BIGUNION_SPLIT] 212THEN ASSUM_LIST PROVE_TAC)); 213 214val R_REFL_def = Define `R_REFL R = !x. R(x,x)`; 215val R_SYM_def = Define `R_SYM R = !x y. R(x,y) = R(y,x)`; 216val R_TRANS_def = Define `R_TRANS R = !x y z. R(x,y) /\ R(y,z) ==> R(x,z)`; 217val R_EQR_def = Define `R_EQR R = R_REFL R /\ R_SYM R /\ R_TRANS R`; 218 219val ReachToClosed = save_thm("ReachToClosed",prove(``!si R s. R_EQR R ==> (s IN ReachTo R si = R(s,si))``, 220REPEAT STRIP_TAC 221THEN SIMP_TAC std_ss [BIGUNION,ReachTo_def,SET_SPEC] 222THEN EQ_TAC THENL [ 223REPEAT STRIP_TAC 224THEN `s IN ReachToRec R si n` by ASSUM_LIST PROVE_TAC 225THEN POP_ASSUM_LIST (fn l => ASSUME_TAC (List.hd l) THEN ASSUME_TAC (List.last l)) 226THEN (SUBGOAL_THEN ``!n (s:'a). s IN ReachToRec R si n ==> R(s,si)`` ASSUME_TAC) THENL [ 227 PAT_ASSUM ``s IN t`` (fn _ => ALL_TAC) 228 THEN Induct_on `n` THENL [ 229 FULL_SIMP_TAC std_ss [ReachToRec_def,IN_SING,R_EQR_def,R_REFL_def], (* 0 *) 230 FULL_SIMP_TAC std_ss [ReachToRec_def,SET_SPEC] 231 THEN RW_TAC std_ss [] THEN RES_TAC 232 THEN PAT_ASSUM ``!x. t`` (fn t => ASSUME_TAC (SPEC ``s'':'a`` t)) 233 THEN FULL_SIMP_TAC std_ss [Prev_def,R_EQR_def,R_TRANS_def] 234 THEN ASSUM_LIST PROVE_TAC 235 ], 236 ASSUM_LIST PROVE_TAC 237 ], (* ==> *) 238DISCH_TAC 239THEN EXISTS_TAC ``ReachToRec (R:'a#'a->bool) si (SUC 0)`` 240THEN CONJ_TAC THENL [ 241 EXISTS_TAC ``SUC 0`` THEN REFL_TAC, 242 SIMP_TAC std_ss [ReachToRec_def,SET_SPEC,Prev_def] 243 THEN DISJ2_TAC 244 THEN EXISTS_TAC ``si:'a`` 245 THEN FULL_SIMP_TAC std_ss [IN_SING] 246 ] 247])); 248 249val ReachFromClosed = save_thm("ReachFromClosed",prove(``!si R s. R_EQR R ==> (s IN ReachFrom R si = R(si,s))``, 250REPEAT STRIP_TAC 251THEN SIMP_TAC std_ss [BIGUNION,ReachFrom_def,SET_SPEC] 252THEN EQ_TAC THENL [ 253REPEAT STRIP_TAC 254THEN `s IN ReachFromRec R si n` by ASSUM_LIST PROVE_TAC 255THEN POP_ASSUM_LIST (fn l => ASSUME_TAC (List.hd l) THEN ASSUME_TAC (List.last l)) 256THEN (SUBGOAL_THEN ``!n (s:'a). s IN ReachFromRec R si n ==> R(si,s)`` ASSUME_TAC) THENL [ 257 PAT_ASSUM ``s IN t`` (fn _ => ALL_TAC) 258 THEN Induct_on `n` THENL [ 259 FULL_SIMP_TAC std_ss [ReachFromRec_def,IN_SING,R_EQR_def,R_REFL_def], (* 0 *) 260 FULL_SIMP_TAC std_ss [ReachFromRec_def,SET_SPEC] 261 THEN RW_TAC std_ss [] THEN RES_TAC 262 THEN PAT_ASSUM ``!x. t`` (fn t => ASSUME_TAC (SPEC ``s'':'a`` t)) 263 THEN FULL_SIMP_TAC std_ss [Next_def,R_EQR_def,R_TRANS_def] 264 THEN ASSUM_LIST PROVE_TAC 265 ], 266 ASSUM_LIST PROVE_TAC 267 ], (* ==> *) 268DISCH_TAC 269THEN EXISTS_TAC ``ReachFromRec (R:'a#'a->bool) si (SUC 0)`` 270THEN CONJ_TAC THENL [ 271 EXISTS_TAC ``SUC 0`` THEN REFL_TAC, 272 SIMP_TAC std_ss [ReachFromRec_def,SET_SPEC,Next_def] 273 THEN DISJ2_TAC 274 THEN EXISTS_TAC ``si:'a`` 275 THEN FULL_SIMP_TAC std_ss [IN_SING] 276 ] 277])); 278 279val SCC_def = save_thm("SCC_def",Define `SCC R s = ReachFrom R s UNION ReachTo R s`); 280 281(* At the moment am not defining the ap field since we don't know that simply by looking at the formal M *) 282(* TODO: since aks.ap is simply the set of abstract state variables, we could pass it in to ABS_KS_def *) 283(* this is possible since the online abs ks would have been created before we use the definition below *) 284val ABS_KS_def = save_thm("ABS_KS_def",Define `ABS_KS M (h:('a#'b)->bool) = 285 <| S := UNIV:'b->bool; 286 S0:= { sh | ?s'. (s' IN M.S0) /\ h(s',sh)}; 287 T := \a. \(sh,sh'). ?s' s''. (M.T a)(s',s'') /\ h(s',sh) /\ h(s'',sh'); 288 L:= \sh. BIGUNION { X | ?s. (X = (M.L s)) /\ h(s,sh)} 289 |>`); 290 291 292val wf_absKS = save_thm("wf_absKS",prove(``!ks h. wfKS ks ==> wfKS (ABS_KS ks h)``, 293FULL_SIMP_TAC std_ss [wfKS_def,ABS_KS_def,KS_accfupds,combinTheory.K_DEF,SUBSET_UNIV])); 294 295val def1 = Define `QP2 h q q' = h(q,q')`; 296val def2 = Define `QP3(h,q) q' = QP2 h q q'`; 297 298val lem1 = prove(``!h q. h(q,@qh. h(q,qh)) = ?qh. h(q,qh)``, 299 REWRITE_TAC [GSYM def1] 300 THEN SPEC_TAC(``QP2 (h :'a # 'b -> bool) (q :'a)``,``Q:'b->bool``) 301 THEN REWRITE_TAC [SELECT_THM]); 302 303val ABS_CONS_LEM = save_thm("ABS_CONS_LEM",prove(``!(f:'prop mu) h (ks:('prop,'state) KS) s sh (e:string -> 'state -> bool) (eh:string -> 'astate -> bool). 304wfKS ks ==> 305(!Q. ~SUBFORMULA (~RV Q) (NNF f)) ==> 306(!s. ?sh. h(s,sh)) ==> 307(!a g. ~SUBFORMULA (<<a>> g) (NNF f)) ==> 308(!p. SUBFORMULA (AP p) f ==> p IN ks.ap) ==> 309(!s1 s2 sh. h(s1,sh) /\ h(s2,sh) ==> !p. p IN ks.ap ==> (s1 IN STATES (AP p) ks e = s2 IN STATES (AP p) ks e)) ==> 310(!Q s sh. h(s,sh) ==> (sh IN eh Q ==> s IN e Q)) ==> 311h(s,sh) ==> 312sh IN STATES (NNF f) (ABS_KS ks h) eh ==> s IN STATES (NNF f) ks e``, 313recInduct NNF_IND_def THEN REPEAT CONJ_TAC THENL [ 314SIMP_TAC std_ss [STATES_def,NNF_def,IN_UNIV,wfKS_def,wf_absKS], (* T *) 315SIMP_TAC std_ss [STATES_def,NNF_def,NOT_IN_EMPTY,wfKS_def], (* F *) 316RW_TAC std_ss [NNF_def,STATES_def,INTER_DEF,SET_SPEC,MU_SUB_def] 317THEN FULL_SIMP_TAC std_ss [SUB_AP_CONJ,IMF_def,FORALL_AND_THM,DISJ_IMP_THM] 318THEN RES_TAC 319THEN ASM_REWRITE_TAC [], (* /\ *) 320RW_TAC std_ss [NNF_def,STATES_def,SET_SPEC,MU_SUB_def] 321THEN FULL_SIMP_TAC std_ss [UNION_DEF,SET_SPEC,SUB_AP_DISJ,IMF_def,FORALL_AND_THM,DISJ_IMP_THM] 322THEN RES_TAC 323THEN ASM_REWRITE_TAC [], (* \/ *) 324RW_TAC std_ss [MU_SUB_def,NNF_def,STATES_def,SET_SPEC] THENL [ 325 FULL_SIMP_TAC std_ss [wfKS_def,IN_UNIV], 326 FULL_SIMP_TAC std_ss [ABS_KS_def,KS_accfupds,combinTheory.K_DEF,IN_UNIV,BIGUNION] 327 THEN WEAKEN_TAC (fn t => Term.compare(t,T)=EQUAL) 328 THEN FULL_SIMP_TAC std_ss [SET_SPEC] 329 THEN POP_ASSUM (fn t => PAT_ASSUM ``p' = ks.L s'`` (fn t' => ASSUME_TAC (REWRITE_RULE [t'] t))) 330 THEN ASSUM_LIST (fn t => PROVE_TAC (wfKS_def::IN_UNIV::t)) 331], (* AP *) 332RW_TAC std_ss [NNF_def,STATES_def,SET_SPEC,IN_UNIV,NOT_IN_EMPTY,DIFF_DEF,wfKS_def] 333THEN ASSUM_LIST (fn t => PROVE_TAC [IN_DEF]), (* RV *) 334RW_TAC std_ss [NNF_def,SUB_DMD_DMD], (* <> *) 335RW_TAC std_ss [] 336THEN FULL_SIMP_TAC std_ss [NNF_def,SUB_DMD_BOX,SUB_AP_BOX,SUB_RV_BOX,STATES_def,SET_SPEC,IN_UNIV,wfKS_def, 337 REWRITE_RULE [wfKS_def] wf_absKS] 338THEN POP_ASSUM MP_TAC 339THEN ASSUM_LIST (fn l => SIMP_TAC std_ss (l@[REWRITE_RULE [wfKS_def] wf_absKS,IN_UNIV])) 340THEN CONV_TAC (FORK_CONV(QUANT_CONV (FORK_CONV(REWRITE_CONV [KS_TRANSITION_def,KS_accfupds,combinTheory.K_DEF],ALL_CONV)), 341 QUANT_CONV (FORK_CONV(REWRITE_CONV [KS_TRANSITION_def,KS_accfupds,combinTheory.K_DEF],ALL_CONV)))) 342THEN REPEAT STRIP_TAC 343THEN PAT_ASSUM ``!q. (ABS_KS ks h).T a (sh,q) ==> q IN STATES (NNF f) (ABS_KS ks h) eh`` (fn t => ASSUME_TAC (CONV_RULE (QUANT_CONV (RATOR_CONV(RAND_CONV(SIMP_CONV std_ss [ABS_KS_def,KS_TRANSITION_def,KS_accfupds,combinTheory.K_DEF])))) t)) 344THEN PAT_ASSUM ``!s1 s2 sh'. h (s1,sh') /\ h (s2,sh') ==> !p. p IN ks.ap ==> (s1 IN ks.S /\ p IN ks.L s1 = s2 IN ks.S /\ p IN ks.L s2)`` 345 (fn t => PAT_ASSUM ``ks.S = UNIV`` (fn t' => ASSUME_TAC t' THEN ASSUME_TAC (SIMP_RULE std_ss [IN_UNIV,t'] t))) 346THEN PAT_ASSUM ``!s. ?sh. h (s,sh)`` (fn t => ASSUME_TAC t THEN ASSUME_TAC (Q.SPEC `q` t)) 347THEN NTAC 6 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fn t => REPEAT DISCH_TAC THEN RES_TAC THEN ASSUME_TAC t) 348THEN NTAC 2 (POP_ASSUM MP_TAC) THEN NTAC 2 (POP_ASSUM (fn _ => ALL_TAC)) THEN REPEAT DISCH_TAC 349THEN PAT_ASSUM ``!a b c d e g. t`` (fn t => ALL_TAC) 350THEN POP_ASSUM (fn t => POP_ASSUM (fn t' => ASSUME_TAC t THEN ASSUME_TAC (SPEC ``q:'state`` (SPEC ``@qh. h((q:'state),(qh:'astate))`` t')))) 351THEN PAT_ASSUM ``!q. (?s' s''. ks.T a (s',s'') /\ h (s',sh) /\ h (s'',q)) ==> 352 q IN STATES (NNF f) (ABS_KS ks h) eh`` (fn t => ASSUME_TAC (SPEC ``@qh. h((q:'state),(qh:'astate))`` t)) 353THEN (SUBGOAL_THEN ``(?(s':'state) s''. (ks:('prop,'state) KS).T a (s',s'') /\ h (s',(sh:'astate)) /\ h (s'',@qh. h (q,qh)))`` ASSUME_TAC) THENL [ 354 MAP_EVERY Q.EXISTS_TAC [`s:'state`,`q:'state`] 355 THEN ASM_REWRITE_TAC [lem1], 356 ASSUM_LIST metisLib.METIS_TAC 357], (* [] *) 358SIMP_TAC std_ss [FV_def,STATES_def,NNF_def,SET_SPEC] 359THEN NTAC 17 STRIP_TAC 360THEN IMP_RES_TAC IMF_MU_MU 361THEN FULL_SIMP_TAC std_ss [SUB_DMD_MU,SUB_AP_MU,SUB_RV_MU] 362THEN RES_TAC 363THEN POP_ASSUM (fn t => NTAC 5 (POP_ASSUM (fn _ => ALL_TAC)) THEN ASSUME_TAC t) 364THEN (SUBGOAL_THEN (mk_forall(``n:num``,list_mk_forall([``sh:'astate``,``s:'state``],mk_imp(``(h :'state # 'astate -> bool)(s,sh)``,mk_imp(``(sh:'astate) IN FP (NNF f) Q (ABS_KS (ks:('prop,'state) KS) h) eh[[[Q<--{}]]] n``,``s IN FP (NNF f) Q (ks:('prop,'state) KS) e[[[Q<--{}]]] n``))))) ASSUME_TAC) THENL [ 365 Induct_on `n` THENL [ 366 SIMP_TAC std_ss [STATES_def,ENV_EVAL,NOT_IN_EMPTY], 367 SIMP_TAC std_ss [STATES_def,ENV_UPDATE] 368 THEN POP_ASSUM (fn t => ASSUME_TAC t THEN UNDISCH_TAC (concl t)) 369 THEN SPEC_TAC (``FP (NNF f) Q (ABS_KS (ks:('prop,'state) KS) (h :'state # 'astate -> bool)) eh[[[Q<--{}]]] n``,``X:'astate -> bool``) 370 THEN SPEC_TAC (``FP (NNF f) Q (ks:('prop,'state) KS) e[[[Q<--{}]]] n``,``Y:'state->bool``) 371 THEN REPEAT GEN_TAC 372 THEN STRIP_TAC 373 THEN (SUBGOAL_THEN ``!e eh sh s. (!Q s (sh:'astate). (h:'state # 'astate -> bool)(s,sh) ==> (sh IN eh Q ==> s IN e Q)) ==> h(s,sh) ==> sh IN STATES (NNF f) (ABS_KS (ks:('prop,'state) KS) h) eh ==> s IN STATES (NNF f) (ks:('prop,'state) KS) e`` ASSUME_TAC) THENL [ 374 NTAC 3 (POP_ASSUM (fn _ => ALL_TAC)) 375 THEN PAT_ASSUM ``!Q s sh. h (s,sh) ==> (sh IN eh Q ==> s IN e Q)`` (fn _ => ALL_TAC) 376 THEN PAT_ASSUM ``h (s,sh)`` (fn _ => ALL_TAC) 377 THEN RES_TAC 378 THEN RW_TAC std_ss [] 379 THEN POP_ASSUM_LIST (fn t => PROVE_TAC (List.take(t,4))), 380 POP_ASSUM (fn t => ASSUME_TAC (SPECL [``(e :string -> 'state -> bool)[[[Q<--(Y :'state -> bool)]]]``,``(eh :string -> 'astate -> bool)[[[(Q :string)<--(X :'astate -> bool)]]]``] t)) 381 THEN (SUBGOAL_THEN``(!(Q' :string) (s :'state) (sh :'astate). (h:'state # 'astate -> bool)(s,sh) ==> (sh IN (eh :string -> 'astate -> bool)[[[(Q :string)<--(X :'astate -> bool)]]] 382 Q' ==> s IN (e :string -> 'state -> bool)[[[Q<--(Y :'state -> bool)]]] Q'))`` ASSUME_TAC) THENL [ 383 PAT_ASSUM ``!sh s. h (s,sh) ==> sh IN X ==> s IN Y`` (fn t => PAT_ASSUM ``!Q s sh. h (s,sh) ==> (sh IN eh Q ==> s IN e Q)`` 384 (fn t'=> POP_ASSUM_LIST (fn _ => ASSUME_TAC t THEN ASSUME_TAC t'))) 385 THEN REPEAT GEN_TAC 386 THEN Cases_on `Q=Q'` THENL [ 387 FULL_SIMP_TAC std_ss [ENV_EVAL] THEN ASSUM_LIST PROVE_TAC, 388 FULL_SIMP_TAC std_ss [ENV_UPDATE_INV] THEN ASSUM_LIST PROVE_TAC 389 ], 390 POP_ASSUM (fn t => POP_ASSUM (fn t' => POP_ASSUM_LIST (fn _ => ASSUME_TAC t THEN ASSUME_TAC t'))) 391 THEN REPEAT GEN_TAC 392 THEN POP_ASSUM (fn t => ASSUME_TAC (SPECL [``sh':'astate``,``s':'state``] t)) 393 THEN ASSUM_LIST PROVE_TAC 394 ] 395 ] 396 ], 397 RES_TAC 398 THEN NTAC 5 (POP_ASSUM (fn _ => ALL_TAC)) 399 THEN POP_ASSUM (fn t => POP_ASSUM_LIST (fn _ => ASSUME_TAC t)) 400 THEN ASSUM_LIST PROVE_TAC 401 ], (* mu *) 402SIMP_TAC std_ss [STATES_def,NNF_def,SET_SPEC] 403THEN NTAC 17 STRIP_TAC 404THEN IMP_RES_TAC IMF_MU_MU 405THEN FULL_SIMP_TAC std_ss [SUB_DMD_NU,SUB_AP_NU,SUB_RV_NU] 406THEN RES_TAC 407THEN POP_ASSUM (fn t => NTAC 5 (POP_ASSUM (fn _ => ALL_TAC)) THEN ASSUME_TAC t) 408THEN (SUBGOAL_THEN (mk_forall(``n:num``,list_mk_forall([``sh:'astate``,``s:'state``],mk_imp(``(h :'state # 'astate -> bool)(s,sh)``,mk_imp(``sh IN FP (NNF f) Q (ABS_KS (ks:('prop,'state) KS) h) eh[[[Q<--(ABS_KS (ks:('prop,'state) KS) (h:'state # 'astate -> bool)).S]]] n``,``s IN FP (NNF f) Q (ks:('prop,'state) KS) e[[[Q<--ks.S]]] n``))))) ASSUME_TAC) THENL [ 409 Induct_on `n` THENL [ 410 FULL_SIMP_TAC std_ss [STATES_def,ENV_EVAL,wfKS_def,wf_absKS,IN_UNIV], 411 SIMP_TAC std_ss [STATES_def,ENV_UPDATE] 412 THEN POP_ASSUM (fn t => ASSUME_TAC t THEN UNDISCH_TAC (concl t)) 413 THEN SPEC_TAC (``FP (NNF f) Q (ABS_KS (ks:('prop,'state) KS) (h :'state # 'astate -> bool)) eh[[[Q<--(ABS_KS (ks:('prop,'state) KS) h).S]]] n``,``X:'astate -> bool``) 414 THEN SPEC_TAC (``FP (NNF f) Q (ks:('prop,'state) KS) e[[[Q<--ks.S]]] n``,``Y:'state->bool``) 415 THEN REPEAT GEN_TAC 416 THEN STRIP_TAC 417 THEN (SUBGOAL_THEN ``!e eh sh s. (!Q s (sh:'astate). (h:'state # 'astate -> bool)(s,sh) ==> (sh IN eh Q ==> s IN e Q)) ==> h(s,sh) ==> sh IN STATES (NNF f) (ABS_KS ks h) eh ==> s IN STATES (NNF f) (ks:('prop,'state) KS) e`` ASSUME_TAC) THENL [ 418 NTAC 2 (POP_ASSUM (fn _ => ALL_TAC)) 419 THEN PAT_ASSUM ``!Q s sh. h (s,sh) ==> sh IN eh Q ==> s IN e Q`` (fn _ => ALL_TAC) 420 THEN PAT_ASSUM ``h (s,sh)`` (fn _ => ALL_TAC) 421 THEN RES_TAC 422 THEN RW_TAC std_ss [] 423 THEN POP_ASSUM_LIST (fn t => PROVE_TAC (List.take(t,4))), 424 POP_ASSUM (fn t => ASSUME_TAC (SPECL [``(e :string -> 'state -> bool)[[[Q<--(Y :'state -> bool)]]]``,``(eh :string -> 'astate -> bool)[[[(Q :string)<--(X :'astate -> bool)]]]``] t)) 425 THEN (SUBGOAL_THEN``(!(Q' :string) (s :'state) (sh :'astate). (h:'state # 'astate -> bool)(s,sh) ==> sh IN (eh :string -> 'astate -> bool)[[[(Q :string)<--(X :'astate -> bool)]]] 426 Q' ==> s IN (e :string -> 'state -> bool)[[[Q<--(Y :'state -> bool)]]] Q')`` ASSUME_TAC) THENL [ 427 PAT_ASSUM ``!sh s. h (s,sh) ==> sh IN X ==> s IN Y`` (fn t => PAT_ASSUM ``!Q s sh. h (s,sh) ==> sh IN eh Q ==> s IN e Q`` 428 (fn t'=> POP_ASSUM_LIST (fn _ => ASSUME_TAC t THEN ASSUME_TAC t'))) 429 THEN REPEAT GEN_TAC 430 THEN Cases_on `Q=Q'` THENL [ 431 FULL_SIMP_TAC std_ss [ENV_EVAL] THEN ASSUM_LIST PROVE_TAC, 432 FULL_SIMP_TAC std_ss [ENV_UPDATE_INV] THEN ASSUM_LIST PROVE_TAC 433 ], 434 POP_ASSUM (fn t => POP_ASSUM (fn t' => POP_ASSUM_LIST (fn _ => ASSUME_TAC t THEN ASSUME_TAC t'))) 435 THEN REPEAT GEN_TAC 436 THEN POP_ASSUM (fn t => ASSUME_TAC (SPECL [``sh':'astate``,``s':'state``] t)) 437 THEN ASSUM_LIST PROVE_TAC 438 ] 439 ] 440 ], 441 RES_TAC 442 THEN NTAC 5 (POP_ASSUM (fn _ => ALL_TAC)) 443 THEN POP_ASSUM (fn t => POP_ASSUM_LIST (fn _ => ASSUME_TAC t)) 444 THEN ASSUM_LIST PROVE_TAC 445 ], (* nu *) 446SIMP_TAC std_ss [STATES_def,NNF_def,NOT_IN_EMPTY,wfKS_def], (* ~T *) 447SIMP_TAC std_ss [STATES_def,NNF_def,IN_UNIV,wfKS_def,wf_absKS], (* ~F *) 448RW_TAC std_ss [NNF_def,STATES_def,UNION_DEF,SET_SPEC,MU_SUB_def] 449THEN FULL_SIMP_TAC std_ss [SUB_AP_DISJ,IMF_def,FORALL_AND_THM,DISJ_IMP_THM] 450THEN RES_TAC 451THEN ASM_REWRITE_TAC [], (* ~/\*) 452RW_TAC std_ss [NNF_def,STATES_def,INTER_DEF,SET_SPEC,MU_SUB_def] 453THEN FULL_SIMP_TAC std_ss [SUB_AP_CONJ,IMF_def,FORALL_AND_THM,DISJ_IMP_THM] 454THEN RES_TAC 455THEN ASM_REWRITE_TAC [], (* ~\/ *) 456FULL_SIMP_TAC std_ss [MU_SUB_def,NNF_def,DIFF_DEF,STATES_def,SET_SPEC] 457THEN REPEAT STRIP_TAC 458THEN FULL_SIMP_TAC std_ss [wfKS_def,IN_UNIV] 459THEN FULL_SIMP_TAC std_ss [ABS_KS_def,KS_accfupds,combinTheory.K_DEF,IN_UNIV,BIGUNION] 460THEN WEAKEN_TAC (fn t => Term.compare(t,T)=EQUAL) 461THEN FULL_SIMP_TAC std_ss [SET_SPEC] 462THEN POP_ASSUM (fn t => ASSUME_TAC (SPEC ``(ks:('prop,'state) KS).L (s:'state)`` t)) 463THEN FULL_SIMP_TAC std_ss [] 464THEN POP_ASSUM (fn t => ASSUME_TAC (SPEC ``s:'state`` t)) 465THEN FULL_SIMP_TAC std_ss [], (* ~AP *) 466RW_TAC std_ss [NNF_def,MU_SUB_def], (* ~RV *) 467FULL_SIMP_TAC std_ss [NNF_def,SUB_DMD_BOX,SUB_AP_NEG_DMD,SUB_RV_BOX,STATES_def,SET_SPEC,IN_UNIV,wfKS_def,REWRITE_RULE [wfKS_def] wf_absKS] 468THEN NTAC 17 STRIP_TAC 469THEN CONV_TAC (FORK_CONV(QUANT_CONV (FORK_CONV(REWRITE_CONV [KS_TRANSITION_def,KS_accfupds,combinTheory.K_DEF],ALL_CONV)), 470 QUANT_CONV (FORK_CONV(REWRITE_CONV [KS_TRANSITION_def,KS_accfupds,combinTheory.K_DEF],ALL_CONV)))) 471THEN REPEAT STRIP_TAC 472THEN PAT_ASSUM ``!q. (ABS_KS ks h).T a (sh,q) ==> q IN STATES (NNF f) (ABS_KS ks h) eh`` (fn t => ASSUME_TAC (CONV_RULE (QUANT_CONV (RATOR_CONV(RAND_CONV(SIMP_CONV std_ss [ABS_KS_def,KS_TRANSITION_def,KS_accfupds,combinTheory.K_DEF])))) t)) 473THEN POP_ASSUM (fn t => POP_ASSUM (fn t' => POP_ASSUM (fn t'' => ASSUME_TAC t THEN ASSUME_TAC t' THEN RES_TAC THEN ASSUME_TAC t''))) 474THEN POP_ASSUM (fn t => POP_ASSUM (fn t' => NTAC 2 (POP_ASSUM (fn _ => ALL_TAC)) THEN ASSUME_TAC t THEN ASSUME_TAC t')) 475THEN PAT_ASSUM ``!a b c d e g. t`` (fn t => ALL_TAC) 476THEN POP_ASSUM (fn t => ASSUME_TAC (SPEC ``q:'state`` (SPEC ``@qh. h((q:'state),(qh:'astate))`` t))) 477THEN POP_ASSUM (fn t => POP_ASSUM (fn t' => POP_ASSUM (fn t''' => POP_ASSUM (fn t'' => ASSUME_TAC t THEN ASSUME_TAC t' THEN ASSUME_TAC t''' THEN ASSUME_TAC (SPEC ``@qh. h((q:'state),(qh:'astate))`` t''))))) 478THEN (SUBGOAL_THEN ``(?(s':'state) s''. (ks:('prop,'state) KS).T a (s',s'') /\ h (s',(sh:'astate)) /\ h (s'',@qh. h (q,qh)))`` ASSUME_TAC) THENL [ 479 MAP_EVERY EXISTS_TAC [``s:'state``,``q:'state``] 480 THEN ASM_REWRITE_TAC [lem1], 481 ASSUM_LIST metisLib.METIS_TAC 482], (* ~<> *) 483SIMP_TAC std_ss [NNF_def,SUB_DMD_DMD], (* ~[] *) 484SIMP_TAC std_ss [NNF_def,SUB_AP_NEG_NEG], (* ~~ *) 485SIMP_TAC std_ss [STATES_def,NNF_def,SET_SPEC] 486THEN NTAC 17 STRIP_TAC 487THEN IMP_RES_TAC IMF_MU_MU 488THEN FULL_SIMP_TAC std_ss [SUB_DMD_NU,SUB_AP_NEG_MU,SUB_RV_NU] 489THEN RES_TAC 490THEN POP_ASSUM (fn t => NTAC 5 (POP_ASSUM (fn _ => ALL_TAC)) THEN ASSUME_TAC t) 491THEN (SUBGOAL_THEN (mk_forall(``n:num``,list_mk_forall([``sh:'astate``,``s:'state``],mk_imp(``(h :'state # 'astate -> bool)(s,sh)``,mk_imp(``sh IN FP (NNF (RVNEG Q ~f)) Q (ABS_KS (ks:('prop,'state) KS) (h :'state # 'astate -> bool)) eh[[[Q<--(ABS_KS (ks:('prop,'state) KS) h).S]]] n``,``s IN FP (NNF (RVNEG Q ~f)) Q (ks:('prop,'state) KS) e[[[Q<--ks.S]]] n``))))) ASSUME_TAC) THENL [ 492 Induct_on `n` THENL [ 493 FULL_SIMP_TAC std_ss [STATES_def,ENV_EVAL,wfKS_def,wf_absKS,IN_UNIV], 494 SIMP_TAC std_ss [STATES_def,ENV_UPDATE] 495 THEN POP_ASSUM (fn t => ASSUME_TAC t THEN UNDISCH_TAC (concl t)) 496 THEN SPEC_TAC (``FP (NNF (RVNEG Q ~f)) Q (ABS_KS (ks:('prop,'state) KS) (h :'state # 'astate -> bool) ) eh[[[Q<--(ABS_KS (ks:('prop,'state) KS) h).S]]] n``,``X:'astate -> bool``) 497 THEN SPEC_TAC (``FP (NNF (RVNEG Q ~f)) Q (ks:('prop,'state) KS) e[[[Q<--ks.S]]] n``,``Y:'state->bool``) 498 THEN REPEAT GEN_TAC 499 THEN STRIP_TAC 500 THEN (SUBGOAL_THEN ``!e eh sh s. (!Q s (sh:'astate). (h :'state # 'astate -> bool)(s,sh) ==> (sh IN eh Q ==> s IN e Q)) ==> h(s,sh) ==> sh IN STATES (NNF (RVNEG Q ~f)) (ABS_KS ks h) eh ==> s IN STATES (NNF (RVNEG Q ~f)) (ks:('prop,'state) KS) e`` ASSUME_TAC) THENL [ 501 NTAC 2 (POP_ASSUM (fn _ => ALL_TAC)) 502 THEN PAT_ASSUM ``!Q s sh. h (s,sh) ==> sh IN eh Q ==> s IN e Q`` (fn _ => ALL_TAC) 503 THEN PAT_ASSUM ``h (s,sh)`` (fn _ => ALL_TAC) 504 THEN RES_TAC 505 THEN RW_TAC std_ss [] 506 THEN POP_ASSUM_LIST (fn t => PROVE_TAC (List.take(t,4))), 507 POP_ASSUM (fn t => ASSUME_TAC (SPECL [``(e :string -> 'state -> bool)[[[Q<--(Y :'state -> bool)]]]``,``(eh :string -> 'astate -> bool)[[[(Q :string)<--(X :'astate -> bool)]]]``] t)) 508 THEN (SUBGOAL_THEN``(!(Q' :string) (s :'state) (sh :'astate). (h :'state # 'astate -> bool)(s,sh) ==> sh IN (eh :string -> 'astate -> bool)[[[(Q :string)<--(X :'astate -> bool)]]] 509 Q' ==> s IN (e :string -> 'state -> bool)[[[Q<--(Y :'state -> bool)]]] Q')`` ASSUME_TAC) THENL [ 510 PAT_ASSUM ``!sh s. h (s,sh) ==> sh IN X ==> s IN Y`` (fn t => PAT_ASSUM ``!Q s sh. h (s,sh) ==> sh IN eh Q ==> s IN e Q`` 511 (fn t'=> POP_ASSUM_LIST (fn _ => ASSUME_TAC t THEN ASSUME_TAC t'))) 512 THEN REPEAT GEN_TAC 513 THEN Cases_on `Q=Q'` THENL [ 514 FULL_SIMP_TAC std_ss [ENV_EVAL] THEN ASSUM_LIST PROVE_TAC, 515 FULL_SIMP_TAC std_ss [ENV_UPDATE_INV] THEN ASSUM_LIST PROVE_TAC 516 ], 517 POP_ASSUM (fn t => POP_ASSUM (fn t' => POP_ASSUM_LIST (fn _ => ASSUME_TAC t THEN ASSUME_TAC t'))) 518 THEN REPEAT GEN_TAC 519 THEN POP_ASSUM (fn t => ASSUME_TAC (SPECL [``sh':'astate``,``s':'state``] t)) 520 THEN ASSUM_LIST PROVE_TAC 521 ] 522 ] 523 ], 524 RES_TAC 525 THEN NTAC 5 (POP_ASSUM (fn _ => ALL_TAC)) 526 THEN POP_ASSUM (fn t => POP_ASSUM_LIST (fn _ => ASSUME_TAC t)) 527 THEN ASSUM_LIST PROVE_TAC 528 ], (* ~mu *) 529SIMP_TAC std_ss [FV_def,STATES_def,NNF_def,SET_SPEC] 530THEN NTAC 17 STRIP_TAC 531THEN IMP_RES_TAC IMF_MU_MU 532THEN FULL_SIMP_TAC std_ss [SUB_DMD_MU,SUB_AP_NEG_NU,SUB_RV_MU] 533THEN RES_TAC 534THEN POP_ASSUM (fn t => NTAC 5 (POP_ASSUM (fn _ => ALL_TAC)) THEN ASSUME_TAC t) 535THEN (SUBGOAL_THEN (mk_forall(``n:num``,list_mk_forall([``sh:'astate``,``s:'state``],mk_imp(``(h :'state # 'astate -> bool)(s,sh)``,mk_imp(``sh IN FP (NNF (RVNEG Q ~f)) Q (ABS_KS (ks:('prop,'state) KS) (h :'state # 'astate -> bool)) eh[[[Q<--{}]]] n``,``s IN FP (NNF (RVNEG Q ~f)) Q (ks:('prop,'state) KS) e[[[Q<--{}]]] n``))))) ASSUME_TAC) THENL [ 536 Induct_on `n` THENL [ 537 SIMP_TAC std_ss [STATES_def,ENV_EVAL,NOT_IN_EMPTY], 538 SIMP_TAC std_ss [STATES_def,ENV_UPDATE] 539 THEN POP_ASSUM (fn t => ASSUME_TAC t THEN UNDISCH_TAC (concl t)) 540 THEN SPEC_TAC (``FP (NNF (RVNEG Q ~f)) Q (ABS_KS (ks:('prop,'state) KS) (h :'state # 'astate -> bool)) eh[[[Q<--{}]]] n``,``X:'astate -> bool``) 541 THEN SPEC_TAC (``FP (NNF (RVNEG Q ~f)) Q (ks:('prop,'state) KS) e[[[Q<--{}]]] n``,``Y:'state->bool``) 542 THEN REPEAT GEN_TAC 543 THEN STRIP_TAC 544 THEN (SUBGOAL_THEN ``!e eh sh s. (!Q s (sh:'astate). (h :'state # 'astate -> bool)(s,sh) ==> (sh IN eh Q ==> s IN e Q)) ==> h(s,sh) ==> sh IN STATES (NNF (RVNEG Q ~f)) (ABS_KS ks h) eh ==> s IN STATES (NNF(RVNEG Q ~f) ) (ks:('prop,'state) KS) e`` ASSUME_TAC) THENL [ 545 PAT_ASSUM ``!Q s sh. h (s,sh) ==> (sh IN eh Q ==> s IN e Q)`` (fn _ => ALL_TAC) 546 THEN PAT_ASSUM ``h (s,sh)`` (fn _ => ALL_TAC) 547 THEN RES_TAC 548 THEN RW_TAC std_ss [] 549 THEN POP_ASSUM_LIST (fn t => PROVE_TAC (List.take(t,4))), 550 POP_ASSUM (fn t => ASSUME_TAC (SPECL [``(e :string -> 'state -> bool)[[[Q<--(Y :'state -> bool)]]]``,``(eh :string -> 'astate -> bool)[[[(Q :string)<--(X :'astate -> bool)]]]``] t)) 551 THEN (SUBGOAL_THEN``(!(Q' :string) (s :'state) (sh :'astate). (h :'state # 'astate -> bool)(s,sh) ==> (sh IN (eh :string -> 'astate -> bool)[[[(Q :string)<--(X :'astate -> bool)]]] 552 Q' ==> s IN (e :string -> 'state -> bool)[[[Q<--(Y :'state -> bool)]]] Q'))`` ASSUME_TAC) THENL [ 553 PAT_ASSUM ``!sh s. h (s,sh) ==> sh IN X ==> s IN Y`` (fn t => PAT_ASSUM ``!Q s sh. h (s,sh) ==> (sh IN eh Q ==> s IN e Q)`` 554 (fn t'=> POP_ASSUM_LIST (fn _ => ASSUME_TAC t THEN ASSUME_TAC t'))) 555 THEN REPEAT GEN_TAC 556 THEN Cases_on `Q=Q'` THENL [ 557 FULL_SIMP_TAC std_ss [ENV_EVAL] THEN ASSUM_LIST PROVE_TAC, 558 FULL_SIMP_TAC std_ss [ENV_UPDATE_INV] THEN ASSUM_LIST PROVE_TAC 559 ], 560 POP_ASSUM (fn t => POP_ASSUM (fn t' => POP_ASSUM_LIST (fn _ => ASSUME_TAC t THEN ASSUME_TAC t'))) 561 THEN REPEAT GEN_TAC 562 THEN POP_ASSUM (fn t => ASSUME_TAC (SPECL [``sh':'astate``,``s':'state``] t)) 563 THEN ASSUM_LIST PROVE_TAC 564 ] 565 ] 566 ], 567 RES_TAC 568 THEN NTAC 5 (POP_ASSUM (fn _ => ALL_TAC)) 569 THEN POP_ASSUM (fn t => POP_ASSUM_LIST (fn _ => ASSUME_TAC t)) 570 THEN ASSUM_LIST PROVE_TAC 571 ] (* ~nu *) 572])); 573 574 575val ABS_CONS_STATES = save_thm("ABS_CONS_STATES",SIMP_RULE std_ss [wf_absKS,STATES_NNF_ID] ABS_CONS_LEM); 576 577val ABS_INIT = save_thm("ABS_INIT",prove(``!ks h s sh. h(s,sh) ==> s IN ks.S0 ==> sh IN (ABS_KS ks h).S0``, 578REPEAT STRIP_TAC 579THEN SIMP_TAC std_ss [ABS_KS_def,ksTheory.KS_accfupds,combinTheory.K_DEF,SET_SPEC] 580THEN Q.EXISTS_TAC `s` 581THEN ASM_REWRITE_TAC [])); 582 583(* note <== direction is not provable because h may make unreachable s reachable *) 584val ABS_REACH = save_thm("ABS_REACH",prove(``!ks h a s sh. (!s. ?sh. h(s,sh)) ==> h(s,sh) ==> s IN Reachable (ks.T a) ks.S0 ==> sh IN Reachable ((ABS_KS ks h).T a) ((ABS_KS ks h).S0)``, 585NTAC 7 STRIP_TAC 586THEN SIMP_TAC std_ss [Reachable_def,BIGUNION,SET_SPEC] 587THEN STRIP_TAC 588THEN POP_ASSUM (fn t => POP_ASSUM (fn t' => ASSUME_TAC (REWRITE_RULE [t'] t))) 589THEN Q.EXISTS_TAC `ReachableRec ((ABS_KS ks h).T a) ((ABS_KS ks h).S0) n` 590THEN CONJ_TAC THENL [ 591 Q.EXISTS_TAC `n` THEN REFL_TAC, 592 POP_ASSUM_LIST (MAP_EVERY MP_TAC) 593 THEN STRIP_TAC 594 THEN MAP_EVERY Q.SPEC_TAC [(`s`,`s`),(`sh`,`sh`)] 595 THEN Induct_on `n` THENL [ 596 SIMP_TAC std_ss [ReachableRec_def,ABS_KS_def,ksTheory.KS_accfupds,combinTheory.K_DEF,SET_SPEC] 597 THEN RW_TAC std_ss [] 598 THEN Q.EXISTS_TAC `s` 599 THEN ASM_REWRITE_TAC [], 600 SIMP_TAC std_ss [ReachableRec_def,SET_SPEC] 601 THEN RW_TAC std_ss [] THENL [ 602 DISJ1_TAC THEN RES_TAC, 603 DISJ2_TAC 604 THEN FULL_SIMP_TAC std_ss [ReachNext_def] 605 THEN CONV_TAC (QUANT_CONV (LAND_CONV (SIMP_CONV std_ss [ABS_KS_def,ksTheory.KS_accfupds,combinTheory.K_DEF]))) 606 THEN Q.PAT_ASSUM `!s. ?sh. h (s,sh)` (fn t => ASSUME_TAC t THEN ASSUME_TAC (Q.SPEC `s''` t)) 607 THEN FULL_SIMP_TAC std_ss [] 608 THEN Q.EXISTS_TAC `@xh. h(s'',xh)` 609 THEN RW_TAC std_ss [] THENL [ 610 SELECT_ELIM_TAC 611 THEN RW_TAC std_ss [] 612 THEN MAP_EVERY Q.EXISTS_TAC [`s''`,`s`] 613 THEN ASM_REWRITE_TAC [], 614 SELECT_ELIM_TAC 615 THEN RW_TAC std_ss [] 616 THEN RES_TAC 617 ] 618 ] 619 ] 620])); 621 622val IS_ABS_FUN_def = Define `IS_ABS_FUN (ks:('prop,'state) KS) e h = (!s. ?(sh:'astate). h(s,sh)) /\ (!s1 s2 (sh:'astate). h(s1,sh) /\ h(s2,sh) ==> !p. p IN ks.ap ==> (s1 IN STATES (AP p) ks e = s2 IN STATES (AP p) ks e))`; 623 624val ABS_CONS_MODEL = save_thm("ABS_CONS_MODEL",prove(``!f h (ks:('prop,'state) KS) (e:string -> 'state -> bool) (eh:string -> 'astate -> bool). wfKS ks ==> (!Q. ~SUBFORMULA (~RV Q) (NNF f)) ==> (!a g. ~SUBFORMULA (<<a>> g) (NNF f)) ==> (!p. SUBFORMULA (AP p) f ==> p IN ks.ap) ==> IS_ABS_FUN (ks:('prop,'state) KS) e h ==> (!Q s sh. h(s,sh) ==> (sh IN eh Q ==> s IN e Q)) ==> MU_MODEL_SAT f (ABS_KS ks h) eh ==> MU_MODEL_SAT f ks e``, 625REPEAT STRIP_TAC 626THEN FULL_SIMP_TAC std_ss [MU_MODEL_SAT_def,MU_SAT_def,IS_ABS_FUN_def] 627THEN REPEAT STRIP_TAC 628THEN Q.PAT_ASSUM `!s. ?sh. h (s,sh)` (fn t => ASSUME_TAC t THEN ASSUME_TAC(Q.SPEC `s` t)) 629THEN FULL_SIMP_TAC std_ss [] 630THEN Q.PAT_ASSUM `!s. s IN (ABS_KS ks h).S0 ==> s IN STATES f (ABS_KS ks h) eh` (fn t => ASSUME_TAC (Q.SPEC `sh` t)) 631THEN IMP_RES_TAC ABS_INIT 632THEN IMP_RES_TAC ABS_CONS_STATES 633THEN FULL_SIMP_TAC std_ss [])); 634 635val SCC_FOLD_BASE = save_thm ("SCC_FOLD_BASE", 636 prove(``!f g pf R s sh k. (s IN {s | !i. i<=k ==> SCC (R i) (f i (0:num)) (pf i s)} = g (0:num) sh) 637 /\ (s IN {s | !i. i<=k ==> SCC (R i) (f i (1:num)) (pf i s)} = g (1:num) sh) 638 = 639 (s IN {s | !j. j<=1 ==> (s IN {s | !i. i<=k ==> (pf i s) IN (SCC (R i) (f i j))} 640 = (g j sh))})``, 641REPEAT STRIP_TAC THEN EQ_TAC THENL [ 642 STRIP_TAC THEN SIMP_TAC std_ss [SET_SPEC] THEN Induct_on `j` THENL [ 643 FULL_SIMP_TAC arith_ss [IN_DEF,DECIDE ``SUC (j:num) <= 1 = (j=0)``,SET_SPEC], 644 DISCH_TAC THEN FULL_SIMP_TAC arith_ss [DECIDE ``SUC (j:num) <= 1 = (j=0)``,IN_DEF,SET_SPEC] 645 ], 646 SIMP_TAC std_ss [SET_SPEC] THEN DISCH_TAC 647 THEN CONJ_TAC THENL [ 648 POP_ASSUM (fn t => ASSUME_TAC (SPEC ``0:num`` t)) 649 THEN FULL_SIMP_TAC arith_ss [IN_DEF], 650 POP_ASSUM (fn t => ASSUME_TAC (SPEC ``1:num`` t)) 651 THEN FULL_SIMP_TAC arith_ss [IN_DEF] 652 ] 653])); 654 655val SCC_FOLD_STEP = save_thm("SCC_FOLD_STEP",prove(``!f g pf R s sh k n. 656 s IN {s | !(j:num). j<=n ==> (s IN {s | !i. i<=k ==> SCC (R i) (f i j) (pf i s)} = (g j sh))} 657 /\ (s IN {s | !i. i<=k ==> SCC (R i) (f i (SUC n)) (pf i s)} = g (SUC n) sh) 658 = s IN {s | !(j:num). j<=(SUC n) ==> (s IN {s | !i. i<=k ==> SCC (R i) (f i j) (pf i s)} = (g j sh))}``, 659REPEAT STRIP_TAC 660THEN FULL_SIMP_TAC std_ss [SET_SPEC,IN_DEF] 661THEN EQ_TAC THEN DISCH_TAC THEN (TRY CONJ_TAC) THEN (TRY (Induct_on `j`)) THEN RW_TAC std_ss [] THENL [ 662 Cases_on `j=n` 663 THEN FULL_SIMP_TAC arith_ss [], 664 Cases_on `j=n` 665 THEN FULL_SIMP_TAC arith_ss [] 666])); 667 668val SCC_INNER_FOLD_BASE1 = save_thm("SCC_INNER_FOLD_BASE1",prove(``!R j f pf s. SCC (R 0) (f 0 j) (pf 0 s) = s IN {s | !i. i<=0 ==> SCC (R i) (f i j) (pf i s)}``, 669SIMP_TAC arith_ss [SET_SPEC])); 670 671val SCC_INNER_FOLD_BASE = save_thm("SCC_INNER_FOLD_BASE",prove(``!f pf R s sh j. (SCC (R 0) (f 0 j) (pf 0 s)) /\ (SCC (R 1) (f 1 j) (pf 1 s)) = s IN {s | !i. i<=1 ==> ((pf i s) IN SCC (R i) (f i j))}``, 672REPEAT STRIP_TAC THEN EQ_TAC THENL [ 673 STRIP_TAC THEN SIMP_TAC std_ss [SET_SPEC] THEN Induct_on `i` THENL [ 674 FULL_SIMP_TAC arith_ss [IN_DEF], 675 DISCH_TAC THEN FULL_SIMP_TAC arith_ss [DECIDE ``SUC (i:num) <= 1 = (i=0)``,IN_DEF] 676 ], 677 SIMP_TAC std_ss [SET_SPEC] THEN DISCH_TAC 678 THEN CONJ_TAC THENL [ 679 POP_ASSUM (fn t => ASSUME_TAC (SPEC ``0:num`` t)) 680 THEN FULL_SIMP_TAC arith_ss [IN_DEF], 681 POP_ASSUM (fn t => ASSUME_TAC (SPEC ``1:num`` t)) 682 THEN FULL_SIMP_TAC arith_ss [IN_DEF] 683 ] 684])); 685 686val SCC_INNER_FOLD_STEP = save_thm("SCC_INNER_FOLD_STEP",prove(``!f pf R s sh j n. s IN {s | !(i:num). i<=n ==> ((pf i s) IN SCC (R i) (f i j))} /\ (SCC (R (SUC n)) (f (SUC n) j) (pf (SUC n) s)) = s IN {s | !(i:num). i<=(SUC n) ==> ((pf i s) IN SCC (R i) (f i j))}``, 687REPEAT STRIP_TAC 688THEN FULL_SIMP_TAC std_ss [SET_SPEC,IN_DEF] 689THEN EQ_TAC THEN DISCH_TAC THEN (TRY CONJ_TAC) THEN (TRY (Induct_on `i`)) THEN RW_TAC std_ss [] THENL [ 690 Cases_on `i=n` 691 THEN FULL_SIMP_TAC arith_ss [] 692 THEN PAT_ASSUM ``!i. t`` (fn t => ASSUME_TAC (SPEC ``SUC i`` t)) THEN FULL_SIMP_TAC arith_ss [], 693 FULL_SIMP_TAC arith_ss [] 694])); 695 696val SCC_REL = save_thm("SCC_REL",prove(``!R s si. R_EQR R ==> (s IN SCC R si = R(s,si))``, 697 FULL_SIMP_TAC std_ss [R_EQR_def,R_SYM_def,SCC_def,ReachFromClosed,ReachToClosed,UNION_DEF,SET_SPEC])); 698 699val SCC_REL_IMP = save_thm("SCC_REL_IMP",prove(``!R s1 s2 si. R_EQR R ==> (s1 IN SCC R si /\ s2 IN SCC R si) ==> R(s1,s2)``, 700PROVE_TAC [SCC_REL,R_EQR_def,R_SYM_def,R_TRANS_def])); 701 702val BIGOR_OVER_AND = store_thm( 703 "BIGOR_OVER_AND", 704 ``!P Q k. (?i. i<=k /\ P i) /\ (?i. i<=k /\ Q i) 705 = ?i j. i<=k /\ j<=k /\ (P i /\ Q j)``, 706 PROVE_TAC []); 707 708val abst_lem1 = save_thm("abst_lem1",prove(``!f sh k i j. ((!i. i<=k /\ f i sh ==> !j. j<=k /\ f j sh ==> (i=j)) ==> i<=k /\ j<=k /\ f i sh /\ f j sh ==> (i=j))``, 709REPEAT STRIP_TAC THEN RES_TAC)); 710 711val _ = export_theory(); 712