[STATEMENT]
lemma viewLn_list: " viewLn t = Some (nd, s)
  \<Longrightarrow> toList t = (nodeToList nd) @ (toList s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. viewLn t = Some (nd, s) \<Longrightarrow> toList t = nodeToList nd @ toList s
[PROOF STEP]
supply [[simproc del: defined_all]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. viewLn t = Some (nd, s) \<Longrightarrow> toList t = nodeToList nd @ toList s
[PROOF STEP]
apply(induct t arbitrary: nd s rule: viewLn.induct)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>nd s. viewLn Empty = Some (nd, s) \<Longrightarrow> toList Empty = nodeToList nd @ toList s
 2. \<And>a nd s. viewLn (Single a) = Some (nd, s) \<Longrightarrow> toList (Single a) = nodeToList nd @ toList s
 3. \<And>uu_ a b m sf nd s. viewLn (Deep uu_ (Two a b) m sf) = Some (nd, s) \<Longrightarrow> toList (Deep uu_ (Two a b) m sf) = nodeToList nd @ toList s
 4. \<And>uv_ a b c m sf nd s. viewLn (Deep uv_ (Three a b c) m sf) = Some (nd, s) \<Longrightarrow> toList (Deep uv_ (Three a b c) m sf) = nodeToList nd @ toList s
 5. \<And>uw_ a b c d m sf nd s. viewLn (Deep uw_ (Four a b c d) m sf) = Some (nd, s) \<Longrightarrow> toList (Deep uw_ (Four a b c d) m sf) = nodeToList nd @ toList s
 6. \<And>ux_ a m sf nd s. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; viewLn (Deep ux_ (One a) m sf) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ (One a) m sf) = nodeToList nd @ toList s
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a nd s. viewLn (Single a) = Some (nd, s) \<Longrightarrow> toList (Single a) = nodeToList nd @ toList s
 2. \<And>uu_ a b m sf nd s. viewLn (Deep uu_ (Two a b) m sf) = Some (nd, s) \<Longrightarrow> toList (Deep uu_ (Two a b) m sf) = nodeToList nd @ toList s
 3. \<And>uv_ a b c m sf nd s. viewLn (Deep uv_ (Three a b c) m sf) = Some (nd, s) \<Longrightarrow> toList (Deep uv_ (Three a b c) m sf) = nodeToList nd @ toList s
 4. \<And>uw_ a b c d m sf nd s. viewLn (Deep uw_ (Four a b c d) m sf) = Some (nd, s) \<Longrightarrow> toList (Deep uw_ (Four a b c d) m sf) = nodeToList nd @ toList s
 5. \<And>ux_ a m sf nd s. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; viewLn (Deep ux_ (One a) m sf) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ (One a) m sf) = nodeToList nd @ toList s
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>uu_ a b m sf nd s. viewLn (Deep uu_ (Two a b) m sf) = Some (nd, s) \<Longrightarrow> toList (Deep uu_ (Two a b) m sf) = nodeToList nd @ toList s
 2. \<And>uv_ a b c m sf nd s. viewLn (Deep uv_ (Three a b c) m sf) = Some (nd, s) \<Longrightarrow> toList (Deep uv_ (Three a b c) m sf) = nodeToList nd @ toList s
 3. \<And>uw_ a b c d m sf nd s. viewLn (Deep uw_ (Four a b c d) m sf) = Some (nd, s) \<Longrightarrow> toList (Deep uw_ (Four a b c d) m sf) = nodeToList nd @ toList s
 4. \<And>ux_ a m sf nd s. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; viewLn (Deep ux_ (One a) m sf) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ (One a) m sf) = nodeToList nd @ toList s
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b m sf nd s. a = nd \<and> deep (One b) m sf = s \<Longrightarrow> nodeToList b @ toList m @ digitToList sf = toList s
 2. \<And>uv_ a b c m sf nd s. viewLn (Deep uv_ (Three a b c) m sf) = Some (nd, s) \<Longrightarrow> toList (Deep uv_ (Three a b c) m sf) = nodeToList nd @ toList s
 3. \<And>uw_ a b c d m sf nd s. viewLn (Deep uw_ (Four a b c d) m sf) = Some (nd, s) \<Longrightarrow> toList (Deep uw_ (Four a b c d) m sf) = nodeToList nd @ toList s
 4. \<And>ux_ a m sf nd s. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; viewLn (Deep ux_ (One a) m sf) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ (One a) m sf) = nodeToList nd @ toList s
[PROOF STEP]
apply(simp add: deep_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b m sf nd s. a = nd \<and> Deep (gmn b + gmft m + gmd sf) (One b) m sf = s \<Longrightarrow> nodeToList b @ toList m @ digitToList sf = toList s
 2. \<And>uv_ a b c m sf nd s. viewLn (Deep uv_ (Three a b c) m sf) = Some (nd, s) \<Longrightarrow> toList (Deep uv_ (Three a b c) m sf) = nodeToList nd @ toList s
 3. \<And>uw_ a b c d m sf nd s. viewLn (Deep uw_ (Four a b c d) m sf) = Some (nd, s) \<Longrightarrow> toList (Deep uw_ (Four a b c d) m sf) = nodeToList nd @ toList s
 4. \<And>ux_ a m sf nd s. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; viewLn (Deep ux_ (One a) m sf) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ (One a) m sf) = nodeToList nd @ toList s
[PROOF STEP]
apply(auto simp add: toList_def)[1]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>uv_ a b c m sf nd s. viewLn (Deep uv_ (Three a b c) m sf) = Some (nd, s) \<Longrightarrow> toList (Deep uv_ (Three a b c) m sf) = nodeToList nd @ toList s
 2. \<And>uw_ a b c d m sf nd s. viewLn (Deep uw_ (Four a b c d) m sf) = Some (nd, s) \<Longrightarrow> toList (Deep uw_ (Four a b c d) m sf) = nodeToList nd @ toList s
 3. \<And>ux_ a m sf nd s. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; viewLn (Deep ux_ (One a) m sf) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ (One a) m sf) = nodeToList nd @ toList s
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b c m sf nd s. a = nd \<and> deep (Two b c) m sf = s \<Longrightarrow> nodeToList b @ nodeToList c @ toList m @ digitToList sf = toList s
 2. \<And>uw_ a b c d m sf nd s. viewLn (Deep uw_ (Four a b c d) m sf) = Some (nd, s) \<Longrightarrow> toList (Deep uw_ (Four a b c d) m sf) = nodeToList nd @ toList s
 3. \<And>ux_ a m sf nd s. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; viewLn (Deep ux_ (One a) m sf) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ (One a) m sf) = nodeToList nd @ toList s
[PROOF STEP]
apply(simp add: deep_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b c m sf nd s. a = nd \<and> Deep (gmn b + gmn c + gmft m + gmd sf) (Two b c) m sf = s \<Longrightarrow> nodeToList b @ nodeToList c @ toList m @ digitToList sf = toList s
 2. \<And>uw_ a b c d m sf nd s. viewLn (Deep uw_ (Four a b c d) m sf) = Some (nd, s) \<Longrightarrow> toList (Deep uw_ (Four a b c d) m sf) = nodeToList nd @ toList s
 3. \<And>ux_ a m sf nd s. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; viewLn (Deep ux_ (One a) m sf) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ (One a) m sf) = nodeToList nd @ toList s
[PROOF STEP]
apply(auto simp add: toList_def)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>uw_ a b c d m sf nd s. viewLn (Deep uw_ (Four a b c d) m sf) = Some (nd, s) \<Longrightarrow> toList (Deep uw_ (Four a b c d) m sf) = nodeToList nd @ toList s
 2. \<And>ux_ a m sf nd s. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; viewLn (Deep ux_ (One a) m sf) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ (One a) m sf) = nodeToList nd @ toList s
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c d m sf nd s. a = nd \<and> deep (Three b c d) m sf = s \<Longrightarrow> nodeToList b @ nodeToList c @ nodeToList d @ toList m @ digitToList sf = toList s
 2. \<And>ux_ a m sf nd s. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; viewLn (Deep ux_ (One a) m sf) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ (One a) m sf) = nodeToList nd @ toList s
[PROOF STEP]
apply(simp add: deep_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c d m sf nd s. a = nd \<and> Deep (gmn b + gmn c + gmn d + gmft m + gmd sf) (Three b c d) m sf = s \<Longrightarrow> nodeToList b @ nodeToList c @ nodeToList d @ toList m @ digitToList sf = toList s
 2. \<And>ux_ a m sf nd s. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; viewLn (Deep ux_ (One a) m sf) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ (One a) m sf) = nodeToList nd @ toList s
[PROOF STEP]
apply(auto simp add: toList_def)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ux_ a m sf nd s. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; viewLn (Deep ux_ (One a) m sf) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ (One a) m sf) = nodeToList nd @ toList s
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a m sf nd s. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; (case viewLn m of None \<Rightarrow> Some (a, digitToTree sf) | Some (b, m2) \<Rightarrow> Some (a, deep (nodeToDigit b) m2 sf)) = Some (nd, s)\<rbrakk> \<Longrightarrow> nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s
[PROOF STEP]
subgoal premises prems for a m sf nd s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s
[PROOF STEP]
using prems
[PROOF STATE]
proof (prove)
using this:
viewLn m = Some (?nd, ?s) \<Longrightarrow> toList m = nodeToList ?nd @ toList ?s
(case viewLn m of None \<Rightarrow> Some (a, digitToTree sf) | Some (b, m2) \<Rightarrow> Some (a, deep (nodeToDigit b) m2 sf)) = Some (nd, s)

goal (1 subgoal):
 1. nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s
