Theory FingerTree

section "2-3 Finger Trees" 

theory FingerTree
imports Main
begin

text 
  We implement and prove correct 2-3 finger trees as described by Ralf Hinze 
  and Ross Paterson\cite{HiPa06}.


text 
  This theory is organized as follows: 
  Section~\ref{sec:datatype} contains the finger-tree datatype, its invariant
  and its abstraction function to lists.
  The Section~\ref{sec:operations} contains the operations 
  on finger trees and their correctness lemmas.
  Section~\ref{sec:hide_invar} contains a finger tree datatype with implicit
  invariant, and, finally, Section~\ref{sec:doc} contains a documentation
  of the implemented operations.


text_raw \paragraph{Technical Issues}
text 
  As Isabelle lacks proper support of namespaces, we
  try to simulate namespaces by locales.

  The problem is, that we define lots of internal functions that
  should not be exposed to the user at all.
  Moreover, we define some functions with names equal to names
  from Isabelle's standard library. These names make perfect sense
  in the context of FingerTrees, however, they shall not be exposed 
  to anyone using this theory indirectly, hiding the standard library
  names there.

  Our approach puts all functions and lemmas inside the locale 
  {\em FingerTree\_loc},
  and then interprets this locale with the prefix {\em FingerTree}.
  This makes all definitions visible outside the locale, with
  qualified names. Inside the locale, however, one can use unqualified names.


subsection "Datatype definition"
text_raw\label{sec:datatype}
locale FingerTreeStruc_loc

text 
  Nodes: Non empty 2-3 trees, with all elements stored within the leafs plus a 
  cached annotation 

datatype ('e,'a) Node = Tip 'e 'a |
  Node2 'a "('e,'a) Node" "('e,'a) Node" | 
  Node3 'a "('e,'a) Node" "('e,'a) Node" "('e,'a) Node"

  text Digit: one to four ordered Nodes
datatype ('e,'a) Digit = One "('e,'a) Node" |
   Two "('e,'a) Node" "('e,'a) Node" |
   Three "('e,'a) Node" "('e,'a) Node" "('e,'a) Node" |
   Four "('e,'a) Node" "('e,'a) Node" "('e,'a) Node" "('e,'a) Node"

  text FingerTreeStruc: 
    The empty tree, a single node or some nodes and a deeper tree
datatype ('e, 'a) FingerTreeStruc = 
  Empty |
  Single "('e,'a) Node" |
  Deep 'a "('e,'a) Digit" "('e,'a) FingerTreeStruc" "('e,'a) Digit"

subsubsection "Invariant"

context FingerTreeStruc_loc
begin
text_raw \paragraph{Auxiliary functions}\ \\

  text Readout the cached annotation of a node
primrec gmn :: "('e,'a::monoid_add) Node  'a" where
  "gmn (Tip e a) = a" |
  "gmn (Node2 a _ _) = a" |
  "gmn (Node3 a _ _ _) = a"

  text The annotation of a digit is computed on the fly
primrec gmd :: "('e,'a::monoid_add) Digit  'a" where
  "gmd (One a) = gmn a" |
  "gmd (Two a b) = (gmn a) + (gmn b)"|
  "gmd (Three a b c) = (gmn a) + (gmn b) + (gmn c)"|
  "gmd (Four a b c d) = (gmn a) + (gmn b) + (gmn c) + (gmn d)"

  text Readout the cached annotation of a finger tree
primrec gmft :: "('e,'a::monoid_add) FingerTreeStruc  'a" where
  "gmft Empty = 0" |
  "gmft (Single nd) = gmn nd" |
  "gmft (Deep a _ _ _) = a"

text Depth and cached annotations have to be correct

fun is_leveln_node :: "nat  ('e,'a) Node  bool" where
  "is_leveln_node 0 (Tip _ _)  True" |
  "is_leveln_node (Suc n) (Node2 _ n1 n2)  
    is_leveln_node n n1  is_leveln_node n n2" |
  "is_leveln_node (Suc n) (Node3 _ n1 n2 n3)  
    is_leveln_node n n1  is_leveln_node n n2  is_leveln_node n n3" |
  "is_leveln_node _ _  False"

primrec is_leveln_digit :: "nat  ('e,'a) Digit  bool" where
  "is_leveln_digit n (One n1)  is_leveln_node n n1" |
  "is_leveln_digit n (Two n1 n2)  is_leveln_node n n1  
    is_leveln_node n n2" |
  "is_leveln_digit n (Three n1 n2 n3)  is_leveln_node n n1  
    is_leveln_node n n2  is_leveln_node n n3" |
  "is_leveln_digit n (Four n1 n2 n3 n4)  is_leveln_node n n1  
    is_leveln_node n n2  is_leveln_node n n3  is_leveln_node n n4"

primrec is_leveln_ftree :: "nat  ('e,'a) FingerTreeStruc  bool" where
  "is_leveln_ftree n Empty  True" |
  "is_leveln_ftree n (Single nd)  is_leveln_node n nd" |
  "is_leveln_ftree n (Deep _ l t r)  is_leveln_digit n l  
    is_leveln_digit n r  is_leveln_ftree (Suc n) t"

primrec is_measured_node :: "('e,'a::monoid_add) Node  bool" where
  "is_measured_node (Tip _ _)  True" |
  "is_measured_node (Node2 a n1 n2)  ((is_measured_node n1)  
    (is_measured_node n2))  (a = (gmn n1) + (gmn n2))" |
  "is_measured_node (Node3 a n1 n2 n3)  ((is_measured_node n1)  
    (is_measured_node n2)  (is_measured_node n3))  
    (a = (gmn n1) + (gmn n2) + (gmn n3))"

primrec is_measured_digit :: "('e,'a::monoid_add) Digit  bool" where
  "is_measured_digit (One a) = is_measured_node a" |
  "is_measured_digit (Two a b) = 
    ((is_measured_node a)  (is_measured_node b))"|
  "is_measured_digit (Three a b c) = 
    ((is_measured_node a)  (is_measured_node b)  (is_measured_node c))"|
  "is_measured_digit (Four a b c d) = ((is_measured_node a)  
    (is_measured_node b)  (is_measured_node c)  (is_measured_node d))"

primrec is_measured_ftree :: "('e,'a::monoid_add) FingerTreeStruc  bool" where
  "is_measured_ftree Empty  True" |
  "is_measured_ftree (Single n1)  (is_measured_node n1)" |
  "is_measured_ftree (Deep a l m r)  ((is_measured_digit l)  
    (is_measured_ftree m)  (is_measured_digit r))  
    (a = ((gmd l) + (gmft m) + (gmd r)))"

text "Structural invariant for finger trees"
definition "ft_invar t == is_leveln_ftree 0 t  is_measured_ftree t"

subsubsection "Abstraction to Lists"

primrec nodeToList :: "('e,'a) Node  ('e × 'a) list" where
  "nodeToList (Tip e a) = [(e,a)]"|
  "nodeToList (Node2 _ a b) = (nodeToList a) @ (nodeToList b)"|
  "nodeToList (Node3 _ a b c) 
    = (nodeToList a) @ (nodeToList b) @ (nodeToList c)"

