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