[STATEMENT]
lemma set_iterator_abs_genord_I2 :
  assumes it_OK: "set_iterator_genord iti S0 Rc"
      and R_OK: "\<And>xc1 xc2. \<lbrakk>invar xc1; invar xc2; Rc xc1 xc2\<rbrakk> \<Longrightarrow> Ra (\<alpha> xc1) (\<alpha> xc2)"
      and dist: "\<And>xc1 xc2. \<lbrakk>invar xc1; invar xc2; xc1 \<in> S0; xc2 \<in> S0; \<alpha> xc1 = \<alpha> xc2\<rbrakk> \<Longrightarrow> xc1 = xc2"
      and invar: "\<And>xc. xc \<in> S0 \<Longrightarrow> invar xc"
      and S0'_eq: "S0' = \<alpha> ` S0"
  shows "set_iterator_abs_genord \<alpha> invar iti S0' Ra"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_abs_genord \<alpha> invar iti S0' Ra
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set_iterator_abs_genord \<alpha> invar iti S0' Ra
[PROOF STEP]
from it_OK
[PROOF STATE]
proof (chain)
picking this:
set_iterator_genord iti S0 Rc
[PROOF STEP]
obtain l0 where dist_l0: "distinct l0" and
          S0_eq: "S0 = set l0" and
          sort_Rc: "sorted_wrt Rc l0"  and iti_eq: "iti = foldli l0"
[PROOF STATE]
proof (prove)
using this:
set_iterator_genord iti S0 Rc

goal (1 subgoal):
 1. (\<And>l0. \<lbrakk>distinct l0; S0 = set l0; sorted_wrt Rc l0; iti = foldli l0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding set_iterator_genord_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l0. distinct l0 \<and> S0 = set l0 \<and> sorted_wrt Rc l0 \<and> iti = foldli l0

goal (1 subgoal):
 1. (\<And>l0. \<lbrakk>distinct l0; S0 = set l0; sorted_wrt Rc l0; iti = foldli l0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct l0
S0 = set l0
sorted_wrt Rc l0
iti = foldli l0

goal (1 subgoal):
 1. set_iterator_abs_genord \<alpha> invar iti S0' Ra
[PROOF STEP]
have "set l0 \<subseteq> S0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set l0 \<subseteq> S0
[PROOF STEP]
unfolding S0_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set l0 \<subseteq> set l0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set l0 \<subseteq> S0

goal (1 subgoal):
 1. set_iterator_abs_genord \<alpha> invar iti S0' Ra
[PROOF STEP]
with dist_l0 sort_Rc
[PROOF STATE]
proof (chain)
picking this:
distinct l0
sorted_wrt Rc l0
set l0 \<subseteq> S0
[PROOF STEP]
have map_props: "distinct (map \<alpha> l0) \<and> sorted_wrt Ra (map \<alpha> l0)"
[PROOF STATE]
proof (prove)
using this:
distinct l0
sorted_wrt Rc l0
set l0 \<subseteq> S0

goal (1 subgoal):
 1. distinct (map \<alpha> l0) \<and> sorted_wrt Ra (map \<alpha> l0)
[PROOF STEP]
proof (induct l0)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>distinct []; sorted_wrt Rc []; set [] \<subseteq> S0\<rbrakk> \<Longrightarrow> distinct (map \<alpha> []) \<and> sorted_wrt Ra (map \<alpha> [])
 2. \<And>a l0. \<lbrakk>\<lbrakk>distinct l0; sorted_wrt Rc l0; set l0 \<subseteq> S0\<rbrakk> \<Longrightarrow> distinct (map \<alpha> l0) \<and> sorted_wrt Ra (map \<alpha> l0); distinct (a # l0); sorted_wrt Rc (a # l0); set (a # l0) \<subseteq> S0\<rbrakk> \<Longrightarrow> distinct (map \<alpha> (a # l0)) \<and> sorted_wrt Ra (map \<alpha> (a # l0))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
distinct []
sorted_wrt Rc []
set [] \<subseteq> S0

goal (2 subgoals):
 1. \<lbrakk>distinct []; sorted_wrt Rc []; set [] \<subseteq> S0\<rbrakk> \<Longrightarrow> distinct (map \<alpha> []) \<and> sorted_wrt Ra (map \<alpha> [])
 2. \<And>a l0. \<lbrakk>\<lbrakk>distinct l0; sorted_wrt Rc l0; set l0 \<subseteq> S0\<rbrakk> \<Longrightarrow> distinct (map \<alpha> l0) \<and> sorted_wrt Ra (map \<alpha> l0); distinct (a # l0); sorted_wrt Rc (a # l0); set (a # l0) \<subseteq> S0\<rbrakk> \<Longrightarrow> distinct (map \<alpha> (a # l0)) \<and> sorted_wrt Ra (map \<alpha> (a # l0))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
distinct []
sorted_wrt Rc []
set [] \<subseteq> S0

goal (1 subgoal):
 1. distinct (map \<alpha> []) \<and> sorted_wrt Ra (map \<alpha> [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (map \<alpha> []) \<and> sorted_wrt Ra (map \<alpha> [])

goal (1 subgoal):
 1. \<And>a l0. \<lbrakk>\<lbrakk>distinct l0; sorted_wrt Rc l0; set l0 \<subseteq> S0\<rbrakk> \<Longrightarrow> distinct (map \<alpha> l0) \<and> sorted_wrt Ra (map \<alpha> l0); distinct (a # l0); sorted_wrt Rc (a # l0); set (a # l0) \<subseteq> S0\<rbrakk> \<Longrightarrow> distinct (map \<alpha> (a # l0)) \<and> sorted_wrt Ra (map \<alpha> (a # l0))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l0. \<lbrakk>\<lbrakk>distinct l0; sorted_wrt Rc l0; set l0 \<subseteq> S0\<rbrakk> \<Longrightarrow> distinct (map \<alpha> l0) \<and> sorted_wrt Ra (map \<alpha> l0); distinct (a # l0); sorted_wrt Rc (a # l0); set (a # l0) \<subseteq> S0\<rbrakk> \<Longrightarrow> distinct (map \<alpha> (a # l0)) \<and> sorted_wrt Ra (map \<alpha> (a # l0))
[PROOF STEP]
case (Cons x l0)
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct l0; sorted_wrt Rc l0; set l0 \<subseteq> S0\<rbrakk> \<Longrightarrow> distinct (map \<alpha> l0) \<and> sorted_wrt Ra (map \<alpha> l0)
distinct (x # l0)
sorted_wrt Rc (x # l0)
set (x # l0) \<subseteq> S0

goal (1 subgoal):
 1. \<And>a l0. \<lbrakk>\<lbrakk>distinct l0; sorted_wrt Rc l0; set l0 \<subseteq> S0\<rbrakk> \<Longrightarrow> distinct (map \<alpha> l0) \<and> sorted_wrt Ra (map \<alpha> l0); distinct (a # l0); sorted_wrt Rc (a # l0); set (a # l0) \<subseteq> S0\<rbrakk> \<Longrightarrow> distinct (map \<alpha> (a # l0)) \<and> sorted_wrt Ra (map \<alpha> (a # l0))
[PROOF STEP]
hence "distinct l0" and "x \<notin> set l0" and "x \<in> S0" and "set l0 \<subseteq> S0" and
            "distinct (map \<alpha> l0)" "sorted_wrt Ra (map \<alpha> l0)" "\<And>x'. x' \<in> set l0 \<Longrightarrow> Rc x x'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct l0; sorted_wrt Rc l0; set l0 \<subseteq> S0\<rbrakk> \<Longrightarrow> distinct (map \<alpha> l0) \<and> sorted_wrt Ra (map \<alpha> l0)
distinct (x # l0)
sorted_wrt Rc (x # l0)
set (x # l0) \<subseteq> S0

goal (1 subgoal):
 1. (distinct l0 &&& x \<notin> set l0) &&& x \<in> S0 &&& set l0 \<subseteq> S0 &&& distinct (map \<alpha> l0) &&& sorted_wrt Ra (map \<alpha> l0) &&& (\<And>x'. x' \<in> set l0 \<Longrightarrow> Rc x x')
[PROOF STEP]
by (simp_all)
[PROOF STATE]
proof (state)
this:
distinct l0
x \<notin> set l0
x \<in> S0
set l0 \<subseteq> S0
distinct (map \<alpha> l0)
sorted_wrt Ra (map \<alpha> l0)
?x' \<in> set l0 \<Longrightarrow> Rc x ?x'

goal (1 subgoal):
 1. \<And>a l0. \<lbrakk>\<lbrakk>distinct l0; sorted_wrt Rc l0; set l0 \<subseteq> S0\<rbrakk> \<Longrightarrow> distinct (map \<alpha> l0) \<and> sorted_wrt Ra (map \<alpha> l0); distinct (a # l0); sorted_wrt Rc (a # l0); set (a # l0) \<subseteq> S0\<rbrakk> \<Longrightarrow> distinct (map \<alpha> (a # l0)) \<and> sorted_wrt Ra (map \<alpha> (a # l0))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
distinct l0
x \<notin> set l0
x \<in> S0
set l0 \<subseteq> S0
distinct (map \<alpha> l0)
sorted_wrt Ra (map \<alpha> l0)
?x' \<in> set l0 \<Longrightarrow> Rc x ?x'

goal (1 subgoal):
 1. distinct (map \<alpha> (x # l0)) \<and> sorted_wrt Ra (map \<alpha> (x # l0))
[PROOF STEP]
using dist[of x] R_OK[of x] invar
[PROOF STATE]
proof (prove)
using this:
distinct l0
x \<notin> set l0
x \<in> S0
set l0 \<subseteq> S0
distinct (map \<alpha> l0)
sorted_wrt Ra (map \<alpha> l0)
?x' \<in> set l0 \<Longrightarrow> Rc x ?x'
\<lbrakk>invar x; invar ?xc2.0; x \<in> S0; ?xc2.0 \<in> S0; \<alpha> x = \<alpha> ?xc2.0\<rbrakk> \<Longrightarrow> x = ?xc2.0
\<lbrakk>invar x; invar ?xc2.0; Rc x ?xc2.0\<rbrakk> \<Longrightarrow> Ra (\<alpha> x) (\<alpha> ?xc2.0)
?xc \<in> S0 \<Longrightarrow> invar ?xc

goal (1 subgoal):
 1. distinct (map \<alpha> (x # l0)) \<and> sorted_wrt Ra (map \<alpha> (x # l0))
[PROOF STEP]
apply (simp add: image_iff Ball_def subset_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct l0; x \<notin> set l0; x \<in> S0; \<forall>t. t \<in> set l0 \<longrightarrow> t \<in> S0; distinct (map \<alpha> l0); sorted_wrt Ra (map \<alpha> l0); \<And>x'. x' \<in> set l0 \<Longrightarrow> Rc x x'; \<And>xc2. \<lbrakk>xc2 \<in> S0; \<alpha> x = \<alpha> xc2\<rbrakk> \<Longrightarrow> x = xc2; \<And>xc2. \<lbrakk>invar xc2; Rc x xc2\<rbrakk> \<Longrightarrow> Ra (\<alpha> x) (\<alpha> xc2); \<And>xc. xc \<in> S0 \<Longrightarrow> invar xc\<rbrakk> \<Longrightarrow> (\<forall>xa. xa \<in> set l0 \<longrightarrow> \<alpha> x \<noteq> \<alpha> xa) \<and> (\<forall>xa. (\<exists>x\<in>set l0. xa = \<alpha> x) \<longrightarrow> Ra (\<alpha> x) xa)
[PROOF STEP]
apply metis
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
distinct (map \<alpha> (x # l0)) \<and> sorted_wrt Ra (map \<alpha> (x # l0))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
distinct (map \<alpha> l0) \<and> sorted_wrt Ra (map \<alpha> l0)

goal (1 subgoal):
 1. set_iterator_abs_genord \<alpha> invar iti S0' Ra
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_abs_genord \<alpha> invar iti S0' Ra
[PROOF STEP]
unfolding S0'_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_abs_genord \<alpha> invar iti (\<alpha> ` S0) Ra
[PROOF STEP]
apply (rule set_iterator_abs_genord.intro)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>lc. (\<forall>xc\<in>set lc. invar xc) \<and> distinct (map \<alpha> lc) \<and> \<alpha> ` S0 = set (map \<alpha> lc) \<and> sorted_wrt Ra (map \<alpha> lc) \<and> iti = foldli lc
[PROOF STEP]
apply (rule_tac exI[where x = l0])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>xc\<in>set l0. invar xc) \<and> distinct (map \<alpha> l0) \<and> \<alpha> ` S0 = set (map \<alpha> l0) \<and> sorted_wrt Ra (map \<alpha> l0) \<and> iti = foldli l0
[PROOF STEP]
apply (simp add: iti_eq map_props S0_eq Ball_def invar)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
set_iterator_abs_genord \<alpha> invar iti S0' Ra

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_to_set_cong:
  "map_to_set m1 = map_to_set m2 \<longleftrightarrow> m1 = m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map_to_set m1 = map_to_set m2) = (m1 = m2)