primrec digitToList :: "('e,'a) Digit  ('e × 'a) list" where
  "digitToList (One a) = nodeToList a"|
  "digitToList (Two a b) = (nodeToList a) @ (nodeToList b)"|
  "digitToList (Three a b c) 
    = (nodeToList a) @ (nodeToList b) @ (nodeToList c)"|
  "digitToList (Four a b c d) 
    = (nodeToList a) @ (nodeToList b) @ (nodeToList c) @ (nodeToList d)"

text "List representation of a finger tree"
primrec toList :: "('e ,'a) FingerTreeStruc  ('e × 'a) list" where
  "toList Empty = []"|
  "toList (Single a) = nodeToList a"|
  "toList (Deep _ pr m sf) = (digitToList pr) @ (toList m) @ (digitToList sf)"

lemma nodeToList_empty: "nodeToList nd  Nil"
  by (induct nd) auto

lemma digitToList_empty: "digitToList d  Nil"
  by (cases d, auto simp add: nodeToList_empty)

text Auxiliary lemmas
lemma gmn_correct:
  assumes "is_measured_node nd"
  shows "gmn nd = sum_list (map snd (nodeToList nd))"
  by (insert assms, induct nd) (auto simp add: add.assoc)

lemma gmd_correct:
  assumes "is_measured_digit d"
  shows "gmd d = sum_list (map snd (digitToList d))"
  by (insert assms, cases d, auto simp add: gmn_correct add.assoc)

lemma gmft_correct: "is_measured_ftree t 
   (gmft t) = sum_list (map snd (toList t))"
  by (induct t, auto simp add: ft_invar_def gmd_correct gmn_correct add.assoc)
lemma gmft_correct2: "ft_invar t  (gmft t) = sum_list (map snd (toList t))"
  by (simp only: ft_invar_def gmft_correct)

subsection Operations
text_raw\label{sec:operations}

subsubsection Empty tree
lemma Empty_correct[simp]: 
  "toList Empty = []"
  "ft_invar Empty"
  by (simp_all add: ft_invar_def)

text Exactly the empty finger tree represents the empty list
lemma toList_empty: "toList t = []  t = Empty"
  by (induct t, auto simp add: nodeToList_empty digitToList_empty)

subsubsection Annotation
text "Sum of annotations of all elements of a finger tree"
definition annot :: "('e,'a::monoid_add) FingerTreeStruc  'a"
  where "annot t = gmft t"

lemma annot_correct:
  "ft_invar t  annot t = sum_list (map snd (toList t))"
  using gmft_correct
  unfolding annot_def
  by (simp add: gmft_correct2)

subsubsection Appending

text Auxiliary functions to fill in the annotations
definition deep:: "('e,'a::monoid_add) Digit  ('e,'a) FingerTreeStruc 
     ('e,'a) Digit  ('e, 'a) FingerTreeStruc" where
  "deep pr m sf = Deep ((gmd pr) + (gmft m) + (gmd sf)) pr m sf"
definition node2 where
  "node2 nd1 nd2 = Node2 ((gmn nd1)+(gmn nd2)) nd1 nd2"
definition node3 where
  "node3 nd1 nd2 nd3 = Node3 ((gmn nd1)+(gmn nd2)+(gmn nd3)) nd1 nd2 nd3"

text "Append a node at the left end"
fun nlcons :: "('e,'a::monoid_add) Node  ('e,'a) FingerTreeStruc 
     ('e,'a) FingerTreeStruc"  
where
― ‹Recursively we append a node, if the digit is full we push down a node3
  "nlcons a Empty = Single a" |
  "nlcons a (Single b) = deep (One a) Empty (One b)" |
  "nlcons a (Deep _ (One b) m sf) = deep (Two a b) m sf" |
  "nlcons a (Deep _ (Two b c) m sf) = deep (Three a b c) m sf" |
  "nlcons a (Deep _ (Three b c d) m sf) = deep (Four a b c d) m sf" |
  "nlcons a (Deep _ (Four b c d e) m sf) 
    = deep (Two a b) (nlcons (node3 c d e) m) sf"

text "Append a node at the right end"
fun nrcons :: "('e,'a::monoid_add) FingerTreeStruc 
     ('e,'a) Node  ('e,'a) FingerTreeStruc"  where
  ― ‹Recursively we append a node, if the digit is full we push down a node3
  "nrcons Empty a = Single a" |
  "nrcons (Single b) a = deep (One b) Empty (One a)" |
  "nrcons (Deep _ pr m (One b)) a = deep pr m (Two  b a)"|
  "nrcons (Deep _ pr m (Two b c)) a = deep pr m (Three b c a)" |
  "nrcons (Deep _ pr m (Three b c d)) a = deep pr m (Four b c d a)" |
  "nrcons (Deep _ pr m (Four b c d e)) a 
    = deep pr (nrcons m (node3 b c d)) (Two e a)"

lemma nlcons_invlevel: "is_leveln_ftree n t; is_leveln_node n nd 
   is_leveln_ftree n (nlcons nd t)"
  by (induct t arbitrary: n nd rule: nlcons.induct) 
(auto simp add: deep_def node3_def)

lemma nlcons_invmeas: "is_measured_ftree t; is_measured_node nd 
   is_measured_ftree (nlcons nd t)"
  by (induct t arbitrary: nd rule: nlcons.induct) 
     (auto simp add: deep_def node3_def)

lemmas nlcons_inv = nlcons_invlevel nlcons_invmeas

lemma nlcons_list: "toList (nlcons a t) = (nodeToList a) @ (toList t)"
  apply (induct t arbitrary: a rule: nlcons.induct)
  apply (auto simp add: deep_def toList_def node3_def)
done

lemma nrcons_invlevel: "is_leveln_ftree n t; is_leveln_node n nd 
   is_leveln_ftree n (nrcons t nd)"
  apply (induct t nd arbitrary: nd n rule:nrcons.induct) 
  apply(auto simp add: deep_def node3_def)
  done

lemma nrcons_invmeas: "is_measured_ftree t; is_measured_node nd 
   is_measured_ftree (nrcons t nd)"
  apply (induct t nd arbitrary: nd rule:nrcons.induct) 
  apply(auto simp add: deep_def node3_def)
  done

lemmas nrcons_inv = nrcons_invlevel nrcons_invmeas

lemma nrcons_list: "toList (nrcons t a) = (toList t) @ (nodeToList a)"
  apply (induct t a arbitrary: a rule: nrcons.induct)
  apply (auto simp add: deep_def toList_def node3_def)
done

text "Append an element at the left end"
definition lcons :: "('e × 'a::monoid_add) 
     ('e,'a) FingerTreeStruc  ('e,'a) FingerTreeStruc" (infixr "" 65) where
  "a  t = nlcons (Tip (fst a) (snd a)) t"

lemma lcons_correct: 
  assumes "ft_invar t" 
  shows "ft_invar (a  t)" and "toList (a  t) = a # (toList t)"
  using assms
  unfolding ft_invar_def
  by (simp_all add: lcons_def nlcons_list nlcons_invlevel nlcons_invmeas)

lemma lcons_inv:"ft_invar t  ft_invar (a  t)"
  by (rule lcons_correct)

lemma lcons_list[simp]: "toList (a  t) = a # (toList t)"
  by (simp add: lcons_def nlcons_list)

