[STATEMENT]
lemma crdt_ops_rem_penultimate:
  assumes "crdt_ops (xs @ [(i1, r1)] @ [(i2, r2)]) deps"
    and "\<And>r. r \<in> deps r2 \<Longrightarrow> r \<noteq> i1"
  shows "crdt_ops (xs @ [(i2, r2)]) deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crdt_ops (xs @ [(i2, r2)]) deps
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. crdt_ops (xs @ [(i2, r2)]) deps
[PROOF STEP]
have "crdt_ops (xs @ [(i1, r1)]) deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crdt_ops (xs @ [(i1, r1)]) deps
[PROOF STEP]
using assms(1) crdt_ops_rem_last
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ [(i1, r1)] @ [(i2, r2)]) deps
crdt_ops (?xs @ [?x]) ?deps \<Longrightarrow> crdt_ops ?xs ?deps

goal (1 subgoal):
 1. crdt_ops (xs @ [(i1, r1)]) deps
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
crdt_ops (xs @ [(i1, r1)]) deps

goal (1 subgoal):
 1. crdt_ops (xs @ [(i2, r2)]) deps
[PROOF STEP]
hence "crdt_ops xs deps"
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ [(i1, r1)]) deps

goal (1 subgoal):
 1. crdt_ops xs deps
[PROOF STEP]
using crdt_ops_rem_last
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ [(i1, r1)]) deps
crdt_ops (?xs @ [?x]) ?deps \<Longrightarrow> crdt_ops ?xs ?deps

goal (1 subgoal):
 1. crdt_ops xs deps
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
crdt_ops xs deps

goal (1 subgoal):
 1. crdt_ops (xs @ [(i2, r2)]) deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
crdt_ops xs deps

goal (1 subgoal):
 1. crdt_ops (xs @ [(i2, r2)]) deps
[PROOF STEP]
have "distinct (map fst (xs @ [(i1, r1)] @ [(i2, r2)]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst (xs @ [(i1, r1)] @ [(i2, r2)]))
[PROOF STEP]
using assms(1) crdt_ops_distinct_fst
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ [(i1, r1)] @ [(i2, r2)]) deps
crdt_ops ?xs ?deps \<Longrightarrow> distinct (map fst ?xs)

goal (1 subgoal):
 1. distinct (map fst (xs @ [(i1, r1)] @ [(i2, r2)]))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinct (map fst (xs @ [(i1, r1)] @ [(i2, r2)]))

goal (1 subgoal):
 1. crdt_ops (xs @ [(i2, r2)]) deps
[PROOF STEP]
hence "i2 \<notin> set (map fst xs)"
[PROOF STATE]
proof (prove)
using this:
distinct (map fst (xs @ [(i1, r1)] @ [(i2, r2)]))

goal (1 subgoal):
 1. i2 \<notin> set (map fst xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i2 \<notin> set (map fst xs)

goal (1 subgoal):
 1. crdt_ops (xs @ [(i2, r2)]) deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i2 \<notin> set (map fst xs)

goal (1 subgoal):
 1. crdt_ops (xs @ [(i2, r2)]) deps
[PROOF STEP]
have "crdt_ops ((xs @ [(i1, r1)]) @ [(i2, r2)]) deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crdt_ops ((xs @ [(i1, r1)]) @ [(i2, r2)]) deps
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ [(i1, r1)] @ [(i2, r2)]) deps

goal (1 subgoal):
 1. crdt_ops ((xs @ [(i1, r1)]) @ [(i2, r2)]) deps
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
crdt_ops ((xs @ [(i1, r1)]) @ [(i2, r2)]) deps

goal (1 subgoal):
 1. crdt_ops (xs @ [(i2, r2)]) deps
[PROOF STEP]
hence "\<And>r. r \<in> deps r2 \<Longrightarrow> r \<in> fst ` set (xs @ [(i1, r1)])"
[PROOF STATE]
proof (prove)
using this:
crdt_ops ((xs @ [(i1, r1)]) @ [(i2, r2)]) deps

goal (1 subgoal):
 1. \<And>r. r \<in> deps r2 \<Longrightarrow> r \<in> fst ` set (xs @ [(i1, r1)])
[PROOF STEP]
using crdt_ops_ref_exists
[PROOF STATE]
proof (prove)
using this:
crdt_ops ((xs @ [(i1, r1)]) @ [(i2, r2)]) deps
\<lbrakk>crdt_ops (?pre @ (?oid, ?oper) # ?suf) ?deps; ?ref \<in> ?deps ?oper\<rbrakk> \<Longrightarrow> ?ref \<in> fst ` set ?pre

goal (1 subgoal):
 1. \<And>r. r \<in> deps r2 \<Longrightarrow> r \<in> fst ` set (xs @ [(i1, r1)])
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?r \<in> deps r2 \<Longrightarrow> ?r \<in> fst ` set (xs @ [(i1, r1)])

goal (1 subgoal):
 1. crdt_ops (xs @ [(i2, r2)]) deps
[PROOF STEP]
hence "\<And>r. r \<in> deps r2 \<Longrightarrow> r \<in> set (map fst xs)"
[PROOF STATE]
proof (prove)
using this:
?r \<in> deps r2 \<Longrightarrow> ?r \<in> fst ` set (xs @ [(i1, r1)])

goal (1 subgoal):
 1. \<And>r. r \<in> deps r2 \<Longrightarrow> r \<in> set (map fst xs)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
?r \<in> deps r2 \<Longrightarrow> ?r \<in> fst ` set (xs @ [(i1, r1)])
?r \<in> deps r2 \<Longrightarrow> ?r \<noteq> i1

goal (1 subgoal):
 1. \<And>r. r \<in> deps r2 \<Longrightarrow> r \<in> set (map fst xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?r \<in> deps r2 \<Longrightarrow> ?r \<in> set (map fst xs)

goal (1 subgoal):
 1. crdt_ops (xs @ [(i2, r2)]) deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?r \<in> deps r2 \<Longrightarrow> ?r \<in> set (map fst xs)

goal (1 subgoal):
 1. crdt_ops (xs @ [(i2, r2)]) deps
[PROOF STEP]
have "\<And>r. r \<in> deps r2 \<Longrightarrow> r < i2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. r \<in> deps r2 \<Longrightarrow> r < i2
[PROOF STEP]
using assms(1) crdt_ops_ref_less
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ [(i1, r1)] @ [(i2, r2)]) deps
\<lbrakk>crdt_ops ?xs ?deps; (?oid, ?oper) \<in> set ?xs; ?r \<in> ?deps ?oper\<rbrakk> \<Longrightarrow> ?r < ?oid

goal (1 subgoal):
 1. \<And>r. r \<in> deps r2 \<Longrightarrow> r < i2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?r \<in> deps r2 \<Longrightarrow> ?r < i2

goal (1 subgoal):
 1. crdt_ops (xs @ [(i2, r2)]) deps
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
crdt_ops xs deps
i2 \<notin> set (map fst xs)
?r \<in> deps r2 \<Longrightarrow> ?r \<in> set (map fst xs)
?r \<in> deps r2 \<Longrightarrow> ?r < i2
[PROOF STEP]
show "crdt_ops (xs @ [(i2, r2)]) deps"
[PROOF STATE]
proof (prove)
using this:
crdt_ops xs deps
i2 \<notin> set (map fst xs)
?r \<in> deps r2 \<Longrightarrow> ?r \<in> set (map fst xs)
?r \<in> deps r2 \<Longrightarrow> ?r < i2

goal (1 subgoal):
 1. crdt_ops (xs @ [(i2, r2)]) deps
[PROOF STEP]
by (simp add: crdt_ops_intro)
[PROOF STATE]
proof (state)
this:
crdt_ops (xs @ [(i2, r2)]) deps

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma crdt_ops_spec_ops_exist:
  assumes "crdt_ops xs deps"
  shows "\<exists>ys. set xs = set ys \<and> spec_ops ys deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ys. set xs = set ys \<and> spec_ops ys deps
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
crdt_ops xs deps

goal (1 subgoal):
 1. \<exists>ys. set xs = set ys \<and> spec_ops ys deps
[PROOF STEP]
proof(induction xs rule: List.rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. crdt_ops [] deps \<Longrightarrow> \<exists>ys. set [] = set ys \<and> spec_ops ys deps
 2. \<And>x xs. \<lbrakk>crdt_ops xs deps \<Longrightarrow> \<exists>ys. set xs = set ys \<and> spec_ops ys deps; crdt_ops (xs @ [x]) deps\<rbrakk> \<Longrightarrow> \<exists>ys. set (xs @ [x]) = set ys \<and> spec_ops ys deps
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
crdt_ops [] deps

goal (2 subgoals):
 1. crdt_ops [] deps \<Longrightarrow> \<exists>ys. set [] = set ys \<and> spec_ops ys deps
 2. \<And>x xs. \<lbrakk>crdt_ops xs deps \<Longrightarrow> \<exists>ys. set xs = set ys \<and> spec_ops ys deps; crdt_ops (xs @ [x]) deps\<rbrakk> \<Longrightarrow> \<exists>ys. set (xs @ [x]) = set ys \<and> spec_ops ys deps
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
crdt_ops [] deps
[PROOF STEP]
show "\<exists>ys. set [] = set ys \<and> spec_ops ys deps"
[PROOF STATE]
proof (prove)
using this:
crdt_ops [] deps

goal (1 subgoal):
 1. \<exists>ys. set [] = set ys \<and> spec_ops ys deps
[PROOF STEP]
by (simp add: spec_ops_empty)
[PROOF STATE]
proof (state)
this:
\<exists>ys. set [] = set ys \<and> spec_ops ys deps

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>crdt_ops xs deps \<Longrightarrow> \<exists>ys. set xs = set ys \<and> spec_ops ys deps; crdt_ops (xs @ [x]) deps\<rbrakk> \<Longrightarrow> \<exists>ys. set (xs @ [x]) = set ys \<and> spec_ops ys deps
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>crdt_ops xs deps \<Longrightarrow> \<exists>ys. set xs = set ys \<and> spec_ops ys deps; crdt_ops (xs @ [x]) deps\<rbrakk> \<Longrightarrow> \<exists>ys. set (xs @ [x]) = set ys \<and> spec_ops ys deps
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
crdt_ops xs deps \<Longrightarrow> \<exists>ys. set xs = set ys \<and> spec_ops ys deps
crdt_ops (xs @ [x]) deps

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>crdt_ops xs deps \<Longrightarrow> \<exists>ys. set xs = set ys \<and> spec_ops ys deps; crdt_ops (xs @ [x]) deps\<rbrakk> \<Longrightarrow> \<exists>ys. set (xs @ [x]) = set ys \<and> spec_ops ys deps
[PROOF STEP]
hence IH: "\<exists>ys. set xs = set ys \<and> spec_ops ys deps"
[PROOF STATE]
proof (prove)
using this:
crdt_ops xs deps \<Longrightarrow> \<exists>ys. set xs = set ys \<and> spec_ops ys deps
crdt_ops (xs @ [x]) deps

goal (1 subgoal):
 1. \<exists>ys. set xs = set ys \<and> spec_ops ys deps
[PROOF STEP]
using crdt_ops_rem_last
[PROOF STATE]
proof (prove)
using this:
crdt_ops xs deps \<Longrightarrow> \<exists>ys. set xs = set ys \<and> spec_ops ys deps
crdt_ops (xs @ [x]) deps
crdt_ops (?xs @ [?x]) ?deps \<Longrightarrow> crdt_ops ?xs ?deps

goal (1 subgoal):
 1. \<exists>ys. set xs = set ys \<and> spec_ops ys deps
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>ys. set xs = set ys \<and> spec_ops ys deps

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>crdt_ops xs deps \<Longrightarrow> \<exists>ys. set xs = set ys \<and> spec_ops ys deps; crdt_ops (xs @ [x]) deps\<rbrakk> \<Longrightarrow> \<exists>ys. set (xs @ [x]) = set ys \<and> spec_ops ys deps
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>ys. set xs = set ys \<and> spec_ops ys deps
[PROOF STEP]
obtain ys oid ref
    where "set xs = set ys" and "spec_ops ys deps" and "x = (oid, ref)"
[PROOF STATE]
proof (prove)
using this:
\<exists>ys. set xs = set ys \<and> spec_ops ys deps

goal (1 subgoal):
 1. (\<And>ys oid ref. \<lbrakk>set xs = set ys; spec_ops ys deps; x = (oid, ref)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
set xs = set ys
spec_ops ys deps
x = (oid, ref)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>crdt_ops xs deps \<Longrightarrow> \<exists>ys. set xs = set ys \<and> spec_ops ys deps; crdt_ops (xs @ [x]) deps\<rbrakk> \<Longrightarrow> \<exists>ys. set (xs @ [x]) = set ys \<and> spec_ops ys deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set xs = set ys
spec_ops ys deps
x = (oid, ref)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>crdt_ops xs deps \<Longrightarrow> \<exists>ys. set xs = set ys \<and> spec_ops ys deps; crdt_ops (xs @ [x]) deps\<rbrakk> \<Longrightarrow> \<exists>ys. set (xs @ [x]) = set ys \<and> spec_ops ys deps
[PROOF STEP]
have "\<exists>pre suf. ys = pre@suf \<and>
                       (\<forall>i \<in> set (map fst pre). i < oid) \<and>
                       (\<forall>i \<in> set (map fst suf). oid < i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>pre suf. ys = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst suf). oid < i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>pre suf. ys = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst suf). oid < i)
