author | berghofe |
Fri, 24 Jul 1998 13:03:20 +0200 | |
changeset 5183 | 89f162de39cf |
parent 5069 | 3ea049f7979d |
child 5223 | 4cb05273f764 |
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 |
open Expr; |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
11 |
|
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
12 |
val evala_elim_cases = map (evala.mk_cases aexp.simps) |
1729 | 13 |
["(N(n),sigma) -a-> i", "(X(x),sigma) -a-> i", |
14 |
"(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
|
15 |
]; |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
16 |
|
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
17 |
val evalb_elim_cases = map (evalb.mk_cases bexp.simps) |
1729 | 18 |
["(true,sigma) -b-> x", "(false,sigma) -b-> x", |
19 |
"(ROp f a0 a1,sigma) -b-> x", "(noti(b),sigma) -b-> x", |
|
20 |
"(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
|
21 |
]; |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
22 |
|
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
23 |
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
|
24 |
(fn _ => [fast_tac (HOL_cs addSIs evalb.intrs addSEs evalb_elim_cases) 1])) |
1729 | 25 |
["((true,sigma) -b-> w) = (w=True)", |
26 |
"((false,sigma) -b-> w) = (w=False)", |
|
27 |
"((ROp f a0 a1,sigma) -b-> w) = \ |
|
28 |
\ (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))", |
|
29 |
"((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))", |
|
30 |
"((b0 andi b1,sigma) -b-> w) = \ |
|
31 |
\ (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))", |
|
32 |
"((b0 ori b1,sigma) -b-> w) = \ |
|
33 |
\ (? 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
|
34 |
|
5069 | 35 |
Goal "!n. ((a,s) -a-> n) = (A a s = n)"; |
5183 | 36 |
by (induct_tac "a" 1); |
4303 | 37 |
by (ALLGOALS |
38 |
(fast_tac (claset() addSIs evala.intrs |
|
39 |
addSEs evala_elim_cases addss (simpset())))); |
|
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
40 |
qed_spec_mp "aexp_iff"; |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
41 |
|
5069 | 42 |
Goal "!w. ((b,s) -b-> w) = (B b s = w)"; |
5183 | 43 |
by (induct_tac "b" 1); |
4303 | 44 |
by (ALLGOALS |
45 |
(fast_tac (claset() |
|
46 |
addss (simpset() addsimps (aexp_iff::evalb_simps))))); |
|
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
47 |
qed_spec_mp "bexp_iff"; |