author | wenzelm |
Sun, 16 Jan 2011 15:53:03 +0100 | |
changeset 41589 | bbd861837ebc |
parent 37736 | 2bf3a2cb5e58 |
child 42174 | d0be2722ce9f |
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.thy |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
2 |
Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
3 |
*) |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
4 |
|
12431 | 5 |
header "Expressions" |
6 |
||
16417 | 7 |
theory Expr imports Main begin |
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
8 |
|
12431 | 9 |
text {* |
10 |
Arithmetic expressions and Boolean expressions. |
|
11 |
Not used in the rest of the language, but included for completeness. |
|
12 |
*} |
|
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
13 |
|
12431 | 14 |
subsection "Arithmetic expressions" |
12546 | 15 |
typedecl loc |
12431 | 16 |
|
17 |
types |
|
18 |
state = "loc => nat" |
|
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 |
datatype |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
21 |
aexp = N nat |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
22 |
| X loc |
12546 | 23 |
| Op1 "nat => nat" aexp |
24 |
| Op2 "nat => nat => nat" aexp aexp |
|
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
25 |
|
12431 | 26 |
subsection "Evaluation of arithmetic expressions" |
23746 | 27 |
|
28 |
inductive |
|
29 |
evala :: "[aexp*state,nat] => bool" (infixl "-a->" 50) |
|
30 |
where |
|
12431 | 31 |
N: "(N(n),s) -a-> n" |
23746 | 32 |
| X: "(X(x),s) -a-> s(x)" |
33 |
| Op1: "(e,s) -a-> n ==> (Op1 f e,s) -a-> f(n)" |
|
34 |
| Op2: "[| (e0,s) -a-> n0; (e1,s) -a-> n1 |] |
|
12431 | 35 |
==> (Op2 f e0 e1,s) -a-> f n0 n1" |
36 |
||
37 |
lemmas [intro] = N X Op1 Op2 |
|
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
38 |
|
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
39 |
|
12431 | 40 |
subsection "Boolean expressions" |
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
41 |
|
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
42 |
datatype |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
43 |
bexp = true |
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
44 |
| false |
12546 | 45 |
| ROp "nat => nat => bool" aexp aexp |
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
46 |
| noti bexp |
22818 | 47 |
| andi bexp bexp (infixl "andi" 60) |
48 |
| ori bexp bexp (infixl "ori" 60) |
|
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
49 |
|
12431 | 50 |
subsection "Evaluation of boolean expressions" |
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
51 |
|
23746 | 52 |
inductive |
53 |
evalb :: "[bexp*state,bool] => bool" (infixl "-b->" 50) |
|
12431 | 54 |
-- "avoid clash with ML constructors true, false" |
23746 | 55 |
where |
12431 | 56 |
tru: "(true,s) -b-> True" |
23746 | 57 |
| fls: "(false,s) -b-> False" |
58 |
| ROp: "[| (a0,s) -a-> n0; (a1,s) -a-> n1 |] |
|
12431 | 59 |
==> (ROp f a0 a1,s) -b-> f n0 n1" |
23746 | 60 |
| noti: "(b,s) -b-> w ==> (noti(b),s) -b-> (~w)" |
61 |
| andi: "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] |
|
1729 | 62 |
==> (b0 andi b1,s) -b-> (w0 & w1)" |
23746 | 63 |
| ori: "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] |
12431 | 64 |
==> (b0 ori b1,s) -b-> (w0 | w1)" |
65 |
||
66 |
lemmas [intro] = tru fls ROp noti andi ori |
|
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
67 |
|
12431 | 68 |
subsection "Denotational semantics of arithmetic and boolean expressions" |
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
69 |
|
27362 | 70 |
primrec A :: "aexp => state => nat" |
71 |
where |
|
1900 | 72 |
"A(N(n)) = (%s. n)" |
27362 | 73 |
| "A(X(x)) = (%s. s(x))" |
74 |
| "A(Op1 f a) = (%s. f(A a s))" |
|
75 |
| "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))" |
|
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
76 |
|
27362 | 77 |
primrec B :: "bexp => state => bool" |
78 |
where |
|
1900 | 79 |
"B(true) = (%s. True)" |
27362 | 80 |
| "B(false) = (%s. False)" |
81 |
| "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))" |
|
82 |
| "B(noti(b)) = (%s. ~(B b s))" |
|
83 |
| "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))" |
|
84 |
| "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))" |
|
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
85 |
|
37736
2bf3a2cb5e58
replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps
bulwahn
parents:
27362
diff
changeset
|
86 |
inductive_simps |
2bf3a2cb5e58
replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps
bulwahn
parents:
27362
diff
changeset
|
87 |
evala_simps [simp]: |
2bf3a2cb5e58
replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps
bulwahn
parents:
27362
diff
changeset
|
88 |
"(N(n),s) -a-> n'" |
2bf3a2cb5e58
replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps
bulwahn
parents:
27362
diff
changeset
|
89 |
"(X(x),sigma) -a-> i" |
2bf3a2cb5e58
replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps
bulwahn
parents:
27362
diff
changeset
|
90 |
"(Op1 f e,sigma) -a-> i" |
2bf3a2cb5e58
replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps
bulwahn
parents:
27362
diff
changeset
|
91 |
"(Op2 f a1 a2,sigma) -a-> i" |
2bf3a2cb5e58
replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps
bulwahn
parents:
27362
diff
changeset
|
92 |
"((true,sigma) -b-> w)" |
2bf3a2cb5e58
replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps
bulwahn
parents:
27362
diff
changeset
|
93 |
"((false,sigma) -b-> w)" |
2bf3a2cb5e58
replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps
bulwahn
parents:
27362
diff
changeset
|
94 |
"((ROp f a0 a1,sigma) -b-> w)" |
2bf3a2cb5e58
replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps
bulwahn
parents:
27362
diff
changeset
|
95 |
"((noti(b),sigma) -b-> w)" |
2bf3a2cb5e58
replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps
bulwahn
parents:
27362
diff
changeset
|
96 |
"((b0 andi b1,sigma) -b-> w)" |
2bf3a2cb5e58
replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps
bulwahn
parents:
27362
diff
changeset
|
97 |
"((b0 ori b1,sigma) -b-> w)" |
12431 | 98 |
|
99 |
||
18372 | 100 |
lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)" |
20503 | 101 |
by (induct a arbitrary: n) auto |
12431 | 102 |
|
12546 | 103 |
lemma bexp_iff: |
18372 | 104 |
"((b,s) -b-> w) = (B b s = w)" |
20503 | 105 |
by (induct b arbitrary: w) (auto simp add: aexp_iff) |
12431 | 106 |
|
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset
|
107 |
end |