[PROOF STEP]
proof (cases "viewLn m" rule: viewnres_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; (case viewLn m of None \<Rightarrow> Some (a, digitToTree sf) | Some (b, m2) \<Rightarrow> Some (a, deep (nodeToDigit b) m2 sf)) = Some (nd, s); viewLn m = None\<rbrakk> \<Longrightarrow> nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s
 2. \<And>aa t. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; (case viewLn m of None \<Rightarrow> Some (a, digitToTree sf) | Some (b, m2) \<Rightarrow> Some (a, deep (nodeToDigit b) m2 sf)) = Some (nd, s); viewLn m = Some (aa, t)\<rbrakk> \<Longrightarrow> nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
viewLn m = None

goal (2 subgoals):
 1. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; (case viewLn m of None \<Rightarrow> Some (a, digitToTree sf) | Some (b, m2) \<Rightarrow> Some (a, deep (nodeToDigit b) m2 sf)) = Some (nd, s); viewLn m = None\<rbrakk> \<Longrightarrow> nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s
 2. \<And>aa t. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; (case viewLn m of None \<Rightarrow> Some (a, digitToTree sf) | Some (b, m2) \<Rightarrow> Some (a, deep (nodeToDigit b) m2 sf)) = Some (nd, s); viewLn m = Some (aa, t)\<rbrakk> \<Longrightarrow> nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s
[PROOF STEP]
hence av: "m = Empty"
[PROOF STATE]
proof (prove)
using this:
viewLn m = None

goal (1 subgoal):
 1. m = Empty
[PROOF STEP]
by (metis viewLn_empty)
[PROOF STATE]
proof (state)
this:
m = Empty

goal (2 subgoals):
 1. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; (case viewLn m of None \<Rightarrow> Some (a, digitToTree sf) | Some (b, m2) \<Rightarrow> Some (a, deep (nodeToDigit b) m2 sf)) = Some (nd, s); viewLn m = None\<rbrakk> \<Longrightarrow> nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s
 2. \<And>aa t. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; (case viewLn m of None \<Rightarrow> Some (a, digitToTree sf) | Some (b, m2) \<Rightarrow> Some (a, deep (nodeToDigit b) m2 sf)) = Some (nd, s); viewLn m = Some (aa, t)\<rbrakk> \<Longrightarrow> nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s
[PROOF STEP]
from av prems
[PROOF STATE]
proof (chain)
picking this:
m = Empty
viewLn m = Some (?nd, ?s) \<Longrightarrow> toList m = nodeToList ?nd @ toList ?s
(case viewLn m of None \<Rightarrow> Some (a, digitToTree sf) | Some (b, m2) \<Rightarrow> Some (a, deep (nodeToDigit b) m2 sf)) = Some (nd, s)
[PROOF STEP]
show "nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s"
[PROOF STATE]
proof (prove)
using this:
m = Empty
viewLn m = Some (?nd, ?s) \<Longrightarrow> toList m = nodeToList ?nd @ toList ?s
(case viewLn m of None \<Rightarrow> Some (a, digitToTree sf) | Some (b, m2) \<Rightarrow> Some (a, deep (nodeToDigit b) m2 sf)) = Some (nd, s)

goal (1 subgoal):
 1. nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s
[PROOF STEP]
by (auto simp add: digitToTree_list)
[PROOF STATE]
proof (state)
this:
nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s

goal (1 subgoal):
 1. \<And>aa t. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; (case viewLn m of None \<Rightarrow> Some (a, digitToTree sf) | Some (b, m2) \<Rightarrow> Some (a, deep (nodeToDigit b) m2 sf)) = Some (nd, s); viewLn m = Some (aa, t)\<rbrakk> \<Longrightarrow> nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa t. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; (case viewLn m of None \<Rightarrow> Some (a, digitToTree sf) | Some (b, m2) \<Rightarrow> Some (a, deep (nodeToDigit b) m2 sf)) = Some (nd, s); viewLn m = Some (aa, t)\<rbrakk> \<Longrightarrow> nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s
[PROOF STEP]
case (Cons b m2)
[PROOF STATE]
proof (state)
this:
viewLn m = Some (b, m2)

goal (1 subgoal):
 1. \<And>aa t. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; (case viewLn m of None \<Rightarrow> Some (a, digitToTree sf) | Some (b, m2) \<Rightarrow> Some (a, deep (nodeToDigit b) m2 sf)) = Some (nd, s); viewLn m = Some (aa, t)\<rbrakk> \<Longrightarrow> nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
viewLn m = Some (?nd, ?s) \<Longrightarrow> toList m = nodeToList ?nd @ toList ?s
(case viewLn m of None \<Rightarrow> Some (a, digitToTree sf) | Some (b, m2) \<Rightarrow> Some (a, deep (nodeToDigit b) m2 sf)) = Some (nd, s)
viewLn m = Some (b, m2)
[PROOF STEP]
have bv: "nd = a" "s = (deep (nodeToDigit b) m2 sf)"
[PROOF STATE]
proof (prove)
using this:
viewLn m = Some (?nd, ?s) \<Longrightarrow> toList m = nodeToList ?nd @ toList ?s
(case viewLn m of None \<Rightarrow> Some (a, digitToTree sf) | Some (b, m2) \<Rightarrow> Some (a, deep (nodeToDigit b) m2 sf)) = Some (nd, s)
viewLn m = Some (b, m2)

goal (1 subgoal):
 1. nd = a &&& s = deep (nodeToDigit b) m2 sf
[PROOF STEP]
by (auto simp add: deep_def)
[PROOF STATE]
proof (state)
this:
nd = a
s = deep (nodeToDigit b) m2 sf

goal (1 subgoal):
 1. \<And>aa t. \<lbrakk>\<And>nd s. viewLn m = Some (nd, s) \<Longrightarrow> toList m = nodeToList nd @ toList s; (case viewLn m of None \<Rightarrow> Some (a, digitToTree sf) | Some (b, m2) \<Rightarrow> Some (a, deep (nodeToDigit b) m2 sf)) = Some (nd, s); viewLn m = Some (aa, t)\<rbrakk> \<Longrightarrow> nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s
[PROOF STEP]
with Cons prems
[PROOF STATE]
proof (chain)
picking this:
viewLn m = Some (b, m2)
viewLn m = Some (?nd, ?s) \<Longrightarrow> toList m = nodeToList ?nd @ toList ?s
(case viewLn m of None \<Rightarrow> Some (a, digitToTree sf) | Some (b, m2) \<Rightarrow> Some (a, deep (nodeToDigit b) m2 sf)) = Some (nd, s)
nd = a
s = deep (nodeToDigit b) m2 sf
[PROOF STEP]
show "nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s"
[PROOF STATE]
proof (prove)
using this:
viewLn m = Some (b, m2)
viewLn m = Some (?nd, ?s) \<Longrightarrow> toList m = nodeToList ?nd @ toList ?s
(case viewLn m of None \<Rightarrow> Some (a, digitToTree sf) | Some (b, m2) \<Rightarrow> Some (a, deep (nodeToDigit b) m2 sf)) = Some (nd, s)
nd = a
s = deep (nodeToDigit b) m2 sf

goal (1 subgoal):
 1. nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>viewLn m = Some (b, m2); \<And>nd s. b = nd \<and> m2 = s \<Longrightarrow> toList m = nodeToList nd @ toList s; nd = a; s = deep (nodeToDigit b) m2 sf\<rbrakk> \<Longrightarrow> nodeToList b @ toList m2 @ digitToList sf = toList (deep (nodeToDigit b) m2 sf)
[PROOF STEP]
apply(simp add: deep_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>viewLn m = Some (b, m2); \<And>nd s. b = nd \<and> m2 = s \<Longrightarrow> toList m = nodeToList nd @ toList s; nd = a; s = Deep (gmd (nodeToDigit b) + gmft m2 + gmd sf) (nodeToDigit b) m2 sf\<rbrakk> \<Longrightarrow> nodeToList b = digitToList (nodeToDigit b)
[PROOF STEP]
apply(simp add: deep_def nodeToDigit_list)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
nodeToList a @ toList m @ digitToList sf = nodeToList nd @ toList s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma viewRn_empty: "t \<noteq> Empty \<longleftrightarrow> (viewRn t) \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t \<noteq> Empty) = (viewRn t \<noteq> None)
[PROOF STEP]
proof (cases t)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. t = Empty \<Longrightarrow> (t \<noteq> Empty) = (viewRn t \<noteq> None)
 2. \<And>x2. t = Single x2 \<Longrightarrow> (t \<noteq> Empty) = (viewRn t \<noteq> None)
 3. \<And>x31 x32 x33 x34. t = Deep x31 x32 x33 x34 \<Longrightarrow> (t \<noteq> Empty) = (viewRn t \<noteq> None)
[PROOF STEP]
case Empty
[PROOF STATE]
proof (state)
this:
t = Empty

goal (3 subgoals):
 1. t = Empty \<Longrightarrow> (t \<noteq> Empty) = (viewRn t \<noteq> None)
 2. \<And>x2. t = Single x2 \<Longrightarrow> (t \<noteq> Empty) = (viewRn t \<noteq> None)
 3. \<And>x31 x32 x33 x34. t = Deep x31 x32 x33 x34 \<Longrightarrow> (t \<noteq> Empty) = (viewRn t \<noteq> None)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
t = Empty

goal (1 subgoal):
 1. (t \<noteq> Empty) = (viewRn t \<noteq> None)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(t \<noteq> Empty) = (viewRn t \<noteq> None)

goal (2 subgoals):
 1. \<And>x2. t = Single x2 \<Longrightarrow> (t \<noteq> Empty) = (viewRn t \<noteq> None)
 2. \<And>x31 x32 x33 x34. t = Deep x31 x32 x33 x34 \<Longrightarrow> (t \<noteq> Empty) = (viewRn t \<noteq> None)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x2. t = Single x2 \<Longrightarrow> (t \<noteq> Empty) = (viewRn t \<noteq> None)
 2. \<And>x31 x32 x33 x34. t = Deep x31 x32 x33 x34 \<Longrightarrow> (t \<noteq> Empty) = (viewRn t \<noteq> None)
[PROOF STEP]
case (Single Node)
[PROOF STATE]
proof (state)
this:
t = Single Node

goal (2 subgoals):
 1. \<And>x2. t = Single x2 \<Longrightarrow> (t \<noteq> Empty) = (viewRn t \<noteq> None)
 2. \<And>x31 x32 x33 x34. t = Deep x31 x32 x33 x34 \<Longrightarrow> (t \<noteq> Empty) = (viewRn t \<noteq> None)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
t = Single Node

goal (1 subgoal):
 1. (t \<noteq> Empty) = (viewRn t \<noteq> None)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(t \<noteq> Empty) = (viewRn t \<noteq> None)

goal (1 subgoal):
 1. \<And>x31 x32 x33 x34. t = Deep x31 x32 x33 x34 \<Longrightarrow> (t \<noteq> Empty) = (viewRn t \<noteq> None)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x31 x32 x33 x34. t = Deep x31 x32 x33 x34 \<Longrightarrow> (t \<noteq> Empty) = (viewRn t \<noteq> None)
[PROOF STEP]
case (Deep a l x r)
[PROOF STATE]
proof (state)
this:
t = Deep a l x r

goal (1 subgoal):
 1. \<And>x31 x32 x33 x34. t = Deep x31 x32 x33 x34 \<Longrightarrow> (t \<noteq> Empty) = (viewRn t \<noteq> None)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
t = Deep a l x r

goal (1 subgoal):
 1. (t \<noteq> Empty) = (viewRn t \<noteq> None)
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = Deep a l x r \<Longrightarrow> \<exists>aa b. viewRn (Deep a l x r) = Some (aa, b)
[PROOF STEP]
apply(case_tac r)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1. \<lbrakk>t = Deep a l x r; r = One x1\<rbrakk> \<Longrightarrow> \<exists>aa b. viewRn (Deep a l x r) = Some (aa, b)
 2. \<And>x21 x22. \<lbrakk>t = Deep a l x r; r = Two x21 x22\<rbrakk> \<Longrightarrow> \<exists>aa b. viewRn (Deep a l x r) = Some (aa, b)
 3. \<And>x31 x32 x33. \<lbrakk>t = Deep a l x r; r = Three x31 x32 x33\<rbrakk> \<Longrightarrow> \<exists>aa b. viewRn (Deep a l x r) = Some (aa, b)
 4. \<And>x41 x42 x43 x44. \<lbrakk>t = Deep a l x r; r = Four x41 x42 x43 x44\<rbrakk> \<Longrightarrow> \<exists>aa b. viewRn (Deep a l x r) = Some (aa, b)
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1. \<lbrakk>t = Deep a l x (One x1); r = One x1\<rbrakk> \<Longrightarrow> \<exists>a b. (case viewRn x of None \<Rightarrow> Some (x1, digitToTree l) | Some (b, m2) \<Rightarrow> Some (x1, deep l m2 (nodeToDigit b))) = Some (a, b)
[PROOF STEP]
apply(cases "viewRn x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>t = Deep a l x (One x1); r = One x1; viewRn x = None\<rbrakk> \<Longrightarrow> \<exists>a b. (case viewRn x of None \<Rightarrow> Some (x1, digitToTree l) | Some (b, m2) \<Rightarrow> Some (x1, deep l m2 (nodeToDigit b))) = Some (a, b)
 2. \<And>x1 aa. \<lbrakk>t = Deep a l x (One x1); r = One x1; viewRn x = Some aa\<rbrakk> \<Longrightarrow> \<exists>a b. (case viewRn x of None \<Rightarrow> Some (x1, digitToTree l) | Some (b, m2) \<Rightarrow> Some (x1, deep l m2 (nodeToDigit b))) = Some (a, b)
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(t \<noteq> Empty) = (viewRn t \<noteq> None)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma viewRn_inv: "\<lbrakk>
  is_measured_ftree t; is_leveln_ftree n t; viewRn t = Some (nd, s)
  \<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and>
       is_leveln_ftree n s \<and> is_leveln_node n nd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_measured_ftree t; is_leveln_ftree n t; viewRn t = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
apply(induct t arbitrary: n nd s rule: viewRn.induct)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>n nd s. \<lbrakk>is_measured_ftree Empty; is_leveln_ftree n Empty; viewRn Empty = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
 2. \<And>a n nd s. \<lbrakk>is_measured_ftree (Single a); is_leveln_ftree n (Single a); viewRn (Single a) = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
 3. \<And>uu_ pr m a b n nd s. \<lbrakk>is_measured_ftree (Deep uu_ pr m (Two a b)); is_leveln_ftree n (Deep uu_ pr m (Two a b)); viewRn (Deep uu_ pr m (Two a b)) = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
 4. \<And>uv_ pr m a b c n nd s. \<lbrakk>is_measured_ftree (Deep uv_ pr m (Three a b c)); is_leveln_ftree n (Deep uv_ pr m (Three a b c)); viewRn (Deep uv_ pr m (Three a b c)) = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
 5. \<And>uw_ pr m a b c d n nd s. \<lbrakk>is_measured_ftree (Deep uw_ pr m (Four a b c d)); is_leveln_ftree n (Deep uw_ pr m (Four a b c d)); viewRn (Deep uw_ pr m (Four a b c d)) = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
 6. \<And>ux_ pr m a n nd s. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
apply(simp add: viewRn_empty)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a n nd s. \<lbrakk>is_measured_ftree (Single a); is_leveln_ftree n (Single a); viewRn (Single a) = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
 2. \<And>uu_ pr m a b n nd s. \<lbrakk>is_measured_ftree (Deep uu_ pr m (Two a b)); is_leveln_ftree n (Deep uu_ pr m (Two a b)); viewRn (Deep uu_ pr m (Two a b)) = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
 3. \<And>uv_ pr m a b c n nd s. \<lbrakk>is_measured_ftree (Deep uv_ pr m (Three a b c)); is_leveln_ftree n (Deep uv_ pr m (Three a b c)); viewRn (Deep uv_ pr m (Three a b c)) = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
 4. \<And>uw_ pr m a b c d n nd s. \<lbrakk>is_measured_ftree (Deep uw_ pr m (Four a b c d)); is_leveln_ftree n (Deep uw_ pr m (Four a b c d)); viewRn (Deep uw_ pr m (Four a b c d)) = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
 5. \<And>ux_ pr m a n nd s. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>uu_ pr m a b n nd s. \<lbrakk>is_measured_ftree (Deep uu_ pr m (Two a b)); is_leveln_ftree n (Deep uu_ pr m (Two a b)); viewRn (Deep uu_ pr m (Two a b)) = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
 2. \<And>uv_ pr m a b c n nd s. \<lbrakk>is_measured_ftree (Deep uv_ pr m (Three a b c)); is_leveln_ftree n (Deep uv_ pr m (Three a b c)); viewRn (Deep uv_ pr m (Three a b c)) = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
 3. \<And>uw_ pr m a b c d n nd s. \<lbrakk>is_measured_ftree (Deep uw_ pr m (Four a b c d)); is_leveln_ftree n (Deep uw_ pr m (Four a b c d)); viewRn (Deep uw_ pr m (Four a b c d)) = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
 4. \<And>ux_ pr m a n nd s. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
apply(auto simp add: deep_def)[1]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>uv_ pr m a b c n nd s. \<lbrakk>is_measured_ftree (Deep uv_ pr m (Three a b c)); is_leveln_ftree n (Deep uv_ pr m (Three a b c)); viewRn (Deep uv_ pr m (Three a b c)) = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
 2. \<And>uw_ pr m a b c d n nd s. \<lbrakk>is_measured_ftree (Deep uw_ pr m (Four a b c d)); is_leveln_ftree n (Deep uw_ pr m (Four a b c d)); viewRn (Deep uw_ pr m (Four a b c d)) = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
 3. \<And>ux_ pr m a n nd s. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
apply(auto simp add: deep_def)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>uw_ pr m a b c d n nd s. \<lbrakk>is_measured_ftree (Deep uw_ pr m (Four a b c d)); is_leveln_ftree n (Deep uw_ pr m (Four a b c d)); viewRn (Deep uw_ pr m (Four a b c d)) = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
 2. \<And>ux_ pr m a n nd s. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
apply(auto simp add: deep_def)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ux_ pr m a n nd s. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ux_ pr m a n nd s. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
fix ux a m "pr" n nd s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ux_ pr m a n nd s. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
assume av: "\<And>n nd s.
           \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk>
           \<Longrightarrow> is_measured_ftree s \<and>
              is_measured_node nd \<and> is_leveln_ftree n s \<and> 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)"
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_measured_ftree m; is_leveln_ftree ?n m; viewRn m = Some (?nd, ?s)\<rbrakk> \<Longrightarrow> is_measured_ftree ?s \<and> is_measured_node ?nd \<and> is_leveln_ftree ?n ?s \<and> 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)

goal (1 subgoal):
 1. \<And>ux_ pr m a n nd s. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
thus "is_measured_ftree s \<and>
          is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_measured_ftree m; is_leveln_ftree ?n m; viewRn m = Some (?nd, ?s)\<rbrakk> \<Longrightarrow> is_measured_ftree ?s \<and> is_measured_node ?nd \<and> is_leveln_ftree ?n ?s \<and> 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)