text "Append an element at the right end"
definition rcons 
  :: "('e,'a::monoid_add) FingerTreeStruc  ('e × 'a)  ('e,'a) FingerTreeStruc"
      (infixl "" 65) where
  "t  a = nrcons t (Tip (fst a) (snd a))"

lemma rcons_correct: 
  assumes "ft_invar t" 
  shows "ft_invar (t  a)" and "toList (t  a) = (toList t) @ [a]"
  using assms
  by (auto simp add: nrcons_inv ft_invar_def rcons_def nrcons_list)

lemma rcons_inv:"ft_invar t  ft_invar (t  a)"
  by (rule rcons_correct)

lemma rcons_list[simp]: "toList (t  a) = (toList t) @ [a]"
  by(auto simp add: nrcons_list rcons_def) 


subsubsection Convert list to tree
primrec toTree :: "('e × 'a::monoid_add) list  ('e,'a) FingerTreeStruc" where
  "toTree [] = Empty"|
  "toTree (a#xs) = a  (toTree xs)"

lemma toTree_correct[simp]:
  "ft_invar (toTree l)"
  "toList (toTree l) = l"
  apply (induct l)
  apply (simp add: ft_invar_def)
  apply simp
  apply (simp add: toTree_def lcons_list lcons_inv)
  apply (simp add: toTree_def lcons_list lcons_inv)
  done

text 
  Note that this lemma is a completeness statement of our implementation, 
  as it can be read as:
  ,,All lists of elements have a valid representation as a finger tree.''


subsubsection Detaching leftmost/rightmost element

primrec digitToTree :: "('e,'a::monoid_add) Digit  ('e,'a) FingerTreeStruc" 
  where
  "digitToTree (One a) = Single a"|
  "digitToTree (Two a b) = deep (One a) Empty (One b)"|
  "digitToTree (Three a b c) = deep (Two a b) Empty (One c)"|
  "digitToTree (Four a b c d) = deep (Two a b) Empty (Two c d)"

primrec nodeToDigit :: "('e,'a) Node  ('e,'a) Digit" where
  "nodeToDigit (Tip e a) = One (Tip e a)"|
  "nodeToDigit (Node2 _ a b) = Two a b"|
  "nodeToDigit (Node3 _ a b c) = Three a b c"

fun nlistToDigit :: "('e,'a) Node list  ('e,'a) Digit" where
  "nlistToDigit [a] = One a" |
  "nlistToDigit [a,b] = Two a b" |
  "nlistToDigit [a,b,c] = Three a b c" |
  "nlistToDigit [a,b,c,d] = Four a b c d"

primrec digitToNlist :: "('e,'a) Digit  ('e,'a) Node list" where
  "digitToNlist (One a) = [a]" |
  "digitToNlist (Two a b) = [a,b] " |
  "digitToNlist (Three a b c) = [a,b,c]" |
  "digitToNlist (Four a b c d) = [a,b,c,d]"

text Auxiliary function to unwrap a Node element 
primrec n_unwrap:: "('e,'a) Node  ('e × 'a)" where
  "n_unwrap (Tip e a) = (e,a)"|
  "n_unwrap (Node2 _ a b) = undefined"|
  "n_unwrap (Node3 _ a b c) = undefined"


type_synonym ('e,'a) ViewnRes = "(('e,'a) Node × ('e,'a) FingerTreeStruc) option"
lemma viewnres_cases:
  fixes r :: "('e,'a) ViewnRes"
  obtains (Nil) "r=None" |
          (Cons) a t where "r=Some (a,t)"
  by (cases r) auto

lemma viewnres_split: 
  "P (case_option f1 (case_prod f2) x) = 
  ((x = None  P f1)  (a b. x = Some (a,b)  P (f2 a b)))"
  by (auto split: option.split prod.split)

text Detach the leftmost node. Return @{const None} on empty finger tree.
fun viewLn :: "('e,'a::monoid_add) FingerTreeStruc  ('e,'a) ViewnRes" where
  "viewLn Empty = None"|
  "viewLn (Single a) = Some (a, Empty)"| 
  "viewLn (Deep _ (Two a b) m sf) = Some (a, (deep (One b) m sf))"|
  "viewLn (Deep _ (Three a b c) m sf) = Some (a, (deep (Two b c) m sf))"|
  "viewLn (Deep _ (Four a b c d) m sf) = Some (a, (deep (Three b c d) m sf))"|
  "viewLn (Deep _ (One a) m sf) = 
    (case viewLn m of 
      None  Some (a, (digitToTree sf)) |
      Some (b, m2)  Some (a, (deep (nodeToDigit b) m2 sf)))"


text Detach the rightmost node. Return @{const None} on empty finger tree.
fun viewRn :: "('e,'a::monoid_add) FingerTreeStruc  ('e,'a) ViewnRes" where
  "viewRn Empty = None" |
  "viewRn (Single a) = Some (a, Empty)" | 
  "viewRn (Deep _ pr m (Two a b)) = Some (b, (deep pr m (One a)))" |
  "viewRn (Deep _ pr m (Three a b c)) = Some (c, (deep pr m (Two a b)))" |
  "viewRn (Deep _ pr m (Four a b c d)) = Some (d, (deep pr m (Three a b c)))" |
  "viewRn (Deep _ pr m (One a)) = 
    (case viewRn m of 
      None  Some (a, (digitToTree pr))|
      Some (b, m2)  Some (a, (deep pr m2 (nodeToDigit b))))"

(* TODO: Head, last geht auch in O(1) !!! *)

lemma 
  digitToTree_inv: "is_leveln_digit n d  is_leveln_ftree n (digitToTree d)"
  "is_measured_digit d  is_measured_ftree (digitToTree d)" 
  apply (cases d,auto simp add: deep_def)
  apply (cases d,auto simp add: deep_def)
  done

lemma digitToTree_list: "toList (digitToTree d) = digitToList d"
  by (cases d) (auto simp add: deep_def)

lemma nodeToDigit_inv:
  "is_leveln_node (Suc n) nd  is_leveln_digit n (nodeToDigit nd) " 
  "is_measured_node nd  is_measured_digit (nodeToDigit nd)"
  by (cases nd, auto) (cases nd, auto)

lemma nodeToDigit_list: "digitToList (nodeToDigit nd) = nodeToList nd"
  by (cases nd,auto)



lemma viewLn_empty: "t  Empty  (viewLn t)  None"
proof (cases t)
  case Empty thus ?thesis by simp
next
  case (Single Node) thus ?thesis by simp
next
  case (Deep a l x r) thus ?thesis 
  apply(auto)
  apply(case_tac l)
  apply(auto)
  apply(cases "viewLn x")
  apply(auto)
  done
qed

lemma viewLn_inv: "
  is_measured_ftree t; is_leveln_ftree n t; viewLn t = Some (nd, s)
    is_measured_ftree s  is_measured_node nd  
        is_leveln_ftree n s  is_leveln_node n nd"
  apply(induct t arbitrary: n nd s rule: viewLn.induct)
  apply(simp add: viewLn_empty)
  apply(simp)
  apply(auto simp add: deep_def)[1]
  apply(auto simp add: deep_def)[1]
  apply(auto simp add: deep_def)[1]
