[STATEMENT]
lemma insert_body_split:
  shows "\<exists>p s. xs = p @ s \<and> insert_body xs e = p @ e # s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p s. xs = p @ s \<and> insert_body xs e = p @ e # s
[PROOF STEP]
proof(induction xs, force)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<exists>p s. xs = p @ s \<and> insert_body xs e = p @ e # s \<Longrightarrow> \<exists>p s. a # xs = p @ s \<and> insert_body (a # xs) e = p @ e # s
[PROOF STEP]
case (Cons a xs)
[PROOF STATE]
proof (state)
this:
\<exists>p s. xs = p @ s \<and> insert_body xs e = p @ e # s

goal (1 subgoal):
 1. \<And>a xs. \<exists>p s. xs = p @ s \<and> insert_body xs e = p @ e # s \<Longrightarrow> \<exists>p s. a # xs = p @ s \<and> insert_body (a # xs) e = p @ e # s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p s. xs = p @ s \<and> insert_body xs e = p @ e # s
[PROOF STEP]
obtain p s where IH: "xs = p @ s \<and> insert_body xs e = p @ e # s"
[PROOF STATE]
proof (prove)
using this:
\<exists>p s. xs = p @ s \<and> insert_body xs e = p @ e # s

goal (1 subgoal):
 1. (\<And>p s. xs = p @ s \<and> insert_body xs e = p @ e # s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xs = p @ s \<and> insert_body xs e = p @ e # s

goal (1 subgoal):
 1. \<And>a xs. \<exists>p s. xs = p @ s \<and> insert_body xs e = p @ e # s \<Longrightarrow> \<exists>p s. a # xs = p @ s \<and> insert_body (a # xs) e = p @ e # s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = p @ s \<and> insert_body xs e = p @ e # s
[PROOF STEP]
show "\<exists>p s. a # xs = p @ s \<and> insert_body (a # xs) e = p @ e # s"
[PROOF STATE]
proof (prove)
using this:
xs = p @ s \<and> insert_body xs e = p @ e # s

goal (1 subgoal):
 1. \<exists>p s. a # xs = p @ s \<and> insert_body (a # xs) e = p @ e # s
[PROOF STEP]
proof(cases "a < e")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>xs = p @ s \<and> insert_body xs e = p @ e # s; a < e\<rbrakk> \<Longrightarrow> \<exists>p s. a # xs = p @ s \<and> insert_body (a # xs) e = p @ e # s
 2. \<lbrakk>xs = p @ s \<and> insert_body xs e = p @ e # s; \<not> a < e\<rbrakk> \<Longrightarrow> \<exists>p s. a # xs = p @ s \<and> insert_body (a # xs) e = p @ e # s
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a < e

goal (2 subgoals):
 1. \<lbrakk>xs = p @ s \<and> insert_body xs e = p @ e # s; a < e\<rbrakk> \<Longrightarrow> \<exists>p s. a # xs = p @ s \<and> insert_body (a # xs) e = p @ e # s
 2. \<lbrakk>xs = p @ s \<and> insert_body xs e = p @ e # s; \<not> a < e\<rbrakk> \<Longrightarrow> \<exists>p s. a # xs = p @ s \<and> insert_body (a # xs) e = p @ e # s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a < e
[PROOF STEP]
have "a # xs = [] @ (a # p @ s) \<and> insert_body (a # xs) e = [] @ e # (a # p @ s)"
[PROOF STATE]
proof (prove)
using this:
a < e

goal (1 subgoal):
 1. a # xs = [] @ a # p @ s \<and> insert_body (a # xs) e = [] @ e # a # p @ s
[PROOF STEP]
by (simp add: IH)
[PROOF STATE]
proof (state)
this:
a # xs = [] @ a # p @ s \<and> insert_body (a # xs) e = [] @ e # a # p @ s

goal (2 subgoals):
 1. \<lbrakk>xs = p @ s \<and> insert_body xs e = p @ e # s; a < e\<rbrakk> \<Longrightarrow> \<exists>p s. a # xs = p @ s \<and> insert_body (a # xs) e = p @ e # s
 2. \<lbrakk>xs = p @ s \<and> insert_body xs e = p @ e # s; \<not> a < e\<rbrakk> \<Longrightarrow> \<exists>p s. a # xs = p @ s \<and> insert_body (a # xs) e = p @ e # s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a # xs = [] @ a # p @ s \<and> insert_body (a # xs) e = [] @ e # a # p @ s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a # xs = [] @ a # p @ s \<and> insert_body (a # xs) e = [] @ e # a # p @ s

goal (1 subgoal):
 1. \<exists>p s. a # xs = p @ s \<and> insert_body (a # xs) e = p @ e # s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>p s. a # xs = p @ s \<and> insert_body (a # xs) e = p @ e # s

goal (1 subgoal):
 1. \<lbrakk>xs = p @ s \<and> insert_body xs e = p @ e # s; \<not> a < e\<rbrakk> \<Longrightarrow> \<exists>p s. a # xs = p @ s \<and> insert_body (a # xs) e = p @ e # s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>xs = p @ s \<and> insert_body xs e = p @ e # s; \<not> a < e\<rbrakk> \<Longrightarrow> \<exists>p s. a # xs = p @ s \<and> insert_body (a # xs) e = p @ e # s
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> a < e

goal (1 subgoal):
 1. \<lbrakk>xs = p @ s \<and> insert_body xs e = p @ e # s; \<not> a < e\<rbrakk> \<Longrightarrow> \<exists>p s. a # xs = p @ s \<and> insert_body (a # xs) e = p @ e # s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> a < e
[PROOF STEP]
have "a # xs = (a # p) @ s \<and> insert_body (a # xs) e = (a # p) @ e # s"
[PROOF STATE]
proof (prove)
using this:
\<not> a < e

goal (1 subgoal):
 1. a # xs = (a # p) @ s \<and> insert_body (a # xs) e = (a # p) @ e # s
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
\<not> a < e
xs = p @ s \<and> insert_body xs e = p @ e # s

goal (1 subgoal):
 1. a # xs = (a # p) @ s \<and> insert_body (a # xs) e = (a # p) @ e # s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a # xs = (a # p) @ s \<and> insert_body (a # xs) e = (a # p) @ e # s

goal (1 subgoal):
 1. \<lbrakk>xs = p @ s \<and> insert_body xs e = p @ e # s; \<not> a < e\<rbrakk> \<Longrightarrow> \<exists>p s. a # xs = p @ s \<and> insert_body (a # xs) e = p @ e # s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a # xs = (a # p) @ s \<and> insert_body (a # xs) e = (a # p) @ e # s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a # xs = (a # p) @ s \<and> insert_body (a # xs) e = (a # p) @ e # s

goal (1 subgoal):
 1. \<exists>p s. a # xs = p @ s \<and> insert_body (a # xs) e = p @ e # s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>p s. a # xs = p @ s \<and> insert_body (a # xs) e = p @ e # s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>p s. a # xs = p @ s \<and> insert_body (a # xs) e = p @ e # s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insert_between_elements:
  assumes "xs = pre @ ref # suf"
    and "distinct xs"
    and "\<And>i. i \<in> set xs \<Longrightarrow> i < e"
  shows "insert_rga xs (e, Some ref) = pre @ ref # e # suf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_rga xs (e, Some ref) = pre @ ref # e # suf
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs = pre @ ref # suf
distinct xs
?i \<in> set xs \<Longrightarrow> ?i < e

goal (1 subgoal):
 1. insert_rga xs (e, Some ref) = pre @ ref # e # suf
[PROOF STEP]
proof(induction xs arbitrary: pre, force)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs pre. \<lbrakk>\<And>pre. \<lbrakk>xs = pre @ ref # suf; distinct xs; \<And>i. i \<in> set xs \<Longrightarrow> i < e\<rbrakk> \<Longrightarrow> insert_rga xs (e, Some ref) = pre @ ref # e # suf; a # xs = pre @ ref # suf; distinct (a # xs); \<And>i. i \<in> set (a # xs) \<Longrightarrow> i < e\<rbrakk> \<Longrightarrow> insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf
[PROOF STEP]
case (Cons a xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>xs = ?pre @ ref # suf; distinct xs; \<And>i. i \<in> set xs \<Longrightarrow> i < e\<rbrakk> \<Longrightarrow> insert_rga xs (e, Some ref) = ?pre @ ref # e # suf
a # xs = pre @ ref # suf
distinct (a # xs)
?i \<in> set (a # xs) \<Longrightarrow> ?i < e

goal (1 subgoal):
 1. \<And>a xs pre. \<lbrakk>\<And>pre. \<lbrakk>xs = pre @ ref # suf; distinct xs; \<And>i. i \<in> set xs \<Longrightarrow> i < e\<rbrakk> \<Longrightarrow> insert_rga xs (e, Some ref) = pre @ ref # e # suf; a # xs = pre @ ref # suf; distinct (a # xs); \<And>i. i \<in> set (a # xs) \<Longrightarrow> i < e\<rbrakk> \<Longrightarrow> insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>xs = ?pre @ ref # suf; distinct xs; \<And>i. i \<in> set xs \<Longrightarrow> i < e\<rbrakk> \<Longrightarrow> insert_rga xs (e, Some ref) = ?pre @ ref # e # suf
a # xs = pre @ ref # suf
distinct (a # xs)
?i \<in> set (a # xs) \<Longrightarrow> ?i < e
[PROOF STEP]
show "insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>xs = ?pre @ ref # suf; distinct xs; \<And>i. i \<in> set xs \<Longrightarrow> i < e\<rbrakk> \<Longrightarrow> insert_rga xs (e, Some ref) = ?pre @ ref # e # suf
a # xs = pre @ ref # suf
distinct (a # xs)
?i \<in> set (a # xs) \<Longrightarrow> ?i < e

goal (1 subgoal):
 1. insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf
[PROOF STEP]
proof(cases pre)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>pre. \<lbrakk>xs = pre @ ref # suf; distinct xs; \<And>i. i \<in> set xs \<Longrightarrow> i < e\<rbrakk> \<Longrightarrow> insert_rga xs (e, Some ref) = pre @ ref # e # suf; a # xs = pre @ ref # suf; distinct (a # xs); \<And>i. i \<in> set (a # xs) \<Longrightarrow> i < e; pre = []\<rbrakk> \<Longrightarrow> insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf
 2. \<And>aa list. \<lbrakk>\<And>pre. \<lbrakk>xs = pre @ ref # suf; distinct xs; \<And>i. i \<in> set xs \<Longrightarrow> i < e\<rbrakk> \<Longrightarrow> insert_rga xs (e, Some ref) = pre @ ref # e # suf; a # xs = pre @ ref # suf; distinct (a # xs); \<And>i. i \<in> set (a # xs) \<Longrightarrow> i < e; pre = aa # list\<rbrakk> \<Longrightarrow> insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf
[PROOF STEP]
case pre_nil: Nil
[PROOF STATE]
proof (state)
this:
pre = []

goal (2 subgoals):
 1. \<lbrakk>\<And>pre. \<lbrakk>xs = pre @ ref # suf; distinct xs; \<And>i. i \<in> set xs \<Longrightarrow> i < e\<rbrakk> \<Longrightarrow> insert_rga xs (e, Some ref) = pre @ ref # e # suf; a # xs = pre @ ref # suf; distinct (a # xs); \<And>i. i \<in> set (a # xs) \<Longrightarrow> i < e; pre = []\<rbrakk> \<Longrightarrow> insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf
 2. \<And>aa list. \<lbrakk>\<And>pre. \<lbrakk>xs = pre @ ref # suf; distinct xs; \<And>i. i \<in> set xs \<Longrightarrow> i < e\<rbrakk> \<Longrightarrow> insert_rga xs (e, Some ref) = pre @ ref # e # suf; a # xs = pre @ ref # suf; distinct (a # xs); \<And>i. i \<in> set (a # xs) \<Longrightarrow> i < e; pre = aa # list\<rbrakk> \<Longrightarrow> insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pre = []
[PROOF STEP]
have "a = ref"
[PROOF STATE]
proof (prove)
using this:
pre = []

goal (1 subgoal):
 1. a = ref
[PROOF STEP]
using Cons.prems(1)
[PROOF STATE]
proof (prove)
using this:
pre = []
a # xs = pre @ ref # suf

goal (1 subgoal):
 1. a = ref
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = ref

goal (2 subgoals):
 1. \<lbrakk>\<And>pre. \<lbrakk>xs = pre @ ref # suf; distinct xs; \<And>i. i \<in> set xs \<Longrightarrow> i < e\<rbrakk> \<Longrightarrow> insert_rga xs (e, Some ref) = pre @ ref # e # suf; a # xs = pre @ ref # suf; distinct (a # xs); \<And>i. i \<in> set (a # xs) \<Longrightarrow> i < e; pre = []\<rbrakk> \<Longrightarrow> insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf
 2. \<And>aa list. \<lbrakk>\<And>pre. \<lbrakk>xs = pre @ ref # suf; distinct xs; \<And>i. i \<in> set xs \<Longrightarrow> i < e\<rbrakk> \<Longrightarrow> insert_rga xs (e, Some ref) = pre @ ref # e # suf; a # xs = pre @ ref # suf; distinct (a # xs); \<And>i. i \<in> set (a # xs) \<Longrightarrow> i < e; pre = aa # list\<rbrakk> \<Longrightarrow> insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = ref
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = ref

goal (1 subgoal):
 1. insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf
[PROOF STEP]
using Cons.prems pre_nil
[PROOF STATE]
proof (prove)
using this:
a = ref
a # xs = pre @ ref # suf
distinct (a # xs)
?i \<in> set (a # xs) \<Longrightarrow> ?i < e
pre = []

goal (1 subgoal):
 1. insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf
[PROOF STEP]
by (cases suf, auto)
[PROOF STATE]
proof (state)
this:
insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf

goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>\<And>pre. \<lbrakk>xs = pre @ ref # suf; distinct xs; \<And>i. i \<in> set xs \<Longrightarrow> i < e\<rbrakk> \<Longrightarrow> insert_rga xs (e, Some ref) = pre @ ref # e # suf; a # xs = pre @ ref # suf; distinct (a # xs); \<And>i. i \<in> set (a # xs) \<Longrightarrow> i < e; pre = aa # list\<rbrakk> \<Longrightarrow> insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>\<And>pre. \<lbrakk>xs = pre @ ref # suf; distinct xs; \<And>i. i \<in> set xs \<Longrightarrow> i < e\<rbrakk> \<Longrightarrow> insert_rga xs (e, Some ref) = pre @ ref # e # suf; a # xs = pre @ ref # suf; distinct (a # xs); \<And>i. i \<in> set (a # xs) \<Longrightarrow> i < e; pre = aa # list\<rbrakk> \<Longrightarrow> insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf
[PROOF STEP]
case (Cons b pre')
[PROOF STATE]
proof (state)
this:
pre = b # pre'

goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>\<And>pre. \<lbrakk>xs = pre @ ref # suf; distinct xs; \<And>i. i \<in> set xs \<Longrightarrow> i < e\<rbrakk> \<Longrightarrow> insert_rga xs (e, Some ref) = pre @ ref # e # suf; a # xs = pre @ ref # suf; distinct (a # xs); \<And>i. i \<in> set (a # xs) \<Longrightarrow> i < e; pre = aa # list\<rbrakk> \<Longrightarrow> insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pre = b # pre'
[PROOF STEP]
have "insert_rga xs (e, Some ref) = pre' @ ref # e # suf"
[PROOF STATE]
proof (prove)
using this:
pre = b # pre'

goal (1 subgoal):
 1. insert_rga xs (e, Some ref) = pre' @ ref # e # suf
[PROOF STEP]
using Cons.IH Cons.prems
[PROOF STATE]
proof (prove)
using this:
pre = b # pre'
\<lbrakk>xs = ?pre @ ref # suf; distinct xs; \<And>i. i \<in> set xs \<Longrightarrow> i < e\<rbrakk> \<Longrightarrow> insert_rga xs (e, Some ref) = ?pre @ ref # e # suf
a # xs = pre @ ref # suf
distinct (a # xs)
?i \<in> set (a # xs) \<Longrightarrow> ?i < e

goal (1 subgoal):
 1. insert_rga xs (e, Some ref) = pre' @ ref # e # suf
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert_rga xs (e, Some ref) = pre' @ ref # e # suf

goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>\<And>pre. \<lbrakk>xs = pre @ ref # suf; distinct xs; \<And>i. i \<in> set xs \<Longrightarrow> i < e\<rbrakk> \<Longrightarrow> insert_rga xs (e, Some ref) = pre @ ref # e # suf; a # xs = pre @ ref # suf; distinct (a # xs); \<And>i. i \<in> set (a # xs) \<Longrightarrow> i < e; pre = aa # list\<rbrakk> \<Longrightarrow> insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert_rga xs (e, Some ref) = pre' @ ref # e # suf
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
insert_rga xs (e, Some ref) = pre' @ ref # e # suf

goal (1 subgoal):
 1. insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf
[PROOF STEP]
using Cons.prems(1) Cons.prems(2) local.Cons
[PROOF STATE]
proof (prove)
using this:
insert_rga xs (e, Some ref) = pre' @ ref # e # suf
a # xs = pre @ ref # suf
distinct (a # xs)
pre = b # pre'

goal (1 subgoal):
 1. insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insert_rga_after_ref:
  assumes "\<forall>x\<in>set as. a \<noteq> x"
    and "insert_body (cs @ ds) e = cs @ e # ds"
  shows "insert_rga (as @ a # cs @ ds) (e, Some a) = as @ a # cs @ e # ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_rga (as @ a # cs @ ds) (e, Some a) = as @ a # cs @ e # ds
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set as. a \<noteq> x
insert_body (cs @ ds) e = cs @ e # ds

goal (1 subgoal):
 1. insert_rga (as @ a # cs @ ds) (e, Some a) = as @ a # cs @ e # ds
[PROOF STEP]
by (induction as; auto)


[STATEMENT]
lemma insert_rga_preserves_order:
  assumes "i = None \<or> (\<exists>i'. i = Some i' \<and> i' \<in> set xs)"
    and "distinct xs"
  shows "\<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf
[PROOF STEP]
proof(cases i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = None \<Longrightarrow> \<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf
 2. \<And>a. i = Some a \<Longrightarrow> \<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
i = None

goal (2 subgoals):
 1. i = None \<Longrightarrow> \<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf
 2. \<And>a. i = Some a \<Longrightarrow> \<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = None
[PROOF STEP]
show "\<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf"
[PROOF STATE]
proof (prove)
using this:
i = None

goal (1 subgoal):
 1. \<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf
[PROOF STEP]
using insert_body_split
[PROOF STATE]
proof (prove)
using this:
i = None
\<exists>p s. ?xs = p @ s \<and> insert_body ?xs ?e = p @ ?e # s

goal (1 subgoal):
 1. \<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf

goal (1 subgoal):
 1. \<And>a. i = Some a \<Longrightarrow> \<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. i = Some a \<Longrightarrow> \<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf
[PROOF STEP]
case (Some r)
[PROOF STATE]
proof (state)
this:
i = Some r

goal (1 subgoal):
 1. \<And>a. i = Some a \<Longrightarrow> \<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i = Some r

goal (1 subgoal):
 1. \<And>a. i = Some a \<Longrightarrow> \<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
i = Some r
[PROOF STEP]
obtain as bs where "xs = as @ r # bs \<and> (\<forall>x \<in> set as. x \<noteq> r)"
[PROOF STATE]
proof (prove)
using this:
i = Some r

goal (1 subgoal):
 1. (\<And>as bs. xs = as @ r # bs \<and> (\<forall>x\<in>set as. x \<noteq> r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1) split_list_first
[PROOF STATE]
proof (prove)
using this:
i = Some r
i = None \<or> (\<exists>i'. i = Some i' \<and> i' \<in> set xs)
?x \<in> set ?xs \<Longrightarrow> \<exists>ys zs. ?xs = ys @ ?x # zs \<and> ?x \<notin> set ys

goal (1 subgoal):
 1. (\<And>as bs. xs = as @ r # bs \<and> (\<forall>x\<in>set as. x \<noteq> r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
xs = as @ r # bs \<and> (\<forall>x\<in>set as. x \<noteq> r)

goal (1 subgoal):
 1. \<And>a. i = Some a \<Longrightarrow> \<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xs = as @ r # bs \<and> (\<forall>x\<in>set as. x \<noteq> r)

goal (1 subgoal):
 1. \<And>a. i = Some a \<Longrightarrow> \<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf
[PROOF STEP]
have "\<exists>cs ds. bs = cs @ ds \<and> insert_body bs e = cs @ e # ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>cs ds. bs = cs @ ds \<and> insert_body bs e = cs @ e # ds
[PROOF STEP]
by (simp add: insert_body_split)
[PROOF STATE]
proof (state)
this:
\<exists>cs ds. bs = cs @ ds \<and> insert_body bs e = cs @ e # ds

goal (1 subgoal):
 1. \<And>a. i = Some a \<Longrightarrow> \<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>cs ds. bs = cs @ ds \<and> insert_body bs e = cs @ e # ds
[PROOF STEP]
obtain cs ds where "bs = cs @ ds \<and> insert_body bs e = cs @ e # ds"
[PROOF STATE]
proof (prove)
using this:
\<exists>cs ds. bs = cs @ ds \<and> insert_body bs e = cs @ e # ds

goal (1 subgoal):
 1. (\<And>cs ds. bs = cs @ ds \<and> insert_body bs e = cs @ e # ds \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bs = cs @ ds \<and> insert_body bs e = cs @ e # ds

goal (1 subgoal):
 1. \<And>a. i = Some a \<Longrightarrow> \<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i = Some r
xs = as @ r # bs \<and> (\<forall>x\<in>set as. x \<noteq> r)
bs = cs @ ds \<and> insert_body bs e = cs @ e # ds
[PROOF STEP]
have "xs = (as @ r # cs) @ ds \<and> insert_rga xs (e, i) = (as @ r # cs) @ e # ds"
[PROOF STATE]
proof (prove)
using this:
i = Some r
xs = as @ r # bs \<and> (\<forall>x\<in>set as. x \<noteq> r)
bs = cs @ ds \<and> insert_body bs e = cs @ e # ds

goal (1 subgoal):
 1. xs = (as @ r # cs) @ ds \<and> insert_rga xs (e, i) = (as @ r # cs) @ e # ds
[PROOF STEP]
using insert_rga_after_ref
[PROOF STATE]
proof (prove)
using this:
i = Some r
xs = as @ r # bs \<and> (\<forall>x\<in>set as. x \<noteq> r)
bs = cs @ ds \<and> insert_body bs e = cs @ e # ds
\<lbrakk>\<forall>x\<in>set ?as. ?a \<noteq> x; insert_body (?cs @ ?ds) ?e = ?cs @ ?e # ?ds\<rbrakk> \<Longrightarrow> insert_rga (?as @ ?a # ?cs @ ?ds) (?e, Some ?a) = ?as @ ?a # ?cs @ ?e # ?ds

goal (1 subgoal):
 1. xs = (as @ r # cs) @ ds \<and> insert_rga xs (e, i) = (as @ r # cs) @ e # ds
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
xs = (as @ r # cs) @ ds \<and> insert_rga xs (e, i) = (as @ r # cs) @ e # ds

goal (1 subgoal):
 1. \<And>a. i = Some a \<Longrightarrow> \<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = (as @ r # cs) @ ds \<and> insert_rga xs (e, i) = (as @ r # cs) @ e # ds
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = (as @ r # cs) @ ds \<and> insert_rga xs (e, i) = (as @ r # cs) @ e # ds

goal (1 subgoal):
 1. \<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>pre suf. xs = pre @ suf \<and> insert_rga xs (e, i) = pre @ e # suf

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rga_ops_rem_last:
  assumes "rga_ops (xs @ [x])"
  shows "rga_ops xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rga_ops xs
[PROOF STEP]
using assms crdt_ops_rem_last rga_ops_def
[PROOF STATE]
proof (prove)
using this:
rga_ops (xs @ [x])
crdt_ops (?xs @ [?x]) ?deps \<Longrightarrow> crdt_ops ?xs ?deps
rga_ops ?list \<equiv> crdt_ops ?list set_option

goal (1 subgoal):
 1. rga_ops xs
[PROOF STEP]
by blast


[STATEMENT]
lemma rga_ops_rem_penultimate:
  assumes "rga_ops (xs @ [(i1, r1), (i2, r2)])"
    and "\<And>r. r2 = Some r \<Longrightarrow> r \<noteq> i1"
  shows "rga_ops (xs @ [(i2, r2)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rga_ops (xs @ [(i2, r2)])
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rga_ops (xs @ [(i1, r1), (i2, r2)])
r2 = Some ?r \<Longrightarrow> ?r \<noteq> i1

goal (1 subgoal):
 1. rga_ops (xs @ [(i2, r2)])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>rga_ops (xs @ [(i1, r1), (i2, r2)]); \<And>r. r2 = Some r \<Longrightarrow> r \<noteq> i1\<rbrakk> \<Longrightarrow> rga_ops (xs @ [(i2, r2)])
[PROOF STEP]
have "crdt_ops (xs @ [(i2, r2)]) set_option"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crdt_ops (xs @ [(i2, r2)]) set_option
[PROOF STEP]
using assms crdt_ops_rem_penultimate rga_ops_def
[PROOF STATE]
proof (prove)
using this:
rga_ops (xs @ [(i1, r1), (i2, r2)])
r2 = Some ?r \<Longrightarrow> ?r \<noteq> i1
\<lbrakk>crdt_ops (?xs @ [(?i1.0, ?r1.0)] @ [(?i2.0, ?r2.0)]) ?deps; \<And>r. r \<in> ?deps ?r2.0 \<Longrightarrow> r \<noteq> ?i1.0\<rbrakk> \<Longrightarrow> crdt_ops (?xs @ [(?i2.0, ?r2.0)]) ?deps
rga_ops ?list \<equiv> crdt_ops ?list set_option

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

goal (1 subgoal):
 1. \<lbrakk>rga_ops (xs @ [(i1, r1), (i2, r2)]); \<And>r. r2 = Some r \<Longrightarrow> r \<noteq> i1\<rbrakk> \<Longrightarrow> rga_ops (xs @ [(i2, r2)])
[PROOF STEP]
thus "rga_ops (xs @ [(i2, r2)])"
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ [(i2, r2)]) set_option

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rga_ops_ref_exists:
  assumes "rga_ops (pre @ (oid, Some ref) # suf)"
  shows "ref \<in> fst ` set pre"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ref \<in> fst ` set pre
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ref \<in> fst ` set pre
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
rga_ops (pre @ (oid, Some ref) # suf)
[PROOF STEP]
have "crdt_ops (pre @ (oid, Some ref) # suf) set_option"
[PROOF STATE]
proof (prove)
using this:
rga_ops (pre @ (oid, Some ref) # suf)

goal (1 subgoal):
 1. crdt_ops (pre @ (oid, Some ref) # suf) set_option
[PROOF STEP]
by (simp add: rga_ops_def)
[PROOF STATE]
proof (state)
this:
crdt_ops (pre @ (oid, Some ref) # suf) set_option

goal (1 subgoal):
 1. ref \<in> fst ` set pre
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
crdt_ops (pre @ (oid, Some ref) # suf) set_option

goal (1 subgoal):
 1. ref \<in> fst ` set pre
[PROOF STEP]
have "set_option (Some ref) = {ref}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_option (Some ref) = {ref}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set_option (Some ref) = {ref}

goal (1 subgoal):
 1. ref \<in> fst ` set pre
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
crdt_ops (pre @ (oid, Some ref) # suf) set_option
set_option (Some ref) = {ref}
[PROOF STEP]
show "ref \<in> fst ` set pre"
[PROOF STATE]
proof (prove)
using this:
crdt_ops (pre @ (oid, Some ref) # suf) set_option
set_option (Some ref) = {ref}

goal (1 subgoal):
 1. ref \<in> fst ` set pre
[PROOF STEP]
using crdt_ops_ref_exists
[PROOF STATE]
proof (prove)
using this:
crdt_ops (pre @ (oid, Some ref) # suf) set_option
set_option (Some ref) = {ref}
\<lbrakk>crdt_ops (?pre @ (?oid, ?oper) # ?suf) ?deps; ?ref \<in> ?deps ?oper\<rbrakk> \<Longrightarrow> ?ref \<in> fst ` set ?pre

goal (1 subgoal):
 1. ref \<in> fst ` set pre
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ref \<in> fst ` set pre

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma interp_rga_tail_unfold:
  shows "interp_rga (xs@[x]) = insert_rga (interp_rga (xs)) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interp_rga (xs @ [x]) = insert_rga (interp_rga xs) x
[PROOF STEP]
by (clarsimp simp add: interp_rga_def)


[STATEMENT]
lemma interp_rga_ids:
  assumes "rga_ops xs"
  shows "set (interp_rga xs) = set (map fst xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (interp_rga xs) = set (map fst xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rga_ops xs

goal (1 subgoal):
 1. set (interp_rga xs) = set (map fst xs)
[PROOF STEP]
proof(induction xs rule: List.rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rga_ops [] \<Longrightarrow> set (interp_rga []) = set (map fst [])
 2. \<And>x xs. \<lbrakk>rga_ops xs \<Longrightarrow> set (interp_rga xs) = set (map fst xs); rga_ops (xs @ [x])\<rbrakk> \<Longrightarrow> set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
rga_ops []

goal (2 subgoals):
 1. rga_ops [] \<Longrightarrow> set (interp_rga []) = set (map fst [])
 2. \<And>x xs. \<lbrakk>rga_ops xs \<Longrightarrow> set (interp_rga xs) = set (map fst xs); rga_ops (xs @ [x])\<rbrakk> \<Longrightarrow> set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rga_ops []
[PROOF STEP]
show "set (interp_rga []) = set (map fst [])"
[PROOF STATE]
proof (prove)
using this:
rga_ops []

goal (1 subgoal):
 1. set (interp_rga []) = set (map fst [])
[PROOF STEP]
by (simp add: interp_rga_def)
[PROOF STATE]
proof (state)
this:
set (interp_rga []) = set (map fst [])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>rga_ops xs \<Longrightarrow> set (interp_rga xs) = set (map fst xs); rga_ops (xs @ [x])\<rbrakk> \<Longrightarrow> set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>rga_ops xs \<Longrightarrow> set (interp_rga xs) = set (map fst xs); rga_ops (xs @ [x])\<rbrakk> \<Longrightarrow> set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
rga_ops xs \<Longrightarrow> set (interp_rga xs) = set (map fst xs)
rga_ops (xs @ [x])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>rga_ops xs \<Longrightarrow> set (interp_rga xs) = set (map fst xs); rga_ops (xs @ [x])\<rbrakk> \<Longrightarrow> set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
[PROOF STEP]
hence IH: "set (interp_rga xs) = set (map fst xs)"
[PROOF STATE]
proof (prove)
using this:
rga_ops xs \<Longrightarrow> set (interp_rga xs) = set (map fst xs)
rga_ops (xs @ [x])

goal (1 subgoal):
 1. set (interp_rga xs) = set (map fst xs)
[PROOF STEP]
using rga_ops_rem_last
[PROOF STATE]
proof (prove)
using this:
rga_ops xs \<Longrightarrow> set (interp_rga xs) = set (map fst xs)
rga_ops (xs @ [x])
rga_ops (?xs @ [?x]) \<Longrightarrow> rga_ops ?xs

goal (1 subgoal):
 1. set (interp_rga xs) = set (map fst xs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set (interp_rga xs) = set (map fst xs)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>rga_ops xs \<Longrightarrow> set (interp_rga xs) = set (map fst xs); rga_ops (xs @ [x])\<rbrakk> \<Longrightarrow> set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
[PROOF STEP]
obtain xi xr where x_pair: "x = (xi, xr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xi xr. x = (xi, xr) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x = (xi, xr)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>rga_ops xs \<Longrightarrow> set (interp_rga xs) = set (map fst xs); rga_ops (xs @ [x])\<rbrakk> \<Longrightarrow> set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = (xi, xr)
[PROOF STEP]
show "set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))"
[PROOF STATE]
proof (prove)
using this:
x = (xi, xr)

goal (1 subgoal):
 1. set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
[PROOF STEP]
proof(cases xr)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x = (xi, xr); xr = None\<rbrakk> \<Longrightarrow> set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
 2. \<And>a. \<lbrakk>x = (xi, xr); xr = Some a\<rbrakk> \<Longrightarrow> set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
xr = None

goal (2 subgoals):
 1. \<lbrakk>x = (xi, xr); xr = None\<rbrakk> \<Longrightarrow> set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
 2. \<And>a. \<lbrakk>x = (xi, xr); xr = Some a\<rbrakk> \<Longrightarrow> set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xr = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xr = None

goal (1 subgoal):
 1. set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
[PROOF STEP]
using IH x_pair
[PROOF STATE]
proof (prove)
using this:
xr = None
set (interp_rga xs) = set (map fst xs)
x = (xi, xr)

goal (1 subgoal):
 1. set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
[PROOF STEP]
by (clarsimp simp add: interp_rga_def)
[PROOF STATE]
proof (state)
this:
set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))

goal (1 subgoal):
 1. \<And>a. \<lbrakk>x = (xi, xr); xr = Some a\<rbrakk> \<Longrightarrow> set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>x = (xi, xr); xr = Some a\<rbrakk> \<Longrightarrow> set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
[PROOF STEP]
case (Some r)
[PROOF STATE]
proof (state)
this:
xr = Some r

goal (1 subgoal):
 1. \<And>a. \<lbrakk>x = (xi, xr); xr = Some a\<rbrakk> \<Longrightarrow> set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xr = Some r

goal (1 subgoal):
 1. \<And>a. \<lbrakk>x = (xi, xr); xr = Some a\<rbrakk> \<Longrightarrow> set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
xr = Some r
[PROOF STEP]
have "r \<in> set (interp_rga xs)"
[PROOF STATE]
proof (prove)
using this:
xr = Some r

goal (1 subgoal):
 1. r \<in> set (interp_rga xs)
[PROOF STEP]
using IH rga_ops_ref_exists
[PROOF STATE]
proof (prove)
using this:
xr = Some r
set (interp_rga xs) = set (map fst xs)
rga_ops (?pre @ (?oid, Some ?ref) # ?suf) \<Longrightarrow> ?ref \<in> fst ` set ?pre

goal (1 subgoal):
 1. r \<in> set (interp_rga xs)
[PROOF STEP]
by (metis x_pair list.set_map snoc.prems)
[PROOF STATE]
proof (state)
this:
r \<in> set (interp_rga xs)

goal (1 subgoal):
 1. \<And>a. \<lbrakk>x = (xi, xr); xr = Some a\<rbrakk> \<Longrightarrow> set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
xr = Some r
r \<in> set (interp_rga xs)
[PROOF STEP]
have "set (interp_rga (xs @ [(xi, xr)])) = insert xi (set (interp_rga xs))"
[PROOF STATE]
proof (prove)
using this:
xr = Some r
r \<in> set (interp_rga xs)

goal (1 subgoal):
 1. set (interp_rga (xs @ [(xi, xr)])) = insert xi (set (interp_rga xs))
[PROOF STEP]
by (simp add: insert_rga_set_ins interp_rga_tail_unfold)
[PROOF STATE]
proof (state)
this:
set (interp_rga (xs @ [(xi, xr)])) = insert xi (set (interp_rga xs))

goal (1 subgoal):
 1. \<And>a. \<lbrakk>x = (xi, xr); xr = Some a\<rbrakk> \<Longrightarrow> set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (interp_rga (xs @ [(xi, xr)])) = insert xi (set (interp_rga xs))
[PROOF STEP]
show "set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))"
[PROOF STATE]
proof (prove)
using this:
set (interp_rga (xs @ [(xi, xr)])) = insert xi (set (interp_rga xs))

goal (1 subgoal):
 1. set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
[PROOF STEP]
using IH x_pair
[PROOF STATE]
proof (prove)
using this:
set (interp_rga (xs @ [(xi, xr)])) = insert xi (set (interp_rga xs))
set (interp_rga xs) = set (map fst xs)
x = (xi, xr)

goal (1 subgoal):
 1. set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma interp_rga_distinct:
  assumes "rga_ops xs"
  shows "distinct (interp_rga xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (interp_rga xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rga_ops xs

goal (1 subgoal):
 1. distinct (interp_rga xs)
[PROOF STEP]
proof(induction xs rule: List.rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rga_ops [] \<Longrightarrow> distinct (interp_rga [])
 2. \<And>x xs. \<lbrakk>rga_ops xs \<Longrightarrow> distinct (interp_rga xs); rga_ops (xs @ [x])\<rbrakk> \<Longrightarrow> distinct (interp_rga (xs @ [x]))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
rga_ops []

goal (2 subgoals):
 1. rga_ops [] \<Longrightarrow> distinct (interp_rga [])
 2. \<And>x xs. \<lbrakk>rga_ops xs \<Longrightarrow> distinct (interp_rga xs); rga_ops (xs @ [x])\<rbrakk> \<Longrightarrow> distinct (interp_rga (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rga_ops []
[PROOF STEP]
show "distinct (interp_rga [])"
[PROOF STATE]
proof (prove)
using this:
rga_ops []

goal (1 subgoal):
 1. distinct (interp_rga [])
[PROOF STEP]
by (simp add: interp_rga_def)
[PROOF STATE]
proof (state)
this:
distinct (interp_rga [])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>rga_ops xs \<Longrightarrow> distinct (interp_rga xs); rga_ops (xs @ [x])\<rbrakk> \<Longrightarrow> distinct (interp_rga (xs @ [x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>rga_ops xs \<Longrightarrow> distinct (interp_rga xs); rga_ops (xs @ [x])\<rbrakk> \<Longrightarrow> distinct (interp_rga (xs @ [x]))
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
rga_ops xs \<Longrightarrow> distinct (interp_rga xs)
rga_ops (xs @ [x])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>rga_ops xs \<Longrightarrow> distinct (interp_rga xs); rga_ops (xs @ [x])\<rbrakk> \<Longrightarrow> distinct (interp_rga (xs @ [x]))
[PROOF STEP]
hence IH: "distinct (interp_rga xs)"
[PROOF STATE]
proof (prove)
using this:
rga_ops xs \<Longrightarrow> distinct (interp_rga xs)
rga_ops (xs @ [x])

goal (1 subgoal):
 1. distinct (interp_rga xs)
[PROOF STEP]
using rga_ops_rem_last
[PROOF STATE]
proof (prove)
using this:
rga_ops xs \<Longrightarrow> distinct (interp_rga xs)
rga_ops (xs @ [x])
rga_ops (?xs @ [?x]) \<Longrightarrow> rga_ops ?xs

goal (1 subgoal):
 1. distinct (interp_rga xs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinct (interp_rga xs)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>rga_ops xs \<Longrightarrow> distinct (interp_rga xs); rga_ops (xs @ [x])\<rbrakk> \<Longrightarrow> distinct (interp_rga (xs @ [x]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (interp_rga xs)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>rga_ops xs \<Longrightarrow> distinct (interp_rga xs); rga_ops (xs @ [x])\<rbrakk> \<Longrightarrow> distinct (interp_rga (xs @ [x]))
[PROOF STEP]
obtain xi xr where x_pair: "x = (xi, xr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xi xr. x = (xi, xr) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x = (xi, xr)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>rga_ops xs \<Longrightarrow> distinct (interp_rga xs); rga_ops (xs @ [x])\<rbrakk> \<Longrightarrow> distinct (interp_rga (xs @ [x]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = (xi, xr)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>rga_ops xs \<Longrightarrow> distinct (interp_rga xs); rga_ops (xs @ [x])\<rbrakk> \<Longrightarrow> distinct (interp_rga (xs @ [x]))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x = (xi, xr)
[PROOF STEP]
have "xi \<notin> set (interp_rga xs)"
[PROOF STATE]
proof (prove)
using this:
x = (xi, xr)

goal (1 subgoal):
 1. xi \<notin> set (interp_rga xs)
[PROOF STEP]
using interp_rga_ids crdt_ops_unique_last rga_ops_rem_last
[PROOF STATE]
proof (prove)
using this:
x = (xi, xr)
rga_ops ?xs \<Longrightarrow> set (interp_rga ?xs) = set (map fst ?xs)
crdt_ops (?xs @ [(?oid, ?oper)]) ?deps \<Longrightarrow> ?oid \<notin> set (map fst ?xs)
rga_ops (?xs @ [?x]) \<Longrightarrow> rga_ops ?xs

goal (1 subgoal):
 1. xi \<notin> set (interp_rga xs)
[PROOF STEP]
by (metis rga_ops_def snoc.prems)
[PROOF STATE]
proof (state)
this:
xi \<notin> set (interp_rga xs)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>rga_ops xs \<Longrightarrow> distinct (interp_rga xs); rga_ops (xs @ [x])\<rbrakk> \<Longrightarrow> distinct (interp_rga (xs @ [x]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xi \<notin> set (interp_rga xs)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>rga_ops xs \<Longrightarrow> distinct (interp_rga xs); rga_ops (xs @ [x])\<rbrakk> \<Longrightarrow> distinct (interp_rga (xs @ [x]))
[PROOF STEP]
have "\<exists>pre suf. interp_rga xs = pre@suf \<and>
           insert_rga (interp_rga xs) (xi, xr) = pre @ xi # suf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>pre suf. interp_rga xs = pre @ suf \<and> insert_rga (interp_rga xs) (xi, xr) = pre @ xi # suf
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>pre suf. interp_rga xs = pre @ suf \<and> insert_rga (interp_rga xs) (xi, xr) = pre @ xi # suf
[PROOF STEP]
have "\<And>r. r \<in> set_option xr \<Longrightarrow> r \<in> set (map fst xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. r \<in> set_option xr \<Longrightarrow> r \<in> set (map fst xs)
[PROOF STEP]
using crdt_ops_ref_exists rga_ops_def snoc.prems x_pair
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>crdt_ops (?pre @ (?oid, ?oper) # ?suf) ?deps; ?ref \<in> ?deps ?oper\<rbrakk> \<Longrightarrow> ?ref \<in> fst ` set ?pre
rga_ops ?list \<equiv> crdt_ops ?list set_option
rga_ops (xs @ [x])
x = (xi, xr)

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

goal (1 subgoal):
 1. \<exists>pre suf. interp_rga xs = pre @ suf \<and> insert_rga (interp_rga xs) (xi, xr) = pre @ xi # suf
[PROOF STEP]
hence "xr = None \<or> (\<exists>r. xr = Some r \<and> r \<in> set (map fst xs))"
[PROOF STATE]
proof (prove)
using this:
?r \<in> set_option xr \<Longrightarrow> ?r \<in> set (map fst xs)

goal (1 subgoal):
 1. xr = None \<or> (\<exists>r. xr = Some r \<and> r \<in> set (map fst xs))
[PROOF STEP]
using option.set_sel
[PROOF STATE]
proof (prove)
using this:
?r \<in> set_option xr \<Longrightarrow> ?r \<in> set (map fst xs)
?a \<noteq> None \<Longrightarrow> the ?a \<in> set_option ?a

goal (1 subgoal):
 1. xr = None \<or> (\<exists>r. xr = Some r \<and> r \<in> set (map fst xs))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xr = None \<or> (\<exists>r. xr = Some r \<and> r \<in> set (map fst xs))

goal (1 subgoal):
 1. \<exists>pre suf. interp_rga xs = pre @ suf \<and> insert_rga (interp_rga xs) (xi, xr) = pre @ xi # suf
[PROOF STEP]
hence "xr = None \<or> (\<exists>r. xr = Some r \<and> r \<in> set (interp_rga xs))"
[PROOF STATE]
proof (prove)
using this:
xr = None \<or> (\<exists>r. xr = Some r \<and> r \<in> set (map fst xs))

goal (1 subgoal):
 1. xr = None \<or> (\<exists>r. xr = Some r \<and> r \<in> set (interp_rga xs))
[PROOF STEP]
using interp_rga_ids rga_ops_rem_last snoc.prems
[PROOF STATE]
proof (prove)
using this:
xr = None \<or> (\<exists>r. xr = Some r \<and> r \<in> set (map fst xs))
rga_ops ?xs \<Longrightarrow> set (interp_rga ?xs) = set (map fst ?xs)
rga_ops (?xs @ [?x]) \<Longrightarrow> rga_ops ?xs
rga_ops (xs @ [x])

goal (1 subgoal):
 1. xr = None \<or> (\<exists>r. xr = Some r \<and> r \<in> set (interp_rga xs))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xr = None \<or> (\<exists>r. xr = Some r \<and> r \<in> set (interp_rga xs))

goal (1 subgoal):
 1. \<exists>pre suf. interp_rga xs = pre @ suf \<and> insert_rga (interp_rga xs) (xi, xr) = pre @ xi # suf
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
xr = None \<or> (\<exists>r. xr = Some r \<and> r \<in> set (interp_rga xs))

goal (1 subgoal):
 1. \<exists>pre suf. interp_rga xs = pre @ suf \<and> insert_rga (interp_rga xs) (xi, xr) = pre @ xi # suf
[PROOF STEP]
using IH insert_rga_preserves_order
[PROOF STATE]
proof (prove)
using this:
xr = None \<or> (\<exists>r. xr = Some r \<and> r \<in> set (interp_rga xs))
distinct (interp_rga xs)
\<lbrakk>?i = None \<or> (\<exists>i'. ?i = Some i' \<and> i' \<in> set ?xs); distinct ?xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. ?xs = pre @ suf \<and> insert_rga ?xs (?e, ?i) = pre @ ?e # suf

goal (1 subgoal):
 1. \<exists>pre suf. interp_rga xs = pre @ suf \<and> insert_rga (interp_rga xs) (xi, xr) = pre @ xi # suf
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>pre suf. interp_rga xs = pre @ suf \<and> insert_rga (interp_rga xs) (xi, xr) = pre @ xi # suf

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>pre suf. interp_rga xs = pre @ suf \<and> insert_rga (interp_rga xs) (xi, xr) = pre @ xi # suf

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>rga_ops xs \<Longrightarrow> distinct (interp_rga xs); rga_ops (xs @ [x])\<rbrakk> \<Longrightarrow> distinct (interp_rga (xs @ [x]))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
distinct (interp_rga xs)
x = (xi, xr)
xi \<notin> set (interp_rga xs)
\<exists>pre suf. interp_rga xs = pre @ suf \<and> insert_rga (interp_rga xs) (xi, xr) = pre @ xi # suf
[PROOF STEP]
show "distinct (interp_rga (xs @ [x]))"
[PROOF STATE]
proof (prove)
using this:
distinct (interp_rga xs)
x = (xi, xr)
xi \<notin> set (interp_rga xs)
\<exists>pre suf. interp_rga xs = pre @ suf \<and> insert_rga (interp_rga xs) (xi, xr) = pre @ xi # suf

goal (1 subgoal):
 1. distinct (interp_rga (xs @ [x]))
[PROOF STEP]
by (metis Un_iff disjoint_insert(1) distinct.simps(2) distinct_append
        interp_rga_tail_unfold list.simps(15) set_append)
[PROOF STATE]
proof (state)
this:
distinct (interp_rga (xs @ [x]))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma final_insert:
  assumes "set (xs @ [x]) = set (ys @ [x])"
    and "rga_ops (xs @ [x])"
    and "insert_ops (ys @ [x])"
    and "interp_rga xs = interp_ins ys"
  shows "interp_rga (xs @ [x]) = interp_ins (ys @ [x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
obtain oid ref where x_pair: "x = (oid, ref)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>oid ref. x = (oid, ref) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x = (oid, ref)

goal (1 subgoal):
 1. interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
have "distinct (xs @ [x])" and "distinct (ys @ [x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (xs @ [x]) &&& distinct (ys @ [x])
[PROOF STEP]
using assms crdt_ops_distinct spec_ops_distinct rga_ops_def insert_ops_def
[PROOF STATE]
proof (prove)
using this:
set (xs @ [x]) = set (ys @ [x])
rga_ops (xs @ [x])
insert_ops (ys @ [x])
interp_rga xs = interp_ins ys
crdt_ops ?xs ?deps \<Longrightarrow> distinct ?xs
spec_ops ?ops ?deps \<Longrightarrow> distinct ?ops
rga_ops ?list \<equiv> crdt_ops ?list set_option
insert_ops ?list \<equiv> spec_ops ?list set_option

goal (1 subgoal):
 1. distinct (xs @ [x]) &&& distinct (ys @ [x])
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
distinct (xs @ [x])
distinct (ys @ [x])

goal (1 subgoal):
 1. interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (xs @ [x])
distinct (ys @ [x])
[PROOF STEP]
have "set xs = set ys"
[PROOF STATE]
proof (prove)
using this:
distinct (xs @ [x])
distinct (ys @ [x])

goal (1 subgoal):
 1. set xs = set ys
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
distinct (xs @ [x])
distinct (ys @ [x])
set (xs @ [x]) = set (ys @ [x])

goal (1 subgoal):
 1. set xs = set ys
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
set xs = set ys

goal (1 subgoal):
 1. interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
have oid_greatest: "\<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid
[PROOF STEP]
have "\<And>i. i \<in> set (map fst ys) \<Longrightarrow> i < oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> set (map fst ys) \<Longrightarrow> i < oid
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
insert_ops (ys @ [x])

goal (1 subgoal):
 1. \<And>i. i \<in> set (map fst ys) \<Longrightarrow> i < oid
[PROOF STEP]
by (simp add: spec_ops_id_inc x_pair insert_ops_def)
[PROOF STATE]
proof (state)
this:
?i \<in> set (map fst ys) \<Longrightarrow> ?i < oid

goal (1 subgoal):
 1. \<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid
[PROOF STEP]
hence "\<And>i. i \<in> set (map fst xs) \<Longrightarrow> i < oid"
[PROOF STATE]
proof (prove)
using this:
?i \<in> set (map fst ys) \<Longrightarrow> ?i < oid

goal (1 subgoal):
 1. \<And>i. i \<in> set (map fst xs) \<Longrightarrow> i < oid
[PROOF STEP]
using \<open>set xs = set ys\<close>
[PROOF STATE]
proof (prove)
using this:
?i \<in> set (map fst ys) \<Longrightarrow> ?i < oid
set xs = set ys

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

goal (1 subgoal):
 1. \<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid
[PROOF STEP]
thus "\<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid"
[PROOF STATE]
proof (prove)
using this:
?i \<in> set (map fst xs) \<Longrightarrow> ?i < oid

goal (1 subgoal):
 1. \<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid
[PROOF STEP]
using assms(2) interp_rga_ids rga_ops_rem_last
[PROOF STATE]
proof (prove)
using this:
?i \<in> set (map fst xs) \<Longrightarrow> ?i < oid
rga_ops (xs @ [x])
rga_ops ?xs \<Longrightarrow> set (interp_rga ?xs) = set (map fst ?xs)
rga_ops (?xs @ [?x]) \<Longrightarrow> rga_ops ?xs

goal (1 subgoal):
 1. \<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?i \<in> set (interp_rga xs) \<Longrightarrow> ?i < oid

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i \<in> set (interp_rga xs) \<Longrightarrow> ?i < oid

goal (1 subgoal):
 1. interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
thus "interp_rga (xs @ [x]) = interp_ins (ys @ [x])"
[PROOF STATE]
proof (prove)
using this:
?i \<in> set (interp_rga xs) \<Longrightarrow> ?i < oid

goal (1 subgoal):
 1. interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
proof(cases ref)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid; ref = None\<rbrakk> \<Longrightarrow> interp_rga (xs @ [x]) = interp_ins (ys @ [x])
 2. \<And>a. \<lbrakk>\<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid; ref = Some a\<rbrakk> \<Longrightarrow> interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
ref = None

goal (2 subgoals):
 1. \<lbrakk>\<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid; ref = None\<rbrakk> \<Longrightarrow> interp_rga (xs @ [x]) = interp_ins (ys @ [x])
 2. \<And>a. \<lbrakk>\<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid; ref = Some a\<rbrakk> \<Longrightarrow> interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ref = None

goal (2 subgoals):
 1. \<lbrakk>\<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid; ref = None\<rbrakk> \<Longrightarrow> interp_rga (xs @ [x]) = interp_ins (ys @ [x])
 2. \<And>a. \<lbrakk>\<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid; ref = Some a\<rbrakk> \<Longrightarrow> interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
ref = None
[PROOF STEP]
have "insert_rga (interp_rga xs) (oid, ref) = oid # interp_rga xs"
[PROOF STATE]
proof (prove)
using this:
ref = None

goal (1 subgoal):
 1. insert_rga (interp_rga xs) (oid, ref) = oid # interp_rga xs
[PROOF STEP]
using oid_greatest hd_in_set insert_body.elims insert_body.simps(1)
        insert_rga.simps(1) list.sel(1)
[PROOF STATE]
proof (prove)
using this:
ref = None
?i \<in> set (interp_rga xs) \<Longrightarrow> ?i < oid
?xs \<noteq> [] \<Longrightarrow> hd ?xs \<in> set ?xs
\<lbrakk>insert_body ?x ?xa = ?y; \<And>e. \<lbrakk>?x = []; ?xa = e; ?y = [e]\<rbrakk> \<Longrightarrow> ?P; \<And>x xs e. \<lbrakk>?x = x # xs; ?xa = e; ?y = (if x < e then e # x # xs else x # insert_body xs e)\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
insert_body [] ?e = [?e]
insert_rga ?xs (?e, None) = insert_body ?xs ?e
hd (?x21.0 # ?x22.0) = ?x21.0

goal (1 subgoal):
 1. insert_rga (interp_rga xs) (oid, ref) = oid # interp_rga xs
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
insert_rga (interp_rga xs) (oid, ref) = oid # interp_rga xs

goal (2 subgoals):
 1. \<lbrakk>\<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid; ref = None\<rbrakk> \<Longrightarrow> interp_rga (xs @ [x]) = interp_ins (ys @ [x])
 2. \<And>a. \<lbrakk>\<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid; ref = Some a\<rbrakk> \<Longrightarrow> interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ref = None
insert_rga (interp_rga xs) (oid, ref) = oid # interp_rga xs
[PROOF STEP]
show "interp_rga (xs @ [x]) = interp_ins (ys @ [x])"
[PROOF STATE]
proof (prove)
using this:
ref = None
insert_rga (interp_rga xs) (oid, ref) = oid # interp_rga xs

goal (1 subgoal):
 1. interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
ref = None
insert_rga (interp_rga xs) (oid, ref) = oid # interp_rga xs
interp_rga xs = interp_ins ys

goal (1 subgoal):
 1. interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
by (simp add: interp_ins_tail_unfold interp_rga_tail_unfold x_pair)
[PROOF STATE]
proof (state)
this:
interp_rga (xs @ [x]) = interp_ins (ys @ [x])

goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid; ref = Some a\<rbrakk> \<Longrightarrow> interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid; ref = Some a\<rbrakk> \<Longrightarrow> interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
case (Some r)
[PROOF STATE]
proof (state)
this:
ref = Some r

goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid; ref = Some a\<rbrakk> \<Longrightarrow> interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
have "\<exists>as bs. interp_rga xs = as @ r # bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>as bs. interp_rga xs = as @ r # bs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>as bs. interp_rga xs = as @ r # bs
[PROOF STEP]
have "r \<in> set (map fst xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> set (map fst xs)
[PROOF STEP]
using assms(2) Some
[PROOF STATE]
proof (prove)
using this:
rga_ops (xs @ [x])
ref = Some r

goal (1 subgoal):
 1. r \<in> set (map fst xs)
[PROOF STEP]
by (simp add: rga_ops_ref_exists x_pair)
[PROOF STATE]
proof (state)
this:
r \<in> set (map fst xs)

goal (1 subgoal):
 1. \<exists>as bs. interp_rga xs = as @ r # bs
[PROOF STEP]
hence "r \<in> set (interp_rga xs)"
[PROOF STATE]
proof (prove)
using this:
r \<in> set (map fst xs)

goal (1 subgoal):
 1. r \<in> set (interp_rga xs)
[PROOF STEP]
using assms(2) interp_rga_ids rga_ops_rem_last
[PROOF STATE]
proof (prove)
using this:
r \<in> set (map fst xs)
rga_ops (xs @ [x])
rga_ops ?xs \<Longrightarrow> set (interp_rga ?xs) = set (map fst ?xs)
rga_ops (?xs @ [?x]) \<Longrightarrow> rga_ops ?xs

goal (1 subgoal):
 1. r \<in> set (interp_rga xs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r \<in> set (interp_rga xs)

goal (1 subgoal):
 1. \<exists>as bs. interp_rga xs = as @ r # bs
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
r \<in> set (interp_rga xs)

goal (1 subgoal):
 1. \<exists>as bs. interp_rga xs = as @ r # bs
[PROOF STEP]
by (simp add: split_list)
[PROOF STATE]
proof (state)
this:
\<exists>as bs. interp_rga xs = as @ r # bs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>as bs. interp_rga xs = as @ r # bs

goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid; ref = Some a\<rbrakk> \<Longrightarrow> interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>as bs. interp_rga xs = as @ r # bs
[PROOF STEP]
obtain as bs where as_bs: "interp_rga xs = as @ r # bs"
[PROOF STATE]
proof (prove)
using this:
\<exists>as bs. interp_rga xs = as @ r # bs

goal (1 subgoal):
 1. (\<And>as bs. interp_rga xs = as @ r # bs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
interp_rga xs = as @ r # bs

goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid; ref = Some a\<rbrakk> \<Longrightarrow> interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
hence "distinct (as @ r # bs)"
[PROOF STATE]
proof (prove)
using this:
interp_rga xs = as @ r # bs

goal (1 subgoal):
 1. distinct (as @ r # bs)
[PROOF STEP]
by (metis assms(2) interp_rga_distinct rga_ops_rem_last)
[PROOF STATE]
proof (state)
this:
distinct (as @ r # bs)

goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid; ref = Some a\<rbrakk> \<Longrightarrow> interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
hence "insert_rga (as @ r # bs) (oid, Some r) = as @ r # oid # bs"
[PROOF STATE]
proof (prove)
using this:
distinct (as @ r # bs)

goal (1 subgoal):
 1. insert_rga (as @ r # bs) (oid, Some r) = as @ r # oid # bs
[PROOF STEP]
by (metis as_bs insert_between_elements oid_greatest)
[PROOF STATE]
proof (state)
this:
insert_rga (as @ r # bs) (oid, Some r) = as @ r # oid # bs

goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid; ref = Some a\<rbrakk> \<Longrightarrow> interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_rga (as @ r # bs) (oid, Some r) = as @ r # oid # bs

goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid; ref = Some a\<rbrakk> \<Longrightarrow> interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
have "insert_spec (as @ r # bs) (oid, Some r) = as @ r # oid # bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_spec (as @ r # bs) (oid, Some r) = as @ r # oid # bs
[PROOF STEP]
by (meson \<open>distinct (as @ r # bs)\<close> insert_after_ref)
[PROOF STATE]
proof (state)
this:
insert_spec (as @ r # bs) (oid, Some r) = as @ r # oid # bs

goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>i. i \<in> set (interp_rga xs) \<Longrightarrow> i < oid; ref = Some a\<rbrakk> \<Longrightarrow> interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
insert_rga (as @ r # bs) (oid, Some r) = as @ r # oid # bs
insert_spec (as @ r # bs) (oid, Some r) = as @ r # oid # bs
[PROOF STEP]
show "interp_rga (xs @ [x]) = interp_ins (ys @ [x])"
[PROOF STATE]
proof (prove)
using this:
insert_rga (as @ r # bs) (oid, Some r) = as @ r # oid # bs
insert_spec (as @ r # bs) (oid, Some r) = as @ r # oid # bs

goal (1 subgoal):
 1. interp_rga (xs @ [x]) = interp_ins (ys @ [x])
[PROOF STEP]
by (metis assms(4) Some as_bs interp_ins_tail_unfold interp_rga_tail_unfold x_pair)
[PROOF STATE]
proof (state)
this:
interp_rga (xs @ [x]) = interp_ins (ys @ [x])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
interp_rga (xs @ [x]) = interp_ins (ys @ [x])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rga_spec_equal:
  assumes "set xs = set ys"
    and "insert_ops xs"
    and "rga_ops ys"
  shows "interp_ins xs = interp_rga ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interp_ins xs = interp_rga ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set xs = set ys
insert_ops xs
rga_ops ys

goal (1 subgoal):
 1. interp_ins xs = interp_rga ys
[PROOF STEP]
proof(induction xs arbitrary: ys rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ys. \<lbrakk>set [] = set ys; insert_ops []; rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins [] = interp_rga ys
 2. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; insert_ops xs; rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins xs = interp_rga ys; set (xs @ [x]) = set ys; insert_ops (xs @ [x]); rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins (xs @ [x]) = interp_rga ys
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
set [] = set ys
insert_ops []
rga_ops ys

goal (2 subgoals):
 1. \<And>ys. \<lbrakk>set [] = set ys; insert_ops []; rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins [] = interp_rga ys
 2. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; insert_ops xs; rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins xs = interp_rga ys; set (xs @ [x]) = set ys; insert_ops (xs @ [x]); rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins (xs @ [x]) = interp_rga ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set [] = set ys
insert_ops []
rga_ops ys
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set [] = set ys
insert_ops []
rga_ops ys

goal (1 subgoal):
 1. interp_ins [] = interp_rga ys
[PROOF STEP]
by (simp add: interp_rga_def interp_ins_def)
[PROOF STATE]
proof (state)
this:
interp_ins [] = interp_rga ys

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; insert_ops xs; rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins xs = interp_rga ys; set (xs @ [x]) = set ys; insert_ops (xs @ [x]); rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins (xs @ [x]) = interp_rga ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; insert_ops xs; rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins xs = interp_rga ys; set (xs @ [x]) = set ys; insert_ops (xs @ [x]); rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins (xs @ [x]) = interp_rga ys
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>set xs = set ?ys; insert_ops xs; rga_ops ?ys\<rbrakk> \<Longrightarrow> interp_ins xs = interp_rga ?ys
set (xs @ [x]) = set ys
insert_ops (xs @ [x])
rga_ops ys

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; insert_ops xs; rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins xs = interp_rga ys; set (xs @ [x]) = set ys; insert_ops (xs @ [x]); rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins (xs @ [x]) = interp_rga ys
[PROOF STEP]
hence "x \<in> set ys"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set xs = set ?ys; insert_ops xs; rga_ops ?ys\<rbrakk> \<Longrightarrow> interp_ins xs = interp_rga ?ys
set (xs @ [x]) = set ys
insert_ops (xs @ [x])
rga_ops ys

goal (1 subgoal):
 1. x \<in> set ys
[PROOF STEP]
by (metis last_in_set snoc_eq_iff_butlast)
[PROOF STATE]
proof (state)
this:
x \<in> set ys

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; insert_ops xs; rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins xs = interp_rga ys; set (xs @ [x]) = set ys; insert_ops (xs @ [x]); rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins (xs @ [x]) = interp_rga ys
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x \<in> set ys
[PROOF STEP]
obtain pre suf where ys_split: "ys = pre @ [x] @ suf"
[PROOF STATE]
proof (prove)
using this:
x \<in> set ys

goal (1 subgoal):
 1. (\<And>pre suf. ys = pre @ [x] @ suf \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using split_list_first
[PROOF STATE]
proof (prove)
using this:
x \<in> set ys
?x \<in> set ?xs \<Longrightarrow> \<exists>ys zs. ?xs = ys @ ?x # zs \<and> ?x \<notin> set ys

goal (1 subgoal):
 1. (\<And>pre suf. ys = pre @ [x] @ suf \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ys = pre @ [x] @ suf

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; insert_ops xs; rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins xs = interp_rga ys; set (xs @ [x]) = set ys; insert_ops (xs @ [x]); rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins (xs @ [x]) = interp_rga ys
[PROOF STEP]
have IH: "interp_ins xs = interp_rga (pre @ suf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interp_ins xs = interp_rga (pre @ suf)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. interp_ins xs = interp_rga (pre @ suf)
[PROOF STEP]
have "crdt_ops (pre @ suf) set_option"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crdt_ops (pre @ suf) set_option
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. crdt_ops (pre @ suf) set_option
[PROOF STEP]
have "crdt_ops (pre @ [x] @ suf) set_option"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crdt_ops (pre @ [x] @ suf) set_option
[PROOF STEP]
using rga_ops_def snoc.prems(3) ys_split
[PROOF STATE]
proof (prove)
using this:
rga_ops ?list \<equiv> crdt_ops ?list set_option
rga_ops ys
ys = pre @ [x] @ suf

goal (1 subgoal):
 1. crdt_ops (pre @ [x] @ suf) set_option
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
crdt_ops (pre @ [x] @ suf) set_option

goal (1 subgoal):
 1. crdt_ops (pre @ suf) set_option
[PROOF STEP]
thus "crdt_ops (pre @ suf) set_option"
[PROOF STATE]
proof (prove)
using this:
crdt_ops (pre @ [x] @ suf) set_option

goal (1 subgoal):
 1. crdt_ops (pre @ suf) set_option
[PROOF STEP]
using crdt_ops_rem_spec snoc.prems ys_split insert_ops_def
[PROOF STATE]
proof (prove)
using this:
crdt_ops (pre @ [x] @ suf) set_option
\<lbrakk>spec_ops (?xs @ [?x]) ?deps; crdt_ops (?ys @ [?x] @ ?zs) ?deps; set (?xs @ [?x]) = set (?ys @ [?x] @ ?zs)\<rbrakk> \<Longrightarrow> crdt_ops (?ys @ ?zs) ?deps
set (xs @ [x]) = set ys
insert_ops (xs @ [x])
rga_ops ys
ys = pre @ [x] @ suf
insert_ops ?list \<equiv> spec_ops ?list set_option

goal (1 subgoal):
 1. crdt_ops (pre @ suf) set_option
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
crdt_ops (pre @ suf) set_option

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
crdt_ops (pre @ suf) set_option

goal (1 subgoal):
 1. interp_ins xs = interp_rga (pre @ suf)
[PROOF STEP]
hence "rga_ops (pre @ suf)"
[PROOF STATE]
proof (prove)
using this:
crdt_ops (pre @ suf) set_option

goal (1 subgoal):
 1. rga_ops (pre @ suf)
[PROOF STEP]
using rga_ops_def
[PROOF STATE]
proof (prove)
using this:
crdt_ops (pre @ suf) set_option
rga_ops ?list \<equiv> crdt_ops ?list set_option

goal (1 subgoal):
 1. rga_ops (pre @ suf)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rga_ops (pre @ suf)

goal (1 subgoal):
 1. interp_ins xs = interp_rga (pre @ suf)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rga_ops (pre @ suf)

goal (1 subgoal):
 1. interp_ins xs = interp_rga (pre @ suf)
[PROOF STEP]
have "set xs = set (pre @ suf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs = set (pre @ suf)
[PROOF STEP]
by (metis append_set_rem_last crdt_ops_distinct insert_ops_def rga_ops_def
          snoc.prems spec_ops_distinct ys_split)
[PROOF STATE]
proof (state)
this:
set xs = set (pre @ suf)

goal (1 subgoal):
 1. interp_ins xs = interp_rga (pre @ suf)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rga_ops (pre @ suf)
set xs = set (pre @ suf)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rga_ops (pre @ suf)
set xs = set (pre @ suf)

goal (1 subgoal):
 1. interp_ins xs = interp_rga (pre @ suf)
[PROOF STEP]
using insert_ops_rem_last ys_split snoc
[PROOF STATE]
proof (prove)
using this:
rga_ops (pre @ suf)
set xs = set (pre @ suf)
insert_ops (?xs @ [?x]) \<Longrightarrow> insert_ops ?xs
ys = pre @ [x] @ suf
\<lbrakk>set xs = set ?ys; insert_ops xs; rga_ops ?ys\<rbrakk> \<Longrightarrow> interp_ins xs = interp_rga ?ys
set (xs @ [x]) = set ys
insert_ops (xs @ [x])
rga_ops ys

goal (1 subgoal):
 1. interp_ins xs = interp_rga (pre @ suf)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
interp_ins xs = interp_rga (pre @ suf)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
interp_ins xs = interp_rga (pre @ suf)

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; insert_ops xs; rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins xs = interp_rga ys; set (xs @ [x]) = set ys; insert_ops (xs @ [x]); rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins (xs @ [x]) = interp_rga ys
[PROOF STEP]
have valid_rga: "rga_ops (pre @ suf @ [x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rga_ops (pre @ suf @ [x])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rga_ops (pre @ suf @ [x])
[PROOF STEP]
have "crdt_ops (pre @ suf @ [x]) set_option"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crdt_ops (pre @ suf @ [x]) set_option
[PROOF STEP]
using snoc.prems ys_split
[PROOF STATE]
proof (prove)
using this:
set (xs @ [x]) = set ys
insert_ops (xs @ [x])
rga_ops ys
ys = pre @ [x] @ suf

goal (1 subgoal):
 1. crdt_ops (pre @ suf @ [x]) set_option
[PROOF STEP]
by (simp add: crdt_ops_reorder_spec insert_ops_def rga_ops_def)
[PROOF STATE]
proof (state)
this:
crdt_ops (pre @ suf @ [x]) set_option

goal (1 subgoal):
 1. rga_ops (pre @ suf @ [x])
[PROOF STEP]
thus "rga_ops (pre @ suf @ [x])"
[PROOF STATE]
proof (prove)
using this:
crdt_ops (pre @ suf @ [x]) set_option

goal (1 subgoal):
 1. rga_ops (pre @ suf @ [x])
[PROOF STEP]
by (simp add: rga_ops_def)
[PROOF STATE]
proof (state)
this:
rga_ops (pre @ suf @ [x])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rga_ops (pre @ suf @ [x])

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; insert_ops xs; rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins xs = interp_rga ys; set (xs @ [x]) = set ys; insert_ops (xs @ [x]); rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins (xs @ [x]) = interp_rga ys
[PROOF STEP]
have "interp_ins (xs @ [x]) = interp_rga (pre @ suf @ [x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interp_ins (xs @ [x]) = interp_rga (pre @ suf @ [x])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. interp_ins (xs @ [x]) = interp_rga (pre @ suf @ [x])
[PROOF STEP]
have "set (xs @ [x]) = set (pre @ suf @ [x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (xs @ [x]) = set (pre @ suf @ [x])
[PROOF STEP]
using snoc.prems(1) ys_split
[PROOF STATE]
proof (prove)
using this:
set (xs @ [x]) = set ys
ys = pre @ [x] @ suf

goal (1 subgoal):
 1. set (xs @ [x]) = set (pre @ suf @ [x])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (xs @ [x]) = set (pre @ suf @ [x])

goal (1 subgoal):
 1. interp_ins (xs @ [x]) = interp_rga (pre @ suf @ [x])
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
set (xs @ [x]) = set (pre @ suf @ [x])

goal (1 subgoal):
 1. interp_ins (xs @ [x]) = interp_rga (pre @ suf @ [x])
[PROOF STEP]
using IH snoc.prems(2) valid_rga final_insert append_assoc
[PROOF STATE]
proof (prove)
using this:
set (xs @ [x]) = set (pre @ suf @ [x])
interp_ins xs = interp_rga (pre @ suf)
insert_ops (xs @ [x])
rga_ops (pre @ suf @ [x])
\<lbrakk>set (?xs @ [?x]) = set (?ys @ [?x]); rga_ops (?xs @ [?x]); insert_ops (?ys @ [?x]); interp_rga ?xs = interp_ins ?ys\<rbrakk> \<Longrightarrow> interp_rga (?xs @ [?x]) = interp_ins (?ys @ [?x])
(?xs @ ?ys) @ ?zs = ?xs @ ?ys @ ?zs

goal (1 subgoal):
 1. interp_ins (xs @ [x]) = interp_rga (pre @ suf @ [x])
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
interp_ins (xs @ [x]) = interp_rga (pre @ suf @ [x])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
interp_ins (xs @ [x]) = interp_rga (pre @ suf @ [x])

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; insert_ops xs; rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins xs = interp_rga ys; set (xs @ [x]) = set ys; insert_ops (xs @ [x]); rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins (xs @ [x]) = interp_rga ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
interp_ins (xs @ [x]) = interp_rga (pre @ suf @ [x])

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; insert_ops xs; rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins xs = interp_rga ys; set (xs @ [x]) = set ys; insert_ops (xs @ [x]); rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins (xs @ [x]) = interp_rga ys
[PROOF STEP]
have "... = interp_rga (pre @ [x] @ suf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interp_rga (pre @ suf @ [x]) = interp_rga (pre @ [x] @ suf)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. interp_rga (pre @ suf @ [x]) = interp_rga (pre @ [x] @ suf)
[PROOF STEP]
obtain oid ref where x_pair: "x = (oid, ref)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>oid ref. x = (oid, ref) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x = (oid, ref)

goal (1 subgoal):
 1. interp_rga (pre @ suf @ [x]) = interp_rga (pre @ [x] @ suf)
[PROOF STEP]
have "\<And>op2 r. op2 \<in> snd ` set suf \<Longrightarrow> r \<in> set_option op2 \<Longrightarrow> r \<noteq> oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>op2 r. \<lbrakk>op2 \<in> snd ` set suf; r \<in> set_option op2\<rbrakk> \<Longrightarrow> r \<noteq> oid
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
set (xs @ [x]) = set ys
insert_ops (xs @ [x])
rga_ops ys

goal (1 subgoal):
 1. \<And>op2 r. \<lbrakk>op2 \<in> snd ` set suf; r \<in> set_option op2\<rbrakk> \<Longrightarrow> r \<noteq> oid
[PROOF STEP]
by (simp add: crdt_ops_independent_suf insert_ops_def rga_ops_def x_pair ys_split)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?op2.0 \<in> snd ` set suf; ?r \<in> set_option ?op2.0\<rbrakk> \<Longrightarrow> ?r \<noteq> oid

goal (1 subgoal):
 1. interp_rga (pre @ suf @ [x]) = interp_rga (pre @ [x] @ suf)
[PROOF STEP]
hence "\<And>i r. (i, Some r) \<in> set suf \<Longrightarrow> r \<noteq> oid"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?op2.0 \<in> snd ` set suf; ?r \<in> set_option ?op2.0\<rbrakk> \<Longrightarrow> ?r \<noteq> oid

goal (1 subgoal):
 1. \<And>i r. (i, Some r) \<in> set suf \<Longrightarrow> r \<noteq> oid
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(?i, Some ?r) \<in> set suf \<Longrightarrow> ?r \<noteq> oid

goal (1 subgoal):
 1. interp_rga (pre @ suf @ [x]) = interp_rga (pre @ [x] @ suf)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(?i, Some ?r) \<in> set suf \<Longrightarrow> ?r \<noteq> oid

goal (1 subgoal):
 1. interp_rga (pre @ suf @ [x]) = interp_rga (pre @ [x] @ suf)
[PROOF STEP]
have "\<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set suf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set suf
[PROOF STEP]
using crdt_ops_no_future_ref snoc.prems(3) x_pair ys_split
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>crdt_ops (?xs @ [(?oid, ?oper)] @ ?ys) ?deps; ?ref \<in> ?deps ?oper\<rbrakk> \<Longrightarrow> ?ref \<notin> fst ` set ?ys
rga_ops ys
x = (oid, ref)
ys = pre @ [x] @ suf

goal (1 subgoal):
 1. \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set suf
[PROOF STEP]
by (metis option.set_intros rga_ops_def)
[PROOF STATE]
proof (state)
this:
ref = Some ?r \<Longrightarrow> ?r \<notin> fst ` set suf

goal (1 subgoal):
 1. interp_rga (pre @ suf @ [x]) = interp_rga (pre @ [x] @ suf)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(?i, Some ?r) \<in> set suf \<Longrightarrow> ?r \<noteq> oid
ref = Some ?r \<Longrightarrow> ?r \<notin> fst ` set suf
[PROOF STEP]
show "interp_rga (pre @ suf @ [x]) = interp_rga (pre @ [x] @ suf)"
[PROOF STATE]
proof (prove)
using this:
(?i, Some ?r) \<in> set suf \<Longrightarrow> ?r \<noteq> oid
ref = Some ?r \<Longrightarrow> ?r \<notin> fst ` set suf

goal (1 subgoal):
 1. interp_rga (pre @ suf @ [x]) = interp_rga (pre @ [x] @ suf)
[PROOF STEP]
using interp_rga_reorder valid_rga x_pair
[PROOF STATE]
proof (prove)
using this:
(?i, Some ?r) \<in> set suf \<Longrightarrow> ?r \<noteq> oid
ref = Some ?r \<Longrightarrow> ?r \<notin> fst ` set suf
\<lbrakk>rga_ops (?pre @ ?suf @ [(?oid, ?ref)]); \<And>i r. (i, Some r) \<in> set ?suf \<Longrightarrow> r \<noteq> ?oid; \<And>r. ?ref = Some r \<Longrightarrow> r \<notin> fst ` set ?suf\<rbrakk> \<Longrightarrow> interp_rga (?pre @ (?oid, ?ref) # ?suf) = interp_rga (?pre @ ?suf @ [(?oid, ?ref)])
rga_ops (pre @ suf @ [x])
x = (oid, ref)

goal (1 subgoal):
 1. interp_rga (pre @ suf @ [x]) = interp_rga (pre @ [x] @ suf)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
interp_rga (pre @ suf @ [x]) = interp_rga (pre @ [x] @ suf)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
interp_rga (pre @ suf @ [x]) = interp_rga (pre @ [x] @ suf)

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; insert_ops xs; rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins xs = interp_rga ys; set (xs @ [x]) = set ys; insert_ops (xs @ [x]); rga_ops ys\<rbrakk> \<Longrightarrow> interp_ins (xs @ [x]) = interp_rga ys
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
interp_ins (xs @ [x]) = interp_rga (pre @ suf @ [x])
interp_rga (pre @ suf @ [x]) = interp_rga (pre @ [x] @ suf)
[PROOF STEP]
show "interp_ins (xs @ [x]) = interp_rga ys"
[PROOF STATE]
proof (prove)
using this:
interp_ins (xs @ [x]) = interp_rga (pre @ suf @ [x])
interp_rga (pre @ suf @ [x]) = interp_rga (pre @ [x] @ suf)

goal (1 subgoal):
 1. interp_ins (xs @ [x]) = interp_rga ys
[PROOF STEP]
by (simp add: ys_split)
[PROOF STATE]
proof (state)
this:
interp_ins (xs @ [x]) = interp_rga ys

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. \<exists>ys. set xs = set ys \<and> insert_ops ys
[PROOF STEP]
by (simp add: crdt_ops_spec_ops_exist insert_ops_def rga_ops_def)


[STATEMENT]
theorem rga_meets_spec:
  assumes "rga_ops xs"
  shows "\<exists>ys. set ys = set xs \<and> insert_ops ys \<and> interp_ins ys = interp_rga xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ys. set ys = set xs \<and> insert_ops ys \<and> interp_ins ys = interp_rga xs
[PROOF STEP]
using assms rga_spec_equal insert_ops_exist
[PROOF STATE]
proof (prove)
using this:
rga_ops xs
\<lbrakk>set ?xs = set ?ys; insert_ops ?xs; rga_ops ?ys\<rbrakk> \<Longrightarrow> interp_ins ?xs = interp_rga ?ys
rga_ops ?xs \<Longrightarrow> \<exists>ys. set ?xs = set ys \<and> insert_ops ys

goal (1 subgoal):
 1. \<exists>ys. set ys = set xs \<and> insert_ops ys \<and> interp_ins ys = interp_rga xs
[PROOF STEP]
by metis


[STATEMENT]
lemma FNTT_termination_aux [simp]: "length (filter P [0..<l]) < Suc l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter P [0..<l]) < Suc l
[PROOF STEP]
by (metis diff_zero le_imp_less_Suc length_filter_le length_upt)


[STATEMENT]
lemma NTT_gen_NTT_full_length:
  assumes "length numbers =n"
  shows "NTT_gen n numbers = NTT numbers"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NTT_gen n numbers = NTT numbers
[PROOF STEP]
unfolding NTT_gen_def ntt_gen_def NTT_def ntt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. \<Sum>j = 0..<length numbers. numbers ! j * \<omega> ^ (n div n * i * j)) [0..<length numbers] = map (\<lambda>i. \<Sum>j = 0..<n. numbers ! j * \<omega> ^ (i * j)) [0..<n]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length numbers = n

goal (1 subgoal):
 1. map (\<lambda>i. \<Sum>j = 0..<length numbers. numbers ! j * \<omega> ^ (n div n * i * j)) [0..<length numbers] = map (\<lambda>i. \<Sum>j = 0..<n. numbers ! j * \<omega> ^ (i * j)) [0..<n]
[PROOF STEP]
by simp


[STATEMENT]
lemma length_even_filter: "length [f i .  i <- (filter even [0..<l])] = l-l div 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map f (filter even [0..<l])) = l - l div 2
[PROOF STEP]
by(induction l) auto


[STATEMENT]
lemma length_odd_filter: "length [f i .  i <- (filter odd [0..<l])] = l div 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map f (filter odd [0..<l])) = l div 2
[PROOF STEP]
by(induction l) auto


[STATEMENT]
lemma map2_length: "length (map2 f xs ys) =  min (length xs) (length ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map2 f xs ys) = min (length xs) (length ys)
[PROOF STEP]
by (induction xs arbitrary: ys) auto


[STATEMENT]
lemma map2_index: "i < length xs \<Longrightarrow> i < length ys \<Longrightarrow> (map2 f xs ys) ! i = f (xs ! i) (ys ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length xs; i < length ys\<rbrakk> \<Longrightarrow> map2 f xs ys ! i = f (xs ! i) (ys ! i)
[PROOF STEP]
by (induction xs arbitrary: ys i) auto


[STATEMENT]
lemma filter_last_not: "\<not> P x \<Longrightarrow> filter P (xs@[x]) = filter P xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> P x \<Longrightarrow> filter P (xs @ [x]) = filter P xs
[PROOF STEP]
by simp


[STATEMENT]
lemma filter_even_map: "filter even [0..<2*(x::nat)] = map ((*) (2::nat)) [0..<x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter even [0..<2 * x] = map ((*) 2) [0..<x]
[PROOF STEP]
by(induction x) simp+


[STATEMENT]
lemma filter_even_nth: "2*j < l \<Longrightarrow> 2*x = l \<Longrightarrow> (filter even [0..<l] ! j) = (2*j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 * j < l; 2 * x = l\<rbrakk> \<Longrightarrow> filter even [0..<l] ! j = 2 * j
[PROOF STEP]
using filter_even_map[of x] nth_map[of j "filter even [0..<l]" "(*) 2"]
[PROOF STATE]
proof (prove)
using this:
filter even [0..<2 * x] = map ((*) 2) [0..<x]
j < length (filter even [0..<l]) \<Longrightarrow> map ((*) 2) (filter even [0..<l]) ! j = 2 * filter even [0..<l] ! j

goal (1 subgoal):
 1. \<lbrakk>2 * j < l; 2 * x = l\<rbrakk> \<Longrightarrow> filter even [0..<l] ! j = 2 * j
[PROOF STEP]
by auto


[STATEMENT]
lemma filter_odd_map: "filter odd [0..<2*(x::nat)] = map (\<lambda> y. (2::nat)*y +1) [0..<x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter odd [0..<2 * x] = map (\<lambda>y. 2 * y + 1) [0..<x]
[PROOF STEP]
by(induction x) simp+


[STATEMENT]
lemma filter_odd_nth: "2*j < l \<Longrightarrow> 2*x = l \<Longrightarrow> (filter odd [0..<l] ! j) = (2*j+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 * j < l; 2 * x = l\<rbrakk> \<Longrightarrow> filter odd [0..<l] ! j = 2 * j + 1
[PROOF STEP]
using filter_odd_map[of x] nth_map[of j "filter even [0..<l]" "(*) 2"]
[PROOF STATE]
proof (prove)
using this:
filter odd [0..<2 * x] = map (\<lambda>y. 2 * y + 1) [0..<x]
j < length (filter even [0..<l]) \<Longrightarrow> map ((*) 2) (filter even [0..<l]) ! j = 2 * filter even [0..<l] ! j

goal (1 subgoal):
 1. \<lbrakk>2 * j < l; 2 * x = l\<rbrakk> \<Longrightarrow> filter odd [0..<l] ! j = 2 * j + 1
[PROOF STEP]
by auto


[STATEMENT]
lemma n_min1_2: "n = 2  \<Longrightarrow> \<omega>  = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = 2 \<Longrightarrow> \<omega> = - 1
[PROOF STEP]
using omega_properties(1) omega_properties(2) power2_eq_1_iff
[PROOF STATE]
proof (prove)
using this:
\<omega> ^ n = 1
\<omega> \<noteq> 1
(?a\<^sup>2 = (1::?'a)) = (?a = (1::?'a) \<or> ?a = - (1::?'a))

goal (1 subgoal):
 1. n = 2 \<Longrightarrow> \<omega> = - 1
[PROOF STEP]
by blast


[STATEMENT]
lemma n_min1_gr2:
  assumes "n > 2"
  shows "\<omega>^(n div 2) = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega> ^ (n div 2) = - 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<omega> ^ (n div 2) = - 1
[PROOF STEP]
have "\<omega>^(n div 2) \<noteq> -1 \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega> ^ (n div 2) \<noteq> - 1 \<Longrightarrow> False
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<omega> ^ (n div 2) \<noteq> - 1 \<Longrightarrow> False
[PROOF STEP]
assume "\<omega>^(n div 2) \<noteq> -1"
[PROOF STATE]
proof (state)
this:
\<omega> ^ (n div 2) \<noteq> - 1

goal (1 subgoal):
 1. \<omega> ^ (n div 2) \<noteq> - 1 \<Longrightarrow> False
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
\<omega> ^ (n div 2) \<noteq> - 1

goal (1 subgoal):
 1. False
[PROOF STEP]
proof(cases "\<omega>^(n div 2) = 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<omega> ^ (n div 2) \<noteq> - 1; \<omega> ^ (n div 2) = 1\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<omega> ^ (n div 2) \<noteq> - 1; \<omega> ^ (n div 2) \<noteq> 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<omega> ^ (n div 2) = 1

goal (2 subgoals):
 1. \<lbrakk>\<omega> ^ (n div 2) \<noteq> - 1; \<omega> ^ (n div 2) = 1\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<omega> ^ (n div 2) \<noteq> - 1; \<omega> ^ (n div 2) \<noteq> 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<omega> ^ (n div 2) = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<omega> ^ (n div 2) = 1

goal (1 subgoal):
 1. False
[PROOF STEP]
using  omega_properties(3)
[PROOF STATE]
proof (prove)
using this:
\<omega> ^ (n div 2) = 1
\<forall>m. \<omega> ^ m = 1 \<and> m \<noteq> 0 \<longrightarrow> n \<le> m

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis Euclidean_Division.div_eq_0_iff div_less_dividend leD less_le_trans n_lst2 one_less_numeral_iff pos2 semiring_norm(76) zero_neq_numeral)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<lbrakk>\<omega> ^ (n div 2) \<noteq> - 1; \<omega> ^ (n div 2) \<noteq> 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<omega> ^ (n div 2) \<noteq> - 1; \<omega> ^ (n div 2) \<noteq> 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<omega> ^ (n div 2) \<noteq> 1

goal (1 subgoal):
 1. \<lbrakk>\<omega> ^ (n div 2) \<noteq> - 1; \<omega> ^ (n div 2) \<noteq> 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "(\<omega>^(n div 2)) ^ (2::nat) \<noteq> 1"
[PROOF STATE]
proof (prove)
using this:
\<omega> ^ (n div 2) \<noteq> 1

goal (1 subgoal):
 1. (\<omega> ^ (n div 2))\<^sup>2 \<noteq> 1
[PROOF STEP]
by (smt (verit, ccfv_threshold) n_two_pot One_nat_def \<open>\<omega> ^ (n div 2) \<noteq> - 1\<close> diff_zero leD n_lst2 not_less_eq omega_properties(1) one_less_numeral_iff one_power2 power2_eq_square power_mult power_one_right power_strict_increasing_iff semiring_norm(76) square_eq_iff two_powr_div two_powrs_div)
[PROOF STATE]
proof (state)
this:
(\<omega> ^ (n div 2))\<^sup>2 \<noteq> 1

goal (1 subgoal):
 1. \<lbrakk>\<omega> ^ (n div 2) \<noteq> - 1; \<omega> ^ (n div 2) \<noteq> 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<omega> ^ (n div 2))\<^sup>2 \<noteq> 1

goal (1 subgoal):
 1. \<lbrakk>\<omega> ^ (n div 2) \<noteq> - 1; \<omega> ^ (n div 2) \<noteq> 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "(n div 2) * 2  = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n div 2 * 2 = n
[PROOF STEP]
using n_two_pot n_lst2
[PROOF STATE]
proof (prove)
using this:
n = 2 ^ N
2 \<le> n

goal (1 subgoal):
 1. n div 2 * 2 = n
[PROOF STEP]
by (metis One_nat_def Suc_lessD assms div_by_Suc_0 one_less_numeral_iff power_0 power_one_right power_strict_increasing_iff semiring_norm(76) two_powrs_div)
[PROOF STATE]
proof (state)
this:
n div 2 * 2 = n

goal (1 subgoal):
 1. \<lbrakk>\<omega> ^ (n div 2) \<noteq> - 1; \<omega> ^ (n div 2) \<noteq> 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<omega> ^ (n div 2))\<^sup>2 \<noteq> 1
n div 2 * 2 = n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<omega> ^ (n div 2))\<^sup>2 \<noteq> 1
n div 2 * 2 = n

goal (1 subgoal):
 1. False
[PROOF STEP]
using omega_properties(1)
[PROOF STATE]
proof (prove)
using this:
(\<omega> ^ (n div 2))\<^sup>2 \<noteq> 1
n div 2 * 2 = n
\<omega> ^ n = 1

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis power_mult)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<omega> ^ (n div 2) \<noteq> - 1 \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<omega> ^ (n div 2) \<noteq> - 1 \<Longrightarrow> False

goal (1 subgoal):
 1. \<omega> ^ (n div 2) = - 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<omega> ^ (n div 2) \<noteq> - 1 \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<omega> ^ (n div 2) \<noteq> - 1 \<Longrightarrow> False

goal (1 subgoal):
 1. \<omega> ^ (n div 2) = - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<omega> ^ (n div 2) = - 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma div_exp_sub: "2^l  < n \<Longrightarrow> n div (2^l) = 2^(N-l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ l < n \<Longrightarrow> n div 2 ^ l = 2 ^ (N - l)
[PROOF STEP]
using n_two_pot
[PROOF STATE]
proof (prove)
using this:
n = 2 ^ N

goal (1 subgoal):
 1. 2 ^ l < n \<Longrightarrow> n div 2 ^ l = 2 ^ (N - l)
[PROOF STEP]
by (smt (z3) One_nat_def diff_is_0_eq diff_le_diff_pow div_if div_le_dividend eq_imp_le le_0_eq le_Suc_eq n_lst2 nat_less_le not_less_eq_eq numeral_2_eq_2 power_0 two_powr_div)


[STATEMENT]
lemma omega_div_exp_min1:
  assumes "2^(Suc l) \<le> n"
  shows "(\<omega> ^(n div 2^(Suc l)))^(2^l) = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<omega> ^ (n div 2 ^ Suc l)) ^ 2 ^ l = - 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<omega> ^ (n div 2 ^ Suc l)) ^ 2 ^ l = - 1
[PROOF STEP]
have "(\<omega> ^(n div 2^(Suc l)))^(2^l) = \<omega> ^((n div 2^(Suc l))*2^l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<omega> ^ (n div 2 ^ Suc l)) ^ 2 ^ l = \<omega> ^ (n div 2 ^ Suc l * 2 ^ l)
[PROOF STEP]
by (simp add: power_mult)
[PROOF STATE]
proof (state)
this:
(\<omega> ^ (n div 2 ^ Suc l)) ^ 2 ^ l = \<omega> ^ (n div 2 ^ Suc l * 2 ^ l)

goal (1 subgoal):
 1. (\<omega> ^ (n div 2 ^ Suc l)) ^ 2 ^ l = - 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<omega> ^ (n div 2 ^ Suc l)) ^ 2 ^ l = \<omega> ^ (n div 2 ^ Suc l * 2 ^ l)

goal (1 subgoal):
 1. (\<omega> ^ (n div 2 ^ Suc l)) ^ 2 ^ l = - 1
[PROOF STEP]
have "(n div 2^(Suc l)) = 2^(N - Suc l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n div 2 ^ Suc l = 2 ^ (N - Suc l)
[PROOF STEP]
using assms div_exp_sub
[PROOF STATE]
proof (prove)
using this:
2 ^ Suc l \<le> n
2 ^ ?l < n \<Longrightarrow> n div 2 ^ ?l = 2 ^ (N - ?l)

goal (1 subgoal):
 1. n div 2 ^ Suc l = 2 ^ (N - Suc l)
[PROOF STEP]
by (metis n_two_pot eq_imp_le le_neq_implies_less one_less_numeral_iff power_diff power_inject_exp semiring_norm(76) zero_neq_numeral)
[PROOF STATE]
proof (state)
this:
n div 2 ^ Suc l = 2 ^ (N - Suc l)

goal (1 subgoal):
 1. (\<omega> ^ (n div 2 ^ Suc l)) ^ 2 ^ l = - 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n div 2 ^ Suc l = 2 ^ (N - Suc l)

goal (1 subgoal):
 1. (\<omega> ^ (n div 2 ^ Suc l)) ^ 2 ^ l = - 1
[PROOF STEP]
have "N \<ge> Suc l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc l \<le> N
[PROOF STEP]
using assms n_two_pot
[PROOF STATE]
proof (prove)
using this:
2 ^ Suc l \<le> n
n = 2 ^ N

goal (1 subgoal):
 1. Suc l \<le> N
[PROOF STEP]
by (metis diff_is_0_eq diff_le_diff_pow gr0I leD le_refl)
[PROOF STATE]
proof (state)
this:
Suc l \<le> N

goal (1 subgoal):
 1. (\<omega> ^ (n div 2 ^ Suc l)) ^ 2 ^ l = - 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Suc l \<le> N

goal (1 subgoal):
 1. (\<omega> ^ (n div 2 ^ Suc l)) ^ 2 ^ l = - 1
[PROOF STEP]
hence "(2::nat)^(N - Suc l)*2^l = 2^(N- 1)"
[PROOF STATE]
proof (prove)
using this:
Suc l \<le> N

goal (1 subgoal):
 1. 2 ^ (N - Suc l) * 2 ^ l = 2 ^ (N - 1)
[PROOF STEP]
by (metis Nat.add_diff_assoc diff_Suc_1 diff_diff_cancel diff_le_self le_add1 le_add_diff_inverse plus_1_eq_Suc power_add)
[PROOF STATE]
proof (state)
this:
2 ^ (N - Suc l) * 2 ^ l = 2 ^ (N - 1)

goal (1 subgoal):
 1. (\<omega> ^ (n div 2 ^ Suc l)) ^ 2 ^ l = - 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<omega> ^ (n div 2 ^ Suc l)) ^ 2 ^ l = \<omega> ^ (n div 2 ^ Suc l * 2 ^ l)
n div 2 ^ Suc l = 2 ^ (N - Suc l)
Suc l \<le> N
2 ^ (N - Suc l) * 2 ^ l = 2 ^ (N - 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<omega> ^ (n div 2 ^ Suc l)) ^ 2 ^ l = \<omega> ^ (n div 2 ^ Suc l * 2 ^ l)
n div 2 ^ Suc l = 2 ^ (N - Suc l)
Suc l \<le> N
2 ^ (N - Suc l) * 2 ^ l = 2 ^ (N - 1)

goal (1 subgoal):
 1. (\<omega> ^ (n div 2 ^ Suc l)) ^ 2 ^ l = - 1
[PROOF STEP]
by (metis n_two_pot One_nat_def \<open>n div 2 ^ Suc l = 2 ^ (N - Suc l)\<close> diff_Suc_1 div_exp_sub n_lst2 n_min1_2 n_min1_gr2 nat_less_le nat_power_eq_Suc_0_iff one_less_numeral_iff power_inject_exp power_one_right semiring_norm(76))
[PROOF STATE]
proof (state)
this:
(\<omega> ^ (n div 2 ^ Suc l)) ^ 2 ^ l = - 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma omg_n_2_min1:  "\<omega>^(n div 2) = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega> ^ (n div 2) = - 1
[PROOF STEP]
by (metis n_lst2 n_min1_2 n_min1_gr2 nat_less_le numeral_Bit0_div_2 numerals(1) power_one_right)


[STATEMENT]
lemma neg_cong: "-(x::('a mod_ring)) = - y \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - x = - y \<Longrightarrow> x = y
[PROOF STEP]
by simp