src/HOL/Induct/ABexp.ML

Infinitely branching trees.

(*  Title:      HOL/Induct/ABexp.ML
    ID:         $Id$
    Author:     Stefan Berghofer, TU Muenchen
    Copyright   1998  TU Muenchen

Arithmetic and boolean expressions
*)

(** substitution theorems for arithmetic and boolean expressions **)

(* One variable *)
Goal
  "evala env (substa (Var(v := a')) a) = evala (env(v := evala env a')) a &  \
 \ evalb env (substb (Var(v := a')) b) = evalb (env(v := evala env a')) b";
by (mutual_induct_tac ["a","b"] 1);
by (ALLGOALS Asm_full_simp_tac);
qed "subst1_aexp_bexp";

(* All variables *)
Goal
  "evala env (substa s a) = evala (%x. evala env (s x)) a &  \
 \ evalb env (substb s b) = evalb (%x. evala env (s x)) b";
by (mutual_induct_tac ["a","b"] 1);
by (Auto_tac);
qed "subst_all_aexp_bexp";