proof -
  fix ux a m sf n nd s
  assume av: "n nd s.
           is_measured_ftree m; is_leveln_ftree n m; viewLn m = Some (nd, s)
            is_measured_ftree s 
              is_measured_node nd  is_leveln_ftree n s  is_leveln_node n nd "
         " is_measured_ftree (Deep ux (One a) m sf) "
         "is_leveln_ftree n (Deep ux (One a) m sf)"
         "viewLn (Deep ux (One a) m sf) = Some (nd, s)"
  thus "is_measured_ftree s 
          is_measured_node nd  is_leveln_ftree n s  is_leveln_node n nd"
  proof (cases "viewLn m" rule: viewnres_cases)
    case Nil
    with av(4) have v1: "nd = a" "s = digitToTree sf"
    by auto
    from v1 av(2,3) show "is_measured_ftree s 
       is_measured_node nd  is_leveln_ftree n s  is_leveln_node n nd"
       apply(auto)
       apply(auto simp add: digitToTree_inv)
    done
  next
    case (Cons b m2)
    with av(4) have v2: "nd = a" "s = (deep (nodeToDigit b) m2 sf)" 
    apply (auto simp add: deep_def)
    done
    note myiv = av(1)[of "Suc n" b m2]
    from v2 av(2,3) have "is_measured_ftree m  is_leveln_ftree (Suc n) m"
    apply(simp)
    done
    hence bv: "is_measured_ftree m2 
   is_measured_node b  is_leveln_ftree (Suc n) m2  is_leveln_node (Suc n) b"
    using myiv Cons
    apply(simp)
    done
    with av(2,3) v2 show "is_measured_ftree s 
          is_measured_node nd  is_leveln_ftree n s  is_leveln_node n nd"
    apply(auto simp add: deep_def nodeToDigit_inv)
    done
  qed
qed

lemma viewLn_list: " viewLn t = Some (nd, s) 
   toList t = (nodeToList nd) @ (toList s)"
  supply [[simproc del: defined_all]]
  apply(induct t arbitrary: nd s rule: viewLn.induct)
  apply(simp)
  apply(simp)
  apply(simp)
  apply(simp add: deep_def)
  apply(auto simp add: toList_def)[1]
  apply(simp)
  apply(simp add: deep_def)
  apply(auto simp add: toList_def)[1]
  apply(simp)
  apply(simp add: deep_def)
  apply(auto simp add: toList_def)[1]
  apply(simp)
  subgoal premises prems for a m sf nd s
    using prems
  proof (cases "viewLn m" rule: viewnres_cases)
    case Nil
    hence av: "m = Empty" by (metis viewLn_empty)  
    from av prems
    show "nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s"
      by (auto simp add: digitToTree_list)
  next        
    case (Cons b m2)
    with prems have bv: "nd = a" "s = (deep (nodeToDigit b) m2 sf)"
      by (auto simp add: deep_def)
    with Cons prems
    show "nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s"
      apply(simp)
      apply(simp add: deep_def)
      apply(simp add: deep_def nodeToDigit_list)
      done
  qed
  done

lemma viewRn_empty: "t  Empty  (viewRn t)  None"
proof (cases t)
  case Empty thus ?thesis by simp
next
  case (Single Node) thus ?thesis by simp
next
  case (Deep a l x r) thus ?thesis 
  apply(auto)
  apply(case_tac r)
  apply(auto)
  apply(cases "viewRn x")
  apply(auto)
  done
qed

lemma viewRn_inv: "
  is_measured_ftree t; is_leveln_ftree n t; viewRn t = Some (nd, s)
    is_measured_ftree s  is_measured_node nd  
       is_leveln_ftree n s  is_leveln_node n nd"
  apply(induct t arbitrary: n nd s rule: viewRn.induct)
  apply(simp add: viewRn_empty)
  apply(simp)
  apply(auto simp add: deep_def)[1]
  apply(auto simp add: deep_def)[1]
  apply(auto simp add: deep_def)[1]
proof -
  fix ux a m "pr" n nd s
  assume av: "n nd s.
           is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)
            is_measured_ftree s 
              is_measured_node nd  is_leveln_ftree n s  is_leveln_node n nd "
         " is_measured_ftree (Deep ux pr m (One a)) "
         "is_leveln_ftree n (Deep ux pr m (One a))"
         "viewRn (Deep ux pr m (One a)) = Some (nd, s)"
  thus "is_measured_ftree s 
          is_measured_node nd  is_leveln_ftree n s  is_leveln_node n nd"
  proof (cases "viewRn m" rule: viewnres_cases)
    case Nil
    with av(4) have v1: "nd = a" "s = digitToTree pr"
    by auto
    from v1 av(2,3) show "is_measured_ftree s 
       is_measured_node nd  is_leveln_ftree n s  is_leveln_node n nd"
       apply(auto)
       apply(auto simp add: digitToTree_inv)
    done
  next
    case (Cons b m2)
    with av(4) have v2: "nd = a" "s = (deep pr m2 (nodeToDigit b))" 
    apply (auto simp add: deep_def)
    done
    note myiv = av(1)[of "Suc n" b m2]
    from v2 av(2,3) have "is_measured_ftree m  is_leveln_ftree (Suc n) m"
    apply(simp)
    done
    hence bv: "is_measured_ftree m2 
   is_measured_node b  is_leveln_ftree (Suc n) m2  is_leveln_node (Suc n) b"
    using myiv Cons
    apply(simp)
    done
    with av(2,3) v2 show "is_measured_ftree s 
          is_measured_node nd  is_leveln_ftree n s  is_leveln_node n nd"
    apply(auto simp add: deep_def nodeToDigit_inv)
    done
  qed
qed

lemma viewRn_list: "viewRn t = Some (nd, s) 
   toList t = (toList s) @ (nodeToList nd)"
  supply [[simproc del: defined_all]]
  apply(induct t arbitrary: nd s rule: viewRn.induct)
  apply(simp)
  apply(simp)
  apply(simp)
  apply(simp add: deep_def)
  apply(auto simp add: toList_def)[1]
  apply(simp)
  apply(simp add: deep_def)
  apply(auto simp add: toList_def)[1]
  apply(simp)
  apply(simp add: deep_def)
  apply(auto simp add: toList_def)[1]
  apply(simp)
  subgoal premises prems for pr m a nd s
  proof (cases "viewRn m" rule: viewnres_cases)
    case Nil
    from Nil have av: "m = Empty" by (metis viewRn_empty)  
    from av prems
    show "digitToList pr @ toList m @ nodeToList a = toList s @ nodeToList nd"
      by (auto simp add: digitToTree_list)
  next        
    case (Cons b m2)
    with prems have bv: "nd = a" "s = (deep pr m2 (nodeToDigit b))"
    apply(auto simp add: deep_def) done
    with Cons prems
    show "digitToList pr @ toList m @ nodeToList a = toList s @ nodeToList nd"
      apply(simp)
      apply(simp add: deep_def)
      apply(simp add: deep_def nodeToDigit_list)
     done
  qed
  done

type_synonym ('e,'a) viewres = "(('e ×'a) × ('e,'a) FingerTreeStruc) option"

text Detach the leftmost element. Return @{const None} on empty finger tree.
definition viewL :: "('e,'a::monoid_add) FingerTreeStruc  ('e,'a) viewres" 
  where 
"viewL t = (case viewLn t of 
  None  None |
  (Some (a, t2))  Some ((n_unwrap a), t2))"

lemma viewL_correct: 
  assumes INV: "ft_invar t" 
  shows
  "(t=Empty  viewL t = None)"
  "(tEmpty  (a s. viewL t = Some (a, s)  ft_invar s 
                         toList t = a # toList s))"
proof -
  assume "t=Empty" thus "viewL t = None" by (simp add: viewL_def)
next
  assume NE: "t  Empty"
  from INV have INV': "is_leveln_ftree 0 t" "is_measured_ftree t" 
    by (simp_all add: ft_invar_def)
  from NE have v1: "viewLn t  None" by (auto simp add: viewLn_empty)
  then obtain nd s where vn: "viewLn t = Some (nd, s)" 
    by (cases "viewLn t") (auto)
  from this obtain a where v1: "viewL t = Some (a, s)"
    by (auto simp add: viewL_def)
  from INV' vn have 
    v2: "is_measured_ftree s  is_leveln_ftree 0 s 
          is_leveln_node 0 nd  is_measured_node nd"
        "toList t = (nodeToList nd) @ (toList s)"
    by (auto simp add: viewLn_inv[of t 0 nd s] viewLn_list[of t])
  with v1 vn have v3: "nodeToList nd = [a]"
    apply (auto simp add: viewL_def )
    apply (induct nd)
    apply (simp_all (no_asm_use))
    done
  with v1 v2
  show "a s. viewL t = Some (a, s)  ft_invar s  toList t = a # toList s"
    by (auto simp add: ft_invar_def)
qed

lemma viewL_correct_empty[simp]: "viewL Empty = None"
  by (simp add: viewL_def)

lemma viewL_correct_nonEmpty: 
  assumes "ft_invar t" "t  Empty" 
  obtains a s where 
  "viewL t = Some (a, s)" "ft_invar s" "toList t = a # toList s"
  using assms viewL_correct by blast


text Detach the rightmost element. Return @{const None} on empty finger tree.
definition viewR :: "('e,'a::monoid_add) FingerTreeStruc  ('e,'a) viewres" 
  where 
  "viewR t = (case viewRn t of 
    None  None |
    (Some (a, t2))  Some ((n_unwrap a), t2))"

lemma viewR_correct: 
  assumes INV: "ft_invar t"
  shows
  "(t = Empty  viewR t = None)"
  "(t  Empty  ( a s. viewR t = Some (a, s)  ft_invar s 
                           toList t = toList s @ [a]))"
proof -
  assume "t=Empty" thus "viewR t = None" by (simp add: viewR_def)
next
  assume NE: "t  Empty"
  from INV have INV': "is_leveln_ftree 0 t" "is_measured_ftree t" 
    unfolding ft_invar_def by simp_all
  from NE have v1: "viewRn t  None" by (auto simp add: viewRn_empty)
  then obtain nd s where vn: "viewRn t = Some (nd, s)" 
    by (cases "viewRn t") (auto)
  from this obtain a where v1: "viewR t = Some (a, s)"
    by (auto simp add: viewR_def)
  from INV' vn have 
    v2: "is_measured_ftree s  is_leveln_ftree 0 s 
          is_leveln_node 0 nd  is_measured_node nd"
        "toList t = (toList s) @ (nodeToList nd)"
    by (auto simp add: viewRn_inv[of t 0 nd s] viewRn_list[of t])
  with v1 vn have v3: "nodeToList nd = [a]"
    apply (auto simp add: viewR_def )
    apply (induct nd)
    apply (simp_all (no_asm_use))
    done
  with v1 v2
  show "a s. viewR t = Some (a, s)  ft_invar s  toList t = toList s @ [a]"
    unfolding ft_invar_def by auto
qed  

lemma viewR_correct_empty[simp]: "viewR Empty = None"
  unfolding viewR_def by simp

lemma viewR_correct_nonEmpty: 
  assumes "ft_invar t" "t  Empty" 
  obtains a s where 
  "viewR t = Some (a, s)" "ft_invar s  toList t = toList s @ [a]"
  using assms viewR_correct by blast

text Finger trees viewed as a double-ended queue. The head and tail functions
  here are only
  defined for non-empty queues, while the view-functions were also defined for
  empty finger trees.
text "Check for emptiness"
definition isEmpty :: "('e,'a) FingerTreeStruc  bool" where
  [code del]: "isEmpty t = (t = Empty)"
lemma isEmpty_correct: "isEmpty t  toList t = []"
  unfolding isEmpty_def by (simp add: toList_empty)
― ‹Avoid comparison with @{text "(=)"}, and thus unnecessary equality-class
    parameter on element types in generated code
lemma [code]: "isEmpty t = (case t of Empty  True | _  False)"
  apply (cases t)
  apply (auto simp add: isEmpty_def)
  done

text "Leftmost element"
definition head :: "('e,'a::monoid_add) FingerTreeStruc  'e × 'a" where
  "head t = (case viewL t of (Some (a, _))  a)"
lemma head_correct:
  assumes "ft_invar t" "t  Empty" 
  shows "head t = hd (toList t)"
proof -
  from assms viewL_correct 
  obtain a s where 
    v1:"viewL t = Some (a, s)  ft_invar s  toList t = a # toList s" by blast
  hence v2: "head t = a" by (auto simp add: head_def)
  from v1 have "hd (toList t) = a" by simp
  with v2 show ?thesis by simp
qed

text "All but the leftmost element"
definition tail 
  :: "('e,'a::monoid_add) FingerTreeStruc  ('e,'a) FingerTreeStruc" 
  where
  "tail t = (case viewL t of (Some (_, m))  m)"
lemma tail_correct: 
  assumes "ft_invar t" "t  Empty" 
  shows "toList (tail t) = tl (toList t)" and "ft_invar (tail t)"
proof -
  from assms viewL_correct 
  obtain a s where 
    v1:"viewL t = Some (a, s)  ft_invar s  toList t = a # toList s" by blast
  hence v2: "tail t = s" by (auto simp add: tail_def)
  from v1 have "tl (toList t) = toList s" by simp
  with v1 v2 show 
    "toList (tail t) = tl (toList t)" 
    "ft_invar (tail t)"
    by simp_all
qed

text "Rightmost element"  
definition headR :: "('e,'a::monoid_add) FingerTreeStruc  'e × 'a" where
  "headR t = (case viewR t of (Some (a, _))  a)"
lemma headR_correct:
  assumes "ft_invar t" "t  Empty" 
  shows  "headR t = last (toList t)"
proof -
  from assms viewR_correct 
  obtain a s where 
    v1:"viewR t = Some (a, s)  ft_invar s  toList t = toList s @ [a]" by blast
  hence v2: "headR t = a" by (auto simp add: headR_def)
  with v1 show ?thesis by auto
qed

text "All but the rightmost element"
definition tailR 
  :: "('e,'a::monoid_add) FingerTreeStruc  ('e,'a) FingerTreeStruc" 
  where
  "tailR t = (case viewR t of (Some (_, m))  m)"
lemma tailR_correct: 
  assumes "ft_invar t" "t  Empty"
  shows "toList (tailR t) = butlast (toList t)" and "ft_invar (tailR t)"