goal (1 subgoal):
 1. is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
proof (cases "viewRn m" rule: viewnres_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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); viewRn m = None\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
 2. \<And>aa t. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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); viewRn m = Some (aa, t)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
viewRn m = None

goal (2 subgoals):
 1. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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); viewRn m = None\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
 2. \<And>aa t. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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); viewRn m = Some (aa, t)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
with av(4)
[PROOF STATE]
proof (chain)
picking this:
viewRn (Deep ux pr m (One a)) = Some (nd, s)
viewRn m = None
[PROOF STEP]
have v1: "nd = a" "s = digitToTree pr"
[PROOF STATE]
proof (prove)
using this:
viewRn (Deep ux pr m (One a)) = Some (nd, s)
viewRn m = None

goal (1 subgoal):
 1. nd = a &&& s = digitToTree pr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nd = a
s = digitToTree pr

goal (2 subgoals):
 1. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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); viewRn m = None\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
 2. \<And>aa t. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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); viewRn m = Some (aa, t)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
from v1 av(2,3)
[PROOF STATE]
proof (chain)
picking this:
nd = a
s = digitToTree pr
is_measured_ftree (Deep ux pr m (One a))
is_leveln_ftree n (Deep ux pr m (One a))
[PROOF STEP]
show "is_measured_ftree s \<and>
       is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd"
[PROOF STATE]
proof (prove)
using this:
nd = a
s = digitToTree pr
is_measured_ftree (Deep ux pr m (One a))
is_leveln_ftree n (Deep ux pr m (One a))

goal (1 subgoal):
 1. is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>nd = a; s = digitToTree pr; is_measured_digit pr; is_leveln_digit n pr; is_measured_ftree m; is_leveln_node n a; is_leveln_ftree (Suc n) m; is_measured_node a; ux = gmd pr + gmft m + gmn a\<rbrakk> \<Longrightarrow> is_measured_ftree (digitToTree pr)
 2. \<lbrakk>nd = a; s = digitToTree pr; is_measured_digit pr; is_leveln_digit n pr; is_measured_ftree m; is_leveln_node n a; is_leveln_ftree (Suc n) m; is_measured_node a; ux = gmd pr + gmft m + gmn a\<rbrakk> \<Longrightarrow> is_leveln_ftree n (digitToTree pr)
[PROOF STEP]
apply(auto simp add: digitToTree_inv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd

goal (1 subgoal):
 1. \<And>aa t. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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); viewRn m = Some (aa, t)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa t. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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); viewRn m = Some (aa, t)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
case (Cons b m2)
[PROOF STATE]
proof (state)
this:
viewRn m = Some (b, m2)

goal (1 subgoal):
 1. \<And>aa t. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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); viewRn m = Some (aa, t)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
with av(4)
[PROOF STATE]
proof (chain)
picking this:
viewRn (Deep ux pr m (One a)) = Some (nd, s)
viewRn m = Some (b, m2)
[PROOF STEP]
have v2: "nd = a" "s = (deep pr m2 (nodeToDigit b))"
[PROOF STATE]
proof (prove)
using this:
viewRn (Deep ux pr m (One a)) = Some (nd, s)
viewRn m = Some (b, m2)

goal (1 subgoal):
 1. nd = a &&& s = deep pr m2 (nodeToDigit b)
[PROOF STEP]
apply (auto simp add: deep_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
nd = a
s = deep pr m2 (nodeToDigit b)

goal (1 subgoal):
 1. \<And>aa t. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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); viewRn m = Some (aa, t)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
note myiv = av(1)[of "Suc n" b m2]
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_measured_ftree m; is_leveln_ftree (Suc n) m; viewRn m = Some (b, m2)\<rbrakk> \<Longrightarrow> is_measured_ftree m2 \<and> is_measured_node b \<and> is_leveln_ftree (Suc n) m2 \<and> is_leveln_node (Suc n) b

goal (1 subgoal):
 1. \<And>aa t. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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); viewRn m = Some (aa, t)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
