1 2open HolKernel boolLib bossLib Parse; 3open pred_setTheory arithmeticTheory set_sepTheory tailrecTheory; 4 5val _ = new_theory "prog"; 6 7infix \\ 8val op \\ = op THEN; 9 10 11(* ---- definitions ----- *) 12 13val _ = type_abbrev("processor", 14 ``: ('a->'b set) # ('a->'a->bool) # ('c->'b set) # ('a->'a->bool) # ('a->bool)``); 15 16val rel_sequence_def = Define ` 17 rel_sequence R seq state = 18 (seq 0 = state) /\ 19 !n. if (?x. R (seq n) x) then R (seq n) (seq (SUC n)) else (seq (SUC n) = seq n)`; 20 21val SEP_REFINE_def = Define ` 22 SEP_REFINE p less to_set state = ?s. less s state /\ p (to_set s)`; 23 24val RUN_def = Define ` 25 RUN ((to_set,next,instr,less,allow):('a,'b,'c)processor) p q = 26 !state r. SEP_REFINE (p * r) less to_set state \/ allow state ==> 27 !seq. rel_sequence next seq state ==> 28 ?i. SEP_REFINE (q * r) less to_set (seq i) \/ allow (seq i)`; 29 30val CODE_POOL_def = Define ` 31 CODE_POOL instr c = \s. s = BIGUNION (IMAGE instr c)`; 32 33val SPEC_def = Define ` 34 SPEC ((to_set,next,instr,less,allow):('a,'b,'c)processor) p c q = 35 RUN (to_set,next,instr,less,allow) (CODE_POOL instr c * p) 36 (CODE_POOL instr c * q)`; 37 38 39(* ---- theorems ---- *) 40 41val INIT_LEMMA = prove( 42 ``(!to_set next instr less allow. P (to_set,next,instr,less,allow)) ==> 43 (!x:('a,'b,'c)processor. P x)``, 44 SIMP_TAC std_ss [pairTheory.FORALL_PROD]); 45 46val INIT_TAC = HO_MATCH_MP_TAC INIT_LEMMA THEN NTAC 5 STRIP_TAC; 47val RW = REWRITE_RULE; 48 49val RUN_thm = store_thm("RUN_thm", 50 ``RUN ((to_set,next,instr,less,allow):('a,'b,'c)processor) p q = 51 !state r. SEP_REFINE (p * r) less to_set state /\ ~allow state ==> 52 !seq. rel_sequence next seq state ==> 53 ?i. SEP_REFINE (q * r) less to_set (seq i) \/ allow (seq i)``, 54 SIMP_TAC std_ss [RUN_def] 55 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC THEN1 (METIS_TAC []) 56 \\ Cases_on `allow state` 57 \\ TRY (Q.EXISTS_TAC `0` \\ FULL_SIMP_TAC std_ss [rel_sequence_def] \\ NO_TAC) 58 \\ METIS_TAC []); 59 60val RUN_EQ_SPEC = store_thm("RUN_EQ_SPEC", 61 ``!x. RUN x p q = SPEC x p {} q``, 62 INIT_TAC \\ sg `CODE_POOL instr {} = emp` 63 \\ ASM_REWRITE_TAC [SEP_CLAUSES,SPEC_def] 64 \\ REWRITE_TAC [FUN_EQ_THM,CODE_POOL_def,IMAGE_EMPTY,BIGUNION_EMPTY,emp_def]); 65 66val SPEC_FRAME = store_thm("SPEC_FRAME", 67 ``!x p c q. SPEC x p c q ==> !r. SPEC x (p * r) c (q * r)``, 68 INIT_TAC \\ SIMP_TAC bool_ss [RUN_def,GSYM STAR_ASSOC,SPEC_def] 69 \\ REPEAT STRIP_TAC 70 \\ Q.PAT_X_ASSUM `!state r. bbb` (ASSUME_TAC o Q.SPECL [`state`,`r * r'`]) 71 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC] \\ METIS_TAC []); 72 73val SPEC_FALSE_PRE = store_thm("SPEC_FALSE_PRE", 74 ``!x c q. SPEC x SEP_F c q``, 75 INIT_TAC \\ REWRITE_TAC [RUN_def,SPEC_def,SEP_CLAUSES,SEP_REFINE_def] 76 \\ SIMP_TAC std_ss [SEP_F_def] 77 \\ REPEAT STRIP_TAC \\ Q.EXISTS_TAC `0` 78 \\ FULL_SIMP_TAC std_ss [rel_sequence_def]); 79 80val SPEC_STRENGTHEN = store_thm("SPEC_STRENGTHEN", 81 ``!x p c q. SPEC x p c q ==> !r. SEP_IMP r p ==> SPEC x r c q``, 82 INIT_TAC \\ SIMP_TAC bool_ss [RUN_thm,SPEC_def,GSYM STAR_ASSOC,SEP_REFINE_def] 83 \\ REPEAT STRIP_TAC 84 \\ `(CODE_POOL instr c * (p * r')) (to_set s)` by 85 METIS_TAC [SEP_IMP_def,SEP_IMP_REFL,SEP_IMP_STAR] 86 \\ METIS_TAC []); 87 88val SPEC_WEAKEN = store_thm("SPEC_WEAKEN", 89 ``!x p c q. SPEC x p c q ==> !r. SEP_IMP q r ==> SPEC x p c r``, 90 INIT_TAC \\ SIMP_TAC bool_ss [RUN_thm,SPEC_def,GSYM STAR_ASSOC,PULL_FORALL] 91 \\ REPEAT STRIP_TAC 92 \\ Q.PAT_X_ASSUM `!x.bbb` (MP_TAC o Q.SPECL [`state`,`r'`,`seq`]) 93 \\ FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 94 \\ Q.EXISTS_TAC `i` \\ FULL_SIMP_TAC std_ss [] 95 \\ DISJ1_TAC \\ FULL_SIMP_TAC std_ss [SEP_REFINE_def] 96 \\ REPEAT STRIP_TAC 97 \\ Q.EXISTS_TAC `s'` \\ ASM_SIMP_TAC std_ss [] 98 \\ METIS_TAC [SEP_IMP_def,SEP_IMP_REFL,SEP_IMP_STAR,SEP_REFINE_def]); 99 100val SPEC_STRENGTHEN_WEAKEN = store_thm("SPEC_STRENGTHEN_WEAKEN", 101 ``!x p c q. SPEC x p c q ==> !r1 r2. SEP_IMP r1 p /\ SEP_IMP q r2 ==> SPEC x r1 c r2``, 102 METIS_TAC [SPEC_STRENGTHEN,SPEC_WEAKEN]); 103 104val CODE_POOL_LEMMA = prove( 105 ``!c c' i. ?r. CODE_POOL i (c UNION c') = CODE_POOL i c * r``, 106 REPEAT STRIP_TAC \\ REWRITE_TAC [CODE_POOL_def,IMAGE_UNION,BIGUNION_UNION,STAR_def] 107 \\ Q.EXISTS_TAC `\s. s = BIGUNION (IMAGE i c') DIFF BIGUNION (IMAGE i c)` 108 \\ ONCE_REWRITE_TAC [FUN_EQ_THM] \\ SIMP_TAC std_ss [] 109 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 110 \\ FULL_SIMP_TAC bool_ss [SPLIT_def,EXTENSION,IN_BIGUNION,IN_DIFF, 111 IN_UNION,DISJOINT_DEF,IN_INTER,NOT_IN_EMPTY] \\ METIS_TAC []); 112 113val SPEC_CODE = store_thm("SPEC_CODE", 114 ``!x p c q. SPEC x (CODE_POOL (FST (SND (SND x))) c * p) {} 115 (CODE_POOL (FST (SND (SND x))) c * q) = 116 SPEC x p c q``, 117 INIT_TAC \\ REWRITE_TAC [pairTheory.SND] \\ REWRITE_TAC [SPEC_def, 118 CODE_POOL_def,IMAGE_EMPTY,BIGUNION_EMPTY,GSYM emp_def,SEP_CLAUSES]); 119 120val SPEC_ADD_CODE = store_thm("SPEC_ADD_CODE", 121 ``!x p c q. SPEC x p c q ==> !c'. SPEC x p (c UNION c') q``, 122 INIT_TAC \\ REWRITE_TAC [ONCE_REWRITE_RULE [STAR_COMM] SPEC_def,RUN_def] 123 \\ REWRITE_TAC [GSYM STAR_ASSOC] \\ REPEAT STRIP_TAC 124 \\ `?t. CODE_POOL instr (c UNION c') = CODE_POOL instr c * t` by 125 METIS_TAC [CODE_POOL_LEMMA] \\ FULL_SIMP_TAC bool_ss [GSYM STAR_ASSOC] 126 \\ RES_TAC \\ FULL_SIMP_TAC bool_ss [GSYM STAR_ASSOC] \\ METIS_TAC []); 127 128val SPEC_COMBINE = store_thm("SPEC_COMBINE", 129 ``!x i j p c1 c2 q b. 130 (b /\ i ==> SPEC x p c1 q) ==> (~b /\ j ==> SPEC x p c2 q) ==> 131 ((if b then i else j) ==> SPEC x p (c1 UNION c2) q)``, 132 Cases_on `b` THEN REWRITE_TAC [] THEN REPEAT STRIP_TAC THEN RES_TAC 133 THEN IMP_RES_TAC SPEC_ADD_CODE 134 THEN ASM_REWRITE_TAC [] 135 THEN ONCE_REWRITE_TAC [UNION_COMM] 136 THEN ASM_REWRITE_TAC []); 137 138val SPEC_SUBSET_CODE = store_thm("SPEC_SUBSET_CODE", 139 ``!x p c q. SPEC x p c q ==> !c'. c SUBSET c' ==> SPEC x p c' q``, 140 REPEAT STRIP_TAC \\ FULL_SIMP_TAC bool_ss [SUBSET_DEF] 141 \\ `c' = c UNION c'` 142 by (FULL_SIMP_TAC bool_ss [EXTENSION,IN_UNION] \\ METIS_TAC[]) 143 \\ METIS_TAC [SPEC_ADD_CODE]); 144 145val SPEC_REFL = store_thm("SPEC_REFL", 146 ``!x:('a,'b,'c)processor p c. SPEC x p c p``, 147 INIT_TAC \\ SIMP_TAC std_ss [RUN_def,SPEC_def] \\ REPEAT STRIP_TAC 148 \\ Q.EXISTS_TAC `0` \\ FULL_SIMP_TAC bool_ss [rel_sequence_def]); 149 150val rel_sequence_shift = prove( 151 ``!n seq s. rel_sequence n seq s ==> !i. rel_sequence n (\j. seq (i + j)) (seq i)``, 152 REWRITE_TAC [rel_sequence_def] \\ REPEAT STRIP_TAC \\ SIMP_TAC std_ss [] 153 \\ Cases_on `?s. n (seq (i + n')) s` \\ ASM_REWRITE_TAC [] 154 \\ FULL_SIMP_TAC std_ss [ADD1,ADD_ASSOC] \\ METIS_TAC []); 155 156val SEP_REFINE_DISJ = prove( 157 ``SEP_REFINE (p \/ q) less to_set state = 158 SEP_REFINE p less to_set state \/ SEP_REFINE q less to_set state``, 159 SIMP_TAC std_ss [SEP_REFINE_def,SEP_DISJ_def] \\ METIS_TAC []); 160 161val SPEC_COMPOSE_LEMMA = prove( 162 ``!x c p1 p2 m q1 q2. 163 SPEC x p1 c (q1 \/ m) /\ SPEC x (m \/ p2) c q2 ==> 164 SPEC x (p1 \/ p2) c (q1 \/ q2)``, 165 INIT_TAC \\ FULL_SIMP_TAC std_ss [SPEC_def,RUN_def] 166 \\ REVERSE (REPEAT STRIP_TAC) 167 THEN1 (Q.EXISTS_TAC `0` \\ FULL_SIMP_TAC std_ss [rel_sequence_def]) 168 \\ REVERSE (FULL_SIMP_TAC bool_ss [SEP_CLAUSES,SEP_REFINE_DISJ]) THEN1 METIS_TAC [] 169 \\ FULL_SIMP_TAC std_ss [PULL_FORALL] 170 \\ Q.PAT_X_ASSUM `!x.bbb` MP_TAC 171 \\ Q.PAT_X_ASSUM `!x.bbb` (MP_TAC o Q.SPECL [`state`,`r`,`seq`]) 172 \\ FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 173 \\ TRY (Q.EXISTS_TAC `i` \\ FULL_SIMP_TAC std_ss [] \\ NO_TAC) 174 \\ Q.PAT_X_ASSUM `!x.bbb` (MP_TAC o Q.SPECL [`seq (i:num)`,`r`,`(\j. seq (i + j))`]) 175 \\ `rel_sequence next (\j. seq (i + j)) (seq i)` by METIS_TAC [rel_sequence_shift] 176 \\ FULL_SIMP_TAC std_ss [] \\ REVERSE STRIP_TAC \\ METIS_TAC []) 177 178val SPEC_MERGE = store_thm("SPEC_MERGE", 179 ``!x p1 p2 c1 m c2 q1 q2. 180 SPEC x p1 c1 (q1 \/ m) /\ SPEC x (m \/ p2) c2 q2 ==> 181 SPEC x (p1 \/ p2) (c1 UNION c2) (q1 \/ q2)``, 182 METIS_TAC [SPEC_ADD_CODE,SPEC_COMPOSE_LEMMA,UNION_COMM]); 183 184val SPEC_COMPOSE = store_thm("SPEC_COMPOSE", 185 ``!x p c1 m c2 q. SPEC x p c1 m /\ SPEC x m c2 q ==> SPEC x p (c1 UNION c2) q``, 186 REPEAT STRIP_TAC \\ MATCH_MP_TAC (REWRITE_RULE [SEP_CLAUSES] 187 (Q.SPECL [`x`,`p`,`SEP_F`,`c1`,`m`,`c2`,`SEP_F`,`q`] SPEC_MERGE)) 188 \\ ASM_SIMP_TAC bool_ss []); 189 190val SPEC_COMPOSE_I = store_thm("SPEC_COMPOSE_I", 191 ``!x p c q1 q2 q3 q4. 192 SPEC x (q1 * q3) c q2 ==> SPEC x p c (q1 * q4) ==> 193 SEP_IMP q4 q3 ==> SPEC x p c q2``, 194 REPEAT STRIP_TAC 195 \\ `SEP_IMP (q1 * q4) (q1 * q3)` by METIS_TAC [SEP_IMP_REFL,SEP_IMP_STAR] 196 \\ IMP_RES_TAC SPEC_WEAKEN \\ METIS_TAC [SPEC_COMPOSE,UNION_IDEMPOT]); 197 198val SPEC_FRAME_COMPOSE = store_thm("SPEC_FRAME_COMPOSE", 199 ``!x p p' c1 m c2 q q' b1 b2. 200 (b1 ==> SPEC x (m * q') c2 q) ==> 201 (b2 ==> SPEC x p c1 (m * p')) ==> 202 (b1 /\ b2) ==> SPEC x (p * q') (c1 UNION c2) (q * p')``, 203 REPEAT STRIP_TAC \\ MATCH_MP_TAC SPEC_COMPOSE 204 \\ Q.EXISTS_TAC `m * p' * q'` \\ REPEAT STRIP_TAC \\ RES_TAC 205 THEN1 (MATCH_MP_TAC SPEC_FRAME \\ ASM_SIMP_TAC std_ss []) 206 \\ IMP_RES_TAC SPEC_FRAME \\ METIS_TAC [STAR_ASSOC,STAR_COMM]); 207 208val SPEC_FRAME_COMPOSE_DISJ = store_thm("SPEC_FRAME_COMPOSE_DISJ", 209 ``!x p p' c1 m c2 q q' b1 b2 d. 210 (b1 ==> SPEC x (m * q') c2 q) ==> 211 (b2 ==> SPEC x p c1 (m * p' \/ d)) ==> 212 (b1 /\ b2) ==> SPEC x (p * q') (c1 UNION c2) (q * p' \/ d * q')``, 213 REPEAT STRIP_TAC \\ MATCH_MP_TAC SPEC_COMPOSE \\ FULL_SIMP_TAC std_ss [] 214 \\ Q.EXISTS_TAC `m * p' * q' \/ d * q'` \\ REPEAT STRIP_TAC 215 \\ IMP_RES_TAC SPEC_FRAME \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES] 216 \\ MATCH_MP_TAC (RW [SEP_CLAUSES,UNION_IDEMPOT] 217 (Q.SPECL [`x`,`p1`,`p2`,`c`,`SEP_F`,`c`] SPEC_MERGE)) 218 \\ POP_ASSUM (MP_TAC o Q.SPEC `p'`) 219 \\ FULL_SIMP_TAC std_ss [SPEC_REFL, AC STAR_ASSOC STAR_COMM]); 220 221val SEP_REFINE_HIDE = prove( 222 ``SEP_REFINE (~p * q) less to_set state = 223 ?x. SEP_REFINE (p x * q) less to_set state``, 224 SIMP_TAC std_ss [SEP_REFINE_def,SEP_HIDE_def,SEP_CLAUSES] 225 \\ SIMP_TAC std_ss [SEP_EXISTS] \\ METIS_TAC []); 226 227val SPEC_HIDE_PRE = store_thm("SPEC_HIDE_PRE", 228 ``!x p p' c q. (!y:'var. SPEC x (p * p' y) c q) = SPEC x (p * ~ p') c q``, 229 INIT_TAC \\ REPEAT STRIP_TAC \\ ONCE_REWRITE_TAC [STAR_COMM] 230 \\ REWRITE_TAC [ONCE_REWRITE_RULE [STAR_COMM] SPEC_def,RUN_def,GSYM STAR_ASSOC] 231 \\ SIMP_TAC std_ss [SEP_REFINE_HIDE] \\ METIS_TAC []); 232 233val SPEC_PRE_EXISTS = store_thm("SPEC_PRE_EXISTS", 234 ``!x p c q. (!y:'var. SPEC x (p y) c q) = SPEC x (SEP_EXISTS y. p y) c q``, 235 INIT_TAC \\ REPEAT STRIP_TAC \\ ONCE_REWRITE_TAC [STAR_COMM] 236 \\ SIMP_TAC std_ss [GSYM (RW [SEP_CLAUSES,SEP_HIDE_def] (Q.SPECL [`x`,`emp`] SPEC_HIDE_PRE))]); 237 238val SEP_HIDE_INTRO = prove( 239 ``!p q x s. SEP_IMP (p * q x) (p * ~ q)``, 240 SIMP_TAC std_ss [STAR_def,SEP_HIDE_def,SEP_IMP_def,SEP_EXISTS] \\ METIS_TAC []); 241 242val SPEC_HIDE_POST = store_thm("SPEC_HIDE_POST", 243 ``!x p c q q' y:'var. SPEC x p c (q * q' y) ==> SPEC x p c (q * ~ q')``, 244 METIS_TAC [SPEC_WEAKEN,SEP_HIDE_INTRO]); 245 246val SPEC_MOVE_COND = store_thm("SPEC_MOVE_COND", 247 ``!x p c q g. SPEC x (p * cond g) c q = g ==> SPEC x p c q``, 248 INIT_TAC \\ Cases_on `g` 249 \\ REWRITE_TAC [SPEC_def,RUN_thm,SEP_CLAUSES,SEP_REFINE_def] 250 \\ REWRITE_TAC [SEP_F_def]); 251 252val SPEC_DUPLICATE_COND = store_thm("SPEC_DUPLICATE_COND", 253 ``!x p c q g. SPEC x (p * cond g) c q ==> SPEC x (p * cond g) c (q * cond g)``, 254 SIMP_TAC std_ss [SPEC_MOVE_COND,SEP_CLAUSES]); 255 256val SPEC_MERGE_COND = store_thm("SPEC_MERGE_COND", 257 ``!x p c1 c2 q b1 b2. 258 SPEC x (p * cond b1) c1 q ==> 259 SPEC x (p * cond b2) c2 q ==> 260 SPEC x (p * cond (b1 \/ b2)) (c1 UNION c2) q``, 261 Cases_on `b1` \\ Cases_on `b2` 262 \\ SIMP_TAC std_ss [SEP_CLAUSES,SPEC_FALSE_PRE] 263 \\ METIS_TAC [SPEC_ADD_CODE,SPEC_MERGE,SEP_CLAUSES,UNION_COMM]); 264 265val SPEC_MOVE_COND_POST = store_thm("SPEC_MOVE_COND_POST", 266 ``SPEC m (p * cond b) c q = SPEC m (p * cond b) c (q * cond b)``, 267 SIMP_TAC std_ss [SPEC_MOVE_COND,SEP_CLAUSES]); 268 269val SPEC_ADD_DISJ = store_thm("SPEC_ADD_DISJ", 270 ``!x p c q. SPEC x p c q ==> !r. SPEC x p c (q \/ r)``, 271 REPEAT STRIP_TAC \\ IMP_RES_TAC SPEC_WEAKEN 272 \\ POP_ASSUM (MATCH_MP_TAC o Q.SPEC `q \/ r`) 273 \\ FULL_SIMP_TAC std_ss [SEP_IMP_def,SEP_DISJ_def]); 274 275val SPEC_PRE_DISJ = store_thm("SPEC_PRE_DISJ", 276 ``!x p1 p2 c q. SPEC x (p1 \/ p2) c q = SPEC x p1 c q /\ SPEC x p2 c q``, 277 INIT_TAC \\ SIMP_TAC std_ss [SPEC_def,SEP_CLAUSES,RUN_def, 278 SEP_REFINE_DISJ] \\ METIS_TAC []); 279 280val SPEC_PRE_DISJ_INTRO = store_thm("SPEC_PRE_DISJ_INTRO", 281 ``!x p c q r. SPEC x p c (q \/ r) ==> SPEC x (p \/ r) c (q \/ r)``, 282 SIMP_TAC std_ss [SPEC_PRE_DISJ] \\ REPEAT STRIP_TAC 283 \\ MATCH_MP_TAC (MATCH_MP SPEC_WEAKEN (SPEC_ALL SPEC_REFL)) 284 \\ FULL_SIMP_TAC std_ss [SEP_IMP_def,SEP_DISJ_def]); 285 286val SPEC_EXISTS_EXISTS = store_thm("SPEC_EXISTS_EXISTS", 287 ``(!x. SPEC m (P x) c (Q x)) ==> SPEC m (SEP_EXISTS x. P x) c (SEP_EXISTS x. Q x)``, 288 SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS] \\ REPEAT STRIP_TAC 289 \\ POP_ASSUM (ASSUME_TAC o Q.SPEC `x`) 290 \\ IMP_RES_TAC SPEC_WEAKEN \\ POP_ASSUM MATCH_MP_TAC 291 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS_THM] \\ METIS_TAC []); 292 293val SPEC_TAILREC = store_thm("SPEC_TAILREC", 294 ``!f1 (f2:'a->'b) g p res res' c m. 295 (!x y. g x /\ p x /\ (y = f1 x) ==> SPEC m (res x) c (res y)) /\ 296 (!x y. ~g x /\ p x /\ (y = f2 x) ==> SPEC m (res x) c (res' y)) ==> 297 (!x. TAILREC_PRE f1 g p x ==> SPEC m (res x) c (res' (TAILREC f1 f2 g x)))``, 298 NTAC 9 STRIP_TAC THEN HO_MATCH_MP_TAC TAILREC_PRE_INDUCT 299 THEN METIS_TAC [TAILREC_THM,UNION_IDEMPOT,SPEC_COMPOSE]); 300 301val SPEC_TAILREC_NEW = store_thm("SPEC_TAILREC_NEW", 302 ``!f1 (f2:'a->'b) g p res res' c m. 303 (!z x y. g x /\ p x /\ (y = f1 x) ==> SPEC m (res z x) c (res z y)) /\ 304 (!z x y. ~g x /\ p x /\ (y = f2 x) ==> SPEC m (res z x) c (res' z y)) ==> 305 (!z x. TAILREC_PRE f1 g p x ==> SPEC m (res z x) c (res' z (TAILREC f1 f2 g x)))``, 306 NTAC 10 STRIP_TAC THEN HO_MATCH_MP_TAC TAILREC_PRE_INDUCT 307 THEN METIS_TAC [TAILREC_THM,UNION_IDEMPOT,SPEC_COMPOSE]); 308 309val SPEC_SHORT_TAILREC = store_thm("SPEC_SHORT_TAILREC", 310 ``!(f:'a -> ('a + 'b) # bool) res res' c m. 311 (!x y. ISL (FST (f x)) /\ SND (f x) /\ (y = OUTL (FST (f x))) ==> SPEC m (res x) c (res y)) /\ 312 (!x y. ~ISL (FST (f x)) /\ SND (f x) /\ (y = OUTR (FST (f x))) ==> SPEC m (res x) c (res' y)) ==> 313 (!x. SHORT_TAILREC_PRE f x ==> SPEC m (res x) c (res' (SHORT_TAILREC f x)))``, 314 SIMP_TAC std_ss [SHORT_TAILREC_PRE_def,SHORT_TAILREC_def] \\ NTAC 6 STRIP_TAC 315 \\ MATCH_MP_TAC SPEC_TAILREC \\ ASM_SIMP_TAC std_ss []); 316 317val SPEC_SHORT_TAILREC_NEW = store_thm("SPEC_SHORT_TAILREC_NEW", 318 ``!(f:'a -> ('a + 'b) # bool) res res' c m. 319 (!z x y. ISL (FST (f x)) /\ SND (f x) /\ (y = OUTL (FST (f x))) ==> SPEC m (res z x) c (res z y)) /\ 320 (!z x y. ~ISL (FST (f x)) /\ SND (f x) /\ (y = OUTR (FST (f x))) ==> SPEC m (res z x) c (res' z y)) ==> 321 (!z x. SHORT_TAILREC_PRE f x ==> SPEC m (res z x) c (res' z (SHORT_TAILREC f x)))``, 322 SIMP_TAC std_ss [SHORT_TAILREC_PRE_def,SHORT_TAILREC_def] \\ NTAC 6 STRIP_TAC 323 \\ MATCH_MP_TAC SPEC_TAILREC_NEW \\ ASM_SIMP_TAC std_ss []); 324 325 326val _ = export_theory(); 327