proof -
  from assms viewR_correct 
  obtain a s where 
    v1:"viewR t = Some (a, s)  ft_invar s  toList t = toList s @ [a]" by blast
  hence v2: "tailR t = s" by (auto simp add: tailR_def)
  with v1 show "toList (tailR t) = butlast (toList t)" and "ft_invar (tailR t)"
    by auto
qed 

subsubsection Concatenation
primrec lconsNlist :: "('e,'a::monoid_add) Node list 
     ('e,'a) FingerTreeStruc  ('e,'a) FingerTreeStruc" where
  "lconsNlist [] t = t" |
  "lconsNlist (x#xs) t = nlcons x (lconsNlist xs t)"
primrec rconsNlist :: "('e,'a::monoid_add) FingerTreeStruc 
     ('e,'a) Node list  ('e,'a) FingerTreeStruc" where
  "rconsNlist t []  = t" |
  "rconsNlist t (x#xs)  = rconsNlist (nrcons t x) xs"

fun nodes :: "('e,'a::monoid_add) Node list   ('e,'a) Node list" where
  "nodes [a, b] = [node2 a b]" |
  "nodes [a, b, c] = [node3 a b c]" |
  "nodes [a,b,c,d] = [node2 a b, node2 c d]" |
  "nodes (a#b#c#xs) = (node3 a b c) # (nodes xs)"


text Recursively we concatenate two FingerTreeStrucs while we keep the 
  inner Nodes in a list
fun app3 :: "('e,'a::monoid_add) FingerTreeStruc  ('e,'a) Node list 
     ('e,'a) FingerTreeStruc  ('e,'a) FingerTreeStruc" where
  "app3 Empty xs t = lconsNlist xs t" |
  "app3 t xs Empty = rconsNlist t xs" |
  "app3 (Single x) xs t = nlcons x (lconsNlist xs t)" |
  "app3 t xs (Single x) = nrcons (rconsNlist t xs) x" |
  "app3 (Deep _ pr1 m1 sf1) ts (Deep _ pr2 m2 sf2) =
    deep pr1 (app3 m1 
      (nodes ((digitToNlist sf1) @ ts @ (digitToNlist pr2))) m2) sf2"

lemma lconsNlist_inv:
  assumes "is_leveln_ftree n t" 
  and "is_measured_ftree t"
  and " xset xs. (is_leveln_node n x  is_measured_node x)"
  shows 
  "is_leveln_ftree n (lconsNlist xs t)  is_measured_ftree (lconsNlist xs t)"
  by (insert assms, induct xs, auto simp add: nlcons_invlevel nlcons_invmeas)

lemma rconsNlist_inv:
  assumes "is_leveln_ftree n t" 
  and "is_measured_ftree t"
  and " xset xs. (is_leveln_node n x  is_measured_node x)"
  shows 
  "is_leveln_ftree n (rconsNlist t xs)  is_measured_ftree (rconsNlist t xs)"
  by (insert assms, induct xs arbitrary: t, 
      auto simp add: nrcons_invlevel nrcons_invmeas)

lemma nodes_inv:
  assumes " x  set ts. is_leveln_node n x  is_measured_node x"
  and "length ts  2"
  shows " x  set (nodes ts). is_leveln_node (Suc n) x  is_measured_node x"
proof (insert assms, induct ts rule: nodes.induct)
  case (1 a b)
  thus ?case by (simp add: node2_def)
next
  case (2 a b c)
  thus ?case by (simp add: node3_def)
next
  case (3 a b c d)
  thus ?case by (simp add: node2_def)
next
  case (4 a b c v vb vc)
  thus ?case by (simp add: node3_def)
next
  show "xset []. is_leveln_node n x  is_measured_node x; 2  length []
     xset (nodes []). is_leveln_node (Suc n) x  is_measured_node x" 
    by  simp
next
  show 
    "v. xset [v]. is_leveln_node n x  is_measured_node x; 2  length [v]
     xset (nodes [v]). is_leveln_node (Suc n) x  is_measured_node x" 
    by simp
qed

lemma nodes_inv2:
  assumes "is_leveln_digit n sf1"
  and "is_measured_digit sf1"
  and "is_leveln_digit n pr2"
  and "is_measured_digit pr2"
  and " x  set ts. is_leveln_node n x  is_measured_node x"
  shows 
  "xset (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)).
                is_leveln_node (Suc n) x  is_measured_node x" 
proof -
  have v1:" xset (digitToNlist sf1 @ ts @ digitToNlist pr2). 
                 is_leveln_node n x  is_measured_node x" 
    using assms
    apply (simp add: digitToNlist_def)
    apply (cases sf1)
    apply (cases pr2)
    apply simp_all
    apply (cases pr2)
    apply (simp_all)
    apply (cases pr2)
    apply (simp_all)
    apply (cases pr2)
    apply (simp_all)
    done
  have v2: "length (digitToNlist sf1 @ ts @ digitToNlist pr2)  2"
    apply (cases sf1)
    apply (cases pr2)
    apply simp_all
    done
  thus ?thesis 
    using v1 nodes_inv[of "digitToNlist sf1 @ ts @ digitToNlist pr2"] 
    by blast
qed

lemma app3_inv:
  assumes "is_leveln_ftree n t1"
  and "is_leveln_ftree n t2"
  and "is_measured_ftree t1"
  and "is_measured_ftree t2"
  and " xset xs. (is_leveln_node n x  is_measured_node x)"
  shows "is_leveln_ftree n (app3 t1 xs t2)  is_measured_ftree (app3 t1 xs t2)"
proof (insert assms, induct t1 xs t2 arbitrary: n rule: app3.induct)
  case (1 xs t n)
  thus ?case using lconsNlist_inv by simp
next
  case "2_1" 
  thus ?case by (simp add: rconsNlist_inv)
next
  case "2_2"
  thus ?case by (simp add: lconsNlist_inv rconsNlist_inv)
next
  case "3_1"
  thus ?case by (simp add: lconsNlist_inv nlcons_invlevel nlcons_invmeas )
next
  case "3_2"
  thus ?case 
    by (simp only: app3.simps) 
       (simp add: lconsNlist_inv nlcons_invlevel nlcons_invmeas)
next
  case 4
  thus ?case 
    by (simp only: app3.simps)
       (simp add: rconsNlist_inv nrcons_invlevel nrcons_invmeas)
next
  case (5 uu pr1 m1 sf1 ts uv pr2 m2 sf2 n)
  thus ?case
  proof -
    have v1: "is_leveln_ftree (Suc n) m1" 
      and v2: "is_leveln_ftree (Suc n) m2"
      using "5.prems" by (simp_all add: is_leveln_ftree_def)
    have v3: "is_measured_ftree m1" 
      and v4: "is_measured_ftree m2"
      using "5.prems" by (simp_all add: is_measured_ftree_def)
    have v5: "is_leveln_digit n sf1"
      "is_measured_digit sf1"
      "is_leveln_digit n pr2"
      "is_measured_digit pr2"
      "xset ts. is_leveln_node n x  is_measured_node x"
      using "5.prems"
      by (simp_all add: is_leveln_ftree_def is_measured_ftree_def)
    note v6 = nodes_inv2[OF v5]
    note v7 = "5.hyps"[OF v1 v2 v3 v4 v6]
    have v8: "is_leveln_digit n sf2"
      "is_measured_digit sf2"
      "is_leveln_digit n pr1"
      "is_measured_digit pr1"
      using "5.prems"
      by (simp_all add: is_leveln_ftree_def is_measured_ftree_def)
    
    show ?thesis using v7 v8
      by (simp add: is_leveln_ftree_def is_measured_ftree_def deep_def)
  qed
