1(*****************************************************************************) 2(* Test script for encoding using finite maps. *) 3(* This is based on the opsem script with translations placed after each *) 4(* definition to mark progress. *) 5(*****************************************************************************) 6 7set_trace "Unicode" 0; 8set_trace "pp_annotations" 0; 9 10app load ["acl2encodeLib", "stringLib", "finite_mapTheory", "intLib", 11 "pred_setTheory","whileTheory","optionTheory","unwindLib", "finite_mapTheory"]; 12open HolKernel Parse boolLib bossLib 13 stringLib IndDefLib IndDefRules finite_mapTheory relationTheory 14 arithmeticTheory prim_recTheory 15 pred_setTheory whileTheory combinTheory optionTheory unwindLib; 16intLib.deprecate_int(); 17clear_overloads_on "TC"; (* Stop TC R printing as TC^+ *) 18 19 20val _ = 21 Hol_datatype 22 `value = Scalar of int | Array of (num |-> int)`; 23 24val _ = acl2encodeLib.initialise_type ``:value``; 25 26val _ = type_abbrev("state", ``:string |-> value``); 27val _ = type_abbrev("sfun", ``:state -> state``); 28val _ = type_abbrev("pred", ``:state -> bool``); 29val _ = type_abbrev("vars", ``:string -> bool``); 30 31val isScalar_def = 32 Define 33 `(isScalar(Scalar n) = T) /\ (isScalar(Array a) = F)`; 34 35val _ = acl2encodeLib.translate_simple_function [(``isScalar``, "acl2isScalar")] isScalar_def; 36 37val ScalarOf_def = 38 Define 39 `ScalarOf(Scalar n) = n`; 40 41val _ = acl2encodeLib.translate_simple_function [(``ScalarOf``, "acl2ScalarOf")] ScalarOf_def; 42 43val isArray_def = 44 Define 45 `(isArray(Array a) = T) /\ (isArray(Scalar n) = F)`; 46 47val _ = acl2encodeLib.translate_simple_function [(``isArray``, "acl2isArray")] isArray_def; 48 49val ArrayOf_def = 50 Define 51 `ArrayOf(Array a) = a`; 52 53val _ = encodeLib.set_bottom_value ``:'a |-> 'b`` ``FEMPTY : 'a |-> 'b``; 54 55val _ = acl2encodeLib.translate_simple_function [(``ArrayOf``, "acl2ArrayOf")] ArrayOf_def; 56 57(*---------------------------------------------------------------------------*) 58(* Syntax of the programming language. *) 59(*---------------------------------------------------------------------------*) 60 61(*---------------------------------------------------------------------------*) 62(* Natural number (nexp), boolean (bexp) and array expressions (aexp) *) 63(* are defined by datatypes with simple evaluation semantics. *) 64(*---------------------------------------------------------------------------*) 65 66val _ = 67 Hol_datatype 68 `nexp = Var of string 69 | Arr of string => nexp 70 | Const of int 71 | Plus of nexp => nexp 72 | Sub of nexp => nexp 73 | Times of nexp => nexp 74 | Div of nexp => nexp 75 | Min of nexp => nexp`; 76 77val _ = acl2encodeLib.initialise_type ``:nexp``; 78 79val _ = 80 Hol_datatype 81 `bexp = Equal of nexp => nexp 82 | Less of nexp => nexp 83 | LessEq of nexp => nexp 84 | Greater of nexp => nexp 85 | GreaterEq of nexp => nexp 86 | And of bexp => bexp 87 | Or of bexp => bexp 88 | Not of bexp`; 89 90val _ = acl2encodeLib.initialise_type ``:bexp``; 91 92val _ = 93 Hol_datatype 94 `aexp = ArrConst of (num |-> int) (* array constant *) 95 | ArrVar of string (* array variable *) 96 | ArrUpdate of aexp => nexp => nexp`; (* array update *) 97 98val _ = acl2encodeLib.initialise_type ``:aexp``; 99 100val neval_def = 101 Define 102 `(neval (Var v) s = ScalarOf(s ' v)) /\ 103 (neval (Arr a e) s = (ArrayOf(s ' a) ' (Num(neval e s)))) /\ 104 (neval (Const c) s = c) /\ 105 (neval (Plus e1 e2) s = integer$int_add (neval e1 s) (neval e2 s)) /\ 106 (neval (Sub e1 e2) s = integer$int_sub (neval e1 s) (neval e2 s)) /\ 107 (neval (Times e1 e2) s = integer$int_mul (neval e1 s) (neval e2 s)) /\ 108 (neval (Div e1 e2) s = integer$int_quot (neval e1 s) (neval e2 s)) /\ 109 (neval (Min e1 e2) s = integer$int_min (neval e1 s) (neval e2 s))`; 110 111(*****************************************************************************) 112(* neval is not a complete function. It cannot complete if any variable in *) 113(* the expression is not in the environment. Therefore, we must define an *) 114(* auxilliary function to determine when a call to neval is safe *) 115(* *) 116(* Unfortunately, this will rely on neval to determine array indices. *) 117(* To avoid a mutually recurse translation we define 'safe_neval' that acts *) 118(* as 'neval' but returns 0 where 'neval' would stop evaluating. *) 119(*****************************************************************************) 120 121val safe_neval_def = 122 Define 123 `(safe_neval (Var v) s = if v IN FDOM s /\ isScalar (s ' v) then ScalarOf(s ' v) else 0i) /\ 124 (safe_neval (Arr a e) s = if a IN FDOM s /\ isArray (s ' a) /\ integer$int_le 0i (safe_neval e s) /\ Num (safe_neval e s) IN FDOM (ArrayOf (s ' a)) then (ArrayOf(s ' a) ' (Num(safe_neval e s))) else 0i) /\ 125 (safe_neval (Const c) s = c) /\ 126 (safe_neval (Plus e1 e2) s = integer$int_add (safe_neval e1 s) (safe_neval e2 s)) /\ 127 (safe_neval (Sub e1 e2) s = integer$int_sub (safe_neval e1 s) (safe_neval e2 s)) /\ 128 (safe_neval (Times e1 e2) s = integer$int_mul (safe_neval e1 s) (safe_neval e2 s)) /\ 129 (safe_neval (Div e1 e2) s = if safe_neval e2 s = 0i then 0i else integer$int_quot (safe_neval e1 s) (safe_neval e2 s)) /\ 130 (safe_neval (Min e1 e2) s = integer$int_min (safe_neval e1 s) (safe_neval e2 s))`; 131 132(*****************************************************************************) 133(* We can then use this to define nevaluates as follows: *) 134(*****************************************************************************) 135 136val nevaluates_def = 137 Define `(nevaluates (Var v) s = v IN FDOM s /\ isScalar (s ' v)) /\ 138 (nevaluates (Arr a e) s = a IN FDOM s /\ isArray (s ' a) /\ integer$int_le 0i (safe_neval e s) /\ nevaluates e s /\ Num (safe_neval e s) IN FDOM (ArrayOf (s ' a))) /\ 139 (nevaluates (Const c) s = T) /\ 140 (nevaluates (Plus e1 e2) s = nevaluates e1 s /\ nevaluates e2 s) /\ 141 (nevaluates (Sub e1 e2) s = nevaluates e1 s /\ nevaluates e2 s) /\ 142 (nevaluates (Times e1 e2) s = nevaluates e1 s /\ nevaluates e2 s) /\ 143 (nevaluates (Div e1 e2) s = ~(safe_neval e2 s = 0i) /\ nevaluates e1 s /\ nevaluates e2 s) /\ 144 (nevaluates (Min e1 e2) s = nevaluates e1 s /\ nevaluates e2 s)`; 145 146(*****************************************************************************) 147(* ...and prove that this implies we are correct. *) 148(*****************************************************************************) 149 150val neval_safe_theorem1 = store_thm("neval_safe_theorem1", 151 ``!e s. nevaluates e s ==> (safe_neval e s = neval e s)``, 152 Induct THEN RW_TAC std_ss [nevaluates_def, safe_neval_def, neval_def]); 153 154(*****************************************************************************) 155(* We now begin by translating safe_neval. *) 156(*****************************************************************************) 157 158val ONE_ONE_str = prove(``ONE_ONE str``, RW_TAC std_ss [ONE_ONE_THM]); 159val ONE_ONE_nat = prove(``ONE_ONE nat``, RW_TAC std_ss [ONE_ONE_THM, sexpTheory.nat_def, translateTheory.INT_CONG, integerTheory.INT_INJ]); 160 161val _ = acl2encodeLib.translate_conditional_function [(``safe_neval``,"acl2safe_neval")] [ONE_ONE_str, ONE_ONE_nat] safe_neval_def; 162 163val _ = acl2encodeLib.translate_conditional_function [(``nevaluates``,"acl2nevaluates")] [ONE_ONE_str, ONE_ONE_nat] nevaluates_def; 164 165(*****************************************************************************) 166(* beval just needs to have neval to be replaced. *) 167(*****************************************************************************) 168 169val beval_def = 170 Define 171 `(beval (Equal e1 e2) s = (neval e1 s = neval e2 s)) /\ 172 (beval (Less e1 e2) s = integer$int_lt (neval e1 s) (neval e2 s)) /\ 173 (beval (LessEq e1 e2) s = integer$int_le (neval e1 s) (neval e2 s)) /\ 174 (beval (Greater e1 e2) s = integer$int_gt (neval e1 s) (neval e2 s)) /\ 175 (beval (GreaterEq e1 e2) s = integer$int_ge (neval e1 s) (neval e2 s)) /\ 176 (beval (And b1 b2) s = (beval b1 s /\ beval b2 s)) /\ 177 (beval (Or b1 b2) s = (beval b1 s \/ beval b2 s)) /\ 178 (beval (Not e) s = ~(beval e s))`; 179 180val safe_beval_def = 181 Define 182 `(safe_beval (Equal e1 e2) s = (safe_neval e1 s = safe_neval e2 s)) /\ 183 (safe_beval (Less e1 e2) s = integer$int_lt (safe_neval e1 s) (safe_neval e2 s)) /\ 184 (safe_beval (LessEq e1 e2) s = integer$int_le (safe_neval e1 s) (safe_neval e2 s)) /\ 185 (safe_beval (Greater e1 e2) s = integer$int_gt (safe_neval e1 s) (safe_neval e2 s)) /\ 186 (safe_beval (GreaterEq e1 e2) s = integer$int_ge (safe_neval e1 s) (safe_neval e2 s)) /\ 187 (safe_beval (And b1 b2) s = (safe_beval b1 s /\ safe_beval b2 s)) /\ 188 (safe_beval (Or b1 b2) s = (safe_beval b1 s \/ safe_beval b2 s)) /\ 189 (safe_beval (Not e) s = ~(safe_beval e s))`; 190 191val bevaluates_def = 192 Define 193 `(bevaluates (Equal e1 e2) s = nevaluates e1 s /\ nevaluates e2 s) /\ 194 (bevaluates (Less e1 e2) s = nevaluates e1 s /\ nevaluates e2 s) /\ 195 (bevaluates (LessEq e1 e2) s = nevaluates e1 s /\ nevaluates e2 s) /\ 196 (bevaluates (Greater e1 e2) s = nevaluates e1 s /\ nevaluates e2 s) /\ 197 (bevaluates (GreaterEq e1 e2) s = nevaluates e1 s /\ nevaluates e2 s) /\ 198 (bevaluates (And b1 b2) s = bevaluates b1 s /\ bevaluates b2 s) /\ 199 (bevaluates (Or b1 b2) s = bevaluates b1 s /\ bevaluates b2 s) /\ 200 (bevaluates (Not e) s = bevaluates e s)`; 201 202val beval_safe_theorem1 = store_thm("beval_safe_theorem1", 203 ``!e s. bevaluates e s ==> (safe_beval e s = beval e s)``, 204 Induct THEN RW_TAC std_ss [bevaluates_def, safe_beval_def, beval_def, neval_safe_theorem1]); 205 206val ONE_ONE_str = prove(``ONE_ONE str``, RW_TAC std_ss [ONE_ONE_THM]); 207val ONE_ONE_nat = prove(``ONE_ONE nat``, RW_TAC std_ss [ONE_ONE_THM, sexpTheory.nat_def, translateTheory.INT_CONG, integerTheory.INT_INJ]); 208 209val _ = acl2encodeLib.translate_conditional_function [(``safe_beval``,"acl2safe_beval")] [ONE_ONE_str, ONE_ONE_nat] safe_beval_def; 210 211val _ = acl2encodeLib.translate_conditional_function [(``bevaluates``,"acl2bevaluates")] [ONE_ONE_str, ONE_ONE_nat] bevaluates_def; 212 213 214(*****************************************************************************) 215(* aeval requires v IN FDOM s. *) 216(*****************************************************************************) 217 218val aeval_def = 219 Define 220 `(aeval (ArrConst f) s = f) /\ 221 (aeval (ArrVar v) s = ArrayOf(s ' v)) /\ 222 (aeval (ArrUpdate a e1 e2) s = aeval a s |+ (Num(neval e1 s), neval e2 s))`; 223 224(*****************************************************************************) 225(* aevaluates defines when aeval will complete *) 226(*****************************************************************************) 227 228val aevaluates_def = 229 Define 230 `(aevaluates (ArrConst f) s = T) /\ 231 (aevaluates (ArrVar v) s = v IN FDOM s) /\ 232 (aevaluates (ArrUpdate a e1 e2) s = aevaluates a s /\ nevaluates e1 s /\ integer$int_le 0i (safe_neval e1 s) /\ nevaluates e2 s)`; 233 234(*****************************************************************************) 235(* safe_aeval always completes. *) 236(*****************************************************************************) 237 238val safe_aeval_def = 239 Define 240 `(safe_aeval (ArrConst f) s = f) /\ 241 (safe_aeval (ArrVar v) s = if v IN FDOM s then ArrayOf(s ' v) else FEMPTY) /\ 242 (safe_aeval (ArrUpdate a e1 e2) s = if integer$int_le 0i (safe_neval e1 s) then safe_aeval a s |+ (Num(safe_neval e1 s), safe_neval e2 s) else safe_aeval a s)`; 243 244(*****************************************************************************) 245(* Proves that aeval is correct. *) 246(*****************************************************************************) 247 248val aeval_safe_theorem1 = store_thm("aeval_safe_theorem1", 249 ``!e s. aevaluates e s ==> (safe_aeval e s = aeval e s)``, 250 Induct THEN RW_TAC std_ss [aevaluates_def, safe_aeval_def, aeval_def, neval_safe_theorem1]); 251 252(*****************************************************************************) 253(* We now begin by translating safe_neval. *) 254(*****************************************************************************) 255 256val ONE_ONE_str = prove(``ONE_ONE str``, RW_TAC std_ss [ONE_ONE_THM]); 257val ONE_ONE_nat = prove(``ONE_ONE nat``, RW_TAC std_ss [ONE_ONE_THM, sexpTheory.nat_def, translateTheory.INT_CONG, integerTheory.INT_INJ]); 258 259val _ = acl2encodeLib.translate_conditional_function [(``safe_aeval``,"acl2safe_aeval")] [ONE_ONE_str, ONE_ONE_nat] safe_aeval_def; 260val _ = acl2encodeLib.translate_conditional_function [(``aevaluates``,"acl2aevaluates")] [ONE_ONE_str, ONE_ONE_nat] aevaluates_def; 261 262(*****************************************************************************) 263(* naeval completes. *) 264(*****************************************************************************) 265 266val naeval_def = 267 Define 268 `(naeval (INL e) s = Scalar(neval e s)) /\ 269 (naeval (INR a) s = Array(aeval a s))`; 270 271val safe_naeval_def = 272 Define 273 `(safe_naeval (INL e) s = Scalar(safe_neval e s)) /\ 274 (safe_naeval (INR a) s = Array(safe_aeval a s))`; 275 276val naevaluates_def = 277 Define 278 `(naevaluates (INL e) s = nevaluates e s) /\ 279 (naevaluates (INR a) s = aevaluates a s)`; 280 281val naeval_safe_theorem1 = store_thm("naeval_safe_theorem1", 282 ``!e s. naevaluates e s ==> (safe_naeval e s = naeval e s)``, 283 Induct THEN RW_TAC std_ss [naevaluates_def, safe_naeval_def, naeval_def, neval_safe_theorem1, aeval_safe_theorem1]); 284 285val _ = acl2encodeLib.translate_simple_function [(``safe_naeval``,"acl2naeval")] safe_naeval_def; 286 287(*****************************************************************************) 288(* Translations of other definitions... *) 289(*****************************************************************************) 290 291val Update_def = 292 Define 293 `Update v e s = s |+ (v, naeval e s)`; 294 295val safe_Update_def = 296 Define 297 `safe_Update v e s = s |+ (v, safe_naeval e s)`; 298 299val Updates_def = 300 Define 301 `Updates v e s = naevaluates e s`; 302 303val Updates_safe_theorem1 = store_thm("Updates_safe_theorem1", 304 ``Updates v e s ==> (safe_Update v e s = Update v e s)``, 305 RW_TAC std_ss [Updates_def, safe_Update_def, Update_def, naeval_safe_theorem1]); 306 307val _ = acl2encodeLib.translate_conditional_function [(``safe_Update``,"acl2Update")] [ONE_ONE_str, ONE_ONE_nat] safe_Update_def; 308 309val UpdateCases = 310 store_thm 311 ("UpdateCases", 312 ``(Update v (INL e) s = s |+ (v, Scalar(neval e s))) /\ 313 (Update v (INR a) s = s |+ (v, Array(aeval a s)))``, 314 RW_TAC std_ss [Update_def,naeval_def]); 315 316(* Convert a value or array to a constant expression *) 317val Exp_def = 318 Define 319 `(Exp(Scalar n) = INL(Const n)) /\ 320 (Exp(Array f) = INR(ArrConst f))`; 321 322val Update_Exp = 323 store_thm 324 ("Update_Exp", 325 ``!v val s. Update v (Exp val) s = s |+ (v, val)``, 326 Cases_on `val` 327 THEN RW_TAC std_ss [UpdateCases,Exp_def,aeval_def,neval_def]); 328 329val _ = acl2encodeLib.initialise_type ``:'a + 'b``; 330 331val _ = acl2encodeLib.translate_conditional_function [(``Exp``,"acl2Exp")] [ONE_ONE_str, ONE_ONE_nat] Exp_def; 332 333(*****************************************************************************) 334(* sfun isn't going to work as we can't encode values of continuous *) 335(* functions. *) 336(*****************************************************************************) 337 338val _ = 339 Hol_datatype 340 `program = 341 Skip (* null command *) 342 | GenAssign of string => (nexp + aexp) (* variable assignment *) 343 | Dispose of string (* deallocate variable *) 344 | Seq of program => program (* sequencing *) 345 | Cond of bexp => program => program (* conditional *) 346 | AnWhile of bexp => nexp => program (* Annotated while loop *) 347 | Local of string => program`; (* local variable block *) 348 349val While_def = Define `While a c = AnWhile a ARB c`; 350 351val _ = acl2encodeLib.initialise_type ``:program``; 352 353(* Simple variable assignment *) 354val Assign_def = 355 Define 356 `Assign v e = GenAssign v (INL e)`; 357 358val _ = acl2encodeLib.translate_conditional_function 359 [(``Assign``,"acl2Assign")] [ONE_ONE_str, ONE_ONE_nat] Assign_def; 360 361(* Array assignment *) 362val ArrayAssign_def = 363 Define 364 `ArrayAssign v e1 e2 = GenAssign v (INR(ArrUpdate (ArrVar v) e1 e2))`; 365 366val _ = acl2encodeLib.translate_conditional_function 367 [(``ArrayAssign``, "acl2ArrayAssign")] [ONE_ONE_str, ONE_ONE_nat] ArrayAssign_def; 368 369(*****************************************************************************) 370(* There is no way we can translate the 'Unannotated' functions as ARB *) 371(* cannot equal any encoding. *) 372(*****************************************************************************) 373 374(* Multiple local variables *) 375val Locals_def = 376 Define 377 `(Locals [] c = c) /\ 378 (Locals (v::vl) c = Local v (Locals vl c))`; 379 380val _ = acl2encodeLib.translate_conditional_function 381 [(``Locals``, "acl2Locals")] [ONE_ONE_str, ONE_ONE_nat] Locals_def; 382 383 384 385val _ = overload_on ("V", ``Var``); 386val _ = overload_on ("C", ``Const``); 387 388val _ = overload_on ("+", ``Plus``); 389val _ = overload_on ("-", ``Sub``); 390val _ = overload_on ("*", ``Times``); 391val _ = overload_on ("/", ``Div``); 392 393val _ = overload_on ("=", ``Equal``); 394val _ = overload_on ("<", ``Less``); 395val _ = overload_on ("<=", ``LessEq``); 396val _ = overload_on (">", ``Greater``); 397val _ = overload_on (">=", ``GreaterEq``); 398 399val _ = overload_on ("~", ``Not``); 400val _ = overload_on ("/\\", ``And``); 401val _ = overload_on ("\\/", ``Or``); 402 403val _ = overload_on ("COND", ``Cond:bexp->program->program->program``); 404 405val _ = overload_on ("::=", ``Assign``); 406val _ = set_fixity "::=" (Infixr 280); 407 408val _ = overload_on (";;", ``Seq``); 409val _ = set_fixity ";;" (Infixr 180); 410 411(*---------------------------------------------------------------------------*) 412(* Big-step operational semantics specified by an inductive relation. *) 413(* *) 414(* EVAL : program -> state -> state -> bool *) 415(* *) 416(* is defined inductively such that *) 417(* *) 418(* EVAL c s1 s2 *) 419(* *) 420(* holds exactly when executing the command c in the initial state s1 *) 421(* terminates in the final state s2. The evaluation relation is defined *) 422(* inductively by the set of rules shown below. *) 423(*---------------------------------------------------------------------------*) 424 425val (rules,induction,ecases) = 426 Hol_reln 427 `(!s. EVAL Skip s s) 428 /\ (!s v e. EVAL (GenAssign v e) s (Update v e s)) 429 /\ (!s v. EVAL (Dispose v) s (s \\ v)) 430 /\ (!c1 c2 s1 s2 s3. EVAL c1 s1 s2 /\ EVAL c2 s2 s3 431 ==> EVAL (Seq c1 c2) s1 s3) 432 /\ (!c1 c2 s1 s2 b. EVAL c1 s1 s2 /\ beval b s1 433 ==> EVAL (Cond b c1 c2) s1 s2) 434 /\ (!c1 c2 s1 s2 b. EVAL c2 s1 s2 /\ ~beval b s1 435 ==> EVAL (Cond b c1 c2) s1 s2) 436 /\ (!c s b n. ~beval b s 437 ==> EVAL (AnWhile b n c) s s) 438 /\ (!c s1 s2 s3 b n. 439 EVAL c s1 s2 /\ EVAL (AnWhile b n c) s2 s3 /\ beval b s1 440 ==> EVAL (AnWhile b n c) s1 s3) 441 /\ (!c s1 s2 v. 442 EVAL c s1 s2 443 ==> EVAL (Local v c) s1 (if v IN FDOM s1 444 then s2|+(v, (s1 ' v)) 445 else s2 \\ v))`; 446 447 448 449 450val rulel = CONJUNCTS rules; 451 452(* --------------------------------------------------------------------- *) 453(* Stronger form of rule induction. *) 454(* --------------------------------------------------------------------- *) 455 456val sinduction = derive_strong_induction(rules,induction); 457 458(* =====================================================================*) 459(* Derivation of backwards case analysis theorems for each rule. *) 460(* *) 461(* These theorems are consequences of the general case analysis theorem *) 462(* proved above. They are used to justify formal reasoning in which the*) 463(* rules are driven 'backwards', inferring premisses from conclusions. *) 464(* =====================================================================*) 465 466val SKIP_THM = store_thm 467("SKIP_THM", 468 ``!s1 s2. EVAL Skip s1 s2 = (s1 = s2)``, 469 RW_TAC std_ss [EQ_IMP_THM,Once ecases] THEN METIS_TAC rulel); 470 471val SKIP = store_thm 472("SKIP", 473 ``!s. EVAL Skip s s``, 474 METIS_TAC rulel); 475 476val GEN_ASSIGN_THM = store_thm 477("GEN_ASSIGN_THM", 478 ``!s1 s2 v e. EVAL (GenAssign v e) s1 s2 = (s2 = Update v e s1)``, 479 RW_TAC std_ss [EQ_IMP_THM,Once ecases] THEN METIS_TAC rulel); 480 481val GEN_ASSIGN = store_thm 482("GEN_ASSIGN", 483 ``!s v e. EVAL (GenAssign v e) s (Update v e s)``, 484 METIS_TAC rulel); 485 486val ASSIGN = store_thm 487("ASSIGN", 488 ``!s v e. EVAL (Assign v e) s (Update v (INL e) s)``, 489 RW_TAC std_ss [Assign_def] THEN METIS_TAC rulel); 490 491val ARRAY_ASSIGN = store_thm 492("ARRAY_ASSIGN", 493 ``!s v e1 e2. 494 EVAL (ArrayAssign v e1 e2) s (Update v (INR(ArrUpdate (ArrVar v) e1 e2)) s)``, 495 RW_TAC std_ss [ArrayAssign_def] THEN METIS_TAC rulel); 496 497val DISPOSE_THM = store_thm 498("DISPOSE_THM", 499 ``!s1 s2 v. EVAL (Dispose v) s1 s2 = (s2 = s1 \\ v)``, 500 RW_TAC std_ss [EQ_IMP_THM,Once ecases] THEN METIS_TAC rulel); 501 502val DISPOSE = store_thm 503("DISPOSE", 504 ``!s v. EVAL (Dispose v) s (s \\ v)``, 505 METIS_TAC rulel); 506 507val SEQ_THM = store_thm 508("SEQ_THM", 509 ``!s1 s3 c1 c2. EVAL (Seq c1 c2) s1 s3 = ?s2. EVAL c1 s1 s2 /\ EVAL c2 s2 s3``, 510 RW_TAC std_ss [EQ_IMP_THM,Once ecases] THEN METIS_TAC rulel); 511 512val IF_T_THM = store_thm 513("IF_T_THM", 514 ``!s1 s2 b c1 c2. 515 beval b s1 ==> (EVAL (Cond b c1 c2) s1 s2 = EVAL c1 s1 s2)``, 516 RW_TAC std_ss [EQ_IMP_THM,Once ecases] THEN METIS_TAC rulel); 517 518val IF_F_THM = store_thm 519("IF_F_THM", 520 ``!s1 s2 b c1 c2. 521 ~beval b s1 ==> (EVAL (Cond b c1 c2) s1 s2 = EVAL c2 s1 s2)``, 522 RW_TAC std_ss [EQ_IMP_THM,Once ecases] THEN METIS_TAC rulel); 523 524val IF_THM = 525 store_thm 526 ("IF_THM", 527 ``!s1 s2 b s1 s2. 528 EVAL (Cond b c1 c2) s1 s2 = 529 if beval b s1 then EVAL c1 s1 s2 else EVAL c2 s1 s2``, 530 METIS_TAC[IF_T_THM,IF_F_THM]); 531 532val ANWHILE_T_THM = store_thm 533("ANWHILE_T_THM", 534 ``!s1 s3 b n c. 535 beval b s1 ==> 536 (EVAL (AnWhile b n c) s1 s3 = 537 ?s2. EVAL c s1 s2 /\ EVAL (AnWhile b n c) s2 s3)``, 538 RW_TAC std_ss [EQ_IMP_THM,Once ecases] 539 THEN METIS_TAC rulel); 540 541val WHILE_T_THM = 542 store_thm 543 ("WHILE_T_THM", 544 ``!s1 s3 b c. 545 beval b s1 ==> 546 (EVAL (While b c) s1 s3 = 547 ?s2. EVAL c s1 s2 /\ EVAL (While b c) s2 s3)``, 548 METIS_TAC[ANWHILE_T_THM,While_def]); 549 550val ANWHILE_F_THM = store_thm 551("ANWHILE_F_THM", 552 ``!s1 s2 b n c. ~beval b s1 ==> (EVAL (AnWhile b n c) s1 s2 = (s1 = s2))``, 553 RW_TAC std_ss [EQ_IMP_THM,Once ecases] 554 THEN METIS_TAC rulel); 555 556val WHILE_F_THM = 557 store_thm 558 ("WHILE_F_THM", 559 ``!s1 s2 b c. ~beval b s1 ==> (EVAL (While b c) s1 s2 = (s1 = s2))``, 560 METIS_TAC[ANWHILE_F_THM,While_def]); 561 562val ANWHILE_THM = store_thm 563("ANWHILE_THM", 564 ``!s1 s3 b n c. 565 EVAL (AnWhile b n c) s1 s3 = 566 if beval b s1 567 then ?s2. EVAL c s1 s2 /\ EVAL (AnWhile b n c) s2 s3 568 else (s1 = s3)``, 569 METIS_TAC[ANWHILE_T_THM,ANWHILE_F_THM]); 570 571val WHILE_THM = store_thm 572("WHILE_THM", 573 ``!s1 s3 b c. 574 EVAL (While b c) s1 s3 = 575 if beval b s1 576 then ?s2. EVAL c s1 s2 /\ EVAL (While b c) s2 s3 577 else (s1 = s3)``, 578 METIS_TAC[ANWHILE_THM,While_def]); 579 580val LOCAL_THM = store_thm 581 ("LOCAL_THM", 582 ``!s1 s2 v c. 583 EVAL (Local v c) s1 s2 = 584 ?s3. EVAL c s1 s3 585 /\ 586 (s2 = if v IN FDOM s1 then s3 |+ (v, (s1 ' v)) else s3 \\ v)``, 587 RW_TAC std_ss [EQ_IMP_THM,Once ecases,While_def] THEN METIS_TAC(FUPDATE_EQ:: rulel)); 588 589(* Semantic associativity of sequencing *) 590val SEQ_ASSOC = 591 store_thm 592 ("SEQ_ASSOC", 593 ``!c1 c2 c3 s1 s2. 594 EVAL (Seq (Seq c1 c2) c3) s1 s2 = EVAL (Seq c1 (Seq c2 c3)) s1 s2``, 595 RW_TAC std_ss [SEQ_THM] 596 THEN METIS_TAC[]); (* METIS does the whole proof, but is slower *) 597 598 599 600val EVAL_DETERMINISTIC = store_thm 601("EVAL_DETERMINISTIC", 602 ``!c st1 st2. EVAL c st1 st2 ==> !st3. EVAL c st1 st3 ==> (st2 = st3)``, 603 HO_MATCH_MP_TAC induction THEN 604 RW_TAC std_ss [SKIP_THM,GEN_ASSIGN_THM,DISPOSE_THM,SEQ_THM, 605 IF_T_THM,IF_F_THM,ANWHILE_T_THM, 606 ANWHILE_F_THM,LOCAL_THM] THEN 607 METIS_TAC[]); 608 609(* Corollary used later *) 610val IMP_EVAL_DETERMINISTIC = 611 store_thm 612 ("IMP_EVAL_DETERMINISTIC", 613 ``!c st1 st2 p. 614 (p st1 ==> EVAL c st1 st2) ==> !st3. EVAL c st1 st3 ==> p st1 ==> (st2 = st3)``, 615 METIS_TAC[EVAL_DETERMINISTIC]); 616(*---------------------------------------------------------------------------*) 617(* Definition of Floyd-Hoare logic judgements for partial correctness and *) 618(* derivation of proof rules. *) 619(*---------------------------------------------------------------------------*) 620 621val SPEC_def = 622 Define 623 `SPEC P c Q = !s1 s2. P s1 /\ EVAL c s1 s2 ==> Q s2`; 624 625(*---------------------------------------------------------------------------*) 626(* Definition of VDM-like Floyd-Hoare logic judgements for partial *) 627(* where the postcondition is a relation between initial and final starts *) 628(*---------------------------------------------------------------------------*) 629 630val RSPEC_def = 631 Define 632 `RSPEC P c R = !s1 s2. P s1 /\ EVAL c s1 s2 ==> R s1 s2`; 633 634(* Corollary used later *) 635val EVAL_RSPEC = 636 store_thm 637 ("EVAL_RSPEC", 638 ``!A c f. 639 (!s. A s ==> EVAL c s (f s)) 640 ==> 641 !P R. 642 (!s. (P s ==> A s) /\ (A s ==> R s (f s))) ==> RSPEC P c R``, 643 METIS_TAC[EVAL_DETERMINISTIC,RSPEC_def]); 644 645(*---------------------------------------------------------------------------*) 646(* Auxiliary definitions for composing correctness judgements *) 647(*---------------------------------------------------------------------------*) 648 649val IMP_def = 650 Define 651 `IMP pre post = \prog. RSPEC pre prog post`; 652 653val AND_def = 654 Define 655 `AND spec1 spec2 = \prog. spec1 prog /\ spec2 prog`; 656 657(*---------------------------------------------------------------------------*) 658(* Skip rule *) 659(*---------------------------------------------------------------------------*) 660 661val SKIP_RULE = store_thm 662("SKIP_RULE", 663 ``!P. SPEC P Skip P``, 664 RW_TAC std_ss [SPEC_def,SKIP_THM]); 665 666(*---------------------------------------------------------------------------*) 667(* Dispose rule *) 668(*---------------------------------------------------------------------------*) 669 670val DISPOSE_RULE = store_thm 671("DISPOSE_RULE", 672 ``!P v e. 673 SPEC (\s. P (s \\ v)) (Dispose v) P``, 674 RW_TAC std_ss [SPEC_def] THEN METIS_TAC [DISPOSE_THM]); 675 676(*---------------------------------------------------------------------------*) 677(* Assignment rule *) 678(*---------------------------------------------------------------------------*) 679 680val GEN_ASSIGN_RULE = store_thm 681("GEN_ASSIGN_RULE", 682 ``!P v e. 683 SPEC (P o Update v e) (GenAssign v e) P``, 684 RW_TAC std_ss [SPEC_def] THEN METIS_TAC [GEN_ASSIGN_THM]); 685 686(*---------------------------------------------------------------------------*) 687(* Dispose rule *) 688(*---------------------------------------------------------------------------*) 689 690val DISPOSE_RULE = store_thm 691("DISPOSE_RULE", 692 ``!P v. 693 SPEC (\s. P (s \\ v)) (Dispose v) P``, 694 RW_TAC std_ss [SPEC_def] THEN METIS_TAC [DISPOSE_THM]); 695 696(*---------------------------------------------------------------------------*) 697(* Sequencing rule *) 698(*---------------------------------------------------------------------------*) 699 700val SEQ_RULE = store_thm 701("SEQ_RULE", 702 ``!P c1 c2 Q R. 703 SPEC P c1 Q /\ SPEC Q c2 R ==> SPEC P (Seq c1 c2) R``, 704 RW_TAC std_ss [SPEC_def] THEN METIS_TAC [SEQ_THM]); 705 706(*---------------------------------------------------------------------------*) 707(* Conditional rule *) 708(*---------------------------------------------------------------------------*) 709 710val COND_RULE = store_thm 711("COND_RULE", 712 ``!P b c1 c2 Q. 713 SPEC (\s. P(s) /\ beval b s) c1 Q /\ 714 SPEC (\s. P(s) /\ ~beval b s) c2 Q ==> SPEC P (Cond b c1 c2) Q``, 715 RW_TAC std_ss [SPEC_def] THEN METIS_TAC [IF_T_THM, IF_F_THM]); 716 717(*---------------------------------------------------------------------------*) 718(* While rule *) 719(*---------------------------------------------------------------------------*) 720 721local 722 723val lemma1 = Q.prove 724(`!c s1 s2. EVAL c s1 s2 ==> !b' n' c'. (c = AnWhile b' n' c') ==> ~beval b' s2`, 725 HO_MATCH_MP_TAC induction THEN RW_TAC std_ss []); 726 727val lemma2 = Q.prove 728(`!c s1 s2. 729 EVAL c s1 s2 ==> 730 !b' n' c'. 731 (c = AnWhile b' n' c') ==> 732 (!s1 s2. P s1 /\ beval b' s1 /\ EVAL c' s1 s2 ==> P s2) 733 ==> (P s1 ==> P s2)`, 734 HO_MATCH_MP_TAC sinduction THEN RW_TAC std_ss [] THEN METIS_TAC[]); 735 736in 737 738val ANWHILE_RULE = store_thm 739("ANWHILE_RULE", 740 ``!P b n c. SPEC (\s. P(s) /\ beval b s) c P ==> 741 SPEC P (AnWhile b n c) (\s. P s /\ ~beval b s)``, 742 RW_TAC std_ss [SPEC_def] THENL [METIS_TAC[lemma2],METIS_TAC[lemma1]]) 743 744end; 745 746val WHILE_RULE = 747 store_thm 748 ("WHILE_RULE", 749 ``!P b c. SPEC (\s. P(s) /\ beval b s) c P ==> 750 SPEC P (While b c) (\s. P s /\ ~beval b s)``, 751 METIS_TAC[ANWHILE_RULE,While_def]); 752 753 754(*---------------------------------------------------------------------------*) 755(* Local rule *) 756(*---------------------------------------------------------------------------*) 757 758val INDEPENDENT_def = 759 Define 760 `INDEPENDENT P v = !s. P(s \\ v) = P s`; 761 762val LOCAL_RULE = store_thm 763("LOCAL_RULE", 764 ``!P Q c v. 765 SPEC P c Q /\ INDEPENDENT Q v 766 ==> 767 SPEC P (Local v c) Q``, 768 RW_TAC std_ss [SPEC_def] 769 THEN FULL_SIMP_TAC std_ss [LOCAL_THM] 770 THEN RW_TAC std_ss [FUPDATE_EQ] 771 THEN METIS_TAC[DOMSUB_FUPDATE,INDEPENDENT_def]); 772 773(* 774val DEPENDS_ON_def = 775 Define 776 `DEPENDS_ON P v = ?s1 s2. ~(s1 ' v = s2 ' v) /\ ~(P s1 = P s2)`; 777 778 `DEPENDS_ON P vs = !s. P(DRESTRICT s vs) = P s) 779 780val DEPENDS_ON_NOT_INDEPENDENT = 781 store_thm 782 ("DEPENDS_ON_NOT_INDEPENDENT", 783 ``!P. DEPENDS_ON P v = ~(INDEPENDENT P v)``, 784 RW_TAC std_ss [DEPENDS_ON_def,INDEPENDENT_def] 785 THEN EQ_TAC 786 THEN RW_TAC std_ss [] 787*) 788 789(*---------------------------------------------------------------------------*) 790(* Precondition strengthening *) 791(*---------------------------------------------------------------------------*) 792 793val PRE_STRENGTHEN = store_thm 794("PRE_STRENGTHEN", 795 ``!P c Q P'. (!s. P' s ==> P s) /\ SPEC P c Q ==> SPEC P' c Q``, 796 RW_TAC std_ss [SPEC_def] THEN METIS_TAC[]); 797 798(*---------------------------------------------------------------------------*) 799(* postcondition weakening *) 800(*---------------------------------------------------------------------------*) 801 802val POST_WEAKEN = store_thm 803("POST_WEAKEN", 804 ``!P c Q Q'. (!s. Q s ==> Q' s) /\ SPEC P c Q ==> SPEC P c Q'``, 805 RW_TAC std_ss [SPEC_def] THEN METIS_TAC[]); 806 807(*---------------------------------------------------------------------------*) 808(* Boolean combinations of pre-and-post-conditions. *) 809(*---------------------------------------------------------------------------*) 810 811val CONJ_TRIPLE = store_thm 812("CONJ_TRIPLE", 813 ``!P1 P2 c Q1 Q2. SPEC P1 c Q1 /\ SPEC P2 c Q2 814 ==> SPEC (\s. P1 s /\ P2 s) c (\s. Q1 s /\ Q2 s)``, 815 RW_TAC std_ss [SPEC_def] THEN METIS_TAC[]); 816 817val DISJ_TRIPLE = store_thm 818("DISJ_TRIPLE", 819 ``!P1 P2 c Q1 Q2. SPEC P1 c Q1 /\ SPEC P2 c Q2 820 ==> SPEC (\s. P1 s \/ P2 s) c (\s. Q1 s \/ Q2 s)``, 821 RW_TAC std_ss [SPEC_def] THEN METIS_TAC[]); 822 823(*===========================================================================*) 824(* End of HOL/examples/ind_def/opsemScript.sml *) 825(*===========================================================================*) 826 827(* ========================================================================= *) 828(* TOTAL-CORRECTNESS HOARE TRIPLES *) 829(* ========================================================================= *) 830 831val TOTAL_SPEC_def = Define ` 832 TOTAL_SPEC p c q = SPEC p c q /\ !s1. p s1 ==> ?s2. EVAL c s1 s2`; 833 834val TOTAL_SKIP_RULE = store_thm("TOTAL_SKIP_RULE", 835 ``!P. TOTAL_SPEC P Skip P``, 836 SIMP_TAC std_ss [TOTAL_SPEC_def,SKIP_RULE] THEN REPEAT STRIP_TAC 837 THEN Q.EXISTS_TAC `s1` THEN REWRITE_TAC [rules]); 838 839val TOTAL_GEN_ASSIGN_RULE = store_thm("TOTAL_GEN_ASSIGN_RULE", 840 ``!P v e. TOTAL_SPEC (P o Update v e) (GenAssign v e) P``, 841 SIMP_TAC std_ss [TOTAL_SPEC_def,GEN_ASSIGN_RULE] THEN REPEAT STRIP_TAC 842 THEN Q.EXISTS_TAC `Update v e s1` THEN REWRITE_TAC [rules]); 843 844val TOTAL_SEQ_RULE = store_thm("TOTAL_SEQ_RULE", 845 ``!P c1 c2 Q R. TOTAL_SPEC P c1 Q /\ TOTAL_SPEC Q c2 R ==> 846 TOTAL_SPEC P (Seq c1 c2) R``, 847 REWRITE_TAC [TOTAL_SPEC_def] THEN REPEAT STRIP_TAC 848 THEN1 (MATCH_MP_TAC SEQ_RULE THEN Q.EXISTS_TAC `Q` THEN ASM_REWRITE_TAC []) 849 THEN FULL_SIMP_TAC bool_ss [SEQ_THM,SPEC_def] 850 THEN RES_TAC THEN RES_TAC THEN METIS_TAC []); 851 852val TOTAL_COND_RULE = store_thm("TOTAL_COND_RULE", 853 ``!P b c1 c2 Q. 854 TOTAL_SPEC (\s. P s /\ beval b s) c1 Q /\ 855 TOTAL_SPEC (\s. P s /\ ~beval b s) c2 Q ==> 856 TOTAL_SPEC P (Cond b c1 c2) Q``, 857 REWRITE_TAC [TOTAL_SPEC_def] THEN REPEAT STRIP_TAC 858 THEN1 (MATCH_MP_TAC COND_RULE THEN ASM_REWRITE_TAC []) 859 THEN FULL_SIMP_TAC std_ss [] 860 THEN Cases_on `beval b s1` THEN RES_TAC 861 THEN IMP_RES_TAC IF_T_THM THEN IMP_RES_TAC IF_F_THM 862 THEN Q.EXISTS_TAC `s2` THEN ASM_REWRITE_TAC []); 863 864val TOTAL_WHILE_F_THM = store_thm("TOTAL_WHILE_F_THM", 865 ``!P b c. TOTAL_SPEC (\s. P s /\ ~beval b s) (While b c) P``, 866 SIMP_TAC std_ss [TOTAL_SPEC_def,SPEC_def,GSYM AND_IMP_INTRO] 867 THEN ONCE_REWRITE_TAC [WHILE_THM] THEN SIMP_TAC std_ss []); 868 869val TOTAL_WHILE_T_THM = store_thm("TOTAL_WHILE_T_THM", 870 ``!P b c M Q. 871 TOTAL_SPEC (\s. P s /\ beval b s) c M /\ TOTAL_SPEC M (While b c) Q ==> 872 TOTAL_SPEC (\s. P s /\ beval b s) (While b c) Q``, 873 SIMP_TAC std_ss [TOTAL_SPEC_def,SPEC_def] THEN REPEAT STRIP_TAC 874 THEN ONCE_REWRITE_TAC [WHILE_THM] THEN ASM_REWRITE_TAC [] 875 THEN RES_TAC THEN RES_TAC THEN METIS_TAC [WHILE_THM]); 876 877val TOTAL_GEN_ASSIGN_THM = store_thm("TOTAL_GEN_ASSIGN_THM", 878 ``!P c v e Q. SPEC P (GenAssign v e) Q = TOTAL_SPEC P (GenAssign v e) Q``, 879 REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC std_ss [TOTAL_SPEC_def] 880 THEN REPEAT STRIP_TAC 881 THEN Q.EXISTS_TAC `Update v e s1` THEN REWRITE_TAC [rules]); 882 883(*===========================================================================*) 884(* Type of outputs of executing programs (e.g. Proc bodies) *) 885(*===========================================================================*) 886 887val _ = 888 Hol_datatype 889 `outcome = RESULT of state | ERROR of state | TIMEOUT of state`; 890 891(* Some automatically proves theorems relating RESULT, TIMEOUT and ERROR *) 892 893val outcome_11 = fetch "-" "outcome_11"; 894val outcome_distinct = fetch "-" "outcome_distinct"; 895val outcome_nchotomy = fetch "-" "outcome_nchotomy"; 896 897(*===========================================================================*) 898(* Small-step semantics based on Collavizza et al. paper *) 899(*===========================================================================*) 900 901val (small_rules,small_induction,small_ecases) = Hol_reln 902 `(!s l. 903 SMALL_EVAL (Skip :: l, s) (l, s)) 904 /\ (!s v e l. 905 SMALL_EVAL (GenAssign v e :: l, s) (l, Update v e s)) 906 /\ (!s v l. 907 SMALL_EVAL (Dispose v :: l, s) (l, s \\ v)) 908 /\ (!s l c1 c2. 909 SMALL_EVAL (Seq c1 c2 :: l, s) (c1 :: c2 :: l, s)) 910 /\ (!s l b c1 c2. 911 beval b s 912 ==> 913 SMALL_EVAL (Cond b c1 c2 :: l, s) (c1 :: l, s)) 914 /\ (!s l b c1 c2. 915 ~(beval b s) 916 ==> 917 SMALL_EVAL (Cond b c1 c2 :: l, s) (c2 :: l, s)) 918 /\ (!s l b R c. 919 beval b s 920 ==> 921 SMALL_EVAL (AnWhile b R c :: l, s) (c :: AnWhile b R c :: l, s)) 922 /\ (!s l b R c. 923 ~(beval b s ) 924 ==> 925 SMALL_EVAL (AnWhile b R c :: l, s) (l, s)) 926 /\ (!s l v c. 927 v IN FDOM s 928 ==> 929 SMALL_EVAL 930 (Local v c :: l, s) 931 (c :: GenAssign v (Exp(s ' v)) :: l, s)) 932 /\ (!s l v c. 933 ~(v IN FDOM s) 934 ==> 935 SMALL_EVAL (Local v c :: l, s) (c :: Dispose v :: l, s))`; 936 937val small_rulel = CONJUNCTS small_rules; 938 939val SMALL_SKIP_THM = store_thm 940("SMALL_SKIP_THM", 941 ``!s1 s2 l1 l2. 942 SMALL_EVAL (Skip :: l1, s1) (l2, s2) = 943 (l2 = l1) /\ (s2 = s1)``, 944 RW_TAC std_ss [EQ_IMP_THM,Once small_ecases,While_def] THEN METIS_TAC small_rulel); 945 946val SMALL_GEN_ASSIGN_THM = store_thm 947("SMALL_GEN_ASSIGN_THM", 948 ``!s1 s2 l1 l2 v e. 949 SMALL_EVAL (GenAssign v e :: l1, s1) (l2, s2) = 950 (l2 = l1) /\ (s2 = Update v e s1)``, 951 RW_TAC std_ss [EQ_IMP_THM,Once small_ecases,While_def] THEN METIS_TAC small_rulel); 952 953val SMALL_DISPOSE_THM = store_thm 954("SMALL_DISPOSE_THM", 955 ``!s1 s2 l1 l2 v. 956 SMALL_EVAL (Dispose v :: l1, s1) (l2, s2) = 957 (l2 = l1) /\ (s2 = s1 \\ v)``, 958 RW_TAC std_ss [EQ_IMP_THM,Once small_ecases,While_def] THEN METIS_TAC small_rulel); 959 960val SMALL_SEQ_THM = store_thm 961("SMALL_SEQ_THM", 962 ``!s1 s3 l1 l3 c1 c2. 963 SMALL_EVAL (Seq c1 c2 :: l1, s1) (l2, s2) = 964 (l2 = c1 :: c2 :: l1) /\ (s2 = s1)``, 965 RW_TAC std_ss [EQ_IMP_THM,Once small_ecases,While_def] THEN METIS_TAC small_rulel); 966 967val SMALL_IF_T_THM = store_thm 968("SMALL_IF_T_THM", 969 ``!s1 s2 l1 l2 b c1 c2. 970 beval b s1 971 ==> 972 (SMALL_EVAL (Cond b c1 c2 :: l1, s1) (l2, s2) = 973 (l2 = c1 :: l1) /\ (s2 = s1))``, 974 RW_TAC std_ss [EQ_IMP_THM,Once small_ecases,While_def] THEN METIS_TAC small_rulel); 975 976val SMALL_IF_F_THM = store_thm 977("SMALL_IF_F_THM", 978 ``!s1 s2 l1 l2 b c1 c2. 979 ~(beval b s1) 980 ==> 981 (SMALL_EVAL (Cond b c1 c2 :: l1, s1) (l2, s2) = 982 (l2 = c2 :: l1) /\ (s2 = s1))``, 983 RW_TAC std_ss [EQ_IMP_THM,Once small_ecases,While_def] THEN METIS_TAC small_rulel); 984 985val SMALL_IF_THM = store_thm 986("SMALL_IF_THM", 987 ``!s1 s2 l1 l2 b c1 c2. 988 SMALL_EVAL (Cond b c1 c2 :: l1, s1) (l2, s2) = 989 (l2 = (if beval b s1 then c1 else c2) :: l1) /\ (s2 = s1)``, 990 METIS_TAC[SMALL_IF_T_THM,SMALL_IF_F_THM]); 991 992val SMALL_ANWHILE_T_THM = store_thm 993("SMALL_ANWHILE_T_THM", 994 ``!s1 s2 l1 l2 b R c. 995 beval b s1 996 ==> 997 (SMALL_EVAL (AnWhile b R c :: l1, s1) (l2, s2) = 998 (l2 = c :: AnWhile b R c :: l1) /\ (s2 = s1))``, 999 RW_TAC std_ss [EQ_IMP_THM,Once small_ecases] 1000 THEN METIS_TAC small_rulel); 1001 1002val SMALL_ANWHILE_F_THM = store_thm 1003("SMALL_ANWHILE_F_THM", 1004 ``!s1 s2 l1 l2 b R c. 1005 ~(beval b s1) ==> 1006 (SMALL_EVAL (AnWhile b R c :: l1, s1) (l2, s2) = 1007 (l2 = l1) /\ (s2 = s1))``, 1008 RW_TAC std_ss [EQ_IMP_THM,Once small_ecases] 1009 THEN METIS_TAC small_rulel); 1010 1011val SMALL_ANWHILE_THM = store_thm 1012("SMALL_ANWHILE_THM", 1013 ``!s1 s2 l1 l2 b R c. 1014 SMALL_EVAL (AnWhile b R c :: l1, s1) (l2, s2) = 1015 (l2 = if beval b s1 then c :: AnWhile b R c :: l1 else l1) /\ (s2 = s1)``, 1016 METIS_TAC[SMALL_ANWHILE_T_THM,SMALL_ANWHILE_F_THM]); 1017 1018val SMALL_WHILE_THM = store_thm 1019("SMALL_WHILE_THM", 1020 ``!s1 s2 l1 l2 b c. 1021 SMALL_EVAL (While b c :: l1, s1) (l2, s2) = 1022 (l2 = if beval b s1 then c :: While b c :: l1 else l1) /\ (s2 = s1)``, 1023 METIS_TAC[SMALL_ANWHILE_THM,While_def]); 1024 1025val SMALL_LOCAL_IN_THM = store_thm 1026 ("SMALL_LOCAL_IN_THM", 1027 ``!s1 s2 l1 l2 v c. 1028 v IN FDOM s1 1029 ==> 1030 (SMALL_EVAL (Local v c :: l1, s1) (l2, s2) = 1031 (l2 = c :: GenAssign v (Exp(s1 ' v)) :: l1) 1032 /\ 1033 (s2 = s1))``, 1034 RW_TAC std_ss [EQ_IMP_THM,Once small_ecases] THEN METIS_TAC(FUPDATE_EQ:: small_rulel)); 1035 1036val SMALL_LOCAL_NOT_IN_THM = store_thm 1037 ("SMALL_LOCAL_NOT_IN_THM", 1038 ``!s1 s2 l1 l2 v c. 1039 ~(v IN FDOM s1) 1040 ==> 1041 (SMALL_EVAL (Local v c :: l1, s1) (l2, s2) = 1042 (l2 = c :: Dispose v :: l1) 1043 /\ 1044 (s2 = s1))``, 1045 RW_TAC std_ss [EQ_IMP_THM,Once small_ecases] THEN METIS_TAC(FUPDATE_EQ:: small_rulel)); 1046 1047val SMALL_LOCAL_THM = store_thm 1048 ("SMALL_LOCAL_THM", 1049 ``!s1 s2 l1 l2 v c. 1050 SMALL_EVAL (Local v c :: l1, s1) (l2, s2) = 1051 (l2 = c :: (if v IN FDOM s1 1052 then GenAssign v (Exp(s1 ' v)) 1053 else Dispose v) :: l1) 1054 /\ 1055 (s2 = s1)``, 1056 METIS_TAC[SMALL_LOCAL_IN_THM,SMALL_LOCAL_NOT_IN_THM]); 1057 1058val EVAL_IMP_SMALL_EVAL_LEMMA = 1059 store_thm 1060 ("EVAL_IMP_SMALL_EVAL_LEMMA", 1061 ``!c s1 s2. 1062 EVAL c s1 s2 1063 ==> 1064 (\c s1 s2. !l. TC SMALL_EVAL (c :: l, s1) (l, s2)) c s1 s2``, 1065 IndDefRules.RULE_TAC 1066 (IndDefRules.derive_mono_strong_induction [] (rules,induction)) 1067 THEN RW_TAC std_ss (TC_RULES :: small_rulel) 1068 THENL 1069 [METIS_TAC[SMALL_SEQ_THM,TC_RULES], (* Seq *) 1070 METIS_TAC[SMALL_IF_T_THM,TC_RULES], (* Cond true *) 1071 METIS_TAC[SMALL_IF_F_THM,TC_RULES], (* Cond false *) 1072 METIS_TAC[SMALL_ANWHILE_T_THM,TC_RULES], (* AnWhile true *) 1073 IMP_RES_TAC small_rules (* Local IN FDOM *) 1074 THEN `!l. TC SMALL_EVAL 1075 (c::GenAssign v (Exp(s1 ' v))::l,s1) 1076 (GenAssign v (Exp(s1 ' v))::l,s2)` 1077 by METIS_TAC[] 1078 THEN `!l. TC SMALL_EVAL 1079 (GenAssign v (Exp(s1 ' v))::l,s2) 1080 (l, s2 |+ (v,s1 ' v))` 1081 by METIS_TAC[small_rules,TC_RULES,neval_def,Update_Exp] 1082 THEN METIS_TAC [TC_RULES], 1083 METIS_TAC (* Local not IN FDOM *) 1084 [SMALL_LOCAL_NOT_IN_THM,SMALL_DISPOSE_THM,TC_RULES]]); 1085 1086val EVAL_IMP_SMALL_EVAL = 1087 store_thm 1088 ("EVAL_IMP_SMALL_EVAL", 1089 ``!c s1 s2. EVAL c s1 s2 ==>TC SMALL_EVAL ([c], s1) ([], s2)``, 1090 METIS_TAC[EVAL_IMP_SMALL_EVAL_LEMMA]); 1091 1092val SMALL_EVAL_NIL_LEMMA = 1093 store_thm 1094 ("SMALL_EVAL_NIL_LEMMA", 1095 ``!con1 con2. 1096 SMALL_EVAL con1 con2 1097 ==> 1098 (\con1 con2. ~(FST con1 = [])) con1 con2``, 1099 IndDefRules.RULE_TAC 1100 (IndDefRules.derive_mono_strong_induction [] (small_rules,small_induction)) 1101 THEN RW_TAC std_ss small_rulel); 1102 1103val SMALL_EVAL_NIL = 1104 store_thm 1105 ("SMALL_EVAL_NIL", 1106 ``!s con. ~(SMALL_EVAL ([],s) con)``, 1107 METIS_TAC[pairTheory.FST,SMALL_EVAL_NIL_LEMMA]); 1108 1109val TC_SMALL_EVAL_NIL_LEMMA = 1110 store_thm 1111 ("TC_SMALL_EVAL_NIL_LEMMA", 1112 ``!con1 con2. 1113 TC SMALL_EVAL con1 con2 1114 ==> 1115 (\con1 con2. ~(FST con1 = [])) con1 con2``, 1116 IndDefRules.RULE_TAC 1117 (IndDefRules.derive_mono_strong_induction [] (TC_RULES,TC_INDUCT)) 1118 THEN RW_TAC std_ss [SMALL_EVAL_NIL_LEMMA]); 1119 1120val TC_SMALL_EVAL_NIL = 1121 store_thm 1122 ("TC_SMALL_EVAL_NIL", 1123 ``!s con. ~(TC SMALL_EVAL ([],s) con)``, 1124 METIS_TAC[pairTheory.FST,TC_SMALL_EVAL_NIL_LEMMA]); 1125 1126(* Seql[c1;c2;...;cn] = Seq c1 (Seq c2 ... (Seq cn Skip) ... ) *) 1127val Seql_def = 1128 Define 1129 `(Seql [] = Skip) 1130 /\ 1131 (Seql (c :: l) = Seq c (Seql l))`; 1132 1133(* http://www4.informatik.tu-muenchen.de/~nipkow/pubs/fac98.html *) 1134val RANAN_FRAER_LEMMA = 1135 store_thm 1136 ("RANAN_FRAER_LEMMA", 1137 ``!con1 con2. 1138 SMALL_EVAL con1 con2 1139 ==> 1140 (\con1 con2. 1141 !s. EVAL (Seql(FST con2)) (SND con2) s 1142 ==> 1143 EVAL (Seql(FST con1)) (SND con1) s) con1 con2``, 1144 IndDefRules.RULE_TAC 1145 (IndDefRules.derive_mono_strong_induction [] (small_rules,small_induction)) 1146 THEN RW_TAC list_ss 1147 [neval_def,Seql_def,Update_Exp, 1148 SKIP_THM,GEN_ASSIGN_THM,DISPOSE_THM,SEQ_THM,IF_THM,LOCAL_THM] 1149 THEN METIS_TAC[ANWHILE_THM]); 1150 1151val SMALL_EVAL_IMP_EVAL_LEMMA = 1152 store_thm 1153 ("SMALL_EVAL_IMP_EVAL_LEMMA", 1154 ``!con1 con2. 1155 TC SMALL_EVAL con1 con2 1156 ==> 1157 (\con1 con2. 1158 !s. EVAL (Seql(FST con2)) (SND con2) s 1159 ==> 1160 EVAL (Seql(FST con1)) (SND con1) s) con1 con2``, 1161 IndDefRules.RULE_TAC 1162 (IndDefRules.derive_mono_strong_induction [] (TC_RULES,TC_INDUCT)) 1163 THEN RW_TAC std_ss [] 1164 THEN METIS_TAC[RANAN_FRAER_LEMMA]); 1165 1166val SMALL_EVAL_IMP_EVAL = 1167 store_thm 1168 ("SMALL_EVAL_IMP_EVAL", 1169 ``!c s1 s2. TC SMALL_EVAL ([c], s1) ([],s2) ==> EVAL c s1 s2``, 1170 RW_TAC std_ss [] 1171 THEN IMP_RES_TAC SMALL_EVAL_IMP_EVAL_LEMMA 1172 THEN FULL_SIMP_TAC list_ss [Seql_def,SEQ_THM,SKIP_THM]); 1173 1174val EVAL_SMALL_EVAL = 1175 store_thm 1176 ("EVAL_SMALL_EVAL", 1177 ``!c s1 s2. EVAL c s1 s2 = TC SMALL_EVAL ([c], s1) ([],s2)``, 1178 METIS_TAC[EVAL_IMP_SMALL_EVAL,SMALL_EVAL_IMP_EVAL]); 1179 1180(* Technical theorem to make EVAL work with lists for executing STEP_LIST *) 1181val CONS_if = 1182 store_thm 1183 ("CONS_if", 1184 ``x :: (if b then l1 else l2) = if b then x :: l1 else x :: l2``, 1185 METIS_TAC[]); 1186 1187(* Technical lemmas to simplify use of EVAL with EVAL_FUN *) 1188 1189val IS_SOME_if = 1190 store_thm 1191 ("IS_SOME_if", 1192 ``!(b:bool) x y. IS_SOME(if b then x else y) = if b then IS_SOME x else IS_SOME y``, 1193 METIS_TAC[]); 1194 1195val THE_if = 1196 store_thm 1197 ("THE_if", 1198 ``!(b:bool) x y. THE(if b then x else y) = if b then THE x else THE y``, 1199 METIS_TAC[]); 1200 1201val if_SOME = 1202 store_thm 1203 ("if_SOME", 1204 ``!(b:bool) x y. (if b then SOME x else SOME y) = SOME(if b then x else y)``, 1205 METIS_TAC[]); 1206 1207val SOME_EQ_ELIM = 1208 store_thm 1209 ("SOME_EQ_ELIM", 1210 ``!x y. (SOME x = SOME y) = (x = y)``, 1211 RW_TAC (srw_ss()) []); 1212 1213val _ = computeLib.add_persistent_funs 1214 ["IS_SOME_if", 1215 "THE_if", 1216 "if_SOME", 1217 "SOME_EQ_ELIM"]; 1218 1219(* Technical theorem to make EVAL work with output from SYMBOLIC_EVAL_PROVE *) 1220val ScalarOf_if = 1221 store_thm 1222 ("ScalarOf_if", 1223 ``ScalarOf((if b then s1 else s2) ' x) = 1224 if b then ScalarOf(s1 ' x) else ScalarOf(s2 ' x)``, 1225 METIS_TAC[]); 1226 1227(* More technical theorems for use with EVAL and the simplifier *) 1228 1229val ScalarOfIf = 1230 store_thm 1231 ("ScalarOfIf", 1232 ``ScalarOf(if b then x else y) = if b then ScalarOf x else ScalarOf y``, 1233 METIS_TAC[]); 1234 1235val ScalarIf = 1236 store_thm 1237 ("ScalarIf", 1238 ``Scalar(if b then x else y) = if b then Scalar x else Scalar y``, 1239 METIS_TAC[]); 1240 1241val EqLeftIf = 1242 store_thm 1243 ("EqLeftIf", 1244 ``(c = if b then x else y) = if b then c = x else c = y``, 1245 METIS_TAC[]); 1246 1247val EqRightIf = 1248 store_thm 1249 ("EqRightIf", 1250 ``((if b then x else y) = c) = if b then x = c else y = c``, 1251 METIS_TAC[]); 1252 1253val _ = computeLib.add_persistent_funs 1254 ["ScalarOfIf", 1255 "ScalarIf", 1256 "EqLeftIf", 1257 "EqRightIf"]; 1258 1259val int_opLeftIf = 1260 store_thm 1261 ("int_opLeftIf", 1262 ``!(f:int->int->int). f n (if b then x else y) = if b then f n x else f n y``, 1263 METIS_TAC[]); 1264 1265val int_opRightIf = 1266 store_thm 1267 ("int_opRightIf", 1268 ``!(f:int->int->int). f (if b then x else y) n = if b then f x n else f y n``, 1269 METIS_TAC[]); 1270 1271val int_relLeftIf = 1272 store_thm 1273 ("int_relLeftIf", 1274 ``!(r:int->int->bool). r n (if b then x else y) = if b then r n x else r n y``, 1275 METIS_TAC[]); 1276 1277val int_relRightIf = 1278 store_thm 1279 ("int_relRightIf", 1280 ``!(r:int->int->bool). r (if b then x else y) n = if b then r x n else r y n``, 1281 METIS_TAC[]); 1282 1283local 1284 fun f thl thr = 1285 (app 1286 (fn con => let 1287 val nl = (fst(dest_const con) ^ "LeftIf") 1288 val nr = (fst(dest_const con) ^ "RightIf") 1289 val _ = save_thm (nl, SPEC con thl) 1290 val _ = save_thm (nr, SPEC con thr) 1291 in computeLib.add_persistent_funs [nl,nr] end)) 1292in 1293 val _ = f int_opLeftIf int_opRightIf 1294 [``$int_add``,``$int_sub``]; 1295 val _ = f int_relLeftIf int_relRightIf 1296 [``$int_lt``,``$int_le``,``$int_gt``,``$int_ge``] 1297end 1298 1299 1300(* Monad binding operation *) 1301val RUN_BIND_def = 1302 Define 1303 `RUN_BIND m f = case m of 1304 TIMEOUT s -> TIMEOUT s 1305 || ERROR s -> ERROR s 1306 || RESULT s -> f s`; 1307 1308val _ = set_fixity ">>=" (Infixl 430); 1309val _ = overload_on (">>=", ``RUN_BIND``); 1310 1311(* Monad unit function *) 1312val RUN_RETURN_def = 1313 Define 1314 `RUN_RETURN x = RESULT x`; 1315 1316val RUN_MONAD_LAWS = 1317 store_thm 1318 ("RUN_MONAD_LAWS", 1319 ``((RUN_RETURN x) >>= f = f x) 1320 /\ 1321 (m >>= RUN_RETURN = m) 1322 /\ 1323 ((m >>= f) >>= g = m >>= (\x. (f x) >>= g))``, 1324 RW_TAC std_ss [RUN_BIND_def, RUN_RETURN_def] 1325 THEN Cases_on `m` 1326 THEN RW_TAC (srw_ss()) []); 1327 1328val RUN_BIND_RUN_RETURN_def = 1329 Define 1330 `RUN_BIND_RUN_RETURN m f = m >>= (RUN_RETURN o f)`; 1331 1332val RUN_BIND_RUN_RETURN = 1333 store_thm 1334 ("RUN_BIND_RUN_RETURN", 1335 ``RUN_BIND_RUN_RETURN m f = 1336 case m of 1337 TIMEOUT s -> TIMEOUT s 1338 || ERROR s -> ERROR s 1339 || RESULT s -> RESULT(f s)``, 1340 RW_TAC std_ss [RUN_BIND_RUN_RETURN_def,RUN_BIND_def,RUN_RETURN_def]); 1341 1342(* Add to EVAL compset *) 1343val _ = computeLib.add_persistent_funs["CONS_if"]; 1344 1345(* Technical theorems to make ML EVAL work with outcomes *) 1346 1347val outcome_case_def = 1348 prove 1349 (``(!f f1 f2 a. outcome_case f f1 f2 (RESULT a) = f a) /\ 1350 (!f f1 f2 a. outcome_case f f1 f2 (ERROR a) = f1 a) /\ 1351 (!f f1 f2 a. outcome_case f f1 f2 (TIMEOUT a) = f2 a)``, 1352 RW_TAC (srw_ss()) []); 1353 1354val outcome_case_if = 1355 store_thm 1356 ("outcome_case_if", 1357 ``!f f1 f2 b x y. 1358 outcome_case f f1 f2 (if b then x else y) = 1359 if b then outcome_case f f1 f2 x else outcome_case f f1 f2 y``, 1360 RW_TAC std_ss []); 1361 1362val pair_case_if = 1363 store_thm 1364 ("pair_case_if", 1365 ``!f b x y. 1366 pair_case f (if b then x else y) = 1367 if b then f (FST x) (SND x) else f (FST y) (SND y)``, 1368 RW_TAC std_ss [] 1369 THENL 1370 [Cases_on `x` 1371 THEN RW_TAC std_ss [], 1372 Cases_on `y` 1373 THEN RW_TAC std_ss []]); 1374 1375(* Add to EVAL compset *) 1376val _ = computeLib.add_persistent_funs 1377 ["outcome_case_def", 1378 "outcome_case_if", 1379 "pair_case_if" 1380 ]; 1381 1382(*===========================================================================*) 1383(* Clocked big step evaluator *) 1384(*===========================================================================*) 1385 1386(* Definition of RUN -- note use of monads to propagate outcomes *) 1387val RUN_def = 1388 Define 1389 `(RUN 0 c s = TIMEOUT s) 1390 /\ 1391 (RUN (SUC n) c s = 1392 case c of 1393 Skip -> RESULT s 1394 || GenAssign v e -> RESULT(Update v e s) 1395 || Dispose v -> RESULT(s \\ v) 1396 || Seq c1 c2 -> RUN n c1 s >>= RUN n c2 1397 || Cond b c1 c2 -> if beval b s 1398 then RUN n c1 s 1399 else RUN n c2 s 1400 || AnWhile b R c -> if beval b s 1401 then RUN n c s >>= RUN n (AnWhile b R c) 1402 else RESULT s 1403 || Local v c -> if v IN FDOM s 1404 then RUN n c s >>= (RESULT o (\s'. s' |+ (v, (s ' v)))) 1405 else RUN n c s >>= (RESULT o (\s'. s' \\ v)) 1406 )`; 1407 1408(* Lemma needed for EVAL_RUN *) 1409val RUN_EVAL_LEMMA = 1410 prove 1411 (``!n c s1 s2. (RUN n c s1 = RESULT s2) ==> EVAL c s1 s2``, 1412 Induct 1413 THEN Cases_on `c` 1414 THEN RW_TAC std_ss [RUN_def,rules,RUN_BIND_def] 1415 THEN RW_TAC std_ss [RUN_def,rules,RUN_BIND_def] 1416 THEN Cases_on `RUN n p s1` 1417 THEN Cases_on `RUN n p' s1` (* hack for PolyML from Magnus *) 1418 THEN FULL_SIMP_TAC (srw_ss()) [] 1419 THEN METIS_TAC[rules]); 1420 1421(* Lemma needed for EVAL_RUN *) 1422val EVAL_RUN_LEMMA = 1423 prove 1424 (``!c s1 s2. 1425 EVAL c s1 s2 1426 ==> 1427 (\c s1 s2. ?m. !n. m < n ==> (RUN n c s1 = RESULT s2)) c s1 s2``, 1428 IndDefRules.RULE_TAC 1429 (IndDefRules.derive_mono_strong_induction [] (rules,induction)) 1430 THEN RW_TAC std_ss [] 1431 THENL 1432 [Q.EXISTS_TAC `0` (* Skip *) 1433 THEN RW_TAC arith_ss [] 1434 THEN `?m. n = SUC m` by intLib.COOPER_TAC 1435 THEN RW_TAC std_ss [RUN_def,RUN_BIND_def], 1436 Q.EXISTS_TAC `0` (* GenAssign *) 1437 THEN RW_TAC arith_ss [] 1438 THEN `?m. n = SUC m` by intLib.COOPER_TAC 1439 THEN RW_TAC std_ss [RUN_def,RUN_BIND_def], 1440 Q.EXISTS_TAC `0` (* Dispose *) 1441 THEN RW_TAC arith_ss [] 1442 THEN `?m. n = SUC m` by intLib.COOPER_TAC 1443 THEN RW_TAC std_ss [RUN_def,RUN_BIND_def], 1444 Q.EXISTS_TAC `SUC(m+m')` (* Seq *) 1445 THEN RW_TAC arith_ss [] 1446 THEN `?p. n = SUC(m+m'+p)` by intLib.COOPER_TAC 1447 THEN RW_TAC std_ss [RUN_def,RUN_BIND_def] 1448 THEN `m < m+m'+p` by intLib.COOPER_TAC 1449 THEN `m' < m+m'+p` by intLib.COOPER_TAC 1450 THEN RW_TAC std_ss [RUN_def,RUN_BIND_def], 1451 Q.EXISTS_TAC `SUC m` (* Cond - test true *) 1452 THEN RW_TAC arith_ss [] 1453 THEN `?p. n = SUC(m+p)` by intLib.COOPER_TAC 1454 THEN RW_TAC std_ss [RUN_def,RUN_BIND_def] 1455 THEN `m < m+p` by intLib.COOPER_TAC 1456 THEN RW_TAC std_ss [RUN_def,RUN_BIND_def], 1457 Q.EXISTS_TAC `SUC m` (* Cond - test false *) 1458 THEN RW_TAC arith_ss [] 1459 THEN `?p. n = SUC(m+p)` by intLib.COOPER_TAC 1460 THEN RW_TAC std_ss [RUN_def,RUN_BIND_def] 1461 THEN `m < m+p` by intLib.COOPER_TAC 1462 THEN RW_TAC std_ss [RUN_def,RUN_BIND_def], 1463 Q.EXISTS_TAC `SUC m` (* While - test false *) 1464 THEN RW_TAC arith_ss [] 1465 THEN `?p. n' = SUC(m+p)` by intLib.COOPER_TAC 1466 THEN RW_TAC std_ss [RUN_def,RUN_BIND_def] 1467 THEN `m < m+p` by intLib.COOPER_TAC 1468 THEN RW_TAC std_ss [RUN_def,RUN_BIND_def], 1469 Q.EXISTS_TAC `SUC(m+m')` (* While - test true *) 1470 THEN RW_TAC arith_ss [] 1471 THEN `?p. n' = SUC(m+m'+p)` by intLib.COOPER_TAC 1472 THEN RW_TAC std_ss [RUN_def,RUN_BIND_def] 1473 THEN `m < m+m'+p` by intLib.COOPER_TAC 1474 THEN `m' < m+m'+p` by intLib.COOPER_TAC 1475 THEN RW_TAC std_ss [RUN_def,RUN_BIND_def], 1476 Q.EXISTS_TAC `SUC m` (* Local - v IN FDOM s1 case*) 1477 THEN RW_TAC arith_ss [] 1478 THEN `?p. n = SUC p` by intLib.COOPER_TAC 1479 THEN `m < p` by intLib.COOPER_TAC 1480 THEN RW_TAC std_ss [RUN_def,RUN_BIND_def], 1481 Q.EXISTS_TAC `SUC m` (* Local - ~(v IN FDOM s1) case*) 1482 THEN RW_TAC arith_ss [] 1483 THEN `?p. n = SUC p` by intLib.COOPER_TAC 1484 THEN `m < p` by intLib.COOPER_TAC 1485 THEN RW_TAC std_ss [RUN_def,RUN_BIND_def] 1486 ]); 1487 1488(* Correctness of RUN with respect to EVAL *) 1489val EVAL_RUN = 1490 store_thm 1491 ("EVAL_RUN", 1492 ``!c s1 s2. EVAL c s1 s2 = ?n. RUN n c s1 = RESULT s2``, 1493 METIS_TAC[DECIDE ``m < SUC m``, RUN_EVAL_LEMMA,EVAL_RUN_LEMMA]); 1494 1495val SPEC_RUN = 1496 store_thm 1497 ("SPEC_RUN", 1498 ``SPEC P c Q = !s1 s2 n. P s1 /\ (RUN n c s1 = RESULT s2) ==> Q s2``, 1499 METIS_TAC[SPEC_def,EVAL_RUN]); 1500 1501(* Corollary relating non-termination and TIMEOUT *) 1502val NOT_EVAL_RUN = 1503 store_thm 1504 ("NOT_EVAL_RUN", 1505 ``!c s1. ~(?s2. EVAL c s1 s2) = 1506 !n. ?s2. (RUN n c s1 = ERROR s2) \/ (RUN n c s1 = TIMEOUT s2)``, 1507 REPEAT STRIP_TAC 1508 THEN EQ_TAC 1509 THEN RW_TAC std_ss [] 1510 THENL 1511 [Cases_on `RUN n c s1` 1512 THEN METIS_TAC[EVAL_RUN], 1513 `!x y. ~(RESULT x = ERROR y) /\ ~(RESULT x = TIMEOUT y)` 1514 by RW_TAC (srw_ss()) [] 1515 THEN METIS_TAC[EVAL_RUN]]); 1516 1517(* Version of RUN for use by the HOL evaluator EVAL *) 1518val RUN = 1519 store_thm 1520 ("RUN", 1521 ``RUN n c s = 1522 if n = 0 1523 then TIMEOUT(s) 1524 else 1525 case c of 1526 Skip -> RESULT s 1527 || GenAssign v e -> RESULT(Update v e s) 1528 || Dispose v -> RESULT(s \\ v) 1529 || Seq c1 c2 -> RUN (n-1) c1 s >>= RUN (n-1) c2 1530 || Cond b c1 c2 -> if beval b s 1531 then RUN (n-1) c1 s 1532 else RUN (n-1) c2 s 1533 || AnWhile b R c -> if beval b s 1534 then RUN (n-1) c s >>= RUN (n-1) (AnWhile b R c) 1535 else RESULT s 1536 || Local v c -> if v IN FDOM s 1537 then RUN (n-1) c s >>= (RESULT o (\s'. s' |+ (v, (s ' v)))) 1538 else RUN (n-1) c s >>= (RESULT o (\s'. s' \\ v))``, 1539 Cases_on `n` 1540 THEN RW_TAC arith_ss [RUN_def,RUN_BIND_def]); 1541 1542(* Tell EVAL about RUN and various properties of finite maps *) 1543 1544val _ = computeLib.add_persistent_funs["RUN"]; 1545 1546(*===========================================================================*) 1547(* Small step next-state function *) 1548(*===========================================================================*) 1549 1550(* Single step *) 1551val STEP1_def = 1552 Define 1553 `(STEP1 ([], s) = ([], ERROR s)) 1554 /\ 1555 (STEP1 (Skip :: l, s) = (l, RESULT s)) 1556 /\ 1557 (STEP1 (GenAssign v e :: l, s) = (l, RESULT(Update v e s))) 1558 /\ 1559 (STEP1 (Dispose v :: l, s) = (l, RESULT(s \\ v))) 1560 /\ 1561 (STEP1 (Seq c1 c2 :: l, s) = (c1 :: c2 :: l, RESULT(s))) 1562 /\ 1563 (STEP1 (Cond b c1 c2 :: l, s) = 1564 if beval b s 1565 then (c1 :: l, RESULT s) 1566 else (c2 :: l, RESULT s)) 1567 /\ 1568 (STEP1 (AnWhile b R c :: l, s) = 1569 if beval b s 1570 then (c :: AnWhile b R c :: l, RESULT s) 1571 else (l, RESULT s)) 1572 /\ 1573 (STEP1 (Local v c :: l, s) = 1574 if v IN FDOM s 1575 then (c :: GenAssign v (Exp(s ' v)) :: l, RESULT s) 1576 else (c :: Dispose v :: l, RESULT s))`; 1577 1578(* Version needed for evaluation by EVAL *) 1579val STEP1 = 1580 store_thm 1581 ("STEP1", 1582 ``!l s. 1583 STEP1 (l, s) = 1584 if NULL l 1585 then (l, ERROR s) 1586 else 1587 case (HD l) of 1588 Skip -> (TL l, RESULT s) 1589 || GenAssign v e -> (TL l, RESULT(Update v e s)) 1590 || Dispose v -> (TL l, RESULT(s \\ v)) 1591 || Seq c1 c2 -> (c1 :: c2 :: TL l, RESULT s) 1592 || Cond b c1 c2 -> if beval b s 1593 then (c1 :: TL l, RESULT s) 1594 else (c2 :: TL l, RESULT s) 1595 || AnWhile b R c -> if beval b s 1596 then (c :: AnWhile b R c :: TL l, RESULT s) 1597 else (TL l, RESULT s) 1598 || Local v c -> if v IN FDOM s 1599 then (c :: GenAssign v (Exp(s ' v)) :: TL l, RESULT s) 1600 else (c :: Dispose v :: TL l, RESULT s)``, 1601 Induct 1602 THEN RW_TAC list_ss [STEP1_def] 1603 THEN Cases_on `h` 1604 THEN RW_TAC list_ss [STEP1_def]); 1605 1606(* Add to EVAL compset *) 1607val _ = computeLib.add_persistent_funs ["STEP1"]; 1608 1609(* Various lemmas follow -- I'm not sure they are all needed *) 1610val SMALL_EVAL_IMP_STEP1 = 1611 prove 1612 (``!con1 con2. 1613 SMALL_EVAL con1 con2 1614 ==> 1615 (\con1 con2. 1616 STEP1 con1 = (FST con2, RESULT(SND con2))) con1 con2``, 1617 IndDefRules.RULE_TAC 1618 (IndDefRules.derive_mono_strong_induction [] (small_rules,small_induction)) 1619 THEN RW_TAC list_ss [STEP1_def]); 1620 1621val STEP1_IMP_SMALL_EVAL = 1622 prove 1623 (``!c l1 s1 l2 s2. 1624 (STEP1 (c :: l1, s1) = (l2, RESULT s2)) 1625 ==> 1626 SMALL_EVAL (c :: l1, s1) (l2, s2)``, 1627 Induct 1628 THEN RW_TAC std_ss 1629 [STEP1_def,small_rules,neval_def, 1630 SMALL_GEN_ASSIGN_THM,SMALL_DISPOSE_THM,SMALL_IF_THM,SMALL_SEQ_THM, 1631 SMALL_LOCAL_THM] 1632 THEN METIS_TAC[small_rules]); 1633 1634val STEP1_SMALL_EVAL = 1635 store_thm 1636 ("STEP1_SMALL_EVAL", 1637 ``!l1 s1 l2 s2. 1638 (STEP1 (l1, s1) = (l2, RESULT s2)) 1639 = 1640 SMALL_EVAL (l1, s1) (l2, s2)``, 1641 Induct 1642 THENL 1643 [RW_TAC (srw_ss()) [STEP1_def,SMALL_EVAL_NIL], 1644 METIS_TAC 1645 [STEP1_IMP_SMALL_EVAL,SMALL_EVAL_IMP_STEP1, 1646 pairTheory.FST,pairTheory.SND]]); 1647 1648val NOT_SMALL_EVAL_ERROR = 1649 store_thm 1650 ("NOT_SMALL_EVAL_ERROR", 1651 ``!con1 con2. 1652 ~(?con2. SMALL_EVAL con1 con2) = 1653 ?s. (SND(STEP1 con1 ) = ERROR s) \/ (SND(STEP1 con1 ) = TIMEOUT s)``, 1654 REPEAT STRIP_TAC 1655 THEN EQ_TAC 1656 THEN RW_TAC std_ss [] 1657 THEN Cases_on `con1` THEN TRY(Cases_on `q`) THEN TRY(Cases_on `h`) 1658 THEN RW_TAC (srw_ss()) [STEP1_def] 1659 THEN FULL_SIMP_TAC (srw_ss()) [STEP1_def] 1660 THEN TRY (METIS_TAC 1661 [SMALL_SKIP_THM,SMALL_GEN_ASSIGN_THM,SMALL_DISPOSE_THM,SMALL_IF_THM,SMALL_SEQ_THM, 1662 SMALL_LOCAL_THM,SMALL_ANWHILE_THM,outcome_distinct,outcome_11, 1663 pairTheory.SND,COND_RAND,SMALL_EVAL_NIL]) 1664 THEN TRY(Cases_on `con2`) 1665 THEN TRY(POP_ASSUM(ASSUME_TAC o Q.GEN `l2` o Q.GEN `s2` o Q.SPEC `(l2,s2)`)) 1666 THEN FULL_SIMP_TAC (srw_ss()) [] 1667 THEN TRY (METIS_TAC 1668 [SMALL_SKIP_THM,SMALL_GEN_ASSIGN_THM,SMALL_DISPOSE_THM,SMALL_IF_THM,SMALL_SEQ_THM, 1669 SMALL_LOCAL_THM,SMALL_ANWHILE_THM,outcome_distinct,outcome_11, 1670 outcome_nchotomy,pairTheory.SND,COND_RAND,SMALL_EVAL_NIL])); 1671 1672(* Iterated SMALL_EVAL *) 1673val SMALL_EVAL_ITER_def = 1674 Define 1675 `(SMALL_EVAL_ITER 0 con1 con2 = SMALL_EVAL con1 con2) 1676 /\ 1677 (SMALL_EVAL_ITER (SUC n) con1 con2 = 1678 ?con. SMALL_EVAL con1 con /\ SMALL_EVAL_ITER n con con2)`; 1679 1680(* More convenient version (doesn't introduce ``con``) *) 1681val SMALL_EVAL_ITER = 1682 store_thm 1683 ("SMALL_EVAL_ITER", 1684 ``(SMALL_EVAL_ITER 0 con1 con2 = SMALL_EVAL con1 con2) 1685 /\ 1686 (SMALL_EVAL_ITER (SUC n) con1 con2 = 1687 ?l s. SMALL_EVAL con1 (l,s) /\ SMALL_EVAL_ITER n (l,s) con2)``, 1688 RW_TAC std_ss [pairTheory.EXISTS_PROD,SMALL_EVAL_ITER_def]); 1689 1690val SMALL_EVAL_ITER_LEMMA = 1691 prove 1692 (``!n1 x y. 1693 SMALL_EVAL_ITER n1 x y 1694 ==> 1695 !n2 z. SMALL_EVAL_ITER n2 y z ==> ?n3. SMALL_EVAL_ITER n3 x z``, 1696 Induct 1697 THEN METIS_TAC[SMALL_EVAL_ITER_def]); 1698 1699val SMALL_EVAL_ITER_TC_LEMMA1 = 1700 prove 1701 (``!n con1 con2. SMALL_EVAL_ITER n con1 con2 ==> TC SMALL_EVAL con1 con2``, 1702 Induct 1703 THEN METIS_TAC[SMALL_EVAL_ITER_def,TC_RULES]); 1704 1705val SMALL_EVAL_ITER_TC_LEMMA2 = 1706 prove 1707 (``!con1 con2. 1708 TC SMALL_EVAL con1 con2 1709 ==> 1710 (\con1 con2. ?n. SMALL_EVAL_ITER n con1 con2) con1 con2``, 1711 IndDefRules.RULE_TAC 1712 (IndDefRules.derive_mono_strong_induction [] (TC_RULES,TC_INDUCT)) 1713 THEN RW_TAC std_ss [] 1714 THEN METIS_TAC[SMALL_EVAL_ITER_def,TC_RULES,SMALL_EVAL_ITER_LEMMA]); 1715 1716val SMALL_EVAL_ITER_TC = 1717 store_thm 1718 ("SMALL_EVAL_ITER_TC", 1719 ``!con1 con2. 1720 TC SMALL_EVAL con1 con2 = ?n. SMALL_EVAL_ITER n con1 con2``, 1721 REPEAT GEN_TAC 1722 THEN EQ_TAC 1723 THEN METIS_TAC[SMALL_EVAL_ITER_TC_LEMMA1,SMALL_EVAL_ITER_TC_LEMMA2,TC_RULES]); 1724 1725val SMALL_EVAL_ITER_TC = 1726 store_thm 1727 ("SMALL_EVAL_ITER_TC", 1728 ``!con1 con2. 1729 TC SMALL_EVAL con1 con2 = ?n. SMALL_EVAL_ITER n con1 con2``, 1730 REPEAT GEN_TAC 1731 THEN EQ_TAC 1732 THEN METIS_TAC[SMALL_EVAL_ITER_TC_LEMMA1,SMALL_EVAL_ITER_TC_LEMMA2,TC_RULES]); 1733 1734val SMALL_EVAL_TC_SMALL_EVAL = 1735 store_thm 1736 ("SMALL_EVAL_TC_SMALL_EVAL", 1737 ``!con1 con2. SMALL_EVAL con1 con2 ==> TC SMALL_EVAL con1 con2``, 1738 METIS_TAC[TC_RULES]); 1739 1740val TC_SMALL_EVAL_TRANS = 1741 store_thm 1742 ("TC_SMALL_EVAL_TRANS", 1743 ``!con1 con2 con3. 1744 TC SMALL_EVAL con1 con2 1745 ==> 1746 TC SMALL_EVAL con2 con3 1747 ==> TC 1748 SMALL_EVAL con1 con3``, 1749 METIS_TAC[TC_RULES]); 1750 1751val STEP_BIND_def = 1752 Define 1753 `STEP_BIND m f = case m of 1754 (l, TIMEOUT s) -> (l, TIMEOUT s) 1755 || (l, ERROR s) -> (l, ERROR s) 1756 || (l, RESULT s) -> f(l, s)`; 1757 1758val _ = overload_on (">>=", ``STEP_BIND``); 1759 1760(* Monad unit function *) 1761val STEP_RETURN_def = 1762 Define 1763 `STEP_RETURN x = (FST x, RESULT(SND x))`; 1764 1765val STEP_MONAD_LAWS = 1766 store_thm 1767 ("STEP_MONAD_LAWS", 1768 ``((STEP_RETURN x) >>= f = f x) 1769 /\ 1770 (m >>= STEP_RETURN = m) 1771 /\ 1772 ((m >>= f) >>= g = m >>= (\x. (f x) >>= g))``, 1773 RW_TAC std_ss [STEP_BIND_def, STEP_RETURN_def] 1774 THEN Cases_on `m` 1775 THEN Cases_on `r` 1776 THEN RW_TAC (srw_ss()) []); 1777 1778 1779(* Clocked next-state function *) 1780val STEP_def = 1781 Define 1782 `STEP (n:num) (l,s) = 1783 if (l = []) 1784 then ([], RESULT s) 1785 else if n = 0 1786 then (l, TIMEOUT s) 1787 else STEP1(l,s) >>= STEP (n-1)`; 1788 1789val STEP0 = 1790 store_thm 1791 ("STEP0", 1792 ``STEP 0 (l,s) = if l = [] then ([], RESULT s) else (l, TIMEOUT s)``, 1793 METIS_TAC[STEP_def,STEP_BIND_def]); 1794 1795val STEP_SUC = 1796 store_thm 1797 ("STEP_SUC", 1798 ``STEP (SUC n) (l, s) = 1799 if (l = []) 1800 then ([], RESULT s) 1801 else STEP1(l,s) >>= STEP n``, 1802 METIS_TAC[STEP_def, DECIDE ``~(SUC n = 0) /\ ((SUC n) - 1 = n)``]); 1803 1804(* Explode into various cases (could have been the definition of STEP) *) 1805val STEP = 1806 store_thm 1807 ("STEP", 1808 ``(STEP n ([],s) = ([], RESULT s)) 1809 /\ 1810 (STEP 0 (l,s) = if l = [] then ([], RESULT s) else (l, TIMEOUT s)) 1811 /\ 1812 (STEP (SUC n) (Skip :: l, s) = 1813 STEP n (l, s)) 1814 /\ 1815 (STEP (SUC n) (GenAssign v e :: l, s) = 1816 STEP n (l, Update v e s)) 1817 /\ 1818 (STEP (SUC n) (Dispose v :: l, s) = 1819 STEP n (l, s \\ v)) 1820 /\ 1821 (STEP (SUC n) (Seq c1 c2 :: l, s) = 1822 STEP n (c1 :: c2 :: l, s)) 1823 /\ 1824 (STEP (SUC n) (Cond b c1 c2 :: l, s) = 1825 if beval b s 1826 then STEP n (c1 :: l, s) 1827 else STEP n (c2 :: l, s)) 1828 /\ 1829 (STEP (SUC n) (AnWhile b R c :: l, s) = 1830 if beval b s 1831 then STEP n (c :: AnWhile b R c :: l, s) 1832 else STEP n (l, s)) 1833 /\ 1834 (STEP (SUC n) (Local v c :: l, s) = 1835 if v IN FDOM s 1836 then STEP n (c :: GenAssign v (Exp(s ' v)) :: l, s) 1837 else STEP n (c :: Dispose v :: l, s))``, 1838 Induct_on `n` 1839 THEN RW_TAC list_ss [STEP1,STEP0,STEP_SUC,STEP_BIND_def]); 1840 1841val STEP_NIL = 1842 store_thm 1843 ("STEP_NIL", 1844 ``!n l1 s1 l2 s2. (STEP n (l1,s1) = (l2, RESULT s2)) ==> (l2 = [])``, 1845 Induct 1846 THEN RW_TAC std_ss [STEP,STEP_BIND_def] 1847 THEN FULL_SIMP_TAC std_ss [STEP_SUC,STEP_BIND_def] 1848 THEN Cases_on `l1 = []` 1849 THEN RW_TAC std_ss [] 1850 THEN POP_ASSUM(fn th => FULL_SIMP_TAC (srw_ss()) [th]) 1851 THEN Cases_on `STEP1 (l1,s1)` 1852 THEN RW_TAC std_ss [] 1853 THEN Cases_on `r` 1854 THEN RW_TAC std_ss [] 1855 THEN FULL_SIMP_TAC (srw_ss()) [] 1856 THEN METIS_TAC[]); 1857 1858val STEP_MONO = 1859 store_thm 1860 ("STEP_MONO", 1861 ``!m n l1 s1 s2. 1862 m <= n /\ (STEP m (l1,s1) = ([], RESULT s2)) 1863 ==> (STEP n (l1,s1) = ([], RESULT s2)) ``, 1864 Induct 1865 THEN RW_TAC std_ss [STEP,STEP_SUC,STEP_BIND_def] 1866 THEN Cases_on `STEP1 (l1,s1)` 1867 THEN RW_TAC std_ss [] 1868 THEN Cases_on `r` 1869 THEN RW_TAC std_ss [] 1870 THEN FULL_SIMP_TAC (srw_ss()) [] 1871 THEN Induct_on `n` 1872 THEN RW_TAC std_ss [STEP,STEP_SUC,STEP_BIND_def]); 1873 1874val SMALL_EVAL_ITER_IMP_STEP = 1875 store_thm 1876 ("SMALL_EVAL_ITER_IMP_STEP", 1877 ``!m n l1 s1 s2. 1878 SMALL_EVAL_ITER m (l1,s1) ([],s2) /\ m < n 1879 ==> (STEP n (l1,s1) = ([], RESULT s2))``, 1880 Induct THEN Induct 1881 THEN FULL_SIMP_TAC (srw_ss()) 1882 [SMALL_EVAL_ITER,STEP_SUC,STEP,GSYM STEP1_SMALL_EVAL,STEP_BIND_def] 1883 THEN Cases_on `l1 = []` 1884 THEN RW_TAC std_ss [] 1885 THEN FULL_SIMP_TAC (srw_ss()) [STEP1]); 1886 1887val STEP_IMP_SMALL_EVAL_ITER = 1888 store_thm 1889 ("STEP_IMP_SMALL_EVAL_ITER", 1890 ``!n l1 s1 s2. 1891 (STEP n (l1,s1) = ([], RESULT s2)) /\ ~(l1 = []) 1892 ==> 1893 ?m. m < n /\ SMALL_EVAL_ITER m (l1,s1) ([],s2)``, 1894 Induct 1895 THEN FULL_SIMP_TAC (srw_ss()) [SMALL_EVAL_ITER,STEP_SUC,STEP,STEP_BIND_def] 1896 THEN RW_TAC (srw_ss()) [] 1897 THEN Cases_on `STEP1 (l1,s1)` 1898 THEN FULL_SIMP_TAC (srw_ss()) [] 1899 THEN Cases_on `r` 1900 THEN RW_TAC std_ss [] 1901 THEN FULL_SIMP_TAC (srw_ss()) [] 1902 THEN Cases_on `q = []` 1903 THEN RW_TAC std_ss [] 1904 THEN FULL_SIMP_TAC (srw_ss()) [STEP,STEP1_SMALL_EVAL] 1905 THEN RW_TAC std_ss [] 1906 THENL 1907 [Q.EXISTS_TAC `0` 1908 THEN RW_TAC std_ss [SMALL_EVAL_ITER], 1909 RES_TAC 1910 THEN Q.EXISTS_TAC `SUC m` 1911 THEN RW_TAC std_ss [SMALL_EVAL_ITER] 1912 THEN METIS_TAC[]]); 1913 1914val SMALL_EVAL_ITER_STEP = 1915 store_thm 1916 ("SMALL_EVAL_ITER_STEP", 1917 ``!n c l s1 s2. 1918 (?m. m < n /\ SMALL_EVAL_ITER m (c :: l, s1) ([],s2)) 1919 = 1920 (STEP n (c :: l, s1) = ([], RESULT s2))``, 1921 REPEAT STRIP_TAC 1922 THEN EQ_TAC 1923 THEN RW_TAC pure_ss [] 1924 THENL 1925 [METIS_TAC[SMALL_EVAL_ITER_IMP_STEP], 1926 `~(c :: l = [])` by RW_TAC list_ss [] 1927 THEN METIS_TAC[STEP_IMP_SMALL_EVAL_ITER]]); 1928 1929val TC_SMALL_EVAL_STEP = 1930 store_thm 1931 ("TC_SMALL_EVAL_STEP", 1932 ``!c l s1 s2. 1933 TC SMALL_EVAL (c :: l, s1) ([],s2) 1934 = 1935 ?n. STEP n (c :: l, s1) = ([], RESULT s2)``, 1936 RW_TAC std_ss [SMALL_EVAL_ITER_TC,GSYM SMALL_EVAL_ITER_STEP] 1937 THEN METIS_TAC[DECIDE``n < SUC n``]); 1938 1939(* Corollary relating non-termination and TIMEOUT *) 1940val NOT_SMALL_EVAL_STEP_COR = 1941 store_thm 1942 ("NOT_SMALL_EVAL_STEP_COR", 1943 ``!c l1 s1. 1944 ~(?s2. TC SMALL_EVAL (c :: l1, s1) ([], s2)) = 1945 !n. ?l2 s2. (STEP n (c :: l1, s1) = (l2,ERROR s2) ) 1946 \/ 1947 (STEP n (c :: l1, s1) = (l2,TIMEOUT s2))``, 1948 REPEAT STRIP_TAC 1949 THEN RW_TAC std_ss [TC_SMALL_EVAL_STEP] 1950 THEN EQ_TAC 1951 THEN RW_TAC std_ss [] 1952 THENL 1953 [Cases_on `STEP n (c :: l1, s1)` 1954 THEN Cases_on `r` 1955 THEN RW_TAC (srw_ss()) [] 1956 THEN METIS_TAC[STEP_NIL], 1957 `!x y. ~(RESULT x = ERROR y) /\ ~(RESULT x = TIMEOUT y)` 1958 by RW_TAC (srw_ss()) [] 1959 THEN `?l2 s2. (STEP n (c::l1,s1) = (l2,ERROR s2)) 1960 \/ 1961 (STEP n (c::l1,s1) = (l2,TIMEOUT s2))` 1962 by METIS_TAC[] 1963 THEN RW_TAC (srw_ss()) []]); 1964 1965val NOT_SMALL_EVAL_STEP = 1966 store_thm 1967 ("NOT_SMALL_EVAL_STEP", 1968 ``!c s1. 1969 ~(?s2. TC SMALL_EVAL ([c], s1) ([], s2)) = 1970 !n. ?l s2. (STEP n ([c], s1) = (l,ERROR s2) ) 1971 \/ 1972 (STEP n ([c], s1) = (l,TIMEOUT s2))``, 1973 METIS_TAC[NOT_SMALL_EVAL_STEP_COR]); 1974 1975val EVAL_STEP = 1976 store_thm 1977 ("EVAL_STEP", 1978 ``!c s1 s2. 1979 EVAL c s1 s2 = ?n. STEP n ([c], s1) = ([], RESULT s2)``, 1980 RW_TAC list_ss [EVAL_SMALL_EVAL,TC_SMALL_EVAL_STEP]); 1981 1982val RUN_STEP = 1983 store_thm 1984 ("RUN_STEP", 1985 ``!c s1 s2. 1986 (?n. RUN n c s1 = RESULT s2) = (?n. STEP n ([c],s1) = ([],RESULT s2))``, 1987 METIS_TAC[EVAL_SMALL_EVAL,EVAL_RUN,TC_SMALL_EVAL_STEP]); 1988 1989(* Some lemmas *) 1990 1991val FUPDATE_ID = 1992 store_thm 1993 ("FUPDATE_ID", 1994 ``!f x. x IN FDOM f ==> (f |+ (x, f ' x) = f)``, 1995 METIS_TAC[FDOM_EQ_FDOM_FUPDATE,FAPPLY_FUPDATE_THM,fmap_EQ_THM]); 1996 1997val DOM_FUPDATE_DOMSUB = 1998 store_thm 1999 ("DOM_FUPDATE_DOMSUB", 2000 ``!f x y. x IN FDOM f ==> (FDOM((f \\ x) |+ (x,y)) = FDOM f)``, 2001 RW_TAC std_ss [FDOM_FUPDATE,FDOM_DOMSUB,pred_setTheory.INSERT_DELETE]); 2002 2003val FUPDATE_DOMSUB = 2004 store_thm 2005 ("FUPDATE_DOMSUB", 2006 ``!f x. x IN FDOM f ==> (f \\ x |+ (x, f ' x) = f)``, 2007 RW_TAC std_ss [] 2008 THEN `FDOM(f \\ x |+ (x,f ' x)) = FDOM f` 2009 by METIS_TAC[FDOM_FUPDATE,FDOM_DOMSUB,pred_setTheory.INSERT_DELETE] 2010 THEN `!z. z IN FDOM f ==> ((f \\ x |+ (x,f ' x)) ' z = f ' z)` 2011 by METIS_TAC[FAPPLY_FUPDATE_THM,DOMSUB_FAPPLY_THM] 2012 THEN METIS_TAC[fmap_EQ_THM]); 2013 2014val NEVAL_FUPDATE_LEMMA = 2015 prove 2016 (``!e s v. neval e (s |+ (v,s ' v)) = neval e s``, 2017 Induct 2018 THEN RW_TAC std_ss [neval_def,FAPPLY_FUPDATE_THM]); 2019 2020val AEVAL_FUPDATE_LEMMA = 2021 prove 2022 (``!a s v. aeval a (s |+ (v,s ' v)) = aeval a s``, 2023 Induct 2024 THEN RW_TAC std_ss 2025 [aeval_def,FAPPLY_FUPDATE_THM,NOT_FDOM_FAPPLY_FEMPTY,NEVAL_FUPDATE_LEMMA]); 2026 2027(* 2028``ACC_PRED p c s1 s2`` is the constraint after 2029executing command c in state s1 with precondition p 2030*) 2031 2032val ACC_PRED_def = 2033 Define 2034 `(ACC_PRED p Skip s1 = p) 2035 /\ 2036 (ACC_PRED p (GenAssign v e) s1 = 2037 \s2. 2038 if v IN FDOM s1 2039 then ((s2 ' v = Update v e s1 ' v) /\ p(s2 |+ (v,(s1 ' v)))) 2040 else ((s2 ' v = Update v e s1 ' v) /\ p(s2 \\ v))) 2041 /\ 2042 (ACC_PRED p (Dispose v) s1 = 2043 \s2. if v IN FDOM s1 then p(s2 |+ (v,(s1 ' v))) else p s2) 2044 /\ 2045 (ACC_PRED p (Seq c1 c2) s1 = p) 2046 /\ 2047 (ACC_PRED p (Cond b c1 c2) s1 = 2048 if beval b s1 2049 then (\s2. beval b s2 /\ p s2) 2050 else (\s2. ~(beval b s2) /\ p s2)) 2051 /\ 2052 (ACC_PRED p (AnWhile b R c) s1 = 2053 if beval b s1 2054 then (\s2. beval b s2 /\ p s2) 2055 else (\s2. ~(beval b s2) /\ p s2)) 2056 /\ 2057 (ACC_PRED p (Local v c) s1 = 2058 if v IN FDOM s1 2059 then (\s2. v IN FDOM s2 /\ p s2) 2060 else (\s2. ~(v IN FDOM s2) /\ p s2))`; 2061 2062val ACC_PRED_ASSIGN_LEMMA = 2063 store_thm 2064 ("ACC_PRED_ASSIGN_LEMMA", 2065 ``!p v e s. p s ==> ACC_PRED p (GenAssign v e) s (Update v e s)``, 2066 RW_TAC std_ss [] 2067 THEN Cases_on `e` 2068 THEN RW_TAC std_ss 2069 [ACC_PRED_def,UpdateCases,FUPDATE_EQ,FAPPLY_FUPDATE,UpdateCases, 2070 FUPDATE_ID,NEVAL_FUPDATE_LEMMA,AEVAL_FUPDATE_LEMMA, 2071 DOMSUB_FUPDATE,DOMSUB_NOT_IN_DOM]); 2072 2073val ACC_PRED_DISPOSE_LEMMA = 2074 store_thm 2075 ("ACC_PRED_DISPOSE_LEMMA", 2076 ``!p v s. p s ==> ACC_PRED p (Dispose v) s (s \\ v)``, 2077 RW_TAC std_ss 2078 [ACC_PRED_def,FUPDATE_EQ,FAPPLY_FUPDATE, 2079 FUPDATE_ID,NEVAL_FUPDATE_LEMMA,AEVAL_FUPDATE_LEMMA, 2080 DOMSUB_FUPDATE,DOMSUB_NOT_IN_DOM,FUPDATE_DOMSUB]); 2081 2082val SMALL_EVAL_ACC_PRED_LEMMA = 2083 store_thm 2084 ("SMALL_EVAL_ACC_PRED_LEMMA", 2085 ``!con1 con2. 2086 SMALL_EVAL con1 con2 2087 ==> 2088 (\con1 con2. 2089 p(SND con1) 2090 ==> 2091 ACC_PRED p (HD(FST con1)) (SND con1) (SND con2)) 2092 con1 con2``, 2093 IndDefRules.RULE_TAC 2094 (IndDefRules.derive_mono_strong_induction [] (small_rules,small_induction)) 2095 THEN RW_TAC list_ss [ACC_PRED_ASSIGN_LEMMA,ACC_PRED_DISPOSE_LEMMA] 2096 THEN RW_TAC list_ss [ACC_PRED_def]); 2097 2098val SMALL_EVAL_ACC_PRED = 2099 store_thm 2100 ("SMALL_EVAL_ACC_PRED", 2101 ``!c p l1 l2 s1 s2. 2102 p s1 2103 ==> 2104 SMALL_EVAL (c::l1,s1) (l2,s2) 2105 ==> 2106 ACC_PRED p c s1 s2``, 2107 METIS_TAC 2108 [SMALL_EVAL_ACC_PRED_LEMMA,listTheory.HD,pairTheory.FST,pairTheory.SND]); 2109 2110val STEP1_ACC_PRED = 2111 store_thm 2112 ("STEP1_ACC_PRED", 2113 ``!c p l1 l2 s1 s2. 2114 p s1 2115 ==> 2116 (STEP1(c::l1,s1) = (l2, RESULT s2)) 2117 ==> 2118 ACC_PRED p c s1 s2``, 2119 METIS_TAC[SMALL_EVAL_ACC_PRED,STEP1_SMALL_EVAL]); 2120 2121(*===========================================================================*) 2122(* Property-acculating small-step semantics as in Collavizza et al. paper *) 2123(*===========================================================================*) 2124 2125val ACC_SMALL_EVAL_def = 2126 Define 2127 `ACC_SMALL_EVAL (con1, p1) (con2, p2) = 2128 SMALL_EVAL con1 con2 /\ (p2 = ACC_PRED p1 (HD(FST con1)) (SND con1))`; 2129 2130val ACC_SMALL_EVAL = 2131 store_thm 2132 ("ACC_SMALL_EVAL", 2133 ``(ACC_SMALL_EVAL (([], s1), p1) ((l2, s2), p2) = F) 2134 /\ 2135 (ACC_SMALL_EVAL ((c :: l1, s1), p1) ((l2, s2), p2) = 2136 SMALL_EVAL (c :: l1, s1) (l2, s2) /\ (p2 = ACC_PRED p1 c s1))``, 2137 RW_TAC list_ss [ACC_SMALL_EVAL_def,SMALL_EVAL_NIL]); 2138 2139val IS_SOME_EXISTS = 2140 store_thm 2141 ("IS_SOME_EXISTS", 2142 ``!x. IS_SOME x = ?y. x = SOME y``, 2143 Cases 2144 THEN RW_TAC std_ss []); 2145 2146val ACC_SMALL_EVAL_CLAUSES = 2147 store_thm 2148 ("ACC_SMALL_EVAL_CLAUSES", 2149 ``(!s1 p1 l2 s2 p2. 2150 ACC_SMALL_EVAL (([], s1), p1) ((l2, s2), p2) = F) 2151 /\ 2152 (!s1 l p. 2153 ACC_SMALL_EVAL ((Skip :: l, s1), p) ((l, s1), p)) 2154 /\ 2155 (!s1 v e l p. 2156 v IN FDOM s1 2157 ==> 2158 ACC_SMALL_EVAL 2159 ((GenAssign v e :: l, s1), p) 2160 ((l, 2161 Update v e s1), 2162 \s2. (s2 ' v = Update v e s1 ' v) 2163 /\ 2164 p(s2 |+ (v,(s1 ' v))))) 2165 /\ 2166 (!s1 v e l p. 2167 ~(v IN FDOM s1) 2168 ==> 2169 ACC_SMALL_EVAL 2170 ((GenAssign v e :: l, s1), p) 2171 ((l, 2172 Update v e s1), 2173 \s2. (s2 ' v = Update v e s1 ' v) 2174 /\ 2175 p(s2 \\ v))) 2176 /\ 2177 (!s1 v l p. 2178 v IN FDOM s1 2179 ==> 2180 ACC_SMALL_EVAL 2181 ((Dispose v :: l, s1), p) 2182 ((l, s1 \\ v), \s2. p(s2 |+ (v,(s1 ' v))))) 2183 /\ 2184 (!s1 v l p. 2185 ~(v IN FDOM s1) 2186 ==> 2187 ACC_SMALL_EVAL 2188 ((Dispose v :: l, s1), p) 2189 ((l, s1 \\ v), p)) 2190 /\ 2191 (!s1 l c1 c2 p. 2192 ACC_SMALL_EVAL 2193 ((Seq c1 c2 :: l, s1), p) 2194 ((c1 :: c2 :: l, s1), p)) 2195 /\ 2196 (!s1 l b c1 c2 p. 2197 beval b s1 2198 ==> 2199 ACC_SMALL_EVAL 2200 ((Cond b c1 c2 :: l, s1), p) 2201 ((c1 :: l, s1), \s2. beval b s2 /\ p s2)) 2202 /\ 2203 (!s1 l b c1 c2 p. 2204 ~(beval b s1) 2205 ==> 2206 ACC_SMALL_EVAL 2207 ((Cond b c1 c2 :: l, s1), p) 2208 ((c2 :: l, s1), \s2. ~(beval b s2) /\ p s2)) 2209 /\ 2210 (!s1 l b R c p. 2211 beval b s1 2212 ==> 2213 ACC_SMALL_EVAL 2214 ((AnWhile b R c :: l, s1), p) 2215 ((c :: AnWhile b R c :: l, s1), \s2. beval b s2 /\ p s2)) 2216 /\ 2217 (!s1 l b R c p. 2218 ~(beval b s1) 2219 ==> 2220 ACC_SMALL_EVAL 2221 ((AnWhile b R c :: l, s1), p) 2222 ((l, s1), \s2. ~(beval b s2) /\ p s2)) 2223 /\ 2224 (!s1 l v c p. 2225 v IN FDOM s1 2226 ==> 2227 ACC_SMALL_EVAL 2228 ((Local v c :: l, s1), p) 2229 ((c :: GenAssign v (Exp(s1 ' v)) :: l, s1), 2230 \s2. v IN FDOM s2 /\ p s2)) 2231 /\ 2232 (!s1 l v c p. 2233 ~(v IN FDOM s1) 2234 ==> 2235 ACC_SMALL_EVAL 2236 ((Local v c :: l, s1), p) 2237 ((c :: Dispose v :: l, s1), 2238 \s2. ~(v IN FDOM s2) /\ p s2))``, 2239 RW_TAC list_ss 2240 ([ACC_SMALL_EVAL,ACC_PRED_def,FUN_EQ_THM,IS_SOME_EXISTS] 2241 @ small_rulel) 2242 THEN RW_TAC std_ss [] 2243 THEN METIS_TAC []); 2244 2245val ACC_SMALL_EVAL_TRUE = 2246 store_thm 2247 ("ACC_SMALL_EVAL_TRUE", 2248 ``!l1 l2 s1 s2 p1 p2. 2249 ACC_SMALL_EVAL ((l1,s1),p1) ((l2,s2),p2) /\ p1 s1 ==> p2 s2``, 2250 Cases 2251 THEN RW_TAC list_ss [ACC_SMALL_EVAL] 2252 THEN METIS_TAC[SMALL_EVAL_ACC_PRED]); 2253 2254val ACC_SMALL_EVAL_SMALL_EVAL = 2255 store_thm 2256 ("ACC_SMALL_EVAL_SMALL_EVAL", 2257 ``!con1 con2 p1 p2. 2258 ACC_SMALL_EVAL (con1,p1) (con2,p2) ==> SMALL_EVAL con1 con2``, 2259 METIS_TAC[ACC_SMALL_EVAL_def]); 2260 2261val ACC_SMALL_EVAL_THM = 2262 store_thm 2263 ("ACC_SMALL_EVAL_THM", 2264 ``!l1 l2 s1 s2 p1 p2. 2265 p1 s1 2266 ==> 2267 ACC_SMALL_EVAL ((l1,s1),p1) ((l2,s2),p2) 2268 ==> 2269 SMALL_EVAL (l1,s1) (l2,s2) /\ p2 s2``, 2270 METIS_TAC[ACC_SMALL_EVAL_TRUE,ACC_SMALL_EVAL_SMALL_EVAL]); 2271 2272(*===========================================================================*) 2273(* Accumulating small step next-state function *) 2274(*===========================================================================*) 2275 2276val ACC_STEP_BIND_def = 2277 Define 2278 `ACC_STEP_BIND m f = case m of 2279 ((l, TIMEOUT s), p) -> ((l, TIMEOUT s), p) 2280 || ((l, ERROR s), p) -> ((l, ERROR s), p) 2281 || ((l, RESULT s), p) -> f((l, s), p)`; 2282 2283val _ = overload_on (">>=", ``ACC_STEP_BIND``); 2284 2285(* Monad unit function *) 2286val ACC_STEP_RETURN_def = 2287 Define 2288 `ACC_STEP_RETURN x = ((FST(FST x), RESULT(SND(FST x))), SND x)`; 2289 2290val ACC_STEP_MONAD_LAWS = 2291 store_thm 2292 ("ACC_STEP_MONAD_LAWS", 2293 ``((ACC_STEP_RETURN x) >>= f = f x) 2294 /\ 2295 (m >>= ACC_STEP_RETURN = m) 2296 /\ 2297 ((m >>= f) >>= g = m >>= (\x. (f x) >>= g))``, 2298 RW_TAC std_ss [ACC_STEP_BIND_def, ACC_STEP_RETURN_def] 2299 THEN Cases_on `m` 2300 THEN Cases_on `q` 2301 THEN Cases_on `r'` 2302 THEN RW_TAC (srw_ss()) []); 2303 2304val ACC_STEP_BIND_RESULT = 2305 store_thm 2306 ("ACC_STEP_BIND_RESULT", 2307 ``!l s p. ((l, RESULT s), p) >>= f = f((l,s),p)``, 2308 RW_TAC std_ss [ACC_STEP_BIND_def, ACC_STEP_RETURN_def]); 2309 2310(* Single step *) 2311val ACC_STEP1_def = 2312 Define 2313 `ACC_STEP1 (con, p) = 2314 (STEP1 con, 2315 if NULL(FST con) then p else ACC_PRED p (HD(FST con)) (SND con))`; 2316 2317(* Clocked accumulating next-state function *) 2318 2319val ACC_STEP_def = 2320 Define 2321 `(ACC_STEP n (([],s),p) = (([], RESULT s), p)) 2322 /\ 2323 (ACC_STEP 0 ((l,s),p) = ((l, TIMEOUT s), p)) 2324 /\ 2325 (ACC_STEP (SUC n) ((l,s),p) = ACC_STEP1 ((l,s),p) >>= ACC_STEP n)`; 2326 2327val NOT_EMPTY_EXISTS = 2328 prove 2329 (``!l. ~(l = []) = ?x l'. l = x :: l'``, 2330 Induct 2331 THEN RW_TAC list_ss []); 2332 2333val ACC_STEP = 2334 store_thm 2335 ("ACC_STEP", 2336 ``!n l s p. 2337 ACC_STEP n ((l,s),p) = 2338 if (l = []) 2339 then (([], RESULT s), p) else 2340 if (n = 0) 2341 then ((l, TIMEOUT s), p) 2342 else ACC_STEP1 ((l,s),p) >>= ACC_STEP (n-1)``, 2343 Cases 2344 THEN RW_TAC std_ss [ACC_STEP_def] 2345 THEN FULL_SIMP_TAC std_ss [NOT_EMPTY_EXISTS] 2346 THEN RW_TAC std_ss [ACC_STEP_def,ACC_STEP_BIND_def]); 2347 2348(* Add to EVAL compset *) 2349val _ = computeLib.add_persistent_funs ["ACC_STEP"]; 2350 2351val ACC_STEP_STEP = 2352 store_thm 2353 ("ACC_STEP_STEP", 2354 ``!n l s1 s2 P Q. 2355 P s1 /\ (ACC_STEP n ((l,s1),P) = (([], RESULT s2), Q)) 2356 ==> 2357 (STEP n (l,s1) = ([], RESULT s2)) /\ Q s2``, 2358 Induct 2359 THEN RW_TAC std_ss [ACC_STEP_def,STEP] 2360 THEN RW_TAC std_ss [] 2361 THEN FULL_SIMP_TAC (srw_ss()) [ACC_STEP_def,NOT_EMPTY_EXISTS] 2362 THEN RW_TAC std_ss [STEP_SUC] 2363 THEN FULL_SIMP_TAC (srw_ss()) [ACC_STEP_def,NOT_EMPTY_EXISTS] 2364 THEN RW_TAC std_ss [] 2365 THEN FULL_SIMP_TAC (srw_ss()) 2366 [ACC_STEP_def,NOT_EMPTY_EXISTS,ACC_STEP1_def,ACC_STEP_BIND_def,STEP_BIND_def] 2367 THENL 2368 [Cases_on `STEP1 (x::l',s1)` 2369 THEN FULL_SIMP_TAC (srw_ss()) [] 2370 THEN Cases_on `r` 2371 THEN FULL_SIMP_TAC (srw_ss()) [] 2372 THEN METIS_TAC[STEP1_ACC_PRED], 2373 Cases_on `l` 2374 THEN FULL_SIMP_TAC list_ss [ACC_STEP_def] 2375 THEN RW_TAC std_ss [] 2376 THEN RW_TAC std_ss [] 2377 THEN FULL_SIMP_TAC list_ss [ACC_STEP_BIND_def] 2378 THEN Cases_on `ACC_STEP1 ((h::t',s1),P)` 2379 THEN FULL_SIMP_TAC (srw_ss()) [] 2380 THEN Cases_on `q` 2381 THEN FULL_SIMP_TAC (srw_ss()) [] 2382 THEN Cases_on `r'` 2383 THEN FULL_SIMP_TAC (srw_ss()) [ACC_STEP1_def] 2384 THEN METIS_TAC[STEP1_ACC_PRED]]); 2385 2386val SPEC_ACC_STEP = 2387 store_thm 2388 ("SPEC_ACC_STEP", 2389 ``!P c R. 2390 (!s1. ?n s2. ACC_STEP n (([c],s1),P) = (([], RESULT s2), R s1)) 2391 ==> 2392 !s1 s2. P s1 /\ EVAL c s1 s2 ==> R s1 s2``, 2393 RW_TAC std_ss [EVAL_STEP] 2394 THEN `?n s2. ACC_STEP n (([c],s1),P) = (([],RESULT s2),R s1)` by METIS_TAC[] 2395 THEN IMP_RES_TAC ACC_STEP_STEP 2396 THEN `n <= n' \/ n' <= n` by DECIDE_TAC 2397 THEN IMP_RES_TAC STEP_MONO 2398 THEN `RESULT s2 = RESULT s2'` by METIS_TAC[pairTheory.PAIR_EQ] 2399 THEN FULL_SIMP_TAC (srw_ss()) []); 2400 2401(* Some miscellaneous theorems used in PATH_EVAL. sml *) 2402 2403 2404(* Rearrangement lemma used in SYMBOLIC_EVAL_PROVE *) 2405val EVAL_SPEC_THM = 2406 store_thm 2407 ("EVAL_SPEC_THM", 2408 ``!A P c Q f. 2409 (!s. A s ==> P s ==> (EVAL c s (f s) /\ (Q(f s) = T))) 2410 ==> 2411 SPEC (\s. P s /\ A s) c Q``, 2412 RW_TAC std_ss [SPEC_def] 2413 THEN RES_TAC 2414 THEN IMP_RES_TAC EVAL_DETERMINISTIC 2415 THEN RW_TAC std_ss []); 2416 2417(* |- !f x y. f |+ (x,y) = f \\ x |+ (x,y) *) 2418val FUPDATE_PRUNE_LEMMA = 2419 Q.GEN `f` 2420 (Q.GEN `x` 2421 (Q.GEN `y` 2422 (GSYM 2423 (CONV_RULE 2424 EVAL 2425 (Q.SPEC `x` (Q.SPEC `f |+ (x,y)` FUPDATE_DOMSUB)))))); 2426 2427val FUPDATE_PRUNE = 2428 store_thm 2429 ("FUPDATE_PRUNE", 2430 ``!f p. f |+ p = f \\ (FST p) |+ p``, 2431 RW_TAC std_ss [] 2432 THEN Cases_on `p` 2433 THEN RW_TAC std_ss [] 2434 THEN METIS_TAC [FUPDATE_PRUNE_LEMMA]); 2435 2436val FUPDATE_LIST_FOLD_LEMMA = 2437 store_thm 2438 ("FUPDATE_LIST_FOLD_LEMMA", 2439 ``!f p. f |+ p = f |++ [p]``, 2440 RW_TAC list_ss [FUPDATE_LIST_THM]); 2441 2442(* Ad hoc collection of theorems used in SYM_RUN *) 2443 2444val NOT_IMP_EQ_F = 2445 save_thm 2446 ("NOT_IMP_EQ_F", 2447 METIS_PROVE [] ``!t. ~t ==> (t =F)``); 2448 2449val TC_SMALL_EVAL_IF = 2450 save_thm 2451 ("TC_SMALL_EVAL_IF", 2452 METIS_PROVE [] 2453 ``!con b s1 s2. 2454 (b ==> TC SMALL_EVAL con ([],s1)) 2455 /\ 2456 (~b ==> TC SMALL_EVAL con ([],s2)) 2457 ==> 2458 TC SMALL_EVAL con ([], if b then s1 else s2)``); 2459 2460val LEFT_T_ELIM = 2461 save_thm 2462 ("LEFT_T_ELIM", 2463 METIS_PROVE [] ``!b. T /\ b = b``); 2464 2465val T_AND_T = 2466 save_thm 2467 ("T_AND_T", 2468 METIS_PROVE [] ``T /\ T = T``); 2469 2470val NOT_EQ_F = 2471 save_thm 2472 ("NOT_EQ_F", 2473 METIS_PROVE [] ``!b. ~b ==> (b = F)``); 2474 2475val NOT_EQ_T = 2476 save_thm 2477 ("NOT_EQ_T", 2478 METIS_PROVE [] ``!b. (b = T) ==> (~b = F)``); 2479 2480val ABS_T_CONJ = 2481 save_thm 2482 ("ABS_T_CONJ", 2483 METIS_PROVE [] 2484 ``!P Q (s:state). P s ==> (Q s = T) ==> (\s. P s /\ Q s) s``); 2485 2486val ABS_F_CONJ = 2487 save_thm 2488 ("ABS_F_CONJ", 2489 METIS_PROVE [] 2490 ``!P Q (s:state). P s ==> (~(Q s) = T) ==> (\s. P s /\ ~(Q s)) s``); 2491 2492val STEP1_T = 2493 save_thm 2494 ("STEP1_T", 2495 METIS_PROVE [] 2496 ``!bx b l s x y. 2497 bx ==> (bx ==> b = T) ==> (STEP1 (l,s) = if b then x else y) 2498 ==> (STEP1 (l,s) = x)``); 2499 2500val STEP1_F = 2501 save_thm 2502 ("STEP1_F", 2503 METIS_PROVE [] 2504 ``!bx b l s x y. 2505 bx ==> (bx ==> ~b = T) ==> (STEP1 (l,s) = if b then x else y) 2506 ==> (STEP1 (l,s) = y)``); 2507 2508(* Utility theorem used by CONJ_DISCH_ALL *) 2509val CONJ_DISCH_ALL_THM = 2510 save_thm 2511 ("CONJ_DISCH_ALL_THM", 2512 METIS_PROVE [] ``!t1 t2 t. t1 ==> (t2 ==> t) = t2 /\ t1 ==> t``); 2513 2514(* Utility theorem used by EVAL_IMP_INTRO *) 2515val IMP_INTRO_THM = 2516 store_thm 2517 ("IMP_INTRO_THM", 2518 ``!pre prog post. RSPEC pre prog post = IMP pre post prog``, 2519 METIS_TAC[IMP_def]); 2520 2521val NOT_CONJ_IMP_F = 2522 save_thm 2523 ("NOT_CONJ_IMP_F", 2524 METIS_PROVE [] ``!p b : bool. ~(p /\ b) ==> ((p ==> ~b) = T)``); 2525 2526(* Type annotations needed below as "~", "/\", "\/" are overloaded *) 2527val NOT_IMP_CONJ = 2528 save_thm 2529 ("NOT_IMP_CONJ", 2530 METIS_PROVE [] ``!A B C : bool . ~((A ==> B) /\ C) = (A /\ ~B) \/ ~C``); 2531 2532val CONJ_RIGHT_ASSOC = 2533 save_thm 2534 ("CONJ_RIGHT_ASSOC", 2535 METIS_PROVE [] ``!A B C : bool. A /\ (B /\ C) = A /\ B /\ C``); 2536 2537val CONJ_LEFT_ASSOC = 2538 save_thm 2539 ("CONJ_LEFT_ASSOC", 2540 METIS_PROVE [] ``!A B C : bool. (A /\ B) /\ C = A /\ B /\ C``); 2541 2542val NOT_DISJ = 2543 save_thm 2544 ("NOT_DISJ", 2545 METIS_PROVE [] ``!A B : bool. ~(A \/ B) = ~A /\ ~B``); 2546 2547val IMP_F_IS_F = 2548 save_thm 2549 ("IMP_F_IS_F", 2550 METIS_PROVE [] ``!P : bool. (!Q. P ==> Q) ==> (P = F)``); 2551 2552(* Identity wrapper to tag ILOG-generated assumptions *) 2553val ILOG_def = Define `ILOG(tm:bool) = tm`; 2554 2555(*===========================================================================*) 2556(* Program transformation/normalisation rules *) 2557(*===========================================================================*) 2558 2559(* Straight line (non-looping) programs *) 2560val STRAIGHT_def = 2561 Define 2562 `(STRAIGHT Skip = T) 2563 /\ 2564 (STRAIGHT (GenAssign v e) = T) 2565 /\ 2566 (STRAIGHT (Dispose v) = F) 2567 /\ 2568 (STRAIGHT (Seq c1 c2) = STRAIGHT c1 /\ STRAIGHT c2) 2569 /\ 2570 (STRAIGHT (Cond b c1 c2) = STRAIGHT c1 /\ STRAIGHT c2) 2571 /\ 2572 (STRAIGHT (AnWhile b R c) = F) 2573 /\ 2574 (STRAIGHT (Local v c) = F)`; 2575 2576(* RUN straight line programs *) 2577 2578(* 2579Semantics that represents states as key-value lists (key = string). If 2580kvl is such a list then the corresponding finite map is FEMPTY |++ kvl. 2581*) 2582 2583(* Update value in a key-value list *) 2584val UPDATE_LIST_def = 2585 Define 2586 `(UPDATE_LIST [] (v,x) = [(v,x)]) 2587 /\ 2588 (UPDATE_LIST ((v2,x2) :: l) (v1,x1) = 2589 if v1 = v2 then (v1,x1) :: l else (v2,x2) :: UPDATE_LIST l (v1,x1))`; 2590 2591(* 2592ZIP_LIST b [(v1,x1);...;(vn,xn)] [(v1,y1);...;(vn,yn)] = 2593 [(v1,if b then x1 else y1);...;(vn,if b then xn else yn)] 2594*) 2595 2596val ZIP_LIST_def = 2597 Define 2598 `(ZIP_LIST (b:bool) l1 [] = []) 2599 /\ 2600 (ZIP_LIST (b:bool) [] l2 = []) 2601 /\ 2602 (ZIP_LIST b ((v1,x1) :: l1) ((v2,x2) :: l2) = 2603 (v1, (if b then x1 else x2)) :: ZIP_LIST b l1 l2)`; 2604 2605val STRAIGHT_RUN_def = 2606 Define 2607 `(STRAIGHT_RUN Skip l = l) 2608 /\ 2609 (STRAIGHT_RUN (GenAssign v e) l = 2610 UPDATE_LIST l (v, naeval e (FEMPTY |++ l))) 2611 /\ 2612 (STRAIGHT_RUN (Seq c1 c2) s = STRAIGHT_RUN c2 (STRAIGHT_RUN c1 s)) 2613 /\ 2614 (STRAIGHT_RUN (Cond b c1 c2) l = 2615 ZIP_LIST (beval b (FEMPTY |++ l)) (STRAIGHT_RUN c1 l) (STRAIGHT_RUN c2 l))`; 2616 2617(* 2618val SIMPLE_RUN_def = 2619 Define 2620 `(SIMPLE_RUN Skip l = l) 2621 /\ 2622 (SIMPLE_RUN (GenAssign v e) l = 2623 UPDATE_LIST l (v, naeval e (FEMPTY |++ l))) 2624 /\ 2625 (SIMPLE_RUN (Seq c1 c2) s = SIMPLE_RUN c2 (SIMPLE_RUN c1 s)) 2626 /\ 2627 (SIMPLE_RUN (Cond b c1 c2) l = 2628 ZIP_LIST (beval b (FEMPTY |++ l)) (SIMPLE_RUN c1 l) (SIMPLE_RUN c2 l)) 2629 /\ 2630 (SIMPLE_RUN (AnWhile b R c) l = SIMPLE_RUN c <???>)`; 2631*) 2632 2633val DISTINCT_VARS_def = 2634 Define 2635 `DISTINCT_VARS l = ALL_DISTINCT(MAP FST l)`; 2636 2637val FUPDATE_LIST_FUPDATE_NOT_MEM = 2638 store_thm 2639 ("FUPDATE_LIST_FUPDATE_NOT_MEM", 2640 ``!l. ~(MEM v (MAP FST l)) /\ DISTINCT_VARS l 2641 ==> !fm x y. fm |+ (v,x) |++ l = (fm |+ (v,y) |++ l) |+ (v,x)``, 2642 Induct 2643 THEN RW_TAC std_ss [FUPDATE_LIST_THM,FUPDATE_EQ] 2644 THEN Cases_on `h` 2645 THEN FULL_SIMP_TAC list_ss 2646 [FUPDATE_LIST_THM,DISTINCT_VARS_def,listTheory.ALL_DISTINCT] 2647 THEN METIS_TAC[FUPDATE_EQ,FUPDATE_COMMUTES]); 2648 2649val UPDATE_LIST_FUPDATE = 2650 store_thm 2651 ("UPDATE_LIST_FUPDATE", 2652 ``!l. DISTINCT_VARS l 2653 ==> !fm v x. fm |++ UPDATE_LIST l (v,x) = (fm |++ l) |+ (v,x)``, 2654 Induct 2655 THEN RW_TAC std_ss [UPDATE_LIST_def,FUPDATE_LIST_THM] 2656 THEN Cases_on `h` 2657 THEN FULL_SIMP_TAC std_ss [UPDATE_LIST_def,FUPDATE_LIST_THM,listTheory.ALL_DISTINCT] 2658 THEN Cases_on `v = q` 2659 THEN FULL_SIMP_TAC list_ss 2660 [UPDATE_LIST_def,FUPDATE_LIST_THM,DISTINCT_VARS_def,listTheory.ALL_DISTINCT] 2661 THEN METIS_TAC[FUPDATE_LIST_FUPDATE_NOT_MEM,DISTINCT_VARS_def]); 2662 2663val MAP_FST_UPDATE_LIST = 2664 prove 2665 (``!l. MAP FST (UPDATE_LIST l (v,x)) = 2666 if MEM v (MAP FST l) then MAP FST l else (MAP FST l) ++ [v]``, 2667 Induct 2668 THEN RW_TAC list_ss [DISTINCT_VARS_def,listTheory.ALL_DISTINCT,UPDATE_LIST_def] 2669 THEN Cases_on `h` 2670 THEN FULL_SIMP_TAC list_ss 2671 [FUPDATE_LIST_THM,DISTINCT_VARS_def,listTheory.ALL_DISTINCT,UPDATE_LIST_def] 2672 THEN Cases_on `q = v` 2673 THEN FULL_SIMP_TAC list_ss 2674 [FUPDATE_LIST_THM,DISTINCT_VARS_def,listTheory.ALL_DISTINCT,UPDATE_LIST_def]); 2675 2676val UpdateDISTINCT = 2677 store_thm 2678 ("UpdateDISTINCT", 2679 ``!l. DISTINCT_VARS l ==> !v x. DISTINCT_VARS(UPDATE_LIST l (v,x))``, 2680 Induct 2681 THEN RW_TAC list_ss [DISTINCT_VARS_def,listTheory.ALL_DISTINCT,UPDATE_LIST_def] 2682 THEN Cases_on `h` 2683 THEN FULL_SIMP_TAC list_ss 2684 [FUPDATE_LIST_THM,DISTINCT_VARS_def,listTheory.ALL_DISTINCT,UPDATE_LIST_def] 2685 THEN Cases_on `q = v` 2686 THEN FULL_SIMP_TAC list_ss 2687 [FUPDATE_LIST_THM,DISTINCT_VARS_def,listTheory.ALL_DISTINCT, 2688 UPDATE_LIST_def,MAP_FST_UPDATE_LIST] 2689 THEN Cases_on `MEM v (MAP FST l)` 2690 THEN FULL_SIMP_TAC list_ss 2691 [FUPDATE_LIST_THM,DISTINCT_VARS_def,listTheory.ALL_DISTINCT, 2692 UPDATE_LIST_def,MAP_FST_UPDATE_LIST]); 2693 2694val MAP_FST_SUBSET_ZIP_LIST = 2695 prove 2696 (``!l1 l2 b x. MEM x (MAP FST (ZIP_LIST b l1 l2)) ==> MEM x (MAP FST l1)``, 2697 Induct 2698 THENL[ALL_TAC,GEN_TAC] 2699 THEN Induct 2700 THEN RW_TAC list_ss [DISTINCT_VARS_def,listTheory.ALL_DISTINCT,ZIP_LIST_def] 2701 THEN Cases_on `h` 2702 THEN TRY(Cases_on `h'`) 2703 THEN FULL_SIMP_TAC list_ss 2704 [FUPDATE_LIST_THM,DISTINCT_VARS_def,listTheory.ALL_DISTINCT,ZIP_LIST_def] 2705 THEN METIS_TAC[]); 2706 2707val ZIP_LIST_DISTINCT = 2708 store_thm 2709 ("ZIP_LIST_DISTINCT", 2710 ``!l1 l2. DISTINCT_VARS l1 /\ DISTINCT_VARS l2 2711 ==> !b. DISTINCT_VARS(ZIP_LIST b l1 l2)``, 2712 Induct 2713 THENL[ALL_TAC,GEN_TAC] 2714 THEN Induct 2715 THEN RW_TAC list_ss [DISTINCT_VARS_def,listTheory.ALL_DISTINCT,ZIP_LIST_def] 2716 THEN Cases_on `h` 2717 THEN TRY(Cases_on `h'`) 2718 THEN FULL_SIMP_TAC list_ss 2719 [FUPDATE_LIST_THM,DISTINCT_VARS_def,listTheory.ALL_DISTINCT,ZIP_LIST_def] 2720 THEN METIS_TAC[MAP_FST_SUBSET_ZIP_LIST]); 2721 2722val STRAIGHT_RUN_DISTINCT = 2723 store_thm 2724 ("STRAIGHT_RUN_DISTINCT", 2725 ``!c. STRAIGHT c ==> !l. DISTINCT_VARS l ==> DISTINCT_VARS(STRAIGHT_RUN c l)``, 2726 Induct 2727 THEN RW_TAC std_ss [rules,STRAIGHT_RUN_def,STRAIGHT_def] 2728 THEN TRY(Cases_on `s0`) 2729 THEN RW_TAC std_ss 2730 [SEQ_THM,IF_THM,rules,GEN_ASSIGN_THM,UpdateCases, 2731 STRAIGHT_RUN_def,UPDATE_LIST_FUPDATE,UpdateDISTINCT,ZIP_LIST_DISTINCT]); 2732 2733val ZIP_LIST_T = 2734 store_thm 2735 ("ZIP_LIST_T", 2736 ``!l1 l2. (LENGTH l1 = LENGTH l2) ==> (ZIP_LIST T l1 l2 = l1)``, 2737 Induct 2738 THENL[ALL_TAC,GEN_TAC] 2739 THEN Induct 2740 THEN RW_TAC list_ss [DISTINCT_VARS_def,listTheory.ALL_DISTINCT,ZIP_LIST_def] 2741 THEN Cases_on `h` 2742 THEN TRY(Cases_on `h'`) 2743 THEN FULL_SIMP_TAC list_ss 2744 [FUPDATE_LIST_THM,DISTINCT_VARS_def,listTheory.ALL_DISTINCT,ZIP_LIST_def]); 2745 2746val ZIP_LIST_F = 2747 store_thm 2748 ("ZIP_LIST_F", 2749 ``!l1 l2. (MAP FST l1 = MAP FST l2) ==> (ZIP_LIST F l1 l2 = l2)``, 2750 Induct 2751 THENL[ALL_TAC,GEN_TAC] 2752 THEN Induct 2753 THEN RW_TAC list_ss [DISTINCT_VARS_def,listTheory.ALL_DISTINCT,ZIP_LIST_def] 2754 THEN Cases_on `h` 2755 THEN TRY(Cases_on `h'`) 2756 THEN FULL_SIMP_TAC list_ss 2757 [FUPDATE_LIST_THM,DISTINCT_VARS_def,listTheory.ALL_DISTINCT,ZIP_LIST_def]); 2758 2759(* Vars assigned to in a program *) 2760val VARS_def = 2761 Define 2762 `(VARS Skip = {}) 2763 /\ 2764 (VARS (GenAssign v e) = {v}) 2765 /\ 2766 (VARS (Seq c1 c2) = VARS c1 UNION VARS c2) 2767 /\ 2768 (VARS (Cond b c1 c2) = VARS c1 UNION VARS c2) 2769 /\ 2770 (VARS (AnWhile b R c) = VARS c) 2771 /\ 2772 (VARS (Local v c) = v INSERT VARS c)`; 2773 2774val LIST_UNION_def = 2775 Define 2776 `(LIST_UNION [] l2 = l2) 2777 /\ 2778 (LIST_UNION (x::l1) l2 = if MEM x l2 then LIST_UNION l1 l2 else x :: LIST_UNION l1 l2)`; 2779 2780val LIST_UNION_UNION = 2781 store_thm 2782 ("LIST_UNION_UNION", 2783 ``!l1 l2. set(LIST_UNION l1 l2) = set l1 UNION set l2``, 2784 Induct 2785 THEN RW_TAC std_ss 2786 [LIST_UNION_def,listTheory.LIST_TO_SET_THM,UNION_EMPTY, 2787 INSERT_UNION,GSYM listTheory.IN_LIST_TO_SET]); 2788 2789val VARL_def = 2790 Define 2791 `(VARL Skip = []) 2792 /\ 2793 (VARL (GenAssign v e) = [v]) 2794 /\ 2795 (VARL (Seq c1 c2) = LIST_UNION (VARL c1) (VARL c2)) 2796 /\ 2797 (VARL (Cond b c1 c2) = LIST_UNION (VARL c1) (VARL c2)) 2798 /\ 2799 (VARL (AnWhile b R c) = VARL c) 2800 /\ 2801 (VARL (Local v c) = LIST_UNION [v] (VARL c))`; 2802 2803(* Simple while programs *) 2804val SIMPLE_def = 2805 Define 2806 `(SIMPLE Skip = T) 2807 /\ 2808 (SIMPLE (GenAssign v e) = T) 2809 /\ 2810 (SIMPLE (Dispose v) = F) 2811 /\ 2812 (SIMPLE (Seq c1 c2) = SIMPLE c1 /\ SIMPLE c2) 2813 /\ 2814 (SIMPLE (Cond b c1 c2) = SIMPLE c1 /\ SIMPLE c2) 2815 /\ 2816 (SIMPLE (AnWhile b R c) = SIMPLE c) 2817 /\ 2818 (SIMPLE (Local v c) = SIMPLE c)`; 2819 2820val VARS_VARL = 2821 store_thm 2822 ("VARS_VARL", 2823 ``!c. SIMPLE c ==> (VARS c = set(VARL c))``, 2824 Induct 2825 THEN RW_TAC std_ss 2826 [SIMPLE_def,VARS_def,VARL_def,listTheory.LIST_TO_SET_THM, 2827 LIST_UNION_UNION,listTheory.SET_TO_LIST_INV] 2828 THEN METIS_TAC [INSERT_SING_UNION]); 2829 2830val MAP_FST_ZIP_LIST = 2831 prove 2832 (``!l1 l2 l b. (MAP FST l1 = l) /\ (MAP FST l2 = l) ==> (MAP FST (ZIP_LIST b l1 l2) = l)``, 2833 Induct 2834 THENL[ALL_TAC,GEN_TAC] 2835 THEN Induct 2836 THEN RW_TAC list_ss [ZIP_LIST_def] 2837 THEN Cases_on `h` 2838 THEN Cases_on `h'` 2839 THEN FULL_SIMP_TAC list_ss [ZIP_LIST_def]); 2840 2841val VARS_IN_def = 2842 Define 2843 `VARS_IN c l = !v. v IN (VARS c) ==> MEM v (MAP FST l)`; 2844 2845val VARS_STRAIGHT_RUN = 2846 prove 2847 (``!c l. STRAIGHT c /\ VARS_IN c l 2848 ==> (MAP FST (STRAIGHT_RUN c l) = MAP FST l)``, 2849 Induct 2850 THEN TRY(Cases_on `s0`) 2851 THEN RW_TAC list_ss 2852 [STRAIGHT_def,VARS_def,NOT_IN_EMPTY,IN_SING,STRAIGHT_RUN_def, 2853 MAP_FST_UPDATE_LIST,IN_UNION,VARS_IN_def,MAP_FST_ZIP_LIST,VARS_IN_def]); 2854 2855val VARS_STRAIGHT_RUN_COR = 2856 prove 2857 (``!c l. STRAIGHT c /\ VARS_IN c l 2858 ==> (LENGTH(STRAIGHT_RUN c l) = LENGTH l)``, 2859 METIS_TAC[VARS_IN_def,rich_listTheory.LENGTH_MAP,VARS_STRAIGHT_RUN]); 2860 2861val STRAIGHT_RUN_EVAL = 2862 store_thm 2863 ("STRAIGHT_RUN_EVAL", 2864 ``!c l. STRAIGHT c 2865 ==> VARS_IN c l 2866 ==> DISTINCT_VARS l 2867 ==> (EVAL c (FEMPTY |++ l) (FEMPTY |++ STRAIGHT_RUN c l))``, 2868 Induct 2869 THEN RW_TAC std_ss 2870 [VARS_IN_def,STRAIGHT_def, rules, STRAIGHT_RUN_def,VARS_def,IN_UNION] 2871 THEN TRY(Cases_on `s0`) 2872 THEN RW_TAC std_ss 2873 [SEQ_THM,IF_THM,rules,GEN_ASSIGN_THM,Update_def, 2874 STRAIGHT_RUN_def,UPDATE_LIST_FUPDATE] 2875 THEN METIS_TAC 2876 [ZIP_LIST_DISTINCT,STRAIGHT_RUN_DISTINCT,ZIP_LIST_T,ZIP_LIST_F, 2877 VARS_IN_def,VARS_STRAIGHT_RUN,VARS_STRAIGHT_RUN_COR]); 2878 2879(* Continuation version of STRAIGHT_RUN *) 2880 2881val STRAIGHT_RUN_CONT_def = 2882 Define 2883 `STRAIGHT_RUN_CONT c (cont:(string#value)list->'a) l = cont(STRAIGHT_RUN c l)`; 2884 2885(* 2886val STRAIGHT_RUN_CONT = 2887 store_thm 2888 ("STRAIGHT_RUN_CONT", 2889 ``(!cont l. STRAIGHT_RUN_CONT Skip cont l = cont l) 2890 /\ 2891 (!cont l v e_or_a. 2892 STRAIGHT_RUN_CONT (GenAssign v e_or_a) cont l = 2893 cont(UPDATE_LIST l (v, naeval e_or_a (FEMPTY |++ l)))) 2894 /\ 2895 (!cont l v e. 2896 STRAIGHT_RUN_CONT (Assign v e) cont l = 2897 cont(UPDATE_LIST l (v, Scalar(neval e (FEMPTY |++ l))))) 2898 /\ 2899 (!cont l v e1 e2. 2900 STRAIGHT_RUN_CONT (ArrayAssign v e1 e2) cont l = 2901 cont(UPDATE_LIST 2902 l 2903 (v, Array(aeval (ArrUpdate (ArrVar v) e1 e2) 2904 (FEMPTY |++ l))))) 2905 /\ 2906 (!cont l c1 c2. 2907 STRAIGHT_RUN_CONT (Seq c1 c2) cont l = 2908 STRAIGHT_RUN_CONT c1 (STRAIGHT_RUN_CONT c2 cont) l) 2909 /\ 2910 (!cont l b c1 c2. 2911 STRAIGHT_RUN_CONT (Cond b c1 c2) cont l = 2912 cont(ZIP_LIST (beval b (FEMPTY |++ l)) 2913 (STRAIGHT_RUN c1 l) 2914 (STRAIGHT_RUN c2 l))) 2915 /\ 2916 (!cont l b c1 c2. 2917 (beval b (FEMPTY |++ l) = T) 2918 ==> STRAIGHT c1 ==> STRAIGHT c2 ==> VARS_IN c1 l ==> VARS_IN c2 l 2919 ==> (STRAIGHT_RUN_CONT (Cond b c1 c2) cont l = 2920 cont(STRAIGHT_RUN c1 l))) 2921 /\ 2922 (!cont l b c1 c2. 2923 (beval b (FEMPTY |++ l) = F) 2924 ==> STRAIGHT c1 ==> STRAIGHT c2 ==> VARS_IN c1 l ==> VARS_IN c2 l 2925 ==> (STRAIGHT_RUN_CONT (Cond b c1 c2) cont l = 2926 cont(STRAIGHT_RUN c2 l)))``, 2927 RW_TAC std_ss 2928 [STRAIGHT_RUN_CONT_def,STRAIGHT_RUN_def,Assign_def, 2929 ArrayAssign_def,naeval_def] 2930 THEN METIS_TAC 2931 [VARS_STRAIGHT_RUN_COR,ZIP_LIST_T,VARS_STRAIGHT_RUN,ZIP_LIST_F]); 2932*) 2933 2934val STRAIGHT_RUN_CONT = 2935 store_thm 2936 ("STRAIGHT_RUN_CONT", 2937 ``(!cont l. 2938 STRAIGHT_RUN_CONT Skip cont l = cont l) 2939 /\ 2940 (!cont l v e_or_a. 2941 STRAIGHT_RUN_CONT (GenAssign v e_or_a) cont l = 2942 cont(UPDATE_LIST l (v, naeval e_or_a (FEMPTY |++ l)))) 2943 /\ 2944 (!cont l v e. 2945 STRAIGHT_RUN_CONT (Assign v e) cont l = 2946 cont(UPDATE_LIST l (v, Scalar(neval e (FEMPTY |++ l))))) 2947 /\ 2948 (!cont l v e1 e2. 2949 STRAIGHT_RUN_CONT (ArrayAssign v e1 e2) cont l = 2950 cont(UPDATE_LIST 2951 l 2952 (v, Array(aeval (ArrUpdate (ArrVar v) e1 e2) 2953 (FEMPTY |++ l))))) 2954 /\ 2955 (!cont l c1 c2. 2956 STRAIGHT_RUN_CONT (Seq c1 c2) cont l = 2957 STRAIGHT_RUN_CONT c1 (STRAIGHT_RUN_CONT c2 cont) l) 2958 /\ 2959 (!cont l b c1 c2. 2960 STRAIGHT_RUN_CONT (Cond b c1 c2) cont l = 2961 STRAIGHT_RUN_CONT c1 2962 (\l1. STRAIGHT_RUN_CONT c2 2963 (\l2. cont(ZIP_LIST (beval b (FEMPTY |++ l)) l1 l2)) l) l) 2964 /\ 2965 (!cont l b c1 c2. 2966 (beval b (FEMPTY |++ l) = T) 2967 ==> STRAIGHT c1 ==> STRAIGHT c2 ==> VARS_IN c1 l ==> VARS_IN c2 l 2968 ==> (STRAIGHT_RUN_CONT (Cond b c1 c2) cont l = 2969 STRAIGHT_RUN_CONT c1 cont l)) 2970 /\ 2971 (!cont l b c1 c2. 2972 (beval b (FEMPTY |++ l) = F) 2973 ==> STRAIGHT c1 ==> STRAIGHT c2 ==> VARS_IN c1 l ==> VARS_IN c2 l 2974 ==> (STRAIGHT_RUN_CONT (Cond b c1 c2) cont l = 2975 STRAIGHT_RUN_CONT c2 cont l))``, 2976 RW_TAC std_ss 2977 [STRAIGHT_RUN_CONT_def,STRAIGHT_RUN_def,Assign_def, 2978 ArrayAssign_def,naeval_def] 2979 THEN METIS_TAC 2980 [VARS_STRAIGHT_RUN_COR,ZIP_LIST_T,VARS_STRAIGHT_RUN,ZIP_LIST_F]); 2981 2982(*===========================================================================*) 2983(* Define WHILE loops, give Hoare rules. *) 2984(* MJCG's modified subset of HOL/src/num/theories/whileScript.sml. *) 2985(*===========================================================================*) 2986 2987(* Monad-style binding operation *) 2988val SOME_BIND_def = 2989 Define 2990 `SOME_BIND m f = case m of 2991 SOME s -> f s 2992 || NONE -> NONE`; 2993 2994val _ = overload_on (">>=", ``SOME_BIND``); 2995 2996(* Sanity check *) 2997val SOME_MONAD_LAWS = 2998 store_thm 2999 ("SOME_MONAD_LAWS", 3000 ``((SOME x) >>= f = f x) 3001 /\ 3002 (m >>= SOME = m) 3003 /\ 3004 ((m >>= f) >>= g = m >>= (\x. (f x) >>= g))``, 3005 RW_TAC std_ss [SOME_BIND_def] 3006 THEN Cases_on `m` 3007 THEN RW_TAC (srw_ss()) []); 3008 3009 3010val SOME_FUNPOW_def = 3011 Define 3012 `(SOME_FUNPOW g 0 x = SOME x) 3013 /\ 3014 (SOME_FUNPOW g (SUC n) x = 3015 case g x of 3016 SOME y -> SOME_FUNPOW g n y 3017 || NONE -> NONE)`; 3018 3019val SOME_FUNPOW = 3020 store_thm 3021 ("SOME_FUNPOWER", 3022 ``(SOME_FUNPOW g 0 x = SOME x) 3023 /\ 3024 (SOME_FUNPOW g (SUC n) x = (g x >>= SOME_FUNPOW g n))``, 3025 METIS_TAC[SOME_BIND_def,SOME_FUNPOW_def]); 3026 3027val EXISTS_LEAST = 3028 store_thm 3029 ("EXISTS_LEAST", 3030 ``!P. (?n. P n) ==> ((LEAST n. P n) = @n. P n /\ !m. m < n ==> ~(P m))``, 3031 RW_TAC std_ss [] 3032 THEN SELECT_ELIM_TAC 3033 THEN RW_TAC std_ss [] 3034 THEN METIS_TAC [LESS_LESS_CASES,LEAST_INTRO,LEAST_EXISTS,LEAST_EXISTS_IMP]); 3035 3036val SOME_ITER_def = 3037 Define 3038 `SOME_ITER P g x = 3039 if (?n. IS_SOME(SOME_FUNPOW g n x) /\ P(THE(SOME_FUNPOW g n x))) 3040 then SOME_FUNPOW 3041 g 3042 (@n. (IS_SOME(SOME_FUNPOW g n x) /\ P(THE(SOME_FUNPOW g n x))) 3043 /\ 3044 !m. m < n ==> ~(IS_SOME(SOME_FUNPOW g m x) /\ P(THE(SOME_FUNPOW g m x)))) 3045 x 3046 else NONE`; 3047 3048val SOME_ITER = 3049 store_thm 3050 ("SOME_ITER", 3051 ``SOME_ITER P g x = 3052 if (?n. IS_SOME(SOME_FUNPOW g n x) /\ P(THE(SOME_FUNPOW g n x))) 3053 then 3054 SOME_FUNPOW g (LEAST n. IS_SOME(SOME_FUNPOW g n x) /\ P(THE(SOME_FUNPOW g n x))) x 3055 else NONE``, 3056 METIS_TAC 3057 [BETA_RULE 3058 (ISPEC 3059 ``\n:num. IS_SOME(SOME_FUNPOW g n x) /\ P(THE(SOME_FUNPOW g n x))`` 3060 EXISTS_LEAST), 3061 SOME_ITER_def]); 3062 3063 3064val SOME_ITER_REC = 3065 store_thm 3066 ("SOME_ITER_REC", 3067 ``SOME_ITER P g x = 3068 if P x then SOME x else g x >>= SOME_ITER P g``, 3069 REWRITE_TAC [SOME_ITER_def,SOME_BIND_def] 3070 THEN COND_CASES_TAC 3071 THENL 3072 [POP_ASSUM STRIP_ASSUME_TAC 3073 THEN COND_CASES_TAC 3074 THENL 3075 [SELECT_ELIM_TAC 3076 THEN CONJ_TAC 3077 THENL 3078 [Q.EXISTS_TAC `0` 3079 THEN ASM_REWRITE_TAC [SOME_FUNPOW_def, NOT_LESS_0] 3080 THEN METIS_TAC[option_CLAUSES], 3081 Q.X_GEN_TAC `m` 3082 THEN REPEAT STRIP_TAC 3083 THEN Q.SUBGOAL_THEN `m = 0` (fn th => REWRITE_TAC [th,SOME_FUNPOW_def]) 3084 THEN Q.SPEC_THEN 3085 `m` (REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC) num_CASES 3086 THEN REWRITE_TAC [] 3087 THEN FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) 3088 THEN FULL_SIMP_TAC (srw_ss()) [SOME_FUNPOW_def, LESS_0]], 3089 SELECT_ELIM_TAC 3090 THEN CONJ_TAC 3091 THENL 3092 [Q.SPEC_THEN `\n. IS_SOME(SOME_FUNPOW g n x) /\ P(THE(SOME_FUNPOW g n x))` (IMP_RES_TAC o BETA_RULE) WOP 3093 THEN METIS_TAC[], 3094 Q.X_GEN_TAC `m` 3095 THEN REPEAT STRIP_TAC 3096 THEN Q.SUBGOAL_THEN `?p. m = SUC p` (CHOOSE_THEN SUBST_ALL_TAC) 3097 THENL 3098 [Q.SPEC_THEN `m` (REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC) num_CASES 3099 THEN FULL_SIMP_TAC bool_ss [SOME_FUNPOW_def] 3100 THEN METIS_TAC [option_CLAUSES], 3101 ALL_TAC] 3102 THEN FULL_SIMP_TAC bool_ss [SOME_FUNPOW_def] 3103 THEN Cases_on `g x` 3104 THEN FULL_SIMP_TAC (srw_ss()) [SOME_FUNPOW_def] 3105 THEN Q.SUBGOAL_THEN 3106 `?n. IS_SOME(SOME_FUNPOW g n (THE(g x))) /\ P(THE(SOME_FUNPOW g n (THE(g x))))` 3107 (fn th => REWRITE_TAC [th]) 3108 THEN1 METIS_TAC [option_CLAUSES] 3109 THEN ASSUM_LIST 3110 ((Q.SPEC_THEN 3111 `SUC m` 3112 (ASSUME_TAC o GEN_ALL o SIMP_RULE bool_ss [FUNPOW,LESS_MONO_EQ])) o el 2) 3113 THEN RW_TAC std_ss [] 3114 THENL 3115 [ALL_TAC, 3116 METIS_TAC[option_CLAUSES]] 3117 THEN SELECT_ELIM_TAC 3118 THEN CONJ_TAC 3119 THENL 3120 [Q.EXISTS_TAC `p` 3121 THEN RW_TAC (srw_ss()) [] 3122 THEN ASSUM_LIST 3123 (fn thl => 3124 ASSUME_TAC 3125 (Q.GEN `n` 3126 (SIMP_RULE (srw_ss()) [el 5 thl](Q.SPECL[`g`,`n`,`x`](CONJUNCT2(SOME_FUNPOW_def)))))) 3127 THEN METIS_TAC[], 3128 Q.X_GEN_TAC `m` 3129 THEN REPEAT STRIP_TAC 3130 THEN ASSUM_LIST 3131 (fn thl => 3132 ASSUME_TAC 3133 (Q.GEN `n` 3134 (SIMP_RULE (srw_ss()) [el 7 thl](Q.SPECL[`g`,`n`,`x`](CONJUNCT2(SOME_FUNPOW_def)))))) 3135 THEN METIS_TAC [LESS_LESS_CASES,option_CLAUSES]]]], 3136 POP_ASSUM (ASSUME_TAC o SIMP_RULE bool_ss []) 3137 THEN FIRST_ASSUM (ASSUME_TAC o SIMP_RULE (srw_ss()) [SOME_FUNPOW_def] o 3138 GEN_ALL o SPEC ``SUC n``) 3139 THEN Cases_on `P x` 3140 THEN FULL_SIMP_TAC (srw_ss()) [] 3141 THEN Cases_on `g x` 3142 THEN FULL_SIMP_TAC (srw_ss()) [] 3143 THEN METIS_TAC[SOME_FUNPOW_def,option_CLAUSES]]); 3144 3145val SOME_ITER_NONE = 3146 store_thm 3147 ("SOME_ITER_NONE", 3148 ``(SOME_ITER P g x = NONE) = 3149 ~ ?n. IS_SOME(SOME_FUNPOW g n x) /\ P(THE(SOME_FUNPOW g n x))``, 3150 RW_TAC std_ss [SOME_ITER_def] 3151 THENL 3152 [SELECT_ELIM_TAC 3153 THEN RW_TAC (srw_ss()) [] 3154 THENL 3155 [Q.EXISTS_TAC `LEAST n. IS_SOME(SOME_FUNPOW g n x) /\ P(THE(SOME_FUNPOW g n x))` 3156 THEN RW_TAC (srw_ss()) [] 3157 THEN METIS_TAC 3158 [BETA_RULE 3159 (ISPEC 3160 ``\n:num. IS_SOME(SOME_FUNPOW g n x) /\ P(THE(SOME_FUNPOW g n x))`` 3161 whileTheory.LEAST_EXISTS_IMP),option_CLAUSES], 3162 RW_TAC (srw_ss()) [] 3163 THEN METIS_TAC [option_CLAUSES]], 3164 METIS_TAC[option_CLAUSES]]); 3165 3166val SOME_ITER_SOME1 = 3167 prove 3168 (``(?y. SOME_ITER P g x = SOME y) 3169 ==> 3170 ?n. IS_SOME(SOME_FUNPOW g n x) 3171 /\ 3172 P(THE(SOME_FUNPOW g n x)) 3173 /\ 3174 (SOME_ITER P g x = SOME_FUNPOW g n x)``, 3175 RW_TAC std_ss [] 3176 THEN Cases_on `?n. IS_SOME (SOME_FUNPOW g n x) /\ P (THE (SOME_FUNPOW g n x))` 3177 THEN FULL_SIMP_TAC (srw_ss()) [SOME_ITER] 3178 THEN RW_TAC (srw_ss()) [] 3179 THEN METIS_TAC 3180 [BETA_RULE 3181 (ISPEC 3182 ``\n:num. IS_SOME(SOME_FUNPOW g n x) /\ P(THE(SOME_FUNPOW g n x))`` 3183 whileTheory.LEAST_EXISTS_IMP),option_CLAUSES]); 3184 3185val SOME_ITER_SOME2 = 3186 prove 3187 (``(?n. IS_SOME(SOME_FUNPOW g n x) 3188 /\ 3189 P(THE(SOME_FUNPOW g n x)) 3190 /\ 3191 (SOME_ITER P g x = SOME_FUNPOW g n x)) 3192 ==> 3193 ?y. SOME_ITER P g x = SOME y``, 3194 RW_TAC std_ss [] 3195 THEN Induct_on `n` 3196 THEN RW_TAC (srw_ss()) [SOME_FUNPOW_def] 3197 THEN Cases_on `g x` 3198 THEN FULL_SIMP_TAC (srw_ss()) [] 3199 THEN METIS_TAC[option_CLAUSES]); 3200 3201val SOME_ITER_SOME = 3202 store_thm 3203 ("SOME_ITER_SOME", 3204 ``(?y. SOME_ITER P g x = SOME y) = 3205 ?n. IS_SOME(SOME_FUNPOW g n x) 3206 /\ 3207 P(THE(SOME_FUNPOW g n x)) 3208 /\ 3209 (SOME_ITER P g x = SOME_FUNPOW g n x)``, 3210 METIS_TAC[SOME_ITER_SOME1,SOME_ITER_SOME2]); 3211 3212val SOME_ITER_LEAST = 3213 store_thm 3214 ("SOME_ITER_LEAST", 3215 ``(?y. SOME_ITER P g x = SOME y) = 3216 (?n. IS_SOME (SOME_FUNPOW g n x) /\ P(THE(SOME_FUNPOW g n x))) 3217 /\ 3218 (SOME_ITER P g x = 3219 SOME_FUNPOW 3220 g 3221 (LEAST n. IS_SOME(SOME_FUNPOW g n x) /\ P(THE(SOME_FUNPOW g n x))) 3222 x)``, 3223 RW_TAC std_ss [SOME_ITER] 3224 THEN Q.EXISTS_TAC 3225 `THE(SOME_FUNPOW g 3226 (LEAST n. 3227 IS_SOME (SOME_FUNPOW g n x) /\ P (THE (SOME_FUNPOW g n x))) 3228 x)` 3229 THEN METIS_TAC 3230 [BETA_RULE 3231 (ISPEC 3232 ``\n:num. IS_SOME(SOME_FUNPOW g n x) /\ P(THE(SOME_FUNPOW g n x))`` 3233 LEAST_EXISTS_IMP), 3234 option_CLAUSES]); 3235 3236val SOME_WHILE_def = 3237 Define 3238 `SOME_WHILE P = SOME_ITER ($~ o P)`; 3239 3240val SOME_WHILE = 3241 store_thm 3242 ("SOME_WHILE", 3243 ``SOME_WHILE P g x = 3244 if (?n. IS_SOME(SOME_FUNPOW g n x) /\ ~P(THE(SOME_FUNPOW g n x))) 3245 then 3246 SOME_FUNPOW g (LEAST n. IS_SOME(SOME_FUNPOW g n x) /\ ~P(THE(SOME_FUNPOW g n x))) x 3247 else NONE``, 3248 RW_TAC std_ss [SOME_WHILE_def,SOME_ITER]); 3249 3250val SOME_WHILE_REC = 3251 store_thm 3252 ("SOME_WHILE_REC", 3253 ``SOME_WHILE P g x = 3254 if P x then g x >>= SOME_WHILE P g else SOME x``, 3255 RW_TAC std_ss [SOME_WHILE_def,SOME_ITER_REC] 3256 THEN METIS_TAC[]); 3257 3258val SOME_WHILE_NONE = 3259 store_thm 3260 ("SOME_WHILE_NONE", 3261 ``(SOME_WHILE P g x = NONE) = 3262 ~?n. IS_SOME(SOME_FUNPOW g n x) /\ ~P(THE(SOME_FUNPOW g n x))``, 3263 RW_TAC std_ss [SOME_WHILE_def,SOME_ITER_NONE]); 3264 3265val SOME_WHILE_NONE_CASES = 3266 store_thm 3267 ("SOME_WHILE_NONE_CASES", 3268 ``(SOME_WHILE P g x = NONE) = 3269 P x /\ ((g x = NONE) \/ ?z. (g x = SOME z) /\ (SOME_WHILE P g z = NONE))``, 3270 RW_TAC (srw_ss()) [Once SOME_WHILE_REC,SOME_BIND_def] 3271 THEN Cases_on `g x` 3272 THEN FULL_SIMP_TAC (srw_ss()) []); 3273 3274val SOME_WHILE_SOME = 3275 store_thm 3276 ("SOME_WHILE_SOME", 3277 ``(?y. SOME_WHILE P g x = SOME y) = 3278 ?n. IS_SOME(SOME_FUNPOW g n x) 3279 /\ 3280 ~P(THE(SOME_FUNPOW g n x)) 3281 /\ 3282 (SOME_WHILE P g x = SOME_FUNPOW g n x)``, 3283 RW_TAC std_ss [SOME_WHILE_def,SOME_ITER_SOME]); 3284 3285val SOME_WHILE_SOME_CASES = 3286 store_thm 3287 ("SOME_WHILE_SOME_CASES", 3288 ``(SOME_WHILE P g x = SOME y) = 3289 if P x 3290 then (?z. (g x = SOME z) /\ (SOME_WHILE P g z = SOME y)) 3291 else (x = y)``, 3292 RW_TAC (srw_ss()) [Once SOME_WHILE_REC,SOME_BIND_def] 3293 THEN Cases_on `g x` 3294 THEN FULL_SIMP_TAC (srw_ss()) []); 3295 3296val SOME_WHILE_LEAST = 3297 store_thm 3298 ("SOME_WHILE_LEAST", 3299 ``(?y. SOME_WHILE P g x = SOME y) = 3300 (?n. IS_SOME (SOME_FUNPOW g n x) /\ ~P(THE(SOME_FUNPOW g n x))) 3301 /\ 3302 (SOME_WHILE P g x = 3303 SOME_FUNPOW 3304 g 3305 (LEAST n. IS_SOME(SOME_FUNPOW g n x) /\ ~P(THE(SOME_FUNPOW g n x))) 3306 x)``, 3307 RW_TAC std_ss [SOME_WHILE_def,SOME_ITER_LEAST]); 3308 3309(* ============================================================================ 3310Denotational semantics using the built-in WHILE function for While 3311============================================================================ *) 3312 3313val EVAL_FUN_def = 3314 Define 3315 `(EVAL_FUN Skip s = SOME s) 3316 /\ 3317 (EVAL_FUN (GenAssign v e) s = SOME(Update v e s)) 3318 /\ 3319 (EVAL_FUN (Dispose v) s = SOME(s \\ v)) 3320 /\ 3321 (EVAL_FUN (Seq c1 c2) s = EVAL_FUN c1 s >>= EVAL_FUN c2) 3322 /\ 3323 (EVAL_FUN (Cond b c1 c2) s = 3324 if beval b s then EVAL_FUN c1 s else EVAL_FUN c2 s) 3325 /\ 3326 (EVAL_FUN (AnWhile b R c) s = SOME_WHILE (beval b) (EVAL_FUN c) s) 3327 /\ 3328 (EVAL_FUN (Local v c) s = 3329 if v IN FDOM s 3330 then EVAL_FUN c s >>= (\s'. SOME(s' |+ (v, (s ' v)))) 3331 else EVAL_FUN c s >>= (\s'. SOME(s' \\ v)))`; 3332 3333val EVAL_IMP_EVAL_FUN_LEMMA = 3334 prove 3335 (``!c s1 s2. 3336 EVAL c s1 s2 3337 ==> 3338 (\c s1 s2. EVAL_FUN c s1 = SOME s2) c s1 s2``, 3339 IndDefRules.RULE_TAC 3340 (IndDefRules.derive_mono_strong_induction [] (rules,induction)) 3341 THEN RW_TAC std_ss [EVAL_FUN_def,SOME_BIND_def] 3342 THENL 3343 [METIS_TAC[SOME_WHILE_REC,optionTheory.option_CLAUSES], 3344 SIMP_TAC std_ss [Once SOME_WHILE_REC] 3345 THEN RW_TAC std_ss [SOME_BIND_def]]); 3346 3347val EVAL_EVAL_FUN = 3348 store_thm 3349 ("EVAL_EVAL_FUN", 3350 ``!c s1. 3351 (?s2. EVAL c s1 s2) 3352 ==> 3353 !s2. EVAL c s1 s2 = (SOME s2 = EVAL_FUN c s1)``, 3354 RW_TAC std_ss [] 3355 THEN IMP_RES_TAC EVAL_IMP_EVAL_FUN_LEMMA 3356 THEN FULL_SIMP_TAC std_ss [] 3357 THEN METIS_TAC [EVAL_DETERMINISTIC]); 3358 3359val Least_AnWhile_LEMMA = 3360 store_thm 3361 ("Least_AnWhile_LEMMA", 3362 ``!f c. (!s1 s2. (f s1 = SOME s2) ==> EVAL c s1 s2) 3363 ==> 3364 !n b s1 s2. 3365 (IS_SOME(SOME_FUNPOW f n s1) /\ ~beval b (THE(SOME_FUNPOW f n s1))) 3366 /\ 3367 (!m. IS_SOME(SOME_FUNPOW f m s1) /\ ~beval b (THE(SOME_FUNPOW f m s1)) ==> n <= m) 3368 /\ 3369 (SOME_FUNPOW f n s1 = SOME s2) 3370 ==> 3371 EVAL (AnWhile b R c) s1 s2``, 3372 STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC 3373 THEN Induct 3374 THEN RW_TAC (srw_ss()) [SOME_FUNPOW_def] 3375 THENL 3376 [METIS_TAC[rules], 3377 Cases_on `f s1` 3378 THEN FULL_SIMP_TAC (srw_ss()) [] 3379 THEN `!m. IS_SOME (SOME_FUNPOW f m s1) /\ 3380 ~beval b (THE (SOME_FUNPOW f m s1)) ==> 3381 n <= m` by METIS_TAC[DECIDE``SUC n <= m ==> n <= m``] 3382 THEN `IS_SOME (SOME_FUNPOW f n x)` by METIS_TAC[option_CLAUSES] 3383 THEN `~beval b (THE (SOME_FUNPOW f n x))` by METIS_TAC[option_CLAUSES] 3384 THEN `(!m. IS_SOME (SOME_FUNPOW f m x) /\ 3385 ~beval b (THE (SOME_FUNPOW f m x)) ==> n <= m) 3386 ==> EVAL (AnWhile b R c) x s2` 3387 by METIS_TAC[SOME_11] 3388 THEN `!m. IS_SOME (SOME_FUNPOW f (SUC m) s1) /\ 3389 ~beval b (THE (SOME_FUNPOW f (SUC m) s1)) ==> 3390 SUC n <= SUC m` by METIS_TAC[] 3391 THEN ASSUM_LIST 3392 (fn thl => ASSUME_TAC(SIMP_RULE (srw_ss()) [el 6 thl,SOME_FUNPOW_def] (el 1 thl))) 3393 THEN METIS_TAC[rules,DECIDE ``~(1 <= 0n) /\ ~(SUC n <= 0)``,SOME_FUNPOW_def,option_CLAUSES]]); 3394 3395val LEAST_AnWhile = 3396 store_thm 3397 ("LEAST_AnWhile", 3398 ``!f c. (!s1 s2. (f s1 = SOME s2) ==> EVAL c s1 s2) 3399 ==> 3400 !b s1 s2. 3401 (?n. IS_SOME(SOME_FUNPOW f n s1) /\ ~beval b (THE(SOME_FUNPOW f n s1))) 3402 /\ 3403 (SOME_FUNPOW f 3404 (LEAST n. IS_SOME(SOME_FUNPOW f n s1) /\ ~beval b (THE(SOME_FUNPOW f n s1))) 3405 s1 = 3406 SOME s2) 3407 ==> 3408 EVAL (AnWhile b R c) s1 s2``, 3409 REPEAT STRIP_TAC 3410 THEN ASSUM_LIST 3411 (fn thl=> 3412 ASSUME_TAC 3413 (SIMP_RULE (srw_ss()) thl 3414 (Q.SPECL 3415 [`LEAST n. IS_SOME(SOME_FUNPOW f n s1) /\ ~beval b (THE (SOME_FUNPOW f n s1))`, 3416 `b`,`s1`,`s2`] 3417 (MATCH_MP Least_AnWhile_LEMMA (el 4 thl))))) 3418 THEN ASSUM_LIST 3419 (fn thl=> 3420 METIS_TAC 3421 [option_CLAUSES, 3422 (BETA_RULE 3423 (ISPECL 3424 [``\n:num. IS_SOME(SOME_FUNPOW f n s1) /\ ~beval b (THE(SOME_FUNPOW f n s1))``] 3425 (Q.GEN `P` FULL_LEAST_INTRO)))])); 3426 3427val EVAL_FUN_IMP_EVAL_LEMMA = 3428 prove 3429 (``!c s1 s2. 3430 (EVAL_FUN c s1 = SOME s2) 3431 ==> 3432 EVAL c s1 s2``, 3433 Induct 3434 THEN RW_TAC std_ss 3435 [EVAL_FUN_def,SOME_BIND_def,rules, 3436 SKIP_THM,GEN_ASSIGN_THM,DISPOSE_THM,SEQ_THM, 3437 IF_T_THM,IF_F_THM,ANWHILE_T_THM, 3438 ANWHILE_F_THM,LOCAL_THM] 3439 THEN FULL_SIMP_TAC (srw_ss()) [] 3440 THEN TRY(Cases_on `EVAL_FUN c s1` 3441 THEN FULL_SIMP_TAC (srw_ss()) [] 3442 THEN METIS_TAC[]) 3443 THEN IMP_RES_TAC SOME_WHILE_LEAST 3444 THEN METIS_TAC[LEAST_AnWhile]); 3445 3446val EVAL_FUN_EVAL = 3447 store_thm 3448 ("EVAL_FUN_EVAL", 3449 ``!c s1 s2. (EVAL_FUN c s1 = SOME s2) = EVAL c s1 s2``, 3450 METIS_TAC[EVAL_FUN_IMP_EVAL_LEMMA,EVAL_IMP_EVAL_FUN_LEMMA]); 3451 3452val EVAL_FUN = 3453 store_thm 3454 ("EVAL_FUN", 3455 ``(EVAL_FUN Skip s = SOME s) 3456 /\ 3457 (EVAL_FUN (GenAssign v e) s = SOME(Update v e s)) 3458 /\ 3459 (EVAL_FUN (Dispose v) s = SOME(s \\ v)) 3460 /\ 3461 (EVAL_FUN (Seq c1 c2) s = EVAL_FUN c1 s >>= EVAL_FUN c2) 3462 /\ 3463 (EVAL_FUN (Cond b c1 c2) s = 3464 if beval b s then EVAL_FUN c1 s else EVAL_FUN c2 s) 3465 /\ 3466 (EVAL_FUN (AnWhile b R c) s = 3467 if beval b s then EVAL_FUN c s >>= EVAL_FUN (AnWhile b R c) else SOME s) 3468 /\ 3469 (EVAL_FUN (Local v c) s = 3470 if v IN FDOM s 3471 then EVAL_FUN c s >>= (\s'. SOME(s' |+ (v, (s ' v)))) 3472 else EVAL_FUN c s >>= (\s'. SOME(s' \\ v)))``, 3473 RW_TAC std_ss [EVAL_FUN_def,SOME_WHILE_REC] 3474 THEN RW_TAC (srw_ss()) [SOME_BIND_def] 3475 THEN Cases_on `EVAL_FUN c s` 3476 THEN FULL_SIMP_TAC (srw_ss()) [] 3477 THEN METIS_TAC[EVAL_FUN_def]); 3478 3479val _ = 3480 computeLib.add_persistent_funs 3481 ["EVAL_FUN"]; 3482 3483 3484(* ============================================================================ 3485Continuation denotational semantics (may not get used) 3486============================================================================ *) 3487 3488val EVAL_CONT_def = 3489 Define 3490 `EVAL_CONT c cont s = EVAL_FUN c s >>= cont`; 3491 3492(* Usual semantic equations for continuation semantics *) 3493 3494val EVAL_CONT = (* This proof should be much easier -- maybe missing key lemmas *) 3495 store_thm 3496 ("EVAL_CONT", 3497 ``(!cont. EVAL_CONT Skip cont s = cont s) 3498 /\ 3499 (!cont. EVAL_CONT (GenAssign v e) cont s = cont(Update v e s)) 3500 /\ 3501 (!cont. EVAL_CONT (Dispose v) cont s = cont(s \\ v)) 3502 /\ 3503 (!cont. EVAL_CONT (Seq c1 c2) cont s = EVAL_CONT c1 (EVAL_CONT c2 cont) s) 3504 /\ 3505 (!cont. EVAL_CONT (Cond b c1 c2) cont s = 3506 if beval b s then EVAL_CONT c1 cont s else EVAL_CONT c2 cont s) 3507 /\ 3508 (!cont. EVAL_CONT (AnWhile b R c) cont s = 3509 if beval b s 3510 then EVAL_CONT c (EVAL_CONT (AnWhile b R c) cont) s 3511 else cont s) 3512 /\ 3513 (!cont. EVAL_CONT (Local v c) cont s = 3514 if v IN FDOM s 3515 then EVAL_CONT c (\s'. cont (s' |+ (v, (s ' v)))) s 3516 else EVAL_CONT c (\s'. cont (s' \\ v)) s)``, 3517 RW_TAC std_ss [EVAL_CONT_def,EVAL_FUN_def,SOME_MONAD_LAWS] 3518 THENL 3519 [RW_TAC std_ss [SOME_BIND_def] 3520 THEN Cases_on `EVAL_FUN c1 s` 3521 THEN FULL_SIMP_TAC (srw_ss())[] 3522 THEN Cases_on `EVAL_FUN c2 x` 3523 THEN FULL_SIMP_TAC (srw_ss())[EVAL_CONT_def,SOME_MONAD_LAWS,SOME_BIND_def], 3524 RW_TAC std_ss [SOME_BIND_def] 3525 THEN Cases_on `SOME_WHILE (beval b) (EVAL_FUN c) s` 3526 THEN FULL_SIMP_TAC (srw_ss())[EVAL_CONT_def,SOME_BIND_def] 3527 THENL 3528 [Cases_on `EVAL_FUN c s` 3529 THEN FULL_SIMP_TAC (srw_ss())[] 3530 THEN Cases_on `EVAL_FUN (AnWhile b R c) x` 3531 THEN FULL_SIMP_TAC (srw_ss())[EVAL_FUN_def] 3532 THEN `(EVAL_FUN c s = NONE) \/ 3533 ?z. (EVAL_FUN c s = SOME z) /\ (SOME_WHILE (beval b) (EVAL_FUN c) z = NONE)` 3534 by METIS_TAC[SOME_WHILE_NONE_CASES] 3535 THENL 3536 [METIS_TAC[option_CLAUSES], 3537 `x = z` by METIS_TAC[option_CLAUSES] 3538 THEN RW_TAC std_ss [] 3539 THEN METIS_TAC[option_CLAUSES]], 3540 Cases_on `EVAL_FUN c s` 3541 THEN FULL_SIMP_TAC (srw_ss())[] 3542 THENL 3543 [METIS_TAC[option_CLAUSES,SOME_WHILE_SOME_CASES], 3544 Cases_on `EVAL_FUN (AnWhile b R c) x'` 3545 THEN FULL_SIMP_TAC (srw_ss())[EVAL_FUN_def] 3546 THENL 3547 [FULL_SIMP_TAC (srw_ss())[Once SOME_WHILE_SOME_CASES], 3548 `?z. (EVAL_FUN c s = SOME z) /\ (SOME_WHILE (beval b) (EVAL_FUN c) z = SOME x)` 3549 by METIS_TAC[SOME_WHILE_SOME_CASES] 3550 THEN METIS_TAC[option_CLAUSES]]]], 3551 RW_TAC std_ss [SOME_BIND_def] 3552 THEN Cases_on `SOME_WHILE (beval b) (EVAL_FUN c) s` 3553 THEN FULL_SIMP_TAC (srw_ss())[] 3554 THENL 3555 [METIS_TAC[SOME_WHILE_NONE_CASES], 3556 METIS_TAC[SOME_WHILE_SOME_CASES]]]); 3557 3558(* Strongest liberal postcondition *) 3559 3560val SP_def = 3561 Define 3562 `SP P c = \s'. ?s. P s /\ (SOME s' = EVAL_FUN c s)`; 3563 3564val SP = 3565 store_thm 3566 ("SP", 3567 ``SPEC P c (SP P c) /\ !Q. SPEC P c Q ==> !s. SP P c s ==> Q s``, 3568 METIS_TAC[SPEC_def,SP_def,EVAL_FUN_EVAL]); 3569 3570 3571val SP_SPEC = 3572 store_thm 3573 ("SP_SPEC", 3574 ``SPEC P c Q = !s. SP P c s ==> Q s``, 3575 METIS_TAC [SPEC_def,SP_def,EVAL_FUN_EVAL]); 3576 3577val RSPEC_SP = 3578 store_thm 3579 ("RSPEC_SP", 3580 ``(!P c. RSPEC P c (\s1 s2. SP (\s. (s = s1) /\ P s1) c s2)) 3581 /\ 3582 (!P c R. RSPEC P c R = !s1 s2. SP (\s. (s = s1) /\ P s1) c s2 ==> R s1 s2)``, 3583 RW_TAC std_ss [RSPEC_def,SP_def] 3584 THEN METIS_TAC[EVAL_FUN_EVAL]); 3585 3586val SKIP_SP = 3587 store_thm 3588 ("SKIP_SP", 3589 ``SP P Skip = P``, 3590 CONV_TAC FUN_EQ_CONV 3591 THEN CONV_TAC EVAL 3592 THEN METIS_TAC[]); 3593 3594val SKIP_SP_EX = 3595 store_thm 3596 ("SKIP_SP_EX", 3597 ``!s0 P. 3598 SP (\s. (s = s0) /\ P s0) Skip = \s'. (s' = s0) /\ P s0``, 3599 RW_TAC std_ss [SKIP_SP] 3600 THEN METIS_TAC[]); 3601 3602val GEN_ASSIGN_SP = 3603 store_thm 3604 ("GEN_ASSIGN_SP", 3605 ``SP P (GenAssign v e) = \s'. ?s. P s /\ (s' = Update v e s)``, 3606 CONV_TAC EVAL 3607 THEN METIS_TAC[SUBSET_DEF]); 3608 3609val GEN_ASSIGN_SP_EX = 3610 store_thm 3611 ("GEN_ASSIGN_SP_EX", 3612 ``!s0 P v e. 3613 SP (\s. (s = s0) /\ P s0) (GenAssign v e) = 3614 \s'. (s' = Update v e s0) /\ P s0``, 3615 RW_TAC std_ss [GEN_ASSIGN_SP] 3616 THEN METIS_TAC[]); 3617 3618val ASSIGN_SP_EX = 3619 store_thm 3620 ("ASSIGN_SP_EX", 3621 ``!s0 P v e. 3622 SP (\s. (s = s0) /\ P s0) (Assign v e) = 3623 \s'. (s' = s0 |+ (v, Scalar (neval e s0))) /\ P s0``, 3624 RW_TAC std_ss [GEN_ASSIGN_SP,Assign_def,UpdateCases] 3625 THEN METIS_TAC[]); 3626 3627val ARRAY_ASSIGN_SP_EX = 3628 store_thm 3629 ("ARRAY_ASSIGN_SP_EX", 3630 ``!s0 P v e1 e2. 3631 SP (\s. (s = s0) /\ P s0) (ArrayAssign v e1 e2) = 3632 \s'. (s' = s0 |+ (v, Array (aeval (ArrUpdate (ArrVar v) e1 e2) s0))) /\ P s0``, 3633 RW_TAC std_ss [GEN_ASSIGN_SP,ArrayAssign_def,UpdateCases] 3634 THEN METIS_TAC[]); 3635 3636val DISPOSE_SP = 3637 store_thm 3638 ("DISPOSE_SP", 3639 ``SP P (Dispose v) = \s'. ?s. P s /\ (s' = s \\ v)``, 3640 CONV_TAC EVAL 3641 THEN METIS_TAC[SUBSET_DEF]); 3642 3643val DISPOSE_SP_EX = 3644 store_thm 3645 ("DISPOSE_SP_EX", 3646 ``!s0 P v. 3647 SP (\s. (s = s0) /\ P s0) (Dispose v) = 3648 \s'. (s' = s0 \\ v) /\ P s0``, 3649 RW_TAC std_ss [DISPOSE_SP] 3650 THEN METIS_TAC[]); 3651 3652val SEQ_SP = 3653 store_thm 3654 ("SEQ_SP", 3655 ``SP P (Seq c1 c2) = SP (SP P c1) c2``, 3656 CONV_TAC FUN_EQ_CONV 3657 THEN CONV_TAC EVAL 3658 THEN METIS_TAC[option_CLAUSES]); 3659 3660val IF_SP = 3661 store_thm 3662 ("IF_SP", 3663 ``SP P (Cond b c1 c2) = 3664 \s'. SP (\s. P s /\ beval b s) c1 s' \/ SP (\s. P s /\ ~(beval b s)) c2 s'``, 3665 CONV_TAC FUN_EQ_CONV 3666 THEN CONV_TAC EVAL 3667 THEN METIS_TAC[option_CLAUSES]); 3668 3669val IF_SP_EX = 3670 store_thm 3671 ("IF_SP_EX", 3672 ``!s0 P b c1 c2. 3673 SP (\s. (s = s0) /\ P s0) (Cond b c1 c2) = 3674 \s'. SP (\s. (s = s0) /\ (P s0 /\ beval b s0)) c1 s' \/ 3675 SP (\s. (s = s0) /\ (P s0 /\ ~beval b s0)) c2 s'``, 3676 RW_TAC std_ss 3677 [IF_SP, 3678 METIS_PROVE [] 3679 ``(\s. ((s = s0) /\ P s0) /\ beval b s) = (\s. (s = s0) /\ P s0 /\ beval b s0)``, 3680 METIS_PROVE [] 3681 ``(\s. ((s = s0) /\ P s0) /\ ~beval b s) = (\s. (s = s0) /\ P s0 /\ ~beval b s0)``]); 3682 3683val ANWHILE_SP = 3684 store_thm 3685 ("ANWHILE_SP", 3686 ``SP P (AnWhile b n c) = 3687 \s'. SP (SP (\s. P s /\ beval b s) c) (AnWhile b n c) s' \/ (P s' /\ ~(beval b s'))``, 3688 CONV_TAC FUN_EQ_CONV 3689 THEN RW_TAC std_ss [SP_def,EVAL_FUN_def] 3690 THEN EQ_TAC 3691 THEN RW_TAC std_ss [] 3692 THENL 3693 [Cases_on `P f /\ ~beval b f` 3694 THEN FULL_SIMP_TAC (srw_ss()) [] 3695 THEN FULL_SIMP_TAC (srw_ss()) [Once SOME_WHILE_SOME_CASES] 3696 THEN Cases_on `beval b s` 3697 THEN FULL_SIMP_TAC (srw_ss()) [] 3698 THEN RW_TAC std_ss [] 3699 THEN FULL_SIMP_TAC (srw_ss()) [] 3700 THEN Q.EXISTS_TAC `z` 3701 THEN RW_TAC std_ss [] 3702 THENL 3703 [METIS_TAC[], 3704 CONV_TAC(RHS_CONV(SIMP_CONV (srw_ss()) [Once SOME_WHILE_REC,SOME_BIND_def])) 3705 THEN Cases_on `beval b z` 3706 THEN FULL_SIMP_TAC (srw_ss()) [] 3707 THEN ONCE_REWRITE_TAC[SOME_WHILE_SOME_CASES] 3708 THEN RW_TAC (srw_ss()) [] 3709 THEN ONCE_REWRITE_TAC[SOME_WHILE_SOME_CASES] 3710 THEN RW_TAC (srw_ss()) [], 3711 METIS_TAC[], 3712 CONV_TAC(RHS_CONV(SIMP_CONV (srw_ss()) [Once SOME_WHILE_REC,SOME_BIND_def])) 3713 THEN Cases_on `beval b z` 3714 THEN FULL_SIMP_TAC (srw_ss()) [] 3715 THEN ONCE_REWRITE_TAC[SOME_WHILE_SOME_CASES] 3716 THEN RW_TAC (srw_ss()) [] 3717 THEN ONCE_REWRITE_TAC[SOME_WHILE_SOME_CASES] 3718 THEN RW_TAC (srw_ss()) []], 3719 Q.EXISTS_TAC `s''` 3720 THEN RW_TAC std_ss [] 3721 THEN CONV_TAC(RHS_CONV(SIMP_CONV (srw_ss()) [Once SOME_WHILE_REC,SOME_BIND_def])) 3722 THEN RW_TAC std_ss [] 3723 THEN Cases_on `EVAL_FUN c s''` 3724 THEN FULL_SIMP_TAC (srw_ss()) [], 3725 Q.EXISTS_TAC `f` 3726 THEN RW_TAC std_ss [] 3727 THEN CONV_TAC(RHS_CONV(SIMP_CONV (srw_ss()) [Once SOME_WHILE_REC,SOME_BIND_def])) 3728 THEN RW_TAC (srw_ss()) []]); 3729 3730val WHILE_SP_EX = 3731 store_thm 3732 ("WHILE_SP_EX", 3733 ``!s0 P b R c. 3734 SP (\s. (s = s0) /\ P s0) (AnWhile b R c) = 3735 \s'. SP (SP (\s. (s = s0) /\ (P s0 /\ beval b s0)) c) (AnWhile b R c) s' 3736 \/ 3737 ((s' = s0) /\ (P s0 /\ ~beval b s0))``, 3738 RW_TAC std_ss 3739 [Once ANWHILE_SP, 3740 METIS_PROVE [] 3741 ``(\s. ((s = s0) /\ P s0) /\ beval b s) = (\s. (s = s0) /\ P s0 /\ beval b s0)``] 3742 THEN METIS_TAC[]); 3743 3744val LOCAL_SP = 3745 store_thm 3746 ("LOCAL_SP", 3747 ``SP P (Local v c) = 3748 \s''. (?s' x. SP (\s. P s /\ v IN FDOM s /\ (s ' v = x)) c s' /\ (s'' = s' |+ (v,x))) 3749 \/ 3750 (?s'. SP (\s. P s /\ ~(v IN FDOM s)) c s' /\ (s'' = s' \\ v))``, 3751 CONV_TAC(FUN_EQ_CONV THENC EVAL) 3752 THEN RW_TAC (srw_ss()) [] 3753 THEN EQ_TAC 3754 THEN RW_TAC (srw_ss()) [] 3755 THENL 3756 [Cases_on 3757 `?s'. (?s. (P s /\ ~(v IN FDOM s)) /\ (SOME s' = EVAL_FUN c s)) /\ 3758 (f = s' \\ v)` 3759 THEN ASM_REWRITE_TAC[] 3760 THEN FULL_SIMP_TAC std_ss [] 3761 THEN RW_TAC std_ss [] 3762 THEN Cases_on `v IN FDOM s` 3763 THEN FULL_SIMP_TAC (srw_ss()) [] 3764 THEN Cases_on `EVAL_FUN c s` 3765 THEN FULL_SIMP_TAC (srw_ss()) [] 3766 THEN METIS_TAC[], 3767 Q.EXISTS_TAC `s` 3768 THEN ASM_REWRITE_TAC[] 3769 THEN METIS_TAC[option_CLAUSES], 3770 Q.EXISTS_TAC `s` 3771 THEN ASM_REWRITE_TAC[] 3772 THEN METIS_TAC[option_CLAUSES]]); 3773 3774val LOCAL_SP_EX = 3775 store_thm 3776 ("LOCAL_SP_EX", 3777 ``!mkstate x P v c. 3778 SP (\s. (s = s0) /\ P s0) (Local v c) = 3779 \s''. (?s'. SP(\s. (s = s0) /\ (P s0 /\ v IN FDOM s)) c s' 3780 /\ (s'' = s' |+ (v,(s0 ' v)))) 3781 \/ 3782 (?s'. SP (\s. (s = s0) /\ (P s0 /\ ~(v IN FDOM s))) c s' 3783 /\ (s'' = s' \\ v))``, 3784 RW_TAC std_ss [LOCAL_SP] 3785 THEN CONV_TAC FUN_EQ_CONV 3786 THEN FULL_SIMP_TAC std_ss [SP_def] 3787 THEN METIS_TAC[]); 3788 3789(* Weakest liberal precondition *) 3790 3791val WLP_def = 3792 Define 3793 `WLP c Q = \s. !s'. (EVAL_FUN c s = SOME s') ==> Q s'`; 3794 3795val WLP = 3796 store_thm 3797 ("WLP", 3798 ``SPEC (WLP c Q) c Q /\ !P. SPEC P c Q ==> !s. P s ==> WLP c Q s``, 3799 METIS_TAC [SPEC_def,WLP_def,EVAL_FUN_EVAL]); 3800 3801val WLP_SPEC = 3802 store_thm 3803 ("WLP_SPEC", 3804 ``SPEC P c Q = !s. P s ==> WLP c Q s``, 3805 METIS_TAC [SPEC_def,WLP_def,EVAL_FUN_EVAL]); 3806 3807val RSPEC_WLP = 3808 store_thm 3809 ("RSPEC_WLP", 3810 ``(!P c. RSPEC (\s. WLP c (R s) s) c R) 3811 /\ 3812 (!P c R. RSPEC P c R = !s. P s ==> WLP c (R s) s)``, 3813 RW_TAC std_ss [RSPEC_def,WLP_def,EVAL_FUN_EVAL] 3814 THEN METIS_TAC[EVAL_FUN_EVAL]); 3815 3816val SKIP_WLP = 3817 store_thm 3818 ("SKIP_WLP", 3819 ``WLP Skip Q = Q``, 3820 CONV_TAC FUN_EQ_CONV 3821 THEN CONV_TAC EVAL 3822 THEN METIS_TAC[]); 3823 3824val GEN_ASSIGN_WLP = 3825 store_thm 3826 ("GEN_ASSIGN_WLP", 3827 ``WLP (GenAssign v e) Q = \s. Q(Update v e s)``, 3828 CONV_TAC EVAL 3829 THEN RW_TAC std_ss [SUBSET_DEF]); 3830 3831val DISPOSE_WLP = 3832 store_thm 3833 ("DISPOSE_WLP", 3834 ``WLP (Dispose v) Q = \s. Q(s \\ v)``, 3835 CONV_TAC EVAL 3836 THEN RW_TAC std_ss [SUBSET_DEF]); 3837 3838val SEQ_WLP = 3839 store_thm 3840 ("SEQ_WLP", 3841 ``WLP (Seq c1 c2) Q = WLP c1 (WLP c2 Q)``, 3842 CONV_TAC FUN_EQ_CONV 3843 THEN CONV_TAC EVAL 3844 THEN METIS_TAC[option_CLAUSES]); 3845 3846val IF_WLP = 3847 store_thm 3848 ("IF_WLP", 3849 ``WLP (Cond b c1 c2) Q = \s. if beval b s then WLP c1 Q s else WLP c2 Q s``, 3850 CONV_TAC FUN_EQ_CONV 3851 THEN CONV_TAC EVAL 3852 THEN METIS_TAC[option_CLAUSES]); 3853 3854val ANWHILE_WLP = 3855 store_thm 3856 ("ANWHILE_WLP", 3857 ``WLP (AnWhile b R c) Q = \s. if beval b s then WLP c (WLP (AnWhile b R c) Q) s else Q s``, 3858 CONV_TAC FUN_EQ_CONV 3859 THEN RW_TAC std_ss [WLP_def,EVAL_FUN_def,SOME_BIND_def] 3860 THEN EQ_TAC 3861 THEN RW_TAC std_ss [] 3862 THEN METIS_TAC[SOME_WHILE_SOME_CASES,SOME_WHILE_NONE_CASES,option_CASES]); 3863 3864val LOCAL_WLP = 3865 store_thm 3866 ("LOCAL_WLP", 3867 ``WLP (Local v c) Q = 3868 \s. if v IN FDOM s 3869 then WLP c (\s'. Q(s' |+ (v, s ' v))) s 3870 else WLP c (\s'. Q(s' \\ v)) s``, 3871 CONV_TAC FUN_EQ_CONV 3872 THEN RW_TAC std_ss [WLP_def,EVAL_FUN_def,SOME_BIND_def] 3873 THEN EQ_TAC 3874 THEN RW_TAC std_ss [] 3875 THEN Cases_on `EVAL_FUN c f` 3876 THEN FULL_SIMP_TAC (srw_ss()) []); 3877 3878val LocP_def = 3879 Define 3880 `LocP (v:string) (P:(state->bool)->(state->bool)) (Q:state->bool) = 3881 \s:state. 3882 if v IN FDOM s 3883 then P (\s'. Q(s' |+ (v, s ' v))) s 3884 else P (\s'. Q(s' \\ v)) s`; 3885 3886val WVC_def = 3887 Define 3888 `(WVC(Skip, Q) = (Q, \s. T)) 3889 /\ 3890 (WVC(GenAssign v e, Q) = ((\s. Q(Update v e s)), \s. T)) 3891 /\ 3892 (WVC(Dispose v, Q) = ((\s. Q(s \\ v)), \s. T)) 3893 /\ 3894 (WVC(Seq c1 c2, Q) = 3895 ((\s. FST (WVC(c1, FST(WVC(c2, Q)))) s), 3896 \s. SND (WVC(c1, FST(WVC(c2, Q)))) s /\ SND (WVC(c2, Q)) s)) 3897 /\ 3898 (WVC(Cond b c1 c2, Q) = 3899 ((\s. (beval b s /\ FST(WVC(c1,Q)) s) 3900 \/ 3901 (~(beval b s) /\ FST(WVC(c2,Q)) s)), 3902 \s. SND (WVC(c1,Q)) s /\ SND (WVC(c2,Q)) s)) 3903 /\ 3904 (WVC(AnWhile b n c, Q) = 3905 ((\s. int_gt (neval n s) 0i), 3906 \s. (int_gt (neval n s) 0i /\ ~(beval b s) ==> Q s) /\ 3907 (int_gt (neval n s) 0i /\ beval b s ==> FST (WVC(c,\s. int_gt (neval n s) 0i)) s) /\ 3908 SND (WVC(c,\s. int_gt (neval n s) 0i)) s)) 3909 /\ 3910 (WVC(Local v c, Q) = 3911 ((\s. if v IN FDOM s 3912 then FST (WVC(c, \s'. Q (s' |+ (v,s ' v)))) s 3913 else FST (WVC(c, \s'. Q (s' \\ v))) s), 3914 \s. (SND (WVC(c,Q)) s) /\ INDEPENDENT Q v))`; 3915 3916val AWLP_def = Define `AWLP c Q = FST(WVC(c, Q))`; 3917 3918val AWLP = 3919 store_thm 3920 ("AWLP", 3921 ``(AWLP Skip Q = Q) 3922 /\ 3923 (AWLP (GenAssign v e) Q = \s. Q(Update v e s)) 3924 /\ 3925 (AWLP (Dispose v) Q = \s. Q(s \\ v)) 3926 /\ 3927 (AWLP (Seq c1 c2) Q = AWLP c1 (AWLP c2 Q)) 3928 /\ 3929 (AWLP (Cond b c1 c2) Q = 3930 \s. (beval b s /\ AWLP c1 Q s) \/ (~(beval b s) /\ AWLP c2 Q s)) 3931 /\ 3932 (AWLP (AnWhile b n c) Q = \s. int_gt (neval n s) 0i) 3933 /\ 3934 (AWLP (Local v c) Q = 3935 \s. if v IN FDOM s 3936 then AWLP c (\s'. Q (s' |+ (v,s ' v))) s 3937 else AWLP c (\s'. Q (s' \\ v)) s)``, 3938 RW_TAC std_ss [AWLP_def,WVC_def] 3939 THEN CONV_TAC (X_FUN_EQ_CONV ``s:state``) 3940 THEN RW_TAC std_ss []); 3941 3942val WLVC_def = Define `WLVC c Q = !s. SND(WVC(c, Q)) s`; 3943 3944val WLVC = 3945 store_thm 3946 ("WLVC", 3947 ``(WLVC Skip Q = T) 3948 /\ 3949 (WLVC (GenAssign v e) Q = T) 3950 /\ 3951 (WLVC (Dispose v) Q = T) 3952 /\ 3953 (WLVC (Seq c1 c2) Q = WLVC c1 (AWLP c2 Q) /\ WLVC c2 Q) 3954 /\ 3955 (WLVC (Cond b c1 c2) Q = WLVC c1 Q /\ WLVC c2 Q) 3956 /\ 3957 (WLVC (AnWhile b n c) Q = 3958 (!s. int_gt (neval n s) 0i /\ ~(beval b s) ==> Q s) /\ 3959 (!s. int_gt (neval n s) 0i /\ beval b s ==> AWLP c (\s. int_gt (neval n s) 0i) s) /\ 3960 WLVC c (\s. int_gt (neval n s) 0i)) 3961 /\ 3962 (WLVC (Local v c) Q = WLVC c Q /\ INDEPENDENT Q v)``, 3963 RW_TAC std_ss [AWLP_def,WLVC_def,WVC_def] 3964 THEN METIS_TAC[]); 3965 3966(*---------------------------------------------------------------------------*) 3967(* A derived While rule *) 3968(*---------------------------------------------------------------------------*) 3969 3970val VALID_def = 3971 Define 3972 `VALID p = !(s:state). p s`; 3973 3974val _= overload_on("|=", ``VALID``); 3975 3976val PRE_DERIVED_ANWHILE_RULE = 3977 store_thm 3978 ("PRE_DERIVED_ANWHILE_RULE", 3979 ``!P n Q S b c. 3980 (|= \s. P s ==> int_gt (neval n s) 0i) 3981 /\ 3982 (|= \s. int_gt (neval n s) 0i /\ beval b s ==> S s) 3983 /\ 3984 SPEC S c (\s. int_gt (neval n s) 0i) 3985 /\ 3986 (|= \s. int_gt (neval n s) 0i /\ ~(beval b s) ==> Q s) 3987 ==> 3988 SPEC P (AnWhile b n c) Q``, 3989 RW_TAC std_ss [SPEC_def,VALID_def] 3990 THEN `!s1 s2. (int_gt (neval n s1) 0i /\ beval b s1) /\ EVAL c s1 s2 ==> int_gt (neval n s2) 0i` 3991 by METIS_TAC[] 3992 THEN IMP_RES_TAC (BETA_RULE (Q.SPEC `\s. int_gt (neval n s) 0i` (SIMP_RULE std_ss [SPEC_def] ANWHILE_RULE))) 3993 THEN METIS_TAC[]); 3994 3995val INDEPENDENT_FUPDATE = 3996 store_thm 3997 ("INDEPENDENT_FUPDATE", 3998 ``!Q v. INDEPENDENT Q v ==> !s e. Q(s |+ (v,e)) = Q s``, 3999 METIS_TAC[INDEPENDENT_def,FUPDATE_EQ,DOMSUB_FUPDATE]); 4000 4001val INDEPENDENT_FUPDATE_ABS = 4002 store_thm 4003 ("INDEPENDENT_FUPDATE_ABS", 4004 ``!Q v. INDEPENDENT Q v 4005 ==> ((\s. Q(s |+ (v,e))) = Q) /\ ((\s. Q(s \\ v)) = Q)``, 4006 RW_TAC std_ss [] 4007 THEN CONV_TAC FUN_EQ_CONV 4008 THEN RW_TAC std_ss [] 4009 THEN METIS_TAC[INDEPENDENT_def,FUPDATE_EQ,DOMSUB_FUPDATE]); 4010 4011(* Simpler and faster than FULL_SIMP_TAC *) 4012fun FULL_REWRITE_TAC thl = 4013 ASSUM_LIST(fn thl => MAP_EVERY UNDISCH_TAC (map concl thl)) 4014 THEN REWRITE_TAC thl 4015 THEN REPEAT STRIP_TAC; 4016 4017(* Weirdly long rewriting times with FULL_SIMP_TAC instead of FULL_REWRITE_TAC *) 4018val WVC = 4019 time store_thm 4020 ("WVC", 4021 ``!c Q. VALID (SND (WVC(c, Q))) ==> SPEC (FST (WVC(c,Q))) c Q``, 4022 Induct 4023 THENL 4024 [SIMP_TAC std_ss 4025 [SPEC_def,VALID_def,WVC_def,SKIP_THM], 4026 SIMP_TAC std_ss 4027 [SPEC_def,VALID_def,WVC_def,GEN_ASSIGN_THM], 4028 SIMP_TAC std_ss 4029 [SPEC_def,VALID_def,WVC_def,DISPOSE_THM], 4030 FULL_REWRITE_TAC 4031 [SPEC_def,VALID_def,WVC_def,SEQ_THM] 4032 THEN METIS_TAC[], 4033 FULL_REWRITE_TAC 4034 [SPEC_def,VALID_def,WVC_def,IF_THM] 4035 THEN METIS_TAC[], 4036 FULL_REWRITE_TAC [WVC_def,VALID_def] 4037 THEN RW_TAC std_ss [] 4038 THEN `SPEC (FST (WVC (c,(\s. int_gt (neval n s) 0i)))) c (\s. int_gt (neval n s) 0i)` by METIS_TAC[] 4039 THEN IMP_RES_TAC(SIMP_RULE std_ss [VALID_def]PRE_DERIVED_ANWHILE_RULE) 4040 THEN POP_ASSUM (MATCH_MP_TAC o CONV_RULE (REDEPTH_CONV (RIGHT_IMP_FORALL_CONV ORELSEC (REWR_CONV AND_IMP_INTRO)))) 4041 THEN METIS_TAC[], 4042 FULL_REWRITE_TAC 4043 [SPEC_def,VALID_def,WVC_def,LOCAL_THM] 4044 THEN Cases_on `s IN FDOM s1` 4045 THEN FULL_SIMP_TAC std_ss [] 4046 THEN RW_TAC std_ss [] 4047 THEN `INDEPENDENT Q s` by METIS_TAC[] 4048 THENL 4049 [`(\s'. Q (s' |+ (s,s1 ' s))) = Q` by METIS_TAC[INDEPENDENT_FUPDATE_ABS] 4050 THEN ASSUM_LIST(fn thl => ASSUME_TAC(SIMP_RULE std_ss [el 1 thl](el 5 thl))) 4051 THEN `Q (s3 |+ (s,s1 ' s)) = Q s3` by METIS_TAC[INDEPENDENT_FUPDATE] 4052 THEN RW_TAC std_ss [] 4053 THEN METIS_TAC[], 4054 `(\s'. Q (s' \\ s)) = Q` by METIS_TAC[INDEPENDENT_FUPDATE_ABS] 4055 THEN ASSUM_LIST(fn thl => ASSUME_TAC(SIMP_RULE std_ss [el 1 thl](el 5 thl))) 4056 THEN `Q (s3 \\ s) = Q s3` by METIS_TAC[INDEPENDENT_FUPDATE] 4057 THEN RW_TAC std_ss [] 4058 THEN METIS_TAC[]]]); 4059 4060val WVLC_AWLP_SPEC = 4061 time store_thm 4062 ("WVLC_AWLP_SPEC", 4063 ``!c Q. WLVC c Q ==> SPEC (AWLP c Q) c Q``, 4064 RW_TAC std_ss [AWLP_def,WLVC_def,WVC_def,REWRITE_RULE [VALID_def] WVC]); 4065 4066(* Haven't figured out how to handle Local, so temporarily not handling it *) 4067val LocalFree_def = 4068 Define 4069 `(LocalFree Skip = T) 4070 /\ 4071 (LocalFree (GenAssign v e) = T) 4072 /\ 4073 (LocalFree (Dispose v) = T) 4074 /\ 4075 (LocalFree (Seq c1 c2) = LocalFree c1 /\ LocalFree c2) 4076 /\ 4077 (LocalFree (Cond b c1 c2) = LocalFree c1 /\ LocalFree c2) 4078 /\ 4079 (LocalFree (AnWhile b R c) = LocalFree c) 4080 /\ 4081 (LocalFree (Local v c) = F)`; 4082 4083(* Old version 4084val ASP_SVC_def = 4085 Define 4086 `(ASP_SVC(P, Skip)= (P, \s. T)) 4087 /\ 4088 (ASP_SVC(P, GenAssign v e) = 4089 ((\s'. ?s. P s /\ (s' = Update v e s)), \s. T)) 4090 /\ 4091 (ASP_SVC(P, Dispose v) = 4092 ((\s'. ?s. P s /\ (s' = s \\ v)), \s. T)) 4093 /\ 4094 (ASP_SVC(P, Seq c1 c2) = 4095 (FST(ASP_SVC(FST(ASP_SVC(P, c1)), c2)), 4096 \s. SND (ASP_SVC(P, c1)) s /\ SND (ASP_SVC(FST(ASP_SVC(P, c1)), c2)) s)) 4097 /\ 4098 (ASP_SVC(P, Cond b c1 c2) = 4099 ((\s'. FST (ASP_SVC((\s. P s /\ beval b s), c1)) s' 4100 \/ 4101 FST (ASP_SVC((\s. P s /\ ~(beval b s)), c2)) s'), 4102 \s'. SND (ASP_SVC((\s. P s /\ beval b s),c1)) s' 4103 /\ 4104 SND (ASP_SVC((\s. P s /\ ~(beval b s)),c2)) s')) 4105 /\ 4106 (ASP_SVC(P, AnWhile b R c) = 4107 ((\s. R s /\ ~(beval b s)), 4108 \s. (P s ==> R s) /\ 4109 (FST(ASP_SVC ((\s. R s /\ beval b s),c)) s ==> R s) /\ 4110 (SND(ASP_SVC ((\s. R s /\ beval b s),c)) s)))`; 4111*) 4112 4113 4114(*---------------------------------------------------------------------------*) 4115(* Another derived While rule *) 4116(*---------------------------------------------------------------------------*) 4117 4118val POST_DERIVED_ANWHILE_RULE = 4119 store_thm 4120 ("POST_DERIVED_ANWHILE_RULE", 4121 ``!P Q n b c. 4122 (|= \s. P s ==> int_gt (neval n s) 0i) 4123 /\ 4124 (|= \s. Q s ==> int_gt (neval n s) 0i) 4125 /\ 4126 SPEC (\s. int_gt (neval n s) 0i /\ beval b s) c Q 4127 ==> 4128 SPEC P (AnWhile b n c) (\s. int_gt (neval n s) 0i /\ ~(beval b s))``, 4129 RW_TAC std_ss [SPEC_def,VALID_def] 4130 THEN `!s1 s2. (int_gt (neval n s1) 0i /\ beval b s1) /\ EVAL c s1 s2 ==> int_gt (neval n s2) 0i` by METIS_TAC [] 4131 THEN IMP_RES_TAC (BETA_RULE (Q.SPEC `\s. int_gt (neval n s) 0i` (SIMP_RULE std_ss [SPEC_def] ANWHILE_RULE))) 4132 THEN METIS_TAC[]); 4133 4134(* 4135val ASP_SVC = 4136 time store_thm 4137 ("ASP_SVC", 4138 ``!c P. LocalFree c /\ |= (SND (ASP_SVC(P, c))) ==> SPEC P c (FST (ASP_SVC(P,c)))``, 4139 Induct 4140 THEN RW_TAC std_ss [LocalFree_def] 4141 THENL 4142 [RW_TAC std_ss [SPEC_def,VALID_def,ASP_SVC_def,SKIP_THM], 4143 RW_TAC std_ss [SPEC_def,VALID_def,ASP_SVC_def,GEN_ASSIGN_THM] 4144 THEN METIS_TAC[], 4145 RW_TAC std_ss [SPEC_def,VALID_def,ASP_SVC_def,DISPOSE_THM] 4146 THEN METIS_TAC[], 4147 FULL_SIMP_TAC std_ss [SPEC_def,VALID_def,ASP_SVC_def,SEQ_THM] 4148 THEN METIS_TAC[], 4149 FULL_SIMP_TAC std_ss [SPEC_def,VALID_def,ASP_SVC_def,IF_THM] 4150 THEN RW_TAC std_ss [] 4151 THEN Cases_on `beval b s1` 4152 THEN FULL_SIMP_TAC std_ss [] 4153 THENL 4154 [ASSUM_LIST 4155 (fn thl => 4156 ASSUME_TAC(SIMP_RULE std_ss[] (Q.ISPEC `\s. P s /\ beval b s` (el 9 thl)))) 4157 THEN METIS_TAC[], 4158 ASSUM_LIST 4159 (fn thl => 4160 ASSUME_TAC(SIMP_RULE std_ss[] (Q.ISPEC `\s. P s /\ ~(beval b s)` (el 8 thl)))) 4161 THEN METIS_TAC[]], 4162 FULL_SIMP_TAC std_ss [ASP_SVC_def,VALID_def] 4163 THEN RW_TAC std_ss [] 4164 THEN `SPEC (\s. f s /\ beval b s) c (FST (ASP_SVC ((\s. f s /\ beval b s),c)))` by METIS_TAC[] 4165 THEN IMP_RES_TAC(SIMP_RULE std_ss [VALID_def]POST_DERIVED_ANWHILE_RULE) 4166 THEN METIS_TAC[], 4167 FULL_SIMP_TAC std_ss [SPEC_def,VALID_def,ASP_SVC_def]]); 4168*) 4169 4170(* LATEST VERSION! - VCs are bools not preds *) 4171val ASP_SVC_def = 4172 Define 4173 `(ASP_SVC(P, Skip)= (P, T)) 4174 /\ 4175 (ASP_SVC(P, GenAssign v e) = 4176 ((\s'. ?s. P s /\ (s' = Update v e s)), T)) 4177 /\ 4178 (ASP_SVC(P, Dispose v) = 4179 ((\s'. ?s. P s /\ (s' = s \\ v)), T)) 4180 /\ 4181 (ASP_SVC(P, Seq c1 c2) = 4182 (FST(ASP_SVC(FST(ASP_SVC(P, c1)), c2)), 4183 SND (ASP_SVC(P, c1)) /\ SND (ASP_SVC(FST(ASP_SVC(P, c1)), c2)))) 4184 /\ 4185 (ASP_SVC(P, Cond b c1 c2) = 4186 ((\s'. FST (ASP_SVC((\s. P s /\ beval b s), c1)) s' 4187 \/ 4188 FST (ASP_SVC((\s. P s /\ ~(beval b s)), c2)) s'), 4189 SND (ASP_SVC((\s. P s /\ beval b s),c1)) 4190 /\ 4191 SND (ASP_SVC((\s. P s /\ ~(beval b s)),c2)))) 4192 /\ 4193 (ASP_SVC(P, AnWhile b n c) = 4194 ((\s. int_gt (neval n s) 0i /\ ~(beval b s)), 4195 (!s. P s ==> int_gt (neval n s) 0i) /\ 4196 (!s. FST(ASP_SVC ((\s. int_gt (neval n s) 0i /\ beval b s),c)) s ==> int_gt (neval n s) 0i) /\ 4197 SND(ASP_SVC ((\s. int_gt (neval n s) 0i /\ beval b s),c))))`; 4198 4199val ASP_def = Define `ASP P c = FST(ASP_SVC(P,c))`; 4200 4201val SVC_def = Define `SVC P c = SND(ASP_SVC(P,c))`; 4202 4203val ASP = 4204 store_thm 4205 ("ASP", 4206 ``(ASP P Skip = P) 4207 /\ 4208 (ASP P (GenAssign v e) = \s'. ?s. P s /\ (s' = Update v e s)) 4209 /\ 4210 (ASP P (Dispose v) = \s'. ?s. P s /\ (s' = s \\ v)) 4211 /\ 4212 (ASP P (Seq c1 c2) = ASP (ASP P c1) c2) 4213 /\ 4214 (ASP P (Cond b c1 c2) = 4215 \s'. ASP (\s. P s /\ beval b s) c1 s' \/ ASP (\s. P s /\ ~(beval b s)) c2 s') 4216 /\ 4217 (ASP P (AnWhile b n c) = \s. int_gt (neval n s) 0i /\ ~(beval b s))``, 4218 RW_TAC std_ss [ASP_def,ASP_SVC_def]); 4219 4220val SVC = 4221 store_thm 4222 ("SVC", 4223 ``(SVC P Skip = T) 4224 /\ 4225 (SVC P (GenAssign v e) = T) 4226 /\ 4227 (SVC P (Dispose v) = T) 4228 /\ 4229 (SVC P (Seq c1 c2) = SVC P c1 /\ SVC (ASP P c1) c2) 4230 /\ 4231 (SVC P (Cond b c1 c2) = 4232 SVC (\s. P s /\ beval b s) c1 /\ SVC (\s. P s /\ ~(beval b s)) c2) 4233 /\ 4234 (SVC P (AnWhile b n c) = 4235 (!s. P s ==> int_gt (neval n s) 0i) /\ 4236 (!s. ASP (\s. int_gt (neval n s) 0i /\ beval b s) c s ==> int_gt (neval n s) 0i) /\ 4237 SVC (\s. int_gt (neval n s) 0i /\ beval b s) c)``, 4238 RW_TAC std_ss [ASP_def,SVC_def,ASP_SVC_def]); 4239 4240(*---------------------------------------------------------------------------*) 4241(* Another derived While rule *) 4242(*---------------------------------------------------------------------------*) 4243 4244val POST_DERIVED_ANWHILE_RULE = 4245 store_thm 4246 ("POST_DERIVED_ANWHILE_RULE", 4247 ``!P Q n b c. 4248 (!s. P s ==> int_gt (neval n s) 0i) 4249 /\ 4250 (!s. Q s ==> int_gt (neval n s) 0i) 4251 /\ 4252 SPEC (\s. int_gt (neval n s) 0i /\ beval b s) c Q 4253 ==> 4254 SPEC P (AnWhile b n c) (\s. int_gt (neval n s) 0i /\ ~(beval b s))``, 4255 RW_TAC std_ss [SPEC_def] 4256 THEN `!s1 s2. (int_gt (neval n s1) 0i /\ beval b s1) /\ EVAL c s1 s2 ==> int_gt (neval n s2) 0i` by METIS_TAC[] 4257 THEN IMP_RES_TAC (BETA_RULE (Q.SPEC `\s. int_gt (neval n s) 0i` (SIMP_RULE std_ss [SPEC_def] ANWHILE_RULE))) 4258 THEN METIS_TAC[]); 4259 4260val ASP_SVC = 4261 time store_thm 4262 ("ASP_SVC", 4263 ``!c P. LocalFree c /\ SND (ASP_SVC(P, c)) ==> SPEC P c (FST (ASP_SVC(P,c)))``, 4264 Induct 4265 THEN RW_TAC std_ss [LocalFree_def] 4266 THENL 4267 [RW_TAC std_ss [SPEC_def,ASP_SVC_def,SKIP_THM], 4268 RW_TAC std_ss [SPEC_def,ASP_SVC_def,GEN_ASSIGN_THM] 4269 THEN METIS_TAC[], 4270 RW_TAC std_ss [SPEC_def,ASP_SVC_def,DISPOSE_THM] 4271 THEN METIS_TAC[], 4272 FULL_SIMP_TAC std_ss [SPEC_def,ASP_SVC_def,SEQ_THM] 4273 THEN METIS_TAC[], 4274 FULL_SIMP_TAC std_ss [SPEC_def,ASP_SVC_def,IF_THM] 4275 THEN RW_TAC std_ss [] 4276 THENL 4277 [ASSUM_LIST 4278 (fn thl => 4279 ASSUME_TAC(SIMP_RULE std_ss[] (Q.ISPEC `\s. P s /\ beval b s` (el 9 thl)))) 4280 THEN METIS_TAC[], 4281 ASSUM_LIST 4282 (fn thl => 4283 ASSUME_TAC(SIMP_RULE std_ss[] (Q.ISPEC `\s. P s /\ ~(beval b s)` (el 8 thl)))) 4284 THEN METIS_TAC[]], 4285 FULL_SIMP_TAC std_ss [ASP_SVC_def] 4286 THEN RW_TAC std_ss [] 4287 THEN `SPEC (\s. int_gt (neval n s) 0i /\ beval b s) c (FST (ASP_SVC ((\s. int_gt (neval n s) 0i /\ beval b s),c)))` by METIS_TAC[] 4288 THEN IMP_RES_TAC(SIMP_RULE std_ss [VALID_def]POST_DERIVED_ANWHILE_RULE)]); 4289 4290val SVLC_ASP_SPEC = 4291 time store_thm 4292 ("SVLC_ASP_SPEC", 4293 ``!c P. LocalFree c /\ SVC P c ==> SPEC P c (ASP P c)``, 4294 RW_TAC std_ss [ASP_def,SVC_def,ASP_SVC_def,ASP_SVC]); 4295 4296(* Failed attempt at GDP theorem to better characterise SVC and ASP 4297 4298val SVLC_ASP_SPEC = 4299 time store_thm 4300 ("SVLC_ASP_SPEC", 4301 ``!c. LocalFree c ==> !P. SVC P c ==> !Q. SPEC P c Q ==> !s. ASP P c s ==> Q s``, 4302 Induct 4303 THEN RW_TAC std_ss [LocalFree_def] 4304 THENL 4305 [FULL_SIMP_TAC std_ss [ASP,SVC,ASP_SVC_def,ASP_SVC,SPEC_def,SKIP_THM], 4306 FULL_SIMP_TAC std_ss [ASP,SVC,ASP_SVC_def,ASP_SVC,SPEC_def,GEN_ASSIGN_THM], 4307 FULL_SIMP_TAC std_ss [ASP,SVC,ASP_SVC_def,ASP_SVC,SPEC_def,DISPOSE_THM], 4308 FULL_SIMP_TAC std_ss [ASP,SVC,ASP_SVC_def,ASP_SVC,SPEC_def,SEQ_THM] 4309 4310*) 4311 4312(* Following stuff on symbolic execution and strongest liberal postconditions *) 4313 4314(* Theorems below are maybe subsumed by STRAIGHT_RUN_SP *) 4315 4316val SKIP_EXEC_SP = 4317 store_thm 4318 ("SKIP_EXEC_SP", 4319 ``!l v e. SP (\s. s = FEMPTY |++ l) Skip = \s. s = FEMPTY |++ l ``, 4320 RW_TAC std_ss [SP_def,EVAL_FUN_def]); 4321 4322val GEN_ASSIGN_EXEC_SP = 4323 store_thm 4324 ("GEN_ASSIGN_EXEC_SP", 4325 ``!l. DISTINCT_VARS l 4326 ==> 4327 !v e. SP (\s. s = FEMPTY |++ l) (GenAssign v e) = 4328 \s. s = FEMPTY |++ (UPDATE_LIST l (v, naeval e (FEMPTY |++ l)))``, 4329 RW_TAC std_ss [SP_def,EVAL_FUN_def,Update_def] 4330 THEN CONV_TAC (X_FUN_EQ_CONV ``s':state``) 4331 THEN REPEAT STRIP_TAC 4332 THEN EQ_TAC 4333 THEN RW_TAC std_ss [UPDATE_LIST_FUPDATE]); 4334 4335val VARS_IN_SEQ = 4336 store_thm 4337 ("VARS_IN_SEQ", 4338 ``!c1 c2 l. VARS_IN c1 l /\ VARS_IN c2 l ==> VARS_IN (Seq c1 c2) l``, 4339 RW_TAC std_ss [VARS_IN_def,VARS_def,IN_UNION] 4340 THEN METIS_TAC[]); 4341 4342val SEQ_EXEC_SP = 4343 store_thm 4344 ("SEQ_EXEC_SP", 4345 ``!l. DISTINCT_VARS l 4346 ==> 4347 !c1 c2. STRAIGHT c1 /\ STRAIGHT c2 /\ VARS_IN c1 l /\ VARS_IN c2 l 4348 ==> 4349 (SP (\s. s = FEMPTY |++ l) (Seq c1 c2) = 4350 \s. s = FEMPTY |++ (STRAIGHT_RUN c2 (STRAIGHT_RUN c1 l)))``, 4351 RW_TAC std_ss [SP_def,EVAL_FUN_EVAL] 4352 THEN CONV_TAC (X_FUN_EQ_CONV ``s':state``) 4353 THEN RW_TAC std_ss [GSYM STRAIGHT_RUN_def] 4354 THEN EQ_TAC 4355 THEN RW_TAC std_ss [] 4356 THEN METIS_TAC[STRAIGHT_RUN_EVAL,EVAL_DETERMINISTIC,STRAIGHT_def,VARS_IN_SEQ]); 4357 4358val VARS_IN_IF = 4359 store_thm 4360 ("VARS_IN_IF", 4361 ``!b c1 c2 l. VARS_IN c1 l /\ VARS_IN c2 l ==> VARS_IN (Cond b c1 c2) l``, 4362 RW_TAC std_ss [VARS_IN_def,VARS_def,IN_UNION] 4363 THEN METIS_TAC[]); 4364 4365val IF_EXEC_SP = 4366 store_thm 4367 ("IF_EXEC_SP", 4368 ``!l. DISTINCT_VARS l 4369 ==> 4370 !c1 c2. STRAIGHT c1 /\ STRAIGHT c2 /\ VARS_IN c1 l /\ VARS_IN c2 l 4371 ==> 4372 (SP (\s. s = FEMPTY |++ l) (Cond b c1 c2) = 4373 \s. s = FEMPTY |++ ZIP_LIST (beval b (FEMPTY |++ l)) (STRAIGHT_RUN c1 l) (STRAIGHT_RUN c2 l))``, 4374 RW_TAC std_ss [SP_def,EVAL_FUN_EVAL] 4375 THEN CONV_TAC (X_FUN_EQ_CONV ``s':state``) 4376 THEN RW_TAC std_ss [GSYM STRAIGHT_RUN_def] 4377 THEN EQ_TAC 4378 THEN RW_TAC std_ss [] 4379 THEN METIS_TAC[STRAIGHT_RUN_EVAL,EVAL_DETERMINISTIC,STRAIGHT_def,VARS_IN_IF]); 4380 4381val STRAIGHT_RUN_SP = 4382 store_thm 4383 ("STRAIGHT_RUN_SP", 4384 ``!c. STRAIGHT c 4385 ==> 4386 !l. DISTINCT_VARS l 4387 ==> 4388 VARS_IN c l 4389 ==> 4390 !P. SP (\s. (s = FEMPTY |++ l) /\ P) c = 4391 \s. (s = FEMPTY |++ (STRAIGHT_RUN c l)) /\ P``, 4392 RW_TAC std_ss [SP_def] 4393 THEN CONV_TAC (X_FUN_EQ_CONV ``s':state``) 4394 THEN REPEAT STRIP_TAC 4395 THEN RW_TAC std_ss [EVAL_FUN_EVAL] 4396 THEN METIS_TAC[STRAIGHT_RUN_EVAL,EVAL_DETERMINISTIC]); 4397 4398(* Utility theorems used in BRANCH_SOLVE *) 4399 4400val PRE_T = 4401 save_thm("PRE_T", METIS_PROVE [] ``!p b : bool. (p ==> b = T) ==> (p ==> (b = T))``); 4402 4403val PRE_F = 4404 save_thm("PRE_F", METIS_PROVE [] ``!p b : bool. (p ==> b = F) ==> (p ==> (b = F))``); 4405 4406val NOT_PRE_T = 4407 save_thm("NOT_PRE_T", METIS_PROVE [] ``!p b : bool. (p ==> ~b = T) ==> (p ==> (b = F))``); 4408 4409val NOT_PRE_F = 4410 save_thm("NOT_PRE_F", METIS_PROVE [] ``!p b : bool. (p ==> ~b = F) ==> (p ==> (b = T))``); 4411 4412(* Utility theorems used in CondTest *) 4413 4414val TEST_F = 4415 save_thm("TEST_F", METIS_PROVE [] ``!p b : bool. (p ==> b = F) ==> (p ==> ~b)``); 4416 4417val NOT_TEST_F = 4418 save_thm("NOT_TEST_F", METIS_PROVE [] ``!p b : bool. (p ==> ~b = F) ==> (p ==> b)``); 4419 4420(* Check if command supports VC generation on a state vector xl *) 4421val VC_CHECK_def = 4422 Define 4423 `(VC_CHECK xl Skip = T) 4424 /\ 4425 (VC_CHECK xl (GenAssign v e) = T) 4426 /\ 4427 (VC_CHECK xl (Dispose v) = F) 4428 /\ 4429 (VC_CHECK xl (Seq c1 c2) = VC_CHECK xl c1 /\ VC_CHECK xl c2) 4430 /\ 4431 (VC_CHECK xl (Cond b c1 c2) = VC_CHECK xl c1 /\ VC_CHECK xl c2) 4432 /\ 4433 (VC_CHECK xl (AnWhile b n c) = 4434 VC_CHECK xl c /\ ?l. (MAP FST l = xl) /\ int_gt (neval n (FEMPTY |++ l)) 0i /\ ~(beval b (FEMPTY |++ l))) 4435 /\ 4436 (VC_CHECK xl (Local v c) = F)`; 4437 4438 4439(* TFL won't accept VC_RUN (see below) as a definition, so need the following *) 4440val VC_RUN_def = 4441 Define 4442 `(VC_RUN Skip lP = (lP, T)) 4443 /\ 4444 (VC_RUN (GenAssign v e) lP = 4445 ((UPDATE_LIST (FST lP) (v, naeval e (FEMPTY |++ (FST lP))), 4446 \s'. ?s. (SND lP) s /\ (s' = Update v e s)), 4447 T)) 4448 /\ 4449 (VC_RUN (Seq c1 c2) lP = 4450 (FST(VC_RUN c2 (FST(VC_RUN c1 lP))), 4451 SND (VC_RUN c1 lP) /\ SND (VC_RUN c2 (FST(VC_RUN c1 lP))))) 4452 /\ 4453 (VC_RUN (Cond b c1 c2) lP = 4454 ((ZIP_LIST 4455 (beval b (FEMPTY |++ (FST lP))) 4456 (FST(FST(VC_RUN c1 ((FST lP), \s. (SND lP) s /\ beval b s)))) 4457 (FST(FST(VC_RUN c2 ((FST lP), \s. (SND lP) s /\ ~(beval b s))))), 4458 \s'. SND (FST(VC_RUN c1 ((FST lP), \s. (SND lP) s /\ beval b s))) s' 4459 /\ 4460 SND (FST(VC_RUN c2 ((FST lP), \s. (SND lP) s /\ ~(beval b s)))) s'), 4461 SND (VC_RUN c1 ((FST lP), \s. (SND lP) s /\ beval b s)) 4462 /\ 4463 SND (VC_RUN c2 ((FST lP), \s. (SND lP) s /\ ~(beval b s))))) 4464 /\ 4465 (VC_RUN (AnWhile b n c) lP = 4466 let newlist l' = (MAP FST (FST lP) = MAP FST l') /\ int_gt (neval n (FEMPTY |++ l')) 0i /\ ~(beval b (FEMPTY |++ l')) 4467 in 4468 (((@l'. newlist l'), \s. int_gt (neval n s) 0i /\ ~(beval b s)), 4469 (?l'. newlist l') 4470 /\ 4471 (!s. SND lP s ==> int_gt (neval n s) 0i) 4472 /\ 4473 SPEC (\s. int_gt (neval n s) 0i /\ beval b s) c (\s. int_gt (neval n s) 0i) 4474 /\ 4475 SND (VC_RUN c ((FST lP), \s. SND lP s /\ beval b s))))`; 4476 4477(* 4478VC_RUN c (l,P) = ((l',P'),vc) 4479ASP_SVC P c = (P',vc) 4480*) 4481 4482val VC_RUN = 4483 store_thm 4484 ("VC_RUN", 4485 ``(VC_RUN Skip (l,P) = ((l,P), T)) 4486 /\ 4487 (VC_RUN (GenAssign v e) (l,P) = 4488 ((UPDATE_LIST l (v, naeval e (FEMPTY |++ l)), 4489 \s'. ?s. P s /\ (s' = Update v e s)), 4490 T)) 4491 /\ 4492 (VC_RUN (Seq c1 c2) (l,P) = 4493 (FST(VC_RUN c2 (FST(VC_RUN c1 (l,P)))), 4494 SND (VC_RUN c1 (l,P)) /\ SND (VC_RUN c2 (FST(VC_RUN c1 (l,P)))))) 4495 /\ 4496 (VC_RUN (Cond b c1 c2) (l,P) = 4497 ((ZIP_LIST 4498 (beval b (FEMPTY |++ l)) 4499 (FST(FST(VC_RUN c1 (l, \s. P s /\ beval b s)))) 4500 (FST(FST(VC_RUN c2 (l, \s. P s /\ ~(beval b s))))), 4501 \s'. SND (FST(VC_RUN c1 (l, \s. P s /\ beval b s))) s' 4502 /\ 4503 SND (FST(VC_RUN c2 (l, \s. P s /\ ~(beval b s)))) s'), 4504 SND (VC_RUN c1 (l, \s. P s /\ beval b s)) 4505 /\ 4506 SND (VC_RUN c2 (l, \s. P s /\ ~(beval b s))))) 4507 /\ 4508 (VC_RUN (AnWhile b n c) (l,P) = 4509 let newlist l' = (MAP FST l = MAP FST l') /\ int_gt (neval n (FEMPTY |++ l')) 0i /\ ~(beval b (FEMPTY |++ l')) 4510 in 4511 (((@l'. newlist l'), \s. int_gt (neval n s) 0i /\ ~(beval b s)), 4512 (?l'. newlist l') 4513 /\ 4514 (!s. P s ==> int_gt (neval n s) 0i) 4515 /\ 4516 SPEC (\s. int_gt (neval n s) 0i /\ beval b s) c (\s. int_gt (neval n s) 0i) 4517 /\ 4518 SND (VC_RUN c (l, \s. P s /\ beval b s))))``, 4519 RW_TAC std_ss [VC_RUN_def]); 4520 4521val SEQ_VARS_IN = 4522 store_thm 4523 ("SEQ_VARS_IN", 4524 ``!c1 c2 l. VARS_IN (Seq c1 c2) l = VARS_IN c1 l /\ VARS_IN c2 l``, 4525 RW_TAC std_ss [VARS_IN_def,VARS_def,IN_UNION] 4526 THEN METIS_TAC[]); 4527 4528val IF_VARS_IN = 4529 store_thm 4530 ("IF_VARS_IN", 4531 ``!b c1 c2 l. VARS_IN (Cond b c1 c2) l = VARS_IN c1 l /\ VARS_IN c2 l``, 4532 RW_TAC std_ss [VARS_IN_def,VARS_def,IN_UNION] 4533 THEN METIS_TAC[]); 4534 4535val ANWHILE_VARS_IN = 4536 store_thm 4537 ("ANWHILE_VARS_IN", 4538 ``!b R c l. VARS_IN (AnWhile b R c) l = VARS_IN c l``, 4539 RW_TAC std_ss [VARS_IN_def,VARS_def,IN_UNION] 4540 THEN METIS_TAC[]); 4541 4542(* Check if command supports VC generation on a state vector xl *) 4543val VC_CHECK_def = 4544 Define 4545 `(VC_CHECK Skip = T) 4546 /\ 4547 (VC_CHECK (GenAssign v e) = T) 4548 /\ 4549 (VC_CHECK (Dispose v) = F) 4550 /\ 4551 (VC_CHECK (Seq c1 c2) = VC_CHECK c1 /\ VC_CHECK c2) 4552 /\ 4553 (VC_CHECK (Cond b c1 c2) = VC_CHECK c1 /\ VC_CHECK c2) 4554 /\ 4555 (VC_CHECK (AnWhile b R c) = VC_CHECK c) 4556 /\ 4557 (VC_CHECK (Local v c) = F)`; 4558 4559val VARS_VC_RUN = 4560 prove 4561 (``!c l. VC_CHECK c /\ VARS_IN c l 4562 ==> !P. SND(VC_RUN c (l,P)) 4563 ==> 4564 (MAP FST (FST(FST(VC_RUN c (l,P)))) = MAP FST l)``, 4565 Induct 4566 THEN RW_TAC list_ss 4567 [VC_CHECK_def,VARS_def,NOT_IN_EMPTY,IN_SING,VC_RUN_def, 4568 MAP_FST_UPDATE_LIST,IN_UNION,MAP_FST_ZIP_LIST,SEQ_VARS_IN,IF_VARS_IN] 4569 THENL 4570 [FULL_SIMP_TAC std_ss [VARS_IN_def,VARS_def,NOT_IN_EMPTY,IN_SING], 4571 METIS_TAC[pairTheory.PAIR,VARS_IN_def], 4572 FULL_SIMP_TAC std_ss [markerTheory.Abbrev_def,LET_DEF] 4573 THEN RW_TAC std_ss [] 4574 THEN SELECT_ELIM_TAC 4575 THEN RW_TAC std_ss [] 4576 THEN METIS_TAC[]]); 4577 4578val VARS_VC_RUN_COR = 4579 prove 4580 (``!c l. VC_CHECK c /\ VARS_IN c l 4581 ==> !P. SND(VC_RUN c (l,P)) 4582 ==> 4583 (LENGTH(FST(FST(VC_RUN c (l,P)))) = LENGTH l)``, 4584 METIS_TAC[VARS_IN_def,rich_listTheory.LENGTH_MAP,VARS_VC_RUN]); 4585 4586val VC_RUN_DISTINCT = 4587 store_thm 4588 ("VC_RUN_DISTINCT", 4589 ``!c l. VC_CHECK c /\ VARS_IN c l /\ DISTINCT_VARS l 4590 ==> !P. SND(VC_RUN c (l,P)) 4591 ==> 4592 DISTINCT_VARS(FST(FST(VC_RUN c (l,P))))``, 4593 Induct 4594 THEN RW_TAC std_ss [rules,VC_RUN_def,VC_CHECK_def] 4595 THEN RW_TAC std_ss 4596 [SEQ_THM,IF_THM,rules,GEN_ASSIGN_THM,UpdateCases, 4597 VC_RUN_def,UPDATE_LIST_FUPDATE,UpdateDISTINCT,ZIP_LIST_DISTINCT] 4598 THEN FULL_SIMP_TAC std_ss [IF_VARS_IN,SEQ_VARS_IN] 4599 THENL 4600 [METIS_TAC[pairTheory.PAIR,VARS_VC_RUN,VARS_IN_def], 4601 METIS_TAC[pairTheory.PAIR,VARS_VC_RUN,VARS_IN_def,ZIP_LIST_DISTINCT], 4602 FULL_SIMP_TAC std_ss [markerTheory.Abbrev_def,LET_DEF] 4603 THEN RW_TAC std_ss [] 4604 THEN SELECT_ELIM_TAC 4605 THEN RW_TAC std_ss [] 4606 THEN METIS_TAC[DISTINCT_VARS_def]]); 4607 4608(* Compare: !c P. LocalFree c /\ |= (SND (ASP_SVC(P, c))) ==> SPEC P c (FST (ASP_SVC(P,c))) *) 4609 4610(* SPEC P c (SND (FST(VC_RUN c (l,P)))) *) 4611 4612(* P(FEMPTY |++ l1) /\ EVAL c (FEMPTY |++ l1) (FEMPTY |++ l2) ==> SND (FST(VC_RUN c (l1,P))) (FEMPTY |++ l2) *) 4613 4614(* P(FEMPTY |++ l) /\ EVAL c (FEMPTY |++ l) s ==> SND (FST(VC_RUN c (l,P))) s *) 4615 4616(* Check if command supports VC generation on a state vector xl *) 4617val VC_CHECK_def = 4618 Define 4619 `(VC_CHECK Skip = T) 4620 /\ 4621 (VC_CHECK (GenAssign v e) = T) 4622 /\ 4623 (VC_CHECK (Dispose v) = F) 4624 /\ 4625 (VC_CHECK (Seq c1 c2) = VC_CHECK c1 /\ VC_CHECK c2) 4626 /\ 4627 (VC_CHECK (Cond b c1 c2) = VC_CHECK c1 /\ VC_CHECK c2) 4628 /\ 4629 (VC_CHECK (AnWhile b R c) = VC_CHECK c) 4630 /\ 4631 (VC_CHECK (Local v c) = F)`; 4632 4633 4634val VC_RUN_def = 4635 Define 4636 `(VC_RUN Skip l = (l, T)) 4637 /\ 4638 (VC_RUN (GenAssign v e) l = (UPDATE_LIST l (v, naeval e (FEMPTY |++ l)), T)) 4639 /\ 4640 (VC_RUN (Seq c1 c2) l = 4641 (FST(VC_RUN c2 (FST(VC_RUN c1 l))), 4642 SND (VC_RUN c1 l) /\ SND (VC_RUN c2 (FST(VC_RUN c1 l))))) 4643 /\ 4644 (VC_RUN (Cond b c1 c2) l = 4645 (ZIP_LIST (beval b (FEMPTY |++ l)) (FST(VC_RUN c1 l)) (FST(VC_RUN c2 l)), 4646 SND(VC_RUN c1 l) /\ SND(VC_RUN c2 l))) 4647 /\ 4648 (VC_RUN (AnWhile b n c) l = 4649 ((@l'. (MAP FST l = MAP FST l') /\ int_gt (neval n (FEMPTY |++ l')) 0i /\ ~(beval b (FEMPTY |++ l'))), 4650 int_gt (neval n (FEMPTY |++ l)) 0i /\ 4651 SPEC (\s. int_gt (neval n s) 0i /\ beval b s) c (\s. int_gt (neval n s) 0i) /\ 4652 ?l'. (MAP FST l' = MAP FST l) /\ int_gt (neval n (FEMPTY |++ l')) 0i /\ ~beval b (FEMPTY |++ l')))`; 4653 4654val SEQ_VARS_IN = 4655 store_thm 4656 ("SEQ_VARS_IN", 4657 ``!c1 c2 l. VARS_IN (Seq c1 c2) l = VARS_IN c1 l /\ VARS_IN c2 l``, 4658 RW_TAC std_ss [VARS_IN_def,VARS_def,IN_UNION] 4659 THEN METIS_TAC[]); 4660 4661val IF_VARS_IN = 4662 store_thm 4663 ("IF_VARS_IN", 4664 ``!b c1 c2 l. VARS_IN (Cond b c1 c2) l = VARS_IN c1 l /\ VARS_IN c2 l``, 4665 RW_TAC std_ss [VARS_IN_def,VARS_def,IN_UNION] 4666 THEN METIS_TAC[]); 4667 4668val VARS_VC_RUN = 4669 prove 4670 (``!c l. VC_CHECK c /\ VARS_IN c l /\ SND(VC_RUN c l) 4671 ==> (MAP FST (FST(VC_RUN c l)) = MAP FST l)``, 4672 Induct 4673 THEN RW_TAC list_ss 4674 [VC_CHECK_def,VARS_def,NOT_IN_EMPTY,IN_SING,VC_RUN_def, 4675 MAP_FST_UPDATE_LIST,IN_UNION,MAP_FST_ZIP_LIST,SEQ_VARS_IN,IF_VARS_IN] 4676 THENL 4677 [FULL_SIMP_TAC std_ss [VARS_IN_def,VARS_def,NOT_IN_EMPTY,IN_SING], 4678 METIS_TAC[pairTheory.PAIR,VARS_IN_def], 4679 SELECT_ELIM_TAC 4680 THEN RW_TAC std_ss [] 4681 THEN METIS_TAC[]]); 4682 4683val VARS_VC_RUN_COR = 4684 prove 4685 (``!c l. VC_CHECK c /\ VARS_IN c l /\ SND(VC_RUN c l) 4686 ==> (LENGTH(FST(VC_RUN c l)) = LENGTH l)``, 4687 METIS_TAC[VARS_IN_def,rich_listTheory.LENGTH_MAP,VARS_VC_RUN]); 4688 4689val VC_RUN_DISTINCT = 4690 store_thm 4691 ("VC_RUN_DISTINCT", 4692 ``!c l. VC_CHECK c /\ VARS_IN c l /\ DISTINCT_VARS l /\ SND(VC_RUN c l) 4693 ==> DISTINCT_VARS(FST(VC_RUN c l))``, 4694 Induct 4695 THEN RW_TAC std_ss [rules,VC_RUN_def,VC_CHECK_def] 4696 THEN RW_TAC std_ss 4697 [SEQ_THM,IF_THM,rules,GEN_ASSIGN_THM,UpdateCases, 4698 VC_RUN_def,UPDATE_LIST_FUPDATE,UpdateDISTINCT,ZIP_LIST_DISTINCT] 4699 THEN FULL_SIMP_TAC std_ss [IF_VARS_IN,SEQ_VARS_IN] 4700 THENL 4701 [METIS_TAC[pairTheory.PAIR,VARS_VC_RUN,VARS_IN_def], 4702 METIS_TAC[pairTheory.PAIR,VARS_VC_RUN,VARS_IN_def,ZIP_LIST_DISTINCT], 4703 SELECT_ELIM_TAC 4704 THEN RW_TAC std_ss [] 4705 THEN METIS_TAC[DISTINCT_VARS_def]]); 4706 4707 4708val PDOM_def = 4709 Define 4710 `PDOM xl P = !s. P s ==> (FDOM s = set xl)`; 4711 4712(* Split ASP_SVC into two functions: ASP_SVC(P,c) = (LP P c, FVC P c) *) 4713 4714val FDOM_SET = 4715 store_thm 4716 ("FDOM_SET", 4717 ``!l. FDOM (FEMPTY |++ l) = set (MAP FST l)``, 4718 Induct 4719 THEN RW_TAC list_ss [FDOM_FUPDATE_LIST,FDOM_FEMPTY,UNION_EMPTY]); 4720 4721val FUPDATE_LIST_FUPDATE_COMMUTE = 4722 store_thm 4723 ("FUPDATE_LIST_FUPDATE_COMMUTE", 4724 ``!l v. ~(MEM v (MAP FST l)) /\ DISTINCT_VARS l 4725 ==> !fm x. fm |++ ((v,x) :: l) = (fm |++ l) |+ (v,x)``, 4726 Induct 4727 THEN RW_TAC std_ss [FUPDATE_LIST_THM,FUPDATE_EQ] 4728 THEN Cases_on `h` 4729 THEN FULL_SIMP_TAC list_ss 4730 [FUPDATE_LIST_THM,DISTINCT_VARS_def,listTheory.ALL_DISTINCT] 4731 THEN METIS_TAC[FUPDATE_EQ,FUPDATE_COMMUTES]); 4732 4733val S2L_def = 4734 Define 4735 `S2L s = MAP (\x. (x, s ' x))`; 4736 4737val MAP_S2L = 4738 store_thm 4739 ("MAP_S2L", 4740 ``!xl. MAP FST (S2L s xl) = xl``, 4741 REWRITE_TAC [S2L_def] 4742 THEN Induct 4743 THEN RW_TAC list_ss []); 4744 4745(* Four ad hoc lemmas used to prove S2L_MAP *) 4746 4747val S2L_MAP_LEMMA1 = 4748 prove 4749 (``!l : (string # value)list. 4750 (!x. MEM x l ==> (f x = g x)) ==> (MAP f l = MAP g l)``, 4751 Induct 4752 THEN RW_TAC list_ss []); 4753 4754val S2L_MAP_LEMMA2 = 4755 prove 4756 (``!l : (string # value)list. MEM p l ==> MEM (FST p) (MAP FST l)``, 4757 Induct 4758 THEN RW_TAC list_ss [] 4759 THEN METIS_TAC[]); 4760 4761val S2L_MAP_LEMMA3 = 4762 prove 4763 (``~MEM q (MAP FST l) 4764 ==> 4765 !p : string # value. 4766 MEM p l 4767 ==> 4768 (((\x. (x,(if x = q then r else ((FEMPTY |++ l) ' x)))) o FST) p = 4769 ((\x. (x,(FEMPTY |++ l) ' x)) o FST) p)``, 4770 RW_TAC std_ss [] 4771 THEN METIS_TAC[S2L_MAP_LEMMA2]); 4772 4773val S2L_MAP_LEMMA4 = 4774 prove 4775 (``!l : (string # value)list. 4776 DISTINCT_VARS l 4777 ==> 4778 (MAP (\x. (x, (FEMPTY |++ l) ' x)) (MAP FST l) = l)``, 4779 Induct 4780 THEN RW_TAC list_ss [] 4781 THEN Cases_on `h` 4782 THEN FULL_SIMP_TAC list_ss [DISTINCT_VARS_def] 4783 THEN FULL_SIMP_TAC list_ss [GSYM DISTINCT_VARS_def] 4784 THEN FULL_SIMP_TAC list_ss [FUPDATE_LIST_FUPDATE_COMMUTE,FAPPLY_FUPDATE_THM] 4785 THEN FULL_SIMP_TAC std_ss [rich_listTheory.MAP_MAP_o] 4786 THEN METIS_TAC[S2L_MAP_LEMMA1,S2L_MAP_LEMMA3]); 4787 4788val S2L_MAP = 4789 store_thm 4790 ("S2L_MAP", 4791 ``!l : (string # value)list. 4792 DISTINCT_VARS l ==> (S2L (FEMPTY |++ l) (MAP FST l) = l)``, 4793 METIS_TAC[S2L_MAP_LEMMA4,S2L_def]); 4794 4795val MAP_FST_LEMMA = 4796 store_thm 4797 ("MAP_FST_LEMMA", 4798 ``!xl f. (!x. FST(f x) = x) ==> (MAP (FST o f) xl = xl)``, 4799 Induct 4800 THEN RW_TAC list_ss []); 4801 4802val ALL_DISTINCT_DISTINCT_VARS = 4803 store_thm 4804 ("ALL_DISTINCT_DISTINCT_VARS", 4805 ``!xl. ALL_DISTINCT xl ==> !f. (!x. FST(f x) = x) ==> DISTINCT_VARS(MAP f xl)``, 4806 Induct 4807 THEN RW_TAC list_ss [MAP_FST_LEMMA,DISTINCT_VARS_def,rich_listTheory.MAP_MAP_o]); 4808 4809val MAP_FAPPLY_LEMMA = 4810 prove 4811 (``!xl. ~MEM h xl ==> (MAP (\x. (x,s ' x)) xl = MAP (\x. (x,(s\\h) ' x)) xl)``, 4812 Induct 4813 THEN RW_TAC list_ss [DOMSUB_FAPPLY_NEQ]); 4814 4815(* Must be a better proof than the following! *) 4816val S2L = 4817 store_thm 4818 ("S2L", 4819 ``!xl. ALL_DISTINCT xl ==> !s. (FDOM s = set xl) ==> (s = FEMPTY |++ S2L s xl)``, 4820 Induct 4821 THEN RW_TAC std_ss 4822 [S2L_def,GSYM fmap_EQ_THM,FDOM_FUPDATE_LIST,FDOM_FEMPTY,UNION_EMPTY, 4823 rich_listTheory.MAP_MAP_o,MAP_FST_LEMMA] 4824 THEN FULL_SIMP_TAC list_ss 4825 [listTheory.IN_LIST_TO_SET,listTheory.LIST_TO_SET_THM,rich_listTheory.IS_EL,S2L_def] 4826 THEN RW_TAC std_ss [] 4827 THEN `!x. FST((\x. (x,s ' x)) x) = x` by RW_TAC std_ss [] 4828 THEN IMP_RES_TAC ALL_DISTINCT_DISTINCT_VARS 4829 THEN RW_TAC std_ss [FUPDATE_LIST_FUPDATE_COMMUTE] 4830 THEN ASSUME_TAC 4831 (SIMP_RULE std_ss [rich_listTheory.MAP_MAP_o] 4832 (SPECL [``MAP (\x. (x,s ' x)) (xl:'a list)``,``h:'a``] FUPDATE_LIST_FUPDATE_COMMUTE)) 4833 THEN FULL_SIMP_TAC std_ss [ALL_DISTINCT_DISTINCT_VARS,MAP_FST_LEMMA,FAPPLY_FUPDATE_THM] 4834 THEN `~(x = h)` by METIS_TAC[] 4835 THEN RW_TAC std_ss [] 4836 THEN `FDOM(s \\ h) = (h INSERT set xl) DELETE h` by METIS_TAC[FDOM_DOMSUB] 4837 THEN FULL_SIMP_TAC std_ss [EXTENSION,IN_DELETE,IN_INSERT] 4838 THEN `FDOM(s \\ h) = set xl` by METIS_TAC[EXTENSION,IN_DELETE,IN_INSERT,listTheory.IN_LIST_TO_SET] 4839 THEN `(s \\ h) ' x = s ' x` by METIS_TAC[DOMSUB_FAPPLY_NEQ] 4840 THEN METIS_TAC[MAP_FAPPLY_LEMMA]); 4841 4842 4843(* LOOKUP function *) 4844val LOOKUP_def = 4845 Define 4846 `(LOOKUP [] (v:string) : value = (FEMPTY ' v)) (* Why are these type annotations needed? *) 4847 /\ 4848 (LOOKUP ((v',val) :: l) v = if v = v' then val else LOOKUP l v)`; 4849 4850val STATE_LOOKUP = 4851 store_thm 4852 ("STATE_LOOKUP", 4853 ``!l. DISTINCT_VARS l ==> !v. (FEMPTY |++ l) ' v = LOOKUP l v``, 4854 Induct 4855 THEN RW_TAC std_ss [LOOKUP_def,FUPDATE_LIST_THM] 4856 THEN Cases_on `h` 4857 THEN RW_TAC std_ss [] 4858 THEN FULL_SIMP_TAC list_ss [DISTINCT_VARS_def] 4859 THEN `DISTINCT_VARS l` by METIS_TAC[DISTINCT_VARS_def] 4860 THEN Cases_on `v = q` 4861 THEN RW_TAC std_ss [LOOKUP_def] 4862 THEN METIS_TAC 4863 [FUPDATE_LIST_FUPDATE_NOT_MEM,FUPDATE_LIST_FUPDATE_COMMUTE, 4864 FUPDATE_LIST_THM,FAPPLY_FUPDATE_THM]); 4865 4866val STATE_LOOKUP = 4867 store_thm 4868 ("STATE_LOOKUP", 4869 ``!l. DISTINCT_VARS l ==> (FAPPLY (FEMPTY |++ l) = LOOKUP l)``, 4870 CONV_TAC (DEPTH_CONV(X_FUN_EQ_CONV ``v:string``)) 4871 THEN Induct 4872 THEN RW_TAC std_ss [LOOKUP_def,FUPDATE_LIST_THM] 4873 THEN Cases_on `h` 4874 THEN RW_TAC std_ss [] 4875 THEN FULL_SIMP_TAC list_ss [DISTINCT_VARS_def] 4876 THEN `DISTINCT_VARS l` by METIS_TAC[DISTINCT_VARS_def] 4877 THEN Cases_on `v = q` 4878 THEN RW_TAC std_ss [LOOKUP_def] 4879 THEN METIS_TAC 4880 [FUPDATE_LIST_FUPDATE_NOT_MEM,FUPDATE_LIST_FUPDATE_COMMUTE, 4881 FUPDATE_LIST_THM,FAPPLY_FUPDATE_THM]); 4882 4883(* Disjunction lifted to functions *) 4884val ORF_def = 4885 Define 4886 `$ORF (f1:state->bool) (f2:state->bool) = \s. (f1 s) \/ (f2 s)`; 4887 4888val _ = set_fixity "ORF" (Infixr 405); 4889 4890(* \s. (s = FEMPTY |++ l) /\ P s *) 4891 4892val XP_def = 4893 Define 4894 `(XP xl P Skip = P) 4895 /\ 4896 (XP xl P (GenAssign v e) = \s'. ?s. P s /\ (s' = Update v e s)) 4897 /\ 4898 (XP xl P (Seq c1 c2) = XP xl (XP xl P c1) c2) 4899 /\ 4900 (XP xl P (Cond b c1 c2) = 4901 (XP xl (\s. P s /\ beval b s) c1) ORF (XP xl (\s. P s /\ ~(beval b s)) c2)) 4902 /\ 4903 (XP xl P (AnWhile b n c) = 4904 \s'. (FDOM s' = set xl) /\ int_gt (neval n s') 0i /\ ~(beval b s') /\ ?s. P s) 4905 /\ 4906 (XP xl P (Local v c) = 4907 \s''. ?s' val. XP xl (\s. P s /\ (val = s ' v)) c s' /\ (s'' = s'|+(v,val)))`; 4908 4909val XP_F = 4910 store_thm 4911 ("XP_F", 4912 ``!c. SIMPLE c ==> !xl. XP xl (\s. F) c = \s. F``, 4913 Induct 4914 THEN RW_TAC std_ss [XP_def,ORF_def,SIMPLE_def] 4915 THEN METIS_TAC[]); 4916 4917(* 4918val ORF_LEMMA = 4919 prove 4920 (``!f1 f2 v val. 4921 (\s':state. f1 s' /\ (val = s' ' v) \/ f2 s' /\ (val = s' ' v)) 4922 = 4923 (\s':state. (f1 s' \/ f2 s') /\ (val = s' ' v))``, 4924 CONV_TAC(DEPTH_CONV(FUN_EQ_CONV)) 4925 THEN RW_TAC std_ss [] 4926 THEN METIS_TAC[]); 4927*) 4928 4929val XP_ORF = 4930 store_thm 4931 ("XP_ORF", 4932 ``!c xl f1 f2. SIMPLE c ==> (XP xl (f1 ORF f2) c = (XP xl f1 c ORF XP xl f2 c))``, 4933 Induct 4934 THEN CONV_TAC(DEPTH_CONV(X_FUN_EQ_CONV ``s:state``)) 4935 THEN FULL_SIMP_TAC std_ss [XP_def,ORF_def,SIMPLE_def] 4936 THEN RW_TAC std_ss [XP_def,ORF_def,SIMPLE_def] 4937 THENL 4938 [METIS_TAC[], 4939 METIS_TAC[], 4940 RES_TAC 4941 THEN ASSUM_LIST 4942 (fn thl => 4943 ASSUME_TAC 4944 (SPECL 4945 [``xl:string list``, ``\s:state. f2 s /\ beval b s``, ``\s:state. f1 s /\ beval b s``] 4946 (el 1 thl))) 4947 THEN FULL_SIMP_TAC std_ss [RIGHT_AND_OVER_OR] 4948 THEN METIS_TAC[], 4949 METIS_TAC[], 4950 RES_TAC 4951 THEN POP_ASSUM 4952 (fn th => 4953 ASSUME_TAC 4954 (SIMP_RULE std_ss [] 4955 (GEN_ALL 4956 (AP_THM 4957 (SPECL 4958 [``xl:string list``, 4959 ``\s':state. f2 s' /\ (val = s' ' s)``, 4960 ``\s':state. f1 s' /\ (val = s' ' s)``]th) 4961 ``s':state``)))) 4962 THEN FULL_SIMP_TAC std_ss [RIGHT_AND_OVER_OR] 4963 THEN METIS_TAC[]]); 4964 4965val XP_CONT_def = 4966 Define 4967 `XP_CONT xl c (cont:(state->bool) -> (state->bool)) P = cont(XP xl P c)`; 4968 4969(* General form of an XP_EXEC rule is: 4970 4971 <conditions> 4972 ==> 4973 (XP xl (\s. ?l. (MAP FST l = xl) /\ P(FEMPTY |++ l) /\ (s = FEMPTY |++ (f l))) c = 4974 (\s. ?l. (MAP FST l = xl) /\ P1(FEMPTY |++ l) /\ (s = FEMPTY |++ (f1 l)))) 4975 ORF ... ORF 4976 (\s. ?l. (MAP FST l = xl) /\ Pn(FEMPTY |++ l) /\ (s = FEMPTY |++ (fn l)))) 4977 4978*) 4979 4980val XP_EXEC_SKIP = 4981 store_thm 4982 ("XP_EXEC_SKIP", 4983 ``!xl f (P:(string#value)list->bool). 4984 XP xl (\s. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ (f l))) Skip = 4985 (\s. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ (f l)))``, 4986 REPEAT STRIP_TAC 4987 THEN CONV_TAC (X_FUN_EQ_CONV ``s:state``) 4988 THEN RW_TAC std_ss [XP_def,ORF_def]); 4989 4990val MAP_UPDATE_LIST = 4991 store_thm 4992 ("MAP_UPDATE_LIST", 4993 ``!l xl v x. MEM v xl ==> (MAP FST l = xl) ==> (MAP FST (UPDATE_LIST l (v,x)) = xl)``, 4994 Induct 4995 THEN RW_TAC list_ss [UPDATE_LIST_def] 4996 THENL 4997 [Cases_on `xl` 4998 THEN FULL_SIMP_TAC list_ss [], 4999 Cases_on `h` 5000 THEN FULL_SIMP_TAC list_ss [UPDATE_LIST_def] 5001 THEN Cases_on `v = q` 5002 THEN FULL_SIMP_TAC list_ss [UPDATE_LIST_def]]); 5003 5004val GEN_ASSIGN_FUN_def = 5005 Define 5006 `GEN_ASSIGN_FUN v e l = UPDATE_LIST l (v, naeval e (FEMPTY |++ l))`; 5007 5008val MAP_GEN_ASSIGN_FUN = 5009 store_thm 5010 ("MAP_GEN_ASSIGN_FUN", 5011 ``!f xl v e. 5012 (!l. (MAP FST l = xl) ==> (MAP FST (f l) = xl)) 5013 ==> 5014 MEM v xl 5015 ==> 5016 !l. (MAP FST l = xl) ==> (MAP FST ((GEN_ASSIGN_FUN v e o f) l) = xl)``, 5017 METIS_TAC[MAP_UPDATE_LIST,GEN_ASSIGN_FUN_def,combinTheory.o_THM]); 5018 5019val XP_EXEC_GEN_ASSIGN = 5020 store_thm 5021 ("XP_EXEC_GEN_ASSIGN", 5022 ``!xl (f:(string#value)list->(string#value)list) P v e. 5023 ALL_DISTINCT xl 5024 ==> 5025 (!l. (MAP FST l = xl) ==> (MAP FST (f l) = xl)) 5026 ==> 5027 (XP xl (\s. ?l. (MAP FST l = xl) /\ P l /\ (s = (FEMPTY |++ (f l)))) (GenAssign v e) = 5028 \s. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ (GEN_ASSIGN_FUN v e o f) l))``, 5029 REPEAT STRIP_TAC 5030 THEN CONV_TAC (X_FUN_EQ_CONV ``s:state``) 5031 THEN RW_TAC std_ss [XP_def,ORF_def,Update_def,GEN_ASSIGN_FUN_def] 5032 THEN METIS_TAC[UPDATE_LIST_FUPDATE,DISTINCT_VARS_def]); 5033 5034val ASSIGN_FUN_def = 5035 Define 5036 `ASSIGN_FUN v e l = UPDATE_LIST l (v, Scalar(neval e (FEMPTY |++ l)))`; 5037 5038val MAP_ASSIGN_FUN = 5039 store_thm 5040 ("MAP_ASSIGN_FUN", 5041 ``!f xl. (!l. (MAP FST l = xl) ==> (MAP FST (f l) = xl)) 5042 ==> 5043 !l v e. 5044 MEM v xl 5045 ==> (MAP FST l = xl) 5046 ==> (MAP FST ((ASSIGN_FUN v e o f) l) = MAP FST l)``, 5047 METIS_TAC[MAP_UPDATE_LIST,ASSIGN_FUN_def,combinTheory.o_THM]); 5048 5049 5050val MAP_ASSIGN_FUN = 5051 store_thm 5052 ("MAP_ASSIGN_FUN", 5053 ``!f xl v e. 5054 (!l. (MAP FST l = xl) ==> (MAP FST (f l) = xl)) 5055 ==> 5056 MEM v xl 5057 ==> 5058 !l. (MAP FST l = xl) ==> (MAP FST ((ASSIGN_FUN v e o f) l) = xl)``, 5059 METIS_TAC[MAP_UPDATE_LIST,ASSIGN_FUN_def,combinTheory.o_THM]); 5060 5061val XP_EXEC_ASSIGN = 5062 store_thm 5063 ("XP_EXEC_ASSIGN", 5064 ``!xl (f:(string#value)list->(string#value)list) P v e. 5065 ALL_DISTINCT xl 5066 ==> 5067 (!l. (MAP FST l = xl) ==> (MAP FST (f l) = xl)) 5068 ==> 5069 (XP xl (\s. ?l. (MAP FST l = xl) /\ P l /\ (s = (FEMPTY |++ (f l)))) (Assign v e) = 5070 \s. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ (ASSIGN_FUN v e o f) l))``, 5071 REPEAT STRIP_TAC 5072 THEN CONV_TAC (X_FUN_EQ_CONV ``s:state``) 5073 THEN RW_TAC std_ss [XP_def,ORF_def,Update_def,ASSIGN_FUN_def,Assign_def,naeval_def] 5074 THEN METIS_TAC[UPDATE_LIST_FUPDATE,DISTINCT_VARS_def]); 5075 5076val XP_EXEC_SEQ = 5077 store_thm 5078 ("XP_EXEC_SEQ", 5079 ``!xl f (P:(string#value)list->bool) c1 c2. 5080 XP xl (\s. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ (f l))) (Seq c1 c2) = 5081 XP xl (XP xl (\s. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ (f l))) c1) c2``, 5082 REPEAT STRIP_TAC 5083 THEN CONV_TAC (X_FUN_EQ_CONV ``s:state``) 5084 THEN RW_TAC std_ss [XP_def,ORF_def]); 5085 5086val Lemma1 = 5087 prove 5088 (``(\s. ?l. (MAP FST l = xl) /\ (P l /\ beval b (FEMPTY |++ f l)) /\ (s = FEMPTY |++ f l)) = 5089 (\s. (?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ f l)) /\ beval b s)``, 5090 CONV_TAC(X_FUN_EQ_CONV ``s:state``) 5091 THEN METIS_TAC[]); 5092 5093val Lemma2 = 5094 prove 5095 (``(\s. ?l. (MAP FST l = xl) /\ (P l /\ ~beval b (FEMPTY |++ f l)) /\ (s = FEMPTY |++ f l)) = 5096 (\s. (?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ f l)) /\ ~beval b s)``, 5097 CONV_TAC(X_FUN_EQ_CONV ``s:state``) 5098 THEN METIS_TAC[]); 5099 5100val XP_EXEC_IF = 5101 store_thm 5102 ("XP_EXEC_IF", 5103 ``!xl f (P:(string#value)list->bool) b c1 c2. 5104 XP xl (\s. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ f l)) (Cond b c1 c2) = 5105 (XP xl (\s. ?l. (MAP FST l = xl) /\ ((\l. P l /\ beval b (FEMPTY |++ f l)) l) /\ (s = FEMPTY |++ f l)) c1) 5106 ORF 5107 (XP xl (\s. ?l. (MAP FST l = xl) /\ ((\l. P l /\ ~(beval b (FEMPTY |++ f l))) l) /\ (s = FEMPTY |++ f l)) c2)``, 5108 CONV_TAC(TOP_DEPTH_CONV(X_FUN_EQ_CONV ``s:state``)) 5109 THEN RW_TAC std_ss [XP_def,ORF_def,Lemma1,Lemma2]); 5110 5111val Lemma3 = 5112 prove 5113 (``(\s. ?l'. (MAP FST l' = MAP FST l) /\ (P l' /\ beval b (FEMPTY |++ f l')) /\ (s = FEMPTY |++ f l')) = 5114 (\s. (?l'. (MAP FST l' = MAP FST l) /\ P l' /\ (s = FEMPTY |++ f l')) /\ beval b s)``, 5115 CONV_TAC(X_FUN_EQ_CONV ``s:state``) 5116 THEN METIS_TAC[]); 5117 5118val Lemma4 = 5119 prove 5120 (``(\s. ?l'. (MAP FST l' = MAP FST l) /\ (P l' /\ ~beval b (FEMPTY |++ f l')) /\ (s = FEMPTY |++ f l')) = 5121 (\s. (?l'. (MAP FST l' = MAP FST l) /\ P l' /\ (s = FEMPTY |++ f l')) /\ ~beval b s)``, 5122 CONV_TAC(X_FUN_EQ_CONV ``s:state``) 5123 THEN METIS_TAC[]); 5124 5125val XP_EXEC_IF_ZIP = 5126 store_thm 5127 ("XP_EXEC_IF_ZIP", 5128 ``!xl f f1 f2 (P:(string#value)list->bool) P1 P2 b c1 c2. 5129 (!l. (MAP FST l = xl) ==> (MAP FST (f1 l) = xl)) 5130 ==> 5131 (!l. (MAP FST l = xl) ==> (MAP FST (f2 l) = xl)) 5132 ==> 5133 (XP xl (\s. ?l. (MAP FST l = xl) /\ (P l /\ beval b (FEMPTY |++ f l)) /\ (s = FEMPTY |++ f l)) c1 = 5134 \s. ?l. (MAP FST l = xl) /\ (P1 l /\ beval b (FEMPTY |++ f l)) /\ (s = FEMPTY |++ f1 l)) 5135 ==> 5136 (XP xl (\s. ?l. (MAP FST l = xl) /\ (P l /\ ~(beval b (FEMPTY |++ f l))) /\ (s = FEMPTY |++ f l)) c2 = 5137 \s. ?l. (MAP FST l = xl) /\ (P2 l /\ ~beval b (FEMPTY |++ f l)) /\ (s = FEMPTY |++ f2 l)) 5138 ==> 5139 (XP xl (\s. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ f l)) (Cond b c1 c2) = 5140 \s. ?l. (MAP FST l = xl) 5141 /\ (if (beval b (FEMPTY |++ f l)) then P1 l else P2 l) 5142 /\ (s = FEMPTY |++ ZIP_LIST (beval b (FEMPTY |++ f l)) (f1 l) (f2 l)))``, 5143 CONV_TAC(DEPTH_CONV(RHS_CONV(REWRITE_CONV[GSYM CONJ_ASSOC]))) (* Hack so previous proof can be reused *) 5144 THEN CONV_TAC(TOP_DEPTH_CONV(X_FUN_EQ_CONV ``s:state``)) 5145 THEN RW_TAC std_ss [XP_def,ORF_def] 5146 THEN EQ_TAC 5147 THEN RW_TAC std_ss [] 5148 THENL 5149 [FULL_SIMP_TAC std_ss [Lemma1] 5150 THEN RES_TAC 5151 THEN RW_TAC std_ss [] 5152 THEN Q.EXISTS_TAC `l` 5153 THEN RW_TAC std_ss [] 5154 THEN `LENGTH (f1 l) = LENGTH (f2 l)` by METIS_TAC[rich_listTheory.LENGTH_MAP] 5155 THEN RW_TAC std_ss [ZIP_LIST_T], 5156 FULL_SIMP_TAC std_ss [Lemma2] 5157 THEN RES_TAC 5158 THEN `MAP FST (f1 l) = MAP FST (f2 l)` by METIS_TAC[rich_listTheory.LENGTH_MAP] 5159 THEN RW_TAC std_ss [] 5160 THEN Q.EXISTS_TAC `l` 5161 THEN RW_TAC std_ss [] 5162 THEN `MAP FST (f1 l) = MAP FST (f2 l)` by METIS_TAC[rich_listTheory.LENGTH_MAP] 5163 THEN RW_TAC std_ss [ZIP_LIST_F], 5164 FULL_SIMP_TAC std_ss [Lemma3,Lemma4] 5165 THEN `MAP FST (f1 l) = MAP FST (f2 l)` by METIS_TAC[rich_listTheory.LENGTH_MAP] 5166 THEN `LENGTH (f1 l) = LENGTH (f2 l)` by METIS_TAC[rich_listTheory.LENGTH_MAP] 5167 THEN Cases_on 5168 `(?l'. (MAP FST l' = MAP FST l) /\ P1 l' /\ beval b (FEMPTY |++ f l') /\ 5169 (FEMPTY |++ ZIP_LIST (beval b (FEMPTY |++ f l)) (f1 l) (f2 l) = 5170 FEMPTY |++ f1 l'))` 5171 THEN ASM_REWRITE_TAC [] 5172 THEN Q.EXISTS_TAC `l` 5173 THEN RW_TAC std_ss [] 5174 THEN FULL_SIMP_TAC std_ss [] 5175 THENL 5176 [POP_ASSUM(STRIP_ASSUME_TAC o SIMP_RULE std_ss [] o Q.SPEC `l`) 5177 THEN Cases_on `~beval b (FEMPTY |++ f l)` 5178 THEN FULL_SIMP_TAC std_ss [] 5179 THEN METIS_TAC[ZIP_LIST_T,ZIP_LIST_F], 5180 POP_ASSUM(STRIP_ASSUME_TAC o SIMP_RULE std_ss [] o Q.SPEC `l`) 5181 THEN RW_TAC std_ss [ZIP_LIST_T,ZIP_LIST_F] 5182 THEN Cases_on `beval b (FEMPTY |++ f l)` 5183 THEN FULL_SIMP_TAC std_ss [] 5184 THEN METIS_TAC[ZIP_LIST_T,ZIP_LIST_F], 5185 POP_ASSUM(STRIP_ASSUME_TAC o SIMP_RULE std_ss [] o Q.SPEC `l`) 5186 THENL 5187 [`~(beval b (FEMPTY |++ f l))` by METIS_TAC[] 5188 THEN FULL_SIMP_TAC std_ss [] 5189 THEN METIS_TAC[ZIP_LIST_T,ZIP_LIST_F], 5190 FULL_SIMP_TAC std_ss [] 5191 THEN METIS_TAC[ZIP_LIST_T,ZIP_LIST_F], 5192 Cases_on `beval b (FEMPTY |++ f l)` 5193 THEN FULL_SIMP_TAC std_ss [] 5194 THEN METIS_TAC[ZIP_LIST_T,ZIP_LIST_F]]]]); 5195 5196val Lemma5 = 5197 prove 5198 (``(!l. (MAP FST l = xl) /\ P l ==> beval b (FEMPTY |++ f l)) 5199 ==> 5200 ((\s. (?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ f l)) /\ beval b s) = 5201 (\s. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ f l)))``, 5202 METIS_TAC[]); 5203 5204val Lemma6 = 5205 prove 5206 (``(!l. (MAP FST l = xl) /\ P l ==> beval b (FEMPTY |++ f l)) 5207 ==> 5208 ((\s. (?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ f l)) /\ ~beval b s) = 5209 (\s. F))``, 5210 METIS_TAC[]); 5211 5212val XP_EXEC_IF_T = 5213 store_thm 5214 ("XP_EXEC_IF_T", 5215 ``!xl f (P:(string#value)list->bool) b c1 c2. 5216 SIMPLE c2 5217 ==> 5218 (!l. (MAP FST l = xl) ==> P l ==> beval b (FEMPTY |++ f l)) 5219 ==> 5220 (XP xl (\s. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ f l)) (Cond b c1 c2) = 5221 XP xl (\s. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ f l)) c1)``, 5222 CONV_TAC(TOP_DEPTH_CONV(X_FUN_EQ_CONV ``s:state``)) 5223 THEN SIMP_TAC std_ss [XP_def,ORF_def] 5224 THEN SIMP_TAC std_ss [Lemma1,Lemma2] 5225 THEN RW_TAC std_ss [Lemma5,Lemma6] 5226 THEN METIS_TAC[XP_F]); 5227 5228val Lemma7 = 5229 prove 5230 (``(!l. (MAP FST l = xl) /\ P l ==> ~(beval b (FEMPTY |++ f l))) 5231 ==> 5232 ((\s. (?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ f l)) /\ beval b s) = 5233 (\s. F))``, 5234 METIS_TAC[]); 5235 5236val Lemma8 = 5237 prove 5238 (``(!l. (MAP FST l = xl) /\ P l ==> ~(beval b (FEMPTY |++ f l))) 5239 ==> 5240 ((\s. (?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ f l)) /\ ~beval b s) = 5241 (\s. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ f l)))``, 5242 METIS_TAC[]); 5243 5244val XP_EXEC_IF_F = 5245 store_thm 5246 ("XP_EXEC_IF_F", 5247 ``!xl f (P:(string#value)list->bool) b c1 c2. 5248 SIMPLE c1 5249 ==> 5250 (!l. (MAP FST l = xl) ==> P l ==> ~(beval b (FEMPTY |++ f l))) 5251 ==> 5252 (XP xl (\s. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ f l)) (Cond b c1 c2) = 5253 XP xl (\s. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ f l)) c2)``, 5254 CONV_TAC(TOP_DEPTH_CONV(X_FUN_EQ_CONV ``s:state``)) 5255 THEN SIMP_TAC std_ss [XP_def,ORF_def] 5256 THEN SIMP_TAC std_ss [Lemma1,Lemma2] 5257 THEN RW_TAC std_ss [Lemma7,Lemma8] 5258 THEN METIS_TAC[XP_F]); 5259 5260val ANWHILE_PRED_def = 5261 Define 5262 `ANWHILE_PRED xl (P:(string#value)list->bool) n b s = 5263 (?l. (MAP FST l = xl) /\ P l) /\ int_gt (neval n s) 0i /\ ~(beval b s)`; 5264 5265val XP_EXEC_ANWHILE = 5266 store_thm 5267 ("XP_EXEC_ANWHILE", 5268 ``!xl (f:(string#value)list->(string#value)list) P c n b. 5269 ALL_DISTINCT xl 5270 ==> 5271 (XP xl (\s. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ (f l))) (AnWhile b n c) = 5272 \s. ?l. (MAP FST l = xl) /\ (ANWHILE_PRED xl P n b o ($|++ FEMPTY)) l /\ (s = FEMPTY |++ (I l)))``, 5273 RW_TAC std_ss [XP_def,ORF_def,ANWHILE_PRED_def] 5274 THEN METIS_TAC[S2L,FDOM_SET,MAP_S2L]); 5275 5276val Lemma9 = 5277 prove 5278 (``(\s. ?l. (MAP FST l = xl) /\ P l /\ (val = s ' v) /\ (s = FEMPTY |++ f l)) 5279 = 5280 (\s. (?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ f l)) /\ (val = s ' v))``, 5281 CONV_TAC FUN_EQ_CONV 5282 THEN RW_TAC std_ss [] 5283 THEN METIS_TAC[]); 5284 5285val Lemma10 = 5286 prove 5287 (``(\s. (?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ f l)) /\ (val = s ' v)) 5288 = 5289 (\s. ?l. (MAP FST l = xl) /\ P l /\ (val = s ' v) /\ (s = FEMPTY |++ f l))``, 5290 CONV_TAC FUN_EQ_CONV 5291 THEN RW_TAC std_ss [] 5292 THEN METIS_TAC[]); 5293 5294val XP_EXEC_LOCAL_LEMMA = 5295 store_thm 5296 ("XP_EXEC_LOCAL_LEMMA", 5297 ``!xl f (P:(string#value)list->bool) v c. 5298 XP xl (\s. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ (f l))) (Local v c) = 5299 \s''. ?s' val. XP xl (\s. ?l. (MAP FST l = xl) /\ P l /\ (val = s ' v) /\ (s = FEMPTY |++ (f l))) c s'/\ (s'' = s' |+ (v,val))``, 5300 REPEAT STRIP_TAC 5301 THEN CONV_TAC (X_FUN_EQ_CONV ``s:state``) 5302 THEN RW_TAC std_ss [XP_def] 5303 THEN EQ_TAC 5304 THEN RW_TAC std_ss [] 5305 THENL 5306 [Q.EXISTS_TAC `s'` THEN Q.EXISTS_TAC `val` 5307 THEN RW_TAC std_ss [Lemma9], 5308 Q.EXISTS_TAC `s'` THEN Q.EXISTS_TAC `val` 5309 THEN RW_TAC std_ss [Lemma10]]); 5310 5311val LOCAL_PRED_def = 5312 Define 5313 `LOCAL_PRED (P:(string#value)list->bool) f v val l = 5314 P l /\ (val = LOOKUP (f l) v)`; 5315 5316val Lemma11 = 5317 prove 5318 (``!xl f (P:(string#value)list->bool) v. 5319 ALL_DISTINCT xl 5320 ==> 5321 (!l. (MAP FST l = xl) ==> (MAP FST (f l) = xl)) 5322 ==> 5323 ((\s. ?l. (MAP FST l = xl) /\ P l /\ (val = s ' v) /\ (s = FEMPTY |++ f l)) 5324 = 5325 (\s. ?l. (MAP FST l = xl) /\ LOCAL_PRED P f v val l /\ (s = FEMPTY |++ f l)))``, 5326 CONV_TAC(DEPTH_CONV FUN_EQ_CONV) 5327 THEN METIS_TAC[XP_EXEC_LOCAL_LEMMA,DISTINCT_VARS_def,STATE_LOOKUP,LOCAL_PRED_def]); 5328 5329val XP_EXEC_LOCAL = 5330 store_thm 5331 ("XP_EXEC_LOCAL", 5332 ``!xl f (P:(string#value)list->bool) v c. 5333 ALL_DISTINCT xl 5334 ==> 5335 (!l. (MAP FST l = xl) ==> (MAP FST (f l) = xl)) 5336 ==> 5337 (XP xl (\s. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ (f l))) (Local v c) = 5338 \s''. ?s' val. 5339 XP xl (\s. ?l. (MAP FST l = xl) /\ LOCAL_PRED P f v val l /\ (s = FEMPTY |++ (f l))) c s' 5340 /\ (s'' = s' |+ (v,val)))``, 5341 CONV_TAC (DEPTH_CONV(X_FUN_EQ_CONV ``s:state``)) 5342 THEN RW_TAC std_ss [XP_EXEC_LOCAL_LEMMA,Lemma11]); 5343 5344val FVC_def = 5345 Define 5346 `(FVC xl P Skip = T) 5347 /\ 5348 (FVC xl P (GenAssign v e) = T) 5349 /\ 5350 (FVC xl P (Seq c1 c2) = FVC xl P c1 /\ FVC xl (XP xl P c1) c2) 5351 /\ 5352 (FVC xl P (Cond b c1 c2) = FVC xl (\s. P s /\ beval b s) c1 /\ FVC xl (\s. P s /\ ~(beval b s)) c2) 5353 /\ 5354 (FVC xl P (AnWhile b n c) = (!s. P s ==> int_gt (neval n s) 0i) /\ SPEC (\s. int_gt (neval n s) 0i /\ beval b s) c (\s. int_gt (neval n s) 0i) /\ FVC xl P c) 5355 /\ 5356 (FVC xl P (Local v c) = !val. FVC xl (\s. P s /\ (val = s ' v)) c)`; 5357 5358val VARS_SUBSET_FDOM = 5359 store_thm 5360 ("VARS_SUBSET_FDOM", 5361 ``!c s1 s2. 5362 EVAL c s1 s2 5363 ==> 5364 SIMPLE c ==> VARS c SUBSET FDOM s1 ==> !xl P. FVC xl P c ==> (FDOM s1 = FDOM s2)``, 5365 HO_MATCH_MP_TAC sinduction 5366 THEN RW_TAC std_ss 5367 [SIMPLE_def,VARS_def,SKIP_THM,GEN_ASSIGN_THM,SEQ_THM,IF_THM, 5368 Update_def,FDOM_FUPDATE,SUBSET_DEF,IN_SING,FVC_def] 5369 THEN METIS_TAC[ABSORPTION,IN_UNION,SUBSET_DEF,DOMSUB_NOT_IN_DOM,IN_INSERT]); 5370 5371val PDOM_XP = 5372 store_thm 5373 ("PDOM_XP", 5374 ``!c. SIMPLE c ==> !P. VARS c SUBSET (set xl) ==> PDOM xl P ==> PDOM xl (XP xl P c)``, 5375 Induct 5376 THEN RW_TAC std_ss [SIMPLE_def,PDOM_def,XP_def,ORF_def] 5377 THEN FULL_SIMP_TAC std_ss [PDOM_def,Update_def,FDOM_FUPDATE,VARS_def,SUBSET_DEF,IN_SING] 5378 THENL 5379 [METIS_TAC[ABSORPTION], 5380 METIS_TAC[IN_UNION], 5381 ASSUM_LIST 5382 (fn thl => ASSUME_TAC(Q.SPEC `(\s. P s /\ beval b s)` (el 7 thl))) 5383 THEN FULL_SIMP_TAC std_ss [] 5384 THEN METIS_TAC[IN_UNION], 5385 ASSUM_LIST 5386 (fn thl => ASSUME_TAC(Q.SPEC `(\s. P s /\ ~beval b s)` (el 6 thl))) 5387 THEN FULL_SIMP_TAC std_ss [] 5388 THEN METIS_TAC[IN_UNION], 5389 ASSUM_LIST(fn thl => MAP_EVERY UNDISCH_TAC (map concl thl)) 5390 THEN REPEAT STRIP_TAC 5391 THEN ASSUM_LIST 5392 (fn thl => ASSUME_TAC(SPEC ``(\s':state. P s' /\ (val = s' ' s))`` (el 5 thl))) 5393 THEN POP_ASSUM(fn th => ASSUME_TAC(SIMP_RULE std_ss [] th)) 5394 THEN FULL_SIMP_TAC list_ss [IN_INSERT] 5395 THEN `FDOM s''' = set xl` by METIS_TAC[] 5396 THEN RW_TAC std_ss [] 5397 THEN `s IN set xl` by METIS_TAC[listTheory.IN_LIST_TO_SET] 5398 THEN METIS_TAC[ABSORPTION]]); 5399 5400val XP_FVC_SPEC = 5401 store_thm 5402 ("XP_FVC_SPEC", 5403 ``!c P xl. SIMPLE c /\ VARS c SUBSET (set xl) ==> PDOM xl P ==> FVC xl P c ==> SPEC P c (XP xl P c)``, 5404 Induct 5405 THEN RW_TAC std_ss [SIMPLE_def,XP_def,ORF_def] 5406 THENL 5407 [RW_TAC std_ss [SPEC_def,XP_def,ORF_def,FVC_def,SKIP_THM], 5408 RW_TAC std_ss [SPEC_def,XP_def,ORF_def,FVC_def,GEN_ASSIGN_THM] THEN METIS_TAC[], 5409 FULL_SIMP_TAC std_ss [SPEC_def,XP_def,ORF_def,FVC_def,SEQ_THM,VARS_def,UNION_SUBSET] 5410 THEN RW_TAC std_ss [] 5411 THEN `XP xl P c s2'` by METIS_TAC[] 5412 THEN METIS_TAC[PDOM_XP], 5413 FULL_SIMP_TAC std_ss [SPEC_def,XP_def,ORF_def,FVC_def,IF_THM,VARS_def,UNION_SUBSET,PDOM_def] 5414 THEN RW_TAC std_ss [] 5415 THENL 5416 [ASSUM_LIST 5417 (fn thl => 5418 ASSUME_TAC(SIMP_RULE std_ss[] (Q.ISPEC `\s. P s /\ beval b s` (el 12 thl)))) 5419 THEN METIS_TAC[], 5420 ASSUM_LIST 5421 (fn thl => 5422 ASSUME_TAC(SIMP_RULE std_ss[] (Q.ISPEC `\s. P s /\ ~(beval b s)` (el 11 thl)))) 5423 THEN METIS_TAC[]], 5424 FULL_SIMP_TAC std_ss [XP_def,ORF_def,FVC_def] 5425 THEN RW_TAC std_ss [] 5426 THEN IMP_RES_TAC(SIMP_RULE std_ss [VALID_def]POST_DERIVED_ANWHILE_RULE) 5427 THEN `SPEC P (AnWhile b n c) (\s. int_gt (neval n s) 0i /\ ~beval b s)`by METIS_TAC[] 5428 THEN POP_ASSUM(ASSUME_TAC o REWRITE_RULE[SPEC_def]) 5429 THEN REWRITE_TAC[SPEC_def] 5430 THEN RW_TAC std_ss [] 5431 THEN TRY(METIS_TAC[]) 5432 THEN FULL_SIMP_TAC std_ss [PDOM_def] 5433 THEN `set xl = FDOM s1` by METIS_TAC[] 5434 THEN `SIMPLE(AnWhile b n c)` by METIS_TAC[SIMPLE_def] 5435 THEN `FVC xl P (AnWhile b n c) ==> (FDOM s1 = FDOM s2)` by METIS_TAC[VARS_SUBSET_FDOM] 5436 THEN METIS_TAC 5437 [SPECL 5438 [``xl:string list``,``P:pred``,``b:bexp``,``n:nexp``,``c:program``] 5439 (el 5 (CONJUNCTS FVC_def))], 5440 FULL_SIMP_TAC std_ss [XP_def,FVC_def,LOCAL_THM,VARS_def,SPEC_def,INSERT_SUBSET,PDOM_def] 5441 THEN RW_TAC std_ss [] 5442 THEN RES_TAC 5443 THEN RW_TAC std_ss [] 5444 THEN Q.EXISTS_TAC `s3` THEN Q.EXISTS_TAC `s1 ' s` 5445 THEN RW_TAC std_ss [] 5446 THEN ASSUM_LIST 5447 (fn thl => ASSUME_TAC(GEN_ALL(SIMP_RULE std_ss thl (SPECL[``(\s':state. P s' /\ (val = s' ' s))``,``xl:string list``] (el 11 thl))))) 5448 THEN METIS_TAC[]]); 5449 5450val VARS_IN_VARS = 5451 store_thm 5452 ("VARS_IN_VARS", 5453 ``!l c. VARS_IN c l = VARS c SUBSET set (MAP FST l)``, 5454 RW_TAC list_ss [VARS_IN_def,SUBSET_DEF]); 5455 5456local 5457val Lemma = 5458 prove 5459 (``(!l:(string#value)list. (MAP FST l = xl) ==> (MAP FST (f l) = xl)) 5460 ==> 5461 PDOM 5462 xl 5463 (\s:state. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ (f l)))``, 5464 RW_TAC std_ss [PDOM_def] 5465 THEN RW_TAC std_ss [PDOM_def,FDOM_SET]); 5466in 5467val XP_FVC_SPEC_COR = 5468 store_thm 5469 ("XP_FVC_SPEC_COR", 5470 ``!xl f P c. 5471 SIMPLE c 5472 ==> 5473 (!l:(string#value)list. (MAP FST l = xl) ==> (MAP FST (f l) = xl)) 5474 ==> 5475 (VARS c SUBSET (set xl)) 5476 ==> 5477 FVC xl (\s. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ (f l))) c 5478 ==> 5479 SPEC 5480 (\s. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ (f l))) 5481 c 5482 (XP xl (\s. ?l. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ (f l))) c)``, 5483 RW_TAC std_ss [] 5484 THEN ASSUME_TAC 5485 (SPECL 5486 [``c : program``, 5487 ``\s:state. ?l:(string#value)list. (MAP FST l = xl) /\ P l /\ (s = FEMPTY |++ (f l))``, 5488 ``xl : string list``] 5489 XP_FVC_SPEC) 5490 THEN ASSUM_LIST 5491 (fn thl => 5492 ASSUME_TAC 5493 (SIMP_RULE std_ss 5494 [el 2 thl,el 3 thl,el 5 thl, MP Lemma (el 4 thl)] 5495 (el 1 thl))) 5496 THEN RW_TAC std_ss []) 5497end; 5498 5499val UNWIND_LEMMA = 5500 store_thm 5501 ("UNWIND_LEMMA", 5502 ``!(l:(string#value)list) P. 5503 (\s. (s = FEMPTY |++ l) /\ P s) = \s. (s = FEMPTY |++ l) /\ P(FEMPTY |++ l)``, 5504 RW_TAC std_ss [] 5505 THEN CONV_TAC FUN_EQ_CONV 5506 THEN RW_TAC std_ss [] 5507 THEN EQ_TAC 5508 THEN RW_TAC std_ss [] 5509 THEN METIS_TAC[]); 5510 5511val MAP_FST_EXPAND_NIL = 5512 store_thm 5513 ("MAP_FST_EXPAND_NIL", 5514 ``!P. (?l:(string#value)list. (MAP FST l = []) /\ P l) = P[]``, 5515 RW_TAC list_ss []); 5516 5517val MAP_FST_EXPAND1 = 5518 prove 5519 (``!l x xl. 5520 (MAP FST l = x::xl) /\ P l 5521 ==> 5522 ?v l'. (MAP FST l' = xl) /\ P((x,v)::l')``, 5523 Induct 5524 THEN RW_TAC list_ss [] 5525 THEN Q.EXISTS_TAC `SND h` 5526 THEN RW_TAC list_ss [] 5527 THEN METIS_TAC[]); 5528 5529val MAP_FST_EXPAND2 = 5530 prove 5531 (``!l' x v xl. (MAP FST l' = xl) /\ P((x,v)::l') ==> ?l. (MAP FST l = x::xl) /\ P l``, 5532 Induct 5533 THEN RW_TAC list_ss [] 5534 THENL 5535 [Q.EXISTS_TAC `[(x,v)]` 5536 THEN RW_TAC list_ss [], 5537 Q.EXISTS_TAC `((x,v)::h::l')` 5538 THEN RW_TAC list_ss []]); 5539 5540val MAP_FST_EXPAND = 5541 store_thm 5542 ("MAP_FST_EXPAND", 5543 ``!P x xl. 5544 (?(l:(string#value)list). (MAP FST l = x::xl) /\ P l) = 5545 (?l. (MAP FST l = xl) /\ ?v. P((x,v)::l))``, 5546 METIS_TAC[MAP_FST_EXPAND1,MAP_FST_EXPAND2]); 5547 5548val MAP_FST_FORALL_EXPAND_NIL = 5549 store_thm 5550 ("MAP_FST_FORALL_EXPAND_NIL", 5551 ``!P. (!l:(string#value)list. (MAP FST l = []) ==> P l) = P[]``, 5552 RW_TAC list_ss []); 5553 5554val MAP_FST_FORALL_EXPAND1 = 5555 prove 5556 (``!xl x. 5557 (!l. (MAP FST l = x::xl) ==> P l) 5558 ==> 5559 !v l'. (MAP FST l' = xl) ==> P((x,v)::l')``, 5560 Induct 5561 THEN RW_TAC list_ss []); 5562 5563val MAP_FST_FORALL_EXPAND2 = 5564 prove 5565 (``!xl x. (!l' v. (MAP FST l' = xl) ==> P((x,v)::l')) ==> !l. (MAP FST l = x::xl) ==> P l``, 5566 REPEAT GEN_TAC THEN STRIP_TAC 5567 THEN Induct 5568 THEN RW_TAC list_ss [] 5569 THEN METIS_TAC[pairTheory.PAIR]); 5570 5571val MAP_FST_FORALL_EXPAND = 5572 store_thm 5573 ("MAP_FST_FORALL_EXPAND", 5574 ``!P x xl. 5575 (!(l:(string#value)list). (MAP FST l = x::xl) ==> P l) = 5576 (!l. (MAP FST l = xl) ==> !v. P((x,v)::l))``, 5577 METIS_TAC[MAP_FST_FORALL_EXPAND1,MAP_FST_FORALL_EXPAND2]); 5578 5579 5580 5581 5582