1 (* Title: HOL/IMP/Expr.thy |
|
2 Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM |
|
3 *) |
|
4 |
|
5 header "Expressions" |
|
6 |
|
7 theory Expr imports Main begin |
|
8 |
|
9 text {* |
|
10 Arithmetic expressions and Boolean expressions. |
|
11 Not used in the rest of the language, but included for completeness. |
|
12 *} |
|
13 |
|
14 subsection "Arithmetic expressions" |
|
15 typedecl loc |
|
16 |
|
17 type_synonym state = "loc => nat" |
|
18 |
|
19 datatype |
|
20 aexp = N nat |
|
21 | X loc |
|
22 | Op1 "nat => nat" aexp |
|
23 | Op2 "nat => nat => nat" aexp aexp |
|
24 |
|
25 subsection "Evaluation of arithmetic expressions" |
|
26 |
|
27 inductive |
|
28 evala :: "[aexp*state,nat] => bool" (infixl "-a->" 50) |
|
29 where |
|
30 N: "(N(n),s) -a-> n" |
|
31 | X: "(X(x),s) -a-> s(x)" |
|
32 | Op1: "(e,s) -a-> n ==> (Op1 f e,s) -a-> f(n)" |
|
33 | Op2: "[| (e0,s) -a-> n0; (e1,s) -a-> n1 |] |
|
34 ==> (Op2 f e0 e1,s) -a-> f n0 n1" |
|
35 |
|
36 lemmas [intro] = N X Op1 Op2 |
|
37 |
|
38 |
|
39 subsection "Boolean expressions" |
|
40 |
|
41 datatype |
|
42 bexp = true |
|
43 | false |
|
44 | ROp "nat => nat => bool" aexp aexp |
|
45 | noti bexp |
|
46 | andi bexp bexp (infixl "andi" 60) |
|
47 | ori bexp bexp (infixl "ori" 60) |
|
48 |
|
49 subsection "Evaluation of boolean expressions" |
|
50 |
|
51 inductive |
|
52 evalb :: "[bexp*state,bool] => bool" (infixl "-b->" 50) |
|
53 -- "avoid clash with ML constructors true, false" |
|
54 where |
|
55 tru: "(true,s) -b-> True" |
|
56 | fls: "(false,s) -b-> False" |
|
57 | ROp: "[| (a0,s) -a-> n0; (a1,s) -a-> n1 |] |
|
58 ==> (ROp f a0 a1,s) -b-> f n0 n1" |
|
59 | noti: "(b,s) -b-> w ==> (noti(b),s) -b-> (~w)" |
|
60 | andi: "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] |
|
61 ==> (b0 andi b1,s) -b-> (w0 & w1)" |
|
62 | ori: "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] |
|
63 ==> (b0 ori b1,s) -b-> (w0 | w1)" |
|
64 |
|
65 lemmas [intro] = tru fls ROp noti andi ori |
|
66 |
|
67 subsection "Denotational semantics of arithmetic and boolean expressions" |
|
68 |
|
69 primrec A :: "aexp => state => nat" |
|
70 where |
|
71 "A(N(n)) = (%s. n)" |
|
72 | "A(X(x)) = (%s. s(x))" |
|
73 | "A(Op1 f a) = (%s. f(A a s))" |
|
74 | "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))" |
|
75 |
|
76 primrec B :: "bexp => state => bool" |
|
77 where |
|
78 "B(true) = (%s. True)" |
|
79 | "B(false) = (%s. False)" |
|
80 | "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))" |
|
81 | "B(noti(b)) = (%s. ~(B b s))" |
|
82 | "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))" |
|
83 | "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))" |
|
84 |
|
85 inductive_simps |
|
86 evala_simps [simp]: |
|
87 "(N(n),s) -a-> n'" |
|
88 "(X(x),sigma) -a-> i" |
|
89 "(Op1 f e,sigma) -a-> i" |
|
90 "(Op2 f a1 a2,sigma) -a-> i" |
|
91 "((true,sigma) -b-> w)" |
|
92 "((false,sigma) -b-> w)" |
|
93 "((ROp f a0 a1,sigma) -b-> w)" |
|
94 "((noti(b),sigma) -b-> w)" |
|
95 "((b0 andi b1,sigma) -b-> w)" |
|
96 "((b0 ori b1,sigma) -b-> w)" |
|
97 |
|
98 |
|
99 lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)" |
|
100 by (induct a arbitrary: n) auto |
|
101 |
|
102 lemma bexp_iff: |
|
103 "((b,s) -b-> w) = (B b s = w)" |
|
104 by (induct b arbitrary: w) (auto simp add: aexp_iff) |
|
105 |
|
106 end |
|