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
