|
1 (* Title: HOL/IMP/Com.ML |
|
2 ID: $Id$ |
|
3 Author: Heiko Loetzbeyer & Robert Sandner, TUM |
|
4 Copyright 1994 TUM |
|
5 *) |
|
6 |
|
7 open Com; |
|
8 |
|
9 val evala_elim_cases = map (evala.mk_cases aexp.simps) |
|
10 ["<N(n),sigma> -a-> i", "<X(x),sigma> -a-> i", |
|
11 "<Op1 f e,sigma> -a-> i", "<Op2 f a1 a2,sigma> -a-> i" |
|
12 ]; |
|
13 |
|
14 val evalb_elim_cases = map (evalb.mk_cases bexp.simps) |
|
15 ["<true,sigma> -b-> x", "<false,sigma> -b-> x", |
|
16 "<ROp f a0 a1,sigma> -b-> x", "<noti(b),sigma> -b-> x", |
|
17 "<b0 andi b1,sigma> -b-> x", "<b0 ori b1,sigma> -b-> x" |
|
18 ]; |
|
19 |
|
20 val evalb_simps = map (fn s => prove_goal Com.thy s |
|
21 (fn _ => [fast_tac (HOL_cs addSIs evalb.intrs addSEs evalb_elim_cases) 1])) |
|
22 ["(<true,sigma> -b-> w) = (w=True)", |
|
23 "(<false,sigma> -b-> w) = (w=False)", |
|
24 "(<ROp f a0 a1,sigma> -b-> w) = \ |
|
25 \ (? m. <a0,sigma> -a-> m & (? n. <a1,sigma> -a-> n & w = f m n))", |
|
26 "(<noti(b),sigma> -b-> w) = (? x. <b,sigma> -b-> x & w = (~x))", |
|
27 "(<b0 andi b1,sigma> -b-> w) = \ |
|
28 \ (? x. <b0,sigma> -b-> x & (? y. <b1,sigma> -b-> y & w = (x&y)))", |
|
29 "(<b0 ori b1,sigma> -b-> w) = \ |
|
30 \ (? x. <b0,sigma> -b-> x & (? y. <b1,sigma> -b-> y & w = (x|y)))"]; |