[STATEMENT]
lemma deepR_inv:
  assumes "is_leveln_ftree (Suc n) m \<and> is_measured_ftree m"
  and "is_leveln_digit n pr \<and> is_measured_digit pr"
  and "\<forall> x \<in> set sf. (is_measured_node x \<and> is_leveln_node n x) \<and> length sf \<le> 4"
  shows "is_leveln_ftree n (deepR pr m sf) \<and> is_measured_ftree (deepR pr m sf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_leveln_ftree n (deepR pr m sf) \<and> is_measured_ftree (deepR pr m sf)
[PROOF STEP]
apply (insert assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; \<forall>x\<in>set sf. (is_measured_node x \<and> is_leveln_node n x) \<and> length sf \<le> 4\<rbrakk> \<Longrightarrow> is_leveln_ftree n (deepR pr m sf) \<and> is_measured_ftree (deepR pr m sf)
[PROOF STEP]
apply (induct "pr" m sf rule: deepR.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pr m. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; \<forall>x\<in>set []. (is_measured_node x \<and> is_leveln_node n x) \<and> length [] \<le> 4\<rbrakk> \<Longrightarrow> is_leveln_ftree n (deepR pr m []) \<and> is_measured_ftree (deepR pr m [])
 2. \<And>pr m v va. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; \<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4\<rbrakk> \<Longrightarrow> is_leveln_ftree n (deepR pr m (v # va)) \<and> is_measured_ftree (deepR pr m (v # va))
[PROOF STEP]
apply (simp split: viewnres_split)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pr m. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr\<rbrakk> \<Longrightarrow> (viewRn m = None \<longrightarrow> is_leveln_ftree n (digitToTree pr) \<and> is_measured_ftree (digitToTree pr)) \<and> (\<forall>a b. viewRn m = Some (a, b) \<longrightarrow> is_leveln_ftree n (deep pr b (nodeToDigit a)) \<and> is_measured_ftree (deep pr b (nodeToDigit a)))
 2. \<And>pr m v va. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; \<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4\<rbrakk> \<Longrightarrow> is_leveln_ftree n (deepR pr m (v # va)) \<and> is_measured_ftree (deepR pr m (v # va))
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>pr m. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = None\<rbrakk> \<Longrightarrow> is_leveln_ftree n (digitToTree pr)
 2. \<And>pr m. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = None\<rbrakk> \<Longrightarrow> is_measured_ftree (digitToTree pr)
 3. \<And>pr m a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_leveln_ftree n (deep pr b (nodeToDigit a))
 4. \<And>pr m a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_measured_ftree (deep pr b (nodeToDigit a))
 5. \<And>pr m v va. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; \<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4\<rbrakk> \<Longrightarrow> is_leveln_ftree n (deepR pr m (v # va)) \<and> is_measured_ftree (deepR pr m (v # va))
[PROOF STEP]
apply (simp_all add: digitToTree_inv deep_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>pr m a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nodeToDigit a) \<and> is_leveln_ftree (Suc n) b
 2. \<And>pr m a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_measured_ftree b \<and> is_measured_digit (nodeToDigit a)
 3. \<And>pr m v va. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>pr m a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nodeToDigit a) \<and> is_leveln_ftree (Suc n) b
 2. \<And>pr m a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_measured_ftree b \<and> is_measured_digit (nodeToDigit a)
 3. \<And>pr m v va. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
fix m "pr" Node FingerTreeStruc
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>pr m a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nodeToDigit a) \<and> is_leveln_ftree (Suc n) b
 2. \<And>pr m a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_measured_ftree b \<and> is_measured_digit (nodeToDigit a)
 3. \<And>pr m v va. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
assume "is_leveln_ftree (Suc n) m" "is_measured_ftree m"
         "is_leveln_digit n pr" "is_measured_digit pr"
         "viewRn m = Some (Node, FingerTreeStruc)"
[PROOF STATE]
proof (state)
this:
is_leveln_ftree (Suc n) m
is_measured_ftree m
is_leveln_digit n pr
is_measured_digit pr
viewRn m = Some (Node, FingerTreeStruc)

goal (3 subgoals):
 1. \<And>pr m a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nodeToDigit a) \<and> is_leveln_ftree (Suc n) b
 2. \<And>pr m a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_measured_ftree b \<and> is_measured_digit (nodeToDigit a)
 3. \<And>pr m v va. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
thus
    "is_leveln_digit n (nodeToDigit Node)
    \<and> is_leveln_ftree (Suc n) FingerTreeStruc"
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree (Suc n) m
is_measured_ftree m
is_leveln_digit n pr
is_measured_digit pr
viewRn m = Some (Node, FingerTreeStruc)

goal (1 subgoal):
 1. is_leveln_digit n (nodeToDigit Node) \<and> is_leveln_ftree (Suc n) FingerTreeStruc
[PROOF STEP]
by (simp add: viewRn_inv[of m "Suc n" Node FingerTreeStruc] nodeToDigit_inv)
[PROOF STATE]
proof (state)
this:
is_leveln_digit n (nodeToDigit Node) \<and> is_leveln_ftree (Suc n) FingerTreeStruc

goal (2 subgoals):
 1. \<And>pr m a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_measured_ftree b \<and> is_measured_digit (nodeToDigit a)
 2. \<And>pr m v va. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>pr m a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_measured_ftree b \<and> is_measured_digit (nodeToDigit a)
 2. \<And>pr m v va. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
fix m "pr" Node FingerTreeStruc
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>pr m a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_measured_ftree b \<and> is_measured_digit (nodeToDigit a)
 2. \<And>pr m v va. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
assume assms1:
    "is_leveln_ftree (Suc n) m" "is_measured_ftree m"
    "is_leveln_digit n pr" "is_measured_digit pr"
    "viewRn m = Some (Node, FingerTreeStruc)"
[PROOF STATE]
proof (state)
this:
is_leveln_ftree (Suc n) m
is_measured_ftree m
is_leveln_digit n pr
is_measured_digit pr
viewRn m = Some (Node, FingerTreeStruc)

goal (2 subgoals):
 1. \<And>pr m a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_measured_ftree b \<and> is_measured_digit (nodeToDigit a)
 2. \<And>pr m v va. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
thus "is_measured_ftree FingerTreeStruc \<and> is_measured_digit (nodeToDigit Node)"
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree (Suc n) m
is_measured_ftree m
is_leveln_digit n pr
is_measured_digit pr
viewRn m = Some (Node, FingerTreeStruc)

goal (1 subgoal):
 1. is_measured_ftree FingerTreeStruc \<and> is_measured_digit (nodeToDigit Node)
[PROOF STEP]
apply (auto simp only: viewRn_inv[of m "Suc n" Node FingerTreeStruc])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (Node, FingerTreeStruc)\<rbrakk> \<Longrightarrow> is_measured_digit (nodeToDigit Node)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (Node, FingerTreeStruc)\<rbrakk> \<Longrightarrow> is_measured_digit (nodeToDigit Node)
[PROOF STEP]
from assms1
[PROOF STATE]
proof (chain)
picking this:
is_leveln_ftree (Suc n) m
is_measured_ftree m
is_leveln_digit n pr
is_measured_digit pr
viewRn m = Some (Node, FingerTreeStruc)
[PROOF STEP]
have "is_measured_node Node \<and> is_leveln_node (Suc n) Node"
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree (Suc n) m
is_measured_ftree m
is_leveln_digit n pr
is_measured_digit pr
viewRn m = Some (Node, FingerTreeStruc)

goal (1 subgoal):
 1. is_measured_node Node \<and> is_leveln_node (Suc n) Node
[PROOF STEP]
by (simp add: viewRn_inv[of m "Suc n" Node FingerTreeStruc])
[PROOF STATE]
proof (state)
this:
is_measured_node Node \<and> is_leveln_node (Suc n) Node

goal (1 subgoal):
 1. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (Node, FingerTreeStruc)\<rbrakk> \<Longrightarrow> is_measured_digit (nodeToDigit Node)
[PROOF STEP]
thus "is_measured_digit (nodeToDigit Node)"
[PROOF STATE]
proof (prove)
using this:
is_measured_node Node \<and> is_leveln_node (Suc n) Node

goal (1 subgoal):
 1. is_measured_digit (nodeToDigit Node)
[PROOF STEP]
by (auto simp add: nodeToDigit_inv)
[PROOF STATE]
proof (state)
this:
is_measured_digit (nodeToDigit Node)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_measured_ftree FingerTreeStruc \<and> is_measured_digit (nodeToDigit Node)

goal (1 subgoal):
 1. \<And>pr m v va. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pr m v va. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
fix v va
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pr m v va. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
assume
    "is_measured_node v \<and> is_leveln_node n (v:: ('a,'b) Node) \<and>
    length  (va::('a, 'b) Node list) \<le> 3 \<and>
    (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)"
[PROOF STATE]
proof (state)
this:
is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)

goal (1 subgoal):
 1. \<And>pr m v va. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
thus "is_leveln_digit n (nlistToDigit (v # va)) \<and>
        is_measured_digit (nlistToDigit (v # va))"
[PROOF STATE]
proof (prove)
using this:
is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)

goal (1 subgoal):
 1. is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
by(cases "v#va" rule: nlistToDigit.cases,simp_all)
[PROOF STATE]
proof (state)
this:
is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma deepR_list:
  assumes "is_leveln_ftree (Suc n) m \<and> is_measured_ftree m"
  and "is_leveln_digit n pr \<and> is_measured_digit pr"
  and "\<forall> x \<in> set sf. (is_measured_node x \<and> is_leveln_node n x) \<and> length sf \<le> 4"
  shows "toList (deepR pr m sf) = digitToList pr @ toList m @ nlistToList sf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList (deepR pr m sf) = digitToList pr @ toList m @ nlistToList sf
[PROOF STEP]
proof (insert assms, induct "pr" m sf rule: deepR.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>pr m. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; \<forall>x\<in>set []. (is_measured_node x \<and> is_leveln_node n x) \<and> length [] \<le> 4\<rbrakk> \<Longrightarrow> toList (deepR pr m []) = digitToList pr @ toList m @ nlistToList []
 2. \<And>pr m v va. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; \<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4\<rbrakk> \<Longrightarrow> toList (deepR pr m (v # va)) = digitToList pr @ toList m @ nlistToList (v # va)
[PROOF STEP]
case (1 "pr" m)
[PROOF STATE]
proof (state)
this:
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n pr \<and> is_measured_digit pr
\<forall>x\<in>set []. (is_measured_node x \<and> is_leveln_node n x) \<and> length [] \<le> 4

goal (2 subgoals):
 1. \<And>pr m. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; \<forall>x\<in>set []. (is_measured_node x \<and> is_leveln_node n x) \<and> length [] \<le> 4\<rbrakk> \<Longrightarrow> toList (deepR pr m []) = digitToList pr @ toList m @ nlistToList []
 2. \<And>pr m v va. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; \<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4\<rbrakk> \<Longrightarrow> toList (deepR pr m (v # va)) = digitToList pr @ toList m @ nlistToList (v # va)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n pr \<and> is_measured_digit pr
\<forall>x\<in>set []. (is_measured_node x \<and> is_leveln_node n x) \<and> length [] \<le> 4

goal (1 subgoal):
 1. toList (deepR pr m []) = digitToList pr @ toList m @ nlistToList []
[PROOF STEP]
proof (auto split: viewnres_split simp add: deep_def)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = None\<rbrakk> \<Longrightarrow> toList (digitToTree pr) = digitToList pr @ toList m
 2. \<And>a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> toList b @ digitToList (nodeToDigit a) = toList m
[PROOF STEP]
assume "viewRn m = None"
[PROOF STATE]
proof (state)
this:
viewRn m = None

goal (2 subgoals):
 1. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = None\<rbrakk> \<Longrightarrow> toList (digitToTree pr) = digitToList pr @ toList m
 2. \<And>a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> toList b @ digitToList (nodeToDigit a) = toList m
[PROOF STEP]
hence "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. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = None\<rbrakk> \<Longrightarrow> toList (digitToTree pr) = digitToList pr @ toList m
 2. \<And>a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> toList b @ digitToList (nodeToDigit a) = toList m
[PROOF STEP]
hence "toList m = []"
[PROOF STATE]
proof (prove)
using this:
m = Empty

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

goal (2 subgoals):
 1. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = None\<rbrakk> \<Longrightarrow> toList (digitToTree pr) = digitToList pr @ toList m
 2. \<And>a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> toList b @ digitToList (nodeToDigit a) = toList m
[PROOF STEP]
thus "toList (digitToTree pr) = digitToList pr @ toList m"
[PROOF STATE]
proof (prove)
using this:
toList m = []

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

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> toList b @ digitToList (nodeToDigit a) = toList m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> toList b @ digitToList (nodeToDigit a) = toList m
[PROOF STEP]
fix nd t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> toList b @ digitToList (nodeToDigit a) = toList m
[PROOF STEP]
assume "viewRn m = Some (nd, t)" "is_leveln_ftree (Suc n) m"
           "is_measured_ftree m"
[PROOF STATE]
proof (state)
this:
viewRn m = Some (nd, t)
is_leveln_ftree (Suc n) m
is_measured_ftree m

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> toList b @ digitToList (nodeToDigit a) = toList m
[PROOF STEP]
hence "toList t @ nodeToList nd = toList m"
[PROOF STATE]
proof (prove)
using this:
viewRn m = Some (nd, t)
is_leveln_ftree (Suc n) m
is_measured_ftree m

goal (1 subgoal):
 1. toList t @ nodeToList nd = toList m
[PROOF STEP]
by (metis viewRn_list)
[PROOF STATE]
proof (state)
this:
toList t @ nodeToList nd = toList m

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n pr; is_measured_digit pr; viewRn m = Some (a, b)\<rbrakk> \<Longrightarrow> toList b @ digitToList (nodeToDigit a) = toList m
[PROOF STEP]
thus "toList t @ digitToList (nodeToDigit nd) = toList m"
[PROOF STATE]
proof (prove)
using this:
toList t @ nodeToList nd = toList m

goal (1 subgoal):
 1. toList t @ digitToList (nodeToDigit nd) = toList m
[PROOF STEP]
by (simp add: nodeToDigit_list)
[PROOF STATE]
proof (state)
this:
toList t @ digitToList (nodeToDigit nd) = toList m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
toList (deepR pr m []) = digitToList pr @ toList m @ nlistToList []

goal (1 subgoal):
 1. \<And>pr m v va. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; \<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4\<rbrakk> \<Longrightarrow> toList (deepR pr m (v # va)) = digitToList pr @ toList m @ nlistToList (v # va)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pr m v va. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; \<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4\<rbrakk> \<Longrightarrow> toList (deepR pr m (v # va)) = digitToList pr @ toList m @ nlistToList (v # va)
[PROOF STEP]
case (2 "pr" m v va)
[PROOF STATE]
proof (state)
this:
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n pr \<and> is_measured_digit pr
\<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4

goal (1 subgoal):
 1. \<And>pr m v va. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; \<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4\<rbrakk> \<Longrightarrow> toList (deepR pr m (v # va)) = digitToList pr @ toList m @ nlistToList (v # va)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n pr \<and> is_measured_digit pr
\<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4

goal (1 subgoal):
 1. toList (deepR pr m (v # va)) = digitToList pr @ toList m @ nlistToList (v # va)
[PROOF STEP]
apply (unfold deepR.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; \<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4\<rbrakk> \<Longrightarrow> toList (deep pr m (nlistToDigit (v # va))) = digitToList pr @ toList m @ nlistToList (v # va)
[PROOF STEP]
apply (simp add: deep_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n pr \<and> is_measured_digit pr; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> digitToList (nlistToDigit (v # va)) = nodeToList v @ nlistToList va
[PROOF STEP]
apply (simp add: nlistToDigit_list)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
toList (deepR pr m (v # va)) = digitToList pr @ toList m @ nlistToList (v # va)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gmnl_correct:
  assumes "\<forall> x \<in> set xs. is_measured_node x"
  shows  "gmnl xs = sum_list (map snd (nlistToList xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gmnl xs = sum_list (map snd (nlistToList xs))
[PROOF STEP]
by (insert assms, induct xs) (auto simp add: add.assoc gmn_correct)


[STATEMENT]
lemma splitNlist_correct:" \<lbrakk>
  \<And>(a::'a) (b::'a). p a \<Longrightarrow> p (a + b);
  \<not> p i;
  p (i + gmnl (nl ::('e,'a::monoid_add) Node list));
  splitNlist p i nl = (l, n, r)
  \<rbrakk> \<Longrightarrow>
  \<not> p (i + (gmnl l))
  \<and>
  p (i + (gmnl l) + (gmn n))
  \<and>
  nl = l @ n # r
  "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmnl nl); splitNlist p i nl = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> nl = l @ n # r
[PROOF STEP]
proof (induct p i nl arbitrary: l n r rule: splitNlist.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p i a l n r. \<lbrakk>\<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmnl [a]); splitNlist p i [a] = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> [a] = l @ n # r
 2. \<And>p i a v va l n r. \<lbrakk>\<And>x l n r. \<lbrakk>x = i + gmn a; \<not> p x; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmnl (v # va)); splitNlist p x (v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (x + gmnl l) \<and> p (x + gmnl l + gmn n) \<and> v # va = l @ n # r; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmnl (a # v # va)); splitNlist p i (a # v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
 3. \<And>a b l n r. \<lbrakk>\<And>aa b. a aa \<Longrightarrow> a (aa + b); \<not> a b; a (b + gmnl []); splitNlist a b [] = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> a (b + gmnl l) \<and> a (b + gmnl l + gmn n) \<and> [] = l @ n # r
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
p_ ?a \<Longrightarrow> p_ (?a + ?b)
\<not> p_ i_
p_ (i_ + gmnl [a_])
splitNlist p_ i_ [a_] = (l, n, r)

goal (3 subgoals):
 1. \<And>p i a l n r. \<lbrakk>\<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmnl [a]); splitNlist p i [a] = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> [a] = l @ n # r
 2. \<And>p i a v va l n r. \<lbrakk>\<And>x l n r. \<lbrakk>x = i + gmn a; \<not> p x; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmnl (v # va)); splitNlist p x (v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (x + gmnl l) \<and> p (x + gmnl l + gmn n) \<and> v # va = l @ n # r; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmnl (a # v # va)); splitNlist p i (a # v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
 3. \<And>a b l n r. \<lbrakk>\<And>aa b. a aa \<Longrightarrow> a (aa + b); \<not> a b; a (b + gmnl []); splitNlist a b [] = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> a (b + gmnl l) \<and> a (b + gmnl l + gmn n) \<and> [] = l @ n # r
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
p_ ?a \<Longrightarrow> p_ (?a + ?b)
\<not> p_ i_
p_ (i_ + gmnl [a_])
splitNlist p_ i_ [a_] = (l, n, r)

goal (1 subgoal):
 1. \<not> p_ (i_ + gmnl l) \<and> p_ (i_ + gmnl l + gmn n) \<and> [a_] = l @ n # r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> p_ (i_ + gmnl l) \<and> p_ (i_ + gmnl l + gmn n) \<and> [a_] = l @ n # r

goal (2 subgoals):
 1. \<And>p i a v va l n r. \<lbrakk>\<And>x l n r. \<lbrakk>x = i + gmn a; \<not> p x; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmnl (v # va)); splitNlist p x (v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (x + gmnl l) \<and> p (x + gmnl l + gmn n) \<and> v # va = l @ n # r; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmnl (a # v # va)); splitNlist p i (a # v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
 2. \<And>a b l n r. \<lbrakk>\<And>aa b. a aa \<Longrightarrow> a (aa + b); \<not> a b; a (b + gmnl []); splitNlist a b [] = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> a (b + gmnl l) \<and> a (b + gmnl l + gmn n) \<and> [] = l @ n # r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p i a v va l n r. \<lbrakk>\<And>x l n r. \<lbrakk>x = i + gmn a; \<not> p x; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmnl (v # va)); splitNlist p x (v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (x + gmnl l) \<and> p (x + gmnl l + gmn n) \<and> v # va = l @ n # r; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmnl (a # v # va)); splitNlist p i (a # v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
 2. \<And>a b l n r. \<lbrakk>\<And>aa b. a aa \<Longrightarrow> a (aa + b); \<not> a b; a (b + gmnl []); splitNlist a b [] = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> a (b + gmnl l) \<and> a (b + gmnl l + gmn n) \<and> [] = l @ n # r
[PROOF STEP]
case (2 p i a v va l n r)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x = i + gmn a; \<not> p ?x; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p ?x; p (?x + gmnl (v # va)); splitNlist p ?x (v # va) = (?l, ?n, ?r)\<rbrakk> \<Longrightarrow> \<not> p (?x + gmnl ?l) \<and> p (?x + gmnl ?l + gmn ?n) \<and> v # va = ?l @ ?n # ?r
p ?a \<Longrightarrow> p (?a + ?b)
\<not> p i
p (i + gmnl (a # v # va))
splitNlist p i (a # v # va) = (l, n, r)

goal (2 subgoals):
 1. \<And>p i a v va l n r. \<lbrakk>\<And>x l n r. \<lbrakk>x = i + gmn a; \<not> p x; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmnl (v # va)); splitNlist p x (v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (x + gmnl l) \<and> p (x + gmnl l + gmn n) \<and> v # va = l @ n # r; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmnl (a # v # va)); splitNlist p i (a # v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
 2. \<And>a b l n r. \<lbrakk>\<And>aa b. a aa \<Longrightarrow> a (aa + b); \<not> a b; a (b + gmnl []); splitNlist a b [] = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> a (b + gmnl l) \<and> a (b + gmnl l + gmn n) \<and> [] = l @ n # r
[PROOF STEP]
note IV = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x = i + gmn a; \<not> p ?x; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p ?x; p (?x + gmnl (v # va)); splitNlist p ?x (v # va) = (?l, ?n, ?r)\<rbrakk> \<Longrightarrow> \<not> p (?x + gmnl ?l) \<and> p (?x + gmnl ?l + gmn ?n) \<and> v # va = ?l @ ?n # ?r
p ?a \<Longrightarrow> p (?a + ?b)
\<not> p i
p (i + gmnl (a # v # va))
splitNlist p i (a # v # va) = (l, n, r)

goal (2 subgoals):
 1. \<And>p i a v va l n r. \<lbrakk>\<And>x l n r. \<lbrakk>x = i + gmn a; \<not> p x; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmnl (v # va)); splitNlist p x (v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (x + gmnl l) \<and> p (x + gmnl l + gmn n) \<and> v # va = l @ n # r; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmnl (a # v # va)); splitNlist p i (a # v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
 2. \<And>a b l n r. \<lbrakk>\<And>aa b. a aa \<Longrightarrow> a (aa + b); \<not> a b; a (b + gmnl []); splitNlist a b [] = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> a (b + gmnl l) \<and> a (b + gmnl l + gmn n) \<and> [] = l @ n # r
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
[PROOF STEP]
proof (cases "p (i + (gmn a))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p (i + gmn a) \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
 2. \<not> p (i + gmn a) \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
p (i + gmn a)

goal (2 subgoals):
 1. p (i + gmn a) \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
 2. \<not> p (i + gmn a) \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
[PROOF STEP]
with IV
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x = i + gmn a; \<not> p ?x; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p ?x; p (?x + gmnl (v # va)); splitNlist p ?x (v # va) = (?l, ?n, ?r)\<rbrakk> \<Longrightarrow> \<not> p (?x + gmnl ?l) \<and> p (?x + gmnl ?l + gmn ?n) \<and> v # va = ?l @ ?n # ?r
p ?a \<Longrightarrow> p (?a + ?b)
\<not> p i
p (i + gmnl (a # v # va))
splitNlist p i (a # v # va) = (l, n, r)
p (i + gmn a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x = i + gmn a; \<not> p ?x; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p ?x; p (?x + gmnl (v # va)); splitNlist p ?x (v # va) = (?l, ?n, ?r)\<rbrakk> \<Longrightarrow> \<not> p (?x + gmnl ?l) \<and> p (?x + gmnl ?l + gmn ?n) \<and> v # va = ?l @ ?n # ?r
p ?a \<Longrightarrow> p (?a + ?b)
\<not> p i
p (i + gmnl (a # v # va))
splitNlist p i (a # v # va) = (l, n, r)
p (i + gmn a)

goal (1 subgoal):
 1. \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r

goal (1 subgoal):
 1. \<not> p (i + gmn a) \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> p (i + gmn a) \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> p (i + gmn a)

goal (1 subgoal):
 1. \<not> p (i + gmn a) \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
[PROOF STEP]
note IV2 = this IV
[PROOF STATE]
proof (state)
this:
\<not> p (i + gmn a)
\<lbrakk>?x = i + gmn a; \<not> p ?x; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p ?x; p (?x + gmnl (v # va)); splitNlist p ?x (v # va) = (?l, ?n, ?r)\<rbrakk> \<Longrightarrow> \<not> p (?x + gmnl ?l) \<and> p (?x + gmnl ?l + gmn ?n) \<and> v # va = ?l @ ?n # ?r
p ?a \<Longrightarrow> p (?a + ?b)
\<not> p i
p (i + gmnl (a # v # va))
splitNlist p i (a # v # va) = (l, n, r)

goal (1 subgoal):
 1. \<not> p (i + gmn a) \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> p (i + gmn a)
\<lbrakk>?x = i + gmn a; \<not> p ?x; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p ?x; p (?x + gmnl (v # va)); splitNlist p ?x (v # va) = (?l, ?n, ?r)\<rbrakk> \<Longrightarrow> \<not> p (?x + gmnl ?l) \<and> p (?x + gmnl ?l + gmn ?n) \<and> v # va = ?l @ ?n # ?r
p ?a \<Longrightarrow> p (?a + ?b)
\<not> p i
p (i + gmnl (a # v # va))
splitNlist p i (a # v # va) = (l, n, r)

goal (1 subgoal):
 1. \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmn a); \<And>x l n r. \<lbrakk>x = i + gmn a; \<not> p x; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmnl (v # va)); splitNlist p x (v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (x + gmnl l) \<and> p (x + gmnl l + gmn n) \<and> v # va = l @ n # r; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmnl (a # v # va)); splitNlist p i (a # v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
[PROOF STEP]
obtain l1 n1 r1 where
        v1[simp]: "splitNlist p (i + gmn a) (v # va) = (l1, n1, r1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l1 n1 r1. splitNlist p (i + gmn a) (v # va) = (l1, n1, r1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "splitNlist p (i + gmn a) (v # va)", blast)
[PROOF STATE]
proof (state)
this:
splitNlist p (i + gmn a) (v # va) = (l1, n1, r1)

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmn a); \<And>x l n r. \<lbrakk>x = i + gmn a; \<not> p x; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmnl (v # va)); splitNlist p x (v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (x + gmnl l) \<and> p (x + gmnl l + gmn n) \<and> v # va = l @ n # r; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmnl (a # v # va)); splitNlist p i (a # v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
[PROOF STEP]
note miv = IV2(2)[of "i + gmn a" l1 n1 r1]
[PROOF STATE]
proof (state)
this:
\<lbrakk>i + gmn a = i + gmn a; \<not> p (i + gmn a); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p (i + gmn a); p (i + gmn a + gmnl (v # va)); splitNlist p (i + gmn a) (v # va) = (l1, n1, r1)\<rbrakk> \<Longrightarrow> \<not> p (i + gmn a + gmnl l1) \<and> p (i + gmn a + gmnl l1 + gmn n1) \<and> v # va = l1 @ n1 # r1

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmn a); \<And>x l n r. \<lbrakk>x = i + gmn a; \<not> p x; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmnl (v # va)); splitNlist p x (v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (x + gmnl l) \<and> p (x + gmnl l + gmn n) \<and> v # va = l @ n # r; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmnl (a # v # va)); splitNlist p i (a # v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
[PROOF STEP]
have v2:"p (i + gmn a + gmnl (v # va))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p (i + gmn a + gmnl (v # va))
[PROOF STEP]
using IV2(5)
[PROOF STATE]
proof (prove)
using this:
p (i + gmnl (a # v # va))

goal (1 subgoal):
 1. p (i + gmn a + gmnl (v # va))
[PROOF STEP]
by (simp add: add.assoc)
[PROOF STATE]
proof (state)
this:
p (i + gmn a + gmnl (v # va))

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmn a); \<And>x l n r. \<lbrakk>x = i + gmn a; \<not> p x; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmnl (v # va)); splitNlist p x (v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (x + gmnl l) \<and> p (x + gmnl l + gmn n) \<and> v # va = l @ n # r; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmnl (a # v # va)); splitNlist p i (a # v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
[PROOF STEP]
note miv2 =  miv[OF _ IV2(1) IV2(3) IV2(1)  v2 v1]
[PROOF STATE]
proof (state)
this:
\<lbrakk>i + gmn a = i + gmn a; \<And>a b. p a \<Longrightarrow> p a\<rbrakk> \<Longrightarrow> \<not> p (i + gmn a + gmnl l1) \<and> p (i + gmn a + gmnl l1 + gmn n1) \<and> v # va = l1 @ n1 # r1

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmn a); \<And>x l n r. \<lbrakk>x = i + gmn a; \<not> p x; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmnl (v # va)); splitNlist p x (v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (x + gmnl l) \<and> p (x + gmnl l + gmn n) \<and> v # va = l @ n # r; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmnl (a # v # va)); splitNlist p i (a # v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
[PROOF STEP]
have v3: "a # l1 = l" "n1 = n" "r1 = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a # l1 = l &&& n1 = n &&& r1 = r
[PROOF STEP]
using IV2 v1
[PROOF STATE]
proof (prove)
using this:
\<not> p (i + gmn a)
\<lbrakk>?x = i + gmn a; \<not> p ?x; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p ?x; p (?x + gmnl (v # va)); splitNlist p ?x (v # va) = (?l, ?n, ?r)\<rbrakk> \<Longrightarrow> \<not> p (?x + gmnl ?l) \<and> p (?x + gmnl ?l + gmn ?n) \<and> v # va = ?l @ ?n # ?r
p ?a \<Longrightarrow> p (?a + ?b)
\<not> p i
p (i + gmnl (a # v # va))
splitNlist p i (a # v # va) = (l, n, r)
splitNlist p (i + gmn a) (v # va) = (l1, n1, r1)

goal (1 subgoal):
 1. a # l1 = l &&& n1 = n &&& r1 = r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a # l1 = l
n1 = n
r1 = r

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmn a); \<And>x l n r. \<lbrakk>x = i + gmn a; \<not> p x; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmnl (v # va)); splitNlist p x (v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (x + gmnl l) \<and> p (x + gmnl l + gmn n) \<and> v # va = l @ n # r; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmnl (a # v # va)); splitNlist p i (a # v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
[PROOF STEP]
with miv2
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i + gmn a = i + gmn a; \<And>a b. p a \<Longrightarrow> p a\<rbrakk> \<Longrightarrow> \<not> p (i + gmn a + gmnl l1) \<and> p (i + gmn a + gmnl l1 + gmn n1) \<and> v # va = l1 @ n1 # r1
a # l1 = l
n1 = n
r1 = r
[PROOF STEP]
have
        v4: "\<not> p (i + gmn a + gmnl l1) \<and>
             p (i + gmn a + gmnl l1 + gmn n1) \<and>
             v # va = l1 @ n1 # r1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i + gmn a = i + gmn a; \<And>a b. p a \<Longrightarrow> p a\<rbrakk> \<Longrightarrow> \<not> p (i + gmn a + gmnl l1) \<and> p (i + gmn a + gmnl l1 + gmn n1) \<and> v # va = l1 @ n1 # r1
a # l1 = l
n1 = n
r1 = r

goal (1 subgoal):
 1. \<not> p (i + gmn a + gmnl l1) \<and> p (i + gmn a + gmnl l1 + gmn n1) \<and> v # va = l1 @ n1 # r1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> p (i + gmn a + gmnl l1) \<and> p (i + gmn a + gmnl l1 + gmn n1) \<and> v # va = l1 @ n1 # r1

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmn a); \<And>x l n r. \<lbrakk>x = i + gmn a; \<not> p x; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmnl (v # va)); splitNlist p x (v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (x + gmnl l) \<and> p (x + gmnl l + gmn n) \<and> v # va = l @ n # r; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmnl (a # v # va)); splitNlist p i (a # v # va) = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
[PROOF STEP]
with v2 v3
[PROOF STATE]
proof (chain)
picking this:
p (i + gmn a + gmnl (v # va))
a # l1 = l
n1 = n
r1 = r
\<not> p (i + gmn a + gmnl l1) \<and> p (i + gmn a + gmnl l1 + gmn n1) \<and> v # va = l1 @ n1 # r1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p (i + gmn a + gmnl (v # va))
a # l1 = l
n1 = n
r1 = r
\<not> p (i + gmn a + gmnl l1) \<and> p (i + gmn a + gmnl l1 + gmn n1) \<and> v # va = l1 @ n1 # r1

goal (1 subgoal):
 1. \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r
[PROOF STEP]
by (auto simp add: add.assoc)
[PROOF STATE]
proof (state)
this:
\<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn n) \<and> a # v # va = l @ n # r

goal (1 subgoal):
 1. \<And>a b l n r. \<lbrakk>\<And>aa b. a aa \<Longrightarrow> a (aa + b); \<not> a b; a (b + gmnl []); splitNlist a b [] = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> a (b + gmnl l) \<and> a (b + gmnl l + gmn n) \<and> [] = l @ n # r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b l n r. \<lbrakk>\<And>aa b. a aa \<Longrightarrow> a (aa + b); \<not> a b; a (b + gmnl []); splitNlist a b [] = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> a (b + gmnl l) \<and> a (b + gmnl l + gmn n) \<and> [] = l @ n # r
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
a_ ?a \<Longrightarrow> a_ (?a + ?b)
\<not> a_ b_
a_ (b_ + gmnl [])
splitNlist a_ b_ [] = (l, n, r)

goal (1 subgoal):
 1. \<And>a b l n r. \<lbrakk>\<And>aa b. a aa \<Longrightarrow> a (aa + b); \<not> a b; a (b + gmnl []); splitNlist a b [] = (l, n, r)\<rbrakk> \<Longrightarrow> \<not> a (b + gmnl l) \<and> a (b + gmnl l + gmn n) \<and> [] = l @ n # r
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
a_ ?a \<Longrightarrow> a_ (?a + ?b)
\<not> a_ b_
a_ (b_ + gmnl [])
splitNlist a_ b_ [] = (l, n, r)

goal (1 subgoal):
 1. \<not> a_ (b_ + gmnl l) \<and> a_ (b_ + gmnl l + gmn n) \<and> [] = l @ n # r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> a_ (b_ + gmnl l) \<and> a_ (b_ + gmnl l + gmn n) \<and> [] = l @ n # r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma digitToNlist_inv:
  "is_measured_digit d \<Longrightarrow> (\<forall> x \<in> set (digitToNlist d). is_measured_node x)"
  "is_leveln_digit n d \<Longrightarrow> (\<forall> x \<in> set (digitToNlist d). is_leveln_node n x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_measured_digit d \<Longrightarrow> \<forall>x\<in>set (digitToNlist d). is_measured_node x) &&& (is_leveln_digit n d \<Longrightarrow> \<forall>x\<in>set (digitToNlist d). is_leveln_node n x)
[PROOF STEP]
by (cases d, auto)(cases d, auto)


[STATEMENT]
lemma gmnl_gmd:
  "is_measured_digit d \<Longrightarrow> gmnl (digitToNlist d) = gmd d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_measured_digit d \<Longrightarrow> gmnl (digitToNlist d) = gmd d
[PROOF STEP]
by (cases d, auto simp add: add.assoc)


[STATEMENT]
lemma gmn_gmd:
  "is_measured_node nd \<Longrightarrow> gmd (nodeToDigit nd) = gmn nd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_measured_node nd \<Longrightarrow> gmd (nodeToDigit nd) = gmn nd
[PROOF STEP]
by (auto simp add: nodeToDigit_inv nodeToDigit_list gmn_correct gmd_correct)


[STATEMENT]
lemma splitDigit_inv:
  "\<lbrakk>
  \<And>(a::'a) (b::'a). p a \<Longrightarrow> p (a + b);
  \<not> p i;
  is_measured_digit d;
  is_leveln_digit n d;
  p (i + gmd (d ::('e,'a::monoid_add) Digit));
  splitDigit p i d = (l, nd, r)
  \<rbrakk> \<Longrightarrow>
  \<not> p (i + (gmnl l))
  \<and>
  p (i + (gmnl l) + (gmn nd))
  \<and>
  (\<forall> x \<in> set l. (is_measured_node x \<and> is_leveln_node n x))
  \<and>
  (\<forall> x \<in> set r. (is_measured_node x \<and> is_leveln_node n x))
  \<and>
  (is_measured_node nd \<and> is_leveln_node n nd )
  "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; is_measured_digit d; is_leveln_digit n d; p (i + gmd d); splitDigit p i d = (l, nd, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> (\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node nd \<and> is_leveln_node n nd
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; is_measured_digit d; is_leveln_digit n d; p (i + gmd d); splitDigit p i d = (l, nd, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> (\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node nd \<and> is_leveln_node n nd
[PROOF STEP]
fix p i d n l nd r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; is_measured_digit d; is_leveln_digit n d; p (i + gmd d); splitDigit p i d = (l, nd, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> (\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node nd \<and> is_leveln_node n nd
[PROOF STEP]
assume assms: "\<And>a b. p a \<Longrightarrow> p (a + b)" "\<not> p i" "is_measured_digit d"
    "p (i + gmd d)" "splitDigit p i d = (l, nd, r)"
    "is_leveln_digit n d"
[PROOF STATE]
proof (state)
this:
p ?a \<Longrightarrow> p (?a + ?b)
\<not> p i
is_measured_digit d
p (i + gmd d)
splitDigit p i d = (l, nd, r)
is_leveln_digit n d

goal (1 subgoal):
 1. \<lbrakk>\<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; is_measured_digit d; is_leveln_digit n d; p (i + gmd d); splitDigit p i d = (l, nd, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> (\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node nd \<and> is_leveln_node n nd
[PROOF STEP]
from assms(3, 4)
[PROOF STATE]
proof (chain)
picking this:
is_measured_digit d
p (i + gmd d)
[PROOF STEP]
have v1: "p (i + gmnl (digitToNlist d))"
[PROOF STATE]
proof (prove)
using this:
is_measured_digit d
p (i + gmd d)

goal (1 subgoal):
 1. p (i + gmnl (digitToNlist d))
[PROOF STEP]
by (simp add: gmnl_gmd)
[PROOF STATE]
proof (state)
this:
p (i + gmnl (digitToNlist d))

goal (1 subgoal):
 1. \<lbrakk>\<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; is_measured_digit d; is_leveln_digit n d; p (i + gmd d); splitDigit p i d = (l, nd, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> (\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node nd \<and> is_leveln_node n nd
[PROOF STEP]
note snc = splitNlist_correct [of p i "digitToNlist d" l nd r]
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmnl (digitToNlist d)); splitNlist p i (digitToNlist d) = (l, nd, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> digitToNlist d = l @ nd # r

goal (1 subgoal):
 1. \<lbrakk>\<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; is_measured_digit d; is_leveln_digit n d; p (i + gmd d); splitDigit p i d = (l, nd, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> (\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node nd \<and> is_leveln_node n nd
[PROOF STEP]
from assms(5)
[PROOF STATE]
proof (chain)
picking this:
splitDigit p i d = (l, nd, r)
[PROOF STEP]
have v2: "splitNlist p i (digitToNlist d) = (l, nd, r)"
[PROOF STATE]
proof (prove)
using this:
splitDigit p i d = (l, nd, r)

goal (1 subgoal):
 1. splitNlist p i (digitToNlist d) = (l, nd, r)
[PROOF STEP]
by (simp add: splitDigit_def)
[PROOF STATE]
proof (state)
this:
splitNlist p i (digitToNlist d) = (l, nd, r)

goal (1 subgoal):
 1. \<lbrakk>\<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; is_measured_digit d; is_leveln_digit n d; p (i + gmd d); splitDigit p i d = (l, nd, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> (\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node nd \<and> is_leveln_node n nd
[PROOF STEP]
note snc1 = snc[OF assms(1) assms(2) v1 v2]
[PROOF STATE]
proof (state)
this:
(\<And>a b. p a \<Longrightarrow> p a) \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> digitToNlist d = l @ nd # r

goal (1 subgoal):
 1. \<lbrakk>\<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; is_measured_digit d; is_leveln_digit n d; p (i + gmd d); splitDigit p i d = (l, nd, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> (\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node nd \<and> is_leveln_node n nd
[PROOF STEP]
hence v3: "\<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and>
             digitToNlist d = l @ nd # r"
[PROOF STATE]
proof (prove)
using this:
(\<And>a b. p a \<Longrightarrow> p a) \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> digitToNlist d = l @ nd # r

goal (1 subgoal):
 1. \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> digitToNlist d = l @ nd # r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> digitToNlist d = l @ nd # r

goal (1 subgoal):
 1. \<lbrakk>\<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; is_measured_digit d; is_leveln_digit n d; p (i + gmd d); splitDigit p i d = (l, nd, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> (\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node nd \<and> is_leveln_node n nd
[PROOF STEP]
from assms(3,6)
[PROOF STATE]
proof (chain)
picking this:
is_measured_digit d
is_leveln_digit n d
[PROOF STEP]
have
    v4:" \<forall> x \<in> set (digitToNlist d). is_measured_node x"
    " \<forall> x \<in> set (digitToNlist d). is_leveln_node n x"
[PROOF STATE]
proof (prove)
using this:
is_measured_digit d
is_leveln_digit n d

goal (1 subgoal):
 1. \<forall>x\<in>set (digitToNlist d). is_measured_node x &&& \<forall>x\<in>set (digitToNlist d). is_leveln_node n x
[PROOF STEP]
by(auto simp add: digitToNlist_inv)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (digitToNlist d). is_measured_node x
\<forall>x\<in>set (digitToNlist d). is_leveln_node n x

goal (1 subgoal):
 1. \<lbrakk>\<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; is_measured_digit d; is_leveln_digit n d; p (i + gmd d); splitDigit p i d = (l, nd, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> (\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node nd \<and> is_leveln_node n nd
[PROOF STEP]
with v3
[PROOF STATE]
proof (chain)
picking this:
\<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> digitToNlist d = l @ nd # r
\<forall>x\<in>set (digitToNlist d). is_measured_node x
\<forall>x\<in>set (digitToNlist d). is_leveln_node n x
[PROOF STEP]
have v5: "\<forall> x \<in> set l. (is_measured_node x \<and> is_leveln_node n x)"
    "\<forall> x \<in> set r. (is_measured_node x \<and> is_leveln_node n x)"
    "is_measured_node nd \<and> is_leveln_node n nd"
[PROOF STATE]
proof (prove)
using this:
\<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> digitToNlist d = l @ nd # r
\<forall>x\<in>set (digitToNlist d). is_measured_node x
\<forall>x\<in>set (digitToNlist d). is_leveln_node n x

goal (1 subgoal):
 1. \<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x &&& \<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x &&& is_measured_node nd \<and> is_leveln_node n nd
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x
\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x
is_measured_node nd \<and> is_leveln_node n nd

goal (1 subgoal):
 1. \<lbrakk>\<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; is_measured_digit d; is_leveln_digit n d; p (i + gmd d); splitDigit p i d = (l, nd, r)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> (\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node nd \<and> is_leveln_node n nd
[PROOF STEP]
with v3 v5
[PROOF STATE]
proof (chain)
picking this:
\<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> digitToNlist d = l @ nd # r
\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x
\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x
is_measured_node nd \<and> is_leveln_node n nd
\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x
\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x
is_measured_node nd \<and> is_leveln_node n nd
[PROOF STEP]
show
    "\<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and>
    (\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x) \<and>
    (\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x) \<and>
    is_measured_node nd \<and> is_leveln_node n nd"
[PROOF STATE]
proof (prove)
using this:
\<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> digitToNlist d = l @ nd # r
\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x
\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x
is_measured_node nd \<and> is_leveln_node n nd
\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x
\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x
is_measured_node nd \<and> is_leveln_node n nd

goal (1 subgoal):
 1. \<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> (\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node nd \<and> is_leveln_node n nd
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> p (i + gmnl l) \<and> p (i + gmnl l + gmn nd) \<and> (\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node nd \<and> is_leveln_node n nd

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma splitDigit_inv':
  "\<lbrakk>
  splitDigit p i d = (l, nd, r);
  is_measured_digit d;
  is_leveln_digit n d
  \<rbrakk> \<Longrightarrow>
  (\<forall> x \<in> set l. (is_measured_node x \<and> is_leveln_node n x))
  \<and>
  (\<forall> x \<in> set r. (is_measured_node x \<and> is_leveln_node n x))
  \<and>
  (is_measured_node nd \<and> is_leveln_node n nd )
  "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>splitDigit p i d = (l, nd, r); is_measured_digit d; is_leveln_digit n d\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node nd \<and> is_leveln_node n nd
[PROOF STEP]
apply (unfold splitDigit_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>splitNlist p i (digitToNlist d) = (l, nd, r); is_measured_digit d; is_leveln_digit n d\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node nd \<and> is_leveln_node n nd
[PROOF STEP]
apply (cases d)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1. \<lbrakk>splitNlist p i (digitToNlist d) = (l, nd, r); is_measured_digit d; is_leveln_digit n d; d = One x1\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node nd \<and> is_leveln_node n nd
 2. \<And>x21 x22. \<lbrakk>splitNlist p i (digitToNlist d) = (l, nd, r); is_measured_digit d; is_leveln_digit n d; d = Two x21 x22\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node nd \<and> is_leveln_node n nd
 3. \<And>x31 x32 x33. \<lbrakk>splitNlist p i (digitToNlist d) = (l, nd, r); is_measured_digit d; is_leveln_digit n d; d = Three x31 x32 x33\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node nd \<and> is_leveln_node n nd
 4. \<And>x41 x42 x43 x44. \<lbrakk>splitNlist p i (digitToNlist d) = (l, nd, r); is_measured_digit d; is_leveln_digit n d; d = Four x41 x42 x43 x44\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set l. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node nd \<and> is_leveln_node n nd
[PROOF STEP]
apply (auto split: if_split_asm simp add: Let_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma splitDigit_list: "splitDigit p i d = (l,n,r) \<Longrightarrow>
  (digitToList d) = (nlistToList l) @ (nodeToList n) @ (nlistToList r)
  \<and> length l \<le> 4 \<and> length r \<le> 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. splitDigit p i d = (l, n, r) \<Longrightarrow> digitToList d = nlistToList l @ nodeToList n @ nlistToList r \<and> length l \<le> 4 \<and> length r \<le> 4
[PROOF STEP]
apply (unfold splitDigit_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. splitNlist p i (digitToNlist d) = (l, n, r) \<Longrightarrow> digitToList d = nlistToList l @ nodeToList n @ nlistToList r \<and> length l \<le> 4 \<and> length r \<le> 4
[PROOF STEP]
apply (cases d)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1. \<lbrakk>splitNlist p i (digitToNlist d) = (l, n, r); d = One x1\<rbrakk> \<Longrightarrow> digitToList d = nlistToList l @ nodeToList n @ nlistToList r \<and> length l \<le> 4 \<and> length r \<le> 4
 2. \<And>x21 x22. \<lbrakk>splitNlist p i (digitToNlist d) = (l, n, r); d = Two x21 x22\<rbrakk> \<Longrightarrow> digitToList d = nlistToList l @ nodeToList n @ nlistToList r \<and> length l \<le> 4 \<and> length r \<le> 4
 3. \<And>x31 x32 x33. \<lbrakk>splitNlist p i (digitToNlist d) = (l, n, r); d = Three x31 x32 x33\<rbrakk> \<Longrightarrow> digitToList d = nlistToList l @ nodeToList n @ nlistToList r \<and> length l \<le> 4 \<and> length r \<le> 4
 4. \<And>x41 x42 x43 x44. \<lbrakk>splitNlist p i (digitToNlist d) = (l, n, r); d = Four x41 x42 x43 x44\<rbrakk> \<Longrightarrow> digitToList d = nlistToList l @ nodeToList n @ nlistToList r \<and> length l \<le> 4 \<and> length r \<le> 4
[PROOF STEP]
apply (auto split: if_split_asm simp add: Let_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma gmnl_gmft: "\<forall> x \<in> set nl. is_measured_node x \<Longrightarrow>
  gmft (nlistToTree nl) = gmnl nl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set nl. is_measured_node x \<Longrightarrow> gmft (nlistToTree nl) = gmnl nl
[PROOF STEP]
by (auto simp add: gmnl_correct[of nl] nlistToTree_list[of nl]
                   nlistToTree_inv[of nl]  gmft_correct[of "nlistToTree nl"])


[STATEMENT]
lemma gmftR_gmnl:
  assumes "is_leveln_ftree (Suc n) m \<and> is_measured_ftree m"
  and "is_leveln_digit n pr \<and> is_measured_digit pr"
  and "\<forall> x \<in> set sf. (is_measured_node x \<and> is_leveln_node n x) \<and> length sf \<le> 4"
  shows "gmft (deepR pr m sf) = gmd pr + gmft m + gmnl sf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gmft (deepR pr m sf) = gmd pr + gmft m + gmnl sf
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gmft (deepR pr m sf) = gmd pr + gmft m + gmnl sf
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n pr \<and> is_measured_digit pr
\<forall>x\<in>set sf. (is_measured_node x \<and> is_leveln_node n x) \<and> length sf \<le> 4
[PROOF STEP]
have
    v1: "toList (deepR pr m sf) = digitToList pr @ toList m @ nlistToList sf"
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n pr \<and> is_measured_digit pr
\<forall>x\<in>set sf. (is_measured_node x \<and> is_leveln_node n x) \<and> length sf \<le> 4

goal (1 subgoal):
 1. toList (deepR pr m sf) = digitToList pr @ toList m @ nlistToList sf
[PROOF STEP]
by (auto simp add: deepR_list)
[PROOF STATE]
proof (state)
this:
toList (deepR pr m sf) = digitToList pr @ toList m @ nlistToList sf

goal (1 subgoal):
 1. gmft (deepR pr m sf) = gmd pr + gmft m + gmnl sf
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n pr \<and> is_measured_digit pr
\<forall>x\<in>set sf. (is_measured_node x \<and> is_leveln_node n x) \<and> length sf \<le> 4
[PROOF STEP]
have
    v2: "is_measured_ftree (deepR pr m sf)"
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n pr \<and> is_measured_digit pr
\<forall>x\<in>set sf. (is_measured_node x \<and> is_leveln_node n x) \<and> length sf \<le> 4

goal (1 subgoal):
 1. is_measured_ftree (deepR pr m sf)
[PROOF STEP]
by (auto simp add: deepR_inv)
[PROOF STATE]
proof (state)
this:
is_measured_ftree (deepR pr m sf)

goal (1 subgoal):
 1. gmft (deepR pr m sf) = gmd pr + gmft m + gmnl sf
[PROOF STEP]
with v1
[PROOF STATE]
proof (chain)
picking this:
toList (deepR pr m sf) = digitToList pr @ toList m @ nlistToList sf
is_measured_ftree (deepR pr m sf)
[PROOF STEP]
have
    v3: "gmft (deepR pr m sf) =
        sum_list (map snd (digitToList pr @ toList m @ nlistToList sf))"
[PROOF STATE]
proof (prove)
using this:
toList (deepR pr m sf) = digitToList pr @ toList m @ nlistToList sf
is_measured_ftree (deepR pr m sf)

goal (1 subgoal):
 1. gmft (deepR pr m sf) = sum_list (map snd (digitToList pr @ toList m @ nlistToList sf))
[PROOF STEP]
by (auto simp add: gmft_correct)
[PROOF STATE]
proof (state)
this:
gmft (deepR pr m sf) = sum_list (map snd (digitToList pr @ toList m @ nlistToList sf))

goal (1 subgoal):
 1. gmft (deepR pr m sf) = gmd pr + gmft m + gmnl sf
[PROOF STEP]
have
    v4:"gmd pr + gmft m + gmnl sf =
        sum_list (map snd (digitToList pr @ toList m @ nlistToList sf))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gmd pr + gmft m + gmnl sf = sum_list (map snd (digitToList pr @ toList m @ nlistToList sf))
[PROOF STEP]
by (auto simp add: gmd_correct gmft_correct gmnl_correct assms add.assoc)
[PROOF STATE]
proof (state)
this:
gmd pr + gmft m + gmnl sf = sum_list (map snd (digitToList pr @ toList m @ nlistToList sf))

goal (1 subgoal):
 1. gmft (deepR pr m sf) = gmd pr + gmft m + gmnl sf
[PROOF STEP]
with v3
[PROOF STATE]
proof (chain)
picking this:
gmft (deepR pr m sf) = sum_list (map snd (digitToList pr @ toList m @ nlistToList sf))
gmd pr + gmft m + gmnl sf = sum_list (map snd (digitToList pr @ toList m @ nlistToList sf))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
gmft (deepR pr m sf) = sum_list (map snd (digitToList pr @ toList m @ nlistToList sf))
gmd pr + gmft m + gmnl sf = sum_list (map snd (digitToList pr @ toList m @ nlistToList sf))

goal (1 subgoal):
 1. gmft (deepR pr m sf) = gmd pr + gmft m + gmnl sf
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gmft (deepR pr m sf) = gmd pr + gmft m + gmnl sf

goal:
No subgoals!
[PROOF STEP]
qed