5 |
5 |
6 Arithmetic expressions and Boolean expressions. |
6 Arithmetic expressions and Boolean expressions. |
7 Not used in the rest of the language, but included for completeness. |
7 Not used in the rest of the language, but included for completeness. |
8 *) |
8 *) |
9 |
9 |
10 val evala_elim_cases = map (evala.mk_cases aexp.simps) |
10 val evala_elim_cases = |
11 ["(N(n),sigma) -a-> i", "(X(x),sigma) -a-> i", |
11 map evala.mk_cases |
12 "(Op1 f e,sigma) -a-> i", "(Op2 f a1 a2,sigma) -a-> i" |
12 ["(N(n),sigma) -a-> i", |
13 ]; |
13 "(X(x),sigma) -a-> i", |
|
14 "(Op1 f e,sigma) -a-> i", |
|
15 "(Op2 f a1 a2,sigma) -a-> i"]; |
14 |
16 |
15 val evalb_elim_cases = map (evalb.mk_cases bexp.simps) |
17 val evalb_elim_cases = |
16 ["(true,sigma) -b-> x", "(false,sigma) -b-> x", |
18 map evalb.mk_cases |
17 "(ROp f a0 a1,sigma) -b-> x", "(noti(b),sigma) -b-> x", |
19 ["(true,sigma) -b-> x", |
18 "(b0 andi b1,sigma) -b-> x", "(b0 ori b1,sigma) -b-> x" |
20 "(false,sigma) -b-> x", |
19 ]; |
21 "(ROp f a0 a1,sigma) -b-> x", |
|
22 "(noti(b),sigma) -b-> x", |
|
23 "(b0 andi b1,sigma) -b-> x", |
|
24 "(b0 ori b1,sigma) -b-> x"]; |
20 |
25 |
21 val evalb_simps = map (fn s => prove_goal Expr.thy s |
26 val evalb_simps = map (fn s => prove_goal Expr.thy s |
22 (fn _ => [fast_tac (HOL_cs addSIs evalb.intrs addSEs evalb_elim_cases) 1])) |
27 (fn _ => [fast_tac (HOL_cs addSIs evalb.intrs addSEs evalb_elim_cases) 1])) |
23 ["((true,sigma) -b-> w) = (w=True)", |
28 ["((true,sigma) -b-> w) = (w=True)", |
24 "((false,sigma) -b-> w) = (w=False)", |
29 "((false,sigma) -b-> w) = (w=False)", |