[STATEMENT]
lemma ereal_truncation_top [tendsto_intros]:
  fixes x::ereal
  shows "(\<lambda>n::nat. min x n) \<longlonglongrightarrow> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
[PROOF STEP]
proof (cases x)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>r. x = ereal r \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
 2. x = \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
 3. x = - \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
[PROOF STEP]
case (real r)
[PROOF STATE]
proof (state)
this:
x = ereal r

goal (3 subgoals):
 1. \<And>r. x = ereal r \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
 2. x = \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
 3. x = - \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = ereal r
[PROOF STEP]
obtain K::nat where "K>0" "K > abs(r)"
[PROOF STATE]
proof (prove)
using this:
x = ereal r

goal (1 subgoal):
 1. (\<And>K. \<lbrakk>0 < K; \<bar>r\<bar> < real K\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using reals_Archimedean2 gr0I
[PROOF STATE]
proof (prove)
using this:
x = ereal r
\<exists>n. ?x < of_nat n
(?n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < ?n

goal (1 subgoal):
 1. (\<And>K. \<lbrakk>0 < K; \<bar>r\<bar> < real K\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < K
\<bar>r\<bar> < real K

goal (3 subgoals):
 1. \<And>r. x = ereal r \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
 2. x = \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
 3. x = - \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < K
\<bar>r\<bar> < real K
[PROOF STEP]
have "min x n = x" if "n \<ge> K" for n
[PROOF STATE]
proof (prove)
using this:
0 < K
\<bar>r\<bar> < real K

goal (1 subgoal):
 1. min x (ereal (real n)) = x
[PROOF STEP]
apply (subst real, subst real, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < K; \<bar>r\<bar> < real K\<rbrakk> \<Longrightarrow> min (ereal r) (ereal (real n)) = ereal r
[PROOF STEP]
using that eq_iff
[PROOF STATE]
proof (prove)
using this:
K \<le> n
(?a = ?b) = (?a \<le> ?b \<and> ?b \<le> ?a)

goal (1 subgoal):
 1. \<lbrakk>0 < K; \<bar>r\<bar> < real K\<rbrakk> \<Longrightarrow> min (ereal r) (ereal (real n)) = ereal r
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
K \<le> ?n \<Longrightarrow> min x (ereal (real ?n)) = x

goal (3 subgoals):
 1. \<And>r. x = ereal r \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
 2. x = \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
 3. x = - \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
K \<le> ?n \<Longrightarrow> min x (ereal (real ?n)) = x
[PROOF STEP]
have "eventually (\<lambda>n. min x n = x) sequentially"
[PROOF STATE]
proof (prove)
using this:
K \<le> ?n \<Longrightarrow> min x (ereal (real ?n)) = x

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. min x (ereal (real n)) = x
[PROOF STEP]
using eventually_at_top_linorder
[PROOF STATE]
proof (prove)
using this:
K \<le> ?n \<Longrightarrow> min x (ereal (real ?n)) = x
eventually ?P at_top = (\<exists>N. \<forall>n\<ge>N. ?P n)

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. min x (ereal (real n)) = x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. min x (ereal (real n)) = x

goal (3 subgoals):
 1. \<And>r. x = ereal r \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
 2. x = \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
 3. x = - \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F n in sequentially. min x (ereal (real n)) = x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. min x (ereal (real n)) = x

goal (1 subgoal):
 1. (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
[PROOF STEP]
by (simp add: tendsto_eventually)
[PROOF STATE]
proof (state)
this:
(\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x

goal (2 subgoals):
 1. x = \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
 2. x = - \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
 2. x = - \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
[PROOF STEP]
case (PInf)
[PROOF STATE]
proof (state)
this:
x = \<infinity>

goal (2 subgoals):
 1. x = \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
 2. x = - \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = \<infinity>
[PROOF STEP]
have "min x n = n" for n::nat
[PROOF STATE]
proof (prove)
using this:
x = \<infinity>

goal (1 subgoal):
 1. min x (ereal (real n)) = ereal (real n)
[PROOF STEP]
by (auto simp add: min_def)
[PROOF STATE]
proof (state)
this:
min x (ereal (real ?n)) = ereal (real ?n)

goal (2 subgoals):
 1. x = \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
 2. x = - \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
min x (ereal (real ?n)) = ereal (real ?n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
min x (ereal (real ?n)) = ereal (real ?n)

goal (1 subgoal):
 1. (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
[PROOF STEP]
using id_nat_ereal_tendsto_PInf PInf
[PROOF STATE]
proof (prove)
using this:
min x (ereal (real ?n)) = ereal (real ?n)
(\<lambda>x. ereal (real x)) \<longlonglongrightarrow> \<infinity>
x = \<infinity>

goal (1 subgoal):
 1. (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x

goal (1 subgoal):
 1. x = - \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = - \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
[PROOF STEP]
case (MInf)
[PROOF STATE]
proof (state)
this:
x = - \<infinity>

goal (1 subgoal):
 1. x = - \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = - \<infinity>
[PROOF STEP]
have "min x n = x" for n::nat
[PROOF STATE]
proof (prove)
using this:
x = - \<infinity>

goal (1 subgoal):
 1. min x (ereal (real n)) = x
[PROOF STEP]
by (auto simp add: min_def)
[PROOF STATE]
proof (state)
this:
min x (ereal (real ?n)) = x

goal (1 subgoal):
 1. x = - \<infinity> \<Longrightarrow> (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
min x (ereal (real ?n)) = x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
min x (ereal (real ?n)) = x

goal (1 subgoal):
 1. (\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>xa. min x (ereal (real xa))) \<longlonglongrightarrow> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma binomial_fact':
  assumes "k \<le> n"
  shows "n choose k = fact n div (fact k * fact (n - k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n choose k = fact n div (fact k * fact (n - k))
[PROOF STEP]
using binomial_fact_lemma [OF assms]
[PROOF STATE]
proof (prove)
using this:
fact k * fact (n - k) * (n choose k) = fact n

goal (1 subgoal):
 1. n choose k = fact n div (fact k * fact (n - k))
[PROOF STEP]
by (metis fact_nonzero mult_eq_0_iff nonzero_mult_div_cancel_left)


[STATEMENT]
lemma tendsto_set_lebesgue_integral_at_right:
  fixes a b :: real and f :: "real \<Rightarrow> 'a :: {banach,second_countable_topology}"
  assumes "a < b" and sets: "\<And>a'. a' \<in> {a<..b} \<Longrightarrow> {a'..b} \<in> sets M"
      and "set_integrable M {a<..b} f"
  shows   "((\<lambda>a'. set_lebesgue_integral M {a'..b} f) \<longlongrightarrow>
             set_lebesgue_integral M {a<..b} f) (at_right a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>a'. set_lebesgue_integral M {a'..b} f) \<longlongrightarrow> set_lebesgue_integral M {a<..b} f) (at_right a)
[PROOF STEP]
proof (rule tendsto_at_right_sequentially[OF assms(1)], goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S. \<lbrakk>\<And>n. a < S n; \<And>n. S n < b; decseq S; S \<longlonglongrightarrow> a\<rbrakk> \<Longrightarrow> (\<lambda>n. set_lebesgue_integral M {S n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M {a<..b} f
[PROOF STEP]
case (1 S)
[PROOF STATE]
proof (state)
this:
a < S ?n
S ?n < b
decseq S
S \<longlonglongrightarrow> a

goal (1 subgoal):
 1. \<And>S. \<lbrakk>\<And>n. a < S n; \<And>n. S n < b; decseq S; S \<longlonglongrightarrow> a\<rbrakk> \<Longrightarrow> (\<lambda>n. set_lebesgue_integral M {S n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M {a<..b} f
[PROOF STEP]
have eq: "(\<Union>n. {S n..b}) = {a<..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>n. {S n..b}) = {a<..b}
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x n. \<lbrakk>n \<in> UNIV; x \<in> {S n..b}\<rbrakk> \<Longrightarrow> x \<in> {a<..b}
 2. \<And>x. x \<in> {a<..b} \<Longrightarrow> x \<in> (\<Union>n. {S n..b})
[PROOF STEP]
fix x n
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x n. \<lbrakk>n \<in> UNIV; x \<in> {S n..b}\<rbrakk> \<Longrightarrow> x \<in> {a<..b}
 2. \<And>x. x \<in> {a<..b} \<Longrightarrow> x \<in> (\<Union>n. {S n..b})
[PROOF STEP]
assume "x \<in> {S n..b}"
[PROOF STATE]
proof (state)
this:
x \<in> {S n..b}

goal (2 subgoals):
 1. \<And>x n. \<lbrakk>n \<in> UNIV; x \<in> {S n..b}\<rbrakk> \<Longrightarrow> x \<in> {a<..b}
 2. \<And>x. x \<in> {a<..b} \<Longrightarrow> x \<in> (\<Union>n. {S n..b})
[PROOF STEP]
with 1(1,2)[of n]
[PROOF STATE]
proof (chain)
picking this:
a < S n
S n < b
x \<in> {S n..b}
[PROOF STEP]
show "x \<in> {a<..b}"
[PROOF STATE]
proof (prove)
using this:
a < S n
S n < b
x \<in> {S n..b}

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

goal (1 subgoal):
 1. \<And>x. x \<in> {a<..b} \<Longrightarrow> x \<in> (\<Union>n. {S n..b})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {a<..b} \<Longrightarrow> x \<in> (\<Union>n. {S n..b})
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {a<..b} \<Longrightarrow> x \<in> (\<Union>n. {S n..b})
[PROOF STEP]
assume "x \<in> {a<..b}"
[PROOF STATE]
proof (state)
this:
x \<in> {a<..b}

goal (1 subgoal):
 1. \<And>x. x \<in> {a<..b} \<Longrightarrow> x \<in> (\<Union>n. {S n..b})
[PROOF STEP]
with order_tendstoD[OF \<open>S \<longlonglongrightarrow> a\<close>, of x]
[PROOF STATE]
proof (chain)
picking this:
x < a \<Longrightarrow> \<forall>\<^sub>F xa in sequentially. x < S xa
a < x \<Longrightarrow> \<forall>\<^sub>F xa in sequentially. S xa < x
x \<in> {a<..b}
[PROOF STEP]
show "x \<in> (\<Union>n. {S n..b})"
[PROOF STATE]
proof (prove)
using this:
x < a \<Longrightarrow> \<forall>\<^sub>F xa in sequentially. x < S xa
a < x \<Longrightarrow> \<forall>\<^sub>F xa in sequentially. S xa < x
x \<in> {a<..b}

goal (1 subgoal):
 1. x \<in> (\<Union>n. {S n..b})
[PROOF STEP]
by (force simp: eventually_at_top_linorder dest: less_imp_le)
[PROOF STATE]
proof (state)
this:
x \<in> (\<Union>n. {S n..b})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Union>n. {S n..b}) = {a<..b}

goal (1 subgoal):
 1. \<And>S. \<lbrakk>\<And>n. a < S n; \<And>n. S n < b; decseq S; S \<longlonglongrightarrow> a\<rbrakk> \<Longrightarrow> (\<lambda>n. set_lebesgue_integral M {S n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M {a<..b} f
[PROOF STEP]
have "(\<lambda>n. set_lebesgue_integral M {S n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M (\<Union>n. {S n..b}) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. set_lebesgue_integral M {S n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M (\<Union>n. {S n..b}) f
[PROOF STEP]
by (rule set_integral_cont_up) (insert assms 1, auto simp: eq incseq_def decseq_def less_imp_le)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. set_lebesgue_integral M {S n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M (\<Union>n. {S n..b}) f

goal (1 subgoal):
 1. \<And>S. \<lbrakk>\<And>n. a < S n; \<And>n. S n < b; decseq S; S \<longlonglongrightarrow> a\<rbrakk> \<Longrightarrow> (\<lambda>n. set_lebesgue_integral M {S n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M {a<..b} f
[PROOF STEP]
with eq
[PROOF STATE]
proof (chain)
picking this:
(\<Union>n. {S n..b}) = {a<..b}
(\<lambda>n. set_lebesgue_integral M {S n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M (\<Union>n. {S n..b}) f
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Union>n. {S n..b}) = {a<..b}
(\<lambda>n. set_lebesgue_integral M {S n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M (\<Union>n. {S n..b}) f

goal (1 subgoal):
 1. (\<lambda>n. set_lebesgue_integral M {S n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M {a<..b} f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>n. set_lebesgue_integral M {S n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M {a<..b} f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma continuous_on_vector_derivative:
  "(\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)) \<Longrightarrow> continuous_on S f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)) \<Longrightarrow> continuous_on S f
[PROOF STEP]
by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)


[STATEMENT]
lemma DERIV_unique: "DERIV f x :> D \<Longrightarrow> DERIV f x :> E \<Longrightarrow> D = E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(f has_field_derivative D) (at x); (f has_field_derivative E) (at x)\<rbrakk> \<Longrightarrow> D = E
[PROOF STEP]
unfolding DERIV_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0::'a\<rightarrow> D; (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0::'a\<rightarrow> E\<rbrakk> \<Longrightarrow> D = E
[PROOF STEP]
by (rule LIM_unique)


[STATEMENT]
lemma continuous_floor:
  fixes x::real
  shows "x \<notin> \<int> \<Longrightarrow> continuous (at x) (real_of_int \<circ> floor)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> \<int> \<Longrightarrow> isCont (real_of_int \<circ> floor) x
[PROOF STEP]
using floor_has_real_derivative [where f=id]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>isCont id ?x; id ?x \<notin> \<int>\<rbrakk> \<Longrightarrow> ((\<lambda>x. real_of_int \<lfloor>id x\<rfloor>) has_real_derivative 0) (at ?x)

goal (1 subgoal):
 1. x \<notin> \<int> \<Longrightarrow> isCont (real_of_int \<circ> floor) x
[PROOF STEP]
by (auto simp: o_def has_field_derivative_def intro: has_derivative_continuous)


[STATEMENT]
lemma DERIV_pos_inc_right:
  fixes f :: "real \<Rightarrow> real"
  assumes der: "DERIV f x :> l"
    and l: "0 < l"
  shows "\<exists>d > 0. \<forall>h > 0. h < d \<longrightarrow> f x < f (x + h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>d>0. \<forall>h>0. h < d \<longrightarrow> f x < f (x + h)
[PROOF STEP]
using has_real_derivative_pos_inc_right[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<exists>d>0. \<forall>h>0. x + h \<in> UNIV \<longrightarrow> h < d \<longrightarrow> f x < f (x + h)

goal (1 subgoal):
 1. \<exists>d>0. \<forall>h>0. h < d \<longrightarrow> f x < f (x + h)
[PROOF STEP]
by auto


[STATEMENT]
lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner (x - y) z = inner x z - inner y z
[PROOF STEP]
using inner_add_left [of x "- y" z]
[PROOF STATE]
proof (prove)
using this:
inner (x + - y) z = inner x z + inner (- y) z

goal (1 subgoal):
 1. inner (x - y) z = inner x z - inner y z
[PROOF STEP]
by simp


[STATEMENT]
lemma norm_eq_square: "norm x = a \<longleftrightarrow> 0 \<le> a \<and> inner x x = a\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (norm x = a) = (0 \<le> a \<and> inner x x = a\<^sup>2)
[PROOF STEP]
by (auto simp add: norm_eq_sqrt_inner)


[STATEMENT]
lemma quot_of_fract_mult:
  "quot_of_fract (x * y) =
     (let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y;
          (e,f) = normalize_quot (a,d); (g,h) = normalize_quot (c,b)
      in  (e*g, f*h))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quot_of_fract (x * y) = (let (a, b) = quot_of_fract x; (c, d) = quot_of_fract y; (e, f) = normalize_quot (a, d); (g, h) = normalize_quot (c, b) in (e * g, f * h))
[PROOF STEP]
by transfer
     (simp add: split_def Let_def coprime_normalize_quot normalize_quot_mult normalize_quot_mult_coprime)


[STATEMENT]
lemma valid_countings_Suc_Suc:
  assumes "b < a"
  shows "valid_countings (Suc a) (Suc b) = valid_countings a (Suc b) + valid_countings (Suc a) b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_countings (Suc a) (Suc b) = valid_countings a (Suc b) + valid_countings (Suc a) b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valid_countings (Suc a) (Suc b) = valid_countings a (Suc b) + valid_countings (Suc a) b
[PROOF STEP]
let ?l = "Suc (a + b)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valid_countings (Suc a) (Suc b) = valid_countings a (Suc b) + valid_countings (Suc a) b
[PROOF STEP]
let ?Q = "\<lambda>V c. \<forall>m\<in>{1..c}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valid_countings (Suc a) (Suc b) = valid_countings a (Suc b) + valid_countings (Suc a) b
[PROOF STEP]
let ?V = "\<lambda>P. {V. (V \<in> Pow {0..<Suc ?l} \<and> P V) \<and> card V = Suc a \<and> ?Q V (Suc ?l)}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valid_countings (Suc a) (Suc b) = valid_countings a (Suc b) + valid_countings (Suc a) b
[PROOF STEP]
have "valid_countings (Suc a) (Suc b) = card (?V (\<lambda>V. ?l \<notin> V)) + card (?V (\<lambda>V. ?l \<in> V))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_countings (Suc a) (Suc b) = card {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<notin> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} + card {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}
[PROOF STEP]
unfolding valid_countings_set
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {V \<in> Pow {0..<Suc a + Suc b}. card V = Suc a \<and> (\<forall>m\<in>{1..Suc a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} = card {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<notin> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} + card {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}
[PROOF STEP]
by (subst card_Un_disjoint[symmetric]) (auto simp add: set_eq_iff intro!: arg_cong[where f=card])
[PROOF STATE]
proof (state)
this:
valid_countings (Suc a) (Suc b) = card {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<notin> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} + card {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}

goal (1 subgoal):
 1. valid_countings (Suc a) (Suc b) = valid_countings a (Suc b) + valid_countings (Suc a) b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
valid_countings (Suc a) (Suc b) = card {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<notin> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} + card {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}

goal (1 subgoal):
 1. valid_countings (Suc a) (Suc b) = valid_countings a (Suc b) + valid_countings (Suc a) b
[PROOF STEP]
have "card (?V (\<lambda>V. ?l \<in> V)) = valid_countings a (Suc b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} = valid_countings a (Suc b)
[PROOF STEP]
unfolding valid_countings_set
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} = card {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}
[PROOF STEP]
proof (rule card_bij'[where f="\<lambda>V. V - {?l}" and g="insert ?l"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. (\<lambda>V. V - {Suc (a + b)}) \<in> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<rightarrow> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}
 2. \<And>x. x \<in> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<Longrightarrow> insert (Suc (a + b)) (x - {Suc (a + b)}) = x
 3. insert (Suc (a + b)) \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<rightarrow> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}
 4. \<And>x. x \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<Longrightarrow> insert (Suc (a + b)) x - {Suc (a + b)} = x
[PROOF STEP]
have *: "\<And>m V. m \<in> {1..a + Suc b} \<Longrightarrow> {0..<m} \<inter> (V - {?l}) = {0..<m} \<inter> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m V. m \<in> {1..a + Suc b} \<Longrightarrow> {0..<m} \<inter> (V - {Suc (a + b)}) = {0..<m} \<inter> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?m \<in> {1..a + Suc b} \<Longrightarrow> {0..<?m} \<inter> (?V - {Suc (a + b)}) = {0..<?m} \<inter> ?V

goal (4 subgoals):
 1. (\<lambda>V. V - {Suc (a + b)}) \<in> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<rightarrow> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}
 2. \<And>x. x \<in> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<Longrightarrow> insert (Suc (a + b)) (x - {Suc (a + b)}) = x
 3. insert (Suc (a + b)) \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<rightarrow> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}
 4. \<And>x. x \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<Longrightarrow> insert (Suc (a + b)) x - {Suc (a + b)} = x
[PROOF STEP]
show "(\<lambda>V. V - {?l}) \<in> ?V (\<lambda>V. ?l \<in> V) \<rightarrow> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> ?Q V (a + Suc b)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>V. V - {Suc (a + b)}) \<in> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<rightarrow> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}
[PROOF STEP]
by (auto simp: Ico_subset_finite *)
[PROOF STATE]
proof (state)
this:
(\<lambda>V. V - {Suc (a + b)}) \<in> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<rightarrow> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}

goal (3 subgoals):
 1. \<And>x. x \<in> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<Longrightarrow> insert (Suc (a + b)) (x - {Suc (a + b)}) = x
 2. insert (Suc (a + b)) \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<rightarrow> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}
 3. \<And>x. x \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<Longrightarrow> insert (Suc (a + b)) x - {Suc (a + b)} = x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(\<lambda>V. V - {Suc (a + b)}) \<in> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<rightarrow> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}

goal (3 subgoals):
 1. \<And>x. x \<in> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<Longrightarrow> insert (Suc (a + b)) (x - {Suc (a + b)}) = x
 2. insert (Suc (a + b)) \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<rightarrow> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}
 3. \<And>x. x \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<Longrightarrow> insert (Suc (a + b)) x - {Suc (a + b)} = x
[PROOF STEP]
fix V
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<Longrightarrow> insert (Suc (a + b)) (x - {Suc (a + b)}) = x
 2. insert (Suc (a + b)) \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<rightarrow> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}
 3. \<And>x. x \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<Longrightarrow> insert (Suc (a + b)) x - {Suc (a + b)} = x
[PROOF STEP]
assume V: "V \<subseteq> {0..<?l}"
[PROOF STATE]
proof (state)
this:
V \<subseteq> {0..<Suc (a + b)}

goal (3 subgoals):
 1. \<And>x. x \<in> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<Longrightarrow> insert (Suc (a + b)) (x - {Suc (a + b)}) = x
 2. insert (Suc (a + b)) \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<rightarrow> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}
 3. \<And>x. x \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<Longrightarrow> insert (Suc (a + b)) x - {Suc (a + b)} = x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
V \<subseteq> {0..<Suc (a + b)}
[PROOF STEP]
have "finite V" "?l \<notin> V" "{0..<Suc ?l} \<inter> V = V"
[PROOF STATE]
proof (prove)
using this:
V \<subseteq> {0..<Suc (a + b)}

goal (1 subgoal):
 1. finite V &&& Suc (a + b) \<notin> V &&& {0..<Suc (Suc (a + b))} \<inter> V = V
[PROOF STEP]
by (auto dest: finite_subset)
[PROOF STATE]
proof (state)
this:
finite V
Suc (a + b) \<notin> V
{0..<Suc (Suc (a + b))} \<inter> V = V

goal (3 subgoals):
 1. \<And>x. x \<in> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<Longrightarrow> insert (Suc (a + b)) (x - {Suc (a + b)}) = x
 2. insert (Suc (a + b)) \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<rightarrow> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}
 3. \<And>x. x \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<Longrightarrow> insert (Suc (a + b)) x - {Suc (a + b)} = x
[PROOF STEP]
with V
[PROOF STATE]
proof (chain)
picking this:
V \<subseteq> {0..<Suc (a + b)}
finite V
Suc (a + b) \<notin> V
{0..<Suc (Suc (a + b))} \<inter> V = V
[PROOF STEP]
have "card (insert ?l V) = Suc (card V)"
        "card ({0..<m} \<inter> insert ?l V) = (if m = Suc ?l then Suc (card V) else card ({0..<m} \<inter> V))"
        if "m \<le> Suc ?l" for m
[PROOF STATE]
proof (prove)
using this:
V \<subseteq> {0..<Suc (a + b)}
finite V
Suc (a + b) \<notin> V
{0..<Suc (Suc (a + b))} \<inter> V = V

goal (1 subgoal):
 1. card (insert (Suc (a + b)) V) = Suc (card V) &&& card ({0..<m} \<inter> insert (Suc (a + b)) V) = (if m = Suc (Suc (a + b)) then Suc (card V) else card ({0..<m} \<inter> V))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
V \<subseteq> {0..<Suc (a + b)}
finite V
Suc (a + b) \<notin> V
{0..<Suc (Suc (a + b))} \<inter> V = V
m \<le> Suc (Suc (a + b))

goal (1 subgoal):
 1. card (insert (Suc (a + b)) V) = Suc (card V) &&& card ({0..<m} \<inter> insert (Suc (a + b)) V) = (if m = Suc (Suc (a + b)) then Suc (card V) else card ({0..<m} \<inter> V))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?m \<le> Suc (Suc (a + b)) \<Longrightarrow> card (insert (Suc (a + b)) V) = Suc (card V)
?m \<le> Suc (Suc (a + b)) \<Longrightarrow> card ({0..<?m} \<inter> insert (Suc (a + b)) V) = (if ?m = Suc (Suc (a + b)) then Suc (card V) else card ({0..<?m} \<inter> V))

goal (3 subgoals):
 1. \<And>x. x \<in> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<Longrightarrow> insert (Suc (a + b)) (x - {Suc (a + b)}) = x
 2. insert (Suc (a + b)) \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<rightarrow> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}
 3. \<And>x. x \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<Longrightarrow> insert (Suc (a + b)) x - {Suc (a + b)} = x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?V3 \<subseteq> {0..<Suc (a + b)}; ?m \<le> Suc (Suc (a + b))\<rbrakk> \<Longrightarrow> card (insert (Suc (a + b)) ?V3) = Suc (card ?V3)
\<lbrakk>?V3 \<subseteq> {0..<Suc (a + b)}; ?m \<le> Suc (Suc (a + b))\<rbrakk> \<Longrightarrow> card ({0..<?m} \<inter> insert (Suc (a + b)) ?V3) = (if ?m = Suc (Suc (a + b)) then Suc (card ?V3) else card ({0..<?m} \<inter> ?V3))

goal (3 subgoals):
 1. \<And>x. x \<in> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<Longrightarrow> insert (Suc (a + b)) (x - {Suc (a + b)}) = x
 2. insert (Suc (a + b)) \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<rightarrow> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}
 3. \<And>x. x \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<Longrightarrow> insert (Suc (a + b)) x - {Suc (a + b)} = x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?V3 \<subseteq> {0..<Suc (a + b)}; ?m \<le> Suc (Suc (a + b))\<rbrakk> \<Longrightarrow> card (insert (Suc (a + b)) ?V3) = Suc (card ?V3)
\<lbrakk>?V3 \<subseteq> {0..<Suc (a + b)}; ?m \<le> Suc (Suc (a + b))\<rbrakk> \<Longrightarrow> card ({0..<?m} \<inter> insert (Suc (a + b)) ?V3) = (if ?m = Suc (Suc (a + b)) then Suc (card ?V3) else card ({0..<?m} \<inter> ?V3))
[PROOF STEP]
show "insert ?l \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> ?Q V (a + Suc b)} \<rightarrow> ?V (\<lambda>V. ?l \<in> V)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?V3 \<subseteq> {0..<Suc (a + b)}; ?m \<le> Suc (Suc (a + b))\<rbrakk> \<Longrightarrow> card (insert (Suc (a + b)) ?V3) = Suc (card ?V3)
\<lbrakk>?V3 \<subseteq> {0..<Suc (a + b)}; ?m \<le> Suc (Suc (a + b))\<rbrakk> \<Longrightarrow> card ({0..<?m} \<inter> insert (Suc (a + b)) ?V3) = (if ?m = Suc (Suc (a + b)) then Suc (card ?V3) else card ({0..<?m} \<inter> ?V3))

goal (1 subgoal):
 1. insert (Suc (a + b)) \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<rightarrow> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}
[PROOF STEP]
using \<open>b < a\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?V3 \<subseteq> {0..<Suc (a + b)}; ?m \<le> Suc (Suc (a + b))\<rbrakk> \<Longrightarrow> card (insert (Suc (a + b)) ?V3) = Suc (card ?V3)
\<lbrakk>?V3 \<subseteq> {0..<Suc (a + b)}; ?m \<le> Suc (Suc (a + b))\<rbrakk> \<Longrightarrow> card ({0..<?m} \<inter> insert (Suc (a + b)) ?V3) = (if ?m = Suc (Suc (a + b)) then Suc (card ?V3) else card ({0..<?m} \<inter> ?V3))
b < a

goal (1 subgoal):
 1. insert (Suc (a + b)) \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<rightarrow> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert (Suc (a + b)) \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<rightarrow> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}

goal (2 subgoals):
 1. \<And>x. x \<in> {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<Longrightarrow> insert (Suc (a + b)) (x - {Suc (a + b)}) = x
 2. \<And>x. x \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> (\<forall>m\<in>{1..a + Suc b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} \<Longrightarrow> insert (Suc (a + b)) x - {Suc (a + b)} = x
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
card {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} = valid_countings a (Suc b)

goal (1 subgoal):
 1. valid_countings (Suc a) (Suc b) = valid_countings a (Suc b) + valid_countings (Suc a) b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<in> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} = valid_countings a (Suc b)

goal (1 subgoal):
 1. valid_countings (Suc a) (Suc b) = valid_countings a (Suc b) + valid_countings (Suc a) b
[PROOF STEP]
have "card (?V (\<lambda>V. ?l \<notin> V)) = valid_countings (Suc a) b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<notin> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} = valid_countings (Suc a) b
[PROOF STEP]
unfolding valid_countings_set
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<notin> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} = card {V \<in> Pow {0..<Suc a + b}. card V = Suc a \<and> (\<forall>m\<in>{1..Suc a + b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))}
[PROOF STEP]
proof (intro arg_cong[where f="\<lambda>P. card {x. P x}"] ext conj_cong)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. (x \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<notin> x) = (x \<in> Pow {0..<Suc a + b})
 2. \<And>x. x \<in> Pow {0..<Suc a + b} \<Longrightarrow> (card x = Suc a) = (card x = Suc a)
 3. \<And>x. \<lbrakk>x \<in> Pow {0..<Suc a + b}; card x = Suc a\<rbrakk> \<Longrightarrow> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> x) < card ({0..<m} \<inter> x)) = (\<forall>m\<in>{1..Suc a + b}. m - card ({0..<m} \<inter> x) < card ({0..<m} \<inter> x))
[PROOF STEP]
fix V
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. (x \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<notin> x) = (x \<in> Pow {0..<Suc a + b})
 2. \<And>x. x \<in> Pow {0..<Suc a + b} \<Longrightarrow> (card x = Suc a) = (card x = Suc a)
 3. \<And>x. \<lbrakk>x \<in> Pow {0..<Suc a + b}; card x = Suc a\<rbrakk> \<Longrightarrow> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> x) < card ({0..<m} \<inter> x)) = (\<forall>m\<in>{1..Suc a + b}. m - card ({0..<m} \<inter> x) < card ({0..<m} \<inter> x))
[PROOF STEP]
assume "V \<in> Pow {0..<Suc a + b}" and [simp]: "card V = Suc a"
[PROOF STATE]
proof (state)
this:
V \<in> Pow {0..<Suc a + b}
card V = Suc a

goal (3 subgoals):
 1. \<And>x. (x \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<notin> x) = (x \<in> Pow {0..<Suc a + b})
 2. \<And>x. x \<in> Pow {0..<Suc a + b} \<Longrightarrow> (card x = Suc a) = (card x = Suc a)
 3. \<And>x. \<lbrakk>x \<in> Pow {0..<Suc a + b}; card x = Suc a\<rbrakk> \<Longrightarrow> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> x) < card ({0..<m} \<inter> x)) = (\<forall>m\<in>{1..Suc a + b}. m - card ({0..<m} \<inter> x) < card ({0..<m} \<inter> x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
V \<in> Pow {0..<Suc a + b}
card V = Suc a
[PROOF STEP]
have [simp]: "V \<subseteq> {0..<Suc ?l}"
[PROOF STATE]
proof (prove)
using this:
V \<in> Pow {0..<Suc a + b}
card V = Suc a

goal (1 subgoal):
 1. V \<subseteq> {0..<Suc (Suc (a + b))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V \<subseteq> {0..<Suc (Suc (a + b))}

goal (3 subgoals):
 1. \<And>x. (x \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<notin> x) = (x \<in> Pow {0..<Suc a + b})
 2. \<And>x. x \<in> Pow {0..<Suc a + b} \<Longrightarrow> (card x = Suc a) = (card x = Suc a)
 3. \<And>x. \<lbrakk>x \<in> Pow {0..<Suc a + b}; card x = Suc a\<rbrakk> \<Longrightarrow> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> x) < card ({0..<m} \<inter> x)) = (\<forall>m\<in>{1..Suc a + b}. m - card ({0..<m} \<inter> x) < card ({0..<m} \<inter> x))
[PROOF STEP]
show "?Q V (Suc ?l) = ?Q V (Suc a + b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V)) = (\<forall>m\<in>{1..Suc a + b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))
[PROOF STEP]
using \<open>b<a\<close>
[PROOF STATE]
proof (prove)
using this:
b < a

goal (1 subgoal):
 1. (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V)) = (\<forall>m\<in>{1..Suc a + b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))
[PROOF STEP]
by (simp add: Int_absorb1 Icc_Suc2)
[PROOF STATE]
proof (state)
this:
(\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V)) = (\<forall>m\<in>{1..Suc a + b}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))

goal (2 subgoals):
 1. \<And>x. (x \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<notin> x) = (x \<in> Pow {0..<Suc a + b})
 2. \<And>x. x \<in> Pow {0..<Suc a + b} \<Longrightarrow> (card x = Suc a) = (card x = Suc a)
[PROOF STEP]
qed (auto simp: subset_eq less_Suc_eq)
[PROOF STATE]
proof (state)
this:
card {V. (V \<in> Pow {0..<Suc (Suc (a + b))} \<and> Suc (a + b) \<notin> V) \<and> card V = Suc a \<and> (\<forall>m\<in>{1..Suc (Suc (a + b))}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V))} = valid_countings (Suc a) b

goal (1 subgoal):
 1. valid_countings (Suc a) (Suc b) = valid_countings a (Suc b) + valid_countings (Suc a) b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
valid_countings (Suc a) (Suc b) = valid_countings (Suc a) b + valid_countings a (Suc b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
valid_countings (Suc a) (Suc b) = valid_countings (Suc a) b + valid_countings a (Suc b)

goal (1 subgoal):
 1. valid_countings (Suc a) (Suc b) = valid_countings a (Suc b) + valid_countings (Suc a) b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
valid_countings (Suc a) (Suc b) = valid_countings a (Suc b) + valid_countings (Suc a) b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nth_default_beyond:
  "length xs \<le> n \<Longrightarrow> nth_default dflt xs n = dflt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs \<le> n \<Longrightarrow> nth_default dflt xs n = dflt
[PROOF STEP]
by (simp add: nth_default_def)


[STATEMENT]
lemma concat_injective: "concat xs = concat ys \<Longrightarrow> length xs = length ys \<Longrightarrow> \<forall>(x, y) \<in> set (zip xs ys). length x = length y \<Longrightarrow> xs = ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>concat xs = concat ys; length xs = length ys; \<forall>(x, y)\<in>set (zip xs ys). length x = length y\<rbrakk> \<Longrightarrow> xs = ys
[PROOF STEP]
by (simp add: concat_eq_concat_iff)


[STATEMENT]
lemma Cons_eq_filterD:
  "x#xs = filter P ys \<Longrightarrow>
  \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
  (is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x # xs = filter P ys \<Longrightarrow> \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
proof(induct ys)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x # xs = filter P [] \<Longrightarrow> \<exists>us vs. [] = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
 2. \<And>a ys. \<lbrakk>x # xs = filter P ys \<Longrightarrow> \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs; x # xs = filter P (a # ys)\<rbrakk> \<Longrightarrow> \<exists>us vs. a # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
x # xs = filter P []

goal (2 subgoals):
 1. x # xs = filter P [] \<Longrightarrow> \<exists>us vs. [] = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
 2. \<And>a ys. \<lbrakk>x # xs = filter P ys \<Longrightarrow> \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs; x # xs = filter P (a # ys)\<rbrakk> \<Longrightarrow> \<exists>us vs. a # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
x # xs = filter P []

goal (1 subgoal):
 1. \<exists>us vs. [] = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>us vs. [] = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs

goal (1 subgoal):
 1. \<And>a ys. \<lbrakk>x # xs = filter P ys \<Longrightarrow> \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs; x # xs = filter P (a # ys)\<rbrakk> \<Longrightarrow> \<exists>us vs. a # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ys. \<lbrakk>x # xs = filter P ys \<Longrightarrow> \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs; x # xs = filter P (a # ys)\<rbrakk> \<Longrightarrow> \<exists>us vs. a # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
case (Cons y ys)
[PROOF STATE]
proof (state)
this:
x # xs = filter P ys \<Longrightarrow> \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
x # xs = filter P (y # ys)

goal (1 subgoal):
 1. \<And>a ys. \<lbrakk>x # xs = filter P ys \<Longrightarrow> \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs; x # xs = filter P (a # ys)\<rbrakk> \<Longrightarrow> \<exists>us vs. a # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
show ?case (is "\<exists>x. ?Q x")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
 2. \<not> ?P \<Longrightarrow> \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
assume Py: "P y"
[PROOF STATE]
proof (state)
this:
P y

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
 2. \<not> ?P \<Longrightarrow> \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
 2. \<not> ?P \<Longrightarrow> \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
assume "x = y"
[PROOF STATE]
proof (state)
this:
x = y

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
 2. \<not> ?P \<Longrightarrow> \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
with Py Cons.prems
[PROOF STATE]
proof (chain)
picking this:
P y
x # xs = filter P (y # ys)
x = y
[PROOF STEP]
have "?Q []"
[PROOF STATE]
proof (prove)
using this:
P y
x # xs = filter P (y # ys)
x = y

goal (1 subgoal):
 1. \<exists>vs. y # ys = [] @ x # vs \<and> (\<forall>u\<in>set []. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>vs. y # ys = [] @ x # vs \<and> (\<forall>u\<in>set []. \<not> P u) \<and> P x \<and> xs = filter P vs

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
 2. \<not> ?P \<Longrightarrow> \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>vs. y # ys = [] @ x # vs \<and> (\<forall>u\<in>set []. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>vs. y # ys = [] @ x # vs \<and> (\<forall>u\<in>set []. \<not> P u) \<and> P x \<and> xs = filter P vs

goal (1 subgoal):
 1. \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
assume "x \<noteq> y"
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
with Py Cons.prems
[PROOF STATE]
proof (chain)
picking this:
P y
x # xs = filter P (y # ys)
x \<noteq> y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P y
x # xs = filter P (y # ys)
x \<noteq> y

goal (1 subgoal):
 1. \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs

goal (1 subgoal):
 1. \<not> P y \<Longrightarrow> \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> P y \<Longrightarrow> \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
assume "\<not> P y"
[PROOF STATE]
proof (state)
this:
\<not> P y

goal (1 subgoal):
 1. \<not> P y \<Longrightarrow> \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
with Cons
[PROOF STATE]
proof (chain)
picking this:
x # xs = filter P ys \<Longrightarrow> \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
x # xs = filter P (y # ys)
\<not> P y
[PROOF STEP]
obtain us vs where "?P (y#ys) (y#us) vs"
[PROOF STATE]
proof (prove)
using this:
x # xs = filter P ys \<Longrightarrow> \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
x # xs = filter P (y # ys)
\<not> P y

goal (1 subgoal):
 1. (\<And>us vs. y # ys = (y # us) @ x # vs \<and> (\<forall>u\<in>set (y # us). \<not> P u) \<and> P x \<and> xs = filter P vs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
y # ys = (y # us) @ x # vs \<and> (\<forall>u\<in>set (y # us). \<not> P u) \<and> P x \<and> xs = filter P vs

goal (1 subgoal):
 1. \<not> P y \<Longrightarrow> \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y # ys = (y # us) @ x # vs \<and> (\<forall>u\<in>set (y # us). \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
have "?Q (y#us)"
[PROOF STATE]
proof (prove)
using this:
y # ys = (y # us) @ x # vs \<and> (\<forall>u\<in>set (y # us). \<not> P u) \<and> P x \<and> xs = filter P vs

goal (1 subgoal):
 1. \<exists>vs. y # ys = (y # us) @ x # vs \<and> (\<forall>u\<in>set (y # us). \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>vs. y # ys = (y # us) @ x # vs \<and> (\<forall>u\<in>set (y # us). \<not> P u) \<and> P x \<and> xs = filter P vs

goal (1 subgoal):
 1. \<not> P y \<Longrightarrow> \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>vs. y # ys = (y # us) @ x # vs \<and> (\<forall>u\<in>set (y # us). \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>vs. y # ys = (y # us) @ x # vs \<and> (\<forall>u\<in>set (y # us). \<not> P u) \<and> P x \<and> xs = filter P vs

goal (1 subgoal):
 1. \<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>us vs. y # ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_in_set_insert [simp]:
  "x \<notin> set xs \<Longrightarrow> List.insert x xs = x # xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> set xs \<Longrightarrow> List.insert x xs = x # xs
[PROOF STEP]
by (simp add: List.insert_def)


[STATEMENT]
lemma sorted_wrt2: "transp P \<Longrightarrow> sorted_wrt P (x # y # zs) = (P x y \<and> sorted_wrt P (y # zs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transp P \<Longrightarrow> sorted_wrt P (x # y # zs) = (P x y \<and> sorted_wrt P (y # zs))
[PROOF STEP]
proof (induction zs arbitrary: x y)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. transp P \<Longrightarrow> sorted_wrt P [x, y] = (P x y \<and> sorted_wrt P [y])
 2. \<And>a zs x y. \<lbrakk>\<And>x y. transp P \<Longrightarrow> sorted_wrt P (x # y # zs) = (P x y \<and> sorted_wrt P (y # zs)); transp P\<rbrakk> \<Longrightarrow> sorted_wrt P (x # y # a # zs) = (P x y \<and> sorted_wrt P (y # a # zs))
[PROOF STEP]
case (Cons z zs)
[PROOF STATE]
proof (state)
this:
transp P \<Longrightarrow> sorted_wrt P (?x # ?y # zs) = (P ?x ?y \<and> sorted_wrt P (?y # zs))
transp P

goal (2 subgoals):
 1. \<And>x y. transp P \<Longrightarrow> sorted_wrt P [x, y] = (P x y \<and> sorted_wrt P [y])
 2. \<And>a zs x y. \<lbrakk>\<And>x y. transp P \<Longrightarrow> sorted_wrt P (x # y # zs) = (P x y \<and> sorted_wrt P (y # zs)); transp P\<rbrakk> \<Longrightarrow> sorted_wrt P (x # y # a # zs) = (P x y \<and> sorted_wrt P (y # a # zs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
transp P \<Longrightarrow> sorted_wrt P (?x # ?y # zs) = (P ?x ?y \<and> sorted_wrt P (?y # zs))
transp P
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
transp P \<Longrightarrow> sorted_wrt P (?x # ?y # zs) = (P ?x ?y \<and> sorted_wrt P (?y # zs))
transp P

goal (1 subgoal):
 1. sorted_wrt P (x # y # z # zs) = (P x y \<and> sorted_wrt P (y # z # zs))
[PROOF STEP]
by simp (meson transpD)+
[PROOF STATE]
proof (state)
this:
sorted_wrt P (x # y # z # zs) = (P x y \<and> sorted_wrt P (y # z # zs))

goal (1 subgoal):
 1. \<And>x y. transp P \<Longrightarrow> sorted_wrt P [x, y] = (P x y \<and> sorted_wrt P [y])
[PROOF STEP]
qed auto


[STATEMENT]
lemma UNIV_coset [code]:
  "UNIV = List.coset []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV = List.coset []
[PROOF STEP]
by simp


[STATEMENT]
lemma multp\<^sub>D\<^sub>M_imp_multp:
  "multp\<^sub>D\<^sub>M r M N \<Longrightarrow> multp r M N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multp\<^sub>D\<^sub>M r M N \<Longrightarrow> multp r M N
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. multp\<^sub>D\<^sub>M r M N \<Longrightarrow> multp r M N
[PROOF STEP]
assume "multp\<^sub>D\<^sub>M r M N"
[PROOF STATE]
proof (state)
this:
multp\<^sub>D\<^sub>M r M N

goal (1 subgoal):
 1. multp\<^sub>D\<^sub>M r M N \<Longrightarrow> multp r M N
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
multp\<^sub>D\<^sub>M r M N
[PROOF STEP]
obtain X Y where
    "X \<noteq> {#}" and "X \<subseteq># N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)"
[PROOF STATE]
proof (prove)
using this:
multp\<^sub>D\<^sub>M r M N

goal (1 subgoal):
 1. (\<And>X Y. \<lbrakk>X \<noteq> {#}; X \<subseteq># N; M = N - X + Y; \<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding multp\<^sub>D\<^sub>M_def
[PROOF STATE]
proof (prove)
using this:
\<exists>X Y. X \<noteq> {#} \<and> X \<subseteq># N \<and> M = N - X + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a))

goal (1 subgoal):
 1. (\<And>X Y. \<lbrakk>X \<noteq> {#}; X \<subseteq># N; M = N - X + Y; \<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
X \<noteq> {#}
X \<subseteq># N
M = N - X + Y
\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)

goal (1 subgoal):
 1. multp\<^sub>D\<^sub>M r M N \<Longrightarrow> multp r M N
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X \<noteq> {#}
X \<subseteq># N
M = N - X + Y
\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)
[PROOF STEP]
have "multp r (N - X + Y) (N - X + X)"
[PROOF STATE]
proof (prove)
using this:
X \<noteq> {#}
X \<subseteq># N
M = N - X + Y
\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)

goal (1 subgoal):
 1. multp r (N - X + Y) (N - X + X)
[PROOF STEP]
by (intro one_step_implies_multp) (auto simp: Bex_def trans_def)
[PROOF STATE]
proof (state)
this:
multp r (N - X + Y) (N - X + X)

goal (1 subgoal):
 1. multp\<^sub>D\<^sub>M r M N \<Longrightarrow> multp r M N
[PROOF STEP]
with \<open>M = N - X + Y\<close> \<open>X \<subseteq># N\<close>
[PROOF STATE]
proof (chain)
picking this:
M = N - X + Y
X \<subseteq># N
multp r (N - X + Y) (N - X + X)
[PROOF STEP]
show "multp r M N"
[PROOF STATE]
proof (prove)
using this:
M = N - X + Y
X \<subseteq># N
multp r (N - X + Y) (N - X + X)

goal (1 subgoal):
 1. multp r M N
[PROOF STEP]
by (metis subset_mset.diff_add)
[PROOF STATE]
proof (state)
this:
multp r M N

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma order_mult: "class.order
  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)
  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
  (is "class.order ?le ?less")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.order (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N) (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. class.order (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N) (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})
[PROOF STEP]
have irrefl: "\<And>M :: 'a multiset. \<not> ?less M M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M. (M, M) \<notin> mult {(x, y). x < y}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M. (M, M) \<in> mult {(x, y). x < y} \<Longrightarrow> False
[PROOF STEP]
fix M :: "'a multiset"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M. (M, M) \<in> mult {(x, y). x < y} \<Longrightarrow> False
[PROOF STEP]
have "trans {(x'::'a, x). x' < x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans {(x, y). x < y}
[PROOF STEP]
by (rule transI) (blast intro: less_trans)
[PROOF STATE]
proof (state)
this:
trans {(x, y). x < y}

goal (1 subgoal):
 1. \<And>M. (M, M) \<in> mult {(x, y). x < y} \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
trans {(x, y). x < y}

goal (1 subgoal):
 1. \<And>M. (M, M) \<in> mult {(x, y). x < y} \<Longrightarrow> False
[PROOF STEP]
assume "(M, M) \<in> mult {(x, y). x < y}"
[PROOF STATE]
proof (state)
this:
(M, M) \<in> mult {(x, y). x < y}

goal (1 subgoal):
 1. \<And>M. (M, M) \<in> mult {(x, y). x < y} \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
trans {(x, y). x < y}
(M, M) \<in> mult {(x, y). x < y}
[PROOF STEP]
have "\<exists>I J K. M = I + J \<and> M = I + K
      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
[PROOF STATE]
proof (prove)
using this:
trans {(x, y). x < y}
(M, M) \<in> mult {(x, y). x < y}

goal (1 subgoal):
 1. \<exists>I J K. M = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>#K. \<exists>j\<in>#J. (k, j) \<in> {(x, y). x < y})
[PROOF STEP]
by (rule mult_implies_one_step)
[PROOF STATE]
proof (state)
this:
\<exists>I J K. M = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>#K. \<exists>j\<in>#J. (k, j) \<in> {(x, y). x < y})

goal (1 subgoal):
 1. \<And>M. (M, M) \<in> mult {(x, y). x < y} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>I J K. M = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>#K. \<exists>j\<in>#J. (k, j) \<in> {(x, y). x < y})
[PROOF STEP]
obtain I J K where "M = I + J" and "M = I + K"
      and "J \<noteq> {#}" and "(\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
[PROOF STATE]
proof (prove)
using this:
\<exists>I J K. M = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>#K. \<exists>j\<in>#J. (k, j) \<in> {(x, y). x < y})

goal (1 subgoal):
 1. (\<And>I J K. \<lbrakk>M = I + J; M = I + K; J \<noteq> {#}; \<forall>k\<in>#K. \<exists>j\<in>#J. (k, j) \<in> {(x, y). x < y}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
M = I + J
M = I + K
J \<noteq> {#}
\<forall>k\<in>#K. \<exists>j\<in>#J. (k, j) \<in> {(x, y). x < y}

goal (1 subgoal):
 1. \<And>M. (M, M) \<in> mult {(x, y). x < y} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
M = I + J
M = I + K
J \<noteq> {#}
\<forall>k\<in>#K. \<exists>j\<in>#J. (k, j) \<in> {(x, y). x < y}
[PROOF STEP]
have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j"
[PROOF STATE]
proof (prove)
using this:
M = I + J
M = I + K
J \<noteq> {#}
\<forall>k\<in>#K. \<exists>j\<in>#J. (k, j) \<in> {(x, y). x < y}

goal (1 subgoal):
 1. K \<noteq> {#} &&& \<forall>k\<in>#K. \<exists>j\<in>#K. k < j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
K \<noteq> {#}
\<forall>k\<in>#K. \<exists>j\<in>#K. k < j

goal (1 subgoal):
 1. \<And>M. (M, M) \<in> mult {(x, y). x < y} \<Longrightarrow> False
[PROOF STEP]
have "finite (set_mset K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set_mset K)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (set_mset K)

goal (1 subgoal):
 1. \<And>M. (M, M) \<in> mult {(x, y). x < y} \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (set_mset K)

goal (1 subgoal):
 1. \<And>M. (M, M) \<in> mult {(x, y). x < y} \<Longrightarrow> False
[PROOF STEP]
note aux2
[PROOF STATE]
proof (state)
this:
\<forall>k\<in>#K. \<exists>j\<in>#K. k < j

goal (1 subgoal):
 1. \<And>M. (M, M) \<in> mult {(x, y). x < y} \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (set_mset K)
\<forall>k\<in>#K. \<exists>j\<in>#K. k < j
[PROOF STEP]
have "set_mset K = {}"
[PROOF STATE]
proof (prove)
using this:
finite (set_mset K)
\<forall>k\<in>#K. \<exists>j\<in>#K. k < j

goal (1 subgoal):
 1. set_mset K = {}
[PROOF STEP]
by (induct rule: finite_induct)
       (simp, metis (mono_tags) insert_absorb insert_iff insert_not_empty less_irrefl less_trans)
[PROOF STATE]
proof (state)
this:
set_mset K = {}

goal (1 subgoal):
 1. \<And>M. (M, M) \<in> mult {(x, y). x < y} \<Longrightarrow> False
[PROOF STEP]
with aux1
[PROOF STATE]
proof (chain)
picking this:
K \<noteq> {#}
set_mset K = {}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
K \<noteq> {#}
set_mset K = {}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(?M, ?M) \<notin> mult {(x, y). x < y}

goal (1 subgoal):
 1. class.order (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N) (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})
[PROOF STEP]
have trans: "\<And>K M N :: 'a multiset. ?less K M \<Longrightarrow> ?less M N \<Longrightarrow> ?less K N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>K M N. \<lbrakk>(K, M) \<in> mult {(x, y). x < y}; (M, N) \<in> mult {(x, y). x < y}\<rbrakk> \<Longrightarrow> (K, N) \<in> mult {(x, y). x < y}
[PROOF STEP]
unfolding mult_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>K M N. \<lbrakk>(K, M) \<in> (mult1 {(x, y). x < y})\<^sup>+; (M, N) \<in> (mult1 {(x, y). x < y})\<^sup>+\<rbrakk> \<Longrightarrow> (K, N) \<in> (mult1 {(x, y). x < y})\<^sup>+
[PROOF STEP]
by (blast intro: trancl_trans)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?K, ?M) \<in> mult {(x, y). x < y}; (?M, ?N) \<in> mult {(x, y). x < y}\<rbrakk> \<Longrightarrow> (?K, ?N) \<in> mult {(x, y). x < y}

goal (1 subgoal):
 1. class.order (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N) (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})
[PROOF STEP]
show "class.order ?le ?less"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.order (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N) (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})
[PROOF STEP]
by standard (auto simp add: less_eq_multiset_def irrefl dest: trans)
[PROOF STATE]
proof (state)
this:
class.order (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N) (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma measurable_sum_nat [measurable (raw)]:
  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> nat"
  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> measurable M (count_space UNIV)"
  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> measurable M (count_space UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<Sum>i\<in>S. f i x) \<in> M \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<lambda>x. \<Sum>i\<in>S. f i x) \<in> M \<rightarrow>\<^sub>M count_space UNIV
 2. \<not> ?P \<Longrightarrow> (\<lambda>x. \<Sum>i\<in>S. f i x) \<in> M \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
assume "finite S"
[PROOF STATE]
proof (state)
this:
finite S

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<lambda>x. \<Sum>i\<in>S. f i x) \<in> M \<rightarrow>\<^sub>M count_space UNIV
 2. \<not> ?P \<Longrightarrow> (\<lambda>x. \<Sum>i\<in>S. f i x) \<in> M \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite S

goal (1 subgoal):
 1. (\<lambda>x. \<Sum>i\<in>S. f i x) \<in> M \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite S
?i \<in> S \<Longrightarrow> f ?i \<in> M \<rightarrow>\<^sub>M count_space UNIV

goal (1 subgoal):
 1. (\<lambda>x. \<Sum>i\<in>S. f i x) \<in> M \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
by induct auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> M \<rightarrow>\<^sub>M count_space UNIV

goal (1 subgoal):
 1. infinite S \<Longrightarrow> (\<lambda>x. \<Sum>i\<in>S. f i x) \<in> M \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
qed simp


[STATEMENT]
lemma ins_rbt_sorted[simp]: "rbt_sorted t \<Longrightarrow> rbt_sorted (rbt_ins f k x t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t \<Longrightarrow> rbt_sorted (rbt_ins f k x t)
[PROOF STEP]
by (induct f k x t rule: rbt_ins.induct) (auto simp: balance_rbt_sorted)


[STATEMENT]
lemma rbt_lookup_ins:
  fixes k :: "'a"
  assumes "rbt_sorted t"
  shows "rbt_lookup (rbt_ins f k v t) x = ((rbt_lookup t)(k |-> case rbt_lookup t k of None \<Rightarrow> v
                                                                | Some w \<Rightarrow> f k w v)) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_lookup (rbt_ins f k v t) x = (rbt_lookup t(k \<mapsto> case rbt_lookup t k of None \<Rightarrow> v | Some w \<Rightarrow> f k w v)) x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rbt_sorted t

goal (1 subgoal):
 1. rbt_lookup (rbt_ins f k v t) x = (rbt_lookup t(k \<mapsto> case rbt_lookup t k of None \<Rightarrow> v | Some w \<Rightarrow> f k w v)) x
[PROOF STEP]
by (induct f k v t rule: rbt_ins.induct) auto


[STATEMENT]
lemma rbt_bheight_rbt_baliL: "bheight l = bheight r \<Longrightarrow> bheight (rbt_baliL l a b r) = Suc (bheight l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bheight l = bheight r \<Longrightarrow> bheight (rbt_baliL l a b r) = Suc (bheight l)
[PROOF STEP]
by (induct l a b r rule: rbt_baliL.induct) auto


[STATEMENT]
lemma iso_tuple_update_compose_snd_snd:
  "h f \<circ> j g = k (f \<circ> g) \<Longrightarrow>
    (iso_tuple_snd_update isom \<circ> h) f \<circ> (iso_tuple_snd_update isom \<circ> j) g =
      (iso_tuple_snd_update isom \<circ> k) (f \<circ> g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h f \<circ> j g = k (f \<circ> g) \<Longrightarrow> (iso_tuple_snd_update isom \<circ> h) f \<circ> (iso_tuple_snd_update isom \<circ> j) g = (iso_tuple_snd_update isom \<circ> k) (f \<circ> g)
[PROOF STEP]
by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose fun_eq_iff)


[STATEMENT]
lemma dense_repr_replicate_zero: "dense_repr ((replicate n \<zero>) @ p) = dense_repr p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dense_repr (replicate n \<zero> @ p) = dense_repr p
[PROOF STEP]
by (induction n) (auto)


[STATEMENT]
theorem (in ring_hom_ring) FactRing_iso_set:
  assumes "h ` carrier R = carrier S"
  shows "(\<lambda>X. the_elem (h ` X)) \<in> ring_iso (R Quot (a_kernel R S h)) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>X. the_elem (h ` X)) \<in> ring_iso (R Quot a_kernel R S h) S
[PROOF STEP]
using FactRing_iso_set_aux assms
[PROOF STATE]
proof (prove)
using this:
(\<lambda>X. the_elem (h ` X)) \<in> ring_iso (R Quot a_kernel R S h) (S\<lparr>carrier := h ` carrier R\<rparr>)
h ` carrier R = carrier S

goal (1 subgoal):
 1. (\<lambda>X. the_elem (h ` X)) \<in> ring_iso (R Quot a_kernel R S h) S
[PROOF STEP]
by auto


[STATEMENT]
lemma items_the_value:
  assumes "sorted (List.map fst xs)" and "distinct (List.map fst xs)" and "0 \<notin> snd ` set xs"
  shows "items (the_value xs) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. items (the_value xs) = xs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. items (the_value xs) = xs
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
sorted (list.map fst xs)
distinct (list.map fst xs)
(0::'b) \<notin> snd ` set xs
[PROOF STEP]
have "sorted_list_of_set (set (List.map fst xs)) = List.map fst xs"
[PROOF STATE]
proof (prove)
using this:
sorted (list.map fst xs)
distinct (list.map fst xs)
(0::'b) \<notin> snd ` set xs

goal (1 subgoal):
 1. sorted_list_of_set (set (list.map fst xs)) = list.map fst xs
[PROOF STEP]
unfolding sorted_list_of_set_sort_remdups
[PROOF STATE]
proof (prove)
using this:
sorted (list.map fst xs)
distinct (list.map fst xs)
(0::'b) \<notin> snd ` set xs

goal (1 subgoal):
 1. sort (remdups (list.map fst xs)) = list.map fst xs
[PROOF STEP]
by (simp add: distinct_remdups_id sorted_sort_id)
[PROOF STATE]
proof (state)
this:
sorted_list_of_set (set (list.map fst xs)) = list.map fst xs

goal (1 subgoal):
 1. items (the_value xs) = xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sorted_list_of_set (set (list.map fst xs)) = list.map fst xs

goal (1 subgoal):
 1. items (the_value xs) = xs
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
sorted (list.map fst xs)
distinct (list.map fst xs)
(0::'b) \<notin> snd ` set xs
[PROOF STEP]
have "keys (the_value xs) = fst ` set xs"
[PROOF STATE]
proof (prove)
using this:
sorted (list.map fst xs)
distinct (list.map fst xs)
(0::'b) \<notin> snd ` set xs

goal (1 subgoal):
 1. keys (the_value xs) = fst ` set xs
[PROOF STEP]
by transfer (auto simp add: image_def split: option.split dest: set_map_of_compr)
[PROOF STATE]
proof (state)
this:
keys (the_value xs) = fst ` set xs

goal (1 subgoal):
 1. items (the_value xs) = xs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sorted_list_of_set (set (list.map fst xs)) = list.map fst xs
keys (the_value xs) = fst ` set xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sorted_list_of_set (set (list.map fst xs)) = list.map fst xs
keys (the_value xs) = fst ` set xs

goal (1 subgoal):
 1. items (the_value xs) = xs
[PROOF STEP]
unfolding items_def
[PROOF STATE]
proof (prove)
using this:
sorted_list_of_set (set (list.map fst xs)) = list.map fst xs
keys (the_value xs) = fst ` set xs

goal (1 subgoal):
 1. list.map (\<lambda>k. (k, lookup (the_value xs) k)) (sorted_list_of_set (keys (the_value xs))) = xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sorted_list_of_set (set (list.map fst xs)) = list.map fst xs
keys (the_value xs) = fst ` set xs
sorted (list.map fst xs)
distinct (list.map fst xs)
(0::'b) \<notin> snd ` set xs

goal (1 subgoal):
 1. list.map (\<lambda>k. (k, lookup (the_value xs) k)) (sorted_list_of_set (keys (the_value xs))) = xs
[PROOF STEP]
by (auto simp add: lookup_the_value intro: map_idI)
[PROOF STATE]
proof (state)
this:
items (the_value xs) = xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
nitpick [expect = none]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "(x::nat) - y + y = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x - y + y = x
[PROOF STEP]
nitpick [expect = genuine]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x - y + y = x
[PROOF STEP]
oops


[STATEMENT]
lemma "rec_X a b c d e f (B x) = b x (rec_X a b c d e f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_X a b c d e f (X.B x) = b x (rec_X a b c d e f x)
[PROOF STEP]
nitpick [card = 1-5, expect = none]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_X a b c d e f (X.B x) = b x (rec_X a b c d e f x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma smallo_powr:
  fixes f :: "'a \<Rightarrow> real"
  assumes "f \<in> o[F](g)" "p > 0"
  shows   "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> o[F](\<lambda>x. \<bar>g x\<bar> powr p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<bar>f x\<bar> powr p) \<in> o[F](\<lambda>x. \<bar>g x\<bar> powr p)
[PROOF STEP]
proof (rule landau_o.smallI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. 0 < c \<Longrightarrow> \<forall>\<^sub>F x in F. norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)
[PROOF STEP]
fix c :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. 0 < c \<Longrightarrow> \<forall>\<^sub>F x in F. norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)
[PROOF STEP]
assume c: "c > 0"
[PROOF STATE]
proof (state)
this:
0 < c

goal (1 subgoal):
 1. \<And>c. 0 < c \<Longrightarrow> \<forall>\<^sub>F x in F. norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)
[PROOF STEP]
hence "c powr (1/p) > 0"
[PROOF STATE]
proof (prove)
using this:
0 < c

goal (1 subgoal):
 1. 0 < c powr (1 / p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < c powr (1 / p)

goal (1 subgoal):
 1. \<And>c. 0 < c \<Longrightarrow> \<forall>\<^sub>F x in F. norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)
[PROOF STEP]
from landau_o.smallD[OF assms(1) this]
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F x in F. norm (f x) \<le> c powr (1 / p) * norm (g x)
[PROOF STEP]
show "eventually (\<lambda>x. norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)) F"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in F. norm (f x) \<le> c powr (1 / p) * norm (g x)

goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)
[PROOF STEP]
proof eventually_elim
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. norm (f x) \<le> c powr (1 / p) * norm (g x) \<Longrightarrow> norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. norm (f x) \<le> c powr (1 / p) * norm (g x) \<Longrightarrow> norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)
[PROOF STEP]
assume "(norm (f x)) \<le> c powr (1 / p) * (norm (g x))"
[PROOF STATE]
proof (state)
this:
norm (f x) \<le> c powr (1 / p) * norm (g x)

goal (1 subgoal):
 1. \<And>x. norm (f x) \<le> c powr (1 / p) * norm (g x) \<Longrightarrow> norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
0 < p
norm (f x) \<le> c powr (1 / p) * norm (g x)
[PROOF STEP]
have "(norm (f x)) powr p \<le> (c powr (1 / p) * (norm (g x))) powr p"
[PROOF STATE]
proof (prove)
using this:
0 < p
norm (f x) \<le> c powr (1 / p) * norm (g x)

goal (1 subgoal):
 1. norm (f x) powr p \<le> (c powr (1 / p) * norm (g x)) powr p
[PROOF STEP]
by (intro powr_mono2) simp_all
[PROOF STATE]
proof (state)
this:
norm (f x) powr p \<le> (c powr (1 / p) * norm (g x)) powr p

goal (1 subgoal):
 1. \<And>x. norm (f x) \<le> c powr (1 / p) * norm (g x) \<Longrightarrow> norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (f x) powr p \<le> (c powr (1 / p) * norm (g x)) powr p

goal (1 subgoal):
 1. \<And>x. norm (f x) \<le> c powr (1 / p) * norm (g x) \<Longrightarrow> norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)
[PROOF STEP]
from assms(2) c
[PROOF STATE]
proof (chain)
picking this:
0 < p
0 < c
[PROOF STEP]
have "... = c * (norm (g x)) powr p"
[PROOF STATE]
proof (prove)
using this:
0 < p
0 < c

goal (1 subgoal):
 1. (c powr (1 / p) * norm (g x)) powr p = c * norm (g x) powr p
[PROOF STEP]
by (simp add: field_simps powr_mult powr_powr)
[PROOF STATE]
proof (state)
this:
(c powr (1 / p) * norm (g x)) powr p = c * norm (g x) powr p

goal (1 subgoal):
 1. \<And>x. norm (f x) \<le> c powr (1 / p) * norm (g x) \<Longrightarrow> norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
norm (f x) powr p \<le> c * norm (g x) powr p
[PROOF STEP]
show "norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)"
[PROOF STATE]
proof (prove)
using this:
norm (f x) powr p \<le> c * norm (g x) powr p

goal (1 subgoal):
 1. norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in F. norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma asymp_equiv_abs_real [asymp_equiv_intros]:
  fixes f g :: "'a \<Rightarrow> real"
  assumes "f \<sim>[F] g"
  shows   "(\<lambda>x. \<bar>f x\<bar>) \<sim>[F] (\<lambda>x. \<bar>g x\<bar>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<bar>f x\<bar>) \<sim>[F] (\<lambda>x. \<bar>g x\<bar>)
[PROOF STEP]
using tendsto_rabs[OF asymp_equivD[OF assms]]
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. \<bar>if f x = 0 \<and> g x = 0 then 1 else f x / g x\<bar>) \<longlongrightarrow> \<bar>1\<bar>) F

goal (1 subgoal):
 1. (\<lambda>x. \<bar>f x\<bar>) \<sim>[F] (\<lambda>x. \<bar>g x\<bar>)
[PROOF STEP]
by (simp add: if_distrib asymp_equiv_def cong: if_cong)


[STATEMENT]
lemma card_calM: "card calM = (p^a) * m choose p^a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card calM = p ^ a * m choose p ^ a
[PROOF STEP]
by (simp add: calM_def n_subsets order_G [symmetric] order_def)


[STATEMENT]
lemma homotopic_points_eq_path_component:
   "homotopic_loops S (linepath a a) (linepath b b) \<longleftrightarrow> path_component S a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. homotopic_loops S (linepath a a) (linepath b b) = path_component S a b
[PROOF STEP]
by (auto simp: path_component_imp_homotopic_points
         dest: homotopic_loops_imp_path_component_value [where t=1])


[STATEMENT]
lemma image_mset_strict_mono:
  assumes
    mono_f: "\<forall>x \<in> set_mset M. \<forall>y \<in> set_mset N. x < y \<longrightarrow> f x < f y" and
    less: "M < N"
  shows "image_mset f M < image_mset f N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. image_mset f M < image_mset f N
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. image_mset f M < image_mset f N
[PROOF STEP]
obtain Y X where
    y_nemp: "Y \<noteq> {#}" and y_sub_N: "Y \<subseteq># N" and M_eq: "M = N - Y + X" and
    ex_y: "\<forall>x. x \<in># X \<longrightarrow> (\<exists>y. y \<in># Y \<and> x < y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Y X. \<lbrakk>Y \<noteq> {#}; Y \<subseteq># N; M = N - Y + X; \<forall>x. x \<in># X \<longrightarrow> (\<exists>y. y \<in># Y \<and> x < y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using less[unfolded less_multiset\<^sub>D\<^sub>M]
[PROOF STATE]
proof (prove)
using this:
\<exists>X Y. X \<noteq> {#} \<and> X \<subseteq># N \<and> M = N - X + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a))

goal (1 subgoal):
 1. (\<And>Y X. \<lbrakk>Y \<noteq> {#}; Y \<subseteq># N; M = N - Y + X; \<forall>x. x \<in># X \<longrightarrow> (\<exists>y. y \<in># Y \<and> x < y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Y \<noteq> {#}
Y \<subseteq># N
M = N - Y + X
\<forall>x. x \<in># X \<longrightarrow> (\<exists>y. y \<in># Y \<and> x < y)

goal (1 subgoal):
 1. image_mset f M < image_mset f N
[PROOF STEP]
have x_sub_M: "X \<subseteq># M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<subseteq># M
[PROOF STEP]
using M_eq
[PROOF STATE]
proof (prove)
using this:
M = N - Y + X

goal (1 subgoal):
 1. X \<subseteq># M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
X \<subseteq># M

goal (1 subgoal):
 1. image_mset f M < image_mset f N
[PROOF STEP]
let ?fY = "image_mset f Y"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. image_mset f M < image_mset f N
[PROOF STEP]
let ?fX = "image_mset f X"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. image_mset f M < image_mset f N
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. image_mset f M < image_mset f N
[PROOF STEP]
unfolding less_multiset\<^sub>D\<^sub>M
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>X Y. X \<noteq> {#} \<and> X \<subseteq># image_mset f N \<and> image_mset f M = image_mset f N - X + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a))
[PROOF STEP]
proof (intro exI conjI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. ?X \<noteq> {#}
 2. ?X \<subseteq># image_mset f N
 3. image_mset f M = image_mset f N - ?X + ?Y1
 4. \<forall>k. k \<in># ?Y1 \<longrightarrow> (\<exists>a. a \<in># ?X \<and> k < a)
[PROOF STEP]
show "image_mset f M = image_mset f N - ?fY + ?fX"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. image_mset f M = image_mset f N - image_mset f Y + image_mset f X
[PROOF STEP]
using M_eq[THEN arg_cong, of "image_mset f"] y_sub_N
[PROOF STATE]
proof (prove)
using this:
image_mset f M = image_mset f (N - Y + X)
Y \<subseteq># N

goal (1 subgoal):
 1. image_mset f M = image_mset f N - image_mset f Y + image_mset f X
[PROOF STEP]
by (metis image_mset_Diff image_mset_union)
[PROOF STATE]
proof (state)
this:
image_mset f M = image_mset f N - image_mset f Y + image_mset f X

goal (3 subgoals):
 1. image_mset f Y \<noteq> {#}
 2. image_mset f Y \<subseteq># image_mset f N
 3. \<forall>k. k \<in># image_mset f X \<longrightarrow> (\<exists>a. a \<in># image_mset f Y \<and> k < a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. image_mset f Y \<noteq> {#}
 2. image_mset f Y \<subseteq># image_mset f N
 3. \<forall>k. k \<in># image_mset f X \<longrightarrow> (\<exists>a. a \<in># image_mset f Y \<and> k < a)
[PROOF STEP]
obtain y where y: "\<forall>x. x \<in># X \<longrightarrow> y x \<in># Y \<and> x < y x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<forall>x. x \<in># X \<longrightarrow> y x \<in># Y \<and> x < y x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ex_y
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in># X \<longrightarrow> (\<exists>y. y \<in># Y \<and> x < y)

goal (1 subgoal):
 1. (\<And>y. \<forall>x. x \<in># X \<longrightarrow> y x \<in># Y \<and> x < y x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by moura
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in># X \<longrightarrow> y x \<in># Y \<and> x < y x

goal (3 subgoals):
 1. image_mset f Y \<noteq> {#}
 2. image_mset f Y \<subseteq># image_mset f N
 3. \<forall>k. k \<in># image_mset f X \<longrightarrow> (\<exists>a. a \<in># image_mset f Y \<and> k < a)
[PROOF STEP]
show "\<forall>fx. fx \<in># ?fX \<longrightarrow> (\<exists>fy. fy \<in># ?fY \<and> fx < fy)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>fx. fx \<in># image_mset f X \<longrightarrow> (\<exists>fy. fy \<in># image_mset f Y \<and> fx < fy)
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>fx. fx \<in># image_mset f X \<Longrightarrow> \<exists>fy. fy \<in># image_mset f Y \<and> fx < fy
[PROOF STEP]
fix fx
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>fx. fx \<in># image_mset f X \<Longrightarrow> \<exists>fy. fy \<in># image_mset f Y \<and> fx < fy
[PROOF STEP]
assume "fx \<in># ?fX"
[PROOF STATE]
proof (state)
this:
fx \<in># image_mset f X

goal (1 subgoal):
 1. \<And>fx. fx \<in># image_mset f X \<Longrightarrow> \<exists>fy. fy \<in># image_mset f Y \<and> fx < fy
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fx \<in># image_mset f X
[PROOF STEP]
obtain x where fx: "fx = f x" and x_in: "x \<in># X"
[PROOF STATE]
proof (prove)
using this:
fx \<in># image_mset f X

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>fx = f x; x \<in># X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fx = f x
x \<in># X

goal (1 subgoal):
 1. \<And>fx. fx \<in># image_mset f X \<Longrightarrow> \<exists>fy. fy \<in># image_mset f Y \<and> fx < fy
[PROOF STEP]
hence y_in: "y x \<in># Y" and y_gt: "x < y x"
[PROOF STATE]
proof (prove)
using this:
fx = f x
x \<in># X

goal (1 subgoal):
 1. y x \<in># Y &&& x < y x
[PROOF STEP]
using y[rule_format, OF x_in]
[PROOF STATE]
proof (prove)
using this:
fx = f x
x \<in># X
y x \<in># Y \<and> x < y x

goal (1 subgoal):
 1. y x \<in># Y &&& x < y x
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
y x \<in># Y
x < y x

goal (1 subgoal):
 1. \<And>fx. fx \<in># image_mset f X \<Longrightarrow> \<exists>fy. fy \<in># image_mset f Y \<and> fx < fy
[PROOF STEP]
hence "f (y x) \<in># ?fY \<and> f x < f (y x)"
[PROOF STATE]
proof (prove)
using this:
y x \<in># Y
x < y x

goal (1 subgoal):
 1. f (y x) \<in># image_mset f Y \<and> f x < f (y x)
[PROOF STEP]
using mono_f y_sub_N x_sub_M x_in
[PROOF STATE]
proof (prove)
using this:
y x \<in># Y
x < y x
\<forall>x\<in>#M. \<forall>y\<in>#N. x < y \<longrightarrow> f x < f y
Y \<subseteq># N
X \<subseteq># M
x \<in># X

goal (1 subgoal):
 1. f (y x) \<in># image_mset f Y \<and> f x < f (y x)
[PROOF STEP]
by (metis image_eqI in_image_mset mset_subset_eqD)
[PROOF STATE]
proof (state)
this:
f (y x) \<in># image_mset f Y \<and> f x < f (y x)

goal (1 subgoal):
 1. \<And>fx. fx \<in># image_mset f X \<Longrightarrow> \<exists>fy. fy \<in># image_mset f Y \<and> fx < fy
[PROOF STEP]
thus "\<exists>fy. fy \<in># ?fY \<and> fx < fy"
[PROOF STATE]
proof (prove)
using this:
f (y x) \<in># image_mset f Y \<and> f x < f (y x)

goal (1 subgoal):
 1. \<exists>fy. fy \<in># image_mset f Y \<and> fx < fy
[PROOF STEP]
unfolding fx
[PROOF STATE]
proof (prove)
using this:
f (y x) \<in># image_mset f Y \<and> f x < f (y x)

goal (1 subgoal):
 1. \<exists>fy. fy \<in># image_mset f Y \<and> f x < fy
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>fy. fy \<in># image_mset f Y \<and> fx < fy

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>fx. fx \<in># image_mset f X \<longrightarrow> (\<exists>fy. fy \<in># image_mset f Y \<and> fx < fy)

goal (2 subgoals):
 1. image_mset f Y \<noteq> {#}
 2. image_mset f Y \<subseteq># image_mset f N
[PROOF STEP]
qed (auto simp: y_nemp y_sub_N image_mset_subseteq_mono)
[PROOF STATE]
proof (state)
this:
image_mset f M < image_mset f N

goal:
No subgoals!
[PROOF STEP]
qed