1open preamble lprefix_lubTheory
2
3val _ = new_theory "while_lang";
4
5Type nat[pp] = ���:num���;
6
7(* -- AST and other types -- *)
8
9Type name  = ���: string         ���
10Type value = ���: nat            ���
11Type store = ���: name -> value  ���
12Type exp   = ���: store -> value ���
13
14Datatype:
15  prog = Skip
16       | Assign name exp
17       | Print exp
18       | Seq prog prog
19       | If exp prog prog
20       | While exp prog
21End
22
23
24(* -- small-step semantics -- *)
25
26Type output    = ���: value list     ���
27Type state[pp] = ���: store # output ���
28
29Definition output_of_def:
30  output_of ((s,out):state) = out
31End
32
33Definition subst_def:
34  subst n e (s,out) = ((n =+ e s) s,out:value list)
35End
36
37Definition print_def:
38  print e ((s,out):state) = (s,out ++ [e s])
39End
40
41Definition guard_def:
42  guard x ((s,out):state) = (x s ��� 0)
43End
44
45Inductive step:
46  (���s:state.
47    step (Skip,s) (Skip,s))
48  ���
49  (���s n x.
50     step (Assign n x,s) (Skip, subst n x s))
51  ���
52  (���s x.
53     step (Print x,s) (Skip, print x s))
54  ���
55  (���s q.
56     step (Seq Skip q,s) (q,s))
57  ���
58  (���p0 p1 q s0 s1.
59     step (p0,s0) (p1,s1) ��� p0 ��� Skip ���
60     step (Seq p0 q,s0) (Seq p1 q,s1))
61  ���
62  (���x p q s.
63     step (If x p q, s) ((if guard x s then p else q), s))
64  ���
65  (���x p s.
66     step (While x p, s) (If x (Seq p (While x p)) Skip, s))
67End
68
69Inductive terminates:
70  ���s p t. RTC step (p,s) (Skip,t) ��� terminates s p t
71End
72
73Inductive diverges:
74  ���s p output.
75    (���t. ~(terminates s p t)) ���
76    output = LUB { fromList out | ���q t. RTC step (p,s) (q,t,out) }
77    ���
78    diverges s p output
79End
80
81val _ = export_theory();
82