[STATEMENT]
lemma alw_holds_smap_conv_comp: "alw (holds P) (smap f s) = alw (\<lambda>s. (P o f) (shd s)) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alw (holds P) (smap f s) = alw (\<lambda>s. (P \<circ> f) (shd s)) s
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. alw (holds P) (smap f s) \<Longrightarrow> alw (\<lambda>s. (P \<circ> f) (shd s)) s
 2. alw (\<lambda>s. (P \<circ> f) (shd s)) s \<Longrightarrow> alw (holds P) (smap f s)
[PROOF STEP]
apply (coinduction arbitrary: s)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. alw (holds P) (smap f s) \<Longrightarrow> \<exists>xs. s = xs \<and> (P \<circ> f) (shd xs) \<and> ((\<exists>s. stl xs = s \<and> alw (holds P) (smap f s)) \<or> alw (\<lambda>s. (P \<circ> f) (shd s)) (stl xs))
 2. alw (\<lambda>s. (P \<circ> f) (shd s)) s \<Longrightarrow> alw (holds P) (smap f s)
[PROOF STEP]
apply auto []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alw (\<lambda>s. (P \<circ> f) (shd s)) s \<Longrightarrow> alw (holds P) (smap f s)
[PROOF STEP]
apply (coinduction arbitrary: s)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. alw (\<lambda>s. (P \<circ> f) (shd s)) s \<Longrightarrow> \<exists>xs. smap f s = xs \<and> holds P xs \<and> ((\<exists>s. stl xs = smap f s \<and> alw (\<lambda>s. (P \<circ> f) (shd s)) s) \<or> alw (holds P) (stl xs))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma alw_relates: "alw (relates P) s \<longleftrightarrow> P (shd s) (shd (stl s)) \<and> alw (relates P) (stl s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alw (relates P) s = (P (shd s) (shd (stl s)) \<and> alw (relates P) (stl s))
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. alw (relates P) s \<Longrightarrow> P (shd s) (shd (stl s)) \<and> alw (relates P) (stl s)
 2. P (shd s) (shd (stl s)) \<and> alw (relates P) (stl s) \<Longrightarrow> alw (relates P) s