from v2 av(2,3)
[PROOF STATE]
proof (chain)
picking this:
nd = a
s = deep pr m2 (nodeToDigit b)
is_measured_ftree (Deep ux pr m (One a))
is_leveln_ftree n (Deep ux pr m (One a))
[PROOF STEP]
have "is_measured_ftree m \<and> is_leveln_ftree (Suc n) m"
[PROOF STATE]
proof (prove)
using this:
nd = a
s = deep pr m2 (nodeToDigit b)
is_measured_ftree (Deep ux pr m (One a))
is_leveln_ftree n (Deep ux pr m (One a))

goal (1 subgoal):
 1. is_measured_ftree m \<and> is_leveln_ftree (Suc n) m
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
is_measured_ftree m \<and> is_leveln_ftree (Suc n) m

goal (1 subgoal):
 1. \<And>aa t. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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); viewRn m = Some (aa, t)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
hence bv: "is_measured_ftree m2 \<and>
   is_measured_node b \<and> is_leveln_ftree (Suc n) m2 \<and> is_leveln_node (Suc n) b"
[PROOF STATE]
proof (prove)
using this:
is_measured_ftree m \<and> is_leveln_ftree (Suc n) m

goal (1 subgoal):
 1. is_measured_ftree m2 \<and> is_measured_node b \<and> is_leveln_ftree (Suc n) m2 \<and> is_leveln_node (Suc n) b
[PROOF STEP]
using myiv Cons
[PROOF STATE]
proof (prove)
using this:
is_measured_ftree m \<and> is_leveln_ftree (Suc n) m
\<lbrakk>is_measured_ftree m; is_leveln_ftree (Suc n) m; viewRn m = Some (b, m2)\<rbrakk> \<Longrightarrow> is_measured_ftree m2 \<and> is_measured_node b \<and> is_leveln_ftree (Suc n) m2 \<and> is_leveln_node (Suc n) b
viewRn m = Some (b, m2)

goal (1 subgoal):
 1. is_measured_ftree m2 \<and> is_measured_node b \<and> is_leveln_ftree (Suc n) m2 \<and> is_leveln_node (Suc n) b
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
is_measured_ftree m2 \<and> is_measured_node b \<and> is_leveln_ftree (Suc n) m2 \<and> is_leveln_node (Suc n) b

goal (1 subgoal):
 1. \<And>aa t. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewRn m = Some (nd, s)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> 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); viewRn m = Some (aa, t)\<rbrakk> \<Longrightarrow> is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
with av(2,3) v2
[PROOF STATE]
proof (chain)
picking this:
is_measured_ftree (Deep ux pr m (One a))
is_leveln_ftree n (Deep ux pr m (One a))
nd = a
s = deep pr m2 (nodeToDigit b)
is_measured_ftree m2 \<and> is_measured_node b \<and> is_leveln_ftree (Suc n) m2 \<and> is_leveln_node (Suc n) b
[PROOF STEP]
show "is_measured_ftree s \<and>
          is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd"
[PROOF STATE]
proof (prove)
using this:
is_measured_ftree (Deep ux pr m (One a))
is_leveln_ftree n (Deep ux pr m (One a))
nd = a
s = deep pr m2 (nodeToDigit b)
is_measured_ftree m2 \<and> is_measured_node b \<and> is_leveln_ftree (Suc n) m2 \<and> is_leveln_node (Suc n) b

goal (1 subgoal):
 1. is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd
[PROOF STEP]
apply(auto simp add: deep_def nodeToDigit_inv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_measured_ftree s \<and> is_measured_node nd \<and> is_leveln_ftree n s \<and> is_leveln_node n nd

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma viewRn_list: "viewRn t = Some (nd, s)
  \<Longrightarrow> toList t = (toList s) @ (nodeToList nd)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. viewRn t = Some (nd, s) \<Longrightarrow> toList t = toList s @ nodeToList nd
[PROOF STEP]
supply [[simproc del: defined_all]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. viewRn t = Some (nd, s) \<Longrightarrow> toList t = toList s @ nodeToList nd
[PROOF STEP]
apply(induct t arbitrary: nd s rule: viewRn.induct)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>nd s. viewRn Empty = Some (nd, s) \<Longrightarrow> toList Empty = toList s @ nodeToList nd
 2. \<And>a nd s. viewRn (Single a) = Some (nd, s) \<Longrightarrow> toList (Single a) = toList s @ nodeToList nd
 3. \<And>uu_ pr m a b nd s. viewRn (Deep uu_ pr m (Two a b)) = Some (nd, s) \<Longrightarrow> toList (Deep uu_ pr m (Two a b)) = toList s @ nodeToList nd
 4. \<And>uv_ pr m a b c nd s. viewRn (Deep uv_ pr m (Three a b c)) = Some (nd, s) \<Longrightarrow> toList (Deep uv_ pr m (Three a b c)) = toList s @ nodeToList nd
 5. \<And>uw_ pr m a b c d nd s. viewRn (Deep uw_ pr m (Four a b c d)) = Some (nd, s) \<Longrightarrow> toList (Deep uw_ pr m (Four a b c d)) = toList s @ nodeToList nd
 6. \<And>ux_ pr m a nd s. \<lbrakk>\<And>nd s. viewRn m = Some (nd, s) \<Longrightarrow> toList m = toList s @ nodeToList nd; viewRn (Deep ux_ pr m (One a)) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ pr m (One a)) = toList s @ nodeToList nd
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a nd s. viewRn (Single a) = Some (nd, s) \<Longrightarrow> toList (Single a) = toList s @ nodeToList nd
 2. \<And>uu_ pr m a b nd s. viewRn (Deep uu_ pr m (Two a b)) = Some (nd, s) \<Longrightarrow> toList (Deep uu_ pr m (Two a b)) = toList s @ nodeToList nd
 3. \<And>uv_ pr m a b c nd s. viewRn (Deep uv_ pr m (Three a b c)) = Some (nd, s) \<Longrightarrow> toList (Deep uv_ pr m (Three a b c)) = toList s @ nodeToList nd
 4. \<And>uw_ pr m a b c d nd s. viewRn (Deep uw_ pr m (Four a b c d)) = Some (nd, s) \<Longrightarrow> toList (Deep uw_ pr m (Four a b c d)) = toList s @ nodeToList nd
 5. \<And>ux_ pr m a nd s. \<lbrakk>\<And>nd s. viewRn m = Some (nd, s) \<Longrightarrow> toList m = toList s @ nodeToList nd; viewRn (Deep ux_ pr m (One a)) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ pr m (One a)) = toList s @ nodeToList nd
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>uu_ pr m a b nd s. viewRn (Deep uu_ pr m (Two a b)) = Some (nd, s) \<Longrightarrow> toList (Deep uu_ pr m (Two a b)) = toList s @ nodeToList nd
 2. \<And>uv_ pr m a b c nd s. viewRn (Deep uv_ pr m (Three a b c)) = Some (nd, s) \<Longrightarrow> toList (Deep uv_ pr m (Three a b c)) = toList s @ nodeToList nd
 3. \<And>uw_ pr m a b c d nd s. viewRn (Deep uw_ pr m (Four a b c d)) = Some (nd, s) \<Longrightarrow> toList (Deep uw_ pr m (Four a b c d)) = toList s @ nodeToList nd
 4. \<And>ux_ pr m a nd s. \<lbrakk>\<And>nd s. viewRn m = Some (nd, s) \<Longrightarrow> toList m = toList s @ nodeToList nd; viewRn (Deep ux_ pr m (One a)) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ pr m (One a)) = toList s @ nodeToList nd
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>pr m a b nd s. b = nd \<and> deep pr m (One a) = s \<Longrightarrow> digitToList pr @ toList m @ nodeToList a = toList s
 2. \<And>uv_ pr m a b c nd s. viewRn (Deep uv_ pr m (Three a b c)) = Some (nd, s) \<Longrightarrow> toList (Deep uv_ pr m (Three a b c)) = toList s @ nodeToList nd
 3. \<And>uw_ pr m a b c d nd s. viewRn (Deep uw_ pr m (Four a b c d)) = Some (nd, s) \<Longrightarrow> toList (Deep uw_ pr m (Four a b c d)) = toList s @ nodeToList nd
 4. \<And>ux_ pr m a nd s. \<lbrakk>\<And>nd s. viewRn m = Some (nd, s) \<Longrightarrow> toList m = toList s @ nodeToList nd; viewRn (Deep ux_ pr m (One a)) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ pr m (One a)) = toList s @ nodeToList nd
[PROOF STEP]
apply(simp add: deep_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>pr m a b nd s. b = nd \<and> Deep (gmd pr + gmft m + gmn a) pr m (One a) = s \<Longrightarrow> digitToList pr @ toList m @ nodeToList a = toList s
 2. \<And>uv_ pr m a b c nd s. viewRn (Deep uv_ pr m (Three a b c)) = Some (nd, s) \<Longrightarrow> toList (Deep uv_ pr m (Three a b c)) = toList s @ nodeToList nd
 3. \<And>uw_ pr m a b c d nd s. viewRn (Deep uw_ pr m (Four a b c d)) = Some (nd, s) \<Longrightarrow> toList (Deep uw_ pr m (Four a b c d)) = toList s @ nodeToList nd
 4. \<And>ux_ pr m a nd s. \<lbrakk>\<And>nd s. viewRn m = Some (nd, s) \<Longrightarrow> toList m = toList s @ nodeToList nd; viewRn (Deep ux_ pr m (One a)) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ pr m (One a)) = toList s @ nodeToList nd
[PROOF STEP]
apply(auto simp add: toList_def)[1]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>uv_ pr m a b c nd s. viewRn (Deep uv_ pr m (Three a b c)) = Some (nd, s) \<Longrightarrow> toList (Deep uv_ pr m (Three a b c)) = toList s @ nodeToList nd
 2. \<And>uw_ pr m a b c d nd s. viewRn (Deep uw_ pr m (Four a b c d)) = Some (nd, s) \<Longrightarrow> toList (Deep uw_ pr m (Four a b c d)) = toList s @ nodeToList nd
 3. \<And>ux_ pr m a nd s. \<lbrakk>\<And>nd s. viewRn m = Some (nd, s) \<Longrightarrow> toList m = toList s @ nodeToList nd; viewRn (Deep ux_ pr m (One a)) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ pr m (One a)) = toList s @ nodeToList nd
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>pr m a b c nd s. c = nd \<and> deep pr m (Two a b) = s \<Longrightarrow> digitToList pr @ toList m @ nodeToList a @ nodeToList b = toList s
 2. \<And>uw_ pr m a b c d nd s. viewRn (Deep uw_ pr m (Four a b c d)) = Some (nd, s) \<Longrightarrow> toList (Deep uw_ pr m (Four a b c d)) = toList s @ nodeToList nd
 3. \<And>ux_ pr m a nd s. \<lbrakk>\<And>nd s. viewRn m = Some (nd, s) \<Longrightarrow> toList m = toList s @ nodeToList nd; viewRn (Deep ux_ pr m (One a)) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ pr m (One a)) = toList s @ nodeToList nd
