[STATEMENT]
lemma denormalize_hd_root:
  assumes "root t \<noteq> []"
  shows "hd (denormalize t) = hd (root t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (denormalize t) = hd (dtree.root t)
[PROOF STEP]
proof(cases "\<forall>x. sucs t \<noteq> {|x|}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>x. sucs t \<noteq> {|x|} \<Longrightarrow> hd (denormalize t) = hd (dtree.root t)
 2. \<not> (\<forall>x. sucs t \<noteq> {|x|}) \<Longrightarrow> hd (denormalize t) = hd (dtree.root t)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>x. sucs t \<noteq> {|x|}

goal (2 subgoals):
 1. \<forall>x. sucs t \<noteq> {|x|} \<Longrightarrow> hd (denormalize t) = hd (dtree.root t)
 2. \<not> (\<forall>x. sucs t \<noteq> {|x|}) \<Longrightarrow> hd (denormalize t) = hd (dtree.root t)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. sucs t \<noteq> {|x|}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x. sucs t \<noteq> {|x|}

goal (1 subgoal):
 1. hd (denormalize t) = hd (dtree.root t)
[PROOF STEP]
using denormalize.simps(2)[of "sucs t" "root t"]
[PROOF STATE]
proof (prove)
using this:
\<forall>x. sucs t \<noteq> {|x|}
\<forall>x. sucs t \<noteq> {|x|} \<Longrightarrow> denormalize (Node (dtree.root t) (sucs t)) = dtree.root t

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

goal (1 subgoal):
 1. \<not> (\<forall>x. sucs t \<noteq> {|x|}) \<Longrightarrow> hd (denormalize t) = hd (dtree.root t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>x. sucs t \<noteq> {|x|}) \<Longrightarrow> hd (denormalize t) = hd (dtree.root t)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>x. sucs t \<noteq> {|x|})

goal (1 subgoal):
 1. \<not> (\<forall>x. sucs t \<noteq> {|x|}) \<Longrightarrow> hd (denormalize t) = hd (dtree.root t)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>x. sucs t \<noteq> {|x|})
[PROOF STEP]
obtain t1 e where "{|(t1, e)|} = sucs t"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>x. sucs t \<noteq> {|x|})

goal (1 subgoal):
 1. (\<And>t1 e. {|(t1, e)|} = sucs t \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{|(t1, e)|} = sucs t

goal (1 subgoal):
 1. \<not> (\<forall>x. sucs t \<noteq> {|x|}) \<Longrightarrow> hd (denormalize t) = hd (dtree.root t)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{|(t1, e)|} = sucs t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{|(t1, e)|} = sucs t

goal (1 subgoal):
 1. hd (denormalize t) = hd (dtree.root t)
[PROOF STEP]
using denormalize.simps(1)[of "root t" t1 e] assms
[PROOF STATE]
proof (prove)
using this:
{|(t1, e)|} = sucs t
denormalize (Node (dtree.root t) {|(t1, e)|}) = dtree.root t @ denormalize t1
dtree.root t \<noteq> []

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

goal:
No subgoals!
[PROOF STEP]
qed