[STATEMENT]
lemma update_dj_by_update:
  assumes "map_update \<alpha> invar update"
  shows "map_update_dj \<alpha> invar update"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_update_dj \<alpha> invar update
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_update_dj \<alpha> invar update
[PROOF STEP]
interpret map_update \<alpha> invar update
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_update \<alpha> invar update
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_update_dj \<alpha> invar update
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_update_dj \<alpha> invar update
[PROOF STEP]
apply (unfold_locales)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m k v. \<lbrakk>invar m; k \<notin> dom (\<alpha> m)\<rbrakk> \<Longrightarrow> \<alpha> (update k v m) = \<alpha> m(k \<mapsto> v)
 2. \<And>m k v. \<lbrakk>invar m; k \<notin> dom (\<alpha> m)\<rbrakk> \<Longrightarrow> invar (update k v m)
[PROOF STEP]
apply (auto simp add: update_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
map_update_dj \<alpha> invar update

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_iterator_linord_is_it:
  "map_iterator_linord m it \<Longrightarrow> map_iterator m it"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_iterator_linord m it \<Longrightarrow> map_iterator m it
[PROOF STEP]
unfolding set_iterator_def set_iterator_map_linord_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_iterator_genord m it (\<lambda>(k, uu_) (k', uu_). k \<le> k') \<Longrightarrow> map_iterator_genord m it (\<lambda>_ _. True)
[PROOF STEP]
apply (erule set_iterator_genord.set_iterator_weaken_R)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> map_to_set it; y \<in> map_to_set it; (case x of (k, uu_) \<Rightarrow> \<lambda>(k', uu_). k \<le> k') y\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
..


[STATEMENT]
lemma map_rev_iterator_linord_is_it:
  "map_iterator_rev_linord m it \<Longrightarrow> map_iterator m it"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_iterator_rev_linord m it \<Longrightarrow> map_iterator m it
[PROOF STEP]
unfolding set_iterator_def set_iterator_map_rev_linord_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_iterator_genord m it (\<lambda>(k, uu_) (k', uu_). k' \<le> k) \<Longrightarrow> map_iterator_genord m it (\<lambda>_ _. True)
[PROOF STEP]
apply (erule set_iterator_genord.set_iterator_weaken_R)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> map_to_set it; y \<in> map_to_set it; (case x of (k, uu_) \<Rightarrow> \<lambda>(k', uu_). k' \<le> k) y\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
..


[STATEMENT]
lemma g_add_impl: "map_add \<alpha> invar g_add"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MapSpec.map_add \<alpha> invar g_add
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m1 m2. \<lbrakk>invar m1; invar m2\<rbrakk> \<Longrightarrow> \<alpha> (g_add m1 m2) = \<alpha> m1 ++ \<alpha> m2
 2. \<And>m1 m2. \<lbrakk>invar m1; invar m2\<rbrakk> \<Longrightarrow> invar (g_add m1 m2)
[PROOF STEP]
fix m1 m2
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m1 m2. \<lbrakk>invar m1; invar m2\<rbrakk> \<Longrightarrow> \<alpha> (g_add m1 m2) = \<alpha> m1 ++ \<alpha> m2
 2. \<And>m1 m2. \<lbrakk>invar m1; invar m2\<rbrakk> \<Longrightarrow> invar (g_add m1 m2)
[PROOF STEP]
assume "invar m1" "invar m2"
[PROOF STATE]
proof (state)
this:
invar m1
invar m2

goal (2 subgoals):
 1. \<And>m1 m2. \<lbrakk>invar m1; invar m2\<rbrakk> \<Longrightarrow> \<alpha> (g_add m1 m2) = \<alpha> m1 ++ \<alpha> m2
 2. \<And>m1 m2. \<lbrakk>invar m1; invar m2\<rbrakk> \<Longrightarrow> invar (g_add m1 m2)
[PROOF STEP]
have A: "g_add m1 m2 = iterate_add_to_map m1 update (iteratei m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g_add m1 m2 = iterate_add_to_map m1 update (iteratei m2)
[PROOF STEP]
unfolding g_add_def iterate_add_to_map_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iterate m2 (\<lambda>(x, y). update x y) m1 = iterate m2 (\<lambda>(x, y). update x y) m1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g_add m1 m2 = iterate_add_to_map m1 update (iteratei m2)

goal (2 subgoals):
 1. \<And>m1 m2. \<lbrakk>invar m1; invar m2\<rbrakk> \<Longrightarrow> \<alpha> (g_add m1 m2) = \<alpha> m1 ++ \<alpha> m2
 2. \<And>m1 m2. \<lbrakk>invar m1; invar m2\<rbrakk> \<Longrightarrow> invar (g_add m1 m2)
[PROOF STEP]
have "\<alpha> (g_add m1 m2) = \<alpha> m1 ++ \<alpha> m2 \<and> invar (g_add m1 m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (g_add m1 m2) = \<alpha> m1 ++ \<alpha> m2 \<and> invar (g_add m1 m2)
[PROOF STEP]
unfolding A
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (iterate_add_to_map m1 update (iteratei m2)) = \<alpha> m1 ++ \<alpha> m2 \<and> invar (iterate_add_to_map m1 update (iteratei m2))
[PROOF STEP]
apply (rule
        iterate_add_to_map_correct[of \<alpha> invar update m1 "iteratei m2" "\<alpha> m2"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. map_update \<alpha> invar update
 2. invar m1
 3. map_iterator (iteratei m2) (\<alpha> m2)
[PROOF STEP]
apply unfold_locales []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. invar m1
 2. map_iterator (iteratei m2) (\<alpha> m2)
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_iterator (iteratei m2) (\<alpha> m2)
[PROOF STEP]
apply (rule iteratei_correct, fact)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<alpha> (g_add m1 m2) = \<alpha> m1 ++ \<alpha> m2 \<and> invar (g_add m1 m2)

goal (2 subgoals):
 1. \<And>m1 m2. \<lbrakk>invar m1; invar m2\<rbrakk> \<Longrightarrow> \<alpha> (g_add m1 m2) = \<alpha> m1 ++ \<alpha> m2
 2. \<And>m1 m2. \<lbrakk>invar m1; invar m2\<rbrakk> \<Longrightarrow> invar (g_add m1 m2)
[PROOF STEP]
thus "\<alpha> (g_add m1 m2) = \<alpha> m1 ++ \<alpha> m2" "invar (g_add m1 m2)"
[PROOF STATE]
proof (prove)
using this:
\<alpha> (g_add m1 m2) = \<alpha> m1 ++ \<alpha> m2 \<and> invar (g_add m1 m2)

goal (1 subgoal):
 1. \<alpha> (g_add m1 m2) = \<alpha> m1 ++ \<alpha> m2 &&& invar (g_add m1 m2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<alpha> (g_add m1 m2) = \<alpha> m1 ++ \<alpha> m2
invar (g_add m1 m2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma g_sel_impl: "map_sel' \<alpha> invar g_sel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_sel' \<alpha> invar g_sel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_sel' \<alpha> invar g_sel
[PROOF STEP]
have A: "\<And>m P. g_sel m P = iterate_sel_no_map (iteratei m) P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m P. g_sel m P = iterate_sel_no_map (iteratei m) P
[PROOF STEP]
unfolding g_sel_def iterate_sel_no_map_def iterate_sel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m P. iteratei m (\<lambda>\<sigma>. \<sigma> = None) (\<lambda>x \<sigma>. if P x then Some x else None) None = iteratei m (\<lambda>\<sigma>. \<sigma> = None) (\<lambda>x \<sigma>. if P x then Some x else None) None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g_sel ?m2 ?P2 = iterate_sel_no_map (iteratei ?m2) ?P2

goal (1 subgoal):
 1. map_sel' \<alpha> invar g_sel
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
g_sel ?m2 ?P2 = iterate_sel_no_map (iteratei ?m2) ?P2

goal (1 subgoal):
 1. map_sel' \<alpha> invar g_sel
[PROOF STEP]
fix m P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_sel' \<alpha> invar g_sel
[PROOF STEP]
assume I: "invar m"
[PROOF STATE]
proof (state)
this:
invar m

goal (1 subgoal):
 1. map_sel' \<alpha> invar g_sel
[PROOF STEP]
note iterate_sel_no_map_correct[OF iteratei_correct[OF I], of P]
[PROOF STATE]
proof (state)
this:
(iterate_sel_no_map (iteratei m) P = None) = (\<forall>x\<in>map_to_set (\<alpha> m). \<not> P x)
iterate_sel_no_map (iteratei m) P = Some ?x \<Longrightarrow> ?x \<in> map_to_set (\<alpha> m) \<and> P ?x

goal (1 subgoal):
 1. map_sel' \<alpha> invar g_sel
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
invar ?m4 \<Longrightarrow> (iterate_sel_no_map (iteratei ?m4) ?P4 = None) = (\<forall>x\<in>map_to_set (\<alpha> ?m4). \<not> ?P4 x)
\<lbrakk>invar ?m4; iterate_sel_no_map (iteratei ?m4) ?P4 = Some ?x\<rbrakk> \<Longrightarrow> ?x \<in> map_to_set (\<alpha> ?m4) \<and> ?P4 ?x

goal (1 subgoal):
 1. map_sel' \<alpha> invar g_sel
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
invar ?m4 \<Longrightarrow> (iterate_sel_no_map (iteratei ?m4) ?P4 = None) = (\<forall>x\<in>map_to_set (\<alpha> ?m4). \<not> ?P4 x)
\<lbrakk>invar ?m4; iterate_sel_no_map (iteratei ?m4) ?P4 = Some ?x\<rbrakk> \<Longrightarrow> ?x \<in> map_to_set (\<alpha> ?m4) \<and> ?P4 ?x

goal (1 subgoal):
 1. map_sel' \<alpha> invar g_sel
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m u v P Q. \<lbrakk>\<And>m P. invar m \<Longrightarrow> (iterate_sel_no_map (iteratei m) P = None) = (\<forall>x\<in>map_to_set (\<alpha> m). \<not> P x); \<And>m P x. \<lbrakk>invar m; iterate_sel_no_map (iteratei m) P = Some x\<rbrakk> \<Longrightarrow> x \<in> map_to_set (\<alpha> m) \<and> P x; invar m; \<alpha> m u = Some v; P (u, v); \<And>u v. \<lbrakk>g_sel m P = Some (u, v); \<alpha> m u = Some v; P (u, v)\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
 2. \<And>m P. \<lbrakk>\<And>m P. invar m \<Longrightarrow> (iterate_sel_no_map (iteratei m) P = None) = (\<forall>x\<in>map_to_set (\<alpha> m). \<not> P x); \<And>m P x. \<lbrakk>invar m; iterate_sel_no_map (iteratei m) P = Some x\<rbrakk> \<Longrightarrow> x \<in> map_to_set (\<alpha> m) \<and> P x; invar m; \<forall>u v. \<alpha> m u = Some v \<longrightarrow> \<not> P (u, v)\<rbrakk> \<Longrightarrow> g_sel m P = None
[PROOF STEP]
unfolding A
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m u v P Q. \<lbrakk>\<And>m P. invar m \<Longrightarrow> (iterate_sel_no_map (iteratei m) P = None) = (\<forall>x\<in>map_to_set (\<alpha> m). \<not> P x); \<And>m P x. \<lbrakk>invar m; iterate_sel_no_map (iteratei m) P = Some x\<rbrakk> \<Longrightarrow> x \<in> map_to_set (\<alpha> m) \<and> P x; invar m; \<alpha> m u = Some v; P (u, v); \<And>u v. \<lbrakk>iterate_sel_no_map (iteratei m) P = Some (u, v); \<alpha> m u = Some v; P (u, v)\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
 2. \<And>m P. \<lbrakk>\<And>m P. invar m \<Longrightarrow> (iterate_sel_no_map (iteratei m) P = None) = (\<forall>x\<in>map_to_set (\<alpha> m). \<not> P x); \<And>m P x. \<lbrakk>invar m; iterate_sel_no_map (iteratei m) P = Some x\<rbrakk> \<Longrightarrow> x \<in> map_to_set (\<alpha> m) \<and> P x; invar m; \<forall>u v. \<alpha> m u = Some v \<longrightarrow> \<not> P (u, v)\<rbrakk> \<Longrightarrow> iterate_sel_no_map (iteratei m) P = None
[PROOF STEP]
apply (simp add: Bex_def Ball_def image_iff map_to_set_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m u v P Q. \<lbrakk>\<And>m P. invar m \<Longrightarrow> (iterate_sel_no_map (iteratei m) P = None) = (\<forall>a b. \<alpha> m a = Some b \<longrightarrow> \<not> P (a, b)); \<And>m P x. \<lbrakk>invar m; iterate_sel_no_map (iteratei m) P = Some x\<rbrakk> \<Longrightarrow> (case x of (k, v) \<Rightarrow> \<alpha> m k = Some v) \<and> P x; invar m; \<alpha> m u = Some v; P (u, v); \<And>u v. \<lbrakk>iterate_sel_no_map (iteratei m) P = Some (u, v); \<alpha> m u = Some v; P (u, v)\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
 2. \<And>m P. \<lbrakk>\<And>m P. invar m \<Longrightarrow> (iterate_sel_no_map (iteratei m) P = None) = (\<forall>x\<in>map_to_set (\<alpha> m). \<not> P x); \<And>m P x. \<lbrakk>invar m; iterate_sel_no_map (iteratei m) P = Some x\<rbrakk> \<Longrightarrow> x \<in> map_to_set (\<alpha> m) \<and> P x; invar m; \<forall>u v. \<alpha> m u = Some v \<longrightarrow> \<not> P (u, v)\<rbrakk> \<Longrightarrow> iterate_sel_no_map (iteratei m) P = None
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m u v P Q. \<lbrakk>\<And>m P. invar m \<Longrightarrow> (iterate_sel_no_map (iteratei m) P = None) = (\<forall>a b. \<alpha> m a = Some b \<longrightarrow> \<not> P (a, b)); \<And>m P a b. \<lbrakk>invar m; iterate_sel_no_map (iteratei m) P = Some (a, b)\<rbrakk> \<Longrightarrow> \<alpha> m a = Some b \<and> P (a, b); invar m; \<alpha> m u = Some v; P (u, v); \<And>u v. \<lbrakk>iterate_sel_no_map (iteratei m) P = Some (u, v); \<alpha> m u = Some v; P (u, v)\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
 2. \<And>m P. \<lbrakk>\<And>m P. invar m \<Longrightarrow> (iterate_sel_no_map (iteratei m) P = None) = (\<forall>x\<in>map_to_set (\<alpha> m). \<not> P x); \<And>m P x. \<lbrakk>invar m; iterate_sel_no_map (iteratei m) P = Some x\<rbrakk> \<Longrightarrow> x \<in> map_to_set (\<alpha> m) \<and> P x; invar m; \<forall>u v. \<alpha> m u = Some v \<longrightarrow> \<not> P (u, v)\<rbrakk> \<Longrightarrow> iterate_sel_no_map (iteratei m) P = None
[PROOF STEP]
apply (metis option.exhaust prod.exhaust)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m P. \<lbrakk>\<And>m P. invar m \<Longrightarrow> (iterate_sel_no_map (iteratei m) P = None) = (\<forall>x\<in>map_to_set (\<alpha> m). \<not> P x); \<And>m P x. \<lbrakk>invar m; iterate_sel_no_map (iteratei m) P = Some x\<rbrakk> \<Longrightarrow> x \<in> map_to_set (\<alpha> m) \<and> P x; invar m; \<forall>u v. \<alpha> m u = Some v \<longrightarrow> \<not> P (u, v)\<rbrakk> \<Longrightarrow> iterate_sel_no_map (iteratei m) P = None
[PROOF STEP]
apply (simp add: Bex_def Ball_def image_iff map_to_set_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
map_sel' \<alpha> invar g_sel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma g_bex_impl: "map_bex \<alpha> invar g_bex"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_bex \<alpha> invar g_bex
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m P. invar m \<Longrightarrow> g_bex m P = (\<exists>u v. \<alpha> m u = Some v \<and> P (u, v))
[PROOF STEP]
unfolding g_bex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m P. invar m \<Longrightarrow> iteratei m Not (\<lambda>kv \<sigma>. P kv) False = (\<exists>u v. \<alpha> m u = Some v \<and> P (u, v))
[PROOF STEP]
apply (rule_tac I="\<lambda>it \<sigma>. \<sigma> \<longleftrightarrow> (\<exists>kv\<in>it. P kv)"
      in iteratei_rule_insert_P)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>m P. invar m \<Longrightarrow> invar m
 2. \<And>m P. invar m \<Longrightarrow> False = (\<exists>kv\<in>{}. P kv)
 3. \<And>m P k v it \<sigma>. \<lbrakk>invar m; \<not> \<sigma>; (k, v) \<in> map_to_set (\<alpha> m) - it; it \<subseteq> map_to_set (\<alpha> m); \<sigma> = (\<exists>kv\<in>it. P kv)\<rbrakk> \<Longrightarrow> P (k, v) = (\<exists>kv\<in>insert (k, v) it. P kv)
 4. \<And>m P \<sigma>. \<lbrakk>invar m; \<sigma> = (\<exists>kv\<in>map_to_set (\<alpha> m). P kv)\<rbrakk> \<Longrightarrow> \<sigma> = (\<exists>u v. \<alpha> m u = Some v \<and> P (u, v))
 5. \<And>m P \<sigma> it. \<lbrakk>invar m; it \<subseteq> map_to_set (\<alpha> m); it \<noteq> map_to_set (\<alpha> m); \<not> \<not> \<sigma>; \<sigma> = (\<exists>kv\<in>it. P kv)\<rbrakk> \<Longrightarrow> \<sigma> = (\<exists>u v. \<alpha> m u = Some v \<and> P (u, v))
[PROOF STEP]
by (auto simp: map_to_set_def)


[STATEMENT]
lemma g_ball_impl: "map_ball \<alpha> invar g_ball"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_ball \<alpha> invar g_ball
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m P. invar m \<Longrightarrow> g_ball m P = (\<forall>u v. \<alpha> m u = Some v \<longrightarrow> P (u, v))
[PROOF STEP]
unfolding g_ball_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m P. invar m \<Longrightarrow> iteratei m id (\<lambda>kv \<sigma>. P kv) True = (\<forall>u v. \<alpha> m u = Some v \<longrightarrow> P (u, v))
[PROOF STEP]
apply (rule_tac I="\<lambda>it \<sigma>. \<sigma> \<longleftrightarrow> (\<forall>kv\<in>it. P kv)"
      in iteratei_rule_insert_P)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>m P. invar m \<Longrightarrow> invar m
 2. \<And>m P. invar m \<Longrightarrow> True = (\<forall>kv\<in>{}. P kv)
 3. \<And>m P k v it \<sigma>. \<lbrakk>invar m; id \<sigma>; (k, v) \<in> map_to_set (\<alpha> m) - it; it \<subseteq> map_to_set (\<alpha> m); \<sigma> = (\<forall>kv\<in>it. P kv)\<rbrakk> \<Longrightarrow> P (k, v) = (\<forall>kv\<in>insert (k, v) it. P kv)
 4. \<And>m P \<sigma>. \<lbrakk>invar m; \<sigma> = (\<forall>kv\<in>map_to_set (\<alpha> m). P kv)\<rbrakk> \<Longrightarrow> \<sigma> = (\<forall>u v. \<alpha> m u = Some v \<longrightarrow> P (u, v))
 5. \<And>m P \<sigma> it. \<lbrakk>invar m; it \<subseteq> map_to_set (\<alpha> m); it \<noteq> map_to_set (\<alpha> m); \<not> id \<sigma>; \<sigma> = (\<forall>kv\<in>it. P kv)\<rbrakk> \<Longrightarrow> \<sigma> = (\<forall>u v. \<alpha> m u = Some v \<longrightarrow> P (u, v))
[PROOF STEP]
apply (auto simp: map_to_set_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma g_size_impl: "map_size \<alpha> invar g_size"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_size \<alpha> invar g_size
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. invar s \<Longrightarrow> g_size s = card (dom (\<alpha> s))
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. invar s \<Longrightarrow> g_size s = card (dom (\<alpha> s))
[PROOF STEP]
assume I: "invar m"
[PROOF STATE]
proof (state)
this:
invar m

goal (1 subgoal):
 1. \<And>s. invar s \<Longrightarrow> g_size s = card (dom (\<alpha> s))
[PROOF STEP]
have A: "g_size m \<equiv> iterate_size (iteratei m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g_size m \<equiv> iterate_size (iteratei m)
[PROOF STEP]
unfolding g_size_def iterate_size_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iterate m (\<lambda>_. Suc) 0 \<equiv> iterate m (\<lambda>x. Suc) 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g_size m \<equiv> iterate_size (iteratei m)

goal (1 subgoal):
 1. \<And>s. invar s \<Longrightarrow> g_size s = card (dom (\<alpha> s))
[PROOF STEP]
from iterate_size_correct [OF iteratei_correct[OF I]]
[PROOF STATE]
proof (chain)
picking this:
iterate_size (iteratei m) = card (map_to_set (\<alpha> m)) \<and> finite (map_to_set (\<alpha> m))
[PROOF STEP]
show "g_size m = card (dom (\<alpha> m))"
[PROOF STATE]
proof (prove)
using this:
iterate_size (iteratei m) = card (map_to_set (\<alpha> m)) \<and> finite (map_to_set (\<alpha> m))

goal (1 subgoal):
 1. g_size m = card (dom (\<alpha> m))
[PROOF STEP]
unfolding A
[PROOF STATE]
proof (prove)
using this:
iterate_size (iteratei m) = card (map_to_set (\<alpha> m)) \<and> finite (map_to_set (\<alpha> m))

goal (1 subgoal):
 1. iterate_size (iteratei m) = card (dom (\<alpha> m))
[PROOF STEP]
by (simp_all add: card_map_to_set)
[PROOF STATE]
proof (state)
this:
g_size m = card (dom (\<alpha> m))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma g_size_abort_impl: "map_size_abort \<alpha> invar g_size_abort"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_size_abort \<alpha> invar g_size_abort
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s m. invar s \<Longrightarrow> g_size_abort m s = min m (card (dom (\<alpha> s)))
[PROOF STEP]
fix s m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s m. invar s \<Longrightarrow> g_size_abort m s = min m (card (dom (\<alpha> s)))
[PROOF STEP]
assume I: "invar m"
[PROOF STATE]
proof (state)
this:
invar m

goal (1 subgoal):
 1. \<And>s m. invar s \<Longrightarrow> g_size_abort m s = min m (card (dom (\<alpha> s)))
[PROOF STEP]
have A: "g_size_abort s m \<equiv> iterate_size_abort (iteratei m) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g_size_abort s m \<equiv> iterate_size_abort (iteratei m) s
[PROOF STEP]
unfolding g_size_abort_def iterate_size_abort_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iteratei m (\<lambda>sa. sa < s) (\<lambda>_. Suc) 0 \<equiv> iteratei m (\<lambda>\<sigma>. \<sigma> < s) (\<lambda>x. Suc) 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g_size_abort s m \<equiv> iterate_size_abort (iteratei m) s

goal (1 subgoal):
 1. \<And>s m. invar s \<Longrightarrow> g_size_abort m s = min m (card (dom (\<alpha> s)))
[PROOF STEP]
from iterate_size_abort_correct [OF iteratei_correct[OF I]]
[PROOF STATE]
proof (chain)
picking this:
iterate_size_abort (iteratei m) ?n = min ?n (card (map_to_set (\<alpha> m))) \<and> finite (map_to_set (\<alpha> m))
[PROOF STEP]
show "g_size_abort s m = min s (card (dom (\<alpha> m)))"
[PROOF STATE]
proof (prove)
using this:
iterate_size_abort (iteratei m) ?n = min ?n (card (map_to_set (\<alpha> m))) \<and> finite (map_to_set (\<alpha> m))

goal (1 subgoal):
 1. g_size_abort s m = min s (card (dom (\<alpha> m)))
[PROOF STEP]
unfolding A
[PROOF STATE]
proof (prove)
using this:
iterate_size_abort (iteratei m) ?n = min ?n (card (map_to_set (\<alpha> m))) \<and> finite (map_to_set (\<alpha> m))

goal (1 subgoal):
 1. iterate_size_abort (iteratei m) s = min s (card (dom (\<alpha> m)))
[PROOF STEP]
by (simp_all add: card_map_to_set)
[PROOF STATE]
proof (state)
this:
g_size_abort s m = min s (card (dom (\<alpha> m)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma g_isEmpty_impl: "map_isEmpty \<alpha> invar g_isEmpty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_isEmpty \<alpha> invar g_isEmpty
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. invar m \<Longrightarrow> g_isEmpty m = (\<alpha> m = Map.empty)
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. invar m \<Longrightarrow> g_isEmpty m = (\<alpha> m = Map.empty)
[PROOF STEP]
assume I: "invar m"
[PROOF STATE]
proof (state)
this:
invar m

goal (1 subgoal):
 1. \<And>m. invar m \<Longrightarrow> g_isEmpty m = (\<alpha> m = Map.empty)
[PROOF STEP]
interpret map_size_abort \<alpha> invar g_size_abort
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_size_abort \<alpha> invar g_size_abort
[PROOF STEP]
by (rule g_size_abort_impl)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. invar m \<Longrightarrow> g_isEmpty m = (\<alpha> m = Map.empty)
[PROOF STEP]
from size_abort_correct[OF I]
[PROOF STATE]
proof (chain)
picking this:
g_size_abort ?m m = min ?m (card (dom (\<alpha> m)))
[PROOF STEP]
have
      "g_size_abort 1 m = min 1 (card (dom (\<alpha> m)))"
[PROOF STATE]
proof (prove)
using this:
g_size_abort ?m m = min ?m (card (dom (\<alpha> m)))

goal (1 subgoal):
 1. g_size_abort 1 m = min 1 (card (dom (\<alpha> m)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
g_size_abort 1 m = min 1 (card (dom (\<alpha> m)))

goal (1 subgoal):
 1. \<And>m. invar m \<Longrightarrow> g_isEmpty m = (\<alpha> m = Map.empty)
[PROOF STEP]
thus "g_isEmpty m = (\<alpha> m = Map.empty)"
[PROOF STATE]
proof (prove)
using this:
g_size_abort 1 m = min 1 (card (dom (\<alpha> m)))

goal (1 subgoal):
 1. g_isEmpty m = (\<alpha> m = Map.empty)
[PROOF STEP]
unfolding g_isEmpty_def
[PROOF STATE]
proof (prove)
using this:
g_size_abort 1 m = min 1 (card (dom (\<alpha> m)))

goal (1 subgoal):
 1. (g_size_abort 1 m = 0) = (\<alpha> m = Map.empty)
[PROOF STEP]
by (auto simp: min_def card_0_eq[OF finite] I)
[PROOF STATE]
proof (state)
this:
g_isEmpty m = (\<alpha> m = Map.empty)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma g_isSng_impl: "map_isSng \<alpha> invar g_isSng"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_isSng \<alpha> invar g_isSng
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. invar s \<Longrightarrow> g_isSng s = (\<exists>k v. \<alpha> s = [k \<mapsto> v])
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. invar s \<Longrightarrow> g_isSng s = (\<exists>k v. \<alpha> s = [k \<mapsto> v])
[PROOF STEP]
assume I: "invar m"
[PROOF STATE]
proof (state)
this:
invar m

goal (1 subgoal):
 1. \<And>s. invar s \<Longrightarrow> g_isSng s = (\<exists>k v. \<alpha> s = [k \<mapsto> v])
[PROOF STEP]
interpret map_size_abort \<alpha> invar g_size_abort
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_size_abort \<alpha> invar g_size_abort
[PROOF STEP]
by (rule g_size_abort_impl)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. invar s \<Longrightarrow> g_isSng s = (\<exists>k v. \<alpha> s = [k \<mapsto> v])
[PROOF STEP]
from size_abort_correct[OF I]
[PROOF STATE]
proof (chain)
picking this:
g_size_abort ?m m = min ?m (card (dom (\<alpha> m)))
[PROOF STEP]
have
      "g_size_abort 2 m = min 2 (card (dom (\<alpha> m)))"
[PROOF STATE]
proof (prove)
using this:
g_size_abort ?m m = min ?m (card (dom (\<alpha> m)))

goal (1 subgoal):
 1. g_size_abort 2 m = min 2 (card (dom (\<alpha> m)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
g_size_abort 2 m = min 2 (card (dom (\<alpha> m)))

goal (1 subgoal):
 1. \<And>s. invar s \<Longrightarrow> g_isSng s = (\<exists>k v. \<alpha> s = [k \<mapsto> v])
[PROOF STEP]
thus "g_isSng m = (\<exists>k v. \<alpha> m = [k \<mapsto> v])"
[PROOF STATE]
proof (prove)
using this:
g_size_abort 2 m = min 2 (card (dom (\<alpha> m)))

goal (1 subgoal):
 1. g_isSng m = (\<exists>k v. \<alpha> m = [k \<mapsto> v])
[PROOF STEP]
unfolding g_isSng_def
[PROOF STATE]
proof (prove)
using this:
g_size_abort 2 m = min 2 (card (dom (\<alpha> m)))

goal (1 subgoal):
 1. (g_size_abort 2 m = 1) = (\<exists>k v. \<alpha> m = [k \<mapsto> v])
[PROOF STEP]
by (auto simp: min_def I card_Suc_eq dom_eq_singleton_conv)
[PROOF STATE]
proof (state)
this:
g_isSng m = (\<exists>k v. \<alpha> m = [k \<mapsto> v])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma g_to_list_impl: "map_to_list \<alpha> invar g_to_list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_to_list \<alpha> invar g_to_list
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m. invar m \<Longrightarrow> map_of (g_to_list m) = \<alpha> m
 2. \<And>m. invar m \<Longrightarrow> distinct (map fst (g_to_list m))
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m. invar m \<Longrightarrow> map_of (g_to_list m) = \<alpha> m
 2. \<And>m. invar m \<Longrightarrow> distinct (map fst (g_to_list m))
[PROOF STEP]
assume I: "invar m"
[PROOF STATE]
proof (state)
this:
invar m

goal (2 subgoals):
 1. \<And>m. invar m \<Longrightarrow> map_of (g_to_list m) = \<alpha> m
 2. \<And>m. invar m \<Longrightarrow> distinct (map fst (g_to_list m))
[PROOF STEP]
have A: "g_to_list m = iterate_to_list (iteratei m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g_to_list m = iterate_to_list (iteratei m)
[PROOF STEP]
unfolding g_to_list_def iterate_to_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iterate m (#) [] = iterate m (#) []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g_to_list m = iterate_to_list (iteratei m)

goal (2 subgoals):
 1. \<And>m. invar m \<Longrightarrow> map_of (g_to_list m) = \<alpha> m
 2. \<And>m. invar m \<Longrightarrow> distinct (map fst (g_to_list m))
[PROOF STEP]
from iterate_to_list_correct [OF iteratei_correct[OF I]]
[PROOF STATE]
proof (chain)
picking this:
set (iterate_to_list (iteratei m)) = map_to_set (\<alpha> m) \<and> distinct (iterate_to_list (iteratei m))
[PROOF STEP]
have set_l_eq: "set (g_to_list m) = map_to_set (\<alpha> m)" and
      dist_l: "distinct (g_to_list m)"
[PROOF STATE]
proof (prove)
using this:
set (iterate_to_list (iteratei m)) = map_to_set (\<alpha> m) \<and> distinct (iterate_to_list (iteratei m))

goal (1 subgoal):
 1. set (g_to_list m) = map_to_set (\<alpha> m) &&& distinct (g_to_list m)
[PROOF STEP]
unfolding A
[PROOF STATE]
proof (prove)
using this:
set (iterate_to_list (iteratei m)) = map_to_set (\<alpha> m) \<and> distinct (iterate_to_list (iteratei m))

goal (1 subgoal):
 1. set (iterate_to_list (iteratei m)) = map_to_set (\<alpha> m) &&& distinct (iterate_to_list (iteratei m))
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
set (g_to_list m) = map_to_set (\<alpha> m)
distinct (g_to_list m)

goal (2 subgoals):
 1. \<And>m. invar m \<Longrightarrow> map_of (g_to_list m) = \<alpha> m
 2. \<And>m. invar m \<Longrightarrow> distinct (map fst (g_to_list m))
[PROOF STEP]
from dist_l
[PROOF STATE]
proof (chain)
picking this:
distinct (g_to_list m)
[PROOF STEP]
show dist_fst_l: "distinct (map fst (g_to_list m))"
[PROOF STATE]
proof (prove)
using this:
distinct (g_to_list m)

goal (1 subgoal):
 1. distinct (map fst (g_to_list m))
[PROOF STEP]
by (simp add: distinct_map set_l_eq map_to_set_def inj_on_def)
[PROOF STATE]
proof (state)
this:
distinct (map fst (g_to_list m))

goal (1 subgoal):
 1. \<And>m. invar m \<Longrightarrow> map_of (g_to_list m) = \<alpha> m
[PROOF STEP]
from map_of_map_to_set[of "(g_to_list m)" "\<alpha> m", OF dist_fst_l] set_l_eq
[PROOF STATE]
proof (chain)
picking this:
(map_of (g_to_list m) = \<alpha> m) = (set (g_to_list m) = map_to_set (\<alpha> m))
set (g_to_list m) = map_to_set (\<alpha> m)
[PROOF STEP]
show "map_of (g_to_list m) = \<alpha> m"
[PROOF STATE]
proof (prove)
using this:
(map_of (g_to_list m) = \<alpha> m) = (set (g_to_list m) = map_to_set (\<alpha> m))
set (g_to_list m) = map_to_set (\<alpha> m)

goal (1 subgoal):
 1. map_of (g_to_list m) = \<alpha> m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_of (g_to_list m) = \<alpha> m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma g_list_to_map_impl: "list_to_map \<alpha> invar g_list_to_map"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_to_map \<alpha> invar g_list_to_map
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_to_map \<alpha> invar g_list_to_map
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_to_map \<alpha> invar g_list_to_map
[PROOF STEP]
fix m0 l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_to_map \<alpha> invar g_list_to_map
[PROOF STEP]
assume "invar m0"
[PROOF STATE]
proof (state)
this:
invar m0

goal (1 subgoal):
 1. list_to_map \<alpha> invar g_list_to_map
[PROOF STEP]
hence "invar (foldl (\<lambda>s (k,v). update k v s) m0 l) \<and>
        \<alpha> (foldl (\<lambda>s (k,v). update k v s) m0 l) = \<alpha> m0 ++ map_of (rev l)"
[PROOF STATE]
proof (prove)
using this:
invar m0

goal (1 subgoal):
 1. invar (foldl (\<lambda>s (k, v). update k v s) m0 l) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 l) = \<alpha> m0 ++ map_of (rev l)
[PROOF STEP]
proof (induction l arbitrary: m0)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m0. invar m0 \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 []) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 []) = \<alpha> m0 ++ map_of (rev [])
 2. \<And>a l m0. \<lbrakk>\<And>m0. invar m0 \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 l) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 l) = \<alpha> m0 ++ map_of (rev l); invar m0\<rbrakk> \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 (a # l)) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 (a # l)) = \<alpha> m0 ++ map_of (rev (a # l))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
invar m0

goal (2 subgoals):
 1. \<And>m0. invar m0 \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 []) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 []) = \<alpha> m0 ++ map_of (rev [])
 2. \<And>a l m0. \<lbrakk>\<And>m0. invar m0 \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 l) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 l) = \<alpha> m0 ++ map_of (rev l); invar m0\<rbrakk> \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 (a # l)) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 (a # l)) = \<alpha> m0 ++ map_of (rev (a # l))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
invar m0

goal (1 subgoal):
 1. invar (foldl (\<lambda>s a. case a of (k, v) \<Rightarrow> update k v s) m0 []) \<and> \<alpha> (foldl (\<lambda>s a. case a of (k, v) \<Rightarrow> update k v s) m0 []) = \<alpha> m0 ++ map_of (rev [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
invar (foldl (\<lambda>s a. case a of (k, v) \<Rightarrow> update k v s) m0 []) \<and> \<alpha> (foldl (\<lambda>s a. case a of (k, v) \<Rightarrow> update k v s) m0 []) = \<alpha> m0 ++ map_of (rev [])

goal (1 subgoal):
 1. \<And>a l m0. \<lbrakk>\<And>m0. invar m0 \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 l) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 l) = \<alpha> m0 ++ map_of (rev l); invar m0\<rbrakk> \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 (a # l)) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 (a # l)) = \<alpha> m0 ++ map_of (rev (a # l))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l m0. \<lbrakk>\<And>m0. invar m0 \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 l) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 l) = \<alpha> m0 ++ map_of (rev l); invar m0\<rbrakk> \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 (a # l)) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 (a # l)) = \<alpha> m0 ++ map_of (rev (a # l))
[PROOF STEP]
case (Cons kv l)
[PROOF STATE]
proof (state)
this:
invar ?m0.2 \<Longrightarrow> invar (foldl (\<lambda>s a. case a of (k, v) \<Rightarrow> update k v s) ?m0.2 l) \<and> \<alpha> (foldl (\<lambda>s a. case a of (k, v) \<Rightarrow> update k v s) ?m0.2 l) = \<alpha> ?m0.2 ++ map_of (rev l)
invar m0

goal (1 subgoal):
 1. \<And>a l m0. \<lbrakk>\<And>m0. invar m0 \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 l) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 l) = \<alpha> m0 ++ map_of (rev l); invar m0\<rbrakk> \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 (a # l)) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 (a # l)) = \<alpha> m0 ++ map_of (rev (a # l))
[PROOF STEP]
obtain k v where [simp]: "kv=(k,v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k v. kv = (k, v) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases kv) auto
[PROOF STATE]
proof (state)
this:
kv = (k, v)

goal (1 subgoal):
 1. \<And>a l m0. \<lbrakk>\<And>m0. invar m0 \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 l) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 l) = \<alpha> m0 ++ map_of (rev l); invar m0\<rbrakk> \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 (a # l)) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 (a # l)) = \<alpha> m0 ++ map_of (rev (a # l))
[PROOF STEP]
have "invar (foldl (\<lambda>s (k, v). update k v s) m0 (kv # l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar (foldl (\<lambda>s (k, v). update k v s) m0 (kv # l))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar (foldl (\<lambda>s (k, v). update k v s) (update k v m0) l)
[PROOF STEP]
apply (rule conjunct1[OF Cons.IH])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar (update k v m0)
[PROOF STEP]
apply (simp add: update_correct Cons.prems)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
invar (foldl (\<lambda>s (k, v). update k v s) m0 (kv # l))

goal (1 subgoal):
 1. \<And>a l m0. \<lbrakk>\<And>m0. invar m0 \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 l) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 l) = \<alpha> m0 ++ map_of (rev l); invar m0\<rbrakk> \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 (a # l)) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 (a # l)) = \<alpha> m0 ++ map_of (rev (a # l))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
invar (foldl (\<lambda>s (k, v). update k v s) m0 (kv # l))

goal (1 subgoal):
 1. \<And>a l m0. \<lbrakk>\<And>m0. invar m0 \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 l) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 l) = \<alpha> m0 ++ map_of (rev l); invar m0\<rbrakk> \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 (a # l)) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 (a # l)) = \<alpha> m0 ++ map_of (rev (a # l))
[PROOF STEP]
have "\<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 (kv # l)) =
          \<alpha> m0 ++ map_of (rev (kv # l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 (kv # l)) = \<alpha> m0 ++ map_of (rev (kv # l))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (foldl (\<lambda>s (k, v). update k v s) (update k v m0) l) = \<alpha> m0(k \<mapsto> v) ++ map_of (rev l)
[PROOF STEP]
apply (rule trans[OF conjunct2[OF Cons.IH]])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. invar (update k v m0)
 2. \<alpha> (update k v m0) ++ map_of (rev l) = \<alpha> m0(k \<mapsto> v) ++ map_of (rev l)
[PROOF STEP]
apply (auto
            simp: update_correct Cons.prems Map.map_add_def[abs_def]
            split: option.split
          )
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 (kv # l)) = \<alpha> m0 ++ map_of (rev (kv # l))

goal (1 subgoal):
 1. \<And>a l m0. \<lbrakk>\<And>m0. invar m0 \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 l) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 l) = \<alpha> m0 ++ map_of (rev l); invar m0\<rbrakk> \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 (a # l)) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 (a # l)) = \<alpha> m0 ++ map_of (rev (a # l))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
invar (foldl (\<lambda>s (k, v). update k v s) m0 (kv # l))
\<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 (kv # l)) = \<alpha> m0 ++ map_of (rev (kv # l))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (foldl (\<lambda>s (k, v). update k v s) m0 (kv # l))
\<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 (kv # l)) = \<alpha> m0 ++ map_of (rev (kv # l))

goal (1 subgoal):
 1. invar (foldl (\<lambda>s a. case a of (k, v) \<Rightarrow> update k v s) m0 (kv # l)) \<and> \<alpha> (foldl (\<lambda>s a. case a of (k, v) \<Rightarrow> update k v s) m0 (kv # l)) = \<alpha> m0 ++ map_of (rev (kv # l))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
invar (foldl (\<lambda>s a. case a of (k, v) \<Rightarrow> update k v s) m0 (kv # l)) \<and> \<alpha> (foldl (\<lambda>s a. case a of (k, v) \<Rightarrow> update k v s) m0 (kv # l)) = \<alpha> m0 ++ map_of (rev (kv # l))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invar (foldl (\<lambda>s (k, v). update k v s) m0 l) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 l) = \<alpha> m0 ++ map_of (rev l)

goal (1 subgoal):
 1. list_to_map \<alpha> invar g_list_to_map
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
invar ?m0.4 \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) ?m0.4 ?l4) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) ?m0.4 ?l4) = \<alpha> ?m0.4 ++ map_of (rev ?l4)

goal (1 subgoal):
 1. list_to_map \<alpha> invar g_list_to_map
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
invar ?m0.4 \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) ?m0.4 ?l4) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) ?m0.4 ?l4) = \<alpha> ?m0.4 ++ map_of (rev ?l4)

goal (1 subgoal):
 1. list_to_map \<alpha> invar g_list_to_map
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l. (\<And>m0 l. invar m0 \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 l) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 l) = \<alpha> m0 ++ map_of (rev l)) \<Longrightarrow> \<alpha> (g_list_to_map l) = map_of l
 2. \<And>l. (\<And>m0 l. invar m0 \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 l) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 l) = \<alpha> m0 ++ map_of (rev l)) \<Longrightarrow> invar (g_list_to_map l)
[PROOF STEP]
unfolding g_list_to_map_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l. (\<And>m0 l. invar m0 \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 l) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 l) = \<alpha> m0 ++ map_of (rev l)) \<Longrightarrow> \<alpha> (foldl (\<lambda>m (k, v). update k v m) (local.empty ()) (rev l)) = map_of l
 2. \<And>l. (\<And>m0 l. invar m0 \<Longrightarrow> invar (foldl (\<lambda>s (k, v). update k v s) m0 l) \<and> \<alpha> (foldl (\<lambda>s (k, v). update k v s) m0 l) = \<alpha> m0 ++ map_of (rev l)) \<Longrightarrow> invar (foldl (\<lambda>m (k, v). update k v m) (local.empty ()) (rev l))
[PROOF STEP]
apply (auto simp: empty_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
list_to_map \<alpha> invar g_list_to_map

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma g_add_dj_impl: "map_add_dj \<alpha> invar g_add_dj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_add_dj \<alpha> invar g_add_dj
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m1 m2. \<lbrakk>invar m1; invar m2; dom (\<alpha> m1) \<inter> dom (\<alpha> m2) = {}\<rbrakk> \<Longrightarrow> \<alpha> (g_add_dj m1 m2) = \<alpha> m1 ++ \<alpha> m2
 2. \<And>m1 m2. \<lbrakk>invar m1; invar m2; dom (\<alpha> m1) \<inter> dom (\<alpha> m2) = {}\<rbrakk> \<Longrightarrow> invar (g_add_dj m1 m2)
[PROOF STEP]
fix m1 m2
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m1 m2. \<lbrakk>invar m1; invar m2; dom (\<alpha> m1) \<inter> dom (\<alpha> m2) = {}\<rbrakk> \<Longrightarrow> \<alpha> (g_add_dj m1 m2) = \<alpha> m1 ++ \<alpha> m2
 2. \<And>m1 m2. \<lbrakk>invar m1; invar m2; dom (\<alpha> m1) \<inter> dom (\<alpha> m2) = {}\<rbrakk> \<Longrightarrow> invar (g_add_dj m1 m2)
[PROOF STEP]
assume "invar m1" "invar m2" and DJ: "dom (\<alpha> m1) \<inter> dom (\<alpha> m2) = {}"
[PROOF STATE]
proof (state)
this:
invar m1
invar m2
dom (\<alpha> m1) \<inter> dom (\<alpha> m2) = {}

goal (2 subgoals):
 1. \<And>m1 m2. \<lbrakk>invar m1; invar m2; dom (\<alpha> m1) \<inter> dom (\<alpha> m2) = {}\<rbrakk> \<Longrightarrow> \<alpha> (g_add_dj m1 m2) = \<alpha> m1 ++ \<alpha> m2
 2. \<And>m1 m2. \<lbrakk>invar m1; invar m2; dom (\<alpha> m1) \<inter> dom (\<alpha> m2) = {}\<rbrakk> \<Longrightarrow> invar (g_add_dj m1 m2)
[PROOF STEP]
have A: "g_add_dj m1 m2 = iterate_add_to_map m1 update_dj (iteratei m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g_add_dj m1 m2 = iterate_add_to_map m1 update_dj (iteratei m2)
[PROOF STEP]
unfolding g_add_dj_def iterate_add_to_map_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iterate m2 (\<lambda>(x, y). update_dj x y) m1 = iterate m2 (\<lambda>(x, y). update_dj x y) m1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g_add_dj m1 m2 = iterate_add_to_map m1 update_dj (iteratei m2)

goal (2 subgoals):
 1. \<And>m1 m2. \<lbrakk>invar m1; invar m2; dom (\<alpha> m1) \<inter> dom (\<alpha> m2) = {}\<rbrakk> \<Longrightarrow> \<alpha> (g_add_dj m1 m2) = \<alpha> m1 ++ \<alpha> m2
 2. \<And>m1 m2. \<lbrakk>invar m1; invar m2; dom (\<alpha> m1) \<inter> dom (\<alpha> m2) = {}\<rbrakk> \<Longrightarrow> invar (g_add_dj m1 m2)
[PROOF STEP]
have "\<alpha> (g_add_dj m1 m2) = \<alpha> m1 ++ \<alpha> m2 \<and> invar (g_add_dj m1 m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (g_add_dj m1 m2) = \<alpha> m1 ++ \<alpha> m2 \<and> invar (g_add_dj m1 m2)
[PROOF STEP]
unfolding A
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (iterate_add_to_map m1 update_dj (iteratei m2)) = \<alpha> m1 ++ \<alpha> m2 \<and> invar (iterate_add_to_map m1 update_dj (iteratei m2))
[PROOF STEP]
apply (rule
        iterate_add_to_map_dj_correct[
        of \<alpha> invar update_dj m1 "iteratei m2" "\<alpha> m2"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. map_update_dj \<alpha> invar update_dj
 2. invar m1
 3. map_iterator (iteratei m2) (\<alpha> m2)
 4. dom (\<alpha> m2) \<inter> dom (\<alpha> m1) = {}
[PROOF STEP]
apply unfold_locales []
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. invar m1
 2. map_iterator (iteratei m2) (\<alpha> m2)
 3. dom (\<alpha> m2) \<inter> dom (\<alpha> m1) = {}
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. map_iterator (iteratei m2) (\<alpha> m2)
 2. dom (\<alpha> m2) \<inter> dom (\<alpha> m1) = {}
[PROOF STEP]
apply (rule iteratei_correct, fact)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (\<alpha> m2) \<inter> dom (\<alpha> m1) = {}
[PROOF STEP]
using DJ
[PROOF STATE]
proof (prove)
using this:
dom (\<alpha> m1) \<inter> dom (\<alpha> m2) = {}

goal (1 subgoal):
 1. dom (\<alpha> m2) \<inter> dom (\<alpha> m1) = {}
[PROOF STEP]
apply (simp add: Int_ac)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<alpha> (g_add_dj m1 m2) = \<alpha> m1 ++ \<alpha> m2 \<and> invar (g_add_dj m1 m2)

goal (2 subgoals):
 1. \<And>m1 m2. \<lbrakk>invar m1; invar m2; dom (\<alpha> m1) \<inter> dom (\<alpha> m2) = {}\<rbrakk> \<Longrightarrow> \<alpha> (g_add_dj m1 m2) = \<alpha> m1 ++ \<alpha> m2
 2. \<And>m1 m2. \<lbrakk>invar m1; invar m2; dom (\<alpha> m1) \<inter> dom (\<alpha> m2) = {}\<rbrakk> \<Longrightarrow> invar (g_add_dj m1 m2)
[PROOF STEP]
thus "\<alpha> (g_add_dj m1 m2) = \<alpha> m1 ++ \<alpha> m2" "invar (g_add_dj m1 m2)"
[PROOF STATE]
proof (prove)
using this:
\<alpha> (g_add_dj m1 m2) = \<alpha> m1 ++ \<alpha> m2 \<and> invar (g_add_dj m1 m2)

goal (1 subgoal):
 1. \<alpha> (g_add_dj m1 m2) = \<alpha> m1 ++ \<alpha> m2 &&& invar (g_add_dj m1 m2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<alpha> (g_add_dj m1 m2) = \<alpha> m1 ++ \<alpha> m2
invar (g_add_dj m1 m2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma g_restrict_impl: "map_restrict \<alpha> invar \<alpha> invar g_restrict"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_restrict \<alpha> invar \<alpha> invar g_restrict
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m P. invar m \<Longrightarrow> \<alpha> (g_restrict P m) = \<alpha> m |` {k. \<exists>v. \<alpha> m k = Some v \<and> P (k, v)}
 2. \<And>m P. invar m \<Longrightarrow> invar (g_restrict P m)
[PROOF STEP]
fix m P
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m P. invar m \<Longrightarrow> \<alpha> (g_restrict P m) = \<alpha> m |` {k. \<exists>v. \<alpha> m k = Some v \<and> P (k, v)}
 2. \<And>m P. invar m \<Longrightarrow> invar (g_restrict P m)
[PROOF STEP]
assume I: "invar m"
[PROOF STATE]
proof (state)
this:
invar m

goal (2 subgoals):
 1. \<And>m P. invar m \<Longrightarrow> \<alpha> (g_restrict P m) = \<alpha> m |` {k. \<exists>v. \<alpha> m k = Some v \<and> P (k, v)}
 2. \<And>m P. invar m \<Longrightarrow> invar (g_restrict P m)
[PROOF STEP]
have AUX: "\<And>k v it \<sigma>.
       \<lbrakk>it \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m k = Some v; (k, v) \<notin> it;
        {(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P\<rbrakk>
       \<Longrightarrow> k \<notin> dom (\<alpha> \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k v it \<sigma>. \<lbrakk>it \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m k = Some v; (k, v) \<notin> it; {(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P\<rbrakk> \<Longrightarrow> k \<notin> dom (\<alpha> \<sigma>)
[PROOF STEP]
proof (rule ccontr, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k v it \<sigma>. \<lbrakk>it \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m k = Some v; (k, v) \<notin> it; {(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P; k \<in> dom (\<alpha> \<sigma>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix k v it \<sigma>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k v it \<sigma>. \<lbrakk>it \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m k = Some v; (k, v) \<notin> it; {(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P; k \<in> dom (\<alpha> \<sigma>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "k\<in>dom (\<alpha> \<sigma>)"
[PROOF STATE]
proof (state)
this:
k \<in> dom (\<alpha> \<sigma>)

goal (1 subgoal):
 1. \<And>k v it \<sigma>. \<lbrakk>it \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m k = Some v; (k, v) \<notin> it; {(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P; k \<in> dom (\<alpha> \<sigma>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<in> dom (\<alpha> \<sigma>)
[PROOF STEP]
obtain v' where "\<alpha> \<sigma> k = Some v'"
[PROOF STATE]
proof (prove)
using this:
k \<in> dom (\<alpha> \<sigma>)

goal (1 subgoal):
 1. (\<And>v'. \<alpha> \<sigma> k = Some v' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<alpha> \<sigma> k = Some v'

goal (1 subgoal):
 1. \<And>k v it \<sigma>. \<lbrakk>it \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m k = Some v; (k, v) \<notin> it; {(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P; k \<in> dom (\<alpha> \<sigma>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<alpha> \<sigma> k = Some v'

goal (1 subgoal):
 1. \<And>k v it \<sigma>. \<lbrakk>it \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m k = Some v; (k, v) \<notin> it; {(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P; k \<in> dom (\<alpha> \<sigma>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "{(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P"
[PROOF STATE]
proof (state)
this:
{(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P

goal (1 subgoal):
 1. \<And>k v it \<sigma>. \<lbrakk>it \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m k = Some v; (k, v) \<notin> it; {(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P; k \<in> dom (\<alpha> \<sigma>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<sigma> k = Some v'
{(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P
[PROOF STEP]
have MEM: "(k,v')\<in>it"
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<sigma> k = Some v'
{(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P

goal (1 subgoal):
 1. (k, v') \<in> it
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(k, v') \<in> it

goal (1 subgoal):
 1. \<And>k v it \<sigma>. \<lbrakk>it \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m k = Some v; (k, v) \<notin> it; {(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P; k \<in> dom (\<alpha> \<sigma>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(k, v') \<in> it

goal (1 subgoal):
 1. \<And>k v it \<sigma>. \<lbrakk>it \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m k = Some v; (k, v) \<notin> it; {(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P; k \<in> dom (\<alpha> \<sigma>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "it \<subseteq> {(k, v). \<alpha> m k = Some v}" and "\<alpha> m k = Some v"
[PROOF STATE]
proof (state)
this:
it \<subseteq> {(k, v). \<alpha> m k = Some v}
\<alpha> m k = Some v

goal (1 subgoal):
 1. \<And>k v it \<sigma>. \<lbrakk>it \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m k = Some v; (k, v) \<notin> it; {(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P; k \<in> dom (\<alpha> \<sigma>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(k, v') \<in> it
it \<subseteq> {(k, v). \<alpha> m k = Some v}
\<alpha> m k = Some v
[PROOF STEP]
have "v'=v"
[PROOF STATE]
proof (prove)
using this:
(k, v') \<in> it
it \<subseteq> {(k, v). \<alpha> m k = Some v}
\<alpha> m k = Some v

goal (1 subgoal):
 1. v' = v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v' = v

goal (1 subgoal):
 1. \<And>k v it \<sigma>. \<lbrakk>it \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m k = Some v; (k, v) \<notin> it; {(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P; k \<in> dom (\<alpha> \<sigma>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v' = v

goal (1 subgoal):
 1. \<And>k v it \<sigma>. \<lbrakk>it \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m k = Some v; (k, v) \<notin> it; {(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P; k \<in> dom (\<alpha> \<sigma>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "(k,v)\<notin>it"
[PROOF STATE]
proof (state)
this:
(k, v) \<notin> it

goal (1 subgoal):
 1. \<And>k v it \<sigma>. \<lbrakk>it \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m k = Some v; (k, v) \<notin> it; {(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P; k \<in> dom (\<alpha> \<sigma>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(k, v) \<notin> it

goal (1 subgoal):
 1. \<And>k v it \<sigma>. \<lbrakk>it \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m k = Some v; (k, v) \<notin> it; {(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P; k \<in> dom (\<alpha> \<sigma>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
note MEM
[PROOF STATE]
proof (state)
this:
(k, v') \<in> it

goal (1 subgoal):
 1. \<And>k v it \<sigma>. \<lbrakk>it \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m k = Some v; (k, v) \<notin> it; {(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P; k \<in> dom (\<alpha> \<sigma>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v' = v
(k, v) \<notin> it
(k, v') \<in> it
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
v' = v
(k, v) \<notin> it
(k, v') \<in> it

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?it2 \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m ?k2 = Some ?v2; (?k2, ?v2) \<notin> ?it2; {(k, v). \<alpha> ?\<sigma>2 k = Some v} = ?it2 \<inter> Collect P\<rbrakk> \<Longrightarrow> ?k2 \<notin> dom (\<alpha> ?\<sigma>2)

goal (2 subgoals):
 1. \<And>m P. invar m \<Longrightarrow> \<alpha> (g_restrict P m) = \<alpha> m |` {k. \<exists>v. \<alpha> m k = Some v \<and> P (k, v)}
 2. \<And>m P. invar m \<Longrightarrow> invar (g_restrict P m)
[PROOF STEP]
have "\<alpha> (g_restrict P m) = \<alpha> m |` {k. \<exists>v. \<alpha> m k = Some v \<and> P (k, v)} \<and>
      invar (g_restrict P m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (g_restrict P m) = \<alpha> m |` {k. \<exists>v. \<alpha> m k = Some v \<and> P (k, v)} \<and> invar (g_restrict P m)
[PROOF STEP]
unfolding g_restrict_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (iterate m (\<lambda>(k, v) \<sigma>. if P (k, v) then update_dj k v \<sigma> else \<sigma>) (local.empty ())) = \<alpha> m |` {k. \<exists>v. \<alpha> m k = Some v \<and> P (k, v)} \<and> invar (iterate m (\<lambda>(k, v) \<sigma>. if P (k, v) then update_dj k v \<sigma> else \<sigma>) (local.empty ()))
[PROOF STEP]
apply (rule_tac I="\<lambda>it \<sigma>. invar \<sigma>
        \<and> map_to_set (\<alpha> \<sigma>) = it \<inter> Collect P"
        in iterate_rule_insert_P)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. invar m
 2. invar (local.empty ()) \<and> map_to_set (\<alpha> (local.empty ())) = {} \<inter> Collect P
 3. \<And>k v it \<sigma>. \<lbrakk>(k, v) \<in> map_to_set (\<alpha> m) - it; it \<subseteq> map_to_set (\<alpha> m); invar \<sigma> \<and> map_to_set (\<alpha> \<sigma>) = it \<inter> Collect P\<rbrakk> \<Longrightarrow> invar ((case (k, v) of (k, v) \<Rightarrow> \<lambda>\<sigma>. if P (k, v) then update_dj k v \<sigma> else \<sigma>) \<sigma>) \<and> map_to_set (\<alpha> ((case (k, v) of (k, v) \<Rightarrow> \<lambda>\<sigma>. if P (k, v) then update_dj k v \<sigma> else \<sigma>) \<sigma>)) = insert (k, v) it \<inter> Collect P
 4. \<And>\<sigma>. invar \<sigma> \<and> map_to_set (\<alpha> \<sigma>) = map_to_set (\<alpha> m) \<inter> Collect P \<Longrightarrow> \<alpha> \<sigma> = \<alpha> m |` {k. \<exists>v. \<alpha> m k = Some v \<and> P (k, v)} \<and> invar \<sigma>
[PROOF STEP]
apply (auto simp: I empty_correct update_dj_correct map_to_set_def AUX)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>k v it \<sigma> a b. \<lbrakk>it \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m k = Some v; (k, v) \<notin> it; invar \<sigma>; {(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P; P (k, v); (if a = k then Some v else \<alpha> \<sigma> a) = Some b; (a, b) \<notin> it\<rbrakk> \<Longrightarrow> b = v
 2. \<And>k v it \<sigma> a b. \<lbrakk>it \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m k = Some v; (k, v) \<notin> it; invar \<sigma>; {(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P; P (k, v); (if a = k then Some v else \<alpha> \<sigma> a) = Some b; \<not> P (a, b)\<rbrakk> \<Longrightarrow> b = v
 3. \<And>k v it \<sigma> b. \<lbrakk>it \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m k = Some v; (k, v) \<notin> it; invar \<sigma>; {(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P; P (k, v); (k, b) \<in> it; P (k, b)\<rbrakk> \<Longrightarrow> v = b
 4. \<And>k v it \<sigma> a b. \<lbrakk>it \<subseteq> {(k, v). \<alpha> m k = Some v}; \<alpha> m k = Some v; (k, v) \<notin> it; invar \<sigma>; {(k, v). \<alpha> \<sigma> k = Some v} = it \<inter> Collect P; P (k, v); (a, b) \<in> it; P (a, b); a \<noteq> k\<rbrakk> \<Longrightarrow> \<alpha> \<sigma> a = Some b
 5. \<And>\<sigma>. \<lbrakk>invar \<sigma>; {(k, v). \<alpha> \<sigma> k = Some v} = {(k, v). \<alpha> m k = Some v} \<inter> Collect P\<rbrakk> \<Longrightarrow> \<alpha> \<sigma> = \<alpha> m |` {k. \<exists>v. \<alpha> m k = Some v \<and> P (k, v)}
[PROOF STEP]
apply (auto split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>invar \<sigma>; {(k, v). \<alpha> \<sigma> k = Some v} = {(k, v). \<alpha> m k = Some v} \<inter> Collect P\<rbrakk> \<Longrightarrow> \<alpha> \<sigma> = \<alpha> m |` {k. \<exists>v. \<alpha> m k = Some v \<and> P (k, v)}
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>invar \<sigma>; {(k, v). \<alpha> \<sigma> k = Some v} = {(k, v). \<alpha> m k = Some v} \<inter> Collect P\<rbrakk> \<Longrightarrow> \<alpha> \<sigma> x = (\<alpha> m |` {k. \<exists>v. \<alpha> m k = Some v \<and> P (k, v)}) x
[PROOF STEP]
apply (auto simp: Map.restrict_map_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x v. \<lbrakk>invar \<sigma>; {(k, v). \<alpha> \<sigma> k = Some v} = {(k, v). \<alpha> m k = Some v} \<inter> Collect P; \<alpha> m x = Some v; P (x, v)\<rbrakk> \<Longrightarrow> \<alpha> \<sigma> x = Some v
 2. \<And>\<sigma> x. \<lbrakk>invar \<sigma>; {(k, v). \<alpha> \<sigma> k = Some v} = {(k, v). \<alpha> m k = Some v} \<inter> Collect P; \<forall>v. \<alpha> m x = Some v \<longrightarrow> \<not> P (x, v)\<rbrakk> \<Longrightarrow> \<alpha> \<sigma> x = None
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>invar \<sigma>; {(k, v). \<alpha> \<sigma> k = Some v} = {(k, v). \<alpha> m k = Some v} \<inter> Collect P; \<forall>v. \<alpha> m x = Some v \<longrightarrow> \<not> P (x, v)\<rbrakk> \<Longrightarrow> \<alpha> \<sigma> x = None
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>invar \<sigma>; {(k, v). \<alpha> \<sigma> k = Some v} = {(k, v). \<alpha> m k = Some v} \<inter> Collect P; \<forall>v. \<alpha> m x = Some v \<longrightarrow> \<not> P (x, v); \<alpha> \<sigma> x \<noteq> None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<alpha> (g_restrict P m) = \<alpha> m |` {k. \<exists>v. \<alpha> m k = Some v \<and> P (k, v)} \<and> invar (g_restrict P m)

goal (2 subgoals):
 1. \<And>m P. invar m \<Longrightarrow> \<alpha> (g_restrict P m) = \<alpha> m |` {k. \<exists>v. \<alpha> m k = Some v \<and> P (k, v)}
 2. \<And>m P. invar m \<Longrightarrow> invar (g_restrict P m)
[PROOF STEP]
thus "\<alpha> (g_restrict P m) = \<alpha> m |` {k. \<exists>v. \<alpha> m k = Some v \<and> P (k, v)}"
      "invar (g_restrict P m)"
[PROOF STATE]
proof (prove)
using this:
\<alpha> (g_restrict P m) = \<alpha> m |` {k. \<exists>v. \<alpha> m k = Some v \<and> P (k, v)} \<and> invar (g_restrict P m)

goal (1 subgoal):
 1. \<alpha> (g_restrict P m) = \<alpha> m |` {k. \<exists>v. \<alpha> m k = Some v \<and> P (k, v)} &&& invar (g_restrict P m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<alpha> (g_restrict P m) = \<alpha> m |` {k. \<exists>v. \<alpha> m k = Some v \<and> P (k, v)}
invar (g_restrict P m)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma g_min_impl: "map_min \<alpha> invar g_min"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_min \<alpha> invar g_min
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P \<noteq> {}\<rbrakk> \<Longrightarrow> g_min s P \<in> Some ` rel_of (\<alpha> s) P
 2. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> fst (the (g_min s P)) \<le> k
 3. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_min s P = None
[PROOF STEP]
fix m P
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P \<noteq> {}\<rbrakk> \<Longrightarrow> g_min s P \<in> Some ` rel_of (\<alpha> s) P
 2. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> fst (the (g_min s P)) \<le> k
 3. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_min s P = None
[PROOF STEP]
assume I: "invar m"
[PROOF STATE]
proof (state)
this:
invar m

goal (3 subgoals):
 1. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P \<noteq> {}\<rbrakk> \<Longrightarrow> g_min s P \<in> Some ` rel_of (\<alpha> s) P
 2. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> fst (the (g_min s P)) \<le> k
 3. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_min s P = None
[PROOF STEP]
from iterateoi_correct[OF I]
[PROOF STATE]
proof (chain)
picking this:
map_iterator_linord (iterateoi m) (\<alpha> m)
[PROOF STEP]
have iti': "map_iterator_linord (iterateoi m) (\<alpha> m)"
[PROOF STATE]
proof (prove)
using this:
map_iterator_linord (iterateoi m) (\<alpha> m)

goal (1 subgoal):
 1. map_iterator_linord (iterateoi m) (\<alpha> m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_iterator_linord (iterateoi m) (\<alpha> m)

goal (3 subgoals):
 1. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P \<noteq> {}\<rbrakk> \<Longrightarrow> g_min s P \<in> Some ` rel_of (\<alpha> s) P
 2. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> fst (the (g_min s P)) \<le> k
 3. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_min s P = None
[PROOF STEP]
note sel_correct = iterate_sel_no_map_map_linord_correct[OF iti', of P]
[PROOF STATE]
proof (state)
this:
(iterate_sel_no_map (iterateoi m) P = None) = (\<forall>k v. \<alpha> m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map (iterateoi m) P = Some (?k, ?v) \<Longrightarrow> \<alpha> m ?k = Some ?v \<and> P (?k, ?v) \<and> (\<forall>k' v'. \<alpha> m k' = Some v' \<and> P (k', v') \<longrightarrow> ?k \<le> k')

goal (3 subgoals):
 1. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P \<noteq> {}\<rbrakk> \<Longrightarrow> g_min s P \<in> Some ` rel_of (\<alpha> s) P
 2. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> fst (the (g_min s P)) \<le> k
 3. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_min s P = None
[PROOF STEP]
have A: "g_min m P = iterate_sel_no_map (iterateoi m) P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g_min m P = iterate_sel_no_map (iterateoi m) P
[PROOF STEP]
unfolding g_min_def iterate_sel_no_map_def iterate_sel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iterateoi m (\<lambda>\<sigma>. \<sigma> = None) (\<lambda>x \<sigma>. if P x then Some x else None) None = iterateoi m (\<lambda>\<sigma>. \<sigma> = None) (\<lambda>x \<sigma>. if P x then Some x else None) None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g_min m P = iterate_sel_no_map (iterateoi m) P

goal (3 subgoals):
 1. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P \<noteq> {}\<rbrakk> \<Longrightarrow> g_min s P \<in> Some ` rel_of (\<alpha> s) P
 2. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> fst (the (g_min s P)) \<le> k
 3. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_min s P = None
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
g_min m P = iterate_sel_no_map (iterateoi m) P

goal (3 subgoals):
 1. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P \<noteq> {}\<rbrakk> \<Longrightarrow> g_min s P \<in> Some ` rel_of (\<alpha> s) P
 2. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> fst (the (g_min s P)) \<le> k
 3. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_min s P = None
[PROOF STEP]
assume "rel_of (\<alpha> m) P \<noteq> {}"
[PROOF STATE]
proof (state)
this:
rel_of (\<alpha> m) P \<noteq> {}

goal (3 subgoals):
 1. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P \<noteq> {}\<rbrakk> \<Longrightarrow> g_min s P \<in> Some ` rel_of (\<alpha> s) P
 2. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> fst (the (g_min s P)) \<le> k
 3. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_min s P = None
[PROOF STEP]
with sel_correct
[PROOF STATE]
proof (chain)
picking this:
(iterate_sel_no_map (iterateoi m) P = None) = (\<forall>k v. \<alpha> m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map (iterateoi m) P = Some (?k, ?v) \<Longrightarrow> \<alpha> m ?k = Some ?v \<and> P (?k, ?v) \<and> (\<forall>k' v'. \<alpha> m k' = Some v' \<and> P (k', v') \<longrightarrow> ?k \<le> k')
rel_of (\<alpha> m) P \<noteq> {}
[PROOF STEP]
show "g_min m P \<in> Some ` rel_of (\<alpha> m) P"
[PROOF STATE]
proof (prove)
using this:
(iterate_sel_no_map (iterateoi m) P = None) = (\<forall>k v. \<alpha> m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map (iterateoi m) P = Some (?k, ?v) \<Longrightarrow> \<alpha> m ?k = Some ?v \<and> P (?k, ?v) \<and> (\<forall>k' v'. \<alpha> m k' = Some v' \<and> P (k', v') \<longrightarrow> ?k \<le> k')
rel_of (\<alpha> m) P \<noteq> {}

goal (1 subgoal):
 1. g_min m P \<in> Some ` rel_of (\<alpha> m) P
[PROOF STEP]
unfolding A
[PROOF STATE]
proof (prove)
using this:
(iterate_sel_no_map (iterateoi m) P = None) = (\<forall>k v. \<alpha> m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map (iterateoi m) P = Some (?k, ?v) \<Longrightarrow> \<alpha> m ?k = Some ?v \<and> P (?k, ?v) \<and> (\<forall>k' v'. \<alpha> m k' = Some v' \<and> P (k', v') \<longrightarrow> ?k \<le> k')
rel_of (\<alpha> m) P \<noteq> {}

goal (1 subgoal):
 1. iterate_sel_no_map (iterateoi m) P \<in> Some ` rel_of (\<alpha> m) P
[PROOF STEP]
by (auto simp add: image_iff rel_of_def)
[PROOF STATE]
proof (state)
this:
g_min m P \<in> Some ` rel_of (\<alpha> m) P

goal (2 subgoals):
 1. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> fst (the (g_min s P)) \<le> k
 2. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_min s P = None
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
rel_of (\<alpha> m) P \<noteq> {} \<Longrightarrow> g_min m P \<in> Some ` rel_of (\<alpha> m) P

goal (2 subgoals):
 1. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> fst (the (g_min s P)) \<le> k
 2. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_min s P = None
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
rel_of (\<alpha> m) P \<noteq> {} \<Longrightarrow> g_min m P \<in> Some ` rel_of (\<alpha> m) P

goal (2 subgoals):
 1. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> fst (the (g_min s P)) \<le> k
 2. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_min s P = None
[PROOF STEP]
assume "rel_of (\<alpha> m) P = {}"
[PROOF STATE]
proof (state)
this:
rel_of (\<alpha> m) P = {}

goal (2 subgoals):
 1. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> fst (the (g_min s P)) \<le> k
 2. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_min s P = None
[PROOF STEP]
with sel_correct
[PROOF STATE]
proof (chain)
picking this:
(iterate_sel_no_map (iterateoi m) P = None) = (\<forall>k v. \<alpha> m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map (iterateoi m) P = Some (?k, ?v) \<Longrightarrow> \<alpha> m ?k = Some ?v \<and> P (?k, ?v) \<and> (\<forall>k' v'. \<alpha> m k' = Some v' \<and> P (k', v') \<longrightarrow> ?k \<le> k')
rel_of (\<alpha> m) P = {}
[PROOF STEP]
show "g_min m P = None"
[PROOF STATE]
proof (prove)
using this:
(iterate_sel_no_map (iterateoi m) P = None) = (\<forall>k v. \<alpha> m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map (iterateoi m) P = Some (?k, ?v) \<Longrightarrow> \<alpha> m ?k = Some ?v \<and> P (?k, ?v) \<and> (\<forall>k' v'. \<alpha> m k' = Some v' \<and> P (k', v') \<longrightarrow> ?k \<le> k')
rel_of (\<alpha> m) P = {}

goal (1 subgoal):
 1. g_min m P = None
[PROOF STEP]
unfolding A
[PROOF STATE]
proof (prove)
using this:
(iterate_sel_no_map (iterateoi m) P = None) = (\<forall>k v. \<alpha> m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map (iterateoi m) P = Some (?k, ?v) \<Longrightarrow> \<alpha> m ?k = Some ?v \<and> P (?k, ?v) \<and> (\<forall>k' v'. \<alpha> m k' = Some v' \<and> P (k', v') \<longrightarrow> ?k \<le> k')
rel_of (\<alpha> m) P = {}

goal (1 subgoal):
 1. iterate_sel_no_map (iterateoi m) P = None
[PROOF STEP]
by (auto simp add: image_iff rel_of_def)
[PROOF STATE]
proof (state)
this:
g_min m P = None

goal (1 subgoal):
 1. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> fst (the (g_min s P)) \<le> k
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
rel_of (\<alpha> m) P = {} \<Longrightarrow> g_min m P = None

goal (1 subgoal):
 1. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> fst (the (g_min s P)) \<le> k
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
rel_of (\<alpha> m) P = {} \<Longrightarrow> g_min m P = None

goal (1 subgoal):
 1. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> fst (the (g_min s P)) \<le> k
[PROOF STEP]
fix k v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> fst (the (g_min s P)) \<le> k
[PROOF STEP]
assume "(k, v) \<in> rel_of (\<alpha> m) P"
[PROOF STATE]
proof (state)
this:
(k, v) \<in> rel_of (\<alpha> m) P

goal (1 subgoal):
 1. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> fst (the (g_min s P)) \<le> k
[PROOF STEP]
with sel_correct
[PROOF STATE]
proof (chain)
picking this:
(iterate_sel_no_map (iterateoi m) P = None) = (\<forall>k v. \<alpha> m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map (iterateoi m) P = Some (?k, ?v) \<Longrightarrow> \<alpha> m ?k = Some ?v \<and> P (?k, ?v) \<and> (\<forall>k' v'. \<alpha> m k' = Some v' \<and> P (k', v') \<longrightarrow> ?k \<le> k')
(k, v) \<in> rel_of (\<alpha> m) P
[PROOF STEP]
show "fst (the (g_min m P)) \<le> k"
[PROOF STATE]
proof (prove)
using this:
(iterate_sel_no_map (iterateoi m) P = None) = (\<forall>k v. \<alpha> m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map (iterateoi m) P = Some (?k, ?v) \<Longrightarrow> \<alpha> m ?k = Some ?v \<and> P (?k, ?v) \<and> (\<forall>k' v'. \<alpha> m k' = Some v' \<and> P (k', v') \<longrightarrow> ?k \<le> k')
(k, v) \<in> rel_of (\<alpha> m) P

goal (1 subgoal):
 1. fst (the (g_min m P)) \<le> k
[PROOF STEP]
unfolding A
[PROOF STATE]
proof (prove)
using this:
(iterate_sel_no_map (iterateoi m) P = None) = (\<forall>k v. \<alpha> m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map (iterateoi m) P = Some (?k, ?v) \<Longrightarrow> \<alpha> m ?k = Some ?v \<and> P (?k, ?v) \<and> (\<forall>k' v'. \<alpha> m k' = Some v' \<and> P (k', v') \<longrightarrow> ?k \<le> k')
(k, v) \<in> rel_of (\<alpha> m) P

goal (1 subgoal):
 1. fst (the (iterate_sel_no_map (iterateoi m) P)) \<le> k
[PROOF STEP]
by (auto simp add: image_iff rel_of_def)
[PROOF STATE]
proof (state)
this:
fst (the (g_min m P)) \<le> k

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?k7, ?v7) \<in> rel_of (\<alpha> m) P \<Longrightarrow> fst (the (g_min m P)) \<le> ?k7

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma g_max_impl: "map_max \<alpha> invar g_max"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_max \<alpha> invar g_max
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P \<noteq> {}\<rbrakk> \<Longrightarrow> g_max s P \<in> Some ` rel_of (\<alpha> s) P
 2. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> k \<le> fst (the (g_max s P))
 3. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_max s P = None
[PROOF STEP]
fix m P
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P \<noteq> {}\<rbrakk> \<Longrightarrow> g_max s P \<in> Some ` rel_of (\<alpha> s) P
 2. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> k \<le> fst (the (g_max s P))
 3. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_max s P = None
[PROOF STEP]
assume I: "invar m"
[PROOF STATE]
proof (state)
this:
invar m

goal (3 subgoals):
 1. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P \<noteq> {}\<rbrakk> \<Longrightarrow> g_max s P \<in> Some ` rel_of (\<alpha> s) P
 2. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> k \<le> fst (the (g_max s P))
 3. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_max s P = None
[PROOF STEP]
from rev_iterateoi_correct[OF I]
[PROOF STATE]
proof (chain)
picking this:
map_iterator_rev_linord (reverse_iterateoi m) (\<alpha> m)
[PROOF STEP]
have iti': "map_iterator_rev_linord (rev_iterateoi m) (\<alpha> m)"
[PROOF STATE]
proof (prove)
using this:
map_iterator_rev_linord (reverse_iterateoi m) (\<alpha> m)

goal (1 subgoal):
 1. map_iterator_rev_linord (reverse_iterateoi m) (\<alpha> m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_iterator_rev_linord (reverse_iterateoi m) (\<alpha> m)

goal (3 subgoals):
 1. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P \<noteq> {}\<rbrakk> \<Longrightarrow> g_max s P \<in> Some ` rel_of (\<alpha> s) P
 2. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> k \<le> fst (the (g_max s P))
 3. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_max s P = None
[PROOF STEP]
note sel_correct = iterate_sel_no_map_map_rev_linord_correct[OF iti', of P]
[PROOF STATE]
proof (state)
this:
(iterate_sel_no_map (reverse_iterateoi m) P = None) = (\<forall>k v. \<alpha> m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map (reverse_iterateoi m) P = Some (?k, ?v) \<Longrightarrow> \<alpha> m ?k = Some ?v \<and> P (?k, ?v) \<and> (\<forall>k' v'. \<alpha> m k' = Some v' \<and> P (k', v') \<longrightarrow> k' \<le> ?k)

goal (3 subgoals):
 1. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P \<noteq> {}\<rbrakk> \<Longrightarrow> g_max s P \<in> Some ` rel_of (\<alpha> s) P
 2. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> k \<le> fst (the (g_max s P))
 3. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_max s P = None
[PROOF STEP]
have A: "g_max m P = iterate_sel_no_map (rev_iterateoi m) P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g_max m P = iterate_sel_no_map (reverse_iterateoi m) P
[PROOF STEP]
unfolding g_max_def iterate_sel_no_map_def iterate_sel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reverse_iterateoi m (\<lambda>\<sigma>. \<sigma> = None) (\<lambda>x \<sigma>. if P x then Some x else None) None = reverse_iterateoi m (\<lambda>\<sigma>. \<sigma> = None) (\<lambda>x \<sigma>. if P x then Some x else None) None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g_max m P = iterate_sel_no_map (reverse_iterateoi m) P

goal (3 subgoals):
 1. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P \<noteq> {}\<rbrakk> \<Longrightarrow> g_max s P \<in> Some ` rel_of (\<alpha> s) P
 2. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> k \<le> fst (the (g_max s P))
 3. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_max s P = None
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
g_max m P = iterate_sel_no_map (reverse_iterateoi m) P

goal (3 subgoals):
 1. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P \<noteq> {}\<rbrakk> \<Longrightarrow> g_max s P \<in> Some ` rel_of (\<alpha> s) P
 2. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> k \<le> fst (the (g_max s P))
 3. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_max s P = None
[PROOF STEP]
assume "rel_of (\<alpha> m) P \<noteq> {}"
[PROOF STATE]
proof (state)
this:
rel_of (\<alpha> m) P \<noteq> {}

goal (3 subgoals):
 1. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P \<noteq> {}\<rbrakk> \<Longrightarrow> g_max s P \<in> Some ` rel_of (\<alpha> s) P
 2. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> k \<le> fst (the (g_max s P))
 3. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_max s P = None
[PROOF STEP]
with sel_correct
[PROOF STATE]
proof (chain)
picking this:
(iterate_sel_no_map (reverse_iterateoi m) P = None) = (\<forall>k v. \<alpha> m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map (reverse_iterateoi m) P = Some (?k, ?v) \<Longrightarrow> \<alpha> m ?k = Some ?v \<and> P (?k, ?v) \<and> (\<forall>k' v'. \<alpha> m k' = Some v' \<and> P (k', v') \<longrightarrow> k' \<le> ?k)
rel_of (\<alpha> m) P \<noteq> {}
[PROOF STEP]
show "g_max m P \<in> Some ` rel_of (\<alpha> m) P"
[PROOF STATE]
proof (prove)
using this:
(iterate_sel_no_map (reverse_iterateoi m) P = None) = (\<forall>k v. \<alpha> m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map (reverse_iterateoi m) P = Some (?k, ?v) \<Longrightarrow> \<alpha> m ?k = Some ?v \<and> P (?k, ?v) \<and> (\<forall>k' v'. \<alpha> m k' = Some v' \<and> P (k', v') \<longrightarrow> k' \<le> ?k)
rel_of (\<alpha> m) P \<noteq> {}

goal (1 subgoal):
 1. g_max m P \<in> Some ` rel_of (\<alpha> m) P
[PROOF STEP]
unfolding A
[PROOF STATE]
proof (prove)
using this:
(iterate_sel_no_map (reverse_iterateoi m) P = None) = (\<forall>k v. \<alpha> m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map (reverse_iterateoi m) P = Some (?k, ?v) \<Longrightarrow> \<alpha> m ?k = Some ?v \<and> P (?k, ?v) \<and> (\<forall>k' v'. \<alpha> m k' = Some v' \<and> P (k', v') \<longrightarrow> k' \<le> ?k)
rel_of (\<alpha> m) P \<noteq> {}

goal (1 subgoal):
 1. iterate_sel_no_map (reverse_iterateoi m) P \<in> Some ` rel_of (\<alpha> m) P
[PROOF STEP]
by (auto simp add: image_iff rel_of_def)
[PROOF STATE]
proof (state)
this:
g_max m P \<in> Some ` rel_of (\<alpha> m) P

goal (2 subgoals):
 1. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> k \<le> fst (the (g_max s P))
 2. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_max s P = None
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
rel_of (\<alpha> m) P \<noteq> {} \<Longrightarrow> g_max m P \<in> Some ` rel_of (\<alpha> m) P

goal (2 subgoals):
 1. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> k \<le> fst (the (g_max s P))
 2. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_max s P = None
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
rel_of (\<alpha> m) P \<noteq> {} \<Longrightarrow> g_max m P \<in> Some ` rel_of (\<alpha> m) P

goal (2 subgoals):
 1. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> k \<le> fst (the (g_max s P))
 2. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_max s P = None
[PROOF STEP]
assume "rel_of (\<alpha> m) P = {}"
[PROOF STATE]
proof (state)
this:
rel_of (\<alpha> m) P = {}

goal (2 subgoals):
 1. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> k \<le> fst (the (g_max s P))
 2. \<And>s P. \<lbrakk>invar s; rel_of (\<alpha> s) P = {}\<rbrakk> \<Longrightarrow> g_max s P = None
[PROOF STEP]
with sel_correct
[PROOF STATE]
proof (chain)
picking this:
(iterate_sel_no_map (reverse_iterateoi m) P = None) = (\<forall>k v. \<alpha> m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map (reverse_iterateoi m) P = Some (?k, ?v) \<Longrightarrow> \<alpha> m ?k = Some ?v \<and> P (?k, ?v) \<and> (\<forall>k' v'. \<alpha> m k' = Some v' \<and> P (k', v') \<longrightarrow> k' \<le> ?k)
rel_of (\<alpha> m) P = {}
[PROOF STEP]
show "g_max m P = None"
[PROOF STATE]
proof (prove)
using this:
(iterate_sel_no_map (reverse_iterateoi m) P = None) = (\<forall>k v. \<alpha> m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map (reverse_iterateoi m) P = Some (?k, ?v) \<Longrightarrow> \<alpha> m ?k = Some ?v \<and> P (?k, ?v) \<and> (\<forall>k' v'. \<alpha> m k' = Some v' \<and> P (k', v') \<longrightarrow> k' \<le> ?k)
rel_of (\<alpha> m) P = {}

goal (1 subgoal):
 1. g_max m P = None
[PROOF STEP]
unfolding A
[PROOF STATE]
proof (prove)
using this:
(iterate_sel_no_map (reverse_iterateoi m) P = None) = (\<forall>k v. \<alpha> m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map (reverse_iterateoi m) P = Some (?k, ?v) \<Longrightarrow> \<alpha> m ?k = Some ?v \<and> P (?k, ?v) \<and> (\<forall>k' v'. \<alpha> m k' = Some v' \<and> P (k', v') \<longrightarrow> k' \<le> ?k)
rel_of (\<alpha> m) P = {}

goal (1 subgoal):
 1. iterate_sel_no_map (reverse_iterateoi m) P = None
[PROOF STEP]
by (auto simp add: image_iff rel_of_def)
[PROOF STATE]
proof (state)
this:
g_max m P = None

goal (1 subgoal):
 1. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> k \<le> fst (the (g_max s P))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
rel_of (\<alpha> m) P = {} \<Longrightarrow> g_max m P = None

goal (1 subgoal):
 1. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> k \<le> fst (the (g_max s P))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
rel_of (\<alpha> m) P = {} \<Longrightarrow> g_max m P = None

goal (1 subgoal):
 1. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> k \<le> fst (the (g_max s P))
[PROOF STEP]
fix k v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> k \<le> fst (the (g_max s P))
[PROOF STEP]
assume "(k, v) \<in> rel_of (\<alpha> m) P"
[PROOF STATE]
proof (state)
this:
(k, v) \<in> rel_of (\<alpha> m) P

goal (1 subgoal):
 1. \<And>s k v P. \<lbrakk>invar s; (k, v) \<in> rel_of (\<alpha> s) P\<rbrakk> \<Longrightarrow> k \<le> fst (the (g_max s P))
[PROOF STEP]
with sel_correct
[PROOF STATE]
proof (chain)
picking this:
(iterate_sel_no_map (reverse_iterateoi m) P = None) = (\<forall>k v. \<alpha> m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map (reverse_iterateoi m) P = Some (?k, ?v) \<Longrightarrow> \<alpha> m ?k = Some ?v \<and> P (?k, ?v) \<and> (\<forall>k' v'. \<alpha> m k' = Some v' \<and> P (k', v') \<longrightarrow> k' \<le> ?k)
(k, v) \<in> rel_of (\<alpha> m) P
[PROOF STEP]
show "fst (the (g_max m P)) \<ge> k"
[PROOF STATE]
proof (prove)
using this:
(iterate_sel_no_map (reverse_iterateoi m) P = None) = (\<forall>k v. \<alpha> m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map (reverse_iterateoi m) P = Some (?k, ?v) \<Longrightarrow> \<alpha> m ?k = Some ?v \<and> P (?k, ?v) \<and> (\<forall>k' v'. \<alpha> m k' = Some v' \<and> P (k', v') \<longrightarrow> k' \<le> ?k)
(k, v) \<in> rel_of (\<alpha> m) P

goal (1 subgoal):
 1. k \<le> fst (the (g_max m P))
[PROOF STEP]
unfolding A
[PROOF STATE]
proof (prove)
using this:
(iterate_sel_no_map (reverse_iterateoi m) P = None) = (\<forall>k v. \<alpha> m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map (reverse_iterateoi m) P = Some (?k, ?v) \<Longrightarrow> \<alpha> m ?k = Some ?v \<and> P (?k, ?v) \<and> (\<forall>k' v'. \<alpha> m k' = Some v' \<and> P (k', v') \<longrightarrow> k' \<le> ?k)
(k, v) \<in> rel_of (\<alpha> m) P

goal (1 subgoal):
 1. k \<le> fst (the (iterate_sel_no_map (reverse_iterateoi m) P))
[PROOF STEP]
by (auto simp add: image_iff rel_of_def)
[PROOF STATE]
proof (state)
this:
k \<le> fst (the (g_max m P))

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?k7, ?v7) \<in> rel_of (\<alpha> m) P \<Longrightarrow> ?k7 \<le> fst (the (g_max m P))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma g_to_sorted_list_impl: "map_to_sorted_list \<alpha> invar g_to_sorted_list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MapSpec.map_to_sorted_list \<alpha> invar g_to_sorted_list
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>m. invar m \<Longrightarrow> map_of (g_to_sorted_list m) = \<alpha> m
 2. \<And>m. invar m \<Longrightarrow> distinct (map fst (g_to_sorted_list m))
 3. \<And>m. invar m \<Longrightarrow> sorted (map fst (g_to_sorted_list m))
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>m. invar m \<Longrightarrow> map_of (g_to_sorted_list m) = \<alpha> m
 2. \<And>m. invar m \<Longrightarrow> distinct (map fst (g_to_sorted_list m))
 3. \<And>m. invar m \<Longrightarrow> sorted (map fst (g_to_sorted_list m))
[PROOF STEP]
assume I: "invar m"
[PROOF STATE]
proof (state)
this:
invar m

goal (3 subgoals):
 1. \<And>m. invar m \<Longrightarrow> map_of (g_to_sorted_list m) = \<alpha> m
 2. \<And>m. invar m \<Longrightarrow> distinct (map fst (g_to_sorted_list m))
 3. \<And>m. invar m \<Longrightarrow> sorted (map fst (g_to_sorted_list m))
[PROOF STEP]
note iti = rev_iterateoi_correct[OF I]
[PROOF STATE]
proof (state)
this:
map_iterator_rev_linord (reverse_iterateoi m) (\<alpha> m)

goal (3 subgoals):
 1. \<And>m. invar m \<Longrightarrow> map_of (g_to_sorted_list m) = \<alpha> m
 2. \<And>m. invar m \<Longrightarrow> distinct (map fst (g_to_sorted_list m))
 3. \<And>m. invar m \<Longrightarrow> sorted (map fst (g_to_sorted_list m))
[PROOF STEP]
from iterate_to_list_map_rev_linord_correct[OF iti]
[PROOF STATE]
proof (chain)
picking this:
map_of (iterate_to_list (reverse_iterateoi m)) = \<alpha> m \<and> distinct (map fst (iterate_to_list (reverse_iterateoi m))) \<and> sorted (map fst (iterate_to_list (reverse_iterateoi m)))
[PROOF STEP]
show "sorted (map fst (g_to_sorted_list m))"
         "distinct (map fst (g_to_sorted_list m))"
         "map_of (g_to_sorted_list m) = \<alpha> m"
[PROOF STATE]
proof (prove)
using this:
map_of (iterate_to_list (reverse_iterateoi m)) = \<alpha> m \<and> distinct (map fst (iterate_to_list (reverse_iterateoi m))) \<and> sorted (map fst (iterate_to_list (reverse_iterateoi m)))

goal (1 subgoal):
 1. sorted (map fst (g_to_sorted_list m)) &&& distinct (map fst (g_to_sorted_list m)) &&& map_of (g_to_sorted_list m) = \<alpha> m
[PROOF STEP]
unfolding g_to_sorted_list_def iterate_to_list_def
[PROOF STATE]
proof (prove)
using this:
map_of (reverse_iterateo m (#) []) = \<alpha> m \<and> distinct (map fst (reverse_iterateo m (#) [])) \<and> sorted (map fst (reverse_iterateo m (#) []))

goal (1 subgoal):
 1. sorted (map fst (reverse_iterateo m (#) [])) &&& distinct (map fst (reverse_iterateo m (#) [])) &&& map_of (reverse_iterateo m (#) []) = \<alpha> m
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
sorted (map fst (g_to_sorted_list m))
distinct (map fst (g_to_sorted_list m))
map_of (g_to_sorted_list m) = \<alpha> m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma g_to_rev_list_impl: "map_to_rev_list \<alpha> invar g_to_rev_list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_to_rev_list \<alpha> invar g_to_rev_list
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>m. invar m \<Longrightarrow> map_of (g_to_rev_list m) = \<alpha> m
 2. \<And>m. invar m \<Longrightarrow> distinct (map fst (g_to_rev_list m))
 3. \<And>m. invar m \<Longrightarrow> sorted (rev (map fst (g_to_rev_list m)))
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>m. invar m \<Longrightarrow> map_of (g_to_rev_list m) = \<alpha> m
 2. \<And>m. invar m \<Longrightarrow> distinct (map fst (g_to_rev_list m))
 3. \<And>m. invar m \<Longrightarrow> sorted (rev (map fst (g_to_rev_list m)))
[PROOF STEP]
assume I: "invar m"
[PROOF STATE]
proof (state)
this:
invar m

goal (3 subgoals):
 1. \<And>m. invar m \<Longrightarrow> map_of (g_to_rev_list m) = \<alpha> m
 2. \<And>m. invar m \<Longrightarrow> distinct (map fst (g_to_rev_list m))
 3. \<And>m. invar m \<Longrightarrow> sorted (rev (map fst (g_to_rev_list m)))
[PROOF STEP]
note iti = iterateoi_correct[OF I]
[PROOF STATE]
proof (state)
this:
map_iterator_linord (iterateoi m) (\<alpha> m)

goal (3 subgoals):
 1. \<And>m. invar m \<Longrightarrow> map_of (g_to_rev_list m) = \<alpha> m
 2. \<And>m. invar m \<Longrightarrow> distinct (map fst (g_to_rev_list m))
 3. \<And>m. invar m \<Longrightarrow> sorted (rev (map fst (g_to_rev_list m)))
[PROOF STEP]
from iterate_to_list_map_linord_correct[OF iti]
[PROOF STATE]
proof (chain)
picking this:
map_of (iterate_to_list (iterateoi m)) = \<alpha> m \<and> distinct (map fst (iterate_to_list (iterateoi m))) \<and> sorted (map fst (rev (iterate_to_list (iterateoi m))))
[PROOF STEP]
show "sorted (rev (map fst (g_to_rev_list m)))"
         "distinct (map fst (g_to_rev_list m))"
         "map_of (g_to_rev_list m) = \<alpha> m"
[PROOF STATE]
proof (prove)
using this:
map_of (iterate_to_list (iterateoi m)) = \<alpha> m \<and> distinct (map fst (iterate_to_list (iterateoi m))) \<and> sorted (map fst (rev (iterate_to_list (iterateoi m))))

goal (1 subgoal):
 1. sorted (rev (map fst (g_to_rev_list m))) &&& distinct (map fst (g_to_rev_list m)) &&& map_of (g_to_rev_list m) = \<alpha> m
[PROOF STEP]
unfolding g_to_rev_list_def iterate_to_list_def
[PROOF STATE]
proof (prove)
using this:
map_of (iterateo m (#) []) = \<alpha> m \<and> distinct (map fst (iterateo m (#) [])) \<and> sorted (map fst (rev (iterateo m (#) [])))

goal (1 subgoal):
 1. sorted (rev (map fst (iterateo m (#) []))) &&& distinct (map fst (iterateo m (#) [])) &&& map_of (iterateo m (#) []) = \<alpha> m
[PROOF STEP]
by (simp_all add: rev_map)
[PROOF STATE]
proof (state)
this:
sorted (rev (map fst (g_to_rev_list m)))
distinct (map fst (g_to_rev_list m))
map_of (g_to_rev_list m) = \<alpha> m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dflt_oops_impl: "StdOMap dflt_oops"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. StdOMap dflt_oops
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. StdOMap dflt_oops
[PROOF STEP]
interpret aux: StdMap dflt_ops
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. StdMap dflt_ops
[PROOF STEP]
by (rule dflt_ops_impl)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. StdOMap dflt_oops
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. StdOMap dflt_oops
[PROOF STEP]
apply (rule StdOMap_intro)
[PROOF STATE]
proof (prove)
goal (25 subgoals):
 1. map_empty (map_op_\<alpha> dflt_oops) (map_op_invar dflt_oops) (map_op_empty dflt_oops)
 2. map_lookup (map_op_\<alpha> dflt_oops) (map_op_invar dflt_oops) (map_op_lookup dflt_oops)
 3. map_update (map_op_\<alpha> dflt_oops) (map_op_invar dflt_oops) (map_op_update dflt_oops)
 4. map_update_dj (map_op_\<alpha> dflt_oops) (map_op_invar dflt_oops) (map_op_update_dj dflt_oops)
 5. map_delete (map_op_\<alpha> dflt_oops) (map_op_invar dflt_oops) (map_op_delete dflt_oops)
 6. poly_map_iteratei (map_op_\<alpha> dflt_oops) (map_op_invar dflt_oops) (map_op_list_it dflt_oops)
 7. map_sng (map_op_\<alpha> dflt_oops) (map_op_invar dflt_oops) (map_op_sng dflt_oops)
 8. map_restrict (map_op_\<alpha> dflt_oops) (map_op_invar dflt_oops) (map_op_\<alpha> dflt_oops) (map_op_invar dflt_oops) (map_op_restrict dflt_oops)
 9. MapSpec.map_add (map_op_\<alpha> dflt_oops) (map_op_invar dflt_oops) (map_op_add dflt_oops)
 10. map_add_dj (map_op_\<alpha> dflt_oops) (map_op_invar dflt_oops) (map_op_add_dj dflt_oops)
A total of 25 subgoals...
[PROOF STEP]
apply icf_locales
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. map_min (map_op_\<alpha> dflt_oops) (map_op_invar dflt_oops) (map_op_min dflt_oops)
 2. map_max (map_op_\<alpha> dflt_oops) (map_op_invar dflt_oops) (map_op_max dflt_oops)
 3. MapSpec.map_to_sorted_list (map_op_\<alpha> dflt_oops) (map_op_invar dflt_oops) (map_op_to_sorted_list dflt_oops)
 4. map_to_rev_list (map_op_\<alpha> dflt_oops) (map_op_invar dflt_oops) (map_op_to_rev_list dflt_oops)
[PROOF STEP]
apply (simp_all add: icf_rec_unf)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. map_min \<alpha> invar g_min
 2. map_max \<alpha> invar g_max
 3. MapSpec.map_to_sorted_list \<alpha> invar g_to_sorted_list
 4. map_to_rev_list \<alpha> invar g_to_rev_list
[PROOF STEP]
apply (rule g_min_impl)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. map_max \<alpha> invar g_max
 2. MapSpec.map_to_sorted_list \<alpha> invar g_to_sorted_list
 3. map_to_rev_list \<alpha> invar g_to_rev_list
[PROOF STEP]
apply (rule g_max_impl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. MapSpec.map_to_sorted_list \<alpha> invar g_to_sorted_list
 2. map_to_rev_list \<alpha> invar g_to_rev_list
[PROOF STEP]
apply (rule g_to_sorted_list_impl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_to_rev_list \<alpha> invar g_to_rev_list
[PROOF STEP]
apply (rule g_to_rev_list_impl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
StdOMap dflt_oops

goal:
No subgoals!
[PROOF STEP]
qed