[PROOF STEP]
apply(simp add: deep_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>pr m a b c nd s. c = nd \<and> Deep (gmd pr + gmft m + (gmn a + gmn b)) pr m (Two a b) = s \<Longrightarrow> digitToList pr @ toList m @ nodeToList a @ nodeToList b = toList s
 2. \<And>uw_ pr m a b c d nd s. viewRn (Deep uw_ pr m (Four a b c d)) = Some (nd, s) \<Longrightarrow> toList (Deep uw_ pr m (Four a b c d)) = toList s @ nodeToList nd
 3. \<And>ux_ pr m a nd s. \<lbrakk>\<And>nd s. viewRn m = Some (nd, s) \<Longrightarrow> toList m = toList s @ nodeToList nd; viewRn (Deep ux_ pr m (One a)) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ pr m (One a)) = toList s @ nodeToList nd
[PROOF STEP]
apply(auto simp add: toList_def)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>uw_ pr m a b c d nd s. viewRn (Deep uw_ pr m (Four a b c d)) = Some (nd, s) \<Longrightarrow> toList (Deep uw_ pr m (Four a b c d)) = toList s @ nodeToList nd
 2. \<And>ux_ pr m a nd s. \<lbrakk>\<And>nd s. viewRn m = Some (nd, s) \<Longrightarrow> toList m = toList s @ nodeToList nd; viewRn (Deep ux_ pr m (One a)) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ pr m (One a)) = toList s @ nodeToList nd
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pr m a b c d nd s. d = nd \<and> deep pr m (Three a b c) = s \<Longrightarrow> digitToList pr @ toList m @ nodeToList a @ nodeToList b @ nodeToList c = toList s
 2. \<And>ux_ pr m a nd s. \<lbrakk>\<And>nd s. viewRn m = Some (nd, s) \<Longrightarrow> toList m = toList s @ nodeToList nd; viewRn (Deep ux_ pr m (One a)) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ pr m (One a)) = toList s @ nodeToList nd
[PROOF STEP]
apply(simp add: deep_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pr m a b c d nd s. d = nd \<and> Deep (gmd pr + gmft m + (gmn a + gmn b + gmn c)) pr m (Three a b c) = s \<Longrightarrow> digitToList pr @ toList m @ nodeToList a @ nodeToList b @ nodeToList c = toList s
 2. \<And>ux_ pr m a nd s. \<lbrakk>\<And>nd s. viewRn m = Some (nd, s) \<Longrightarrow> toList m = toList s @ nodeToList nd; viewRn (Deep ux_ pr m (One a)) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ pr m (One a)) = toList s @ nodeToList nd
