[STATEMENT]
lemma ideal_generated_mult_unit:
  assumes f: "finite S" and u: "u dvd 1"
  shows "ideal_generated ((\<lambda>x. u*x)` S) = ideal_generated S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated ((*) u ` S) = ideal_generated S
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
finite S

goal (1 subgoal):
 1. ideal_generated ((*) u ` S) = ideal_generated S
[PROOF STEP]
proof (induct S)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ideal_generated ((*) u ` {}) = ideal_generated {}
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; ideal_generated ((*) u ` F) = ideal_generated F\<rbrakk> \<Longrightarrow> ideal_generated ((*) u ` insert x F) = ideal_generated (insert x F)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. ideal_generated ((*) u ` {}) = ideal_generated {}
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; ideal_generated ((*) u ` F) = ideal_generated F\<rbrakk> \<Longrightarrow> ideal_generated ((*) u ` insert x F) = ideal_generated (insert x F)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated ((*) u ` {}) = ideal_generated {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ideal_generated ((*) u ` {}) = ideal_generated {}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; ideal_generated ((*) u ` F) = ideal_generated F\<rbrakk> \<Longrightarrow> ideal_generated ((*) u ` insert x F) = ideal_generated (insert x F)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; ideal_generated ((*) u ` F) = ideal_generated F\<rbrakk> \<Longrightarrow> ideal_generated ((*) u ` insert x F) = ideal_generated (insert x F)
[PROOF STEP]
case (insert x S)
[PROOF STATE]
proof (state)
this:
finite S
x \<notin> S
ideal_generated ((*) u ` S) = ideal_generated S

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; ideal_generated ((*) u ` F) = ideal_generated F\<rbrakk> \<Longrightarrow> ideal_generated ((*) u ` insert x F) = ideal_generated (insert x F)
[PROOF STEP]
obtain inv_u where inv_u: "inv_u * u = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>inv_u. inv_u * u = (1::'a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using u
[PROOF STATE]
proof (prove)
using this:
u dvd (1::'a)

goal (1 subgoal):
 1. (\<And>inv_u. inv_u * u = (1::'a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dvd_def
[PROOF STATE]
proof (prove)
using this:
\<exists>k. (1::'a) = u * k

goal (1 subgoal):
 1. (\<And>inv_u. inv_u * u = (1::'a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using mult_ac
[PROOF STATE]
proof (prove)
using this:
\<exists>k. (1::'a) = u * k
?a * ?b * ?c = ?a * (?b * ?c)
?a * ?b = ?b * ?a
?b * (?a * ?c) = ?a * (?b * ?c)

goal (1 subgoal):
 1. (\<And>inv_u. inv_u * u = (1::'a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inv_u * u = (1::'a)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; ideal_generated ((*) u ` F) = ideal_generated F\<rbrakk> \<Longrightarrow> ideal_generated ((*) u ` insert x F) = ideal_generated (insert x F)
[PROOF STEP]
have f: "finite (insert (u*x) ((\<lambda>x. u*x)` S))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (insert (u * x) ((*) u ` S))
[PROOF STEP]
using insert.hyps
[PROOF STATE]
proof (prove)
using this:
finite S
x \<notin> S
ideal_generated ((*) u ` S) = ideal_generated S

goal (1 subgoal):
 1. finite (insert (u * x) ((*) u ` S))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (insert (u * x) ((*) u ` S))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; ideal_generated ((*) u ` F) = ideal_generated F\<rbrakk> \<Longrightarrow> ideal_generated ((*) u ` insert x F) = ideal_generated (insert x F)
[PROOF STEP]
have f2: "finite (insert x S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (insert x S)
[PROOF STEP]
by (simp add: insert(1))
[PROOF STATE]
proof (state)
this:
finite (insert x S)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; ideal_generated ((*) u ` F) = ideal_generated F\<rbrakk> \<Longrightarrow> ideal_generated ((*) u ` insert x F) = ideal_generated (insert x F)
[PROOF STEP]
have f3: "finite S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S
[PROOF STEP]
by (simp add: insert)
[PROOF STATE]
proof (state)
this:
finite S

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; ideal_generated ((*) u ` F) = ideal_generated F\<rbrakk> \<Longrightarrow> ideal_generated ((*) u ` insert x F) = ideal_generated (insert x F)
[PROOF STEP]
have f4: "finite ((*) u ` S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ((*) u ` S)
[PROOF STEP]
by (simp add: insert)
[PROOF STATE]
proof (state)
this:
finite ((*) u ` S)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; ideal_generated ((*) u ` F) = ideal_generated F\<rbrakk> \<Longrightarrow> ideal_generated ((*) u ` insert x F) = ideal_generated (insert x F)
[PROOF STEP]
have inj_ux: "inj_on (\<lambda>x. u*x) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on ((*) u) S
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>S. \<forall>y\<in>S. u * x = u * y \<longrightarrow> x = y
[PROOF STEP]
by (auto, metis inv_u local.mult_1_left local.semiring_normalization_rules(18))
[PROOF STATE]
proof (state)
this:
inj_on ((*) u) S

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; ideal_generated ((*) u ` F) = ideal_generated F\<rbrakk> \<Longrightarrow> ideal_generated ((*) u ` insert x F) = ideal_generated (insert x F)
[PROOF STEP]
have "ideal_generated ((\<lambda>x. u*x)` (insert x S)) = ideal_generated (insert (u*x) ((\<lambda>x. u*x)` S))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated ((*) u ` insert x S) = ideal_generated (insert (u * x) ((*) u ` S))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ideal_generated ((*) u ` insert x S) = ideal_generated (insert (u * x) ((*) u ` S))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; ideal_generated ((*) u ` F) = ideal_generated F\<rbrakk> \<Longrightarrow> ideal_generated ((*) u ` insert x F) = ideal_generated (insert x F)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ideal_generated ((*) u ` insert x S) = ideal_generated (insert (u * x) ((*) u ` S))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; ideal_generated ((*) u ` F) = ideal_generated F\<rbrakk> \<Longrightarrow> ideal_generated ((*) u ` insert x F) = ideal_generated (insert x F)
[PROOF STEP]
have "... = {y. \<exists>f. (\<Sum>i\<in>insert (u*x) ((\<lambda>x. u*x)` S). f i * i) = y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated (insert (u * x) ((*) u ` S)) = {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
using ideal_explicit2[OF f]
[PROOF STATE]
proof (prove)
using this:
ideal_generated (insert (u * x) ((*) u ` S)) = {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}

goal (1 subgoal):
 1. ideal_generated (insert (u * x) ((*) u ` S)) = {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ideal_generated (insert (u * x) ((*) u ` S)) = {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; ideal_generated ((*) u ` F) = ideal_generated F\<rbrakk> \<Longrightarrow> ideal_generated ((*) u ` insert x F) = ideal_generated (insert x F)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ideal_generated (insert (u * x) ((*) u ` S)) = {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; ideal_generated ((*) u ` F) = ideal_generated F\<rbrakk> \<Longrightarrow> ideal_generated ((*) u ` insert x F) = ideal_generated (insert x F)
[PROOF STEP]
have "... = {y. \<exists>f. (\<Sum>i\<in>(insert x S). f i * i) = y}" (is "?L = ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y} = {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y} = {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
have "a \<in> ?L"  if a: "a \<in> ?R" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
obtain f where sum_rw: "(\<Sum>i\<in>(insert x S). f i * i) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. (\<Sum>i\<in>insert x S. f i * i) = a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}

goal (1 subgoal):
 1. (\<And>f. (\<Sum>i\<in>insert x S. f i * i) = a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>insert x S. f i * i) = a

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
define b where "b=(\<Sum>i\<in>S. f i * i)"
[PROOF STATE]
proof (state)
this:
b = (\<Sum>i\<in>S. f i * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
have "b \<in> ideal_generated S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in> ideal_generated S
[PROOF STEP]
unfolding b_def ideal_explicit2[OF f3]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>S. f i * i) \<in> {y. \<exists>f. (\<Sum>i\<in>S. f i * i) = y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> ideal_generated S

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
hence "b \<in> ideal_generated ((*) u ` S)"
[PROOF STATE]
proof (prove)
using this:
b \<in> ideal_generated S

goal (1 subgoal):
 1. b \<in> ideal_generated ((*) u ` S)
[PROOF STEP]
using insert.hyps(3)
[PROOF STATE]
proof (prove)
using this:
b \<in> ideal_generated S
ideal_generated ((*) u ` S) = ideal_generated S

goal (1 subgoal):
 1. b \<in> ideal_generated ((*) u ` S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> ideal_generated ((*) u ` S)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
b \<in> ideal_generated ((*) u ` S)
[PROOF STEP]
obtain g where "(\<Sum>i\<in>((*) u ` S). g i * i) = b"
[PROOF STATE]
proof (prove)
using this:
b \<in> ideal_generated ((*) u ` S)

goal (1 subgoal):
 1. (\<And>g. (\<Sum>i\<in>(*) u ` S. g i * i) = b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ideal_explicit2[OF f4]
[PROOF STATE]
proof (prove)
using this:
b \<in> {y. \<exists>f. (\<Sum>i\<in>(*) u ` S. f i * i) = y}

goal (1 subgoal):
 1. (\<And>g. (\<Sum>i\<in>(*) u ` S. g i * i) = b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>(*) u ` S. g i * i) = b

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
hence sum_rw2: "(\<Sum>i\<in>S. f i * i) = (\<Sum>i\<in>((*) u ` S). g i * i)"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>(*) u ` S. g i * i) = b

goal (1 subgoal):
 1. (\<Sum>i\<in>S. f i * i) = (\<Sum>i\<in>(*) u ` S. g i * i)
[PROOF STEP]
unfolding b_def
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>(*) u ` S. g i * i) = (\<Sum>i\<in>S. f i * i)

goal (1 subgoal):
 1. (\<Sum>i\<in>S. f i * i) = (\<Sum>i\<in>(*) u ` S. g i * i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>S. f i * i) = (\<Sum>i\<in>(*) u ` S. g i * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
let ?g = "\<lambda>i. if i = u*x then f x * inv_u else g i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
have sum_rw3: "sum ((\<lambda>i. g i * i) \<circ> (\<lambda>x. u*x)) S = sum ((\<lambda>i. ?g i * i) \<circ> (\<lambda>x. u*x)) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((\<lambda>i. g i * i) \<circ> (*) u) S = sum ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) S
[PROOF STEP]
by (rule sum.cong, auto, metis inv_u local.insert(2) local.mult_1_right
              local.mult_ac(2) local.semiring_normalization_rules(18))
[PROOF STATE]
proof (state)
this:
sum ((\<lambda>i. g i * i) \<circ> (*) u) S = sum ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) S

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
have sum_rw4: "(\<Sum>i\<in>(\<lambda>x. u*x)` S. g i * i) = sum ((\<lambda>i. g i * i) \<circ> (\<lambda>x. u*x)) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>(*) u ` S. g i * i) = sum ((\<lambda>i. g i * i) \<circ> (*) u) S
[PROOF STEP]
by (rule sum.reindex[OF inj_ux])
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>(*) u ` S. g i * i) = sum ((\<lambda>i. g i * i) \<circ> (*) u) S

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
have "a = f x * x + (\<Sum>i\<in>S. f i * i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = f x * x + (\<Sum>i\<in>S. f i * i)
[PROOF STEP]
using sum_rw local.insert(1) local.insert(2)
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>insert x S. f i * i) = a
finite S
x \<notin> S

goal (1 subgoal):
 1. a = f x * x + (\<Sum>i\<in>S. f i * i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = f x * x + (\<Sum>i\<in>S. f i * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a = f x * x + (\<Sum>i\<in>S. f i * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
have "... = f x * x + (\<Sum>i\<in>(\<lambda>x. u*x)` S. g i * i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x * x + (\<Sum>i\<in>S. f i * i) = f x * x + (\<Sum>i\<in>(*) u ` S. g i * i)
[PROOF STEP]
using sum_rw2
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>S. f i * i) = (\<Sum>i\<in>(*) u ` S. g i * i)

goal (1 subgoal):
 1. f x * x + (\<Sum>i\<in>S. f i * i) = f x * x + (\<Sum>i\<in>(*) u ` S. g i * i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f x * x + (\<Sum>i\<in>S. f i * i) = f x * x + (\<Sum>i\<in>(*) u ` S. g i * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f x * x + (\<Sum>i\<in>S. f i * i) = f x * x + (\<Sum>i\<in>(*) u ` S. g i * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
have "... = ?g (u * x) * (u * x) + (\<Sum>i\<in>(\<lambda>x. u*x)` S. g i * i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x * x + (\<Sum>i\<in>(*) u ` S. g i * i) = (if u * x = u * x then f x * inv_u else g (u * x)) * (u * x) + (\<Sum>i\<in>(*) u ` S. g i * i)
[PROOF STEP]
using inv_u
[PROOF STATE]
proof (prove)
using this:
inv_u * u = (1::'a)

goal (1 subgoal):
 1. f x * x + (\<Sum>i\<in>(*) u ` S. g i * i) = (if u * x = u * x then f x * inv_u else g (u * x)) * (u * x) + (\<Sum>i\<in>(*) u ` S. g i * i)
[PROOF STEP]
by (smt local.mult_1_right local.mult_ac(1))
[PROOF STATE]
proof (state)
this:
f x * x + (\<Sum>i\<in>(*) u ` S. g i * i) = (if u * x = u * x then f x * inv_u else g (u * x)) * (u * x) + (\<Sum>i\<in>(*) u ` S. g i * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f x * x + (\<Sum>i\<in>(*) u ` S. g i * i) = (if u * x = u * x then f x * inv_u else g (u * x)) * (u * x) + (\<Sum>i\<in>(*) u ` S. g i * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
have "... =  ?g (u * x) * (u * x) + sum ((\<lambda>i. g i * i) \<circ> (\<lambda>x. u*x)) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if u * x = u * x then f x * inv_u else g (u * x)) * (u * x) + (\<Sum>i\<in>(*) u ` S. g i * i) = (if u * x = u * x then f x * inv_u else g (u * x)) * (u * x) + sum ((\<lambda>i. g i * i) \<circ> (*) u) S
[PROOF STEP]
using sum_rw4
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>(*) u ` S. g i * i) = sum ((\<lambda>i. g i * i) \<circ> (*) u) S

goal (1 subgoal):
 1. (if u * x = u * x then f x * inv_u else g (u * x)) * (u * x) + (\<Sum>i\<in>(*) u ` S. g i * i) = (if u * x = u * x then f x * inv_u else g (u * x)) * (u * x) + sum ((\<lambda>i. g i * i) \<circ> (*) u) S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(if u * x = u * x then f x * inv_u else g (u * x)) * (u * x) + (\<Sum>i\<in>(*) u ` S. g i * i) = (if u * x = u * x then f x * inv_u else g (u * x)) * (u * x) + sum ((\<lambda>i. g i * i) \<circ> (*) u) S

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(if u * x = u * x then f x * inv_u else g (u * x)) * (u * x) + (\<Sum>i\<in>(*) u ` S. g i * i) = (if u * x = u * x then f x * inv_u else g (u * x)) * (u * x) + sum ((\<lambda>i. g i * i) \<circ> (*) u) S

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
have "... = ((\<lambda>i. ?g i * i) \<circ> (\<lambda>x. u*x)) x + sum ((\<lambda>i. g i * i) \<circ> (\<lambda>x. u*x)) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if u * x = u * x then f x * inv_u else g (u * x)) * (u * x) + sum ((\<lambda>i. g i * i) \<circ> (*) u) S = ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) x + sum ((\<lambda>i. g i * i) \<circ> (*) u) S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(if u * x = u * x then f x * inv_u else g (u * x)) * (u * x) + sum ((\<lambda>i. g i * i) \<circ> (*) u) S = ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) x + sum ((\<lambda>i. g i * i) \<circ> (*) u) S

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(if u * x = u * x then f x * inv_u else g (u * x)) * (u * x) + sum ((\<lambda>i. g i * i) \<circ> (*) u) S = ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) x + sum ((\<lambda>i. g i * i) \<circ> (*) u) S

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
have "... = ((\<lambda>i. ?g i * i) \<circ> (\<lambda>x. u*x)) x + sum ((\<lambda>i. ?g i * i) \<circ> (\<lambda>x. u*x)) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) x + sum ((\<lambda>i. g i * i) \<circ> (*) u) S = ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) x + sum ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) S
[PROOF STEP]
using sum_rw3
[PROOF STATE]
proof (prove)
using this:
sum ((\<lambda>i. g i * i) \<circ> (*) u) S = sum ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) S

goal (1 subgoal):
 1. ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) x + sum ((\<lambda>i. g i * i) \<circ> (*) u) S = ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) x + sum ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) x + sum ((\<lambda>i. g i * i) \<circ> (*) u) S = ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) x + sum ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) S

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) x + sum ((\<lambda>i. g i * i) \<circ> (*) u) S = ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) x + sum ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) S

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
have "... = sum ((\<lambda>i. ?g i * i) \<circ> (\<lambda>x. u*x)) (insert x S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) x + sum ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) S = sum ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) (insert x S)
[PROOF STEP]
by (rule sum.insert[symmetric], auto simp add: insert)
[PROOF STATE]
proof (state)
this:
((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) x + sum ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) S = sum ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) (insert x S)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) x + sum ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) S = sum ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) (insert x S)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
have "... = (\<Sum>i\<in>insert (u * x) ((\<lambda>x. u*x)` S). ?g i * i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) (insert x S) = (\<Sum>i\<in>insert (u * x) ((*) u ` S). (if i = u * x then f x * inv_u else g i) * i)
[PROOF STEP]
by (smt abel_semigroup.commute f2 image_insert inv_u mult.abel_semigroup_axioms mult_1_right
            semiring_normalization_rules(18) sum.reindex_nontrivial)
[PROOF STATE]
proof (state)
this:
sum ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) (insert x S) = (\<Sum>i\<in>insert (u * x) ((*) u ` S). (if i = u * x then f x * inv_u else g i) * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum ((\<lambda>i. (if i = u * x then f x * inv_u else g i) * i) \<circ> (*) u) (insert x S) = (\<Sum>i\<in>insert (u * x) ((*) u ` S). (if i = u * x then f x * inv_u else g i) * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
have "... = (\<Sum>i\<in>(\<lambda>x. u*x)` (insert x S). ?g i * i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>insert (u * x) ((*) u ` S). (if i = u * x then f x * inv_u else g i) * i) = (\<Sum>i\<in>(*) u ` insert x S. (if i = u * x then f x * inv_u else g i) * i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>insert (u * x) ((*) u ` S). (if i = u * x then f x * inv_u else g i) * i) = (\<Sum>i\<in>(*) u ` insert x S. (if i = u * x then f x * inv_u else g i) * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
a = (\<Sum>i\<in>(*) u ` insert x S. (if i = u * x then f x * inv_u else g i) * i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = (\<Sum>i\<in>(*) u ` insert x S. (if i = u * x then f x * inv_u else g i) * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?a1 \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y} \<Longrightarrow> ?a1 \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}

goal (1 subgoal):
 1. {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y} = {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?a1 \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y} \<Longrightarrow> ?a1 \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}

