author | wenzelm |
Mon, 12 Jul 2010 21:38:37 +0200 | |
changeset 37781 | 2fbbf0a48cef |
parent 36862 | 952b2b102a0a |
child 39246 | 9e58f0499f57 |
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 |
|
23 |
consts |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
24 |
evala :: "('a => nat) => 'a aexp => nat" |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
25 |
evalb :: "('a => nat) => 'a bexp => bool" |
5737 | 26 |
|
27 |
primrec |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
28 |
"evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)" |
5802 | 29 |
"evala env (Sum a1 a2) = evala env a1 + evala env a2" |
30 |
"evala env (Diff a1 a2) = evala env a1 - evala env a2" |
|
31 |
"evala env (Var v) = env v" |
|
32 |
"evala env (Num n) = n" |
|
5737 | 33 |
|
5802 | 34 |
"evalb env (Less a1 a2) = (evala env a1 < evala env a2)" |
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
35 |
"evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)" |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
36 |
"evalb env (Neg b) = (\<not> evalb env b)" |
5737 | 37 |
|
38 |
||
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
39 |
text {* \medskip Substitution on arithmetic and boolean expressions *} |
5737 | 40 |
|
41 |
consts |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
42 |
substa :: "('a => 'b aexp) => 'a aexp => 'b aexp" |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
43 |
substb :: "('a => 'b aexp) => 'a bexp => 'b bexp" |
5737 | 44 |
|
45 |
primrec |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
46 |
"substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)" |
5802 | 47 |
"substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)" |
48 |
"substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)" |
|
49 |
"substa f (Var v) = f v" |
|
50 |
"substa f (Num n) = Num n" |
|
5737 | 51 |
|
5802 | 52 |
"substb f (Less a1 a2) = Less (substa f a1) (substa f a2)" |
53 |
"substb f (And b1 b2) = And (substb f b1) (substb f b2)" |
|
54 |
"substb f (Neg b) = Neg (substb f b)" |
|
5737 | 55 |
|
12171 | 56 |
lemma subst1_aexp: |
57 |
"evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a" |
|
58 |
and subst1_bexp: |
|
59 |
"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
|
60 |
-- {* one variable *} |
12171 | 61 |
by (induct a and b) simp_all |
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
62 |
|
12171 | 63 |
lemma subst_all_aexp: |
64 |
"evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a" |
|
65 |
and subst_all_bexp: |
|
66 |
"evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b" |
|
67 |
by (induct a and b) auto |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5802
diff
changeset
|
68 |
|
5737 | 69 |
end |