[PROOF STEP]
apply (auto simp: relates_def dest: alwD) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (shd s) (shd (stl s)) \<and> alw (relates P) (stl s) \<Longrightarrow> alw (relates P) s
[PROOF STEP]
apply (coinduction arbitrary: s)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. P (shd s) (shd (stl s)) \<and> alw (relates P) (stl s) \<Longrightarrow> \<exists>xs. s = xs \<and> relates P xs \<and> ((\<exists>s. stl xs = s \<and> P (shd s) (shd (stl s)) \<and> alw (relates P) (stl s)) \<or> alw (relates P) (stl xs))
[PROOF STEP]
apply (auto simp: relates_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iterate_ball_correct :
assumes it: "set_iterator it S0"
shows "iterate_ball it P = (\<forall>x\<in>S0. P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iterate_ball it P = (\<forall>x\<in>S0. P x)
[PROOF STEP]
unfolding iterate_ball_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it id (\<lambda>x \<sigma>. P x) True = (\<forall>x\<in>S0. P x)
[PROOF STEP]
apply (rule set_iterator_rule_P [OF it,
            where I = "\<lambda>S \<sigma>. \<sigma> = (\<forall>x\<in>S0-S. P x)"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. True = (\<forall>x\<in>S0 - S0. P x)
 2. \<And>S \<sigma> x. \<lbrakk>id \<sigma>; x \<in> S; \<sigma> = (\<forall>x\<in>S0 - S. P x); S \<subseteq> S0\<rbrakk> \<Longrightarrow> P x = (\<forall>x\<in>S0 - (S - {x}). P x)
 3. \<And>\<sigma>. \<sigma> = (\<forall>x\<in>S0 - {}. P x) \<Longrightarrow> \<sigma> = (\<forall>x\<in>S0. P x)
 4. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> {}; \<not> id \<sigma>; \<sigma> = (\<forall>x\<in>S0 - S. P x)\<rbrakk> \<Longrightarrow> \<sigma> = (\<forall>x\<in>S0. P x)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iterate_bex_correct :
assumes it: "set_iterator it S0"
shows "iterate_bex it P = (\<exists>x\<in>S0. P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iterate_bex it P = (\<exists>x\<in>S0. P x)
[PROOF STEP]
unfolding iterate_bex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it Not (\<lambda>x \<sigma>. P x) False = (\<exists>x\<in>S0. P x)
[PROOF STEP]
apply (rule set_iterator_rule_P [OF it, where I = "\<lambda>S \<sigma>. \<sigma> = (\<exists>x\<in>S0-S. P x)"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. False = (\<exists>x\<in>S0 - S0. P x)
 2. \<And>S \<sigma> x. \<lbrakk>\<not> \<sigma>; x \<in> S; \<sigma> = (\<exists>x\<in>S0 - S. P x); S \<subseteq> S0\<rbrakk> \<Longrightarrow> P x = (\<exists>x\<in>S0 - (S - {x}). P x)
 3. \<And>\<sigma>. \<sigma> = (\<exists>x\<in>S0 - {}. P x) \<Longrightarrow> \<sigma> = (\<exists>x\<in>S0. P x)
 4. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> {}; \<not> \<not> \<sigma>; \<sigma> = (\<exists>x\<in>S0 - S. P x)\<rbrakk> \<Longrightarrow> \<sigma> = (\<exists>x\<in>S0. P x)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iterate_to_list_foldli [simp] :
  "iterate_to_list (foldli xs) = rev xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iterate_to_list (foldli xs) = rev xs
[PROOF STEP]
unfolding iterate_to_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldli xs (\<lambda>_. True) (#) [] = rev xs
[PROOF STEP]
by (induct xs rule: rev_induct, simp_all add: foldli_snoc)


[STATEMENT]
lemma iterate_to_list_genord_correct :
assumes it: "set_iterator_genord it S0 R"
shows "set (iterate_to_list it) = S0 \<and> distinct (iterate_to_list it) \<and>
       sorted_wrt R (rev (iterate_to_list it))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (iterate_to_list it) = S0 \<and> distinct (iterate_to_list it) \<and> sorted_wrt R (rev (iterate_to_list it))
[PROOF STEP]
using it
[PROOF STATE]
proof (prove)
using this:
set_iterator_genord it S0 R

goal (1 subgoal):
 1. set (iterate_to_list it) = S0 \<and> distinct (iterate_to_list it) \<and> sorted_wrt R (rev (iterate_to_list it))
[PROOF STEP]
unfolding set_iterator_genord_foldli_conv
[PROOF STATE]
proof (prove)
using this:
\<exists>l0. distinct l0 \<and> S0 = set l0 \<and> sorted_wrt R l0 \<and> it = foldli l0

goal (1 subgoal):
 1. set (iterate_to_list it) = S0 \<and> distinct (iterate_to_list it) \<and> sorted_wrt R (rev (iterate_to_list it))
[PROOF STEP]
by auto


[STATEMENT]
lemma iterate_to_list_correct :
assumes it: "set_iterator it S0"
shows "set (iterate_to_list it) = S0 \<and> distinct (iterate_to_list it)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (iterate_to_list it) = S0 \<and> distinct (iterate_to_list it)
[PROOF STEP]
using iterate_to_list_genord_correct [OF it[unfolded set_iterator_def]]
[PROOF STATE]
proof (prove)
using this:
set (iterate_to_list it) = S0 \<and> distinct (iterate_to_list it) \<and> sorted_wrt (\<lambda>_ _. True) (rev (iterate_to_list it))

goal (1 subgoal):
 1. set (iterate_to_list it) = S0 \<and> distinct (iterate_to_list it)
[PROOF STEP]
by simp


[STATEMENT]
lemma (in linorder) iterate_to_list_linord_correct :
fixes S0 :: "'a set"
assumes it_OK: "set_iterator_linord it S0"
shows "set (iterate_to_list it) = S0 \<and> distinct (iterate_to_list it) \<and>
       sorted (rev (iterate_to_list it))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (iterate_to_list it) = S0 \<and> distinct (iterate_to_list it) \<and> sorted (rev (iterate_to_list it))
[PROOF STEP]
using it_OK
[PROOF STATE]
proof (prove)
using this:
set_iterator_linord it S0

goal (1 subgoal):
 1. set (iterate_to_list it) = S0 \<and> distinct (iterate_to_list it) \<and> sorted (rev (iterate_to_list it))
[PROOF STEP]
unfolding set_iterator_linord_foldli_conv
[PROOF STATE]
proof (prove)
using this:
\<exists>l0. distinct l0 \<and> S0 = set l0 \<and> sorted l0 \<and> it = foldli l0

goal (1 subgoal):
 1. set (iterate_to_list it) = S0 \<and> distinct (iterate_to_list it) \<and> sorted (rev (iterate_to_list it))
[PROOF STEP]
by auto


[STATEMENT]
lemma (in linorder) iterate_to_list_rev_linord_correct :
fixes S0 :: "'a set"
assumes it_OK: "set_iterator_rev_linord it S0"
shows "set (iterate_to_list it) = S0 \<and> distinct (iterate_to_list it) \<and>
       sorted (iterate_to_list it)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (iterate_to_list it) = S0 \<and> distinct (iterate_to_list it) \<and> sorted (iterate_to_list it)
[PROOF STEP]
using it_OK
[PROOF STATE]
proof (prove)
using this:
set_iterator_rev_linord it S0

goal (1 subgoal):
 1. set (iterate_to_list it) = S0 \<and> distinct (iterate_to_list it) \<and> sorted (iterate_to_list it)
[PROOF STEP]
unfolding set_iterator_rev_linord_foldli_conv
[PROOF STATE]
proof (prove)
using this:
\<exists>l0. distinct l0 \<and> S0 = set l0 \<and> sorted (rev l0) \<and> it = foldli l0

goal (1 subgoal):
 1. set (iterate_to_list it) = S0 \<and> distinct (iterate_to_list it) \<and> sorted (iterate_to_list it)
[PROOF STEP]
by auto


[STATEMENT]
lemma (in linorder) iterate_to_list_map_linord_correct :
assumes it_OK: "map_iterator_linord it m"
shows "map_of (iterate_to_list it) = m \<and> distinct (map fst (iterate_to_list it)) \<and>
       sorted (map fst (rev (iterate_to_list it)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (iterate_to_list it) = m \<and> distinct (map fst (iterate_to_list it)) \<and> sorted (map fst (rev (iterate_to_list it)))
[PROOF STEP]
using it_OK
[PROOF STATE]
proof (prove)
using this:
map_iterator_linord it m

goal (1 subgoal):
 1. map_of (iterate_to_list it) = m \<and> distinct (map fst (iterate_to_list it)) \<and> sorted (map fst (rev (iterate_to_list it)))
[PROOF STEP]
unfolding map_iterator_linord_foldli_conv
[PROOF STATE]
proof (prove)
using this:
\<exists>l0. distinct (map fst l0) \<and> m = map_of l0 \<and> sorted (map fst l0) \<and> it = foldli l0

goal (1 subgoal):
 1. map_of (iterate_to_list it) = m \<and> distinct (map fst (iterate_to_list it)) \<and> sorted (map fst (rev (iterate_to_list it)))
[PROOF STEP]
by clarify (simp add: rev_map[symmetric])


[STATEMENT]
lemma (in linorder) iterate_to_list_map_rev_linord_correct :
assumes it_OK: "map_iterator_rev_linord it m"
shows "map_of (iterate_to_list it) = m \<and> distinct (map fst (iterate_to_list it)) \<and>
       sorted (map fst (iterate_to_list it))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (iterate_to_list it) = m \<and> distinct (map fst (iterate_to_list it)) \<and> sorted (map fst (iterate_to_list it))
[PROOF STEP]
using it_OK
[PROOF STATE]
proof (prove)
using this:
map_iterator_rev_linord it m

goal (1 subgoal):
 1. map_of (iterate_to_list it) = m \<and> distinct (map fst (iterate_to_list it)) \<and> sorted (map fst (iterate_to_list it))
[PROOF STEP]
unfolding map_iterator_rev_linord_foldli_conv
[PROOF STATE]
proof (prove)
using this:
\<exists>l0. distinct (map fst l0) \<and> m = map_of l0 \<and> sorted (rev (map fst l0)) \<and> it = foldli l0

goal (1 subgoal):
 1. map_of (iterate_to_list it) = m \<and> distinct (map fst (iterate_to_list it)) \<and> sorted (map fst (iterate_to_list it))
[PROOF STEP]
by clarify (simp add: rev_map[symmetric])


[STATEMENT]
lemma set_iterator_finite :
assumes it: "set_iterator it S0"
shows "finite S0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S0
[PROOF STEP]
using set_iterator_genord.finite_S0 [OF it[unfolded set_iterator_def]]
[PROOF STATE]
proof (prove)
using this:
finite S0

goal (1 subgoal):
 1. finite S0
[PROOF STEP]
.


[STATEMENT]
lemma map_iterator_finite :
assumes it: "map_iterator it m"
shows "finite (dom m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (dom m)
[PROOF STEP]
using set_iterator_genord.finite_S0 [OF it[unfolded set_iterator_def]]
[PROOF STATE]
proof (prove)
using this:
finite (map_to_set m)

goal (1 subgoal):
 1. finite (dom m)
[PROOF STEP]
by (simp add: finite_map_to_set)


[STATEMENT]
lemma iterate_size_correct :
assumes it: "set_iterator it S0"
shows "iterate_size it = card S0 \<and> finite S0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iterate_size it = card S0 \<and> finite S0
[PROOF STEP]
unfolding iterate_size_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it (\<lambda>_. True) (\<lambda>x. Suc) 0 = card S0 \<and> finite S0
[PROOF STEP]
apply (rule_tac set_iterator_rule_insert_P [OF it,
    where I = "\<lambda>S \<sigma>. \<sigma> = card S \<and> finite S"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. 0 = card {} \<and> finite {}
 2. \<And>S \<sigma> x. \<lbrakk>True; x \<in> S0 - S; \<sigma> = card S \<and> finite S; S \<subseteq> S0\<rbrakk> \<Longrightarrow> Suc \<sigma> = card (insert x S) \<and> finite (insert x S)
 3. \<And>\<sigma>. \<sigma> = card S0 \<and> finite S0 \<Longrightarrow> \<sigma> = card S0 \<and> finite S0
 4. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<not> True; \<sigma> = card S \<and> finite S\<rbrakk> \<Longrightarrow> \<sigma> = card S0 \<and> finite S0
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iterate_size_abort_correct :
assumes it: "set_iterator it S0"
shows "iterate_size_abort it n = (min n (card S0)) \<and> finite S0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iterate_size_abort it n = min n (card S0) \<and> finite S0
[PROOF STEP]
unfolding iterate_size_abort_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it (\<lambda>\<sigma>. \<sigma> < n) (\<lambda>x. Suc) 0 = min n (card S0) \<and> finite S0
[PROOF STEP]
proof (rule set_iterator_rule_insert_P [OF it,
   where I = "\<lambda>S \<sigma>. \<sigma> = (min n (card S)) \<and> finite S"], goal_cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. 0 = min n (card {}) \<and> finite {}
 2. \<And>S \<sigma> x. \<lbrakk>\<sigma> < n; x \<in> S0 - S; \<sigma> = min n (card S) \<and> finite S; S \<subseteq> S0\<rbrakk> \<Longrightarrow> Suc \<sigma> = min n (card (insert x S)) \<and> finite (insert x S)
 3. \<And>\<sigma>. \<sigma> = min n (card S0) \<and> finite S0 \<Longrightarrow> \<sigma> = min n (card S0) \<and> finite S0
 4. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<not> \<sigma> < n; \<sigma> = min n (card S) \<and> finite S\<rbrakk> \<Longrightarrow> \<sigma> = min n (card S0) \<and> finite S0
[PROOF STEP]
case (4 \<sigma> S)
[PROOF STATE]
proof (state)
this:
S \<subseteq> S0
S \<noteq> S0
\<not> \<sigma> < n
\<sigma> = min n (card S) \<and> finite S

goal (4 subgoals):
 1. 0 = min n (card {}) \<and> finite {}
 2. \<And>S \<sigma> x. \<lbrakk>\<sigma> < n; x \<in> S0 - S; \<sigma> = min n (card S) \<and> finite S; S \<subseteq> S0\<rbrakk> \<Longrightarrow> Suc \<sigma> = min n (card (insert x S)) \<and> finite (insert x S)
 3. \<And>\<sigma>. \<sigma> = min n (card S0) \<and> finite S0 \<Longrightarrow> \<sigma> = min n (card S0) \<and> finite S0
 4. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<not> \<sigma> < n; \<sigma> = min n (card S) \<and> finite S\<rbrakk> \<Longrightarrow> \<sigma> = min n (card S0) \<and> finite S0
[PROOF STEP]
assume "S \<subseteq> S0" "S \<noteq> S0" "\<not> \<sigma> < n" "\<sigma> = min n (card S) \<and> finite S"
[PROOF STATE]
proof (state)
this:
S \<subseteq> S0
S \<noteq> S0
\<not> \<sigma> < n
\<sigma> = min n (card S) \<and> finite S

goal (4 subgoals):
 1. 0 = min n (card {}) \<and> finite {}
 2. \<And>S \<sigma> x. \<lbrakk>\<sigma> < n; x \<in> S0 - S; \<sigma> = min n (card S) \<and> finite S; S \<subseteq> S0\<rbrakk> \<Longrightarrow> Suc \<sigma> = min n (card (insert x S)) \<and> finite (insert x S)
 3. \<And>\<sigma>. \<sigma> = min n (card S0) \<and> finite S0 \<Longrightarrow> \<sigma> = min n (card S0) \<and> finite S0
 4. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<not> \<sigma> < n; \<sigma> = min n (card S) \<and> finite S\<rbrakk> \<Longrightarrow> \<sigma> = min n (card S0) \<and> finite S0
[PROOF STEP]
from \<open>\<sigma> = min n (card S) \<and> finite S\<close> \<open>\<not> \<sigma> < n\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> = min n (card S) \<and> finite S
\<not> \<sigma> < n
[PROOF STEP]
have "\<sigma> = n" "n \<le> card S"
[PROOF STATE]
proof (prove)
using this:
\<sigma> = min n (card S) \<and> finite S
\<not> \<sigma> < n

goal (1 subgoal):
 1. \<sigma> = n &&& n \<le> card S
[PROOF STEP]
by (auto simp add: min_less_iff_disj)
[PROOF STATE]
proof (state)
this:
\<sigma> = n
n \<le> card S

goal (4 subgoals):
 1. 0 = min n (card {}) \<and> finite {}
 2. \<And>S \<sigma> x. \<lbrakk>\<sigma> < n; x \<in> S0 - S; \<sigma> = min n (card S) \<and> finite S; S \<subseteq> S0\<rbrakk> \<Longrightarrow> Suc \<sigma> = min n (card (insert x S)) \<and> finite (insert x S)
 3. \<And>\<sigma>. \<sigma> = min n (card S0) \<and> finite S0 \<Longrightarrow> \<sigma> = min n (card S0) \<and> finite S0
 4. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<not> \<sigma> < n; \<sigma> = min n (card S) \<and> finite S\<rbrakk> \<Longrightarrow> \<sigma> = min n (card S0) \<and> finite S0
[PROOF STEP]
note fin_S0 = set_iterator_genord.finite_S0 [OF it[unfolded set_iterator_def]]
[PROOF STATE]
proof (state)
this:
finite S0

goal (4 subgoals):
 1. 0 = min n (card {}) \<and> finite {}
 2. \<And>S \<sigma> x. \<lbrakk>\<sigma> < n; x \<in> S0 - S; \<sigma> = min n (card S) \<and> finite S; S \<subseteq> S0\<rbrakk> \<Longrightarrow> Suc \<sigma> = min n (card (insert x S)) \<and> finite (insert x S)
 3. \<And>\<sigma>. \<sigma> = min n (card S0) \<and> finite S0 \<Longrightarrow> \<sigma> = min n (card S0) \<and> finite S0
 4. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<not> \<sigma> < n; \<sigma> = min n (card S) \<and> finite S\<rbrakk> \<Longrightarrow> \<sigma> = min n (card S0) \<and> finite S0
[PROOF STEP]
from card_mono [OF fin_S0 \<open>S \<subseteq> S0\<close>]
[PROOF STATE]
proof (chain)
picking this:
card S \<le> card S0
[PROOF STEP]
have "card S \<le> card S0"
[PROOF STATE]
proof (prove)
using this:
card S \<le> card S0

goal (1 subgoal):
 1. card S \<le> card S0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card S \<le> card S0

goal (4 subgoals):
 1. 0 = min n (card {}) \<and> finite {}
 2. \<And>S \<sigma> x. \<lbrakk>\<sigma> < n; x \<in> S0 - S; \<sigma> = min n (card S) \<and> finite S; S \<subseteq> S0\<rbrakk> \<Longrightarrow> Suc \<sigma> = min n (card (insert x S)) \<and> finite (insert x S)
 3. \<And>\<sigma>. \<sigma> = min n (card S0) \<and> finite S0 \<Longrightarrow> \<sigma> = min n (card S0) \<and> finite S0
 4. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<not> \<sigma> < n; \<sigma> = min n (card S) \<and> finite S\<rbrakk> \<Longrightarrow> \<sigma> = min n (card S0) \<and> finite S0
[PROOF STEP]
with \<open>\<sigma> = n\<close> \<open>n \<le> card S\<close> fin_S0
[PROOF STATE]
proof (chain)
picking this:
\<sigma> = n
n \<le> card S
finite S0
card S \<le> card S0
[PROOF STEP]
show "\<sigma> = min n (card S0) \<and> finite S0"
[PROOF STATE]
proof (prove)
using this:
\<sigma> = n
n \<le> card S
finite S0
card S \<le> card S0

goal (1 subgoal):
 1. \<sigma> = min n (card S0) \<and> finite S0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<sigma> = min n (card S0) \<and> finite S0

goal (3 subgoals):
 1. 0 = min n (card {}) \<and> finite {}
 2. \<And>S \<sigma> x. \<lbrakk>\<sigma> < n; x \<in> S0 - S; \<sigma> = min n (card S) \<and> finite S; S \<subseteq> S0\<rbrakk> \<Longrightarrow> Suc \<sigma> = min n (card (insert x S)) \<and> finite (insert x S)
 3. \<And>\<sigma>. \<sigma> = min n (card S0) \<and> finite S0 \<Longrightarrow> \<sigma> = min n (card S0) \<and> finite S0
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma iterate_is_empty_by_size_correct :
assumes it: "set_iterator it S0"
shows "iterate_is_empty_by_size it = (S0 = {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iterate_is_empty_by_size it = (S0 = {})
[PROOF STEP]
using iterate_size_abort_correct[OF it, of 1]
[PROOF STATE]
proof (prove)
using this:
iterate_size_abort it 1 = min 1 (card S0) \<and> finite S0

goal (1 subgoal):
 1. iterate_is_empty_by_size it = (S0 = {})
[PROOF STEP]
unfolding iterate_is_empty_by_size_def
[PROOF STATE]
proof (prove)
using this:
iterate_size_abort it 1 = min 1 (card S0) \<and> finite S0

goal (1 subgoal):
 1. (iterate_size_abort it 1 = 0) = (S0 = {})
[PROOF STEP]
by (cases "card S0") auto


[STATEMENT]
lemma iterate_is_empty_correct :
assumes it: "set_iterator it S0"
shows "iterate_is_empty it = (S0 = {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iterate_is_empty it = (S0 = {})
[PROOF STEP]
unfolding iterate_is_empty_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it (\<lambda>b. b) (\<lambda>_ _. False) True = (S0 = {})
[PROOF STEP]
apply (rule set_iterator_rule_insert_P [OF it,
   where I = "\<lambda>S \<sigma>. \<sigma> \<longleftrightarrow> S = {}"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. True = ({} = {})
 2. \<And>S \<sigma> x. \<lbrakk>\<sigma>; x \<in> S0 - S; \<sigma> = (S = {}); S \<subseteq> S0\<rbrakk> \<Longrightarrow> False = (insert x S = {})
 3. \<And>\<sigma>. \<sigma> = (S0 = {}) \<Longrightarrow> \<sigma> = (S0 = {})
 4. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<not> \<sigma>; \<sigma> = (S = {})\<rbrakk> \<Longrightarrow> \<sigma> = (S0 = {})
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iterate_is_sng_correct :
assumes it: "set_iterator it S0"
shows "iterate_is_sng it = (card S0 = 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iterate_is_sng it = (card S0 = 1)
[PROOF STEP]
using iterate_size_abort_correct[OF it, of 2]
[PROOF STATE]
proof (prove)
using this:
iterate_size_abort it 2 = min 2 (card S0) \<and> finite S0

goal (1 subgoal):
 1. iterate_is_sng it = (card S0 = 1)
[PROOF STEP]
unfolding iterate_is_sng_def
[PROOF STATE]
proof (prove)
using this:
iterate_size_abort it 2 = min 2 (card S0) \<and> finite S0

goal (1 subgoal):
 1. (iterate_size_abort it 2 = 1) = (card S0 = 1)
[PROOF STEP]
apply (cases "card S0", simp, rename_tac n')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n'. \<lbrakk>iterate_size_abort it 2 = min 2 (card S0) \<and> finite S0; card S0 = Suc n'; iterate_size_abort it 2 = min 2 (card S0) \<and> finite S0\<rbrakk> \<Longrightarrow> (iterate_size_abort it 2 = 1) = (card S0 = 1)
[PROOF STEP]
apply (case_tac n')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n'. \<lbrakk>iterate_size_abort it 2 = min 2 (card S0) \<and> finite S0; card S0 = Suc n'; iterate_size_abort it 2 = min 2 (card S0) \<and> finite S0; n' = 0\<rbrakk> \<Longrightarrow> (iterate_size_abort it 2 = 1) = (card S0 = 1)
 2. \<And>n' nat. \<lbrakk>iterate_size_abort it 2 = min 2 (card S0) \<and> finite S0; card S0 = Suc n'; iterate_size_abort it 2 = min 2 (card S0) \<and> finite S0; n' = Suc nat\<rbrakk> \<Longrightarrow> (iterate_size_abort it 2 = 1) = (card S0 = 1)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iterate_sel_genord_correct :
assumes it_OK: "set_iterator_genord it S0 R"
shows "iterate_sel it f = None \<longleftrightarrow> (\<forall>x\<in>S0. (f x = None))"
      "iterate_sel it f = Some y \<Longrightarrow> (\<exists>x \<in> S0. f x = Some y \<and> (\<forall>x' \<in> S0-{x}. \<forall>y. f x' = Some y' \<longrightarrow> R x x'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iterate_sel it f = None) = (\<forall>x\<in>S0. f x = None) &&& (iterate_sel it f = Some y \<Longrightarrow> \<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y. f x' = Some y' \<longrightarrow> R x x'))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (iterate_sel it f = None) = (\<forall>x\<in>S0. f x = None)
 2. iterate_sel it f = Some y \<Longrightarrow> \<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y. f x' = Some y' \<longrightarrow> R x x')
[PROOF STEP]
show "iterate_sel it f = None \<longleftrightarrow> (\<forall>x\<in>S0. (f x = None))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iterate_sel it f = None) = (\<forall>x\<in>S0. f x = None)
[PROOF STEP]
unfolding iterate_sel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (it (\<lambda>\<sigma>. \<sigma> = None) (\<lambda>x \<sigma>. f x) None = None) = (\<forall>x\<in>S0. f x = None)
[PROOF STEP]
apply (rule_tac set_iterator_genord.iteratei_rule_insert_P [OF it_OK,
       where I = "\<lambda>S \<sigma>. (\<sigma> = None) \<longleftrightarrow> (\<forall>x\<in>S. (f x = None))"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (None = None) = (\<forall>x\<in>{}. f x = None)
 2. \<And>S \<sigma> x. \<lbrakk>\<sigma> = None; x \<in> S0 - S; (\<sigma> = None) = (\<forall>x\<in>S. f x = None); S \<subseteq> S0; \<forall>y\<in>S0 - S - {x}. R x y; \<forall>y\<in>S. R y x\<rbrakk> \<Longrightarrow> (f x = None) = (\<forall>x\<in>insert x S. f x = None)
 3. \<And>\<sigma>. (\<sigma> = None) = (\<forall>x\<in>S0. f x = None) \<Longrightarrow> (\<sigma> = None) = (\<forall>x\<in>S0. f x = None)
 4. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<sigma> \<noteq> None; (\<sigma> = None) = (\<forall>x\<in>S. f x = None); \<forall>x\<in>S0 - S. \<forall>y\<in>S. R y x\<rbrakk> \<Longrightarrow> (\<sigma> = None) = (\<forall>x\<in>S0. f x = None)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(iterate_sel it f = None) = (\<forall>x\<in>S0. f x = None)

goal (1 subgoal):
 1. iterate_sel it f = Some y \<Longrightarrow> \<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y. f x' = Some y' \<longrightarrow> R x x')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iterate_sel it f = Some y \<Longrightarrow> \<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y. f x' = Some y' \<longrightarrow> R x x')
[PROOF STEP]
have "iterate_sel it f = Some y \<longrightarrow> (\<exists>x \<in> S0. f x = Some y \<and> (\<forall>x' \<in> S0-{x}. \<forall>y'. f x' = Some y' \<longrightarrow> R x x'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iterate_sel it f = Some y \<longrightarrow> (\<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y'. f x' = Some y' \<longrightarrow> R x x'))
[PROOF STEP]
unfolding iterate_sel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it (\<lambda>\<sigma>. \<sigma> = None) (\<lambda>x \<sigma>. f x) None = Some y \<longrightarrow> (\<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y'. f x' = Some y' \<longrightarrow> R x x'))
[PROOF STEP]
apply (rule_tac set_iterator_genord.iteratei_rule_insert_P [OF it_OK,
       where I = "\<lambda>S \<sigma>. (\<forall>y. \<sigma> = Some y \<longrightarrow> (\<exists>x \<in> S. f x = Some y \<and> (\<forall>x' \<in> S-{x}.\<forall>y'. f x' = Some y' \<longrightarrow> R x x'))) \<and>
                        ((\<sigma> = None) \<longleftrightarrow> (\<forall>x\<in>S. f x = None))"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (\<forall>y. None = Some y \<longrightarrow> (\<exists>x\<in>{}. f x = Some y \<and> (\<forall>x'\<in>{} - {x}. \<forall>y'. f x' = Some y' \<longrightarrow> R x x'))) \<and> (None = None) = (\<forall>x\<in>{}. f x = None)
 2. \<And>S \<sigma> x. \<lbrakk>\<sigma> = None; x \<in> S0 - S; (\<forall>y. \<sigma> = Some y \<longrightarrow> (\<exists>x\<in>S. f x = Some y \<and> (\<forall>x'\<in>S - {x}. \<forall>y'. f x' = Some y' \<longrightarrow> R x x'))) \<and> (\<sigma> = None) = (\<forall>x\<in>S. f x = None); S \<subseteq> S0; \<forall>y\<in>S0 - S - {x}. R x y; \<forall>y\<in>S. R y x\<rbrakk> \<Longrightarrow> (\<forall>y. f x = Some y \<longrightarrow> (\<exists>xa\<in>insert x S. f xa = Some y \<and> (\<forall>x'\<in>insert x S - {xa}. \<forall>y'. f x' = Some y' \<longrightarrow> R xa x'))) \<and> (f x = None) = (\<forall>x\<in>insert x S. f x = None)
 3. \<And>\<sigma>. (\<forall>y. \<sigma> = Some y \<longrightarrow> (\<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y'. f x' = Some y' \<longrightarrow> R x x'))) \<and> (\<sigma> = None) = (\<forall>x\<in>S0. f x = None) \<Longrightarrow> \<sigma> = Some y \<longrightarrow> (\<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y'. f x' = Some y' \<longrightarrow> R x x'))
 4. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<sigma> \<noteq> None; (\<forall>y. \<sigma> = Some y \<longrightarrow> (\<exists>x\<in>S. f x = Some y \<and> (\<forall>x'\<in>S - {x}. \<forall>y'. f x' = Some y' \<longrightarrow> R x x'))) \<and> (\<sigma> = None) = (\<forall>x\<in>S. f x = None); \<forall>x\<in>S0 - S. \<forall>y\<in>S. R y x\<rbrakk> \<Longrightarrow> \<sigma> = Some y \<longrightarrow> (\<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y'. f x' = Some y' \<longrightarrow> R x x'))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>S \<sigma> x. \<lbrakk>\<sigma> = None; x \<in> S0 - S; (\<forall>y. \<sigma> = Some y \<longrightarrow> (\<exists>x\<in>S. f x = Some y \<and> (\<forall>x'\<in>S - {x}. \<forall>y'. f x' = Some y' \<longrightarrow> R x x'))) \<and> (\<sigma> = None) = (\<forall>x\<in>S. f x = None); S \<subseteq> S0; \<forall>y\<in>S0 - S - {x}. R x y; \<forall>y\<in>S. R y x\<rbrakk> \<Longrightarrow> (\<forall>y. f x = Some y \<longrightarrow> (\<exists>xa\<in>insert x S. f xa = Some y \<and> (\<forall>x'\<in>insert x S - {xa}. \<forall>y'. f x' = Some y' \<longrightarrow> R xa x'))) \<and> (f x = None) = (\<forall>x\<in>insert x S. f x = None)
 2. \<And>\<sigma>. (\<forall>y. \<sigma> = Some y \<longrightarrow> (\<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y'. f x' = Some y' \<longrightarrow> R x x'))) \<and> (\<sigma> = None) = (\<forall>x\<in>S0. f x = None) \<Longrightarrow> \<sigma> = Some y \<longrightarrow> (\<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y'. f x' = Some y' \<longrightarrow> R x x'))
 3. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<sigma> \<noteq> None; (\<forall>y. \<sigma> = Some y \<longrightarrow> (\<exists>x\<in>S. f x = Some y \<and> (\<forall>x'\<in>S - {x}. \<forall>y'. f x' = Some y' \<longrightarrow> R x x'))) \<and> (\<sigma> = None) = (\<forall>x\<in>S. f x = None); \<forall>x\<in>S0 - S. \<forall>y\<in>S. R y x\<rbrakk> \<Longrightarrow> \<sigma> = Some y \<longrightarrow> (\<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y'. f x' = Some y' \<longrightarrow> R x x'))
[PROOF STEP]
apply (auto simp add: Bex_def subset_iff Ball_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S x ya xa xb xc. \<lbrakk>\<forall>t. t \<in> S \<longrightarrow> t \<in> S0; \<forall>x. x \<in> S0 \<and> x \<notin> S \<longrightarrow> (\<forall>xa. xa \<in> S \<longrightarrow> R xa x); x \<in> S; f x = Some ya; \<forall>x. f x = Some y \<longrightarrow> x \<in> S0 \<longrightarrow> (\<exists>xa. xa \<in> S0 \<and> xa \<noteq> x \<and> (\<exists>y'. f xa = Some y') \<and> \<not> R x xa); xa \<in> S0; xa \<notin> S; xb \<in> S; xc \<in> S; f xc = Some y; \<forall>x. x \<in> S \<and> x \<noteq> xc \<longrightarrow> (\<exists>y'. f x = Some y') \<longrightarrow> R xc x\<rbrakk> \<Longrightarrow> f xb = None
[PROOF STEP]
apply metis
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
iterate_sel it f = Some y \<longrightarrow> (\<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y'. f x' = Some y' \<longrightarrow> R x x'))

goal (1 subgoal):
 1. iterate_sel it f = Some y \<Longrightarrow> \<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y. f x' = Some y' \<longrightarrow> R x x')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
iterate_sel it f = Some y \<longrightarrow> (\<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y'. f x' = Some y' \<longrightarrow> R x x'))

goal (1 subgoal):
 1. iterate_sel it f = Some y \<Longrightarrow> \<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y. f x' = Some y' \<longrightarrow> R x x')
[PROOF STEP]
assume "iterate_sel it f = Some y"
[PROOF STATE]
proof (state)
this:
iterate_sel it f = Some y

goal (1 subgoal):
 1. iterate_sel it f = Some y \<Longrightarrow> \<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y. f x' = Some y' \<longrightarrow> R x x')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y'. f x' = Some y' \<longrightarrow> R x x')
[PROOF STEP]
show "(\<exists>x \<in> S0. f x = Some y \<and> (\<forall>x' \<in> S0-{x}. \<forall>y. f x' = Some y' \<longrightarrow> R x x'))"
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y'. f x' = Some y' \<longrightarrow> R x x')

goal (1 subgoal):
 1. \<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y. f x' = Some y' \<longrightarrow> R x x')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>S0. f x = Some y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y. f x' = Some y' \<longrightarrow> R x x')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iterate_sel_no_map_genord_correct :
assumes it_OK: "set_iterator_genord it S0 R"
shows "iterate_sel_no_map it P = None \<longleftrightarrow> (\<forall>x\<in>S0. \<not>(P x))"
      "iterate_sel_no_map it P = Some x \<Longrightarrow> (x \<in> S0 \<and> P x \<and> (\<forall>x' \<in> S0-{x}. P x' \<longrightarrow> R x x'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x) &&& (iterate_sel_no_map it P = Some x \<Longrightarrow> x \<in> S0 \<and> P x \<and> (\<forall>x'\<in>S0 - {x}. P x' \<longrightarrow> R x x'))
[PROOF STEP]
unfolding iterate_sel_no_map_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iterate_sel it (\<lambda>x. if P x then Some x else None) = None) = (\<forall>x\<in>S0. \<not> P x) &&& (iterate_sel it (\<lambda>x. if P x then Some x else None) = Some x \<Longrightarrow> x \<in> S0 \<and> P x \<and> (\<forall>x'\<in>S0 - {x}. P x' \<longrightarrow> R x x'))
[PROOF STEP]
using iterate_sel_genord_correct[OF it_OK, of "\<lambda>x. if P x then Some x else None"]
[PROOF STATE]
proof (prove)
using this:
(iterate_sel it (\<lambda>x. if P x then Some x else None) = None) = (\<forall>x\<in>S0. (if P x then Some x else None) = None)
iterate_sel it (\<lambda>x. if P x then Some x else None) = Some ?y \<Longrightarrow> \<exists>x\<in>S0. (if P x then Some x else None) = Some ?y \<and> (\<forall>x'\<in>S0 - {x}. \<forall>y. (if P x' then Some x' else None) = Some ?y' \<longrightarrow> R x x')

goal (1 subgoal):
 1. (iterate_sel it (\<lambda>x. if P x then Some x else None) = None) = (\<forall>x\<in>S0. \<not> P x) &&& (iterate_sel it (\<lambda>x. if P x then Some x else None) = Some x \<Longrightarrow> x \<in> S0 \<and> P x \<and> (\<forall>x'\<in>S0 - {x}. P x' \<longrightarrow> R x x'))
[PROOF STEP]
apply (simp_all add: Bex_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>iterate_sel it (\<lambda>x. if P x then Some x else None) = Some x; \<exists>x. x \<in> S0 \<and> (\<exists>y. (if P x then Some x else None) = Some y); \<And>y y'. x = y \<Longrightarrow> \<exists>x. x \<in> S0 \<and> (if P x then Some x else None) = Some y \<and> (\<forall>x'\<in>S0 - {x}. (if P x' then Some x' else None) = Some y' \<longrightarrow> R x x')\<rbrakk> \<Longrightarrow> x \<in> S0 \<and> P x \<and> (\<forall>x'\<in>S0 - {x}. P x' \<longrightarrow> R x x')
[PROOF STEP]
apply (metis option.inject option.simps(2))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iterate_sel_no_map_correct :
assumes it_OK: "set_iterator it S0"
shows "iterate_sel_no_map it P = None \<longleftrightarrow> (\<forall>x\<in>S0. \<not>(P x))"
      "iterate_sel_no_map it P = Some x \<Longrightarrow> x \<in> S0 \<and> P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x) &&& (iterate_sel_no_map it P = Some x \<Longrightarrow> x \<in> S0 \<and> P x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x)
 2. iterate_sel_no_map it P = Some x \<Longrightarrow> x \<in> S0 \<and> P x
[PROOF STEP]
note iterate_sel_no_map_genord_correct [OF it_OK[unfolded set_iterator_def], of P]
[PROOF STATE]
proof (state)
this:
(iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x)
iterate_sel_no_map it P = Some ?x \<Longrightarrow> ?x \<in> S0 \<and> P ?x \<and> (\<forall>x'\<in>S0 - {?x}. P x' \<longrightarrow> True)

goal (2 subgoals):
 1. (iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x)
 2. iterate_sel_no_map it P = Some x \<Longrightarrow> x \<in> S0 \<and> P x
[PROOF STEP]
thus "iterate_sel_no_map it P = None \<longleftrightarrow> (\<forall>x\<in>S0. \<not>(P x))"
       "iterate_sel_no_map it P = Some x \<Longrightarrow> x \<in> S0 \<and> P x"
[PROOF STATE]
proof (prove)
using this:
(iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x)
iterate_sel_no_map it P = Some ?x \<Longrightarrow> ?x \<in> S0 \<and> P ?x \<and> (\<forall>x'\<in>S0 - {?x}. P x' \<longrightarrow> True)

goal (1 subgoal):
 1. (iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x) &&& (iterate_sel_no_map it P = Some x \<Longrightarrow> x \<in> S0 \<and> P x)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
(iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x)
iterate_sel_no_map it P = Some x \<Longrightarrow> x \<in> S0 \<and> P x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in linorder) iterate_sel_no_map_linord_correct :
assumes it_OK: "set_iterator_linord it S0"
shows "iterate_sel_no_map it P = None \<longleftrightarrow> (\<forall>x\<in>S0. \<not>(P x))"
      "iterate_sel_no_map it P = Some x \<Longrightarrow> (x \<in> S0 \<and> P x \<and> (\<forall>x'\<in>S0. P x' \<longrightarrow> x \<le> x'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x) &&& (iterate_sel_no_map it P = Some x \<Longrightarrow> x \<in> S0 \<and> P x \<and> (\<forall>x'\<in>S0. P x' \<longrightarrow> x \<le> x'))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x)
 2. iterate_sel_no_map it P = Some x \<Longrightarrow> x \<in> S0 \<and> P x \<and> (\<forall>x'\<in>S0. P x' \<longrightarrow> x \<le> x')
[PROOF STEP]
note iterate_sel_no_map_genord_correct [OF it_OK[unfolded set_iterator_linord_def], of P]
[PROOF STATE]
proof (state)
this:
(iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x)
iterate_sel_no_map it P = Some ?x \<Longrightarrow> ?x \<in> S0 \<and> P ?x \<and> (\<forall>x'\<in>S0 - {?x}. P x' \<longrightarrow> ?x \<le> x')

goal (2 subgoals):
 1. (iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x)
 2. iterate_sel_no_map it P = Some x \<Longrightarrow> x \<in> S0 \<and> P x \<and> (\<forall>x'\<in>S0. P x' \<longrightarrow> x \<le> x')
[PROOF STEP]
thus "iterate_sel_no_map it P = None \<longleftrightarrow> (\<forall>x\<in>S0. \<not>(P x))"
       "iterate_sel_no_map it P = Some x \<Longrightarrow> (x \<in> S0 \<and> P x \<and> (\<forall>x'\<in>S0. P x' \<longrightarrow> x \<le> x'))"
[PROOF STATE]
proof (prove)
using this:
(iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x)
iterate_sel_no_map it P = Some ?x \<Longrightarrow> ?x \<in> S0 \<and> P ?x \<and> (\<forall>x'\<in>S0 - {?x}. P x' \<longrightarrow> ?x \<le> x')

goal (1 subgoal):
 1. (iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x) &&& (iterate_sel_no_map it P = Some x \<Longrightarrow> x \<in> S0 \<and> P x \<and> (\<forall>x'\<in>S0. P x' \<longrightarrow> x \<le> x'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x)
iterate_sel_no_map it P = Some x \<Longrightarrow> x \<in> S0 \<and> P x \<and> (\<forall>x'\<in>S0. P x' \<longrightarrow> x \<le> x')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in linorder) iterate_sel_no_map_rev_linord_correct :
assumes it_OK: "set_iterator_rev_linord it S0"
shows "iterate_sel_no_map it P = None \<longleftrightarrow> (\<forall>x\<in>S0. \<not>(P x))"
      "iterate_sel_no_map it P = Some x \<Longrightarrow> (x \<in> S0 \<and> P x \<and> (\<forall>x'\<in>S0. P x' \<longrightarrow> x' \<le> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x) &&& (iterate_sel_no_map it P = Some x \<Longrightarrow> x \<in> S0 \<and> P x \<and> (\<forall>x'\<in>S0. P x' \<longrightarrow> x' \<le> x))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x)
 2. iterate_sel_no_map it P = Some x \<Longrightarrow> x \<in> S0 \<and> P x \<and> (\<forall>x'\<in>S0. P x' \<longrightarrow> x' \<le> x)
[PROOF STEP]
note iterate_sel_no_map_genord_correct [OF it_OK[unfolded set_iterator_rev_linord_def], of P]
[PROOF STATE]
proof (state)
this:
(iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x)
iterate_sel_no_map it P = Some ?x \<Longrightarrow> ?x \<in> S0 \<and> P ?x \<and> (\<forall>x'\<in>S0 - {?x}. P x' \<longrightarrow> x' \<le> ?x)

goal (2 subgoals):
 1. (iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x)
 2. iterate_sel_no_map it P = Some x \<Longrightarrow> x \<in> S0 \<and> P x \<and> (\<forall>x'\<in>S0. P x' \<longrightarrow> x' \<le> x)
[PROOF STEP]
thus "iterate_sel_no_map it P = None \<longleftrightarrow> (\<forall>x\<in>S0. \<not>(P x))"
       "iterate_sel_no_map it P = Some x \<Longrightarrow> (x \<in> S0 \<and> P x \<and> (\<forall>x'\<in>S0. P x' \<longrightarrow> x' \<le> x))"
[PROOF STATE]
proof (prove)
using this:
(iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x)
iterate_sel_no_map it P = Some ?x \<Longrightarrow> ?x \<in> S0 \<and> P ?x \<and> (\<forall>x'\<in>S0 - {?x}. P x' \<longrightarrow> x' \<le> ?x)

goal (1 subgoal):
 1. (iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x) &&& (iterate_sel_no_map it P = Some x \<Longrightarrow> x \<in> S0 \<and> P x \<and> (\<forall>x'\<in>S0. P x' \<longrightarrow> x' \<le> x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(iterate_sel_no_map it P = None) = (\<forall>x\<in>S0. \<not> P x)
iterate_sel_no_map it P = Some x \<Longrightarrow> x \<in> S0 \<and> P x \<and> (\<forall>x'\<in>S0. P x' \<longrightarrow> x' \<le> x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iterate_sel_no_map_map_correct :
assumes it_OK: "map_iterator it m"
shows "iterate_sel_no_map it P = None \<longleftrightarrow> (\<forall>k v. m k = Some v \<longrightarrow> \<not>(P (k, v)))"
      "iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> (m k = Some v \<and> P (k, v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iterate_sel_no_map it P = None) = (\<forall>k v. m k = Some v \<longrightarrow> \<not> P (k, v)) &&& (iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> m k = Some v \<and> P (k, v))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (iterate_sel_no_map it P = None) = (\<forall>k v. m k = Some v \<longrightarrow> \<not> P (k, v))
 2. iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> m k = Some v \<and> P (k, v)
[PROOF STEP]
note iterate_sel_no_map_genord_correct [OF it_OK[unfolded set_iterator_def], of P]
[PROOF STATE]
proof (state)
this:
(iterate_sel_no_map it P = None) = (\<forall>x\<in>map_to_set m. \<not> P x)
iterate_sel_no_map it P = Some ?x \<Longrightarrow> ?x \<in> map_to_set m \<and> P ?x \<and> (\<forall>x'\<in>map_to_set m - {?x}. P x' \<longrightarrow> True)

goal (2 subgoals):
 1. (iterate_sel_no_map it P = None) = (\<forall>k v. m k = Some v \<longrightarrow> \<not> P (k, v))
 2. iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> m k = Some v \<and> P (k, v)
[PROOF STEP]
thus "iterate_sel_no_map it P = None \<longleftrightarrow> (\<forall>k v. m k = Some v \<longrightarrow> \<not>(P (k, v)))"
       "iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> (m k = Some v \<and> P (k, v))"
[PROOF STATE]
proof (prove)
using this:
(iterate_sel_no_map it P = None) = (\<forall>x\<in>map_to_set m. \<not> P x)
iterate_sel_no_map it P = Some ?x \<Longrightarrow> ?x \<in> map_to_set m \<and> P ?x \<and> (\<forall>x'\<in>map_to_set m - {?x}. P x' \<longrightarrow> True)

goal (1 subgoal):
 1. (iterate_sel_no_map it P = None) = (\<forall>k v. m k = Some v \<longrightarrow> \<not> P (k, v)) &&& (iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> m k = Some v \<and> P (k, v))
[PROOF STEP]
by (auto simp add: map_to_set_def)
[PROOF STATE]
proof (state)
this:
(iterate_sel_no_map it P = None) = (\<forall>k v. m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> m k = Some v \<and> P (k, v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in linorder) iterate_sel_no_map_map_linord_correct :
assumes it_OK: "map_iterator_linord it m"
shows "iterate_sel_no_map it P = None \<longleftrightarrow> (\<forall>k v. m k = Some v \<longrightarrow> \<not>(P (k, v)))"
      "iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> (m k = Some v \<and> P (k, v) \<and> (\<forall>k' v' . m k' = Some v' \<and>
           P (k', v') \<longrightarrow> k \<le> k'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iterate_sel_no_map it P = None) = (\<forall>k v. m k = Some v \<longrightarrow> \<not> P (k, v)) &&& (iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> m k = Some v \<and> P (k, v) \<and> (\<forall>k' v'. m k' = Some v' \<and> P (k', v') \<longrightarrow> k \<le> k'))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (iterate_sel_no_map it P = None) = (\<forall>k v. m k = Some v \<longrightarrow> \<not> P (k, v))
 2. iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> m k = Some v \<and> P (k, v) \<and> (\<forall>k' v'. m k' = Some v' \<and> P (k', v') \<longrightarrow> k \<le> k')
[PROOF STEP]
note iterate_sel_no_map_genord_correct [OF it_OK[unfolded set_iterator_map_linord_def], of P]
[PROOF STATE]
proof (state)
this:
(iterate_sel_no_map it P = None) = (\<forall>x\<in>map_to_set m. \<not> P x)
iterate_sel_no_map it P = Some ?x \<Longrightarrow> ?x \<in> map_to_set m \<and> P ?x \<and> (\<forall>x'\<in>map_to_set m - {?x}. P x' \<longrightarrow> (case ?x of (k, uu_) \<Rightarrow> \<lambda>(k', uu_). k \<le> k') x')

goal (2 subgoals):
 1. (iterate_sel_no_map it P = None) = (\<forall>k v. m k = Some v \<longrightarrow> \<not> P (k, v))
 2. iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> m k = Some v \<and> P (k, v) \<and> (\<forall>k' v'. m k' = Some v' \<and> P (k', v') \<longrightarrow> k \<le> k')
[PROOF STEP]
thus "iterate_sel_no_map it P = None \<longleftrightarrow> (\<forall>k v. m k = Some v \<longrightarrow> \<not>(P (k, v)))"
       "iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> (m k = Some v \<and> P (k, v) \<and> (\<forall>k' v' . m k' = Some v' \<and>
           P (k', v') \<longrightarrow> k \<le> k'))"
[PROOF STATE]
proof (prove)
using this:
(iterate_sel_no_map it P = None) = (\<forall>x\<in>map_to_set m. \<not> P x)
iterate_sel_no_map it P = Some ?x \<Longrightarrow> ?x \<in> map_to_set m \<and> P ?x \<and> (\<forall>x'\<in>map_to_set m - {?x}. P x' \<longrightarrow> (case ?x of (k, uu_) \<Rightarrow> \<lambda>(k', uu_). k \<le> k') x')

goal (1 subgoal):
 1. (iterate_sel_no_map it P = None) = (\<forall>k v. m k = Some v \<longrightarrow> \<not> P (k, v)) &&& (iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> m k = Some v \<and> P (k, v) \<and> (\<forall>k' v'. m k' = Some v' \<and> P (k', v') \<longrightarrow> k \<le> k'))
[PROOF STEP]
apply (auto simp add: map_to_set_def Ball_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(iterate_sel_no_map it P = None) = (\<forall>k v. m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> m k = Some v \<and> P (k, v) \<and> (\<forall>k' v'. m k' = Some v' \<and> P (k', v') \<longrightarrow> k \<le> k')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in linorder) iterate_sel_no_map_map_rev_linord_correct :
assumes it_OK: "map_iterator_rev_linord it m"
shows "iterate_sel_no_map it P = None \<longleftrightarrow> (\<forall>k v. m k = Some v \<longrightarrow> \<not>(P (k, v)))"
      "iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> (m k = Some v \<and> P (k, v) \<and> (\<forall>k' v' . m k' = Some v' \<and>
           P (k', v') \<longrightarrow> k' \<le> k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iterate_sel_no_map it P = None) = (\<forall>k v. m k = Some v \<longrightarrow> \<not> P (k, v)) &&& (iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> m k = Some v \<and> P (k, v) \<and> (\<forall>k' v'. m k' = Some v' \<and> P (k', v') \<longrightarrow> k' \<le> k))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (iterate_sel_no_map it P = None) = (\<forall>k v. m k = Some v \<longrightarrow> \<not> P (k, v))
 2. iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> m k = Some v \<and> P (k, v) \<and> (\<forall>k' v'. m k' = Some v' \<and> P (k', v') \<longrightarrow> k' \<le> k)
[PROOF STEP]
note iterate_sel_no_map_genord_correct [OF it_OK[unfolded set_iterator_map_rev_linord_def], of P]
[PROOF STATE]
proof (state)
this:
(iterate_sel_no_map it P = None) = (\<forall>x\<in>map_to_set m. \<not> P x)
iterate_sel_no_map it P = Some ?x \<Longrightarrow> ?x \<in> map_to_set m \<and> P ?x \<and> (\<forall>x'\<in>map_to_set m - {?x}. P x' \<longrightarrow> (case ?x of (k, uu_) \<Rightarrow> \<lambda>(k', uu_). k' \<le> k) x')

goal (2 subgoals):
 1. (iterate_sel_no_map it P = None) = (\<forall>k v. m k = Some v \<longrightarrow> \<not> P (k, v))
 2. iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> m k = Some v \<and> P (k, v) \<and> (\<forall>k' v'. m k' = Some v' \<and> P (k', v') \<longrightarrow> k' \<le> k)
[PROOF STEP]
thus "iterate_sel_no_map it P = None \<longleftrightarrow> (\<forall>k v. m k = Some v \<longrightarrow> \<not>(P (k, v)))"
       "iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> (m k = Some v \<and> P (k, v) \<and> (\<forall>k' v' . m k' = Some v' \<and>
           P (k', v') \<longrightarrow> k' \<le> k))"
[PROOF STATE]
proof (prove)
using this:
(iterate_sel_no_map it P = None) = (\<forall>x\<in>map_to_set m. \<not> P x)
iterate_sel_no_map it P = Some ?x \<Longrightarrow> ?x \<in> map_to_set m \<and> P ?x \<and> (\<forall>x'\<in>map_to_set m - {?x}. P x' \<longrightarrow> (case ?x of (k, uu_) \<Rightarrow> \<lambda>(k', uu_). k' \<le> k) x')

goal (1 subgoal):
 1. (iterate_sel_no_map it P = None) = (\<forall>k v. m k = Some v \<longrightarrow> \<not> P (k, v)) &&& (iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> m k = Some v \<and> P (k, v) \<and> (\<forall>k' v'. m k' = Some v' \<and> P (k', v') \<longrightarrow> k' \<le> k))
[PROOF STEP]
apply (auto simp add: map_to_set_def Ball_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(iterate_sel_no_map it P = None) = (\<forall>k v. m k = Some v \<longrightarrow> \<not> P (k, v))
iterate_sel_no_map it P = Some (k, v) \<Longrightarrow> m k = Some v \<and> P (k, v) \<and> (\<forall>k' v'. m k' = Some v' \<and> P (k', v') \<longrightarrow> k' \<le> k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iterator_to_ordered_iterator_correct :
assumes sort_fun_OK: "\<And>l. sorted_wrt R (sort_fun l) \<and> mset (sort_fun l) = mset l"
    and it_OK: "set_iterator it S0"
shows "set_iterator_genord (iterator_to_ordered_iterator sort_fun it) S0 R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_genord (iterator_to_ordered_iterator sort_fun it) S0 R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set_iterator_genord (iterator_to_ordered_iterator sort_fun it) S0 R
[PROOF STEP]
define l where "l = iterate_to_list it"
[PROOF STATE]
proof (state)
this:
l = iterate_to_list it

goal (1 subgoal):
 1. set_iterator_genord (iterator_to_ordered_iterator sort_fun it) S0 R
[PROOF STEP]
have l_props: "set l = S0" "distinct l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set l = S0 &&& distinct l
[PROOF STEP]
using iterate_to_list_correct [OF it_OK, folded l_def]
[PROOF STATE]
proof (prove)
using this:
set l = S0 \<and> distinct l

goal (1 subgoal):
 1. set l = S0 &&& distinct l
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
set l = S0
distinct l

goal (1 subgoal):
 1. set_iterator_genord (iterator_to_ordered_iterator sort_fun it) S0 R
[PROOF STEP]
with sort_fun_OK[of l]
[PROOF STATE]
proof (chain)
picking this:
sorted_wrt R (sort_fun l) \<and> mset (sort_fun l) = mset l
set l = S0
distinct l
[PROOF STEP]
have sort_l_props:
    "sorted_wrt R (sort_fun l)"
    "set (sort_fun l) = S0" "distinct (sort_fun l)"
[PROOF STATE]
proof (prove)
using this:
sorted_wrt R (sort_fun l) \<and> mset (sort_fun l) = mset l
set l = S0
distinct l

goal (1 subgoal):
 1. sorted_wrt R (sort_fun l) &&& set (sort_fun l) = S0 &&& distinct (sort_fun l)
[PROOF STEP]
apply (simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sorted_wrt R (sort_fun l) \<and> mset (sort_fun l) = mset l; set l = S0; distinct l\<rbrakk> \<Longrightarrow> set (sort_fun l) = S0
 2. \<lbrakk>sorted_wrt R (sort_fun l) \<and> mset (sort_fun l) = mset l; set l = S0; distinct l\<rbrakk> \<Longrightarrow> distinct (sort_fun l)
[PROOF STEP]
apply (metis set_mset_mset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sorted_wrt R (sort_fun l) \<and> mset (sort_fun l) = mset l; set l = S0; distinct l\<rbrakk> \<Longrightarrow> distinct (sort_fun l)
[PROOF STEP]
apply (metis distinct_count_atmost_1 set_mset_mset)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
sorted_wrt R (sort_fun l)
set (sort_fun l) = S0
distinct (sort_fun l)

goal (1 subgoal):
 1. set_iterator_genord (iterator_to_ordered_iterator sort_fun it) S0 R
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_genord (iterator_to_ordered_iterator sort_fun it) S0 R
[PROOF STEP]
apply (rule set_iterator_genord_I[of "sort_fun l"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. distinct (sort_fun l)
 2. S0 = set (sort_fun l)
 3. sorted_wrt R (sort_fun l)
 4. iterator_to_ordered_iterator sort_fun it = foldli (sort_fun l)
[PROOF STEP]
apply (simp_all add: sort_l_props iterator_to_ordered_iterator_def l_def[symmetric])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
set_iterator_genord (iterator_to_ordered_iterator sort_fun it) S0 R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iterator_to_ordered_iterator_quicksort_correct :
assumes lin : "\<And>x y. (R x y) \<or> (R y x)"
    and trans_R: "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
    and it_OK: "set_iterator it S0"
shows "set_iterator_genord (iterator_to_ordered_iterator_quicksort R it) S0 R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_genord (iterator_to_ordered_iterator_quicksort R it) S0 R
[PROOF STEP]
unfolding iterator_to_ordered_iterator_quicksort_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_genord (iterator_to_ordered_iterator (quicksort_by_rel R []) it) S0 R
[PROOF STEP]
apply (rule iterator_to_ordered_iterator_correct [OF _ it_OK])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. sorted_wrt R (quicksort_by_rel R [] l) \<and> mset (quicksort_by_rel R [] l) = mset l
[PROOF STEP]
apply (simp_all add: sorted_wrt_quicksort_by_rel[OF lin trans_R])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iterator_to_ordered_iterator_mergesort_correct :
assumes lin : "\<And>x y. (R x y) \<or> (R y x)"
    and trans_R: "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
    and it_OK: "set_iterator it S0"
shows "set_iterator_genord (iterator_to_ordered_iterator_mergesort R it) S0 R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_genord (iterator_to_ordered_iterator_mergesort R it) S0 R
[PROOF STEP]
unfolding iterator_to_ordered_iterator_mergesort_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_genord (iterator_to_ordered_iterator (mergesort_by_rel R) it) S0 R
[PROOF STEP]
apply (rule iterator_to_ordered_iterator_correct [OF _ it_OK])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. sorted_wrt R (mergesort_by_rel R l) \<and> mset (mergesort_by_rel R l) = mset l
[PROOF STEP]
apply (simp_all add: sorted_wrt_mergesort_by_rel[OF lin trans_R])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mappings\<^sub>C_code:
  "mappings\<^sub>C \<Sigma> \<phi> = (
    let
      Gs = G_list \<phi>;
      max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of\<^sub>C \<Sigma>))
    in
      set (concat (map (mapping_generator_list (\<lambda>x. [0 ..< the (max_rank x)])) (subseqs Gs))))"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mappings\<^sub>C \<Sigma> \<phi> = (let Gs = G_list \<phi>; max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of\<^sub>C \<Sigma>)) in set (concat (map (mapping_generator_list (\<lambda>x. [0..<the (max_rank x)])) (subseqs Gs))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mappings\<^sub>C \<Sigma> \<phi> = (let Gs = G_list \<phi>; max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of\<^sub>C \<Sigma>)) in set (concat (map (mapping_generator_list (\<lambda>x. [0..<the (max_rank x)])) (subseqs Gs))))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mappings\<^sub>C \<Sigma> \<phi> = (let Gs = G_list \<phi>; max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of\<^sub>C \<Sigma>)) in set (concat (map (mapping_generator_list (\<lambda>x. [0..<the (max_rank x)])) (subseqs Gs))))
[PROOF STEP]
fix xs :: "'a ltl list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mappings\<^sub>C \<Sigma> \<phi> = (let Gs = G_list \<phi>; max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of\<^sub>C \<Sigma>)) in set (concat (map (mapping_generator_list (\<lambda>x. [0..<the (max_rank x)])) (subseqs Gs))))
[PROOF STEP]
have subset_G: "\<And>x. x \<in> set (subseqs (xs)) \<Longrightarrow> set x \<subseteq> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set (subseqs xs) \<Longrightarrow> set x \<subseteq> set xs
[PROOF STEP]
apply (induction xs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set (subseqs []) \<Longrightarrow> set x \<subseteq> set []
 2. \<And>a xs x. \<lbrakk>\<And>x. x \<in> set (subseqs xs) \<Longrightarrow> set x \<subseteq> set xs; x \<in> set (subseqs (a # xs))\<rbrakk> \<Longrightarrow> set x \<subseteq> set (a # xs)
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs x. \<lbrakk>\<And>x. x \<in> set (subseqs xs) \<Longrightarrow> set x \<subseteq> set xs; x \<in> set (subseqs (a # xs))\<rbrakk> \<Longrightarrow> set x \<subseteq> set (a # xs)
[PROOF STEP]
by (insert subseqs_powset; blast)
[PROOF STATE]
proof (state)
this:
?x17 \<in> set (subseqs xs) \<Longrightarrow> set ?x17 \<subseteq> set xs

goal (1 subgoal):
 1. mappings\<^sub>C \<Sigma> \<phi> = (let Gs = G_list \<phi>; max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of\<^sub>C \<Sigma>)) in set (concat (map (mapping_generator_list (\<lambda>x. [0..<the (max_rank x)])) (subseqs Gs))))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x17 \<in> set (subseqs ?xs20) \<Longrightarrow> set ?x17 \<subseteq> set ?xs20

goal (1 subgoal):
 1. mappings\<^sub>C \<Sigma> \<phi> = (let Gs = G_list \<phi>; max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of\<^sub>C \<Sigma>)) in set (concat (map (mapping_generator_list (\<lambda>x. [0..<the (max_rank x)])) (subseqs Gs))))
[PROOF STEP]
hence subset_G: "\<And>x. x \<in> set (subseqs (G_list \<phi>)) \<Longrightarrow> set x \<subseteq> \<^bold>G \<phi>"
[PROOF STATE]
proof (prove)
using this:
?x17 \<in> set (subseqs ?xs20) \<Longrightarrow> set ?x17 \<subseteq> set ?xs20

goal (1 subgoal):
 1. \<And>x. x \<in> set (subseqs (G_list \<phi>)) \<Longrightarrow> set x \<subseteq> \<^bold>G \<phi>
[PROOF STEP]
unfolding G_eq_G_list
[PROOF STATE]
proof (prove)
using this:
?x17 \<in> set (subseqs ?xs20) \<Longrightarrow> set ?x17 \<subseteq> set ?xs20

goal (1 subgoal):
 1. \<And>x. x \<in> set (subseqs (G_list \<phi>)) \<Longrightarrow> set x \<subseteq> set (G_list \<phi>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x17 \<in> set (subseqs (G_list \<phi>)) \<Longrightarrow> set ?x17 \<subseteq> \<^bold>G \<phi>

goal (1 subgoal):
 1. mappings\<^sub>C \<Sigma> \<phi> = (let Gs = G_list \<phi>; max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of\<^sub>C \<Sigma>)) in set (concat (map (mapping_generator_list (\<lambda>x. [0..<the (max_rank x)])) (subseqs Gs))))
[PROOF STEP]
have "?lhs = \<Union>{{\<pi>. Mapping.keys \<pi> = xs \<and> (\<forall>\<chi>\<in>Mapping.keys \<pi>. the (Mapping.lookup \<pi> \<chi>) < max_rank_of\<^sub>C \<Sigma> \<chi>)} | xs. xs \<in> set ` (set (subseqs (G_list \<phi>)))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mappings\<^sub>C \<Sigma> \<phi> = \<Union> {{\<pi>. Mapping.keys \<pi> = xs \<and> (\<forall>\<chi>\<in>Mapping.keys \<pi>. the (Mapping.lookup \<pi> \<chi>) < max_rank_of\<^sub>C \<Sigma> \<chi>)} |xs. xs \<in> set ` set (subseqs (G_list \<phi>))}
[PROOF STEP]
unfolding mappings\<^sub>C_def G_eq_G_list subseqs_powset
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<pi>. Mapping.keys \<pi> \<subseteq> set (G_list \<phi>) \<and> (\<forall>\<chi>\<in>Mapping.keys \<pi>. the (Mapping.lookup \<pi> \<chi>) < max_rank_of\<^sub>C \<Sigma> \<chi>)} = \<Union> {{\<pi>. Mapping.keys \<pi> = xs \<and> (\<forall>\<chi>\<in>Mapping.keys \<pi>. the (Mapping.lookup \<pi> \<chi>) < max_rank_of\<^sub>C \<Sigma> \<chi>)} |xs. xs \<in> Pow (set (G_list \<phi>))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mappings\<^sub>C \<Sigma> \<phi> = \<Union> {{\<pi>. Mapping.keys \<pi> = xs \<and> (\<forall>\<chi>\<in>Mapping.keys \<pi>. the (Mapping.lookup \<pi> \<chi>) < max_rank_of\<^sub>C \<Sigma> \<chi>)} |xs. xs \<in> set ` set (subseqs (G_list \<phi>))}

goal (1 subgoal):
 1. mappings\<^sub>C \<Sigma> \<phi> = (let Gs = G_list \<phi>; max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of\<^sub>C \<Sigma>)) in set (concat (map (mapping_generator_list (\<lambda>x. [0..<the (max_rank x)])) (subseqs Gs))))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mappings\<^sub>C \<Sigma> \<phi> = \<Union> {{\<pi>. Mapping.keys \<pi> = xs \<and> (\<forall>\<chi>\<in>Mapping.keys \<pi>. the (Mapping.lookup \<pi> \<chi>) < max_rank_of\<^sub>C \<Sigma> \<chi>)} |xs. xs \<in> set ` set (subseqs (G_list \<phi>))}

goal (1 subgoal):
 1. mappings\<^sub>C \<Sigma> \<phi> = (let Gs = G_list \<phi>; max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of\<^sub>C \<Sigma>)) in set (concat (map (mapping_generator_list (\<lambda>x. [0..<the (max_rank x)])) (subseqs Gs))))
[PROOF STEP]
have "\<dots> = \<Union>{{\<pi>. Mapping.keys \<pi> = set xs \<and> (\<forall>\<chi> \<in> set xs. the (Mapping.lookup \<pi> \<chi>) < max_rank_of\<^sub>C \<Sigma> \<chi>)} |
       xs. xs \<in> set (subseqs (G_list \<phi>))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> {{\<pi>. Mapping.keys \<pi> = xs \<and> (\<forall>\<chi>\<in>Mapping.keys \<pi>. the (Mapping.lookup \<pi> \<chi>) < max_rank_of\<^sub>C \<Sigma> \<chi>)} |xs. xs \<in> set ` set (subseqs (G_list \<phi>))} = \<Union> {{\<pi>. Mapping.keys \<pi> = set xs \<and> (\<forall>\<chi>\<in>set xs. the (Mapping.lookup \<pi> \<chi>) < max_rank_of\<^sub>C \<Sigma> \<chi>)} |xs. xs \<in> set (subseqs (G_list \<phi>))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Union> {{\<pi>. Mapping.keys \<pi> = xs \<and> (\<forall>\<chi>\<in>Mapping.keys \<pi>. the (Mapping.lookup \<pi> \<chi>) < max_rank_of\<^sub>C \<Sigma> \<chi>)} |xs. xs \<in> set ` set (subseqs (G_list \<phi>))} = \<Union> {{\<pi>. Mapping.keys \<pi> = set xs \<and> (\<forall>\<chi>\<in>set xs. the (Mapping.lookup \<pi> \<chi>) < max_rank_of\<^sub>C \<Sigma> \<chi>)} |xs. xs \<in> set (subseqs (G_list \<phi>))}

goal (1 subgoal):
 1. mappings\<^sub>C \<Sigma> \<phi> = (let Gs = G_list \<phi>; max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of\<^sub>C \<Sigma>)) in set (concat (map (mapping_generator_list (\<lambda>x. [0..<the (max_rank x)])) (subseqs Gs))))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Union> {{\<pi>. Mapping.keys \<pi> = xs \<and> (\<forall>\<chi>\<in>Mapping.keys \<pi>. the (Mapping.lookup \<pi> \<chi>) < max_rank_of\<^sub>C \<Sigma> \<chi>)} |xs. xs \<in> set ` set (subseqs (G_list \<phi>))} = \<Union> {{\<pi>. Mapping.keys \<pi> = set xs \<and> (\<forall>\<chi>\<in>set xs. the (Mapping.lookup \<pi> \<chi>) < max_rank_of\<^sub>C \<Sigma> \<chi>)} |xs. xs \<in> set (subseqs (G_list \<phi>))}

goal (1 subgoal):
 1. mappings\<^sub>C \<Sigma> \<phi> = (let Gs = G_list \<phi>; max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of\<^sub>C \<Sigma>)) in set (concat (map (mapping_generator_list (\<lambda>x. [0..<the (max_rank x)])) (subseqs Gs))))
[PROOF STEP]
have "\<dots> = ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> {{\<pi>. Mapping.keys \<pi> = set xs \<and> (\<forall>\<chi>\<in>set xs. the (Mapping.lookup \<pi> \<chi>) < max_rank_of\<^sub>C \<Sigma> \<chi>)} |xs. xs \<in> set (subseqs (G_list \<phi>))} = (let Gs = G_list \<phi>; max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of\<^sub>C \<Sigma>)) in set (concat (map (mapping_generator_list (\<lambda>x. [0..<the (max_rank x)])) (subseqs Gs))))
[PROOF STEP]
using subset_G
[PROOF STATE]
proof (prove)
using this:
?x17 \<in> set (subseqs (G_list \<phi>)) \<Longrightarrow> set ?x17 \<subseteq> \<^bold>G \<phi>

goal (1 subgoal):
 1. \<Union> {{\<pi>. Mapping.keys \<pi> = set xs \<and> (\<forall>\<chi>\<in>set xs. the (Mapping.lookup \<pi> \<chi>) < max_rank_of\<^sub>C \<Sigma> \<chi>)} |xs. xs \<in> set (subseqs (G_list \<phi>))} = (let Gs = G_list \<phi>; max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of\<^sub>C \<Sigma>)) in set (concat (map (mapping_generator_list (\<lambda>x. [0..<the (max_rank x)])) (subseqs Gs))))
[PROOF STEP]
by (auto simp add: Let_def mapping_generator_code [symmetric]
        lookup_tabulate G_eq_G_list [symmetric] mapping_generator_set_eq
        cong del: SUP_cong_simp; blast)
[PROOF STATE]
proof (state)
this:
\<Union> {{\<pi>. Mapping.keys \<pi> = set xs \<and> (\<forall>\<chi>\<in>set xs. the (Mapping.lookup \<pi> \<chi>) < max_rank_of\<^sub>C \<Sigma> \<chi>)} |xs. xs \<in> set (subseqs (G_list \<phi>))} = (let Gs = G_list \<phi>; max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of\<^sub>C \<Sigma>)) in set (concat (map (mapping_generator_list (\<lambda>x. [0..<the (max_rank x)])) (subseqs Gs))))

goal (1 subgoal):
 1. mappings\<^sub>C \<Sigma> \<phi> = (let Gs = G_list \<phi>; max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of\<^sub>C \<Sigma>)) in set (concat (map (mapping_generator_list (\<lambda>x. [0..<the (max_rank x)])) (subseqs Gs))))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mappings\<^sub>C \<Sigma> \<phi> = (let Gs = G_list \<phi>; max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of\<^sub>C \<Sigma>)) in set (concat (map (mapping_generator_list (\<lambda>x. [0..<the (max_rank x)])) (subseqs Gs))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mappings\<^sub>C \<Sigma> \<phi> = (let Gs = G_list \<phi>; max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of\<^sub>C \<Sigma>)) in set (concat (map (mapping_generator_list (\<lambda>x. [0..<the (max_rank x)])) (subseqs Gs))))

goal (1 subgoal):
 1. mappings\<^sub>C \<Sigma> \<phi> = (let Gs = G_list \<phi>; max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of\<^sub>C \<Sigma>)) in set (concat (map (mapping_generator_list (\<lambda>x. [0..<the (max_rank x)])) (subseqs Gs))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mappings\<^sub>C \<Sigma> \<phi> = (let Gs = G_list \<phi>; max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of\<^sub>C \<Sigma>)) in set (concat (map (mapping_generator_list (\<lambda>x. [0..<the (max_rank x)])) (subseqs Gs))))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reach_delta_initial:
  assumes "(x, y) \<in> reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)"
  assumes "\<chi> \<in> \<^bold>G \<phi>"
  shows "Mapping.lookup y \<chi> \<noteq> None" (is ?t1)
    and "distinct (the (Mapping.lookup y \<chi>))" (is ?t2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.lookup y \<chi> \<noteq> None &&& distinct (the (Mapping.lookup y \<chi>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Mapping.lookup y \<chi> \<noteq> None
 2. distinct (the (Mapping.lookup y \<chi>))
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)
[PROOF STEP]
obtain w i where y_def: "y = run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M o q\<^sub>0\<^sub>M o theG)) (Mapping.tabulate (G_list \<phi>) (init o q\<^sub>0\<^sub>M o theG)) w i"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)

goal (1 subgoal):
 1. (\<And>w i. y = run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding reach_def delta\<^sub>C.simps initial\<^sub>C.simps simple_product_run
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(run \<delta> (q\<^sub>0 \<phi>) w n, run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w n) |w n. range w \<subseteq> \<Sigma>}

goal (1 subgoal):
 1. (\<And>w i. y = run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
y = run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i

goal (2 subgoals):
 1. Mapping.lookup y \<chi> \<noteq> None
 2. distinct (the (Mapping.lookup y \<chi>))
[PROOF STEP]
from assms(2) nxt_run_distinct
[PROOF STATE]
proof (chain)
picking this:
\<chi> \<in> \<^bold>G \<phi>
distinct (run (nxt ?\<Sigma> ?\<Delta> ?q\<^sub>0) (init ?q\<^sub>0) ?w ?n)
[PROOF STEP]
show ?t1
[PROOF STATE]
proof (prove)
using this:
\<chi> \<in> \<^bold>G \<phi>
distinct (run (nxt ?\<Sigma> ?\<Delta> ?q\<^sub>0) (init ?q\<^sub>0) ?w ?n)

goal (1 subgoal):
 1. Mapping.lookup y \<chi> \<noteq> None
[PROOF STEP]
unfolding y_def
[PROOF STATE]
proof (prove)
using this:
\<chi> \<in> \<^bold>G \<phi>
distinct (run (nxt ?\<Sigma> ?\<Delta> ?q\<^sub>0) (init ?q\<^sub>0) ?w ?n)

goal (1 subgoal):
 1. Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i) \<chi> \<noteq> None
[PROOF STEP]
using product_abs_run_Some[of "Mapping.tabulate (G_list \<phi>) (init o q\<^sub>0\<^sub>M o theG)" \<chi>]
[PROOF STATE]
proof (prove)
using this:
\<chi> \<in> \<^bold>G \<phi>
distinct (run (nxt ?\<Sigma> ?\<Delta> ?q\<^sub>0) (init ?q\<^sub>0) ?w ?n)
Mapping.lookup (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) \<chi> = Some ?q\<^sub>0 \<Longrightarrow> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> ?\<delta>\<^sub>m) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) ?w ?i) \<chi> = Some (run (?\<delta>\<^sub>m \<chi>) ?q\<^sub>0 ?w ?i)

goal (1 subgoal):
 1. Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i) \<chi> \<noteq> None
[PROOF STEP]
unfolding G_eq_G_list
[PROOF STATE]
proof (prove)
using this:
\<chi> \<in> set (G_list \<phi>)
distinct (run (nxt ?\<Sigma> ?\<Delta> ?q\<^sub>0) (init ?q\<^sub>0) ?w ?n)
Mapping.lookup (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) \<chi> = Some ?q\<^sub>0 \<Longrightarrow> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> ?\<delta>\<^sub>m) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) ?w ?i) \<chi> = Some (run (?\<delta>\<^sub>m \<chi>) ?q\<^sub>0 ?w ?i)

goal (1 subgoal):
 1. Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i) \<chi> \<noteq> None
[PROOF STEP]
unfolding lookup_tabulate
[PROOF STATE]
proof (prove)
using this:
\<chi> \<in> set (G_list \<phi>)
distinct (run (nxt ?\<Sigma> ?\<Delta> ?q\<^sub>0) (init ?q\<^sub>0) ?w ?n)
(if \<chi> \<in> set (G_list \<phi>) then Some ((init \<circ> q\<^sub>0\<^sub>M \<circ> theG) \<chi>) else None) = Some ?q\<^sub>0 \<Longrightarrow> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> ?\<delta>\<^sub>m) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) ?w ?i) \<chi> = Some (run (?\<delta>\<^sub>m \<chi>) ?q\<^sub>0 ?w ?i)

goal (1 subgoal):
 1. Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i) \<chi> \<noteq> None
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Mapping.lookup y \<chi> \<noteq> None

goal (1 subgoal):
 1. distinct (the (Mapping.lookup y \<chi>))
[PROOF STEP]
with nxt_run_distinct
[PROOF STATE]
proof (chain)
picking this:
distinct (run (nxt ?\<Sigma> ?\<Delta> ?q\<^sub>0) (init ?q\<^sub>0) ?w ?n)
Mapping.lookup y \<chi> \<noteq> None
[PROOF STEP]
show ?t2
[PROOF STATE]
proof (prove)
using this:
distinct (run (nxt ?\<Sigma> ?\<Delta> ?q\<^sub>0) (init ?q\<^sub>0) ?w ?n)
Mapping.lookup y \<chi> \<noteq> None

goal (1 subgoal):
 1. distinct (the (Mapping.lookup y \<chi>))
[PROOF STEP]
unfolding y_def
[PROOF STATE]
proof (prove)
using this:
distinct (run (nxt ?\<Sigma> ?\<Delta> ?q\<^sub>0) (init ?q\<^sub>0) ?w ?n)
Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i) \<chi> \<noteq> None

goal (1 subgoal):
 1. distinct (the (Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i) \<chi>))
[PROOF STEP]
using lookup_tabulate
[PROOF STATE]
proof (prove)
using this:
distinct (run (nxt ?\<Sigma> ?\<Delta> ?q\<^sub>0) (init ?q\<^sub>0) ?w ?n)
Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i) \<chi> \<noteq> None
Mapping.lookup (Mapping.tabulate ?xs ?f) ?x = (if ?x \<in> set ?xs then Some (?f ?x) else None)

goal (1 subgoal):
 1. distinct (the (Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i) \<chi>))
[PROOF STEP]
by (metis (no_types) G_eq_G_list assms(2) comp_eq_dest_lhs option.sel product_abs_run_Some)
[PROOF STATE]
proof (state)
this:
distinct (the (Mapping.lookup y \<chi>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_reach\<^sub>C:
  "finite (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>))
[PROOF STEP]
note finite_reach'
[PROOF STATE]
proof (state)
this:
finite (reach \<Sigma> \<delta> (q\<^sub>0 ?\<phi>))

goal (1 subgoal):
 1. finite (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (reach \<Sigma> \<delta> (q\<^sub>0 ?\<phi>))

goal (1 subgoal):
 1. finite (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>))
[PROOF STEP]
have "(\<And>x. x \<in> \<^bold>G \<phi> \<Longrightarrow> finite (reach \<Sigma> ((nxt \<Sigma> \<delta>\<^sub>M o q\<^sub>0\<^sub>M o theG) x) ((init o q\<^sub>0\<^sub>M o theG) x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> \<^bold>G \<phi> \<Longrightarrow> finite (reach \<Sigma> ((nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) x) ((init \<circ> q\<^sub>0\<^sub>M \<circ> theG) x))
[PROOF STEP]
using semi_mojmir.finite_Q[OF semi_mojmir]
[PROOF STATE]
proof (prove)
using this:
finite (semi_mojmir_def.Q\<^sub>E \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M ?\<psi>1))

goal (1 subgoal):
 1. \<And>x. x \<in> \<^bold>G \<phi> \<Longrightarrow> finite (reach \<Sigma> ((nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) x) ((init \<circ> q\<^sub>0\<^sub>M \<circ> theG) x))
[PROOF STEP]
unfolding G_eq_G_list semi_mojmir_def.Q\<^sub>E_def
[PROOF STATE]
proof (prove)
using this:
finite (reach \<Sigma> (nxt \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M ?\<psi>1)) (init (q\<^sub>0\<^sub>M ?\<psi>1)))

goal (1 subgoal):
 1. \<And>x. x \<in> set (G_list \<phi>) \<Longrightarrow> finite (reach \<Sigma> ((nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) x) ((init \<circ> q\<^sub>0\<^sub>M \<circ> theG) x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?x17 \<in> \<^bold>G \<phi> \<Longrightarrow> finite (reach \<Sigma> ((nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) ?x17) ((init \<circ> q\<^sub>0\<^sub>M \<circ> theG) ?x17))

goal (1 subgoal):
 1. finite (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>))
[PROOF STEP]
hence "finite (reach \<Sigma> (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M o q\<^sub>0\<^sub>M o theG)) (Mapping.tabulate (G_list \<phi>) (init o q\<^sub>0\<^sub>M o theG)))"
[PROOF STATE]
proof (prove)
using this:
?x17 \<in> \<^bold>G \<phi> \<Longrightarrow> finite (reach \<Sigma> ((nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) ?x17) ((init \<circ> q\<^sub>0\<^sub>M \<circ> theG) ?x17))

goal (1 subgoal):
 1. finite (reach \<Sigma> (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)))
[PROOF STEP]
by (metis (no_types) finite_reach_product_abs[OF finite_keys_tabulate] G_eq_G_list  keys_tabulate lookup_tabulate_Some)
[PROOF STATE]
proof (state)
this:
finite (reach \<Sigma> (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)))

goal (1 subgoal):
 1. finite (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (reach \<Sigma> \<delta> (q\<^sub>0 ?\<phi>))
finite (reach \<Sigma> (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)))
[PROOF STEP]
have "finite (reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>))"
[PROOF STATE]
proof (prove)
using this:
finite (reach \<Sigma> \<delta> (q\<^sub>0 ?\<phi>))
finite (reach \<Sigma> (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)))

goal (1 subgoal):
 1. finite (reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>))
[PROOF STEP]
using finite_reach_simple_product
[PROOF STATE]
proof (prove)
using this:
finite (reach \<Sigma> \<delta> (q\<^sub>0 ?\<phi>))
finite (reach \<Sigma> (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)))
\<lbrakk>finite (reach ?\<Sigma> ?\<delta>\<^sub>1 ?q\<^sub>1); finite (reach ?\<Sigma> ?\<delta>\<^sub>2 ?q\<^sub>2)\<rbrakk> \<Longrightarrow> finite (reach ?\<Sigma> ?\<delta>\<^sub>1 \<times> ?\<delta>\<^sub>2 (?q\<^sub>1, ?q\<^sub>2))

goal (1 subgoal):
 1. finite (reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
finite (reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>))

goal (1 subgoal):
 1. finite (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>))

goal (1 subgoal):
 1. finite (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>))
[PROOF STEP]
using finite_\<Sigma>
[PROOF STATE]
proof (prove)
using this:
finite (reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>))
finite \<Sigma>

goal (1 subgoal):
 1. finite (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>))
[PROOF STEP]
by (simp add: finite_reach\<^sub>t)
[PROOF STATE]
proof (state)
this:
finite (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma max_rank_of\<^sub>C_eq:
  assumes "\<Sigma> = set \<Sigma>'"
  shows "max_rank_of\<^sub>C \<Sigma>' \<psi> = max_rank_of \<Sigma> \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_rank_of\<^sub>C \<Sigma>' \<psi> = max_rank_of \<Sigma> \<psi>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max_rank_of\<^sub>C \<Sigma>' \<psi> = max_rank_of \<Sigma> \<psi>
[PROOF STEP]
interpret \<MM>: semi_mojmir "set \<Sigma>'" \<delta>\<^sub>M "q\<^sub>0\<^sub>M (theG \<psi>)" w
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semi_mojmir (set \<Sigma>') \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<psi>)) w
[PROOF STEP]
using semi_mojmir assms
[PROOF STATE]
proof (prove)
using this:
semi_mojmir \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M ?\<psi>) w
\<Sigma> = set \<Sigma>'

goal (1 subgoal):
 1. semi_mojmir (set \<Sigma>') \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<psi>)) w
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max_rank_of\<^sub>C \<Sigma>' \<psi> = max_rank_of \<Sigma> \<psi>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_rank_of\<^sub>C \<Sigma>' \<psi> = max_rank_of \<Sigma> \<psi>
[PROOF STEP]
unfolding max_rank_of_def max_rank_of\<^sub>C_def Q\<^sub>L_reach[OF \<MM>.finite_reach] semi_mojmir_def.max_rank_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (Set.filter (Not \<circ> \<MM>.sink) (reach (set \<Sigma>') \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<psi>)))) = card (reach \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<psi>)) - Collect (semi_mojmir_def.sink \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<psi>))))
[PROOF STEP]
by (simp add: Set.filter_def set_diff_eq assms)
[PROOF STATE]
proof (state)
this:
max_rank_of\<^sub>C \<Sigma>' \<psi> = max_rank_of \<Sigma> \<psi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reachable_transitions\<^sub>C_eq:
  assumes "\<Sigma> = set \<Sigma>'"
  shows "reachable_transitions\<^sub>C \<Sigma>' \<phi> = reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable_transitions\<^sub>C \<Sigma>' \<phi> = reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)
[PROOF STEP]
by (simp only: reachable_transitions\<^sub>C_def \<delta>\<^sub>L_reach[OF finite_reach\<^sub>C[unfolded assms]] assms)