[PROOF STEP]
apply (simp add: set_eq_iff map_to_set_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>a b. (m1 a = Some b) = (m2 a = Some b)) = (m1 = m2)
[PROOF STEP]
apply (simp add: fun_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>a b. (m1 a = Some b) = (m2 a = Some b)) = (\<forall>x. m1 x = m2 x)
[PROOF STEP]
apply (metis not_Some_eq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma map_iterator_abs_genord_I2 :
  assumes it_OK: "map_iterator_genord iti m R'"
      and invar: "\<And>k v. m k = Some v \<Longrightarrow> invar v"
      and R_OK: "\<And>k v k' v'. invar v \<Longrightarrow> invar v' \<Longrightarrow> R' (k, v) (k', v') \<Longrightarrow> R (k, \<alpha> v) (k', \<alpha> v')"
      and m'_eq: "m' = ((map_option \<alpha>) o m)"
  shows "map_iterator_abs_genord \<alpha> invar iti m' R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_iterator_abs_genord \<alpha> invar iti m' R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_iterator_abs_genord \<alpha> invar iti m' R
[PROOF STEP]
let ?\<alpha>' = "\<lambda>(k,v). (k, \<alpha> v)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_iterator_abs_genord \<alpha> invar iti m' R
[PROOF STEP]
let ?invar' = "\<lambda>(k,v). invar v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_iterator_abs_genord \<alpha> invar iti m' R
[PROOF STEP]
have \<alpha>_rewr: "?\<alpha>' ` (map_to_set m) = map_to_set ((map_option \<alpha>) o m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(k, v). (k, \<alpha> v)) ` map_to_set m = map_to_set (map_option \<alpha> \<circ> m)
[PROOF STEP]
by (auto simp add: map_to_set_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>(k, v). (k, \<alpha> v)) ` map_to_set m = map_to_set (map_option \<alpha> \<circ> m)

goal (1 subgoal):
 1. map_iterator_abs_genord \<alpha> invar iti m' R
[PROOF STEP]
note rule' = set_iterator_abs_genord_I2[OF it_OK[unfolded set_iterator_def],
    of ?invar' R ?\<alpha>' "map_to_set (map_option \<alpha> \<circ> m)", unfolded \<alpha>_rewr map_iterator_abs_genord_def[symmetric]]
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>xc1 xc2. \<lbrakk>case xc1 of (k, v) \<Rightarrow> invar v; case xc2 of (k, v) \<Rightarrow> invar v; R' xc1 xc2\<rbrakk> \<Longrightarrow> R (case xc1 of (k, v) \<Rightarrow> (k, \<alpha> v)) (case xc2 of (k, v) \<Rightarrow> (k, \<alpha> v)); \<And>xc1 xc2. \<lbrakk>case xc1 of (k, v) \<Rightarrow> invar v; case xc2 of (k, v) \<Rightarrow> invar v; xc1 \<in> map_to_set m; xc2 \<in> map_to_set m; (case xc1 of (k, v) \<Rightarrow> (k, \<alpha> v)) = (case xc2 of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> xc1 = xc2; \<And>xc. xc \<in> map_to_set m \<Longrightarrow> case xc of (k, v) \<Rightarrow> invar v; map_to_set (map_option \<alpha> \<circ> m) = map_to_set (map_option \<alpha> \<circ> m)\<rbrakk> \<Longrightarrow> map_iterator_abs_genord \<alpha> invar iti (map_option \<alpha> \<circ> m) R

goal (1 subgoal):
 1. map_iterator_abs_genord \<alpha> invar iti m' R
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_iterator_abs_genord \<alpha> invar iti m' R
[PROOF STEP]
unfolding m'_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_iterator_abs_genord \<alpha> invar iti (map_option \<alpha> \<circ> m) R
[PROOF STEP]
apply (rule rule')
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>xc1 xc2. \<lbrakk>case xc1 of (k, v) \<Rightarrow> invar v; case xc2 of (k, v) \<Rightarrow> invar v; R' xc1 xc2\<rbrakk> \<Longrightarrow> R (case xc1 of (k, v) \<Rightarrow> (k, \<alpha> v)) (case xc2 of (k, v) \<Rightarrow> (k, \<alpha> v))
 2. \<And>xc1 xc2. \<lbrakk>case xc1 of (k, v) \<Rightarrow> invar v; case xc2 of (k, v) \<Rightarrow> invar v; xc1 \<in> map_to_set m; xc2 \<in> map_to_set m; (case xc1 of (k, v) \<Rightarrow> (k, \<alpha> v)) = (case xc2 of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> xc1 = xc2
 3. \<And>xc. xc \<in> map_to_set m \<Longrightarrow> case xc of (k, v) \<Rightarrow> invar v
 4. map_to_set (map_option \<alpha> \<circ> m) = map_to_set (map_option \<alpha> \<circ> m)
[PROOF STEP]
apply (auto simp add: map_to_set_def invar R_OK)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
map_iterator_abs_genord \<alpha> invar iti m' R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_iterator_abs_genord_remove_abs2 :
  assumes iti: "map_iterator_abs_genord \<alpha> invar iti m R"
  obtains m' where "map_iterator_genord iti m' (\<lambda>(k, v) (k', v'). R (k, \<alpha> v) (k', \<alpha> v'))"
       "(map_option \<alpha>) o m' = m" "\<And>k v. m' k = Some v \<Longrightarrow> invar v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m'. \<lbrakk>map_iterator_genord iti m' (\<lambda>(k, v) (k', v'). R (k, \<alpha> v) (k', \<alpha> v')); map_option \<alpha> \<circ> m' = m; \<And>k v. m' k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>m'. \<lbrakk>map_iterator_genord iti m' (\<lambda>(k, v) (k', v'). R (k, \<alpha> v) (k', \<alpha> v')); map_option \<alpha> \<circ> m' = m; \<And>k v. m' k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?\<alpha>' = "\<lambda>(k,v). (k, \<alpha> v)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>m'. \<lbrakk>map_iterator_genord iti m' (\<lambda>(k, v) (k', v'). R (k, \<alpha> v) (k', \<alpha> v')); map_option \<alpha> \<circ> m' = m; \<And>k v. m' k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?invar' = "\<lambda>(k,v). invar v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>m'. \<lbrakk>map_iterator_genord iti m' (\<lambda>(k, v) (k', v'). R (k, \<alpha> v) (k', \<alpha> v')); map_option \<alpha> \<circ> m' = m; \<And>k v. m' k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from set_iterator_abs_genord.foldli_transform [OF iti[unfolded map_iterator_abs_genord_def]]
[PROOF STATE]
proof (chain)
picking this:
\<exists>lc. (\<forall>xc\<in>set lc. case xc of (k, v) \<Rightarrow> invar v) \<and> distinct (map (\<lambda>(k, v). (k, \<alpha> v)) lc) \<and> map_to_set m = set (map (\<lambda>(k, v). (k, \<alpha> v)) lc) \<and> sorted_wrt R (map (\<lambda>(k, v). (k, \<alpha> v)) lc) \<and> iti = foldli lc
[PROOF STEP]
obtain lc where lc_invar: "\<And>k v. (k, v) \<in> set lc \<Longrightarrow> invar v"
      and \<alpha>_props: "distinct (map ?\<alpha>' lc)" "map_to_set m = set (map ?\<alpha>' lc)"
                   "sorted_wrt R (map ?\<alpha>' lc)"
      and iti_eq: "iti = foldli lc"
[PROOF STATE]
proof (prove)
using this:
\<exists>lc. (\<forall>xc\<in>set lc. case xc of (k, v) \<Rightarrow> invar v) \<and> distinct (map (\<lambda>(k, v). (k, \<alpha> v)) lc) \<and> map_to_set m = set (map (\<lambda>(k, v). (k, \<alpha> v)) lc) \<and> sorted_wrt R (map (\<lambda>(k, v). (k, \<alpha> v)) lc) \<and> iti = foldli lc

goal (1 subgoal):
 1. (\<And>lc. \<lbrakk>\<And>k v. (k, v) \<in> set lc \<Longrightarrow> invar v; distinct (map (\<lambda>(k, v). (k, \<alpha> v)) lc); map_to_set m = set (map (\<lambda>(k, v). (k, \<alpha> v)) lc); sorted_wrt R (map (\<lambda>(k, v). (k, \<alpha> v)) lc); iti = foldli lc\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(?k2, ?v2) \<in> set lc \<Longrightarrow> invar ?v2
distinct (map (\<lambda>(k, v). (k, \<alpha> v)) lc)
map_to_set m = set (map (\<lambda>(k, v). (k, \<alpha> v)) lc)
sorted_wrt R (map (\<lambda>(k, v). (k, \<alpha> v)) lc)
iti = foldli lc

goal (1 subgoal):
 1. (\<And>m'. \<lbrakk>map_iterator_genord iti m' (\<lambda>(k, v) (k', v'). R (k, \<alpha> v) (k', \<alpha> v')); map_option \<alpha> \<circ> m' = m; \<And>k v. m' k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<alpha>_props(2)[symmetric]
[PROOF STATE]
proof (chain)
picking this:
set (map (\<lambda>(k, v). (k, \<alpha> v)) lc) = map_to_set m
[PROOF STEP]
have in_lc: "\<And>k v. (k, v) \<in> set lc \<Longrightarrow> m k = Some (\<alpha> v)"
[PROOF STATE]
proof (prove)
using this:
set (map (\<lambda>(k, v). (k, \<alpha> v)) lc) = map_to_set m

goal (1 subgoal):
 1. \<And>k v. (k, v) \<in> set lc \<Longrightarrow> m k = Some (\<alpha> v)
[PROOF STEP]
by (auto simp add: set_eq_iff image_iff map_to_set_def Ball_def Bex_def)
[PROOF STATE]
proof (state)
this:
(?k2, ?v2) \<in> set lc \<Longrightarrow> m ?k2 = Some (\<alpha> ?v2)

goal (1 subgoal):
 1. (\<And>m'. \<lbrakk>map_iterator_genord iti m' (\<lambda>(k, v) (k', v'). R (k, \<alpha> v) (k', \<alpha> v')); map_option \<alpha> \<circ> m' = m; \<And>k v. m' k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<alpha>_props(1)
[PROOF STATE]
proof (chain)
picking this:
distinct (map (\<lambda>(k, v). (k, \<alpha> v)) lc)
[PROOF STEP]
have inj_on_\<alpha>': "inj_on ?\<alpha>' (set lc)"
[PROOF STATE]
proof (prove)
using this:
distinct (map (\<lambda>(k, v). (k, \<alpha> v)) lc)

goal (1 subgoal):
 1. inj_on (\<lambda>(k, v). (k, \<alpha> v)) (set lc)
[PROOF STEP]
by (simp add: distinct_map)
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>(k, v). (k, \<alpha> v)) (set lc)

goal (1 subgoal):
 1. (\<And>m'. \<lbrakk>map_iterator_genord iti m' (\<lambda>(k, v) (k', v'). R (k, \<alpha> v) (k', \<alpha> v')); map_option \<alpha> \<circ> m' = m; \<And>k v. m' k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from in_lc inj_on_\<alpha>'
[PROOF STATE]
proof (chain)
picking this:
(?k2, ?v2) \<in> set lc \<Longrightarrow> m ?k2 = Some (\<alpha> ?v2)
inj_on (\<lambda>(k, v). (k, \<alpha> v)) (set lc)
[PROOF STEP]
have inj_on_fst: "inj_on fst (set lc)"
[PROOF STATE]
proof (prove)
using this:
(?k2, ?v2) \<in> set lc \<Longrightarrow> m ?k2 = Some (\<alpha> ?v2)
inj_on (\<lambda>(k, v). (k, \<alpha> v)) (set lc)

goal (1 subgoal):
 1. inj_on fst (set lc)
[PROOF STEP]
apply (simp add: inj_on_def Ball_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>k v. (k, v) \<in> set lc \<Longrightarrow> m k = Some (\<alpha> v); \<forall>a b. (a, b) \<in> set lc \<longrightarrow> (\<forall>ba. (a, ba) \<in> set lc \<longrightarrow> \<alpha> b = \<alpha> ba \<longrightarrow> b = ba)\<rbrakk> \<Longrightarrow> \<forall>a b. (a, b) \<in> set lc \<longrightarrow> (\<forall>ba. (a, ba) \<in> set lc \<longrightarrow> b = ba)
[PROOF STEP]
apply (metis option.inject)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
inj_on fst (set lc)

goal (1 subgoal):
 1. (\<And>m'. \<lbrakk>map_iterator_genord iti m' (\<lambda>(k, v) (k', v'). R (k, \<alpha> v) (k', \<alpha> v')); map_option \<alpha> \<circ> m' = m; \<And>k v. m' k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?m' = "map_of lc"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>m'. \<lbrakk>map_iterator_genord iti m' (\<lambda>(k, v) (k', v'). R (k, \<alpha> v) (k', \<alpha> v')); map_option \<alpha> \<circ> m' = m; \<And>k v. m' k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<alpha>_props
[PROOF STATE]
proof (chain)
picking this:
distinct (map (\<lambda>(k, v). (k, \<alpha> v)) lc)
map_to_set m = set (map (\<lambda>(k, v). (k, \<alpha> v)) lc)
sorted_wrt R (map (\<lambda>(k, v). (k, \<alpha> v)) lc)
[PROOF STEP]
have it': "map_iterator_genord iti ?m' (\<lambda>x y. R (?\<alpha>' x) (?\<alpha>' y))"
[PROOF STATE]
proof (prove)
using this:
distinct (map (\<lambda>(k, v). (k, \<alpha> v)) lc)
map_to_set m = set (map (\<lambda>(k, v). (k, \<alpha> v)) lc)
sorted_wrt R (map (\<lambda>(k, v). (k, \<alpha> v)) lc)

goal (1 subgoal):
 1. map_iterator_genord iti (map_of lc) (\<lambda>x y. R (case x of (k, v) \<Rightarrow> (k, \<alpha> v)) (case y of (k, v) \<Rightarrow> (k, \<alpha> v)))
[PROOF STEP]
apply (rule_tac set_iterator_genord_I [of lc])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>distinct (map (\<lambda>(k, v). (k, \<alpha> v)) lc); map_to_set m = set (map (\<lambda>(k, v). (k, \<alpha> v)) lc); sorted_wrt R (map (\<lambda>(k, v). (k, \<alpha> v)) lc)\<rbrakk> \<Longrightarrow> distinct lc
 2. \<lbrakk>distinct (map (\<lambda>(k, v). (k, \<alpha> v)) lc); map_to_set m = set (map (\<lambda>(k, v). (k, \<alpha> v)) lc); sorted_wrt R (map (\<lambda>(k, v). (k, \<alpha> v)) lc)\<rbrakk> \<Longrightarrow> map_to_set (map_of lc) = set lc
 3. \<lbrakk>distinct (map (\<lambda>(k, v). (k, \<alpha> v)) lc); map_to_set m = set (map (\<lambda>(k, v). (k, \<alpha> v)) lc); sorted_wrt R (map (\<lambda>(k, v). (k, \<alpha> v)) lc)\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. R (case x of (k, v) \<Rightarrow> (k, \<alpha> v)) (case y of (k, v) \<Rightarrow> (k, \<alpha> v))) lc
 4. \<lbrakk>distinct (map (\<lambda>(k, v). (k, \<alpha> v)) lc); map_to_set m = set (map (\<lambda>(k, v). (k, \<alpha> v)) lc); sorted_wrt R (map (\<lambda>(k, v). (k, \<alpha> v)) lc)\<rbrakk> \<Longrightarrow> iti = foldli lc
[PROOF STEP]
apply (simp_all add: distinct_map sorted_wrt_map iti_eq map_to_set_map_of inj_on_fst)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
map_iterator_genord iti (map_of lc) (\<lambda>x y. R (case x of (k, v) \<Rightarrow> (k, \<alpha> v)) (case y of (k, v) \<Rightarrow> (k, \<alpha> v)))

goal (1 subgoal):
 1. (\<And>m'. \<lbrakk>map_iterator_genord iti m' (\<lambda>(k, v) (k', v'). R (k, \<alpha> v) (k', \<alpha> v')); map_option \<alpha> \<circ> m' = m; \<And>k v. m' k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from inj_on_fst \<alpha>_props(1)
[PROOF STATE]
proof (chain)
picking this:
inj_on fst (set lc)
distinct (map (\<lambda>(k, v). (k, \<alpha> v)) lc)
[PROOF STEP]
have "distinct (map fst (map ?\<alpha>' lc))"
[PROOF STATE]
proof (prove)
using this:
inj_on fst (set lc)
distinct (map (\<lambda>(k, v). (k, \<alpha> v)) lc)

goal (1 subgoal):
 1. distinct (map fst (map (\<lambda>(k, v). (k, \<alpha> v)) lc))
[PROOF STEP]
by (auto simp add: distinct_map inj_on_def Ball_def)
[PROOF STATE]
proof (state)
this:
distinct (map fst (map (\<lambda>(k, v). (k, \<alpha> v)) lc))

goal (1 subgoal):
 1. (\<And>m'. \<lbrakk>map_iterator_genord iti m' (\<lambda>(k, v) (k', v'). R (k, \<alpha> v) (k', \<alpha> v')); map_option \<alpha> \<circ> m' = m; \<And>k v. m' k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "map_to_set m = map_to_set (map_of (map ?\<alpha>' lc))"
[PROOF STATE]
proof (prove)
using this:
distinct (map fst (map (\<lambda>(k, v). (k, \<alpha> v)) lc))

goal (1 subgoal):
 1. map_to_set m = map_to_set (map_of (map (\<lambda>(k, v). (k, \<alpha> v)) lc))
[PROOF STEP]
by (simp add: \<alpha>_props map_to_set_map_of)
[PROOF STATE]
proof (state)
this:
map_to_set m = map_to_set (map_of (map (\<lambda>(k, v). (k, \<alpha> v)) lc))

goal (1 subgoal):
 1. (\<And>m'. \<lbrakk>map_iterator_genord iti m' (\<lambda>(k, v) (k', v'). R (k, \<alpha> v) (k', \<alpha> v')); map_option \<alpha> \<circ> m' = m; \<And>k v. m' k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence m_eq: "map_option \<alpha> \<circ> map_of lc = m"
[PROOF STATE]
proof (prove)
using this:
map_to_set m = map_to_set (map_of (map (\<lambda>(k, v). (k, \<alpha> v)) lc))

goal (1 subgoal):
 1. (map_option \<alpha> \<circ>\<circ> map_of) lc = m
[PROOF STEP]
by (simp add: map_of_map[symmetric] map_to_set_cong)
[PROOF STATE]
proof (state)
this:
(map_option \<alpha> \<circ>\<circ> map_of) lc = m

goal (1 subgoal):
 1. (\<And>m'. \<lbrakk>map_iterator_genord iti m' (\<lambda>(k, v) (k', v'). R (k, \<alpha> v) (k', \<alpha> v')); map_option \<alpha> \<circ> m' = m; \<And>k v. m' k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from that[of ?m'] it' lc_invar \<alpha>_props(1)
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>map_iterator_genord iti (map_of lc) (\<lambda>(k, v) (k', v'). R (k, \<alpha> v) (k', \<alpha> v')); (map_option \<alpha> \<circ>\<circ> map_of) lc = m; \<And>k v. map_of lc k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> thesis
map_iterator_genord iti (map_of lc) (\<lambda>x y. R (case x of (k, v) \<Rightarrow> (k, \<alpha> v)) (case y of (k, v) \<Rightarrow> (k, \<alpha> v)))
(?k2, ?v2) \<in> set lc \<Longrightarrow> invar ?v2
distinct (map (\<lambda>(k, v). (k, \<alpha> v)) lc)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>map_iterator_genord iti (map_of lc) (\<lambda>(k, v) (k', v'). R (k, \<alpha> v) (k', \<alpha> v')); (map_option \<alpha> \<circ>\<circ> map_of) lc = m; \<And>k v. map_of lc k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> thesis
map_iterator_genord iti (map_of lc) (\<lambda>x y. R (case x of (k, v) \<Rightarrow> (k, \<alpha> v)) (case y of (k, v) \<Rightarrow> (k, \<alpha> v)))
(?k2, ?v2) \<in> set lc \<Longrightarrow> invar ?v2
distinct (map (\<lambda>(k, v). (k, \<alpha> v)) lc)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (simp add: distinct_map split_def inj_on_fst ran_distinct m_eq)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_iterator_abs_genord_rule_P:
  assumes iti_OK: "map_iterator_abs_genord \<alpha> invar iti m R"
      and I0: "I (dom m) \<sigma>0"
      and IP: "!!k v it \<sigma>. \<lbrakk> c \<sigma>; k \<in> it; invar v; m k = Some (\<alpha> v); it \<subseteq> dom m; I it \<sigma>;
                             \<forall>k' v'. k' \<in> it-{k} \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> R (k, \<alpha> v) (k', \<alpha> v');
                             \<forall>k' v'. k' \<notin> it \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> R (k', \<alpha> v') (k, \<alpha> v)\<rbrakk> \<Longrightarrow>
                            I (it - {k}) (f (k, v) \<sigma>)"
      and IF: "!!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>"
      and II: "!!\<sigma> it. \<lbrakk> it \<subseteq> dom m; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma>;
                         \<forall>k v k' v'. k \<notin> it \<and> invar v \<and> m k = Some (\<alpha> v) \<and>
                                     k' \<in> it \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow>
                                     R (k, \<alpha> v) (k', \<alpha> v') \<rbrakk> \<Longrightarrow> P \<sigma>"
  shows "P (iti c f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
let ?\<alpha>' = "\<lambda>(k,v). (k, \<alpha> v)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
let ?invar' = "\<lambda>(k,v). invar v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
from map_iterator_abs_genord_remove_abs2 [OF iti_OK]
[PROOF STATE]
proof (chain)
picking this:
(\<And>m'. \<lbrakk>map_iterator_genord iti m' (\<lambda>(k, v) (k', v'). R (k, \<alpha> v) (k', \<alpha> v')); map_option \<alpha> \<circ> m' = m; \<And>k v. m' k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain m' where m'_props: "map_iterator_genord iti m' (\<lambda>x y. R (?\<alpha>' x) (?\<alpha>' y))"
     "m = map_option \<alpha> \<circ> m'" "\<And>k v. m' k = Some v \<Longrightarrow> invar v"
[PROOF STATE]
proof (prove)
using this:
(\<And>m'. \<lbrakk>map_iterator_genord iti m' (\<lambda>(k, v) (k', v'). R (k, \<alpha> v) (k', \<alpha> v')); map_option \<alpha> \<circ> m' = m; \<And>k v. m' k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>m'. \<lbrakk>map_iterator_genord iti m' (\<lambda>x y. R (case x of (k, v) \<Rightarrow> (k, \<alpha> v)) (case y of (k, v) \<Rightarrow> (k, \<alpha> v))); m = map_option \<alpha> \<circ> m'; \<And>k v. m' k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: split_def)
[PROOF STATE]
proof (state)
this:
map_iterator_genord iti m' (\<lambda>x y. R (case x of (k, v) \<Rightarrow> (k, \<alpha> v)) (case y of (k, v) \<Rightarrow> (k, \<alpha> v)))
m = map_option \<alpha> \<circ> m'
m' ?k2 = Some ?v2 \<Longrightarrow> invar ?v2

goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
have dom_m'_eq: "dom m' = dom m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom m' = dom m
[PROOF STEP]
unfolding m'_props
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom m' = dom (map_option \<alpha> \<circ> m')
[PROOF STEP]
by (simp add: dom_def)
[PROOF STATE]
proof (state)
this:
dom m' = dom m

goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
proof (rule map_iterator_genord_rule_P[OF m'_props(1), of I], goal_cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. I (dom m') \<sigma>0
 2. \<And>k v it \<sigma>. \<lbrakk>c \<sigma>; k \<in> it; m' k = Some v; it \<subseteq> dom m'; I it \<sigma>; \<forall>k' v'. k' \<in> it - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)); \<forall>k' v'. k' \<notin> it \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> I (it - {k}) (f (k, v) \<sigma>)
 3. \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>
 4. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<notin> it \<and> m' k = Some v \<and> k' \<in> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. I (dom m') \<sigma>0
 2. \<And>k v it \<sigma>. \<lbrakk>c \<sigma>; k \<in> it; m' k = Some v; it \<subseteq> dom m'; I it \<sigma>; \<forall>k' v'. k' \<in> it - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)); \<forall>k' v'. k' \<notin> it \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> I (it - {k}) (f (k, v) \<sigma>)
 3. \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>
 4. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<notin> it \<and> m' k = Some v \<and> k' \<in> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I (dom m') \<sigma>0
[PROOF STEP]
using I0
[PROOF STATE]
proof (prove)
using this:
I (dom m) \<sigma>0

goal (1 subgoal):
 1. I (dom m') \<sigma>0
[PROOF STEP]
by (simp add: dom_m'_eq)
[PROOF STATE]
proof (state)
this:
I (dom m') \<sigma>0

goal (3 subgoals):
 1. \<And>k v it \<sigma>. \<lbrakk>c \<sigma>; k \<in> it; m' k = Some v; it \<subseteq> dom m'; I it \<sigma>; \<forall>k' v'. k' \<in> it - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)); \<forall>k' v'. k' \<notin> it \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> I (it - {k}) (f (k, v) \<sigma>)
 2. \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>
 3. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<notin> it \<and> m' k = Some v \<and> k' \<in> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>k v it \<sigma>. \<lbrakk>c \<sigma>; k \<in> it; m' k = Some v; it \<subseteq> dom m'; I it \<sigma>; \<forall>k' v'. k' \<in> it - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)); \<forall>k' v'. k' \<notin> it \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> I (it - {k}) (f (k, v) \<sigma>)
 2. \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>
 3. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<notin> it \<and> m' k = Some v \<and> k' \<in> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
I {} \<sigma>_

goal (3 subgoals):
 1. \<And>k v it \<sigma>. \<lbrakk>c \<sigma>; k \<in> it; m' k = Some v; it \<subseteq> dom m'; I it \<sigma>; \<forall>k' v'. k' \<in> it - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)); \<forall>k' v'. k' \<notin> it \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> I (it - {k}) (f (k, v) \<sigma>)
 2. \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>
 3. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<notin> it \<and> m' k = Some v \<and> k' \<in> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
I {} \<sigma>_

goal (1 subgoal):
 1. P \<sigma>_
[PROOF STEP]
using IF
[PROOF STATE]
proof (prove)
using this:
I {} \<sigma>_
I {} ?\<sigma> \<Longrightarrow> P ?\<sigma>

goal (1 subgoal):
 1. P \<sigma>_
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<sigma>_

goal (2 subgoals):
 1. \<And>k v it \<sigma>. \<lbrakk>c \<sigma>; k \<in> it; m' k = Some v; it \<subseteq> dom m'; I it \<sigma>; \<forall>k' v'. k' \<in> it - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)); \<forall>k' v'. k' \<notin> it \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> I (it - {k}) (f (k, v) \<sigma>)
 2. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<notin> it \<and> m' k = Some v \<and> k' \<in> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k v it \<sigma>. \<lbrakk>c \<sigma>; k \<in> it; m' k = Some v; it \<subseteq> dom m'; I it \<sigma>; \<forall>k' v'. k' \<in> it - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)); \<forall>k' v'. k' \<notin> it \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> I (it - {k}) (f (k, v) \<sigma>)
 2. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<notin> it \<and> m' k = Some v \<and> k' \<in> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
case prems: (2 k v S \<sigma>)
[PROOF STATE]
proof (state)
this:
c \<sigma>
k \<in> S
m' k = Some v
S \<subseteq> dom m'
I S \<sigma>
\<forall>k' v'. k' \<in> S - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))
\<forall>k' v'. k' \<notin> S \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))

goal (2 subgoals):
 1. \<And>k v it \<sigma>. \<lbrakk>c \<sigma>; k \<in> it; m' k = Some v; it \<subseteq> dom m'; I it \<sigma>; \<forall>k' v'. k' \<in> it - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)); \<forall>k' v'. k' \<notin> it \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> I (it - {k}) (f (k, v) \<sigma>)
 2. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<notin> it \<and> m' k = Some v \<and> k' \<in> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
from IP [of \<sigma> k S v] prems
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>c \<sigma>; k \<in> S; invar v; m k = Some (\<alpha> v); S \<subseteq> dom m; I S \<sigma>; \<forall>k' v'. k' \<in> S - {k} \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> R (k, \<alpha> v) (k', \<alpha> v'); \<forall>k' v'. k' \<notin> S \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> R (k', \<alpha> v') (k, \<alpha> v)\<rbrakk> \<Longrightarrow> I (S - {k}) (f (k, v) \<sigma>)
c \<sigma>
k \<in> S
m' k = Some v
S \<subseteq> dom m'
I S \<sigma>
\<forall>k' v'. k' \<in> S - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))
\<forall>k' v'. k' \<notin> S \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>c \<sigma>; k \<in> S; invar v; m k = Some (\<alpha> v); S \<subseteq> dom m; I S \<sigma>; \<forall>k' v'. k' \<in> S - {k} \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> R (k, \<alpha> v) (k', \<alpha> v'); \<forall>k' v'. k' \<notin> S \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> R (k', \<alpha> v') (k, \<alpha> v)\<rbrakk> \<Longrightarrow> I (S - {k}) (f (k, v) \<sigma>)
c \<sigma>
k \<in> S
m' k = Some v
S \<subseteq> dom m'
I S \<sigma>
\<forall>k' v'. k' \<in> S - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))
\<forall>k' v'. k' \<notin> S \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))

goal (1 subgoal):
 1. I (S - {k}) (f (k, v) \<sigma>)
[PROOF STEP]
by (simp add: m'_props) metis
[PROOF STATE]
proof (state)
this:
I (S - {k}) (f (k, v) \<sigma>)

goal (1 subgoal):
 1. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<notin> it \<and> m' k = Some v \<and> k' \<in> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<notin> it \<and> m' k = Some v \<and> k' \<in> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
case prems: (4 \<sigma> S)
[PROOF STATE]
proof (state)
this:
S \<subseteq> dom m'
S \<noteq> {}
\<not> c \<sigma>
I S \<sigma>
\<forall>k v k' v'. k \<notin> S \<and> m' k = Some v \<and> k' \<in> S \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))

goal (1 subgoal):
 1. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<notin> it \<and> m' k = Some v \<and> k' \<in> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<sigma>
[PROOF STEP]
using II[of S \<sigma>] prems
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>S \<subseteq> dom m; S \<noteq> {}; \<not> c \<sigma>; I S \<sigma>; \<forall>k v k' v'. k \<notin> S \<and> invar v \<and> m k = Some (\<alpha> v) \<and> k' \<in> S \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> R (k, \<alpha> v) (k', \<alpha> v')\<rbrakk> \<Longrightarrow> P \<sigma>
S \<subseteq> dom m'
S \<noteq> {}
\<not> c \<sigma>
I S \<sigma>
\<forall>k v k' v'. k \<notin> S \<and> m' k = Some v \<and> k' \<in> S \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))

goal (1 subgoal):
 1. P \<sigma>
[PROOF STEP]
by (simp add: m'_props) metis
[PROOF STATE]
proof (state)
this:
P \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P (iti c f \<sigma>0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_iterator_abs_genord_rule_insert_P:
  assumes iti_OK: "map_iterator_abs_genord \<alpha> invar iti m R"
      and I0: "I {} \<sigma>0"
      and IP: "!!k v it \<sigma>. \<lbrakk> c \<sigma>; k \<in> dom m - it; invar v; m k = Some (\<alpha> v); it \<subseteq> dom m; I it \<sigma>;
                             \<forall>k' v'. k' \<in> (dom m - it)-{k} \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> R (k, \<alpha> v) (k', \<alpha> v');
                             \<forall>k' v'. k' \<in> it \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> R (k', \<alpha> v') (k, \<alpha> v)\<rbrakk> \<Longrightarrow>
                            I (insert k it) (f (k, v) \<sigma>)"
      and IF: "!!\<sigma>. I (dom m) \<sigma> \<Longrightarrow> P \<sigma>"
      and II: "!!\<sigma> it. \<lbrakk> it \<subseteq> dom m; it \<noteq> dom m; \<not> c \<sigma>; I it \<sigma>;
                         \<forall>k v k' v'. k \<in> it \<and> invar v \<and> m k = Some (\<alpha> v) \<and>
                                     k' \<notin> it \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow>
                                     R (k, \<alpha> v) (k', \<alpha> v') \<rbrakk> \<Longrightarrow> P \<sigma>"
  shows "P (iti c f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
let ?\<alpha>' = "\<lambda>(k,v). (k, \<alpha> v)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
let ?invar' = "\<lambda>(k,v). invar v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
from map_iterator_abs_genord_remove_abs2 [OF iti_OK]
[PROOF STATE]
proof (chain)
picking this:
(\<And>m'. \<lbrakk>map_iterator_genord iti m' (\<lambda>(k, v) (k', v'). R (k, \<alpha> v) (k', \<alpha> v')); map_option \<alpha> \<circ> m' = m; \<And>k v. m' k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain m' where m'_props: "map_iterator_genord iti m' (\<lambda>x y. R (?\<alpha>' x) (?\<alpha>' y))"
     "m = map_option \<alpha> \<circ> m'" "\<And>k v. m' k = Some v \<Longrightarrow> invar v"
[PROOF STATE]
proof (prove)
using this:
(\<And>m'. \<lbrakk>map_iterator_genord iti m' (\<lambda>(k, v) (k', v'). R (k, \<alpha> v) (k', \<alpha> v')); map_option \<alpha> \<circ> m' = m; \<And>k v. m' k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>m'. \<lbrakk>map_iterator_genord iti m' (\<lambda>x y. R (case x of (k, v) \<Rightarrow> (k, \<alpha> v)) (case y of (k, v) \<Rightarrow> (k, \<alpha> v))); m = map_option \<alpha> \<circ> m'; \<And>k v. m' k = Some v \<Longrightarrow> invar v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: split_def)
[PROOF STATE]
proof (state)
this:
map_iterator_genord iti m' (\<lambda>x y. R (case x of (k, v) \<Rightarrow> (k, \<alpha> v)) (case y of (k, v) \<Rightarrow> (k, \<alpha> v)))
m = map_option \<alpha> \<circ> m'
m' ?k2 = Some ?v2 \<Longrightarrow> invar ?v2

goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
have dom_m'_eq: "dom m' = dom m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom m' = dom m
[PROOF STEP]
unfolding m'_props
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom m' = dom (map_option \<alpha> \<circ> m')
[PROOF STEP]
by (simp add: dom_def)
[PROOF STATE]
proof (state)
this:
dom m' = dom m

goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
proof (rule map_iterator_genord_rule_insert_P[OF m'_props(1), of I], goal_cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. I {} \<sigma>0
 2. \<And>k v it \<sigma>. \<lbrakk>c \<sigma>; k \<in> dom m' - it; m' k = Some v; it \<subseteq> dom m'; I it \<sigma>; \<forall>k' v'. k' \<in> dom m' - it - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)); \<forall>k' v'. k' \<in> it \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> I (insert k it) (f (k, v) \<sigma>)
 3. \<And>\<sigma>. I (dom m') \<sigma> \<Longrightarrow> P \<sigma>
 4. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> dom m'; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<in> it \<and> m' k = Some v \<and> k' \<notin> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. I {} \<sigma>0
 2. \<And>k v it \<sigma>. \<lbrakk>c \<sigma>; k \<in> dom m' - it; m' k = Some v; it \<subseteq> dom m'; I it \<sigma>; \<forall>k' v'. k' \<in> dom m' - it - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)); \<forall>k' v'. k' \<in> it \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> I (insert k it) (f (k, v) \<sigma>)
 3. \<And>\<sigma>. I (dom m') \<sigma> \<Longrightarrow> P \<sigma>
 4. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> dom m'; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<in> it \<and> m' k = Some v \<and> k' \<notin> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I {} \<sigma>0
[PROOF STEP]
using I0
[PROOF STATE]
proof (prove)
using this:
I {} \<sigma>0

goal (1 subgoal):
 1. I {} \<sigma>0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
I {} \<sigma>0

goal (3 subgoals):
 1. \<And>k v it \<sigma>. \<lbrakk>c \<sigma>; k \<in> dom m' - it; m' k = Some v; it \<subseteq> dom m'; I it \<sigma>; \<forall>k' v'. k' \<in> dom m' - it - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)); \<forall>k' v'. k' \<in> it \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> I (insert k it) (f (k, v) \<sigma>)
 2. \<And>\<sigma>. I (dom m') \<sigma> \<Longrightarrow> P \<sigma>
 3. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> dom m'; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<in> it \<and> m' k = Some v \<and> k' \<notin> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>k v it \<sigma>. \<lbrakk>c \<sigma>; k \<in> dom m' - it; m' k = Some v; it \<subseteq> dom m'; I it \<sigma>; \<forall>k' v'. k' \<in> dom m' - it - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)); \<forall>k' v'. k' \<in> it \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> I (insert k it) (f (k, v) \<sigma>)
 2. \<And>\<sigma>. I (dom m') \<sigma> \<Longrightarrow> P \<sigma>
 3. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> dom m'; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<in> it \<and> m' k = Some v \<and> k' \<notin> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
I (dom m') \<sigma>_

goal (3 subgoals):
 1. \<And>k v it \<sigma>. \<lbrakk>c \<sigma>; k \<in> dom m' - it; m' k = Some v; it \<subseteq> dom m'; I it \<sigma>; \<forall>k' v'. k' \<in> dom m' - it - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)); \<forall>k' v'. k' \<in> it \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> I (insert k it) (f (k, v) \<sigma>)
 2. \<And>\<sigma>. I (dom m') \<sigma> \<Longrightarrow> P \<sigma>
 3. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> dom m'; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<in> it \<and> m' k = Some v \<and> k' \<notin> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
I (dom m') \<sigma>_

goal (1 subgoal):
 1. P \<sigma>_
[PROOF STEP]
using IF
[PROOF STATE]
proof (prove)
using this:
I (dom m') \<sigma>_
I (dom m) ?\<sigma> \<Longrightarrow> P ?\<sigma>

goal (1 subgoal):
 1. P \<sigma>_
[PROOF STEP]
by (simp add: dom_m'_eq)
[PROOF STATE]
proof (state)
this:
P \<sigma>_

goal (2 subgoals):
 1. \<And>k v it \<sigma>. \<lbrakk>c \<sigma>; k \<in> dom m' - it; m' k = Some v; it \<subseteq> dom m'; I it \<sigma>; \<forall>k' v'. k' \<in> dom m' - it - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)); \<forall>k' v'. k' \<in> it \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> I (insert k it) (f (k, v) \<sigma>)
 2. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> dom m'; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<in> it \<and> m' k = Some v \<and> k' \<notin> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k v it \<sigma>. \<lbrakk>c \<sigma>; k \<in> dom m' - it; m' k = Some v; it \<subseteq> dom m'; I it \<sigma>; \<forall>k' v'. k' \<in> dom m' - it - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)); \<forall>k' v'. k' \<in> it \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> I (insert k it) (f (k, v) \<sigma>)
 2. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> dom m'; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<in> it \<and> m' k = Some v \<and> k' \<notin> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
case prems: (2 k v S \<sigma>)
[PROOF STATE]
proof (state)
this:
c \<sigma>
k \<in> dom m' - S
m' k = Some v
S \<subseteq> dom m'
I S \<sigma>
\<forall>k' v'. k' \<in> dom m' - S - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))
\<forall>k' v'. k' \<in> S \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))

goal (2 subgoals):
 1. \<And>k v it \<sigma>. \<lbrakk>c \<sigma>; k \<in> dom m' - it; m' k = Some v; it \<subseteq> dom m'; I it \<sigma>; \<forall>k' v'. k' \<in> dom m' - it - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)); \<forall>k' v'. k' \<in> it \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> I (insert k it) (f (k, v) \<sigma>)
 2. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> dom m'; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<in> it \<and> m' k = Some v \<and> k' \<notin> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
from IP [of \<sigma> k S v] prems
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>c \<sigma>; k \<in> dom m - S; invar v; m k = Some (\<alpha> v); S \<subseteq> dom m; I S \<sigma>; \<forall>k' v'. k' \<in> dom m - S - {k} \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> R (k, \<alpha> v) (k', \<alpha> v'); \<forall>k' v'. k' \<in> S \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> R (k', \<alpha> v') (k, \<alpha> v)\<rbrakk> \<Longrightarrow> I (insert k S) (f (k, v) \<sigma>)
c \<sigma>
k \<in> dom m' - S
m' k = Some v
S \<subseteq> dom m'
I S \<sigma>
\<forall>k' v'. k' \<in> dom m' - S - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))
\<forall>k' v'. k' \<in> S \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>c \<sigma>; k \<in> dom m - S; invar v; m k = Some (\<alpha> v); S \<subseteq> dom m; I S \<sigma>; \<forall>k' v'. k' \<in> dom m - S - {k} \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> R (k, \<alpha> v) (k', \<alpha> v'); \<forall>k' v'. k' \<in> S \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> R (k', \<alpha> v') (k, \<alpha> v)\<rbrakk> \<Longrightarrow> I (insert k S) (f (k, v) \<sigma>)
c \<sigma>
k \<in> dom m' - S
m' k = Some v
S \<subseteq> dom m'
I S \<sigma>
\<forall>k' v'. k' \<in> dom m' - S - {k} \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))
\<forall>k' v'. k' \<in> S \<and> m' k' = Some v' \<longrightarrow> R (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v))

goal (1 subgoal):
 1. I (insert k S) (f (k, v) \<sigma>)
[PROOF STEP]
by (simp add: m'_props) metis
[PROOF STATE]
proof (state)
this:
I (insert k S) (f (k, v) \<sigma>)

goal (1 subgoal):
 1. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> dom m'; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<in> it \<and> m' k = Some v \<and> k' \<notin> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> dom m'; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<in> it \<and> m' k = Some v \<and> k' \<notin> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
case prems: (4 \<sigma> S)
[PROOF STATE]
proof (state)
this:
S \<subseteq> dom m'
S \<noteq> dom m'
\<not> c \<sigma>
I S \<sigma>
\<forall>k v k' v'. k \<in> S \<and> m' k = Some v \<and> k' \<notin> S \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))

goal (1 subgoal):
 1. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m'; it \<noteq> dom m'; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<in> it \<and> m' k = Some v \<and> k' \<notin> it \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<sigma>
[PROOF STEP]
using II[of S \<sigma>] prems
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>S \<subseteq> dom m; S \<noteq> dom m; \<not> c \<sigma>; I S \<sigma>; \<forall>k v k' v'. k \<in> S \<and> invar v \<and> m k = Some (\<alpha> v) \<and> k' \<notin> S \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> R (k, \<alpha> v) (k', \<alpha> v')\<rbrakk> \<Longrightarrow> P \<sigma>
S \<subseteq> dom m'
S \<noteq> dom m'
\<not> c \<sigma>
I S \<sigma>
\<forall>k v k' v'. k \<in> S \<and> m' k = Some v \<and> k' \<notin> S \<and> m' k' = Some v' \<longrightarrow> R (case (k, v) of (k, v) \<Rightarrow> (k, \<alpha> v)) (case (k', v') of (k, v) \<Rightarrow> (k, \<alpha> v))

goal (1 subgoal):
 1. P \<sigma>
[PROOF STEP]
by (simp add: m'_props) metis
[PROOF STATE]
proof (state)
this:
P \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P (iti c f \<sigma>0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_iterator_abs_trivial:
  "set_iterator_abs id (\<lambda>_. True) = set_iterator"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_abs id (\<lambda>_. True) = set_iterator
[PROOF STEP]
by (simp add: set_iterator_def set_iterator_abs_def fun_eq_iff)


[STATEMENT]
lemma set_iterator_abs_trivial_simp [simp]:
  assumes "\<forall>x. invar x"
      and "\<forall>x. \<alpha> x = x"
shows "set_iterator_abs \<alpha> invar = set_iterator"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_abs \<alpha> invar = set_iterator
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set_iterator_abs \<alpha> invar = set_iterator
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. invar x
\<forall>x. \<alpha> x = x
[PROOF STEP]
have "invar = (\<lambda>_. True)" and "\<alpha> = id"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. invar x
\<forall>x. \<alpha> x = x

goal (1 subgoal):
 1. invar = (\<lambda>_. True) &&& \<alpha> = id
[PROOF STEP]
by (simp_all add: fun_eq_iff)
[PROOF STATE]
proof (state)
this:
invar = (\<lambda>_. True)
\<alpha> = id

goal (1 subgoal):
 1. set_iterator_abs \<alpha> invar = set_iterator
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
invar = (\<lambda>_. True)
\<alpha> = id

goal (1 subgoal):
 1. set_iterator_abs \<alpha> invar = set_iterator
[PROOF STEP]
by (simp add: set_iterator_abs_trivial)
[PROOF STATE]
proof (state)
this:
set_iterator_abs \<alpha> invar = set_iterator

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_iterator_abs_I2 :
  assumes it_OK: "set_iterator iti S0"
      and dist: "\<And>xc1 xc2. \<lbrakk>invar xc1; invar xc2; xc1 \<in> S0; xc2 \<in> S0; \<alpha> xc1 = \<alpha> xc2\<rbrakk> \<Longrightarrow> xc1 = xc2"
      and invar: "\<And>xc. xc \<in> S0 \<Longrightarrow> invar xc"
      and S0'_OK: "S0' = \<alpha> ` S0"
  shows "set_iterator_abs \<alpha> invar iti S0'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_abs \<alpha> invar iti S0'
[PROOF STEP]
unfolding set_iterator_abs_def S0'_OK
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_abs_genord \<alpha> invar iti (\<alpha> ` S0) (\<lambda>_ _. True)
[PROOF STEP]
apply (rule set_iterator_abs_genord_I2[OF it_OK[unfolded set_iterator_def], of invar _ \<alpha>])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>xc1 xc2. \<lbrakk>invar xc1; invar xc2; True\<rbrakk> \<Longrightarrow> True
 2. \<And>xc1 xc2. \<lbrakk>invar xc1; invar xc2; xc1 \<in> S0; xc2 \<in> S0; \<alpha> xc1 = \<alpha> xc2\<rbrakk> \<Longrightarrow> xc1 = xc2
 3. \<And>xc. xc \<in> S0 \<Longrightarrow> invar xc
 4. \<alpha> ` S0 = \<alpha> ` S0
[PROOF STEP]
apply (simp_all add: dist invar)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma set_iterator_abs_simple_rule_P:
"\<lbrakk> set_iterator_abs \<alpha> invar it S0;
   (\<And>xc. invar xc \<Longrightarrow> f xc = f' (\<alpha> xc));
   I S0 \<sigma>0;
   !!S \<sigma> x. \<lbrakk> c \<sigma>; x \<in> S; I S \<sigma>; S \<subseteq> S0 \<rbrakk> \<Longrightarrow> I (S - {x}) (f' x \<sigma>);
   !!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>;
   !!\<sigma> S. S \<subseteq> S0 \<Longrightarrow> S \<noteq> {} \<Longrightarrow> \<not> c \<sigma> \<Longrightarrow> I S \<sigma> \<Longrightarrow> P \<sigma>
 \<rbrakk> \<Longrightarrow> P (it c f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set_iterator_abs \<alpha> invar it S0; \<And>xc. invar xc \<Longrightarrow> f xc = f' (\<alpha> xc); I S0 \<sigma>0; \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (S - {x}) (f' x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> {}; \<not> c \<sigma>; I S \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it c f \<sigma>0)
[PROOF STEP]
unfolding set_iterator_abs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set_iterator_abs_genord \<alpha> invar it S0 (\<lambda>_ _. True); \<And>xc. invar xc \<Longrightarrow> f xc = f' (\<alpha> xc); I S0 \<sigma>0; \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (S - {x}) (f' x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> {}; \<not> c \<sigma>; I S \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it c f \<sigma>0)
[PROOF STEP]
using set_iterator_abs_genord.iteratei_abs_simple_rule_P [of \<alpha> invar it S0 "\<lambda>_ _. True" f f' I \<sigma>0 c P]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set_iterator_abs_genord \<alpha> invar it S0 (\<lambda>_ _. True); \<And>xc. \<lbrakk>invar xc; \<alpha> xc \<in> S0\<rbrakk> \<Longrightarrow> f xc = f' (\<alpha> xc); I S0 \<sigma>0; \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S; I S \<sigma>; S \<subseteq> S0; \<forall>y\<in>S - {x}. True; \<forall>y\<in>S0 - S. True\<rbrakk> \<Longrightarrow> I (S - {x}) (f' x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> {}; \<not> c \<sigma>; I S \<sigma>; \<forall>x\<in>S. \<forall>y\<in>S0 - S. True\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it c f \<sigma>0)

goal (1 subgoal):
 1. \<lbrakk>set_iterator_abs_genord \<alpha> invar it S0 (\<lambda>_ _. True); \<And>xc. invar xc \<Longrightarrow> f xc = f' (\<alpha> xc); I S0 \<sigma>0; \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (S - {x}) (f' x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> {}; \<not> c \<sigma>; I S \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it c f \<sigma>0)
[PROOF STEP]
by simp


[STATEMENT]
lemma set_iterator_abs_simple_no_cond_rule_P:
"\<lbrakk> set_iterator_abs \<alpha> invar it S0;
   (\<And>xc. invar xc \<Longrightarrow> f xc = f' (\<alpha> xc));
   I S0 \<sigma>0;
   !!S \<sigma> x. \<lbrakk> x \<in> S; I S \<sigma>; S \<subseteq> S0 \<rbrakk> \<Longrightarrow> I (S - {x}) (f' x \<sigma>);
   !!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>
 \<rbrakk> \<Longrightarrow> P (it (\<lambda>_. True) f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set_iterator_abs \<alpha> invar it S0; \<And>xc. invar xc \<Longrightarrow> f xc = f' (\<alpha> xc); I S0 \<sigma>0; \<And>S \<sigma> x. \<lbrakk>x \<in> S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (S - {x}) (f' x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it (\<lambda>_. True) f \<sigma>0)
[PROOF STEP]
using set_iterator_abs_simple_rule_P[of \<alpha> invar it S0 f f' I \<sigma>0 "\<lambda>_. True" P]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set_iterator_abs \<alpha> invar it S0; \<And>xc. invar xc \<Longrightarrow> f xc = f' (\<alpha> xc); I S0 \<sigma>0; \<And>S \<sigma> x. \<lbrakk>True; x \<in> S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (S - {x}) (f' x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> {}; \<not> True; I S \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it (\<lambda>_. True) f \<sigma>0)

goal (1 subgoal):
 1. \<lbrakk>set_iterator_abs \<alpha> invar it S0; \<And>xc. invar xc \<Longrightarrow> f xc = f' (\<alpha> xc); I S0 \<sigma>0; \<And>S \<sigma> x. \<lbrakk>x \<in> S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (S - {x}) (f' x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it (\<lambda>_. True) f \<sigma>0)
[PROOF STEP]
by simp


[STATEMENT]
lemma set_iterator_abs_simple_rule_insert_P :
"\<lbrakk> set_iterator_abs \<alpha> invar it S0;
   (\<And>xc. invar xc \<Longrightarrow> f xc = f' (\<alpha> xc));
   I {} \<sigma>0;
   !!S \<sigma> x. \<lbrakk> c \<sigma>; x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0 \<rbrakk>  \<Longrightarrow> I (insert x S) (f' x \<sigma>);
   !!\<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>;
   !!\<sigma> S. S \<subseteq> S0 \<Longrightarrow> S \<noteq> S0 \<Longrightarrow> \<not> c \<sigma> \<Longrightarrow> I S \<sigma> \<Longrightarrow> P \<sigma>
 \<rbrakk> \<Longrightarrow> P (it c f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set_iterator_abs \<alpha> invar it S0; \<And>xc. invar xc \<Longrightarrow> f xc = f' (\<alpha> xc); I {} \<sigma>0; \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (insert x S) (f' x \<sigma>); \<And>\<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<not> c \<sigma>; I S \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it c f \<sigma>0)
[PROOF STEP]
unfolding set_iterator_abs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set_iterator_abs_genord \<alpha> invar it S0 (\<lambda>_ _. True); \<And>xc. invar xc \<Longrightarrow> f xc = f' (\<alpha> xc); I {} \<sigma>0; \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (insert x S) (f' x \<sigma>); \<And>\<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<not> c \<sigma>; I S \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it c f \<sigma>0)
[PROOF STEP]
using set_iterator_abs_genord.iteratei_abs_simple_rule_insert_P [of \<alpha> invar it S0 "\<lambda>_ _. True" f f' I \<sigma>0 c P]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set_iterator_abs_genord \<alpha> invar it S0 (\<lambda>_ _. True); \<And>xc. \<lbrakk>invar xc; \<alpha> xc \<in> S0\<rbrakk> \<Longrightarrow> f xc = f' (\<alpha> xc); I {} \<sigma>0; \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0; \<forall>y\<in>S0 - S - {x}. True; \<forall>y\<in>S. True\<rbrakk> \<Longrightarrow> I (insert x S) (f' x \<sigma>); \<And>\<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<not> c \<sigma>; I S \<sigma>; \<forall>x\<in>S0 - S. \<forall>y\<in>S. True\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it c f \<sigma>0)

goal (1 subgoal):
 1. \<lbrakk>set_iterator_abs_genord \<alpha> invar it S0 (\<lambda>_ _. True); \<And>xc. invar xc \<Longrightarrow> f xc = f' (\<alpha> xc); I {} \<sigma>0; \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (insert x S) (f' x \<sigma>); \<And>\<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<not> c \<sigma>; I S \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it c f \<sigma>0)
[PROOF STEP]
by simp


[STATEMENT]
lemma set_iterator_abs_no_cond_simple_rule_insert_P :
"\<lbrakk> set_iterator_abs \<alpha> invar it S0;
   (\<And>xc. invar xc \<Longrightarrow> f xc = f' (\<alpha> xc));
   I {} \<sigma>0;
   !!S \<sigma> x. \<lbrakk> x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0 \<rbrakk>  \<Longrightarrow> I (insert x S) (f' x \<sigma>);
   !!\<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>
 \<rbrakk> \<Longrightarrow> P (it (\<lambda>_. True) f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set_iterator_abs \<alpha> invar it S0; \<And>xc. invar xc \<Longrightarrow> f xc = f' (\<alpha> xc); I {} \<sigma>0; \<And>S \<sigma> x. \<lbrakk>x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (insert x S) (f' x \<sigma>); \<And>\<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it (\<lambda>_. True) f \<sigma>0)
[PROOF STEP]
using set_iterator_abs_simple_rule_insert_P[of \<alpha> invar it S0 f f' I \<sigma>0 "\<lambda>_. True" P]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set_iterator_abs \<alpha> invar it S0; \<And>xc. invar xc \<Longrightarrow> f xc = f' (\<alpha> xc); I {} \<sigma>0; \<And>S \<sigma> x. \<lbrakk>True; x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (insert x S) (f' x \<sigma>); \<And>\<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<not> True; I S \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it (\<lambda>_. True) f \<sigma>0)

goal (1 subgoal):
 1. \<lbrakk>set_iterator_abs \<alpha> invar it S0; \<And>xc. invar xc \<Longrightarrow> f xc = f' (\<alpha> xc); I {} \<sigma>0; \<And>S \<sigma> x. \<lbrakk>x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (insert x S) (f' x \<sigma>); \<And>\<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it (\<lambda>_. True) f \<sigma>0)
[PROOF STEP]
by simp


[STATEMENT]
lemma set_iterator_abs_rule_P:
"\<lbrakk> set_iterator_abs \<alpha> invar it S0;
   I S0 \<sigma>0;
   !!S \<sigma> x. \<lbrakk> c \<sigma>; invar x; \<alpha> x \<in> S; I S \<sigma>; S \<subseteq> S0 \<rbrakk> \<Longrightarrow> I (S - {\<alpha> x}) (f x \<sigma>);
   !!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>;
   !!\<sigma> S. S \<subseteq> S0 \<Longrightarrow> S \<noteq> {} \<Longrightarrow> \<not> c \<sigma> \<Longrightarrow> I S \<sigma> \<Longrightarrow> P \<sigma>
 \<rbrakk> \<Longrightarrow> P (it c f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set_iterator_abs \<alpha> invar it S0; I S0 \<sigma>0; \<And>S \<sigma> x. \<lbrakk>c \<sigma>; invar x; \<alpha> x \<in> S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (S - {\<alpha> x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> {}; \<not> c \<sigma>; I S \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it c f \<sigma>0)
[PROOF STEP]
unfolding set_iterator_abs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set_iterator_abs_genord \<alpha> invar it S0 (\<lambda>_ _. True); I S0 \<sigma>0; \<And>S \<sigma> x. \<lbrakk>c \<sigma>; invar x; \<alpha> x \<in> S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (S - {\<alpha> x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> {}; \<not> c \<sigma>; I S \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it c f \<sigma>0)
[PROOF STEP]
using set_iterator_abs_genord.iteratei_abs_rule_P [of \<alpha> invar it S0 "\<lambda>_ _. True" I \<sigma>0 c f P]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set_iterator_abs_genord \<alpha> invar it S0 (\<lambda>_ _. True); I S0 \<sigma>0; \<And>S \<sigma> x. \<lbrakk>c \<sigma>; invar x; \<alpha> x \<in> S; I S \<sigma>; S \<subseteq> S0; \<forall>y\<in>S - {\<alpha> x}. True; \<forall>y\<in>S0 - S. True\<rbrakk> \<Longrightarrow> I (S - {\<alpha> x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> {}; \<not> c \<sigma>; I S \<sigma>; \<forall>x\<in>S. \<forall>y\<in>S0 - S. True\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it c f \<sigma>0)

goal (1 subgoal):
 1. \<lbrakk>set_iterator_abs_genord \<alpha> invar it S0 (\<lambda>_ _. True); I S0 \<sigma>0; \<And>S \<sigma> x. \<lbrakk>c \<sigma>; invar x; \<alpha> x \<in> S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (S - {\<alpha> x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> {}; \<not> c \<sigma>; I S \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it c f \<sigma>0)
[PROOF STEP]
by simp


[STATEMENT]
lemma set_iterator_abs_no_cond_rule_P:
"\<lbrakk> set_iterator_abs \<alpha> invar it S0;
   I S0 \<sigma>0;
   !!S \<sigma> x. \<lbrakk> invar x; \<alpha> x \<in> S; I S \<sigma>; S \<subseteq> S0 \<rbrakk> \<Longrightarrow> I (S - {\<alpha> x}) (f x \<sigma>);
   !!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>
 \<rbrakk> \<Longrightarrow> P (it (\<lambda>_. True) f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set_iterator_abs \<alpha> invar it S0; I S0 \<sigma>0; \<And>S \<sigma> x. \<lbrakk>invar x; \<alpha> x \<in> S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (S - {\<alpha> x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it (\<lambda>_. True) f \<sigma>0)
[PROOF STEP]
using set_iterator_abs_rule_P[of \<alpha> invar it S0 I \<sigma>0 "\<lambda>_. True" f P]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set_iterator_abs \<alpha> invar it S0; I S0 \<sigma>0; \<And>S \<sigma> x. \<lbrakk>True; invar x; \<alpha> x \<in> S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (S - {\<alpha> x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> {}; \<not> True; I S \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it (\<lambda>_. True) f \<sigma>0)

goal (1 subgoal):
 1. \<lbrakk>set_iterator_abs \<alpha> invar it S0; I S0 \<sigma>0; \<And>S \<sigma> x. \<lbrakk>invar x; \<alpha> x \<in> S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (S - {\<alpha> x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it (\<lambda>_. True) f \<sigma>0)
[PROOF STEP]
by simp


[STATEMENT]
lemma set_iterator_abs_rule_insert_P :
"\<lbrakk> set_iterator_abs \<alpha> invar it S0;
   I {} \<sigma>0;
   !!S \<sigma> x. \<lbrakk> c \<sigma>; invar x; \<alpha> x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0 \<rbrakk>  \<Longrightarrow> I (insert (\<alpha> x) S) (f x \<sigma>);
   !!\<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>;
   !!\<sigma> S. S \<subseteq> S0 \<Longrightarrow> S \<noteq> S0 \<Longrightarrow> \<not> c \<sigma> \<Longrightarrow> I S \<sigma> \<Longrightarrow> P \<sigma>
 \<rbrakk> \<Longrightarrow> P (it c f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set_iterator_abs \<alpha> invar it S0; I {} \<sigma>0; \<And>S \<sigma> x. \<lbrakk>c \<sigma>; invar x; \<alpha> x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (insert (\<alpha> x) S) (f x \<sigma>); \<And>\<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<not> c \<sigma>; I S \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it c f \<sigma>0)
[PROOF STEP]
unfolding set_iterator_abs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set_iterator_abs_genord \<alpha> invar it S0 (\<lambda>_ _. True); I {} \<sigma>0; \<And>S \<sigma> x. \<lbrakk>c \<sigma>; invar x; \<alpha> x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (insert (\<alpha> x) S) (f x \<sigma>); \<And>\<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<not> c \<sigma>; I S \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it c f \<sigma>0)
[PROOF STEP]
using set_iterator_abs_genord.iteratei_abs_rule_insert_P [of \<alpha> invar it S0 "\<lambda>_ _. True" I \<sigma>0 c f P]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set_iterator_abs_genord \<alpha> invar it S0 (\<lambda>_ _. True); I {} \<sigma>0; \<And>S \<sigma> x. \<lbrakk>c \<sigma>; invar x; \<alpha> x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0; \<forall>y\<in>S0 - S - {\<alpha> x}. True; \<forall>y\<in>S. True\<rbrakk> \<Longrightarrow> I (insert (\<alpha> x) S) (f x \<sigma>); \<And>\<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<not> c \<sigma>; I S \<sigma>; \<forall>x\<in>S0 - S. \<forall>y\<in>S. True\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it c f \<sigma>0)

goal (1 subgoal):
 1. \<lbrakk>set_iterator_abs_genord \<alpha> invar it S0 (\<lambda>_ _. True); I {} \<sigma>0; \<And>S \<sigma> x. \<lbrakk>c \<sigma>; invar x; \<alpha> x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (insert (\<alpha> x) S) (f x \<sigma>); \<And>\<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<not> c \<sigma>; I S \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it c f \<sigma>0)
[PROOF STEP]
by simp


[STATEMENT]
lemma set_iterator_abs_no_cond_rule_insert_P :
"\<lbrakk> set_iterator_abs \<alpha> invar it S0;
   I {} \<sigma>0;
   !!S \<sigma> x. \<lbrakk> invar x; \<alpha> x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0 \<rbrakk>  \<Longrightarrow> I (insert (\<alpha> x) S) (f x \<sigma>);
   !!\<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>
 \<rbrakk> \<Longrightarrow> P (it (\<lambda>_. True) f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set_iterator_abs \<alpha> invar it S0; I {} \<sigma>0; \<And>S \<sigma> x. \<lbrakk>invar x; \<alpha> x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (insert (\<alpha> x) S) (f x \<sigma>); \<And>\<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it (\<lambda>_. True) f \<sigma>0)
[PROOF STEP]
using set_iterator_abs_rule_insert_P[of \<alpha> invar it S0 I \<sigma>0 "\<lambda>_. True" f P]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set_iterator_abs \<alpha> invar it S0; I {} \<sigma>0; \<And>S \<sigma> x. \<lbrakk>True; invar x; \<alpha> x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (insert (\<alpha> x) S) (f x \<sigma>); \<And>\<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<not> True; I S \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it (\<lambda>_. True) f \<sigma>0)

goal (1 subgoal):
 1. \<lbrakk>set_iterator_abs \<alpha> invar it S0; I {} \<sigma>0; \<And>S \<sigma> x. \<lbrakk>invar x; \<alpha> x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0\<rbrakk> \<Longrightarrow> I (insert (\<alpha> x) S) (f x \<sigma>); \<And>\<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (it (\<lambda>_. True) f \<sigma>0)
[PROOF STEP]
by simp


[STATEMENT]
lemma map_iterator_abs_trivial:
  "map_iterator_abs id (\<lambda>_. True) = map_iterator"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_iterator_abs id (\<lambda>_. True) = map_iterator
[PROOF STEP]
by (simp add: set_iterator_def map_iterator_abs_def map_iterator_abs_genord_def
              set_iterator_abs_genord_def set_iterator_genord_def fun_eq_iff)


[STATEMENT]
lemma map_iterator_abs_trivial_simp [simp] :
  assumes "\<forall>x. invar x"
      and "\<forall>x. \<alpha> x = x"
shows "map_iterator_abs \<alpha> invar = map_iterator"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_iterator_abs \<alpha> invar = map_iterator
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_iterator_abs \<alpha> invar = map_iterator
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. invar x
\<forall>x. \<alpha> x = x
[PROOF STEP]
have "invar = (\<lambda>_. True)" and "\<alpha> = id"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. invar x
\<forall>x. \<alpha> x = x

goal (1 subgoal):
 1. invar = (\<lambda>_. True) &&& \<alpha> = id
[PROOF STEP]
by (simp_all add: fun_eq_iff)
[PROOF STATE]
proof (state)
this:
invar = (\<lambda>_. True)
\<alpha> = id

goal (1 subgoal):
 1. map_iterator_abs \<alpha> invar = map_iterator
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
invar = (\<lambda>_. True)
\<alpha> = id

goal (1 subgoal):
 1. map_iterator_abs \<alpha> invar = map_iterator
[PROOF STEP]
by (simp add: map_iterator_abs_trivial)
[PROOF STATE]
proof (state)
this:
map_iterator_abs \<alpha> invar = map_iterator

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_iterator_abs_I2 :
  assumes it_OK: "map_iterator iti m"
      and invar: "\<And>k v. m k = Some v \<Longrightarrow> invar v"
      and m'_eq: "m' = map_option \<alpha> \<circ> m"
  shows "map_iterator_abs \<alpha> invar iti m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_iterator_abs \<alpha> invar iti m'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
map_iterator iti m
m ?k = Some ?v \<Longrightarrow> invar ?v
m' = map_option \<alpha> \<circ> m

goal (1 subgoal):
 1. map_iterator_abs \<alpha> invar iti m'
[PROOF STEP]
unfolding map_iterator_abs_def set_iterator_def
[PROOF STATE]
proof (prove)
using this:
map_iterator_genord iti m (\<lambda>_ _. True)
m ?k = Some ?v \<Longrightarrow> invar ?v
m' = map_option \<alpha> \<circ> m

goal (1 subgoal):
 1. map_iterator_abs_genord \<alpha> invar iti m' (\<lambda>_ _. True)
[PROOF STEP]
by (rule_tac map_iterator_abs_genord_I2 [OF it_OK[unfolded set_iterator_def]]) simp_all


[STATEMENT]
lemma map_iterator_abs_rule_P:
  assumes iti_OK: "map_iterator_abs \<alpha> invar iti m"
      and I0: "I (dom m) \<sigma>0"
      and IP: "!!k v it \<sigma>. \<lbrakk> c \<sigma>; k \<in> it; invar v; m k = Some (\<alpha> v); it \<subseteq> dom m; I it \<sigma> \<rbrakk> \<Longrightarrow>
                            I (it - {k}) (f (k, v) \<sigma>)"
      and IF: "!!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>"
      and II: "!!\<sigma> it. \<lbrakk> it \<subseteq> dom m; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma> \<rbrakk> \<Longrightarrow> P \<sigma>"
  shows "P (iti c f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
apply (rule map_iterator_abs_genord_rule_P [OF iti_OK[unfolded map_iterator_abs_def], of I])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. I (dom m) \<sigma>0
 2. \<And>k v it \<sigma>. \<lbrakk>c \<sigma>; k \<in> it; invar v; m k = Some (\<alpha> v); it \<subseteq> dom m; I it \<sigma>; \<forall>k' v'. k' \<in> it - {k} \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> True; \<forall>k' v'. k' \<notin> it \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> True\<rbrakk> \<Longrightarrow> I (it - {k}) (f (k, v) \<sigma>)
 3. \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>
 4. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<notin> it \<and> invar v \<and> m k = Some (\<alpha> v) \<and> k' \<in> it \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> True\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
apply (simp_all add: I0 IP IF II)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma map_iterator_abs_no_cond_rule_P:
  assumes iti_OK: "map_iterator_abs \<alpha> invar iti m"
      and I0: "I (dom m) \<sigma>0"
      and IP: "!!k v it \<sigma>. \<lbrakk> k \<in> it; invar v; m k = Some (\<alpha> v); it \<subseteq> dom m; I it \<sigma> \<rbrakk> \<Longrightarrow>
                            I (it - {k}) (f (k, v) \<sigma>)"
      and IF: "!!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>"
  shows "P (iti (\<lambda>_. True) f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (iti (\<lambda>_. True) f \<sigma>0)
[PROOF STEP]
apply (rule map_iterator_abs_rule_P [OF iti_OK, of I])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. I (dom m) \<sigma>0
 2. \<And>k v it \<sigma>. \<lbrakk>True; k \<in> it; invar v; m k = Some (\<alpha> v); it \<subseteq> dom m; I it \<sigma>\<rbrakk> \<Longrightarrow> I (it - {k}) (f (k, v) \<sigma>)
 3. \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>
 4. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m; it \<noteq> {}; \<not> True; I it \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
apply (simp_all add: I0 IP IF)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma map_iterator_abs_rule_insert_P:
  assumes iti_OK: "map_iterator_abs \<alpha> invar iti m"
      and I0: "I {} \<sigma>0"
      and IP: "!!k v it \<sigma>. \<lbrakk> c \<sigma>; k \<in> dom m - it; invar v; m k = Some (\<alpha> v); it \<subseteq> dom m; I it \<sigma> \<rbrakk> \<Longrightarrow>
                            I (insert k it) (f (k, v) \<sigma>)"
      and IF: "!!\<sigma>. I (dom m) \<sigma> \<Longrightarrow> P \<sigma>"
      and II: "!!\<sigma> it. \<lbrakk> it \<subseteq> dom m; it \<noteq> dom m; \<not> c \<sigma>; I it \<sigma> \<rbrakk> \<Longrightarrow> P \<sigma>"
  shows "P (iti c f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
apply (rule map_iterator_abs_genord_rule_insert_P [OF iti_OK[unfolded map_iterator_abs_def], of I])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. I {} \<sigma>0
 2. \<And>k v it \<sigma>. \<lbrakk>c \<sigma>; k \<in> dom m - it; invar v; m k = Some (\<alpha> v); it \<subseteq> dom m; I it \<sigma>; \<forall>k' v'. k' \<in> dom m - it - {k} \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> True; \<forall>k' v'. k' \<in> it \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> True\<rbrakk> \<Longrightarrow> I (insert k it) (f (k, v) \<sigma>)
 3. \<And>\<sigma>. I (dom m) \<sigma> \<Longrightarrow> P \<sigma>
 4. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m; it \<noteq> dom m; \<not> c \<sigma>; I it \<sigma>; \<forall>k v k' v'. k \<in> it \<and> invar v \<and> m k = Some (\<alpha> v) \<and> k' \<notin> it \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> True\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
apply (simp_all add: I0 IP IF II)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma map_iterator_abs_no_cond_rule_insert_P:
  assumes iti_OK: "map_iterator_abs \<alpha> invar iti m"
      and I0: "I {} \<sigma>0"
      and IP: "!!k v it \<sigma>. \<lbrakk> k \<in> dom m - it; invar v; m k = Some (\<alpha> v); it \<subseteq> dom m; I it \<sigma> \<rbrakk> \<Longrightarrow>
                            I (insert k it) (f (k, v) \<sigma>)"
      and IF: "!!\<sigma>. I (dom m) \<sigma> \<Longrightarrow> P \<sigma>"
  shows "P (iti (\<lambda>_. True) f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (iti (\<lambda>_. True) f \<sigma>0)
[PROOF STEP]
apply (rule map_iterator_abs_genord_rule_insert_P [OF iti_OK[unfolded map_iterator_abs_def], of I])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. I {} \<sigma>0
 2. \<And>k v it \<sigma>. \<lbrakk>True; k \<in> dom m - it; invar v; m k = Some (\<alpha> v); it \<subseteq> dom m; I it \<sigma>; \<forall>k' v'. k' \<in> dom m - it - {k} \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> True; \<forall>k' v'. k' \<in> it \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> True\<rbrakk> \<Longrightarrow> I (insert k it) (f (k, v) \<sigma>)
 3. \<And>\<sigma>. I (dom m) \<sigma> \<Longrightarrow> P \<sigma>
 4. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m; it \<noteq> dom m; \<not> True; I it \<sigma>; \<forall>k v k' v'. k \<in> it \<and> invar v \<and> m k = Some (\<alpha> v) \<and> k' \<notin> it \<and> invar v' \<and> m k' = Some (\<alpha> v') \<longrightarrow> True\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
apply (simp_all add: I0 IP IF)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done