5737
|
1 |
(* Title: HOL/Induct/ABexp.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Stefan Berghofer, TU Muenchen
|
|
4 |
Copyright 1998 TU Muenchen
|
|
5 |
|
|
6 |
Arithmetic and boolean expressions
|
|
7 |
*)
|
|
8 |
|
5802
|
9 |
(** substitution theorems for arithmetic and boolean expressions **)
|
5737
|
10 |
|
5802
|
11 |
(* One variable *)
|
5737
|
12 |
Goal
|
5802
|
13 |
"evala env (substa (Var(v := a')) a) = evala (env(v := evala env a')) a & \
|
|
14 |
\ evalb env (substb (Var(v := a')) b) = evalb (env(v := evala env a')) b";
|
5737
|
15 |
by (mutual_induct_tac ["a","b"] 1);
|
|
16 |
by (ALLGOALS Asm_full_simp_tac);
|
5802
|
17 |
qed "subst1_aexp_bexp";
|
|
18 |
|
|
19 |
(* All variables *)
|
|
20 |
Goal
|
|
21 |
"evala env (substa s a) = evala (%x. evala env (s x)) a & \
|
|
22 |
\ evalb env (substb s b) = evalb (%x. evala env (s x)) b";
|
|
23 |
by (mutual_induct_tac ["a","b"] 1);
|
|
24 |
by (Auto_tac);
|
|
25 |
qed "subst_all_aexp_bexp";
|