5737
|
1 |
(* Title: HOL/Induct/ABexp.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Stefan Berghofer, TU Muenchen
|
|
4 |
Copyright 1998 TU Muenchen
|
|
5 |
|
|
6 |
Arithmetic and boolean expressions
|
|
7 |
*)
|
|
8 |
|
|
9 |
ABexp = Main +
|
|
10 |
|
|
11 |
datatype
|
5802
|
12 |
'a aexp = IF ('a bexp) ('a aexp) ('a aexp)
|
5737
|
13 |
| Sum ('a aexp) ('a aexp)
|
|
14 |
| Diff ('a aexp) ('a aexp)
|
|
15 |
| Var 'a
|
|
16 |
| Num nat
|
|
17 |
and
|
|
18 |
'a bexp = Less ('a aexp) ('a aexp)
|
|
19 |
| And ('a bexp) ('a bexp)
|
5802
|
20 |
| Neg ('a bexp)
|
5737
|
21 |
|
|
22 |
|
|
23 |
(** evaluation of arithmetic and boolean expressions **)
|
|
24 |
|
|
25 |
consts
|
5802
|
26 |
evala :: ('a => nat) => 'a aexp => nat
|
|
27 |
evalb :: ('a => nat) => 'a bexp => bool
|
5737
|
28 |
|
|
29 |
primrec
|
5802
|
30 |
"evala env (IF b a1 a2) =
|
|
31 |
(if evalb env b then evala env a1 else evala env a2)"
|
|
32 |
"evala env (Sum a1 a2) = evala env a1 + evala env a2"
|
|
33 |
"evala env (Diff a1 a2) = evala env a1 - evala env a2"
|
|
34 |
"evala env (Var v) = env v"
|
|
35 |
"evala env (Num n) = n"
|
5737
|
36 |
|
5802
|
37 |
"evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
|
|
38 |
"evalb env (And b1 b2) = (evalb env b1 & evalb env b2)"
|
|
39 |
"evalb env (Neg b) = (~ evalb env b)"
|
5737
|
40 |
|
|
41 |
|
|
42 |
(** substitution on arithmetic and boolean expressions **)
|
|
43 |
|
|
44 |
consts
|
5802
|
45 |
substa :: ('a => 'b aexp) => 'a aexp => 'b aexp
|
|
46 |
substb :: ('a => 'b aexp) => 'a bexp => 'b bexp
|
5737
|
47 |
|
|
48 |
primrec
|
5802
|
49 |
"substa f (IF b a1 a2) =
|
|
50 |
IF (substb f b) (substa f a1) (substa f a2)"
|
|
51 |
"substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
|
|
52 |
"substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
|
|
53 |
"substa f (Var v) = f v"
|
|
54 |
"substa f (Num n) = Num n"
|
5737
|
55 |
|
5802
|
56 |
"substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
|
|
57 |
"substb f (And b1 b2) = And (substb f b1) (substb f b2)"
|
|
58 |
"substb f (Neg b) = Neg (substb f b)"
|
5737
|
59 |
|
|
60 |
end
|