src/HOL/Induct/ABexp.thy
 author berghofe Fri, 23 Oct 1998 12:55:36 +0200 changeset 5737 31fc1d0e66d5 child 5802 614f2f30781a permissions -rw-r--r--
New example for using the datatype package: Arithmetic and boolean expressions.
```
(*  Title:      HOL/Induct/ABexp.thy
ID:         \$Id\$
Author:     Stefan Berghofer, TU Muenchen

Arithmetic and boolean expressions
*)

ABexp = Main +

datatype
'a aexp = If_then_else ('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)
| Or ('a bexp) ('a bexp)

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

consts
eval_aexp :: "['a => nat, 'a aexp] => nat"
eval_bexp :: "['a => nat, 'a bexp] => bool"

primrec
"eval_aexp env (If_then_else b a1 a2) =
(if eval_bexp env b then eval_aexp env a1 else eval_aexp env a2)"
"eval_aexp env (Sum a1 a2) = eval_aexp env a1 + eval_aexp env a2"
"eval_aexp env (Diff a1 a2) = eval_aexp env a1 - eval_aexp env a2"
"eval_aexp env (Var v) = env v"
"eval_aexp env (Num n) = n"

"eval_bexp env (Less a1 a2) = (eval_aexp env a1 < eval_aexp env a2)"
"eval_bexp env (And b1 b2) = (eval_bexp env b1 & eval_bexp env b2)"
"eval_bexp env (Or b1 b2) = (eval_bexp env b1 & eval_bexp env b2)"

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

consts
subst_aexp :: "['a => 'b aexp, 'a aexp] => 'b aexp"
subst_bexp :: "['a => 'b aexp, 'a bexp] => 'b bexp"

primrec
"subst_aexp f (If_then_else b a1 a2) =
If_then_else (subst_bexp f b) (subst_aexp f a1) (subst_aexp f a2)"
"subst_aexp f (Sum a1 a2) = Sum (subst_aexp f a1) (subst_aexp f a2)"
"subst_aexp f (Diff a1 a2) = Diff (subst_aexp f a1) (subst_aexp f a2)"
"subst_aexp f (Var v) = f v"
"subst_aexp f (Num n) = Num n"

"subst_bexp f (Less a1 a2) = Less (subst_aexp f a1) (subst_aexp f a2)"
"subst_bexp f (And b1 b2) = And (subst_bexp f b1) (subst_bexp f b2)"
"subst_bexp f (Or b1 b2) = Or (subst_bexp f b1) (subst_bexp f b2)"

end
```