goal (1 subgoal):
 1. {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y} = {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
have "a \<in> ?R" if a: "a \<in> ?L" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
obtain f where sum_rw: "(\<Sum>i\<in>(insert (u * x) ((*) u ` S)). f i * i) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
a \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}

goal (1 subgoal):
 1. (\<And>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = a

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
have ux_notin: "u*x \<notin> ((*) u ` S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u * x \<notin> (*) u ` S
[PROOF STEP]
by (metis UNIV_I inj_on_image_mem_iff inj_on_inverseI inv_u local.insert(2) local.mult_1_left
            local.semiring_normalization_rules(18) subsetI)
[PROOF STATE]
proof (state)
this:
u * x \<notin> (*) u ` S

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
let ?f = "(\<lambda>x. f x * x)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
have "sum ?f ((*) u ` S) \<in> ideal_generated ((*) u ` S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>(*) u ` S. f x * x) \<in> ideal_generated ((*) u ` S)
[PROOF STEP]
unfolding ideal_explicit2[OF f4]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>(*) u ` S. f x * x) \<in> {y. \<exists>f. (\<Sum>i\<in>(*) u ` S. f i * i) = y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>(*) u ` S. f x * x) \<in> ideal_generated ((*) u ` S)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>x\<in>(*) u ` S. f x * x) \<in> ideal_generated ((*) u ` S)
[PROOF STEP]
obtain g where sum_rw1: "sum (\<lambda>i. g i * i) S = sum ?f (((*) u ` S))"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>(*) u ` S. f x * x) \<in> ideal_generated ((*) u ` S)

