[STATEMENT]
lemma If_THE_False: "Suc (THE n. \<exists>a. (c2, s) \<Rightarrow> n \<Down> a) =  (THE n. \<exists>a. (IF b THEN c1 ELSE c2, s) \<Rightarrow> n \<Down> a)"
     if T: "\<not>bval b s" and c2_t: "\<down> (c2,s)" for s l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (\<down>\<^sub>t (c2, s)) = \<down>\<^sub>t (IF b THEN c1 ELSE c2, s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc (\<down>\<^sub>t (c2, s)) = \<down>\<^sub>t (IF b THEN c1 ELSE c2, s)
[PROOF STEP]
from c2_t
[PROOF STATE]
proof (chain)
picking this:
\<down> (c2, s)
[PROOF STEP]
obtain p t where a: "(c2, s) \<Rightarrow> p \<Down> t"
[PROOF STATE]
proof (prove)
using this:
\<down> (c2, s)

goal (1 subgoal):
 1. (\<And>p t. (c2, s) \<Rightarrow> p \<Down> t \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(c2, s) \<Rightarrow> p \<Down> t

goal (1 subgoal):
 1. Suc (\<down>\<^sub>t (c2, s)) = \<down>\<^sub>t (IF b THEN c1 ELSE c2, s)
[PROOF STEP]
with T
[PROOF STATE]
proof (chain)
picking this:
\<not> bval b s
(c2, s) \<Rightarrow> p \<Down> t
[PROOF STEP]
have b: "(IF b THEN c1 ELSE c2, s) \<Rightarrow> p+1 \<Down> t"
[PROOF STATE]
proof (prove)
using this:
\<not> bval b s
(c2, s) \<Rightarrow> p \<Down> t

goal (1 subgoal):
 1. (IF b THEN c1 ELSE c2, s) \<Rightarrow> p + 1 \<Down> t
[PROOF STEP]
using IfFalse
[PROOF STATE]
proof (prove)
using this:
\<not> bval b s
(c2, s) \<Rightarrow> p \<Down> t
\<lbrakk>\<not> bval ?b ?s; (?c2.0, ?s) \<Rightarrow> ?x \<Down> ?t; ?y = ?x + 1\<rbrakk> \<Longrightarrow> (IF ?b THEN ?c1.0 ELSE ?c2.0, ?s) \<Rightarrow> ?y \<Down> ?t

goal (1 subgoal):
 1. (IF b THEN c1 ELSE c2, s) \<Rightarrow> p + 1 \<Down> t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(IF b THEN c1 ELSE c2, s) \<Rightarrow> p + 1 \<Down> t

goal (1 subgoal):
 1. Suc (\<down>\<^sub>t (c2, s)) = \<down>\<^sub>t (IF b THEN c1 ELSE c2, s)
[PROOF STEP]
from a bigstepT_the_cost
[PROOF STATE]
proof (chain)
picking this:
(c2, s) \<Rightarrow> p \<Down> t
(?c, ?s) \<Rightarrow> ?t \<Down> ?s' \<Longrightarrow> \<down>\<^sub>t (?c, ?s) = ?t
[PROOF STEP]
have "(THE n. \<exists>a. (c2, s) \<Rightarrow> n \<Down> a) = p"
[PROOF STATE]
proof (prove)
using this:
(c2, s) \<Rightarrow> p \<Down> t
(?c, ?s) \<Rightarrow> ?t \<Down> ?s' \<Longrightarrow> \<down>\<^sub>t (?c, ?s) = ?t

goal (1 subgoal):
 1. \<down>\<^sub>t (c2, s) = p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<down>\<^sub>t (c2, s) = p

goal (1 subgoal):
 1. Suc (\<down>\<^sub>t (c2, s)) = \<down>\<^sub>t (IF b THEN c1 ELSE c2, s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<down>\<^sub>t (c2, s) = p

goal (1 subgoal):
 1. Suc (\<down>\<^sub>t (c2, s)) = \<down>\<^sub>t (IF b THEN c1 ELSE c2, s)
[PROOF STEP]
from b bigstepT_the_cost
[PROOF STATE]
proof (chain)
picking this:
(IF b THEN c1 ELSE c2, s) \<Rightarrow> p + 1 \<Down> t
(?c, ?s) \<Rightarrow> ?t \<Down> ?s' \<Longrightarrow> \<down>\<^sub>t (?c, ?s) = ?t
[PROOF STEP]
have "(THE n. \<exists>a. (IF b THEN c1 ELSE c2, s) \<Rightarrow> n \<Down> a) = p+1"
[PROOF STATE]
proof (prove)
using this:
(IF b THEN c1 ELSE c2, s) \<Rightarrow> p + 1 \<Down> t
(?c, ?s) \<Rightarrow> ?t \<Down> ?s' \<Longrightarrow> \<down>\<^sub>t (?c, ?s) = ?t

goal (1 subgoal):
 1. \<down>\<^sub>t (IF b THEN c1 ELSE c2, s) = p + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<down>\<^sub>t (IF b THEN c1 ELSE c2, s) = p + 1

goal (1 subgoal):
 1. Suc (\<down>\<^sub>t (c2, s)) = \<down>\<^sub>t (IF b THEN c1 ELSE c2, s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<down>\<^sub>t (c2, s) = p
\<down>\<^sub>t (IF b THEN c1 ELSE c2, s) = p + 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<down>\<^sub>t (c2, s) = p
\<down>\<^sub>t (IF b THEN c1 ELSE c2, s) = p + 1

goal (1 subgoal):
 1. Suc (\<down>\<^sub>t (c2, s)) = \<down>\<^sub>t (IF b THEN c1 ELSE c2, s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (\<down>\<^sub>t (c2, s)) = \<down>\<^sub>t (IF b THEN c1 ELSE c2, s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nths_intersection_eq:
  assumes "{0..<length xs} \<subseteq> A"
  shows "nths xs B = nths xs (A \<inter> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths xs B = nths xs (A \<inter> B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nths xs B = nths xs (A \<inter> B)
[PROOF STEP]
have "\<And>x. x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd x < length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd x < length xs
[PROOF STEP]
by (metis atLeastLessThan_iff atLeastLessThan_upt in_set_zip nth_mem)
[PROOF STATE]
proof (state)
this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd ?x < length xs

goal (1 subgoal):
 1. nths xs B = nths xs (A \<inter> B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd ?x < length xs
[PROOF STEP]
have "\<And>x. x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd x \<in> A"
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd ?x < length xs

goal (1 subgoal):
 1. \<And>x. x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd x \<in> A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd ?x < length xs
{0..<length xs} \<subseteq> A

goal (1 subgoal):
 1. \<And>x. x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd x \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd ?x \<in> A

goal (1 subgoal):
 1. nths xs B = nths xs (A \<inter> B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd ?x \<in> A
[PROOF STEP]
have eqp: "\<And>x. x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd x \<in> B = (snd x \<in> (A \<inter> B))"
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd ?x \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> (snd x \<in> B) = (snd x \<in> A \<inter> B)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> (snd ?x \<in> B) = (snd ?x \<in> A \<inter> B)

goal (1 subgoal):
 1. nths xs B = nths xs (A \<inter> B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> (snd ?x \<in> B) = (snd ?x \<in> A \<inter> B)
[PROOF STEP]
have "filter (\<lambda>p. snd p \<in> B) (zip xs [0..<length xs]) = filter (\<lambda>p. snd p \<in> (A \<inter> B)) (zip xs [0..<length xs])"
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> (snd ?x \<in> B) = (snd ?x \<in> A \<inter> B)

goal (1 subgoal):
 1. filter (\<lambda>p. snd p \<in> B) (zip xs [0..<length xs]) = filter (\<lambda>p. snd p \<in> A \<inter> B) (zip xs [0..<length xs])
[PROOF STEP]
using filter_cong[of "(zip xs [0..<length xs])" "(zip xs [0..<length xs])", OF _ eqp]
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> (snd ?x \<in> B) = (snd ?x \<in> A \<inter> B)
\<lbrakk>zip xs [0..<length xs] = zip xs [0..<length xs]; \<And>x. x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> ?x1 x \<in> set (zip xs [0..<length xs])\<rbrakk> \<Longrightarrow> filter (\<lambda>x. snd (?x1 x) \<in> B) (zip xs [0..<length xs]) = filter (\<lambda>x. snd (?x1 x) \<in> A \<inter> B) (zip xs [0..<length xs])

goal (1 subgoal):
 1. filter (\<lambda>p. snd p \<in> B) (zip xs [0..<length xs]) = filter (\<lambda>p. snd p \<in> A \<inter> B) (zip xs [0..<length xs])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
filter (\<lambda>p. snd p \<in> B) (zip xs [0..<length xs]) = filter (\<lambda>p. snd p \<in> A \<inter> B) (zip xs [0..<length xs])

goal (1 subgoal):
 1. nths xs B = nths xs (A \<inter> B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
filter (\<lambda>p. snd p \<in> B) (zip xs [0..<length xs]) = filter (\<lambda>p. snd p \<in> A \<inter> B) (zip xs [0..<length xs])
[PROOF STEP]
show "nths xs B = nths xs (A \<inter> B)"
[PROOF STATE]
proof (prove)
using this:
filter (\<lambda>p. snd p \<in> B) (zip xs [0..<length xs]) = filter (\<lambda>p. snd p \<in> A \<inter> B) (zip xs [0..<length xs])

goal (1 subgoal):
 1. nths xs B = nths xs (A \<inter> B)
[PROOF STEP]
unfolding nths_def
[PROOF STATE]
proof (prove)
using this:
filter (\<lambda>p. snd p \<in> B) (zip xs [0..<length xs]) = filter (\<lambda>p. snd p \<in> A \<inter> B) (zip xs [0..<length xs])

goal (1 subgoal):
 1. map fst (filter (\<lambda>p. snd p \<in> B) (zip xs [0..<length xs])) = map fst (filter (\<lambda>p. snd p \<in> A \<inter> B) (zip xs [0..<length xs]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths xs B = nths xs (A \<inter> B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nths_minus_eq:
  assumes "{0..<length xs} \<subseteq> A"
  shows "nths xs (-B) = nths xs (A - B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths xs (- B) = nths xs (A - B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nths xs (- B) = nths xs (A - B)
[PROOF STEP]
have "\<And>x. x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd x < length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd x < length xs
[PROOF STEP]
by (metis atLeastLessThan_iff atLeastLessThan_upt in_set_zip nth_mem)
[PROOF STATE]
proof (state)
this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd ?x < length xs

goal (1 subgoal):
 1. nths xs (- B) = nths xs (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd ?x < length xs
[PROOF STEP]
have "\<And>x. x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd x \<in> A"
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd ?x < length xs

goal (1 subgoal):
 1. \<And>x. x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd x \<in> A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd ?x < length xs
{0..<length xs} \<subseteq> A

goal (1 subgoal):
 1. \<And>x. x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd x \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd ?x \<in> A

goal (1 subgoal):
 1. nths xs (- B) = nths xs (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd ?x \<in> A
[PROOF STEP]
have eqp: "\<And>x. x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd x \<in> (-B) = (snd x \<in> (A - B))"
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> snd ?x \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> (snd x \<in> - B) = (snd x \<in> A - B)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> (snd ?x \<in> - B) = (snd ?x \<in> A - B)

goal (1 subgoal):
 1. nths xs (- B) = nths xs (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> (snd ?x \<in> - B) = (snd ?x \<in> A - B)
[PROOF STEP]
have "filter (\<lambda>p. snd p \<in> (-B)) (zip xs [0..<length xs]) = filter (\<lambda>p. snd p \<in> (A-B)) (zip xs [0..<length xs])"
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> (snd ?x \<in> - B) = (snd ?x \<in> A - B)

goal (1 subgoal):
 1. filter (\<lambda>p. snd p \<in> - B) (zip xs [0..<length xs]) = filter (\<lambda>p. snd p \<in> A - B) (zip xs [0..<length xs])
[PROOF STEP]
using filter_cong[of "(zip xs [0..<length xs])" "(zip xs [0..<length xs])", OF _ eqp]
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> (snd ?x \<in> - B) = (snd ?x \<in> A - B)
\<lbrakk>zip xs [0..<length xs] = zip xs [0..<length xs]; \<And>x. x \<in> set (zip xs [0..<length xs]) \<Longrightarrow> ?x1 x \<in> set (zip xs [0..<length xs])\<rbrakk> \<Longrightarrow> filter (\<lambda>x. snd (?x1 x) \<in> - B) (zip xs [0..<length xs]) = filter (\<lambda>x. snd (?x1 x) \<in> A - B) (zip xs [0..<length xs])

goal (1 subgoal):
 1. filter (\<lambda>p. snd p \<in> - B) (zip xs [0..<length xs]) = filter (\<lambda>p. snd p \<in> A - B) (zip xs [0..<length xs])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
filter (\<lambda>p. snd p \<in> - B) (zip xs [0..<length xs]) = filter (\<lambda>p. snd p \<in> A - B) (zip xs [0..<length xs])

goal (1 subgoal):
 1. nths xs (- B) = nths xs (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
filter (\<lambda>p. snd p \<in> - B) (zip xs [0..<length xs]) = filter (\<lambda>p. snd p \<in> A - B) (zip xs [0..<length xs])
[PROOF STEP]
show "nths xs (-B) = nths xs (A - B)"
[PROOF STATE]
proof (prove)
using this:
filter (\<lambda>p. snd p \<in> - B) (zip xs [0..<length xs]) = filter (\<lambda>p. snd p \<in> A - B) (zip xs [0..<length xs])

goal (1 subgoal):
 1. nths xs (- B) = nths xs (A - B)
[PROOF STEP]
unfolding nths_def
[PROOF STATE]
proof (prove)
using this:
filter (\<lambda>p. snd p \<in> - B) (zip xs [0..<length xs]) = filter (\<lambda>p. snd p \<in> A - B) (zip xs [0..<length xs])

goal (1 subgoal):
 1. map fst (filter (\<lambda>p. snd p \<in> - B) (zip xs [0..<length xs])) = map fst (filter (\<lambda>p. snd p \<in> A - B) (zip xs [0..<length xs]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths xs (- B) = nths xs (A - B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nths_split_complement_eq:
  assumes "A \<inter> B = {}"
  and "{0..<length xs} \<subseteq> A \<union> B"
shows "nths xs A = nths xs (-B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths xs A = nths xs (- B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nths xs A = nths xs (- B)
[PROOF STEP]
have "nths xs (-B) = nths xs (A \<union> B - B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths xs (- B) = nths xs (A \<union> B - B)
[PROOF STEP]
using nths_minus_eq assms
[PROOF STATE]
proof (prove)
using this:
{0..<length ?xs} \<subseteq> ?A \<Longrightarrow> nths ?xs (- ?B) = nths ?xs (?A - ?B)
A \<inter> B = {}
{0..<length xs} \<subseteq> A \<union> B

goal (1 subgoal):
 1. nths xs (- B) = nths xs (A \<union> B - B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths xs (- B) = nths xs (A \<union> B - B)

goal (1 subgoal):
 1. nths xs A = nths xs (- B)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nths xs (- B) = nths xs (A \<union> B - B)

goal (1 subgoal):
 1. nths xs A = nths xs (- B)
[PROOF STEP]
have "A \<union> B - B = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<union> B - B = A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<inter> B = {}
{0..<length xs} \<subseteq> A \<union> B

goal (1 subgoal):
 1. A \<union> B - B = A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<union> B - B = A

goal (1 subgoal):
 1. nths xs A = nths xs (- B)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
nths xs (- B) = nths xs (A \<union> B - B)
A \<union> B - B = A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nths xs (- B) = nths xs (A \<union> B - B)
A \<union> B - B = A

goal (1 subgoal):
 1. nths xs A = nths xs (- B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths xs A = nths xs (- B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lt_set_card_lt:
  fixes A :: "nat set"
  assumes "finite A" and "x \<in> A"
  shows "card {y. y \<in> A \<and> y < x} < card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {y \<in> A. y < x} < card A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {y \<in> A. y < x} < card A
[PROOF STEP]
have "x \<notin> {y. y \<in> A \<and> y < x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> {y \<in> A. y < x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<notin> {y \<in> A. y < x}

goal (1 subgoal):
 1. card {y \<in> A. y < x} < card A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<notin> {y \<in> A. y < x}
[PROOF STEP]
have "{y. y \<in> A \<and> y < x} \<subseteq> A - {x}"
[PROOF STATE]
proof (prove)
using this:
x \<notin> {y \<in> A. y < x}

goal (1 subgoal):
 1. {y \<in> A. y < x} \<subseteq> A - {x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{y \<in> A. y < x} \<subseteq> A - {x}

goal (1 subgoal):
 1. card {y \<in> A. y < x} < card A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{y \<in> A. y < x} \<subseteq> A - {x}
[PROOF STEP]
have "card {y. y \<in> A \<and> y < x} \<le> card (A - {x})"
[PROOF STATE]
proof (prove)
using this:
{y \<in> A. y < x} \<subseteq> A - {x}

goal (1 subgoal):
 1. card {y \<in> A. y < x} \<le> card (A - {x})
[PROOF STEP]
using card_mono finite_Diff[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
{y \<in> A. y < x} \<subseteq> A - {x}
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> card ?A \<le> card ?B
finite (A - ?B)

goal (1 subgoal):
 1. card {y \<in> A. y < x} \<le> card (A - {x})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {y \<in> A. y < x} \<le> card (A - {x})

goal (1 subgoal):
 1. card {y \<in> A. y < x} < card A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card {y \<in> A. y < x} \<le> card (A - {x})

goal (1 subgoal):
 1. card {y \<in> A. y < x} < card A
[PROOF STEP]
have "\<dots> < card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (A - {x}) < card A
[PROOF STEP]
using card_Diff1_less[OF assms]
[PROOF STATE]
proof (prove)
using this:
card (A - {x}) < card A

goal (1 subgoal):
 1. card (A - {x}) < card A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (A - {x}) < card A

goal (1 subgoal):
 1. card {y \<in> A. y < x} < card A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card {y \<in> A. y < x} < card A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card {y \<in> A. y < x} < card A

goal (1 subgoal):
 1. card {y \<in> A. y < x} < card A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {y \<in> A. y < x} < card A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_ind_in_set_bound:
  fixes M :: "nat" and v0 :: "nat set"
  assumes "\<And>x. f x = card {y. y \<in> v0 \<and> y < x}"
  shows "bij_betw f ({0..<M} \<inter> v0) {0..<card ({0..<M} \<inter> v0)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw f ({0..<M} \<inter> v0) {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
unfolding bij_betw_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f ({0..<M} \<inter> v0) \<and> f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on f ({0..<M} \<inter> v0)
 2. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
let ?dom = "{0..<M} \<inter> v0"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on f ({0..<M} \<inter> v0)
 2. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
let ?ran = "{0..<card ({0..<M} \<inter> v0)}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on f ({0..<M} \<inter> v0)
 2. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on f ({0..<M} \<inter> v0)
 2. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
fix x1 x2 :: nat
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on f ({0..<M} \<inter> v0)
 2. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
assume x1: "x1 \<in> ?dom" and x2: "x2 \<in> ?dom" and "f x1 = f x2"
[PROOF STATE]
proof (state)
this:
x1 \<in> {0..<M} \<inter> v0
x2 \<in> {0..<M} \<inter> v0
f x1 = f x2

goal (2 subgoals):
 1. inj_on f ({0..<M} \<inter> v0)
 2. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x1 \<in> {0..<M} \<inter> v0
x2 \<in> {0..<M} \<inter> v0
f x1 = f x2
[PROOF STEP]
have "card {y. y \<in> v0 \<and> y < x1} = card {y. y \<in> v0 \<and> y < x2}"
[PROOF STATE]
proof (prove)
using this:
x1 \<in> {0..<M} \<inter> v0
x2 \<in> {0..<M} \<inter> v0
f x1 = f x2

goal (1 subgoal):
 1. card {y \<in> v0. y < x1} = card {y \<in> v0. y < x2}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x1 \<in> {0..<M} \<inter> v0
x2 \<in> {0..<M} \<inter> v0
f x1 = f x2
f ?x = card {y \<in> v0. y < ?x}

goal (1 subgoal):
 1. card {y \<in> v0. y < x1} = card {y \<in> v0. y < x2}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {y \<in> v0. y < x1} = card {y \<in> v0. y < x2}

goal (2 subgoals):
 1. inj_on f ({0..<M} \<inter> v0)
 2. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card {y \<in> v0. y < x1} = card {y \<in> v0. y < x2}
[PROOF STEP]
have "pick v0 (card {y. y \<in> v0 \<and> y < x1}) = pick v0 (card {y. y \<in> v0 \<and> y < x2})"
[PROOF STATE]
proof (prove)
using this:
card {y \<in> v0. y < x1} = card {y \<in> v0. y < x2}

goal (1 subgoal):
 1. pick v0 (card {y \<in> v0. y < x1}) = pick v0 (card {y \<in> v0. y < x2})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pick v0 (card {y \<in> v0. y < x1}) = pick v0 (card {y \<in> v0. y < x2})

goal (2 subgoals):
 1. inj_on f ({0..<M} \<inter> v0)
 2. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pick v0 (card {y \<in> v0. y < x1}) = pick v0 (card {y \<in> v0. y < x2})

goal (2 subgoals):
 1. inj_on f ({0..<M} \<inter> v0)
 2. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
have "pick v0 (card {y. y \<in> v0 \<and> y < x1}) = x1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pick v0 (card {y \<in> v0. y < x1}) = x1
[PROOF STEP]
using pick_card_in_set x1
[PROOF STATE]
proof (prove)
using this:
?i \<in> ?I \<Longrightarrow> pick ?I (card {a \<in> ?I. a < ?i}) = ?i
x1 \<in> {0..<M} \<inter> v0

goal (1 subgoal):
 1. pick v0 (card {y \<in> v0. y < x1}) = x1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pick v0 (card {y \<in> v0. y < x1}) = x1

goal (2 subgoals):
 1. inj_on f ({0..<M} \<inter> v0)
 2. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pick v0 (card {y \<in> v0. y < x1}) = x1

goal (2 subgoals):
 1. inj_on f ({0..<M} \<inter> v0)
 2. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
have "pick v0 (card {y. y \<in> v0 \<and> y < x2}) = x2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pick v0 (card {y \<in> v0. y < x2}) = x2
[PROOF STEP]
using pick_card_in_set x2
[PROOF STATE]
proof (prove)
using this:
?i \<in> ?I \<Longrightarrow> pick ?I (card {a \<in> ?I. a < ?i}) = ?i
x2 \<in> {0..<M} \<inter> v0

goal (1 subgoal):
 1. pick v0 (card {y \<in> v0. y < x2}) = x2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pick v0 (card {y \<in> v0. y < x2}) = x2

goal (2 subgoals):
 1. inj_on f ({0..<M} \<inter> v0)
 2. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pick v0 (card {y \<in> v0. y < x1}) = pick v0 (card {y \<in> v0. y < x2})
pick v0 (card {y \<in> v0. y < x1}) = x1
pick v0 (card {y \<in> v0. y < x2}) = x2
[PROOF STEP]
have "x1 = x2"
[PROOF STATE]
proof (prove)
using this:
pick v0 (card {y \<in> v0. y < x1}) = pick v0 (card {y \<in> v0. y < x2})
pick v0 (card {y \<in> v0. y < x1}) = x1
pick v0 (card {y \<in> v0. y < x2}) = x2

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

goal (2 subgoals):
 1. inj_on f ({0..<M} \<inter> v0)
 2. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x1.2 \<in> {0..<M} \<inter> v0; ?x2.2 \<in> {0..<M} \<inter> v0; f ?x1.2 = f ?x2.2\<rbrakk> \<Longrightarrow> ?x1.2 = ?x2.2

goal (2 subgoals):
 1. inj_on f ({0..<M} \<inter> v0)
 2. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x1.2 \<in> {0..<M} \<inter> v0; ?x2.2 \<in> {0..<M} \<inter> v0; f ?x1.2 = f ?x2.2\<rbrakk> \<Longrightarrow> ?x1.2 = ?x2.2
[PROOF STEP]
show "inj_on f ?dom"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x1.2 \<in> {0..<M} \<inter> v0; ?x2.2 \<in> {0..<M} \<inter> v0; f ?x1.2 = f ?x2.2\<rbrakk> \<Longrightarrow> ?x1.2 = ?x2.2

goal (1 subgoal):
 1. inj_on f ({0..<M} \<inter> v0)
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x1.2 \<in> {0..<M} \<inter> v0; ?x2.2 \<in> {0..<M} \<inter> v0; f ?x1.2 = f ?x2.2\<rbrakk> \<Longrightarrow> ?x1.2 = ?x2.2

goal (1 subgoal):
 1. \<forall>x\<in>{0..<M} \<inter> v0. \<forall>y\<in>{0..<M} \<inter> v0. f x = f y \<longrightarrow> x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inj_on f ({0..<M} \<inter> v0)

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
inj_on f ({0..<M} \<inter> v0)

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
assume x: "x \<in> ?dom"
[PROOF STATE]
proof (state)
this:
x \<in> {0..<M} \<inter> v0

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> {0..<M} \<inter> v0
[PROOF STEP]
have "(y \<in> v0 \<and> y < x) = (y \<in> ?dom \<and> y < x)" for y
[PROOF STATE]
proof (prove)
using this:
x \<in> {0..<M} \<inter> v0

goal (1 subgoal):
 1. (y \<in> v0 \<and> y < x) = (y \<in> {0..<M} \<inter> v0 \<and> y < x)
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x \<in> {0..<M} \<inter> v0
x \<in> {0..<M} \<inter> v0

goal (1 subgoal):
 1. (y \<in> v0 \<and> y < x) = (y \<in> {0..<M} \<inter> v0 \<and> y < x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(?y \<in> v0 \<and> ?y < x) = (?y \<in> {0..<M} \<inter> v0 \<and> ?y < x)

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?y \<in> v0 \<and> ?y < x) = (?y \<in> {0..<M} \<inter> v0 \<and> ?y < x)
[PROOF STEP]
have "card {y. y \<in> v0 \<and> y < x} = card {y. y \<in> ?dom \<and> y < x}"
[PROOF STATE]
proof (prove)
using this:
(?y \<in> v0 \<and> ?y < x) = (?y \<in> {0..<M} \<inter> v0 \<and> ?y < x)

goal (1 subgoal):
 1. card {y \<in> v0. y < x} = card {y \<in> {0..<M} \<inter> v0. y < x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {y \<in> v0. y < x} = card {y \<in> {0..<M} \<inter> v0. y < x}

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card {y \<in> v0. y < x} = card {y \<in> {0..<M} \<inter> v0. y < x}

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
have "card {y. y \<in> ?dom \<and> y < x} < card ?dom"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {y \<in> {0..<M} \<inter> v0. y < x} < card ({0..<M} \<inter> v0)
[PROOF STEP]
using x lt_set_card_lt[of ?dom]
[PROOF STATE]
proof (prove)
using this:
x \<in> {0..<M} \<inter> v0
\<lbrakk>finite ({0..<M} \<inter> v0); ?x \<in> {0..<M} \<inter> v0\<rbrakk> \<Longrightarrow> card {y \<in> {0..<M} \<inter> v0. y < ?x} < card ({0..<M} \<inter> v0)

goal (1 subgoal):
 1. card {y \<in> {0..<M} \<inter> v0. y < x} < card ({0..<M} \<inter> v0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {y \<in> {0..<M} \<inter> v0. y < x} < card ({0..<M} \<inter> v0)

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card {y \<in> v0. y < x} = card {y \<in> {0..<M} \<inter> v0. y < x}
card {y \<in> {0..<M} \<inter> v0. y < x} < card ({0..<M} \<inter> v0)
[PROOF STEP]
have "f x \<in> ?ran"
[PROOF STATE]
proof (prove)
using this:
card {y \<in> v0. y < x} = card {y \<in> {0..<M} \<inter> v0. y < x}
card {y \<in> {0..<M} \<inter> v0. y < x} < card ({0..<M} \<inter> v0)

goal (1 subgoal):
 1. f x \<in> {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
card {y \<in> v0. y < x} = card {y \<in> {0..<M} \<inter> v0. y < x}
card {y \<in> {0..<M} \<inter> v0. y < x} < card ({0..<M} \<inter> v0)
f ?x = card {y \<in> v0. y < ?x}

goal (1 subgoal):
 1. f x \<in> {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f x \<in> {0..<card ({0..<M} \<inter> v0)}

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> {0..<M} \<inter> v0 \<Longrightarrow> f ?x2 \<in> {0..<card ({0..<M} \<inter> v0)}

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x2 \<in> {0..<M} \<inter> v0 \<Longrightarrow> f ?x2 \<in> {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
have sub: "(f ` ?dom) \<subseteq> ?ran"
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> {0..<M} \<inter> v0 \<Longrightarrow> f ?x2 \<in> {0..<card ({0..<M} \<inter> v0)}

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) \<subseteq> {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ` ({0..<M} \<inter> v0) \<subseteq> {0..<card ({0..<M} \<inter> v0)}

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
f ` ({0..<M} \<inter> v0) \<subseteq> {0..<card ({0..<M} \<inter> v0)}

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
assume y: "y \<in> ?ran"
[PROOF STATE]
proof (state)
this:
y \<in> {0..<card ({0..<M} \<inter> v0)}

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
have yle: "y < card ?dom"
[PROOF STATE]
proof (prove)
using this:
y \<in> {0..<card ({0..<M} \<inter> v0)}

goal (1 subgoal):
 1. y < card ({0..<M} \<inter> v0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y < card ({0..<M} \<inter> v0)

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y < card ({0..<M} \<inter> v0)
[PROOF STEP]
have pyindom: "pick ?dom y \<in> ?dom"
[PROOF STATE]
proof (prove)
using this:
y < card ({0..<M} \<inter> v0)

goal (1 subgoal):
 1. pick ({0..<M} \<inter> v0) y \<in> {0..<M} \<inter> v0
[PROOF STEP]
using pick_in_set_le[of y ?dom]
[PROOF STATE]
proof (prove)
using this:
y < card ({0..<M} \<inter> v0)
y < card ({0..<M} \<inter> v0) \<Longrightarrow> pick ({0..<M} \<inter> v0) y \<in> {0..<M} \<inter> v0

goal (1 subgoal):
 1. pick ({0..<M} \<inter> v0) y \<in> {0..<M} \<inter> v0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pick ({0..<M} \<inter> v0) y \<in> {0..<M} \<inter> v0

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pick ({0..<M} \<inter> v0) y \<in> {0..<M} \<inter> v0
[PROOF STEP]
have "pick ?dom y < M"
[PROOF STATE]
proof (prove)
using this:
pick ({0..<M} \<inter> v0) y \<in> {0..<M} \<inter> v0

goal (1 subgoal):
 1. pick ({0..<M} \<inter> v0) y < M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pick ({0..<M} \<inter> v0) y < M

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pick ({0..<M} \<inter> v0) y < M
[PROOF STEP]
have "\<And>z. (z < pick ?dom y \<Longrightarrow> z \<in> v0 = (z \<in> ?dom))"
[PROOF STATE]
proof (prove)
using this:
pick ({0..<M} \<inter> v0) y < M

goal (1 subgoal):
 1. \<And>z. z < pick ({0..<M} \<inter> v0) y \<Longrightarrow> (z \<in> v0) = (z \<in> {0..<M} \<inter> v0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?z < pick ({0..<M} \<inter> v0) y \<Longrightarrow> (?z \<in> v0) = (?z \<in> {0..<M} \<inter> v0)

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?z < pick ({0..<M} \<inter> v0) y \<Longrightarrow> (?z \<in> v0) = (?z \<in> {0..<M} \<inter> v0)
[PROOF STEP]
have "{z. z \<in> v0 \<and> z < pick ?dom y} = {z. z \<in> ?dom \<and> z < pick ?dom y}"
[PROOF STATE]
proof (prove)
using this:
?z < pick ({0..<M} \<inter> v0) y \<Longrightarrow> (?z \<in> v0) = (?z \<in> {0..<M} \<inter> v0)

goal (1 subgoal):
 1. {z \<in> v0. z < pick ({0..<M} \<inter> v0) y} = {z \<in> {0..<M} \<inter> v0. z < pick ({0..<M} \<inter> v0) y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{z \<in> v0. z < pick ({0..<M} \<inter> v0) y} = {z \<in> {0..<M} \<inter> v0. z < pick ({0..<M} \<inter> v0) y}

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{z \<in> v0. z < pick ({0..<M} \<inter> v0) y} = {z \<in> {0..<M} \<inter> v0. z < pick ({0..<M} \<inter> v0) y}
[PROOF STEP]
have "card {z. z \<in> v0 \<and> z < pick ?dom y} = card {z. z \<in> ?dom \<and> z < pick ?dom y}"
[PROOF STATE]
proof (prove)
using this:
{z \<in> v0. z < pick ({0..<M} \<inter> v0) y} = {z \<in> {0..<M} \<inter> v0. z < pick ({0..<M} \<inter> v0) y}

goal (1 subgoal):
 1. card {z \<in> v0. z < pick ({0..<M} \<inter> v0) y} = card {z \<in> {0..<M} \<inter> v0. z < pick ({0..<M} \<inter> v0) y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {z \<in> v0. z < pick ({0..<M} \<inter> v0) y} = card {z \<in> {0..<M} \<inter> v0. z < pick ({0..<M} \<inter> v0) y}

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card {z \<in> v0. z < pick ({0..<M} \<inter> v0) y} = card {z \<in> {0..<M} \<inter> v0. z < pick ({0..<M} \<inter> v0) y}
[PROOF STEP]
have "f (pick ?dom y) = y"
[PROOF STATE]
proof (prove)
using this:
card {z \<in> v0. z < pick ({0..<M} \<inter> v0) y} = card {z \<in> {0..<M} \<inter> v0. z < pick ({0..<M} \<inter> v0) y}

goal (1 subgoal):
 1. f (pick ({0..<M} \<inter> v0) y) = y
[PROOF STEP]
using card_pick_le[OF yle] assms
[PROOF STATE]
proof (prove)
using this:
card {z \<in> v0. z < pick ({0..<M} \<inter> v0) y} = card {z \<in> {0..<M} \<inter> v0. z < pick ({0..<M} \<inter> v0) y}
card {a \<in> {0..<M} \<inter> v0. a < pick ({0..<M} \<inter> v0) y} = y
f ?x = card {y \<in> v0. y < ?x}

goal (1 subgoal):
 1. f (pick ({0..<M} \<inter> v0) y) = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (pick ({0..<M} \<inter> v0) y) = y

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
with pyindom
[PROOF STATE]
proof (chain)
picking this:
pick ({0..<M} \<inter> v0) y \<in> {0..<M} \<inter> v0
f (pick ({0..<M} \<inter> v0) y) = y
[PROOF STEP]
have "\<exists>x\<in>?dom. f x = y"
[PROOF STATE]
proof (prove)
using this:
pick ({0..<M} \<inter> v0) y \<in> {0..<M} \<inter> v0
f (pick ({0..<M} \<inter> v0) y) = y

goal (1 subgoal):
 1. \<exists>x\<in>{0..<M} \<inter> v0. f x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>{0..<M} \<inter> v0. f x = y

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?y2 \<in> {0..<card ({0..<M} \<inter> v0)} \<Longrightarrow> \<exists>x\<in>{0..<M} \<inter> v0. f x = ?y2

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?y2 \<in> {0..<card ({0..<M} \<inter> v0)} \<Longrightarrow> \<exists>x\<in>{0..<M} \<inter> v0. f x = ?y2
[PROOF STEP]
have sup: "?ran \<subseteq> (f ` ?dom)"
[PROOF STATE]
proof (prove)
using this:
?y2 \<in> {0..<card ({0..<M} \<inter> v0)} \<Longrightarrow> \<exists>x\<in>{0..<M} \<inter> v0. f x = ?y2

goal (1 subgoal):
 1. {0..<card ({0..<M} \<inter> v0)} \<subseteq> f ` ({0..<M} \<inter> v0)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
{0..<card ({0..<M} \<inter> v0)} \<subseteq> f ` ({0..<M} \<inter> v0)

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
show "(f ` ?dom) = ?ran"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
using sub sup
[PROOF STATE]
proof (prove)
using this:
f ` ({0..<M} \<inter> v0) \<subseteq> {0..<card ({0..<M} \<inter> v0)}
{0..<card ({0..<M} \<inter> v0)} \<subseteq> f ` ({0..<M} \<inter> v0)

goal (1 subgoal):
 1. f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ` ({0..<M} \<inter> v0) = {0..<card ({0..<M} \<inter> v0)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ind_in_set_bound:
  fixes A :: "nat set" and M N :: "nat"
  assumes "N \<ge> M"
  shows "ind_in_set A N \<notin> (ind_in_set A ` ({0..<M} \<inter> A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set A N \<notin> ind_in_set A ` ({0..<M} \<inter> A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ind_in_set A N \<notin> ind_in_set A ` ({0..<M} \<inter> A)
[PROOF STEP]
have "{0..<M}\<inter>A \<subseteq> {i. i \<in> A \<and> i < N}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<M} \<inter> A \<subseteq> {i \<in> A. i < N}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
M \<le> N

goal (1 subgoal):
 1. {0..<M} \<inter> A \<subseteq> {i \<in> A. i < N}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{0..<M} \<inter> A \<subseteq> {i \<in> A. i < N}

goal (1 subgoal):
 1. ind_in_set A N \<notin> ind_in_set A ` ({0..<M} \<inter> A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{0..<M} \<inter> A \<subseteq> {i \<in> A. i < N}
[PROOF STEP]
have "card ({0..<M}\<inter>A) \<le> card {i. i \<in> A \<and> i < N}"
[PROOF STATE]
proof (prove)
using this:
{0..<M} \<inter> A \<subseteq> {i \<in> A. i < N}

goal (1 subgoal):
 1. card ({0..<M} \<inter> A) \<le> card {i \<in> A. i < N}
[PROOF STEP]
using card_mono[of "{i. i \<in> A \<and> i < N}"]
[PROOF STATE]
proof (prove)
using this:
{0..<M} \<inter> A \<subseteq> {i \<in> A. i < N}
\<lbrakk>finite {i \<in> A. i < N}; ?A \<subseteq> {i \<in> A. i < N}\<rbrakk> \<Longrightarrow> card ?A \<le> card {i \<in> A. i < N}

goal (1 subgoal):
 1. card ({0..<M} \<inter> A) \<le> card {i \<in> A. i < N}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card ({0..<M} \<inter> A) \<le> card {i \<in> A. i < N}

goal (1 subgoal):
 1. ind_in_set A N \<notin> ind_in_set A ` ({0..<M} \<inter> A)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card ({0..<M} \<inter> A) \<le> card {i \<in> A. i < N}

goal (1 subgoal):
 1. ind_in_set A N \<notin> ind_in_set A ` ({0..<M} \<inter> A)
[PROOF STEP]
have "ind_in_set A N = card {i. i \<in> A \<and> i < N}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set A N = card {i \<in> A. i < N}
[PROOF STEP]
unfolding ind_in_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i \<in> A. i < N} = card {i \<in> A. i < N}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ind_in_set A N = card {i \<in> A. i < N}

goal (1 subgoal):
 1. ind_in_set A N \<notin> ind_in_set A ` ({0..<M} \<inter> A)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card ({0..<M} \<inter> A) \<le> card {i \<in> A. i < N}
ind_in_set A N = card {i \<in> A. i < N}
[PROOF STEP]
have "ind_in_set A N \<ge> card ({0..<M}\<inter>A)"
[PROOF STATE]
proof (prove)
using this:
card ({0..<M} \<inter> A) \<le> card {i \<in> A. i < N}
ind_in_set A N = card {i \<in> A. i < N}

goal (1 subgoal):
 1. card ({0..<M} \<inter> A) \<le> ind_in_set A N
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card ({0..<M} \<inter> A) \<le> ind_in_set A N

goal (1 subgoal):
 1. ind_in_set A N \<notin> ind_in_set A ` ({0..<M} \<inter> A)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card ({0..<M} \<inter> A) \<le> ind_in_set A N

goal (1 subgoal):
 1. ind_in_set A N \<notin> ind_in_set A ` ({0..<M} \<inter> A)
[PROOF STEP]
have "y \<in> ind_in_set A ` (A \<inter> {0..<M}) \<Longrightarrow> y < card ({0..<M}\<inter>A)" for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> ind_in_set A ` (A \<inter> {0..<M}) \<Longrightarrow> y < card ({0..<M} \<inter> A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<in> ind_in_set A ` (A \<inter> {0..<M}) \<Longrightarrow> y < card ({0..<M} \<inter> A)
[PROOF STEP]
let ?dom = "{0..<M} \<inter> A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<in> ind_in_set A ` (A \<inter> {0..<M}) \<Longrightarrow> y < card ({0..<M} \<inter> A)
[PROOF STEP]
assume "y \<in> ind_in_set A ` (A \<inter> {0..<M})"
[PROOF STATE]
proof (state)
this:
y \<in> ind_in_set A ` (A \<inter> {0..<M})

goal (1 subgoal):
 1. y \<in> ind_in_set A ` (A \<inter> {0..<M}) \<Longrightarrow> y < card ({0..<M} \<inter> A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> ind_in_set A ` (A \<inter> {0..<M})
[PROOF STEP]
obtain x where x: "x \<in> ?dom" and y: "ind_in_set A x = y"
[PROOF STATE]
proof (prove)
using this:
y \<in> ind_in_set A ` (A \<inter> {0..<M})

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> {0..<M} \<inter> A; ind_in_set A x = y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> {0..<M} \<inter> A
ind_in_set A x = y

goal (1 subgoal):
 1. y \<in> ind_in_set A ` (A \<inter> {0..<M}) \<Longrightarrow> y < card ({0..<M} \<inter> A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> {0..<M} \<inter> A
ind_in_set A x = y
[PROOF STEP]
have "(y \<in> A \<and> y < x) = (y \<in> ?dom \<and> y < x)" for y
[PROOF STATE]
proof (prove)
using this:
x \<in> {0..<M} \<inter> A
ind_in_set A x = y__

goal (1 subgoal):
 1. (y \<in> A \<and> y < x) = (y \<in> {0..<M} \<inter> A \<and> y < x)
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x \<in> {0..<M} \<inter> A
ind_in_set A x = y__
x \<in> {0..<M} \<inter> A

goal (1 subgoal):
 1. (y \<in> A \<and> y < x) = (y \<in> {0..<M} \<inter> A \<and> y < x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(?y \<in> A \<and> ?y < x) = (?y \<in> {0..<M} \<inter> A \<and> ?y < x)

goal (1 subgoal):
 1. y \<in> ind_in_set A ` (A \<inter> {0..<M}) \<Longrightarrow> y < card ({0..<M} \<inter> A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?y \<in> A \<and> ?y < x) = (?y \<in> {0..<M} \<inter> A \<and> ?y < x)
[PROOF STEP]
have "card {y. y \<in> A \<and> y < x} = card {y. y \<in> ?dom \<and> y < x}"
[PROOF STATE]
proof (prove)
using this:
(?y \<in> A \<and> ?y < x) = (?y \<in> {0..<M} \<inter> A \<and> ?y < x)

goal (1 subgoal):
 1. card {y \<in> A. y < x} = card {y \<in> {0..<M} \<inter> A. y < x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {y \<in> A. y < x} = card {y \<in> {0..<M} \<inter> A. y < x}

goal (1 subgoal):
 1. y \<in> ind_in_set A ` (A \<inter> {0..<M}) \<Longrightarrow> y < card ({0..<M} \<inter> A)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card {y \<in> A. y < x} = card {y \<in> {0..<M} \<inter> A. y < x}

goal (1 subgoal):
 1. y \<in> ind_in_set A ` (A \<inter> {0..<M}) \<Longrightarrow> y < card ({0..<M} \<inter> A)
[PROOF STEP]
have "card {y. y \<in> ?dom \<and> y < x} < card ?dom"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {y \<in> {0..<M} \<inter> A. y < x} < card ({0..<M} \<inter> A)
[PROOF STEP]
using x lt_set_card_lt[of ?dom]
[PROOF STATE]
proof (prove)
using this:
x \<in> {0..<M} \<inter> A
\<lbrakk>finite ({0..<M} \<inter> A); ?x \<in> {0..<M} \<inter> A\<rbrakk> \<Longrightarrow> card {y \<in> {0..<M} \<inter> A. y < ?x} < card ({0..<M} \<inter> A)

goal (1 subgoal):
 1. card {y \<in> {0..<M} \<inter> A. y < x} < card ({0..<M} \<inter> A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {y \<in> {0..<M} \<inter> A. y < x} < card ({0..<M} \<inter> A)

goal (1 subgoal):
 1. y \<in> ind_in_set A ` (A \<inter> {0..<M}) \<Longrightarrow> y < card ({0..<M} \<inter> A)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card {y \<in> A. y < x} = card {y \<in> {0..<M} \<inter> A. y < x}
card {y \<in> {0..<M} \<inter> A. y < x} < card ({0..<M} \<inter> A)
[PROOF STEP]
show "y < card ({0..<M}\<inter>A)"
[PROOF STATE]
proof (prove)
using this:
card {y \<in> A. y < x} = card {y \<in> {0..<M} \<inter> A. y < x}
card {y \<in> {0..<M} \<inter> A. y < x} < card ({0..<M} \<inter> A)

goal (1 subgoal):
 1. y < card ({0..<M} \<inter> A)
[PROOF STEP]
using y
[PROOF STATE]
proof (prove)
using this:
card {y \<in> A. y < x} = card {y \<in> {0..<M} \<inter> A. y < x}
card {y \<in> {0..<M} \<inter> A. y < x} < card ({0..<M} \<inter> A)
ind_in_set A x = y

goal (1 subgoal):
 1. y < card ({0..<M} \<inter> A)
[PROOF STEP]
unfolding ind_in_set_def
[PROOF STATE]
proof (prove)
using this:
card {y \<in> A. y < x} = card {y \<in> {0..<M} \<inter> A. y < x}
card {y \<in> {0..<M} \<inter> A. y < x} < card ({0..<M} \<inter> A)
card {i \<in> A. i < x} = y

goal (1 subgoal):
 1. y < card ({0..<M} \<inter> A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y < card ({0..<M} \<inter> A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?y \<in> ind_in_set A ` (A \<inter> {0..<M}) \<Longrightarrow> ?y < card ({0..<M} \<inter> A)

goal (1 subgoal):
 1. ind_in_set A N \<notin> ind_in_set A ` ({0..<M} \<inter> A)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card ({0..<M} \<inter> A) \<le> ind_in_set A N
?y \<in> ind_in_set A ` (A \<inter> {0..<M}) \<Longrightarrow> ?y < card ({0..<M} \<inter> A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card ({0..<M} \<inter> A) \<le> ind_in_set A N
?y \<in> ind_in_set A ` (A \<inter> {0..<M}) \<Longrightarrow> ?y < card ({0..<M} \<inter> A)

goal (1 subgoal):
 1. ind_in_set A N \<notin> ind_in_set A ` ({0..<M} \<inter> A)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ind_in_set A N \<notin> ind_in_set A ` ({0..<M} \<inter> A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_minus_subset:
  "bij_betw f A B \<Longrightarrow> C \<subseteq> A \<Longrightarrow> (f ` A) - (f ` C) = f ` (A - C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bij_betw f A B; C \<subseteq> A\<rbrakk> \<Longrightarrow> f ` A - f ` C = f ` (A - C)
[PROOF STEP]
by (metis Diff_subset bij_betw_imp_inj_on bij_betw_imp_surj_on inj_on_image_set_diff)


[STATEMENT]
lemma ind_in_set_minus_subset_bound:
  fixes A B :: "nat set" and M :: "nat"
  assumes "B \<subseteq> A"
  shows "(ind_in_set A ` ({0..<M} \<inter> A)) - (ind_in_set A ` B) = (ind_in_set A ` ({0..<M} \<inter> A)) \<inter> (ind_in_set A ` (A - B))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
let ?dom = "{0..<M} \<inter> A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
let ?ran = "{0..<card ({0..<M} \<inter> A)}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
let ?f = "ind_in_set A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
let ?C = "A - B"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
have bij: "bij_betw ?f ?dom ?ran"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (ind_in_set A) ({0..<M} \<inter> A) {0..<card ({0..<M} \<inter> A)}
[PROOF STEP]
using bij_ind_in_set_bound[of "?f" A M]
[PROOF STATE]
proof (prove)
using this:
(\<And>x. ind_in_set A x = card {y \<in> A. y < x}) \<Longrightarrow> bij_betw (ind_in_set A) ({0..<M} \<inter> A) {0..<card ({0..<M} \<inter> A)}

goal (1 subgoal):
 1. bij_betw (ind_in_set A) ({0..<M} \<inter> A) {0..<card ({0..<M} \<inter> A)}
[PROOF STEP]
unfolding ind_in_set_def
[PROOF STATE]
proof (prove)
using this:
(\<And>x. card {i \<in> A. i < x} = card {y \<in> A. y < x}) \<Longrightarrow> bij_betw (\<lambda>x. card {i \<in> A. i < x}) ({0..<M} \<inter> A) {0..<card ({0..<M} \<inter> A)}

goal (1 subgoal):
 1. bij_betw (\<lambda>x. card {i \<in> A. i < x}) ({0..<M} \<inter> A) {0..<card ({0..<M} \<inter> A)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bij_betw (ind_in_set A) ({0..<M} \<inter> A) {0..<card ({0..<M} \<inter> A)}

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bij_betw (ind_in_set A) ({0..<M} \<inter> A) {0..<card ({0..<M} \<inter> A)}
[PROOF STEP]
have eq: "?f ` ?dom = ?ran"
[PROOF STATE]
proof (prove)
using this:
bij_betw (ind_in_set A) ({0..<M} \<inter> A) {0..<card ({0..<M} \<inter> A)}

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) = {0..<card ({0..<M} \<inter> A)}
[PROOF STEP]
using bij_betw_imp_surj_on
[PROOF STATE]
proof (prove)
using this:
bij_betw (ind_in_set A) ({0..<M} \<inter> A) {0..<card ({0..<M} \<inter> A)}
bij_betw ?f ?A ?B \<Longrightarrow> ?f ` ?A = ?B

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) = {0..<card ({0..<M} \<inter> A)}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ind_in_set A ` ({0..<M} \<inter> A) = {0..<card ({0..<M} \<inter> A)}

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
have "(?f ` B) = (?f ` ({0..<M} \<inter> B)) \<union> (?f ` ({n. n \<ge> M} \<inter> B))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> B) \<union> ind_in_set A ` ({n. M \<le> n} \<inter> B)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> B) \<union> ind_in_set A ` ({n. M \<le> n} \<inter> B)

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> B) \<union> ind_in_set A ` ({n. M \<le> n} \<inter> B)
[PROOF STEP]
have "(?f ` ?dom) - (?f ` B)
    = (?f ` ?dom) - (?f ` ({n. n \<ge> M} \<inter> B)) - (?f ` ({0..<M} \<inter> B))"
[PROOF STATE]
proof (prove)
using this:
ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> B) \<union> ind_in_set A ` ({n. M \<le> n} \<inter> B)

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` ({n. M \<le> n} \<inter> B) - ind_in_set A ` ({0..<M} \<inter> B)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` ({n. M \<le> n} \<inter> B) - ind_in_set A ` ({0..<M} \<inter> B)

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` ({n. M \<le> n} \<inter> B) - ind_in_set A ` ({0..<M} \<inter> B)

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
have "(?f ` ({n. n \<ge> M} \<inter> B)) \<inter> (?f ` ?dom) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set A ` ({n. M \<le> n} \<inter> B) \<inter> ind_in_set A ` ({0..<M} \<inter> A) = {}
[PROOF STEP]
using ind_in_set_bound[of M _ A]
[PROOF STATE]
proof (prove)
using this:
M \<le> ?N \<Longrightarrow> ind_in_set A ?N \<notin> ind_in_set A ` ({0..<M} \<inter> A)

goal (1 subgoal):
 1. ind_in_set A ` ({n. M \<le> n} \<inter> B) \<inter> ind_in_set A ` ({0..<M} \<inter> A) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ind_in_set A ` ({n. M \<le> n} \<inter> B) \<inter> ind_in_set A ` ({0..<M} \<inter> A) = {}

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` ({n. M \<le> n} \<inter> B) - ind_in_set A ` ({0..<M} \<inter> B)
ind_in_set A ` ({n. M \<le> n} \<inter> B) \<inter> ind_in_set A ` ({0..<M} \<inter> A) = {}
[PROOF STEP]
have eq1: "(?f ` ?dom) - (?f ` B) = (?f ` ?dom) - (?f ` ({0..<M} \<inter> B))"
[PROOF STATE]
proof (prove)
using this:
ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` ({n. M \<le> n} \<inter> B) - ind_in_set A ` ({0..<M} \<inter> B)
ind_in_set A ` ({n. M \<le> n} \<inter> B) \<inter> ind_in_set A ` ({0..<M} \<inter> A) = {}

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` ({0..<M} \<inter> B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` ({0..<M} \<inter> B)

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
have "{0..<M} \<inter> B \<subseteq> ?dom"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<M} \<inter> B \<subseteq> {0..<M} \<inter> A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> A

goal (1 subgoal):
 1. {0..<M} \<inter> B \<subseteq> {0..<M} \<inter> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{0..<M} \<inter> B \<subseteq> {0..<M} \<inter> A

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{0..<M} \<inter> B \<subseteq> {0..<M} \<inter> A
[PROOF STEP]
have "(?f ` ?dom) - (?f ` ({0..<M} \<inter> B)) = ?f ` (?dom - ({0..<M} \<inter> B))"
[PROOF STATE]
proof (prove)
using this:
{0..<M} \<inter> B \<subseteq> {0..<M} \<inter> A

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` ({0..<M} \<inter> B) = ind_in_set A ` ({0..<M} \<inter> A - {0..<M} \<inter> B)
[PROOF STEP]
using bij bij_minus_subset[of "?f"]
[PROOF STATE]
proof (prove)
using this:
{0..<M} \<inter> B \<subseteq> {0..<M} \<inter> A
bij_betw (ind_in_set A) ({0..<M} \<inter> A) {0..<card ({0..<M} \<inter> A)}
\<lbrakk>bij_betw (ind_in_set A) ?A ?B; ?C \<subseteq> ?A\<rbrakk> \<Longrightarrow> ind_in_set A ` ?A - ind_in_set A ` ?C = ind_in_set A ` (?A - ?C)

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` ({0..<M} \<inter> B) = ind_in_set A ` ({0..<M} \<inter> A - {0..<M} \<inter> B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` ({0..<M} \<inter> B) = ind_in_set A ` ({0..<M} \<inter> A - {0..<M} \<inter> B)

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` ({0..<M} \<inter> B) = ind_in_set A ` ({0..<M} \<inter> A - {0..<M} \<inter> B)

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
have "\<dots> = ?f ` ({0..<M} \<inter> ?C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A - {0..<M} \<inter> B) = ind_in_set A ` ({0..<M} \<inter> (A - B))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ind_in_set A ` ({0..<M} \<inter> A - {0..<M} \<inter> B) = ind_in_set A ` ({0..<M} \<inter> (A - B))

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` ({0..<M} \<inter> B) = ind_in_set A ` ({0..<M} \<inter> (A - B))
[PROOF STEP]
have eq2: "(?f ` ?dom) - (?f ` B) = ?f ` ({0..<M} \<inter> ?C)"
[PROOF STATE]
proof (prove)
using this:
ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` ({0..<M} \<inter> B) = ind_in_set A ` ({0..<M} \<inter> (A - B))

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> (A - B))
[PROOF STEP]
using eq1
[PROOF STATE]
proof (prove)
using this:
ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` ({0..<M} \<inter> B) = ind_in_set A ` ({0..<M} \<inter> (A - B))
ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` ({0..<M} \<inter> B)

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> (A - B))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> (A - B))

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
have "(?f ` ?C) = (?f ` ({0..<M} \<inter> ?C)) \<union> (?f ` ({n. n \<ge> M} \<inter> ?C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set A ` (A - B) = ind_in_set A ` ({0..<M} \<inter> (A - B)) \<union> ind_in_set A ` ({n. M \<le> n} \<inter> (A - B))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ind_in_set A ` (A - B) = ind_in_set A ` ({0..<M} \<inter> (A - B)) \<union> ind_in_set A ` ({n. M \<le> n} \<inter> (A - B))

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ind_in_set A ` (A - B) = ind_in_set A ` ({0..<M} \<inter> (A - B)) \<union> ind_in_set A ` ({n. M \<le> n} \<inter> (A - B))

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
have "(?f ` ({n. n \<ge> M} \<inter> ?C)) \<inter> (?f ` ?dom) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set A ` ({n. M \<le> n} \<inter> (A - B)) \<inter> ind_in_set A ` ({0..<M} \<inter> A) = {}
[PROOF STEP]
using ind_in_set_bound[of M _ A]
[PROOF STATE]
proof (prove)
using this:
M \<le> ?N \<Longrightarrow> ind_in_set A ?N \<notin> ind_in_set A ` ({0..<M} \<inter> A)

goal (1 subgoal):
 1. ind_in_set A ` ({n. M \<le> n} \<inter> (A - B)) \<inter> ind_in_set A ` ({0..<M} \<inter> A) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ind_in_set A ` ({n. M \<le> n} \<inter> (A - B)) \<inter> ind_in_set A ` ({0..<M} \<inter> A) = {}

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ind_in_set A ` (A - B) = ind_in_set A ` ({0..<M} \<inter> (A - B)) \<union> ind_in_set A ` ({n. M \<le> n} \<inter> (A - B))
ind_in_set A ` ({n. M \<le> n} \<inter> (A - B)) \<inter> ind_in_set A ` ({0..<M} \<inter> A) = {}
[PROOF STEP]
have eq3:"(ind_in_set A ` ?dom) \<inter> (?f ` ?C) = (ind_in_set A ` ?dom) \<inter> (?f ` ({0..<M} \<inter> ?C))"
[PROOF STATE]
proof (prove)
using this:
ind_in_set A ` (A - B) = ind_in_set A ` ({0..<M} \<inter> (A - B)) \<union> ind_in_set A ` ({n. M \<le> n} \<inter> (A - B))
ind_in_set A ` ({n. M \<le> n} \<inter> (A - B)) \<inter> ind_in_set A ` ({0..<M} \<inter> A) = {}

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B) = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` ({0..<M} \<inter> (A - B))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B) = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` ({0..<M} \<inter> (A - B))

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
have "{0..<M} \<inter> ?C \<subseteq> ?dom"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<M} \<inter> (A - B) \<subseteq> {0..<M} \<inter> A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> A

goal (1 subgoal):
 1. {0..<M} \<inter> (A - B) \<subseteq> {0..<M} \<inter> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{0..<M} \<inter> (A - B) \<subseteq> {0..<M} \<inter> A

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{0..<M} \<inter> (A - B) \<subseteq> {0..<M} \<inter> A
[PROOF STEP]
have "(ind_in_set A ` ?dom) \<inter> (?f ` ({0..<M} \<inter> ?C)) = (?f ` ({0..<M} \<inter> ?C))"
[PROOF STATE]
proof (prove)
using this:
{0..<M} \<inter> (A - B) \<subseteq> {0..<M} \<inter> A

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` ({0..<M} \<inter> (A - B)) = ind_in_set A ` ({0..<M} \<inter> (A - B))
[PROOF STEP]
using bij
[PROOF STATE]
proof (prove)
using this:
{0..<M} \<inter> (A - B) \<subseteq> {0..<M} \<inter> A
bij_betw (ind_in_set A) ({0..<M} \<inter> A) {0..<card ({0..<M} \<inter> A)}

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` ({0..<M} \<inter> (A - B)) = ind_in_set A ` ({0..<M} \<inter> (A - B))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` ({0..<M} \<inter> (A - B)) = ind_in_set A ` ({0..<M} \<inter> (A - B))

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` ({0..<M} \<inter> (A - B)) = ind_in_set A ` ({0..<M} \<inter> (A - B))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` ({0..<M} \<inter> (A - B)) = ind_in_set A ` ({0..<M} \<inter> (A - B))

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
using eq2 eq3
[PROOF STATE]
proof (prove)
using this:
ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` ({0..<M} \<inter> (A - B)) = ind_in_set A ` ({0..<M} \<inter> (A - B))
ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> (A - B))
ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B) = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` ({0..<M} \<inter> (A - B))

goal (1 subgoal):
 1. ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ind_in_set A ` ({0..<M} \<inter> A) - ind_in_set A ` B = ind_in_set A ` ({0..<M} \<inter> A) \<inter> ind_in_set A ` (A - B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ind_in_set_iff:
  fixes A B :: "nat set"
  assumes "x \<in> A" and "B \<subseteq> A"
  shows "ind_in_set A x \<in> (ind_in_set A ` B) = (x \<in> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ind_in_set A x \<in> ind_in_set A ` B) = (x \<in> B)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ind_in_set A x \<in> ind_in_set A ` B \<Longrightarrow> x \<in> B
 2. x \<in> B \<Longrightarrow> ind_in_set A x \<in> ind_in_set A ` B
[PROOF STEP]
have lemm: "card {i. i \<in> A \<and> i < (x::nat) } = card {i. i \<in> A \<and> i < (y::nat) } \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x = y" for A x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>card {i \<in> A. i < x} = card {i \<in> A. i < y}; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
by (metis (full_types) pick_card_in_set)
[PROOF STATE]
proof (state)
this:
\<lbrakk>card {i \<in> ?A. i < ?x} = card {i \<in> ?A. i < ?y}; ?x \<in> ?A; ?y \<in> ?A\<rbrakk> \<Longrightarrow> ?x = ?y

goal (2 subgoals):
 1. ind_in_set A x \<in> ind_in_set A ` B \<Longrightarrow> x \<in> B
 2. x \<in> B \<Longrightarrow> ind_in_set A x \<in> ind_in_set A ` B
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>card {i \<in> ?A. i < ?x} = card {i \<in> ?A. i < ?y}; ?x \<in> ?A; ?y \<in> ?A\<rbrakk> \<Longrightarrow> ?x = ?y

goal (2 subgoals):
 1. ind_in_set A x \<in> ind_in_set A ` B \<Longrightarrow> x \<in> B
 2. x \<in> B \<Longrightarrow> ind_in_set A x \<in> ind_in_set A ` B
[PROOF STEP]
assume "ind_in_set A x \<in> (ind_in_set A ` B)"
[PROOF STATE]
proof (state)
this:
ind_in_set A x \<in> ind_in_set A ` B

goal (2 subgoals):
 1. ind_in_set A x \<in> ind_in_set A ` B \<Longrightarrow> x \<in> B
 2. x \<in> B \<Longrightarrow> ind_in_set A x \<in> ind_in_set A ` B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ind_in_set A x \<in> ind_in_set A ` B
[PROOF STEP]
have "\<exists>y \<in> B. card {i \<in> A. i < x} = card {i \<in> A. i < y}"
[PROOF STATE]
proof (prove)
using this:
ind_in_set A x \<in> ind_in_set A ` B

goal (1 subgoal):
 1. \<exists>y\<in>B. card {i \<in> A. i < x} = card {i \<in> A. i < y}
[PROOF STEP]
unfolding ind_in_set_def
[PROOF STATE]
proof (prove)
using this:
card {i \<in> A. i < x} \<in> (\<lambda>x. card {i \<in> A. i < x}) ` B

goal (1 subgoal):
 1. \<exists>y\<in>B. card {i \<in> A. i < x} = card {i \<in> A. i < y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>B. card {i \<in> A. i < x} = card {i \<in> A. i < y}

goal (2 subgoals):
 1. ind_in_set A x \<in> ind_in_set A ` B \<Longrightarrow> x \<in> B
 2. x \<in> B \<Longrightarrow> ind_in_set A x \<in> ind_in_set A ` B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y\<in>B. card {i \<in> A. i < x} = card {i \<in> A. i < y}
[PROOF STEP]
obtain y where y1: "y \<in> B" and ceq: "card {i \<in> A. i < x} = card {i \<in> A. i < y}"
[PROOF STATE]
proof (prove)
using this:
\<exists>y\<in>B. card {i \<in> A. i < x} = card {i \<in> A. i < y}

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> B; card {i \<in> A. i < x} = card {i \<in> A. i < y}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> B
card {i \<in> A. i < x} = card {i \<in> A. i < y}

goal (2 subgoals):
 1. ind_in_set A x \<in> ind_in_set A ` B \<Longrightarrow> x \<in> B
 2. x \<in> B \<Longrightarrow> ind_in_set A x \<in> ind_in_set A ` B
[PROOF STEP]
with y1 assms
[PROOF STATE]
proof (chain)
picking this:
y \<in> B
x \<in> A
B \<subseteq> A
y \<in> B
card {i \<in> A. i < x} = card {i \<in> A. i < y}
[PROOF STEP]
have y0: "y \<in> A"
[PROOF STATE]
proof (prove)
using this:
y \<in> B
x \<in> A
B \<subseteq> A
y \<in> B
card {i \<in> A. i < x} = card {i \<in> A. i < y}

goal (1 subgoal):
 1. y \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> A

goal (2 subgoals):
 1. ind_in_set A x \<in> ind_in_set A ` B \<Longrightarrow> x \<in> B
 2. x \<in> B \<Longrightarrow> ind_in_set A x \<in> ind_in_set A ` B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> A
[PROOF STEP]
have "x = y"
[PROOF STATE]
proof (prove)
using this:
y \<in> A

goal (1 subgoal):
 1. x = y
[PROOF STEP]
using lemm[OF ceq] y0 assms
[PROOF STATE]
proof (prove)
using this:
y \<in> A
\<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x = y
y \<in> A
x \<in> A
B \<subseteq> A

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

goal (2 subgoals):
 1. ind_in_set A x \<in> ind_in_set A ` B \<Longrightarrow> x \<in> B
 2. x \<in> B \<Longrightarrow> ind_in_set A x \<in> ind_in_set A ` B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = y
[PROOF STEP]
show "x \<in> B"
[PROOF STATE]
proof (prove)
using this:
x = y

goal (1 subgoal):
 1. x \<in> B
[PROOF STEP]
using y1
[PROOF STATE]
proof (prove)
using this:
x = y
y \<in> B

goal (1 subgoal):
 1. x \<in> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> B

goal (1 subgoal):
 1. x \<in> B \<Longrightarrow> ind_in_set A x \<in> ind_in_set A ` B
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
ind_in_set A x \<in> ind_in_set A ` B \<Longrightarrow> x \<in> B

goal (1 subgoal):
 1. x \<in> B \<Longrightarrow> ind_in_set A x \<in> ind_in_set A ` B
[PROOF STEP]
qed (simp add: ind_in_set_def)