[STATEMENT]
lemma ren_upper_time: assumes "upper_time_bound f"
  shows "ren.upper_time_bound f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ren.upper_time_bound f
[PROOF STEP]
unfolding ren.upper_time_bound_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w c n. set w \<subseteq> ra ` \<Sigma> \<longrightarrow> (ren.init_config w, c) \<in> ren.step ^^ n \<longrightarrow> n \<le> f (length w)
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w c n. \<lbrakk>set w \<subseteq> ra ` \<Sigma>; (ren.init_config w, c) \<in> ren.step ^^ n\<rbrakk> \<Longrightarrow> n \<le> f (length w)
[PROOF STEP]
fix w c n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w c n. \<lbrakk>set w \<subseteq> ra ` \<Sigma>; (ren.init_config w, c) \<in> ren.step ^^ n\<rbrakk> \<Longrightarrow> n \<le> f (length w)
[PROOF STEP]
assume w: "set w \<subseteq> ra ` \<Sigma>" and steps: "(ren.init_config w, c) \<in> ren.step ^^ n"
[PROOF STATE]
proof (state)
this:
set w \<subseteq> ra ` \<Sigma>
(ren.init_config w, c) \<in> ren.step ^^ n

goal (1 subgoal):
 1. \<And>w c n. \<lbrakk>set w \<subseteq> ra ` \<Sigma>; (ren.init_config w, c) \<in> ren.step ^^ n\<rbrakk> \<Longrightarrow> n \<le> f (length w)
[PROOF STEP]
define v where "v = map ira w"
[PROOF STATE]
proof (state)
this:
v = map ira w

goal (1 subgoal):
 1. \<And>w c n. \<lbrakk>set w \<subseteq> ra ` \<Sigma>; (ren.init_config w, c) \<in> ren.step ^^ n\<rbrakk> \<Longrightarrow> n \<le> f (length w)
[PROOF STEP]
from w
[PROOF STATE]
proof (chain)
picking this:
set w \<subseteq> ra ` \<Sigma>
[PROOF STEP]
have v: "set v \<subseteq> \<Sigma>"
[PROOF STATE]
proof (prove)
using this:
set w \<subseteq> ra ` \<Sigma>

goal (1 subgoal):
 1. set v \<subseteq> \<Sigma>
[PROOF STEP]
unfolding v_def
[PROOF STATE]
proof (prove)
using this:
set w \<subseteq> ra ` \<Sigma>

goal (1 subgoal):
 1. set (map ira w) \<subseteq> \<Sigma>
[PROOF STEP]
using inv_ren_Sigma
[PROOF STATE]
proof (prove)
using this:
set w \<subseteq> ra ` \<Sigma>
ira ` ra ` \<Sigma> = \<Sigma>

goal (1 subgoal):
 1. set (map ira w) \<subseteq> \<Sigma>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
set v \<subseteq> \<Sigma>

goal (1 subgoal):
 1. \<And>w c n. \<lbrakk>set w \<subseteq> ra ` \<Sigma>; (ren.init_config w, c) \<in> ren.step ^^ n\<rbrakk> \<Longrightarrow> n \<le> f (length w)
[PROOF STEP]
from inv.ren_steps_count[OF steps]
[PROOF STATE]
proof (chain)
picking this:
(inv.rc (ren.init_config w), inv.rc c) \<in> inv.ren.step ^^ n
[PROOF STEP]
have "(inv.rc (ren.init_config w), inv.rc c) \<in> inv.ren.step ^^ n"
[PROOF STATE]
proof (prove)
using this:
(inv.rc (ren.init_config w), inv.rc c) \<in> inv.ren.step ^^ n

goal (1 subgoal):
 1. (inv.rc (ren.init_config w), inv.rc c) \<in> inv.ren.step ^^ n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(inv.rc (ren.init_config w), inv.rc c) \<in> inv.ren.step ^^ n

goal (1 subgoal):
 1. \<And>w c n. \<lbrakk>set w \<subseteq> ra ` \<Sigma>; (ren.init_config w, c) \<in> ren.step ^^ n\<rbrakk> \<Longrightarrow> n \<le> f (length w)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(inv.rc (ren.init_config w), inv.rc c) \<in> inv.ren.step ^^ n

goal (1 subgoal):
 1. \<And>w c n. \<lbrakk>set w \<subseteq> ra ` \<Sigma>; (ren.init_config w, c) \<in> ren.step ^^ n\<rbrakk> \<Longrightarrow> n \<le> f (length w)
[PROOF STEP]
have "inv.ren.step = step"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv.ren.step = step
[PROOF STEP]
using inv_ren_\<delta>
[PROOF STATE]
proof (prove)
using this:
inv.rd ` rd ` \<delta> = \<delta>

goal (1 subgoal):
 1. inv.ren.step = step
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
inv.ren.step = step

goal (1 subgoal):
 1. \<And>w c n. \<lbrakk>set w \<subseteq> ra ` \<Sigma>; (ren.init_config w, c) \<in> ren.step ^^ n\<rbrakk> \<Longrightarrow> n \<le> f (length w)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inv.ren.step = step

goal (1 subgoal):
 1. \<And>w c n. \<lbrakk>set w \<subseteq> ra ` \<Sigma>; (ren.init_config w, c) \<in> ren.step ^^ n\<rbrakk> \<Longrightarrow> n \<le> f (length w)
[PROOF STEP]
have "inv.rc (ren.init_config w) = init_config v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv.rc (ren.init_config w) = init_config v
[PROOF STEP]
unfolding v_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv.rc (ren.init_config w) = init_config (map ira w)
[PROOF STEP]
using v w
[PROOF STATE]
proof (prove)
using this:
set v \<subseteq> \<Sigma>
set w \<subseteq> ra ` \<Sigma>

goal (1 subgoal):
 1. inv.rc (ren.init_config w) = init_config (map ira w)
[PROOF STEP]
by (simp add: inv.ren_init inv_ren_LE inv_ren_blank inv_ren_s)
[PROOF STATE]
proof (state)
this:
inv.rc (ren.init_config w) = init_config v

goal (1 subgoal):
 1. \<And>w c n. \<lbrakk>set w \<subseteq> ra ` \<Sigma>; (ren.init_config w, c) \<in> ren.step ^^ n\<rbrakk> \<Longrightarrow> n \<le> f (length w)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(init_config v, inv.rc c) \<in> step ^^ n
[PROOF STEP]
have "(init_config v, inv.rc c) \<in> step ^^ n"
[PROOF STATE]
proof (prove)
using this:
(init_config v, inv.rc c) \<in> step ^^ n

goal (1 subgoal):
 1. (init_config v, inv.rc c) \<in> step ^^ n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(init_config v, inv.rc c) \<in> step ^^ n

goal (1 subgoal):
 1. \<And>w c n. \<lbrakk>set w \<subseteq> ra ` \<Sigma>; (ren.init_config w, c) \<in> ren.step ^^ n\<rbrakk> \<Longrightarrow> n \<le> f (length w)
[PROOF STEP]
with assms[unfolded upper_time_bound_def] v
[PROOF STATE]
proof (chain)
picking this:
\<forall>w c n. set w \<subseteq> \<Sigma> \<longrightarrow> (init_config w, c) \<in> step ^^ n \<longrightarrow> n \<le> f (length w)
set v \<subseteq> \<Sigma>
(init_config v, inv.rc c) \<in> step ^^ n
[PROOF STEP]
have "n \<le> f (length v)"
[PROOF STATE]
proof (prove)
using this:
\<forall>w c n. set w \<subseteq> \<Sigma> \<longrightarrow> (init_config w, c) \<in> step ^^ n \<longrightarrow> n \<le> f (length w)
set v \<subseteq> \<Sigma>
(init_config v, inv.rc c) \<in> step ^^ n

goal (1 subgoal):
 1. n \<le> f (length v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n \<le> f (length v)

goal (1 subgoal):
 1. \<And>w c n. \<lbrakk>set w \<subseteq> ra ` \<Sigma>; (ren.init_config w, c) \<in> ren.step ^^ n\<rbrakk> \<Longrightarrow> n \<le> f (length w)
[PROOF STEP]
thus "n \<le> f (length w)"
[PROOF STATE]
proof (prove)
using this:
n \<le> f (length v)

goal (1 subgoal):
 1. n \<le> f (length w)
[PROOF STEP]
unfolding v_def
[PROOF STATE]
proof (prove)
using this:
n \<le> f (length (map ira w))

