src/HOL/Induct/ABexp.thy

deleted rogue copy of localTo_imp_o_localTo

(*  Title:      HOL/Induct/ABexp.thy
    ID:         $Id$
    Author:     Stefan Berghofer, TU Muenchen
    Copyright   1998  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