# Theory ABexp

Up to index of Isabelle/HOL/Induct

theory ABexp
imports Main
begin

    (*  Title:      HOL/Induct/ABexp.thy
        ID:         $Id: ABexp.thy,v 1.7 2005/06/17 14:13:07 haftmann Exp $
        Author:     Stefan Berghofer, TU Muenchen
    *)

    header {* Arithmetic and boolean expressions *}

    theory ABexp imports Main begin

    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"

    text {* \medskip 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)"

    text {* \medskip 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)"

    lemma subst1_aexp:
      "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a"
    and subst1_bexp:
      "evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
        --  {* one variable *}
      by (induct a and b) simp_all

    lemma subst_all_aexp:
      "evala env (substa s a) = evala (λx. evala env (s x)) a"
    and subst_all_bexp:
      "evalb env (substb s b) = evalb (λx. evala env (s x)) b"
      by (induct a and b) auto

    end

lemma subst1_aexp:

      evala env (substa (Var(v := a')) a) = evala (env(v := evala env a')) a

and subst1_bexp:

      evalb env (substb (Var(v := a')) b) = evalb (env(v := evala env a')) b

lemma subst_all_aexp:

      evala env (substa s a) = evala (%x. evala env (s x)) a

and subst_all_bexp:

      evalb env (substb s b) = evalb (%x. evala env (s x)) b