1open HolKernel boolLib bossLib Parse pred_setTheory pairTheory wordsTheory; 2 3val _ = new_theory "set_sep"; 4val _ = ParseExtras.temp_loose_equality() 5 6(* ---- definitions ---- *) 7 8val one_def = Define `one x = \s. (s = {x})`; 9val emp_def = Define `emp = \s. (s = {})`; 10val cond_def = Define `cond c = \s. (s = {}) /\ c`; 11val SEP_F_def = Define `SEP_F s = F`; 12val SEP_T_def = Define `SEP_T s = T`; 13val SPLIT_def = Define `SPLIT (s:'a set) (u,v) ��� (u ��� v = s) ��� DISJOINT u v`; 14val STAR_def = Define `STAR p q = (\s. ?u v. SPLIT s (u,v) /\ p u /\ q v)`; 15val SEP_EQ_def = Define `SEP_EQ x = \s. s = x`; 16 17val SEP_EXISTS = new_binder_definition("SEP_EXISTS", 18 ``($SEP_EXISTS) = \f s:'a set. $? (\y. f y s)``); 19 20val SEP_HIDE_def = Define `SEP_HIDE p = SEP_EXISTS x. p x`; 21val SEP_DISJ_def = Define `SEP_DISJ p q = (\s. p s \/ q s)`; 22 23val _ = overload_on ("*",Term`STAR`); 24val _ = overload_on ("~",Term`SEP_HIDE`); 25val _ = overload_on ("\\/",Term`SEP_DISJ`); 26 27val sidecond_def = Define `sidecond = cond`; 28val precond_def = Define `precond = cond`; 29 30val SEP_IMP_def = Define `SEP_IMP p q = !s. p s ==> q s`; 31 32val fun2set_def = Define `fun2set (f:'b->'a,d) = { (a,f a) | a IN d }`; 33 34val SEP_ARRAY_def = Define ` 35 (SEP_ARRAY p i a [] = emp) /\ 36 (SEP_ARRAY p i a (x::xs) = p a x * SEP_ARRAY p i (a + i:'a word) xs)`; 37 38 39(* ---- theorems ---- *) 40 41val SPLIT_ss = rewrites [SPLIT_def,SUBSET_DEF,DISJOINT_DEF,DELETE_DEF,IN_INSERT,SEP_EQ_def, 42 EXTENSION,NOT_IN_EMPTY,IN_DEF,IN_UNION,IN_INTER,IN_DIFF]; 43 44val SPLIT_TAC = FULL_SIMP_TAC (pure_ss++SPLIT_ss) [] \\ METIS_TAC []; 45 46val STAR_COMM = store_thm("STAR_COMM", 47 ``!p:'a set->bool q. p * q = q * p``, 48 REWRITE_TAC [STAR_def,SPLIT_def,DISJOINT_DEF] 49 \\ METIS_TAC [UNION_COMM,INTER_COMM,CONJ_SYM,CONJ_ASSOC]); 50 51val STAR_ASSOC_LEMMA = prove( 52 ``!x p:'a set->bool q r. (p * (q * r)) x ==> ((p * q) * r) x``, 53 SIMP_TAC std_ss [STAR_def] \\ REPEAT STRIP_TAC 54 \\ Q.EXISTS_TAC `u UNION u'` \\ Q.EXISTS_TAC `v'` 55 \\ STRIP_TAC THEN1 SPLIT_TAC 56 \\ ASM_SIMP_TAC bool_ss [] 57 \\ Q.EXISTS_TAC `u` \\ Q.EXISTS_TAC `u'` \\ SPLIT_TAC); 58 59val STAR_ASSOC = store_thm("STAR_ASSOC", 60 ``!p:'a set->bool q r. p * (q * r) = (p * q) * r``, 61 ONCE_REWRITE_TAC [FUN_EQ_THM] \\ METIS_TAC [STAR_ASSOC_LEMMA,STAR_COMM]); 62 63val SEP_CLAUSES = store_thm("SEP_CLAUSES", 64 ``!p q t c c'. 65 (((SEP_EXISTS v. p v) * q) = SEP_EXISTS v. p v * q) /\ 66 ((q * (SEP_EXISTS v. p v)) = SEP_EXISTS v. q * p v) /\ 67 (((SEP_EXISTS v. p v) \/ q) = SEP_EXISTS v. p v \/ q) /\ 68 ((q \/ (SEP_EXISTS v. p v)) = SEP_EXISTS v. q \/ p v) /\ 69 ((SEP_EXISTS v. q) = q) /\ ((SEP_EXISTS v. p v * cond (v = x)) = p x) /\ 70 (q \/ SEP_F = q) /\ (SEP_F \/ q = q) /\ (SEP_F * q = SEP_F) /\ (q * SEP_F = SEP_F) /\ 71 (r \/ r = r) /\ (q * (r \/ t) = q * r \/ q * t) /\ ((r \/ t) * q = r * q \/ t * q) /\ 72 (cond c \/ cond c' = cond (c \/ c')) /\ (cond c * cond c' = cond (c /\ c')) /\ 73 (cond T = emp) /\ (cond F = SEP_F) /\ (emp * q = q) /\ (q * emp = q)``, 74 ONCE_REWRITE_TAC [FUN_EQ_THM] 75 \\ SIMP_TAC std_ss [SEP_EXISTS,STAR_def,SEP_DISJ_def,cond_def,SEP_F_def,emp_def] 76 \\ SPLIT_TAC); 77 78val SEP_EXISTS_COND = save_thm("SEP_EXISTS_COND", 79 (GEN_ALL o GSYM o Q.INST [`q`|->`cond c`] o hd o 80 CONJUNCTS o SPEC_ALL) SEP_CLAUSES); 81 82val SEP_EXISTS_THM = store_thm("SEP_EXISTS_THM", 83 ``(SEP_EXISTS x. p x) s = ?x. p x s``, 84 SIMP_TAC std_ss [SEP_EXISTS]); 85 86val SPLIT_LEMMA = prove( 87 ``!s t v. SPLIT s (t,v) = (v = s DIFF t) /\ t SUBSET s``,SPLIT_TAC); 88 89val cond_STAR = store_thm("cond_STAR", 90 ``!c s p. ((cond c * p) s = c /\ p s) /\ ((p * cond c) s = c /\ p s)``, 91 Cases \\ SIMP_TAC std_ss [SEP_CLAUSES] \\ SIMP_TAC std_ss [SEP_F_def]); 92 93val one_STAR = store_thm("one_STAR", 94 ``!x s p. (one x * p) s = x IN s /\ p (s DELETE x)``, 95 SIMP_TAC std_ss [STAR_def,one_def,SPLIT_LEMMA,DELETE_DEF,INSERT_SUBSET,EMPTY_SUBSET]); 96 97val EQ_STAR = store_thm("EQ_STAR", 98 ``!p s t. (SEP_EQ t * p) s = p (s DIFF t) /\ t SUBSET s``, 99 SIMP_TAC std_ss [SEP_EQ_def,STAR_def,SPLIT_LEMMA] \\ METIS_TAC []); 100 101val SEP_IMP_REFL = store_thm("SEP_IMP_REFL", 102 ``!p. SEP_IMP p p``, 103 SIMP_TAC std_ss [SEP_IMP_def]); 104 105val SEP_IMP_TRANS = store_thm("SEP_IMP_TRANS", 106 ``!p q r. SEP_IMP p q /\ SEP_IMP q r ==> SEP_IMP p r``, 107 SIMP_TAC std_ss [SEP_IMP_def] \\ METIS_TAC []); 108 109val SEP_IMP_FRAME = store_thm("SEP_IMP_FRAME", 110 ``!p q. SEP_IMP p q ==> !r. SEP_IMP (p * r) (q * r)``, 111 SIMP_TAC std_ss [SEP_IMP_def,STAR_def] \\ REPEAT STRIP_TAC 112 \\ Q.EXISTS_TAC `u` \\ Q.EXISTS_TAC `v` \\ METIS_TAC []); 113 114val SEP_IMP_MOVE_COND = store_thm("SEP_IMP_MOVE_COND", 115 ``!c p q. SEP_IMP (p * cond c) q = c ==> SEP_IMP p q``, 116 Cases \\ SIMP_TAC bool_ss [SEP_CLAUSES] \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_F_def]); 117 118val SEP_IMP_emp = store_thm("SEP_IMP_emp", 119 ``!p. SEP_IMP emp p = p {}``,SIMP_TAC std_ss [SEP_IMP_def,emp_def]); 120 121val SEP_IMP_cond = store_thm("SEP_IMP_cond", 122 ``!g h. SEP_IMP (cond g) (cond h) = g ==> h``, 123 SIMP_TAC std_ss [SEP_IMP_def,cond_def]); 124 125val SEP_IMP_STAR = store_thm("SEP_IMP_STAR", 126 ``!p p' q q'. SEP_IMP p p' /\ SEP_IMP q q' ==> SEP_IMP (p * q) (p' * q')``, 127 SIMP_TAC std_ss [SEP_IMP_def,STAR_def] \\ METIS_TAC []); 128 129val SEP_IMP_DISJ = store_thm("SEP_IMP_DISJ", 130 ``!p p' q q'. SEP_IMP p p' /\ SEP_IMP q q' ==> SEP_IMP (p \/ q) (p' \/ q')``, 131 SIMP_TAC std_ss [SEP_IMP_def,SEP_DISJ_def] \\ METIS_TAC []); 132 133val SEP_IMP_EQ = store_thm("SEP_IMP_EQ", 134 ``!p q. (p = q) = SEP_IMP p q /\ SEP_IMP q p``, 135 FULL_SIMP_TAC bool_ss [SEP_IMP_def,FUN_EQ_THM] \\ METIS_TAC []); 136 137val SEP_IMP_EXISTS_EXISTS = store_thm("SEP_IMP_EXISTS_EXISTS", 138 ``(!x. SEP_IMP (p x) (q x)) ==> SEP_IMP ($SEP_EXISTS p) ($SEP_EXISTS q)``, 139 SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS] \\ REPEAT STRIP_TAC 140 \\ Q.EXISTS_TAC `y` \\ ASM_SIMP_TAC std_ss []); 141 142val SEP_IMP_SEP_HIDE = store_thm("SEP_IMP_SEP_HIDE", 143 ``!p x. SEP_IMP (p x) (~p)``, 144 SIMP_TAC std_ss [SEP_IMP_def,SEP_HIDE_def,SEP_EXISTS_THM] THEN METIS_TAC []); 145 146val SEP_IMP_PRE_DISJ = store_thm("SEP_IMP_PRE_DISJ", 147 ``!p1 p2 q. SEP_IMP (p1 \/ p2) q = SEP_IMP p1 q /\ SEP_IMP p2 q``, 148 SIMP_TAC std_ss [SEP_IMP_def,SEP_DISJ_def] \\ METIS_TAC []); 149 150val SEP_IMP_PRE_EXISTS = store_thm("SEP_IMP_PRE_EXISTS", 151 ``!p q. SEP_IMP (SEP_EXISTS x. p x) q = !x. SEP_IMP (p x) q``, 152 SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS_THM] \\ METIS_TAC []); 153 154val SEP_DISJ_COMM = store_thm("SEP_DISJ_COMM", 155 ``!p q. p \/ q = SEP_DISJ q p``, 156 SIMP_TAC std_ss [SEP_DISJ_def,FUN_EQ_THM] \\ REPEAT STRIP_TAC 157 \\ EQ_TAC \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss []); 158 159val SEP_DISJ_ASSOC = store_thm("SEP_DISJ_ASSOC", 160 ``!p q r. SEP_DISJ (SEP_DISJ p q) r = p \/ (q \/ r)``, 161 SIMP_TAC std_ss [SEP_DISJ_def,FUN_EQ_THM] \\ REPEAT STRIP_TAC 162 \\ EQ_TAC \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss []); 163 164val SPLIT_EQ = store_thm("SPLIT_EQ", 165 ``!s u v. SPLIT s (u,v) = (u SUBSET s) /\ (v = s DIFF u)``, 166 SIMP_TAC std_ss [SPLIT_def,SUBSET_DEF,EXTENSION,IN_DIFF,IN_UNION, 167 DISJOINT_DEF,NOT_IN_EMPTY,IN_INTER] \\ METIS_TAC []); 168 169val fun2set_thm = store_thm("fun2set_thm", 170 ``!f d a x. fun2set (f:'b->'a,d) (a,x) = (f a = x) /\ a IN d``, 171 REWRITE_TAC [SIMP_RULE std_ss [IN_DEF] GSPECIFICATION,fun2set_def] 172 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ SIMP_TAC std_ss [pairTheory.EXISTS_PROD]); 173 174val read_fun2set = store_thm("read_fun2set", 175 ``!a x p f. (one (a,x) * p) (fun2set (f,d)) ==> (f a = x) /\ a IN d``, 176 SIMP_TAC std_ss [one_STAR,IN_DEF,fun2set_thm]); 177 178val write_fun2set = store_thm("write_fun2set", 179 ``!y a x p f. (one (a,x) * p) (fun2set (f,d)) ==> (p * one (a,y)) (fun2set ((a =+ y) f,d))``, 180 SIMP_TAC std_ss [one_STAR,IN_DEF,fun2set_thm,combinTheory.APPLY_UPDATE_THM] 181 \\ ONCE_REWRITE_TAC [STAR_COMM] 182 \\ SIMP_TAC std_ss [one_STAR,IN_DEF,fun2set_thm,combinTheory.APPLY_UPDATE_THM] 183 \\ NTAC 4 STRIP_TAC \\ MATCH_MP_TAC (METIS_PROVE [] ``(x = y) ==> (t /\ p x ==> p y)``) 184 \\ SIMP_TAC std_ss [EXTENSION] \\ Cases 185 \\ SIMP_TAC std_ss [fun2set_thm,IN_DELETE] 186 \\ SIMP_TAC std_ss [fun2set_thm,IN_DELETE,IN_DEF] 187 \\ Cases_on `q = a` \\ ASM_SIMP_TAC std_ss [combinTheory.APPLY_UPDATE_THM] 188 \\ METIS_TAC []); 189 190val fun2set_eq = Q.store_thm("fun2set_eq", 191 `!f g d. (fun2set (f, d) = fun2set (g, d)) = (!a. a IN d ==> (f a = g a))`, 192 SRW_TAC [] [FUN_EQ_THM] 193 \\ EQ_TAC 194 \\ REPEAT STRIP_TAC 195 THENL [ 196 Q.PAT_X_ASSUM `!x. P` (Q.SPEC_THEN `(a, f a)` ASSUME_TAC), 197 Cases_on `x` \\ Cases_on `q IN d` 198 ] 199 \\ REV_FULL_SIMP_TAC std_ss [fun2set_thm] 200 ) 201 202val one_fun2set = store_thm("one_fun2set", 203 ``!a x p f. (one (a,x) * p) (fun2set (f,d)) = 204 (f a = x) /\ a IN d /\ p (fun2set (f,d DELETE a))``, 205 SIMP_TAC std_ss [fun2set_def,one_STAR,GSPECIFICATION] \\ REPEAT STRIP_TAC 206 \\ Cases_on `f a = x` \\ ASM_SIMP_TAC std_ss [] 207 \\ Cases_on `a IN d` \\ ASM_SIMP_TAC std_ss [] \\ AP_TERM_TAC 208 \\ FULL_SIMP_TAC std_ss [EXTENSION,GSPECIFICATION,IN_DELETE,FORALL_PROD] 209 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 210 \\ FULL_SIMP_TAC std_ss [] \\ METIS_TAC []); 211 212val fun2set_NEQ = store_thm("fun2set_NEQ", 213 ``!a b x y f g p. (one (a,x) * one (b,y) * p) (fun2set (f,g)) ==> ~(a = b)``, 214 REWRITE_TAC [GSYM STAR_ASSOC,one_STAR,IN_DELETE,PAIR_EQ,fun2set_def] 215 \\ SIMP_TAC std_ss [GSPECIFICATION]); 216 217val fun2set_DIFF = store_thm("fun2set_DIFF", 218 ``!f x y. fun2set (f,x) DIFF fun2set (f,y) = fun2set (f,x DIFF y)``, 219 SIMP_TAC std_ss [fun2set_def,EXTENSION,IN_DIFF,GSPECIFICATION] 220 \\ SIMP_TAC std_ss [FORALL_PROD,PAIR_EQ] \\ METIS_TAC []) 221 222val SUBSET_fun2set = store_thm("SUBSET_fun2set", 223 ``!v df f:'a->'b. v SUBSET fun2set (f,df) ==> ?z. v = fun2set (f,z)``, 224 REPEAT STRIP_TAC \\ Q.EXISTS_TAC `{ x | (x,f x) IN v }` 225 \\ FULL_SIMP_TAC std_ss [fun2set_def,EXTENSION,GSPECIFICATION,SUBSET_DEF] 226 \\ FULL_SIMP_TAC std_ss [FORALL_PROD] \\ METIS_TAC []); 227 228val fun2set_EMPTY = store_thm("fun2set_EMPTY", 229 ``!f df. (fun2set (f,df) = {}) = (df = {})``, 230 SIMP_TAC std_ss [fun2set_def,EXTENSION,GSPECIFICATION,NOT_IN_EMPTY]) 231 232val IN_fun2set = store_thm("IN_fun2set", 233 ``!a y h dh. (a,y) IN fun2set (h,dh) = (h a = y) /\ a IN dh``, 234 SIMP_TAC std_ss [fun2set_def,GSPECIFICATION] \\ METIS_TAC []); 235 236val fun2set_DELETE = store_thm("fun2set_DELETE", 237 ``!a h dh. fun2set (h,dh) DELETE (a, h a) = fun2set (h,dh DELETE a)``, 238 SIMP_TAC std_ss [fun2set_def,GSPECIFICATION,IN_DELETE,EXTENSION, 239 FORALL_PROD] THEN METIS_TAC []); 240 241val SPLIT_fun2set_IMP = prove( 242 ``SPLIT (fun2set (f,df)) (u,v) ==> 243 (u = fun2set(f,df DIFF { x | (x,f x) IN v }))``, 244 SIMP_TAC std_ss [SPLIT_def] \\ REPEAT STRIP_TAC 245 \\ FULL_SIMP_TAC std_ss [SPLIT_def,EXTENSION,IN_UNION,NOT_IN_EMPTY, 246 DISJOINT_DEF,IN_INTER,fun2set_def,GSPECIFICATION,IN_DIFF] 247 \\ METIS_TAC []); 248 249val SPLIT_SYM_IMP = prove( 250 ``SPLIT x (u,v) ==> SPLIT x (v,u) ``, 251 SIMP_TAC std_ss [SPLIT_def,DISJOINT_DEF] \\ METIS_TAC [UNION_COMM,INTER_COMM]); 252 253val fun2set_STAR_IMP = store_thm("fun2set_STAR_IMP", 254 ``(p * q) (fun2set (f,df)) ==> 255 ?x y. p (fun2set (f,df DIFF y)) /\ q (fun2set (f,df DIFF x))``, 256 SIMP_TAC std_ss [STAR_def] \\ REPEAT STRIP_TAC \\ IMP_RES_TAC SPLIT_SYM_IMP 257 \\ IMP_RES_TAC SPLIT_fun2set_IMP \\ METIS_TAC []); 258 259val one_fun2set_IMP = store_thm("one_fun2set_IMP", 260 ``(one (a,x)) (fun2set (f,df)) ==> (f a = x) /\ a IN df``, 261 REPEAT STRIP_TAC 262 \\ IMP_RES_TAC (REWRITE_RULE [SEP_CLAUSES] (Q.SPECL [`a`,`x`,`emp`] one_fun2set))); 263 264val DIFF_UNION = store_thm("DIFF_UNION", 265 ``!x y z. x DIFF y DIFF z = x DIFF (y UNION z)``, 266 SIMP_TAC std_ss [EXTENSION,IN_DIFF,IN_UNION] \\ METIS_TAC []); 267 268val SEP_ARRAY_APPEND = store_thm("SEP_ARRAY_APPEND", 269 ``!xs ys p i a. 270 SEP_ARRAY p i a (xs ++ ys) = 271 SEP_ARRAY p i a xs * SEP_ARRAY p i (a + n2w (LENGTH xs) * i) ys``, 272 Induct \\ ASM_SIMP_TAC std_ss [SEP_ARRAY_def,STAR_ASSOC, 273 listTheory.APPEND,listTheory.LENGTH,SEP_CLAUSES,WORD_MULT_CLAUSES,WORD_ADD_0] 274 \\ SIMP_TAC std_ss [arithmeticTheory.ADD1,WORD_MULT_CLAUSES,GSYM word_add_n2w, 275 AC WORD_ADD_ASSOC WORD_ADD_COMM]); 276 277val SEP_REWRITE_THM = store_thm("SEP_REWRITE_THM", 278 ``!q p x y. (!s. q s ==> (x = y)) ==> (q * p x = q * p y) /\ (p x * q = p y * q)``, 279 SIMP_TAC std_ss [FUN_EQ_THM,STAR_def] THEN REPEAT STRIP_TAC THEN METIS_TAC []); 280 281val cond_CONJ = store_thm("cond_CONJ", 282 ``cond (c /\ d) = (cond c * cond d) : 'a set set``, 283 SIMP_TAC std_ss [SEP_CLAUSES]); 284 285val IMP_IMP = store_thm("IMP_IMP", 286 ``!b c d.b /\ (c ==> d) ==> ((b ==> c) ==> d)``, 287 METIS_TAC []); 288 289val _ = export_theory(); 290