[PROOF STEP]
apply(auto simp add: toList_def)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ux_ pr m a nd s. \<lbrakk>\<And>nd s. viewRn m = Some (nd, s) \<Longrightarrow> toList m = toList s @ nodeToList nd; viewRn (Deep ux_ pr m (One a)) = Some (nd, s)\<rbrakk> \<Longrightarrow> toList (Deep ux_ pr m (One a)) = toList s @ nodeToList nd
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pr m a nd s. \<lbrakk>\<And>nd s. viewRn m = Some (nd, s) \<Longrightarrow> toList m = toList s @ nodeToList nd; (case viewRn m of None \<Rightarrow> Some (a, digitToTree pr) | Some (b, m2) \<Rightarrow> Some (a, deep pr m2 (nodeToDigit b))) = Some (nd, s)\<rbrakk> \<Longrightarrow> digitToList pr @ toList m @ nodeToList a = toList s @ nodeToList nd
[PROOF STEP]
subgoal premises prems for pr m a nd s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digitToList pr @ toList m @ nodeToList a = toList s @ nodeToList nd
[PROOF STEP]
proof (cases "viewRn m" rule: viewnres_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. viewRn m = None \<Longrightarrow> digitToList pr @ toList m @ nodeToList a = toList s @ nodeToList nd
 2. \<And>aa t. viewRn m = Some (aa, t) \<Longrightarrow> digitToList pr @ toList m @ nodeToList a = toList s @ nodeToList nd
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
viewRn m = None

goal (2 subgoals):
 1. viewRn m = None \<Longrightarrow> digitToList pr @ toList m @ nodeToList a = toList s @ nodeToList nd
 2. \<And>aa t. viewRn m = Some (aa, t) \<Longrightarrow> digitToList pr @ toList m @ nodeToList a = toList s @ nodeToList nd
[PROOF STEP]
from Nil
[PROOF STATE]
proof (chain)
picking this:
viewRn m = None
[PROOF STEP]
have av: "m = Empty"
[PROOF STATE]
proof (prove)
using this:
viewRn m = None

goal (1 subgoal):
 1. m = Empty
[PROOF STEP]
by (metis viewRn_empty)
[PROOF STATE]
proof (state)
this:
m = Empty

goal (2 subgoals):
 1. viewRn m = None \<Longrightarrow> digitToList pr @ toList m @ nodeToList a = toList s @ nodeToList nd
 2. \<And>aa t. viewRn m = Some (aa, t) \<Longrightarrow> digitToList pr @ toList m @ nodeToList a = toList s @ nodeToList nd
[PROOF STEP]
from av prems
[PROOF STATE]
proof (chain)
picking this:
m = Empty
viewRn m = Some (?nd, ?s) \<Longrightarrow> toList m = toList ?s @ nodeToList ?nd
(case viewRn m of None \<Rightarrow> Some (a, digitToTree pr) | Some (b, m2) \<Rightarrow> Some (a, deep pr m2 (nodeToDigit b))) = Some (nd, s)
[PROOF STEP]
show "digitToList pr @ toList m @ nodeToList a = toList s @ nodeToList nd"
[PROOF STATE]
proof (prove)
using this:
m = Empty
viewRn m = Some (?nd, ?s) \<Longrightarrow> toList m = toList ?s @ nodeToList ?nd
(case viewRn m of None \<Rightarrow> Some (a, digitToTree pr) | Some (b, m2) \<Rightarrow> Some (a, deep pr m2 (nodeToDigit b))) = Some (nd, s)

goal (1 subgoal):
 1. digitToList pr @ toList m @ nodeToList a = toList s @ nodeToList nd
[PROOF STEP]
by (auto simp add: digitToTree_list)
[PROOF STATE]
proof (state)
this:
digitToList pr @ toList m @ nodeToList a = toList s @ nodeToList nd

goal (1 subgoal):
 1. \<And>aa t. viewRn m = Some (aa, t) \<Longrightarrow> digitToList pr @ toList m @ nodeToList a = toList s @ nodeToList nd
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa t. viewRn m = Some (aa, t) \<Longrightarrow> digitToList pr @ toList m @ nodeToList a = toList s @ nodeToList nd
[PROOF STEP]
case (Cons b m2)
[PROOF STATE]
proof (state)
this:
viewRn m = Some (b, m2)

goal (1 subgoal):
 1. \<And>aa t. viewRn m = Some (aa, t) \<Longrightarrow> digitToList pr @ toList m @ nodeToList a = toList s @ nodeToList nd
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
viewRn m = Some (?nd, ?s) \<Longrightarrow> toList m = toList ?s @ nodeToList ?nd
(case viewRn m of None \<Rightarrow> Some (a, digitToTree pr) | Some (b, m2) \<Rightarrow> Some (a, deep pr m2 (nodeToDigit b))) = Some (nd, s)
viewRn m = Some (b, m2)
[PROOF STEP]
have bv: "nd = a" "s = (deep pr m2 (nodeToDigit b))"
[PROOF STATE]
proof (prove)
using this:
viewRn m = Some (?nd, ?s) \<Longrightarrow> toList m = toList ?s @ nodeToList ?nd
(case viewRn m of None \<Rightarrow> Some (a, digitToTree pr) | Some (b, m2) \<Rightarrow> Some (a, deep pr m2 (nodeToDigit b))) = Some (nd, s)
viewRn m = Some (b, m2)

goal (1 subgoal):
 1. nd = a &&& s = deep pr m2 (nodeToDigit b)
[PROOF STEP]
apply(auto simp add: deep_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
nd = a
s = deep pr m2 (nodeToDigit b)

goal (1 subgoal):
 1. \<And>aa t. viewRn m = Some (aa, t) \<Longrightarrow> digitToList pr @ toList m @ nodeToList a = toList s @ nodeToList nd
[PROOF STEP]
with Cons prems
[PROOF STATE]
proof (chain)
picking this:
viewRn m = Some (b, m2)
viewRn m = Some (?nd, ?s) \<Longrightarrow> toList m = toList ?s @ nodeToList ?nd
(case viewRn m of None \<Rightarrow> Some (a, digitToTree pr) | Some (b, m2) \<Rightarrow> Some (a, deep pr m2 (nodeToDigit b))) = Some (nd, s)
nd = a
s = deep pr m2 (nodeToDigit b)
[PROOF STEP]
show "digitToList pr @ toList m @ nodeToList a = toList s @ nodeToList nd"
[PROOF STATE]
proof (prove)
using this:
viewRn m = Some (b, m2)
viewRn m = Some (?nd, ?s) \<Longrightarrow> toList m = toList ?s @ nodeToList ?nd
(case viewRn m of None \<Rightarrow> Some (a, digitToTree pr) | Some (b, m2) \<Rightarrow> Some (a, deep pr m2 (nodeToDigit b))) = Some (nd, s)
nd = a
s = deep pr m2 (nodeToDigit b)

goal (1 subgoal):
 1. digitToList pr @ toList m @ nodeToList a = toList s @ nodeToList nd
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>viewRn m = Some (b, m2); \<And>nd s. b = nd \<and> m2 = s \<Longrightarrow> toList m = toList s @ nodeToList nd; nd = a; s = deep pr m2 (nodeToDigit b)\<rbrakk> \<Longrightarrow> digitToList pr @ toList m2 @ nodeToList b = toList (deep pr m2 (nodeToDigit b))
[PROOF STEP]
apply(simp add: deep_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>viewRn m = Some (b, m2); \<And>nd s. b = nd \<and> m2 = s \<Longrightarrow> toList m = toList s @ nodeToList nd; nd = a; s = Deep (gmd pr + gmft m2 + gmd (nodeToDigit b)) pr m2 (nodeToDigit b)\<rbrakk> \<Longrightarrow> nodeToList b = digitToList (nodeToDigit b)
[PROOF STEP]
apply(simp add: deep_def nodeToDigit_list)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
digitToList pr @ toList m @ nodeToList a = toList s @ nodeToList nd

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma viewL_correct:
  assumes INV: "ft_invar t"
  shows
  "(t=Empty \<Longrightarrow> viewL t = None)"
  "(t\<noteq>Empty \<Longrightarrow> (\<exists>a s. viewL t = Some (a, s) \<and> ft_invar s
                        \<and> toList t = a # toList s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t = Empty \<Longrightarrow> viewL t = None) &&& (t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t = Empty \<Longrightarrow> viewL t = None
 2. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s
[PROOF STEP]
assume "t=Empty"
[PROOF STATE]
proof (state)
this:
t = Empty

goal (2 subgoals):
 1. t = Empty \<Longrightarrow> viewL t = None
 2. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s
[PROOF STEP]
thus "viewL t = None"
[PROOF STATE]
proof (prove)
using this:
t = Empty

goal (1 subgoal):
 1. viewL t = None
[PROOF STEP]
by (simp add: viewL_def)
[PROOF STATE]
proof (state)
this:
viewL t = None

goal (1 subgoal):
 1. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s
[PROOF STEP]
assume NE: "t \<noteq> Empty"
[PROOF STATE]
proof (state)
this:
t \<noteq> Empty

goal (1 subgoal):
 1. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s
[PROOF STEP]
from INV
[PROOF STATE]
proof (chain)
picking this:
ft_invar t
[PROOF STEP]
have INV': "is_leveln_ftree 0 t" "is_measured_ftree t"
[PROOF STATE]
proof (prove)
using this:
ft_invar t

goal (1 subgoal):
 1. is_leveln_ftree 0 t &&& is_measured_ftree t
[PROOF STEP]
by (simp_all add: ft_invar_def)
[PROOF STATE]
proof (state)
this:
is_leveln_ftree 0 t
is_measured_ftree t

goal (1 subgoal):
 1. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s
[PROOF STEP]
from NE
[PROOF STATE]
proof (chain)
picking this:
t \<noteq> Empty
[PROOF STEP]
have v1: "viewLn t \<noteq> None"
[PROOF STATE]
proof (prove)
using this:
t \<noteq> Empty

goal (1 subgoal):
 1. viewLn t \<noteq> None
[PROOF STEP]
by (auto simp add: viewLn_empty)
[PROOF STATE]
proof (state)
this:
viewLn t \<noteq> None

goal (1 subgoal):
 1. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
viewLn t \<noteq> None
[PROOF STEP]
obtain nd s where vn: "viewLn t = Some (nd, s)"
[PROOF STATE]
proof (prove)
using this:
viewLn t \<noteq> None

goal (1 subgoal):
 1. (\<And>nd s. viewLn t = Some (nd, s) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "viewLn t") (auto)
[PROOF STATE]
proof (state)
this:
viewLn t = Some (nd, s)

goal (1 subgoal):
 1. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
viewLn t = Some (nd, s)
[PROOF STEP]
obtain a where v1: "viewL t = Some (a, s)"
[PROOF STATE]
proof (prove)
using this:
viewLn t = Some (nd, s)

goal (1 subgoal):
 1. (\<And>a. viewL t = Some (a, s) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: viewL_def)
[PROOF STATE]
proof (state)
this:
viewL t = Some (a, s)

goal (1 subgoal):
 1. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s
[PROOF STEP]
from INV' vn
[PROOF STATE]
proof (chain)
picking this:
is_leveln_ftree 0 t
is_measured_ftree t
viewLn t = Some (nd, s)
[PROOF STEP]
have
    v2: "is_measured_ftree s \<and> is_leveln_ftree 0 s
         \<and> is_leveln_node 0 nd \<and> is_measured_node nd"
        "toList t = (nodeToList nd) @ (toList s)"
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree 0 t
is_measured_ftree t
viewLn t = Some (nd, s)

goal (1 subgoal):
 1. is_measured_ftree s \<and> is_leveln_ftree 0 s \<and> is_leveln_node 0 nd \<and> is_measured_node nd &&& toList t = nodeToList nd @ toList s
[PROOF STEP]
by (auto simp add: viewLn_inv[of t 0 nd s] viewLn_list[of t])
[PROOF STATE]
proof (state)
this:
is_measured_ftree s \<and> is_leveln_ftree 0 s \<and> is_leveln_node 0 nd \<and> is_measured_node nd
toList t = nodeToList nd @ toList s

goal (1 subgoal):
 1. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s
[PROOF STEP]
with v1 vn
[PROOF STATE]
proof (chain)
picking this:
viewL t = Some (a, s)
viewLn t = Some (nd, s)
is_measured_ftree s \<and> is_leveln_ftree 0 s \<and> is_leveln_node 0 nd \<and> is_measured_node nd
toList t = nodeToList nd @ toList s
[PROOF STEP]
have v3: "nodeToList nd = [a]"
[PROOF STATE]
proof (prove)
using this:
viewL t = Some (a, s)
viewLn t = Some (nd, s)
is_measured_ftree s \<and> is_leveln_ftree 0 s \<and> is_leveln_node 0 nd \<and> is_measured_node nd
toList t = nodeToList nd @ toList s

goal (1 subgoal):
 1. nodeToList nd = [a]
[PROOF STEP]
apply (auto simp add: viewL_def )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>viewLn t = Some (nd, s); toList t = nodeToList nd @ toList s; a = n_unwrap nd; is_measured_ftree s; is_leveln_ftree 0 s; is_leveln_node 0 nd; is_measured_node nd\<rbrakk> \<Longrightarrow> nodeToList nd = [n_unwrap nd]
[PROOF STEP]
apply (induct nd)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2. \<lbrakk>viewLn t = Some (Tip x1 x2, s); toList t = nodeToList (Tip x1 x2) @ toList s; a = n_unwrap (Tip x1 x2); is_measured_ftree s; is_leveln_ftree 0 s; is_leveln_node 0 (Tip x1 x2); is_measured_node (Tip x1 x2)\<rbrakk> \<Longrightarrow> nodeToList (Tip x1 x2) = [n_unwrap (Tip x1 x2)]
 2. \<And>x1 nd1 nd2. \<lbrakk>\<lbrakk>viewLn t = Some (nd1, s); toList t = nodeToList nd1 @ toList s; a = n_unwrap nd1; is_measured_ftree s; is_leveln_ftree 0 s; is_leveln_node 0 nd1; is_measured_node nd1\<rbrakk> \<Longrightarrow> nodeToList nd1 = [n_unwrap nd1]; \<lbrakk>viewLn t = Some (nd2, s); toList t = nodeToList nd2 @ toList s; a = n_unwrap nd2; is_measured_ftree s; is_leveln_ftree 0 s; is_leveln_node 0 nd2; is_measured_node nd2\<rbrakk> \<Longrightarrow> nodeToList nd2 = [n_unwrap nd2]; viewLn t = Some (Node2 x1 nd1 nd2, s); toList t = nodeToList (Node2 x1 nd1 nd2) @ toList s; a = n_unwrap (Node2 x1 nd1 nd2); is_measured_ftree s; is_leveln_ftree 0 s; is_leveln_node 0 (Node2 x1 nd1 nd2); is_measured_node (Node2 x1 nd1 nd2)\<rbrakk> \<Longrightarrow> nodeToList (Node2 x1 nd1 nd2) = [n_unwrap (Node2 x1 nd1 nd2)]
 3. \<And>x1 nd1 nd2 nd3. \<lbrakk>\<lbrakk>viewLn t = Some (nd1, s); toList t = nodeToList nd1 @ toList s; a = n_unwrap nd1; is_measured_ftree s; is_leveln_ftree 0 s; is_leveln_node 0 nd1; is_measured_node nd1\<rbrakk> \<Longrightarrow> nodeToList nd1 = [n_unwrap nd1]; \<lbrakk>viewLn t = Some (nd2, s); toList t = nodeToList nd2 @ toList s; a = n_unwrap nd2; is_measured_ftree s; is_leveln_ftree 0 s; is_leveln_node 0 nd2; is_measured_node nd2\<rbrakk> \<Longrightarrow> nodeToList nd2 = [n_unwrap nd2]; \<lbrakk>viewLn t = Some (nd3, s); toList t = nodeToList nd3 @ toList s; a = n_unwrap nd3; is_measured_ftree s; is_leveln_ftree 0 s; is_leveln_node 0 nd3; is_measured_node nd3\<rbrakk> \<Longrightarrow> nodeToList nd3 = [n_unwrap nd3]; viewLn t = Some (Node3 x1 nd1 nd2 nd3, s); toList t = nodeToList (Node3 x1 nd1 nd2 nd3) @ toList s; a = n_unwrap (Node3 x1 nd1 nd2 nd3); is_measured_ftree s; is_leveln_ftree 0 s; is_leveln_node 0 (Node3 x1 nd1 nd2 nd3); is_measured_node (Node3 x1 nd1 nd2 nd3)\<rbrakk> \<Longrightarrow> nodeToList (Node3 x1 nd1 nd2 nd3) = [n_unwrap (Node3 x1 nd1 nd2 nd3)]
[PROOF STEP]
apply (simp_all (no_asm_use))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
nodeToList nd = [a]

goal (1 subgoal):
 1. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s
[PROOF STEP]
with v1 v2
[PROOF STATE]
proof (chain)
picking this:
viewL t = Some (a, s)
is_measured_ftree s \<and> is_leveln_ftree 0 s \<and> is_leveln_node 0 nd \<and> is_measured_node nd
toList t = nodeToList nd @ toList s
nodeToList nd = [a]
[PROOF STEP]
show "\<exists>a s. viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s"
[PROOF STATE]
proof (prove)
using this:
viewL t = Some (a, s)
is_measured_ftree s \<and> is_leveln_ftree 0 s \<and> is_leveln_node 0 nd \<and> is_measured_node nd
toList t = nodeToList nd @ toList s
nodeToList nd = [a]

goal (1 subgoal):
 1. \<exists>a s. viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s
[PROOF STEP]
by (auto simp add: ft_invar_def)
[PROOF STATE]
proof (state)
this:
\<exists>a s. viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma viewL_correct_empty[simp]: "viewL Empty = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. viewL Empty = None
[PROOF STEP]
by (simp add: viewL_def)


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

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


[STATEMENT]
lemma viewR_correct:
  assumes INV: "ft_invar t"
  shows
  "(t = Empty \<Longrightarrow> viewR t = None)"
  "(t \<noteq> Empty \<Longrightarrow> (\<exists> a s. viewR t = Some (a, s) \<and> ft_invar s
                          \<and> toList t = toList s @ [a]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t = Empty \<Longrightarrow> viewR t = None) &&& (t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t = Empty \<Longrightarrow> viewR t = None
 2. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]
[PROOF STEP]
assume "t=Empty"
[PROOF STATE]
proof (state)
this:
t = Empty

goal (2 subgoals):
 1. t = Empty \<Longrightarrow> viewR t = None
 2. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]
[PROOF STEP]
thus "viewR t = None"
[PROOF STATE]
proof (prove)
using this:
t = Empty

goal (1 subgoal):
 1. viewR t = None
[PROOF STEP]
by (simp add: viewR_def)
[PROOF STATE]
proof (state)
this:
viewR t = None

goal (1 subgoal):
 1. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]
[PROOF STEP]
assume NE: "t \<noteq> Empty"
[PROOF STATE]
proof (state)
this:
t \<noteq> Empty

goal (1 subgoal):
 1. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]
