author | nipkow |
Tue, 05 Jan 1999 17:27:59 +0100 | |
changeset 6059 | aa00e235ea27 |
parent 5535 | 678999604ee9 |
child 6141 | a6922171b396 |
permissions | -rw-r--r-- |
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
1 |
(* Title: HOL/IMP/Expr.ML |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
3 |
Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
4 |
Copyright 1994 TUM |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
5 |
|
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
6 |
Arithmetic expressions and Boolean expressions. |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
7 |
Not used in the rest of the language, but included for completeness. |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
8 |
*) |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
9 |
|
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
10 |
val evala_elim_cases = map (evala.mk_cases aexp.simps) |
1729 | 11 |
["(N(n),sigma) -a-> i", "(X(x),sigma) -a-> i", |
12 |
"(Op1 f e,sigma) -a-> i", "(Op2 f a1 a2,sigma) -a-> i" |
|
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
13 |
]; |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
14 |
|
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
15 |
val evalb_elim_cases = map (evalb.mk_cases bexp.simps) |
1729 | 16 |
["(true,sigma) -b-> x", "(false,sigma) -b-> x", |
17 |
"(ROp f a0 a1,sigma) -b-> x", "(noti(b),sigma) -b-> x", |
|
18 |
"(b0 andi b1,sigma) -b-> x", "(b0 ori b1,sigma) -b-> x" |
|
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
19 |
]; |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
20 |
|
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
21 |
val evalb_simps = map (fn s => prove_goal Expr.thy s |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
22 |
(fn _ => [fast_tac (HOL_cs addSIs evalb.intrs addSEs evalb_elim_cases) 1])) |
1729 | 23 |
["((true,sigma) -b-> w) = (w=True)", |
24 |
"((false,sigma) -b-> w) = (w=False)", |
|
25 |
"((ROp f a0 a1,sigma) -b-> w) = \ |
|
26 |
\ (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))", |
|
27 |
"((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))", |
|
28 |
"((b0 andi b1,sigma) -b-> w) = \ |
|
29 |
\ (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))", |
|
30 |
"((b0 ori b1,sigma) -b-> w) = \ |
|
31 |
\ (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"]; |
|
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
32 |
|
5069 | 33 |
Goal "!n. ((a,s) -a-> n) = (A a s = n)"; |
5183 | 34 |
by (induct_tac "a" 1); |
5535 | 35 |
by (auto_tac (claset() addSIs evala.intrs addSEs evala_elim_cases, |
36 |
simpset())); |
|
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
37 |
qed_spec_mp "aexp_iff"; |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
38 |
|
5069 | 39 |
Goal "!w. ((b,s) -b-> w) = (B b s = w)"; |
5183 | 40 |
by (induct_tac "b" 1); |
5535 | 41 |
by (auto_tac (claset(), |
42 |
simpset() addsimps aexp_iff::evalb_simps)); |
|
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
43 |
qed_spec_mp "bexp_iff"; |