goal (1 subgoal):
 1. (\<And>g. (\<Sum>i\<in>S. g i * i) = (\<Sum>x\<in>(*) u ` S. f x * x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using insert.hyps(3)
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>(*) u ` S. f x * x) \<in> ideal_generated ((*) u ` S)
ideal_generated ((*) u ` S) = ideal_generated S

goal (1 subgoal):
 1. (\<And>g. (\<Sum>i\<in>S. g i * i) = (\<Sum>x\<in>(*) u ` S. f x * x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ideal_explicit2[OF f3]
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>(*) u ` S. f x * x) \<in> ideal_generated ((*) u ` S)
ideal_generated ((*) u ` S) = {y. \<exists>f. (\<Sum>i\<in>S. f i * i) = y}

goal (1 subgoal):
 1. (\<And>g. (\<Sum>i\<in>S. g i * i) = (\<Sum>x\<in>(*) u ` S. f x * x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>S. g i * i) = (\<Sum>x\<in>(*) u ` S. f x * x)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
let ?g = "(\<lambda>i. if i = x  then (f (u*x) *u) * x else g i * i)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
let ?g' = "\<lambda>i. if i = x  then f (u*x) * u else g i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
have sum_rw2: "sum (\<lambda>i. g i * i) S = sum ?g S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>S. g i * i) = (\<Sum>i\<in>S. if i = x then f (u * x) * u * x else g i * i)
[PROOF STEP]
by (rule sum.cong, insert inj_ux ux_notin, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>S. g i * i) = (\<Sum>i\<in>S. if i = x then f (u * x) * u * x else g i * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
have "a = (\<Sum>i\<in>(insert (u * x) ((*) u ` S)). f i * i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i)
[PROOF STEP]
using sum_rw
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = a

goal (1 subgoal):
 1. a = (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a = (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a = (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
have "... = ?f (u*x) +  sum ?f (((*) u ` S))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = f (u * x) * (u * x) + (\<Sum>x\<in>(*) u ` S. f x * x)
[PROOF STEP]
by (rule sum.insert[OF f4], insert inj_ux) (metis UNIV_I inj_on_image_mem_iff inj_on_inverseI
            inv_u local.insert(2) local.mult_1_left local.semiring_normalization_rules(18) subsetI)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = f (u * x) * (u * x) + (\<Sum>x\<in>(*) u ` S. f x * x)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = f (u * x) * (u * x) + (\<Sum>x\<in>(*) u ` S. f x * x)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
have "... = ?f (u*x) + sum (\<lambda>i. g i * i) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (u * x) * (u * x) + (\<Sum>x\<in>(*) u ` S. f x * x) = f (u * x) * (u * x) + (\<Sum>i\<in>S. g i * i)
[PROOF STEP]
unfolding sum_rw1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (u * x) * (u * x) + (\<Sum>x\<in>(*) u ` S. f x * x) = f (u * x) * (u * x) + (\<Sum>x\<in>(*) u ` S. f x * x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (u * x) * (u * x) + (\<Sum>x\<in>(*) u ` S. f x * x) = f (u * x) * (u * x) + (\<Sum>i\<in>S. g i * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (u * x) * (u * x) + (\<Sum>x\<in>(*) u ` S. f x * x) = f (u * x) * (u * x) + (\<Sum>i\<in>S. g i * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
have "... = ?g x + sum ?g S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (u * x) * (u * x) + (\<Sum>i\<in>S. g i * i) = (if x = x then f (u * x) * u * x else g x * x) + (\<Sum>i\<in>S. if i = x then f (u * x) * u * x else g i * i)
[PROOF STEP]
unfolding sum_rw2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (u * x) * (u * x) + (\<Sum>i\<in>S. if i = x then f (u * x) * u * x else g i * i) = (if x = x then f (u * x) * u * x else g x * x) + (\<Sum>i\<in>S. if i = x then f (u * x) * u * x else g i * i)
[PROOF STEP]
using mult.assoc
[PROOF STATE]
proof (prove)
using this:
?a * ?b * ?c = ?a * (?b * ?c)

goal (1 subgoal):
 1. f (u * x) * (u * x) + (\<Sum>i\<in>S. if i = x then f (u * x) * u * x else g i * i) = (if x = x then f (u * x) * u * x else g x * x) + (\<Sum>i\<in>S. if i = x then f (u * x) * u * x else g i * i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (u * x) * (u * x) + (\<Sum>i\<in>S. g i * i) = (if x = x then f (u * x) * u * x else g x * x) + (\<Sum>i\<in>S. if i = x then f (u * x) * u * x else g i * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (u * x) * (u * x) + (\<Sum>i\<in>S. g i * i) = (if x = x then f (u * x) * u * x else g x * x) + (\<Sum>i\<in>S. if i = x then f (u * x) * u * x else g i * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
have "... = sum ?g (insert x S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if x = x then f (u * x) * u * x else g x * x) + (\<Sum>i\<in>S. if i = x then f (u * x) * u * x else g i * i) = (\<Sum>i\<in>insert x S. if i = x then f (u * x) * u * x else g i * i)
[PROOF STEP]
by (rule sum.insert[symmetric, OF f3 insert.hyps(2)])
[PROOF STATE]
proof (state)
this:
(if x = x then f (u * x) * u * x else g x * x) + (\<Sum>i\<in>S. if i = x then f (u * x) * u * x else g i * i) = (\<Sum>i\<in>insert x S. if i = x then f (u * x) * u * x else g i * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(if x = x then f (u * x) * u * x else g x * x) + (\<Sum>i\<in>S. if i = x then f (u * x) * u * x else g i * i) = (\<Sum>i\<in>insert x S. if i = x then f (u * x) * u * x else g i * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
have "... = sum (\<lambda>i. ?g' i * i) (insert x S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>insert x S. if i = x then f (u * x) * u * x else g i * i) = (\<Sum>i\<in>insert x S. (if i = x then f (u * x) * u else g i) * i)
[PROOF STEP]
by (rule sum.cong, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>insert x S. if i = x then f (u * x) * u * x else g i * i) = (\<Sum>i\<in>insert x S. (if i = x then f (u * x) * u else g i) * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
a = (\<Sum>i\<in>insert x S. (if i = x then f (u * x) * u else g i) * i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = (\<Sum>i\<in>insert x S. (if i = x then f (u * x) * u else g i) * i)

goal (1 subgoal):
 1. a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
a \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?a1 \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y} \<Longrightarrow> ?a1 \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}

goal (1 subgoal):
 1. {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y} = {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?a1 \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y} \<Longrightarrow> ?a1 \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
?a1 \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y} \<Longrightarrow> ?a1 \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?a1 \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y} \<Longrightarrow> ?a1 \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y}
?a1 \<in> {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y} \<Longrightarrow> ?a1 \<in> {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}

goal (1 subgoal):
 1. {y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y} = {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y} = {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y} = {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; ideal_generated ((*) u ` F) = ideal_generated F\<rbrakk> \<Longrightarrow> ideal_generated ((*) u ` insert x F) = ideal_generated (insert x F)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{y. \<exists>f. (\<Sum>i\<in>insert (u * x) ((*) u ` S). f i * i) = y} = {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; ideal_generated ((*) u ` F) = ideal_generated F\<rbrakk> \<Longrightarrow> ideal_generated ((*) u ` insert x F) = ideal_generated (insert x F)
[PROOF STEP]
have "... = ideal_generated (insert x S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y} = ideal_generated (insert x S)
[PROOF STEP]
using ideal_explicit2[OF f2]
[PROOF STATE]
proof (prove)
using this:
ideal_generated (insert x S) = {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y}

goal (1 subgoal):
 1. {y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y} = ideal_generated (insert x S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{y. \<exists>f. (\<Sum>i\<in>insert x S. f i * i) = y} = ideal_generated (insert x S)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; ideal_generated ((*) u ` F) = ideal_generated F\<rbrakk> \<Longrightarrow> ideal_generated ((*) u ` insert x F) = ideal_generated (insert x F)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ideal_generated ((*) u ` insert x S) = ideal_generated (insert x S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ideal_generated ((*) u ` insert x S) = ideal_generated (insert x S)

goal (1 subgoal):
 1. ideal_generated ((*) u ` insert x S) = ideal_generated (insert x S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ideal_generated ((*) u ` insert x S) = ideal_generated (insert x S)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ideal_generated_1[simp]: "ideal_generated {1} = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated {1::'a} = UNIV
[PROOF STEP]
by (metis ideal_generated_unit dvd_ideal_generated_singleton order_refl)


[STATEMENT]
lemma ideal_generated_pair: "ideal_generated {a,b} = {p*a+q*b | p q. True}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated {a, b} = {p * a + q * b |p q. True}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ideal_generated {a, b} = {p * a + q * b |p q. True}
[PROOF STEP]
have i: "ideal_generated {a,b} = {y. \<exists>f. (\<Sum>i\<in>{a,b}. f i * i) = y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated {a, b} = {y. \<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = y}
[PROOF STEP]
using ideal_explicit2
[PROOF STATE]
proof (prove)
using this:
finite ?S \<Longrightarrow> ideal_generated ?S = {y. \<exists>f. (\<Sum>i\<in>?S. f i * i) = y}

goal (1 subgoal):
 1. ideal_generated {a, b} = {y. \<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ideal_generated {a, b} = {y. \<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = y}

goal (1 subgoal):
 1. ideal_generated {a, b} = {p * a + q * b |p q. True}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated {a, b} = {p * a + q * b |p q. True}
[PROOF STEP]
proof (cases "a=b")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = b \<Longrightarrow> ideal_generated {a, b} = {p * a + q * b |p q. True}
 2. a \<noteq> b \<Longrightarrow> ideal_generated {a, b} = {p * a + q * b |p q. True}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = b

goal (2 subgoals):
 1. a = b \<Longrightarrow> ideal_generated {a, b} = {p * a + q * b |p q. True}
 2. a \<noteq> b \<Longrightarrow> ideal_generated {a, b} = {p * a + q * b |p q. True}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated {a, b} = {p * a + q * b |p q. True}
[PROOF STEP]
using True i
[PROOF STATE]
proof (prove)
using this:
a = b
ideal_generated {a, b} = {y. \<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = y}

goal (1 subgoal):
 1. ideal_generated {a, b} = {p * a + q * b |p q. True}
[PROOF STEP]
by (auto, metis mult_ac(2) semiring_normalization_rules)
      (metis (no_types, opaque_lifting) add_minus_cancel mult_ac ring_distribs semiring_normalization_rules)
[PROOF STATE]
proof (state)
this:
ideal_generated {a, b} = {p * a + q * b |p q. True}

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> ideal_generated {a, b} = {p * a + q * b |p q. True}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> ideal_generated {a, b} = {p * a + q * b |p q. True}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> b

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> ideal_generated {a, b} = {p * a + q * b |p q. True}
[PROOF STEP]
have 1: "\<exists>p q. (\<Sum>i\<in>{a, b}. f i * i) = p * a + q * b" for f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p q. (\<Sum>i\<in>{a, b}. f i * i) = p * a + q * b
[PROOF STEP]
by (rule exI[of _ "f a"], rule exI[of _ "f b"], rule sum_two_elements[OF False])
[PROOF STATE]
proof (state)
this:
\<exists>p q. (\<Sum>i\<in>{a, b}. ?f1 i * i) = p * a + q * b

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> ideal_generated {a, b} = {p * a + q * b |p q. True}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>p q. (\<Sum>i\<in>{a, b}. ?f1 i * i) = p * a + q * b

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> ideal_generated {a, b} = {p * a + q * b |p q. True}
[PROOF STEP]
have "\<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = p * a + q * b" for p q
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = p * a + q * b
[PROOF STEP]
by (rule exI[of _ "\<lambda>i. if i=a then p else q"],
          unfold sum_two_elements[OF False], insert False, auto)
[PROOF STATE]
proof (state)
this:
\<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = ?p1 * a + ?q1 * b

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> ideal_generated {a, b} = {p * a + q * b |p q. True}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>p q. (\<Sum>i\<in>{a, b}. ?f1 i * i) = p * a + q * b
\<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = ?p1 * a + ?q1 * b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>p q. (\<Sum>i\<in>{a, b}. ?f1 i * i) = p * a + q * b
\<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = ?p1 * a + ?q1 * b

goal (1 subgoal):
 1. ideal_generated {a, b} = {p * a + q * b |p q. True}
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
\<exists>p q. (\<Sum>i\<in>{a, b}. ?f1 i * i) = p * a + q * b
\<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = ?p1 * a + ?q1 * b
ideal_generated {a, b} = {y. \<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = y}

goal (1 subgoal):
 1. ideal_generated {a, b} = {p * a + q * b |p q. True}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ideal_generated {a, b} = {p * a + q * b |p q. True}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ideal_generated {a, b} = {p * a + q * b |p q. True}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ideal_generated_pair_exists_pq1:
  assumes i: "ideal_generated {a,b} = (UNIV::'a set)"
  shows "\<exists>p q. p*a + q*b = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p q. p * a + q * b = (1::'a)
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
ideal_generated {a, b} = UNIV

goal (1 subgoal):
 1. \<exists>p q. p * a + q * b = (1::'a)
[PROOF STEP]
unfolding ideal_generated_pair
[PROOF STATE]
proof (prove)
using this:
{p * a + q * b |p q. True} = UNIV

goal (1 subgoal):
 1. \<exists>p q. p * a + q * b = (1::'a)
[PROOF STEP]
by (smt iso_tuple_UNIV_I mem_Collect_eq)


[STATEMENT]
lemma ideal_generated_pair_UNIV:
  assumes sa_tb_u: "s*a+t*b = u" and u: "u dvd 1"
  shows "ideal_generated {a,b} = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated {a, b} = UNIV
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ideal_generated {a, b} = UNIV
[PROOF STEP]
have f: "finite {a,b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {a, b}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {a, b}

goal (1 subgoal):
 1. ideal_generated {a, b} = UNIV
[PROOF STEP]
obtain inv_u where inv_u: "inv_u * u = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>inv_u. inv_u * u = (1::'a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using u
[PROOF STATE]
proof (prove)
using this:
u dvd (1::'a)

goal (1 subgoal):
 1. (\<And>inv_u. inv_u * u = (1::'a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dvd_def
[PROOF STATE]
proof (prove)
using this:
\<exists>k. (1::'a) = u * k

goal (1 subgoal):
 1. (\<And>inv_u. inv_u * u = (1::'a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis mult.commute)
[PROOF STATE]
proof (state)
this:
inv_u * u = (1::'a)

goal (1 subgoal):
 1. ideal_generated {a, b} = UNIV
[PROOF STEP]
have "x \<in> ideal_generated {a,b}" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> ideal_generated {a, b}
[PROOF STEP]
proof (cases "a = b")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = b \<Longrightarrow> x \<in> ideal_generated {a, b}
 2. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = b

goal (2 subgoals):
 1. a = b \<Longrightarrow> x \<in> ideal_generated {a, b}
 2. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = b

goal (1 subgoal):
 1. x \<in> ideal_generated {a, b}
[PROOF STEP]
by (metis UNIV_I dvd_def dvd_ideal_generated_singleton' ideal_generated_unit insert_absorb2
          mult.commute sa_tb_u semiring_normalization_rules(34) subsetI subset_antisym u)
[PROOF STATE]
proof (state)
this:
x \<in> ideal_generated {a, b}

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> b

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
note a_not_b = False
[PROOF STATE]
proof (state)
this:
a \<noteq> b

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
let ?f = "\<lambda>y. if y = a then inv_u * x * s else inv_u * x * t"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
have "(\<Sum>i\<in>{a,b}. ?f i * i) = ?f a * a + ?f b * b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{a, b}. (if i = a then inv_u * x * s else inv_u * x * t) * i) = (if a = a then inv_u * x * s else inv_u * x * t) * a + (if b = a then inv_u * x * s else inv_u * x * t) * b
[PROOF STEP]
by (rule sum_two_elements[OF a_not_b])
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{a, b}. (if i = a then inv_u * x * s else inv_u * x * t) * i) = (if a = a then inv_u * x * s else inv_u * x * t) * a + (if b = a then inv_u * x * s else inv_u * x * t) * b

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{a, b}. (if i = a then inv_u * x * s else inv_u * x * t) * i) = (if a = a then inv_u * x * s else inv_u * x * t) * a + (if b = a then inv_u * x * s else inv_u * x * t) * b

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
have "... = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if a = a then inv_u * x * s else inv_u * x * t) * a + (if b = a then inv_u * x * s else inv_u * x * t) * b = x
[PROOF STEP]
using a_not_b sa_tb_u inv_u
[PROOF STATE]
proof (prove)
using this:
a \<noteq> b
s * a + t * b = u
inv_u * u = (1::'a)

goal (1 subgoal):
 1. (if a = a then inv_u * x * s else inv_u * x * t) * a + (if b = a then inv_u * x * s else inv_u * x * t) * b = x
[PROOF STEP]
by (auto, metis mult_ac(1) mult_ac(2) ring_distribs(1) semiring_normalization_rules(12))
[PROOF STATE]
proof (state)
this:
(if a = a then inv_u * x * s else inv_u * x * t) * a + (if b = a then inv_u * x * s else inv_u * x * t) * b = x

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i\<in>{a, b}. (if i = a then inv_u * x * s else inv_u * x * t) * i) = x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>{a, b}. (if i = a then inv_u * x * s else inv_u * x * t) * i) = x

goal (1 subgoal):
 1. x \<in> ideal_generated {a, b}
[PROOF STEP]
unfolding ideal_explicit2[OF f]
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>{a, b}. (if i = a then inv_u * x * s else inv_u * x * t) * i) = x

goal (1 subgoal):
 1. x \<in> {y. \<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> ideal_generated {a, b}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x1 \<in> ideal_generated {a, b}

goal (1 subgoal):
 1. ideal_generated {a, b} = UNIV
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> ideal_generated {a, b}

goal (1 subgoal):
 1. ideal_generated {a, b} = UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ideal_generated {a, b} = UNIV

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ideal_generated_pair_exists:
  assumes l: "(ideal_generated {a,b} = ideal_generated {d})"
  shows "(\<exists> p q. p*a+q*b = d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p q. p * a + q * b = d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>p q. p * a + q * b = d
[PROOF STEP]
have d: "d \<in> ideal_generated {d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<in> ideal_generated {d}
[PROOF STEP]
by (simp add: ideal_generated_in)
[PROOF STATE]
proof (state)
this:
d \<in> ideal_generated {d}

goal (1 subgoal):
 1. \<exists>p q. p * a + q * b = d
[PROOF STEP]
hence "d \<in> ideal_generated {a,b}"
[PROOF STATE]
proof (prove)
using this:
d \<in> ideal_generated {d}

goal (1 subgoal):
 1. d \<in> ideal_generated {a, b}
[PROOF STEP]
using l
[PROOF STATE]
proof (prove)
using this:
d \<in> ideal_generated {d}
ideal_generated {a, b} = ideal_generated {d}

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

goal (1 subgoal):
 1. \<exists>p q. p * a + q * b = d
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
d \<in> ideal_generated {a, b}
[PROOF STEP]
obtain p q where "d = p*a+q*b"
[PROOF STATE]
proof (prove)
using this:
d \<in> ideal_generated {a, b}

goal (1 subgoal):
 1. (\<And>p q. d = p * a + q * b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ideal_generated_pair[of a b]
[PROOF STATE]
proof (prove)
using this:
d \<in> ideal_generated {a, b}
ideal_generated {a, b} = {p * a + q * b |p q. True}

goal (1 subgoal):
 1. (\<And>p q. d = p * a + q * b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d = p * a + q * b

goal (1 subgoal):
 1. \<exists>p q. p * a + q * b = d
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
d = p * a + q * b

goal (1 subgoal):
 1. \<exists>p q. p * a + q * b = d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>p q. p * a + q * b = d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma obtain_ideal_generated_pair:
  assumes "c \<in> ideal_generated {a,b}"
  obtains p q where "p*a+q*b=c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p q. p * a + q * b = c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>p q. p * a + q * b = c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "c \<in> {p * a + q * b |p q. True}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<in> {p * a + q * b |p q. True}
[PROOF STEP]
using assms ideal_generated_pair
[PROOF STATE]
proof (prove)
using this:
c \<in> ideal_generated {a, b}
ideal_generated {?a, ?b} = {p * ?a + q * ?b |p q. True}

goal (1 subgoal):
 1. c \<in> {p * a + q * b |p q. True}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<in> {p * a + q * b |p q. True}

goal (1 subgoal):
 1. (\<And>p q. p * a + q * b = c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
c \<in> {p * a + q * b |p q. True}

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
c \<in> {p * a + q * b |p q. True}
?p1 * a + ?q1 * b = c \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ideal_generated_pair_exists_UNIV:
  shows "(ideal_generated {a,b} = ideal_generated {1}) = (\<exists>p q. p*a+q*b = 1)" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ideal_generated {a, b} = ideal_generated {1::'a}) = (\<exists>p q. p * a + q * b = (1::'a))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ideal_generated {a, b} = ideal_generated {1::'a} \<Longrightarrow> \<exists>p q. p * a + q * b = (1::'a)
 2. \<exists>p q. p * a + q * b = (1::'a) \<Longrightarrow> ideal_generated {a, b} = ideal_generated {1::'a}
[PROOF STEP]
assume r: ?rhs
[PROOF STATE]
proof (state)
this:
\<exists>p q. p * a + q * b = (1::'a)

goal (2 subgoals):
 1. ideal_generated {a, b} = ideal_generated {1::'a} \<Longrightarrow> \<exists>p q. p * a + q * b = (1::'a)
 2. \<exists>p q. p * a + q * b = (1::'a) \<Longrightarrow> ideal_generated {a, b} = ideal_generated {1::'a}
[PROOF STEP]
have "x \<in> ideal_generated {a,b}" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> ideal_generated {a, b}
[PROOF STEP]
proof (cases "a=b")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = b \<Longrightarrow> x \<in> ideal_generated {a, b}
 2. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = b

goal (2 subgoals):
 1. a = b \<Longrightarrow> x \<in> ideal_generated {a, b}
 2. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = b

goal (1 subgoal):
 1. x \<in> ideal_generated {a, b}
[PROOF STEP]
by (metis UNIV_I r dvd_ideal_generated_singleton finite.intros ideal_generated_1
          ideal_generated_pair_UNIV ideal_generated_singleton_subset)
[PROOF STATE]
proof (state)
this:
x \<in> ideal_generated {a, b}

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> b

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
have f: "finite {a,b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {a, b}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {a, b}

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
have 1: "1 \<in> ideal_generated {a,b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<in> ideal_generated {a, b}
[PROOF STEP]
using ideal_generated_pair_UNIV local.one_dvd r
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?s * ?a + ?t * ?b = ?u; ?u dvd (1::'a)\<rbrakk> \<Longrightarrow> ideal_generated {?a, ?b} = UNIV
(1::'a) dvd ?a
\<exists>p q. p * a + q * b = (1::'a)

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

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
hence i: "ideal_generated {a,b} = {y. \<exists>f. (\<Sum>i\<in>{a,b}. f i * i) = y}"
[PROOF STATE]
proof (prove)
using this:
(1::'a) \<in> ideal_generated {a, b}

goal (1 subgoal):
 1. ideal_generated {a, b} = {y. \<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = y}
[PROOF STEP]
using ideal_explicit2[of "{a,b}"]
[PROOF STATE]
proof (prove)
using this:
(1::'a) \<in> ideal_generated {a, b}
finite {a, b} \<Longrightarrow> ideal_generated {a, b} = {y. \<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = y}

goal (1 subgoal):
 1. ideal_generated {a, b} = {y. \<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ideal_generated {a, b} = {y. \<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = y}

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
ideal_generated {a, b} = {y. \<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = y}
[PROOF STEP]
obtain f where f: "f a * a + f b * b = 1"
[PROOF STATE]
proof (prove)
using this:
ideal_generated {a, b} = {y. \<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = y}

goal (1 subgoal):
 1. (\<And>f. f a * a + f b * b = (1::'a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using sum_two_elements 1 False
[PROOF STATE]
proof (prove)
using this:
ideal_generated {a, b} = {y. \<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = y}
?a \<noteq> ?b \<Longrightarrow> sum ?f {?a, ?b} = ?f ?a + ?f ?b
(1::'a) \<in> ideal_generated {a, b}
a \<noteq> b

goal (1 subgoal):
 1. (\<And>f. f a * a + f b * b = (1::'a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f a * a + f b * b = (1::'a)

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
let ?f = "\<lambda>y. if y = a then x * f a else x * f b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
have "(\<Sum>i\<in>{a,b}. ?f i * i) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{a, b}. (if i = a then x * f a else x * f b) * i) = x
[PROOF STEP]
unfolding sum_two_elements[OF False]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if a = a then x * f a else x * f b) * a + (if b = a then x * f a else x * f b) * b = x
[PROOF STEP]
using f False
[PROOF STATE]
proof (prove)
using this:
f a * a + f b * b = (1::'a)
a \<noteq> b

goal (1 subgoal):
 1. (if a = a then x * f a else x * f b) * a + (if b = a then x * f a else x * f b) * b = x
[PROOF STEP]
using mult_ac(1) ring_distribs(1) semiring_normalization_rules(12)
[PROOF STATE]
proof (prove)
using this:
f a * a + f b * b = (1::'a)
a \<noteq> b
?a * ?b * ?c = ?a * (?b * ?c)
?a * (?b + ?c) = ?a * ?b + ?a * ?c
?a * (1::'a) = ?a

goal (1 subgoal):
 1. (if a = a then x * f a else x * f b) * a + (if b = a then x * f a else x * f b) * b = x
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{a, b}. (if i = a then x * f a else x * f b) * i) = x

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> x \<in> ideal_generated {a, b}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>{a, b}. (if i = a then x * f a else x * f b) * i) = x

goal (1 subgoal):
 1. x \<in> ideal_generated {a, b}
[PROOF STEP]
unfolding i
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>{a, b}. (if i = a then x * f a else x * f b) * i) = x

goal (1 subgoal):
 1. x \<in> {y. \<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> ideal_generated {a, b}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x1 \<in> ideal_generated {a, b}

goal (2 subgoals):
 1. ideal_generated {a, b} = ideal_generated {1::'a} \<Longrightarrow> \<exists>p q. p * a + q * b = (1::'a)
 2. \<exists>p q. p * a + q * b = (1::'a) \<Longrightarrow> ideal_generated {a, b} = ideal_generated {1::'a}
[PROOF STEP]
thus ?lhs
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> ideal_generated {a, b}

goal (1 subgoal):
 1. ideal_generated {a, b} = ideal_generated {1::'a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ideal_generated {a, b} = ideal_generated {1::'a}

goal (1 subgoal):
 1. ideal_generated {a, b} = ideal_generated {1::'a} \<Longrightarrow> \<exists>p q. p * a + q * b = (1::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ideal_generated {a, b} = ideal_generated {1::'a} \<Longrightarrow> \<exists>p q. p * a + q * b = (1::'a)
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
ideal_generated {a, b} = ideal_generated {1::'a}

goal (1 subgoal):
 1. ideal_generated {a, b} = ideal_generated {1::'a} \<Longrightarrow> \<exists>p q. p * a + q * b = (1::'a)
[PROOF STEP]
thus ?rhs
[PROOF STATE]
proof (prove)
using this:
ideal_generated {a, b} = ideal_generated {1::'a}

goal (1 subgoal):
 1. \<exists>p q. p * a + q * b = (1::'a)
[PROOF STEP]
using ideal_generated_pair_exists[of a b 1]
[PROOF STATE]
proof (prove)
using this:
ideal_generated {a, b} = ideal_generated {1::'a}
ideal_generated {a, b} = ideal_generated {1::'a} \<Longrightarrow> \<exists>p q. p * a + q * b = (1::'a)

goal (1 subgoal):
 1. \<exists>p q. p * a + q * b = (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>p q. p * a + q * b = (1::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_three_elements:
  shows "\<exists>x y z::'a. (\<Sum>i\<in>{a,b,c}. f i * i) = x * a + y * b + z * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x y z. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
proof (cases "a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c \<Longrightarrow> \<exists>x y z. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
 2. \<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c) \<Longrightarrow> \<exists>x y z. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c

goal (2 subgoals):
 1. a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c \<Longrightarrow> \<exists>x y z. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
 2. \<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c) \<Longrightarrow> \<exists>x y z. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c

goal (1 subgoal):
 1. \<exists>x y z. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
by (auto, metis add.assoc)
[PROOF STATE]
proof (state)
this:
\<exists>x y z. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c

goal (1 subgoal):
 1. \<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c) \<Longrightarrow> \<exists>x y z. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c) \<Longrightarrow> \<exists>x y z. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c)

goal (1 subgoal):
 1. \<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c) \<Longrightarrow> \<exists>x y z. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
have 1: "\<exists>x y z. f c * c = x * c + y * c + z * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x y z. f c * c = x * c + y * c + z * c
[PROOF STEP]
by (rule exI[of _ 0],rule exI[of _ 0], rule exI[of _ "f c"], auto)
[PROOF STATE]
proof (state)
this:
\<exists>x y z. f c * c = x * c + y * c + z * c

goal (1 subgoal):
 1. \<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c) \<Longrightarrow> \<exists>x y z. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
have 2: "\<exists>x y z. f b * b + f c * c = x * b + y * b + z * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x y z. f b * b + f c * c = x * b + y * b + z * c
[PROOF STEP]
by (rule exI[of _ 0],rule exI[of _ "f b"], rule exI[of _ "f c"], auto)
[PROOF STATE]
proof (state)
this:
\<exists>x y z. f b * b + f c * c = x * b + y * b + z * c

goal (1 subgoal):
 1. \<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c) \<Longrightarrow> \<exists>x y z. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
have 3: "\<exists>x y z. f a * a + f c * c = x * a + y * c + z * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x y z. f a * a + f c * c = x * a + y * c + z * c
[PROOF STEP]
by (rule exI[of _ "f a"],rule exI[of _ 0], rule exI[of _ "f c"], auto)
[PROOF STATE]
proof (state)
this:
\<exists>x y z. f a * a + f c * c = x * a + y * c + z * c

goal (1 subgoal):
 1. \<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c) \<Longrightarrow> \<exists>x y z. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
have 4: "\<exists>x y z. (\<Sum>i\<in>{c, b, c}. f i * i) = x * c + y * b + z * c" if a: "a = c" and b: "b \<noteq> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x y z. (\<Sum>i\<in>{c, b, c}. f i * i) = x * c + y * b + z * c
[PROOF STEP]
by (rule exI[of _ 0],rule exI[of _ "f b"], rule exI[of _ "f c"], insert a b,
        auto simp add: insert_commute)
[PROOF STATE]
proof (state)
this:
\<lbrakk>a = c; b \<noteq> c\<rbrakk> \<Longrightarrow> \<exists>x y z. (\<Sum>i\<in>{c, b, c}. f i * i) = x * c + y * b + z * c

goal (1 subgoal):
 1. \<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c) \<Longrightarrow> \<exists>x y z. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x y z. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c)

goal (1 subgoal):
 1. \<exists>x y z. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
by (cases "b=c", cases "a=c", auto simp add: 1 2 3 4)
[PROOF STATE]
proof (state)
this:
\<exists>x y z. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_three_elements':
  shows "\<exists>f::'a\<Rightarrow>'a. (\<Sum>i\<in>{a,b,c}. f i * i) = x * a + y * b + z * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
proof (cases "a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c \<Longrightarrow> \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
 2. \<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c) \<Longrightarrow> \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c

goal (2 subgoals):
 1. a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c \<Longrightarrow> \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
 2. \<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c) \<Longrightarrow> \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
let ?f = "\<lambda>i. if i = a then x else if i = b then y else if i = c then z else 0"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c \<Longrightarrow> \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
 2. \<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c) \<Longrightarrow> \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
by (rule exI[of _ "?f"], insert True mult.assoc, auto simp add: local.add_ac)
[PROOF STATE]
proof (state)
this:
\<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c

goal (1 subgoal):
 1. \<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c) \<Longrightarrow> \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c) \<Longrightarrow> \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c)

goal (1 subgoal):
 1. \<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c) \<Longrightarrow> \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
have 1: "\<exists>f. f c * c = x * c + y * c + z * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. f c * c = x * c + y * c + z * c
[PROOF STEP]
by (rule exI[of _ "\<lambda>i. if i = c then x+y+z else 0"], auto simp add: local.ring_distribs)
[PROOF STATE]
proof (state)
this:
\<exists>f. f c * c = x * c + y * c + z * c

goal (1 subgoal):
 1. \<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c) \<Longrightarrow> \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
have 2: "\<exists>f. f a * a + f c * c = x * a + y * c + z * c" if bc: " b = c" and ac: "a \<noteq> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. f a * a + f c * c = x * a + y * c + z * c
[PROOF STEP]
by (rule exI[of _ "\<lambda>i. if i = a then x else y+z"], insert ac bc add_ac ring_distribs, auto)
[PROOF STATE]
proof (state)
this:
\<lbrakk>b = c; a \<noteq> c\<rbrakk> \<Longrightarrow> \<exists>f. f a * a + f c * c = x * a + y * c + z * c

goal (1 subgoal):
 1. \<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c) \<Longrightarrow> \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
have 3: "\<exists>f. f b * b + f c * c = x * b + y * b + z * c" if bc: " b \<noteq> c" and ac: "a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. f b * b + f c * c = x * b + y * b + z * c
[PROOF STEP]
by (rule exI[of _ "\<lambda>i. if i = a then x+y else z"], insert ac bc add_ac ring_distribs, auto)
[PROOF STATE]
proof (state)
this:
\<lbrakk>b \<noteq> c; a = b\<rbrakk> \<Longrightarrow> \<exists>f. f b * b + f c * c = x * b + y * b + z * c

goal (1 subgoal):
 1. \<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c) \<Longrightarrow> \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
have 4: "\<exists>f. (\<Sum>i\<in>{c, b, c}. f i * i) = x * c + y * b + z * c" if a: "a = c" and b: "b \<noteq> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. (\<Sum>i\<in>{c, b, c}. f i * i) = x * c + y * b + z * c
[PROOF STEP]
by (rule exI[of _ "\<lambda>i. if i = c then x+z else y"], insert a b add_ac ring_distribs,
        auto simp add: insert_commute)
[PROOF STATE]
proof (state)
this:
\<lbrakk>a = c; b \<noteq> c\<rbrakk> \<Longrightarrow> \<exists>f. (\<Sum>i\<in>{c, b, c}. f i * i) = x * c + y * b + z * c

goal (1 subgoal):
 1. \<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c) \<Longrightarrow> \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c)

goal (1 subgoal):
 1. \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
[PROOF STEP]
by (cases "b=c", cases "a=c", auto simp add: 1 2 3 4)
[PROOF STATE]
proof (state)
this:
\<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ideal_generated_triple_pair_rewrite:
  assumes i1: "ideal_generated {a, b, c} = ideal_generated {d}"
    and i2: "ideal_generated {a, b} = ideal_generated {d'}"
  shows "ideal_generated{d',c} = ideal_generated {d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated {d', c} = ideal_generated {d}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ideal_generated {d', c} \<subseteq> ideal_generated {d}
 2. ideal_generated {d} \<subseteq> ideal_generated {d', c}
[PROOF STEP]
have d': "d' \<in> ideal_generated {a,b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d' \<in> ideal_generated {a, b}
[PROOF STEP]
using i2
[PROOF STATE]
proof (prove)
using this:
ideal_generated {a, b} = ideal_generated {d'}

goal (1 subgoal):
 1. d' \<in> ideal_generated {a, b}
[PROOF STEP]
by (simp add: ideal_generated_in)
[PROOF STATE]
proof (state)
this:
d' \<in> ideal_generated {a, b}

goal (2 subgoals):
 1. ideal_generated {d', c} \<subseteq> ideal_generated {d}
 2. ideal_generated {d} \<subseteq> ideal_generated {d', c}
[PROOF STEP]
show "ideal_generated {d', c} \<subseteq> ideal_generated {d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated {d', c} \<subseteq> ideal_generated {d}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated {d', c} \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated {d', c} \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
assume x: "x \<in> ideal_generated {d', c}"
[PROOF STATE]
proof (state)
this:
x \<in> ideal_generated {d', c}

goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated {d', c} \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
obtain f1 f2 where f: "f1*d' + f2*c = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f1 f2. f1 * d' + f2 * c = x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obtain_ideal_generated_pair[OF x]
[PROOF STATE]
proof (prove)
using this:
(\<And>p q. p * d' + q * c = x \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>f1 f2. f1 * d' + f2 * c = x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f1 * d' + f2 * c = x

goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated {d', c} \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
obtain g1 g2 where g: "g1*a + g2*b = d'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g1 g2. g1 * a + g2 * b = d' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obtain_ideal_generated_pair[OF d']
[PROOF STATE]
proof (prove)
using this:
(\<And>p q. p * a + q * b = d' \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>g1 g2. g1 * a + g2 * b = d' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
g1 * a + g2 * b = d'

goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated {d', c} \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
have 1: "f1*g1*a + f1*g2*b + f2*c = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f1 * g1 * a + f1 * g2 * b + f2 * c = x
[PROOF STEP]
using f g local.ring_distribs(1) local.semiring_normalization_rules(18)
[PROOF STATE]
proof (prove)
using this:
f1 * d' + f2 * c = x
g1 * a + g2 * b = d'
?a * (?b + ?c) = ?a * ?b + ?a * ?c
?lx * (?rx * ?ry) = ?lx * ?rx * ?ry

goal (1 subgoal):
 1. f1 * g1 * a + f1 * g2 * b + f2 * c = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f1 * g1 * a + f1 * g2 * b + f2 * c = x

goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated {d', c} \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
have "x \<in> ideal_generated {a, b, c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> ideal_generated {a, b, c}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> ideal_generated {a, b, c}
[PROOF STEP]
obtain f where "(\<Sum>i\<in>{a,b,c}. f i * i) = f1*g1*a + f1*g2*b + f2*c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. (\<Sum>i\<in>{a, b, c}. f i * i) = f1 * g1 * a + f1 * g2 * b + f2 * c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using sum_three_elements' 1
[PROOF STATE]
proof (prove)
using this:
\<exists>f. (\<Sum>i\<in>{?a, ?b, ?c}. f i * i) = ?x * ?a + ?y * ?b + ?z * ?c
f1 * g1 * a + f1 * g2 * b + f2 * c = x

goal (1 subgoal):
 1. (\<And>f. (\<Sum>i\<in>{a, b, c}. f i * i) = f1 * g1 * a + f1 * g2 * b + f2 * c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{a, b, c}. f i * i) = f1 * g1 * a + f1 * g2 * b + f2 * c

goal (1 subgoal):
 1. x \<in> ideal_generated {a, b, c}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{a, b, c}. f i * i) = f1 * g1 * a + f1 * g2 * b + f2 * c

goal (1 subgoal):
 1. x \<in> ideal_generated {a, b, c}
[PROOF STEP]
have "ideal_generated {a,b,c} = {y. \<exists>f. (\<Sum>i\<in>{a,b,c}. f i * i) = y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated {a, b, c} = {y. \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = y}
[PROOF STEP]
using ideal_explicit2[of "{a,b,c}"]
[PROOF STATE]
proof (prove)
using this:
finite {a, b, c} \<Longrightarrow> ideal_generated {a, b, c} = {y. \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = y}

goal (1 subgoal):
 1. ideal_generated {a, b, c} = {y. \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = y}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ideal_generated {a, b, c} = {y. \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = y}

goal (1 subgoal):
 1. x \<in> ideal_generated {a, b, c}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i\<in>{a, b, c}. f i * i) = f1 * g1 * a + f1 * g2 * b + f2 * c
ideal_generated {a, b, c} = {y. \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = y}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>{a, b, c}. f i * i) = f1 * g1 * a + f1 * g2 * b + f2 * c
ideal_generated {a, b, c} = {y. \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = y}

goal (1 subgoal):
 1. x \<in> ideal_generated {a, b, c}
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>{a, b, c}. f i * i) = f1 * g1 * a + f1 * g2 * b + f2 * c
ideal_generated {a, b, c} = {y. \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = y}
f1 * g1 * a + f1 * g2 * b + f2 * c = x

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> ideal_generated {a, b, c}

goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated {d', c} \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
thus "x \<in> ideal_generated {d}"
[PROOF STATE]
proof (prove)
using this:
x \<in> ideal_generated {a, b, c}

goal (1 subgoal):
 1. x \<in> ideal_generated {d}
[PROOF STEP]
using i1
[PROOF STATE]
proof (prove)
using this:
x \<in> ideal_generated {a, b, c}
ideal_generated {a, b, c} = ideal_generated {d}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ideal_generated {d', c} \<subseteq> ideal_generated {d}

goal (1 subgoal):
 1. ideal_generated {d} \<subseteq> ideal_generated {d', c}
[PROOF STEP]
show "ideal_generated {d} \<subseteq> ideal_generated {d', c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated {d} \<subseteq> ideal_generated {d', c}
[PROOF STEP]
proof (rule ideal_generated_singleton_subset)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. d \<in> ideal_generated {d', c}
 2. finite {d', c}
[PROOF STEP]
obtain f1 f2 f3 where f: "f1*a + f2*b + f3*c = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f1 f2 f3. f1 * a + f2 * b + f3 * c = d \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>f1 f2 f3. f1 * a + f2 * b + f3 * c = d \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "d \<in> ideal_generated {a,b,c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<in> ideal_generated {a, b, c}
[PROOF STEP]
using i1
[PROOF STATE]
proof (prove)
using this:
ideal_generated {a, b, c} = ideal_generated {d}

goal (1 subgoal):
 1. d \<in> ideal_generated {a, b, c}
[PROOF STEP]
by (simp add: ideal_generated_in)
[PROOF STATE]
proof (state)
this:
d \<in> ideal_generated {a, b, c}

goal (1 subgoal):
 1. (\<And>f1 f2 f3. f1 * a + f2 * b + f3 * c = d \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
d \<in> ideal_generated {a, b, c}
[PROOF STEP]
obtain f where d: "(\<Sum>i\<in>{a,b,c}. f i * i) = d"
[PROOF STATE]
proof (prove)
using this:
d \<in> ideal_generated {a, b, c}

goal (1 subgoal):
 1. (\<And>f. (\<Sum>i\<in>{a, b, c}. f i * i) = d \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ideal_explicit2[of "{a,b,c}"]
[PROOF STATE]
proof (prove)
using this:
d \<in> ideal_generated {a, b, c}
finite {a, b, c} \<Longrightarrow> ideal_generated {a, b, c} = {y. \<exists>f. (\<Sum>i\<in>{a, b, c}. f i * i) = y}

goal (1 subgoal):
 1. (\<And>f. (\<Sum>i\<in>{a, b, c}. f i * i) = d \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{a, b, c}. f i * i) = d

goal (1 subgoal):
 1. (\<And>f1 f2 f3. f1 * a + f2 * b + f3 * c = d \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain x y z where "(\<Sum>i\<in>{a,b,c}. f i * i) = x * a + y * b + z * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y z. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using sum_three_elements
[PROOF STATE]
proof (prove)
using this:
\<exists>x y z. (\<Sum>i\<in>{?a, ?b, ?c}. ?f i * i) = x * ?a + y * ?b + z * ?c

goal (1 subgoal):
 1. (\<And>x y z. (\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c

goal (1 subgoal):
 1. (\<And>f1 f2 f3. f1 * a + f2 * b + f3 * c = d \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using d that
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>{a, b, c}. f i * i) = x * a + y * b + z * c
(\<Sum>i\<in>{a, b, c}. f i * i) = d
?f1.1 * a + ?f2.1 * b + ?f3.1 * c = d \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f1 * a + f2 * b + f3 * c = d

goal (2 subgoals):
 1. d \<in> ideal_generated {d', c}
 2. finite {d', c}
[PROOF STEP]
obtain k where k: "f1*a + f2*b = k*d'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. f1 * a + f2 * b = k * d' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>k. f1 * a + f2 * b = k * d' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "f1*a + f2*b \<in> ideal_generated{a,b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f1 * a + f2 * b \<in> ideal_generated {a, b}
[PROOF STEP]
using ideal_generated_pair
[PROOF STATE]
proof (prove)
using this:
ideal_generated {?a, ?b} = {p * ?a + q * ?b |p q. True}

goal (1 subgoal):
 1. f1 * a + f2 * b \<in> ideal_generated {a, b}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f1 * a + f2 * b \<in> ideal_generated {a, b}

goal (1 subgoal):
 1. (\<And>k. f1 * a + f2 * b = k * d' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f1 * a + f2 * b \<in> ideal_generated {a, b}

goal (1 subgoal):
 1. (\<And>k. f1 * a + f2 * b = k * d' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "... = ideal_generated {d'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated {a, b} = ideal_generated {d'}
[PROOF STEP]
using i2
[PROOF STATE]
proof (prove)
using this:
ideal_generated {a, b} = ideal_generated {d'}

goal (1 subgoal):
 1. ideal_generated {a, b} = ideal_generated {d'}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ideal_generated {a, b} = ideal_generated {d'}

goal (1 subgoal):
 1. (\<And>k. f1 * a + f2 * b = k * d' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ideal_generated {a, b} = ideal_generated {d'}

goal (1 subgoal):
 1. (\<And>k. f1 * a + f2 * b = k * d' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "... = {k*d' |k. k\<in>UNIV}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated {d'} = {k * d' |k. k \<in> UNIV}
[PROOF STEP]
using ideal_generated_singleton
[PROOF STATE]
proof (prove)
using this:
ideal_generated {?a} = {k * ?a |k. k \<in> UNIV}

goal (1 subgoal):
 1. ideal_generated {d'} = {k * d' |k. k \<in> UNIV}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ideal_generated {d'} = {k * d' |k. k \<in> UNIV}

goal (1 subgoal):
 1. (\<And>k. f1 * a + f2 * b = k * d' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f1 * a + f2 * b \<in> {k * d' |k. k \<in> UNIV}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f1 * a + f2 * b \<in> {k * d' |k. k \<in> UNIV}

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
f1 * a + f2 * b \<in> {k * d' |k. k \<in> UNIV}
f1 * a + f2 * b = ?k1 * d' \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f1 * a + f2 * b = k * d'

goal (2 subgoals):
 1. d \<in> ideal_generated {d', c}
 2. finite {d', c}
[PROOF STEP]
have "k*d'+f3*c=d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k * d' + f3 * c = d
[PROOF STEP]
using f k
[PROOF STATE]
proof (prove)
using this:
f1 * a + f2 * b + f3 * c = d
f1 * a + f2 * b = k * d'

goal (1 subgoal):
 1. k * d' + f3 * c = d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k * d' + f3 * c = d

goal (2 subgoals):
 1. d \<in> ideal_generated {d', c}
 2. finite {d', c}
[PROOF STEP]
thus "d \<in> ideal_generated {d', c}"
[PROOF STATE]
proof (prove)
using this:
k * d' + f3 * c = d

goal (1 subgoal):
 1. d \<in> ideal_generated {d', c}
[PROOF STEP]
using ideal_generated_pair
[PROOF STATE]
proof (prove)
using this:
k * d' + f3 * c = d
ideal_generated {?a, ?b} = {p * ?a + q * ?b |p q. True}

goal (1 subgoal):
 1. d \<in> ideal_generated {d', c}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
d \<in> ideal_generated {d', c}

goal (1 subgoal):
 1. finite {d', c}
[PROOF STEP]
qed (simp)
[PROOF STATE]
proof (state)
this:
ideal_generated {d} \<subseteq> ideal_generated {d', c}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ideal_generated_dvd:
  assumes i: "ideal_generated {a,b::'a} = ideal_generated{d} "
  and a: "d' dvd a" and b: "d' dvd b"
shows "d' dvd d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d' dvd d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d' dvd d
[PROOF STEP]
obtain p q where "p*a+q*b = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p q. p * a + q * b = d \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using i ideal_generated_pair_exists
[PROOF STATE]
proof (prove)
using this:
ideal_generated {a, b} = ideal_generated {d}
ideal_generated {?a, ?b} = ideal_generated {?d} \<Longrightarrow> \<exists>p q. p * ?a + q * ?b = ?d

goal (1 subgoal):
 1. (\<And>p q. p * a + q * b = d \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p * a + q * b = d

goal (1 subgoal):
 1. d' dvd d
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p * a + q * b = d

goal (1 subgoal):
 1. d' dvd d
[PROOF STEP]
using a b
[PROOF STATE]
proof (prove)
using this:
p * a + q * b = d
d' dvd a
d' dvd b

goal (1 subgoal):
 1. d' dvd d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d' dvd d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ideal_generated_dvd2:
  assumes i: "ideal_generated S = ideal_generated{d::'a} "
  and "finite S"
  and x: "\<forall>x\<in>S. d' dvd x"
shows "d' dvd d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d' dvd d
[PROOF STEP]
by (metis assms dvd_ideal_generated_singleton ideal_generated_dvd_subset)


[STATEMENT]
lemma sum_two_elements':
  fixes d::'a
  assumes s: "(\<Sum>i\<in>{a,b}. f i * i) = d"
  obtains p and q where "d = p * a + q * b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p q. d = p * a + q * b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (cases "a=b")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>p q. d = p * a + q * b \<Longrightarrow> thesis; a = b\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>p q. d = p * a + q * b \<Longrightarrow> thesis; a \<noteq> b\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = b

goal (2 subgoals):
 1. \<lbrakk>\<And>p q. d = p * a + q * b \<Longrightarrow> thesis; a = b\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>p q. d = p * a + q * b \<Longrightarrow> thesis; a \<noteq> b\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = b

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (metis (no_types, lifting) add_diff_cancel_left' emptyE finite.emptyI insert_absorb2
        left_diff_distrib' s sum.insert sum_singleton that)
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<lbrakk>\<And>p q. d = p * a + q * b \<Longrightarrow> thesis; a \<noteq> b\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>p q. d = p * a + q * b \<Longrightarrow> thesis; a \<noteq> b\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> b

goal (1 subgoal):
 1. \<lbrakk>\<And>p q. d = p * a + q * b \<Longrightarrow> thesis; a \<noteq> b\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>{a, b}. f i * i) = d

goal (1 subgoal):
 1. thesis
[PROOF STEP]
unfolding sum_two_elements[OF False]
[PROOF STATE]
proof (prove)
using this:
f a * a + f b * b = d

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
f a * a + f b * b = d
d = ?p * a + ?q * b \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed