1(* ========================================================================= *) 2(* FILE : onestepScript.sml *) 3(* DESCRIPTION : Algebraic framework for verifying processor correctness *) 4(* *) 5(* AUTHOR : (c) Anthony Fox, University of Cambridge *) 6(* DATE : 2000 - 2004 *) 7(* ========================================================================= *) 8 9open HolKernel boolLib bossLib Q; 10open simpLib numLib; 11open combinTheory arithmeticTheory prim_recTheory pred_setTheory; 12 13val _ = new_theory "onestep"; 14 15(* vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv *) 16 17infix \\ << >> 18 19val op \\ = op THEN; 20val op << = op THENL; 21val op >> = op THEN1; 22 23(* ------------------------------------------------------------------------- *) 24 25val FUNPOW_THM = store_thm("FUNPOW_THM", 26 `!f n x. FUNPOW f n (f x) = f (FUNPOW f n x)`, 27 Induct_on `n` \\ ASM_REWRITE_TAC [FUNPOW]); 28 29val FUNPOW_EVAL = store_thm("FUNPOW_EVAL", 30 `!f n x. FUNPOW f n x = if n = 0 then x else FUNPOW f (n-1) (f x)`, 31 Induct_on `n` \\ RW_TAC arith_ss [FUNPOW]); 32 33val FUNPOW_COMP = store_thm("FUNPOW_COMP", 34 `!f a b x. FUNPOW f (a+b) x = FUNPOW f a (FUNPOW f b x)`, 35 Induct_on `b` \\ ASM_REWRITE_TAC [ADD_CLAUSES,FUNPOW]); 36 37(*--------------------------------------------------------------------------- 38 - Iterated Maps ----------------------------------------------------------- 39 ---------------------------------------------------------------------------*) 40 41val IMAP_def = Define ` 42 IMAP f init next = 43 (!a. (f 0 a = init a)) /\ 44 (!t a. (f (SUC t) a = next (f t a)))`; 45 46val IS_IMAP_INIT_def = Define` 47 IS_IMAP_INIT f init = ?next. IMAP f init next`; 48 49val IS_IMAP_def = Define` 50 IS_IMAP f = ?init next. IMAP f init next`; 51 52(*--------------------------------------------------------------------------- 53 - Data Abstraction Criterion ---------------------------------------------- 54 ---------------------------------------------------------------------------*) 55 56val RANGE_def = Define`RANGE f = IMAGE f UNIV`; 57 58val DATA_ABSTRACTION_def = Define ` 59 DATA_ABSTRACTION abs initi inits = 60 SURJ abs (RANGE initi) (RANGE inits)`; 61 62(*--------------------------------------------------------------------------- 63 - Immersions : General, Uniform and Adjunct ------------------------------- 64 ---------------------------------------------------------------------------*) 65 66val FREE_IMMERSION_def = Define` 67 FREE_IMMERSION imm = 68 ((imm 0 = 0) /\ 69 (!t1 t2. t1 < t2 ==> imm t1 < imm t2))`; 70 71val IMMERSION_def = Define ` 72 IMMERSION imm = !a. FREE_IMMERSION (imm a)`; 73 74val IMMERSION = REWRITE_RULE [FREE_IMMERSION_def] IMMERSION_def; 75 76(* 77val IMMERSION = 78 (CONV_RULE (DEPTH_CONV FORALL_AND_CONV) o 79 REWRITE_RULE [FREE_IMMERSION_def]) IMMERSION_def; 80*) 81 82val UIMMERSION_def = Define ` 83 UIMMERSION imm f dur = 84 ((!a. 0 < dur a) /\ 85 (!a. imm a 0 = 0) /\ 86 (!a t. imm a (SUC t) = dur (f (imm a t) a) + imm a t))`; 87 88val AUIMMERSION_def = Define ` 89 AUIMMERSION imm1 imm2 f dur1 dur2 = 90 ((UIMMERSION imm2 f dur2) /\ 91 (!a. 0 < dur1 a) /\ 92 (!a. imm1 a 0 = 0) /\ 93 (!a t. imm1 a (SUC t) = dur1 (f (imm2 a t) a) + imm1 a t))`; 94 95val UNIFORM_def = Define` 96 UNIFORM imm f = ?dur. UIMMERSION imm f dur`; 97 98val ADJUNCT_def = Define` 99 ADJUNCT imm1 imm2 f = ?dur1 dur2. AUIMMERSION imm1 imm2 f dur1 dur2`; 100 101(*--------------------------------------------------------------------------- 102 - Correctness Definitions ------------------------------------------------- 103 ---------------------------------------------------------------------------*) 104 105val CORRECT_def = Define ` 106 CORRECT spec impl imm abs = 107 IMMERSION imm /\ DATA_ABSTRACTION abs (impl 0) (spec 0) /\ 108 (!t a. spec t (abs a) = abs (impl (imm a t) a))`; 109 110val CORRECT_SUP_def = Define ` 111 CORRECT_SUP spec impl imm1 imm2 abs = 112 IMMERSION imm1 /\ IMMERSION imm2 /\ 113 DATA_ABSTRACTION abs (impl 0) (spec 0) /\ 114 (!r a. spec (imm1 a r) (abs a) = abs (impl (imm2 a r) a))`; 115 116val IS_CORRECT_def = Define` 117 IS_CORRECT spec impl = ?imm abs. CORRECT spec impl imm abs`; 118 119val IS_CORRECT_SUP_def = Define` 120 IS_CORRECT_SUP spec impl = 121 ?imm1 imm2 abs. CORRECT_SUP spec impl imm1 imm2 abs`; 122 123(*--------------------------------------------------------------------------- 124 - Time-Consistent State Functions ----------------------------------------- 125 ---------------------------------------------------------------------------*) 126 127val TCON_def = Define ` 128 TCON f = !t1 t2 a. f (t1 + t2) a = f t1 (f t2 a)`; 129 130val TCON_IMMERSION_def = Define ` 131 TCON_IMMERSION f imm = 132 !t1 t2 a. 133 f (imm (f (imm a t2) a) t1 + imm a t2) a = 134 f (imm (f (imm a t2) a) t1) (f (imm a t2) a)`; 135 136(*--------------------------------------------------------------------------- 137 - Data Abstraction Id ----------------------------------------------------- 138 ---------------------------------------------------------------------------*) 139 140val DATA_ABSTRACTION_I = store_thm("DATA_ABSTRACTION_I", 141 `!abs initi. DATA_ABSTRACTION abs initi I = (!a. ?b. abs (initi b) = a)`, 142 RW_TAC std_ss [DATA_ABSTRACTION_def,RANGE_def,IMAGE_DEF,SURJ_DEF, 143 IN_UNIV,GSPECIFICATION] \\ PROVE_TAC []); 144 145(*--------------------------------------------------------------------------- 146 - Uniform Immersions are Immersions --------------------------------------- 147 ---------------------------------------------------------------------------*) 148 149val SUC_COMM_LEMMA = prove( 150 `!t p. t + (SUC p + 1) = SUC (t + (p + 1))`, ARITH_TAC); 151 152val UIMMERSION_MONO_LEMMA = prove( 153 `!imm f dur a t. UIMMERSION imm f dur ==> imm a t < imm a (SUC t)`, 154 RW_TAC bool_ss [UIMMERSION_def,ADD_COMM,LESS_NOT_EQ,LESS_ADD_NONZERO]); 155 156val UIMMERSION_MONO_LEMMA2 = prove( 157 `!imm f dur a t p. UIMMERSION imm f dur ==> imm a t < imm a (t + (p + 1))`, 158 REPEAT STRIP_TAC 159 \\ IMP_RES_TAC UIMMERSION_MONO_LEMMA 160 \\ Induct_on `p` 161 >> ASM_REWRITE_TAC [SYM ONE,GSYM ADD1,UIMMERSION_MONO_LEMMA] 162 \\ FULL_SIMP_TAC bool_ss 163 [SUC_COMM_LEMMA,LESS_IMP_LESS_ADD,ADD_COMM,UIMMERSION_def]); 164 165val UIMMERSION_IS_IMMERSION_LEMMA = store_thm("UIMMERSION_IS_IMMERSION_LEMMA", 166 `!imm f dur. UIMMERSION imm f dur ==> IMMERSION imm`, 167 REPEAT STRIP_TAC 168 \\ IMP_RES_TAC UIMMERSION_MONO_LEMMA2 169 \\ FULL_SIMP_TAC bool_ss [UIMMERSION_def] 170 \\ RW_TAC bool_ss [IMMERSION] 171 \\ IMP_RES_TAC LESS_ADD_1 172 \\ ASM_REWRITE_TAC [UIMMERSION_MONO_LEMMA2]); 173 174val UNIFORM_IMP_IMMERSION = store_thm("UNIFORM_IMP_IMMERSION", 175 `!imm f. UNIFORM imm f ==> IMMERSION imm`, 176 PROVE_TAC [UNIFORM_def,UIMMERSION_IS_IMMERSION_LEMMA]); 177 178(*--------------------------------------------------------------------------- 179 - Uniform Adjunct Immersions are Immersions ------------------------------- 180 ---------------------------------------------------------------------------*) 181 182val AUIMMERSION_MONO_LEMMA = prove( 183 `!f imm1 imm2 dur1 dur2 a t. 184 AUIMMERSION imm1 imm2 f dur1 dur2 ==> imm1 a t < imm1 a (SUC t)`, 185 RW_TAC bool_ss [AUIMMERSION_def,ADD_COMM,LESS_NOT_EQ,LESS_ADD_NONZERO]); 186 187val AUIMMERSION_MONO_LEMMA2 = prove( 188 `!f imm1 imm2 dur1 dur2 a t p. 189 AUIMMERSION imm1 imm2 f dur1 dur2 ==>imm1 a t < imm1 a (t + (p + 1))`, 190 REPEAT STRIP_TAC 191 \\ IMP_RES_TAC AUIMMERSION_MONO_LEMMA 192 \\ Induct_on `p` 193 >> ASM_REWRITE_TAC [SYM ONE,GSYM ADD1,AUIMMERSION_MONO_LEMMA] 194 \\ FULL_SIMP_TAC bool_ss 195 [SUC_COMM_LEMMA,LESS_IMP_LESS_ADD,ADD_COMM,AUIMMERSION_def]); 196 197val AUIMMERSION_IS_IMMERSION_LEMMA = store_thm("AUIMMERSION_IS_IMMERSION_LEMMA", 198 `!f imm1 imm2 dur1 dur2. 199 AUIMMERSION imm1 imm2 f dur1 dur2 ==> IMMERSION imm1 /\ IMMERSION imm2`, 200 REPEAT STRIP_TAC 201 \\ IMP_RES_TAC AUIMMERSION_MONO_LEMMA2 202 \\ FULL_SIMP_TAC bool_ss [AUIMMERSION_def] 203 \\ IMP_RES_TAC UIMMERSION_IS_IMMERSION_LEMMA 204 \\ RW_TAC bool_ss [IMMERSION] 205 \\ IMP_RES_TAC LESS_ADD_1 206 \\ ASM_REWRITE_TAC [AUIMMERSION_MONO_LEMMA2]); 207 208val ADJUNCT_IMP_IMMERSIONS = store_thm("ADJUNCT_IMP_IMMERSIONS", 209 `!imm1 imm2 f. ADJUNCT imm1 imm2 f ==> IMMERSION imm1 /\ IMMERSION imm2`, 210 PROVE_TAC [ADJUNCT_def,AUIMMERSION_IS_IMMERSION_LEMMA]); 211 212val ADJUNCT_IMP_UNIFORM = store_thm("ADJUNCT_IMP__UNIFORM", 213 `!imm1 imm2 f. ADJUNCT imm1 imm2 f ==> UNIFORM imm2 f`, 214 PROVE_TAC [ADJUNCT_def,UNIFORM_def,AUIMMERSION_def]); 215 216(*--------------------------------------------------------------------------- 217 - Correct then Super Correct ---------------------------------------------- 218 ---------------------------------------------------------------------------*) 219 220val CORRECT_IMP_CORRECT_SUP = store_thm("CORRECT_IMP_CORRECT_SUP", 221 `!spec impl. IS_CORRECT spec impl ==> IS_CORRECT_SUP spec impl`, 222 RW_TAC bool_ss [IS_CORRECT_def,IS_CORRECT_SUP_def] 223 \\ EXISTS_TAC `\a t. t` 224 \\ EXISTS_TAC `imm` 225 \\ EXISTS_TAC `abs` 226 \\ FULL_SIMP_TAC arith_ss [CORRECT_def,CORRECT_SUP_def,IMMERSION]); 227 228(*--------------------------------------------------------------------------- 229 - Iterated Maps Unique --------------------------------------------------- 230 ---------------------------------------------------------------------------*) 231 232val IMAP_UNIQUE1 = store_thm("IMAP_UNIQUE1", 233 `!f g init next. IMAP f init next /\ IMAP g init next ==> (f = g)`, 234 RW_TAC bool_ss [IMAP_def] 235 \\ ONCE_REWRITE_TAC [FUN_EQ_THM] 236 \\ Induct 237 \\ ONCE_REWRITE_TAC [FUN_EQ_THM] 238 \\ ASM_REWRITE_TAC []); 239 240(*--------------------------------------------------------------------------- 241 - Time-Consistency Results ------------------------------------------------ 242 ---------------------------------------------------------------------------*) 243 244val TC_IMP_IMAP = store_thm("TC_IMP_IMAP", 245 `!f. TCON f ==> IS_IMAP f`, 246 RW_TAC bool_ss [TCON_def,IMAP_def,IS_IMAP_def] 247 \\ EXISTS_TAC `f 0` 248 \\ EXISTS_TAC `f (SUC 0)` 249 \\ POP_ASSUM (fn th => ASSUME_TAC 250 (GEN_ALL (ONCE_REWRITE_RULE [ADD_COMM] (SPECL [`1`,`t`] th)))) 251 \\ ASM_REWRITE_TAC [ADD1,SYM ONE]); 252 253val TC_THM = store_thm("TC_THM", 254 `!f. TCON f = IS_IMAP f /\ (!t a. f 0 (f t a) = f t a)`, 255 STRIP_TAC \\ EQ_TAC 256 \\ REPEAT STRIP_TAC 257 << [ 258 PROVE_TAC [TC_IMP_IMAP], 259 FULL_SIMP_TAC bool_ss [TCON_def] 260 \\ POP_ASSUM (fn th => REWRITE_TAC 261 [GSYM (REDUCE_RULE (SPECL [`0`,`t`] th))]), 262 FULL_SIMP_TAC bool_ss [TCON_def,IS_IMAP_def,IMAP_def] 263 \\ Induct_on `t1` \\ ASM_REWRITE_TAC [ADD_CLAUSES]]); 264 265val TC_I_THM = store_thm("TC_I_THM", 266 `!f. IS_IMAP_INIT f I ==> TCON f`, 267 PROVE_TAC [TC_THM,IS_IMAP_def,IS_IMAP_INIT_def,IMAP_def,I_THM]); 268 269val TC_IMP_TC_IMMERSION = store_thm("TC_IMP_TC_IMMERSION", 270 `!f. TCON f ==> !imm. TCON_IMMERSION f imm`, 271 RW_TAC bool_ss [TCON_def,TCON_IMMERSION_def]); 272 273val TC_IMMERSION_TC = store_thm("TC_IMMERSION_TC", 274 `!f. TCON_IMMERSION f (\a t. t) = TCON f`, 275 STRIP_TAC \\ EQ_TAC \\ 276 SIMP_TAC bool_ss [TC_IMP_TC_IMMERSION,TCON_def,TCON_IMMERSION_def]); 277 278val IMAP_INIT = store_thm("IMAP_INIT", 279 `!f init. IS_IMAP_INIT f init ==> (f 0 = init)`, 280 RW_TAC bool_ss [IS_IMAP_INIT_def,IMAP_def,FUN_EQ_THM]); 281 282val STATE_FUNPOW_ADD = store_thm("STATE_FUNPOW_ADD", 283 `!f init next. IMAP f init next ==> 284 (!x y a. f (x + y) a = FUNPOW next x (f y a))`, 285 RW_TAC bool_ss [IMAP_def] 286 \\ Induct_on `x` 287 \\ ASM_REWRITE_TAC [ADD,FUNPOW,FUNPOW_THM]); 288 289val STATE_FUNPOW_ZERO = store_thm("STATE_FUNPOW_ZERO", 290 `!f init next. IMAP f init next ==> (!t a. f t a = FUNPOW next t (f 0 a))`, 291 PROVE_TAC [ADD_0,STATE_FUNPOW_ADD]); 292 293val STATE_FUNPOW_INIT = store_thm("STATE_FUNPOW_INIT", 294 `!f init next. IMAP f init next ==> (!t a. f t a = FUNPOW next t (init a))`, 295 PROVE_TAC [STATE_FUNPOW_ZERO,IMAP_def]); 296 297val TC_IMMERSION_LEMMA = store_thm("TC_IMMERSION_LEMMA", 298 `!f imm. IMMERSION imm /\ TCON_IMMERSION f imm ==> 299 (!t a. f 0 (f (imm a t) a) = f (imm a t) a)`, 300 RW_TAC bool_ss [TCON_IMMERSION_def,IMMERSION] 301 \\ POP_ASSUM (fn th => ASSUME_TAC (SPECL [`0`,`t`,`a`] th)) 302 \\ PAT_ASSUM `!a. P` (fn th => RULE_ASSUM_TAC (SIMP_RULE arith_ss [th])) 303 \\ POP_ASSUM (fn th => REWRITE_TAC [SYM th])); 304 305val TC_IMMERSION_LEMMA2 = store_thm("TC_IMMERSION_LEMMA2", 306 `!f imm. IMMERSION imm /\ IS_IMAP f ==> 307 (TCON_IMMERSION f imm = !t a. f 0 (f (imm a t) a) = f (imm a t) a)`, 308 RW_TAC bool_ss [IS_IMAP_def,IMMERSION,TCON_IMMERSION_def] 309 \\ EQ_TAC 310 \\ REPEAT STRIP_TAC << [ 311 POP_ASSUM (fn th => ASSUME_TAC (SPECL [`0`,`t`] th)) 312 \\ PAT_ASSUM `!a. x /\ y` 313 (fn th => RULE_ASSUM_TAC (SIMP_RULE arith_ss [th])) 314 \\ PROVE_TAC [], 315 `IS_IMAP_INIT f init` by PROVE_TAC [IS_IMAP_INIT_def] 316 \\ IMP_RES_TAC IMAP_INIT 317 \\ POP_ASSUM (fn th => RULE_ASSUM_TAC (REWRITE_RULE [th])) 318 \\ IMP_RES_TAC STATE_FUNPOW_INIT 319 \\ ASSUME_TAC FUNPOW_COMP 320 \\ ASM_REWRITE_TAC []]); 321 322(* ------------------------------------------------------------------------- *) 323 324val TC_IMM_LEM = store_thm("TC_IMM_LEM", 325 `!f g imm dur. 326 TCON_IMMERSION f imm /\ UIMMERSION imm f dur /\ 327 IMAP g (f 0) (\a. f (dur a) a) ==> 328 !t a. g t a = f (imm a t) a`, 329 NTAC 5 STRIP_TAC 330 \\ FULL_SIMP_TAC bool_ss [UIMMERSION_def,IMAP_def,TCON_IMMERSION_def] 331 \\ Induct \\ STRIP_TAC 332 \\ ASM_REWRITE_TAC [] 333 \\ PAT_ASSUM `!t1 t2 a. 334 f (imm (f (imm a t2) a) t1 + imm a t2) a = 335 f (imm (f (imm a t2) a) t1) (f (imm a t2) a)` 336 (fn th => ASSUME_TAC (SPECL [`1`,`t`,`a`] th) 337 \\ ASSUME_TAC (SPECL [`0`,`t`] th)) 338 \\ PAT_ASSUM `!a t. imm a (SUC t) = dur (f (imm a t) a) + imm a t` 339 (fn th => ASSUME_TAC (REDUCE_RULE (GEN_ALL (SPECL [`a`,`0`] th)))) 340 \\ PAT_ASSUM `!a. imm a 0 = 0` (fn th => FULL_SIMP_TAC arith_ss [th]) 341 \\ PAT_ASSUM `!a. f (imm a t) a = f 0 (f (imm a t) a)` 342 (fn th => FULL_SIMP_TAC bool_ss [GSYM th])); 343 344val TC_IMMERSION_THM = store_thm("TC_IMMERSION_THM", 345 `!f g imm dur. 346 UIMMERSION imm f dur /\ 347 IMAP g (f 0) (\a. f (dur a) a) ==> 348 (TCON_IMMERSION f imm ==> TCON g)`, 349 REPEAT STRIP_TAC 350 \\ IMP_RES_TAC UIMMERSION_IS_IMMERSION_LEMMA 351 \\ IMP_RES_TAC TC_IMMERSION_LEMMA 352 \\ FULL_SIMP_TAC bool_ss [IS_IMAP_def,TC_THM] 353 \\ STRIP_TAC >> PROVE_TAC [] 354 \\ IMP_RES_TAC TC_IMM_LEM \\ FULL_SIMP_TAC bool_ss [IMAP_def]); 355 356(*--------------------------------------------------------------------------- 357 - Time-Consistency One-Step Theorems -------------------------------------- 358 ---------------------------------------------------------------------------*) 359 360val SPLIT_ITER_LEMMA = prove( 361 `!f init next imm dur. IMAP f init next /\ UIMMERSION imm f dur ==> 362 (!t a. f (dur (f 0 (f (imm a t) a)) + imm a t) a = 363 FUNPOW next (imm (f (imm a t) a) 1) (f (imm a t) a))`, 364 REPEAT STRIP_TAC 365 \\ IMP_RES_TAC STATE_FUNPOW_INIT 366 \\ FULL_SIMP_TAC bool_ss 367 [FUNPOW_COMP,UIMMERSION_def,ONE,ADD_CLAUSES,FUNPOW,FUNPOW_THM]); 368 369val TC_IMMERSION_ONE_STEP_THM = store_thm("TC_IMMERSION_ONE_STEP_THM", 370 `!f imm . IS_IMAP f /\ UNIFORM imm f ==> 371 (TCON_IMMERSION f imm = 372 (!a. f 0 (f (imm a 0) a) = f (imm a 0) a) /\ 373 (!a. f 0 (f (imm a 1) a) = f (imm a 1) a))`, 374 REPEAT STRIP_TAC 375 \\ IMP_RES_TAC UNIFORM_IMP_IMMERSION 376 \\ EQ_TAC \\ STRIP_TAC 377 \\ ASM_SIMP_TAC bool_ss [TC_IMMERSION_LEMMA,TC_IMMERSION_LEMMA2] 378 \\ Induct >> ASM_REWRITE_TAC [] 379 \\ GEN_TAC \\ FULL_SIMP_TAC bool_ss [UNIFORM_def,IS_IMAP_def] 380 \\ PAT_ASSUM `UIMMERSION imm f dur` (fn th => 381 REWRITE_TAC [REWRITE_RULE [UIMMERSION_def] th] \\ ASSUME_TAC th) 382 \\ PAT_ASSUM `!a. f 0 (f (imm a t) a) = f (imm a t) a` 383 (fn th => (ONCE_REWRITE_TAC [GSYM th] \\ ASSUME_TAC th)) 384 \\ IMP_RES_TAC SPLIT_ITER_LEMMA 385 \\ POP_ASSUM (fn th => REWRITE_TAC [th]) 386 \\ POP_ASSUM (fn th => (ONCE_REWRITE_TAC [GSYM th] \\ ASSUME_TAC th)) 387 \\ IMP_RES_TAC STATE_FUNPOW_ZERO 388 \\ POP_ASSUM (fn th => REWRITE_TAC [GSYM th]) 389 \\ ASM_REWRITE_TAC []); 390 391val UNIFORM_ID = prove( 392 `!f. UNIFORM (\a t. t) f`, 393 RW_TAC bool_ss [UNIFORM_def] \\ EXISTS_TAC `\a. 1` 394 \\ REWRITE_TAC [UIMMERSION_def] \\ SIMP_TAC arith_ss []); 395 396val TC_ONE_STEP_THM = store_thm("TC_ONE_STEP_THM", 397 `!f. TCON f = IS_IMAP f /\ 398 (!a. f 0 (f 0 a) = f 0 a) /\ 399 (!a. f 0 (f 1 a) = f 1 a)`, 400 PROVE_TAC [TC_IMP_IMAP, 401 (SIMP_RULE std_ss [UNIFORM_ID,TC_IMMERSION_TC] o 402 SPECL [`f`,`\a t. t`]) TC_IMMERSION_ONE_STEP_THM]); 403 404val TCON_IMMERSION_COR = store_thm("TCON_IMMERSION_COR", 405 `!f imm. 406 UNIFORM imm f /\ TCON_IMMERSION f imm ==> 407 !t1 t2 a. imm a (t1 + t2) = imm (f (imm a t1) a) t2 + imm a t1`, 408 RW_TAC bool_ss [UNIFORM_def,UIMMERSION_def,TCON_IMMERSION_def] 409 \\ Induct_on `t2` \\ ASM_REWRITE_TAC [ADD_CLAUSES] 410 \\ numLib.ARITH_TAC); 411 412(*--------------------------------------------------------------------------- 413 - Correctnes One-Step Theorems -------------------------------------------- 414 ---------------------------------------------------------------------------*) 415 416val ONE_STEP_LEMMA = prove( 417 `!f imm dur. 418 UNIFORM imm f /\ TCON_IMMERSION f imm ==> 419 (!t a. imm a (SUC t) = (imm (f (imm a t) a) 1 + imm a t))`, 420 REPEAT STRIP_TAC 421 \\ IMP_RES_TAC UNIFORM_IMP_IMMERSION 422 \\ IMP_RES_TAC TC_IMMERSION_LEMMA 423 \\ FULL_SIMP_TAC bool_ss [UNIFORM_def,UIMMERSION_def,ONE,ADD_CLAUSES]); 424 425val ONE_STEP_THM = store_thm("ONE_STEP_THM", 426 `!spec impl imm abs. 427 UNIFORM imm impl /\ 428 TCON spec /\ 429 TCON_IMMERSION impl imm /\ 430 DATA_ABSTRACTION abs (impl 0) (spec 0) ==> 431 (CORRECT spec impl imm abs = 432 (!a. spec 0 (abs a) = abs (impl (imm a 0) a)) /\ 433 !a. spec 1 (abs a) = abs (impl (imm a 1) a))`, 434 REPEAT STRIP_TAC 435 \\ IMP_RES_TAC ONE_STEP_LEMMA 436 \\ EQ_TAC 437 \\ RW_TAC bool_ss [CORRECT_def] 438 >> IMP_RES_TAC UNIFORM_IMP_IMMERSION 439 \\ Induct_on `t` >> ASM_REWRITE_TAC [] 440 \\ PAT_ASSUM `!t a. imm a (SUC t) = imm (impl (imm a t) a) 1 + imm a t` 441 (fn th => REWRITE_TAC [th]) 442 \\ PAT_ASSUM `TCON_IMMERSION impl imm` 443 (fn th => REWRITE_TAC [REWRITE_RULE [TCON_IMMERSION_def] th]) 444 \\ PAT_ASSUM `!a. spec 1 (abs a) = abs (impl (imm a 1) a)` 445 (fn th => REWRITE_TAC [ONE,GSYM th]) 446 \\ POP_ASSUM (fn th => REWRITE_TAC [GSYM th]) 447 \\ RULE_ASSUM_TAC (REWRITE_RULE [TCON_def]) 448 \\ PAT_ASSUM `!t1 t2 a. spec (t1 + t2) a = spec t1 (spec t2 a)` 449 (fn th => REWRITE_TAC [SYM ONE,GSYM (SPECL [`SUC 0`,`t`] th)]) 450 \\ SIMP_TAC arith_ss [ADD1]); 451 452(* ------------------------------------------------------------------------- *) 453 454val ONE_STEP_SUP_LEMMA = prove( 455 `!f imm1 imm2. ADJUNCT imm1 imm2 f /\ TCON_IMMERSION f imm2 ==> 456 (!r a. imm1 a (SUC r) = (imm1 (f (imm2 a r) a) 1 + imm1 a r))`, 457 REPEAT STRIP_TAC 458 \\ IMP_RES_TAC ADJUNCT_IMP_IMMERSIONS 459 \\ IMP_RES_TAC TC_IMMERSION_LEMMA 460 \\ FULL_SIMP_TAC bool_ss 461 [ADJUNCT_def,UIMMERSION_def,AUIMMERSION_def,ONE,ADD_CLAUSES]); 462 463val ONE_STEP_SUP_THM = store_thm("ONE_STEP_SUP_THM", 464 `!spec impl imm1 imm2 abs. 465 (ADJUNCT imm1 imm2 impl /\ 466 TCON spec /\ 467 TCON_IMMERSION impl imm2) ==> 468 (CORRECT_SUP spec impl imm1 imm2 abs = 469 DATA_ABSTRACTION abs (impl 0) (spec 0) /\ 470 (!a. spec (imm1 a 0) (abs a) = abs (impl (imm2 a 0) a)) /\ 471 !a. spec (imm1 a 1) (abs a) = abs (impl (imm2 a 1) a))`, 472 REPEAT STRIP_TAC 473 \\ IMP_RES_TAC ADJUNCT_IMP_UNIFORM 474 \\ EQ_TAC 475 \\ RW_TAC bool_ss [CORRECT_SUP_def] 476 << [ 477 IMP_RES_TAC ADJUNCT_IMP_IMMERSIONS, 478 IMP_RES_TAC ADJUNCT_IMP_IMMERSIONS, 479 Induct_on `r` >> ASM_REWRITE_TAC [] 480 \\ IMP_RES_TAC ONE_STEP_SUP_LEMMA 481 \\ POP_ASSUM (fn th => REWRITE_TAC [th]) 482 \\ IMP_RES_TAC ONE_STEP_LEMMA 483 \\ REWRITE_TAC [ONE] 484 \\ POP_ASSUM (fn th => REWRITE_TAC [th]) 485 \\ PAT_ASSUM `TCON_IMMERSION impl imm2` 486 (fn th => REWRITE_TAC [REWRITE_RULE [TCON_IMMERSION_def] th]) 487 \\ PAT_ASSUM `!a. spec (imm1 a 1) (abs a) = abs (impl (imm2 a 1) a)` 488 (fn th => REWRITE_TAC [ONE,GSYM th]) 489 \\ RULE_ASSUM_TAC (REWRITE_RULE [TCON_def]) 490 \\ POP_ASSUM (fn th => ASM_REWRITE_TAC [GSYM th])]); 491 492(* ------------------------------------------------------------------------- *) 493 494val CORRECT_TRANS = store_thm("CORRECT_TRANS", 495 `!f1 f2 f3 imm1 imm2 abs1 abs2. 496 CORRECT f1 f2 imm1 abs1 /\ CORRECT f2 f3 imm2 abs2 ==> 497 CORRECT f1 f3 (\x. imm2 x o imm1 (abs2 x)) (abs1 o abs2)`, 498 RW_TAC bool_ss [CORRECT_def,IMMERSION,DATA_ABSTRACTION_def,o_THM, 499 SURJ_DEF,RANGE_def,IMAGE_DEF,IN_UNIV,GSPECIFICATION] 500 \\ PROVE_TAC []); 501 502(* ------------------------------------------------------------------------- *) 503 504val IMAP_COMP = store_thm("IMAP_COMP", 505 `!f init next. IMAP f init next ==> 506 (!t a. f t a = if t = 0 then init a else next (f (t-1) a))`, 507 REPEAT STRIP_TAC \\ FULL_SIMP_TAC bool_ss [IMAP_def] 508 \\ RW_TAC bool_ss [] 509 \\ RULE_ASSUM_TAC (REWRITE_RULE [NOT_ZERO_LT_ZERO]) 510 \\ IMP_RES_TAC LESS_ADD_1 511 \\ RW_TAC arith_ss [GSYM ADD1]); 512 513val UIMMERSION_COMP = prove( 514 `!imm f dur. UIMMERSION imm f dur ==> 515 (!t a. imm a t = 516 if t = 0 then 0 517 else dur (f (imm a (t-1)) a) + imm a (t-1))`, 518 REPEAT STRIP_TAC \\ FULL_SIMP_TAC bool_ss [UIMMERSION_def] 519 \\ RW_TAC bool_ss [UIMMERSION_def] 520 \\ RULE_ASSUM_TAC (REWRITE_RULE [NOT_ZERO_LT_ZERO]) 521 \\ IMP_RES_TAC LESS_ADD_1 522 \\ RW_TAC arith_ss [GSYM ADD1]); 523 524val UIMMERSION_ONE = store_thm("UIMMERSION_ONE", 525 `!f init next imm dur. 526 IS_IMAP_INIT f init /\ UIMMERSION imm f dur ==> 527 !a. imm a 1 = dur (init a)`, 528 RW_TAC bool_ss [UIMMERSION_def,IS_IMAP_INIT_def,IMAP_def,ONE,ADD_0] 529 \\ ASM_REWRITE_TAC []); 530 531val IMAP_NEXT = store_thm("IMAP_NEXT", 532 `!f init next. IMAP f init next ==> 533 (f t a = b) /\ (next b = c) ==> 534 (f (t + 1) a = c)`, 535 RW_TAC std_ss [IMAP_def,ADD1] 536); 537 538(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *) 539 540val _ = export_theory(); 541