author | haftmann |
Wed, 08 Sep 2010 19:21:46 +0200 | |
changeset 39246 | 9e58f0499f57 |
parent 36862 | 952b2b102a0a |
child 46914 | c2ca2c3d23a6 |
permissions | -rw-r--r-- |
5737 | 1 |
(* Title: HOL/Induct/ABexp.thy |
2 |
Author: Stefan Berghofer, TU Muenchen |
|
3 |
*) |
|
4 |
||
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
5 |
header {* Arithmetic and boolean expressions *} |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
6 |
|
16417 | 7 |
theory ABexp imports Main begin |
5737 | 8 |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
9 |
datatype 'a aexp = |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
10 |
IF "'a bexp" "'a aexp" "'a aexp" |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
11 |
| Sum "'a aexp" "'a aexp" |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
12 |
| Diff "'a aexp" "'a aexp" |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
13 |
| Var 'a |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
14 |
| Num nat |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
15 |
and 'a bexp = |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
16 |
Less "'a aexp" "'a aexp" |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
17 |
| And "'a bexp" "'a bexp" |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
18 |
| Neg "'a bexp" |
5737 | 19 |
|
20 |
||
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
21 |
text {* \medskip Evaluation of arithmetic and boolean expressions *} |
5737 | 22 |
|
39246 | 23 |
primrec evala :: "('a => nat) => 'a aexp => nat" |
24 |
and evalb :: "('a => nat) => 'a bexp => bool" where |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
25 |
"evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)" |
39246 | 26 |
| "evala env (Sum a1 a2) = evala env a1 + evala env a2" |
27 |
| "evala env (Diff a1 a2) = evala env a1 - evala env a2" |
|
28 |
| "evala env (Var v) = env v" |
|
29 |
| "evala env (Num n) = n" |
|
5737 | 30 |
|
39246 | 31 |
| "evalb env (Less a1 a2) = (evala env a1 < evala env a2)" |
32 |
| "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)" |
|
33 |
| "evalb env (Neg b) = (\<not> evalb env b)" |
|
5737 | 34 |
|
35 |
||
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
36 |
text {* \medskip Substitution on arithmetic and boolean expressions *} |
5737 | 37 |
|
39246 | 38 |
primrec substa :: "('a => 'b aexp) => 'a aexp => 'b aexp" |
39 |
and substb :: "('a => 'b aexp) => 'a bexp => 'b bexp" where |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
40 |
"substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)" |
39246 | 41 |
| "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)" |
42 |
| "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)" |
|
43 |
| "substa f (Var v) = f v" |
|
44 |
| "substa f (Num n) = Num n" |
|
5737 | 45 |
|
39246 | 46 |
| "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)" |
47 |
| "substb f (And b1 b2) = And (substb f b1) (substb f b2)" |
|
48 |
| "substb f (Neg b) = Neg (substb f b)" |
|
5737 | 49 |
|
12171 | 50 |
lemma subst1_aexp: |
51 |
"evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a" |
|
52 |
and subst1_bexp: |
|
53 |
"evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b" |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
54 |
-- {* one variable *} |
12171 | 55 |
by (induct a and b) simp_all |
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
56 |
|
12171 | 57 |
lemma subst_all_aexp: |
58 |
"evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a" |
|
59 |
and subst_all_bexp: |
|
60 |
"evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b" |
|
61 |
by (induct a and b) auto |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
62 |
|
5737 | 63 |
end |