[STATEMENT]
lemma equal_card_inter_fin_eq_sets: "finite A \<Longrightarrow> finite B \<Longrightarrow> card A = card B \<Longrightarrow>
  card (A \<inter> B) = card A \<Longrightarrow> A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; finite B; card A = card B; card (A \<inter> B) = card A\<rbrakk> \<Longrightarrow> A = B
[PROOF STEP]
by (metis Int_lower1 Int_lower2 card_subset_eq)


[STATEMENT]
lemma insert_filter_set_true: "P x \<Longrightarrow> {a \<in> (insert x A) . P a} = insert x {a \<in> A . P a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P x \<Longrightarrow> {a \<in> insert x A. P a} = insert x {a \<in> A. P a}
[PROOF STEP]
by auto


[STATEMENT]
lemma insert_filter_set_false: "\<not> P x \<Longrightarrow> {a \<in> (insert x A) . P a} = {a \<in> A . P a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> P x \<Longrightarrow> {a \<in> insert x A. P a} = {a \<in> A. P a}
[PROOF STEP]
by auto


[STATEMENT]
lemma obtain_two_items_mset:
  assumes "size A > 1"
  obtains x y where "x \<in># A" and "y \<in># A - {#x#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in># A; y \<in># remove1_mset x A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in># A; y \<in># remove1_mset x A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain x where "x \<in># A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in># A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis assms gr_implies_not_zero multiset_nonemptyE size_empty)