qed

primrec nlistToList:: "(('e, 'a) Node) list  ('e × 'a) list" where
  "nlistToList [] = []"|
  "nlistToList (x#xs) = (nodeToList x) @ (nlistToList xs)"

lemma nodes_list: "length xs  2  nlistToList (nodes xs) = nlistToList xs"
  by (induct xs rule: nodes.induct) (auto simp add: node2_def node3_def)

lemma nlistToList_app: 
  "nlistToList (xs@ys) = (nlistToList xs) @ (nlistToList ys)"
  by (induct xs arbitrary: ys, simp_all)

lemma nlistListLCons: "toList (lconsNlist xs t) = (nlistToList xs) @ (toList t)"
  by (induct xs) (auto simp add: nlcons_list)
 
lemma nlistListRCons: "toList (rconsNlist t xs) = (toList t) @ (nlistToList xs)"
  by (induct xs arbitrary: t) (auto simp add: nrcons_list)

lemma app3_list_lem1: 
  "nlistToList (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) =
       digitToList sf1 @ nlistToList ts @ digitToList pr2"
proof -
  have len1: "length (digitToNlist sf1 @ ts @ digitToNlist pr2)  2"
    by (cases sf1,cases pr2,simp_all)
  
  have "(nlistToList (digitToNlist sf1 @ ts @ digitToNlist pr2)) 
       = (digitToList sf1 @ nlistToList ts @ digitToList pr2)"
    apply (cases sf1, cases pr2) 
    apply (simp_all add: nlistToList_app)
    apply (cases pr2, auto)
    apply (cases pr2, auto)
    apply (cases pr2, auto)
    done
  with nodes_list[OF len1] show ?thesis by simp
qed


lemma app3_list: 
  "toList (app3 t1 xs t2) = (toList t1) @ (nlistToList xs) @ (toList t2)"
  apply (induct t1 xs t2 rule: app3.induct)
  apply (simp_all add: nlistListLCons nlistListRCons nlcons_list nrcons_list)
  apply (simp add: app3_list_lem1 deep_def)
  done


definition app 
  :: "('e,'a::monoid_add) FingerTreeStruc  ('e,'a) FingerTreeStruc 
        ('e,'a) FingerTreeStruc" 
  where "app t1 t2 = app3 t1 [] t2"

lemma app_correct: 
  assumes "ft_invar t1" "ft_invar t2" 
  shows "toList (app t1 t2) = (toList t1) @ (toList t2)" 
    and "ft_invar (app t1 t2)"
  using assms
  by (auto simp add: app3_inv app3_list ft_invar_def app_def)

lemma app_inv: "ft_invar t1;ft_invar t2  ft_invar (app t1 t2)"
  by (auto simp add: app3_inv ft_invar_def app_def)

lemma app_list[simp]: "toList (app t1 t2) = (toList t1) @ (toList t2)"
  by (simp add: app3_list app_def)


subsubsection "Splitting"

type_synonym ('e,'a) SplitDigit = 
  "('e,'a) Node list  × ('e,'a) Node × ('e,'a) Node list"
type_synonym ('e,'a) SplitTree  = 
  "('e,'a) FingerTreeStruc × ('e,'a) Node × ('e,'a) FingerTreeStruc"

  text Auxiliary functions to create a correct finger tree 
    even if the left or right digit is empty 
fun deepL :: "('e,'a::monoid_add) Node list  ('e,'a) FingerTreeStruc 
     ('e,'a) Digit  ('e,'a) FingerTreeStruc" where
  "deepL [] m sf = (case (viewLn m) of None  digitToTree sf |
                                 (Some (a, m2))  deep (nodeToDigit a) m2 sf)" |
  "deepL pr m sf = deep (nlistToDigit pr) m sf"
fun deepR :: "('e,'a::monoid_add) Digit  ('e,'a) FingerTreeStruc 
     ('e,'a) Node list  ('e,'a) FingerTreeStruc" where
  "deepR pr m [] = (case (viewRn m) of None  digitToTree pr |
                                 (Some (a, m2))  deep pr m2 (nodeToDigit a))" |
  "deepR pr m sf = deep pr m (nlistToDigit sf)"

  text Splitting a list of nodes
