1open HolKernel Parse boolLib bossLib 2 3val _ = new_theory("cache") 4 5 6open bossLib 7open pairTheory 8open pairLib 9open pairTools 10open pairSyntax 11open pred_setTheory 12open pred_setLib 13open listTheory 14open stringTheory 15open sumTheory 16open simpLib 17open stringLib 18open numLib 19open metisLib 20open ksTheory 21open setLemmasTheory 22open reachTheory 23open muSyntaxTheory 24open envTheory 25open muTheory 26 27infix &&; infix 8 by; 28 29fun tsimps ty = let val {convs,rewrs} = TypeBase.simpls_of ty in rewrs end 30 31(* thms for environment-invariant satisfiability *) 32 33val MU_SAT_RV_ENV_EQ = save_thm("MU_SAT_RV_ENV_EQ",prove(``!(ks: ('prop,'state) KS) . wfKS ks ==> (!s Q e e' X. ((MU_SAT (RV Q) ks e s = X) /\ (e Q = e' Q)) ==> (MU_SAT (RV Q) ks e' s = X))``,SIMP_TAC std_ss [wfKS_def,MU_SAT_def,STATES_def,MU_SAT_RV])) 34 35val SAT_T_ENV_INV = save_thm("SAT_T_ENV_INV", GENL [``ks: ('prop,'state) KS``,``e:string -> 'state -> bool``,``e':string -> 'state -> bool``] (EXT (GEN ``s:'state`` (SPEC_ALL (prove(``!(ks: ('prop,'state) KS) e e' s. MU_SAT T ks e s = MU_SAT T ks e' s``,SIMP_TAC std_ss [MU_SAT_def,STATES_def])))))) 36 37val SAT_F_ENV_INV = save_thm("SAT_F_ENV_INV", GENL [``ks: ('prop,'state) KS``,``e:string -> 'state -> bool``,``e':string -> 'state -> bool``] (EXT (GEN ``s:'state`` (SPEC_ALL (prove(``!(ks: ('prop,'state) KS) e e' s. MU_SAT F ks e s = MU_SAT F ks e' s``,SIMP_TAC std_ss [MU_SAT_def,STATES_def])))))) 38 39val SAT_AP_ENV_INV = save_thm("SAT_AP_ENV_INV", GENL [``ks: ('prop,'state) KS``,``p:'prop``,``e:string -> 'state -> bool``,``e':string -> 'state -> bool``] (EXT (GEN ``s:'state`` (SPEC_ALL (prove(``!(ks: ('prop,'state) KS) (p:'prop) e e' s. MU_SAT (AP p) ks e s = MU_SAT (AP p) ks e' s``,SIMP_TAC std_ss [MU_SAT_def,STATES_def])))))) 40 41val SAT_RV_ENV_INV = save_thm("SAT_RV_ENV_INV",prove(``!(ks: ('prop,'state) KS) Q e e'. (e Q = e' Q) ==> (MU_SAT (RV Q) ks e = MU_SAT (RV Q) ks e')``,REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN FULL_SIMP_TAC std_ss [MU_SAT_def,STATES_def,MU_SAT_RV])) 42 43val SAT_ENV_INV_META = prove(``(!e e'. MU_SAT (f:'prop mu) (ks : ('prop,'state) KS) e = MU_SAT (f:'prop mu) (ks : ('prop,'state) KS) e') = (!e e' (s:'state). MU_SAT (f:'prop mu) (ks : ('prop,'state) KS) e s = MU_SAT (f:'prop mu) (ks : ('prop,'state) KS) e' s)``,SIMP_TAC std_ss [GEN_ALL (FUN_EQ_CONV ``MU_SAT (f :'prop mu) (ks :('prop,'state) KS) (e: string -> 'state -> bool)= MU_SAT f ks (e' :string -> 'state -> bool)``)]) 44 45val SAT_ENV_INV_META2=FUN_EQ_CONV ``MU_SAT (f:'prop mu) (ks : ('prop,'state) KS) e = MU_SAT (f:'prop mu) (ks : ('prop,'state) KS) e'`` 46 47val SAT_NEG_ENV_INV = save_thm("SAT_NEG_ENV_INV", prove(``!(ks:('prop,'state) KS) . wfKS ks ==> (!(f:'prop mu) e e'. ((!e e'. MU_SAT f ks e = MU_SAT f ks e') ==> (MU_SAT (~f) ks e = MU_SAT (~f) ks e')))``,REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN FULL_SIMP_TAC std_ss [SAT_ENV_INV_META,MU_SAT_def,STATES_def,wfKS_def,UNIV_DEF,DIFF_DEF,SET_SPEC] THEN FULL_SIMP_TAC std_ss [IN_DEF])) 48 49 50val SAT_NEG_ENV_INV2 = save_thm("SAT_NEG_ENV_INV2", prove(``!(ks:('prop,'state) KS) . wfKS ks ==> (!(f:'prop mu) e e'. ((MU_SAT f ks e = MU_SAT f ks e') ==> (MU_SAT (~f) ks e = MU_SAT (~f) ks e')))``,REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN FULL_SIMP_TAC std_ss [SAT_ENV_INV_META2,MU_SAT_def,STATES_def,wfKS_def,UNIV_DEF,DIFF_DEF,SET_SPEC])) 51 52val SAT_CONJ_ENV_INV = save_thm("SAT_CONJ_ENV_INV", prove(``!(ks:('prop,'state) KS) (f:'prop mu) (g:'prop mu) e e'. ((!e e'. MU_SAT f ks e = MU_SAT f ks e') /\ (!e e'. MU_SAT g ks e = MU_SAT g ks e')) ==> (MU_SAT (f /\ g) ks e = MU_SAT (f /\ g) ks e')``,REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN FULL_SIMP_TAC std_ss [SAT_ENV_INV_META,MU_SAT_def,STATES_def,INTER_DEF,SET_SPEC] THEN ASSUM_LIST PROVE_TAC)) 53 54val SAT_CONJ_ENV_INV2 = save_thm("SAT_CONJ_ENV_INV2", prove(``!(ks:('prop,'state) KS) f (g:'prop mu) e e'. ((MU_SAT f ks e = MU_SAT f ks e') /\ (MU_SAT g ks e = MU_SAT g ks e')) ==> (MU_SAT (f /\ g) ks e = MU_SAT (f /\ g) ks e')``,REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN FULL_SIMP_TAC std_ss [SAT_ENV_INV_META2,MU_SAT_def,STATES_def,INTER_DEF,SET_SPEC] THEN ASSUM_LIST PROVE_TAC)) 55 56val SAT_DISJ_ENV_INV = save_thm("SAT_DISJ_ENV_INV", prove(``!(ks:('prop,'state) KS) f (g:'prop mu) e e'. ((!e e'. MU_SAT f ks e = MU_SAT f ks e') /\ (!e e'. MU_SAT g ks e = MU_SAT g ks e')) ==> (MU_SAT (f \/ g) ks e = MU_SAT (f \/ g) ks e')``,REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN FULL_SIMP_TAC std_ss [SAT_ENV_INV_META,MU_SAT_def,STATES_def,UNION_DEF,SET_SPEC] THEN ASSUM_LIST PROVE_TAC)) 57 58val SAT_DISJ_ENV_INV2 = save_thm("SAT_DISJ_ENV_INV2", prove(``!(ks:('prop,'state) KS) f (g:'prop mu) e e'. ((MU_SAT f ks e = MU_SAT f ks e') /\ (MU_SAT g ks e = MU_SAT g ks e')) ==> (MU_SAT (f \/ g) ks e = MU_SAT (f \/ g) ks e')``,REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN FULL_SIMP_TAC std_ss [SAT_ENV_INV_META2,MU_SAT_def,STATES_def,UNION_DEF,SET_SPEC] THEN ASSUM_LIST PROVE_TAC)) 59 60val SAT_DMD_ENV_INV = save_thm("SAT_DMD_ENV_INV", prove(``!(ks:('prop,'state) KS) a f e e'. (!e e'. MU_SAT f ks e = MU_SAT f ks e') ==> (MU_SAT (<<a>> f) ks e = MU_SAT (<<a>> f) ks e')``,REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN FULL_SIMP_TAC std_ss [SAT_ENV_INV_META,MU_SAT_def,STATES_def,SET_SPEC] THEN ASSUM_LIST PROVE_TAC)) 61 62val SAT_DMD_ENV_INV2 = save_thm("SAT_DMD_ENV_INV2", prove(``!(ks:('prop,'state) KS) a f e e'. (MU_SAT f ks e = MU_SAT f ks e') ==> (MU_SAT (<<a>> f) ks e = MU_SAT (<<a>> f) ks e')``,REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN FULL_SIMP_TAC std_ss [SAT_ENV_INV_META2,MU_SAT_def,STATES_def,UNION_DEF,SET_SPEC] THEN ASSUM_LIST PROVE_TAC)) 63 64val SAT_BOX_ENV_INV = save_thm("SAT_BOX_ENV_INV", prove(``!(ks:('prop,'state) KS) a f e e'. (!e e'. MU_SAT f ks e = MU_SAT f ks e') ==> (MU_SAT ([[a]] f) ks e = MU_SAT ([[a]] f) ks e')``,REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN FULL_SIMP_TAC std_ss [SAT_ENV_INV_META,MU_SAT_def,STATES_def,SET_SPEC] THEN ASSUM_LIST PROVE_TAC)) 65 66val SAT_BOX_ENV_INV2 = save_thm("SAT_BOX_ENV_INV2", prove(``!(ks:('prop,'state) KS) a f e e'. (MU_SAT f ks e = MU_SAT f ks e') ==> (MU_SAT ([[a]] f) ks e = MU_SAT ([[a]] f) ks e')``,REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN FULL_SIMP_TAC std_ss [SAT_ENV_INV_META2,MU_SAT_def,STATES_def,INTER_DEF,SET_SPEC] THEN ASSUM_LIST PROVE_TAC)) 67 68val SAT_LFP_ENV_INV = 69 save_thm("SAT_LFP_ENV_INV", 70 prove(``!(ks:('prop,'state) KS) s Q f e e'. (!s X e e'. MU_SAT f ks e[[[Q<--X]]] s = MU_SAT f ks e'[[[Q<--X]]] s) 71 ==> (MU_SAT (mu Q.. f) ks e s = MU_SAT (mu Q .. f) ks e' s)``, 72 SIMP_TAC std_ss [MU_SAT_def,STATES_def,SET_SPEC] 73 THEN REPEAT STRIP_TAC 74 THEN (SUBGOAL_THEN ``!(n:num) (s: 'state) . (s :'state) IN 75 FP (f :'prop mu) (Q :string) (ks :('prop,'state) KS) 76 (e :string -> 'state -> bool)[[[Q<--{}]]] n = s IN FP f Q (ks: ('prop,'state) KS) 77 (e' :string -> 'state -> bool)[[[Q<--{}]]] n`` 78 (fn th => ASSUM_LIST (fn t => PROVE_TAC (th::t)))) 79 THEN Induct_on `n` 80 THENL [SIMP_TAC std_ss [STATES_def,ENV_UPDATE_def,NOT_IN_EMPTY], 81 FULL_SIMP_TAC std_ss [IN_DEF,STATES_def,SYM (ISPECL [`` FP (f :'prop mu) (Q :string) (ks :('prop,'state) KS) 82 (e :string -> 'state -> bool)[[[Q<--{}]]] 83 (n :num)``,``FP (f :'prop mu) (Q :string) 84 (ks :('prop,'state) KS) 85 (e':string -> 'state -> bool)[[[Q<--{}]]] 86 (n :num)``] FUN_EQ_THM),ENV_UPDATE]])) 87 88val SAT_LFP_ENV_INV2 = 89 save_thm("SAT_LFP_ENV_INV2", 90 prove(``!(ks:('prop,'state) KS) Q f e e'. (!X. MU_SAT f ks e[[[Q<--X]]] = MU_SAT f ks e'[[[Q<--X]]]) 91 ==> (MU_SAT (mu Q.. f) ks e = MU_SAT (mu Q .. f) ks e')``, 92 REPEAT STRIP_TAC 93 THEN CONV_TAC FUN_EQ_CONV 94 THEN FULL_SIMP_TAC std_ss [SAT_ENV_INV_META2,MU_SAT_def,STATES_def,SET_SPEC] 95 THEN REPEAT STRIP_TAC 96 THEN (SUBGOAL_THEN ``!(n:num) (s: 'state) . (s :'state) IN 97 FP (f :'prop mu) (Q :string) (ks :('prop,'state) KS) 98 (e :string -> 'state -> bool)[[[Q<--{}]]] n = s IN FP f Q (ks: ('prop,'state) KS) 99 (e' :string -> 'state -> bool)[[[Q<--{}]]] n`` 100 (fn th => ASSUM_LIST (fn t => PROVE_TAC (th::t)))) 101 THEN Induct_on `n` 102 THENL [SIMP_TAC std_ss [STATES_def,ENV_UPDATE_def,NOT_IN_EMPTY], 103 FULL_SIMP_TAC std_ss [IN_DEF,STATES_def,SYM (ISPECL [`` FP (f :'prop mu) (Q :string) (ks :('prop,'state) KS) 104 (e :string -> 'state -> bool)[[[Q<--{}]]] 105 (n :num)``,``FP (f :'prop mu) (Q :string) 106 (ks :('prop,'state) KS) 107 (e':string -> 'state -> bool)[[[Q<--{}]]] 108 (n :num)``] FUN_EQ_THM),ENV_UPDATE]])) 109 110val SAT_GFP_ENV_INV = 111 save_thm("SAT_GFP_ENV_INV", 112 prove(``!(ks:('prop,'state) KS) s Q f e e'. (!s X e e'. MU_SAT f ks e[[[Q<--X]]] s = MU_SAT f ks e'[[[Q<--X]]] s) 113 ==> (MU_SAT (nu Q.. f) ks e s = MU_SAT (nu Q .. f) ks e' s)``, 114 SIMP_TAC std_ss [MU_SAT_def,STATES_def,SET_SPEC] 115 THEN REPEAT STRIP_TAC 116 THEN (SUBGOAL_THEN ``!(n:num) (s: 'state) . (s :'state) IN 117 FP (f :'prop mu) (Q :string) (ks :('prop,'state) KS) 118 (e :string -> 'state -> bool)[[[Q<--ks.S]]] n = s IN FP f Q (ks: ('prop,'state) KS) 119 (e' :string -> 'state -> bool)[[[Q<--ks.S]]] n`` 120 (fn th => ASSUM_LIST (fn t => PROVE_TAC (th::t)))) 121 THEN Induct_on `n` 122 THENL [SIMP_TAC std_ss [STATES_def,ENV_UPDATE_def,NOT_IN_EMPTY], 123 FULL_SIMP_TAC std_ss [IN_DEF,STATES_def,SYM (ISPECL [`` FP (f :'prop mu) (Q :string) (ks :('prop,'state) KS) 124 (e :string -> 'state -> bool)[[[Q<--ks.S]]] 125 (n :num)``,``FP (f :'prop mu) (Q :string) 126 (ks :('prop,'state) KS) 127 (e':string -> 'state -> bool)[[[Q<--ks.S]]] 128 (n :num)``] FUN_EQ_THM),ENV_UPDATE]])) 129 130val SAT_GFP_ENV_INV2 = 131 save_thm("SAT_GFP_ENV_INV2", 132 prove(``!(ks:('prop,'state) KS) Q f e e'. (!X. MU_SAT f ks e[[[Q<--X]]] = MU_SAT f ks e'[[[Q<--X]]]) 133 ==> (MU_SAT (nu Q.. f) ks e = MU_SAT (nu Q .. f) ks e')``, 134 REPEAT STRIP_TAC 135 THEN CONV_TAC FUN_EQ_CONV 136 THEN FULL_SIMP_TAC std_ss [SAT_ENV_INV_META2,MU_SAT_def,STATES_def,SET_SPEC] 137 THEN REPEAT STRIP_TAC 138 THEN (SUBGOAL_THEN ``!(n:num) (s: 'state) . (s :'state) IN 139 FP (f :'prop mu) (Q :string) (ks :('prop,'state) KS) 140 (e :string -> 'state -> bool)[[[Q<--ks.S]]] n = s IN FP f Q (ks: ('prop,'state) KS) 141 (e' :string -> 'state -> bool)[[[Q<--ks.S]]] n`` 142 (fn th => ASSUM_LIST (fn t => PROVE_TAC (th::t)))) 143 THEN Induct_on `n` 144 THENL [SIMP_TAC std_ss [STATES_def,ENV_UPDATE_def,NOT_IN_EMPTY], 145 FULL_SIMP_TAC std_ss [IN_DEF,STATES_def,SYM (ISPECL [`` FP (f :'prop mu) (Q :string) (ks :('prop,'state) KS) 146 (e :string -> 'state -> bool)[[[Q<--ks.S]]] 147 (n :num)``,``FP (f :'prop mu) (Q :string) 148 (ks :('prop,'state) KS) 149 (e':string -> 'state -> bool)[[[Q<--ks.S]]] 150 (n :num)``] FUN_EQ_THM),ENV_UPDATE]])) 151 152 153(* thms used by checker for ado *) 154 155val STATES_LFP_2_LEM = prove(``!f ks e P X Y Q. 156 IMF (mu Q.. f) /\ IMF (mu P.. f) /\ wfKS ks /\ X SUBSET Y ==> STATES f ks e[[[P<--X]]][[[Q<--{}]]] SUBSET 157 STATES f ks e[[[P<--Y]]][[[Q<--{}]]]``, 158REPEAT STRIP_TAC 159THEN Q.SUBGOAL_THEN `(!Q'. 160 (if ~RV Q' SUBF NNF f then 161 e[[[P<--X]]] Q' = e[[[P<--Y]]] Q' else e[[[P<--X]]] Q' SUBSET e[[[P<--Y]]] Q'))` ASSUME_TAC THENL [ 162FULL_SIMP_TAC std_ss [IMF_def] 163THEN GEN_TAC 164THEN Cases_on `Q'=P` THENL [ 165FULL_SIMP_TAC std_ss [ENV_EVAL], 166IMP_RES_TAC (INST_TYPE [alpha|->beta] ENV_UPDATE_INV) 167THEN Cases_on `~RV Q' SUBF NNF f` THENL [ 168FULL_SIMP_TAC std_ss [], 169FULL_SIMP_TAC std_ss [SUBSET_REFL]]], 170ASSUM_LIST (fn t=> METIS_TAC (STATES_MONO::SUBSET_REFL::t))]) 171 172val STATES_LFP_2 = prove(``!f ks e P X Y Q. IMF (mu Q..f) /\ IMF (mu P.. f) /\ wfKS ks /\ X SUBSET Y ==> (!n. FP f Q ks e[[[P<--X]]][[[Q<--{}]]] n SUBSET FP f Q ks e[[[P<--Y]]][[[Q<--{}]]] n)``, 173REPEAT STRIP_TAC 174THEN `!e. STATES f ks e[[[P<--X]]][[[Q<--{}]]] SUBSET STATES f ks e[[[P<--Y]]][[[Q<--{}]]]` by IMP_RES_TAC STATES_LFP_2_LEM 175THEN POP_ASSUM (fn t => ASSUME_TAC (Q.SPEC `e` t)) 176THEN Cases_on `P=Q` THENL [ 177POP_ASSUM (fn t => ASSUME_TAC (SYM t)) 178THEN FULL_SIMP_TAC std_ss [ENV_UPDATE,SUBSET_REFL], 179IMP_RES_TAC (INST_TYPE [alpha|->beta] ENV_SWAP) 180THEN Q.PAT_ASSUM `t SUBSET t'` MP_TAC 181THEN ASM_REWRITE_TAC [] 182THEN Q.SPEC_TAC (`e[[[Q<--{}]]]`,`e`) 183THEN POP_ASSUM (fn _ => ALL_TAC) 184THEN POP_ASSUM (fn t => ASSUME_TAC (CONV_RULE (RAND_CONV SYM_CONV) t)) 185THEN REPEAT STRIP_TAC 186THEN Induct_on `n` THENL [ 187FULL_SIMP_TAC std_ss [STATES_def,ENV_UPDATE,ENV_UPDATE_INV,SUBSET_REFL], 188SIMP_TAC std_ss [STATES_def,ENV_EVAL,ENV_UPDATE] 189THEN Q.SUBGOAL_THEN `(!Q'. 190 (if ~RV Q' SUBF NNF f then 191 e[[[P<--X]]] Q' = e[[[P<--Y]]] Q' else e[[[P<--X]]] Q' SUBSET e[[[P<--Y]]] Q'))` ASSUME_TAC THENL [ 192FULL_SIMP_TAC std_ss [IMF_def] 193THEN GEN_TAC 194THEN Cases_on `Q'=P` THENL [ 195FULL_SIMP_TAC std_ss [ENV_EVAL], 196IMP_RES_TAC (INST_TYPE [alpha|->beta] ENV_UPDATE_INV) 197THEN Cases_on `~RV Q' SUBF NNF f` THENL [ 198FULL_SIMP_TAC std_ss [], 199FULL_SIMP_TAC std_ss [SUBSET_REFL]]], 200IMP_RES_TAC STATES_MONO 201]]]) 202 203val STATES_FP_BIGUNION_2 = save_thm("STATES_FP_BIGUNION_2",prove(``!f ks e Q1 X Y Q. IMF (mu Q..f) /\ IMF (mu Q1.. f) /\ wfKS ks /\ X SUBSET Y ==> BIGUNION {P | ?n. (P = FP f Q ks e[[[Q1<--X]]][[[Q<--{}]]] n)} SUBSET BIGUNION {P | ?n. (P = FP f Q ks e[[[Q1<--Y]]][[[Q<--{}]]] n)}``, 204REPEAT STRIP_TAC 205THEN SIMP_TAC std_ss [BIGUNION,SET_SPEC,SUBSET_DEF] 206THEN REPEAT STRIP_TAC 207THEN RW_TAC std_ss [] 208THEN Q.EXISTS_TAC `FP f Q ks e[[[Q1<--Y]]][[[Q<--{}]]] n` 209THEN CONV_TAC LEFT_AND_EXISTS_CONV 210THEN Q.EXISTS_TAC `n` 211THEN REWRITE_TAC [] 212THEN POP_ASSUM MP_TAC THEN Q.SPEC_TAC (`x`,`x`) 213THEN REWRITE_TAC [GSYM SUBSET_DEF] 214THEN METIS_TAC [STATES_LFP_2])) 215 216val GEN_STATES_LFP = prove(``!f ks e e' Q. wfKS ks /\ IMF (mu Q.. f) /\ 217 (!Q'. (if ~RV Q' SUBF NNF f then e Q' = e' Q' else e Q' SUBSET e' Q')) ==> 218 (!n. FP f Q ks e[[[Q<--{}]]] n SUBSET FP f Q ks e'[[[Q<--{}]]] n)``, 219REPEAT STRIP_TAC 220THEN Induct_on `n` THENL [ 221FULL_SIMP_TAC std_ss [STATES_def,ENV_UPDATE,SUBSET_REFL,ENV_EVAL], 222FULL_SIMP_TAC std_ss [STATES_def,ENV_EVAL,ENV_UPDATE] 223THEN METIS_TAC [STATES_MONO,SUBSET_REFL]]) 224 225val GEN_STATES_FP_BIGUNION = save_thm("GEN_STATES_FP_BIGUNION",prove(``!f ks e e' Q. wfKS ks /\ IMF (mu Q.. f) /\ 226 (!Q'. (if ~RV Q' SUBF NNF f then e Q' = e' Q' else e Q' SUBSET e' Q')) ==> 227 BIGUNION {P | ?n. (P = FP f Q ks e[[[Q<--{}]]] n)} SUBSET BIGUNION {P | ?n. (P = FP f Q ks e'[[[Q<--{}]]] n)}``, 228REPEAT STRIP_TAC 229THEN SIMP_TAC std_ss [BIGUNION,SET_SPEC,SUBSET_DEF] 230THEN REPEAT STRIP_TAC 231THEN RW_TAC std_ss [] 232THEN Q.EXISTS_TAC `FP f Q ks e'[[[Q<--{}]]] n` 233THEN CONV_TAC LEFT_AND_EXISTS_CONV 234THEN Q.EXISTS_TAC `n` 235THEN REWRITE_TAC [] 236THEN POP_ASSUM MP_TAC THEN Q.SPEC_TAC (`x`,`x`) 237THEN REWRITE_TAC [GSYM SUBSET_DEF] 238THEN METIS_TAC [GEN_STATES_LFP])) 239 240val STATES_DEF_SYM_MU = save_thm("STATES_DEF_SYM_MU",prove(``!f ks e Q n. STATES f ks e[[[Q<--FP f Q ks e[[[Q<--{}]]] n]]] = FP f Q ks e[[[Q<--{}]]] (SUC n)``,SIMP_TAC std_ss [STATES_def,ENV_UPDATE])) 241 242val STATES_GFP_2_LEM = prove(``!f ks e P X Y Q. 243 IMF (nu Q.. f) /\ IMF (nu P.. f) /\ wfKS ks /\ X SUBSET Y ==> STATES f ks e[[[P<--X]]][[[Q<--ks.S]]] SUBSET 244 STATES f ks e[[[P<--Y]]][[[Q<--ks.S]]]``, 245REPEAT STRIP_TAC 246THEN Q.SUBGOAL_THEN `(!Q'. 247 (if ~RV Q' SUBF NNF f then 248 e[[[P<--X]]] Q' = e[[[P<--Y]]] Q' else e[[[P<--X]]] Q' SUBSET e[[[P<--Y]]] Q'))` ASSUME_TAC THENL [ 249FULL_SIMP_TAC std_ss [IMF_def] 250THEN GEN_TAC 251THEN Cases_on `Q'=P` THENL [ 252FULL_SIMP_TAC std_ss [ENV_EVAL], 253IMP_RES_TAC (INST_TYPE [alpha|->beta] ENV_UPDATE_INV) 254THEN Cases_on `~RV Q' SUBF NNF f` THENL [ 255FULL_SIMP_TAC std_ss [], 256FULL_SIMP_TAC std_ss [SUBSET_REFL]]], 257FULL_SIMP_TAC std_ss [GSYM IMF_MU_IFF_IMF_NU] 258THEN ASSUM_LIST (fn t=> METIS_TAC (STATES_MONO::SUBSET_REFL::t))]) 259 260val STATES_GFP_2 = prove(``!f ks e P X Y Q. IMF (nu Q..f) /\ IMF (nu P.. f) /\ wfKS ks /\ X SUBSET Y ==> (!n. FP f Q ks e[[[P<--X]]][[[Q<--ks.S]]] n SUBSET FP f Q ks e[[[P<--Y]]][[[Q<--ks.S]]] n)``, 261REPEAT STRIP_TAC 262THEN `!e. STATES f ks e[[[P<--X]]][[[Q<--ks.S]]] SUBSET STATES f ks e[[[P<--Y]]][[[Q<--ks.S]]]` by IMP_RES_TAC STATES_GFP_2_LEM 263THEN POP_ASSUM (fn t => ASSUME_TAC (Q.SPEC `e` t)) 264THEN Cases_on `P=Q` THENL [ 265POP_ASSUM (fn t => ASSUME_TAC (SYM t)) 266THEN FULL_SIMP_TAC std_ss [ENV_UPDATE,SUBSET_REFL], 267IMP_RES_TAC (INST_TYPE [alpha|->beta] ENV_SWAP) 268THEN Q.PAT_ASSUM `t SUBSET t'` MP_TAC 269THEN ASM_REWRITE_TAC [] 270THEN Q.SPEC_TAC (`e[[[Q<--ks.S]]]`,`e`) 271THEN POP_ASSUM (fn _ => ALL_TAC) 272THEN POP_ASSUM (fn t => ASSUME_TAC (CONV_RULE (RAND_CONV SYM_CONV) t)) 273THEN REPEAT STRIP_TAC 274THEN Induct_on `n` THENL [ 275FULL_SIMP_TAC std_ss [STATES_def,ENV_UPDATE,ENV_UPDATE_INV,SUBSET_REFL], 276SIMP_TAC std_ss [STATES_def,ENV_EVAL,ENV_UPDATE] 277THEN Q.SUBGOAL_THEN `(!Q'. 278 (if ~RV Q' SUBF NNF f then 279 e[[[P<--X]]] Q' = e[[[P<--Y]]] Q' else e[[[P<--X]]] Q' SUBSET e[[[P<--Y]]] Q'))` ASSUME_TAC THENL [ 280FULL_SIMP_TAC std_ss [IMF_def] 281THEN GEN_TAC 282THEN Cases_on `Q'=P` THENL [ 283FULL_SIMP_TAC std_ss [ENV_EVAL], 284IMP_RES_TAC (INST_TYPE [alpha|->beta] ENV_UPDATE_INV) 285THEN Cases_on `~RV Q' SUBF NNF f` THENL [ 286FULL_SIMP_TAC std_ss [], 287FULL_SIMP_TAC std_ss [SUBSET_REFL]]], 288FULL_SIMP_TAC std_ss [GSYM IMF_MU_IFF_IMF_NU] 289THEN IMP_RES_TAC STATES_MONO 290]]]) 291 292 293val STATES_FP_BIGINTER_2 = save_thm("STATES_FP_BIGINTER_2",prove(``!f ks e Q1 X Y Q. IMF (nu Q..f) /\ IMF (nu Q1.. f) /\ wfKS ks /\ X SUBSET Y ==> BIGINTER {P | ?n. (P = FP f Q ks e[[[Q1<--X]]][[[Q<--ks.S]]] n)} SUBSET BIGINTER {P | ?n. (P = FP f Q ks e[[[Q1<--Y]]][[[Q<--ks.S]]] n)}``, 294REPEAT STRIP_TAC 295THEN SIMP_TAC std_ss [BIGINTER,SET_SPEC,SUBSET_DEF] 296THEN REPEAT STRIP_TAC 297THEN PAT_ASSUM ``!x. t`` (fn t => ASSUME_TAC (CONV_RULE ((QUANT_CONV LEFT_IMP_EXISTS_CONV) THENC SWAP_VARS_CONV) t)) 298THEN POP_ASSUM (fn t => ASSUME_TAC (Q.SPECL [`n`,`FP f Q ks e[[[Q1<--X]]][[[Q<--ks.S]]] n`] t)) 299THEN RW_TAC std_ss [] 300THEN POP_ASSUM MP_TAC THEN Q.SPEC_TAC (`x`,`x`) 301THEN REWRITE_TAC [GSYM SUBSET_DEF] 302THEN METIS_TAC [STATES_GFP_2])) 303 304val GEN_STATES_GFP = prove(``!f ks e e' Q.wfKS ks /\ IMF (nu Q.. f) /\ 305 (!Q'. (if ~RV Q' SUBF NNF f then e Q' = e' Q' else e Q' SUBSET e' Q')) ==> 306 (!n. FP f Q ks e[[[Q<--ks.S]]] n SUBSET FP f Q ks e'[[[Q<--ks.S]]] n)``, 307REPEAT STRIP_TAC 308THEN Induct_on `n` THENL [ 309FULL_SIMP_TAC std_ss [STATES_def,ENV_UPDATE,SUBSET_REFL,ENV_EVAL], 310FULL_SIMP_TAC std_ss [STATES_def,ENV_EVAL,ENV_UPDATE,GSYM IMF_MU_IFF_IMF_NU] 311THEN METIS_TAC [STATES_MONO,SUBSET_REFL]]) 312 313val GEN_STATES_FP_BIGINTER = save_thm("GEN_STATES_FP_BIGINTER",prove(``!f ks e e' Q. wfKS ks /\ IMF (nu Q.. f) /\ 314 (!Q'. (if ~RV Q' SUBF NNF f then e Q' = e' Q' else e Q' SUBSET e' Q')) ==> 315 BIGINTER {P | ?n. (P = FP f Q ks e[[[Q<--ks.S]]] n)} SUBSET BIGINTER {P | ?n. (P = FP f Q ks e'[[[Q<--ks.S]]] n)}``, 316REPEAT STRIP_TAC 317THEN SIMP_TAC std_ss [BIGINTER,SET_SPEC,SUBSET_DEF] 318THEN REPEAT STRIP_TAC 319THEN PAT_ASSUM ``!x. t`` (fn t => ASSUME_TAC (CONV_RULE ((QUANT_CONV LEFT_IMP_EXISTS_CONV) THENC SWAP_VARS_CONV) t)) 320THEN POP_ASSUM (fn t => ASSUME_TAC (Q.SPECL [`n`,`FP f Q ks e[[[Q<--ks.S]]] n`] t)) 321THEN RW_TAC std_ss [] 322THEN POP_ASSUM MP_TAC THEN Q.SPEC_TAC (`x`,`x`) 323THEN REWRITE_TAC [GSYM SUBSET_DEF] 324THEN METIS_TAC [GEN_STATES_GFP])) 325 326val STATES_DEF_SYM_NU = save_thm("STATES_DEF_SYM_NU",prove(``!f ks e Q n. STATES f ks e[[[Q<--FP f Q ks e[[[Q<--ks.S]]] n]]] = FP f Q ks e[[[Q<--ks.S]]] (SUC n)``,SIMP_TAC std_ss [STATES_def,ENV_UPDATE])) 327 328val _ = export_theory() 329