[PROOF STEP]
have "oid \<notin> set (map fst xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oid \<notin> set (map fst xs)
[PROOF STEP]
using calculation(3) crdt_ops_unique_last snoc.prems
[PROOF STATE]
proof (prove)
using this:
x = (oid, ref)
crdt_ops (?xs @ [(?oid, ?oper)]) ?deps \<Longrightarrow> ?oid \<notin> set (map fst ?xs)
crdt_ops (xs @ [x]) deps

goal (1 subgoal):
 1. oid \<notin> set (map fst xs)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
oid \<notin> set (map fst xs)

goal (1 subgoal):
 1. \<exists>pre suf. ys = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst suf). oid < i)
[PROOF STEP]
hence "oid \<notin> set (map fst ys)"
[PROOF STATE]
proof (prove)
using this:
oid \<notin> set (map fst xs)

goal (1 subgoal):
 1. oid \<notin> set (map fst ys)
[PROOF STEP]
by (simp add: calculation(1))
[PROOF STATE]
proof (state)
this:
oid \<notin> set (map fst ys)

goal (1 subgoal):
 1. \<exists>pre suf. ys = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst suf). oid < i)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
oid \<notin> set (map fst ys)

goal (1 subgoal):
 1. \<exists>pre suf. ys = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst suf). oid < i)
[PROOF STEP]
using spec_ops_split \<open>spec_ops ys deps\<close>
[PROOF STATE]
proof (prove)
using this:
oid \<notin> set (map fst ys)
\<lbrakk>spec_ops ?xs ?deps; ?oid \<notin> set (map fst ?xs)\<rbrakk> \<Longrightarrow> \<exists>pre suf. ?xs = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < ?oid) \<and> (\<forall>i\<in>set (map fst suf). ?oid < i)
spec_ops ys deps

goal (1 subgoal):
 1. \<exists>pre suf. ys = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst suf). oid < i)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>pre suf. ys = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst suf). oid < i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>pre suf. ys = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst suf). oid < i)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>crdt_ops xs deps \<Longrightarrow> \<exists>ys. set xs = set ys \<and> spec_ops ys deps; crdt_ops (xs @ [x]) deps\<rbrakk> \<Longrightarrow> \<exists>ys. set (xs @ [x]) = set ys \<and> spec_ops ys deps
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>pre suf. ys = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst suf). oid < i)
[PROOF STEP]
obtain pre suf where "ys = pre @ suf" and
    "\<forall>i \<in> set (map fst pre). i < oid" and
    "\<forall>i \<in> set (map fst suf). oid < i"
[PROOF STATE]
proof (prove)
using this:
\<exists>pre suf. ys = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst suf). oid < i)

goal (1 subgoal):
 1. (\<And>pre suf. \<lbrakk>ys = pre @ suf; \<forall>i\<in>set (map fst pre). i < oid; \<forall>i\<in>set (map fst suf). oid < i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
ys = pre @ suf
\<forall>i\<in>set (map fst pre). i < oid
\<forall>i\<in>set (map fst suf). oid < i

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>crdt_ops xs deps \<Longrightarrow> \<exists>ys. set xs = set ys \<and> spec_ops ys deps; crdt_ops (xs @ [x]) deps\<rbrakk> \<Longrightarrow> \<exists>ys. set (xs @ [x]) = set ys \<and> spec_ops ys deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ys = pre @ suf
\<forall>i\<in>set (map fst pre). i < oid
\<forall>i\<in>set (map fst suf). oid < i

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>crdt_ops xs deps \<Longrightarrow> \<exists>ys. set xs = set ys \<and> spec_ops ys deps; crdt_ops (xs @ [x]) deps\<rbrakk> \<Longrightarrow> \<exists>ys. set (xs @ [x]) = set ys \<and> spec_ops ys deps
[PROOF STEP]
have "set (xs @ [(oid, ref)]) = set (pre @ [(oid, ref)] @ suf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (xs @ [(oid, ref)]) = set (pre @ [(oid, ref)] @ suf)
[PROOF STEP]
using crdt_ops_distinct calculation snoc.prems
[PROOF STATE]
proof (prove)
using this:
crdt_ops ?xs ?deps \<Longrightarrow> distinct ?xs
set xs = set ys
spec_ops ys deps
x = (oid, ref)
ys = pre @ suf
\<forall>i\<in>set (map fst pre). i < oid
\<forall>i\<in>set (map fst suf). oid < i
crdt_ops (xs @ [x]) deps

goal (1 subgoal):
 1. set (xs @ [(oid, ref)]) = set (pre @ [(oid, ref)] @ suf)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (xs @ [(oid, ref)]) = set (pre @ [(oid, ref)] @ suf)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>crdt_ops xs deps \<Longrightarrow> \<exists>ys. set xs = set ys \<and> spec_ops ys deps; crdt_ops (xs @ [x]) deps\<rbrakk> \<Longrightarrow> \<exists>ys. set (xs @ [x]) = set ys \<and> spec_ops ys deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (xs @ [(oid, ref)]) = set (pre @ [(oid, ref)] @ suf)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>crdt_ops xs deps \<Longrightarrow> \<exists>ys. set xs = set ys \<and> spec_ops ys deps; crdt_ops (xs @ [x]) deps\<rbrakk> \<Longrightarrow> \<exists>ys. set (xs @ [x]) = set ys \<and> spec_ops ys deps
[PROOF STEP]
have "spec_ops (pre @ [(oid, ref)] @ suf) deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec_ops (pre @ [(oid, ref)] @ suf) deps
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. spec_ops (pre @ [(oid, ref)] @ suf) deps
[PROOF STEP]
have "\<forall>r \<in> deps ref. r < oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r\<in>deps ref. r < oid
[PROOF STEP]
using calculation(3) crdt_ops_ref_less_last snoc.prems
[PROOF STATE]
proof (prove)
using this:
x = (oid, ref)
\<lbrakk>crdt_ops (?xs @ [(?oid, ?oper)]) ?deps; ?r \<in> ?deps ?oper\<rbrakk> \<Longrightarrow> ?r < ?oid
crdt_ops (xs @ [x]) deps

goal (1 subgoal):
 1. \<forall>r\<in>deps ref. r < oid
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>r\<in>deps ref. r < oid

goal (1 subgoal):
 1. spec_ops (pre @ [(oid, ref)] @ suf) deps
[PROOF STEP]
hence "spec_ops (pre @ [(oid, ref)] @ suf) deps"
[PROOF STATE]
proof (prove)
using this:
\<forall>r\<in>deps ref. r < oid

goal (1 subgoal):
 1. spec_ops (pre @ [(oid, ref)] @ suf) deps
[PROOF STEP]
using spec_ops_add_any calculation
[PROOF STATE]
proof (prove)
using this:
\<forall>r\<in>deps ref. r < oid
\<lbrakk>spec_ops (?xs @ ?ys) ?deps; \<forall>i\<in>set (map fst ?xs). i < ?oid; \<forall>i\<in>set (map fst ?ys). ?oid < i; \<forall>ref\<in>?deps ?oper. ref < ?oid\<rbrakk> \<Longrightarrow> spec_ops (?xs @ [(?oid, ?oper)] @ ?ys) ?deps
set xs = set ys
spec_ops ys deps
x = (oid, ref)
ys = pre @ suf
\<forall>i\<in>set (map fst pre). i < oid
\<forall>i\<in>set (map fst suf). oid < i
set (xs @ [(oid, ref)]) = set (pre @ [(oid, ref)] @ suf)

goal (1 subgoal):
 1. spec_ops (pre @ [(oid, ref)] @ suf) deps
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
spec_ops (pre @ [(oid, ref)] @ suf) deps

goal (1 subgoal):
 1. spec_ops (pre @ [(oid, ref)] @ suf) deps
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
spec_ops (pre @ [(oid, ref)] @ suf) deps

goal (1 subgoal):
 1. spec_ops (pre @ [(oid, ref)] @ suf) deps
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
spec_ops (pre @ [(oid, ref)] @ suf) deps

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
spec_ops (pre @ [(oid, ref)] @ suf) deps

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>crdt_ops xs deps \<Longrightarrow> \<exists>ys. set xs = set ys \<and> spec_ops ys deps; crdt_ops (xs @ [x]) deps\<rbrakk> \<Longrightarrow> \<exists>ys. set (xs @ [x]) = set ys \<and> spec_ops ys deps
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set xs = set ys
spec_ops ys deps
x = (oid, ref)
ys = pre @ suf
\<forall>i\<in>set (map fst pre). i < oid
\<forall>i\<in>set (map fst suf). oid < i
set (xs @ [(oid, ref)]) = set (pre @ [(oid, ref)] @ suf)
spec_ops (pre @ [(oid, ref)] @ suf) deps
[PROOF STEP]
show "\<exists>ys. set (xs @ [x]) = set ys \<and> spec_ops ys deps"
[PROOF STATE]
proof (prove)
using this:
set xs = set ys
spec_ops ys deps
x = (oid, ref)
ys = pre @ suf
\<forall>i\<in>set (map fst pre). i < oid
\<forall>i\<in>set (map fst suf). oid < i
set (xs @ [(oid, ref)]) = set (pre @ [(oid, ref)] @ suf)
spec_ops (pre @ [(oid, ref)] @ suf) deps

goal (1 subgoal):
 1. \<exists>ys. set (xs @ [x]) = set ys \<and> spec_ops ys deps
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>ys. set (xs @ [x]) = set ys \<and> spec_ops ys deps

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bi_unique_intersect_r:
  assumes "bi_unique T"
    and "rel_set T a a'"
    and "rel_set T b b'"
    and "rel_set T (a \<inter> b) xr"
  shows "a' \<inter> b' = xr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
assume "x \<in> a \<inter> b"
[PROOF STATE]
proof (state)
this:
x \<in> a \<inter> b

goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> a \<inter> b
[PROOF STEP]
have "x \<in> a" and "x \<in> b"
[PROOF STATE]
proof (prove)
using this:
x \<in> a \<inter> b

goal (1 subgoal):
 1. x \<in> a &&& x \<in> b
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
x \<in> a
x \<in> b

goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
from assms(2) \<open>x \<in> a\<close>
[PROOF STATE]
proof (chain)
picking this:
rel_set T a a'
x \<in> a
[PROOF STEP]
have "\<exists>y \<in> a'. T x y"
[PROOF STATE]
proof (prove)
using this:
rel_set T a a'
x \<in> a

goal (1 subgoal):
 1. \<exists>y\<in>a'. T x y
[PROOF STEP]
by (rule rel_setD1)
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>a'. T x y

goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>a'. T x y

goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
from assms(3) \<open>x \<in> b\<close>
[PROOF STATE]
proof (chain)
picking this:
rel_set T b b'
x \<in> b
[PROOF STEP]
have "\<exists>y \<in> b'. T x y"
[PROOF STATE]
proof (prove)
using this:
rel_set T b b'
x \<in> b

goal (1 subgoal):
 1. \<exists>y\<in>b'. T x y
[PROOF STEP]
by (rule rel_setD1)
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>b'. T x y

goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>y\<in>a'. T x y
\<exists>y\<in>b'. T x y
[PROOF STEP]
have "\<exists>y \<in> a' \<inter> b'. T x y"
[PROOF STATE]
proof (prove)
using this:
\<exists>y\<in>a'. T x y
\<exists>y\<in>b'. T x y

goal (1 subgoal):
 1. \<exists>y\<in>a' \<inter> b'. T x y
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<exists>y\<in>a'. T x y
\<exists>y\<in>b'. T x y
bi_unique T

goal (1 subgoal):
 1. \<exists>y\<in>a' \<inter> b'. T x y
[PROOF STEP]
by (auto dest: bi_uniqueDr)
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>a' \<inter> b'. T x y

goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> a \<inter> b \<Longrightarrow> \<exists>y\<in>a' \<inter> b'. T ?x2 y

goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
note unique_r = this
[PROOF STATE]
proof (state)
this:
?x2 \<in> a \<inter> b \<Longrightarrow> \<exists>y\<in>a' \<inter> b'. T ?x2 y

goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?x2 \<in> a \<inter> b \<Longrightarrow> \<exists>y\<in>a' \<inter> b'. T ?x2 y

goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
assume "x \<in> a' \<inter> b'"
[PROOF STATE]
proof (state)
this:
x \<in> a' \<inter> b'

goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> a' \<inter> b'
[PROOF STEP]
have "x \<in> a'" and "x \<in> b'"
[PROOF STATE]
proof (prove)
using this:
x \<in> a' \<inter> b'

goal (1 subgoal):
 1. x \<in> a' &&& x \<in> b'
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
x \<in> a'
x \<in> b'

goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
from assms(2) \<open>x \<in> a'\<close>
[PROOF STATE]
proof (chain)
picking this:
rel_set T a a'
x \<in> a'
[PROOF STEP]
have "\<exists>y \<in> a. T y x"
[PROOF STATE]
proof (prove)
using this:
rel_set T a a'
x \<in> a'

goal (1 subgoal):
 1. \<exists>y\<in>a. T y x
[PROOF STEP]
by (rule rel_setD2)
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>a. T y x

goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>a. T y x

goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
from assms(3) \<open>x \<in> b'\<close>
[PROOF STATE]
proof (chain)
picking this:
rel_set T b b'
x \<in> b'
[PROOF STEP]
have "\<exists>y \<in> b. T y x"
[PROOF STATE]
proof (prove)
using this:
rel_set T b b'
x \<in> b'

goal (1 subgoal):
 1. \<exists>y\<in>b. T y x
[PROOF STEP]
by (rule rel_setD2)
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>b. T y x

goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>y\<in>a. T y x
\<exists>y\<in>b. T y x
[PROOF STEP]
have "\<exists>y \<in> a \<inter> b. T y x"
[PROOF STATE]
proof (prove)
using this:
\<exists>y\<in>a. T y x
\<exists>y\<in>b. T y x

goal (1 subgoal):
 1. \<exists>y\<in>a \<inter> b. T y x
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<exists>y\<in>a. T y x
\<exists>y\<in>b. T y x
bi_unique T

goal (1 subgoal):
 1. \<exists>y\<in>a \<inter> b. T y x
[PROOF STEP]
by (auto dest: bi_uniqueDl)
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>a \<inter> b. T y x

goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> a' \<inter> b' \<Longrightarrow> \<exists>y\<in>a \<inter> b. T y ?x2

goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
with unique_r
[PROOF STATE]
proof (chain)
picking this:
?x2 \<in> a \<inter> b \<Longrightarrow> \<exists>y\<in>a' \<inter> b'. T ?x2 y
?x2 \<in> a' \<inter> b' \<Longrightarrow> \<exists>y\<in>a \<inter> b. T y ?x2
[PROOF STEP]
have "rel_set T (a \<inter> b) (a' \<inter> b')"
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> a \<inter> b \<Longrightarrow> \<exists>y\<in>a' \<inter> b'. T ?x2 y
?x2 \<in> a' \<inter> b' \<Longrightarrow> \<exists>y\<in>a \<inter> b. T y ?x2

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
using rel_setI
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> a \<inter> b \<Longrightarrow> \<exists>y\<in>a' \<inter> b'. T ?x2 y
?x2 \<in> a' \<inter> b' \<Longrightarrow> \<exists>y\<in>a \<inter> b. T y ?x2
\<lbrakk>\<And>x. x \<in> ?A \<Longrightarrow> \<exists>y\<in>?B. ?R x y; \<And>y. y \<in> ?B \<Longrightarrow> \<exists>x\<in>?A. ?R x y\<rbrakk> \<Longrightarrow> rel_set ?R ?A ?B

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rel_set T (a \<inter> b) (a' \<inter> b')

goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
with assms(1,4)
[PROOF STATE]
proof (chain)
picking this:
bi_unique T
rel_set T (a \<inter> b) xr
rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bi_unique T
rel_set T (a \<inter> b) xr
rel_set T (a \<inter> b) (a' \<inter> b')

goal (1 subgoal):
 1. a' \<inter> b' = xr
[PROOF STEP]
by (auto dest: bi_uniqueDr bi_unique_rel_set)
[PROOF STATE]
proof (state)
this:
a' \<inter> b' = xr

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bi_unique_intersect_l:
  assumes "bi_unique T"
    and "rel_set T a a'"
    and "rel_set T b b'"
    and "rel_set T xl (a' \<inter> b')"
  shows "a \<inter> b = xl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<inter> b = xl
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<inter> b = xl
[PROOF STEP]
let ?T' = "\<lambda> y x. T x y"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<inter> b = xl
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
bi_unique T
[PROOF STEP]
have "bi_unique ?T'"
[PROOF STATE]
proof (prove)
using this:
bi_unique T

goal (1 subgoal):
 1. bi_unique (\<lambda>y x. T x y)
[PROOF STEP]
unfolding bi_unique_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x y z. T x y \<longrightarrow> T x z \<longrightarrow> y = z) \<and> (\<forall>x y z. T x z \<longrightarrow> T y z \<longrightarrow> x = y)

