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
berghofe@5737
     1
(*  Title:      HOL/Induct/ABexp.thy
berghofe@5737
     2
    ID:         $Id$
berghofe@5737
     3
    Author:     Stefan Berghofer, TU Muenchen
berghofe@5737
     4
*)
berghofe@5737
     5
wenzelm@11046
     6
header {* Arithmetic and boolean expressions *}
wenzelm@11046
     7
haftmann@16417
     8
theory ABexp imports Main begin
berghofe@5737
     9
wenzelm@11046
    10
datatype 'a aexp =
wenzelm@11046
    11
    IF "'a bexp"  "'a aexp"  "'a aexp"
wenzelm@11046
    12
  | Sum "'a aexp"  "'a aexp"
wenzelm@11046
    13
  | Diff "'a aexp"  "'a aexp"
wenzelm@11046
    14
  | Var 'a
wenzelm@11046
    15
  | Num nat
wenzelm@11046
    16
and 'a bexp =
wenzelm@11046
    17
    Less "'a aexp"  "'a aexp"
wenzelm@11046
    18
  | And "'a bexp"  "'a bexp"
wenzelm@11046
    19
  | Neg "'a bexp"
berghofe@5737
    20
berghofe@5737
    21
wenzelm@11046
    22
text {* \medskip Evaluation of arithmetic and boolean expressions *}
berghofe@5737
    23
berghofe@5737
    24
consts
wenzelm@11046
    25
  evala :: "('a => nat) => 'a aexp => nat"
wenzelm@11046
    26
  evalb :: "('a => nat) => 'a bexp => bool"
berghofe@5737
    27
berghofe@5737
    28
primrec
wenzelm@11046
    29
  "evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)"
nipkow@5802
    30
  "evala env (Sum a1 a2) = evala env a1 + evala env a2"
nipkow@5802
    31
  "evala env (Diff a1 a2) = evala env a1 - evala env a2"
nipkow@5802
    32
  "evala env (Var v) = env v"
nipkow@5802
    33
  "evala env (Num n) = n"
berghofe@5737
    34
nipkow@5802
    35
  "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
wenzelm@11046
    36
  "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"
wenzelm@11046
    37
  "evalb env (Neg b) = (\<not> evalb env b)"
berghofe@5737
    38
berghofe@5737
    39
wenzelm@11046
    40
text {* \medskip Substitution on arithmetic and boolean expressions *}
berghofe@5737
    41
berghofe@5737
    42
consts
wenzelm@11046
    43
  substa :: "('a => 'b aexp) => 'a aexp => 'b aexp"
wenzelm@11046
    44
  substb :: "('a => 'b aexp) => 'a bexp => 'b bexp"
berghofe@5737
    45
berghofe@5737
    46
primrec
wenzelm@11046
    47
  "substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)"
nipkow@5802
    48
  "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
nipkow@5802
    49
  "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
nipkow@5802
    50
  "substa f (Var v) = f v"
nipkow@5802
    51
  "substa f (Num n) = Num n"
berghofe@5737
    52
nipkow@5802
    53
  "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
nipkow@5802
    54
  "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
nipkow@5802
    55
  "substb f (Neg b) = Neg (substb f b)"
berghofe@5737
    56
wenzelm@12171
    57
lemma subst1_aexp:
wenzelm@12171
    58
  "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a"
wenzelm@12171
    59
and subst1_bexp:
wenzelm@12171
    60
  "evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
wenzelm@11046
    61
    --  {* one variable *}
wenzelm@12171
    62
  by (induct a and b) simp_all
wenzelm@11046
    63
wenzelm@12171
    64
lemma subst_all_aexp:
wenzelm@12171
    65
  "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a"
wenzelm@12171
    66
and subst_all_bexp:
wenzelm@12171
    67
  "evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
wenzelm@12171
    68
  by (induct a and b) auto
wenzelm@11046
    69
berghofe@5737
    70
end