[STATEMENT]
lemma os_prec:
  "precise os_list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. precise os_list
[PROOF STEP]
by rule (simp add: lseg_prec2)


[STATEMENT]
lemma os_imp_list_impl: "imp_list os_list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_list os_list
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. precise os_list
[PROOF STEP]
apply (rule os_prec)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma os_empty_rule: "<emp> os_empty <os_list []>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <emp> os_empty <os_list []>
[PROOF STEP]
unfolding os_empty_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <emp> return None <os_list []>
[PROOF STEP]
apply sep_auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma os_empty_impl: "imp_list_empty os_list os_empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_list_empty os_list os_empty
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <emp> os_empty <os_list []>\<^sub>t
[PROOF STEP]
apply (sep_auto heap add: os_empty_rule)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma os_is_empty_rule:
  "<os_list xs b> os_is_empty b <\<lambda>r. os_list xs b * \<up>(r \<longleftrightarrow> xs = [])>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_list xs b> os_is_empty b <\<lambda>r. os_list xs b * \<up> (r = (xs = []))>
[PROOF STEP]
unfolding os_is_empty_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_list xs b> return (b = None) <\<lambda>r. os_list xs b * \<up> (r = (xs = []))>
[PROOF STEP]
apply sep_auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma os_is_empty_impl: "imp_list_is_empty os_list os_is_empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_list_is_empty os_list os_is_empty
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l p. <os_list l p> os_is_empty p <\<lambda>r. os_list l p * \<up> (r = (l = []))>\<^sub>t
[PROOF STEP]
apply (sep_auto heap add: os_is_empty_rule)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma os_prepend_rule:
  "<os_list xs n> os_prepend x n <os_list (x # xs)>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_list xs n> os_prepend x n <os_list (x # xs)>
