1 2open HolKernel Parse boolLib bossLib; 3open stringLib integerTheory; 4open lcsymtacs; 5val ect = BasicProvers.EVERY_CASE_TAC; 6 7val _ = new_theory "imp"; 8 9(* 10 11This file defines a funcional big-step semantics for the IMP languages 12of Nipkow and Klein's book Concrete Semantics. 13 14http://www.concrete-semantics.org/ 15 16*) 17 18val _ = temp_type_abbrev("vname",``:string``); 19 20val _ = Datatype ` 21 aexp = N int | V vname | Plus aexp aexp`; 22 23val _ = Datatype ` 24 bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp`; 25 26val _ = Datatype ` 27 com = SKIP 28 | Assign vname aexp 29 | Seq com com 30 | If bexp com com 31 | While bexp com` 32 33val aval_def = Define ` 34 (aval (N n) s = n) /\ 35 (aval (V x) s = s x) /\ 36 (aval (Plus a1 a2) s = aval a1 s + aval a2 s)`; 37 38val bval_def = Define ` 39 (bval (Bc v) s = v) /\ 40 (bval (Not b) s = ~bval b s) /\ 41 (bval (And b1 b2) s = bval b1 s /\ bval b2 s) /\ 42 (bval (Less a1 a2) s = aval a1 s < aval a2 s)`; 43 44val STOP_def = Define `STOP x = x`; 45 46(* The following function defines the semantics of statement evaluation. 47 The clock decreases when entering the body of the While loop. 48 49 NB: the definition mechanism in HOL4 is not smart enough to notice 50 that the clock doesn't increase. In order to make the termination 51 simple, we insert an extra `if t < t2 then t else t2` in the Seq 52 case. In cval_def_with_stop below, we remove this redundant 53 if-statement. *) 54 55val cval_def = tDefine "cval" ` 56 (cval SKIP s (t:num) = SOME (s,t)) /\ 57 (cval (Assign x a) s t = SOME ((x =+ aval a s) s,t)) /\ 58 (cval (Seq c1 c2) s t = 59 case cval c1 s t of 60 | NONE => NONE 61 | SOME (s2,t2) => cval c2 s2 (if t < t2 then t else t2)) /\ 62 (cval (If b c1 c2) s t = 63 cval (if bval b s then c1 else c2) s t) /\ 64 (cval (While b c) s t = 65 if bval b s then 66 if t = 0 then NONE else cval (Seq c (STOP (While b c))) s (t - 1) 67 else SOME (s,t))` 68 (WF_REL_TAC `inv_image (measure I LEX measure com_size) 69 (\(c,s,t). (t,c))` 70 \\ SRW_TAC [] [] \\ DECIDE_TAC) 71 72val clock_bound = prove( 73 ``!c s t s' t'. (cval c s t = SOME (s',t')) ==> t' <= t``, 74 recInduct (theorem "cval_ind") \\ rpt strip_tac 75 \\ fs [cval_def] \\ ect \\ fs [] \\ decide_tac); 76 77fun term_rewrite tms = let 78 fun f tm = ASSUME (list_mk_forall(free_vars tm,tm)) 79 in rand o concl o QCONV (REWRITE_CONV (map f tms)) end 80 81val r = term_rewrite [``(if t < t2 then t else t2) = t2:num``]; 82 83val cval_def_with_stop = store_thm("cval_def_with_stop", 84 cval_def |> concl |> r, 85 REPEAT STRIP_TAC \\ SIMP_TAC std_ss [Once cval_def] 86 \\ ect \\ imp_res_tac clock_bound \\ `r = t` by DECIDE_TAC \\ fs []); 87 88val cval_def = 89 save_thm("cval_def",REWRITE_RULE [STOP_def] cval_def_with_stop); 90 91(* We also remove the redundant if-statement from the induction theorem. *) 92 93val cval_ind = prove( 94 theorem "cval_ind" |> concl |> r, 95 NTAC 2 STRIP_TAC \\ HO_MATCH_MP_TAC (theorem "cval_ind") 96 \\ REPEAT STRIP_TAC \\ fs [] 97 \\ FIRST_X_ASSUM MATCH_MP_TAC \\ fs [] 98 \\ REPEAT STRIP_TAC \\ fs [STOP_def] 99 \\ RES_TAC \\ imp_res_tac clock_bound 100 \\ Cases_on `t < t2` \\ fs [] 101 \\ `t = t2` by DECIDE_TAC \\ fs []) |> REWRITE_RULE [STOP_def]; 102 103val _ = save_thm("cval_ind",cval_ind); 104 105val _ = export_theory(); 106