[STATEMENT]
lemma last_index_image_set: "distinct xs \<Longrightarrow> last_index xs ` set xs = {..<size xs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct xs \<Longrightarrow> last_index xs ` set xs = {..<length xs}
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct xs \<Longrightarrow> last_index xs ` set xs = {..<length xs}
[PROOF STEP]
by(induct xs rule:rev_induct) (auto simp add: image_last_index)


[STATEMENT]
lemma D_compE\<^sub>1:
  "\<lbrakk> \<D> e \<lfloor>set Vs\<rfloor>; fv e \<subseteq> set Vs; distinct Vs \<rbrakk> \<Longrightarrow> \<D> (compE\<^sub>1 Vs e) \<lfloor>{..<length Vs}\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<D> e \<lfloor>set Vs\<rfloor>; fv e \<subseteq> set Vs; distinct Vs\<rbrakk> \<Longrightarrow> \<D> (compE\<^sub>1 Vs e) \<lfloor>{..<length Vs}\<rfloor>
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<D> e \<lfloor>set Vs\<rfloor>; fv e \<subseteq> set Vs; distinct Vs\<rbrakk> \<Longrightarrow> \<D> (compE\<^sub>1 Vs e) \<lfloor>{..<length Vs}\<rfloor>
[PROOF STEP]
by(fastforce dest!: D_last_index_compE\<^sub>1[OF subset_refl] simp add:last_index_image_set)


[STATEMENT]
lemma D_compE\<^sub>1':
assumes "\<D> e \<lfloor>set(V#Vs)\<rfloor>" and "fv e \<subseteq> set(V#Vs)" and "distinct(V#Vs)"
shows "\<D> (compE\<^sub>1 (V#Vs) e) \<lfloor>{..length Vs}\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D> (compE\<^sub>1 (V # Vs) e) \<lfloor>{..length Vs}\<rfloor>
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D> (compE\<^sub>1 (V # Vs) e) \<lfloor>{..length Vs}\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<D> (compE\<^sub>1 (V # Vs) e) \<lfloor>{..length Vs}\<rfloor>
[PROOF STEP]
have "{..size Vs} = {..<size(V#Vs)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {..length Vs} = {..<length (V # Vs)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{..length Vs} = {..<length (V # Vs)}

goal (1 subgoal):
 1. \<D> (compE\<^sub>1 (V # Vs) e) \<lfloor>{..length Vs}\<rfloor>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{..length Vs} = {..<length (V # Vs)}

goal (1 subgoal):
 1. \<D> (compE\<^sub>1 (V # Vs) e) \<lfloor>{..length Vs}\<rfloor>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
{..length Vs} = {..<length (V # Vs)}
\<D> e \<lfloor>set (V # Vs)\<rfloor>
fv e \<subseteq> set (V # Vs)
distinct (V # Vs)

goal (1 subgoal):
 1. \<D> (compE\<^sub>1 (V # Vs) e) \<lfloor>{..length Vs}\<rfloor>
[PROOF STEP]
by (simp only:)(rule D_compE\<^sub>1)
[PROOF STATE]
proof (state)
this:
\<D> (compE\<^sub>1 (V # Vs) e) \<lfloor>{..length Vs}\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma compP\<^sub>1_pres_wf: "wf_J_prog P \<Longrightarrow> wf_J\<^sub>1_prog (compP\<^sub>1 P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_J_prog P \<Longrightarrow> wf_J\<^sub>1_prog (compP\<^sub>1 P)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_J_prog P \<Longrightarrow> wf_J\<^sub>1_prog (compP\<^sub>1 P)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_J_prog P \<Longrightarrow> wf_J\<^sub>1_prog (compP\<^sub>1 P)
[PROOF STEP]
assume wf: "wf_J_prog P"
[PROOF STATE]
proof (state)
this:
wf_J_prog P

goal (1 subgoal):
 1. wf_J_prog P \<Longrightarrow> wf_J\<^sub>1_prog (compP\<^sub>1 P)
[PROOF STEP]
let ?f = "(\<lambda>(pns, body). compE\<^sub>1 (this # pns) body)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_J_prog P \<Longrightarrow> wf_J\<^sub>1_prog (compP\<^sub>1 P)
[PROOF STEP]
let ?wf\<^sub>2 = "wf_J\<^sub>1_mdecl"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_J_prog P \<Longrightarrow> wf_J\<^sub>1_prog (compP\<^sub>1 P)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_J_prog P \<Longrightarrow> wf_J\<^sub>1_prog (compP\<^sub>1 P)
[PROOF STEP]
fix C M b Ts T m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_J_prog P \<Longrightarrow> wf_J\<^sub>1_prog (compP\<^sub>1 P)
[PROOF STEP]
assume cM: "P \<turnstile> C sees M :  Ts\<rightarrow>T = m in C"
      and wfm: "wf_mdecl wf_J_mdecl P C (M, Ts, T, m)"
[PROOF STATE]
proof (state)
this:
P \<turnstile> C sees M: Ts\<rightarrow>T = m in C
wf_mdecl wf_J_mdecl P C (M, Ts, T, m)

goal (1 subgoal):
 1. wf_J_prog P \<Longrightarrow> wf_J\<^sub>1_prog (compP\<^sub>1 P)
[PROOF STEP]
obtain pns body where [simp]: "m = (pns, body)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pns body. m = (pns, body) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases m) simp
[PROOF STATE]
proof (state)
this:
m = (pns, body)

goal (1 subgoal):
 1. wf_J_prog P \<Longrightarrow> wf_J\<^sub>1_prog (compP\<^sub>1 P)
[PROOF STEP]
let ?E = "[pns [\<mapsto>] Ts, this \<mapsto> Class C]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_J_prog P \<Longrightarrow> wf_J\<^sub>1_prog (compP\<^sub>1 P)
[PROOF STEP]
obtain T' where WT: "P,?E \<turnstile> body :: T'" and subT: "P \<turnstile> T' \<le> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T'. \<lbrakk>P,[pns [\<mapsto>] Ts, this \<mapsto> Class C] \<turnstile> body :: T'; P \<turnstile> T' \<le> T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfm
[PROOF STATE]
proof (prove)
using this:
wf_mdecl wf_J_mdecl P C (M, Ts, T, m)

goal (1 subgoal):
 1. (\<And>T'. \<lbrakk>P,[pns [\<mapsto>] Ts, this \<mapsto> Class C] \<turnstile> body :: T'; P \<turnstile> T' \<le> T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp: wf_mdecl_def)
[PROOF STATE]
proof (state)
this:
P,[pns [\<mapsto>] Ts, this \<mapsto> Class C] \<turnstile> body :: T'
P \<turnstile> T' \<le> T

goal (1 subgoal):
 1. wf_J_prog P \<Longrightarrow> wf_J\<^sub>1_prog (compP\<^sub>1 P)
[PROOF STEP]
have fv: "fv body \<subseteq> dom ?E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv body \<subseteq> dom [pns [\<mapsto>] Ts, this \<mapsto> Class C]
[PROOF STEP]
by(rule WT_fv[OF WT])
[PROOF STATE]
proof (state)
this:
fv body \<subseteq> dom [pns [\<mapsto>] Ts, this \<mapsto> Class C]

goal (1 subgoal):
 1. wf_J_prog P \<Longrightarrow> wf_J\<^sub>1_prog (compP\<^sub>1 P)
[PROOF STEP]
have "wf_mdecl ?wf\<^sub>2 (compP ?f P) C (M, Ts, T, ?f m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_mdecl wf_J\<^sub>1_mdecl (compP (\<lambda>(pns, body). compE\<^sub>1 (this # pns) body) P) C (M, Ts, T, case m of (pns, body) \<Rightarrow> compE\<^sub>1 (this # pns) body)
[PROOF STEP]
using cM wfm fv
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C sees M: Ts\<rightarrow>T = m in C
wf_mdecl wf_J_mdecl P C (M, Ts, T, m)
fv body \<subseteq> dom [pns [\<mapsto>] Ts, this \<mapsto> Class C]

goal (1 subgoal):
 1. wf_mdecl wf_J\<^sub>1_mdecl (compP (\<lambda>(pns, body). compE\<^sub>1 (this # pns) body) P) C (M, Ts, T, case m of (pns, body) \<Rightarrow> compE\<^sub>1 (this # pns) body)
[PROOF STEP]
by(clarsimp simp add:wf_mdecl_def wf_J\<^sub>1_mdecl_def)
        (fastforce intro!: compE\<^sub>1_pres_wt D_compE\<^sub>1' \<B>)
[PROOF STATE]
proof (state)
this:
wf_mdecl wf_J\<^sub>1_mdecl (compP (\<lambda>(pns, body). compE\<^sub>1 (this # pns) body) P) C (M, Ts, T, case m of (pns, body) \<Rightarrow> compE\<^sub>1 (this # pns) body)

goal (1 subgoal):
 1. wf_J_prog P \<Longrightarrow> wf_J\<^sub>1_prog (compP\<^sub>1 P)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>P \<turnstile> ?C2 sees ?M2: ?Ts2\<rightarrow>?T2 = ?m2 in ?C2; wf_mdecl wf_J_mdecl P ?C2 (?M2, ?Ts2, ?T2, ?m2)\<rbrakk> \<Longrightarrow> wf_mdecl wf_J\<^sub>1_mdecl (compP (\<lambda>(pns, body). compE\<^sub>1 (this # pns) body) P) ?C2 (?M2, ?Ts2, ?T2, case ?m2 of (pns, body) \<Rightarrow> compE\<^sub>1 (this # pns) body)

goal (1 subgoal):
 1. wf_J_prog P \<Longrightarrow> wf_J\<^sub>1_prog (compP\<^sub>1 P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>P \<turnstile> ?C2 sees ?M2: ?Ts2\<rightarrow>?T2 = ?m2 in ?C2; wf_mdecl wf_J_mdecl P ?C2 (?M2, ?Ts2, ?T2, ?m2)\<rbrakk> \<Longrightarrow> wf_mdecl wf_J\<^sub>1_mdecl (compP (\<lambda>(pns, body). compE\<^sub>1 (this # pns) body) P) ?C2 (?M2, ?Ts2, ?T2, case ?m2 of (pns, body) \<Rightarrow> compE\<^sub>1 (this # pns) body)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>P \<turnstile> ?C2 sees ?M2: ?Ts2\<rightarrow>?T2 = ?m2 in ?C2; wf_mdecl wf_J_mdecl P ?C2 (?M2, ?Ts2, ?T2, ?m2)\<rbrakk> \<Longrightarrow> wf_mdecl wf_J\<^sub>1_mdecl (compP (\<lambda>(pns, body). compE\<^sub>1 (this # pns) body) P) ?C2 (?M2, ?Ts2, ?T2, case ?m2 of (pns, body) \<Rightarrow> compE\<^sub>1 (this # pns) body)

goal (1 subgoal):
 1. wf_J\<^sub>1_prog (compP\<^sub>1 P)
[PROOF STEP]
by simp (rule wf_prog_compPI[OF _ wf])
[PROOF STATE]
proof (state)
this:
wf_J\<^sub>1_prog (compP\<^sub>1 P)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma crel_vs1_execute_None:
  False if "crel_vs1 R a b" "execute b heap = None" "P heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
crel_vs1 R a b
execute b heap = None
P heap

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding crel_vs1_def
[PROOF STATE]
proof (prove)
using this:
\<forall>heap. P heap \<longrightarrow> (case execute b heap of None \<Rightarrow> False | Some (v', heap') \<Rightarrow> P heap' \<and> (state_dp_consistency.cmem heap \<longrightarrow> R a v' \<and> state_dp_consistency.cmem heap'))
execute b heap = None
P heap

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto


[STATEMENT]
lemma crel_vs1_execute_Some:
  assumes "crel_vs1 R a b" "P heap"
  obtains x heap' where "execute b heap = Some (x, heap')" "P heap'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x heap'. \<lbrakk>execute b heap = Some (x, heap'); P heap'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
crel_vs1 R a b
P heap

goal (1 subgoal):
 1. (\<And>x heap'. \<lbrakk>execute b heap = Some (x, heap'); P heap'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding crel_vs1_def
[PROOF STATE]
proof (prove)
using this:
\<forall>heap. P heap \<longrightarrow> (case execute b heap of None \<Rightarrow> False | Some (v', heap') \<Rightarrow> P heap' \<and> (state_dp_consistency.cmem heap \<longrightarrow> R a v' \<and> state_dp_consistency.cmem heap'))
P heap

goal (1 subgoal):
 1. (\<And>x heap'. \<lbrakk>execute b heap = Some (x, heap'); P heap'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "execute b heap") auto


[STATEMENT]
lemma crel_vs1_executeD:
  assumes "crel_vs1 R a b" "P heap" "state_dp_consistency.cmem heap"
  obtains x heap' where "execute b heap = Some (x, heap')" "P heap'" "state_dp_consistency.cmem heap'" "R a x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x heap'. \<lbrakk>execute b heap = Some (x, heap'); P heap'; state_dp_consistency.cmem heap'; R a x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
crel_vs1 R a b
P heap
state_dp_consistency.cmem heap

goal (1 subgoal):
 1. (\<And>x heap'. \<lbrakk>execute b heap = Some (x, heap'); P heap'; state_dp_consistency.cmem heap'; R a x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding crel_vs1_def
[PROOF STATE]
proof (prove)
using this:
\<forall>heap. P heap \<longrightarrow> (case execute b heap of None \<Rightarrow> False | Some (v', heap') \<Rightarrow> P heap' \<and> (state_dp_consistency.cmem heap \<longrightarrow> R a v' \<and> state_dp_consistency.cmem heap'))
P heap
state_dp_consistency.cmem heap

goal (1 subgoal):
 1. (\<And>x heap'. \<lbrakk>execute b heap = Some (x, heap'); P heap'; state_dp_consistency.cmem heap'; R a x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "execute b heap") auto


[STATEMENT]
lemma rel_state_state_of:
  "rel_state (=) (state_of b) b" if "crel_vs1 R a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.rel_state (=) (state_of b) b
[PROOF STEP]
unfolding rel_state_def state_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>heap. P heap \<longrightarrow> (case run_state (State (\<lambda>heap. the (execute b heap))) heap of (v1, heap1) \<Rightarrow> case execute b heap of None \<Rightarrow> False | Some (v2, heap2) \<Rightarrow> v1 = v2 \<and> heap1 = heap2 \<and> P heap2)
[PROOF STEP]
by (auto split: option.split elim: crel_vs1_execute_Some[OF that])


[STATEMENT]
lemma crel_vs1_state_of:
  "state_dp_consistency.crel_vs R a (state_of b)" if "crel_vs1 R a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_dp_consistency.crel_vs R a (state_of b)
[PROOF STEP]
unfolding state_dp_consistency.crel_vs_def state_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>M. state_dp_consistency.cmem M \<and> P M \<longrightarrow> (case run_state (State (\<lambda>heap. the (execute b heap))) M of (v', M') \<Rightarrow> R a v' \<and> state_dp_consistency.cmem M' \<and> P M')
[PROOF STEP]
by (auto elim: crel_vs1_executeD[OF that])


[STATEMENT]
lemma crel_vs1_alt_def:
  "crel_vs1 R = (state_dp_consistency.crel_vs R OO rel_state (=))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crel_vs1 R = state_dp_consistency.crel_vs R OO local.rel_state (=)
[PROOF STEP]
proof (intro ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. crel_vs1 R x xa = (state_dp_consistency.crel_vs R OO local.rel_state (=)) x xa
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. crel_vs1 R x xa = (state_dp_consistency.crel_vs R OO local.rel_state (=)) x xa
[PROOF STEP]
have "(state_dp_consistency.crel_vs R OO rel_state (=)) a b" if "crel_vs1 R a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (state_dp_consistency.crel_vs R OO local.rel_state (=)) a b
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
crel_vs1 R a b

goal (1 subgoal):
 1. (state_dp_consistency.crel_vs R OO local.rel_state (=)) a b
[PROOF STEP]
by - (rule relcomppI; erule crel_vs1_state_of rel_state_state_of)
[PROOF STATE]
proof (state)
this:
crel_vs1 R a b \<Longrightarrow> (state_dp_consistency.crel_vs R OO local.rel_state (=)) a b

goal (1 subgoal):
 1. \<And>x xa. crel_vs1 R x xa = (state_dp_consistency.crel_vs R OO local.rel_state (=)) x xa
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
crel_vs1 R a b \<Longrightarrow> (state_dp_consistency.crel_vs R OO local.rel_state (=)) a b

goal (1 subgoal):
 1. \<And>x xa. crel_vs1 R x xa = (state_dp_consistency.crel_vs R OO local.rel_state (=)) x xa
[PROOF STEP]
have "crel_vs1 R a b" if "(state_dp_consistency.crel_vs R OO rel_state (=)) a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crel_vs1 R a b
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
(state_dp_consistency.crel_vs R OO local.rel_state (=)) a b

goal (1 subgoal):
 1. crel_vs1 R a b
[PROOF STEP]
by (auto 4 3 elim: state_dp_consistency.crel_vs_elim rel_state_elim simp: crel_vs1_def)
[PROOF STATE]
proof (state)
this:
(state_dp_consistency.crel_vs R OO local.rel_state (=)) a b \<Longrightarrow> crel_vs1 R a b

goal (1 subgoal):
 1. \<And>x xa. crel_vs1 R x xa = (state_dp_consistency.crel_vs R OO local.rel_state (=)) x xa
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
crel_vs1 R a b \<Longrightarrow> (state_dp_consistency.crel_vs R OO local.rel_state (=)) a b
(state_dp_consistency.crel_vs R OO local.rel_state (=)) a b \<Longrightarrow> crel_vs1 R a b
[PROOF STEP]
show "crel_vs1 R a b = (state_dp_consistency.crel_vs R OO rel_state (=)) a b"
[PROOF STATE]
proof (prove)
using this:
crel_vs1 R a b \<Longrightarrow> (state_dp_consistency.crel_vs R OO local.rel_state (=)) a b
(state_dp_consistency.crel_vs R OO local.rel_state (=)) a b \<Longrightarrow> crel_vs1 R a b

goal (1 subgoal):
 1. crel_vs1 R a b = (state_dp_consistency.crel_vs R OO local.rel_state (=)) a b
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
crel_vs1 R a b = (state_dp_consistency.crel_vs R OO local.rel_state (=)) a b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma transfer_return1[transfer_rule]:
  "(R ===> crel_vs1 R) Wrap return"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (R ===> crel_vs1 R) Wrap return
[PROOF STEP]
unfolding crel_vs1_alt_def Wrap_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (R ===> state_dp_consistency.crel_vs R OO local.rel_state (=)) (\<lambda>x. x) return
[PROOF STEP]
by (rule rel_fun_comp1 state_dp_consistency.return_transfer[unfolded Wrap_def] transfer_return)+ auto


[STATEMENT]
lemma crel_vs_return1:
  "\<lbrakk>R x y\<rbrakk> \<Longrightarrow> crel_vs1 R (Wrap x) (return y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R x y \<Longrightarrow> crel_vs1 R (Wrap x) (return y)
[PROOF STEP]
by (rule transfer_return1[unfolded rel_fun_def, rule_format])


[STATEMENT]
lemma crel_vs_rel_state:
  "(R0 ===> state_dp_consistency.crel_vs R1) x (state_of o y)" if "(R0 ===> state_dp_consistency.crel_vs R1 OO rel_state (=)) x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_dp_consistency.rel_fun_lifted R0 R1 x (state_of \<circ> y)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
(R0 ===> state_dp_consistency.crel_vs R1 OO local.rel_state (=)) x y

goal (1 subgoal):
 1. state_dp_consistency.rel_fun_lifted R0 R1 x (state_of \<circ> y)
[PROOF STEP]
unfolding state_of_def
[PROOF STATE]
proof (prove)
using this:
(R0 ===> state_dp_consistency.crel_vs R1 OO local.rel_state (=)) x y

goal (1 subgoal):
 1. state_dp_consistency.rel_fun_lifted R0 R1 x ((\<lambda>s. State (\<lambda>heap. the (execute s heap))) \<circ> y)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (R0 ===> state_dp_consistency.crel_vs R1 OO local.rel_state (=)) x y \<Longrightarrow> state_dp_consistency.rel_fun_lifted R0 R1 x ((\<lambda>s. State (\<lambda>heap. the (execute s heap))) \<circ> y)
[PROOF STEP]
apply (rule rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa ya. \<lbrakk>(R0 ===> state_dp_consistency.crel_vs R1 OO local.rel_state (=)) x y; R0 xa ya\<rbrakk> \<Longrightarrow> state_dp_consistency.crel_vs R1 (x xa) (((\<lambda>s. State (\<lambda>heap. the (execute s heap))) \<circ> y) ya)
[PROOF STEP]
apply (drule rel_funD, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa ya. \<lbrakk>R0 xa ya; (state_dp_consistency.crel_vs R1 OO local.rel_state (=)) (x xa) (y ya)\<rbrakk> \<Longrightarrow> state_dp_consistency.crel_vs R1 (x xa) (((\<lambda>s. State (\<lambda>heap. the (execute s heap))) \<circ> y) ya)
[PROOF STEP]
apply (erule relcomppE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa ya b. \<lbrakk>R0 xa ya; state_dp_consistency.crel_vs R1 (x xa) b; local.rel_state (=) b (y ya)\<rbrakk> \<Longrightarrow> state_dp_consistency.crel_vs R1 (x xa) (((\<lambda>s. State (\<lambda>heap. the (execute s heap))) \<circ> y) ya)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa ya b. \<lbrakk>R0 xa ya; state_dp_consistency.crel_vs R1 (x xa) b; local.rel_state (=) b (y ya)\<rbrakk> \<Longrightarrow> state_dp_consistency.crel_vs R1 (x xa) (State (\<lambda>heap. the (execute (y ya) heap)))
[PROOF STEP]
apply (rule state_dp_consistency.crel_vs_intro)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa ya b M v' M'. \<lbrakk>R0 xa ya; state_dp_consistency.crel_vs R1 (x xa) b; local.rel_state (=) b (y ya); state_dp_consistency.cmem M; P M; run_state (State (\<lambda>heap. the (execute (y ya) heap))) M = (v', M')\<rbrakk> \<Longrightarrow> R1 (x xa) v' \<and> state_dp_consistency.cmem M' \<and> P M'
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa ya b M v' M'. \<lbrakk>R0 xa ya; state_dp_consistency.crel_vs R1 (x xa) b; local.rel_state (=) b (y ya); state_dp_consistency.cmem M; P M; the (execute (y ya) M) = (v', M')\<rbrakk> \<Longrightarrow> R1 (x xa) v'
 2. \<And>xa ya b M v' M'. \<lbrakk>R0 xa ya; state_dp_consistency.crel_vs R1 (x xa) b; local.rel_state (=) b (y ya); state_dp_consistency.cmem M; P M; the (execute (y ya) M) = (v', M')\<rbrakk> \<Longrightarrow> state_dp_consistency.cmem M'
 3. \<And>xa ya b M v' M'. \<lbrakk>R0 xa ya; state_dp_consistency.crel_vs R1 (x xa) b; local.rel_state (=) b (y ya); state_dp_consistency.cmem M; P M; the (execute (y ya) M) = (v', M')\<rbrakk> \<Longrightarrow> P M'
[PROOF STEP]
apply (erule rel_state_elim, assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa ya b M v' M' heap' v v'a. \<lbrakk>R0 xa ya; state_dp_consistency.crel_vs R1 (x xa) b; state_dp_consistency.cmem M; P M; the (execute (y ya) M) = (v', M'); run_state b M = (v, heap'); execute (y ya) M = Some (v'a, heap'); v = v'a; P heap'\<rbrakk> \<Longrightarrow> R1 (x xa) v'
 2. \<And>xa ya b M v' M'. \<lbrakk>R0 xa ya; state_dp_consistency.crel_vs R1 (x xa) b; local.rel_state (=) b (y ya); state_dp_consistency.cmem M; P M; the (execute (y ya) M) = (v', M')\<rbrakk> \<Longrightarrow> state_dp_consistency.cmem M'
 3. \<And>xa ya b M v' M'. \<lbrakk>R0 xa ya; state_dp_consistency.crel_vs R1 (x xa) b; local.rel_state (=) b (y ya); state_dp_consistency.cmem M; P M; the (execute (y ya) M) = (v', M')\<rbrakk> \<Longrightarrow> P M'
[PROOF STEP]
apply (erule state_dp_consistency.crel_vs_elim)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x ya b M v' M' heap' v v'a. \<lbrakk>R0 x ya; state_dp_consistency.cmem M; P M; the (execute (y ya) M) = (v', M'); run_state b M = (v, heap'); execute (y ya) M = Some (v'a, heap'); v = v'a; P heap'\<rbrakk> \<Longrightarrow> state_dp_consistency.cmem (?M15 x ya b M v' M' heap' v v'a)
 2. \<And>x ya b M v' M' heap' v v'a. \<lbrakk>R0 x ya; state_dp_consistency.cmem M; P M; the (execute (y ya) M) = (v', M'); run_state b M = (v, heap'); execute (y ya) M = Some (v'a, heap'); v = v'a; P heap'\<rbrakk> \<Longrightarrow> P (?M15 x ya b M v' M' heap' v v'a)
 3. \<And>xa ya b M v' M' heap' v v'a v'b M'a. \<lbrakk>R0 xa ya; state_dp_consistency.cmem M; P M; the (execute (y ya) M) = (v', M'); run_state b M = (v, heap'); execute (y ya) M = Some (v'a, heap'); v = v'a; P heap'; run_state b (?M15 xa ya b M v' M' heap' v v'a) = (v'b, M'a); R1 (x xa) v'b; state_dp_consistency.cmem M'a; P M'a\<rbrakk> \<Longrightarrow> R1 (x xa) v'
 4. \<And>xa ya b M v' M'. \<lbrakk>R0 xa ya; state_dp_consistency.crel_vs R1 (x xa) b; local.rel_state (=) b (y ya); state_dp_consistency.cmem M; P M; the (execute (y ya) M) = (v', M')\<rbrakk> \<Longrightarrow> state_dp_consistency.cmem M'
 5. \<And>xa ya b M v' M'. \<lbrakk>R0 xa ya; state_dp_consistency.crel_vs R1 (x xa) b; local.rel_state (=) b (y ya); state_dp_consistency.cmem M; P M; the (execute (y ya) M) = (v', M')\<rbrakk> \<Longrightarrow> P M'
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa ya b M v' M' heap' v v'a v'b M'a. \<lbrakk>R0 xa ya; state_dp_consistency.cmem M; P M; the (execute (y ya) M) = (v', M'); run_state b M = (v, heap'); execute (y ya) M = Some (v'a, heap'); v = v'a; P heap'; run_state b M = (v'b, M'a); R1 (x xa) v'b; state_dp_consistency.cmem M'a; P M'a\<rbrakk> \<Longrightarrow> R1 (x xa) v'
 2. \<And>xa ya b M v' M'. \<lbrakk>R0 xa ya; state_dp_consistency.crel_vs R1 (x xa) b; local.rel_state (=) b (y ya); state_dp_consistency.cmem M; P M; the (execute (y ya) M) = (v', M')\<rbrakk> \<Longrightarrow> state_dp_consistency.cmem M'
 3. \<And>xa ya b M v' M'. \<lbrakk>R0 xa ya; state_dp_consistency.crel_vs R1 (x xa) b; local.rel_state (=) b (y ya); state_dp_consistency.cmem M; P M; the (execute (y ya) M) = (v', M')\<rbrakk> \<Longrightarrow> P M'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa ya b M v' M'. \<lbrakk>R0 xa ya; state_dp_consistency.crel_vs R1 (x xa) b; local.rel_state (=) b (y ya); state_dp_consistency.cmem M; P M; the (execute (y ya) M) = (v', M')\<rbrakk> \<Longrightarrow> state_dp_consistency.cmem M'
 2. \<And>xa ya b M v' M'. \<lbrakk>R0 xa ya; state_dp_consistency.crel_vs R1 (x xa) b; local.rel_state (=) b (y ya); state_dp_consistency.cmem M; P M; the (execute (y ya) M) = (v', M')\<rbrakk> \<Longrightarrow> P M'
[PROOF STEP]
subgoal premises prems for x' y' b M v' M'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_dp_consistency.cmem M'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. state_dp_consistency.cmem M'
[PROOF STEP]
from prems(2,3)
[PROOF STATE]
proof (chain)
picking this:
state_dp_consistency.crel_vs R1 (x x') b
local.rel_state (=) b (y y')
[PROOF STEP]
have "crel_vs1 R1 (x x') (y y')"
[PROOF STATE]
proof (prove)
using this:
state_dp_consistency.crel_vs R1 (x x') b
local.rel_state (=) b (y y')

goal (1 subgoal):
 1. crel_vs1 R1 (x x') (y y')
[PROOF STEP]
unfolding crel_vs1_alt_def
[PROOF STATE]
proof (prove)
using this:
state_dp_consistency.crel_vs R1 (x x') b
local.rel_state (=) b (y y')

goal (1 subgoal):
 1. (state_dp_consistency.crel_vs R1 OO local.rel_state (=)) (x x') (y y')
[PROOF STEP]
by (rule relcomppI)
[PROOF STATE]
proof (state)
this:
crel_vs1 R1 (x x') (y y')

goal (1 subgoal):
 1. state_dp_consistency.cmem M'
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
R0 x' y'
state_dp_consistency.crel_vs R1 (x x') b
local.rel_state (=) b (y y')
state_dp_consistency.cmem M
P M
the (execute (y y') M) = (v', M')
crel_vs1 R1 (x x') (y y')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
R0 x' y'
state_dp_consistency.crel_vs R1 (x x') b
local.rel_state (=) b (y y')
state_dp_consistency.cmem M
P M
the (execute (y y') M) = (v', M')
crel_vs1 R1 (x x') (y y')

goal (1 subgoal):
 1. state_dp_consistency.cmem M'
[PROOF STEP]
by (auto elim: crel_vs1_executeD)
[PROOF STATE]
proof (state)
this:
state_dp_consistency.cmem M'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa ya b M v' M'. \<lbrakk>R0 xa ya; state_dp_consistency.crel_vs R1 (x xa) b; local.rel_state (=) b (y ya); state_dp_consistency.cmem M; P M; the (execute (y ya) M) = (v', M')\<rbrakk> \<Longrightarrow> P M'
[PROOF STEP]
subgoal premises prems for x' y' b M v' M'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P M'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P M'
[PROOF STEP]
from prems(2,3)
[PROOF STATE]
proof (chain)
picking this:
state_dp_consistency.crel_vs R1 (x x') b
local.rel_state (=) b (y y')
[PROOF STEP]
have "crel_vs1 R1 (x x') (y y')"
[PROOF STATE]
proof (prove)
using this:
state_dp_consistency.crel_vs R1 (x x') b
local.rel_state (=) b (y y')

goal (1 subgoal):
 1. crel_vs1 R1 (x x') (y y')
[PROOF STEP]
unfolding crel_vs1_alt_def
[PROOF STATE]
proof (prove)
using this:
state_dp_consistency.crel_vs R1 (x x') b
local.rel_state (=) b (y y')

goal (1 subgoal):
 1. (state_dp_consistency.crel_vs R1 OO local.rel_state (=)) (x x') (y y')
[PROOF STEP]
by (rule relcomppI)
[PROOF STATE]
proof (state)
this:
crel_vs1 R1 (x x') (y y')

goal (1 subgoal):
 1. P M'
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
R0 x' y'
state_dp_consistency.crel_vs R1 (x x') b
local.rel_state (=) b (y y')
state_dp_consistency.cmem M
P M
the (execute (y y') M) = (v', M')
crel_vs1 R1 (x x') (y y')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
R0 x' y'
state_dp_consistency.crel_vs R1 (x x') b
local.rel_state (=) b (y y')
state_dp_consistency.cmem M
P M
the (execute (y y') M) = (v', M')
crel_vs1 R1 (x x') (y y')

goal (1 subgoal):
 1. P M'
[PROOF STEP]
by (auto elim: crel_vs1_executeD)
[PROOF STATE]
proof (state)
this:
P M'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bind_transfer1:
  "(crel_vs1 R0 ===> (R0 ===> crel_vs1 R1) ===> crel_vs1 R1) (\<lambda>v f. f v) (\<bind>)"
  if "\<And> x. R0 x x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (crel_vs1 R0 ===> (R0 ===> crel_vs1 R1) ===> crel_vs1 R1) (\<lambda>v f. f v) (\<bind>)
[PROOF STEP]
unfolding crel_vs1_alt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (state_dp_consistency.crel_vs R0 OO local.rel_state (=) ===> (R0 ===> state_dp_consistency.crel_vs R1 OO local.rel_state (=)) ===> state_dp_consistency.crel_vs R1 OO local.rel_state (=)) (\<lambda>v f. f v) (\<bind>)
[PROOF STEP]
apply (rule rel_fun_comp2')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (state_dp_consistency.crel_vs R0 ===> ?S1.0) (\<lambda>v f. f v) ?g
 2. (local.rel_state (=) ===> ?S2.0) ?g (\<bind>)
 3. \<And>a b. (?S1.0 OO ?S2.0) a b \<Longrightarrow> ((R0 ===> state_dp_consistency.crel_vs R1 OO local.rel_state (=)) ===> state_dp_consistency.crel_vs R1 OO local.rel_state (=)) a b
[PROOF STEP]
apply (rule state_dp_consistency.bind_transfer)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (local.rel_state (=) ===> ?S2.0) (\<bind>) (\<bind>)
 2. \<And>a b. (state_dp_consistency.rel_fun_lifted (state_dp_consistency.rel_fun_lifted R0 ?R1.4) ?R1.4 OO ?S2.0) a b \<Longrightarrow> ((R0 ===> state_dp_consistency.crel_vs R1 OO local.rel_state (=)) ===> state_dp_consistency.crel_vs R1 OO local.rel_state (=)) a b
[PROOF STEP]
apply (rule transfer_bind)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (state_dp_consistency.rel_fun_lifted (state_dp_consistency.rel_fun_lifted R0 ?R1.4) ?R1.4 OO (((=) ===> local.rel_state ?Q5) ===> local.rel_state ?Q5)) a b \<Longrightarrow> ((R0 ===> state_dp_consistency.crel_vs R1 OO local.rel_state (=)) ===> state_dp_consistency.crel_vs R1 OO local.rel_state (=)) a b
[PROOF STEP]
apply (drule rel_fun_relcompp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (state_dp_consistency.rel_fun_lifted R0 ?R1.4 OO ((=) ===> local.rel_state ?Q5) ===> state_dp_consistency.crel_vs ?R1.4 OO local.rel_state ?Q5) a b \<Longrightarrow> ((R0 ===> state_dp_consistency.crel_vs R1 OO local.rel_state (=)) ===> state_dp_consistency.crel_vs R1 OO local.rel_state (=)) a b
[PROOF STEP]
apply (erule rel_fun_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b x y. (R0 ===> state_dp_consistency.crel_vs R1 OO local.rel_state (=)) x y \<longrightarrow> (state_dp_consistency.rel_fun_lifted R0 ?R1.4 OO ((=) ===> local.rel_state ?Q5)) x y
 2. \<And>a b x y. (state_dp_consistency.crel_vs ?R1.4 OO local.rel_state ?Q5) x y \<Longrightarrow> (state_dp_consistency.crel_vs R1 OO local.rel_state (=)) x y
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b x y. (state_dp_consistency.crel_vs ?R1.4 OO local.rel_state ?Q5) x y \<Longrightarrow> (state_dp_consistency.crel_vs R1 OO local.rel_state (=)) x y
 2. \<And>a b x y. (R0 ===> state_dp_consistency.crel_vs R1 OO local.rel_state (=)) x y \<longrightarrow> (state_dp_consistency.rel_fun_lifted R0 ?R1.4 OO ((=) ===> local.rel_state ?Q5)) x y
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b x y. (R0 ===> state_dp_consistency.crel_vs R1 OO local.rel_state (=)) x y \<longrightarrow> (state_dp_consistency.rel_fun_lifted R0 R1 OO ((=) ===> local.rel_state (=))) x y
[PROOF STEP]
apply (intro impI relcomppI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b x y. (R0 ===> state_dp_consistency.crel_vs R1 OO local.rel_state (=)) x y \<Longrightarrow> state_dp_consistency.rel_fun_lifted R0 R1 x (?b12 a b x y)
 2. \<And>a b x y. (R0 ===> state_dp_consistency.crel_vs R1 OO local.rel_state (=)) x y \<Longrightarrow> ((=) ===> local.rel_state (=)) (?b12 a b x y) y
[PROOF STEP]
apply (erule crel_vs_rel_state)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b x y. (R0 ===> state_dp_consistency.crel_vs R1 OO local.rel_state (=)) x y \<Longrightarrow> ((=) ===> local.rel_state (=)) (state_of \<circ> y) y
[PROOF STEP]
by (auto 4 4 dest: rel_funD intro: that elim: rel_state_state_of simp: crel_vs1_alt_def[symmetric])


[STATEMENT]
lemma fun_app_transfer[transfer_rule]:
  "(crel_vs1 (R0 ===> crel_vs1 R1) ===> crel_vs1 R0 ===> crel_vs1 R1) App Heap_Monad_Ext.fun_app_lifted"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (crel_vs1 (R0 ===> crel_vs1 R1) ===> crel_vs1 R0 ===> crel_vs1 R1) App Heap_Monad_Ext.fun_app_lifted
[PROOF STEP]
unfolding App_def Heap_Monad_Ext.fun_app_lifted_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (crel_vs1 (R0 ===> crel_vs1 R1) ===> crel_vs1 R0 ===> crel_vs1 R1) (\<lambda>f. f) (\<lambda>f\<^sub>T x\<^sub>T. f\<^sub>T \<bind> (\<bind>) x\<^sub>T)
[PROOF STEP]
oops