goal (1 subgoal):
 1. (\<forall>x y z. T y x \<longrightarrow> T z x \<longrightarrow> y = z) \<and> (\<forall>x y z. T z x \<longrightarrow> T z y \<longrightarrow> x = y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bi_unique (\<lambda>y x. T x y)

goal (1 subgoal):
 1. a \<inter> b = xl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bi_unique (\<lambda>y x. T x y)

goal (1 subgoal):
 1. a \<inter> b = xl
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
rel_set T a a'
[PROOF STEP]
have "rel_set ?T' a' a"
[PROOF STATE]
proof (prove)
using this:
rel_set T a a'

goal (1 subgoal):
 1. rel_set (\<lambda>y x. T x y) a' a
[PROOF STEP]
unfolding rel_set_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>a. Bex a' (T x)) \<and> (\<forall>y\<in>a'. \<exists>x\<in>a. T x y)

goal (1 subgoal):
 1. (\<forall>x\<in>a'. \<exists>xa\<in>a. T xa x) \<and> (\<forall>y\<in>a. Bex a' (T y))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rel_set (\<lambda>y x. T x y) a' a

goal (1 subgoal):
 1. a \<inter> b = xl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rel_set (\<lambda>y x. T x y) a' a

goal (1 subgoal):
 1. a \<inter> b = xl
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
rel_set T b b'
[PROOF STEP]
have "rel_set ?T' b' b"
[PROOF STATE]
proof (prove)
using this:
rel_set T b b'

goal (1 subgoal):
 1. rel_set (\<lambda>y x. T x y) b' b
[PROOF STEP]
unfolding rel_set_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>b. Bex b' (T x)) \<and> (\<forall>y\<in>b'. \<exists>x\<in>b. T x y)

goal (1 subgoal):
 1. (\<forall>x\<in>b'. \<exists>xa\<in>b. T xa x) \<and> (\<forall>y\<in>b. Bex b' (T y))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rel_set (\<lambda>y x. T x y) b' b

goal (1 subgoal):
 1. a \<inter> b = xl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rel_set (\<lambda>y x. T x y) b' b

goal (1 subgoal):
 1. a \<inter> b = xl
[PROOF STEP]
from assms(4)
[PROOF STATE]
proof (chain)
picking this:
rel_set T xl (a' \<inter> b')
[PROOF STEP]
have "rel_set ?T' (a' \<inter> b') xl"
[PROOF STATE]
proof (prove)
using this:
rel_set T xl (a' \<inter> b')

goal (1 subgoal):
 1. rel_set (\<lambda>y x. T x y) (a' \<inter> b') xl
[PROOF STEP]
unfolding rel_set_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>xl. Bex (a' \<inter> b') (T x)) \<and> (\<forall>y\<in>a' \<inter> b'. \<exists>x\<in>xl. T x y)

goal (1 subgoal):
 1. (\<forall>x\<in>a' \<inter> b'. \<exists>xa\<in>xl. T xa x) \<and> (\<forall>y\<in>xl. Bex (a' \<inter> b') (T y))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rel_set (\<lambda>y x. T x y) (a' \<inter> b') xl

goal (1 subgoal):
 1. a \<inter> b = xl
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bi_unique (\<lambda>y x. T x y)
rel_set (\<lambda>y x. T x y) a' a
rel_set (\<lambda>y x. T x y) b' b
rel_set (\<lambda>y x. T x y) (a' \<inter> b') xl
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bi_unique (\<lambda>y x. T x y)
rel_set (\<lambda>y x. T x y) a' a
rel_set (\<lambda>y x. T x y) b' b
rel_set (\<lambda>y x. T x y) (a' \<inter> b') xl

goal (1 subgoal):
 1. a \<inter> b = xl
[PROOF STEP]
by (rule bi_unique_intersect_r)
[PROOF STATE]
proof (state)
this:
a \<inter> b = xl

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bi_unique_intersect:
  assumes "bi_unique T" and "rel_set T a a'" and "rel_set T b b'"
  shows "rel_set T (a \<inter> b) (a' \<inter> b')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
fix xl
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
assume "xl \<in> a \<inter> b"
[PROOF STATE]
proof (state)
this:
xl \<in> a \<inter> b

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xl \<in> a \<inter> b
[PROOF STEP]
have "xl \<in> a" and "xl \<in> b"
[PROOF STATE]
proof (prove)
using this:
xl \<in> a \<inter> b

goal (1 subgoal):
 1. xl \<in> a &&& xl \<in> b
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
xl \<in> a
xl \<in> b

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
with assms(3)
[PROOF STATE]
proof (chain)
picking this:
rel_set T b b'
xl \<in> a
xl \<in> b
[PROOF STEP]
obtain xr where "T xl xr"
[PROOF STATE]
proof (prove)
using this:
rel_set T b b'
xl \<in> a
xl \<in> b

goal (1 subgoal):
 1. (\<And>xr. T xl xr \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding rel_set_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>b. Bex b' (T x)) \<and> (\<forall>y\<in>b'. \<exists>x\<in>b. T x y)
xl \<in> a
xl \<in> b

