equal
deleted
inserted
replaced
53 |
53 |
54 lemma subst1_aexp: |
54 lemma subst1_aexp: |
55 "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a" |
55 "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a" |
56 and subst1_bexp: |
56 and subst1_bexp: |
57 "evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b" |
57 "evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b" |
58 \<comment> \<open>one variable\<close> |
58 \<comment> \<open>one variable\<close> |
59 by (induct a and b) simp_all |
59 by (induct a and b) simp_all |
60 |
60 |
61 lemma subst_all_aexp: |
61 lemma subst_all_aexp: |
62 "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a" |
62 "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a" |
63 and subst_all_bexp: |
63 and subst_all_bexp: |