[STATEMENT]
lemma splitTree_invpres:
  assumes inv: "ft_invar (s:: ('e,'a::monoid_add) FingerTreeStruc)"
  assumes init_ff: "\<not> p i"
  assumes sum_tt: "p (i + annot s)"
  assumes fmt: "(splitTree p i s) = (l, (e,a), r)"
  shows "ft_invar l" and "ft_invar r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ft_invar l &&& ft_invar r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ft_invar l
 2. ft_invar r
[PROOF STEP]
obtain l1 nd r1 where
    l1_nd_r1: "nsplitTree p i s = (l1, nd, r1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l1 nd r1. nsplitTree p i s = (l1, nd, r1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "nsplitTree p i s", blast)
[PROOF STATE]
proof (state)
this:
nsplitTree p i s = (l1, nd, r1)

goal (2 subgoals):
 1. ft_invar l
 2. ft_invar r
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
ft_invar s
\<not> p i
p (i + annot s)
splitTree p i s = (l, (e, a), r)
nsplitTree p i s = (l1, nd, r1)
[PROOF STEP]
have
    l0: "l = l1"
    "(e,a) = n_unwrap nd"
    "r = r1"
[PROOF STATE]
proof (prove)
using this:
ft_invar s
\<not> p i
p (i + annot s)
splitTree p i s = (l, (e, a), r)
nsplitTree p i s = (l1, nd, r1)

goal (1 subgoal):
 1. l = l1 &&& (e, a) = n_unwrap nd &&& r = r1
[PROOF STEP]
by (auto simp add: splitTree_def)
[PROOF STATE]
proof (state)
this:
l = l1
(e, a) = n_unwrap nd
r = r1

goal (2 subgoals):
 1. ft_invar l
 2. ft_invar r
[PROOF STEP]
note nsp = nsplitTree_invpres[of 0 s p i l1 nd r1]
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_leveln_ftree 0 s; is_measured_ftree s; \<not> p i; p (i + gmft s); nsplitTree p i s = (l1, nd, r1)\<rbrakk> \<Longrightarrow> is_leveln_ftree 0 l1 \<and> is_measured_ftree l1 \<and> is_leveln_ftree 0 r1 \<and> is_measured_ftree r1 \<and> is_leveln_node 0 nd \<and> is_measured_node nd

goal (2 subgoals):
 1. ft_invar l
 2. ft_invar r
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
ft_invar s
\<not> p i
p (i + annot s)
splitTree p i s = (l, (e, a), r)
[PROOF STEP]
have "p (i + gmft s)"
[PROOF STATE]
proof (prove)
using this:
ft_invar s
\<not> p i
p (i + annot s)
splitTree p i s = (l, (e, a), r)

goal (1 subgoal):
 1. p (i + gmft s)
[PROOF STEP]
by (simp add:  ft_invar_def annot_def)
[PROOF STATE]
proof (state)
this:
p (i + gmft s)

goal (2 subgoals):
 1. ft_invar l
 2. ft_invar r
[PROOF STEP]
with assms l1_nd_r1 l0
[PROOF STATE]
proof (chain)
picking this:
ft_invar s
\<not> p i
p (i + annot s)
splitTree p i s = (l, (e, a), r)
nsplitTree p i s = (l1, nd, r1)
l = l1
(e, a) = n_unwrap nd
r = r1
p (i + gmft s)
[PROOF STEP]
have
    v1:
    "is_leveln_ftree 0 l \<and> is_measured_ftree l"
    "is_leveln_ftree 0 r \<and> is_measured_ftree r"
    "is_leveln_node 0 nd  \<and> is_measured_node nd"
[PROOF STATE]
proof (prove)
using this:
ft_invar s
\<not> p i
p (i + annot s)
splitTree p i s = (l, (e, a), r)
nsplitTree p i s = (l1, nd, r1)
l = l1
(e, a) = n_unwrap nd
r = r1
p (i + gmft s)

goal (1 subgoal):
 1. is_leveln_ftree 0 l \<and> is_measured_ftree l &&& is_leveln_ftree 0 r \<and> is_measured_ftree r &&& is_leveln_node 0 nd \<and> is_measured_node nd
[PROOF STEP]
by (auto simp add: nsp ft_invar_def)
[PROOF STATE]
proof (state)
this:
is_leveln_ftree 0 l \<and> is_measured_ftree l
is_leveln_ftree 0 r \<and> is_measured_ftree r
is_leveln_node 0 nd \<and> is_measured_node nd

goal (2 subgoals):
 1. ft_invar l
 2. ft_invar r
[PROOF STEP]
thus "ft_invar l" and "ft_invar r"
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree 0 l \<and> is_measured_ftree l
is_leveln_ftree 0 r \<and> is_measured_ftree r
is_leveln_node 0 nd \<and> is_measured_node nd

goal (1 subgoal):
 1. ft_invar l &&& ft_invar r
[PROOF STEP]
by (simp_all add: ft_invar_def annot_def)
[PROOF STATE]
proof (state)
this:
ft_invar l
ft_invar r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma splitTree_correct:
  assumes inv: "ft_invar (s:: ('e,'a::monoid_add) FingerTreeStruc)"
  assumes mono: "\<forall>a b. p a \<longrightarrow> p (a + b)"
  assumes init_ff: "\<not> p i"
  assumes sum_tt: "p (i + annot s)"
  assumes fmt: "(splitTree p i s) = (l, (e,a), r)"
  shows "(toList s) = (toList l) @ (e,a) # (toList r)"
  and   "\<not> p (i + annot l)"
  and   "p (i + annot l + a)"
  and   "ft_invar l" and "ft_invar r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (toList s = toList l @ (e, a) # toList r &&& \<not> p (i + annot l)) &&& p (i + annot l + a) &&& ft_invar l &&& ft_invar r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. toList s = toList l @ (e, a) # toList r
 2. \<not> p (i + annot l)
 3. p (i + annot l + a)
 4. ft_invar l
 5. ft_invar r
[PROOF STEP]
obtain l1 nd r1 where
    l1_nd_r1: "nsplitTree p i s = (l1, nd, r1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l1 nd r1. nsplitTree p i s = (l1, nd, r1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "nsplitTree p i s", blast)
[PROOF STATE]
proof (state)
this:
nsplitTree p i s = (l1, nd, r1)

goal (5 subgoals):
 1. toList s = toList l @ (e, a) # toList r
 2. \<not> p (i + annot l)
 3. p (i + annot l + a)
 4. ft_invar l
 5. ft_invar r
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
ft_invar s
\<forall>a b. p a \<longrightarrow> p (a + b)
\<not> p i
p (i + annot s)
splitTree p i s = (l, (e, a), r)
nsplitTree p i s = (l1, nd, r1)
[PROOF STEP]
have
    l0: "l = l1"
    "(e,a) = n_unwrap nd"
    "r = r1"
[PROOF STATE]
proof (prove)
using this:
ft_invar s
\<forall>a b. p a \<longrightarrow> p (a + b)
\<not> p i
p (i + annot s)
splitTree p i s = (l, (e, a), r)
nsplitTree p i s = (l1, nd, r1)

goal (1 subgoal):
 1. l = l1 &&& (e, a) = n_unwrap nd &&& r = r1
[PROOF STEP]
by (auto simp add: splitTree_def)
[PROOF STATE]
proof (state)
this:
l = l1
(e, a) = n_unwrap nd
r = r1

goal (5 subgoals):
 1. toList s = toList l @ (e, a) # toList r
 2. \<not> p (i + annot l)
 3. p (i + annot l + a)
 4. ft_invar l
 5. ft_invar r
[PROOF STEP]
note nsp = nsplitTree_correct[of 0 s p i l1 nd r1]
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_leveln_ftree 0 s; is_measured_ftree s; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft s); nsplitTree p i s = (l1, nd, r1)\<rbrakk> \<Longrightarrow> toList s = toList l1 @ nodeToList nd @ toList r1 \<and> \<not> p (i + gmft l1) \<and> p (i + gmft l1 + gmn nd) \<and> is_leveln_ftree 0 l1 \<and> is_measured_ftree l1 \<and> is_leveln_ftree 0 r1 \<and> is_measured_ftree r1 \<and> is_leveln_node 0 nd \<and> is_measured_node nd