goal (1 subgoal):
 1. (\<And>xr. T xl xr \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T xl xr

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
with assms(1,2) \<open>xl \<in> a\<close>
[PROOF STATE]
proof (chain)
picking this:
bi_unique T
rel_set T a a'
xl \<in> a
T xl xr
[PROOF STEP]
have "xr \<in> a'"
[PROOF STATE]
proof (prove)
using this:
bi_unique T
rel_set T a a'
xl \<in> a
T xl xr

goal (1 subgoal):
 1. xr \<in> a'
[PROOF STEP]
by (auto dest: bi_uniqueDr rel_setD1)
[PROOF STATE]
proof (state)
this:
xr \<in> a'

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xr \<in> a'

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
with assms(1,3) \<open>xl \<in> b\<close> \<open>T xl xr\<close>
[PROOF STATE]
proof (chain)
picking this:
bi_unique T
rel_set T b b'
xl \<in> b
T xl xr
xr \<in> a'
[PROOF STEP]
have "xr \<in> b'"
[PROOF STATE]
proof (prove)
using this:
bi_unique T
rel_set T b b'
xl \<in> b
T xl xr
xr \<in> a'

goal (1 subgoal):
 1. xr \<in> b'
[PROOF STEP]
by (auto dest: bi_uniqueDr rel_setD1)
[PROOF STATE]
proof (state)
this:
xr \<in> b'

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
xr \<in> a'
xr \<in> b'
[PROOF STEP]
have "xr \<in> a' \<inter> b'"
[PROOF STATE]
proof (prove)
using this:
xr \<in> a'
xr \<in> b'

goal (1 subgoal):
 1. xr \<in> a' \<inter> b'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xr \<in> a' \<inter> b'

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
with \<open>T xl xr\<close>
[PROOF STATE]
proof (chain)
picking this:
T xl xr
xr \<in> a' \<inter> b'
[PROOF STEP]
have "\<exists>xr. xr \<in> a' \<inter> b' \<and> T xl xr"
[PROOF STATE]
proof (prove)
using this:
T xl xr
xr \<in> a' \<inter> b'

goal (1 subgoal):
 1. \<exists>xr. xr \<in> a' \<inter> b' \<and> T xl xr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xr. xr \<in> a' \<inter> b' \<and> T xl xr

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?xl2 \<in> a \<inter> b \<Longrightarrow> \<exists>xr. xr \<in> a' \<inter> b' \<and> T ?xl2 xr

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?xl2 \<in> a \<inter> b \<Longrightarrow> \<exists>xr. xr \<in> a' \<inter> b' \<and> T ?xl2 xr
[PROOF STEP]
have prem_lhs: "\<forall>xl \<in> a \<inter> b. \<exists>xr. xr \<in> a' \<inter> b' \<and> T xl xr"
[PROOF STATE]
proof (prove)
using this:
?xl2 \<in> a \<inter> b \<Longrightarrow> \<exists>xr. xr \<in> a' \<inter> b' \<and> T ?xl2 xr

goal (1 subgoal):
 1. \<forall>xl\<in>a \<inter> b. \<exists>xr. xr \<in> a' \<inter> b' \<and> T xl xr
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>xl\<in>a \<inter> b. \<exists>xr. xr \<in> a' \<inter> b' \<and> T xl xr

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>xl\<in>a \<inter> b. \<exists>xr. xr \<in> a' \<inter> b' \<and> T xl xr

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
fix xr
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
assume "xr \<in> a' \<inter> b'"
[PROOF STATE]
proof (state)
this:
xr \<in> a' \<inter> b'

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xr \<in> a' \<inter> b'
[PROOF STEP]
have "xr \<in> a'" and "xr \<in> b'"
[PROOF STATE]
proof (prove)
using this:
xr \<in> a' \<inter> b'

goal (1 subgoal):
 1. xr \<in> a' &&& xr \<in> b'
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
xr \<in> a'
xr \<in> b'

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
with assms(3)
[PROOF STATE]
proof (chain)
picking this:
rel_set T b b'
xr \<in> a'
xr \<in> b'
[PROOF STEP]
obtain xl where "T xl xr"
[PROOF STATE]
proof (prove)
using this:
rel_set T b b'
xr \<in> a'
xr \<in> b'

goal (1 subgoal):
 1. (\<And>xl. T xl xr \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding rel_set_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>b. Bex b' (T x)) \<and> (\<forall>y\<in>b'. \<exists>x\<in>b. T x y)
xr \<in> a'
xr \<in> b'

goal (1 subgoal):
 1. (\<And>xl. T xl xr \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T xl xr

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
with assms(1,2) \<open>xr \<in> a'\<close>
[PROOF STATE]
proof (chain)
picking this:
bi_unique T
rel_set T a a'
xr \<in> a'
T xl xr
[PROOF STEP]
have "xl \<in> a"
[PROOF STATE]
proof (prove)
using this:
bi_unique T
rel_set T a a'
xr \<in> a'
T xl xr

goal (1 subgoal):
 1. xl \<in> a
[PROOF STEP]
by (auto dest: bi_uniqueDl rel_setD2)
[PROOF STATE]
proof (state)
this:
xl \<in> a

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xl \<in> a

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
with assms(1,3) \<open>xr \<in> b'\<close> \<open>T xl xr\<close>
[PROOF STATE]
proof (chain)
picking this:
bi_unique T
rel_set T b b'
xr \<in> b'
T xl xr
xl \<in> a
[PROOF STEP]
have "xl \<in> b"
[PROOF STATE]
proof (prove)
using this:
bi_unique T
rel_set T b b'
xr \<in> b'
T xl xr
xl \<in> a

goal (1 subgoal):
 1. xl \<in> b
[PROOF STEP]
by (auto dest: bi_uniqueDl rel_setD2)
[PROOF STATE]
proof (state)
this:
xl \<in> b

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
xl \<in> a
xl \<in> b
[PROOF STEP]
have "xl \<in> a \<inter> b"
[PROOF STATE]
proof (prove)
using this:
xl \<in> a
xl \<in> b

goal (1 subgoal):
 1. xl \<in> a \<inter> b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xl \<in> a \<inter> b

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
with \<open>T xl xr\<close>
[PROOF STATE]
proof (chain)
picking this:
T xl xr
xl \<in> a \<inter> b
[PROOF STEP]
have "\<exists>xl. xl \<in> a \<inter> b \<and> T xl xr"
[PROOF STATE]
proof (prove)
using this:
T xl xr
xl \<in> a \<inter> b

goal (1 subgoal):
 1. \<exists>xl. xl \<in> a \<inter> b \<and> T xl xr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xl. xl \<in> a \<inter> b \<and> T xl xr

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?xr2 \<in> a' \<inter> b' \<Longrightarrow> \<exists>xl. xl \<in> a \<inter> b \<and> T xl ?xr2

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?xr2 \<in> a' \<inter> b' \<Longrightarrow> \<exists>xl. xl \<in> a \<inter> b \<and> T xl ?xr2
[PROOF STEP]
have prem_rhs: "\<forall>xr \<in> a' \<inter> b'. \<exists>xl. xl \<in> a \<inter> b \<and> T xl xr"
[PROOF STATE]
proof (prove)
using this:
?xr2 \<in> a' \<inter> b' \<Longrightarrow> \<exists>xl. xl \<in> a \<inter> b \<and> T xl ?xr2

goal (1 subgoal):
 1. \<forall>xr\<in>a' \<inter> b'. \<exists>xl. xl \<in> a \<inter> b \<and> T xl xr
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>xr\<in>a' \<inter> b'. \<exists>xl. xl \<in> a \<inter> b \<and> T xl xr

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
from prem_lhs prem_rhs
[PROOF STATE]
proof (chain)
picking this:
\<forall>xl\<in>a \<inter> b. \<exists>xr. xr \<in> a' \<inter> b' \<and> T xl xr
\<forall>xr\<in>a' \<inter> b'. \<exists>xl. xl \<in> a \<inter> b \<and> T xl xr
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>xl\<in>a \<inter> b. \<exists>xr. xr \<in> a' \<inter> b' \<and> T xl xr
\<forall>xr\<in>a' \<inter> b'. \<exists>xl. xl \<in> a \<inter> b \<and> T xl xr

goal (1 subgoal):
 1. rel_set T (a \<inter> b) (a' \<inter> b')
[PROOF STEP]
unfolding rel_set_def
[PROOF STATE]
proof (prove)
using this:
\<forall>xl\<in>a \<inter> b. \<exists>xr. xr \<in> a' \<inter> b' \<and> T xl xr
\<forall>xr\<in>a' \<inter> b'. \<exists>xl. xl \<in> a \<inter> b \<and> T xl xr

goal (1 subgoal):
 1. (\<forall>x\<in>a \<inter> b. Bex (a' \<inter> b') (T x)) \<and> (\<forall>y\<in>a' \<inter> b'. \<exists>x\<in>a \<inter> b. T x y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rel_set T (a \<inter> b) (a' \<inter> b')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bi_unique_union_r:
  assumes "bi_unique T"
    and "rel_set T a a'"
    and "rel_set T b b'"
    and "rel_set T (a \<union> b) xr"
  shows "a' \<union> b' = xr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
assume "x \<in> a \<union> b"
[PROOF STATE]
proof (state)
this:
x \<in> a \<union> b

goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> a \<union> b
[PROOF STEP]
have "x \<in> a \<or> x \<in> b"
[PROOF STATE]
proof (prove)
using this:
x \<in> a \<union> b

goal (1 subgoal):
 1. x \<in> a \<or> x \<in> b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> a \<or> x \<in> b

goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
rel_set T a a'
[PROOF STEP]
have "\<exists>y \<in> a'. T x y" if "x \<in> a"
[PROOF STATE]
proof (prove)
using this:
rel_set T a a'

goal (1 subgoal):
 1. \<exists>y\<in>a'. T x y
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
rel_set T a a'
x \<in> a

goal (1 subgoal):
 1. \<exists>y\<in>a'. T x y
[PROOF STEP]
by (rule rel_setD1)
[PROOF STATE]
proof (state)
this:
x \<in> a \<Longrightarrow> \<exists>y\<in>a'. T x y

goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> a \<Longrightarrow> \<exists>y\<in>a'. T x y

goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
rel_set T b b'
[PROOF STEP]
have "\<exists>y \<in> b'. T x y" if "x \<in> b"
[PROOF STATE]
proof (prove)
using this:
rel_set T b b'

goal (1 subgoal):
 1. \<exists>y\<in>b'. T x y
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
rel_set T b b'
x \<in> b

goal (1 subgoal):
 1. \<exists>y\<in>b'. T x y
[PROOF STEP]
by (rule rel_setD1)
[PROOF STATE]
proof (state)
this:
x \<in> b \<Longrightarrow> \<exists>y\<in>b'. T x y

goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> a \<Longrightarrow> \<exists>y\<in>a'. T x y
x \<in> b \<Longrightarrow> \<exists>y\<in>b'. T x y
[PROOF STEP]
have "\<exists>y \<in> a' \<union> b'. T x y"
[PROOF STATE]
proof (prove)
using this:
x \<in> a \<Longrightarrow> \<exists>y\<in>a'. T x y
x \<in> b \<Longrightarrow> \<exists>y\<in>b'. T x y

goal (1 subgoal):
 1. \<exists>y\<in>a' \<union> b'. T x y
[PROOF STEP]
using \<open>x \<in> a \<or> x \<in> b\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> a \<Longrightarrow> \<exists>y\<in>a'. T x y
x \<in> b \<Longrightarrow> \<exists>y\<in>b'. T x y
x \<in> a \<or> x \<in> b

goal (1 subgoal):
 1. \<exists>y\<in>a' \<union> b'. T x y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>a' \<union> b'. T x y

goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> a \<union> b \<Longrightarrow> \<exists>y\<in>a' \<union> b'. T ?x2 y

goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
note unique_r = this
[PROOF STATE]
proof (state)
this:
?x2 \<in> a \<union> b \<Longrightarrow> \<exists>y\<in>a' \<union> b'. T ?x2 y

goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?x2 \<in> a \<union> b \<Longrightarrow> \<exists>y\<in>a' \<union> b'. T ?x2 y

goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
assume "x \<in> a' \<union> b'"
[PROOF STATE]
proof (state)
this:
x \<in> a' \<union> b'

goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> a' \<union> b'
[PROOF STEP]
have "x \<in> a' \<or> x \<in> b'"
[PROOF STATE]
proof (prove)
using this:
x \<in> a' \<union> b'

goal (1 subgoal):
 1. x \<in> a' \<or> x \<in> b'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> a' \<or> x \<in> b'

goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
rel_set T a a'
[PROOF STEP]
have "\<exists>y \<in> a. T y x" if "x \<in> a'"
[PROOF STATE]
proof (prove)
using this:
rel_set T a a'

goal (1 subgoal):
 1. \<exists>y\<in>a. T y x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
rel_set T a a'
x \<in> a'

goal (1 subgoal):
 1. \<exists>y\<in>a. T y x
[PROOF STEP]
by (rule rel_setD2)
[PROOF STATE]
proof (state)
this:
x \<in> a' \<Longrightarrow> \<exists>y\<in>a. T y x

goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> a' \<Longrightarrow> \<exists>y\<in>a. T y x

goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
rel_set T b b'
[PROOF STEP]
have "\<exists>y \<in> b. T y x" if "x \<in> b'"
[PROOF STATE]
proof (prove)
using this:
rel_set T b b'

goal (1 subgoal):
 1. \<exists>y\<in>b. T y x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
rel_set T b b'
x \<in> b'

goal (1 subgoal):
 1. \<exists>y\<in>b. T y x
[PROOF STEP]
by (rule rel_setD2)
[PROOF STATE]
proof (state)
this:
x \<in> b' \<Longrightarrow> \<exists>y\<in>b. T y x

goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> a' \<Longrightarrow> \<exists>y\<in>a. T y x
x \<in> b' \<Longrightarrow> \<exists>y\<in>b. T y x
[PROOF STEP]
have "\<exists>y \<in> a \<union> b. T y x"
[PROOF STATE]
proof (prove)
using this:
x \<in> a' \<Longrightarrow> \<exists>y\<in>a. T y x
x \<in> b' \<Longrightarrow> \<exists>y\<in>b. T y x

goal (1 subgoal):
 1. \<exists>y\<in>a \<union> b. T y x
[PROOF STEP]
using \<open>x \<in> a' \<or> x \<in> b'\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> a' \<Longrightarrow> \<exists>y\<in>a. T y x
x \<in> b' \<Longrightarrow> \<exists>y\<in>b. T y x
x \<in> a' \<or> x \<in> b'

goal (1 subgoal):
 1. \<exists>y\<in>a \<union> b. T y x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>a \<union> b. T y x

goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> a' \<union> b' \<Longrightarrow> \<exists>y\<in>a \<union> b. T y ?x2

goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
with unique_r
[PROOF STATE]
proof (chain)
picking this:
?x2 \<in> a \<union> b \<Longrightarrow> \<exists>y\<in>a' \<union> b'. T ?x2 y
?x2 \<in> a' \<union> b' \<Longrightarrow> \<exists>y\<in>a \<union> b. T y ?x2
[PROOF STEP]
have "rel_set T (a \<union> b) (a' \<union> b')"
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> a \<union> b \<Longrightarrow> \<exists>y\<in>a' \<union> b'. T ?x2 y
?x2 \<in> a' \<union> b' \<Longrightarrow> \<exists>y\<in>a \<union> b. T y ?x2

goal (1 subgoal):
 1. rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
by (auto intro: rel_setI)
[PROOF STATE]
proof (state)
this:
rel_set T (a \<union> b) (a' \<union> b')

goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
with assms(1,4)
[PROOF STATE]
proof (chain)
picking this:
bi_unique T
rel_set T (a \<union> b) xr
rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bi_unique T
rel_set T (a \<union> b) xr
rel_set T (a \<union> b) (a' \<union> b')

goal (1 subgoal):
 1. a' \<union> b' = xr
[PROOF STEP]
by (auto dest: bi_uniqueDr bi_unique_rel_set)
[PROOF STATE]
proof (state)
this:
a' \<union> b' = xr

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bi_unique_union_l:
  assumes "bi_unique T"
    and "rel_set T a a'"
    and "rel_set T b b'"
    and "rel_set T xl (a' \<union> b')"
  shows "a \<union> b = xl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<union> b = xl
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<union> b = xl
[PROOF STEP]
let ?T' = "\<lambda>y x. T x y"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<union> b = xl
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
bi_unique T
[PROOF STEP]
have "bi_unique ?T'"
[PROOF STATE]
proof (prove)
using this:
bi_unique T

goal (1 subgoal):
 1. bi_unique (\<lambda>y x. T x y)
[PROOF STEP]
unfolding bi_unique_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x y z. T x y \<longrightarrow> T x z \<longrightarrow> y = z) \<and> (\<forall>x y z. T x z \<longrightarrow> T y z \<longrightarrow> x = y)

goal (1 subgoal):
 1. (\<forall>x y z. T y x \<longrightarrow> T z x \<longrightarrow> y = z) \<and> (\<forall>x y z. T z x \<longrightarrow> T z y \<longrightarrow> x = y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bi_unique (\<lambda>y x. T x y)

goal (1 subgoal):
 1. a \<union> b = xl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bi_unique (\<lambda>y x. T x y)

goal (1 subgoal):
 1. a \<union> b = xl
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
rel_set T a a'
[PROOF STEP]
have "rel_set ?T' a' a"
[PROOF STATE]
proof (prove)
using this:
rel_set T a a'

goal (1 subgoal):
 1. rel_set (\<lambda>y x. T x y) a' a
[PROOF STEP]
unfolding rel_set_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>a. Bex a' (T x)) \<and> (\<forall>y\<in>a'. \<exists>x\<in>a. T x y)

goal (1 subgoal):
 1. (\<forall>x\<in>a'. \<exists>xa\<in>a. T xa x) \<and> (\<forall>y\<in>a. Bex a' (T y))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rel_set (\<lambda>y x. T x y) a' a

goal (1 subgoal):
 1. a \<union> b = xl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rel_set (\<lambda>y x. T x y) a' a

goal (1 subgoal):
 1. a \<union> b = xl
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
rel_set T b b'
[PROOF STEP]
have "rel_set ?T' b' b"
[PROOF STATE]
proof (prove)
using this:
rel_set T b b'

goal (1 subgoal):
 1. rel_set (\<lambda>y x. T x y) b' b
[PROOF STEP]
unfolding rel_set_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>b. Bex b' (T x)) \<and> (\<forall>y\<in>b'. \<exists>x\<in>b. T x y)

goal (1 subgoal):
 1. (\<forall>x\<in>b'. \<exists>xa\<in>b. T xa x) \<and> (\<forall>y\<in>b. Bex b' (T y))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rel_set (\<lambda>y x. T x y) b' b

goal (1 subgoal):
 1. a \<union> b = xl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rel_set (\<lambda>y x. T x y) b' b

goal (1 subgoal):
 1. a \<union> b = xl
[PROOF STEP]
from assms(4)
[PROOF STATE]
proof (chain)
picking this:
rel_set T xl (a' \<union> b')
[PROOF STEP]
have "rel_set ?T' (a' \<union> b') xl"
[PROOF STATE]
proof (prove)
using this:
rel_set T xl (a' \<union> b')

goal (1 subgoal):
 1. rel_set (\<lambda>y x. T x y) (a' \<union> b') xl
[PROOF STEP]
unfolding rel_set_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>xl. Bex (a' \<union> b') (T x)) \<and> (\<forall>y\<in>a' \<union> b'. \<exists>x\<in>xl. T x y)

