src/HOL/Induct/ABexp.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 16417 9bc16273c2d4
child 36862 952b2b102a0a
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
     1 (*  Title:      HOL/Induct/ABexp.thy
     2     ID:         $Id$
     3     Author:     Stefan Berghofer, TU Muenchen
     4 *)
     5 
     6 header {* Arithmetic and boolean expressions *}
     7 
     8 theory ABexp imports Main begin
     9 
    10 datatype 'a aexp =
    11     IF "'a bexp"  "'a aexp"  "'a aexp"
    12   | Sum "'a aexp"  "'a aexp"
    13   | Diff "'a aexp"  "'a aexp"
    14   | Var 'a
    15   | Num nat
    16 and 'a bexp =
    17     Less "'a aexp"  "'a aexp"
    18   | And "'a bexp"  "'a bexp"
    19   | Neg "'a bexp"
    20 
    21 
    22 text {* \medskip Evaluation of arithmetic and boolean expressions *}
    23 
    24 consts
    25   evala :: "('a => nat) => 'a aexp => nat"
    26   evalb :: "('a => nat) => 'a bexp => bool"
    27 
    28 primrec
    29   "evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)"
    30   "evala env (Sum a1 a2) = evala env a1 + evala env a2"
    31   "evala env (Diff a1 a2) = evala env a1 - evala env a2"
    32   "evala env (Var v) = env v"
    33   "evala env (Num n) = n"
    34 
    35   "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
    36   "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"
    37   "evalb env (Neg b) = (\<not> evalb env b)"
    38 
    39 
    40 text {* \medskip Substitution on arithmetic and boolean expressions *}
    41 
    42 consts
    43   substa :: "('a => 'b aexp) => 'a aexp => 'b aexp"
    44   substb :: "('a => 'b aexp) => 'a bexp => 'b bexp"
    45 
    46 primrec
    47   "substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)"
    48   "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
    49   "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
    50   "substa f (Var v) = f v"
    51   "substa f (Num n) = Num n"
    52 
    53   "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
    54   "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
    55   "substb f (Neg b) = Neg (substb f b)"
    56 
    57 lemma subst1_aexp:
    58   "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a"
    59 and subst1_bexp:
    60   "evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
    61     --  {* one variable *}
    62   by (induct a and b) simp_all
    63 
    64 lemma subst_all_aexp:
    65   "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a"
    66 and subst_all_bexp:
    67   "evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
    68   by (induct a and b) auto
    69 
    70 end