src/HOL/Induct/ABexp.thy
 author wenzelm Sun Nov 02 18:21:45 2014 +0100 (2014-11-02) changeset 58889 5b7a9633cfa8 parent 58310 91ea607a34d8 child 60530 44f9873d6f6f permissions -rw-r--r--
```     1 (*  Title:      HOL/Induct/ABexp.thy
```
```     2     Author:     Stefan Berghofer, TU Muenchen
```
```     3 *)
```
```     4
```
```     5 section {* Arithmetic and boolean expressions *}
```
```     6
```
```     7 theory ABexp
```
```     8 imports Main
```
```     9 begin
```
```    10
```
```    11 datatype 'a aexp =
```
```    12     IF "'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 'a bexp =
```
```    18     Less "'a aexp"  "'a aexp"
```
```    19   | And "'a bexp"  "'a bexp"
```
```    20   | Neg "'a bexp"
```
```    21
```
```    22
```
```    23 text {* \medskip Evaluation of arithmetic and boolean expressions *}
```
```    24
```
```    25 primrec evala :: "('a => nat) => 'a aexp => nat"
```
```    26   and evalb :: "('a => nat) => 'a bexp => bool"
```
```    27 where
```
```    28   "evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)"
```
```    29 | "evala env (Sum a1 a2) = evala env a1 + evala env a2"
```
```    30 | "evala env (Diff a1 a2) = evala env a1 - evala env a2"
```
```    31 | "evala env (Var v) = env v"
```
```    32 | "evala env (Num n) = n"
```
```    33
```
```    34 | "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
```
```    35 | "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"
```
```    36 | "evalb env (Neg b) = (\<not> evalb env b)"
```
```    37
```
```    38
```
```    39 text {* \medskip Substitution on arithmetic and boolean expressions *}
```
```    40
```
```    41 primrec substa :: "('a => 'b aexp) => 'a aexp => 'b aexp"
```
```    42   and substb :: "('a => 'b aexp) => 'a bexp => 'b bexp"
```
```    43 where
```
```    44   "substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)"
```
```    45 | "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
```
```    46 | "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
```
```    47 | "substa f (Var v) = f v"
```
```    48 | "substa f (Num n) = Num n"
```
```    49
```
```    50 | "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
```
```    51 | "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
```
```    52 | "substb f (Neg b) = Neg (substb f b)"
```
```    53
```
```    54 lemma subst1_aexp:
```
```    55   "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a"
```
```    56 and subst1_bexp:
```
```    57   "evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
```
```    58     --  {* one variable *}
```
```    59   by (induct a and b) simp_all
```
```    60
```
```    61 lemma subst_all_aexp:
```
```    62   "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a"
```
```    63 and subst_all_bexp:
```
```    64   "evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
```
```    65   by (induct a and b) auto
```
```    66
```
```    67 end
```