goal (5 subgoals):
 1. toList s = toList l @ (e, a) # toList r
 2. \<not> p (i + annot l)
 3. p (i + annot l + a)
 4. ft_invar l
 5. ft_invar r
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
ft_invar s
\<forall>a b. p a \<longrightarrow> p (a + b)
\<not> p i
p (i + annot s)
splitTree p i s = (l, (e, a), r)
[PROOF STEP]
have "p (i + gmft s)"
[PROOF STATE]
proof (prove)
using this:
ft_invar s
\<forall>a b. p a \<longrightarrow> p (a + b)
\<not> p i
p (i + annot s)
splitTree p i s = (l, (e, a), r)

goal (1 subgoal):
 1. p (i + gmft s)
[PROOF STEP]
by (simp add:  ft_invar_def annot_def)
[PROOF STATE]
proof (state)
this:
p (i + gmft s)

goal (5 subgoals):
 1. toList s = toList l @ (e, a) # toList r
 2. \<not> p (i + annot l)
 3. p (i + annot l + a)
 4. ft_invar l
 5. ft_invar r
[PROOF STEP]
with assms l1_nd_r1 l0
[PROOF STATE]
proof (chain)
picking this:
ft_invar s
\<forall>a b. p a \<longrightarrow> p (a + b)
\<not> p i
p (i + annot s)
splitTree p i s = (l, (e, a), r)
nsplitTree p i s = (l1, nd, r1)
l = l1
(e, a) = n_unwrap nd
r = r1
p (i + gmft s)
[PROOF STEP]
have
    v1:
    "(toList s) = (toList l) @ (nodeToList nd) @ (toList r)"
    "\<not> p (i + (gmft l))"
    "p (i + (gmft l) + (gmn nd))"
    "is_leveln_ftree 0 l \<and> is_measured_ftree l"
    "is_leveln_ftree 0 r \<and> is_measured_ftree r"
    "is_leveln_node 0 nd  \<and> is_measured_node nd"
[PROOF STATE]
proof (prove)
using this:
ft_invar s
\<forall>a b. p a \<longrightarrow> p (a + b)
\<not> p i
p (i + annot s)
splitTree p i s = (l, (e, a), r)
nsplitTree p i s = (l1, nd, r1)
l = l1
(e, a) = n_unwrap nd
r = r1
p (i + gmft s)

goal (1 subgoal):
 1. (toList s = toList l @ nodeToList nd @ toList r &&& \<not> p (i + gmft l) &&& p (i + gmft l + gmn nd)) &&& is_leveln_ftree 0 l \<and> is_measured_ftree l &&& is_leveln_ftree 0 r \<and> is_measured_ftree r &&& is_leveln_node 0 nd \<and> is_measured_node nd
[PROOF STEP]
by (auto simp add: nsp ft_invar_def)
[PROOF STATE]
proof (state)
this:
toList s = toList l @ nodeToList nd @ toList r
\<not> p (i + gmft l)
p (i + gmft l + gmn nd)
is_leveln_ftree 0 l \<and> is_measured_ftree l
is_leveln_ftree 0 r \<and> is_measured_ftree r
is_leveln_node 0 nd \<and> is_measured_node nd

goal (5 subgoals):
 1. toList s = toList l @ (e, a) # toList r
 2. \<not> p (i + annot l)
 3. p (i + annot l + a)
 4. ft_invar l
 5. ft_invar r
[PROOF STEP]
from v1(6) l0(2)
[PROOF STATE]
proof (chain)
picking this:
is_leveln_node 0 nd \<and> is_measured_node nd
(e, a) = n_unwrap nd
[PROOF STEP]
have
    ndea: "nd = Tip e a"
[PROOF STATE]
proof (prove)
using this:
is_leveln_node 0 nd \<and> is_measured_node nd
(e, a) = n_unwrap nd

goal (1 subgoal):
 1. nd = Tip e a
[PROOF STEP]
by (cases nd)  auto
[PROOF STATE]
proof (state)
this:
nd = Tip e a

goal (5 subgoals):
 1. toList s = toList l @ (e, a) # toList r
 2. \<not> p (i + annot l)
 3. p (i + annot l + a)
 4. ft_invar l
 5. ft_invar r
[PROOF STEP]
hence nd_list_inv: "nodeToList nd = [(e,a)]"
    "gmn nd = a"
[PROOF STATE]
proof (prove)
using this:
nd = Tip e a

goal (1 subgoal):
 1. nodeToList nd = [(e, a)] &&& gmn nd = a
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
nodeToList nd = [(e, a)]
gmn nd = a

goal (5 subgoals):
 1. toList s = toList l @ (e, a) # toList r
 2. \<not> p (i + annot l)
 3. p (i + annot l + a)
 4. ft_invar l
 5. ft_invar r
[PROOF STEP]
with v1
[PROOF STATE]
proof (chain)
picking this:
toList s = toList l @ nodeToList nd @ toList r
\<not> p (i + gmft l)
p (i + gmft l + gmn nd)
is_leveln_ftree 0 l \<and> is_measured_ftree l
is_leveln_ftree 0 r \<and> is_measured_ftree r
is_leveln_node 0 nd \<and> is_measured_node nd
nodeToList nd = [(e, a)]
gmn nd = a
[PROOF STEP]
show  "(toList s) = (toList l) @ (e,a) # (toList r)"
    and   "\<not> p (i + annot l)"
    and   "p (i + annot l + a)"
    and   "ft_invar l" and "ft_invar r"
[PROOF STATE]
proof (prove)
using this:
toList s = toList l @ nodeToList nd @ toList r
\<not> p (i + gmft l)
p (i + gmft l + gmn nd)
is_leveln_ftree 0 l \<and> is_measured_ftree l
is_leveln_ftree 0 r \<and> is_measured_ftree r
is_leveln_node 0 nd \<and> is_measured_node nd
nodeToList nd = [(e, a)]
gmn nd = a