goal (1 subgoal):
 1. (\<forall>x\<in>a' \<union> b'. \<exists>xa\<in>xl. T xa x) \<and> (\<forall>y\<in>xl. Bex (a' \<union> b') (T y))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rel_set (\<lambda>y x. T x y) (a' \<union> b') xl

goal (1 subgoal):
 1. a \<union> b = xl
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bi_unique (\<lambda>y x. T x y)
rel_set (\<lambda>y x. T x y) a' a
rel_set (\<lambda>y x. T x y) b' b
rel_set (\<lambda>y x. T x y) (a' \<union> b') xl
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bi_unique (\<lambda>y x. T x y)
rel_set (\<lambda>y x. T x y) a' a
rel_set (\<lambda>y x. T x y) b' b
rel_set (\<lambda>y x. T x y) (a' \<union> b') xl

goal (1 subgoal):
 1. a \<union> b = xl
[PROOF STEP]
by (rule bi_unique_union_r)
[PROOF STATE]
proof (state)
this:
a \<union> b = xl

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bi_unique_union:
  assumes "bi_unique T" and "rel_set T a a'" and "rel_set T b b'"
  shows "rel_set T (a \<union> b) (a' \<union> b')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
fix xl
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
assume "xl \<in> a \<union> b"
[PROOF STATE]
proof (state)
this:
xl \<in> a \<union> b

goal (1 subgoal):
 1. rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
with assms(2,3)
[PROOF STATE]
proof (chain)
picking this:
rel_set T a a'
rel_set T b b'
xl \<in> a \<union> b
[PROOF STEP]
obtain xr where "T xl xr"
[PROOF STATE]
proof (prove)
using this:
rel_set T a a'
rel_set T b b'
xl \<in> a \<union> b

goal (1 subgoal):
 1. (\<And>xr. T xl xr \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding rel_set_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>a. Bex a' (T x)) \<and> (\<forall>y\<in>a'. \<exists>x\<in>a. T x y)
(\<forall>x\<in>b. Bex b' (T x)) \<and> (\<forall>y\<in>b'. \<exists>x\<in>b. T x y)
xl \<in> a \<union> b

goal (1 subgoal):
 1. (\<And>xr. T xl xr \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T xl xr

goal (1 subgoal):
 1. rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
with assms \<open>xl \<in> a \<union> b\<close>
[PROOF STATE]
proof (chain)
picking this:
bi_unique T
rel_set T a a'
rel_set T b b'
xl \<in> a \<union> b
T xl xr
[PROOF STEP]
have "xr \<in> a' \<union> b'"
[PROOF STATE]
proof (prove)
using this:
bi_unique T
rel_set T a a'
rel_set T b b'
xl \<in> a \<union> b
T xl xr

goal (1 subgoal):
 1. xr \<in> a' \<union> b'
[PROOF STEP]
unfolding bi_unique_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x y z. T x y \<longrightarrow> T x z \<longrightarrow> y = z) \<and> (\<forall>x y z. T x z \<longrightarrow> T y z \<longrightarrow> x = y)
rel_set T a a'
rel_set T b b'
xl \<in> a \<union> b
T xl xr

goal (1 subgoal):
 1. xr \<in> a' \<union> b'
[PROOF STEP]
using Un_iff
[PROOF STATE]
proof (prove)
using this:
(\<forall>x y z. T x y \<longrightarrow> T x z \<longrightarrow> y = z) \<and> (\<forall>x y z. T x z \<longrightarrow> T y z \<longrightarrow> x = y)
rel_set T a a'
rel_set T b b'
xl \<in> a \<union> b
T xl xr
(?c \<in> ?A \<union> ?B) = (?c \<in> ?A \<or> ?c \<in> ?B)

goal (1 subgoal):
 1. xr \<in> a' \<union> b'
[PROOF STEP]
by (metis Un_iff rel_setD1)
[PROOF STATE]
proof (state)
this:
xr \<in> a' \<union> b'

goal (1 subgoal):
 1. rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
with \<open>T xl xr\<close>
[PROOF STATE]
proof (chain)
picking this:
T xl xr
xr \<in> a' \<union> b'
[PROOF STEP]
have "\<exists>xr. xr \<in> a' \<union> b' \<and> T xl xr"
[PROOF STATE]
proof (prove)
using this:
T xl xr
xr \<in> a' \<union> b'

goal (1 subgoal):
 1. \<exists>xr. xr \<in> a' \<union> b' \<and> T xl xr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xr. xr \<in> a' \<union> b' \<and> T xl xr

goal (1 subgoal):
 1. rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?xl2 \<in> a \<union> b \<Longrightarrow> \<exists>xr. xr \<in> a' \<union> b' \<and> T ?xl2 xr

goal (1 subgoal):
 1. rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?xl2 \<in> a \<union> b \<Longrightarrow> \<exists>xr. xr \<in> a' \<union> b' \<and> T ?xl2 xr
[PROOF STEP]
have prem_lhs: "\<forall>xl \<in> a \<union> b. \<exists>xr. xr \<in> a' \<union> b' \<and> T xl xr"
[PROOF STATE]
proof (prove)
using this:
?xl2 \<in> a \<union> b \<Longrightarrow> \<exists>xr. xr \<in> a' \<union> b' \<and> T ?xl2 xr

goal (1 subgoal):
 1. \<forall>xl\<in>a \<union> b. \<exists>xr. xr \<in> a' \<union> b' \<and> T xl xr
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>xl\<in>a \<union> b. \<exists>xr. xr \<in> a' \<union> b' \<and> T xl xr

goal (1 subgoal):
 1. rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>xl\<in>a \<union> b. \<exists>xr. xr \<in> a' \<union> b' \<and> T xl xr

goal (1 subgoal):
 1. rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
fix xr
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
assume "xr \<in> a' \<union> b'"
[PROOF STATE]
proof (state)
this:
xr \<in> a' \<union> b'

goal (1 subgoal):
 1. rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
with assms(2,3)
[PROOF STATE]
proof (chain)
picking this:
rel_set T a a'
rel_set T b b'
xr \<in> a' \<union> b'
[PROOF STEP]
obtain xl where "T xl xr"
[PROOF STATE]
proof (prove)
using this:
rel_set T a a'
rel_set T b b'
xr \<in> a' \<union> b'

goal (1 subgoal):
 1. (\<And>xl. T xl xr \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding rel_set_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>a. Bex a' (T x)) \<and> (\<forall>y\<in>a'. \<exists>x\<in>a. T x y)
(\<forall>x\<in>b. Bex b' (T x)) \<and> (\<forall>y\<in>b'. \<exists>x\<in>b. T x y)
xr \<in> a' \<union> b'

goal (1 subgoal):
 1. (\<And>xl. T xl xr \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T xl xr

goal (1 subgoal):
 1. rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
with assms \<open>xr \<in> a' \<union> b'\<close>
[PROOF STATE]
proof (chain)
picking this:
bi_unique T
rel_set T a a'
rel_set T b b'
xr \<in> a' \<union> b'
T xl xr
[PROOF STEP]
have "xl \<in> a \<union> b"
[PROOF STATE]
proof (prove)
using this:
bi_unique T
rel_set T a a'
rel_set T b b'
xr \<in> a' \<union> b'
T xl xr

goal (1 subgoal):
 1. xl \<in> a \<union> b
[PROOF STEP]
unfolding bi_unique_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x y z. T x y \<longrightarrow> T x z \<longrightarrow> y = z) \<and> (\<forall>x y z. T x z \<longrightarrow> T y z \<longrightarrow> x = y)
rel_set T a a'
rel_set T b b'
xr \<in> a' \<union> b'
T xl xr

goal (1 subgoal):
 1. xl \<in> a \<union> b
[PROOF STEP]
by (metis Un_iff rel_setD2)
[PROOF STATE]
proof (state)
this:
xl \<in> a \<union> b

goal (1 subgoal):
 1. rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
with \<open>T xl xr\<close>
[PROOF STATE]
proof (chain)
picking this:
T xl xr
xl \<in> a \<union> b
[PROOF STEP]
have "\<exists>xl. xl \<in> a \<union> b \<and> T xl xr"
[PROOF STATE]
proof (prove)
using this:
T xl xr
xl \<in> a \<union> b

goal (1 subgoal):
 1. \<exists>xl. xl \<in> a \<union> b \<and> T xl xr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xl. xl \<in> a \<union> b \<and> T xl xr

goal (1 subgoal):
 1. rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?xr2 \<in> a' \<union> b' \<Longrightarrow> \<exists>xl. xl \<in> a \<union> b \<and> T xl ?xr2

goal (1 subgoal):
 1. rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?xr2 \<in> a' \<union> b' \<Longrightarrow> \<exists>xl. xl \<in> a \<union> b \<and> T xl ?xr2
[PROOF STEP]
have prem_rhs: "\<forall>xr \<in> a' \<union> b'. \<exists>xl. xl \<in> a \<union> b \<and> T xl xr"
[PROOF STATE]
proof (prove)
using this:
?xr2 \<in> a' \<union> b' \<Longrightarrow> \<exists>xl. xl \<in> a \<union> b \<and> T xl ?xr2

goal (1 subgoal):
 1. \<forall>xr\<in>a' \<union> b'. \<exists>xl. xl \<in> a \<union> b \<and> T xl xr
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>xr\<in>a' \<union> b'. \<exists>xl. xl \<in> a \<union> b \<and> T xl xr

goal (1 subgoal):
 1. rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
from prem_lhs prem_rhs
[PROOF STATE]
proof (chain)
picking this:
\<forall>xl\<in>a \<union> b. \<exists>xr. xr \<in> a' \<union> b' \<and> T xl xr
\<forall>xr\<in>a' \<union> b'. \<exists>xl. xl \<in> a \<union> b \<and> T xl xr
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>xl\<in>a \<union> b. \<exists>xr. xr \<in> a' \<union> b' \<and> T xl xr
\<forall>xr\<in>a' \<union> b'. \<exists>xl. xl \<in> a \<union> b \<and> T xl xr

goal (1 subgoal):
 1. rel_set T (a \<union> b) (a' \<union> b')