[PROOF STEP]
unfolding os_prepend_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_list xs n> ref (Node x n) \<bind> (\<lambda>p. return (Some p)) <os_list (x # xs)>
[PROOF STEP]
apply sep_auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma os_prepend_impl: "imp_list_prepend os_list os_prepend"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_list_prepend os_list os_prepend
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l p a. <os_list l p> os_prepend a p <os_list (a # l)>\<^sub>t
[PROOF STEP]
apply (sep_auto heap add: os_prepend_rule)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma os_pop_rule:
  "xs \<noteq> [] \<Longrightarrow> <os_list xs r>
  os_pop r
  <\<lambda>(x,r'). os_list (tl xs) r' * (the r) \<mapsto>\<^sub>r (Node x r') * \<up>(x = hd xs)>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> <os_list xs r> os_pop r <\<lambda>(x, r'). os_list (tl xs) r' * the r \<mapsto>\<^sub>r Node x r' * \<up> (x = hd xs)>
[PROOF STEP]
apply (cases r, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>xs \<noteq> []; r = Some a\<rbrakk> \<Longrightarrow> <os_list xs (Some a)> os_pop (Some a) <\<lambda>(x, r'). os_list (tl xs) r' * a \<mapsto>\<^sub>r Node x r' * \<up> (x = hd xs)>
[PROOF STEP]
apply (cases xs, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa list. \<lbrakk>r = Some a; xs = aa # list\<rbrakk> \<Longrightarrow> <\<exists>\<^sub>App n. pp \<mapsto>\<^sub>r Node aa n * os_list list n * \<up> (a = pp)> os_pop (Some a) <\<lambda>(x, r'). os_list list r' * a \<mapsto>\<^sub>r Node x r' * \<up> (x = aa)>
[PROOF STEP]
apply (sep_auto simp: os_pop.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma os_pop_impl: "imp_list_pop os_list os_pop"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_list_pop os_list os_pop
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l p. l \<noteq> [] \<Longrightarrow> <os_list l p> os_pop p <\<lambda>r. case r of (r, p') \<Rightarrow> os_list (tl l) p' * \<up> (r = hd l)>\<^sub>t
[PROOF STEP]
apply (sep_auto heap add: os_pop_rule)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [simp, sep_dflt_simps]:
  "os_reverse_aux q None = return q"
  "os_reverse_aux q (Some r) = do {
      v \<leftarrow> !r;
      r := Node (val v) q;
      os_reverse_aux (Some r) (next v) }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. os_reverse_aux q None = return q &&& os_reverse_aux q (Some r) = !r \<bind> (\<lambda>v. r := Node (val v) q \<bind> (\<lambda>_. os_reverse_aux (Some r) (next v)))
[PROOF STEP]
apply (subst os_reverse_aux.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (case None of None \<Rightarrow> return q | Some r \<Rightarrow> !r \<bind> (\<lambda>v. r := Node (val v) q \<bind> (\<lambda>_. os_reverse_aux None (next v)))) = return q
 2. os_reverse_aux q (Some r) = !r \<bind> (\<lambda>v. r := Node (val v) q \<bind> (\<lambda>_. os_reverse_aux (Some r) (next v)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. os_reverse_aux q (Some r) = !r \<bind> (\<lambda>v. r := Node (val v) q \<bind> (\<lambda>_. os_reverse_aux (Some r) (next v)))
[PROOF STEP]
apply (subst os_reverse_aux.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case Some r of None \<Rightarrow> return q | Some ra \<Rightarrow> !ra \<bind> (\<lambda>v. ra := Node (val v) q \<bind> (\<lambda>_. os_reverse_aux (Some r) (next v)))) = !r \<bind> (\<lambda>v. r := Node (val v) q \<bind> (\<lambda>_. os_reverse_aux (Some r) (next v)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma os_reverse_aux_rule:
  "<os_list xs p * os_list ys q>
    os_reverse_aux q p
  <os_list ((rev xs) @ ys) >"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_list xs p * os_list ys q> os_reverse_aux q p <os_list (rev xs @ ys)>
[PROOF STEP]
proof (induct xs arbitrary: p q ys)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p q ys. <os_list [] p * os_list ys q> os_reverse_aux q p <os_list (rev [] @ ys)>
 2. \<And>a xs p q ys. (\<And>p q ys. <os_list xs p * os_list ys q> os_reverse_aux q p <os_list (rev xs @ ys)>) \<Longrightarrow> <os_list (a # xs) p * os_list ys q> os_reverse_aux q p <os_list (rev (a # xs) @ ys)>
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>p q ys. <os_list [] p * os_list ys q> os_reverse_aux q p <os_list (rev [] @ ys)>
 2. \<And>a xs p q ys. (\<And>p q ys. <os_list xs p * os_list ys q> os_reverse_aux q p <os_list (rev xs @ ys)>) \<Longrightarrow> <os_list (a # xs) p * os_list ys q> os_reverse_aux q p <os_list (rev (a # xs) @ ys)>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_list [] p * os_list ys q> os_reverse_aux q p <os_list (rev [] @ ys)>
[PROOF STEP]
apply sep_auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
<os_list [] p * os_list ys q> os_reverse_aux q p <os_list (rev [] @ ys)>

goal (1 subgoal):
 1. \<And>a xs p q ys. (\<And>p q ys. <os_list xs p * os_list ys q> os_reverse_aux q p <os_list (rev xs @ ys)>) \<Longrightarrow> <os_list (a # xs) p * os_list ys q> os_reverse_aux q p <os_list (rev (a # xs) @ ys)>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs p q ys. (\<And>p q ys. <os_list xs p * os_list ys q> os_reverse_aux q p <os_list (rev xs @ ys)>) \<Longrightarrow> <os_list (a # xs) p * os_list ys q> os_reverse_aux q p <os_list (rev (a # xs) @ ys)>
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
<os_list xs ?p * os_list ?ys ?q> os_reverse_aux ?q ?p <os_list (rev xs @ ?ys)>

goal (1 subgoal):
 1. \<And>a xs p q ys. (\<And>p q ys. <os_list xs p * os_list ys q> os_reverse_aux q p <os_list (rev xs @ ys)>) \<Longrightarrow> <os_list (a # xs) p * os_list ys q> os_reverse_aux q p <os_list (rev (a # xs) @ ys)>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_list (x # xs) p * os_list ys q> os_reverse_aux q p <os_list (rev (x # xs) @ ys)>
[PROOF STEP]
apply (cases p, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. p = Some a \<Longrightarrow> <\<exists>\<^sub>App n. pp \<mapsto>\<^sub>r Node x n * os_list xs n * os_list ys q * \<up> (a = pp)> !a \<bind> (\<lambda>v. a := Node (val v) q \<bind> (\<lambda>_. os_reverse_aux (Some a) (next v))) <os_list (rev xs @ x # ys)>
[PROOF STEP]
apply (sep_auto heap add: cons_pre_rule[OF _ Cons.hyps])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
<os_list (x # xs) p * os_list ys q> os_reverse_aux q p <os_list (rev (x # xs) @ ys)>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma os_reverse_rule: "<os_list xs p> os_reverse p <os_list (rev xs)>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_list xs p> os_reverse p <os_list (rev xs)>
[PROOF STEP]
unfolding os_reverse_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_list xs p> os_reverse_aux None p <os_list (rev xs)>
[PROOF STEP]
apply (auto simp: os_reverse_aux_rule[where ys="[]", simplified, rule_format])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma os_reverse_impl: "imp_list_reverse os_list os_reverse"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_list_reverse os_list os_reverse
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l p. <os_list l p> os_reverse p <os_list (rev l)>\<^sub>t
[PROOF STEP]
apply (sep_auto heap add: os_reverse_rule)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [simp, sep_dflt_simps]:
  "os_rem x None = return None"
  "os_rem x (Some p) = do {
       n \<leftarrow> !p;
       q \<leftarrow> os_rem x (next n);
       (if (val n = x)
         then return q
         else do {
           p := Node (val n) q;
           return (Some p) }) }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. os_rem x None = return None &&& os_rem x (Some p) = !p \<bind> (\<lambda>n. os_rem x (next n) \<bind> (\<lambda>q. if val n = x then return q else p := Node (val n) q \<bind> (\<lambda>_. return (Some p))))
[PROOF STEP]
apply (subst os_rem.simps, simp)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma os_rem_rule[sep_heap_rules]:
  "<os_list xs b> os_rem x b <\<lambda>r. os_list (removeAll x xs) r * true>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_list xs b> os_rem x b <os_list (removeAll x xs)>\<^sub>t
[PROOF STEP]
proof (induct xs arbitrary: b x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>b x. <os_list [] b> os_rem x b <os_list (removeAll x [])>\<^sub>t
 2. \<And>a xs b x. (\<And>b x. <os_list xs b> os_rem x b <os_list (removeAll x xs)>\<^sub>t) \<Longrightarrow> <os_list (a # xs) b> os_rem x b <os_list (removeAll x (a # xs))>\<^sub>t
[PROOF STEP]
(* Have to generalize over x, as
    sep_auto preprocessor introduces a new variable. Alternative:
    No preprocessing. (See alternative proof below) *)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>b x. <os_list [] b> os_rem x b <os_list (removeAll x [])>\<^sub>t
 2. \<And>a xs b x. (\<And>b x. <os_list xs b> os_rem x b <os_list (removeAll x xs)>\<^sub>t) \<Longrightarrow> <os_list (a # xs) b> os_rem x b <os_list (removeAll x (a # xs))>\<^sub>t
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>b x. <os_list [] b> os_rem x b <os_list (removeAll x [])>\<^sub>t
 2. \<And>a xs b x. (\<And>b x. <os_list xs b> os_rem x b <os_list (removeAll x xs)>\<^sub>t) \<Longrightarrow> <os_list (a # xs) b> os_rem x b <os_list (removeAll x (a # xs))>\<^sub>t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_list [] b> os_rem x b <os_list (removeAll x [])>\<^sub>t
[PROOF STEP]
apply sep_auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
<os_list [] b> os_rem x b <os_list (removeAll x [])>\<^sub>t

goal (1 subgoal):
 1. \<And>a xs b x. (\<And>b x. <os_list xs b> os_rem x b <os_list (removeAll x xs)>\<^sub>t) \<Longrightarrow> <os_list (a # xs) b> os_rem x b <os_list (removeAll x (a # xs))>\<^sub>t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs b x. (\<And>b x. <os_list xs b> os_rem x b <os_list (removeAll x xs)>\<^sub>t) \<Longrightarrow> <os_list (a # xs) b> os_rem x b <os_list (removeAll x (a # xs))>\<^sub>t
[PROOF STEP]
case (Cons y xs)
[PROOF STATE]
proof (state)
this:
<os_list xs ?b> os_rem ?x ?b <os_list (removeAll ?x xs)>\<^sub>t

goal (1 subgoal):
 1. \<And>a xs b x. (\<And>b x. <os_list xs b> os_rem x b <os_list (removeAll x xs)>\<^sub>t) \<Longrightarrow> <os_list (a # xs) b> os_rem x b <os_list (removeAll x (a # xs))>\<^sub>t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_list (y # xs) b> os_rem x b <os_list (removeAll x (y # xs))>\<^sub>t
[PROOF STEP]
by (sep_auto heap add: Cons.hyps)
[PROOF STATE]
proof (state)
this:
<os_list (y # xs) b> os_rem x b <os_list (removeAll x (y # xs))>\<^sub>t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma os_rem_rule_alt_proof:
  "<os_list xs b> os_rem x b <\<lambda>r. os_list (removeAll x xs) r * true>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_list xs b> os_rem x b <os_list (removeAll x xs)>\<^sub>t
[PROOF STEP]
proof (induct xs arbitrary: b)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>b. <os_list [] b> os_rem x b <os_list (removeAll x [])>\<^sub>t
 2. \<And>a xs b. (\<And>b. <os_list xs b> os_rem x b <os_list (removeAll x xs)>\<^sub>t) \<Longrightarrow> <os_list (a # xs) b> os_rem x b <os_list (removeAll x (a # xs))>\<^sub>t
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>b. <os_list [] b> os_rem x b <os_list (removeAll x [])>\<^sub>t
 2. \<And>a xs b. (\<And>b. <os_list xs b> os_rem x b <os_list (removeAll x xs)>\<^sub>t) \<Longrightarrow> <os_list (a # xs) b> os_rem x b <os_list (removeAll x (a # xs))>\<^sub>t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_list [] b> os_rem x b <os_list (removeAll x [])>\<^sub>t
[PROOF STEP]
apply sep_auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
<os_list [] b> os_rem x b <os_list (removeAll x [])>\<^sub>t

goal (1 subgoal):
 1. \<And>a xs b. (\<And>b. <os_list xs b> os_rem x b <os_list (removeAll x xs)>\<^sub>t) \<Longrightarrow> <os_list (a # xs) b> os_rem x b <os_list (removeAll x (a # xs))>\<^sub>t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs b. (\<And>b. <os_list xs b> os_rem x b <os_list (removeAll x xs)>\<^sub>t) \<Longrightarrow> <os_list (a # xs) b> os_rem x b <os_list (removeAll x (a # xs))>\<^sub>t
[PROOF STEP]
case (Cons y xs)
[PROOF STATE]
proof (state)
this:
<os_list xs ?b> os_rem x ?b <os_list (removeAll x xs)>\<^sub>t

goal (1 subgoal):
 1. \<And>a xs b. (\<And>b. <os_list xs b> os_rem x b <os_list (removeAll x xs)>\<^sub>t) \<Longrightarrow> <os_list (a # xs) b> os_rem x b <os_list (removeAll x (a # xs))>\<^sub>t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_list (y # xs) b> os_rem x b <os_list (removeAll x (y # xs))>\<^sub>t
[PROOF STEP]
by (sep_auto (nopre) heap add: Cons.hyps)
[PROOF STATE]
proof (state)
this:
<os_list (y # xs) b> os_rem x b <os_list (removeAll x (y # xs))>\<^sub>t

goal:
No subgoals!
[PROOF STEP]
(* Switching off preprocessor *)
[PROOF STATE]
proof (state)
this:
<os_list (y # xs) b> os_rem x b <os_list (removeAll x (y # xs))>\<^sub>t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma os_iterate_impl:
  "imp_list_iterate os_list os_is_it os_it_init os_it_has_next os_it_next"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_list_iterate os_list os_is_it os_it_init os_it_has_next os_it_next
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>l p. <os_list l p> os_it_init p <os_is_it l p l>\<^sub>t
 2. \<And>l' l p it. l' \<noteq> [] \<Longrightarrow> <os_is_it l p l' it> os_it_next it <\<lambda>r. case r of (a, it') \<Rightarrow> os_is_it l p (tl l') it' * \<up> (a = hd l')>\<^sub>t
 3. \<And>l p l' it. <os_is_it l p l' it> os_it_has_next it <\<lambda>r. os_is_it l p l' it * \<up> (r = (l' \<noteq> []))>\<^sub>t
 4. \<And>l p l' it. os_is_it l p l' it \<Longrightarrow>\<^sub>A os_list l p * true
[PROOF STEP]
unfolding os_it_init_def os_is_it_def[abs_def]
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>l p. <os_list l p> return p <\<lambda>r. \<exists>\<^sub>Al1. \<up> (l = l1 @ l) * lseg l1 p r * os_list l r>\<^sub>t
 2. \<And>l' l p it. l' \<noteq> [] \<Longrightarrow> <\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it> os_it_next it <\<lambda>r. case r of (a, it') \<Rightarrow> (\<exists>\<^sub>Al1. \<up> (l = l1 @ tl l') * lseg l1 p it' * os_list (tl l') it') * \<up> (a = hd l')>\<^sub>t
 3. \<And>l p l' it. <\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it> os_it_has_next it <\<lambda>r. (\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it) * \<up> (r = (l' \<noteq> []))>\<^sub>t
 4. \<And>l p l' it. \<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it \<Longrightarrow>\<^sub>A os_list l p * true
[PROOF STEP]
apply sep_auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>l' l p it. l' \<noteq> [] \<Longrightarrow> <\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it> os_it_next it <\<lambda>r. case r of (a, it') \<Rightarrow> (\<exists>\<^sub>Al1. \<up> (l = l1 @ tl l') * lseg l1 p it' * os_list (tl l') it') * \<up> (a = hd l')>\<^sub>t
 2. \<And>l p l' it. <\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it> os_it_has_next it <\<lambda>r. (\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it) * \<up> (r = (l' \<noteq> []))>\<^sub>t
 3. \<And>l p l' it. \<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it \<Longrightarrow>\<^sub>A os_list l p * true
[PROOF STEP]
apply (case_tac it, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>l' l p it a. \<lbrakk>l' \<noteq> []; it = Some a\<rbrakk> \<Longrightarrow> <\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it> os_it_next it <\<lambda>r. case r of (a, it') \<Rightarrow> (\<exists>\<^sub>Al1. \<up> (l = l1 @ tl l') * lseg l1 p it' * os_list (tl l') it') * \<up> (a = hd l')>\<^sub>t
 2. \<And>l p l' it. <\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it> os_it_has_next it <\<lambda>r. (\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it) * \<up> (r = (l' \<noteq> []))>\<^sub>t
 3. \<And>l p l' it. \<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it \<Longrightarrow>\<^sub>A os_list l p * true
[PROOF STEP]
apply (case_tac l', simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>l' l p it a aa list. \<lbrakk>l' \<noteq> []; it = Some a; l' = aa # list\<rbrakk> \<Longrightarrow> <\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it> os_it_next it <\<lambda>r. case r of (a, it') \<Rightarrow> (\<exists>\<^sub>Al1. \<up> (l = l1 @ tl l') * lseg l1 p it' * os_list (tl l') it') * \<up> (a = hd l')>\<^sub>t
 2. \<And>l p l' it. <\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it> os_it_has_next it <\<lambda>r. (\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it) * \<up> (r = (l' \<noteq> []))>\<^sub>t
 3. \<And>l p l' it. \<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it \<Longrightarrow>\<^sub>A os_list l p * true
[PROOF STEP]
apply sep_auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>p a aa list l1 n. a \<mapsto>\<^sub>r Node aa n * lseg l1 p (Some a) * os_list list n \<Longrightarrow>\<^sub>A lseg (l1 @ [aa]) p n * os_list list n * true
 2. \<And>l p l' it. <\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it> os_it_has_next it <\<lambda>r. (\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it) * \<up> (r = (l' \<noteq> []))>\<^sub>t
 3. \<And>l p l' it. \<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it \<Longrightarrow>\<^sub>A os_list l p * true
[PROOF STEP]
apply (rule ent_frame_fwd[OF lseg_append])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>p a aa list l1 n. a \<mapsto>\<^sub>r Node aa n * lseg l1 p (Some a) * os_list list n \<Longrightarrow>\<^sub>A lseg (?l88 p a aa list l1 n) (?p88 p a aa list l1 n) (Some (?s88 p a aa list l1 n)) * ?s88 p a aa list l1 n \<mapsto>\<^sub>r Node (?x88 p a aa list l1 n) (?q88 p a aa list l1 n) * ?F87 p a aa list l1 n
 2. \<And>p a aa list l1 n. lseg (?l88 p a aa list l1 n @ [?x88 p a aa list l1 n]) (?p88 p a aa list l1 n) (?q88 p a aa list l1 n) * ?F87 p a aa list l1 n \<Longrightarrow>\<^sub>A lseg (l1 @ [aa]) p n * os_list list n * true
 3. \<And>l p l' it. <\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it> os_it_has_next it <\<lambda>r. (\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it) * \<up> (r = (l' \<noteq> []))>\<^sub>t
 4. \<And>l p l' it. \<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it \<Longrightarrow>\<^sub>A os_list l p * true
[PROOF STEP]
apply frame_inference
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>p a aa list l1 n. lseg (l1 @ [aa]) p n * os_list list n \<Longrightarrow>\<^sub>A lseg (l1 @ [aa]) p n * os_list list n * true
 2. \<And>l p l' it. <\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it> os_it_has_next it <\<lambda>r. (\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it) * \<up> (r = (l' \<noteq> []))>\<^sub>t
 3. \<And>l p l' it. \<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it \<Longrightarrow>\<^sub>A os_list l p * true
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>p aa list l1 n. lseg (l1 @ [aa]) p n * os_list list n \<Longrightarrow>\<^sub>A lseg (l1 @ [aa]) p n * os_list list n * true
 2. \<And>l p l' it. <\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it> os_it_has_next it <\<lambda>r. (\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it) * \<up> (r = (l' \<noteq> []))>\<^sub>t
 3. \<And>l p l' it. \<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it \<Longrightarrow>\<^sub>A os_list l p * true
[PROOF STEP]
apply (sep_auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l p l' it. <\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it> os_it_has_next it <\<lambda>r. (\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it) * \<up> (r = (l' \<noteq> []))>\<^sub>t
 2. \<And>l p l' it. \<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it \<Longrightarrow>\<^sub>A os_list l p * true
[PROOF STEP]
unfolding os_it_has_next_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l p l' it. <\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it> return (it \<noteq> None) <\<lambda>r. (\<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it) * \<up> (r = (l' \<noteq> []))>\<^sub>t
 2. \<And>l p l' it. \<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it \<Longrightarrow>\<^sub>A os_list l p * true
[PROOF STEP]
apply (sep_auto elim!: neq_NilE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l p l' it. \<exists>\<^sub>Al1. \<up> (l = l1 @ l') * lseg l1 p it * os_list l' it \<Longrightarrow>\<^sub>A os_list l p * true
[PROOF STEP]
apply solve_entails
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l p l' it l1. l = l1 @ l' \<Longrightarrow> lseg l1 p it * os_list l' it \<Longrightarrow>\<^sub>A os_list (l1 @ l') p * true
[PROOF STEP]
apply (rule ent_frame_fwd[OF lseg_conc])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l p l' it l1. l = l1 @ l' \<Longrightarrow> lseg l1 p it * os_list l' it \<Longrightarrow>\<^sub>A lseg (?l1.165 l p l' it l1) (?p165 l p l' it l1) (?q165 l p l' it l1) * lseg (?l2.165 l p l' it l1) (?q165 l p l' it l1) (?r165 l p l' it l1) * ?F164 l p l' it l1
 2. \<And>l p l' it l1. l = l1 @ l' \<Longrightarrow> lseg (?l1.165 l p l' it l1 @ ?l2.165 l p l' it l1) (?p165 l p l' it l1) (?r165 l p l' it l1) * ?F164 l p l' it l1 \<Longrightarrow>\<^sub>A os_list (l1 @ l') p * true
[PROOF STEP]
apply frame_inference
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l p l' it l1. l = l1 @ l' \<Longrightarrow> os_list (l1 @ l') p * emp \<Longrightarrow>\<^sub>A os_list (l1 @ l') p * true
[PROOF STEP]
apply solve_entails
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma os_sum'_rule[sep_heap_rules]:
  "<os_is_it l p l' it>
    os_sum' it s
  <\<lambda>r. os_list l p * \<up>(r = s + sum_list l')>\<^sub>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_is_it l p l' it> os_sum' it s <\<lambda>r. os_list l p * \<up> (r = s + sum_list l')>\<^sub>t
[PROOF STEP]
proof (induct l' arbitrary: it s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>it s. <os_is_it l p [] it> os_sum' it s <\<lambda>r. os_list l p * \<up> (r = s + sum_list [])>\<^sub>t
 2. \<And>a l' it s. (\<And>it s. <os_is_it l p l' it> os_sum' it s <\<lambda>r. os_list l p * \<up> (r = s + sum_list l')>\<^sub>t) \<Longrightarrow> <os_is_it l p (a # l') it> os_sum' it s <\<lambda>r. os_list l p * \<up> (r = s + sum_list (a # l'))>\<^sub>t
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>it s. <os_is_it l p [] it> os_sum' it s <\<lambda>r. os_list l p * \<up> (r = s + sum_list [])>\<^sub>t
 2. \<And>a l' it s. (\<And>it s. <os_is_it l p l' it> os_sum' it s <\<lambda>r. os_list l p * \<up> (r = s + sum_list l')>\<^sub>t) \<Longrightarrow> <os_is_it l p (a # l') it> os_sum' it s <\<lambda>r. os_list l p * \<up> (r = s + sum_list (a # l'))>\<^sub>t
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_is_it l p [] it> os_sum' it s <\<lambda>r. os_list l p * \<up> (r = s + sum_list [])>\<^sub>t
[PROOF STEP]
apply (subst os_sum'.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_is_it l p [] it> os_it_has_next it \<bind> (\<lambda>b. if b then os_it_next it \<bind> (\<lambda>(x, it'). os_sum' it' (s + x)) else return s) <\<lambda>r. os_list l p * \<up> (r = s + sum_list [])>\<^sub>t
[PROOF STEP]
apply (sep_auto intro: os.quit_iteration ent_true_drop(1))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
<os_is_it l p [] it> os_sum' it s <\<lambda>r. os_list l p * \<up> (r = s + sum_list [])>\<^sub>t

goal (1 subgoal):
 1. \<And>a l' it s. (\<And>it s. <os_is_it l p l' it> os_sum' it s <\<lambda>r. os_list l p * \<up> (r = s + sum_list l')>\<^sub>t) \<Longrightarrow> <os_is_it l p (a # l') it> os_sum' it s <\<lambda>r. os_list l p * \<up> (r = s + sum_list (a # l'))>\<^sub>t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l' it s. (\<And>it s. <os_is_it l p l' it> os_sum' it s <\<lambda>r. os_list l p * \<up> (r = s + sum_list l')>\<^sub>t) \<Longrightarrow> <os_is_it l p (a # l') it> os_sum' it s <\<lambda>r. os_list l p * \<up> (r = s + sum_list (a # l'))>\<^sub>t
[PROOF STEP]
case (Cons x l')
[PROOF STATE]
proof (state)
this:
<os_is_it l p l' ?it> os_sum' ?it ?s <\<lambda>r. os_list l p * \<up> (r = ?s + sum_list l')>\<^sub>t

goal (1 subgoal):
 1. \<And>a l' it s. (\<And>it s. <os_is_it l p l' it> os_sum' it s <\<lambda>r. os_list l p * \<up> (r = s + sum_list l')>\<^sub>t) \<Longrightarrow> <os_is_it l p (a # l') it> os_sum' it s <\<lambda>r. os_list l p * \<up> (r = s + sum_list (a # l'))>\<^sub>t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_is_it l p (x # l') it> os_sum' it s <\<lambda>r. os_list l p * \<up> (r = s + sum_list (x # l'))>\<^sub>t
[PROOF STEP]
apply (subst os_sum'.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_is_it l p (x # l') it> os_it_has_next it \<bind> (\<lambda>b. if b then os_it_next it \<bind> (\<lambda>(x, it'). os_sum' it' (s + x)) else return s) <\<lambda>r. os_list l p * \<up> (r = s + sum_list (x # l'))>\<^sub>t
[PROOF STEP]
apply (sep_auto heap: Cons.hyps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
<os_is_it l p (x # l') it> os_sum' it s <\<lambda>r. os_list l p * \<up> (r = s + sum_list (x # l'))>\<^sub>t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma os_sum_rule[sep_heap_rules]:
  "<os_list l p> os_sum p <\<lambda>r. os_list l p * \<up>(r=sum_list l)>\<^sub>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_list l p> os_sum p <\<lambda>r. os_list l p * \<up> (r = sum_list l)>\<^sub>t
[PROOF STEP]
unfolding os_sum_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <os_list l p> os_it_init p \<bind> (\<lambda>it. os_sum' it 0) <\<lambda>r. os_list l p * \<up> (r = sum_list l)>\<^sub>t
[PROOF STEP]
by sep_auto


[STATEMENT]
lemma "attack\<langle>ln 0\<rangle> \<in> set (fst LOSS_KEY_ATT_fixpoint)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. attack\<langle>ln 0\<rangle> \<in> set (fst LOSS_KEY_ATT_fixpoint)
[PROOF STEP]
by code_simp


[STATEMENT]
lemma card_signed [simp]: "CARD (('a::len0) signed) = CARD('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('a signed) = CARD('a)
[PROOF STEP]
unfolding type_definition.card [OF type_definition_signed]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('a) = CARD('a)
[PROOF STEP]
by simp


[STATEMENT]
lemma scast_scast_id [simp]:
  "scast (scast x :: ('a::len) signed word) = (x :: 'a word)"
  "scast (scast y :: ('a::len) word) = (y :: 'a signed word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scast (scast x) = x &&& scast (scast y) = y
[PROOF STEP]
by (auto simp: is_up scast_up_scast_id)


[STATEMENT]
lemma ucast_scast_id [simp]:
  "ucast (scast (x :: 'a::len signed word) :: 'a word) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ucast (scast x) = x
[PROOF STEP]
by transfer (simp add: take_bit_signed_take_bit)


[STATEMENT]
lemma scast_of_nat [simp]:
  "scast (of_nat x :: 'a::len signed word) = (of_nat x :: 'a word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scast (word_of_nat x) = word_of_nat x
[PROOF STEP]
by transfer (simp add: take_bit_signed_take_bit)


[STATEMENT]
lemma scast_ucast_id [simp]:
  "scast (ucast (x :: 'a::len word) :: 'a signed word) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scast (ucast x) = x
[PROOF STEP]
by transfer (simp add: take_bit_signed_take_bit)


[STATEMENT]
lemma scast_eq_scast_id [simp]:
  "((scast (a :: 'a::len signed word) :: 'a word) = scast b) = (a = b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (scast a = scast b) = (a = b)
[PROOF STEP]
by (metis ucast_scast_id)


[STATEMENT]
lemma ucast_eq_ucast_id [simp]:
  "((ucast (a :: 'a::len word) :: 'a signed word) = ucast b) = (a = b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ucast a = ucast b) = (a = b)
[PROOF STEP]
by (metis scast_ucast_id)


[STATEMENT]
lemma scast_ucast_norm [simp]:
  "(ucast (a :: 'a::len word) = (b :: 'a signed word)) = (a = scast b)"
  "((b :: 'a signed word) = ucast (a :: 'a::len word)) = (a = scast b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ucast a = b) = (a = scast b) &&& (b = ucast a) = (a = scast b)
[PROOF STEP]
by (metis scast_ucast_id ucast_scast_id)+


[STATEMENT]
lemma scast_2_power [simp]: "scast ((2 :: 'a::len signed word) ^ x) = ((2 :: 'a word) ^ x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scast (2 ^ x) = 2 ^ x
[PROOF STEP]
by (rule bit_word_eqI) (auto simp add: bit_simps)


[STATEMENT]
lemma ucast_nat_def':
  "of_nat (unat x) = (ucast :: 'a :: len word \<Rightarrow> ('b :: len) signed word) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_of_nat (unat x) = ucast x
[PROOF STEP]
by (fact of_nat_unat)


[STATEMENT]
lemma zero_sle_ucast_up:
  "\<not> is_down (ucast :: 'a word \<Rightarrow> 'b signed word) \<Longrightarrow>
          (0 <=s ((ucast (b::('a::len) word)) :: ('b::len) signed word))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_down ucast \<Longrightarrow> 0 \<le>s ucast b
[PROOF STEP]
by transfer (simp add: bit_simps)


[STATEMENT]
lemma word_le_ucast_sless:
  "\<lbrakk> x \<le> y; y \<noteq> -1; LENGTH('a) < LENGTH('b) \<rbrakk> \<Longrightarrow>
    (ucast x :: ('b :: len) signed word) <s ucast (y + 1)"
  for x y :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y \<noteq> - 1; LENGTH('a) < LENGTH('b)\<rbrakk> \<Longrightarrow> ucast x <s ucast (y + 1)
[PROOF STEP]
apply (cases \<open>LENGTH('b)\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<le> y; y \<noteq> - 1; LENGTH('a) < LENGTH('b); LENGTH('b) = 0\<rbrakk> \<Longrightarrow> ucast x <s ucast (y + 1)
 2. \<And>nat. \<lbrakk>x \<le> y; y \<noteq> - 1; LENGTH('a) < LENGTH('b); LENGTH('b) = Suc nat\<rbrakk> \<Longrightarrow> ucast x <s ucast (y + 1)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>x \<le> y; y \<noteq> - 1; LENGTH('a) < Suc nat; LENGTH('b) = Suc nat\<rbrakk> \<Longrightarrow> ucast x <s ucast (y + 1)
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat x y. \<lbrakk>take_bit LENGTH('a) x \<le> take_bit LENGTH('a) y; take_bit LENGTH('a) y \<noteq> take_bit LENGTH('a) (- 1); LENGTH('a) < Suc nat; LENGTH('b) = Suc nat\<rbrakk> \<Longrightarrow> signed_take_bit (LENGTH('b signed) - Suc 0) (take_bit LENGTH('a) x) < signed_take_bit (LENGTH('b signed) - Suc 0) (take_bit LENGTH('a) (y + 1))
[PROOF STEP]
apply (simp add: signed_take_bit_take_bit)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat x y. \<lbrakk>take_bit LENGTH('a) x \<le> take_bit LENGTH('a) y; take_bit LENGTH('a) y \<noteq> mask LENGTH('a); LENGTH('a) < Suc nat; LENGTH('b) = Suc nat\<rbrakk> \<Longrightarrow> take_bit LENGTH('a) x < take_bit LENGTH('a) (y + 1)
[PROOF STEP]
apply (metis add.commute mask_eq_exp_minus_1 take_bit_incr_eq zle_add1_eq_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma zero_sle_ucast:
  "(0 <=s ((ucast (b::('a::len) word)) :: ('a::len) signed word))
                = (uint b < 2 ^ (LENGTH('a) - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 \<le>s ucast b) = (uint b < 2 ^ (LENGTH('a) - 1))
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. (signed_take_bit (LENGTH('a signed) - Suc 0) 0 \<le> signed_take_bit (LENGTH('a signed) - Suc 0) (take_bit LENGTH('a) b)) = (take_bit LENGTH('a) b < 2 ^ (LENGTH('a) - 1))
[PROOF STEP]
apply (cases \<open>LENGTH('a)\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b. LENGTH('a) = 0 \<Longrightarrow> (signed_take_bit (LENGTH('a signed) - Suc 0) 0 \<le> signed_take_bit (LENGTH('a signed) - Suc 0) (take_bit LENGTH('a) b)) = (take_bit LENGTH('a) b < 2 ^ (LENGTH('a) - 1))
 2. \<And>b nat. LENGTH('a) = Suc nat \<Longrightarrow> (signed_take_bit (LENGTH('a signed) - Suc 0) 0 \<le> signed_take_bit (LENGTH('a signed) - Suc 0) (take_bit LENGTH('a) b)) = (take_bit LENGTH('a) b < 2 ^ (LENGTH('a) - 1))
[PROOF STEP]
apply (simp_all add: take_bit_Suc_from_most bit_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b nat. LENGTH('a) = Suc nat \<Longrightarrow> bit b nat \<longrightarrow> bit (2 ^ nat + take_bit nat b) nat
[PROOF STEP]
apply (simp_all add: bit_simps disjunctive_add)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nth_w2p_scast:
  "(bit (scast ((2::'a::len signed word) ^ n) :: 'a word) m)
         \<longleftrightarrow> (bit (((2::'a::len  word) ^ n) :: 'a word) m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (scast (2 ^ n)) m = bit (2 ^ n) m
[PROOF STEP]
by (simp add: bit_simps)


[STATEMENT]
lemma scast_nop1 [simp]:
  "((scast ((of_int x)::('a::len) word))::'a signed word) = of_int x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scast (word_of_int x) = word_of_int x
[PROOF STEP]
by transfer (simp add: take_bit_signed_take_bit)


[STATEMENT]
lemma scast_nop2 [simp]:
  "((scast ((of_int x)::('a::len) signed word))::'a word) = of_int x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scast (word_of_int x) = word_of_int x
[PROOF STEP]
by transfer (simp add: take_bit_signed_take_bit)


[STATEMENT]
lemma nodeToList_empty: "nodeToList nd \<noteq> Nil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodeToList nd \<noteq> []
[PROOF STEP]
by (induct nd) auto


[STATEMENT]
lemma digitToList_empty: "digitToList d \<noteq> Nil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digitToList d \<noteq> []
[PROOF STEP]
by (cases d, auto simp add: nodeToList_empty)


[STATEMENT]
lemma gmn_correct:
  assumes "is_measured_node nd"
  shows "gmn nd = sum_list (map snd (nodeToList nd))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gmn nd = sum_list (map snd (nodeToList nd))
[PROOF STEP]
by (insert assms, induct nd) (auto simp add: add.assoc)


[STATEMENT]
lemma gmd_correct:
  assumes "is_measured_digit d"
  shows "gmd d = sum_list (map snd (digitToList d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gmd d = sum_list (map snd (digitToList d))
[PROOF STEP]
by (insert assms, cases d, auto simp add: gmn_correct add.assoc)


[STATEMENT]
lemma gmft_correct: "is_measured_ftree t
  \<Longrightarrow> (gmft t) = sum_list (map snd (toList t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_measured_ftree t \<Longrightarrow> gmft t = sum_list (map snd (toList t))
[PROOF STEP]
by (induct t, auto simp add: ft_invar_def gmd_correct gmn_correct add.assoc)


[STATEMENT]
lemma gmft_correct2: "ft_invar t \<Longrightarrow> (gmft t) = sum_list (map snd (toList t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ft_invar t \<Longrightarrow> gmft t = sum_list (map snd (toList t))
[PROOF STEP]
by (simp only: ft_invar_def gmft_correct)


[STATEMENT]
lemma Empty_correct[simp]:
  "toList Empty = []"
  "ft_invar Empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList Empty = [] &&& ft_invar Empty
[PROOF STEP]
by (simp_all add: ft_invar_def)


[STATEMENT]
lemma toList_empty: "toList t = [] \<longleftrightarrow> t = Empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (toList t = []) = (t = Empty)
[PROOF STEP]
by (induct t, auto simp add: nodeToList_empty digitToList_empty)


[STATEMENT]
lemma annot_correct:
  "ft_invar t \<Longrightarrow> annot t = sum_list (map snd (toList t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ft_invar t \<Longrightarrow> annot t = sum_list (map snd (toList t))
[PROOF STEP]
using gmft_correct
[PROOF STATE]
proof (prove)
using this:
is_measured_ftree ?t \<Longrightarrow> gmft ?t = sum_list (map snd (toList ?t))

goal (1 subgoal):
 1. ft_invar t \<Longrightarrow> annot t = sum_list (map snd (toList t))
[PROOF STEP]
unfolding annot_def
[PROOF STATE]
proof (prove)
using this:
is_measured_ftree ?t \<Longrightarrow> gmft ?t = sum_list (map snd (toList ?t))

goal (1 subgoal):
 1. ft_invar t \<Longrightarrow> gmft t = sum_list (map snd (toList t))
[PROOF STEP]
by (simp add: gmft_correct2)


[STATEMENT]
lemma nlcons_invlevel: "\<lbrakk>is_leveln_ftree n t; is_leveln_node n nd\<rbrakk>
  \<Longrightarrow> is_leveln_ftree n (nlcons nd t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_leveln_ftree n t; is_leveln_node n nd\<rbrakk> \<Longrightarrow> is_leveln_ftree n (nlcons nd t)
[PROOF STEP]
by (induct t arbitrary: n nd rule: nlcons.induct)
(auto simp add: deep_def node3_def)


[STATEMENT]
lemma nlcons_invmeas: "\<lbrakk>is_measured_ftree t; is_measured_node nd\<rbrakk>
  \<Longrightarrow> is_measured_ftree (nlcons nd t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_measured_ftree t; is_measured_node nd\<rbrakk> \<Longrightarrow> is_measured_ftree (nlcons nd t)
[PROOF STEP]
by (induct t arbitrary: nd rule: nlcons.induct)
     (auto simp add: deep_def node3_def)


[STATEMENT]
lemma nlcons_list: "toList (nlcons a t) = (nodeToList a) @ (toList t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList (nlcons a t) = nodeToList a @ toList t
[PROOF STEP]
apply (induct t arbitrary: a rule: nlcons.induct)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a aa. toList (nlcons aa Empty) = nodeToList aa @ toList Empty
 2. \<And>a b aa. toList (nlcons aa (Single b)) = nodeToList aa @ toList (Single b)
 3. \<And>a uu_ b m sf aa. toList (nlcons aa (Deep uu_ (One b) m sf)) = nodeToList aa @ toList (Deep uu_ (One b) m sf)
 4. \<And>a uv_ b c m sf aa. toList (nlcons aa (Deep uv_ (Two b c) m sf)) = nodeToList aa @ toList (Deep uv_ (Two b c) m sf)
 5. \<And>a uw_ b c d m sf aa. toList (nlcons aa (Deep uw_ (Three b c d) m sf)) = nodeToList aa @ toList (Deep uw_ (Three b c d) m sf)
 6. \<And>a ux_ b c d e m sf aa. (\<And>a. toList (nlcons a m) = nodeToList a @ toList m) \<Longrightarrow> toList (nlcons aa (Deep ux_ (Four b c d e) m sf)) = nodeToList aa @ toList (Deep ux_ (Four b c d e) m sf)
[PROOF STEP]
apply (auto simp add: deep_def toList_def node3_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nrcons_invlevel: "\<lbrakk>is_leveln_ftree n t; is_leveln_node n nd\<rbrakk>
  \<Longrightarrow> is_leveln_ftree n (nrcons t nd)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_leveln_ftree n t; is_leveln_node n nd\<rbrakk> \<Longrightarrow> is_leveln_ftree n (nrcons t nd)
[PROOF STEP]
apply (induct t nd arbitrary: nd n rule:nrcons.induct)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a nd n. \<lbrakk>is_leveln_ftree n Empty; is_leveln_node n nd\<rbrakk> \<Longrightarrow> is_leveln_ftree n (nrcons Empty nd)
 2. \<And>b a nd n. \<lbrakk>is_leveln_ftree n (Single b); is_leveln_node n nd\<rbrakk> \<Longrightarrow> is_leveln_ftree n (nrcons (Single b) nd)
 3. \<And>uu_ pr m b a nd n. \<lbrakk>is_leveln_ftree n (Deep uu_ pr m (One b)); is_leveln_node n nd\<rbrakk> \<Longrightarrow> is_leveln_ftree n (nrcons (Deep uu_ pr m (One b)) nd)
 4. \<And>uv_ pr m b c a nd n. \<lbrakk>is_leveln_ftree n (Deep uv_ pr m (Two b c)); is_leveln_node n nd\<rbrakk> \<Longrightarrow> is_leveln_ftree n (nrcons (Deep uv_ pr m (Two b c)) nd)
 5. \<And>uw_ pr m b c d a nd n. \<lbrakk>is_leveln_ftree n (Deep uw_ pr m (Three b c d)); is_leveln_node n nd\<rbrakk> \<Longrightarrow> is_leveln_ftree n (nrcons (Deep uw_ pr m (Three b c d)) nd)
 6. \<And>ux_ pr m b c d e a nd n. \<lbrakk>\<And>nd n. \<lbrakk>is_leveln_ftree n m; is_leveln_node n nd\<rbrakk> \<Longrightarrow> is_leveln_ftree n (nrcons m nd); is_leveln_ftree n (Deep ux_ pr m (Four b c d e)); is_leveln_node n nd\<rbrakk> \<Longrightarrow> is_leveln_ftree n (nrcons (Deep ux_ pr m (Four b c d e)) nd)
[PROOF STEP]
apply(auto simp add: deep_def node3_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nrcons_invmeas: "\<lbrakk>is_measured_ftree t; is_measured_node nd\<rbrakk>
  \<Longrightarrow> is_measured_ftree (nrcons t nd)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_measured_ftree t; is_measured_node nd\<rbrakk> \<Longrightarrow> is_measured_ftree (nrcons t nd)
[PROOF STEP]
apply (induct t nd arbitrary: nd rule:nrcons.induct)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a nd. \<lbrakk>is_measured_ftree Empty; is_measured_node nd\<rbrakk> \<Longrightarrow> is_measured_ftree (nrcons Empty nd)
 2. \<And>b a nd. \<lbrakk>is_measured_ftree (Single b); is_measured_node nd\<rbrakk> \<Longrightarrow> is_measured_ftree (nrcons (Single b) nd)
 3. \<And>uu_ pr m b a nd. \<lbrakk>is_measured_ftree (Deep uu_ pr m (One b)); is_measured_node nd\<rbrakk> \<Longrightarrow> is_measured_ftree (nrcons (Deep uu_ pr m (One b)) nd)
 4. \<And>uv_ pr m b c a nd. \<lbrakk>is_measured_ftree (Deep uv_ pr m (Two b c)); is_measured_node nd\<rbrakk> \<Longrightarrow> is_measured_ftree (nrcons (Deep uv_ pr m (Two b c)) nd)
 5. \<And>uw_ pr m b c d a nd. \<lbrakk>is_measured_ftree (Deep uw_ pr m (Three b c d)); is_measured_node nd\<rbrakk> \<Longrightarrow> is_measured_ftree (nrcons (Deep uw_ pr m (Three b c d)) nd)
 6. \<And>ux_ pr m b c d e a nd. \<lbrakk>\<And>nd. \<lbrakk>is_measured_ftree m; is_measured_node nd\<rbrakk> \<Longrightarrow> is_measured_ftree (nrcons m nd); is_measured_ftree (Deep ux_ pr m (Four b c d e)); is_measured_node nd\<rbrakk> \<Longrightarrow> is_measured_ftree (nrcons (Deep ux_ pr m (Four b c d e)) nd)
[PROOF STEP]
apply(auto simp add: deep_def node3_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nrcons_list: "toList (nrcons t a) = (toList t) @ (nodeToList a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList (nrcons t a) = toList t @ nodeToList a
[PROOF STEP]
apply (induct t a arbitrary: a rule: nrcons.induct)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a aa. toList (nrcons Empty aa) = toList Empty @ nodeToList aa
 2. \<And>b a aa. toList (nrcons (Single b) aa) = toList (Single b) @ nodeToList aa
 3. \<And>uu_ pr m b a aa. toList (nrcons (Deep uu_ pr m (One b)) aa) = toList (Deep uu_ pr m (One b)) @ nodeToList aa
 4. \<And>uv_ pr m b c a aa. toList (nrcons (Deep uv_ pr m (Two b c)) aa) = toList (Deep uv_ pr m (Two b c)) @ nodeToList aa
 5. \<And>uw_ pr m b c d a aa. toList (nrcons (Deep uw_ pr m (Three b c d)) aa) = toList (Deep uw_ pr m (Three b c d)) @ nodeToList aa
 6. \<And>ux_ pr m b c d e a aa. (\<And>a. toList (nrcons m a) = toList m @ nodeToList a) \<Longrightarrow> toList (nrcons (Deep ux_ pr m (Four b c d e)) aa) = toList (Deep ux_ pr m (Four b c d e)) @ nodeToList aa
[PROOF STEP]
apply (auto simp add: deep_def toList_def node3_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma lcons_correct:
  assumes "ft_invar t"
  shows "ft_invar (a \<lhd> t)" and "toList (a \<lhd> t) = a # (toList t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ft_invar (a \<lhd> t) &&& toList (a \<lhd> t) = a # toList t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ft_invar t

goal (1 subgoal):
 1. ft_invar (a \<lhd> t) &&& toList (a \<lhd> t) = a # toList 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 (a \<lhd> t) \<and> is_measured_ftree (a \<lhd> t) &&& toList (a \<lhd> t) = a # toList t
[PROOF STEP]
by (simp_all add: lcons_def nlcons_list nlcons_invlevel nlcons_invmeas)


[STATEMENT]
lemma lcons_inv:"ft_invar t \<Longrightarrow> ft_invar (a \<lhd> t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ft_invar t \<Longrightarrow> ft_invar (a \<lhd> t)
[PROOF STEP]
by (rule lcons_correct)


[STATEMENT]
lemma lcons_list[simp]: "toList (a \<lhd> t) = a # (toList t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList (a \<lhd> t) = a # toList t
[PROOF STEP]
by (simp add: lcons_def nlcons_list)


[STATEMENT]
lemma rcons_correct:
  assumes "ft_invar t"
  shows "ft_invar (t \<rhd> a)" and "toList (t \<rhd> a) = (toList t) @ [a]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ft_invar (t \<rhd> a) &&& toList (t \<rhd> a) = toList t @ [a]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ft_invar t

goal (1 subgoal):
 1. ft_invar (t \<rhd> a) &&& toList (t \<rhd> a) = toList t @ [a]
[PROOF STEP]
by (auto simp add: nrcons_inv ft_invar_def rcons_def nrcons_list)


[STATEMENT]
lemma rcons_inv:"ft_invar t \<Longrightarrow> ft_invar (t \<rhd> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ft_invar t \<Longrightarrow> ft_invar (t \<rhd> a)
[PROOF STEP]
by (rule rcons_correct)


[STATEMENT]
lemma rcons_list[simp]: "toList (t \<rhd> a) = (toList t) @ [a]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList (t \<rhd> a) = toList t @ [a]
[PROOF STEP]
by(auto simp add: nrcons_list rcons_def)


[STATEMENT]
lemma toTree_correct[simp]:
  "ft_invar (toTree l)"
  "toList (toTree l) = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ft_invar (toTree l) &&& toList (toTree l) = l
[PROOF STEP]
apply (induct l)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. ft_invar (toTree [])
 2. toList (toTree []) = []
 3. \<And>a l. \<lbrakk>ft_invar (toTree l); toList (toTree l) = l\<rbrakk> \<Longrightarrow> ft_invar (toTree (a # l))
 4. \<And>a l. \<lbrakk>ft_invar (toTree l); toList (toTree l) = l\<rbrakk> \<Longrightarrow> toList (toTree (a # l)) = a # l
[PROOF STEP]
apply (simp add: ft_invar_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. toList (toTree []) = []
 2. \<And>a l. \<lbrakk>ft_invar (toTree l); toList (toTree l) = l\<rbrakk> \<Longrightarrow> ft_invar (toTree (a # l))
 3. \<And>a l. \<lbrakk>ft_invar (toTree l); toList (toTree l) = l\<rbrakk> \<Longrightarrow> toList (toTree (a # l)) = a # l
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a l. \<lbrakk>ft_invar (toTree l); toList (toTree l) = l\<rbrakk> \<Longrightarrow> ft_invar (toTree (a # l))
 2. \<And>a l. \<lbrakk>ft_invar (toTree l); toList (toTree l) = l\<rbrakk> \<Longrightarrow> toList (toTree (a # l)) = a # l
[PROOF STEP]
apply (simp add: toTree_def lcons_list lcons_inv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>ft_invar (toTree l); toList (toTree l) = l\<rbrakk> \<Longrightarrow> toList (toTree (a # l)) = a # l
[PROOF STEP]
apply (simp add: toTree_def lcons_list lcons_inv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma viewnres_cases:
  fixes r :: "('e,'a) ViewnRes"
  obtains (Nil) "r=None" |
          (Cons) a t where "r=Some (a,t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r = None \<Longrightarrow> thesis; \<And>a t. r = Some (a, t) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (cases r) auto


[STATEMENT]
lemma viewnres_split:
  "P (case_option f1 (case_prod f2) x) =
  ((x = None \<longrightarrow> P f1) \<and> (\<forall>a b. x = Some (a,b) \<longrightarrow> P (f2 a b)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (case x of None \<Rightarrow> f1 | Some (xa, xb) \<Rightarrow> f2 xa xb) = ((x = None \<longrightarrow> P f1) \<and> (\<forall>a b. x = Some (a, b) \<longrightarrow> P (f2 a b)))
[PROOF STEP]
by (auto split: option.split prod.split)


[STATEMENT]
lemma
  digitToTree_inv: "is_leveln_digit n d \<Longrightarrow> is_leveln_ftree n (digitToTree d)"
  "is_measured_digit d \<Longrightarrow> is_measured_ftree (digitToTree d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_leveln_digit n d \<Longrightarrow> is_leveln_ftree n (digitToTree d)) &&& (is_measured_digit d \<Longrightarrow> is_measured_ftree (digitToTree d))
[PROOF STEP]
apply (cases d,auto simp add: deep_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_measured_digit d \<Longrightarrow> is_measured_ftree (digitToTree d)
[PROOF STEP]
apply (cases d,auto simp add: deep_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma digitToTree_list: "toList (digitToTree d) = digitToList d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList (digitToTree d) = digitToList d
[PROOF STEP]
by (cases d) (auto simp add: deep_def)


[STATEMENT]
lemma nodeToDigit_inv:
  "is_leveln_node (Suc n) nd \<Longrightarrow> is_leveln_digit n (nodeToDigit nd) "
  "is_measured_node nd \<Longrightarrow> is_measured_digit (nodeToDigit nd)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_leveln_node (Suc n) nd \<Longrightarrow> is_leveln_digit n (nodeToDigit nd)) &&& (is_measured_node nd \<Longrightarrow> is_measured_digit (nodeToDigit nd))
[PROOF STEP]
by (cases nd, auto) (cases nd, auto)


[STATEMENT]
lemma nodeToDigit_list: "digitToList (nodeToDigit nd) = nodeToList nd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digitToList (nodeToDigit nd) = nodeToList nd
[PROOF STEP]
by (cases nd,auto)


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

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

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

goal (2 subgoals):
 1. \<And>x2. t = Single x2 \<Longrightarrow> (t \<noteq> Empty) = (viewLn t \<noteq> None)
 2. \<And>x31 x32 x33 x34. t = Deep x31 x32 x33 x34 \<Longrightarrow> (t \<noteq> Empty) = (viewLn t \<noteq> None)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x2. t = Single x2 \<Longrightarrow> (t \<noteq> Empty) = (viewLn t \<noteq> None)
 2. \<And>x31 x32 x33 x34. t = Deep x31 x32 x33 x34 \<Longrightarrow> (t \<noteq> Empty) = (viewLn 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) = (viewLn t \<noteq> None)
 2. \<And>x31 x32 x33 x34. t = Deep x31 x32 x33 x34 \<Longrightarrow> (t \<noteq> Empty) = (viewLn t \<noteq> None)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
t = Single Node

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma viewLn_inv: "\<lbrakk>
  is_measured_ftree t; is_leveln_ftree n t; viewLn 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; viewLn 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: viewLn.induct)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>n nd s. \<lbrakk>is_measured_ftree Empty; is_leveln_ftree n Empty; viewLn 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); viewLn (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_ a b m sf n nd s. \<lbrakk>is_measured_ftree (Deep uu_ (Two a b) m sf); is_leveln_ftree n (Deep uu_ (Two a b) m sf); viewLn (Deep uu_ (Two a b) m sf) = 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_ a b c m sf n nd s. \<lbrakk>is_measured_ftree (Deep uv_ (Three a b c) m sf); is_leveln_ftree n (Deep uv_ (Three a b c) m sf); viewLn (Deep uv_ (Three a b c) m sf) = 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_ a b c d m sf n nd s. \<lbrakk>is_measured_ftree (Deep uw_ (Four a b c d) m sf); is_leveln_ftree n (Deep uw_ (Four a b c d) m sf); viewLn (Deep uw_ (Four a b c d) m sf) = 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_ a m sf n nd s. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewLn 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_ (One a) m sf); is_leveln_ftree n (Deep ux_ (One a) m sf); viewLn (Deep ux_ (One a) m sf) = 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: viewLn_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); viewLn (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_ a b m sf n nd s. \<lbrakk>is_measured_ftree (Deep uu_ (Two a b) m sf); is_leveln_ftree n (Deep uu_ (Two a b) m sf); viewLn (Deep uu_ (Two a b) m sf) = 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_ a b c m sf n nd s. \<lbrakk>is_measured_ftree (Deep uv_ (Three a b c) m sf); is_leveln_ftree n (Deep uv_ (Three a b c) m sf); viewLn (Deep uv_ (Three a b c) m sf) = 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_ a b c d m sf n nd s. \<lbrakk>is_measured_ftree (Deep uw_ (Four a b c d) m sf); is_leveln_ftree n (Deep uw_ (Four a b c d) m sf); viewLn (Deep uw_ (Four a b c d) m sf) = 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_ a m sf n nd s. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewLn 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_ (One a) m sf); is_leveln_ftree n (Deep ux_ (One a) m sf); viewLn (Deep ux_ (One a) m sf) = 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_ a b m sf n nd s. \<lbrakk>is_measured_ftree (Deep uu_ (Two a b) m sf); is_leveln_ftree n (Deep uu_ (Two a b) m sf); viewLn (Deep uu_ (Two a b) m sf) = 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_ a b c m sf n nd s. \<lbrakk>is_measured_ftree (Deep uv_ (Three a b c) m sf); is_leveln_ftree n (Deep uv_ (Three a b c) m sf); viewLn (Deep uv_ (Three a b c) m sf) = 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_ a b c d m sf n nd s. \<lbrakk>is_measured_ftree (Deep uw_ (Four a b c d) m sf); is_leveln_ftree n (Deep uw_ (Four a b c d) m sf); viewLn (Deep uw_ (Four a b c d) m sf) = 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_ a m sf n nd s. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewLn 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_ (One a) m sf); is_leveln_ftree n (Deep ux_ (One a) m sf); viewLn (Deep ux_ (One a) m sf) = 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_ a b c m sf n nd s. \<lbrakk>is_measured_ftree (Deep uv_ (Three a b c) m sf); is_leveln_ftree n (Deep uv_ (Three a b c) m sf); viewLn (Deep uv_ (Three a b c) m sf) = 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_ a b c d m sf n nd s. \<lbrakk>is_measured_ftree (Deep uw_ (Four a b c d) m sf); is_leveln_ftree n (Deep uw_ (Four a b c d) m sf); viewLn (Deep uw_ (Four a b c d) m sf) = 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_ a m sf n nd s. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewLn 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_ (One a) m sf); is_leveln_ftree n (Deep ux_ (One a) m sf); viewLn (Deep ux_ (One a) m sf) = 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_ a b c d m sf n nd s. \<lbrakk>is_measured_ftree (Deep uw_ (Four a b c d) m sf); is_leveln_ftree n (Deep uw_ (Four a b c d) m sf); viewLn (Deep uw_ (Four a b c d) m sf) = 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_ a m sf n nd s. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewLn 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_ (One a) m sf); is_leveln_ftree n (Deep ux_ (One a) m sf); viewLn (Deep ux_ (One a) m sf) = 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_ a m sf n nd s. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewLn 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_ (One a) m sf); is_leveln_ftree n (Deep ux_ (One a) m sf); viewLn (Deep ux_ (One a) m sf) = 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_ a m sf n nd s. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewLn 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_ (One a) m sf); is_leveln_ftree n (Deep ux_ (One a) m sf); viewLn (Deep ux_ (One a) m sf) = 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 sf n nd s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ux_ a m sf n nd s. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewLn 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_ (One a) m sf); is_leveln_ftree n (Deep ux_ (One a) m sf); viewLn (Deep ux_ (One a) m sf) = 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; viewLn 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 (One a) m sf) "
         "is_leveln_ftree n (Deep ux (One a) m sf)"
         "viewLn (Deep ux (One a) m sf) = Some (nd, s)"
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_measured_ftree m; is_leveln_ftree ?n m; viewLn 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 (One a) m sf)
is_leveln_ftree n (Deep ux (One a) m sf)
viewLn (Deep ux (One a) m sf) = Some (nd, s)

goal (1 subgoal):
 1. \<And>ux_ a m sf n nd s. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewLn 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_ (One a) m sf); is_leveln_ftree n (Deep ux_ (One a) m sf); viewLn (Deep ux_ (One a) m sf) = 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; viewLn 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 (One a) m sf)
is_leveln_ftree n (Deep ux (One a) m sf)
viewLn (Deep ux (One a) m sf) = 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 "viewLn 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; viewLn 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 (One a) m sf); is_leveln_ftree n (Deep ux (One a) m sf); viewLn (Deep ux (One a) m sf) = Some (nd, s); viewLn 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; viewLn 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 (One a) m sf); is_leveln_ftree n (Deep ux (One a) m sf); viewLn (Deep ux (One a) m sf) = Some (nd, s); viewLn 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:
viewLn m = None

goal (2 subgoals):
 1. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewLn 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 (One a) m sf); is_leveln_ftree n (Deep ux (One a) m sf); viewLn (Deep ux (One a) m sf) = Some (nd, s); viewLn 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; viewLn 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 (One a) m sf); is_leveln_ftree n (Deep ux (One a) m sf); viewLn (Deep ux (One a) m sf) = Some (nd, s); viewLn 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:
viewLn (Deep ux (One a) m sf) = Some (nd, s)
viewLn m = None
[PROOF STEP]
have v1: "nd = a" "s = digitToTree sf"
[PROOF STATE]
proof (prove)
using this:
viewLn (Deep ux (One a) m sf) = Some (nd, s)
viewLn m = None

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

goal (2 subgoals):
 1. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewLn 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 (One a) m sf); is_leveln_ftree n (Deep ux (One a) m sf); viewLn (Deep ux (One a) m sf) = Some (nd, s); viewLn 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; viewLn 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 (One a) m sf); is_leveln_ftree n (Deep ux (One a) m sf); viewLn (Deep ux (One a) m sf) = Some (nd, s); viewLn 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 sf
is_measured_ftree (Deep ux (One a) m sf)
is_leveln_ftree n (Deep ux (One a) m sf)
[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 sf
is_measured_ftree (Deep ux (One a) m sf)
is_leveln_ftree n (Deep ux (One a) m sf)

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 sf; is_measured_node a; is_leveln_node n a; is_measured_ftree m; is_leveln_digit n sf; is_leveln_ftree (Suc n) m; is_measured_digit sf; ux = gmn a + gmft m + gmd sf\<rbrakk> \<Longrightarrow> is_measured_ftree (digitToTree sf)
 2. \<lbrakk>nd = a; s = digitToTree sf; is_measured_node a; is_leveln_node n a; is_measured_ftree m; is_leveln_digit n sf; is_leveln_ftree (Suc n) m; is_measured_digit sf; ux = gmn a + gmft m + gmd sf\<rbrakk> \<Longrightarrow> is_leveln_ftree n (digitToTree sf)
[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; viewLn 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 (One a) m sf); is_leveln_ftree n (Deep ux (One a) m sf); viewLn (Deep ux (One a) m sf) = Some (nd, s); viewLn 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; viewLn 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 (One a) m sf); is_leveln_ftree n (Deep ux (One a) m sf); viewLn (Deep ux (One a) m sf) = Some (nd, s); viewLn 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:
viewLn 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; viewLn 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 (One a) m sf); is_leveln_ftree n (Deep ux (One a) m sf); viewLn (Deep ux (One a) m sf) = Some (nd, s); viewLn 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:
viewLn (Deep ux (One a) m sf) = Some (nd, s)
viewLn m = Some (b, m2)
[PROOF STEP]
have v2: "nd = a" "s = (deep (nodeToDigit b) m2 sf)"
[PROOF STATE]
proof (prove)
using this:
viewLn (Deep ux (One a) m sf) = Some (nd, s)
viewLn m = Some (b, m2)

goal (1 subgoal):
 1. nd = a &&& s = deep (nodeToDigit b) m2 sf
[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 (nodeToDigit b) m2 sf

goal (1 subgoal):
 1. \<And>aa t. \<lbrakk>\<And>n nd s. \<lbrakk>is_measured_ftree m; is_leveln_ftree n m; viewLn 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 (One a) m sf); is_leveln_ftree n (Deep ux (One a) m sf); viewLn (Deep ux (One a) m sf) = Some (nd, s); viewLn 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; viewLn 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; viewLn 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 (One a) m sf); is_leveln_ftree n (Deep ux (One a) m sf); viewLn (Deep ux (One a) m sf) = Some (nd, s); viewLn 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 (nodeToDigit b) m2 sf
is_measured_ftree (Deep ux (One a) m sf)
is_leveln_ftree n (Deep ux (One a) m sf)
[PROOF STEP]
have "is_measured_ftree m \<and> is_leveln_ftree (Suc n) m"
[PROOF STATE]
proof (prove)
using this:
nd = a
s = deep (nodeToDigit b) m2 sf
is_measured_ftree (Deep ux (One a) m sf)
is_leveln_ftree n (Deep ux (One a) m sf)

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; viewLn 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 (One a) m sf); is_leveln_ftree n (Deep ux (One a) m sf); viewLn (Deep ux (One a) m sf) = Some (nd, s); viewLn 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; viewLn 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
viewLn 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; viewLn 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 (One a) m sf); is_leveln_ftree n (Deep ux (One a) m sf); viewLn (Deep ux (One a) m sf) = Some (nd, s); viewLn 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 (One a) m sf)
is_leveln_ftree n (Deep ux (One a) m sf)
nd = a
s = deep (nodeToDigit b) m2 sf
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 (One a) m sf)
is_leveln_ftree n (Deep ux (One a) m sf)
nd = a
s = deep (nodeToDigit b) m2 sf
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