src/HOL/Induct/ABexp.thy
changeset 5737 31fc1d0e66d5
child 5802 614f2f30781a
equal deleted inserted replaced
5736:8a1be8e50d9f 5737:31fc1d0e66d5
       
     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
       
    12   'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp)
       
    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)
       
    20           | Or ('a bexp) ('a bexp)
       
    21 
       
    22 
       
    23 (** evaluation of arithmetic and boolean expressions **)
       
    24 
       
    25 consts
       
    26   eval_aexp :: "['a => nat, 'a aexp] => nat"
       
    27   eval_bexp :: "['a => nat, 'a bexp] => bool"
       
    28 
       
    29 primrec
       
    30   "eval_aexp env (If_then_else b a1 a2) =
       
    31      (if eval_bexp env b then eval_aexp env a1 else eval_aexp env a2)"
       
    32   "eval_aexp env (Sum a1 a2) = eval_aexp env a1 + eval_aexp env a2"
       
    33   "eval_aexp env (Diff a1 a2) = eval_aexp env a1 - eval_aexp env a2"
       
    34   "eval_aexp env (Var v) = env v"
       
    35   "eval_aexp env (Num n) = n"
       
    36 
       
    37   "eval_bexp env (Less a1 a2) = (eval_aexp env a1 < eval_aexp env a2)"
       
    38   "eval_bexp env (And b1 b2) = (eval_bexp env b1 & eval_bexp env b2)"
       
    39   "eval_bexp env (Or b1 b2) = (eval_bexp env b1 & eval_bexp env b2)"
       
    40 
       
    41 
       
    42 (** substitution on arithmetic and boolean expressions **)
       
    43 
       
    44 consts
       
    45   subst_aexp :: "['a => 'b aexp, 'a aexp] => 'b aexp"
       
    46   subst_bexp :: "['a => 'b aexp, 'a bexp] => 'b bexp"
       
    47 
       
    48 primrec
       
    49   "subst_aexp f (If_then_else b a1 a2) =
       
    50      If_then_else (subst_bexp f b) (subst_aexp f a1) (subst_aexp f a2)"
       
    51   "subst_aexp f (Sum a1 a2) = Sum (subst_aexp f a1) (subst_aexp f a2)"
       
    52   "subst_aexp f (Diff a1 a2) = Diff (subst_aexp f a1) (subst_aexp f a2)"
       
    53   "subst_aexp f (Var v) = f v"
       
    54   "subst_aexp f (Num n) = Num n"
       
    55 
       
    56   "subst_bexp f (Less a1 a2) = Less (subst_aexp f a1) (subst_aexp f a2)"
       
    57   "subst_bexp f (And b1 b2) = And (subst_bexp f b1) (subst_bexp f b2)"
       
    58   "subst_bexp f (Or b1 b2) = Or (subst_bexp f b1) (subst_bexp f b2)"
       
    59 
       
    60 end