[STATEMENT]
lemma iam_delete_correct:
  "(iam_delete,op_map_delete) \<in> Id \<rightarrow> iam_rel' \<rightarrow> iam_rel'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_delete, op_map_delete) \<in> nat_rel \<rightarrow> iam_rel' \<rightarrow> iam_rel'
[PROOF STEP]
unfolding iam_\<alpha>_def[abs_def] iam_delete_def[abs_def] iam_rel'_def br_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k a. if k < array_length a then array_set a k None else a, op_map_delete) \<in> nat_rel \<rightarrow> {(c, a). a = (\<lambda>i. if i < array_length c then array_get c i else None) \<and> True} \<rightarrow> {(c, a). a = (\<lambda>i. if i < array_length c then array_get c i else None) \<and> True}
[PROOF STEP]
by (auto simp: Let_def array_get_set_iff)


[STATEMENT]
lemma iam_map_rel_def:
  "\<langle>nat_rel,Rv\<rangle>iam_map_rel \<equiv> \<langle>Rv\<rangle>iam_rel O iam_rel'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>nat_rel, Rv\<rangle>iam_map_rel \<equiv> \<langle>Rv\<rangle>iam_rel O iam_rel'
[PROOF STEP]
unfolding iam_map_rel_def_internal relAPP_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. if nat_rel = nat_rel then iam_rel Rv O iam_rel' else {} \<equiv> iam_rel Rv O iam_rel'
[PROOF STEP]
by simp


[STATEMENT]
lemma iam_map_rel_sv[relator_props]:
  "single_valued Rv \<Longrightarrow> single_valued (\<langle>nat_rel,Rv\<rangle>iam_map_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_valued Rv \<Longrightarrow> single_valued (\<langle>nat_rel, Rv\<rangle>iam_map_rel)
[PROOF STEP]
unfolding iam_map_rel_def iam_rel'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_valued Rv \<Longrightarrow> single_valued (\<langle>Rv\<rangle>iam_rel O br iam_\<alpha> iam_invar)
[PROOF STEP]
by tagged_solver


[STATEMENT]
lemma iam_empty_impl:
    "(iam_empty (), op_map_empty) \<in> \<langle>nat_rel,R\<rangle>iam_map_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_empty (), op_map_empty) \<in> \<langle>nat_rel, R\<rangle>iam_map_rel
[PROOF STEP]
unfolding iam_map_rel_def op_map_empty_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_empty (), Map.empty) \<in> \<langle>R\<rangle>iam_rel O iam_rel'
[PROOF STEP]
apply (intro relcompI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (iam_empty (), ?b) \<in> \<langle>R\<rangle>iam_rel
 2. (?b, Map.empty) \<in> iam_rel'
[PROOF STEP]
apply (rule param_iam_empty[THEN fun_relD], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_empty ?x'1, Map.empty) \<in> iam_rel'
[PROOF STEP]
apply (rule iam_empty_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iam_lookup_impl:
    "(iam_lookup, op_map_lookup)
  \<in> nat_rel \<rightarrow> \<langle>nat_rel,R\<rangle>iam_map_rel \<rightarrow> \<langle>R\<rangle>option_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_lookup, op_map_lookup) \<in> nat_rel \<rightarrow> \<langle>nat_rel, R\<rangle>iam_map_rel \<rightarrow> \<langle>R\<rangle>option_rel
[PROOF STEP]
unfolding iam_map_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_lookup, op_map_lookup) \<in> nat_rel \<rightarrow> \<langle>R\<rangle>iam_rel O iam_rel' \<rightarrow> \<langle>R\<rangle>option_rel
[PROOF STEP]
apply (intro fun_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> nat_rel; (aa, a'a) \<in> \<langle>R\<rangle>iam_rel O iam_rel'\<rbrakk> \<Longrightarrow> (iam_lookup a aa, op_map_lookup a' a'a) \<in> \<langle>R\<rangle>option_rel
[PROOF STEP]
apply (elim relcompE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a x y z. \<lbrakk>(a, a') \<in> nat_rel; (aa, a'a) = (x, z); (x, y) \<in> \<langle>R\<rangle>iam_rel; (y, z) \<in> iam_rel'\<rbrakk> \<Longrightarrow> (iam_lookup a aa, op_map_lookup a' a'a) \<in> \<langle>R\<rangle>option_rel
[PROOF STEP]
apply (frule iam_lookup_correct[param_fo], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a x y z. \<lbrakk>(a, a') \<in> nat_rel; (aa, a'a) = (x, z); (x, y) \<in> \<langle>R\<rangle>iam_rel; (y, z) \<in> iam_rel'; (iam_lookup a y, op_map_lookup a' z) \<in> \<langle>Id\<rangle>option_rel\<rbrakk> \<Longrightarrow> (iam_lookup a aa, op_map_lookup a' a'a) \<in> \<langle>R\<rangle>option_rel
[PROOF STEP]
apply (frule param_iam_lookup[param_fo], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a x y z. \<lbrakk>(a, a') \<in> nat_rel; (aa, a'a) = (x, z); (x, y) \<in> \<langle>R\<rangle>iam_rel; (y, z) \<in> iam_rel'; (iam_lookup a y, op_map_lookup a' z) \<in> \<langle>Id\<rangle>option_rel; (iam_lookup a x, iam_lookup a' y) \<in> \<langle>R\<rangle>option_rel\<rbrakk> \<Longrightarrow> (iam_lookup a aa, op_map_lookup a' a'a) \<in> \<langle>R\<rangle>option_rel
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iam_update_impl:
   "(iam_update, op_map_update) \<in>
     nat_rel \<rightarrow> R \<rightarrow> \<langle>nat_rel,R\<rangle>iam_map_rel \<rightarrow> \<langle>nat_rel,R\<rangle>iam_map_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_update, op_map_update) \<in> nat_rel \<rightarrow> R \<rightarrow> \<langle>nat_rel, R\<rangle>iam_map_rel \<rightarrow> \<langle>nat_rel, R\<rangle>iam_map_rel
[PROOF STEP]
unfolding iam_map_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_update, op_map_update) \<in> nat_rel \<rightarrow> R \<rightarrow> \<langle>R\<rangle>iam_rel O iam_rel' \<rightarrow> \<langle>R\<rangle>iam_rel O iam_rel'
[PROOF STEP]
apply (intro fun_relI, elim relcompEpair, intro relcompI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a' aa a'a ab a'b b. \<lbrakk>(a, a') \<in> nat_rel; (aa, a'a) \<in> R; (ab, b) \<in> \<langle>R\<rangle>iam_rel; (b, a'b) \<in> iam_rel'\<rbrakk> \<Longrightarrow> (iam_update a aa ab, ?b4 a a' aa a'a ab a'b b) \<in> \<langle>R\<rangle>iam_rel
 2. \<And>a a' aa a'a ab a'b b. \<lbrakk>(a, a') \<in> nat_rel; (aa, a'a) \<in> R; (ab, b) \<in> \<langle>R\<rangle>iam_rel; (b, a'b) \<in> iam_rel'\<rbrakk> \<Longrightarrow> (?b4 a a' aa a'a ab a'b b, op_map_update a' a'a a'b) \<in> iam_rel'
[PROOF STEP]
apply (erule (2) param_iam_update[param_fo])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a ab a'b b. \<lbrakk>(a, a') \<in> nat_rel; (aa, a'a) \<in> R; (ab, b) \<in> \<langle>R\<rangle>iam_rel; (b, a'b) \<in> iam_rel'\<rbrakk> \<Longrightarrow> (iam_update a' a'a b, op_map_update a' a'a a'b) \<in> iam_rel'
[PROOF STEP]
apply (rule iam_update_correct[param_fo])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a a' aa a'a ab a'b b. \<lbrakk>(a, a') \<in> nat_rel; (aa, a'a) \<in> R; (ab, b) \<in> \<langle>R\<rangle>iam_rel; (b, a'b) \<in> iam_rel'\<rbrakk> \<Longrightarrow> (a', a') \<in> nat_rel
 2. \<And>a a' aa a'a ab a'b b. \<lbrakk>(a, a') \<in> nat_rel; (aa, a'a) \<in> R; (ab, b) \<in> \<langle>R\<rangle>iam_rel; (b, a'b) \<in> iam_rel'\<rbrakk> \<Longrightarrow> (a'a, a'a) \<in> Id
 3. \<And>a a' aa a'a ab a'b b. \<lbrakk>(a, a') \<in> nat_rel; (aa, a'a) \<in> R; (ab, b) \<in> \<langle>R\<rangle>iam_rel; (b, a'b) \<in> iam_rel'\<rbrakk> \<Longrightarrow> (b, a'b) \<in> iam_rel'
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iam_delete_impl:
    "(iam_delete, op_map_delete) \<in>
        nat_rel \<rightarrow> \<langle>nat_rel,R\<rangle>iam_map_rel \<rightarrow> \<langle>nat_rel,R\<rangle>iam_map_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_delete, op_map_delete) \<in> nat_rel \<rightarrow> \<langle>nat_rel, R\<rangle>iam_map_rel \<rightarrow> \<langle>nat_rel, R\<rangle>iam_map_rel
[PROOF STEP]
unfolding iam_map_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_delete, op_map_delete) \<in> nat_rel \<rightarrow> \<langle>R\<rangle>iam_rel O iam_rel' \<rightarrow> \<langle>R\<rangle>iam_rel O iam_rel'
[PROOF STEP]
apply (intro fun_relI, elim relcompEpair, intro relcompI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a' aa a'a b. \<lbrakk>(a, a') \<in> nat_rel; (aa, b) \<in> \<langle>R\<rangle>iam_rel; (b, a'a) \<in> iam_rel'\<rbrakk> \<Longrightarrow> (iam_delete a aa, ?b3 a a' aa a'a b) \<in> \<langle>R\<rangle>iam_rel
 2. \<And>a a' aa a'a b. \<lbrakk>(a, a') \<in> nat_rel; (aa, b) \<in> \<langle>R\<rangle>iam_rel; (b, a'a) \<in> iam_rel'\<rbrakk> \<Longrightarrow> (?b3 a a' aa a'a b, op_map_delete a' a'a) \<in> iam_rel'
[PROOF STEP]
apply (erule (1) param_iam_delete[param_fo])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a b. \<lbrakk>(a, a') \<in> nat_rel; (aa, b) \<in> \<langle>R\<rangle>iam_rel; (b, a'a) \<in> iam_rel'\<rbrakk> \<Longrightarrow> (iam_delete a' b, op_map_delete a' a'a) \<in> iam_rel'
[PROOF STEP]
apply (rule iam_delete_correct[param_fo])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a' aa a'a b. \<lbrakk>(a, a') \<in> nat_rel; (aa, b) \<in> \<langle>R\<rangle>iam_rel; (b, a'a) \<in> iam_rel'\<rbrakk> \<Longrightarrow> (a', a') \<in> nat_rel
 2. \<And>a a' aa a'a b. \<lbrakk>(a, a') \<in> nat_rel; (aa, b) \<in> \<langle>R\<rangle>iam_rel; (b, a'a) \<in> iam_rel'\<rbrakk> \<Longrightarrow> (b, a'a) \<in> iam_rel'
[PROOF STEP]
by simp_all


[STATEMENT]
lemma distinct_iam_to_list_aux:
  shows "\<lbrakk>distinct xs; \<forall>(i,_)\<in>set xs. i \<ge> n\<rbrakk> \<Longrightarrow>
        distinct (iam_iteratei_aux n a
            (\<lambda>_.True) (\<lambda>x y. y @ [x]) xs)"
   (is "\<lbrakk>_;_\<rbrakk> \<Longrightarrow> distinct (?iam_to_list_aux n xs)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; \<forall>(i, uu_)\<in>set xs. n \<le> i\<rbrakk> \<Longrightarrow> distinct (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
proof (induction n arbitrary: xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs. \<lbrakk>distinct xs; \<forall>(i, uu_)\<in>set xs. 0 \<le> i\<rbrakk> \<Longrightarrow> distinct (iam_iteratei_aux 0 a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
 2. \<And>n xs. \<lbrakk>\<And>xs. \<lbrakk>distinct xs; \<forall>(i, uu_)\<in>set xs. n \<le> i\<rbrakk> \<Longrightarrow> distinct (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs); distinct xs; \<forall>(i, uu_)\<in>set xs. Suc n \<le> i\<rbrakk> \<Longrightarrow> distinct (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
case (0 xs)
[PROOF STATE]
proof (state)
this:
distinct xs
\<forall>a\<in>set xs. case a of (i, uu_) \<Rightarrow> 0 \<le> i

goal (2 subgoals):
 1. \<And>xs. \<lbrakk>distinct xs; \<forall>(i, uu_)\<in>set xs. 0 \<le> i\<rbrakk> \<Longrightarrow> distinct (iam_iteratei_aux 0 a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
 2. \<And>n xs. \<lbrakk>\<And>xs. \<lbrakk>distinct xs; \<forall>(i, uu_)\<in>set xs. n \<le> i\<rbrakk> \<Longrightarrow> distinct (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs); distinct xs; \<forall>(i, uu_)\<in>set xs. Suc n \<le> i\<rbrakk> \<Longrightarrow> distinct (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
distinct xs
\<forall>a\<in>set xs. case a of (i, uu_) \<Rightarrow> 0 \<le> i

goal (1 subgoal):
 1. distinct (iam_iteratei_aux 0 a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (iam_iteratei_aux 0 a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)

goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>\<And>xs. \<lbrakk>distinct xs; \<forall>(i, uu_)\<in>set xs. n \<le> i\<rbrakk> \<Longrightarrow> distinct (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs); distinct xs; \<forall>(i, uu_)\<in>set xs. Suc n \<le> i\<rbrakk> \<Longrightarrow> distinct (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>\<And>xs. \<lbrakk>distinct xs; \<forall>(i, uu_)\<in>set xs. n \<le> i\<rbrakk> \<Longrightarrow> distinct (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs); distinct xs; \<forall>(i, uu_)\<in>set xs. Suc n \<le> i\<rbrakk> \<Longrightarrow> distinct (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
case (Suc i xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct ?xs; \<forall>a\<in>set ?xs. case a of (ia, uu_) \<Rightarrow> i \<le> ia\<rbrakk> \<Longrightarrow> distinct (iam_iteratei_aux i a (\<lambda>_. True) (\<lambda>x y. y @ [x]) ?xs)
distinct xs
\<forall>a\<in>set xs. case a of (ia, uu_) \<Rightarrow> Suc i \<le> ia

goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>\<And>xs. \<lbrakk>distinct xs; \<forall>(i, uu_)\<in>set xs. n \<le> i\<rbrakk> \<Longrightarrow> distinct (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs); distinct xs; \<forall>(i, uu_)\<in>set xs. Suc n \<le> i\<rbrakk> \<Longrightarrow> distinct (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (iam_iteratei_aux (Suc i) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
proof (cases "array_get a i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. array_get a i = None \<Longrightarrow> distinct (iam_iteratei_aux (Suc i) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
 2. \<And>aa. array_get a i = Some aa \<Longrightarrow> distinct (iam_iteratei_aux (Suc i) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
array_get a i = None

goal (2 subgoals):
 1. array_get a i = None \<Longrightarrow> distinct (iam_iteratei_aux (Suc i) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
 2. \<And>aa. array_get a i = Some aa \<Longrightarrow> distinct (iam_iteratei_aux (Suc i) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
with Suc.IH[OF Suc.prems(1)] Suc.prems(2)
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>set xs. case a of (ia, uu_) \<Rightarrow> i \<le> ia \<Longrightarrow> distinct (iam_iteratei_aux i a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
\<forall>a\<in>set xs. case a of (ia, uu_) \<Rightarrow> Suc i \<le> ia
array_get a i = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set xs. case a of (ia, uu_) \<Rightarrow> i \<le> ia \<Longrightarrow> distinct (iam_iteratei_aux i a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
\<forall>a\<in>set xs. case a of (ia, uu_) \<Rightarrow> Suc i \<le> ia
array_get a i = None

goal (1 subgoal):
 1. distinct (iam_iteratei_aux (Suc i) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
distinct (iam_iteratei_aux (Suc i) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)

goal (1 subgoal):
 1. \<And>aa. array_get a i = Some aa \<Longrightarrow> distinct (iam_iteratei_aux (Suc i) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa. array_get a i = Some aa \<Longrightarrow> distinct (iam_iteratei_aux (Suc i) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
case (Some x)
[PROOF STATE]
proof (state)
this:
array_get a i = Some x

goal (1 subgoal):
 1. \<And>aa. array_get a i = Some aa \<Longrightarrow> distinct (iam_iteratei_aux (Suc i) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
let ?xs' = "xs @ [(i,x)]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa. array_get a i = Some aa \<Longrightarrow> distinct (iam_iteratei_aux (Suc i) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
from Suc.prems
[PROOF STATE]
proof (chain)
picking this:
distinct xs
\<forall>a\<in>set xs. case a of (ia, uu_) \<Rightarrow> Suc i \<le> ia
[PROOF STEP]
have "distinct ?xs'" and
            "\<forall>(i',x)\<in>set ?xs'. i' \<ge> i"
[PROOF STATE]
proof (prove)
using this:
distinct xs
\<forall>a\<in>set xs. case a of (ia, uu_) \<Rightarrow> Suc i \<le> ia

goal (1 subgoal):
 1. distinct (xs @ [(i, x)]) &&& \<forall>(i', x)\<in>set (xs @ [(i, x)]). i \<le> i'
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
distinct (xs @ [(i, x)])
\<forall>(i', x)\<in>set (xs @ [(i, x)]). i \<le> i'

goal (1 subgoal):
 1. \<And>aa. array_get a i = Some aa \<Longrightarrow> distinct (iam_iteratei_aux (Suc i) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
from Some and Suc.IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
array_get a i = Some x
distinct (iam_iteratei_aux i a (\<lambda>_. True) (\<lambda>x y. y @ [x]) (xs @ [(i, x)]))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
array_get a i = Some x
distinct (iam_iteratei_aux i a (\<lambda>_. True) (\<lambda>x y. y @ [x]) (xs @ [(i, x)]))

goal (1 subgoal):
 1. distinct (iam_iteratei_aux (Suc i) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (iam_iteratei_aux (Suc i) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
distinct (iam_iteratei_aux (Suc i) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distinct_iam_to_list:
  "distinct (iam_to_list a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (iam_to_list a)
[PROOF STEP]
unfolding it_to_list_def iam_iteratei_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (iam_iteratei_aux (array_length a) a (\<lambda>_. True) (\<lambda>x l. l @ [x]) [])
[PROOF STEP]
by (force intro: distinct_iam_to_list_aux)


[STATEMENT]
lemma iam_to_list_set_correct_aux:
  assumes "(a, m) \<in> iam_rel'"
  shows "\<lbrakk>n \<le> array_length a; map_to_set m - {(k,v). k < n} = set xs\<rbrakk>
         \<Longrightarrow> map_to_set m =
             set (iam_iteratei_aux n a (\<lambda>_.True) (\<lambda>x y. y @ [x]) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> array_length a; map_to_set m - {(k, v). k < n} = set xs\<rbrakk> \<Longrightarrow> map_to_set m = set (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
proof (induction n arbitrary: xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs. \<lbrakk>0 \<le> array_length a; map_to_set m - {(k, v). k < 0} = set xs\<rbrakk> \<Longrightarrow> map_to_set m = set (iam_iteratei_aux 0 a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
 2. \<And>n xs. \<lbrakk>\<And>xs. \<lbrakk>n \<le> array_length a; map_to_set m - {(k, v). k < n} = set xs\<rbrakk> \<Longrightarrow> map_to_set m = set (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs); Suc n \<le> array_length a; map_to_set m - {(k, v). k < Suc n} = set xs\<rbrakk> \<Longrightarrow> map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
case (0 xs)
[PROOF STATE]
proof (state)
this:
0 \<le> array_length a
map_to_set m - {a. case a of (k, v) \<Rightarrow> k < 0} = set xs

goal (2 subgoals):
 1. \<And>xs. \<lbrakk>0 \<le> array_length a; map_to_set m - {(k, v). k < 0} = set xs\<rbrakk> \<Longrightarrow> map_to_set m = set (iam_iteratei_aux 0 a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
 2. \<And>n xs. \<lbrakk>\<And>xs. \<lbrakk>n \<le> array_length a; map_to_set m - {(k, v). k < n} = set xs\<rbrakk> \<Longrightarrow> map_to_set m = set (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs); Suc n \<le> array_length a; map_to_set m - {(k, v). k < Suc n} = set xs\<rbrakk> \<Longrightarrow> map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
0 \<le> array_length a
map_to_set m - {a. case a of (k, v) \<Rightarrow> k < 0} = set xs

goal (1 subgoal):
 1. map_to_set m = set (iam_iteratei_aux 0 a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_to_set m = set (iam_iteratei_aux 0 a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)

goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>\<And>xs. \<lbrakk>n \<le> array_length a; map_to_set m - {(k, v). k < n} = set xs\<rbrakk> \<Longrightarrow> map_to_set m = set (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs); Suc n \<le> array_length a; map_to_set m - {(k, v). k < Suc n} = set xs\<rbrakk> \<Longrightarrow> map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>\<And>xs. \<lbrakk>n \<le> array_length a; map_to_set m - {(k, v). k < n} = set xs\<rbrakk> \<Longrightarrow> map_to_set m = set (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs); Suc n \<le> array_length a; map_to_set m - {(k, v). k < Suc n} = set xs\<rbrakk> \<Longrightarrow> map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
case (Suc n xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>n \<le> array_length a; map_to_set m - {a. case a of (k, v) \<Rightarrow> k < n} = set ?xs\<rbrakk> \<Longrightarrow> map_to_set m = set (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) ?xs)
Suc n \<le> array_length a
map_to_set m - {a. case a of (k, v) \<Rightarrow> k < Suc n} = set xs

goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>\<And>xs. \<lbrakk>n \<le> array_length a; map_to_set m - {(k, v). k < n} = set xs\<rbrakk> \<Longrightarrow> map_to_set m = set (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs); Suc n \<le> array_length a; map_to_set m - {(k, v). k < Suc n} = set xs\<rbrakk> \<Longrightarrow> map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
(a, m) \<in> iam_rel'
\<lbrakk>n \<le> array_length a; map_to_set m - {a. case a of (k, v) \<Rightarrow> k < n} = set ?xs\<rbrakk> \<Longrightarrow> map_to_set m = set (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) ?xs)
Suc n \<le> array_length a
map_to_set m - {a. case a of (k, v) \<Rightarrow> k < Suc n} = set xs
[PROOF STEP]
have [simp]: "array_get a n = m n"
[PROOF STATE]
proof (prove)
using this:
(a, m) \<in> iam_rel'
\<lbrakk>n \<le> array_length a; map_to_set m - {a. case a of (k, v) \<Rightarrow> k < n} = set ?xs\<rbrakk> \<Longrightarrow> map_to_set m = set (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) ?xs)
Suc n \<le> array_length a
map_to_set m - {a. case a of (k, v) \<Rightarrow> k < Suc n} = set xs

goal (1 subgoal):
 1. array_get a n = m n
[PROOF STEP]
unfolding iam_rel'_def br_def iam_\<alpha>_def[abs_def]
[PROOF STATE]
proof (prove)
using this:
(a, m) \<in> {(c, a). a = (\<lambda>i. if i < array_length c then array_get c i else None) \<and> True}
\<lbrakk>n \<le> array_length a; map_to_set m - {a. case a of (k, v) \<Rightarrow> k < n} = set ?xs\<rbrakk> \<Longrightarrow> map_to_set m = set (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) ?xs)
Suc n \<le> array_length a
map_to_set m - {a. case a of (k, v) \<Rightarrow> k < Suc n} = set xs

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

goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>\<And>xs. \<lbrakk>n \<le> array_length a; map_to_set m - {(k, v). k < n} = set xs\<rbrakk> \<Longrightarrow> map_to_set m = set (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs); Suc n \<le> array_length a; map_to_set m - {(k, v). k < Suc n} = set xs\<rbrakk> \<Longrightarrow> map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
proof (cases "m n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. m n = None \<Longrightarrow> map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
 2. \<And>aa. m n = Some aa \<Longrightarrow> map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
m n = None

goal (2 subgoals):
 1. m n = None \<Longrightarrow> map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
 2. \<And>aa. m n = Some aa \<Longrightarrow> map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
with Suc.prems(2)
[PROOF STATE]
proof (chain)
picking this:
map_to_set m - {a. case a of (k, v) \<Rightarrow> k < Suc n} = set xs
m n = None
[PROOF STEP]
have "map_to_set m - {(k,v). k < n} = set xs"
[PROOF STATE]
proof (prove)
using this:
map_to_set m - {a. case a of (k, v) \<Rightarrow> k < Suc n} = set xs
m n = None

goal (1 subgoal):
 1. map_to_set m - {(k, v). k < n} = set xs
[PROOF STEP]
unfolding map_to_set_def
[PROOF STATE]
proof (prove)
using this:
{(k, v). m k = Some v} - {a. case a of (k, v) \<Rightarrow> k < Suc n} = set xs
m n = None

goal (1 subgoal):
 1. {(k, v). m k = Some v} - {(k, v). k < n} = set xs
[PROOF STEP]
by (fastforce simp: less_Suc_eq)
[PROOF STATE]
proof (state)
this:
map_to_set m - {(k, v). k < n} = set xs

goal (2 subgoals):
 1. m n = None \<Longrightarrow> map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
 2. \<And>aa. m n = Some aa \<Longrightarrow> map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
from None and Suc.IH[OF _ this] and Suc.prems(1)
[PROOF STATE]
proof (chain)
picking this:
m n = None
n \<le> array_length a \<Longrightarrow> map_to_set m = set (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
Suc n \<le> array_length a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m n = None
n \<le> array_length a \<Longrightarrow> map_to_set m = set (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
Suc n \<le> array_length a

goal (1 subgoal):
 1. map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)

goal (1 subgoal):
 1. \<And>aa. m n = Some aa \<Longrightarrow> map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa. m n = Some aa \<Longrightarrow> map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
case (Some x)
[PROOF STATE]
proof (state)
this:
m n = Some x

goal (1 subgoal):
 1. \<And>aa. m n = Some aa \<Longrightarrow> map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
let ?xs' = "xs @ [(n,x)]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa. m n = Some aa \<Longrightarrow> map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
from Some and Suc.prems(2)
[PROOF STATE]
proof (chain)
picking this:
m n = Some x
map_to_set m - {a. case a of (k, v) \<Rightarrow> k < Suc n} = set xs
[PROOF STEP]
have "map_to_set m - {(k,v). k < n} = set ?xs'"
[PROOF STATE]
proof (prove)
using this:
m n = Some x
map_to_set m - {a. case a of (k, v) \<Rightarrow> k < Suc n} = set xs

goal (1 subgoal):
 1. map_to_set m - {(k, v). k < n} = set (xs @ [(n, x)])
[PROOF STEP]
unfolding map_to_set_def
[PROOF STATE]
proof (prove)
using this:
m n = Some x
{(k, v). m k = Some v} - {a. case a of (k, v) \<Rightarrow> k < Suc n} = set xs

goal (1 subgoal):
 1. {(k, v). m k = Some v} - {(k, v). k < n} = set (xs @ [(n, x)])
[PROOF STEP]
by (fastforce simp: less_Suc_eq)
[PROOF STATE]
proof (state)
this:
map_to_set m - {(k, v). k < n} = set (xs @ [(n, x)])

goal (1 subgoal):
 1. \<And>aa. m n = Some aa \<Longrightarrow> map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
from Some and Suc.IH[OF _ this] and Suc.prems(1)
[PROOF STATE]
proof (chain)
picking this:
m n = Some x
n \<le> array_length a \<Longrightarrow> map_to_set m = set (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) (xs @ [(n, x)]))
Suc n \<le> array_length a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m n = Some x
n \<le> array_length a \<Longrightarrow> map_to_set m = set (iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x y. y @ [x]) (xs @ [(n, x)]))
Suc n \<le> array_length a

goal (1 subgoal):
 1. map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
map_to_set m = set (iam_iteratei_aux (Suc n) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iam_to_list_set_correct:
  assumes "(a, m) \<in> iam_rel'"
  shows "map_to_set m = set (iam_to_list a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_to_set m = set (iam_to_list a)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_to_set m = set (iam_to_list a)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
(a, m) \<in> iam_rel'
[PROOF STEP]
have A: "map_to_set m - {(k, v). k < array_length a} = set []"
[PROOF STATE]
proof (prove)
using this:
(a, m) \<in> iam_rel'

goal (1 subgoal):
 1. map_to_set m - {(k, v). k < array_length a} = set []
[PROOF STEP]
unfolding map_to_set_def iam_rel'_def br_def iam_\<alpha>_def[abs_def]
[PROOF STATE]
proof (prove)
using this:
(a, m) \<in> {(c, a). a = (\<lambda>i. if i < array_length c then array_get c i else None) \<and> True}

goal (1 subgoal):
 1. {(k, v). m k = Some v} - {(k, v). k < array_length a} = set []
[PROOF STEP]
by (force split: if_split_asm)
[PROOF STATE]
proof (state)
this:
map_to_set m - {(k, v). k < array_length a} = set []

goal (1 subgoal):
 1. map_to_set m = set (iam_to_list a)
[PROOF STEP]
with iam_to_list_set_correct_aux[OF assms _ A]
[PROOF STATE]
proof (chain)
picking this:
array_length a \<le> array_length a \<Longrightarrow> map_to_set m = set (iam_iteratei_aux (array_length a) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) [])
map_to_set m - {(k, v). k < array_length a} = set []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
array_length a \<le> array_length a \<Longrightarrow> map_to_set m = set (iam_iteratei_aux (array_length a) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) [])
map_to_set m - {(k, v). k < array_length a} = set []

goal (1 subgoal):
 1. map_to_set m = set (iam_to_list a)
[PROOF STEP]
unfolding it_to_list_def iam_iteratei_def
[PROOF STATE]
proof (prove)
using this:
array_length a \<le> array_length a \<Longrightarrow> map_to_set m = set (iam_iteratei_aux (array_length a) a (\<lambda>_. True) (\<lambda>x y. y @ [x]) [])
map_to_set m - {(k, v). k < array_length a} = set []

goal (1 subgoal):
 1. map_to_set m = set (iam_iteratei_aux (array_length a) a (\<lambda>_. True) (\<lambda>x l. l @ [x]) [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_to_set m = set (iam_to_list a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iam_iteratei_aux_append:
  "n \<le> length xs \<Longrightarrow> iam_iteratei_aux n (Array (xs @ ys)) =
             iam_iteratei_aux n (Array xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> length xs \<Longrightarrow> iam_iteratei_aux n (Array (xs @ ys)) = iam_iteratei_aux n (Array xs)
[PROOF STEP]
apply (induction n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 \<le> length xs \<Longrightarrow> iam_iteratei_aux 0 (Array (xs @ ys)) = iam_iteratei_aux 0 (Array xs)
 2. \<And>n. \<lbrakk>n \<le> length xs \<Longrightarrow> iam_iteratei_aux n (Array (xs @ ys)) = iam_iteratei_aux n (Array xs); Suc n \<le> length xs\<rbrakk> \<Longrightarrow> iam_iteratei_aux (Suc n) (Array (xs @ ys)) = iam_iteratei_aux (Suc n) (Array xs)
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<le> length xs \<Longrightarrow> iam_iteratei_aux n (Array (xs @ ys)) = iam_iteratei_aux n (Array xs); Suc n \<le> length xs\<rbrakk> \<Longrightarrow> iam_iteratei_aux (Suc n) (Array (xs @ ys)) = iam_iteratei_aux (Suc n) (Array xs)
[PROOF STEP]
apply (intro ext, auto split: option.split simp: nth_append)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iam_iteratei_append:
  "iam_iteratei (Array (xs @ [None])) c f \<sigma> =
       iam_iteratei (Array xs) c f \<sigma>"
  "iam_iteratei (Array (xs @ [Some x])) c f \<sigma> =
       iam_iteratei (Array xs) c f
       (if c \<sigma> then (f (length xs, x) \<sigma>) else \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iam_iteratei (Array (xs @ [None])) c f \<sigma> = iam_iteratei (Array xs) c f \<sigma> &&& iam_iteratei (Array (xs @ [Some x])) c f \<sigma> = iam_iteratei (Array xs) c f (if c \<sigma> then f (length xs, x) \<sigma> else \<sigma>)
[PROOF STEP]
unfolding  iam_iteratei_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iam_iteratei_aux (array_length (Array (xs @ [None]))) (Array (xs @ [None])) c f \<sigma> = iam_iteratei_aux (array_length (Array xs)) (Array xs) c f \<sigma> &&& iam_iteratei_aux (array_length (Array (xs @ [Some x]))) (Array (xs @ [Some x])) c f \<sigma> = iam_iteratei_aux (array_length (Array xs)) (Array xs) c f (if c \<sigma> then f (length xs, x) \<sigma> else \<sigma>)
[PROOF STEP]
apply (cases "length xs")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. length xs = 0 \<Longrightarrow> iam_iteratei_aux (array_length (Array (xs @ [None]))) (Array (xs @ [None])) c f \<sigma> = iam_iteratei_aux (array_length (Array xs)) (Array xs) c f \<sigma>
 2. \<And>nat. length xs = Suc nat \<Longrightarrow> iam_iteratei_aux (array_length (Array (xs @ [None]))) (Array (xs @ [None])) c f \<sigma> = iam_iteratei_aux (array_length (Array xs)) (Array xs) c f \<sigma>
 3. iam_iteratei_aux (array_length (Array (xs @ [Some x]))) (Array (xs @ [Some x])) c f \<sigma> = iam_iteratei_aux (array_length (Array xs)) (Array xs) c f (if c \<sigma> then f (length xs, x) \<sigma> else \<sigma>)
[PROOF STEP]
apply (simp add: iam_iteratei_aux_append)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>nat. length xs = Suc nat \<Longrightarrow> iam_iteratei_aux (array_length (Array (xs @ [None]))) (Array (xs @ [None])) c f \<sigma> = iam_iteratei_aux (array_length (Array xs)) (Array xs) c f \<sigma>
 2. iam_iteratei_aux (array_length (Array (xs @ [Some x]))) (Array (xs @ [Some x])) c f \<sigma> = iam_iteratei_aux (array_length (Array xs)) (Array xs) c f (if c \<sigma> then f (length xs, x) \<sigma> else \<sigma>)
[PROOF STEP]
apply (force simp: nth_append iam_iteratei_aux_append) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iam_iteratei_aux (array_length (Array (xs @ [Some x]))) (Array (xs @ [Some x])) c f \<sigma> = iam_iteratei_aux (array_length (Array xs)) (Array xs) c f (if c \<sigma> then f (length xs, x) \<sigma> else \<sigma>)
[PROOF STEP]
apply (cases "length xs")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length xs = 0 \<Longrightarrow> iam_iteratei_aux (array_length (Array (xs @ [Some x]))) (Array (xs @ [Some x])) c f \<sigma> = iam_iteratei_aux (array_length (Array xs)) (Array xs) c f (if c \<sigma> then f (length xs, x) \<sigma> else \<sigma>)
 2. \<And>nat. length xs = Suc nat \<Longrightarrow> iam_iteratei_aux (array_length (Array (xs @ [Some x]))) (Array (xs @ [Some x])) c f \<sigma> = iam_iteratei_aux (array_length (Array xs)) (Array xs) c f (if c \<sigma> then f (length xs, x) \<sigma> else \<sigma>)
[PROOF STEP]
apply (simp add: iam_iteratei_aux_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. length xs = Suc nat \<Longrightarrow> iam_iteratei_aux (array_length (Array (xs @ [Some x]))) (Array (xs @ [Some x])) c f \<sigma> = iam_iteratei_aux (array_length (Array xs)) (Array xs) c f (if c \<sigma> then f (length xs, x) \<sigma> else \<sigma>)
[PROOF STEP]
apply (force split: option.split
             simp: nth_append iam_iteratei_aux_append) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iam_iteratei_aux_Cons:
  "n < array_length a \<Longrightarrow>
      iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x l. l @ [x]) (x#xs) =
      x # iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x l. l @ [x]) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < array_length a \<Longrightarrow> iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x l. l @ [x]) (x # xs) = x # iam_iteratei_aux n a (\<lambda>_. True) (\<lambda>x l. l @ [x]) xs
[PROOF STEP]
by (induction n arbitrary: xs, auto split: option.split)


[STATEMENT]
lemma iam_to_list_append:
  "iam_to_list (Array (xs @ [None])) = iam_to_list (Array xs)"
  "iam_to_list (Array (xs @ [Some x])) =
       (length xs, x) # iam_to_list (Array xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iam_to_list (Array (xs @ [None])) = iam_to_list (Array xs) &&& iam_to_list (Array (xs @ [Some x])) = (length xs, x) # iam_to_list (Array xs)
[PROOF STEP]
unfolding  it_to_list_def iam_iteratei_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iam_iteratei_aux (array_length (Array (xs @ [None]))) (Array (xs @ [None])) (\<lambda>_. True) (\<lambda>x l. l @ [x]) [] = iam_iteratei_aux (array_length (Array xs)) (Array xs) (\<lambda>_. True) (\<lambda>x l. l @ [x]) [] &&& iam_iteratei_aux (array_length (Array (xs @ [Some x]))) (Array (xs @ [Some x])) (\<lambda>_. True) (\<lambda>x l. l @ [x]) [] = (length xs, x) # iam_iteratei_aux (array_length (Array xs)) (Array xs) (\<lambda>_. True) (\<lambda>x l. l @ [x]) []
[PROOF STEP]
apply (simp add: iam_iteratei_aux_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iam_iteratei_aux (array_length (Array (xs @ [Some x]))) (Array (xs @ [Some x])) (\<lambda>_. True) (\<lambda>x l. l @ [x]) [] = (length xs, x) # iam_iteratei_aux (array_length (Array xs)) (Array xs) (\<lambda>_. True) (\<lambda>x l. l @ [x]) []
[PROOF STEP]
apply (simp add: iam_iteratei_aux_Cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iam_iteratei_aux (length xs) (Array (xs @ [Some x])) (\<lambda>_. True) (\<lambda>x l. l @ [x]) [] = iam_iteratei_aux (length xs) (Array xs) (\<lambda>_. True) (\<lambda>x l. l @ [x]) []
[PROOF STEP]
apply (simp add: iam_iteratei_aux_append)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma autoref_iam_is_iterator[autoref_ga_rules]:
  shows "is_map_to_list nat_rel Rv iam_map_rel iam_to_list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_map_to_list nat_rel Rv iam_map_rel iam_to_list
[PROOF STEP]
unfolding is_map_to_list_def is_map_to_sorted_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m m'. (m, m') \<in> \<langle>nat_rel, Rv\<rangle>iam_map_rel \<longrightarrow> (\<exists>l'. (iam_to_list m, l') \<in> \<langle>nat_rel \<times>\<^sub>r Rv\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set m'))
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m m'. (m, m') \<in> \<langle>nat_rel, Rv\<rangle>iam_map_rel \<Longrightarrow> \<exists>l'. (iam_to_list m, l') \<in> \<langle>nat_rel \<times>\<^sub>r Rv\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set m')
[PROOF STEP]
fix a m'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m m'. (m, m') \<in> \<langle>nat_rel, Rv\<rangle>iam_map_rel \<Longrightarrow> \<exists>l'. (iam_to_list m, l') \<in> \<langle>nat_rel \<times>\<^sub>r Rv\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set m')
[PROOF STEP]
assume "(a,m') \<in> \<langle>nat_rel,Rv\<rangle>iam_map_rel"
[PROOF STATE]
proof (state)
this:
(a, m') \<in> \<langle>nat_rel, Rv\<rangle>iam_map_rel

goal (1 subgoal):
 1. \<And>m m'. (m, m') \<in> \<langle>nat_rel, Rv\<rangle>iam_map_rel \<Longrightarrow> \<exists>l'. (iam_to_list m, l') \<in> \<langle>nat_rel \<times>\<^sub>r Rv\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set m')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(a, m') \<in> \<langle>nat_rel, Rv\<rangle>iam_map_rel
[PROOF STEP]
obtain a' where [param]: "(a,a')\<in>\<langle>Rv\<rangle>iam_rel"
    and "(a',m')\<in>iam_rel'"
[PROOF STATE]
proof (prove)
using this:
(a, m') \<in> \<langle>nat_rel, Rv\<rangle>iam_map_rel

goal (1 subgoal):
 1. (\<And>a'. \<lbrakk>(a, a') \<in> \<langle>Rv\<rangle>iam_rel; (a', m') \<in> iam_rel'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding iam_map_rel_def
[PROOF STATE]
proof (prove)
using this:
(a, m') \<in> \<langle>Rv\<rangle>iam_rel O iam_rel'

goal (1 subgoal):
 1. (\<And>a'. \<lbrakk>(a, a') \<in> \<langle>Rv\<rangle>iam_rel; (a', m') \<in> iam_rel'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(a, a') \<in> \<langle>Rv\<rangle>iam_rel
(a', m') \<in> iam_rel'

goal (1 subgoal):
 1. \<And>m m'. (m, m') \<in> \<langle>nat_rel, Rv\<rangle>iam_map_rel \<Longrightarrow> \<exists>l'. (iam_to_list m, l') \<in> \<langle>nat_rel \<times>\<^sub>r Rv\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set m')
[PROOF STEP]
have "(iam_to_list a, iam_to_list a')
            \<in> \<langle>\<langle>nat_rel, Rv\<rangle>prod_rel\<rangle>list_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_to_list a, iam_to_list a') \<in> \<langle>nat_rel \<times>\<^sub>r Rv\<rangle>list_rel
[PROOF STEP]
by parametricity
[PROOF STATE]
proof (state)
this:
(iam_to_list a, iam_to_list a') \<in> \<langle>nat_rel \<times>\<^sub>r Rv\<rangle>list_rel

goal (1 subgoal):
 1. \<And>m m'. (m, m') \<in> \<langle>nat_rel, Rv\<rangle>iam_map_rel \<Longrightarrow> \<exists>l'. (iam_to_list m, l') \<in> \<langle>nat_rel \<times>\<^sub>r Rv\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set m')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(iam_to_list a, iam_to_list a') \<in> \<langle>nat_rel \<times>\<^sub>r Rv\<rangle>list_rel

goal (1 subgoal):
 1. \<And>m m'. (m, m') \<in> \<langle>nat_rel, Rv\<rangle>iam_map_rel \<Longrightarrow> \<exists>l'. (iam_to_list m, l') \<in> \<langle>nat_rel \<times>\<^sub>r Rv\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set m')
[PROOF STEP]
from distinct_iam_to_list and
                iam_to_list_set_correct[OF \<open>(a',m')\<in>iam_rel'\<close>]
[PROOF STATE]
proof (chain)
picking this:
distinct (iam_to_list ?a)
map_to_set m' = set (iam_to_list a')
[PROOF STEP]
have "RETURN (iam_to_list a') \<le> it_to_sorted_list
               (key_rel (\<lambda>_ _. True)) (map_to_set m')"
[PROOF STATE]
proof (prove)
using this:
distinct (iam_to_list ?a)
map_to_set m' = set (iam_to_list a')

goal (1 subgoal):
 1. RETURN (iam_to_list a') \<le> it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set m')
[PROOF STEP]
unfolding it_to_sorted_list_def key_rel_def[abs_def]
[PROOF STATE]
proof (prove)
using this:
distinct (iam_to_list ?a)
map_to_set m' = set (iam_to_list a')

goal (1 subgoal):
 1. RETURN (iam_to_list a') \<le> SPEC (\<lambda>l. distinct l \<and> map_to_set m' = set l \<and> sorted_wrt (\<lambda>a b. True) l)
[PROOF STEP]
by (force intro: refine_vcg)
[PROOF STATE]
proof (state)
this:
RETURN (iam_to_list a') \<le> it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set m')

goal (1 subgoal):
 1. \<And>m m'. (m, m') \<in> \<langle>nat_rel, Rv\<rangle>iam_map_rel \<Longrightarrow> \<exists>l'. (iam_to_list m, l') \<in> \<langle>nat_rel \<times>\<^sub>r Rv\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set m')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(iam_to_list a, iam_to_list a') \<in> \<langle>nat_rel \<times>\<^sub>r Rv\<rangle>list_rel
RETURN (iam_to_list a') \<le> it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set m')
[PROOF STEP]
show "\<exists>l'. (iam_to_list a, l') \<in>
                            \<langle>\<langle>nat_rel, Rv\<rangle>prod_rel\<rangle>list_rel
                    \<and> RETURN l' \<le> it_to_sorted_list (
                        key_rel (\<lambda>_ _. True)) (map_to_set m')"
[PROOF STATE]
proof (prove)
using this:
(iam_to_list a, iam_to_list a') \<in> \<langle>nat_rel \<times>\<^sub>r Rv\<rangle>list_rel
RETURN (iam_to_list a') \<le> it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set m')

goal (1 subgoal):
 1. \<exists>l'. (iam_to_list a, l') \<in> \<langle>nat_rel \<times>\<^sub>r Rv\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set m')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>l'. (iam_to_list a, l') \<in> \<langle>nat_rel \<times>\<^sub>r Rv\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set m')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iam_iteratei_altdef:
    "iam_iteratei a = foldli (iam_to_list a)"
     (is "?f a = ?g (iam_to_list a)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iam_iteratei a = foldli (iam_to_list a)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iam_iteratei a = foldli (iam_to_list a)
[PROOF STEP]
obtain l where "a = Array l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. a = Array l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases a)
[PROOF STATE]
proof (state)
this:
a = Array l

goal (1 subgoal):
 1. iam_iteratei a = foldli (iam_to_list a)
[PROOF STEP]
have "?f (Array l) = ?g (iam_to_list (Array l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
proof (induction "length l" arbitrary: l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l. 0 = length l \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
 2. \<And>x l. \<lbrakk>\<And>l. x = length l \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l)); Suc x = length l\<rbrakk> \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
case (0 l)
[PROOF STATE]
proof (state)
this:
0 = length l

goal (2 subgoals):
 1. \<And>l. 0 = length l \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
 2. \<And>x l. \<lbrakk>\<And>l. x = length l \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l)); Suc x = length l\<rbrakk> \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
0 = length l

goal (1 subgoal):
 1. iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
by (intro ext,
          simp add: iam_iteratei_def it_to_list_def)
[PROOF STATE]
proof (state)
this:
iam_iteratei (Array l) = foldli (iam_to_list (Array l))

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. x = length l \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l)); Suc x = length l\<rbrakk> \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. x = length l \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l)); Suc x = length l\<rbrakk> \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
case (Suc n l)
[PROOF STATE]
proof (state)
this:
n = length ?l \<Longrightarrow> iam_iteratei (Array ?l) = foldli (iam_to_list (Array ?l))
Suc n = length l

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. x = length l \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l)); Suc x = length l\<rbrakk> \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
hence "l \<noteq> []" and [simp]: "length l = Suc n"
[PROOF STATE]
proof (prove)
using this:
n = length ?l \<Longrightarrow> iam_iteratei (Array ?l) = foldli (iam_to_list (Array ?l))
Suc n = length l

goal (1 subgoal):
 1. l \<noteq> [] &&& length l = Suc n
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
l \<noteq> []
length l = Suc n

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. x = length l \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l)); Suc x = length l\<rbrakk> \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
with append_butlast_last_id
[PROOF STATE]
proof (chain)
picking this:
?xs \<noteq> [] \<Longrightarrow> butlast ?xs @ [last ?xs] = ?xs
l \<noteq> []
length l = Suc n
[PROOF STEP]
have [simp]:
          "butlast l @ [last l] = l"
[PROOF STATE]
proof (prove)
using this:
?xs \<noteq> [] \<Longrightarrow> butlast ?xs @ [last ?xs] = ?xs
l \<noteq> []
length l = Suc n

goal (1 subgoal):
 1. butlast l @ [last l] = l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
butlast l @ [last l] = l

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. x = length l \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l)); Suc x = length l\<rbrakk> \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
with Suc
[PROOF STATE]
proof (chain)
picking this:
n = length ?l \<Longrightarrow> iam_iteratei (Array ?l) = foldli (iam_to_list (Array ?l))
Suc n = length l
butlast l @ [last l] = l
[PROOF STEP]
have [simp]: "length (butlast l) = n"
[PROOF STATE]
proof (prove)
using this:
n = length ?l \<Longrightarrow> iam_iteratei (Array ?l) = foldli (iam_to_list (Array ?l))
Suc n = length l
butlast l @ [last l] = l

goal (1 subgoal):
 1. length (butlast l) = n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (butlast l) = n

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. x = length l \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l)); Suc x = length l\<rbrakk> \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
note IH = Suc(1)[OF this[symmetric]]
[PROOF STATE]
proof (state)
this:
iam_iteratei (Array (butlast l)) = foldli (iam_to_list (Array (butlast l)))

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. x = length l \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l)); Suc x = length l\<rbrakk> \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
let ?l' = "iam_to_list (Array l)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. x = length l \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l)); Suc x = length l\<rbrakk> \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
proof (cases "last l")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. last l = None \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
 2. \<And>a. last l = Some a \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
last l = None

goal (2 subgoals):
 1. last l = None \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
 2. \<And>a. last l = Some a \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
have "?f (Array l) =
              ?f (Array (butlast l @ [last l]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iam_iteratei (Array l) = iam_iteratei (Array (butlast l @ [last l]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
iam_iteratei (Array l) = iam_iteratei (Array (butlast l @ [last l]))

goal (2 subgoals):
 1. last l = None \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
 2. \<And>a. last l = Some a \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
iam_iteratei (Array l) = iam_iteratei (Array (butlast l @ [last l]))

goal (2 subgoals):
 1. last l = None \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
 2. \<And>a. last l = Some a \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
have "... = ?g (iam_to_list (Array (butlast l)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iam_iteratei (Array (butlast l @ [last l])) = foldli (iam_to_list (Array (butlast l)))
[PROOF STEP]
by (force simp: None iam_iteratei_append IH)
[PROOF STATE]
proof (state)
this:
iam_iteratei (Array (butlast l @ [last l])) = foldli (iam_to_list (Array (butlast l)))

goal (2 subgoals):
 1. last l = None \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
 2. \<And>a. last l = Some a \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
iam_iteratei (Array (butlast l @ [last l])) = foldli (iam_to_list (Array (butlast l)))

goal (2 subgoals):
 1. last l = None \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
 2. \<And>a. last l = Some a \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
have "iam_to_list (Array (butlast l)) =
              iam_to_list (Array (butlast l @ [last l]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iam_to_list (Array (butlast l)) = iam_to_list (Array (butlast l @ [last l]))
[PROOF STEP]
using None
[PROOF STATE]
proof (prove)
using this:
last l = None

goal (1 subgoal):
 1. iam_to_list (Array (butlast l)) = iam_to_list (Array (butlast l @ [last l]))
[PROOF STEP]
by (simp add: iam_to_list_append)
[PROOF STATE]
proof (state)
this:
iam_to_list (Array (butlast l)) = iam_to_list (Array (butlast l @ [last l]))

goal (2 subgoals):
 1. last l = None \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
 2. \<And>a. last l = Some a \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
iam_iteratei (Array l) = foldli (iam_to_list (Array (butlast l @ [last l])))
[PROOF STEP]
show "?f (Array l) = ?g ?l'"
[PROOF STATE]
proof (prove)
using this:
iam_iteratei (Array l) = foldli (iam_to_list (Array (butlast l @ [last l])))

goal (1 subgoal):
 1. iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
iam_iteratei (Array l) = foldli (iam_to_list (Array l))

goal (1 subgoal):
 1. \<And>a. last l = Some a \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. last l = Some a \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
case (Some x)
[PROOF STATE]
proof (state)
this:
last l = Some x

goal (1 subgoal):
 1. \<And>a. last l = Some a \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
have "?f (Array l) =
              ?f (Array (butlast l @ [last l]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iam_iteratei (Array l) = iam_iteratei (Array (butlast l @ [last l]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
iam_iteratei (Array l) = iam_iteratei (Array (butlast l @ [last l]))

goal (1 subgoal):
 1. \<And>a. last l = Some a \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
iam_iteratei (Array l) = iam_iteratei (Array (butlast l @ [last l]))

goal (1 subgoal):
 1. \<And>a. last l = Some a \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
have "... = ?g (iam_to_list
              (Array (butlast l @ [last l])))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iam_iteratei (Array (butlast l @ [last l])) = foldli (iam_to_list (Array (butlast l @ [last l])))
[PROOF STEP]
by (force simp: IH iam_iteratei_append
                      iam_to_list_append Some)
[PROOF STATE]
proof (state)
this:
iam_iteratei (Array (butlast l @ [last l])) = foldli (iam_to_list (Array (butlast l @ [last l])))

goal (1 subgoal):
 1. \<And>a. last l = Some a \<Longrightarrow> iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
iam_iteratei (Array l) = foldli (iam_to_list (Array (butlast l @ [last l])))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
iam_iteratei (Array l) = foldli (iam_to_list (Array (butlast l @ [last l])))

goal (1 subgoal):
 1. iam_iteratei (Array l) = foldli (iam_to_list (Array l))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
iam_iteratei (Array l) = foldli (iam_to_list (Array l))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
iam_iteratei (Array l) = foldli (iam_to_list (Array l))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
iam_iteratei (Array l) = foldli (iam_to_list (Array l))

goal (1 subgoal):
 1. iam_iteratei a = foldli (iam_to_list a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
iam_iteratei (Array l) = foldli (iam_to_list (Array l))

goal (1 subgoal):
 1. iam_iteratei a = foldli (iam_to_list a)
[PROOF STEP]
by (simp add: \<open>a = Array l\<close>)
[PROOF STATE]
proof (state)
this:
iam_iteratei a = foldli (iam_to_list a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pi_iam[icf_proper_iteratorI]:
  "proper_it (iam_iteratei a) (iam_iteratei a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (iam_iteratei a) (iam_iteratei a)
[PROOF STEP]
unfolding proper_it_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. iam_iteratei a = foldli l \<and> iam_iteratei a = foldli l
[PROOF STEP]
by (force simp: iam_iteratei_altdef)


[STATEMENT]
lemma pi'_iam[icf_proper_iteratorI]:
  "proper_it' iam_iteratei iam_iteratei"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it' iam_iteratei iam_iteratei
[PROOF STEP]
by (rule proper_it'I, rule pi_iam)


[STATEMENT]
lemma invariant_run:
      assumes "P p" "\<And> p. P p \<Longrightarrow> \<exists> a. enabled a p \<and> P (execute a p) \<and> Q p a"
      obtains r
      where "run r p" "pred_stream P (p ## trace r p)" "stream_all2 Q (p ## trace r p) r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; pred_stream P (p ## trace r p); stream_all2 Q (p ## trace r p) r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; pred_stream P (p ## trace r p); stream_all2 Q (p ## trace r p) r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain f where 1: "enabled (f p) p" "P (execute (f p) p)" "Q p (f p)" if "P p" for p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<And>p. P p \<Longrightarrow> enabled (f p) p; \<And>p. P p \<Longrightarrow> P (execute (f p) p); \<And>p. P p \<Longrightarrow> Q p (f p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
P ?p \<Longrightarrow> \<exists>a. enabled a ?p \<and> P (execute a ?p) \<and> Q ?p a

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<And>p. P p \<Longrightarrow> enabled (f p) p; \<And>p. P p \<Longrightarrow> P (execute (f p) p); \<And>p. P p \<Longrightarrow> Q p (f p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
P ?p \<Longrightarrow> enabled (f ?p) ?p
P ?p \<Longrightarrow> P (execute (f ?p) ?p)
P ?p \<Longrightarrow> Q ?p (f ?p)

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; pred_stream P (p ## trace r p); stream_all2 Q (p ## trace r p) r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?g = "\<lambda> p. execute (f p) p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; pred_stream P (p ## trace r p); stream_all2 Q (p ## trace r p) r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?r = "\<lambda> p. smap f (siterate ?g p)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; pred_stream P (p ## trace r p); stream_all2 Q (p ## trace r p) r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. run ?r p
 2. pred_stream P (p ## trace ?r p)
 3. stream_all2 Q (p ## trace ?r p) ?r
[PROOF STEP]
show "run (?r p) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run (smap f (siterate (\<lambda>p. execute (f p) p) p)) p
[PROOF STEP]
using assms(1) 1
[PROOF STATE]
proof (prove)
using this:
P p
P ?p \<Longrightarrow> enabled (f ?p) ?p
P ?p \<Longrightarrow> P (execute (f ?p) ?p)
P ?p \<Longrightarrow> Q ?p (f ?p)

goal (1 subgoal):
 1. run (smap f (siterate (\<lambda>p. execute (f p) p) p)) p
[PROOF STEP]
by (coinduction arbitrary: p) (auto)
[PROOF STATE]
proof (state)
this:
run (smap f (siterate (\<lambda>p. execute (f p) p) p)) p

goal (2 subgoals):
 1. pred_stream P (p ## trace (smap f (siterate (\<lambda>p. execute (f p) p) p)) p)
 2. stream_all2 Q (p ## trace (smap f (siterate (\<lambda>p. execute (f p) p) p)) p) (smap f (siterate (\<lambda>p. execute (f p) p) p))
[PROOF STEP]
show "pred_stream P (p ## trace (?r p) p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred_stream P (p ## trace (smap f (siterate (\<lambda>p. execute (f p) p) p)) p)
[PROOF STEP]
using assms(1) 1
[PROOF STATE]
proof (prove)
using this:
P p
P ?p \<Longrightarrow> enabled (f ?p) ?p
P ?p \<Longrightarrow> P (execute (f ?p) ?p)
P ?p \<Longrightarrow> Q ?p (f ?p)

goal (1 subgoal):
 1. pred_stream P (p ## trace (smap f (siterate (\<lambda>p. execute (f p) p) p)) p)
[PROOF STEP]
by (coinduction arbitrary: p) (auto)
[PROOF STATE]
proof (state)
this:
pred_stream P (p ## trace (smap f (siterate (\<lambda>p. execute (f p) p) p)) p)

goal (1 subgoal):
 1. stream_all2 Q (p ## trace (smap f (siterate (\<lambda>p. execute (f p) p) p)) p) (smap f (siterate (\<lambda>p. execute (f p) p) p))
[PROOF STEP]
show "stream_all2 Q (p ## trace (?r p) p) (?r p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stream_all2 Q (p ## trace (smap f (siterate (\<lambda>p. execute (f p) p) p)) p) (smap f (siterate (\<lambda>p. execute (f p) p) p))
[PROOF STEP]
using assms(1) 1
[PROOF STATE]
proof (prove)
using this:
P p
P ?p \<Longrightarrow> enabled (f ?p) ?p
P ?p \<Longrightarrow> P (execute (f ?p) ?p)
P ?p \<Longrightarrow> Q ?p (f ?p)

goal (1 subgoal):
 1. stream_all2 Q (p ## trace (smap f (siterate (\<lambda>p. execute (f p) p) p)) p) (smap f (siterate (\<lambda>p. execute (f p) p) p))
[PROOF STEP]
by (coinduction arbitrary: p) (auto)
[PROOF STATE]
proof (state)
this:
stream_all2 Q (p ## trace (smap f (siterate (\<lambda>p. execute (f p) p) p)) p) (smap f (siterate (\<lambda>p. execute (f p) p) p))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma recurring_condition:
      assumes "P p" "\<And> p. P p \<Longrightarrow> \<exists> r. r \<noteq> [] \<and> path r p \<and> P (target r p)"
      obtains r
      where "run r p" "infs P (p ## trace r p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; infs P (p ## trace r p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; infs P (p ## trace r p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain f where 1: "f p \<noteq> []" "path (f p) p" "P (target (f p) p)" if "P p" for p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<And>p. P p \<Longrightarrow> f p \<noteq> []; \<And>p. P p \<Longrightarrow> path (f p) p; \<And>p. P p \<Longrightarrow> P (target (f p) p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
P ?p \<Longrightarrow> \<exists>r. r \<noteq> [] \<and> path r ?p \<and> P (target r ?p)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<And>p. P p \<Longrightarrow> f p \<noteq> []; \<And>p. P p \<Longrightarrow> path (f p) p; \<And>p. P p \<Longrightarrow> P (target (f p) p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
P ?p \<Longrightarrow> f ?p \<noteq> []
P ?p \<Longrightarrow> path (f ?p) ?p
P ?p \<Longrightarrow> P (target (f ?p) ?p)

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; infs P (p ## trace r p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?g = "\<lambda> p. target (f p) p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; infs P (p ## trace r p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?r = "\<lambda> p. flat (smap f (siterate ?g p))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; infs P (p ## trace r p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have 2: "?r p = f p @- ?r (?g p)" if "P p" for p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. flat (smap f (siterate (\<lambda>p. target (f p) p) p)) = f p @- flat (smap f (siterate (\<lambda>p. target (f p) p) (target (f p) p)))
[PROOF STEP]
using that 1(1)
[PROOF STATE]
proof (prove)
using this:
P p
P ?p \<Longrightarrow> f ?p \<noteq> []

goal (1 subgoal):
 1. flat (smap f (siterate (\<lambda>p. target (f p) p) p)) = f p @- flat (smap f (siterate (\<lambda>p. target (f p) p) (target (f p) p)))
[PROOF STEP]
by (simp add: flat_unfold)
[PROOF STATE]
proof (state)
this:
P ?p \<Longrightarrow> flat (smap f (siterate (\<lambda>p. target (f p) p) ?p)) = f ?p @- flat (smap f (siterate (\<lambda>p. target (f p) p) (target (f ?p) ?p)))

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; infs P (p ## trace r p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. run ?r p
 2. infs P (p ## trace ?r p)
[PROOF STEP]
show "run (?r p) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run (flat (smap f (siterate (\<lambda>p. target (f p) p) p))) p
[PROOF STEP]
using assms(1) 1 2
[PROOF STATE]
proof (prove)
using this:
P p
P ?p \<Longrightarrow> f ?p \<noteq> []
P ?p \<Longrightarrow> path (f ?p) ?p
P ?p \<Longrightarrow> P (target (f ?p) ?p)
P ?p \<Longrightarrow> flat (smap f (siterate (\<lambda>p. target (f p) p) ?p)) = f ?p @- flat (smap f (siterate (\<lambda>p. target (f p) p) (target (f ?p) ?p)))

goal (1 subgoal):
 1. run (flat (smap f (siterate (\<lambda>p. target (f p) p) p))) p
[PROOF STEP]
by (coinduction arbitrary: p rule: run_coinduct_shift) (blast)
[PROOF STATE]
proof (state)
this:
run (flat (smap f (siterate (\<lambda>p. target (f p) p) p))) p

goal (1 subgoal):
 1. infs P (p ## trace (flat (smap f (siterate (\<lambda>p. target (f p) p) p))) p)
[PROOF STEP]
show "infs P (p ## trace (?r p) p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infs P (p ## trace (flat (smap f (siterate (\<lambda>p. target (f p) p) p))) p)
[PROOF STEP]
using assms(1) 1 2
[PROOF STATE]
proof (prove)
using this:
P p
P ?p \<Longrightarrow> f ?p \<noteq> []
P ?p \<Longrightarrow> path (f ?p) ?p
P ?p \<Longrightarrow> P (target (f ?p) ?p)
P ?p \<Longrightarrow> flat (smap f (siterate (\<lambda>p. target (f p) p) ?p)) = f ?p @- flat (smap f (siterate (\<lambda>p. target (f p) p) (target (f ?p) ?p)))

goal (1 subgoal):
 1. infs P (p ## trace (flat (smap f (siterate (\<lambda>p. target (f p) p) p))) p)
[PROOF STEP]
by (coinduction arbitrary: p rule: infs_sscan_coinduct) (blast)
[PROOF STATE]
proof (state)
this:
infs P (p ## trace (flat (smap f (siterate (\<lambda>p. target (f p) p) p))) p)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma invariant_run_index:
      assumes "P n p" "\<And> n p. P n p \<Longrightarrow> \<exists> a. enabled a p \<and> P (Suc n) (execute a p) \<and> Q n p a"
      obtains r
      where
        "run r p"
        "\<And> i. P (n + i) (target (stake i r) p)"
        "\<And> i. Q (n + i) (target (stake i r) p) (r !! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; \<And>i. P (n + i) (target (stake i r) p); \<And>i. Q (n + i) (target (stake i r) p) (r !! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; \<And>i. P (n + i) (target (stake i r) p); \<And>i. Q (n + i) (target (stake i r) p) (r !! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define s where "s \<equiv> (n, p)"
[PROOF STATE]
proof (state)
this:
s \<equiv> (n, p)

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; \<And>i. P (n + i) (target (stake i r) p); \<And>i. Q (n + i) (target (stake i r) p) (r !! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have 1: "case_prod P s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case s of (x, xa) \<Rightarrow> P x xa
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
P n p

goal (1 subgoal):
 1. case s of (x, xa) \<Rightarrow> P x xa
[PROOF STEP]
unfolding s_def
[PROOF STATE]
proof (prove)
using this:
P n p

goal (1 subgoal):
 1. case (n, p) of (x, xa) \<Rightarrow> P x xa
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
case s of (x, xa) \<Rightarrow> P x xa

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; \<And>i. P (n + i) (target (stake i r) p); \<And>i. Q (n + i) (target (stake i r) p) (r !! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain f where 2:
        "\<And> n p. P n p \<Longrightarrow> enabled (f n p) p"
        "\<And> n p. P n p \<Longrightarrow> P (Suc n) (execute (f n p) p)"
        "\<And> n p. P n p \<Longrightarrow> Q n p (f n p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<And>n p. P n p \<Longrightarrow> enabled (f n p) p; \<And>n p. P n p \<Longrightarrow> P (Suc n) (execute (f n p) p); \<And>n p. P n p \<Longrightarrow> Q n p (f n p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
P ?n ?p \<Longrightarrow> \<exists>a. enabled a ?p \<and> P (Suc ?n) (execute a ?p) \<and> Q ?n ?p a

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<And>n p. P n p \<Longrightarrow> enabled (f n p) p; \<And>n p. P n p \<Longrightarrow> P (Suc n) (execute (f n p) p); \<And>n p. P n p \<Longrightarrow> Q n p (f n p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
P ?n ?p \<Longrightarrow> enabled (f ?n ?p) ?p
P ?n ?p \<Longrightarrow> P (Suc ?n) (execute (f ?n ?p) ?p)
P ?n ?p \<Longrightarrow> Q ?n ?p (f ?n ?p)

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; \<And>i. P (n + i) (target (stake i r) p); \<And>i. Q (n + i) (target (stake i r) p) (r !! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define g where "g \<equiv> \<lambda> (n, p). (Suc n, execute (f n p) p)"
[PROOF STATE]
proof (state)
this:
g \<equiv> \<lambda>(n, p). (Suc n, execute (f n p) p)

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; \<And>i. P (n + i) (target (stake i r) p); \<And>i. Q (n + i) (target (stake i r) p) (r !! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?r = "smap (case_prod f) (siterate g s)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; \<And>i. P (n + i) (target (stake i r) p); \<And>i. Q (n + i) (target (stake i r) p) (r !! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have 3: "run ?r (snd s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run (smap (\<lambda>(x, y). f x y) (siterate g s)) (snd s)
[PROOF STEP]
using 1 2(1, 2)
[PROOF STATE]
proof (prove)
using this:
case s of (x, xa) \<Rightarrow> P x xa
P ?n ?p \<Longrightarrow> enabled (f ?n ?p) ?p
P ?n ?p \<Longrightarrow> P (Suc ?n) (execute (f ?n ?p) ?p)

goal (1 subgoal):
 1. run (smap (\<lambda>(x, y). f x y) (siterate g s)) (snd s)
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
using this:
case s of (x, xa) \<Rightarrow> P x xa
P ?n ?p \<Longrightarrow> enabled (f ?n ?p) ?p
P ?n ?p \<Longrightarrow> P (Suc ?n) (execute (f ?n ?p) ?p)

goal (1 subgoal):
 1. run (smap (\<lambda>(x, y). f x y) (siterate (\<lambda>(n, p). (Suc n, execute (f n p) p)) s)) (snd s)
[PROOF STEP]
by (coinduction arbitrary: s) (auto)
[PROOF STATE]
proof (state)
this:
run (smap (\<lambda>(x, y). f x y) (siterate g s)) (snd s)

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; \<And>i. P (n + i) (target (stake i r) p); \<And>i. Q (n + i) (target (stake i r) p) (r !! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have 4: "case_prod P (compow k g s)" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case (g ^^ k) s of (x, xa) \<Rightarrow> P x xa
[PROOF STEP]
using 1 2(2)
[PROOF STATE]
proof (prove)
using this:
case s of (x, xa) \<Rightarrow> P x xa
P ?n ?p \<Longrightarrow> P (Suc ?n) (execute (f ?n ?p) ?p)

goal (1 subgoal):
 1. case (g ^^ k) s of (x, xa) \<Rightarrow> P x xa
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
using this:
case s of (x, xa) \<Rightarrow> P x xa
P ?n ?p \<Longrightarrow> P (Suc ?n) (execute (f ?n ?p) ?p)

goal (1 subgoal):
 1. case ((\<lambda>(n, p). (Suc n, execute (f n p) p)) ^^ k) s of (x, xa) \<Rightarrow> P x xa
[PROOF STEP]
by (induct k) (auto)
[PROOF STATE]
proof (state)
this:
case (g ^^ ?k) s of (x, xa) \<Rightarrow> P x xa

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; \<And>i. P (n + i) (target (stake i r) p); \<And>i. Q (n + i) (target (stake i r) p) (r !! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have 5: "case_prod Q (compow k g s) (?r !! k)" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (g ^^ k) s of (x, xa) \<Rightarrow> Q x xa) (smap (\<lambda>(x, y). f x y) (siterate g s) !! k)
[PROOF STEP]
using 2(3) 4
[PROOF STATE]
proof (prove)
using this:
P ?n ?p \<Longrightarrow> Q ?n ?p (f ?n ?p)
case (g ^^ ?k) s of (x, xa) \<Rightarrow> P x xa

goal (1 subgoal):
 1. (case (g ^^ k) s of (x, xa) \<Rightarrow> Q x xa) (smap (\<lambda>(x, y). f x y) (siterate g s) !! k)
[PROOF STEP]
by (simp add: case_prod_beta)
[PROOF STATE]
proof (state)
this:
(case (g ^^ ?k) s of (x, xa) \<Rightarrow> Q x xa) (smap (\<lambda>(x, y). f x y) (siterate g s) !! ?k)

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; \<And>i. P (n + i) (target (stake i r) p); \<And>i. Q (n + i) (target (stake i r) p) (r !! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have 6: "compow k g (n, p) = (n + k, target (stake k ?r) p)" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g ^^ k) (n, p) = (n + k, target (stake k (smap (\<lambda>(x, y). f x y) (siterate g s))) p)
[PROOF STEP]
unfolding s_def g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>(n, p). (Suc n, execute (f n p) p)) ^^ k) (n, p) = (n + k, target (stake k (smap (\<lambda>(x, y). f x y) (siterate (\<lambda>(n, p). (Suc n, execute (f n p) p)) (n, p)))) p)
[PROOF STEP]
by (induct k) (auto simp add: stake_Suc simp del: stake.simps(2))
[PROOF STATE]
proof (state)
this:
(g ^^ ?k) (n, p) = (n + ?k, target (stake ?k (smap (\<lambda>(x, y). f x y) (siterate g s))) p)

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>run r p; \<And>i. P (n + i) (target (stake i r) p); \<And>i. Q (n + i) (target (stake i r) p) (r !! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that 3 4 5
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>run ?r p; \<And>i. P (n + i) (target (stake i ?r) p); \<And>i. Q (n + i) (target (stake i ?r) p) (?r !! i)\<rbrakk> \<Longrightarrow> thesis
run (smap (\<lambda>(x, y). f x y) (siterate g s)) (snd s)
case (g ^^ ?k) s of (x, xa) \<Rightarrow> P x xa
(case (g ^^ ?k) s of (x, xa) \<Rightarrow> Q x xa) (smap (\<lambda>(x, y). f x y) (siterate g s) !! ?k)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
unfolding s_def 6
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>run ?r p; \<And>i. P (n + i) (target (stake i ?r) p); \<And>i. Q (n + i) (target (stake i ?r) p) (?r !! i)\<rbrakk> \<Longrightarrow> thesis
run (smap (\<lambda>(x, y). f x y) (siterate g (n, p))) (snd (n, p))
case (n + ?k, target (stake ?k (smap (\<lambda>(x, y). f x y) (siterate g (n, p)))) p) of (x, xa) \<Rightarrow> P x xa
(case (n + ?k, target (stake ?k (smap (\<lambda>(x, y). f x y) (siterate g (n, p)))) p) of (x, xa) \<Rightarrow> Q x xa) (smap (\<lambda>(x, y). f x y) (siterate g (n, p)) !! ?k)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma koenig:
      assumes "infinite (reachable p)"
      assumes "\<And> q. q \<in> reachable p \<Longrightarrow> finite (successors q)"
      obtains r
      where "run r p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r. run r p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (rule invariant_run[where ?P = "\<lambda> q. q \<in> reachable p \<and> infinite (reachable q)"])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (\<And>r. run r p \<Longrightarrow> thesis) \<Longrightarrow> ?p2 \<in> reachable p \<and> infinite (reachable ?p2)
 2. \<And>pa. \<lbrakk>\<And>r. run r p \<Longrightarrow> thesis; pa \<in> reachable p \<and> infinite (reachable pa)\<rbrakk> \<Longrightarrow> \<exists>a. enabled a pa \<and> (execute a pa \<in> reachable p \<and> infinite (reachable (execute a pa))) \<and> ?Q2 pa a
 3. \<And>r. \<lbrakk>\<And>r. run r p \<Longrightarrow> thesis; run r ?p2; pred_stream (\<lambda>q. q \<in> reachable p \<and> infinite (reachable q)) (?p2 ## trace r ?p2); stream_all2 ?Q2 (?p2 ## trace r ?p2) r\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show "p \<in> reachable p \<and> infinite (reachable p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> reachable p \<and> infinite (reachable p)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
infinite (reachable p)

goal (1 subgoal):
 1. p \<in> reachable p \<and> infinite (reachable p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<in> reachable p \<and> infinite (reachable p)

goal (2 subgoals):
 1. \<And>pa. \<lbrakk>\<And>r. run r p \<Longrightarrow> thesis; pa \<in> reachable p \<and> infinite (reachable pa)\<rbrakk> \<Longrightarrow> \<exists>a. enabled a pa \<and> (execute a pa \<in> reachable p \<and> infinite (reachable (execute a pa))) \<and> ?Q2 pa a
 2. \<And>r. \<lbrakk>\<And>r. run r p \<Longrightarrow> thesis; run r p; pred_stream (\<lambda>q. q \<in> reachable p \<and> infinite (reachable q)) (p ## trace r p); stream_all2 ?Q2 (p ## trace r p) r\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>\<And>r. run r p \<Longrightarrow> thesis; pa \<in> reachable p \<and> infinite (reachable pa)\<rbrakk> \<Longrightarrow> \<exists>a. enabled a pa \<and> (execute a pa \<in> reachable p \<and> infinite (reachable (execute a pa))) \<and> ?Q2 pa a
 2. \<And>r. \<lbrakk>\<And>r. run r p \<Longrightarrow> thesis; run r p; pred_stream (\<lambda>q. q \<in> reachable p \<and> infinite (reachable q)) (p ## trace r p); stream_all2 ?Q2 (p ## trace r p) r\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
fix q
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>\<And>r. run r p \<Longrightarrow> thesis; pa \<in> reachable p \<and> infinite (reachable pa)\<rbrakk> \<Longrightarrow> \<exists>a. enabled a pa \<and> (execute a pa \<in> reachable p \<and> infinite (reachable (execute a pa))) \<and> ?Q2 pa a
 2. \<And>r. \<lbrakk>\<And>r. run r p \<Longrightarrow> thesis; run r p; pred_stream (\<lambda>q. q \<in> reachable p \<and> infinite (reachable q)) (p ## trace r p); stream_all2 ?Q2 (p ## trace r p) r\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume 1: "q \<in> reachable p \<and> infinite (reachable q)"
[PROOF STATE]
proof (state)
this:
q \<in> reachable p \<and> infinite (reachable q)

goal (2 subgoals):
 1. \<And>pa. \<lbrakk>\<And>r. run r p \<Longrightarrow> thesis; pa \<in> reachable p \<and> infinite (reachable pa)\<rbrakk> \<Longrightarrow> \<exists>a. enabled a pa \<and> (execute a pa \<in> reachable p \<and> infinite (reachable (execute a pa))) \<and> ?Q2 pa a
 2. \<And>r. \<lbrakk>\<And>r. run r p \<Longrightarrow> thesis; run r p; pred_stream (\<lambda>q. q \<in> reachable p \<and> infinite (reachable q)) (p ## trace r p); stream_all2 ?Q2 (p ## trace r p) r\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have 2: "finite (successors q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (successors q)
[PROOF STEP]
using assms(2) 1
[PROOF STATE]
proof (prove)
using this:
?q \<in> reachable p \<Longrightarrow> finite (successors ?q)
q \<in> reachable p \<and> infinite (reachable q)

goal (1 subgoal):
 1. finite (successors q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (successors q)

goal (2 subgoals):
 1. \<And>pa. \<lbrakk>\<And>r. run r p \<Longrightarrow> thesis; pa \<in> reachable p \<and> infinite (reachable pa)\<rbrakk> \<Longrightarrow> \<exists>a. enabled a pa \<and> (execute a pa \<in> reachable p \<and> infinite (reachable (execute a pa))) \<and> ?Q2 pa a
 2. \<And>r. \<lbrakk>\<And>r. run r p \<Longrightarrow> thesis; run r p; pred_stream (\<lambda>q. q \<in> reachable p \<and> infinite (reachable q)) (p ## trace r p); stream_all2 ?Q2 (p ## trace r p) r\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have 3: "infinite (insert q (\<Union>(reachable ` (successors q))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (insert q (\<Union> (reachable ` successors q)))
[PROOF STEP]
using reachable_step 1
[PROOF STATE]
proof (prove)
using this:
reachable ?p = insert ?p (\<Union> (reachable ` successors ?p))
q \<in> reachable p \<and> infinite (reachable q)

goal (1 subgoal):
 1. infinite (insert q (\<Union> (reachable ` successors q)))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
infinite (insert q (\<Union> (reachable ` successors q)))

goal (2 subgoals):
 1. \<And>pa. \<lbrakk>\<And>r. run r p \<Longrightarrow> thesis; pa \<in> reachable p \<and> infinite (reachable pa)\<rbrakk> \<Longrightarrow> \<exists>a. enabled a pa \<and> (execute a pa \<in> reachable p \<and> infinite (reachable (execute a pa))) \<and> ?Q2 pa a
 2. \<And>r. \<lbrakk>\<And>r. run r p \<Longrightarrow> thesis; run r p; pred_stream (\<lambda>q. q \<in> reachable p \<and> infinite (reachable q)) (p ## trace r p); stream_all2 ?Q2 (p ## trace r p) r\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
obtain s where 4: "s \<in> successors q" "infinite (reachable s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> successors q; infinite (reachable s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 2 3
[PROOF STATE]
proof (prove)
using this:
finite (successors q)
infinite (insert q (\<Union> (reachable ` successors q)))

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> successors q; infinite (reachable s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<in> successors q
infinite (reachable s)

goal (2 subgoals):
 1. \<And>pa. \<lbrakk>\<And>r. run r p \<Longrightarrow> thesis; pa \<in> reachable p \<and> infinite (reachable pa)\<rbrakk> \<Longrightarrow> \<exists>a. enabled a pa \<and> (execute a pa \<in> reachable p \<and> infinite (reachable (execute a pa))) \<and> ?Q2 pa a
 2. \<And>r. \<lbrakk>\<And>r. run r p \<Longrightarrow> thesis; run r p; pred_stream (\<lambda>q. q \<in> reachable p \<and> infinite (reachable q)) (p ## trace r p); stream_all2 ?Q2 (p ## trace r p) r\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show "\<exists> a. enabled a q \<and> (execute a q \<in> reachable p \<and> infinite (reachable (execute a q))) \<and> True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. enabled a q \<and> (execute a q \<in> reachable p \<and> infinite (reachable (execute a q))) \<and> True
[PROOF STEP]
using 1 4
[PROOF STATE]
proof (prove)
using this:
q \<in> reachable p \<and> infinite (reachable q)
s \<in> successors q
infinite (reachable s)

goal (1 subgoal):
 1. \<exists>a. enabled a q \<and> (execute a q \<in> reachable p \<and> infinite (reachable (execute a q))) \<and> True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a. enabled a q \<and> (execute a q \<in> reachable p \<and> infinite (reachable (execute a q))) \<and> True

goal (1 subgoal):
 1. \<And>r. \<lbrakk>\<And>r. run r p \<Longrightarrow> thesis; run r p; pred_stream (\<lambda>q. q \<in> reachable p \<and> infinite (reachable q)) (p ## trace r p); stream_all2 (\<lambda>p a. True) (p ## trace r p) r\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
qed


[STATEMENT]
lemma splay_code: "splay (x::_::linorder) t = (case t of Leaf \<Rightarrow> Leaf |
  Node al a ar \<Rightarrow> (case cmp x (fst a) of
    EQ \<Rightarrow> t |
    LT \<Rightarrow> (case al of
      Leaf \<Rightarrow> t |
      Node bl b br \<Rightarrow> (case cmp x (fst b) of
        EQ \<Rightarrow> Node bl b (Node br a ar) |
        LT \<Rightarrow> if bl = Leaf then Node bl b (Node br a ar)
              else case splay x bl of
                Node bll y blr \<Rightarrow> Node bll y (Node blr b (Node br a ar)) |
        GT \<Rightarrow> if br = Leaf then Node bl b (Node br a ar)
              else case splay x br of
                Node brl y brr \<Rightarrow> Node (Node bl b brl) y (Node brr a ar))) |
    GT \<Rightarrow> (case ar of
      Leaf \<Rightarrow> t |
      Node bl b br \<Rightarrow> (case cmp x (fst b) of
        EQ \<Rightarrow> Node (Node al a bl) b br |
        LT \<Rightarrow> if bl = Leaf then Node (Node al a bl) b br
              else case splay x bl of
                Node bll y blr \<Rightarrow> Node (Node al a bll) y (Node blr b br) |
        GT \<Rightarrow> if br=Leaf then Node (Node al a bl) b br
              else case splay x br of
                Node bll y blr \<Rightarrow> Node (Node (Node al a bl) b bll) y blr))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Splay_Map.splay x t = (case t of \<langle>\<rangle> \<Rightarrow> \<langle>\<rangle> | \<langle>al, a, ar\<rangle> \<Rightarrow> case cmp x (fst a) of LT \<Rightarrow> case al of \<langle>\<rangle> \<Rightarrow> t | \<langle>bl, b, br\<rangle> \<Rightarrow> case cmp x (fst b) of LT \<Rightarrow> if bl = \<langle>\<rangle> then \<langle>bl, b, \<langle>br, a, ar\<rangle>\<rangle> else case Splay_Map.splay x bl of \<langle>bll, y, blr\<rangle> \<Rightarrow> \<langle>bll, y, \<langle>blr, b, \<langle>br, a, ar\<rangle>\<rangle>\<rangle> | EQ \<Rightarrow> \<langle>bl, b, \<langle>br, a, ar\<rangle>\<rangle> | GT \<Rightarrow> if br = \<langle>\<rangle> then \<langle>bl, b, \<langle>br, a, ar\<rangle>\<rangle> else case Splay_Map.splay x br of \<langle>brl, y, brr\<rangle> \<Rightarrow> \<langle>\<langle>bl, b, brl\<rangle>, y, \<langle>brr, a, ar\<rangle>\<rangle> | EQ \<Rightarrow> t | GT \<Rightarrow> case ar of \<langle>\<rangle> \<Rightarrow> t | \<langle>bl, b, br\<rangle> \<Rightarrow> case cmp x (fst b) of LT \<Rightarrow> if bl = \<langle>\<rangle> then \<langle>\<langle>al, a, bl\<rangle>, b, br\<rangle> else case Splay_Map.splay x bl of \<langle>bll, y, blr\<rangle> \<Rightarrow> \<langle>\<langle>al, a, bll\<rangle>, y, \<langle>blr, b, br\<rangle>\<rangle> | EQ \<Rightarrow> \<langle>\<langle>al, a, bl\<rangle>, b, br\<rangle> | GT \<Rightarrow> if br = \<langle>\<rangle> then \<langle>\<langle>al, a, bl\<rangle>, b, br\<rangle> else case Splay_Map.splay x br of \<langle>bll, y, blr\<rangle> \<Rightarrow> \<langle>\<langle>\<langle>al, a, bl\<rangle>, b, bll\<rangle>, y, blr\<rangle>)
[PROOF STEP]
by(auto split!: tree.split)


[STATEMENT]
lemma splay_Leaf_iff: "(splay x t = Leaf) = (t = Leaf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Splay_Map.splay x t = \<langle>\<rangle>) = (t = \<langle>\<rangle>)
[PROOF STEP]
by(induction x t rule: splay.induct) (auto split: tree.splits)


[STATEMENT]
lemma splay_map_of_inorder:
  "splay x t = Node l a r \<Longrightarrow> sorted1(inorder t) \<Longrightarrow>
   map_of (inorder t) x = (if x = fst a then Some(snd a) else None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Splay_Map.splay x t = \<langle>l, a, r\<rangle>; sorted1 (inorder t)\<rbrakk> \<Longrightarrow> AList_Upd_Del.map_of (inorder t) x = (if x = fst a then Some (snd a) else None)
[PROOF STEP]
by(induction x t arbitrary: l a r rule: splay.induct)
  (auto simp: map_of_simps splay_Leaf_iff split: tree.splits)


[STATEMENT]
lemma lookup_eq:
  "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted1 (inorder t) \<Longrightarrow> lookup t x = AList_Upd_Del.map_of (inorder t) x
[PROOF STEP]
by(auto simp: lookup_def splay_Leaf_iff splay_map_of_inorder split: tree.split)


[STATEMENT]
lemma inorder_splay: "inorder(splay x t) = inorder t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inorder (Splay_Map.splay x t) = inorder t
[PROOF STEP]
by(induction x t rule: splay.induct)
  (auto simp: neq_Leaf_iff split: tree.split)


[STATEMENT]
lemma sorted_splay:
  "sorted1(inorder t) \<Longrightarrow> splay x t = Node l a r \<Longrightarrow>
  sorted(map fst (inorder l) @ x # map fst (inorder r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sorted1 (inorder t); Splay_Map.splay x t = \<langle>l, a, r\<rangle>\<rbrakk> \<Longrightarrow> Sorted_Less.sorted (map fst (inorder l) @ x # map fst (inorder r))
[PROOF STEP]
unfolding inorder_splay[of x t, symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sorted1 (inorder (Splay_Map.splay x t)); Splay_Map.splay x t = \<langle>l, a, r\<rangle>\<rbrakk> \<Longrightarrow> Sorted_Less.sorted (map fst (inorder l) @ x # map fst (inorder r))
[PROOF STEP]
by(induction x t arbitrary: l a r rule: splay.induct)
  (auto simp: sorted_lems sorted_Cons_le sorted_snoc_le splay_Leaf_iff split: tree.splits)


[STATEMENT]
lemma inorder_update_splay:
  "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted1 (inorder t) \<Longrightarrow> inorder (update x y t) = upd_list x y (inorder t)
[PROOF STEP]
using inorder_splay[of x t, symmetric] sorted_splay[of t x]
[PROOF STATE]
proof (prove)
using this:
inorder t = inorder (Splay_Map.splay x t)
\<lbrakk>sorted1 (inorder t); Splay_Map.splay x t = \<langle>?l, ?a, ?r\<rangle>\<rbrakk> \<Longrightarrow> Sorted_Less.sorted (map fst (inorder ?l) @ x # map fst (inorder ?r))

goal (1 subgoal):
 1. sorted1 (inorder t) \<Longrightarrow> inorder (update x y t) = upd_list x y (inorder t)
[PROOF STEP]
by(auto simp: upd_list_simps upd_list_Cons upd_list_snoc neq_Leaf_iff split: tree.split)


[STATEMENT]
lemma inorder_splay_maxD:
  "splay_max t = Node l a r \<Longrightarrow> sorted1(inorder t) \<Longrightarrow>
  inorder l @ [a] = inorder t \<and> r = Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>splay_max t = \<langle>l, a, r\<rangle>; sorted1 (inorder t)\<rbrakk> \<Longrightarrow> inorder l @ [a] = inorder t \<and> r = \<langle>\<rangle>
[PROOF STEP]
by(induction t arbitrary: l a r rule: splay_max.induct)
  (auto simp: sorted_lems split: tree.splits if_splits)


[STATEMENT]
lemma inorder_delete_splay:
  "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted1 (inorder t) \<Longrightarrow> inorder (Splay_Map.delete x t) = AList_Upd_Del.del_list x (inorder t)
[PROOF STEP]
using inorder_splay[of x t, symmetric] sorted_splay[of t x]
[PROOF STATE]
proof (prove)
using this:
inorder t = inorder (Splay_Map.splay x t)
\<lbrakk>sorted1 (inorder t); Splay_Map.splay x t = \<langle>?l, ?a, ?r\<rangle>\<rbrakk> \<Longrightarrow> Sorted_Less.sorted (map fst (inorder ?l) @ x # map fst (inorder ?r))

goal (1 subgoal):
 1. sorted1 (inorder t) \<Longrightarrow> inorder (Splay_Map.delete x t) = AList_Upd_Del.del_list x (inorder t)
[PROOF STEP]
by (auto simp: del_list_simps del_list_sorted_app delete_def del_list_notin_Cons inorder_splay_maxD
  split: tree.splits)


[STATEMENT]
lemma wf_J1_mdecl[simp]:
  "wf_J1_mdecl P C (M,Ts,T,body) \<equiv>
    ((\<exists>T'. P,Class C#Ts \<turnstile>1 body :: T' \<and> P \<turnstile> T' \<le> T) \<and>
     \<D> body \<lfloor>{..size Ts}\<rfloor> \<and> \<B> body (size Ts + 1)) \<and> syncvars body"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_J1_mdecl P C (M, Ts, T, body) \<equiv> ((\<exists>T'. P,Class C # Ts \<turnstile>1 body :: T' \<and> P \<turnstile> T' \<le> T) \<and> \<D> body \<lfloor>{..length Ts}\<rfloor> \<and> \<B> body (length Ts + 1)) \<and> syncvars body
[PROOF STEP]
by (simp add:wf_J1_mdecl_def)


[STATEMENT]
lemma abort_parametric [transfer_rule]: includes lifting_syntax shows (* Move to Isabelle distribution *)
  "((=) ===> ((=) ===> A) ===> A) Code.abort Code.abort"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> ((=) ===> A) ===> A) Code.abort Code.abort
[PROOF STEP]
unfolding Code.abort_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> ((=) ===> A) ===> A) (\<lambda>uu f. f ()) (\<lambda>uu f. f ())
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma uprod_eq_simps [simp, code]:
  "uprod_eq eq (Upair a b) (Upair c d) \<longleftrightarrow>
   Rep_equal eq a c \<and> Rep_equal eq b d \<or> Rep_equal eq b c \<and> Rep_equal eq a d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uprod_eq eq (Upair a b) (Upair c d) = (Rep_equal eq a c \<and> Rep_equal eq b d \<or> Rep_equal eq b c \<and> Rep_equal eq a d)
[PROOF STEP]
supply Upair.transfer[transfer_rule]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uprod_eq eq (Upair a b) (Upair c d) = (Rep_equal eq a c \<and> Rep_equal eq b d \<or> Rep_equal eq b c \<and> Rep_equal eq a d)
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma uprod_compare_simps [simp, code]:
  "uprod_compare compare (Upair a b) (Upair c d) =
   (let (x, y) = case Rep_compare compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a);
        (x', y') = case Rep_compare compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c)
    in case Rep_compare compare x x' of Eq \<Rightarrow> Rep_compare compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt)"
  for compare
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uprod_compare compare (Upair a b) (Upair c d) = (let (x, y) = case Rep_compare compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case Rep_compare compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case Rep_compare compare x x' of Eq \<Rightarrow> Rep_compare compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt)
[PROOF STEP]
supply Upair.transfer[transfer_rule]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uprod_compare compare (Upair a b) (Upair c d) = (let (x, y) = case Rep_compare compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case Rep_compare compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case Rep_compare compare x x' of Eq \<Rightarrow> Rep_compare compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt)
[PROOF STEP]
by transfer simp