[STATEMENT]
lemma zippers_rose_tree_same_hash':
  assumes "z \<in> set (zippers_rose_tree e h (p, t))"
  shows "hash_tree h (tree_of_zipper\<^sub>m z) = 
    hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
z \<in> set (zippers_rose_tree e h (p, t))

goal (1 subgoal):
 1. hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
proof(induction "(p, t)" arbitrary: p t rule: zippers_rose_tree.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p t. \<lbrakk>\<And>pa ta. \<lbrakk>(pa, ta) \<in> set (zipper_children (p, t)); z \<in> set (zippers_rose_tree e h (pa, ta))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e pa, embed_source_tree e ta)); z \<in> set (zippers_rose_tree e h (p, t))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
case (1 p t)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?p, ?t) \<in> set (zipper_children (p, t)); z \<in> set (zippers_rose_tree e h (?p, ?t))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e ?p, embed_source_tree e ?t))
z \<in> set (zippers_rose_tree e h (p, t))

goal (1 subgoal):
 1. \<And>p t. \<lbrakk>\<And>pa ta. \<lbrakk>(pa, ta) \<in> set (zipper_children (p, t)); z \<in> set (zippers_rose_tree e h (pa, ta))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e pa, embed_source_tree e ta)); z \<in> set (zippers_rose_tree e h (p, t))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
from "1.prems"[unfolded zippers_rose_tree.simps]
[PROOF STATE]
proof (chain)
picking this:
z \<in> set ((blind_path e h p, embed_source_tree e t) # concat (map (zippers_rose_tree e h) (zipper_children (p, t))))
[PROOF STEP]
consider (find) "z = (blind_path e h p, embed_source_tree e t)"
    | (rec) x ts l t' r where "t = Tree (x, ts)" "(l, t', r) \<in> set (splits ts)" "z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))"
[PROOF STATE]
proof (prove)
using this:
z \<in> set ((blind_path e h p, embed_source_tree e t) # concat (map (zippers_rose_tree e h) (zipper_children (p, t))))

goal (1 subgoal):
 1. \<lbrakk>z = (blind_path e h p, embed_source_tree e t) \<Longrightarrow> thesis; \<And>x ts l t' r. \<lbrakk>t = Tree (x, ts); (l, t', r) \<in> set (splits ts); z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by(cases t)(auto simp add: zipper_children.simps)
[PROOF STATE]
proof (state)
this:
\<lbrakk>z = (blind_path e h p, embed_source_tree e t) \<Longrightarrow> ?thesis; \<And>x ts l t' r. \<lbrakk>t = Tree (x, ts); (l, t', r) \<in> set (splits ts); z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>p t. \<lbrakk>\<And>pa ta. \<lbrakk>(pa, ta) \<in> set (zipper_children (p, t)); z \<in> set (zippers_rose_tree e h (pa, ta))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e pa, embed_source_tree e ta)); z \<in> set (zippers_rose_tree e h (p, t))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>z = (blind_path e h p, embed_source_tree e t) \<Longrightarrow> ?thesis; \<And>x ts l t' r. \<lbrakk>t = Tree (x, ts); (l, t', r) \<in> set (splits ts); z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>z = (blind_path e h p, embed_source_tree e t) \<Longrightarrow> ?thesis; \<And>x ts l t' r. \<lbrakk>t = Tree (x, ts); (l, t', r) \<in> set (splits ts); z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = (blind_path e h p, embed_source_tree e t) \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
 2. \<And>x ts l t' r. \<lbrakk>t = Tree (x, ts); (l, t', r) \<in> set (splits ts); z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
case rec
[PROOF STATE]
proof (state)
this:
t = Tree (x, ts)
(l, t', r) \<in> set (splits ts)
z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))

goal (2 subgoals):
 1. z = (blind_path e h p, embed_source_tree e t) \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
 2. \<And>x ts l t' r. \<lbrakk>t = Tree (x, ts); (l, t', r) \<in> set (splits ts); z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t = Tree (x, ts)
(l, t', r) \<in> set (splits ts)
z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t = Tree (x, ts)
(l, t', r) \<in> set (splits ts)
z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))

goal (1 subgoal):
 1. hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
apply(subst "1.hyps"[of "(x, l, r) # p" "t'"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>t = Tree (x, ts); (l, t', r) \<in> set (splits ts); z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))\<rbrakk> \<Longrightarrow> ((x, l, r) # p, t') \<in> set (zipper_children (p, t))
 2. \<lbrakk>t = Tree (x, ts); (l, t', r) \<in> set (splits ts); z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))\<rbrakk> \<Longrightarrow> z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))
 3. \<lbrakk>t = Tree (x, ts); (l, t', r) \<in> set (splits ts); z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m (embed_path e ((x, l, r) # p), embed_source_tree e t')) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
apply(simp_all add: rev_image_eqI zipper_children.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t = Tree (x, ts); (l, t', r) \<in> set (splits ts); z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m (embed_path e ((x, l, r) # p), embed_source_tree e t')) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, Tree\<^sub>m (Unblinded (e x, map (embed_source_tree e) ts))))
[PROOF STEP]
by (metis (no_types) childz_same_tree comp_apply embed_source_tree.simps rec(2))
[PROOF STATE]
proof (state)
this:
hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))

goal (1 subgoal):
 1. z = (blind_path e h p, embed_source_tree e t) \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
qed(simp add: blind_embed_path_same_hash)
[PROOF STATE]
proof (state)
this:
hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))

goal:
No subgoals!
[PROOF STEP]
qed