goal (1 subgoal):
 1. n \<le> f (length w)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<le> f (length w)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tm_renaming: assumes "valid_tm (tm :: ('q,'a)tm)"
  and "inj_on (ra :: 'a \<Rightarrow> 'b) (\<Gamma>_tm tm)"
  and "inj_on (rq :: 'q \<Rightarrow> 'p) (Q_tm tm)"
shows "\<exists> tm' :: ('p,'b)tm.
  valid_tm tm' \<and>
  Lang_tm tm' = map ra ` Lang_tm tm \<and>
  (det_tm tm \<longrightarrow> det_tm tm') \<and>
  (\<forall> f. upperb_time_tm tm f \<longrightarrow> upperb_time_tm tm' f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>tm'. valid_tm tm' \<and> Lang_tm tm' = map ra ` Lang_tm tm \<and> (det_tm tm \<longrightarrow> det_tm tm') \<and> (\<forall>f. upperb_time_tm tm f \<longrightarrow> upperb_time_tm tm' f)
[PROOF STEP]
proof (cases tm)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x7 x8 x9. tm = TM x1 x2 x3 x4 x5 x6 x7 x8 x9 \<Longrightarrow> \<exists>tm'. valid_tm tm' \<and> Lang_tm tm' = map ra ` Lang_tm tm \<and> (det_tm tm \<longrightarrow> det_tm tm') \<and> (\<forall>f. upperb_time_tm tm f \<longrightarrow> upperb_time_tm tm' f)
[PROOF STEP]
case (TM Q \<Sigma> \<Gamma> bl le \<delta> s t r)
[PROOF STATE]
proof (state)
this:
tm = TM Q \<Sigma> \<Gamma> bl le \<delta> s t r

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x7 x8 x9. tm = TM x1 x2 x3 x4 x5 x6 x7 x8 x9 \<Longrightarrow> \<exists>tm'. valid_tm tm' \<and> Lang_tm tm' = map ra ` Lang_tm tm \<and> (det_tm tm \<longrightarrow> det_tm tm') \<and> (\<forall>f. upperb_time_tm tm f \<longrightarrow> upperb_time_tm tm' f)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
valid_tm tm
inj_on ra (\<Gamma>_tm tm)
inj_on rq (Q_tm tm)
tm = TM Q \<Sigma> \<Gamma> bl le \<delta> s t r
[PROOF STEP]
interpret singletape_tm Q \<Sigma> \<Gamma> bl le \<delta> s t r
[PROOF STATE]
proof (prove)
using this:
valid_tm tm
inj_on ra (\<Gamma>_tm tm)
inj_on rq (Q_tm tm)
tm = TM Q \<Sigma> \<Gamma> bl le \<delta> s t r

goal (1 subgoal):
 1. singletape_tm Q \<Sigma> \<Gamma> bl le \<delta> s t r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x7 x8 x9. tm = TM x1 x2 x3 x4 x5 x6 x7 x8 x9 \<Longrightarrow> \<exists>tm'. valid_tm tm' \<and> Lang_tm tm' = map ra ` Lang_tm tm \<and> (det_tm tm \<longrightarrow> det_tm tm') \<and> (\<forall>f. upperb_time_tm tm f \<longrightarrow> upperb_time_tm tm' f)
[PROOF STEP]
interpret renaming_of_singletape_tm Q \<Sigma> \<Gamma> bl le \<delta> s t r ra rq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. renaming_of_singletape_tm Q \<Sigma> \<Gamma> bl le \<delta> s t r ra rq
[PROOF STEP]
by (unfold_locales, insert assms TM, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x7 x8 x9. tm = TM x1 x2 x3 x4 x5 x6 x7 x8 x9 \<Longrightarrow> \<exists>tm'. valid_tm tm' \<and> Lang_tm tm' = map ra ` Lang_tm tm \<and> (det_tm tm \<longrightarrow> det_tm tm') \<and> (\<forall>f. upperb_time_tm tm f \<longrightarrow> upperb_time_tm tm' f)
[PROOF STEP]
let ?tm' = "TM (rq ` Q) (ra ` \<Sigma>) (ra ` \<Gamma>) (ra bl) (ra le) (rd ` \<delta>) (rq s) (rq t) (rq r)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x7 x8 x9. tm = TM x1 x2 x3 x4 x5 x6 x7 x8 x9 \<Longrightarrow> \<exists>tm'. valid_tm tm' \<and> Lang_tm tm' = map ra ` Lang_tm tm \<and> (det_tm tm \<longrightarrow> det_tm tm') \<and> (\<forall>f. upperb_time_tm tm f \<longrightarrow> upperb_time_tm tm' f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>tm'. valid_tm tm' \<and> Lang_tm tm' = map ra ` Lang_tm tm \<and> (det_tm tm \<longrightarrow> det_tm tm') \<and> (\<forall>f. upperb_time_tm tm f \<longrightarrow> upperb_time_tm tm' f)
[PROOF STEP]
by (rule exI[where x = ?tm'])
       (simp add: TM ren.singletape_tm_axioms ren_Lang ren_det ren_upper_time)
[PROOF STATE]
proof (state)
this:
\<exists>tm'. valid_tm tm' \<and> Lang_tm tm' = map ra ` Lang_tm tm \<and> (det_tm tm \<longrightarrow> det_tm tm') \<and> (\<forall>f. upperb_time_tm tm f \<longrightarrow> upperb_time_tm tm' f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma restrictI: "\<forall>x\<in>S. s1 x = s2 x \<Longrightarrow> restrict S s1 = restrict S s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s1 = s2 on S \<Longrightarrow> restrict S s1 = restrict S s2
[PROOF STEP]
unfolding restrict_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s1 = s2 on S \<Longrightarrow> (\<lambda>x. if x \<in> S then Some (s1 x) else None) = (\<lambda>x. if x \<in> S then Some (s2 x) else None)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma restrictE: "restrict S s1 = restrict S s2 \<Longrightarrow> s1 = s2 on S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict S s1 = restrict S s2 \<Longrightarrow> s1 = s2 on S
[PROOF STEP]
unfolding restrict_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if x \<in> S then Some (s1 x) else None) = (\<lambda>x. if x \<in> S then Some (s2 x) else None) \<Longrightarrow> s1 = s2 on S
[PROOF STEP]
by (meson option.inject)


[STATEMENT]
lemma dom_restrict[simp]: "dom (restrict S s) = S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (restrict S s) = S
[PROOF STEP]
unfolding restrict_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (\<lambda>x. if x \<in> S then Some (s x) else None) = S
[PROOF STEP]
using domIff
[PROOF STATE]
proof (prove)
using this:
(?a \<in> dom ?m) = (?m ?a \<noteq> None)

goal (1 subgoal):
 1. dom (\<lambda>x. if x \<in> S then Some (s x) else None) = S
[PROOF STEP]
by fastforce


[STATEMENT]
lemma restrict_less_part: "restrict S t \<preceq> part t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict S t \<preceq> part t
[PROOF STEP]
unfolding restrict_def map_le_substate_conv[symmetric] map_le_def part_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a. if a \<in> S then Some (t a) else None) = \<lambda>a. Some (t a) on dom (\<lambda>x. if x \<in> S then Some (t x) else None)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a y. (if a \<in> S then Some (t a) else None) = Some y \<Longrightarrow> a \<in> S
[PROOF STEP]
by (metis option.simps(3))


[STATEMENT]
lemma subState: "x \<preceq> y \<Longrightarrow> v \<in> dom x \<Longrightarrow> x v = y v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<preceq> y; v \<in> dom x\<rbrakk> \<Longrightarrow> x v = y v
[PROOF STEP]
unfolding map_le_substate_conv[symmetric] map_le_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = y on dom x; v \<in> dom x\<rbrakk> \<Longrightarrow> x v = y v
[PROOF STEP]
by blast


[STATEMENT]
lemma  fixes ps:: partstate
    and s::state
  assumes "vars a \<subseteq> dom ps" "ps \<preceq> part s"
  shows emb_update: "emb [x \<mapsto> paval a ps] s = (emb ps s) (x := aval a (emb ps s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emb [x \<mapsto> paval a ps] s = (emb ps s)(x := aval a (emb ps s))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vars a \<subseteq> dom ps
ps \<preceq> part s

goal (1 subgoal):
 1. emb [x \<mapsto> paval a ps] s = (emb ps s)(x := aval a (emb ps s))
[PROOF STEP]
unfolding emb_def
[PROOF STATE]
proof (prove)
using this:
vars a \<subseteq> dom ps
ps \<preceq> part s

goal (1 subgoal):
 1. (\<lambda>v. case [x \<mapsto> paval a ps] v of None \<Rightarrow> s v | Some r \<Rightarrow> r) = (\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r)(x := aval a (\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vars a \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> (\<lambda>v. case if v = x then Some (paval a ps) else None of None \<Rightarrow> s v | Some r \<Rightarrow> r) = (\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r)(x := aval a (\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r))
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>vars a \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> (case if v = x then Some (paval a ps) else None of None \<Rightarrow> s v | Some r \<Rightarrow> r) = ((\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r)(x := aval a (\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r))) v
[PROOF STEP]
apply(case_tac "v=x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>vars a \<subseteq> dom ps; ps \<preceq> part s; v = x\<rbrakk> \<Longrightarrow> (case if v = x then Some (paval a ps) else None of None \<Rightarrow> s v | Some r \<Rightarrow> r) = ((\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r)(x := aval a (\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r))) v
 2. \<And>v. \<lbrakk>vars a \<subseteq> dom ps; ps \<preceq> part s; v \<noteq> x\<rbrakk> \<Longrightarrow> (case if v = x then Some (paval a ps) else None of None \<Rightarrow> s v | Some r \<Rightarrow> r) = ((\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r)(x := aval a (\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r))) v
[PROOF STEP]
apply(simp add: paval_aval)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>vars a \<subseteq> dom ps; ps \<preceq> part s; v \<noteq> x\<rbrakk> \<Longrightarrow> (case if v = x then Some (paval a ps) else None of None \<Rightarrow> s v | Some r \<Rightarrow> r) = ((\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r)(x := aval a (\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r))) v
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>vars a \<subseteq> dom ps; ps \<preceq> part s; v \<noteq> x\<rbrakk> \<Longrightarrow> s v = (case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r)
[PROOF STEP]
unfolding part_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>vars a \<subseteq> dom ps; ps \<preceq> (\<lambda>v. Some (s v)); v \<noteq> x\<rbrakk> \<Longrightarrow> s v = (case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r)
[PROOF STEP]
apply(case_tac "v \<in> dom ps")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>vars a \<subseteq> dom ps; ps \<preceq> (\<lambda>v. Some (s v)); v \<noteq> x; v \<in> dom ps\<rbrakk> \<Longrightarrow> s v = (case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r)
 2. \<And>v. \<lbrakk>vars a \<subseteq> dom ps; ps \<preceq> (\<lambda>v. Some (s v)); v \<noteq> x; v \<notin> dom ps\<rbrakk> \<Longrightarrow> s v = (case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r)
[PROOF STEP]
using subState
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<preceq> ?y; ?v \<in> dom ?x\<rbrakk> \<Longrightarrow> ?x ?v = ?y ?v

goal (2 subgoals):
 1. \<And>v. \<lbrakk>vars a \<subseteq> dom ps; ps \<preceq> (\<lambda>v. Some (s v)); v \<noteq> x; v \<in> dom ps\<rbrakk> \<Longrightarrow> s v = (case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r)
 2. \<And>v. \<lbrakk>vars a \<subseteq> dom ps; ps \<preceq> (\<lambda>v. Some (s v)); v \<noteq> x; v \<notin> dom ps\<rbrakk> \<Longrightarrow> s v = (case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>vars a \<subseteq> dom ps; ps \<preceq> (\<lambda>v. Some (s v)); v \<noteq> x; v \<notin> dom ps\<rbrakk> \<Longrightarrow> s v = (case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r)
[PROOF STEP]
by (simp add: domIff)


[STATEMENT]
lemma paval_aval2: "vars a \<subseteq> dom ps \<Longrightarrow> ps \<preceq> part s \<Longrightarrow> paval a ps = aval a s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vars a \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval a ps = aval a s
[PROOF STEP]
apply(induct a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>vars (N x) \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval (N x) ps = aval (N x) s
 2. \<And>x. \<lbrakk>vars (V x) \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval (V x) ps = aval (V x) s
 3. \<And>a1 a2. \<lbrakk>\<lbrakk>vars a1 \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval a1 ps = aval a1 s; \<lbrakk>vars a2 \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval a2 ps = aval a2 s; vars (Plus a1 a2) \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval (Plus a1 a2) ps = aval (Plus a1 a2) s
 4. \<And>a1 a2. \<lbrakk>\<lbrakk>vars a1 \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval a1 ps = aval a1 s; \<lbrakk>vars a2 \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval a2 ps = aval a2 s; vars (Times a1 a2) \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval (Times a1 a2) ps = aval (Times a1 a2) s
 5. \<And>a1 a2. \<lbrakk>\<lbrakk>vars a1 \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval a1 ps = aval a1 s; \<lbrakk>vars a2 \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval a2 ps = aval a2 s; vars (Div a1 a2) \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval (Div a1 a2) ps = aval (Div a1 a2) s
[PROOF STEP]
using subState
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<preceq> ?y; ?v \<in> dom ?x\<rbrakk> \<Longrightarrow> ?x ?v = ?y ?v

goal (5 subgoals):
 1. \<And>x. \<lbrakk>vars (N x) \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval (N x) ps = aval (N x) s
 2. \<And>x. \<lbrakk>vars (V x) \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval (V x) ps = aval (V x) s
 3. \<And>a1 a2. \<lbrakk>\<lbrakk>vars a1 \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval a1 ps = aval a1 s; \<lbrakk>vars a2 \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval a2 ps = aval a2 s; vars (Plus a1 a2) \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval (Plus a1 a2) ps = aval (Plus a1 a2) s
 4. \<And>a1 a2. \<lbrakk>\<lbrakk>vars a1 \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval a1 ps = aval a1 s; \<lbrakk>vars a2 \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval a2 ps = aval a2 s; vars (Times a1 a2) \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval (Times a1 a2) ps = aval (Times a1 a2) s
 5. \<And>a1 a2. \<lbrakk>\<lbrakk>vars a1 \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval a1 ps = aval a1 s; \<lbrakk>vars a2 \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval a2 ps = aval a2 s; vars (Div a1 a2) \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> paval (Div a1 a2) ps = aval (Div a1 a2) s
[PROOF STEP]
unfolding part_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<preceq> ?y; ?v \<in> dom ?x\<rbrakk> \<Longrightarrow> ?x ?v = ?y ?v

goal (5 subgoals):
 1. \<And>x. \<lbrakk>vars (N x) \<subseteq> dom ps; ps \<preceq> (\<lambda>v. Some (s v))\<rbrakk> \<Longrightarrow> paval (N x) ps = aval (N x) s
 2. \<And>x. \<lbrakk>vars (V x) \<subseteq> dom ps; ps \<preceq> (\<lambda>v. Some (s v))\<rbrakk> \<Longrightarrow> paval (V x) ps = aval (V x) s
 3. \<And>a1 a2. \<lbrakk>\<lbrakk>vars a1 \<subseteq> dom ps; ps \<preceq> (\<lambda>v. Some (s v))\<rbrakk> \<Longrightarrow> paval a1 ps = aval a1 s; \<lbrakk>vars a2 \<subseteq> dom ps; ps \<preceq> (\<lambda>v. Some (s v))\<rbrakk> \<Longrightarrow> paval a2 ps = aval a2 s; vars (Plus a1 a2) \<subseteq> dom ps; ps \<preceq> (\<lambda>v. Some (s v))\<rbrakk> \<Longrightarrow> paval (Plus a1 a2) ps = aval (Plus a1 a2) s
 4. \<And>a1 a2. \<lbrakk>\<lbrakk>vars a1 \<subseteq> dom ps; ps \<preceq> (\<lambda>v. Some (s v))\<rbrakk> \<Longrightarrow> paval a1 ps = aval a1 s; \<lbrakk>vars a2 \<subseteq> dom ps; ps \<preceq> (\<lambda>v. Some (s v))\<rbrakk> \<Longrightarrow> paval a2 ps = aval a2 s; vars (Times a1 a2) \<subseteq> dom ps; ps \<preceq> (\<lambda>v. Some (s v))\<rbrakk> \<Longrightarrow> paval (Times a1 a2) ps = aval (Times a1 a2) s
 5. \<And>a1 a2. \<lbrakk>\<lbrakk>vars a1 \<subseteq> dom ps; ps \<preceq> (\<lambda>v. Some (s v))\<rbrakk> \<Longrightarrow> paval a1 ps = aval a1 s; \<lbrakk>vars a2 \<subseteq> dom ps; ps \<preceq> (\<lambda>v. Some (s v))\<rbrakk> \<Longrightarrow> paval a2 ps = aval a2 s; vars (Div a1 a2) \<subseteq> dom ps; ps \<preceq> (\<lambda>v. Some (s v))\<rbrakk> \<Longrightarrow> paval (Div a1 a2) ps = aval (Div a1 a2) s
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>ps \<preceq> (\<lambda>v. Some (s v)); \<And>x y v. \<lbrakk>x \<preceq> y; v \<in> dom x\<rbrakk> \<Longrightarrow> x v = y v; ps x = Some y\<rbrakk> \<Longrightarrow> y = s x
[PROOF STEP]
by fastforce


[STATEMENT]
lemma  fixes ps:: partstate
    and s::state
  assumes "vars a \<subseteq> dom ps" "ps \<preceq> part s"
  shows emb_update2: "emb (ps(x \<mapsto> paval a ps)) s = (emb ps s)(x := aval a (emb ps s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emb (ps(x \<mapsto> paval a ps)) s = (emb ps s)(x := aval a (emb ps s))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vars a \<subseteq> dom ps
ps \<preceq> part s

goal (1 subgoal):
 1. emb (ps(x \<mapsto> paval a ps)) s = (emb ps s)(x := aval a (emb ps s))
[PROOF STEP]
unfolding emb_def
[PROOF STATE]
proof (prove)
using this:
vars a \<subseteq> dom ps
ps \<preceq> part s

goal (1 subgoal):
 1. (\<lambda>v. case (ps(x \<mapsto> paval a ps)) v of None \<Rightarrow> s v | Some r \<Rightarrow> r) = (\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r)(x := aval a (\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vars a \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> (\<lambda>v. case if v = x then Some (paval a ps) else ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r) = (\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r)(x := aval a (\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r))
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>vars a \<subseteq> dom ps; ps \<preceq> part s\<rbrakk> \<Longrightarrow> (case if v = x then Some (paval a ps) else ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r) = ((\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r)(x := aval a (\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r))) v
[PROOF STEP]
apply(case_tac "v=x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>vars a \<subseteq> dom ps; ps \<preceq> part s; v = x\<rbrakk> \<Longrightarrow> (case if v = x then Some (paval a ps) else ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r) = ((\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r)(x := aval a (\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r))) v
 2. \<And>v. \<lbrakk>vars a \<subseteq> dom ps; ps \<preceq> part s; v \<noteq> x\<rbrakk> \<Longrightarrow> (case if v = x then Some (paval a ps) else ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r) = ((\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r)(x := aval a (\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r))) v
[PROOF STEP]
apply(simp add: paval_aval)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>vars a \<subseteq> dom ps; ps \<preceq> part s; v \<noteq> x\<rbrakk> \<Longrightarrow> (case if v = x then Some (paval a ps) else ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r) = ((\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r)(x := aval a (\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r))) v
[PROOF STEP]
by (simp)


[STATEMENT]
lemma big_step_t3_post_dom_conv: "(c,ps) \<Rightarrow>\<^sub>A t \<Down> ps' \<Longrightarrow> dom ps' = dom ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c, ps) \<Rightarrow>\<^sub>A t \<Down> ps' \<Longrightarrow> dom ps' = dom ps
[PROOF STEP]
apply(induct rule: big_step_t_part_induct)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>s. dom s = dom s
 2. \<And>a x ps v ps'. \<lbrakk>vars a \<union> {x} \<subseteq> dom ps; paval a ps = v; ps' = ps(x \<mapsto> v)\<rbrakk> \<Longrightarrow> dom ps' = dom ps
 3. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; dom s2 = dom s1; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; dom s3 = dom s2; z = x + y\<rbrakk> \<Longrightarrow> dom s3 = dom s1
 4. \<And>b ps ps' c1 x y c2. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; dom ps' = dom ps; y = x + 1\<rbrakk> \<Longrightarrow> dom ps' = dom ps
 5. \<And>b ps ps' c2 x y c1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; dom ps' = dom ps; y = x + 1\<rbrakk> \<Longrightarrow> dom ps' = dom ps
 6. \<And>b s c. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s\<rbrakk> \<Longrightarrow> dom s = dom s
 7. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; dom s2 = dom s1; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; dom s3 = dom s2; 1 + x + y = z\<rbrakk> \<Longrightarrow> dom s3 = dom s1
[PROOF STEP]
apply (auto simp: sep_disj_fun_def plus_fun_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x ps y xa ya. \<lbrakk>vars a \<subseteq> dom ps; ps x = Some y; (if xa = x then Some (paval a ps) else ps xa) = Some ya\<rbrakk> \<Longrightarrow> \<exists>y. ps xa = Some y
[PROOF STEP]
apply metis
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma add_update_distrib: "ps1 x1 = Some y \<Longrightarrow> ps1 ## ps2 \<Longrightarrow> vars x2 \<subseteq> dom ps1 \<Longrightarrow> ps1(x1 \<mapsto> paval x2 ps1) + ps2  = (ps1 + ps2)(x1 \<mapsto> paval x2 ps1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps1 x1 = Some y; ps1 ## ps2; vars x2 \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> ps1(x1 \<mapsto> paval x2 ps1) + ps2 = (ps1 + ps2)(x1 \<mapsto> paval x2 ps1)
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ps1 x1 = Some y; ps1 ## ps2; vars x2 \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> (ps1(x1 \<mapsto> paval x2 ps1) + ps2) x = ((ps1 + ps2)(x1 \<mapsto> paval x2 ps1)) x
[PROOF STEP]
apply (auto simp: sep_disj_fun_def plus_fun_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ya. \<lbrakk>ps1 x1 = Some y; domain ps1 \<inter> domain ps2 = {}; vars x2 \<subseteq> dom ps1; ps2 x1 = Some ya\<rbrakk> \<Longrightarrow> ya = paval x2 ps1
[PROOF STEP]
by (metis disjoint_iff_not_equal domI domain_conv)


[STATEMENT]
lemma paval_extend:  "ps1 ## ps2 \<Longrightarrow> vars a \<subseteq> dom ps1 \<Longrightarrow> paval a (ps1 + ps2) = paval a ps1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps1 ## ps2; vars a \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> paval a (ps1 + ps2) = paval a ps1
[PROOF STEP]
apply(induct a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>ps1 ## ps2; vars (N x) \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> paval (N x) (ps1 + ps2) = paval (N x) ps1
 2. \<And>x. \<lbrakk>ps1 ## ps2; vars (V x) \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> paval (V x) (ps1 + ps2) = paval (V x) ps1
 3. \<And>a1 a2. \<lbrakk>\<lbrakk>ps1 ## ps2; vars a1 \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> paval a1 (ps1 + ps2) = paval a1 ps1; \<lbrakk>ps1 ## ps2; vars a2 \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> paval a2 (ps1 + ps2) = paval a2 ps1; ps1 ## ps2; vars (Plus a1 a2) \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> paval (Plus a1 a2) (ps1 + ps2) = paval (Plus a1 a2) ps1
 4. \<And>a1 a2. \<lbrakk>\<lbrakk>ps1 ## ps2; vars a1 \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> paval a1 (ps1 + ps2) = paval a1 ps1; \<lbrakk>ps1 ## ps2; vars a2 \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> paval a2 (ps1 + ps2) = paval a2 ps1; ps1 ## ps2; vars (Times a1 a2) \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> paval (Times a1 a2) (ps1 + ps2) = paval (Times a1 a2) ps1
 5. \<And>a1 a2. \<lbrakk>\<lbrakk>ps1 ## ps2; vars a1 \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> paval a1 (ps1 + ps2) = paval a1 ps1; \<lbrakk>ps1 ## ps2; vars a2 \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> paval a2 (ps1 + ps2) = paval a2 ps1; ps1 ## ps2; vars (Div a1 a2) \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> paval (Div a1 a2) (ps1 + ps2) = paval (Div a1 a2) ps1
[PROOF STEP]
apply (auto simp: sep_disj_fun_def domain_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>dom ps1 \<inter> dom ps2 = {}; ps1 x = Some y\<rbrakk> \<Longrightarrow> the ((ps1 + ps2) x) = y
[PROOF STEP]
by (metis domI map_add_comm map_add_dom_app_simps(1) option.sel plus_fun_conv)


[STATEMENT]
lemma pbval_extend: "ps1 ## ps2 \<Longrightarrow> vars b \<subseteq> dom ps1 \<Longrightarrow> pbval b (ps1 + ps2) = pbval b ps1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps1 ## ps2; vars b \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> pbval b (ps1 + ps2) = pbval b ps1
[PROOF STEP]
apply(induct b)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>ps1 ## ps2; vars (Bc x) \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> pbval (Bc x) (ps1 + ps2) = pbval (Bc x) ps1
 2. \<And>b. \<lbrakk>\<lbrakk>ps1 ## ps2; vars b \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> pbval b (ps1 + ps2) = pbval b ps1; ps1 ## ps2; vars (bexp.Not b) \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> pbval (bexp.Not b) (ps1 + ps2) = pbval (bexp.Not b) ps1
 3. \<And>b1 b2. \<lbrakk>\<lbrakk>ps1 ## ps2; vars b1 \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> pbval b1 (ps1 + ps2) = pbval b1 ps1; \<lbrakk>ps1 ## ps2; vars b2 \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> pbval b2 (ps1 + ps2) = pbval b2 ps1; ps1 ## ps2; vars (And b1 b2) \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> pbval (And b1 b2) (ps1 + ps2) = pbval (And b1 b2) ps1
 4. \<And>x1a x2a. \<lbrakk>ps1 ## ps2; vars (Less x1a x2a) \<subseteq> dom ps1\<rbrakk> \<Longrightarrow> pbval (Less x1a x2a) (ps1 + ps2) = pbval (Less x1a x2a) ps1
[PROOF STEP]
by (auto simp: paval_extend)


[STATEMENT]
lemma Framer: "(C, ps1) \<Rightarrow>\<^sub>A m \<Down> ps1' \<Longrightarrow> ps1 ## ps2 \<Longrightarrow> (C, ps1 + ps2) \<Rightarrow>\<^sub>A m \<Down>  ps1'+ps2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(C, ps1) \<Rightarrow>\<^sub>A m \<Down> ps1'; ps1 ## ps2\<rbrakk> \<Longrightarrow> (C, ps1 + ps2) \<Rightarrow>\<^sub>A m \<Down> ps1' + ps2
[PROOF STEP]
proof (induct rule: big_step_t_part_induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>s. s ## ps2 \<Longrightarrow> (SKIP, s + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> s + ps2
 2. \<And>a x ps v ps'. \<lbrakk>vars a \<union> {x} \<subseteq> dom ps; paval a ps = v; ps' = ps(x \<mapsto> v); ps ## ps2\<rbrakk> \<Longrightarrow> (x ::= a, ps + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> ps' + ps2
 3. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
 4. \<And>b ps ps' c1 x y c2. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps ## ps2 \<Longrightarrow> (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = x + 1; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
 5. \<And>b ps ps' c2 x y c1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps ## ps2 \<Longrightarrow> (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = x + 1; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
 6. \<And>b s c. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> s + ps2
 7. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; 1 + x + y = z; s1 ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
case (Skip s)
[PROOF STATE]
proof (state)
this:
s ## ps2

goal (7 subgoals):
 1. \<And>s. s ## ps2 \<Longrightarrow> (SKIP, s + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> s + ps2
 2. \<And>a x ps v ps'. \<lbrakk>vars a \<union> {x} \<subseteq> dom ps; paval a ps = v; ps' = ps(x \<mapsto> v); ps ## ps2\<rbrakk> \<Longrightarrow> (x ::= a, ps + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> ps' + ps2
 3. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
 4. \<And>b ps ps' c1 x y c2. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps ## ps2 \<Longrightarrow> (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = x + 1; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
 5. \<And>b ps ps' c2 x y c1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps ## ps2 \<Longrightarrow> (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = x + 1; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
 6. \<And>b s c. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> s + ps2
 7. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; 1 + x + y = z; s1 ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s ## ps2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s ## ps2

goal (1 subgoal):
 1. (SKIP, s + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> s + ps2
[PROOF STEP]
by (auto simp: big_step_t_part.Skip)
[PROOF STATE]
proof (state)
this:
(SKIP, s + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> s + ps2

goal (6 subgoals):
 1. \<And>a x ps v ps'. \<lbrakk>vars a \<union> {x} \<subseteq> dom ps; paval a ps = v; ps' = ps(x \<mapsto> v); ps ## ps2\<rbrakk> \<Longrightarrow> (x ::= a, ps + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> ps' + ps2
 2. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
 3. \<And>b ps ps' c1 x y c2. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps ## ps2 \<Longrightarrow> (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = x + 1; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
 4. \<And>b ps ps' c2 x y c1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps ## ps2 \<Longrightarrow> (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = x + 1; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
 5. \<And>b s c. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> s + ps2
 6. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; 1 + x + y = z; s1 ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>a x ps v ps'. \<lbrakk>vars a \<union> {x} \<subseteq> dom ps; paval a ps = v; ps' = ps(x \<mapsto> v); ps ## ps2\<rbrakk> \<Longrightarrow> (x ::= a, ps + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> ps' + ps2
 2. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
 3. \<And>b ps ps' c1 x y c2. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps ## ps2 \<Longrightarrow> (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = x + 1; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
 4. \<And>b ps ps' c2 x y c1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps ## ps2 \<Longrightarrow> (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = x + 1; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
 5. \<And>b s c. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> s + ps2
 6. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; 1 + x + y = z; s1 ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
case (Assign a x ps v ps')
[PROOF STATE]
proof (state)
this:
vars a \<union> {x} \<subseteq> dom ps
paval a ps = v
ps' = ps(x \<mapsto> v)
ps ## ps2

goal (6 subgoals):
 1. \<And>a x ps v ps'. \<lbrakk>vars a \<union> {x} \<subseteq> dom ps; paval a ps = v; ps' = ps(x \<mapsto> v); ps ## ps2\<rbrakk> \<Longrightarrow> (x ::= a, ps + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> ps' + ps2
 2. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
 3. \<And>b ps ps' c1 x y c2. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps ## ps2 \<Longrightarrow> (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = x + 1; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
 4. \<And>b ps ps' c2 x y c1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps ## ps2 \<Longrightarrow> (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = x + 1; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
 5. \<And>b s c. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> s + ps2
 6. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; 1 + x + y = z; s1 ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x ::= a, ps + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> ps' + ps2
[PROOF STEP]
apply(rule big_step_t_part.Assign)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. vars a \<union> {x} \<subseteq> dom (ps + ps2)
 2. paval a (ps + ps2) = ?v
 3. ps' + ps2 = (ps + ps2)(x \<mapsto> ?v)
[PROOF STEP]
using Assign
[PROOF STATE]
proof (prove)
using this:
vars a \<union> {x} \<subseteq> dom ps
paval a ps = v
ps' = ps(x \<mapsto> v)
ps ## ps2

goal (3 subgoals):
 1. vars a \<union> {x} \<subseteq> dom (ps + ps2)
 2. paval a (ps + ps2) = ?v
 3. ps' + ps2 = (ps + ps2)(x \<mapsto> ?v)
[PROOF STEP]
apply (auto simp: plus_fun_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>ps' = ps(x \<mapsto> paval a ps); ps ## ps2; v = paval a ps; vars a \<subseteq> dom ps; ps x = Some y\<rbrakk> \<Longrightarrow> (\<lambda>b. if ps2 b = None then if b = x then Some (paval a ps) else ps b else ps2 b) = (\<lambda>a. if ps2 a = None then ps a else ps2 a)(x \<mapsto> paval a (\<lambda>a. if ps2 a = None then ps a else ps2 a))
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y xa. \<lbrakk>ps' = ps(x \<mapsto> paval a ps); ps ## ps2; v = paval a ps; vars a \<subseteq> dom ps; ps x = Some y\<rbrakk> \<Longrightarrow> (if ps2 xa = None then if xa = x then Some (paval a ps) else ps xa else ps2 xa) = ((\<lambda>a. if ps2 a = None then ps a else ps2 a)(x \<mapsto> paval a (\<lambda>a. if ps2 a = None then ps a else ps2 a))) xa
[PROOF STEP]
apply(case_tac "xa=x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y xa. \<lbrakk>ps' = ps(x \<mapsto> paval a ps); ps ## ps2; v = paval a ps; vars a \<subseteq> dom ps; ps x = Some y; xa = x\<rbrakk> \<Longrightarrow> (if ps2 xa = None then if xa = x then Some (paval a ps) else ps xa else ps2 xa) = ((\<lambda>a. if ps2 a = None then ps a else ps2 a)(x \<mapsto> paval a (\<lambda>a. if ps2 a = None then ps a else ps2 a))) xa
 2. \<And>y xa. \<lbrakk>ps' = ps(x \<mapsto> paval a ps); ps ## ps2; v = paval a ps; vars a \<subseteq> dom ps; ps x = Some y; xa \<noteq> x\<rbrakk> \<Longrightarrow> (if ps2 xa = None then if xa = x then Some (paval a ps) else ps xa else ps2 xa) = ((\<lambda>a. if ps2 a = None then ps a else ps2 a)(x \<mapsto> paval a (\<lambda>a. if ps2 a = None then ps a else ps2 a))) xa
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps' = ps(x \<mapsto> paval a ps); ps ## ps2; v = paval a ps; vars a \<subseteq> dom ps; ps x = Some y_; xa_ = x\<rbrakk> \<Longrightarrow> (if ps2 xa_ = None then if xa_ = x then Some (paval a ps) else ps xa_ else ps2 xa_) = ((\<lambda>a. if ps2 a = None then ps a else ps2 a)(x \<mapsto> paval a (\<lambda>a. if ps2 a = None then ps a else ps2 a))) xa_
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ps' = ps(x \<mapsto> paval a ps); ps ## ps2; v = paval a ps; vars a \<subseteq> dom ps; ps x = Some y_; xa_ = x; ps2 x = None\<rbrakk> \<Longrightarrow> paval a ps = paval a (\<lambda>a. if ps2 a = None then ps a else ps2 a)
 2. \<And>ya. \<lbrakk>ps' = ps(x \<mapsto> paval a ps); ps ## ps2; v = paval a ps; vars a \<subseteq> dom ps; ps x = Some y_; xa_ = x; ps2 x = Some ya\<rbrakk> \<Longrightarrow> ya = paval a (\<lambda>a. if ps2 a = None then ps a else ps2 a)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps' = ps(x \<mapsto> paval a ps); ps ## ps2; v = paval a ps; vars a \<subseteq> dom ps; ps x = Some y_; xa_ = x; ps2 x = None\<rbrakk> \<Longrightarrow> paval a ps = paval a (\<lambda>a. if ps2 a = None then ps a else ps2 a)
[PROOF STEP]
using paval_extend[unfolded plus_fun_def]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?ps1.0 ## ?ps2.0; vars ?a \<subseteq> dom ?ps1.0\<rbrakk> \<Longrightarrow> paval ?a (\<lambda>x. if ?ps2.0 x = none then ?ps1.0 x else ?ps2.0 x) = paval ?a ?ps1.0

goal (1 subgoal):
 1. \<lbrakk>ps' = ps(x \<mapsto> paval a ps); ps ## ps2; v = paval a ps; vars a \<subseteq> dom ps; ps x = Some y_; xa_ = x; ps2 x = None\<rbrakk> \<Longrightarrow> paval a ps = paval a (\<lambda>a. if ps2 a = None then ps a else ps2 a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ya. \<lbrakk>ps' = ps(x \<mapsto> paval a ps); ps ## ps2; v = paval a ps; vars a \<subseteq> dom ps; ps x = Some y_; xa_ = x; ps2 x = Some ya\<rbrakk> \<Longrightarrow> ya = paval a (\<lambda>a. if ps2 a = None then ps a else ps2 a)
[PROOF STEP]
unfolding sep_disj_fun_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ya. \<lbrakk>ps' = ps(x \<mapsto> paval a ps); domain ps \<inter> domain ps2 = {}; v = paval a ps; vars a \<subseteq> dom ps; ps x = Some y_; xa_ = x; ps2 x = Some ya\<rbrakk> \<Longrightarrow> ya = paval a (\<lambda>a. if ps2 a = None then ps a else ps2 a)
[PROOF STEP]
by (metis disjoint_iff_not_equal domI domain_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y xa. \<lbrakk>ps' = ps(x \<mapsto> paval a ps); ps ## ps2; v = paval a ps; vars a \<subseteq> dom ps; ps x = Some y; xa \<noteq> x\<rbrakk> \<Longrightarrow> (if ps2 xa = None then if xa = x then Some (paval a ps) else ps xa else ps2 xa) = ((\<lambda>a. if ps2 a = None then ps a else ps2 a)(x \<mapsto> paval a (\<lambda>a. if ps2 a = None then ps a else ps2 a))) xa
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps' = ps(x \<mapsto> paval a ps); ps ## ps2; v = paval a ps; vars a \<subseteq> dom ps; ps x = Some y_; xa_ \<noteq> x\<rbrakk> \<Longrightarrow> (if ps2 xa_ = None then if xa_ = x then Some (paval a ps) else ps xa_ else ps2 xa_) = ((\<lambda>a. if ps2 a = None then ps a else ps2 a)(x \<mapsto> paval a (\<lambda>a. if ps2 a = None then ps a else ps2 a))) xa_
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(x ::= a, ps + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> ps' + ps2

goal (5 subgoals):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
 2. \<And>b ps ps' c1 x y c2. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps ## ps2 \<Longrightarrow> (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = x + 1; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
 3. \<And>b ps ps' c2 x y c1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps ## ps2 \<Longrightarrow> (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = x + 1; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
 4. \<And>b s c. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> s + ps2
 5. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; 1 + x + y = z; s1 ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
 2. \<And>b ps ps' c1 x y c2. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps ## ps2 \<Longrightarrow> (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = x + 1; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
 3. \<And>b ps ps' c2 x y c1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps ## ps2 \<Longrightarrow> (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = x + 1; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
 4. \<And>b s c. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> s + ps2
 5. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; 1 + x + y = z; s1 ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
case (IfTrue b ps ps' c1 x y c2)
[PROOF STATE]
proof (state)
this:
vars b \<subseteq> dom ps
dom ps' = dom ps
pbval b ps
(c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'
ps ## ps2 \<Longrightarrow> (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2
y = x + 1
ps ## ps2

goal (5 subgoals):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
 2. \<And>b ps ps' c1 x y c2. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps ## ps2 \<Longrightarrow> (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = x + 1; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
 3. \<And>b ps ps' c2 x y c1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps ## ps2 \<Longrightarrow> (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = x + 1; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
 4. \<And>b s c. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> s + ps2
 5. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; 1 + x + y = z; s1 ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vars b \<subseteq> dom ps
dom ps' = dom ps
pbval b ps
(c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'
ps ## ps2 \<Longrightarrow> (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2
y = x + 1
ps ## ps2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
vars b \<subseteq> dom ps
dom ps' = dom ps
pbval b ps
(c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'
ps ## ps2 \<Longrightarrow> (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2
y = x + 1
ps ## ps2

goal (1 subgoal):
 1. (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
[PROOF STEP]
apply (auto )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A Suc x \<Down> ps' + ps2
[PROOF STEP]
apply(subst big_step_t_part.IfTrue)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2\<rbrakk> \<Longrightarrow> vars b \<subseteq> dom (ps + ps2)
 2. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2\<rbrakk> \<Longrightarrow> dom (ps' + ps2) = dom (ps + ps2)
 3. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2\<rbrakk> \<Longrightarrow> pbval b (ps + ps2)
 4. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2\<rbrakk> \<Longrightarrow> (c1, ps + ps2) \<Rightarrow>\<^sub>A ?x7 \<Down> ps' + ps2
 5. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2\<rbrakk> \<Longrightarrow> Suc x = ?x7 + 1
 6. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
apply (auto simp: pbval_extend)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2; xa \<in> vars b\<rbrakk> \<Longrightarrow> \<exists>y. (ps + ps2) xa = Some y
 2. \<And>xa ya. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2; (ps' + ps2) xa = Some ya\<rbrakk> \<Longrightarrow> \<exists>y. (ps + ps2) xa = Some y
 3. \<And>xa ya. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2; (ps + ps2) xa = Some ya\<rbrakk> \<Longrightarrow> \<exists>y. (ps' + ps2) xa = Some y
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2; xa_ \<in> vars b\<rbrakk> \<Longrightarrow> \<exists>y. (ps + ps2) xa_ = Some y
[PROOF STEP]
by (auto simp: plus_fun_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa ya. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2; (ps' + ps2) xa = Some ya\<rbrakk> \<Longrightarrow> \<exists>y. (ps + ps2) xa = Some y
 2. \<And>xa ya. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2; (ps + ps2) xa = Some ya\<rbrakk> \<Longrightarrow> \<exists>y. (ps' + ps2) xa = Some y
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2; (ps' + ps2) xa_ = Some ya_\<rbrakk> \<Longrightarrow> \<exists>y. (ps + ps2) xa_ = Some y
[PROOF STEP]
by (auto simp: plus_fun_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa ya. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2; (ps + ps2) xa = Some ya\<rbrakk> \<Longrightarrow> \<exists>y. (ps' + ps2) xa = Some y
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2; (ps + ps2) xa_ = Some ya_\<rbrakk> \<Longrightarrow> \<exists>y. (ps' + ps2) xa_ = Some y
[PROOF STEP]
by (auto simp: plus_fun_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2

goal (4 subgoals):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
 2. \<And>b ps ps' c2 x y c1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps ## ps2 \<Longrightarrow> (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = x + 1; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
 3. \<And>b s c. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> s + ps2
 4. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; 1 + x + y = z; s1 ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
 2. \<And>b ps ps' c2 x y c1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps ## ps2 \<Longrightarrow> (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = x + 1; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
 3. \<And>b s c. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> s + ps2
 4. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; 1 + x + y = z; s1 ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
case (IfFalse b ps ps' c2 x y c1)
[PROOF STATE]
proof (state)
this:
vars b \<subseteq> dom ps
dom ps' = dom ps
\<not> pbval b ps
(c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'
ps ## ps2 \<Longrightarrow> (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2
y = x + 1
ps ## ps2

goal (4 subgoals):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
 2. \<And>b ps ps' c2 x y c1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps ## ps2 \<Longrightarrow> (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = x + 1; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
 3. \<And>b s c. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> s + ps2
 4. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; 1 + x + y = z; s1 ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vars b \<subseteq> dom ps
dom ps' = dom ps
\<not> pbval b ps
(c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'
ps ## ps2 \<Longrightarrow> (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2
y = x + 1
ps ## ps2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
vars b \<subseteq> dom ps
dom ps' = dom ps
\<not> pbval b ps
(c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'
ps ## ps2 \<Longrightarrow> (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2
y = x + 1
ps ## ps2

goal (1 subgoal):
 1. (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2
[PROOF STEP]
apply (auto )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A Suc x \<Down> ps' + ps2
[PROOF STEP]
apply(subst big_step_t_part.IfFalse)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2\<rbrakk> \<Longrightarrow> vars b \<subseteq> dom (ps + ps2)
 2. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2\<rbrakk> \<Longrightarrow> dom (ps' + ps2) = dom (ps + ps2)
 3. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2\<rbrakk> \<Longrightarrow> \<not> pbval b (ps + ps2)
 4. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2\<rbrakk> \<Longrightarrow> (c2, ps + ps2) \<Rightarrow>\<^sub>A ?x7 \<Down> ps' + ps2
 5. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2\<rbrakk> \<Longrightarrow> Suc x = ?x7 + 1
 6. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
apply (auto simp: pbval_extend)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2; xa \<in> vars b\<rbrakk> \<Longrightarrow> \<exists>y. (ps + ps2) xa = Some y
 2. \<And>xa ya. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2; (ps' + ps2) xa = Some ya\<rbrakk> \<Longrightarrow> \<exists>y. (ps + ps2) xa = Some y
 3. \<And>xa ya. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2; (ps + ps2) xa = Some ya\<rbrakk> \<Longrightarrow> \<exists>y. (ps' + ps2) xa = Some y
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2; xa_ \<in> vars b\<rbrakk> \<Longrightarrow> \<exists>y. (ps + ps2) xa_ = Some y
[PROOF STEP]
by (auto simp: plus_fun_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa ya. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2; (ps' + ps2) xa = Some ya\<rbrakk> \<Longrightarrow> \<exists>y. (ps + ps2) xa = Some y
 2. \<And>xa ya. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2; (ps + ps2) xa = Some ya\<rbrakk> \<Longrightarrow> \<exists>y. (ps' + ps2) xa = Some y
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2; (ps' + ps2) xa_ = Some ya_\<rbrakk> \<Longrightarrow> \<exists>y. (ps + ps2) xa_ = Some y
[PROOF STEP]
by (auto simp: plus_fun_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa ya. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2; (ps + ps2) xa = Some ya\<rbrakk> \<Longrightarrow> \<exists>y. (ps' + ps2) xa = Some y
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, ps + ps2) \<Rightarrow>\<^sub>A x \<Down> ps' + ps2; y = Suc x; ps ## ps2; (ps + ps2) xa_ = Some ya_\<rbrakk> \<Longrightarrow> \<exists>y. (ps' + ps2) xa_ = Some y
[PROOF STEP]
by (auto simp: plus_fun_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(IF b THEN c1 ELSE c2, ps + ps2) \<Rightarrow>\<^sub>A y \<Down> ps' + ps2

goal (3 subgoals):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
 2. \<And>b s c. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> s + ps2
 3. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; 1 + x + y = z; s1 ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
 2. \<And>b s c. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> s + ps2
 3. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; 1 + x + y = z; s1 ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
case (WhileFalse b s c)
[PROOF STATE]
proof (state)
this:
vars b \<subseteq> dom s
\<not> pbval b s
s ## ps2

goal (3 subgoals):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
 2. \<And>b s c. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> s + ps2
 3. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; 1 + x + y = z; s1 ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vars b \<subseteq> dom s
\<not> pbval b s
s ## ps2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
vars b \<subseteq> dom s
\<not> pbval b s
s ## ps2

goal (1 subgoal):
 1. (WHILE b DO c, s + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> s + ps2
[PROOF STEP]
apply(subst big_step_t_part.WhileFalse)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> vars b \<subseteq> dom (s + ps2)
 2. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> \<not> pbval b (s + ps2)
 3. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> vars b \<subseteq> dom (s + ps2)
[PROOF STEP]
by (auto simp: plus_fun_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> \<not> pbval b (s + ps2)
 2. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> \<not> pbval b (s + ps2)
[PROOF STEP]
by (auto simp: pbval_extend)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s; s ## ps2\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(WHILE b DO c, s + ps2) \<Rightarrow>\<^sub>A Suc 0 \<Down> s + ps2

goal (2 subgoals):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
 2. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; 1 + x + y = z; s1 ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
 2. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; 1 + x + y = z; s1 ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
case (WhileTrue b s1 c x s2 y s3 z)
[PROOF STATE]
proof (state)
this:
pbval b s1
vars b \<subseteq> dom s1
(c, s1) \<Rightarrow>\<^sub>A x \<Down> s2
s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2
(WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3
s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2
1 + x + y = z
s1 ## ps2

goal (2 subgoals):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
 2. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; 1 + x + y = z; s1 ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
from big_step_t3_post_dom_conv[OF WhileTrue(3)]
[PROOF STATE]
proof (chain)
picking this:
dom s2 = dom s1
[PROOF STEP]
have "dom s2 = dom s1"
[PROOF STATE]
proof (prove)
using this:
dom s2 = dom s1

goal (1 subgoal):
 1. dom s2 = dom s1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dom s2 = dom s1

goal (2 subgoals):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
 2. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; 1 + x + y = z; s1 ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
with WhileTrue(8)
[PROOF STATE]
proof (chain)
picking this:
s1 ## ps2
dom s2 = dom s1
[PROOF STEP]
have "s2 ## ps2"
[PROOF STATE]
proof (prove)
using this:
s1 ## ps2
dom s2 = dom s1

goal (1 subgoal):
 1. s2 ## ps2
[PROOF STEP]
unfolding sep_disj_fun_def domain_conv
[PROOF STATE]
proof (prove)
using this:
dom s1 \<inter> dom ps2 = {}
dom s2 = dom s1

goal (1 subgoal):
 1. dom s2 \<inter> dom ps2 = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s2 ## ps2

goal (2 subgoals):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
 2. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; 1 + x + y = z; s1 ## ps2\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
with WhileTrue
[PROOF STATE]
proof (chain)
picking this:
pbval b s1
vars b \<subseteq> dom s1
(c, s1) \<Rightarrow>\<^sub>A x \<Down> s2
s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2
(WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3
s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2
1 + x + y = z
s1 ## ps2
s2 ## ps2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
pbval b s1
vars b \<subseteq> dom s1
(c, s1) \<Rightarrow>\<^sub>A x \<Down> s2
s1 ## ps2 \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2
(WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3
s2 ## ps2 \<Longrightarrow> (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2
1 + x + y = z
s1 ## ps2
s2 ## ps2

goal (1 subgoal):
 1. (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; s1 ## ps2; s2 ## ps2; z = Suc (x + y)\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A Suc (x + y) \<Down> s3 + ps2
[PROOF STEP]
apply(subst big_step_t_part.WhileTrue)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; s1 ## ps2; s2 ## ps2; z = Suc (x + y)\<rbrakk> \<Longrightarrow> pbval b (s1 + ps2)
 2. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; s1 ## ps2; s2 ## ps2; z = Suc (x + y)\<rbrakk> \<Longrightarrow> vars b \<subseteq> dom (s1 + ps2)
 3. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; s1 ## ps2; s2 ## ps2; z = Suc (x + y)\<rbrakk> \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A ?x12 \<Down> ?s2.12
 4. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; s1 ## ps2; s2 ## ps2; z = Suc (x + y)\<rbrakk> \<Longrightarrow> (WHILE b DO c, ?s2.12) \<Rightarrow>\<^sub>A ?y12 \<Down> s3 + ps2
 5. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; s1 ## ps2; s2 ## ps2; z = Suc (x + y)\<rbrakk> \<Longrightarrow> 1 + ?x12 + ?y12 = Suc (x + y)
 6. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; s1 ## ps2; s2 ## ps2; z = Suc (x + y)\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; s1 ## ps2; s2 ## ps2; z = Suc (x + y)\<rbrakk> \<Longrightarrow> pbval b (s1 + ps2)
[PROOF STEP]
by (auto simp: pbval_extend)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; s1 ## ps2; s2 ## ps2; z = Suc (x + y)\<rbrakk> \<Longrightarrow> vars b \<subseteq> dom (s1 + ps2)
 2. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; s1 ## ps2; s2 ## ps2; z = Suc (x + y)\<rbrakk> \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A ?x12 \<Down> ?s2.12
 3. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; s1 ## ps2; s2 ## ps2; z = Suc (x + y)\<rbrakk> \<Longrightarrow> (WHILE b DO c, ?s2.12) \<Rightarrow>\<^sub>A ?y12 \<Down> s3 + ps2
 4. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; s1 ## ps2; s2 ## ps2; z = Suc (x + y)\<rbrakk> \<Longrightarrow> 1 + ?x12 + ?y12 = Suc (x + y)
 5. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; s1 ## ps2; s2 ## ps2; z = Suc (x + y)\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; s1 ## ps2; s2 ## ps2; z = Suc (x + y)\<rbrakk> \<Longrightarrow> vars b \<subseteq> dom (s1 + ps2)
[PROOF STEP]
by (auto simp: plus_fun_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; s1 ## ps2; s2 ## ps2; z = Suc (x + y)\<rbrakk> \<Longrightarrow> (c, s1 + ps2) \<Rightarrow>\<^sub>A ?x12 \<Down> ?s2.12
 2. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; s1 ## ps2; s2 ## ps2; z = Suc (x + y)\<rbrakk> \<Longrightarrow> (WHILE b DO c, ?s2.12) \<Rightarrow>\<^sub>A ?y12 \<Down> s3 + ps2
 3. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; s1 ## ps2; s2 ## ps2; z = Suc (x + y)\<rbrakk> \<Longrightarrow> 1 + ?x12 + ?y12 = Suc (x + y)
 4. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; s1 ## ps2; s2 ## ps2; z = Suc (x + y)\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(WHILE b DO c, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2

goal (1 subgoal):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
case (Seq c1 s1 x s2 c2 y s3 z)
[PROOF STATE]
proof (state)
this:
(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2
s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2
(c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3
s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2
z = x + y
s1 ## ps2

goal (1 subgoal):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
from big_step_t3_post_dom_conv[OF Seq(1)]
[PROOF STATE]
proof (chain)
picking this:
dom s2 = dom s1
[PROOF STEP]
have "dom s2 = dom s1"
[PROOF STATE]
proof (prove)
using this:
dom s2 = dom s1

goal (1 subgoal):
 1. dom s2 = dom s1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dom s2 = dom s1

goal (1 subgoal):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
with Seq(6)
[PROOF STATE]
proof (chain)
picking this:
s1 ## ps2
dom s2 = dom s1
[PROOF STEP]
have "s2 ## ps2"
[PROOF STATE]
proof (prove)
using this:
s1 ## ps2
dom s2 = dom s1

goal (1 subgoal):
 1. s2 ## ps2
[PROOF STEP]
unfolding sep_disj_fun_def domain_conv
[PROOF STATE]
proof (prove)
using this:
dom s1 \<inter> dom ps2 = {}
dom s2 = dom s1

goal (1 subgoal):
 1. dom s2 \<inter> dom ps2 = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s2 ## ps2

goal (1 subgoal):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2\<rbrakk> \<Longrightarrow> (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
with Seq
[PROOF STATE]
proof (chain)
picking this:
(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2
s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2
(c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3
s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2
z = x + y
s1 ## ps2
s2 ## ps2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2
s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2
(c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3
s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2
z = x + y
s1 ## ps2
s2 ## ps2

goal (1 subgoal):
 1. (c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2
[PROOF STEP]
apply (subst big_step_t_part.Seq)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2; s2 ## ps2\<rbrakk> \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A ?x7 \<Down> ?s2.7
 2. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2; s2 ## ps2\<rbrakk> \<Longrightarrow> (c2, ?s2.7) \<Rightarrow>\<^sub>A ?y7 \<Down> s3 + ps2
 3. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2; s2 ## ps2\<rbrakk> \<Longrightarrow> z = ?x7 + ?y7
 4. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 ## ps2 \<Longrightarrow> (c1, s1 + ps2) \<Rightarrow>\<^sub>A x \<Down> s2 + ps2; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 ## ps2 \<Longrightarrow> (c2, s2 + ps2) \<Rightarrow>\<^sub>A y \<Down> s3 + ps2; z = x + y; s1 ## ps2; s2 ## ps2\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(c1;; c2, s1 + ps2) \<Rightarrow>\<^sub>A z \<Down> s3 + ps2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Framer2: "(C, ps1) \<Rightarrow>\<^sub>A m \<Down> ps1' \<Longrightarrow> ps1 ## ps2 \<Longrightarrow> ps = ps1 + ps2 \<Longrightarrow> ps' = ps1'+ps2 \<Longrightarrow> (C, ps) \<Rightarrow>\<^sub>A m \<Down> ps' "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(C, ps1) \<Rightarrow>\<^sub>A m \<Down> ps1'; ps1 ## ps2; ps = ps1 + ps2; ps' = ps1' + ps2\<rbrakk> \<Longrightarrow> (C, ps) \<Rightarrow>\<^sub>A m \<Down> ps'
[PROOF STEP]
using Framer
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?C, ?ps1.0) \<Rightarrow>\<^sub>A ?m \<Down> ?ps1'; ?ps1.0 ## ?ps2.0\<rbrakk> \<Longrightarrow> (?C, ?ps1.0 + ?ps2.0) \<Rightarrow>\<^sub>A ?m \<Down> ?ps1' + ?ps2.0

goal (1 subgoal):
 1. \<lbrakk>(C, ps1) \<Rightarrow>\<^sub>A m \<Down> ps1'; ps1 ## ps2; ps = ps1 + ps2; ps' = ps1' + ps2\<rbrakk> \<Longrightarrow> (C, ps) \<Rightarrow>\<^sub>A m \<Down> ps'
[PROOF STEP]
by auto


[STATEMENT]
lemma paval_aval_part: "paval a (part s) = aval a s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paval a (part s) = aval a s
[PROOF STEP]
apply(induct a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. paval (N x) (part s) = aval (N x) s
 2. \<And>x. paval (V x) (part s) = aval (V x) s
 3. \<And>a1 a2. \<lbrakk>paval a1 (part s) = aval a1 s; paval a2 (part s) = aval a2 s\<rbrakk> \<Longrightarrow> paval (Plus a1 a2) (part s) = aval (Plus a1 a2) s
 4. \<And>a1 a2. \<lbrakk>paval a1 (part s) = aval a1 s; paval a2 (part s) = aval a2 s\<rbrakk> \<Longrightarrow> paval (Times a1 a2) (part s) = aval (Times a1 a2) s
 5. \<And>a1 a2. \<lbrakk>paval a1 (part s) = aval a1 s; paval a2 (part s) = aval a2 s\<rbrakk> \<Longrightarrow> paval (Div a1 a2) (part s) = aval (Div a1 a2) s
[PROOF STEP]
by (auto simp: part_def)