src/HOL/Induct/ABexp.thy
 author nipkow Thu, 05 Nov 1998 14:05:57 +0100 changeset 5802 614f2f30781a parent 5737 31fc1d0e66d5 child 11046 b5f5942781a0 permissions -rw-r--r--
Shortened names and added new thm.
```
(*  Title:      HOL/Induct/ABexp.thy
ID:         \$Id\$
Author:     Stefan Berghofer, TU Muenchen

Arithmetic and boolean expressions
*)

ABexp = Main +

datatype
'a aexp = IF ('a bexp) ('a aexp) ('a aexp)
| Sum ('a aexp) ('a aexp)
| Diff ('a aexp) ('a aexp)
| Var 'a
| Num nat
and
'a bexp = Less ('a aexp) ('a aexp)
| And ('a bexp) ('a bexp)
| Neg ('a bexp)

(** evaluation of arithmetic and boolean expressions **)

consts
evala :: ('a => nat) => 'a aexp => nat
evalb :: ('a => nat) => 'a bexp => bool

primrec
"evala env (IF b a1 a2) =
(if evalb env b then evala env a1 else evala env a2)"
"evala env (Sum a1 a2) = evala env a1 + evala env a2"
"evala env (Diff a1 a2) = evala env a1 - evala env a2"
"evala env (Var v) = env v"
"evala env (Num n) = n"

"evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
"evalb env (And b1 b2) = (evalb env b1 & evalb env b2)"
"evalb env (Neg b) = (~ evalb env b)"

(** substitution on arithmetic and boolean expressions **)

consts
substa :: ('a => 'b aexp) => 'a aexp => 'b aexp
substb :: ('a => 'b aexp) => 'a bexp => 'b bexp

primrec
"substa f (IF b a1 a2) =
IF (substb f b) (substa f a1) (substa f a2)"
"substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
"substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
"substa f (Var v) = f v"
"substa f (Num n) = Num n"

"substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
"substb f (And b1 b2) = And (substb f b1) (substb f b2)"
"substb f (Neg b) = Neg (substb f b)"

end
```