[PROOF STATE]
proof (state)
this:
x \<in># A

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in># A; y \<in># remove1_mset x A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "size (A - {#x#}) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < size (remove1_mset x A)
[PROOF STEP]
by (metis \<open>x \<in># A\<close> assms insert_DiffM less_irrefl_nat nonempty_has_size size_single)
[PROOF STATE]
proof (state)
this:
0 < size (remove1_mset x A)

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in># A; y \<in># remove1_mset x A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < size (remove1_mset x A)
[PROOF STEP]
obtain bl2 where "bl2 \<in># A - {#x#}"
[PROOF STATE]
proof (prove)
using this:
0 < size (remove1_mset x A)

goal (1 subgoal):
 1. (\<And>bl2. bl2 \<in># remove1_mset x A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis less_not_refl multiset_nonemptyE size_empty)
[PROOF STATE]
proof (state)
this:
bl2 \<in># remove1_mset x A

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in># A; y \<in># remove1_mset x A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
bl2 \<in># remove1_mset x A

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using \<open>x \<in># A\<close> that
[PROOF STATE]
proof (prove)
using this:
bl2 \<in># remove1_mset x A
x \<in># A
\<lbrakk>?x \<in># A; ?y \<in># remove1_mset ?x A\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma obtain_two_items_mset_filter:
  assumes "size {#a \<in># A . P a #} > 1"
  obtains x y where "x \<in># A" and "y \<in># A - {#x#}" and "P x" and "P y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in># A; y \<in># remove1_mset x A; P x; P y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in># A; y \<in># remove1_mset x A; P x; P y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain x y where xin: "x \<in># {#a \<in># A . P a #}" and yin: "y \<in># {#a \<in># A . P a #} - {#x#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in># filter_mset P A; y \<in># remove1_mset x (filter_mset P A)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obtain_two_items_mset assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>1 < size ?A; \<And>x y. \<lbrakk>x \<in># ?A; y \<in># remove1_mset x ?A\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
1 < size (filter_mset P A)

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in># filter_mset P A; y \<in># remove1_mset x (filter_mset P A)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in># filter_mset P A
y \<in># remove1_mset x (filter_mset P A)

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in># A; y \<in># remove1_mset x A; P x; P y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in># filter_mset P A
y \<in># remove1_mset x (filter_mset P A)
[PROOF STEP]
have xdets: "x \<in># A" "P x"
[PROOF STATE]
proof (prove)
using this:
x \<in># filter_mset P A
y \<in># remove1_mset x (filter_mset P A)

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

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in># A; y \<in># remove1_mset x A; P x; P y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in># A
P x
[PROOF STEP]
have yin2: "y \<in># {#a \<in># (A - {#x#}) . P a #}"
[PROOF STATE]
proof (prove)
using this:
x \<in># A
P x

goal (1 subgoal):
 1. y \<in># filter_mset P (remove1_mset x A)
[PROOF STEP]
using yin
[PROOF STATE]
proof (prove)
using this:
x \<in># A
P x
y \<in># remove1_mset x (filter_mset P A)

goal (1 subgoal):
 1. y \<in># filter_mset P (remove1_mset x A)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
y \<in># filter_mset P (remove1_mset x A)

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in># A; y \<in># remove1_mset x A; P x; P y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in># filter_mset P (remove1_mset x A)
[PROOF STEP]
have "y \<in># (A - {#x#})" "P y"
[PROOF STATE]
proof (prove)
using this:
y \<in># filter_mset P (remove1_mset x A)

goal (1 subgoal):
 1. y \<in># remove1_mset x A &&& P y
[PROOF STEP]
by (metis multiset_partition union_iff) (meson yin2 filter_mset_eq_conv)
[PROOF STATE]
proof (state)
this:
y \<in># remove1_mset x A
P y

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in># A; y \<in># remove1_mset x A; P x; P y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<in># remove1_mset x A
P y

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using xdets that
[PROOF STATE]
proof (prove)
using this:
y \<in># remove1_mset x A
P y
x \<in># A
P x
\<lbrakk>?x \<in># A; ?y \<in># remove1_mset ?x A; P ?x; P ?y\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma size_count_mset_ss:
  assumes "finite B"
  assumes "(set_mset A) \<subseteq> B"
  shows "size A = (\<Sum> x \<in> B . count A x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size A = sum (count A) B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. size A = sum (count A) B
[PROOF STEP]
obtain C where cdef: "B - (set_mset A) = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C. B - set_mset A = C \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite B
set_mset A \<subseteq> B

goal (1 subgoal):
 1. (\<And>C. B - set_mset A = C \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
B - set_mset A = C

goal (1 subgoal):
 1. size A = sum (count A) B
[PROOF STEP]
have fin: "finite (set_mset A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set_mset A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite B
set_mset A \<subseteq> B

goal (1 subgoal):
 1. finite (set_mset A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (set_mset A)

goal (1 subgoal):
 1. size A = sum (count A) B
[PROOF STEP]
have un: "C \<union> (set_mset A) = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<union> set_mset A = B
[PROOF STEP]
using Diff_partition \<open>B - set_mset A = C\<close> assms
[PROOF STATE]
proof (prove)
using this:
?A \<subseteq> ?B \<Longrightarrow> ?A \<union> (?B - ?A) = ?B
B - set_mset A = C
finite B
set_mset A \<subseteq> B

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

goal (1 subgoal):
 1. size A = sum (count A) B
[PROOF STEP]
have disj: "C \<inter> (set_mset A) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<inter> set_mset A = {}
[PROOF STEP]
using \<open>B - set_mset A = C\<close>
[PROOF STATE]
proof (prove)
using this:
B - set_mset A = C

goal (1 subgoal):
 1. C \<inter> set_mset A = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C \<inter> set_mset A = {}

goal (1 subgoal):
 1. size A = sum (count A) B
[PROOF STEP]
have zero: "\<And> x . x\<in> C \<Longrightarrow> count A x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> C \<Longrightarrow> count A x = 0
[PROOF STEP]
by (meson count_eq_zero_iff disj disjoint_iff_not_equal)
[PROOF STATE]
proof (state)
this:
?x \<in> C \<Longrightarrow> count A ?x = 0

goal (1 subgoal):
 1. size A = sum (count A) B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> C \<Longrightarrow> count A ?x = 0
[PROOF STEP]
have "(\<Sum> x \<in> B . count A x) = (\<Sum> x \<in> (C \<union> set_mset A) . count A x)"
[PROOF STATE]
proof (prove)
using this:
?x \<in> C \<Longrightarrow> count A ?x = 0

goal (1 subgoal):
 1. sum (count A) B = sum (count A) (C \<union> set_mset A)
[PROOF STEP]
using un
[PROOF STATE]
proof (prove)
using this:
?x \<in> C \<Longrightarrow> count A ?x = 0
C \<union> set_mset A = B

goal (1 subgoal):
 1. sum (count A) B = sum (count A) (C \<union> set_mset A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum (count A) B = sum (count A) (C \<union> set_mset A)

goal (1 subgoal):
 1. size A = sum (count A) B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum (count A) B = sum (count A) (C \<union> set_mset A)

goal (1 subgoal):
 1. size A = sum (count A) B
[PROOF STEP]
have "... = (\<Sum> x \<in> C . count A x) + (\<Sum> x \<in> (set_mset A) . count A x) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (count A) (C \<union> set_mset A) = sum (count A) C + sum (count A) (set_mset A)
[PROOF STEP]
using disj fin assms cdef sum.subset_diff
[PROOF STATE]
proof (prove)
using this:
C \<inter> set_mset A = {}
finite (set_mset A)
finite B
set_mset A \<subseteq> B
B - set_mset A = C
\<lbrakk>?B \<subseteq> ?A; finite ?A\<rbrakk> \<Longrightarrow> sum ?g ?A = sum ?g (?A - ?B) + sum ?g ?B

goal (1 subgoal):
 1. sum (count A) (C \<union> set_mset A) = sum (count A) C + sum (count A) (set_mset A)
[PROOF STEP]
by (metis un)
[PROOF STATE]
proof (state)
this:
sum (count A) (C \<union> set_mset A) = sum (count A) C + sum (count A) (set_mset A)

goal (1 subgoal):
 1. size A = sum (count A) B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum (count A) (C \<union> set_mset A) = sum (count A) C + sum (count A) (set_mset A)

goal (1 subgoal):
 1. size A = sum (count A) B
[PROOF STEP]
have "... = (\<Sum> x \<in> (set_mset A) . count A x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (count A) C + sum (count A) (set_mset A) = sum (count A) (set_mset A)
[PROOF STEP]
using zero
[PROOF STATE]
proof (prove)
using this:
?x \<in> C \<Longrightarrow> count A ?x = 0

goal (1 subgoal):
 1. sum (count A) C + sum (count A) (set_mset A) = sum (count A) (set_mset A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum (count A) C + sum (count A) (set_mset A) = sum (count A) (set_mset A)

goal (1 subgoal):
 1. size A = sum (count A) B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum (count A) B = sum (count A) (set_mset A)
[PROOF STEP]
have "(\<Sum> x \<in> B . count A x) = size A"
[PROOF STATE]
proof (prove)
using this:
sum (count A) B = sum (count A) (set_mset A)

goal (1 subgoal):
 1. sum (count A) B = size A
[PROOF STEP]
by (simp add: size_multiset_overloaded_eq)
[PROOF STATE]
proof (state)
this:
sum (count A) B = size A

goal (1 subgoal):
 1. size A = sum (count A) B
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sum (count A) B = size A

goal (1 subgoal):
 1. size A = sum (count A) B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
size A = sum (count A) B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mset_list_by_index: "mset (xs) = image_mset (\<lambda> i . (xs ! i)) (mset_set {..<length xs})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset xs = image_mset ((!) xs) (mset_set {..<length xs})
[PROOF STEP]
by (metis map_nth mset_map mset_set_upto_eq_mset_upto)


[STATEMENT]
lemma count_mset_split_image_filter:
  assumes "\<And> x. x \<in>#A \<Longrightarrow> a \<noteq> g x"
  shows "count (image_mset (\<lambda>x. if P x then a else g x) A ) a = size (filter_mset P A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count {#if P x then a else g x. x \<in># A#} a = size (filter_mset P A)
[PROOF STEP]
using image_mset_If image_mset_filter_swap size_image_mset
[PROOF STATE]
proof (prove)
using this:
{#if ?P x then ?f x else ?g x. x \<in># ?A#} = image_mset ?f (filter_mset ?P ?A) + image_mset ?g {#x \<in># ?A. \<not> ?P x#}
image_mset ?f {#x \<in># ?M. ?P (?f x)#} = filter_mset ?P (image_mset ?f ?M)
size (image_mset ?f ?M) = size ?M

goal (1 subgoal):
 1. count {#if P x then a else g x. x \<in># A#} a = size (filter_mset P A)
[PROOF STEP]
by (smt (verit) assms count_size_set_repr filter_mset_cong)


[STATEMENT]
lemma count_mset_split_image_filter_not:
  assumes "\<And> x. x \<in>#A \<Longrightarrow> b \<noteq> f x"
  shows "count (image_mset (\<lambda>x. if P x then f x else b) A ) b = size (filter_mset (\<lambda> x. \<not> P x) A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count {#if P x then f x else b. x \<in># A#} b = size {#x \<in># A. \<not> P x#}
[PROOF STEP]
using image_mset_If image_mset_filter_swap size_image_mset
[PROOF STATE]
proof (prove)
using this:
{#if ?P x then ?f x else ?g x. x \<in># ?A#} = image_mset ?f (filter_mset ?P ?A) + image_mset ?g {#x \<in># ?A. \<not> ?P x#}
image_mset ?f {#x \<in># ?M. ?P (?f x)#} = filter_mset ?P (image_mset ?f ?M)
size (image_mset ?f ?M) = size ?M

goal (1 subgoal):
 1. count {#if P x then f x else b. x \<in># A#} b = size {#x \<in># A. \<not> P x#}
[PROOF STEP]
by (smt (verit) assms count_size_set_repr filter_mset_cong)


[STATEMENT]
lemma removeAll_size_lt: "size (removeAll_mset C M) \<le> size M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (removeAll_mset C M) \<le> size M
[PROOF STEP]
by (simp add: size_mset_mono)


[STATEMENT]
lemma mset_image_eq_filter_eq: "A = image_mset f B \<Longrightarrow>
  filter_mset P A = (image_mset f (filter_mset (\<lambda> x. P (f x)) B))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = image_mset f B \<Longrightarrow> filter_mset P A = image_mset f {#x \<in># B. P (f x)#}
[PROOF STEP]
by (simp add: filter_mset_image_mset)


[STATEMENT]
lemma elem_permutation_of_set_empty_iff: "finite A \<Longrightarrow> xs \<in> permutations_of_set A \<Longrightarrow>
    xs = [] \<longleftrightarrow> A = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; xs \<in> permutations_of_set A\<rbrakk> \<Longrightarrow> (xs = []) = (A = {})
[PROOF STEP]
using permutations_of_setD(1)
[PROOF STATE]
proof (prove)
using this:
?xs \<in> permutations_of_set ?A \<Longrightarrow> set ?xs = ?A

goal (1 subgoal):
 1. \<lbrakk>finite A; xs \<in> permutations_of_set A\<rbrakk> \<Longrightarrow> (xs = []) = (A = {})
[PROOF STEP]
by fastforce


[STATEMENT]
lemma elem_permutation_of_mset_empty_iff: "xs \<in> permutations_of_multiset A \<Longrightarrow> xs = [] \<longleftrightarrow> A = {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> permutations_of_multiset A \<Longrightarrow> (xs = []) = (A = {#})
[PROOF STEP]
using permutations_of_multisetD
[PROOF STATE]
proof (prove)
using this:
?xs \<in> permutations_of_multiset ?A \<Longrightarrow> mset ?xs = ?A

goal (1 subgoal):
 1. xs \<in> permutations_of_multiset A \<Longrightarrow> (xs = []) = (A = {#})
[PROOF STEP]
by fastforce


[STATEMENT]
lemma count_distinct_mset_list_index: "i1 < length xs \<Longrightarrow> i2 < length xs \<Longrightarrow> i1 \<noteq> i2 \<Longrightarrow>
    distinct_mset (mset xs) \<Longrightarrow> xs ! i1 \<noteq> xs ! i2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i1 < length xs; i2 < length xs; i1 \<noteq> i2; distinct_mset (mset xs)\<rbrakk> \<Longrightarrow> xs ! i1 \<noteq> xs ! i2
[PROOF STEP]
by (simp add:  nth_eq_iff_index_eq)


[STATEMENT]
lemma index_remove1_mset_ne:
  assumes "x \<in># (mset xs)"
  assumes "y \<in># remove1_mset x (mset xs)"
  assumes "xs ! j1 = x"
  assumes "j1 < length xs"
  obtains j2 where "xs ! j2 = y" and "j2 < length xs" and "j1 \<noteq> j2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (cases "x = y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x = y\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = y

goal (2 subgoals):
 1. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x = y\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = y
[PROOF STEP]
have "count (mset xs) x \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
x = y

goal (1 subgoal):
 1. 2 \<le> count (mset xs) x
[PROOF STEP]
using assms(2) count_eq_zero_iff
[PROOF STATE]
proof (prove)
using this:
x = y
y \<in># remove1_mset x (mset xs)
(count ?M ?x = 0) = (?x \<notin># ?M)

goal (1 subgoal):
 1. 2 \<le> count (mset xs) x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
2 \<le> count (mset xs) x

goal (2 subgoals):
 1. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x = y\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 \<le> count (mset xs) x
[PROOF STEP]
have crm: "count (remove1_mset x (mset xs)) x \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
2 \<le> count (mset xs) x

goal (1 subgoal):
 1. 1 \<le> count (remove1_mset x (mset xs)) x
[PROOF STEP]
by (metis True assms(2) count_greater_eq_one_iff)
[PROOF STATE]
proof (state)
this:
1 \<le> count (remove1_mset x (mset xs)) x

goal (2 subgoals):
 1. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x = y\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
obtain ys zs where xseq: "xs = ys @ (x # zs)" and yseq: "ys = take j1 xs" and zseq: "zs = drop (Suc j1) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ys zs. \<lbrakk>xs = ys @ x # zs; ys = take j1 xs; zs = drop (Suc j1) xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using  assms(1) assms(3) id_take_nth_drop in_mset_conv_nth assms(4)
[PROOF STATE]
proof (prove)
using this:
x \<in># mset xs
xs ! j1 = x
?i < length ?xs \<Longrightarrow> ?xs = take ?i ?xs @ ?xs ! ?i # drop (Suc ?i) ?xs
(?x \<in># mset ?xs) = (\<exists>i<length ?xs. ?xs ! i = ?x)
j1 < length xs

goal (1 subgoal):
 1. (\<And>ys zs. \<lbrakk>xs = ys @ x # zs; ys = take j1 xs; zs = drop (Suc j1) xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xs = ys @ x # zs
ys = take j1 xs
zs = drop (Suc j1) xs

goal (2 subgoals):
 1. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x = y\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "mset xs = mset ys + mset (x # zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset xs = mset ys + mset (x # zs)
[PROOF STEP]
by (simp add: xseq)
[PROOF STATE]
proof (state)
this:
mset xs = mset ys + mset (x # zs)

goal (2 subgoals):
 1. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x = y\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mset xs = mset ys + mset (x # zs)
[PROOF STEP]
have "remove1_mset x (mset xs) = mset (ys) + mset (zs)"
[PROOF STATE]
proof (prove)
using this:
mset xs = mset ys + mset (x # zs)

goal (1 subgoal):
 1. remove1_mset x (mset xs) = mset ys + mset zs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mset xs = mset ys + mset (x # zs)
x \<in># mset xs
y \<in># remove1_mset x (mset xs)
xs ! j1 = x
j1 < length xs

goal (1 subgoal):
 1. remove1_mset x (mset xs) = mset ys + mset zs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
remove1_mset x (mset xs) = mset ys + mset zs

goal (2 subgoals):
 1. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x = y\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
remove1_mset x (mset xs) = mset ys + mset zs
[PROOF STEP]
have "y \<in># (mset ys + mset zs)"
[PROOF STATE]
proof (prove)
using this:
remove1_mset x (mset xs) = mset ys + mset zs

goal (1 subgoal):
 1. y \<in># mset ys + mset zs
[PROOF STEP]
using crm
[PROOF STATE]
proof (prove)
using this:
remove1_mset x (mset xs) = mset ys + mset zs
1 \<le> count (remove1_mset x (mset xs)) x

goal (1 subgoal):
 1. y \<in># mset ys + mset zs
[PROOF STEP]
using True \<open>remove1_mset x (mset xs) = mset ys + mset zs\<close> assms(2)
[PROOF STATE]
proof (prove)
using this:
remove1_mset x (mset xs) = mset ys + mset zs
1 \<le> count (remove1_mset x (mset xs)) x
x = y
remove1_mset x (mset xs) = mset ys + mset zs
y \<in># remove1_mset x (mset xs)

goal (1 subgoal):
 1. y \<in># mset ys + mset zs
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
y \<in># mset ys + mset zs

goal (2 subgoals):
 1. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x = y\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in># mset ys + mset zs
[PROOF STEP]
have yinor: "y \<in># mset ys \<or> y \<in># mset zs"
[PROOF STATE]
proof (prove)
using this:
y \<in># mset ys + mset zs

goal (1 subgoal):
 1. y \<in># mset ys \<or> y \<in># mset zs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y \<in># mset ys \<or> y \<in># mset zs

goal (2 subgoals):
 1. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x = y\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in># mset ys \<or> y \<in># mset zs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<in># mset ys \<or> y \<in># mset zs

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (cases "y \<in># mset ys")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>y \<in># mset ys \<or> y \<in># mset zs; y \<in># mset ys\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>y \<in># mset ys \<or> y \<in># mset zs; y \<notin># mset ys\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y \<in># mset ys

goal (2 subgoals):
 1. \<lbrakk>y \<in># mset ys \<or> y \<in># mset zs; y \<in># mset ys\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>y \<in># mset ys \<or> y \<in># mset zs; y \<notin># mset ys\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in># mset ys
[PROOF STEP]
obtain j2 where yeq: "ys ! j2 = y" and j2lt: "j2 < length ys"
[PROOF STATE]
proof (prove)
using this:
y \<in># mset ys

goal (1 subgoal):
 1. (\<And>j2. \<lbrakk>ys ! j2 = y; j2 < length ys\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson in_mset_conv_nth)
[PROOF STATE]
proof (state)
this:
ys ! j2 = y
j2 < length ys

goal (2 subgoals):
 1. \<lbrakk>y \<in># mset ys \<or> y \<in># mset zs; y \<in># mset ys\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>y \<in># mset ys \<or> y \<in># mset zs; y \<notin># mset ys\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ys ! j2 = y
j2 < length ys
[PROOF STEP]
have 1: "xs ! j2 = y"
[PROOF STATE]
proof (prove)
using this:
ys ! j2 = y
j2 < length ys

goal (1 subgoal):
 1. xs ! j2 = y
[PROOF STEP]
using yseq
[PROOF STATE]
proof (prove)
using this:
ys ! j2 = y
j2 < length ys
ys = take j1 xs

goal (1 subgoal):
 1. xs ! j2 = y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xs ! j2 = y

goal (2 subgoals):
 1. \<lbrakk>y \<in># mset ys \<or> y \<in># mset zs; y \<in># mset ys\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>y \<in># mset ys \<or> y \<in># mset zs; y \<notin># mset ys\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "j2 < j1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j2 < j1
[PROOF STEP]
using yseq j2lt
[PROOF STATE]
proof (prove)
using this:
ys = take j1 xs
j2 < length ys

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

goal (2 subgoals):
 1. \<lbrakk>y \<in># mset ys \<or> y \<in># mset zs; y \<in># mset ys\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>y \<in># mset ys \<or> y \<in># mset zs; y \<notin># mset ys\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j2 < j1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
j2 < j1

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that 1 j2lt xseq
[PROOF STATE]
proof (prove)
using this:
j2 < j1
\<lbrakk>xs ! ?j2.0 = y; ?j2.0 < length xs; j1 \<noteq> ?j2.0\<rbrakk> \<Longrightarrow> thesis
xs ! j2 = y
j2 < length ys
xs = ys @ x # zs

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

goal (1 subgoal):
 1. \<lbrakk>y \<in># mset ys \<or> y \<in># mset zs; y \<notin># mset ys\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>y \<in># mset ys \<or> y \<in># mset zs; y \<notin># mset ys\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
y \<notin># mset ys

goal (1 subgoal):
 1. \<lbrakk>y \<in># mset ys \<or> y \<in># mset zs; y \<notin># mset ys\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<notin># mset ys
[PROOF STEP]
have "y \<in># mset zs"
[PROOF STATE]
proof (prove)
using this:
y \<notin># mset ys

goal (1 subgoal):
 1. y \<in># mset zs
[PROOF STEP]
using yinor
[PROOF STATE]
proof (prove)
using this:
y \<notin># mset ys
y \<in># mset ys \<or> y \<in># mset zs

goal (1 subgoal):
 1. y \<in># mset zs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y \<in># mset zs

goal (1 subgoal):
 1. \<lbrakk>y \<in># mset ys \<or> y \<in># mset zs; y \<notin># mset ys\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in># mset zs
[PROOF STEP]
obtain j2 where zsy: "zs ! j2 = y" and j2lt: "j2 < length zs"
[PROOF STATE]
proof (prove)
using this:
y \<in># mset zs

goal (1 subgoal):
 1. (\<And>j2. \<lbrakk>zs ! j2 = y; j2 < length zs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson in_mset_conv_nth)
[PROOF STATE]
proof (state)
this:
zs ! j2 = y
j2 < length zs

goal (1 subgoal):
 1. \<lbrakk>y \<in># mset ys \<or> y \<in># mset zs; y \<notin># mset ys\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zs ! j2 = y
j2 < length zs
[PROOF STEP]
have 1: "xs ! ((Suc j1) + j2) = y"
[PROOF STATE]
proof (prove)
using this:
zs ! j2 = y
j2 < length zs

goal (1 subgoal):
 1. xs ! (Suc j1 + j2) = y
[PROOF STEP]
using zseq zsy assms(4)
[PROOF STATE]
proof (prove)
using this:
zs ! j2 = y
j2 < length zs
zs = drop (Suc j1) xs
zs ! j2 = y
j1 < length xs

goal (1 subgoal):
 1. xs ! (Suc j1 + j2) = y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xs ! (Suc j1 + j2) = y

goal (1 subgoal):
 1. \<lbrakk>y \<in># mset ys \<or> y \<in># mset zs; y \<notin># mset ys\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "length xs = (Suc j1) + length zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = Suc j1 + length zs
[PROOF STEP]
using zseq xseq
[PROOF STATE]
proof (prove)
using this:
zs = drop (Suc j1) xs
xs = ys @ x # zs

goal (1 subgoal):
 1. length xs = Suc j1 + length zs
[PROOF STEP]
by (metis Suc_diff_Suc add_Suc_shift add_diff_inverse_nat assms(4) length_drop less_imp_not_less)
[PROOF STATE]
proof (state)
this:
length xs = Suc j1 + length zs

goal (1 subgoal):
 1. \<lbrakk>y \<in># mset ys \<or> y \<in># mset zs; y \<notin># mset ys\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs = Suc j1 + length zs
[PROOF STEP]
have 2: "(Suc j1) + j2 < length xs"
[PROOF STATE]
proof (prove)
using this:
length xs = Suc j1 + length zs

goal (1 subgoal):
 1. Suc j1 + j2 < length xs
[PROOF STEP]
using j2lt
[PROOF STATE]
proof (prove)
using this:
length xs = Suc j1 + length zs
j2 < length zs

goal (1 subgoal):
 1. Suc j1 + j2 < length xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc j1 + j2 < length xs

goal (1 subgoal):
 1. \<lbrakk>y \<in># mset ys \<or> y \<in># mset zs; y \<notin># mset ys\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Suc j1 + j2 < length xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Suc j1 + j2 < length xs

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using 1 that
[PROOF STATE]
proof (prove)
using this:
Suc j1 + j2 < length xs
xs ! (Suc j1 + j2) = y
\<lbrakk>xs ! ?j2.0 = y; ?j2.0 < length xs; j1 \<noteq> ?j2.0\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. \<lbrakk>\<And>j2. \<lbrakk>xs ! j2 = y; j2 < length xs; j1 \<noteq> j2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (metis that assms(2) assms(3) in_diffD in_mset_conv_nth)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma count_list_mset: "count_list xs x = count (mset xs) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_list xs x = count (mset xs) x
[PROOF STEP]
proof (induct xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. count_list [] x = count (mset []) x
 2. \<And>a xs. count_list xs x = count (mset xs) x \<Longrightarrow> count_list (a # xs) x = count (mset (a # xs)) x
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. count_list [] x = count (mset []) x
 2. \<And>a xs. count_list xs x = count (mset xs) x \<Longrightarrow> count_list (a # xs) x = count (mset (a # xs)) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_list [] x = count (mset []) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
count_list [] x = count (mset []) x

goal (1 subgoal):
 1. \<And>a xs. count_list xs x = count (mset xs) x \<Longrightarrow> count_list (a # xs) x = count (mset (a # xs)) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. count_list xs x = count (mset xs) x \<Longrightarrow> count_list (a # xs) x = count (mset (a # xs)) x
[PROOF STEP]
case (Cons a xs)
[PROOF STATE]
proof (state)
this:
count_list xs x = count (mset xs) x

goal (1 subgoal):
 1. \<And>a xs. count_list xs x = count (mset xs) x \<Longrightarrow> count_list (a # xs) x = count (mset (a # xs)) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
count_list xs x = count (mset xs) x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
count_list xs x = count (mset xs) x

goal (1 subgoal):
 1. count_list (a # xs) x = count (mset (a # xs)) x
[PROOF STEP]
proof (cases "a = x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>count_list xs x = count (mset xs) x; a = x\<rbrakk> \<Longrightarrow> count_list (a # xs) x = count (mset (a # xs)) x
 2. \<lbrakk>count_list xs x = count (mset xs) x; a \<noteq> x\<rbrakk> \<Longrightarrow> count_list (a # xs) x = count (mset (a # xs)) x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = x

goal (2 subgoals):
 1. \<lbrakk>count_list xs x = count (mset xs) x; a = x\<rbrakk> \<Longrightarrow> count_list (a # xs) x = count (mset (a # xs)) x
 2. \<lbrakk>count_list xs x = count (mset xs) x; a \<noteq> x\<rbrakk> \<Longrightarrow> count_list (a # xs) x = count (mset (a # xs)) x
[PROOF STEP]
have mset_add_split: "count (mset (a # xs)) x = count (add_mset a (mset xs)) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count (mset (a # xs)) x = count (add_mset a (mset xs)) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
count (mset (a # xs)) x = count (add_mset a (mset xs)) x

goal (2 subgoals):
 1. \<lbrakk>count_list xs x = count (mset xs) x; a = x\<rbrakk> \<Longrightarrow> count_list (a # xs) x = count (mset (a # xs)) x
 2. \<lbrakk>count_list xs x = count (mset xs) x; a \<noteq> x\<rbrakk> \<Longrightarrow> count_list (a # xs) x = count (mset (a # xs)) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
count (mset (a # xs)) x = count (add_mset a (mset xs)) x
[PROOF STEP]
have "count (mset (a # xs)) x = count (mset xs) x + 1"
[PROOF STATE]
proof (prove)
using this:
count (mset (a # xs)) x = count (add_mset a (mset xs)) x

goal (1 subgoal):
 1. count (mset (a # xs)) x = count (mset xs) x + 1
[PROOF STEP]
by (metis True Suc_eq_plus1 count_add_mset)
[PROOF STATE]
proof (state)
this:
count (mset (a # xs)) x = count (mset xs) x + 1

goal (2 subgoals):
 1. \<lbrakk>count_list xs x = count (mset xs) x; a = x\<rbrakk> \<Longrightarrow> count_list (a # xs) x = count (mset (a # xs)) x
 2. \<lbrakk>count_list xs x = count (mset xs) x; a \<noteq> x\<rbrakk> \<Longrightarrow> count_list (a # xs) x = count (mset (a # xs)) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
count (mset (a # xs)) x = count (mset xs) x + 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
count (mset (a # xs)) x = count (mset xs) x + 1

goal (1 subgoal):
 1. count_list (a # xs) x = count (mset (a # xs)) x
[PROOF STEP]
using True Cons.hyps
[PROOF STATE]
proof (prove)
using this:
count (mset (a # xs)) x = count (mset xs) x + 1
a = x
count_list xs x = count (mset xs) x

goal (1 subgoal):
 1. count_list (a # xs) x = count (mset (a # xs)) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
count_list (a # xs) x = count (mset (a # xs)) x

goal (1 subgoal):
 1. \<lbrakk>count_list xs x = count (mset xs) x; a \<noteq> x\<rbrakk> \<Longrightarrow> count_list (a # xs) x = count (mset (a # xs)) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>count_list xs x = count (mset xs) x; a \<noteq> x\<rbrakk> \<Longrightarrow> count_list (a # xs) x = count (mset (a # xs)) x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> x

goal (1 subgoal):
 1. \<lbrakk>count_list xs x = count (mset xs) x; a \<noteq> x\<rbrakk> \<Longrightarrow> count_list (a # xs) x = count (mset (a # xs)) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<noteq> x

goal (1 subgoal):
 1. count_list (a # xs) x = count (mset (a # xs)) x
[PROOF STEP]
using Cons.hyps
[PROOF STATE]
proof (prove)
using this:
a \<noteq> x
count_list xs x = count (mset xs) x

goal (1 subgoal):
 1. count_list (a # xs) x = count (mset (a # xs)) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
count_list (a # xs) x = count (mset (a # xs)) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
count_list (a # xs) x = count (mset (a # xs)) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma count_min_2_indices_lt:
  assumes "i1 < i2"
  assumes "xs ! i1 = x"
  assumes "xs ! i2 = x"
  assumes "i1 < length xs" "i2 < length xs"
  shows "count (mset xs) x \<ge> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 \<le> count (mset xs) x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 2 \<le> count (mset xs) x
[PROOF STEP]
obtain xs1 xs2 where xse: "xs = xs1 @ xs2" and xs1: "xs1 = take i2 xs" and xs2: "xs2 = drop i2 xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs1 xs2. \<lbrakk>xs = xs1 @ xs2; xs1 = take i2 xs; xs2 = drop i2 xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xs = xs1 @ xs2
xs1 = take i2 xs
xs2 = drop i2 xs

goal (1 subgoal):
 1. 2 \<le> count (mset xs) x
[PROOF STEP]
have "i1 < length xs1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i1 < length xs1
[PROOF STEP]
using assms length_take
[PROOF STATE]
proof (prove)
using this:
i1 < i2
xs ! i1 = x
xs ! i2 = x
i1 < length xs
i2 < length xs
length (take ?n ?xs) = min (length ?xs) ?n

goal (1 subgoal):
 1. i1 < length xs1
[PROOF STEP]
by (simp add: assms(4) \<open>xs1 = take i2 xs\<close>)
[PROOF STATE]
proof (state)
this:
i1 < length xs1

goal (1 subgoal):
 1. 2 \<le> count (mset xs) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i1 < length xs1
[PROOF STEP]
have xs1in:  "xs ! i1 \<in># mset xs1"
[PROOF STATE]
proof (prove)
using this:
i1 < length xs1

goal (1 subgoal):
 1. xs ! i1 \<in># mset xs1
[PROOF STEP]
by (simp add: nth_append xse)
[PROOF STATE]
proof (state)
this:
xs ! i1 \<in># mset xs1

goal (1 subgoal):
 1. 2 \<le> count (mset xs) x
[PROOF STEP]
have "i2 \<ge> length xs1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs1 \<le> i2
[PROOF STEP]
using assms length_take xs1
[PROOF STATE]
proof (prove)
using this:
i1 < i2
xs ! i1 = x
xs ! i2 = x
i1 < length xs
i2 < length xs
length (take ?n ?xs) = min (length ?xs) ?n
xs1 = take i2 xs

goal (1 subgoal):
 1. length xs1 \<le> i2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length xs1 \<le> i2

goal (1 subgoal):
 1. 2 \<le> count (mset xs) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs1 \<le> i2
[PROOF STEP]
have xs2in: "xs ! i2 \<in># mset xs2"
[PROOF STATE]
proof (prove)
using this:
length xs1 \<le> i2

goal (1 subgoal):
 1. xs ! i2 \<in># mset xs2
[PROOF STEP]
using xse nth_append
[PROOF STATE]
proof (prove)
using this:
length xs1 \<le> i2
xs = xs1 @ xs2
(?xs @ ?ys) ! ?n = (if ?n < length ?xs then ?xs ! ?n else ?ys ! (?n - length ?xs))

goal (1 subgoal):
 1. xs ! i2 \<in># mset xs2
[PROOF STEP]
by (metis (no_types, lifting) assms(5) in_mset_conv_nth leD leI take_all_iff take_append)
[PROOF STATE]
proof (state)
this:
xs ! i2 \<in># mset xs2

goal (1 subgoal):
 1. 2 \<le> count (mset xs) x
[PROOF STEP]
have "count (mset xs) x = count ((mset xs1) + (mset xs2)) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count (mset xs) x = count (mset xs1 + mset xs2) x
[PROOF STEP]
by (simp add: xse)
[PROOF STATE]
proof (state)
this:
count (mset xs) x = count (mset xs1 + mset xs2) x

goal (1 subgoal):
 1. 2 \<le> count (mset xs) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
count (mset xs) x = count (mset xs1 + mset xs2) x
[PROOF STEP]
have "count (mset xs) x = count (mset xs1) x + count (mset xs2) x"
[PROOF STATE]
proof (prove)
using this:
count (mset xs) x = count (mset xs1 + mset xs2) x

goal (1 subgoal):
 1. count (mset xs) x = count (mset xs1) x + count (mset xs2) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
count (mset xs) x = count (mset xs1) x + count (mset xs2) x

goal (1 subgoal):
 1. 2 \<le> count (mset xs) x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
count (mset xs) x = count (mset xs1) x + count (mset xs2) x

goal (1 subgoal):
 1. 2 \<le> count (mset xs) x
[PROOF STEP]
using xs1in xs2in
[PROOF STATE]
proof (prove)
using this:
count (mset xs) x = count (mset xs1) x + count (mset xs2) x
xs ! i1 \<in># mset xs1
xs ! i2 \<in># mset xs2

goal (1 subgoal):
 1. 2 \<le> count (mset xs) x
[PROOF STEP]
by (metis add_mono assms(2) assms(3) count_greater_eq_one_iff nat_1_add_1)
[PROOF STATE]
proof (state)
this:
2 \<le> count (mset xs) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma count_min_2_indices: "i1 \<noteq> i2 \<Longrightarrow> xs ! i1 = x \<Longrightarrow> xs ! i2 = x \<Longrightarrow> i1 < length xs \<Longrightarrow>
  i2 < length xs \<Longrightarrow> count (mset xs) x \<ge> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i1 \<noteq> i2; xs ! i1 = x; xs ! i2 = x; i1 < length xs; i2 < length xs\<rbrakk> \<Longrightarrow> 2 \<le> count (mset xs) x
[PROOF STEP]
apply (cases "i1 < i2", simp add: count_min_2_indices_lt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i1 \<noteq> i2; xs ! i1 = x; xs ! i2 = x; i1 < length xs; i2 < length xs; \<not> i1 < i2\<rbrakk> \<Longrightarrow> 2 \<le> count (mset xs) x
[PROOF STEP]
by (metis count_min_2_indices_lt linorder_cases)


[STATEMENT]
lemma obtain_set_list_item:
  assumes "x \<in> set xs"
  obtains i where "i < length xs" and "xs ! i = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < length xs; xs ! i = x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson assms in_set_conv_nth)


[STATEMENT]
lemma double_sum_mult_hom:
  fixes k :: "'b :: {comm_ring_1}"
  shows "(\<Sum> i \<in> A . (\<Sum> j \<in> g i . k * (f i j))) = k* (\<Sum> i \<in> A . (\<Sum> j \<in> g i . f i j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>A. \<Sum>j\<in>g i. k * f i j) = k * (\<Sum>i\<in>A. sum (f i) (g i))
[PROOF STEP]
by (metis (mono_tags, lifting) comm_monoid_add_class.sum.cong sum_distrib_left)


[STATEMENT]
lemma double_sum_split_case:
  assumes "finite A"
  shows "(\<Sum> i \<in> A . (\<Sum> j \<in> A . f i j)) = (\<Sum> i \<in> A . (f i i)) + (\<Sum> i \<in> A . (\<Sum> j \<in> (A - {i}) . f i j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>A. sum (f i) A) = (\<Sum>i\<in>A. f i i) + (\<Sum>i\<in>A. sum (f i) (A - {i}))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i\<in>A. sum (f i) A) = (\<Sum>i\<in>A. f i i) + (\<Sum>i\<in>A. sum (f i) (A - {i}))
[PROOF STEP]
have "\<And> i. i \<in> A \<Longrightarrow> (\<Sum> j \<in> A . f i j) = f i i + (\<Sum> j \<in> (A - {i}) . f i j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> A \<Longrightarrow> sum (f i) A = f i i + sum (f i) (A - {i})
[PROOF STEP]
using sum.remove assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; ?x \<in> ?A\<rbrakk> \<Longrightarrow> sum ?g ?A = ?g ?x + sum ?g (?A - {?x})
finite A

goal (1 subgoal):
 1. \<And>i. i \<in> A \<Longrightarrow> sum (f i) A = f i i + sum (f i) (A - {i})
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?i1 \<in> A \<Longrightarrow> sum (f ?i1) A = f ?i1 ?i1 + sum (f ?i1) (A - {?i1})

goal (1 subgoal):
 1. (\<Sum>i\<in>A. sum (f i) A) = (\<Sum>i\<in>A. f i i) + (\<Sum>i\<in>A. sum (f i) (A - {i}))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?i1 \<in> A \<Longrightarrow> sum (f ?i1) A = f ?i1 ?i1 + sum (f ?i1) (A - {?i1})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?i1 \<in> A \<Longrightarrow> sum (f ?i1) A = f ?i1 ?i1 + sum (f ?i1) (A - {?i1})

goal (1 subgoal):
 1. (\<Sum>i\<in>A. sum (f i) A) = (\<Sum>i\<in>A. f i i) + (\<Sum>i\<in>A. sum (f i) (A - {i}))
[PROOF STEP]
by (simp add: sum.distrib)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>A. sum (f i) A) = (\<Sum>i\<in>A. f i i) + (\<Sum>i\<in>A. sum (f i) (A - {i}))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma double_sum_split_case2: "(\<Sum> i \<in> A . (\<Sum> j \<in> A . g i j)) =
  (\<Sum> i \<in> A . (g i i)) + (\<Sum> i \<in> A . (\<Sum> j \<in> {a \<in> A . a \<noteq> i} . g i j)) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>A. sum (g i) A) = (\<Sum>i\<in>A. g i i) + (\<Sum>i\<in>A. sum (g i) {a \<in> A. a \<noteq> i})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i\<in>A. sum (g i) A) = (\<Sum>i\<in>A. g i i) + (\<Sum>i\<in>A. sum (g i) {a \<in> A. a \<noteq> i})
[PROOF STEP]
have "\<And> i. A = {a \<in> A . a = i} \<union> {a \<in> A . a \<noteq> i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. A = {a \<in> A. a = i} \<union> {a \<in> A. a \<noteq> i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A = {a \<in> A. a = ?i1} \<union> {a \<in> A. a \<noteq> ?i1}

goal (1 subgoal):
 1. (\<Sum>i\<in>A. sum (g i) A) = (\<Sum>i\<in>A. g i i) + (\<Sum>i\<in>A. sum (g i) {a \<in> A. a \<noteq> i})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A = {a \<in> A. a = ?i1} \<union> {a \<in> A. a \<noteq> ?i1}
[PROOF STEP]
have part: "\<And> i. i \<in> A \<Longrightarrow> A = {i} \<union> {a \<in> A . a \<noteq> i}"
[PROOF STATE]
proof (prove)
using this:
A = {a \<in> A. a = ?i1} \<union> {a \<in> A. a \<noteq> ?i1}

goal (1 subgoal):
 1. \<And>i. i \<in> A \<Longrightarrow> A = {i} \<union> {a \<in> A. a \<noteq> i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i1 \<in> A \<Longrightarrow> A = {?i1} \<union> {a \<in> A. a \<noteq> ?i1}

goal (1 subgoal):
 1. (\<Sum>i\<in>A. sum (g i) A) = (\<Sum>i\<in>A. g i i) + (\<Sum>i\<in>A. sum (g i) {a \<in> A. a \<noteq> i})
[PROOF STEP]
have empt:"\<And> i. {i} \<inter> {a \<in> A . a \<noteq> i} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. {i} \<inter> {a \<in> A. a \<noteq> i} = {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{?i1} \<inter> {a \<in> A. a \<noteq> ?i1} = {}

goal (1 subgoal):
 1. (\<Sum>i\<in>A. sum (g i) A) = (\<Sum>i\<in>A. g i i) + (\<Sum>i\<in>A. sum (g i) {a \<in> A. a \<noteq> i})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{?i1} \<inter> {a \<in> A. a \<noteq> ?i1} = {}
[PROOF STEP]
have "(\<Sum> i \<in> A . (\<Sum> j \<in> A . g i j)) =
    (\<Sum> i \<in> A . ((\<Sum> j \<in> {i} . g i j) + (\<Sum> j \<in> {a \<in> A . a \<noteq> i} . g i j)))"
[PROOF STATE]
proof (prove)
using this:
{?i1} \<inter> {a \<in> A. a \<noteq> ?i1} = {}

goal (1 subgoal):
 1. (\<Sum>i\<in>A. sum (g i) A) = (\<Sum>i\<in>A. sum (g i) {i} + sum (g i) {a \<in> A. a \<noteq> i})
[PROOF STEP]
using part
[PROOF STATE]
proof (prove)
using this:
{?i1} \<inter> {a \<in> A. a \<noteq> ?i1} = {}
?i1 \<in> A \<Longrightarrow> A = {?i1} \<union> {a \<in> A. a \<noteq> ?i1}

goal (1 subgoal):
 1. (\<Sum>i\<in>A. sum (g i) A) = (\<Sum>i\<in>A. sum (g i) {i} + sum (g i) {a \<in> A. a \<noteq> i})
[PROOF STEP]
by (smt (verit) finite_Un local.sum.cong local.sum.infinite local.sum.union_disjoint)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>A. sum (g i) A) = (\<Sum>i\<in>A. sum (g i) {i} + sum (g i) {a \<in> A. a \<noteq> i})

goal (1 subgoal):
 1. (\<Sum>i\<in>A. sum (g i) A) = (\<Sum>i\<in>A. g i i) + (\<Sum>i\<in>A. sum (g i) {a \<in> A. a \<noteq> i})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>A. sum (g i) A) = (\<Sum>i\<in>A. sum (g i) {i} + sum (g i) {a \<in> A. a \<noteq> i})

goal (1 subgoal):
 1. (\<Sum>i\<in>A. sum (g i) A) = (\<Sum>i\<in>A. g i i) + (\<Sum>i\<in>A. sum (g i) {a \<in> A. a \<noteq> i})
[PROOF STEP]
have "... = (\<Sum> i \<in> A . ((\<Sum> j \<in> {i} . g i j))) + (\<Sum> i \<in> A . (\<Sum> j \<in> {a \<in> A . a \<noteq> i} . g i j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>A. sum (g i) {i} + sum (g i) {a \<in> A. a \<noteq> i}) = (\<Sum>i\<in>A. sum (g i) {i}) + (\<Sum>i\<in>A. sum (g i) {a \<in> A. a \<noteq> i})
[PROOF STEP]
by (simp add: local.sum.distrib)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>A. sum (g i) {i} + sum (g i) {a \<in> A. a \<noteq> i}) = (\<Sum>i\<in>A. sum (g i) {i}) + (\<Sum>i\<in>A. sum (g i) {a \<in> A. a \<noteq> i})

goal (1 subgoal):
 1. (\<Sum>i\<in>A. sum (g i) A) = (\<Sum>i\<in>A. g i i) + (\<Sum>i\<in>A. sum (g i) {a \<in> A. a \<noteq> i})
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i\<in>A. sum (g i) A) = (\<Sum>i\<in>A. sum (g i) {i}) + (\<Sum>i\<in>A. sum (g i) {a \<in> A. a \<noteq> i})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>A. sum (g i) A) = (\<Sum>i\<in>A. sum (g i) {i}) + (\<Sum>i\<in>A. sum (g i) {a \<in> A. a \<noteq> i})

goal (1 subgoal):
 1. (\<Sum>i\<in>A. sum (g i) A) = (\<Sum>i\<in>A. g i i) + (\<Sum>i\<in>A. sum (g i) {a \<in> A. a \<noteq> i})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>A. sum (g i) A) = (\<Sum>i\<in>A. g i i) + (\<Sum>i\<in>A. sum (g i) {a \<in> A. a \<noteq> i})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma double_sum_split_case_square:
  assumes "finite A"
  shows "(\<Sum> i \<in> A . f i )^2 = (\<Sum> i \<in> A . (f i * f i)) + (\<Sum> i \<in> A . (\<Sum> j \<in> (A - {i}) . f i * f j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sum f A)\<^sup>2 = (\<Sum>i\<in>A. f i * f i) + (\<Sum>i\<in>A. \<Sum>j\<in>A - {i}. f i * f j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (sum f A)\<^sup>2 = (\<Sum>i\<in>A. f i * f i) + (\<Sum>i\<in>A. \<Sum>j\<in>A - {i}. f i * f j)
[PROOF STEP]
have "(\<Sum> i \<in> A . f i )^2 = (\<Sum> i \<in> A . f i) * (\<Sum> i \<in> A . f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sum f A)\<^sup>2 = sum f A * sum f A
[PROOF STEP]
using power2_eq_square
[PROOF STATE]
proof (prove)
using this:
?a\<^sup>2 = ?a * ?a

goal (1 subgoal):
 1. (sum f A)\<^sup>2 = sum f A * sum f A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(sum f A)\<^sup>2 = sum f A * sum f A

goal (1 subgoal):
 1. (sum f A)\<^sup>2 = (\<Sum>i\<in>A. f i * f i) + (\<Sum>i\<in>A. \<Sum>j\<in>A - {i}. f i * f j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(sum f A)\<^sup>2 = sum f A * sum f A
[PROOF STEP]
have "(\<Sum> i \<in> A . f i) * (\<Sum> i \<in> A . f i) = (\<Sum> i \<in> A . f i) * (\<Sum> j \<in> A . f j)"
[PROOF STATE]
proof (prove)
using this:
(sum f A)\<^sup>2 = sum f A * sum f A

goal (1 subgoal):
 1. sum f A * sum f A = sum f A * sum f A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum f A * sum f A = sum f A * sum f A

goal (1 subgoal):
 1. (sum f A)\<^sup>2 = (\<Sum>i\<in>A. f i * f i) + (\<Sum>i\<in>A. \<Sum>j\<in>A - {i}. f i * f j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum f A * sum f A = sum f A * sum f A

goal (1 subgoal):
 1. (sum f A)\<^sup>2 = (\<Sum>i\<in>A. f i * f i) + (\<Sum>i\<in>A. \<Sum>j\<in>A - {i}. f i * f j)
[PROOF STEP]
have 1: "... = (\<Sum> i \<in> A . f i * (\<Sum> j \<in> A . f j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f A * sum f A = (\<Sum>i\<in>A. f i * sum f A)
[PROOF STEP]
using sum_distrib_right
[PROOF STATE]
proof (prove)
using this:
sum ?f ?A * ?r = (\<Sum>n\<in>?A. ?f n * ?r)

goal (1 subgoal):
 1. sum f A * sum f A = (\<Sum>i\<in>A. f i * sum f A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum f A * sum f A = (\<Sum>i\<in>A. f i * sum f A)

goal (1 subgoal):
 1. (sum f A)\<^sup>2 = (\<Sum>i\<in>A. f i * f i) + (\<Sum>i\<in>A. \<Sum>j\<in>A - {i}. f i * f j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum f A * sum f A = (\<Sum>i\<in>A. f i * sum f A)

goal (1 subgoal):
 1. (sum f A)\<^sup>2 = (\<Sum>i\<in>A. f i * f i) + (\<Sum>i\<in>A. \<Sum>j\<in>A - {i}. f i * f j)
[PROOF STEP]
have 2: "... = (\<Sum> i \<in> A .  (\<Sum> j \<in> A . f i * f j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>A. f i * sum f A) = (\<Sum>i\<in>A. \<Sum>j\<in>A. f i * f j)
[PROOF STEP]
using sum_distrib_left
[PROOF STATE]
proof (prove)
using this:
?r * sum ?f ?A = (\<Sum>n\<in>?A. ?r * ?f n)

goal (1 subgoal):
 1. (\<Sum>i\<in>A. f i * sum f A) = (\<Sum>i\<in>A. \<Sum>j\<in>A. f i * f j)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>A. f i * sum f A) = (\<Sum>i\<in>A. \<Sum>j\<in>A. f i * f j)

goal (1 subgoal):
 1. (sum f A)\<^sup>2 = (\<Sum>i\<in>A. f i * f i) + (\<Sum>i\<in>A. \<Sum>j\<in>A - {i}. f i * f j)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i\<in>A. \<Sum>j\<in>A. f i * f j) = (\<Sum>i\<in>A. \<Sum>j\<in>A. f i * f j)
[PROOF STEP]
have "(\<Sum> i \<in> A . f i) * (\<Sum> i \<in> A . f i) =
    (\<Sum> i \<in> A . (f i * f i)) + (\<Sum> i \<in> A . (\<Sum> j \<in> (A - {i}) . f i * f j))"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>A. \<Sum>j\<in>A. f i * f j) = (\<Sum>i\<in>A. \<Sum>j\<in>A. f i * f j)

goal (1 subgoal):
 1. sum f A * sum f A = (\<Sum>i\<in>A. f i * f i) + (\<Sum>i\<in>A. \<Sum>j\<in>A - {i}. f i * f j)
[PROOF STEP]
using assms double_sum_split_case[of "A" "\<lambda> i j . f i * f j"] 1 2
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>A. \<Sum>j\<in>A. f i * f j) = (\<Sum>i\<in>A. \<Sum>j\<in>A. f i * f j)
finite A
finite A \<Longrightarrow> (\<Sum>i\<in>A. \<Sum>j\<in>A. f i * f j) = (\<Sum>i\<in>A. f i * f i) + (\<Sum>i\<in>A. \<Sum>j\<in>A - {i}. f i * f j)
sum f A * sum f A = (\<Sum>i\<in>A. f i * sum f A)
(\<Sum>i\<in>A. f i * sum f A) = (\<Sum>i\<in>A. \<Sum>j\<in>A. f i * f j)

goal (1 subgoal):
 1. sum f A * sum f A = (\<Sum>i\<in>A. f i * f i) + (\<Sum>i\<in>A. \<Sum>j\<in>A - {i}. f i * f j)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
sum f A * sum f A = (\<Sum>i\<in>A. f i * f i) + (\<Sum>i\<in>A. \<Sum>j\<in>A - {i}. f i * f j)

goal (1 subgoal):
 1. (sum f A)\<^sup>2 = (\<Sum>i\<in>A. f i * f i) + (\<Sum>i\<in>A. \<Sum>j\<in>A - {i}. f i * f j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sum f A * sum f A = (\<Sum>i\<in>A. f i * f i) + (\<Sum>i\<in>A. \<Sum>j\<in>A - {i}. f i * f j)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum f A * sum f A = (\<Sum>i\<in>A. f i * f i) + (\<Sum>i\<in>A. \<Sum>j\<in>A - {i}. f i * f j)

goal (1 subgoal):
 1. (sum f A)\<^sup>2 = (\<Sum>i\<in>A. f i * f i) + (\<Sum>i\<in>A. \<Sum>j\<in>A - {i}. f i * f j)
[PROOF STEP]
using power2_eq_square
[PROOF STATE]
proof (prove)
using this:
sum f A * sum f A = (\<Sum>i\<in>A. f i * f i) + (\<Sum>i\<in>A. \<Sum>j\<in>A - {i}. f i * f j)
?a\<^sup>2 = ?a * ?a

goal (1 subgoal):
 1. (sum f A)\<^sup>2 = (\<Sum>i\<in>A. f i * f i) + (\<Sum>i\<in>A. \<Sum>j\<in>A - {i}. f i * f j)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
(sum f A)\<^sup>2 = (\<Sum>i\<in>A. f i * f i) + (\<Sum>i\<in>A. \<Sum>j\<in>A - {i}. f i * f j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma double_sum_split_square_diff:  "finite {0..<x} \<Longrightarrow>
  (\<Sum> i \<in> {0..<x} . (\<Sum> j \<in> ({0..< x} - {i}) . c i * c j)) =
  (\<Sum> i \<in> {0..<x} . c i)^2 - (\<Sum> i \<in> {0..<x} . c i * c i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {0::'b..<x} \<Longrightarrow> (\<Sum>i = 0::'b..<x. \<Sum>j\<in>{0::'b..<x} - {i}. c i * c j) = (sum c {0::'b..<x})\<^sup>2 - (\<Sum>i = 0::'b..<x. c i * c i)
[PROOF STEP]
using double_sum_split_case_square[of "{0..<x}" "\<lambda> i. c i"]
[PROOF STATE]
proof (prove)
using this:
finite {0::'b..<x} \<Longrightarrow> (sum c {0::'b..<x})\<^sup>2 = (\<Sum>i = 0::'b..<x. c i * c i) + (\<Sum>i = 0::'b..<x. \<Sum>j\<in>{0::'b..<x} - {i}. c i * c j)

goal (1 subgoal):
 1. finite {0::'b..<x} \<Longrightarrow> (\<Sum>i = 0::'b..<x. \<Sum>j\<in>{0::'b..<x} - {i}. c i * c j) = (sum c {0::'b..<x})\<^sup>2 - (\<Sum>i = 0::'b..<x. c i * c i)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma swap_swap : "swap i j (swap i j x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swap i j (swap i j x) = x
[PROOF STEP]
unfolding swap_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if (if x = i then j else if x = j then i else x) = i then j else if (if x = i then j else if x = j then i else x) = j then i else if x = i then j else if x = j then i else x) = x
[PROOF STEP]
by auto


[STATEMENT]
lemma finite_swap_ne: "finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (swap b i x) \<noteq> c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (swap b i x) \<noteq> c}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (swap b i x) \<noteq> c}
[PROOF STEP]
assume finset: "finite {x. f x \<noteq> c}"
[PROOF STATE]
proof (state)
this:
finite {x. f x \<noteq> c}

goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (swap b i x) \<noteq> c}
[PROOF STEP]
let ?A = "{x. f x \<noteq> c}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (swap b i x) \<noteq> c}
[PROOF STEP]
let ?B = "{x. f (swap b i x) \<noteq> c}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (swap b i x) \<noteq> c}
[PROOF STEP]
have finsubset: "finite (?A - {i, b})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ({x. f x \<noteq> c} - {i, b})
[PROOF STEP]
using finset
[PROOF STATE]
proof (prove)
using this:
finite {x. f x \<noteq> c}

goal (1 subgoal):
 1. finite ({x. f x \<noteq> c} - {i, b})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite ({x. f x \<noteq> c} - {i, b})

goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (swap b i x) \<noteq> c}
[PROOF STEP]
have sames: "(?A - {i, b}) = (?B - {i, b})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. f x \<noteq> c} - {i, b} = {x. f (swap b i x) \<noteq> c} - {i, b}
[PROOF STEP]
unfolding swap_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. f x \<noteq> c} - {i, b} = {x. f (if x = b then i else if x = i then b else x) \<noteq> c} - {i, b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x. f x \<noteq> c} - {i, b} = {x. f (swap b i x) \<noteq> c} - {i, b}

goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (swap b i x) \<noteq> c}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{x. f x \<noteq> c} - {i, b} = {x. f (swap b i x) \<noteq> c} - {i, b}
[PROOF STEP]
have "finite (?B - {i, b})"
[PROOF STATE]
proof (prove)
using this:
{x. f x \<noteq> c} - {i, b} = {x. f (swap b i x) \<noteq> c} - {i, b}

goal (1 subgoal):
 1. finite ({x. f (swap b i x) \<noteq> c} - {i, b})
[PROOF STEP]
using finsubset
[PROOF STATE]
proof (prove)
using this:
{x. f x \<noteq> c} - {i, b} = {x. f (swap b i x) \<noteq> c} - {i, b}
finite ({x. f x \<noteq> c} - {i, b})

goal (1 subgoal):
 1. finite ({x. f (swap b i x) \<noteq> c} - {i, b})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite ({x. f (swap b i x) \<noteq> c} - {i, b})

goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (swap b i x) \<noteq> c}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite ({x. f (swap b i x) \<noteq> c} - {i, b})
[PROOF STEP]
have finBset: "finite ((?B - {i, b}) \<union> {i, b})"
[PROOF STATE]
proof (prove)
using this:
finite ({x. f (swap b i x) \<noteq> c} - {i, b})

goal (1 subgoal):
 1. finite ({x. f (swap b i x) \<noteq> c} - {i, b} \<union> {i, b})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite ({x. f (swap b i x) \<noteq> c} - {i, b} \<union> {i, b})

goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (swap b i x) \<noteq> c}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite ({x. f (swap b i x) \<noteq> c} - {i, b} \<union> {i, b})
[PROOF STEP]
have "?B \<subseteq> ((?B - {i, b}) \<union> {i, b})"
[PROOF STATE]
proof (prove)
using this:
finite ({x. f (swap b i x) \<noteq> c} - {i, b} \<union> {i, b})

goal (1 subgoal):
 1. {x. f (swap b i x) \<noteq> c} \<subseteq> {x. f (swap b i x) \<noteq> c} - {i, b} \<union> {i, b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x. f (swap b i x) \<noteq> c} \<subseteq> {x. f (swap b i x) \<noteq> c} - {i, b} \<union> {i, b}

goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (swap b i x) \<noteq> c}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{x. f (swap b i x) \<noteq> c} \<subseteq> {x. f (swap b i x) \<noteq> c} - {i, b} \<union> {i, b}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{x. f (swap b i x) \<noteq> c} \<subseteq> {x. f (swap b i x) \<noteq> c} - {i, b} \<union> {i, b}

goal (1 subgoal):
 1. finite {x. f (swap b i x) \<noteq> c}
[PROOF STEP]
using finBset
[PROOF STATE]
proof (prove)
using this:
{x. f (swap b i x) \<noteq> c} \<subseteq> {x. f (swap b i x) \<noteq> c} - {i, b} \<union> {i, b}
finite ({x. f (swap b i x) \<noteq> c} - {i, b} \<union> {i, b})

goal (1 subgoal):
 1. finite {x. f (swap b i x) \<noteq> c}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {x. f (swap b i x) \<noteq> c}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma swap0_swap0: "swap0 n i (swap0 n i x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swap0 n i (swap0 n i x) = x
[PROOF STEP]
by transfer (force simp: swap_def)


[STATEMENT]
lemma inj_swap: "inj (swap b i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (swap b i)
[PROOF STEP]
using swap_swap
[PROOF STATE]
proof (prove)
using this:
swap ?i ?j (swap ?i ?j ?x) = ?x

goal (1 subgoal):
 1. inj (swap b i)
[PROOF STEP]
by (rule inj_on_inverseI)


[STATEMENT]
lemma inj_swap0: "inj (swap0 b i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (swap0 b i)
[PROOF STEP]
using swap0_swap0
[PROOF STATE]
proof (prove)
using this:
swap0 ?n ?i (swap0 ?n ?i ?x) = ?x

goal (1 subgoal):
 1. inj (swap0 b i)
[PROOF STEP]
by (rule inj_on_inverseI)


[STATEMENT]
lemma swap0_eq: "lookup (swap0 b i p) x = lookup p (swap b i x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (swap0 b i p) x = lookup p (swap b i x)
[PROOF STEP]
by (simp_all add: swap0.rep_eq)


[STATEMENT]
lemma eq_onp_swap : "eq_onp (\<lambda>f. finite {x. f x \<noteq> 0}) (\<lambda>x. lookup m (swap b i x))
   (\<lambda>x. lookup m (swap b i x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_onp (\<lambda>f. finite {x. f x \<noteq> (0::'b)}) (\<lambda>x. lookup m (swap b i x)) (\<lambda>x. lookup m (swap b i x))
[PROOF STEP]
unfolding eq_onp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {x. lookup m (swap b i x) \<noteq> (0::'b)} \<and> (\<lambda>x. lookup m (swap b i x)) = (\<lambda>x. lookup m (swap b i x))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {x. lookup m (swap b i x) \<noteq> (0::'b)}
[PROOF STEP]
apply(rule finite_swap_ne)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {x. lookup m x \<noteq> (0::'b)}
[PROOF STEP]
by auto


[STATEMENT]
lemma keys_swap: "keys (swap0 b i m) = swap b i ` keys m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys (swap0 b i m) = swap b i ` keys m
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> keys (swap0 b i m) \<Longrightarrow> x \<in> swap b i ` keys m
 2. \<And>x xa. xa \<in> keys m \<Longrightarrow> swap b i xa \<in> keys (swap0 b i m)
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> keys (swap0 b i m) \<Longrightarrow> x \<in> swap b i ` keys m
[PROOF STEP]
unfolding swap0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> keys (map_fun id (map_fun id (map_fun lookup Abs_poly_mapping)) (\<lambda>b i p x. p (swap b i x)) b i m) \<Longrightarrow> x \<in> swap b i ` keys m
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> keys (Abs_poly_mapping (\<lambda>x. lookup m (swap b i x))) \<Longrightarrow> x \<in> swap b i ` keys m
[PROOF STEP]
unfolding keys.abs_eq[OF eq_onp_swap]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> {k. lookup m (swap b i k) \<noteq> (0::'a)} \<Longrightarrow> x \<in> swap b i ` keys m
[PROOF STEP]
by (metis (mono_tags, lifting) Reindex.swap_swap image_eqI lookupNotIn mem_Collect_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. xa \<in> keys m \<Longrightarrow> swap b i xa \<in> keys (swap0 b i m)
[PROOF STEP]
subgoal for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> keys m \<Longrightarrow> swap b i y \<in> keys (swap0 b i m)
[PROOF STEP]
unfolding swap0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> keys m \<Longrightarrow> swap b i y \<in> keys (map_fun id (map_fun id (map_fun lookup Abs_poly_mapping)) (\<lambda>b i p x. p (swap b i x)) b i m)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> keys m \<Longrightarrow> swap b i y \<in> keys (Abs_poly_mapping (\<lambda>x. lookup m (swap b i x)))
[PROOF STEP]
unfolding keys.abs_eq[OF eq_onp_swap]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> keys m \<Longrightarrow> swap b i y \<in> {k. lookup m (swap b i k) \<noteq> (0::'a)}
[PROOF STEP]
by (metis (mono_tags, lifting) Reindex.swap_swap lookup_eq_zero_in_keys_contradict mem_Collect_eq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma compute_swap\<^sub>f[code]: "swap\<^sub>f b i (fmap_of_list xs) =
  fmap_of_list (map (\<lambda>(k, v). (swap b i k, v)) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swap\<^sub>f b i (fmap_of_list xs) = fmap_of_list (map (\<lambda>(k, v). (swap b i k, v)) xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. swap\<^sub>f b i (fmap_of_list xs) = fmap_of_list (map (\<lambda>(k, v). (swap b i k, v)) xs)
[PROOF STEP]
have *: "map_of (map (\<lambda>(k, y). (swap b i k, y)) (xs)) x =
    map_of xs (swap b i x)"
    for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (map (\<lambda>(k, y). (swap b i k, y)) xs) x = map_of xs (swap b i x)
[PROOF STEP]
apply (rule map_of_map_key_inverse_fun_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set xs \<Longrightarrow> swap b i (swap b i (fst x)) = fst x
 2. swap b i (swap b i x) = x
[PROOF STEP]
unfolding swap_swap
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set xs \<Longrightarrow> fst x = fst x
 2. x = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map_of (map (\<lambda>(k, y). (swap b i k, y)) xs) ?x = map_of xs (swap b i ?x)

goal (1 subgoal):
 1. swap\<^sub>f b i (fmap_of_list xs) = fmap_of_list (map (\<lambda>(k, v). (swap b i k, v)) xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swap\<^sub>f b i (fmap_of_list xs) = fmap_of_list (map (\<lambda>(k, v). (swap b i k, v)) xs)
[PROOF STEP]
unfolding swap\<^sub>f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_fun id (map_fun id (map_fun fmlookup Abs_fmap)) (\<lambda>b i p x. p (swap b i x)) b i (fmap_of_list xs) = fmap_of_list (map (\<lambda>(k, v). (swap b i k, v)) xs)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_fmap (\<lambda>x. fmlookup (fmap_of_list xs) (swap b i x)) = fmap_of_list (map (\<lambda>(k, v). (swap b i k, v)) xs)
[PROOF STEP]
unfolding fmlookup_of_list
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_fmap (\<lambda>x. map_of xs (swap b i x)) = fmap_of_list (map (\<lambda>(k, v). (swap b i k, v)) xs)
[PROOF STEP]
unfolding Finite_Map.fmap_of_list.abs_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_fmap (\<lambda>x. map_of xs (swap b i x)) = Abs_fmap (map_of (map (\<lambda>(k, y). (swap b i k, y)) xs))
[PROOF STEP]
using map_of_map_key_inverse_fun_eq[where f="swap b i", where g="swap b i", where xs=xs]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> swap b i (swap b i (fst x)) = fst x; swap b i (swap b i ?x) = ?x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(k, y). (swap b i k, y)) xs) ?x = map_of xs (swap b i ?x)

goal (1 subgoal):
 1. Abs_fmap (\<lambda>x. map_of xs (swap b i x)) = Abs_fmap (map_of (map (\<lambda>(k, y). (swap b i k, y)) xs))
[PROOF STEP]
unfolding swap_swap
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> fst x = fst x; ?x = ?x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(k, y). (swap b i k, y)) xs) ?x = map_of xs (swap b i ?x)

goal (1 subgoal):
 1. Abs_fmap (\<lambda>x. map_of xs (swap b i x)) = Abs_fmap (map_of (map (\<lambda>(k, y). (swap b i k, y)) xs))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. map_of (map (\<lambda>(k, y). (swap b i k, y)) xs) x = map_of xs (swap b i x)) \<Longrightarrow> Abs_fmap (\<lambda>x. map_of xs (swap b i x)) = Abs_fmap (map_of (map (\<lambda>(k, y). (swap b i k, y)) xs))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
swap\<^sub>f b i (fmap_of_list xs) = fmap_of_list (map (\<lambda>(k, v). (swap b i k, v)) xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma compute_swap[code]: "swap0 n i (Pm_fmap xs) = Pm_fmap (swap\<^sub>f n i xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swap0 n i (Pm_fmap xs) = Pm_fmap (swap\<^sub>f n i xs)
[PROOF STEP]
apply(rule poly_mapping_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. lookup (swap0 n i (Pm_fmap xs)) k = lookup (Pm_fmap (swap\<^sub>f n i xs)) k
[PROOF STEP]
by  (auto simp: swap\<^sub>f.rep_eq swap0.rep_eq fmlookup_default_def swap_def
      split: option.splits)


[STATEMENT]
lemma swap_zero[simp]: "swap0 b i 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swap0 b i 0 = 0
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma keys_swap\<^sub>0: "keys (swapPoly\<^sub>0 b i mp) = swap0 b i ` (keys mp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys (swapPoly\<^sub>0 b i mp) = swap0 b i ` keys mp
[PROOF STEP]
apply (auto )
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> keys (swapPoly\<^sub>0 b i mp) \<Longrightarrow> x \<in> swap0 b i ` keys mp
 2. \<And>xa. xa \<in> keys mp \<Longrightarrow> swap0 b i xa \<in> keys (swapPoly\<^sub>0 b i mp)
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> keys (swapPoly\<^sub>0 b i mp) \<Longrightarrow> x \<in> swap0 b i ` keys mp
[PROOF STEP]
apply (rule image_eqI[where x="swap0 b i x"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<in> keys (swapPoly\<^sub>0 b i mp) \<Longrightarrow> x = swap0 b i (swap0 b i x)
 2. x \<in> keys (swapPoly\<^sub>0 b i mp) \<Longrightarrow> swap0 b i x \<in> keys mp
[PROOF STEP]
by (auto simp: swap0_swap0 in_keys_iff swapPoly\<^sub>0.rep_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> keys mp \<Longrightarrow> swap0 b i xa \<in> keys (swapPoly\<^sub>0 b i mp)
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> keys mp \<Longrightarrow> swap0 b i x \<in> keys (swapPoly\<^sub>0 b i mp)
[PROOF STEP]
apply (auto simp: in_keys_iff swapPoly\<^sub>0.rep_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lookup mp x \<noteq> (0::'a); lookup mp (swap0 b i (swap0 b i x)) = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (simp add: swap0_swap0)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma compute_swapPoly\<^sub>0[code]: "swapPoly\<^sub>0 n i (Pm_fmap m) = Pm_fmap (swapPoly\<^sub>f n i m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swapPoly\<^sub>0 n i (Pm_fmap m) = Pm_fmap (swapPoly\<^sub>f n i m)
[PROOF STEP]
by (auto simp: swapPoly\<^sub>0.rep_eq fmlookup_default_def swapPoly\<^sub>f.rep_eq
      split: option.splits
      intro!: poly_mapping_eqI)


[STATEMENT]
lemma compute_swapPoly\<^sub>f[code]: "swapPoly\<^sub>f n i (fmap_of_list xs) =
  (fmap_of_list (map (\<lambda>(mon, c). (swap0 n i mon, c))
    xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swapPoly\<^sub>f n i (fmap_of_list xs) = fmap_of_list (map (\<lambda>(mon, c). (swap0 n i mon, c)) xs)
[PROOF STEP]
apply (rule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmap_of_list (map (\<lambda>(mon, c). (swap0 n i mon, c)) xs) = swapPoly\<^sub>f n i (fmap_of_list xs)
[PROOF STEP]
apply (rule fmap_ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. fmlookup (fmap_of_list (map (\<lambda>(mon, c). (swap0 n i mon, c)) xs)) x = fmlookup (swapPoly\<^sub>f n i (fmap_of_list xs)) x
[PROOF STEP]
unfolding swapPoly\<^sub>f.rep_eq fmlookup_of_list
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. map_of (map (\<lambda>(mon, y). (swap0 n i mon, y)) xs) x = map_of xs (swap0 n i x)
[PROOF STEP]
apply (subst map_of_map_key_inverse_fun_eq[where g="swap0 n i"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa. xa \<in> set xs \<Longrightarrow> swap0 n i (swap0 n i (fst xa)) = fst xa
 2. \<And>x. swap0 n i (swap0 n i x) = x
 3. \<And>x. map_of xs (swap0 n i x) = map_of xs (swap0 n i x)
[PROOF STEP]
unfolding swap0_swap0
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa. xa \<in> set xs \<Longrightarrow> fst xa = fst xa
 2. \<And>x. x = x
 3. \<And>x. map_of xs (swap0 n i x) = map_of xs (swap0 n i x)
[PROOF STEP]
by auto


[STATEMENT]
lemma coeff_swap_poly: "MPoly_Type.coeff (swap_poly b i mp) x = MPoly_Type.coeff mp (swap0 b i x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (swap_poly b i mp) x = MPoly_Type.coeff mp (swap0 b i x)
[PROOF STEP]
by (transfer') (simp add: swapPoly\<^sub>0.rep_eq)


[STATEMENT]
lemma monomials_swap_poly: "monomials (swap_poly b i mp) = swap0 b i ` (monomials mp) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monomials (swap_poly b i mp) = swap0 b i ` monomials mp
[PROOF STEP]
by transfer' (simp add: keys_swap\<^sub>0)


[STATEMENT]
lemma swap_list_cons: "swap_list (Suc a) (Suc b) (x # L) = x # swap_list a b L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swap_list (Suc a) (Suc b) (x # L) = x # swap_list a b L
[PROOF STEP]
by auto


[STATEMENT]
lemma inj_on : "inj_on (swap0 a b) (monomials p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (swap0 a b) (monomials p)
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>monomials p. \<forall>y\<in>monomials p. swap0 a b x = swap0 a b y \<longrightarrow> x = y
[PROOF STEP]
by (metis swap0_swap0)


[STATEMENT]
lemma inj_on' : "inj_on (swap a b) (keys m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (swap a b) (keys m)
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>keys m. \<forall>y\<in>keys m. swap a b x = swap a b y \<longrightarrow> x = y
[PROOF STEP]
by (meson Reindex.inj_swap injD)


[STATEMENT]
lemma swap_list :
  assumes  "a < length L"
  assumes "b < length L"
  shows "nth_default 0 (L[b := L ! a, a := L ! b]) (swap a b xa) = nth_default 0 L xa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_default (0::'a) (L[b := L ! a, a := L ! b]) (swap a b xa) = nth_default (0::'a) L xa
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a < length L
b < length L

goal (1 subgoal):
 1. nth_default (0::'a) (L[b := L ! a, a := L ! b]) (swap a b xa) = nth_default (0::'a) L xa
[PROOF STEP]
unfolding swap_def
[PROOF STATE]
proof (prove)
using this:
a < length L
b < length L

goal (1 subgoal):
 1. nth_default (0::'a) (L[b := L ! a, a := L ! b]) (if xa = a then b else if xa = b then a else xa) = nth_default (0::'a) L xa
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a < length L; b < length L; xa = b; b \<noteq> a\<rbrakk> \<Longrightarrow> nth_default (0::'a) (L[b := L ! a, a := L ! b]) a = nth_default (0::'a) L b
 2. \<lbrakk>a < length L; b < length L; a \<noteq> b; xa = a\<rbrakk> \<Longrightarrow> nth_default (0::'a) (L[b := L ! a, a := L ! b]) b = nth_default (0::'a) L a
 3. \<lbrakk>a < length L; b < length L; xa \<noteq> b; xa \<noteq> a\<rbrakk> \<Longrightarrow> nth_default (0::'a) (L[b := L ! a, a := L ! b]) xa = nth_default (0::'a) L xa
[PROOF STEP]
apply (simp_all add: nth_default_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < length L; b < length L; xa \<noteq> b; xa \<noteq> a\<rbrakk> \<Longrightarrow> nth_default (0::'a) (L[b := L ! a, a := L ! b]) xa = nth_default (0::'a) L xa
[PROOF STEP]
by (simp add: nth_default_def)


[STATEMENT]
lemma swap_poly :
  assumes "length L > a"
  assumes "length L > b"
  shows "insertion (nth_default 0 L) p = insertion (nth_default 0 (swap_list a b L)) (swap_poly a b p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion (nth_default (0::'a) L) p = insertion (nth_default (0::'a) (swap_list a b L)) (swap_poly a b p)
[PROOF STEP]
unfolding insertion_code
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m\<in>monomials p. MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. nth_default (0::'a) L k ^ lookup m k)) = (\<Sum>m\<in>monomials (swap_poly a b p). MPoly_Type.coeff (swap_poly a b p) m * (\<Prod>k\<in>keys m. nth_default (0::'a) (swap_list a b L) k ^ lookup m k))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m\<in>monomials p. MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. nth_default (0::'a) L k ^ lookup m k)) = (\<Sum>m\<in>monomials (swap_poly a b p). MPoly_Type.coeff (swap_poly a b p) m * (\<Prod>k\<in>keys m. nth_default (0::'a) (L[b := L ! a, a := L ! b]) k ^ lookup m k))
[PROOF STEP]
unfolding monomials.abs_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m\<in>monomials p. MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. nth_default (0::'a) L k ^ lookup m k)) = (\<Sum>m\<in>monomials (swap_poly a b p). MPoly_Type.coeff (swap_poly a b p) m * (\<Prod>k\<in>keys m. nth_default (0::'a) (L[b := L ! a, a := L ! b]) k ^ lookup m k))
[PROOF STEP]
unfolding coeff_swap_poly monomials_swap_poly
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m\<in>monomials p. MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. nth_default (0::'a) L k ^ lookup m k)) = (\<Sum>m\<in>swap0 a b ` monomials p. MPoly_Type.coeff p (swap0 a b m) * (\<Prod>k\<in>keys m. nth_default (0::'a) (L[b := L ! a, a := L ! b]) k ^ lookup m k))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m\<in>monomials p. MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. nth_default (0::'a) L k ^ lookup m k)) = (\<Sum>m\<in>swap0 a b ` monomials p. MPoly_Type.coeff p (swap0 a b m) * (\<Prod>k\<in>keys m. nth_default (0::'a) (L[b := L ! a, a := L ! b]) k ^ lookup m k))
[PROOF STEP]
unfolding Groups_Big.comm_monoid_add_class.sum.reindex[OF inj_on]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m\<in>monomials p. MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. nth_default (0::'a) L k ^ lookup m k)) = sum ((\<lambda>m. MPoly_Type.coeff p (swap0 a b m) * (\<Prod>k\<in>keys m. nth_default (0::'a) (L[b := L ! a, a := L ! b]) k ^ lookup m k)) \<circ> swap0 a b) (monomials p)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m\<in>monomials p. MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. nth_default (0::'a) L k ^ lookup m k)) = (\<Sum>x\<in>monomials p. MPoly_Type.coeff p (swap0 a b (swap0 a b x)) * (\<Prod>k\<in>keys (swap0 a b x). nth_default (0::'a) (L[b := L ! a, a := L ! b]) k ^ lookup (swap0 a b x) k))
[PROOF STEP]
unfolding swap0_swap0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m\<in>monomials p. MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. nth_default (0::'a) L k ^ lookup m k)) = (\<Sum>x\<in>monomials p. MPoly_Type.coeff p x * (\<Prod>k\<in>keys (swap0 a b x). nth_default (0::'a) (L[b := L ! a, a := L ! b]) k ^ lookup (swap0 a b x) k))
[PROOF STEP]
unfolding keys_swap
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m\<in>monomials p. MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. nth_default (0::'a) L k ^ lookup m k)) = (\<Sum>x\<in>monomials p. MPoly_Type.coeff p x * (\<Prod>k\<in>swap a b ` keys x. nth_default (0::'a) (L[b := L ! a, a := L ! b]) k ^ lookup (swap0 a b x) k))
[PROOF STEP]
unfolding Groups_Big.comm_monoid_mult_class.prod.reindex[OF inj_on']
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m\<in>monomials p. MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. nth_default (0::'a) L k ^ lookup m k)) = (\<Sum>x\<in>monomials p. MPoly_Type.coeff p x * prod ((\<lambda>k. nth_default (0::'a) (L[b := L ! a, a := L ! b]) k ^ lookup (swap0 a b x) k) \<circ> swap a b) (keys x))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m\<in>monomials p. MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. nth_default (0::'a) L k ^ lookup m k)) = (\<Sum>x\<in>monomials p. MPoly_Type.coeff p x * (\<Prod>xa\<in>keys x. nth_default (0::'a) (L[b := L ! a, a := L ! b]) (swap a b xa) ^ lookup (swap0 a b x) (swap a b xa)))
[PROOF STEP]
unfolding swap0_eq swap_swap swap_list[OF assms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m\<in>monomials p. MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. nth_default (0::'a) L k ^ lookup m k)) = (\<Sum>x\<in>monomials p. MPoly_Type.coeff p x * (\<Prod>xa\<in>keys x. nth_default (0::'a) L xa ^ lookup x xa))
[PROOF STEP]
by auto