[PROOF STEP]
from INV
[PROOF STATE]
proof (chain)
picking this:
ft_invar t
[PROOF STEP]
have INV': "is_leveln_ftree 0 t" "is_measured_ftree t"
[PROOF STATE]
proof (prove)
using this:
ft_invar t

goal (1 subgoal):
 1. is_leveln_ftree 0 t &&& is_measured_ftree t
[PROOF STEP]
unfolding ft_invar_def
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree 0 t \<and> is_measured_ftree t

goal (1 subgoal):
 1. is_leveln_ftree 0 t &&& is_measured_ftree t
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
is_leveln_ftree 0 t
is_measured_ftree t

goal (1 subgoal):
 1. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]
[PROOF STEP]
from NE
[PROOF STATE]
proof (chain)
picking this:
t \<noteq> Empty
[PROOF STEP]
have v1: "viewRn t \<noteq> None"
[PROOF STATE]
proof (prove)
using this:
t \<noteq> Empty

goal (1 subgoal):
 1. viewRn t \<noteq> None
[PROOF STEP]
by (auto simp add: viewRn_empty)
[PROOF STATE]
proof (state)
this:
viewRn t \<noteq> None

goal (1 subgoal):
 1. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
viewRn t \<noteq> None
[PROOF STEP]
obtain nd s where vn: "viewRn t = Some (nd, s)"
[PROOF STATE]
proof (prove)
using this:
viewRn t \<noteq> None

goal (1 subgoal):
 1. (\<And>nd s. viewRn t = Some (nd, s) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "viewRn t") (auto)
[PROOF STATE]
proof (state)
this:
viewRn t = Some (nd, s)

goal (1 subgoal):
 1. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
viewRn t = Some (nd, s)
[PROOF STEP]
obtain a where v1: "viewR t = Some (a, s)"
[PROOF STATE]
proof (prove)
using this:
viewRn t = Some (nd, s)

goal (1 subgoal):
 1. (\<And>a. viewR t = Some (a, s) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: viewR_def)
[PROOF STATE]
proof (state)
this:
viewR t = Some (a, s)

goal (1 subgoal):
 1. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]
[PROOF STEP]
from INV' vn
[PROOF STATE]
proof (chain)
picking this:
is_leveln_ftree 0 t
is_measured_ftree t
viewRn t = Some (nd, s)
[PROOF STEP]
have
    v2: "is_measured_ftree s \<and> is_leveln_ftree 0 s
         \<and> is_leveln_node 0 nd \<and> is_measured_node nd"
        "toList t = (toList s) @ (nodeToList nd)"
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree 0 t
is_measured_ftree t
viewRn t = Some (nd, s)

goal (1 subgoal):
 1. is_measured_ftree s \<and> is_leveln_ftree 0 s \<and> is_leveln_node 0 nd \<and> is_measured_node nd &&& toList t = toList s @ nodeToList nd
[PROOF STEP]
by (auto simp add: viewRn_inv[of t 0 nd s] viewRn_list[of t])
[PROOF STATE]
proof (state)
this:
is_measured_ftree s \<and> is_leveln_ftree 0 s \<and> is_leveln_node 0 nd \<and> is_measured_node nd
toList t = toList s @ nodeToList nd

goal (1 subgoal):
 1. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]
[PROOF STEP]
with v1 vn
[PROOF STATE]
proof (chain)
picking this:
viewR t = Some (a, s)
viewRn t = Some (nd, s)
is_measured_ftree s \<and> is_leveln_ftree 0 s \<and> is_leveln_node 0 nd \<and> is_measured_node nd
toList t = toList s @ nodeToList nd
[PROOF STEP]
have v3: "nodeToList nd = [a]"
[PROOF STATE]
proof (prove)
using this:
viewR t = Some (a, s)
viewRn t = Some (nd, s)
is_measured_ftree s \<and> is_leveln_ftree 0 s \<and> is_leveln_node 0 nd \<and> is_measured_node nd
toList t = toList s @ nodeToList nd

goal (1 subgoal):
 1. nodeToList nd = [a]
[PROOF STEP]
apply (auto simp add: viewR_def )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>viewRn t = Some (nd, s); toList t = toList s @ nodeToList nd; a = n_unwrap nd; is_measured_ftree s; is_leveln_ftree 0 s; is_leveln_node 0 nd; is_measured_node nd\<rbrakk> \<Longrightarrow> nodeToList nd = [n_unwrap nd]
[PROOF STEP]
apply (induct nd)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2. \<lbrakk>viewRn t = Some (Tip x1 x2, s); toList t = toList s @ nodeToList (Tip x1 x2); a = n_unwrap (Tip x1 x2); is_measured_ftree s; is_leveln_ftree 0 s; is_leveln_node 0 (Tip x1 x2); is_measured_node (Tip x1 x2)\<rbrakk> \<Longrightarrow> nodeToList (Tip x1 x2) = [n_unwrap (Tip x1 x2)]
 2. \<And>x1 nd1 nd2. \<lbrakk>\<lbrakk>viewRn t = Some (nd1, s); toList t = toList s @ nodeToList nd1; a = n_unwrap nd1; is_measured_ftree s; is_leveln_ftree 0 s; is_leveln_node 0 nd1; is_measured_node nd1\<rbrakk> \<Longrightarrow> nodeToList nd1 = [n_unwrap nd1]; \<lbrakk>viewRn t = Some (nd2, s); toList t = toList s @ nodeToList nd2; a = n_unwrap nd2; is_measured_ftree s; is_leveln_ftree 0 s; is_leveln_node 0 nd2; is_measured_node nd2\<rbrakk> \<Longrightarrow> nodeToList nd2 = [n_unwrap nd2]; viewRn t = Some (Node2 x1 nd1 nd2, s); toList t = toList s @ nodeToList (Node2 x1 nd1 nd2); a = n_unwrap (Node2 x1 nd1 nd2); is_measured_ftree s; is_leveln_ftree 0 s; is_leveln_node 0 (Node2 x1 nd1 nd2); is_measured_node (Node2 x1 nd1 nd2)\<rbrakk> \<Longrightarrow> nodeToList (Node2 x1 nd1 nd2) = [n_unwrap (Node2 x1 nd1 nd2)]
 3. \<And>x1 nd1 nd2 nd3. \<lbrakk>\<lbrakk>viewRn t = Some (nd1, s); toList t = toList s @ nodeToList nd1; a = n_unwrap nd1; is_measured_ftree s; is_leveln_ftree 0 s; is_leveln_node 0 nd1; is_measured_node nd1\<rbrakk> \<Longrightarrow> nodeToList nd1 = [n_unwrap nd1]; \<lbrakk>viewRn t = Some (nd2, s); toList t = toList s @ nodeToList nd2; a = n_unwrap nd2; is_measured_ftree s; is_leveln_ftree 0 s; is_leveln_node 0 nd2; is_measured_node nd2\<rbrakk> \<Longrightarrow> nodeToList nd2 = [n_unwrap nd2]; \<lbrakk>viewRn t = Some (nd3, s); toList t = toList s @ nodeToList nd3; a = n_unwrap nd3; is_measured_ftree s; is_leveln_ftree 0 s; is_leveln_node 0 nd3; is_measured_node nd3\<rbrakk> \<Longrightarrow> nodeToList nd3 = [n_unwrap nd3]; viewRn t = Some (Node3 x1 nd1 nd2 nd3, s); toList t = toList s @ nodeToList (Node3 x1 nd1 nd2 nd3); a = n_unwrap (Node3 x1 nd1 nd2 nd3); is_measured_ftree s; is_leveln_ftree 0 s; is_leveln_node 0 (Node3 x1 nd1 nd2 nd3); is_measured_node (Node3 x1 nd1 nd2 nd3)\<rbrakk> \<Longrightarrow> nodeToList (Node3 x1 nd1 nd2 nd3) = [n_unwrap (Node3 x1 nd1 nd2 nd3)]
[PROOF STEP]
apply (simp_all (no_asm_use))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
nodeToList nd = [a]

goal (1 subgoal):
 1. t \<noteq> Empty \<Longrightarrow> \<exists>a s. viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]
[PROOF STEP]
with v1 v2
[PROOF STATE]
proof (chain)
picking this:
viewR t = Some (a, s)
is_measured_ftree s \<and> is_leveln_ftree 0 s \<and> is_leveln_node 0 nd \<and> is_measured_node nd
toList t = toList s @ nodeToList nd
nodeToList nd = [a]
[PROOF STEP]
show "\<exists>a s. viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]"
[PROOF STATE]
proof (prove)
using this:
viewR t = Some (a, s)
is_measured_ftree s \<and> is_leveln_ftree 0 s \<and> is_leveln_node 0 nd \<and> is_measured_node nd
toList t = toList s @ nodeToList nd
nodeToList nd = [a]

goal (1 subgoal):
 1. \<exists>a s. viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]
[PROOF STEP]
unfolding ft_invar_def
[PROOF STATE]
proof (prove)
using this:
viewR t = Some (a, s)
is_measured_ftree s \<and> is_leveln_ftree 0 s \<and> is_leveln_node 0 nd \<and> is_measured_node nd
toList t = toList s @ nodeToList nd
nodeToList nd = [a]

goal (1 subgoal):
 1. \<exists>a s. viewR t = Some (a, s) \<and> (is_leveln_ftree 0 s \<and> is_measured_ftree s) \<and> toList t = toList s @ [a]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a s. viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma viewR_correct_empty[simp]: "viewR Empty = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. viewR Empty = None
[PROOF STEP]
unfolding viewR_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case viewRn Empty of None \<Rightarrow> None | Some (a, t2) \<Rightarrow> Some (n_unwrap a, t2)) = None
[PROOF STEP]
by simp


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

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


[STATEMENT]
lemma isEmpty_correct: "isEmpty t \<longleftrightarrow> toList t = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isEmpty t = (toList t = [])
[PROOF STEP]
unfolding isEmpty_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t = Empty) = (toList t = [])
[PROOF STEP]
by (simp add: toList_empty)
\<comment> \<open>Avoid comparison with @{text "(=)"}, and thus unnecessary equality-class
    parameter on element types in generated code\<close>


[STATEMENT]
lemma [code]: "isEmpty t = (case t of Empty \<Rightarrow> True | _ \<Rightarrow> False)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isEmpty t = (case t of Empty \<Rightarrow> True | _ \<Rightarrow> False)
[PROOF STEP]
apply (cases t)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. t = Empty \<Longrightarrow> isEmpty t = (case t of Empty \<Rightarrow> True | _ \<Rightarrow> False)
 2. \<And>x2. t = Single x2 \<Longrightarrow> isEmpty t = (case t of Empty \<Rightarrow> True | _ \<Rightarrow> False)
 3. \<And>x31 x32 x33 x34. t = Deep x31 x32 x33 x34 \<Longrightarrow> isEmpty t = (case t of Empty \<Rightarrow> True | _ \<Rightarrow> False)
