[STATEMENT]
lemma frame_contract_RID:
  assumes "vwb_lens x" "P is RID(x)" "x \<bowtie> y"
  shows "(x;y):[P] = y:[P]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x, y}:[P] = {y}:[P]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {x, y}:[P] = {y}:[P]
[PROOF STEP]
from assms(1,3)
[PROOF STATE]
proof (chain)
picking this:
vwb_lens x
x \<bowtie> y
[PROOF STEP]
have "(x;y):[RID(x)(P)] = y:[RID(x)(P)]"
[PROOF STATE]
proof (prove)
using this:
vwb_lens x
x \<bowtie> y

goal (1 subgoal):
 1. {x, y}:[RID x P] = {y}:[RID x P]
[PROOF STEP]
apply (rel_auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b v va. \<lbrakk>vwb_lens x; x \<bowtie> y; \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, put\<^bsub>x\<^esub> b va); get\<^bsub>x\<^esub> b = get\<^bsub>x\<^esub> a; b = put\<^bsub>x\<^esub> (put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> b)) (get\<^bsub>x\<^esub> a)\<rbrakk> \<Longrightarrow> b = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> b)
 2. \<And>a b v va. \<lbrakk>vwb_lens x; x \<bowtie> y; \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, put\<^bsub>x\<^esub> b va); get\<^bsub>x\<^esub> b = get\<^bsub>x\<^esub> a; b = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> b)\<rbrakk> \<Longrightarrow> b = put\<^bsub>x\<^esub> b (get\<^bsub>x\<^esub> a)
[PROOF STEP]
apply (simp add: lens_indep.lens_put_comm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b v va. \<lbrakk>vwb_lens x; x \<bowtie> y; \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, put\<^bsub>x\<^esub> b va); get\<^bsub>x\<^esub> b = get\<^bsub>x\<^esub> a; b = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> b)\<rbrakk> \<Longrightarrow> b = put\<^bsub>x\<^esub> b (get\<^bsub>x\<^esub> a)
[PROOF STEP]
apply (metis (no_types) vwb_lens_wb wb_lens.get_put)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
{x, y}:[RID x P] = {y}:[RID x P]

goal (1 subgoal):
 1. {x, y}:[P] = {y}:[P]
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{x, y}:[RID x P] = {y}:[RID x P]

goal (1 subgoal):
 1. {x, y}:[P] = {y}:[P]
[PROOF STEP]
by (simp add: Healthy_if assms)
[PROOF STATE]
proof (state)
this:
{x, y}:[P] = {y}:[P]

goal:
No subgoals!
[PROOF STEP]
qed