fun splitNlist :: "('a::monoid_add  bool)  'a  ('e,'a) Node list 
     ('e,'a) SplitDigit" where
  "splitNlist p i [a]   = ([],a,[])" |
  "splitNlist p i (a#b) = 
    (let i2 = (i + gmn a) in 
      (if (p i2) 
        then ([],a,b) 
        else 
         (let (l,x,r) = (splitNlist p i2 b) in ((a#l),x,r))))" 

  text Splitting a digit by converting it into a list of nodes
definition splitDigit :: "('a::monoid_add  bool)  'a  ('e,'a) Digit 
     ('e,'a) SplitDigit" where
  "splitDigit p i d = splitNlist p i (digitToNlist d)" 

  text Creating a finger tree from list of nodes
definition nlistToTree :: "('e,'a::monoid_add) Node list 
     ('e,'a) FingerTreeStruc" where 
  "nlistToTree xs = lconsNlist xs Empty"

    text Recursive splitting into a left and right tree and a center node
fun nsplitTree :: "('a::monoid_add  bool)  'a  ('e,'a) FingerTreeStruc 
     ('e,'a) SplitTree" where
  "nsplitTree p i Empty = (Empty, Tip undefined undefined, Empty)" 
      ― ‹Making the function total |
  "nsplitTree p i (Single ea) = (Empty,ea,Empty)" |
  "nsplitTree p i (Deep _ pr m sf) = 
     (let 
       vpr = (i + gmd pr); 
       vm = (vpr + gmft m) 
      in 
        if (p vpr) then 
          (let (l,x,r) = (splitDigit p i pr) in 
            (nlistToTree l,x,deepL r m sf)) 
        else (if (p vm) then 
          (let (ml,xs,mr) = (nsplitTree p vpr m); 
            (l,x,r) = (splitDigit p (vpr + gmft ml) (nodeToDigit xs)) in
              (deepR pr ml l,x,deepL r mr sf))
        else 
          (let (l,x,r) = (splitDigit p vm sf) in 
            (deepR pr m l,x,nlistToTree r))    
      ))"


lemma nlistToTree_inv: 
  " x  set nl. is_measured_node x  is_measured_ftree (nlistToTree nl)"
  " x  set nl. is_leveln_node n x  is_leveln_ftree n (nlistToTree nl)"
  by (unfold nlistToTree_def, induct nl, auto simp add: nlcons_invmeas)
     (induct nl, auto simp add: nlcons_invlevel)

lemma nlistToTree_list: "toList (nlistToTree nl) = nlistToList nl"
  by (auto simp add: nlistToTree_def nlistListLCons)

lemma deepL_inv:
  assumes "is_leveln_ftree (Suc n) m  is_measured_ftree m"
  and "is_leveln_digit n sf  is_measured_digit sf"
  and " x  set pr. (is_measured_node x  is_leveln_node n x)  length pr  4"
  shows  "is_leveln_ftree n (deepL pr m sf)  is_measured_ftree (deepL pr m sf)"
  apply (insert assms)
  apply (induct "pr" m sf rule: deepL.induct)
  apply (simp split: viewnres_split)
  apply auto[1]
  apply (simp_all add: digitToTree_inv deep_def)
proof -
  fix m sf Node FingerTreeStruc
  assume "is_leveln_ftree (Suc n) m" "is_measured_ftree m" 
         "is_leveln_digit n sf" "is_measured_digit sf" 
         "viewLn m = Some (Node, FingerTreeStruc)"
  thus "is_leveln_digit n (nodeToDigit Node) 
         is_leveln_ftree (Suc n) FingerTreeStruc"
    by (simp add: viewLn_inv[of m "Suc n" Node FingerTreeStruc] nodeToDigit_inv)
next
  fix m sf Node FingerTreeStruc
  assume assms1: 
    "is_leveln_ftree (Suc n) m" "is_measured_ftree m" 
    "is_leveln_digit n sf" "is_measured_digit sf" 
    "viewLn m = Some (Node, FingerTreeStruc)"
  thus "is_measured_digit (nodeToDigit Node)  is_measured_ftree FingerTreeStruc"
    apply (auto simp only: viewLn_inv[of m "Suc n" Node FingerTreeStruc])
  proof -
    from assms1 have "is_measured_node Node  is_leveln_node (Suc n) Node" 
      by (simp add: viewLn_inv[of m "Suc n" Node FingerTreeStruc])
    thus "is_measured_digit (nodeToDigit Node)" 
      by (auto simp add: nodeToDigit_inv)
  qed
next
  fix v va
  assume 
    "is_measured_node v  is_leveln_node n (v:: ('a,'b) Node) 
    length  (va::('a, 'b) Node list)  3  
    (xset va. is_measured_node x  is_leveln_node n x  length va  3)"
  thus "is_leveln_digit n (nlistToDigit (v # va)) 
        is_measured_digit (nlistToDigit (v # va))"
    by(cases "v#va" rule: nlistToDigit.cases,simp_all)
qed

(*corollary deepL_inv':
  assumes "is_leveln_ftree (Suc n) m" "is_measured_ftree m"
  and "is_leveln_digit n sf" "is_measured_digit sf"
  and "∀ x ∈ set pr. (is_measured_node x ∧ is_leveln_node n x)" "length pr ≤ 4"
  shows  "is_leveln_ftree n (deepL pr m sf)" "is_measured_ftree (deepL pr m sf)"
  using assms deepL_inv by blast+
*)
            
lemma nlistToDigit_list:
  assumes "1  length xs  length xs  4"
  shows "digitToList(nlistToDigit xs) = nlistToList xs" 
  by (insert assms, cases xs rule: nlistToDigit.cases,auto)

lemma deepL_list:
  assumes "is_leveln_ftree (Suc n) m  is_measured_ftree m"
  and "is_leveln_digit n sf  is_measured_digit sf"
  and " x  set pr. (is_measured_node x  is_leveln_node n x)  length pr  4"
  shows "toList (deepL pr m sf) = nlistToList pr @ toList m @ digitToList sf"
proof (insert assms, induct "pr" m sf rule: deepL.induct)
  case (1 m sf)
  thus ?case
  proof (auto split: viewnres_split simp add: deep_def)
    assume "viewLn m = None"
    hence "m = Empty" by (metis viewLn_empty)
    hence "toList m = []" by simp
    thus "toList (digitToTree sf) = toList m @ digitToList sf" 
      by (simp add:digitToTree_list)
  next
    fix nd t
    assume "viewLn m = Some (nd, t)" 
      "is_leveln_ftree (Suc n) m" "is_measured_ftree m"
    hence "nodeToList nd @ toList t = toList m" by (metis viewLn_list)
    thus "digitToList (nodeToDigit nd) @ toList t = toList m"
      by (simp add: nodeToDigit_list)
  qed
next
  case (2 v va m sf)
  thus ?case
    apply (unfold deepL.simps)
    apply (simp add: deep_def)
    apply (simp add: nlistToDigit_list)
    done
qed
  
lemma deepR_inv:
  assumes "is_leveln_ftree (Suc n) m  is_measured_ftree m"
  and "is_leveln_digit n pr  is_measured_digit pr"
  and " x  set sf. (is_measured_node x  is_leveln_node n x)  length sf  4"
  shows "is_leveln_ftree n (deepR pr m sf)  is_measured_ftree (deepR pr m sf)"
  apply (insert assms)
  apply (induct "pr" m sf rule: deepR.induct)
  apply (simp split: viewnres_split)
  apply auto[1]
  apply (simp_all add: digitToTree_inv deep_def)
proof -
  fix m "pr" Node FingerTreeStruc  
  assume "is_leveln_ftree (Suc n) m" "is_measured_ftree m" 
         "is_leveln_digit n pr" "is_measured_digit pr"
         "viewRn m = Some (Node, FingerTreeStruc)"
  thus 
    "is_leveln_digit n (nodeToDigit Node) 
     is_leveln_ftree (Suc n) FingerTreeStruc"
    by (simp add: viewRn_inv[of m "Suc n" Node FingerTreeStruc] nodeToDigit_inv)
next
  fix m "pr" Node FingerTreeStruc
  assume assms1: 
    "is_leveln_ftree (Suc n) m" "is_measured_ftree m" 
    "is_leveln_digit n pr" "is_measured_digit pr" 
    "viewRn m = Some (Node, FingerTreeStruc)"
  thus "is_measured_ftree FingerTreeStruc  is_measured_digit (nodeToDigit Node)"
    apply (auto simp only: viewRn_inv[of m "Suc n" Node FingerTreeStruc])
  proof -
    from assms1 have "is_measured_node Node  is_leveln_node (Suc n) Node" 
      by (simp add: viewRn_inv[of m "Suc n" Node FingerTreeStruc])
    thus "is_measured_digit (nodeToDigit Node)" 
      by (auto simp add: nodeToDigit_inv)
  qed
next
  fix v va
  assume 
    "is_measured_node v  is_leveln_node n (v:: ('a,'b) Node) 
    length  (va::('a, 'b) Node list)  3  
    (xset va. is_measured_node x  is_leveln_node n x  length va  3)"
  thus "is_leveln_digit n (nlistToDigit (v # va))  
        is_measured_digit (nlistToDigit (v # va))"
    by(cases "v#va" rule: nlistToDigit.cases,simp_all)
qed
           

lemma deepR_list:
  assumes "is_leveln_ftree (Suc n) m  is_measured_ftree m"
  and "is_leveln_digit n pr  is_measured_digit pr"
  and " x  set sf. (is_measured_node x  is_leveln_node n x)  length sf  4"
  shows "toList (deepR pr m sf) = digitToList pr @ toList m @ nlistToList sf"
proof (insert assms, induct "pr" m sf rule: deepR.induct)
  case (1 "pr" m)
  thus ?case
  proof (auto split: viewnres_split simp add: deep_def)
    assume "viewRn m = None"