[PROOF STEP]
apply (auto simp add: isEmpty_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma head_correct:
  assumes "ft_invar t" "t \<noteq> Empty"
  shows "head t = hd (toList t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. head t = hd (toList t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. head t = hd (toList t)
[PROOF STEP]
from assms viewL_correct
[PROOF STATE]
proof (chain)
picking this:
ft_invar t
t \<noteq> Empty
\<lbrakk>ft_invar ?t; ?t = Empty\<rbrakk> \<Longrightarrow> viewL ?t = None
\<lbrakk>ft_invar ?t; ?t \<noteq> Empty\<rbrakk> \<Longrightarrow> \<exists>a s. viewL ?t = Some (a, s) \<and> ft_invar s \<and> toList ?t = a # toList s
[PROOF STEP]
obtain a s where
    v1:"viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s"
[PROOF STATE]
proof (prove)
using this:
ft_invar t
t \<noteq> Empty
\<lbrakk>ft_invar ?t; ?t = Empty\<rbrakk> \<Longrightarrow> viewL ?t = None
\<lbrakk>ft_invar ?t; ?t \<noteq> Empty\<rbrakk> \<Longrightarrow> \<exists>a s. viewL ?t = Some (a, s) \<and> ft_invar s \<and> toList ?t = a # toList s

goal (1 subgoal):
 1. (\<And>a s. viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s

goal (1 subgoal):
 1. head t = hd (toList t)
[PROOF STEP]
hence v2: "head t = a"
[PROOF STATE]
proof (prove)
using this:
viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s

goal (1 subgoal):
 1. head t = a
[PROOF STEP]
by (auto simp add: head_def)
[PROOF STATE]
proof (state)
this:
head t = a

goal (1 subgoal):
 1. head t = hd (toList t)
[PROOF STEP]
from v1
[PROOF STATE]
proof (chain)
picking this:
viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s
[PROOF STEP]
have "hd (toList t) = a"
[PROOF STATE]
proof (prove)
using this:
viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s

goal (1 subgoal):
 1. hd (toList t) = a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hd (toList t) = a

goal (1 subgoal):
 1. head t = hd (toList t)
[PROOF STEP]
with v2
[PROOF STATE]
proof (chain)
picking this:
head t = a
hd (toList t) = a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
head t = a
hd (toList t) = a

goal (1 subgoal):
 1. head t = hd (toList t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
head t = hd (toList t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tail_correct:
  assumes "ft_invar t" "t \<noteq> Empty"
  shows "toList (tail t) = tl (toList t)" and "ft_invar (tail t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList (tail t) = tl (toList t) &&& ft_invar (tail t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. toList (tail t) = tl (toList t)
 2. ft_invar (tail t)
[PROOF STEP]
from assms viewL_correct
[PROOF STATE]
proof (chain)
picking this:
ft_invar t
t \<noteq> Empty
\<lbrakk>ft_invar ?t; ?t = Empty\<rbrakk> \<Longrightarrow> viewL ?t = None
\<lbrakk>ft_invar ?t; ?t \<noteq> Empty\<rbrakk> \<Longrightarrow> \<exists>a s. viewL ?t = Some (a, s) \<and> ft_invar s \<and> toList ?t = a # toList s
[PROOF STEP]
obtain a s where
    v1:"viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s"
[PROOF STATE]
proof (prove)
using this:
ft_invar t
t \<noteq> Empty
\<lbrakk>ft_invar ?t; ?t = Empty\<rbrakk> \<Longrightarrow> viewL ?t = None
\<lbrakk>ft_invar ?t; ?t \<noteq> Empty\<rbrakk> \<Longrightarrow> \<exists>a s. viewL ?t = Some (a, s) \<and> ft_invar s \<and> toList ?t = a # toList s

goal (1 subgoal):
 1. (\<And>a s. viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s

goal (2 subgoals):
 1. toList (tail t) = tl (toList t)
 2. ft_invar (tail t)
[PROOF STEP]
hence v2: "tail t = s"
[PROOF STATE]
proof (prove)
using this:
viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s

goal (1 subgoal):
 1. tail t = s
[PROOF STEP]
by (auto simp add: tail_def)
[PROOF STATE]
proof (state)
this:
tail t = s

goal (2 subgoals):
 1. toList (tail t) = tl (toList t)
 2. ft_invar (tail t)
[PROOF STEP]
from v1
[PROOF STATE]
proof (chain)
picking this:
viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s
[PROOF STEP]
have "tl (toList t) = toList s"
[PROOF STATE]
proof (prove)
using this:
viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s

goal (1 subgoal):
 1. tl (toList t) = toList s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
tl (toList t) = toList s

goal (2 subgoals):
 1. toList (tail t) = tl (toList t)
 2. ft_invar (tail t)
[PROOF STEP]
with v1 v2
[PROOF STATE]
proof (chain)
picking this:
viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s
tail t = s
tl (toList t) = toList s
[PROOF STEP]
show
    "toList (tail t) = tl (toList t)"
    "ft_invar (tail t)"
[PROOF STATE]
proof (prove)
using this:
viewL t = Some (a, s) \<and> ft_invar s \<and> toList t = a # toList s
tail t = s
tl (toList t) = toList s

goal (1 subgoal):
 1. toList (tail t) = tl (toList t) &&& ft_invar (tail t)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
toList (tail t) = tl (toList t)
ft_invar (tail t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma headR_correct:
  assumes "ft_invar t" "t \<noteq> Empty"
  shows  "headR t = last (toList t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. headR t = last (toList t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. headR t = last (toList t)
[PROOF STEP]
from assms viewR_correct
[PROOF STATE]
proof (chain)
picking this:
ft_invar t
t \<noteq> Empty
\<lbrakk>ft_invar ?t; ?t = Empty\<rbrakk> \<Longrightarrow> viewR ?t = None
\<lbrakk>ft_invar ?t; ?t \<noteq> Empty\<rbrakk> \<Longrightarrow> \<exists>a s. viewR ?t = Some (a, s) \<and> ft_invar s \<and> toList ?t = toList s @ [a]
[PROOF STEP]
obtain a s where
    v1:"viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]"
[PROOF STATE]
proof (prove)
using this:
ft_invar t
t \<noteq> Empty
\<lbrakk>ft_invar ?t; ?t = Empty\<rbrakk> \<Longrightarrow> viewR ?t = None
\<lbrakk>ft_invar ?t; ?t \<noteq> Empty\<rbrakk> \<Longrightarrow> \<exists>a s. viewR ?t = Some (a, s) \<and> ft_invar s \<and> toList ?t = toList s @ [a]

goal (1 subgoal):
 1. (\<And>a s. viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]

goal (1 subgoal):
 1. headR t = last (toList t)
[PROOF STEP]
hence v2: "headR t = a"
[PROOF STATE]
proof (prove)
using this:
viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]

goal (1 subgoal):
 1. headR t = a
[PROOF STEP]
by (auto simp add: headR_def)
[PROOF STATE]
proof (state)
this:
headR t = a

goal (1 subgoal):
 1. headR t = last (toList t)
[PROOF STEP]
with v1
[PROOF STATE]
proof (chain)
picking this:
viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]
headR t = a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]
headR t = a

goal (1 subgoal):
 1. headR t = last (toList t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
headR t = last (toList t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tailR_correct:
  assumes "ft_invar t" "t \<noteq> Empty"
  shows "toList (tailR t) = butlast (toList t)" and "ft_invar (tailR t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList (tailR t) = butlast (toList t) &&& ft_invar (tailR t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. toList (tailR t) = butlast (toList t)
 2. ft_invar (tailR t)
[PROOF STEP]
from assms viewR_correct
[PROOF STATE]
proof (chain)
picking this:
ft_invar t
t \<noteq> Empty
\<lbrakk>ft_invar ?t; ?t = Empty\<rbrakk> \<Longrightarrow> viewR ?t = None
\<lbrakk>ft_invar ?t; ?t \<noteq> Empty\<rbrakk> \<Longrightarrow> \<exists>a s. viewR ?t = Some (a, s) \<and> ft_invar s \<and> toList ?t = toList s @ [a]
[PROOF STEP]
obtain a s where
    v1:"viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]"
[PROOF STATE]
proof (prove)
using this:
ft_invar t
t \<noteq> Empty
\<lbrakk>ft_invar ?t; ?t = Empty\<rbrakk> \<Longrightarrow> viewR ?t = None
\<lbrakk>ft_invar ?t; ?t \<noteq> Empty\<rbrakk> \<Longrightarrow> \<exists>a s. viewR ?t = Some (a, s) \<and> ft_invar s \<and> toList ?t = toList s @ [a]

goal (1 subgoal):
 1. (\<And>a s. viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]

goal (2 subgoals):
 1. toList (tailR t) = butlast (toList t)
 2. ft_invar (tailR t)
[PROOF STEP]
hence v2: "tailR t = s"
[PROOF STATE]
proof (prove)
using this:
viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]

goal (1 subgoal):
 1. tailR t = s
[PROOF STEP]
by (auto simp add: tailR_def)
[PROOF STATE]
proof (state)
this:
tailR t = s

goal (2 subgoals):
 1. toList (tailR t) = butlast (toList t)
 2. ft_invar (tailR t)
[PROOF STEP]
with v1
[PROOF STATE]
proof (chain)
picking this:
viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]
tailR t = s
[PROOF STEP]
show "toList (tailR t) = butlast (toList t)" and "ft_invar (tailR t)"
[PROOF STATE]
proof (prove)
using this:
viewR t = Some (a, s) \<and> ft_invar s \<and> toList t = toList s @ [a]
tailR t = s

goal (1 subgoal):
 1. toList (tailR t) = butlast (toList t) &&& ft_invar (tailR t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
toList (tailR t) = butlast (toList t)
ft_invar (tailR t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lconsNlist_inv:
  assumes "is_leveln_ftree n t"
  and "is_measured_ftree t"
  and "\<forall> x\<in>set xs. (is_leveln_node n x \<and> is_measured_node x)"
  shows
  "is_leveln_ftree n (lconsNlist xs t) \<and> is_measured_ftree (lconsNlist xs t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_leveln_ftree n (lconsNlist xs t) \<and> is_measured_ftree (lconsNlist xs t)
[PROOF STEP]
by (insert assms, induct xs, auto simp add: nlcons_invlevel nlcons_invmeas)


[STATEMENT]
lemma rconsNlist_inv:
  assumes "is_leveln_ftree n t"
  and "is_measured_ftree t"
  and "\<forall> x\<in>set xs. (is_leveln_node n x \<and> is_measured_node x)"
  shows
  "is_leveln_ftree n (rconsNlist t xs) \<and> is_measured_ftree (rconsNlist t xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_leveln_ftree n (rconsNlist t xs) \<and> is_measured_ftree (rconsNlist t xs)
[PROOF STEP]
by (insert assms, induct xs arbitrary: t,
      auto simp add: nrcons_invlevel nrcons_invmeas)