[STATEMENT]
lemma symvars_of_adapt_bexp :
  "Bexp.vars (adapt_bexp e s) \<subseteq> symvars s" (is "Bexp.vars ?e' \<subseteq> ?SV")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bexp.vars (adapt_bexp e s) \<subseteq> symvars s
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Bexp.vars (adapt_bexp e s) \<Longrightarrow> x \<in> symvars s
[PROOF STEP]
fix sv
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Bexp.vars (adapt_bexp e s) \<Longrightarrow> x \<in> symvars s
[PROOF STEP]
assume "sv \<in> Bexp.vars ?e'"
[PROOF STATE]
proof (state)
this:
sv \<in> Bexp.vars (adapt_bexp e s)

goal (1 subgoal):
 1. \<And>x. x \<in> Bexp.vars (adapt_bexp e s) \<Longrightarrow> x \<in> symvars s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sv \<in> Bexp.vars (adapt_bexp e s)
[PROOF STEP]
obtain \<sigma>\<^sub>s\<^sub>y\<^sub>m val 
  where "?e' (\<sigma>\<^sub>s\<^sub>y\<^sub>m (sv := val)) \<noteq> ?e' \<sigma>\<^sub>s\<^sub>y\<^sub>m"
[PROOF STATE]
proof (prove)
using this:
sv \<in> Bexp.vars (adapt_bexp e s)

goal (1 subgoal):
 1. (\<And>\<sigma>\<^sub>s\<^sub>y\<^sub>m val. adapt_bexp e s (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) \<noteq> adapt_bexp e s \<sigma>\<^sub>s\<^sub>y\<^sub>m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp add : Bexp.vars_def, blast)
[PROOF STATE]
proof (state)
this:
adapt_bexp e s (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) \<noteq> adapt_bexp e s \<sigma>\<^sub>s\<^sub>y\<^sub>m

goal (1 subgoal):
 1. \<And>x. x \<in> Bexp.vars (adapt_bexp e s) \<Longrightarrow> x \<in> symvars s
[PROOF STEP]
hence "(\<lambda> x. (\<sigma>\<^sub>s\<^sub>y\<^sub>m (sv := val)) (symvar x s)) \<noteq> (\<lambda> x. \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar x s))"
[PROOF STATE]
proof (prove)
using this:
adapt_bexp e s (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) \<noteq> adapt_bexp e s \<sigma>\<^sub>s\<^sub>y\<^sub>m

goal (1 subgoal):
 1. (\<lambda>x. (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) (symvar x s)) \<noteq> (\<lambda>x. \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar x s))
[PROOF STEP]
by (auto simp add : adapt_bexp_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) (symvar x s)) \<noteq> (\<lambda>x. \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar x s))

goal (1 subgoal):
 1. \<And>x. x \<in> Bexp.vars (adapt_bexp e s) \<Longrightarrow> x \<in> symvars s
[PROOF STEP]
hence "\<exists> v. (\<sigma>\<^sub>s\<^sub>y\<^sub>m (sv := val)) (symvar v s) \<noteq> \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar v s)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) (symvar x s)) \<noteq> (\<lambda>x. \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar x s))

goal (1 subgoal):
 1. \<exists>v. (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) (symvar v s) \<noteq> \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar v s)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>v. (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) (symvar v s) \<noteq> \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar v s)

goal (1 subgoal):
 1. \<And>x. x \<in> Bexp.vars (adapt_bexp e s) \<Longrightarrow> x \<in> symvars s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>v. (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) (symvar v s) \<noteq> \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar v s)
[PROOF STEP]
obtain v 
  where "(\<sigma>\<^sub>s\<^sub>y\<^sub>m (sv := val)) (symvar v s) \<noteq> \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar v s)"
[PROOF STATE]
proof (prove)
using this:
\<exists>v. (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) (symvar v s) \<noteq> \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar v s)

goal (1 subgoal):
 1. (\<And>v. (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) (symvar v s) \<noteq> \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar v s) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) (symvar v s) \<noteq> \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar v s)

goal (1 subgoal):
 1. \<And>x. x \<in> Bexp.vars (adapt_bexp e s) \<Longrightarrow> x \<in> symvars s
[PROOF STEP]
hence "sv = symvar v s"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) (symvar v s) \<noteq> \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar v s)

goal (1 subgoal):
 1. sv = symvar v s
[PROOF STEP]
by (case_tac "sv = symvar v s", simp_all)
[PROOF STATE]
proof (state)
this:
sv = symvar v s

goal (1 subgoal):
 1. \<And>x. x \<in> Bexp.vars (adapt_bexp e s) \<Longrightarrow> x \<in> symvars s
[PROOF STEP]
thus "sv \<in> symvars s"
[PROOF STATE]
proof (prove)
using this:
sv = symvar v s

goal (1 subgoal):
 1. sv \<in> symvars s
[PROOF STEP]
by (simp add : symvars_def)
[PROOF STATE]
proof (state)
this:
sv \<in> symvars s

goal:
No subgoals!
[PROOF STEP]
qed