goal (1 subgoal):
 1. (toList s = toList l @ (e, a) # toList r &&& \<not> p (i + annot l)) &&& p (i + annot l + a) &&& ft_invar l &&& ft_invar r
[PROOF STEP]
by (simp_all add: ft_invar_def annot_def)
[PROOF STATE]
proof (state)
this:
toList s = toList l @ (e, a) # toList r
\<not> p (i + annot l)
p (i + annot l + a)
ft_invar l
ft_invar r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma splitTree_correctE:
  assumes inv: "ft_invar (s:: ('e,'a::monoid_add) FingerTreeStruc)"
  assumes mono: "\<forall>a b. p a \<longrightarrow> p (a + b)"
  assumes init_ff: "\<not> p i"
  assumes sum_tt: "p (i + annot s)"
  obtains l e a r where
    "(splitTree p i s) = (l, (e,a), r)" and
    "(toList s) = (toList l) @ (e,a) # (toList r)" and
    "\<not> p (i + annot l)" and
    "p (i + annot l + a)" and
    "ft_invar l" and "ft_invar r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l e a r. \<lbrakk>splitTree p i s = (l, (e, a), r); toList s = toList l @ (e, a) # toList r; \<not> p (i + annot l); p (i + annot l + a); ft_invar l; ft_invar r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>l e a r. \<lbrakk>splitTree p i s = (l, (e, a), r); toList s = toList l @ (e, a) # toList r; \<not> p (i + annot l); p (i + annot l + a); ft_invar l; ft_invar r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain l e a r where fmt: "(splitTree p i s) = (l, (e,a), r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l e a r. splitTree p i s = (l, (e, a), r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "(splitTree p i s)") auto
[PROOF STATE]
proof (state)
this:
splitTree p i s = (l, (e, a), r)

goal (1 subgoal):
 1. (\<And>l e a r. \<lbrakk>splitTree p i s = (l, (e, a), r); toList s = toList l @ (e, a) # toList r; \<not> p (i + annot l); p (i + annot l + a); ft_invar l; ft_invar r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from splitTree_correct[of s p, OF assms fmt] fmt
[PROOF STATE]
proof (chain)
picking this:
toList s = toList l @ (e, a) # toList r
\<not> p (i + annot l)
p (i + annot l + a)
ft_invar l
ft_invar r
splitTree p i s = (l, (e, a), r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
toList s = toList l @ (e, a) # toList r
\<not> p (i + annot l)
p (i + annot l + a)
ft_invar l
ft_invar r
splitTree p i s = (l, (e, a), r)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (blast intro: that)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma foldl_node_correct:
  "foldl_node f \<sigma> nd = List.foldl f \<sigma> (nodeToList nd)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl_node f \<sigma> nd = foldl f \<sigma> (nodeToList nd)
[PROOF STEP]
by (induct nd arbitrary: "\<sigma>") (auto simp add: nodeToList_def)


[STATEMENT]
lemma foldl_digit_correct:
  "foldl_digit f \<sigma> d = List.foldl f \<sigma> (digitToList d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl_digit f \<sigma> d = foldl f \<sigma> (digitToList d)
[PROOF STEP]
by (induct d arbitrary: "\<sigma>") (auto
    simp add: digitToList_def foldl_node_correct)


[STATEMENT]
lemma foldr_node_correct:
  "foldr_node f nd \<sigma> = List.foldr f (nodeToList nd) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldr_node f nd \<sigma> = foldr f (nodeToList nd) \<sigma>
[PROOF STEP]
by (induct nd arbitrary: "\<sigma>") (auto simp add: nodeToList_def)


[STATEMENT]
lemma foldr_digit_correct:
  "foldr_digit f d \<sigma> = List.foldr f (digitToList d) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldr_digit f d \<sigma> = foldr f (digitToList d) \<sigma>
[PROOF STEP]
by (induct d arbitrary: "\<sigma>") (auto
    simp add: digitToList_def foldr_node_correct)


[STATEMENT]
lemma foldl_correct:
  "foldl f \<sigma> t = List.foldl f \<sigma> (toList t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.foldl f \<sigma> t = List.foldl f \<sigma> (toList t)
[PROOF STEP]
by (induct t arbitrary: "\<sigma>") (auto
    simp add: toList_def foldl_node_correct foldl_digit_correct)


[STATEMENT]
lemma foldr_correct:
  "foldr f t \<sigma> = List.foldr f (toList t) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.foldr f t \<sigma> = List.foldr f (toList t) \<sigma>
[PROOF STEP]
by (induct t arbitrary: "\<sigma>") (auto
    simp add: toList_def foldr_node_correct foldr_digit_correct)


[STATEMENT]
lemma count_node_correct:
  "count_node n = length (nodeToList n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_node n = length (nodeToList n)
[PROOF STEP]
by (induct n,auto simp add: nodeToList_def count_node_def)


[STATEMENT]
lemma count_digit_correct:
  "count_digit d = length (digitToList d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_digit d = length (digitToList d)
[PROOF STEP]
by (cases d, auto simp add: digitToList_def count_digit_def count_node_correct)


[STATEMENT]
lemma count_correct[simp]:
  "count t = length (toList t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count t = length (toList t)
[PROOF STEP]
by (induct t,
    auto simp add: toList_def count_def
                   count_digit_correct count_node_correct)


[STATEMENT]
lemma Rep_FingerTree_invar[simp]: "FingerTreeStruc.ft_invar (Rep_FingerTree t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FingerTreeStruc.ft_invar (Rep_FingerTree t)
[PROOF STEP]
using Rep_FingerTree
[PROOF STATE]
proof (prove)
using this:
Rep_FingerTree ?x \<in> {t. FingerTreeStruc.ft_invar t}

goal (1 subgoal):
 1. FingerTreeStruc.ft_invar (Rep_FingerTree t)
[PROOF STEP]
by simp


[STATEMENT]
lemma [simp]:
  "FingerTreeStruc.ft_invar t \<Longrightarrow> Rep_FingerTree (Abs_FingerTree t) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FingerTreeStruc.ft_invar t \<Longrightarrow> Rep_FingerTree (Abs_FingerTree t) = t
[PROOF STEP]
using Abs_FingerTree_inverse
[PROOF STATE]
proof (prove)
using this:
?y \<in> {t. FingerTreeStruc.ft_invar t} \<Longrightarrow> Rep_FingerTree (Abs_FingerTree ?y) = ?y

goal (1 subgoal):
 1. FingerTreeStruc.ft_invar t \<Longrightarrow> Rep_FingerTree (Abs_FingerTree t) = t
[PROOF STEP]
by simp


[STATEMENT]
lemma [simp, code abstype]: "Abs_FingerTree (Rep_FingerTree t) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_FingerTree (Rep_FingerTree t) = t
[PROOF STEP]
by (rule Rep_FingerTree_inverse)


[STATEMENT]
lemma [simp, code abstype]: "Abs_viewres (Rep_viewres x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_viewres (Rep_viewres x) = x
[PROOF STEP]
by (rule Rep_viewres_inverse)


[STATEMENT]
lemma Abs_viewres_inverse_Some:
  "FingerTreeStruc.ft_invar t \<Longrightarrow>
    Rep_viewres (Abs_viewres (Some (a,t))) = Some (a,t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FingerTreeStruc.ft_invar t \<Longrightarrow> Rep_viewres (Abs_viewres (Some (a, t))) = Some (a, t)
[PROOF STEP]
by (auto simp add: Abs_viewres_inverse)


[STATEMENT]
lemma [code abstract]: "Rep_FingerTree (extract_viewres_t r) =
    (case (Rep_viewres r) of None \<Rightarrow> Empty | Some (a,t) \<Rightarrow> t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_FingerTree (extract_viewres_t r) = (case Rep_viewres r of None \<Rightarrow> Empty | Some (a, t) \<Rightarrow> t)
[PROOF STEP]
apply (cases r)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>r = Abs_viewres y; y \<in> {r. case r of None \<Rightarrow> True | Some (a, t) \<Rightarrow> FingerTreeStruc.ft_invar t}\<rbrakk> \<Longrightarrow> Rep_FingerTree (extract_viewres_t r) = (case Rep_viewres r of None \<Rightarrow> Empty | Some (a, t) \<Rightarrow> t)
[PROOF STEP]
apply (auto split: option.split option.split_asm
             simp add: extract_viewres_t_def Abs_viewres_inverse_Some)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [simp, code abstype]: "Abs_splitres (Rep_splitres x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_splitres (Rep_splitres x) = x
[PROOF STEP]
by (rule Rep_splitres_inverse)


[STATEMENT]
lemma Abs_splitres_inverse:
  "FingerTreeStruc.ft_invar r \<Longrightarrow> FingerTreeStruc.ft_invar s \<Longrightarrow>
      Rep_splitres (Abs_splitres ((r,a,s))) = (r,a,s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>FingerTreeStruc.ft_invar r; FingerTreeStruc.ft_invar s\<rbrakk> \<Longrightarrow> Rep_splitres (Abs_splitres (r, a, s)) = (r, a, s)
[PROOF STEP]
by (auto simp add: Abs_splitres_inverse)


[STATEMENT]
lemma [code abstract]: "Rep_FingerTree (extract_splitres_l r) = (case
    (Rep_splitres r) of (l,a,r) \<Rightarrow> l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_FingerTree (extract_splitres_l r) = (case Rep_splitres r of (l, a, r) \<Rightarrow> l)
[PROOF STEP]
apply (cases r)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>r = Abs_splitres y; y \<in> {(l, a, r) |l a r. FingerTreeStruc.ft_invar l \<and> FingerTreeStruc.ft_invar r}\<rbrakk> \<Longrightarrow> Rep_FingerTree (extract_splitres_l r) = (case Rep_splitres r of (l, a, r) \<Rightarrow> l)
[PROOF STEP]
apply (auto split: option.split option.split_asm
    simp add: extract_splitres_l_def Abs_splitres_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [code abstract]: "Rep_FingerTree (extract_splitres_r r) = (case
  (Rep_splitres r) of (l,a,r) \<Rightarrow> r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_FingerTree (extract_splitres_r r) = (case Rep_splitres r of (l, a, r) \<Rightarrow> r)
[PROOF STEP]
apply (cases r)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>r = Abs_splitres y; y \<in> {(l, a, r) |l a r. FingerTreeStruc.ft_invar l \<and> FingerTreeStruc.ft_invar r}\<rbrakk> \<Longrightarrow> Rep_FingerTree (extract_splitres_r r) = (case Rep_splitres r of (l, a, r) \<Rightarrow> r)
[PROOF STEP]
apply (auto split: option.split option.split_asm
    simp add: extract_splitres_r_def Abs_splitres_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [code abstract]: "Rep_FingerTree empty = FingerTreeStruc.Empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_FingerTree local.empty = Empty
[PROOF STEP]
by (simp add: empty_def)


[STATEMENT]
lemma empty_rep: "t=empty \<longleftrightarrow> Rep_FingerTree t = Empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t = local.empty) = (Rep_FingerTree t = Empty)
[PROOF STEP]
apply (auto simp add: empty_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_FingerTree t = Empty \<Longrightarrow> t = Abs_FingerTree Empty
[PROOF STEP]
apply (metis Rep_FingerTree_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [code abstract]: "Rep_FingerTree (toTree t) = FingerTreeStruc.toTree t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_FingerTree (toTree t) = FingerTreeStruc.toTree t
[PROOF STEP]
by (simp add: toTree_def)


[STATEMENT]
lemma [code abstract]:
    "Rep_FingerTree (lcons a t) = (FingerTreeStruc.lcons a (Rep_FingerTree t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_FingerTree (lcons a t) = FingerTreeStruc.lcons a (Rep_FingerTree t)
[PROOF STEP]
by (simp add: lcons_def FingerTreeStruc.lcons_correct)


[STATEMENT]
lemma [code abstract]:
    "Rep_FingerTree (rcons t a) = (FingerTreeStruc.rcons (Rep_FingerTree t) a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_FingerTree (rcons t a) = FingerTreeStruc.rcons (Rep_FingerTree t) a
[PROOF STEP]
by (simp add: rcons_def FingerTreeStruc.rcons_correct)


[STATEMENT]
lemma [code abstract]:
    "Rep_viewres (viewL_aux t) = (FingerTreeStruc.viewL (Rep_FingerTree t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_viewres (viewL_aux t) = FingerTreeStruc.viewL (Rep_FingerTree t)
[PROOF STEP]
apply (cases "(FingerTreeStruc.viewL (Rep_FingerTree t))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. FingerTreeStruc.viewL (Rep_FingerTree t) = None \<Longrightarrow> Rep_viewres (viewL_aux t) = FingerTreeStruc.viewL (Rep_FingerTree t)
 2. \<And>a. FingerTreeStruc.viewL (Rep_FingerTree t) = Some a \<Longrightarrow> Rep_viewres (viewL_aux t) = FingerTreeStruc.viewL (Rep_FingerTree t)
[PROOF STEP]
apply (auto simp add: viewL_aux_def )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. FingerTreeStruc.viewL (Rep_FingerTree t) = Some ((a, b), ba) \<Longrightarrow> Rep_viewres (Abs_viewres (Some ((a, b), ba))) = Some ((a, b), ba)
[PROOF STEP]
apply (cases "Rep_FingerTree t = Empty")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. \<lbrakk>FingerTreeStruc.viewL (Rep_FingerTree t) = Some ((a, b), ba); Rep_FingerTree t = Empty\<rbrakk> \<Longrightarrow> Rep_viewres (Abs_viewres (Some ((a, b), ba))) = Some ((a, b), ba)
 2. \<And>a b ba. \<lbrakk>FingerTreeStruc.viewL (Rep_FingerTree t) = Some ((a, b), ba); Rep_FingerTree t \<noteq> Empty\<rbrakk> \<Longrightarrow> Rep_viewres (Abs_viewres (Some ((a, b), ba))) = Some ((a, b), ba)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>FingerTreeStruc.viewL (Rep_FingerTree t) = Some ((a, b), ba); Rep_FingerTree t \<noteq> Empty\<rbrakk> \<Longrightarrow> Rep_viewres (Abs_viewres (Some ((a, b), ba))) = Some ((a, b), ba)
[PROOF STEP]
apply (auto
      elim!: FingerTreeStruc.viewL_correct_nonEmpty
                 [of "Rep_FingerTree t", simplified]
      simp add: Abs_viewres_inverse_Some)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [code abstract]:
    "Rep_viewres (viewR_aux t) = (FingerTreeStruc.viewR (Rep_FingerTree t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_viewres (viewR_aux t) = FingerTreeStruc.viewR (Rep_FingerTree t)
[PROOF STEP]
apply (cases "(FingerTreeStruc.viewR (Rep_FingerTree t))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. FingerTreeStruc.viewR (Rep_FingerTree t) = None \<Longrightarrow> Rep_viewres (viewR_aux t) = FingerTreeStruc.viewR (Rep_FingerTree t)
 2. \<And>a. FingerTreeStruc.viewR (Rep_FingerTree t) = Some a \<Longrightarrow> Rep_viewres (viewR_aux t) = FingerTreeStruc.viewR (Rep_FingerTree t)
[PROOF STEP]
apply (auto simp add: viewR_aux_def )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. FingerTreeStruc.viewR (Rep_FingerTree t) = Some ((a, b), ba) \<Longrightarrow> Rep_viewres (Abs_viewres (Some ((a, b), ba))) = Some ((a, b), ba)
[PROOF STEP]
apply (cases "Rep_FingerTree t = Empty")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. \<lbrakk>FingerTreeStruc.viewR (Rep_FingerTree t) = Some ((a, b), ba); Rep_FingerTree t = Empty\<rbrakk> \<Longrightarrow> Rep_viewres (Abs_viewres (Some ((a, b), ba))) = Some ((a, b), ba)
 2. \<And>a b ba. \<lbrakk>FingerTreeStruc.viewR (Rep_FingerTree t) = Some ((a, b), ba); Rep_FingerTree t \<noteq> Empty\<rbrakk> \<Longrightarrow> Rep_viewres (Abs_viewres (Some ((a, b), ba))) = Some ((a, b), ba)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>FingerTreeStruc.viewR (Rep_FingerTree t) = Some ((a, b), ba); Rep_FingerTree t \<noteq> Empty\<rbrakk> \<Longrightarrow> Rep_viewres (Abs_viewres (Some ((a, b), ba))) = Some ((a, b), ba)
[PROOF STEP]
apply (auto
      elim!: FingerTreeStruc.viewR_correct_nonEmpty
                [of "Rep_FingerTree t", simplified]
      simp add: Abs_viewres_inverse_Some)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [code abstract]: "Rep_FingerTree (tail t) =
    (if (FingerTreeStruc.isEmpty (Rep_FingerTree t)) then Empty
     else FingerTreeStruc.tail (Rep_FingerTree t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_FingerTree (tail t) = (if FingerTreeStruc.isEmpty (Rep_FingerTree t) then Empty else FingerTreeStruc.tail (Rep_FingerTree t))
[PROOF STEP]
apply (simp add: tail_def FingerTreeStruc.tail_correct FingerTreeStruc.isEmpty_def empty_rep)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_FingerTree t = Empty \<longrightarrow> Rep_FingerTree local.empty = Empty
[PROOF STEP]
apply (auto simp add: empty_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [code abstract]: "Rep_FingerTree (tailR t) =
    (if (FingerTreeStruc.isEmpty (Rep_FingerTree t)) then Empty
    else FingerTreeStruc.tailR (Rep_FingerTree t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_FingerTree (tailR t) = (if FingerTreeStruc.isEmpty (Rep_FingerTree t) then Empty else FingerTreeStruc.tailR (Rep_FingerTree t))
[PROOF STEP]
apply (simp add: tailR_def FingerTreeStruc.tailR_correct FingerTreeStruc.isEmpty_def empty_rep)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_FingerTree t = Empty \<longrightarrow> Rep_FingerTree local.empty = Empty
[PROOF STEP]
apply (simp add: empty_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [code abstract]:
    "Rep_FingerTree (app s t) =
      FingerTreeStruc.app (Rep_FingerTree s) (Rep_FingerTree t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_FingerTree (app s t) = FingerTreeStruc.app (Rep_FingerTree s) (Rep_FingerTree t)
[PROOF STEP]
by (simp add: app_def FingerTreeStruc.app_correct)


[STATEMENT]
lemma [code abstract]:
    "Rep_splitres (splitTree_aux p i t) = (if (\<not>p i \<and> p (i+annot t)) then
      (FingerTreeStruc.splitTree p i (Rep_FingerTree t))
    else
      (Empty,undefined,Empty))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_splitres (splitTree_aux p i t) = (if \<not> p i \<and> p (i + annot t) then FingerTreeStruc.splitTree p i (Rep_FingerTree t) else (Empty, undefined, Empty))
[PROOF STEP]
using FingerTreeStruc.splitTree_invpres[of "Rep_FingerTree t" p i]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>FingerTreeStruc.ft_invar (Rep_FingerTree t); \<not> p i; p (i + FingerTreeStruc.annot (Rep_FingerTree t)); FingerTreeStruc.splitTree p i (Rep_FingerTree t) = (?l, (?e, ?a), ?r)\<rbrakk> \<Longrightarrow> FingerTreeStruc.ft_invar ?l
\<lbrakk>FingerTreeStruc.ft_invar (Rep_FingerTree t); \<not> p i; p (i + FingerTreeStruc.annot (Rep_FingerTree t)); FingerTreeStruc.splitTree p i (Rep_FingerTree t) = (?l, (?e, ?a), ?r)\<rbrakk> \<Longrightarrow> FingerTreeStruc.ft_invar ?r

goal (1 subgoal):
 1. Rep_splitres (splitTree_aux p i t) = (if \<not> p i \<and> p (i + annot t) then FingerTreeStruc.splitTree p i (Rep_FingerTree t) else (Empty, undefined, Empty))
[PROOF STEP]
apply (auto simp add: splitTree_aux_def annot_def Abs_splitres_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>l e a r. FingerTreeStruc.splitTree p i (Rep_FingerTree t) = (l, (e, a), r) \<Longrightarrow> FingerTreeStruc.ft_invar l; \<And>l e a r. FingerTreeStruc.splitTree p i (Rep_FingerTree t) = (l, (e, a), r) \<Longrightarrow> FingerTreeStruc.ft_invar r; \<not> p i; p (i + FingerTreeStruc.annot (Rep_FingerTree t))\<rbrakk> \<Longrightarrow> Rep_splitres (Abs_splitres (FingerTreeStruc.splitTree p i (Rep_FingerTree t))) = FingerTreeStruc.splitTree p i (Rep_FingerTree t)
[PROOF STEP]
apply (cases "FingerTreeStruc.splitTree p i (Rep_FingerTree t)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>\<And>l e a r. FingerTreeStruc.splitTree p i (Rep_FingerTree t) = (l, (e, a), r) \<Longrightarrow> FingerTreeStruc.ft_invar l; \<And>l e a r. FingerTreeStruc.splitTree p i (Rep_FingerTree t) = (l, (e, a), r) \<Longrightarrow> FingerTreeStruc.ft_invar r; \<not> p i; p (i + FingerTreeStruc.annot (Rep_FingerTree t)); FingerTreeStruc.splitTree p i (Rep_FingerTree t) = (a, b, c)\<rbrakk> \<Longrightarrow> Rep_splitres (Abs_splitres (FingerTreeStruc.splitTree p i (Rep_FingerTree t))) = FingerTreeStruc.splitTree p i (Rep_FingerTree t)
[PROOF STEP]
apply (force simp add: Abs_FingerTree_inverse Abs_splitres_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma empty_correct: "toList t = [] \<longleftrightarrow> t=empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (toList t = []) = (t = local.empty)
[PROOF STEP]
apply (unfold toList_def empty_rep)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (FingerTreeStruc.toList (Rep_FingerTree t) = []) = (Rep_FingerTree t = Empty)
[PROOF STEP]
apply (simp add: FingerTreeStruc.toList_empty)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma toList_of_empty[simp]: "toList empty = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList local.empty = []
[PROOF STEP]
apply (unfold toList_def empty_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FingerTreeStruc.toList (Rep_FingerTree (Abs_FingerTree Empty)) = []
[PROOF STEP]
apply (auto simp add: FingerTreeStruc.toList_empty)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma annot_correct: "annot t = sum_list (map snd (toList t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. annot t = sum_list (map snd (toList t))
[PROOF STEP]
apply (unfold toList_def annot_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FingerTreeStruc.annot (Rep_FingerTree t) = sum_list (map snd (FingerTreeStruc.toList (Rep_FingerTree t)))
[PROOF STEP]
apply (simp add: FingerTreeStruc.annot_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma toTree_correct: "toList (toTree l) = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList (toTree l) = l
[PROOF STEP]
apply (unfold toList_def toTree_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FingerTreeStruc.toList (Rep_FingerTree (Abs_FingerTree (FingerTreeStruc.toTree l))) = l
[PROOF STEP]
apply (simp add: FingerTreeStruc.toTree_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma lcons_correct: "toList (lcons a t) = a#toList t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList (lcons a t) = a # toList t
[PROOF STEP]
apply (unfold toList_def lcons_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FingerTreeStruc.toList (Rep_FingerTree (Abs_FingerTree (FingerTreeStruc.lcons a (Rep_FingerTree t)))) = a # FingerTreeStruc.toList (Rep_FingerTree t)
[PROOF STEP]
apply (simp add: FingerTreeStruc.lcons_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rcons_correct: "toList (rcons t a) = toList t@[a]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList (rcons t a) = toList t @ [a]
[PROOF STEP]
apply (unfold toList_def rcons_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FingerTreeStruc.toList (Rep_FingerTree (Abs_FingerTree (FingerTreeStruc.rcons (Rep_FingerTree t) a))) = FingerTreeStruc.toList (Rep_FingerTree t) @ [a]
[PROOF STEP]
apply (simp add: FingerTreeStruc.rcons_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma viewL_correct:
    "t = empty \<Longrightarrow> viewL t = None"
    "t \<noteq> empty \<Longrightarrow> \<exists>a s. viewL t = Some (a,s) \<and> toList t = a#toList s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t = local.empty \<Longrightarrow> viewL t = None) &&& (t \<noteq> local.empty \<Longrightarrow> \<exists>a s. viewL t = Some (a, s) \<and> toList t = a # toList s)
[PROOF STEP]
apply (unfold toList_def viewL_def viewL_aux_def
      extract_viewres_def extract_viewres_isNone_def
      extract_viewres_a_def
      extract_viewres_t_def
      empty_rep)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_FingerTree t = Empty \<Longrightarrow> (if Rep_viewres (Abs_viewres (FingerTreeStruc.viewL (Rep_FingerTree t))) = None then None else Some (case Rep_viewres (Abs_viewres (FingerTreeStruc.viewL (Rep_FingerTree t))) of Some (a, t) \<Rightarrow> a, case Rep_viewres (Abs_viewres (FingerTreeStruc.viewL (Rep_FingerTree t))) of None \<Rightarrow> Abs_FingerTree Empty | Some (a, t) \<Rightarrow> Abs_FingerTree t)) = None
 2. Rep_FingerTree t \<noteq> Empty \<Longrightarrow> \<exists>a s. (if Rep_viewres (Abs_viewres (FingerTreeStruc.viewL (Rep_FingerTree t))) = None then None else Some (case Rep_viewres (Abs_viewres (FingerTreeStruc.viewL (Rep_FingerTree t))) of Some (a, t) \<Rightarrow> a, case Rep_viewres (Abs_viewres (FingerTreeStruc.viewL (Rep_FingerTree t))) of None \<Rightarrow> Abs_FingerTree Empty | Some (a, t) \<Rightarrow> Abs_FingerTree t)) = Some (a, s) \<and> FingerTreeStruc.toList (Rep_FingerTree t) = a # FingerTreeStruc.toList (Rep_FingerTree s)
[PROOF STEP]
apply (simp add: FingerTreeStruc.viewL_correct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_FingerTree t \<noteq> Empty \<Longrightarrow> \<exists>a s. (if Rep_viewres (Abs_viewres (FingerTreeStruc.viewL (Rep_FingerTree t))) = None then None else Some (case Rep_viewres (Abs_viewres (FingerTreeStruc.viewL (Rep_FingerTree t))) of Some (a, t) \<Rightarrow> a, case Rep_viewres (Abs_viewres (FingerTreeStruc.viewL (Rep_FingerTree t))) of None \<Rightarrow> Abs_FingerTree Empty | Some (a, t) \<Rightarrow> Abs_FingerTree t)) = Some (a, s) \<and> FingerTreeStruc.toList (Rep_FingerTree t) = a # FingerTreeStruc.toList (Rep_FingerTree s)
[PROOF STEP]
apply (drule FingerTreeStruc.viewL_correct(2)[OF Rep_FingerTree_invar])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a s. FingerTreeStruc.viewL (Rep_FingerTree t) = Some (a, s) \<and> FingerTreeStruc.ft_invar s \<and> FingerTreeStruc.toList (Rep_FingerTree t) = a # FingerTreeStruc.toList s \<Longrightarrow> \<exists>a s. (if Rep_viewres (Abs_viewres (FingerTreeStruc.viewL (Rep_FingerTree t))) = None then None else Some (case Rep_viewres (Abs_viewres (FingerTreeStruc.viewL (Rep_FingerTree t))) of Some (a, t) \<Rightarrow> a, case Rep_viewres (Abs_viewres (FingerTreeStruc.viewL (Rep_FingerTree t))) of None \<Rightarrow> Abs_FingerTree Empty | Some (a, t) \<Rightarrow> Abs_FingerTree t)) = Some (a, s) \<and> FingerTreeStruc.toList (Rep_FingerTree t) = a # FingerTreeStruc.toList (Rep_FingerTree s)
[PROOF STEP]
apply (auto simp add: Abs_viewres_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma viewL_empty[simp]: "viewL empty = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. viewL local.empty = None
[PROOF STEP]
using viewL_correct
[PROOF STATE]
proof (prove)
using this:
?t = local.empty \<Longrightarrow> viewL ?t = None
?t \<noteq> local.empty \<Longrightarrow> \<exists>a s. viewL ?t = Some (a, s) \<and> toList ?t = a # toList s

goal (1 subgoal):
 1. viewL local.empty = None
[PROOF STEP]
by auto


[STATEMENT]
lemma viewL_nonEmpty:
    assumes "t\<noteq>empty"
    obtains a s where "viewL t = Some (a,s)" "toList t = a#toList s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a s. \<lbrakk>viewL t = Some (a, s); toList t = a # toList s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms viewL_correct
[PROOF STATE]
proof (prove)
using this:
t \<noteq> local.empty
?t = local.empty \<Longrightarrow> viewL ?t = None
?t \<noteq> local.empty \<Longrightarrow> \<exists>a s. viewL ?t = Some (a, s) \<and> toList ?t = a # toList s

goal (1 subgoal):
 1. (\<And>a s. \<lbrakk>viewL t = Some (a, s); toList t = a # toList s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma viewR_correct:
    "t = empty \<Longrightarrow> viewR t = None"
    "t \<noteq> empty \<Longrightarrow> \<exists>a s. viewR t = Some (a,s) \<and> toList t = toList s@[a]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t = local.empty \<Longrightarrow> viewR t = None) &&& (t \<noteq> local.empty \<Longrightarrow> \<exists>a s. viewR t = Some (a, s) \<and> toList t = toList s @ [a])
[PROOF STEP]
apply (unfold toList_def viewR_def viewR_aux_def
      extract_viewres_def extract_viewres_isNone_def
      extract_viewres_a_def
      extract_viewres_t_def
      empty_rep)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_FingerTree t = Empty \<Longrightarrow> (if Rep_viewres (Abs_viewres (FingerTreeStruc.viewR (Rep_FingerTree t))) = None then None else Some (case Rep_viewres (Abs_viewres (FingerTreeStruc.viewR (Rep_FingerTree t))) of Some (a, t) \<Rightarrow> a, case Rep_viewres (Abs_viewres (FingerTreeStruc.viewR (Rep_FingerTree t))) of None \<Rightarrow> Abs_FingerTree Empty | Some (a, t) \<Rightarrow> Abs_FingerTree t)) = None
 2. Rep_FingerTree t \<noteq> Empty \<Longrightarrow> \<exists>a s. (if Rep_viewres (Abs_viewres (FingerTreeStruc.viewR (Rep_FingerTree t))) = None then None else Some (case Rep_viewres (Abs_viewres (FingerTreeStruc.viewR (Rep_FingerTree t))) of Some (a, t) \<Rightarrow> a, case Rep_viewres (Abs_viewres (FingerTreeStruc.viewR (Rep_FingerTree t))) of None \<Rightarrow> Abs_FingerTree Empty | Some (a, t) \<Rightarrow> Abs_FingerTree t)) = Some (a, s) \<and> FingerTreeStruc.toList (Rep_FingerTree t) = FingerTreeStruc.toList (Rep_FingerTree s) @ [a]
[PROOF STEP]
apply (simp add: FingerTreeStruc.viewR_correct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_FingerTree t \<noteq> Empty \<Longrightarrow> \<exists>a s. (if Rep_viewres (Abs_viewres (FingerTreeStruc.viewR (Rep_FingerTree t))) = None then None else Some (case Rep_viewres (Abs_viewres (FingerTreeStruc.viewR (Rep_FingerTree t))) of Some (a, t) \<Rightarrow> a, case Rep_viewres (Abs_viewres (FingerTreeStruc.viewR (Rep_FingerTree t))) of None \<Rightarrow> Abs_FingerTree Empty | Some (a, t) \<Rightarrow> Abs_FingerTree t)) = Some (a, s) \<and> FingerTreeStruc.toList (Rep_FingerTree t) = FingerTreeStruc.toList (Rep_FingerTree s) @ [a]
[PROOF STEP]
apply (drule FingerTreeStruc.viewR_correct(2)[OF Rep_FingerTree_invar])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a s. FingerTreeStruc.viewR (Rep_FingerTree t) = Some (a, s) \<and> FingerTreeStruc.ft_invar s \<and> FingerTreeStruc.toList (Rep_FingerTree t) = FingerTreeStruc.toList s @ [a] \<Longrightarrow> \<exists>a s. (if Rep_viewres (Abs_viewres (FingerTreeStruc.viewR (Rep_FingerTree t))) = None then None else Some (case Rep_viewres (Abs_viewres (FingerTreeStruc.viewR (Rep_FingerTree t))) of Some (a, t) \<Rightarrow> a, case Rep_viewres (Abs_viewres (FingerTreeStruc.viewR (Rep_FingerTree t))) of None \<Rightarrow> Abs_FingerTree Empty | Some (a, t) \<Rightarrow> Abs_FingerTree t)) = Some (a, s) \<and> FingerTreeStruc.toList (Rep_FingerTree t) = FingerTreeStruc.toList (Rep_FingerTree s) @ [a]
[PROOF STEP]
apply (auto simp add: Abs_viewres_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma viewR_empty[simp]: "viewR empty = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. viewR local.empty = None
[PROOF STEP]
using viewR_correct
[PROOF STATE]
proof (prove)
using this:
?t = local.empty \<Longrightarrow> viewR ?t = None
?t \<noteq> local.empty \<Longrightarrow> \<exists>a s. viewR ?t = Some (a, s) \<and> toList ?t = toList s @ [a]

goal (1 subgoal):
 1. viewR local.empty = None
[PROOF STEP]
by auto


[STATEMENT]
lemma viewR_nonEmpty:
    assumes "t\<noteq>empty"
    obtains a s where "viewR t = Some (a,s)" "toList t = toList s@[a]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a s. \<lbrakk>viewR t = Some (a, s); toList t = toList s @ [a]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms viewR_correct
[PROOF STATE]
proof (prove)
using this:
t \<noteq> local.empty
?t = local.empty \<Longrightarrow> viewR ?t = None
?t \<noteq> local.empty \<Longrightarrow> \<exists>a s. viewR ?t = Some (a, s) \<and> toList ?t = toList s @ [a]

goal (1 subgoal):
 1. (\<And>a s. \<lbrakk>viewR t = Some (a, s); toList t = toList s @ [a]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma isEmpty_correct: "isEmpty t \<longleftrightarrow> t=empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isEmpty t = (t = local.empty)
[PROOF STEP]
apply (unfold toList_def isEmpty_def empty_rep)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FingerTreeStruc.isEmpty (Rep_FingerTree t) = (Rep_FingerTree t = Empty)
[PROOF STEP]
apply (simp add: FingerTreeStruc.isEmpty_correct FingerTreeStruc.toList_empty)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma head_correct: "t\<noteq>empty \<Longrightarrow> head t = hd (toList t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<noteq> local.empty \<Longrightarrow> head t = hd (toList t)
[PROOF STEP]
apply (unfold toList_def head_def empty_rep)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_FingerTree t \<noteq> Empty \<Longrightarrow> FingerTreeStruc.head (Rep_FingerTree t) = hd (FingerTreeStruc.toList (Rep_FingerTree t))
[PROOF STEP]
apply (simp add: FingerTreeStruc.head_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma tail_correct: "t\<noteq>empty \<Longrightarrow> toList (tail t) = tl (toList t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<noteq> local.empty \<Longrightarrow> toList (tail t) = tl (toList t)
[PROOF STEP]
apply (unfold toList_def tail_def empty_rep)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_FingerTree t \<noteq> Empty \<Longrightarrow> FingerTreeStruc.toList (Rep_FingerTree (if Rep_FingerTree t = Empty then local.empty else Abs_FingerTree (FingerTreeStruc.tail (Rep_FingerTree t)))) = tl (FingerTreeStruc.toList (Rep_FingerTree t))
[PROOF STEP]
apply (simp add: FingerTreeStruc.tail_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma headR_correct: "t\<noteq>empty \<Longrightarrow> headR t = last (toList t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<noteq> local.empty \<Longrightarrow> headR t = last (toList t)
[PROOF STEP]
apply (unfold toList_def headR_def empty_rep)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_FingerTree t \<noteq> Empty \<Longrightarrow> FingerTreeStruc.headR (Rep_FingerTree t) = last (FingerTreeStruc.toList (Rep_FingerTree t))
[PROOF STEP]
apply (simp add: FingerTreeStruc.headR_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma app_correct: "toList (app s t) = toList s @ toList t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList (app s t) = toList s @ toList t
[PROOF STEP]
apply (unfold toList_def app_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FingerTreeStruc.toList (Rep_FingerTree (Abs_FingerTree (FingerTreeStruc.app (Rep_FingerTree s) (Rep_FingerTree t)))) = FingerTreeStruc.toList (Rep_FingerTree s) @ FingerTreeStruc.toList (Rep_FingerTree t)
[PROOF STEP]
apply (simp add: FingerTreeStruc.app_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma splitTree_correct:
    assumes mono: "\<forall>a b. p a \<longrightarrow> p (a + b)"
    assumes init_ff: "\<not> p i"
    assumes sum_tt: "p (i + annot s)"
    assumes fmt: "(splitTree p i s) = (l, (e,a), r)"
    shows "(toList s) = (toList l) @ (e,a) # (toList r)"
    and   "\<not> p (i + annot l)"
    and   "p (i + annot l + a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList s = toList l @ (e, a) # toList r &&& \<not> p (i + annot l) &&& p (i + annot l + a)
[PROOF STEP]
apply (rule
      FingerTreeStruc.splitTree_correctE[
      where p=p and s="Rep_FingerTree s",
      OF _ mono init_ff sum_tt[unfolded annot_def],
      simplified
      ])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>la ea aa ra. \<lbrakk>FingerTreeStruc.splitTree p i (Rep_FingerTree s) = (la, (ea, aa), ra); FingerTreeStruc.toList (Rep_FingerTree s) = FingerTreeStruc.toList la @ (ea, aa) # FingerTreeStruc.toList ra; \<not> p (i + FingerTreeStruc.annot la); p (i + FingerTreeStruc.annot la + aa); FingerTreeStruc.ft_invar la; FingerTreeStruc.ft_invar ra\<rbrakk> \<Longrightarrow> toList s = toList l @ (e, a) # toList r
 2. \<not> p (i + annot l)
 3. p (i + annot l + a)
[PROOF STEP]
using fmt
[PROOF STATE]
proof (prove)
using this:
splitTree p i s = (l, (e, a), r)

goal (3 subgoals):
 1. \<And>la ea aa ra. \<lbrakk>FingerTreeStruc.splitTree p i (Rep_FingerTree s) = (la, (ea, aa), ra); FingerTreeStruc.toList (Rep_FingerTree s) = FingerTreeStruc.toList la @ (ea, aa) # FingerTreeStruc.toList ra; \<not> p (i + FingerTreeStruc.annot la); p (i + FingerTreeStruc.annot la + aa); FingerTreeStruc.ft_invar la; FingerTreeStruc.ft_invar ra\<rbrakk> \<Longrightarrow> toList s = toList l @ (e, a) # toList r
 2. \<not> p (i + annot l)
 3. p (i + annot l + a)
[PROOF STEP]
apply (unfold toList_def splitTree_aux_def splitTree_def annot_def
      extract_splitres_def extract_splitres_l_def
      extract_splitres_a_def extract_splitres_r_def) [1]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>la ea aa ra. \<lbrakk>FingerTreeStruc.splitTree p i (Rep_FingerTree s) = (la, (ea, aa), ra); FingerTreeStruc.toList (Rep_FingerTree s) = FingerTreeStruc.toList la @ (ea, aa) # FingerTreeStruc.toList ra; \<not> p (i + FingerTreeStruc.annot la); p (i + FingerTreeStruc.annot la + aa); FingerTreeStruc.ft_invar la; FingerTreeStruc.ft_invar ra; (case Rep_splitres (if \<not> p i \<and> p (i + FingerTreeStruc.annot (Rep_FingerTree s)) then Abs_splitres (FingerTreeStruc.splitTree p i (Rep_FingerTree s)) else Abs_splitres (Empty, undefined, Empty)) of (l, a, r) \<Rightarrow> Abs_FingerTree l, case Rep_splitres (if \<not> p i \<and> p (i + FingerTreeStruc.annot (Rep_FingerTree s)) then Abs_splitres (FingerTreeStruc.splitTree p i (Rep_FingerTree s)) else Abs_splitres (Empty, undefined, Empty)) of (l, a, s) \<Rightarrow> a, case Rep_splitres (if \<not> p i \<and> p (i + FingerTreeStruc.annot (Rep_FingerTree s)) then Abs_splitres (FingerTreeStruc.splitTree p i (Rep_FingerTree s)) else Abs_splitres (Empty, undefined, Empty)) of (l, a, r) \<Rightarrow> Abs_FingerTree r) = (l, (e, a), r)\<rbrakk> \<Longrightarrow> FingerTreeStruc.toList (Rep_FingerTree s) = FingerTreeStruc.toList (Rep_FingerTree l) @ (e, a) # FingerTreeStruc.toList (Rep_FingerTree r)
 2. \<not> p (i + annot l)
 3. p (i + annot l + a)
[PROOF STEP]
apply (auto split: if_split_asm prod.split_asm
      simp add: init_ff sum_tt[unfolded annot_def] Abs_splitres_inverse) [1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<not> p (i + annot l)
 2. p (i + annot l + a)
[PROOF STEP]
apply (rule
      FingerTreeStruc.splitTree_correctE[
      where p=p and s="Rep_FingerTree s",
      OF _ mono init_ff sum_tt[unfolded annot_def],
      simplified
      ])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>la e a r. \<lbrakk>FingerTreeStruc.splitTree p i (Rep_FingerTree s) = (la, (e, a), r); FingerTreeStruc.toList (Rep_FingerTree s) = FingerTreeStruc.toList la @ (e, a) # FingerTreeStruc.toList r; \<not> p (i + FingerTreeStruc.annot la); p (i + FingerTreeStruc.annot la + a); FingerTreeStruc.ft_invar la; FingerTreeStruc.ft_invar r\<rbrakk> \<Longrightarrow> \<not> p (i + annot l)
 2. p (i + annot l + a)
[PROOF STEP]
using fmt
[PROOF STATE]
proof (prove)
using this:
splitTree p i s = (l, (e, a), r)

goal (2 subgoals):
 1. \<And>la e a r. \<lbrakk>FingerTreeStruc.splitTree p i (Rep_FingerTree s) = (la, (e, a), r); FingerTreeStruc.toList (Rep_FingerTree s) = FingerTreeStruc.toList la @ (e, a) # FingerTreeStruc.toList r; \<not> p (i + FingerTreeStruc.annot la); p (i + FingerTreeStruc.annot la + a); FingerTreeStruc.ft_invar la; FingerTreeStruc.ft_invar r\<rbrakk> \<Longrightarrow> \<not> p (i + annot l)
 2. p (i + annot l + a)
[PROOF STEP]
apply (unfold toList_def splitTree_aux_def splitTree_def annot_def
      extract_splitres_def extract_splitres_l_def
      extract_splitres_a_def extract_splitres_r_def) [1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>la ea aa ra. \<lbrakk>FingerTreeStruc.splitTree p i (Rep_FingerTree s) = (la, (ea, aa), ra); FingerTreeStruc.toList (Rep_FingerTree s) = FingerTreeStruc.toList la @ (ea, aa) # FingerTreeStruc.toList ra; \<not> p (i + FingerTreeStruc.annot la); p (i + FingerTreeStruc.annot la + aa); FingerTreeStruc.ft_invar la; FingerTreeStruc.ft_invar ra; (case Rep_splitres (if \<not> p i \<and> p (i + FingerTreeStruc.annot (Rep_FingerTree s)) then Abs_splitres (FingerTreeStruc.splitTree p i (Rep_FingerTree s)) else Abs_splitres (Empty, undefined, Empty)) of (l, a, r) \<Rightarrow> Abs_FingerTree l, case Rep_splitres (if \<not> p i \<and> p (i + FingerTreeStruc.annot (Rep_FingerTree s)) then Abs_splitres (FingerTreeStruc.splitTree p i (Rep_FingerTree s)) else Abs_splitres (Empty, undefined, Empty)) of (l, a, s) \<Rightarrow> a, case Rep_splitres (if \<not> p i \<and> p (i + FingerTreeStruc.annot (Rep_FingerTree s)) then Abs_splitres (FingerTreeStruc.splitTree p i (Rep_FingerTree s)) else Abs_splitres (Empty, undefined, Empty)) of (l, a, r) \<Rightarrow> Abs_FingerTree r) = (l, (e, a), r)\<rbrakk> \<Longrightarrow> \<not> p (i + FingerTreeStruc.annot (Rep_FingerTree l))
 2. p (i + annot l + a)
[PROOF STEP]
apply (auto split: if_split_asm prod.split_asm
      simp add: init_ff sum_tt[unfolded annot_def] Abs_splitres_inverse) [1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p (i + annot l + a)
[PROOF STEP]
apply (rule
      FingerTreeStruc.splitTree_correctE[
      where p=p and s="Rep_FingerTree s",
      OF _ mono init_ff sum_tt[unfolded annot_def],
      simplified
      ])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>la e aa r. \<lbrakk>FingerTreeStruc.splitTree p i (Rep_FingerTree s) = (la, (e, aa), r); FingerTreeStruc.toList (Rep_FingerTree s) = FingerTreeStruc.toList la @ (e, aa) # FingerTreeStruc.toList r; \<not> p (i + FingerTreeStruc.annot la); p (i + FingerTreeStruc.annot la + aa); FingerTreeStruc.ft_invar la; FingerTreeStruc.ft_invar r\<rbrakk> \<Longrightarrow> p (i + annot l + a)
[PROOF STEP]
using fmt
[PROOF STATE]
proof (prove)
using this:
splitTree p i s = (l, (e, a), r)

goal (1 subgoal):
 1. \<And>la e aa r. \<lbrakk>FingerTreeStruc.splitTree p i (Rep_FingerTree s) = (la, (e, aa), r); FingerTreeStruc.toList (Rep_FingerTree s) = FingerTreeStruc.toList la @ (e, aa) # FingerTreeStruc.toList r; \<not> p (i + FingerTreeStruc.annot la); p (i + FingerTreeStruc.annot la + aa); FingerTreeStruc.ft_invar la; FingerTreeStruc.ft_invar r\<rbrakk> \<Longrightarrow> p (i + annot l + a)
[PROOF STEP]
apply (unfold toList_def splitTree_aux_def splitTree_def annot_def
      extract_splitres_def extract_splitres_l_def
      extract_splitres_a_def extract_splitres_r_def) [1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>la ea aa ra. \<lbrakk>FingerTreeStruc.splitTree p i (Rep_FingerTree s) = (la, (ea, aa), ra); FingerTreeStruc.toList (Rep_FingerTree s) = FingerTreeStruc.toList la @ (ea, aa) # FingerTreeStruc.toList ra; \<not> p (i + FingerTreeStruc.annot la); p (i + FingerTreeStruc.annot la + aa); FingerTreeStruc.ft_invar la; FingerTreeStruc.ft_invar ra; (case Rep_splitres (if \<not> p i \<and> p (i + FingerTreeStruc.annot (Rep_FingerTree s)) then Abs_splitres (FingerTreeStruc.splitTree p i (Rep_FingerTree s)) else Abs_splitres (Empty, undefined, Empty)) of (l, a, r) \<Rightarrow> Abs_FingerTree l, case Rep_splitres (if \<not> p i \<and> p (i + FingerTreeStruc.annot (Rep_FingerTree s)) then Abs_splitres (FingerTreeStruc.splitTree p i (Rep_FingerTree s)) else Abs_splitres (Empty, undefined, Empty)) of (l, a, s) \<Rightarrow> a, case Rep_splitres (if \<not> p i \<and> p (i + FingerTreeStruc.annot (Rep_FingerTree s)) then Abs_splitres (FingerTreeStruc.splitTree p i (Rep_FingerTree s)) else Abs_splitres (Empty, undefined, Empty)) of (l, a, r) \<Rightarrow> Abs_FingerTree r) = (l, (e, a), r)\<rbrakk> \<Longrightarrow> p (i + FingerTreeStruc.annot (Rep_FingerTree l) + a)
[PROOF STEP]
apply (auto split: if_split_asm prod.split_asm
      simp add: init_ff sum_tt[unfolded annot_def] Abs_splitres_inverse) [1]
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma splitTree_correctE:
    assumes mono: "\<forall>a b. p a \<longrightarrow> p (a + b)"
    assumes init_ff: "\<not> p i"
    assumes sum_tt: "p (i + annot s)"
    obtains l e a r where
    "(splitTree p i s) = (l, (e,a), r)" and
    "(toList s) = (toList l) @ (e,a) # (toList r)" and
    "\<not> p (i + annot l)" and
    "p (i + annot l + a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l e a r. \<lbrakk>splitTree p i s = (l, (e, a), r); toList s = toList l @ (e, a) # toList r; \<not> p (i + annot l); p (i + annot l + a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>l e a r. \<lbrakk>splitTree p i s = (l, (e, a), r); toList s = toList l @ (e, a) # toList r; \<not> p (i + annot l); p (i + annot l + a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain l e a r where fmt: "(splitTree p i s) = (l, (e,a), r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l e a r. splitTree p i s = (l, (e, a), r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "(splitTree p i s)") auto
[PROOF STATE]
proof (state)
this:
splitTree p i s = (l, (e, a), r)

goal (1 subgoal):
 1. (\<And>l e a r. \<lbrakk>splitTree p i s = (l, (e, a), r); toList s = toList l @ (e, a) # toList r; \<not> p (i + annot l); p (i + annot l + a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from splitTree_correct[of p, OF assms fmt] fmt
[PROOF STATE]
proof (chain)
picking this:
toList s = toList l @ (e, a) # toList r
\<not> p (i + annot l)
p (i + annot l + a)
splitTree p i s = (l, (e, a), r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
toList s = toList l @ (e, a) # toList r
\<not> p (i + annot l)
p (i + annot l + a)
splitTree p i s = (l, (e, a), r)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (blast intro: that)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma foldl_correct: "foldl f \<sigma> t = List.foldl f \<sigma> (toList t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.foldl f \<sigma> t = List.foldl f \<sigma> (toList t)
[PROOF STEP]
apply (unfold toList_def foldl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FingerTreeStruc.foldl f \<sigma> (Rep_FingerTree t) = List.foldl f \<sigma> (FingerTreeStruc.toList (Rep_FingerTree t))
[PROOF STEP]
apply (simp add: FingerTreeStruc.foldl_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma foldr_correct: "foldr f t \<sigma> = List.foldr f (toList t) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.foldr f t \<sigma> = List.foldr f (toList t) \<sigma>
[PROOF STEP]
apply (unfold toList_def foldr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FingerTreeStruc.foldr f (Rep_FingerTree t) \<sigma> = List.foldr f (FingerTreeStruc.toList (Rep_FingerTree t)) \<sigma>
[PROOF STEP]
apply (simp add: FingerTreeStruc.foldr_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma count_correct: "count t = length (toList t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count t = length (toList t)
[PROOF STEP]
apply (unfold toList_def count_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FingerTreeStruc.count (Rep_FingerTree t) = length (FingerTreeStruc.toList (Rep_FingerTree t))
[PROOF STEP]
apply (simp add: FingerTreeStruc.count_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma distinct4_def:
  "distinct [A,B,C,D] = ((A \<noteq> B) \<and> (A \<noteq> C) \<and> (A \<noteq> D) \<and> (B \<noteq> C) \<and> (B \<noteq> D) \<and> (C \<noteq> D))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct [A, B, C, D] = (A \<noteq> B \<and> A \<noteq> C \<and> A \<noteq> D \<and> B \<noteq> C \<and> B \<noteq> D \<and> C \<noteq> D)
[PROOF STEP]
by auto


[STATEMENT]
lemma distinct3_def:
  "distinct [A,B,C] = ((A \<noteq> B) \<and> (A \<noteq> C) \<and> (B \<noteq> C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct [A, B, C] = (A \<noteq> B \<and> A \<noteq> C \<and> B \<noteq> C)
[PROOF STEP]
by auto