[PROOF STEP]
unfolding rel_set_def
[PROOF STATE]
proof (prove)
using this:
\<forall>xl\<in>a \<union> b. \<exists>xr. xr \<in> a' \<union> b' \<and> T xl xr
\<forall>xr\<in>a' \<union> b'. \<exists>xl. xl \<in> a \<union> b \<and> T xl xr

goal (1 subgoal):
 1. (\<forall>x\<in>a \<union> b. Bex (a' \<union> b') (T x)) \<and> (\<forall>y\<in>a' \<union> b'. \<exists>x\<in>a \<union> b. T x y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rel_set T (a \<union> b) (a' \<union> b')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bi_unique_Union_r:
  fixes T :: "['a, 'b] \<Rightarrow> bool" and K
  defines K':  "K' \<equiv> {(x, y). rel_set T x y} `` K"
  assumes "bi_unique T"
    and "\<Union>K \<subseteq> Collect (Domainp T)"
    and "rel_set T (\<Union>K) xr"
  shows "\<Union>K' = xr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
assume "x \<in> \<Union>K"
[PROOF STATE]
proof (state)
this:
x \<in> \<Union> K

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<Union> K
[PROOF STEP]
obtain k where "x \<in> k" and "k \<in> K"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<Union> K

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>x \<in> k; k \<in> K\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
x \<in> k
k \<in> K

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
K' \<equiv> {(x, y). rel_set T x y} `` K
bi_unique T
\<Union> K \<subseteq> Collect (Domainp T)
rel_set T (\<Union> K) xr
[PROOF STEP]
have ex_k'_prem: "\<forall>k \<in> K. \<forall>x \<in> k. \<exists>x'. T x x'"
[PROOF STATE]
proof (prove)
using this:
K' \<equiv> {(x, y). rel_set T x y} `` K
bi_unique T
\<Union> K \<subseteq> Collect (Domainp T)
rel_set T (\<Union> K) xr

goal (1 subgoal):
 1. \<forall>k\<in>K. \<forall>x\<in>k. \<exists>x'. T x x'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>k\<in>K. \<forall>x\<in>k. \<exists>x'. T x x'

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
define k' where k': "k' = {x'. \<exists>x \<in> k. T x x'}"
[PROOF STATE]
proof (state)
this:
k' = {x'. \<exists>x\<in>k. T x x'}

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
have "rel_set T k k'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_set T k k'
[PROOF STEP]
unfolding rel_set_def Bex_def k'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>k. \<exists>xa. xa \<in> {x'. \<exists>x. x \<in> k \<and> T x x'} \<and> T x xa) \<and> (\<forall>y\<in>{x'. \<exists>x. x \<in> k \<and> T x x'}. \<exists>x. x \<in> k \<and> T x y)
[PROOF STEP]
using \<open>k \<in> K\<close>
[PROOF STATE]
proof (prove)
using this:
k \<in> K

goal (1 subgoal):
 1. (\<forall>x\<in>k. \<exists>xa. xa \<in> {x'. \<exists>x. x \<in> k \<and> T x x'} \<and> T x xa) \<and> (\<forall>y\<in>{x'. \<exists>x. x \<in> k \<and> T x x'}. \<exists>x. x \<in> k \<and> T x y)
[PROOF STEP]
by (blast dest: ex_k'_prem[rule_format])
[PROOF STATE]
proof (state)
this:
rel_set T k k'

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
with \<open>k \<in> K\<close>
[PROOF STATE]
proof (chain)
picking this:
k \<in> K
rel_set T k k'
[PROOF STEP]
have "k' \<in> K'"
[PROOF STATE]
proof (prove)
using this:
k \<in> K
rel_set T k k'

goal (1 subgoal):
 1. k' \<in> K'
[PROOF STEP]
unfolding K'
[PROOF STATE]
proof (prove)
using this:
k \<in> K
rel_set T k k'

goal (1 subgoal):
 1. k' \<in> {(x, y). rel_set T x y} `` K
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k' \<in> K'

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
from \<open>rel_set T k k'\<close> \<open>x \<in> k\<close>
[PROOF STATE]
proof (chain)
picking this:
rel_set T k k'
x \<in> k
[PROOF STEP]
obtain y where "y \<in> k' \<and> T x y"
[PROOF STATE]
proof (prove)
using this:
rel_set T k k'
x \<in> k

goal (1 subgoal):
 1. (\<And>y. y \<in> k' \<and> T x y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest: rel_setD1)
[PROOF STATE]
proof (state)
this:
y \<in> k' \<and> T x y

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> k' \<and> T x y
[PROOF STEP]
have "\<exists>y \<in> \<Union>K'. T x y"
[PROOF STATE]
proof (prove)
using this:
y \<in> k' \<and> T x y

goal (1 subgoal):
 1. \<exists>y\<in>\<Union> K'. T x y
[PROOF STEP]
using \<open>k' \<in> K'\<close>
[PROOF STATE]
proof (prove)
using this:
y \<in> k' \<and> T x y
k' \<in> K'

goal (1 subgoal):
 1. \<exists>y\<in>\<Union> K'. T x y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>\<Union> K'. T x y

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> \<Union> K \<Longrightarrow> \<exists>y\<in>\<Union> K'. T ?x2 y

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
note unique_r = this
[PROOF STATE]
proof (state)
this:
?x2 \<in> \<Union> K \<Longrightarrow> \<exists>y\<in>\<Union> K'. T ?x2 y

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?x2 \<in> \<Union> K \<Longrightarrow> \<exists>y\<in>\<Union> K'. T ?x2 y

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
fix x'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
assume "x' \<in> \<Union>K'"
[PROOF STATE]
proof (state)
this:
x' \<in> \<Union> K'

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x' \<in> \<Union> K'
[PROOF STEP]
obtain k' where "x' \<in> k'" and "k' \<in> K'"
[PROOF STATE]
proof (prove)
using this:
x' \<in> \<Union> K'

goal (1 subgoal):
 1. (\<And>k'. \<lbrakk>x' \<in> k'; k' \<in> K'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
x' \<in> k'
k' \<in> K'

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x' \<in> k'
k' \<in> K'
[PROOF STEP]
have ex_k_prem: "\<forall>k' \<in> K'. \<forall>x \<in> k'. \<exists>x. T x x'"
[PROOF STATE]
proof (prove)
using this:
x' \<in> k'
k' \<in> K'

goal (1 subgoal):
 1. \<forall>k'\<in>K'. \<forall>x\<in>k'. \<exists>x. T x x'
[PROOF STEP]
unfolding K'
[PROOF STATE]
proof (prove)
using this:
x' \<in> k'
k' \<in> {(x, y). rel_set T x y} `` K

goal (1 subgoal):
 1. \<forall>k'\<in>{(x, y). rel_set T x y} `` K. \<forall>x\<in>k'. \<exists>x. T x x'
[PROOF STEP]
by (auto dest: rel_setD2)
[PROOF STATE]
proof (state)
this:
\<forall>k'\<in>K'. \<forall>x\<in>k'. \<exists>x. T x x'

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
define k where k: "k = {x. \<exists>x' \<in> k'. T x x'}"
[PROOF STATE]
proof (state)
this:
k = {x. \<exists>x'\<in>k'. T x x'}

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
have "rel_set T k k'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_set T k k'
[PROOF STEP]
unfolding rel_set_def Bex_def k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>{x. \<exists>xa. xa \<in> k' \<and> T x xa}. \<exists>xa. xa \<in> k' \<and> T x xa) \<and> (\<forall>y\<in>k'. \<exists>x. x \<in> {x. \<exists>xa. xa \<in> k' \<and> T x xa} \<and> T x y)
[PROOF STEP]
using \<open>k' \<in> K'\<close> K'
[PROOF STATE]
proof (prove)
using this:
k' \<in> K'
K' \<equiv> {(x, y). rel_set T x y} `` K

goal (1 subgoal):
 1. (\<forall>x\<in>{x. \<exists>xa. xa \<in> k' \<and> T x xa}. \<exists>xa. xa \<in> k' \<and> T x xa) \<and> (\<forall>y\<in>k'. \<exists>x. x \<in> {x. \<exists>xa. xa \<in> k' \<and> T x xa} \<and> T x y)
[PROOF STEP]
by (blast dest: rel_setD2)
[PROOF STATE]
proof (state)
this:
rel_set T k k'

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
bi_unique T
[PROOF STEP]
have "bi_unique (rel_set T)"
[PROOF STATE]
proof (prove)
using this:
bi_unique T

goal (1 subgoal):
 1. bi_unique (rel_set T)
[PROOF STEP]
by (rule bi_unique_rel_set)
[PROOF STATE]
proof (state)
this:
bi_unique (rel_set T)

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
with \<open>rel_set T k k'\<close>
[PROOF STATE]
proof (chain)
picking this:
rel_set T k k'
bi_unique (rel_set T)
[PROOF STEP]
have "\<exists>!k. rel_set T k k'"
[PROOF STATE]
proof (prove)
using this:
rel_set T k k'
bi_unique (rel_set T)

goal (1 subgoal):
 1. \<exists>!k. rel_set T k k'
[PROOF STEP]
by (auto dest: bi_uniqueDl)
[PROOF STATE]
proof (state)
this:
\<exists>!k. rel_set T k k'

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
with \<open>rel_set T k k'\<close> K' \<open>k' \<in> K'\<close>
[PROOF STATE]
proof (chain)
picking this:
rel_set T k k'
K' \<equiv> {(x, y). rel_set T x y} `` K
k' \<in> K'
\<exists>!k. rel_set T k k'
[PROOF STEP]
have "k \<in> K"
[PROOF STATE]
proof (prove)
using this:
rel_set T k k'
K' \<equiv> {(x, y). rel_set T x y} `` K
k' \<in> K'
\<exists>!k. rel_set T k k'

goal (1 subgoal):
 1. k \<in> K
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<in> K

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
from \<open>rel_set T k k'\<close> \<open>x' \<in> k'\<close>
[PROOF STATE]
proof (chain)
picking this:
rel_set T k k'
x' \<in> k'
[PROOF STEP]
obtain y where "y \<in> k \<and> T y x'"
[PROOF STATE]
proof (prove)
using this:
rel_set T k k'
x' \<in> k'

goal (1 subgoal):
 1. (\<And>y. y \<in> k \<and> T y x' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest: rel_setD2)
[PROOF STATE]
proof (state)
this:
y \<in> k \<and> T y x'

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> k \<and> T y x'
[PROOF STEP]
have "\<exists>y \<in> \<Union>K. T y x'"
[PROOF STATE]
proof (prove)
using this:
y \<in> k \<and> T y x'

goal (1 subgoal):
 1. \<exists>y\<in>\<Union> K. T y x'
[PROOF STEP]
using \<open>k \<in> K\<close>
[PROOF STATE]
proof (prove)
using this:
y \<in> k \<and> T y x'
k \<in> K

goal (1 subgoal):
 1. \<exists>y\<in>\<Union> K. T y x'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>\<Union> K. T y x'

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x'2 \<in> \<Union> K' \<Longrightarrow> \<exists>y\<in>\<Union> K. T y ?x'2

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
with unique_r
[PROOF STATE]
proof (chain)
picking this:
?x2 \<in> \<Union> K \<Longrightarrow> \<exists>y\<in>\<Union> K'. T ?x2 y
?x'2 \<in> \<Union> K' \<Longrightarrow> \<exists>y\<in>\<Union> K. T y ?x'2
[PROOF STEP]
have "rel_set T (\<Union>K) (\<Union>K')"
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> \<Union> K \<Longrightarrow> \<exists>y\<in>\<Union> K'. T ?x2 y
?x'2 \<in> \<Union> K' \<Longrightarrow> \<exists>y\<in>\<Union> K. T y ?x'2

goal (1 subgoal):
 1. rel_set T (\<Union> K) (\<Union> K')
[PROOF STEP]
by (intro rel_setI)
[PROOF STATE]
proof (state)
this:
rel_set T (\<Union> K) (\<Union> K')

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
with assms(2,4)
[PROOF STATE]
proof (chain)
picking this:
bi_unique T
rel_set T (\<Union> K) xr
rel_set T (\<Union> K) (\<Union> K')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bi_unique T
rel_set T (\<Union> K) xr
rel_set T (\<Union> K) (\<Union> K')

goal (1 subgoal):
 1. \<Union> K' = xr
[PROOF STEP]
by (auto dest: bi_uniqueDr bi_unique_rel_set)
[PROOF STATE]
proof (state)
this:
\<Union> K' = xr

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bi_unique_Union_l:
  fixes T :: "['a, 'b] \<Rightarrow> bool" and K'
  defines K: "K \<equiv> {(x, y). rel_set (\<lambda> y x. T x y) x y} `` K'"
  assumes "bi_unique T"
    and "\<Union>K' \<subseteq> Collect (Rangep T)"
    and "rel_set T xl (\<Union>K')"
  shows "\<Union>K = xl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> K = xl
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> K = xl
[PROOF STEP]
let ?T' = "\<lambda> y x. T x y"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> K = xl
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
bi_unique T
[PROOF STEP]
have "bi_unique ?T'"
[PROOF STATE]
proof (prove)
using this:
bi_unique T

goal (1 subgoal):
 1. bi_unique (\<lambda>y x. T x y)
[PROOF STEP]
unfolding bi_unique_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x y z. T x y \<longrightarrow> T x z \<longrightarrow> y = z) \<and> (\<forall>x y z. T x z \<longrightarrow> T y z \<longrightarrow> x = y)

goal (1 subgoal):
 1. (\<forall>x y z. T y x \<longrightarrow> T z x \<longrightarrow> y = z) \<and> (\<forall>x y z. T z x \<longrightarrow> T z y \<longrightarrow> x = y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bi_unique (\<lambda>y x. T x y)

goal (1 subgoal):
 1. \<Union> K = xl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bi_unique (\<lambda>y x. T x y)

goal (1 subgoal):
 1. \<Union> K = xl
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
\<Union> K' \<subseteq> Collect (Rangep T)
[PROOF STEP]
have "\<Union>K' \<subseteq> Collect (Domainp ?T')"
[PROOF STATE]
proof (prove)
using this:
\<Union> K' \<subseteq> Collect (Rangep T)

goal (1 subgoal):
 1. \<Union> K' \<subseteq> Collect (Domainp (\<lambda>y x. T x y))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<Union> K' \<subseteq> Collect (Domainp (\<lambda>y x. T x y))

goal (1 subgoal):
 1. \<Union> K = xl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Union> K' \<subseteq> Collect (Domainp (\<lambda>y x. T x y))

goal (1 subgoal):
 1. \<Union> K = xl
[PROOF STEP]
from assms(4)
[PROOF STATE]
proof (chain)
picking this:
rel_set T xl (\<Union> K')
[PROOF STEP]
have "rel_set ?T' (\<Union>K') xl"
[PROOF STATE]
proof (prove)
using this:
rel_set T xl (\<Union> K')

goal (1 subgoal):
 1. rel_set (\<lambda>y x. T x y) (\<Union> K') xl
[PROOF STEP]
unfolding rel_set_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>xl. Bex (\<Union> K') (T x)) \<and> (\<forall>y\<in>\<Union> K'. \<exists>x\<in>xl. T x y)

goal (1 subgoal):
 1. (\<forall>x\<in>\<Union> K'. \<exists>xa\<in>xl. T xa x) \<and> (\<forall>y\<in>xl. Bex (\<Union> K') (T y))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rel_set (\<lambda>y x. T x y) (\<Union> K') xl

goal (1 subgoal):
 1. \<Union> K = xl
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bi_unique (\<lambda>y x. T x y)
\<Union> K' \<subseteq> Collect (Domainp (\<lambda>y x. T x y))
rel_set (\<lambda>y x. T x y) (\<Union> K') xl
[PROOF STEP]
have "\<Union>({(x, y). rel_set ?T' x y} `` K') = xl"
[PROOF STATE]
proof (prove)
using this:
bi_unique (\<lambda>y x. T x y)
\<Union> K' \<subseteq> Collect (Domainp (\<lambda>y x. T x y))
rel_set (\<lambda>y x. T x y) (\<Union> K') xl

goal (1 subgoal):
 1. \<Union> ({(x, y). rel_set (\<lambda>y x. T x y) x y} `` K') = xl
[PROOF STEP]
by (rule bi_unique_Union_r)
[PROOF STATE]
proof (state)
this:
\<Union> ({(x, y). rel_set (\<lambda>y x. T x y) x y} `` K') = xl

goal (1 subgoal):
 1. \<Union> K = xl
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Union> ({(x, y). rel_set (\<lambda>y x. T x y) x y} `` K') = xl

goal (1 subgoal):
 1. \<Union> K = xl
[PROOF STEP]
using K
[PROOF STATE]
proof (prove)
using this:
\<Union> ({(x, y). rel_set (\<lambda>y x. T x y) x y} `` K') = xl
K \<equiv> {(x, y). rel_set (\<lambda>y x. T x y) x y} `` K'

goal (1 subgoal):
 1. \<Union> K = xl
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Union> K = xl

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Domainp_applyI:
  includes lifting_syntax
  shows "(A ===> B) f g \<Longrightarrow> A x y \<Longrightarrow> Domainp B (f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(A ===> B) f g; A x y\<rbrakk> \<Longrightarrow> Domainp B (f x)
[PROOF STEP]
by (auto simp: rel_fun_def)


[STATEMENT]
lemma Domainp_fun:
  assumes "left_unique A"
  shows
    "Domainp (rel_fun A B) =
      (\<lambda>f. f ` (Collect (Domainp A)) \<subseteq> (Collect (Domainp B)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Domainp (A ===> B) = (\<lambda>f. f ` Collect (Domainp A) \<subseteq> Collect (Domainp B))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Domainp (A ===> B) = (\<lambda>f. f ` Collect (Domainp A) \<subseteq> Collect (Domainp B))
[PROOF STEP]
have
    "pred_fun (Domainp A) (Domainp B) =
      (\<lambda>f. f ` (Collect (Domainp A)) \<subseteq> (Collect (Domainp B)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred_fun (Domainp A) (Domainp B) = (\<lambda>f. f ` Collect (Domainp A) \<subseteq> Collect (Domainp B))
[PROOF STEP]
by (simp add: image_subset_iff)
[PROOF STATE]
proof (state)
this:
pred_fun (Domainp A) (Domainp B) = (\<lambda>f. f ` Collect (Domainp A) \<subseteq> Collect (Domainp B))

goal (1 subgoal):
 1. Domainp (A ===> B) = (\<lambda>f. f ` Collect (Domainp A) \<subseteq> Collect (Domainp B))
[PROOF STEP]
from Domainp_pred_fun_eq[OF \<open>left_unique A\<close>, of B, unfolded this]
[PROOF STATE]
proof (chain)
picking this:
Domainp (A ===> B) = (\<lambda>f. f ` Collect (Domainp A) \<subseteq> Collect (Domainp B))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Domainp (A ===> B) = (\<lambda>f. f ` Collect (Domainp A) \<subseteq> Collect (Domainp B))

goal (1 subgoal):
 1. Domainp (A ===> B) = (\<lambda>f. f ` Collect (Domainp A) \<subseteq> Collect (Domainp B))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Domainp (A ===> B) = (\<lambda>f. f ` Collect (Domainp A) \<subseteq> Collect (Domainp B))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Bex_fun_transfer[transfer_rule]:
  assumes "bi_unique A" "right_total B"
  shows
    "(((A ===> B) ===> (=)) ===> (=))
      (Bex (Collect (\<lambda>f. f ` (Collect (Domainp A)) \<subseteq> (Collect (Domainp B)))))
      Ex"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((A ===> B) ===> (=)) ===> (=)) (Bex {f. f ` Collect (Domainp A) \<subseteq> Collect (Domainp B)}) Ex
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (((A ===> B) ===> (=)) ===> (=)) (Bex {f. f ` Collect (Domainp A) \<subseteq> Collect (Domainp B)}) Ex
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
bi_unique A
[PROOF STEP]
have "left_unique A"
[PROOF STATE]
proof (prove)
using this:
bi_unique A

goal (1 subgoal):
 1. left_unique A
[PROOF STEP]
by (simp add: bi_unique_alt_def)
[PROOF STATE]
proof (state)
this:
left_unique A

goal (1 subgoal):
 1. (((A ===> B) ===> (=)) ===> (=)) (Bex {f. f ` Collect (Domainp A) \<subseteq> Collect (Domainp B)}) Ex
[PROOF STEP]
note right_total_BA[transfer_rule] =
    right_total_fun[
      OF conjunct2[OF bi_unique_alt_def[THEN iffD1, OF assms(1)]] assms(2)
      ]
[PROOF STATE]
proof (state)
this:
right_total (A ===> B)

goal (1 subgoal):
 1. (((A ===> B) ===> (=)) ===> (=)) (Bex {f. f ` Collect (Domainp A) \<subseteq> Collect (Domainp B)}) Ex
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((A ===> B) ===> (=)) ===> (=)) (Bex {f. f ` Collect (Domainp A) \<subseteq> Collect (Domainp B)}) Ex
[PROOF STEP]
unfolding Domainp_fun[OF \<open>left_unique A\<close>, symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((A ===> B) ===> (=)) ===> (=)) (Bex (Collect (Domainp (A ===> B)))) Ex
[PROOF STEP]
by transfer_prover
[PROOF STATE]
proof (state)
this:
(((A ===> B) ===> (=)) ===> (=)) (Bex {f. f ` Collect (Domainp A) \<subseteq> Collect (Domainp B)}) Ex

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ci_stk_offerI:
  "(\<And>ins P h stk stk' loc C M pc frs. ci ins P h stk loc C M pc frs \<Longrightarrow> ci ins P h (stk @ stk') loc C M pc frs) \<Longrightarrow> ci_stk_offer ci"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ins P h stk stk' loc C M pc frs. ci ins P h stk loc C M pc frs \<Longrightarrow> ci ins P h (stk @ stk') loc C M pc frs) \<Longrightarrow> ci_stk_offer ci
[PROOF STEP]
unfolding ci_stk_offer_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ins P h stk stk' loc C M pc frs. ci ins P h stk loc C M pc frs \<Longrightarrow> ci ins P h (stk @ stk') loc C M pc frs) \<Longrightarrow> \<forall>ins P h stk stk' loc C M pc frs. ci ins P h stk loc C M pc frs \<longrightarrow> ci ins P h (stk @ stk') loc C M pc frs
[PROOF STEP]
by blast


[STATEMENT]
lemma ci_stk_offerD:
  "\<lbrakk> ci_stk_offer ci; ci ins P h stk loc C M pc frs \<rbrakk> \<Longrightarrow> ci ins P h (stk @ stk') loc C M pc frs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ci_stk_offer ci; ci ins P h stk loc C M pc frs\<rbrakk> \<Longrightarrow> ci ins P h (stk @ stk') loc C M pc frs
[PROOF STEP]
unfolding ci_stk_offer_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ins P h stk stk' loc C M pc frs. ci ins P h stk loc C M pc frs \<longrightarrow> ci ins P h (stk @ stk') loc C M pc frs; ci ins P h stk loc C M pc frs\<rbrakk> \<Longrightarrow> ci ins P h (stk @ stk') loc C M pc frs
[PROOF STEP]
by blast


[STATEMENT]
lemma check_instr'_stk_offer:
  "ci_stk_offer check_instr'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ci_stk_offer check_instr'
[PROOF STEP]
proof(rule ci_stk_offerI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ins P h stk stk' loc C M pc frs. check_instr' ins P h stk loc C M pc frs \<Longrightarrow> check_instr' ins P h (stk @ stk') loc C M pc frs
[PROOF STEP]
fix ins P h stk stk' loc C M pc frs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ins P h stk stk' loc C M pc frs. check_instr' ins P h stk loc C M pc frs \<Longrightarrow> check_instr' ins P h (stk @ stk') loc C M pc frs
[PROOF STEP]
assume "check_instr' ins P h stk loc C M pc frs"
[PROOF STATE]
proof (state)
this:
check_instr' ins P h stk loc C M pc frs

goal (1 subgoal):
 1. \<And>ins P h stk stk' loc C M pc frs. check_instr' ins P h stk loc C M pc frs \<Longrightarrow> check_instr' ins P h (stk @ stk') loc C M pc frs
[PROOF STEP]
thus "check_instr' ins P h (stk @ stk') loc C M pc frs"
[PROOF STATE]
proof (prove)
using this:
check_instr' ins P h stk loc C M pc frs

goal (1 subgoal):
 1. check_instr' ins P h (stk @ stk') loc C M pc frs
[PROOF STEP]
by(cases ins) auto
[PROOF STATE]
proof (state)
this:
check_instr' ins P h (stk @ stk') loc C M pc frs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma check_instr_imp_check_instr':
  "check_instr ins P h stk loc C M pc frs \<Longrightarrow> check_instr' ins P h stk loc C M pc frs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_instr ins P h stk loc C M pc frs \<Longrightarrow> check_instr' ins P h stk loc C M pc frs
[PROOF STEP]
by(cases ins) auto


[STATEMENT]
lemma check_instr_stk_offer:
  "ci_stk_offer check_instr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ci_stk_offer check_instr
[PROOF STEP]
proof(rule ci_stk_offerI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ins P h stk stk' loc C M pc frs. check_instr ins P h stk loc C M pc frs \<Longrightarrow> check_instr ins P h (stk @ stk') loc C M pc frs
[PROOF STEP]
fix ins P h stk stk' loc C M pc frs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ins P h stk stk' loc C M pc frs. check_instr ins P h stk loc C M pc frs \<Longrightarrow> check_instr ins P h (stk @ stk') loc C M pc frs
[PROOF STEP]
assume "check_instr ins P h stk loc C M pc frs"
[PROOF STATE]
proof (state)
this:
check_instr ins P h stk loc C M pc frs

goal (1 subgoal):
 1. \<And>ins P h stk stk' loc C M pc frs. check_instr ins P h stk loc C M pc frs \<Longrightarrow> check_instr ins P h (stk @ stk') loc C M pc frs
[PROOF STEP]
thus "check_instr ins P h (stk @ stk') loc C M pc frs"
[PROOF STATE]
proof (prove)
using this:
check_instr ins P h stk loc C M pc frs

goal (1 subgoal):
 1. check_instr ins P h (stk @ stk') loc C M pc frs
[PROOF STEP]
by(cases ins)(auto simp add: nth_append hd_append neq_Nil_conv tl_append split: list.split)
[PROOF STATE]
proof (state)
this:
check_instr ins P h (stk @ stk') loc C M pc frs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma jump_ok_append [simp]:
  "jump_ok (xs @ xs') n n' \<longleftrightarrow> jump_ok xs n (n' + length xs') \<and> jump_ok xs' (n + length xs) n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. jump_ok (xs @ xs') n n' = (jump_ok xs n (n' + length xs') \<and> jump_ok xs' (n + length xs) n')
[PROOF STEP]
apply(induct xs arbitrary: n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. jump_ok ([] @ xs') n n' = (jump_ok [] n (n' + length xs') \<and> jump_ok xs' (n + length []) n')
 2. \<And>a xs n. (\<And>n. jump_ok (xs @ xs') n n' = (jump_ok xs n (n' + length xs') \<and> jump_ok xs' (n + length xs) n')) \<Longrightarrow> jump_ok ((a # xs) @ xs') n n' = (jump_ok (a # xs) n (n' + length xs') \<and> jump_ok xs' (n + length (a # xs)) n')
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs n. (\<And>n. jump_ok (xs @ xs') n n' = (jump_ok xs n (n' + length xs') \<and> jump_ok xs' (n + length xs) n')) \<Longrightarrow> jump_ok ((a # xs) @ xs') n n' = (jump_ok (a # xs) n (n' + length xs') \<and> jump_ok xs' (n + length (a # xs)) n')
[PROOF STEP]
apply(auto split: instr.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma jump_ok_GotoD:
  "\<lbrakk> jump_ok ins n n'; ins ! pc = Goto m; pc < length ins \<rbrakk> \<Longrightarrow> - int (pc + n) \<le> m \<and> m < int (length ins - pc + n')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>jump_ok ins n n'; ins ! pc = Goto m; pc < length ins\<rbrakk> \<Longrightarrow> - int (pc + n) \<le> m \<and> m < int (length ins - pc + n')
[PROOF STEP]
apply(induct ins arbitrary: n n' pc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n n' pc. \<lbrakk>jump_ok [] n n'; [] ! pc = Goto m; pc < length []\<rbrakk> \<Longrightarrow> - int (pc + n) \<le> m \<and> m < int (length [] - pc + n')
 2. \<And>a ins n n' pc. \<lbrakk>\<And>n n' pc. \<lbrakk>jump_ok ins n n'; ins ! pc = Goto m; pc < length ins\<rbrakk> \<Longrightarrow> - int (pc + n) \<le> m \<and> m < int (length ins - pc + n'); jump_ok (a # ins) n n'; (a # ins) ! pc = Goto m; pc < length (a # ins)\<rbrakk> \<Longrightarrow> - int (pc + n) \<le> m \<and> m < int (length (a # ins) - pc + n')
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a ins n n' pc. \<lbrakk>\<And>n n' pc. \<lbrakk>jump_ok ins n n'; ins ! pc = Goto m; pc < length ins\<rbrakk> \<Longrightarrow> - int (pc + n) \<le> m \<and> m < int (length ins - pc + n'); jump_ok (a # ins) n n'; (a # ins) ! pc = Goto m; pc < length (a # ins)\<rbrakk> \<Longrightarrow> - int (pc + n) \<le> m \<and> m < int (length (a # ins) - pc + n')
[PROOF STEP]
apply(clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a ins n n' pc. \<lbrakk>\<And>n n' pc. \<lbrakk>jump_ok ins n n'; ins ! pc = Goto m; pc < length ins\<rbrakk> \<Longrightarrow> - int pc - int n \<le> m \<and> m < int (length ins + n' - pc); (a # ins) ! pc = Goto m; pc < Suc (length ins); jump_ok ins (Suc n) n'; case a of Goto m \<Rightarrow> - int n \<le> m \<and> m \<le> int (n' + length ins) | IfFalse m \<Rightarrow> - int n \<le> m \<and> m \<le> int (n' + length ins) | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> - int pc - int n \<le> m \<and> m < int (Suc (length ins + n') - pc)
[PROOF STEP]
apply(case_tac pc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a ins n n' pc. \<lbrakk>\<And>n n' pc. \<lbrakk>jump_ok ins n n'; ins ! pc = Goto m; pc < length ins\<rbrakk> \<Longrightarrow> - int pc - int n \<le> m \<and> m < int (length ins + n' - pc); (a # ins) ! pc = Goto m; pc < Suc (length ins); jump_ok ins (Suc n) n'; case a of Goto m \<Rightarrow> - int n \<le> m \<and> m \<le> int (n' + length ins) | IfFalse m \<Rightarrow> - int n \<le> m \<and> m \<le> int (n' + length ins) | _ \<Rightarrow> True; pc = 0\<rbrakk> \<Longrightarrow> - int pc - int n \<le> m \<and> m < int (Suc (length ins + n') - pc)
 2. \<And>a ins n n' pc nat. \<lbrakk>\<And>n n' pc. \<lbrakk>jump_ok ins n n'; ins ! pc = Goto m; pc < length ins\<rbrakk> \<Longrightarrow> - int pc - int n \<le> m \<and> m < int (length ins + n' - pc); (a # ins) ! pc = Goto m; pc < Suc (length ins); jump_ok ins (Suc n) n'; case a of Goto m \<Rightarrow> - int n \<le> m \<and> m \<le> int (n' + length ins) | IfFalse m \<Rightarrow> - int n \<le> m \<and> m \<le> int (n' + length ins) | _ \<Rightarrow> True; pc = Suc nat\<rbrakk> \<Longrightarrow> - int pc - int n \<le> m \<and> m < int (Suc (length ins + n') - pc)
[PROOF STEP]
apply(fastforce)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma jump_ok_IfFalseD:
  "\<lbrakk> jump_ok ins n n'; ins ! pc = IfFalse m; pc < length ins \<rbrakk> \<Longrightarrow> - int (pc + n) \<le> m \<and> m < int (length ins - pc + n')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>jump_ok ins n n'; ins ! pc = IfFalse m; pc < length ins\<rbrakk> \<Longrightarrow> - int (pc + n) \<le> m \<and> m < int (length ins - pc + n')
[PROOF STEP]
apply(induct ins arbitrary: n n' pc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n n' pc. \<lbrakk>jump_ok [] n n'; [] ! pc = IfFalse m; pc < length []\<rbrakk> \<Longrightarrow> - int (pc + n) \<le> m \<and> m < int (length [] - pc + n')
 2. \<And>a ins n n' pc. \<lbrakk>\<And>n n' pc. \<lbrakk>jump_ok ins n n'; ins ! pc = IfFalse m; pc < length ins\<rbrakk> \<Longrightarrow> - int (pc + n) \<le> m \<and> m < int (length ins - pc + n'); jump_ok (a # ins) n n'; (a # ins) ! pc = IfFalse m; pc < length (a # ins)\<rbrakk> \<Longrightarrow> - int (pc + n) \<le> m \<and> m < int (length (a # ins) - pc + n')
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a ins n n' pc. \<lbrakk>\<And>n n' pc. \<lbrakk>jump_ok ins n n'; ins ! pc = IfFalse m; pc < length ins\<rbrakk> \<Longrightarrow> - int (pc + n) \<le> m \<and> m < int (length ins - pc + n'); jump_ok (a # ins) n n'; (a # ins) ! pc = IfFalse m; pc < length (a # ins)\<rbrakk> \<Longrightarrow> - int (pc + n) \<le> m \<and> m < int (length (a # ins) - pc + n')
[PROOF STEP]
apply(clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a ins n n' pc. \<lbrakk>\<And>n n' pc. \<lbrakk>jump_ok ins n n'; ins ! pc = IfFalse m; pc < length ins\<rbrakk> \<Longrightarrow> - int pc - int n \<le> m \<and> m < int (length ins + n' - pc); (a # ins) ! pc = IfFalse m; pc < Suc (length ins); jump_ok ins (Suc n) n'; case a of Goto m \<Rightarrow> - int n \<le> m \<and> m \<le> int (n' + length ins) | IfFalse m \<Rightarrow> - int n \<le> m \<and> m \<le> int (n' + length ins) | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> - int pc - int n \<le> m \<and> m < int (Suc (length ins + n') - pc)
[PROOF STEP]
apply(case_tac pc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a ins n n' pc. \<lbrakk>\<And>n n' pc. \<lbrakk>jump_ok ins n n'; ins ! pc = IfFalse m; pc < length ins\<rbrakk> \<Longrightarrow> - int pc - int n \<le> m \<and> m < int (length ins + n' - pc); (a # ins) ! pc = IfFalse m; pc < Suc (length ins); jump_ok ins (Suc n) n'; case a of Goto m \<Rightarrow> - int n \<le> m \<and> m \<le> int (n' + length ins) | IfFalse m \<Rightarrow> - int n \<le> m \<and> m \<le> int (n' + length ins) | _ \<Rightarrow> True; pc = 0\<rbrakk> \<Longrightarrow> - int pc - int n \<le> m \<and> m < int (Suc (length ins + n') - pc)
 2. \<And>a ins n n' pc nat. \<lbrakk>\<And>n n' pc. \<lbrakk>jump_ok ins n n'; ins ! pc = IfFalse m; pc < length ins\<rbrakk> \<Longrightarrow> - int pc - int n \<le> m \<and> m < int (length ins + n' - pc); (a # ins) ! pc = IfFalse m; pc < Suc (length ins); jump_ok ins (Suc n) n'; case a of Goto m \<Rightarrow> - int n \<le> m \<and> m \<le> int (n' + length ins) | IfFalse m \<Rightarrow> - int n \<le> m \<and> m \<le> int (n' + length ins) | _ \<Rightarrow> True; pc = Suc nat\<rbrakk> \<Longrightarrow> - int pc - int n \<le> m \<and> m < int (Suc (length ins + n') - pc)
[PROOF STEP]
apply(fastforce)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fixes e :: "'addr expr1" and es :: "'addr expr1 list"
  shows compE2_jump_ok [intro!]: "jump_ok (compE2 e) n (Suc n')"
  and compEs2_jump_ok [intro!]: "jump_ok (compEs2 es) n (Suc n')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. jump_ok (compE2 e) n (Suc n') &&& jump_ok (compEs2 es) n (Suc n')
[PROOF STEP]
apply(induct e and es arbitrary: n n' and n n' rule: compE2.induct compEs2.induct)
[PROOF STATE]
proof (prove)
goal (25 subgoals):
 1. \<And>x n n'. jump_ok (compE2 (new x)) n (Suc n')
 2. \<And>x1 x2 n n'. (\<And>n n'. jump_ok (compE2 x2) n (Suc n')) \<Longrightarrow> jump_ok (compE2 (newA x1\<lfloor>x2\<rceil>)) n (Suc n')
 3. \<And>x1 x2 n n'. (\<And>n n'. jump_ok (compE2 x2) n (Suc n')) \<Longrightarrow> jump_ok (compE2 (Cast x1 x2)) n (Suc n')
 4. \<And>x1 x2 n n'. (\<And>n n'. jump_ok (compE2 x1) n (Suc n')) \<Longrightarrow> jump_ok (compE2 (x1 instanceof x2)) n (Suc n')
 5. \<And>x n n'. jump_ok (compE2 (Val x)) n (Suc n')
 6. \<And>x1 x2 x3 n n'. \<lbrakk>\<And>n n'. jump_ok (compE2 x1) n (Suc n'); \<And>n n'. jump_ok (compE2 x3) n (Suc n')\<rbrakk> \<Longrightarrow> jump_ok (compE2 (x1 \<guillemotleft>x2\<guillemotright> x3)) n (Suc n')
 7. \<And>x n n'. jump_ok (compE2 (Var x)) n (Suc n')
 8. \<And>x1 x2 n n'. (\<And>n n'. jump_ok (compE2 x2) n (Suc n')) \<Longrightarrow> jump_ok (compE2 (x1:=x2)) n (Suc n')
 9. \<And>x1 x2 n n'. \<lbrakk>\<And>n n'. jump_ok (compE2 x1) n (Suc n'); \<And>n n'. jump_ok (compE2 x2) n (Suc n')\<rbrakk> \<Longrightarrow> jump_ok (compE2 (x1\<lfloor>x2\<rceil>)) n (Suc n')
 10. \<And>x1 x2 x3 n n'. \<lbrakk>\<And>n n'. jump_ok (compE2 x1) n (Suc n'); \<And>n n'. jump_ok (compE2 x2) n (Suc n'); \<And>n n'. jump_ok (compE2 x3) n (Suc n')\<rbrakk> \<Longrightarrow> jump_ok (compE2 (x1\<lfloor>x2\<rceil> := x3)) n (Suc n')
A total of 25 subgoals...
[PROOF STEP]
apply(auto split: bop.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done