[STATEMENT]
lemma all_fin_gen_ideals_are_principal_imp_bezout:
  assumes all: "\<forall>I::'a set. finitely_generated_ideal I \<longrightarrow> principal_ideal I"
  shows "OFCLASS ('a, bezout_ring_class)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OFCLASS('a, bezout_ring_class)
[PROOF STEP]
proof (intro_classes)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<exists>p q d. p * a + q * b = d \<and> d dvd a \<and> d dvd b \<and> (\<forall>d'. d' dvd a \<and> d' dvd b \<longrightarrow> d' dvd d)
[PROOF STEP]
fix a b::'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<exists>p q d. p * a + q * b = d \<and> d dvd a \<and> d dvd b \<and> (\<forall>d'. d' dvd a \<and> d' dvd b \<longrightarrow> d' dvd d)
[PROOF STEP]
obtain d where ideal_d: "ideal_generated {a,b} = ideal_generated {d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d. ideal_generated {a, b} = ideal_generated {d} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using all
[PROOF STATE]
proof (prove)
using this:
\<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I

goal (1 subgoal):
 1. (\<And>d. ideal_generated {a, b} = ideal_generated {d} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding finitely_generated_ideal_def
[PROOF STATE]
proof (prove)
using this:
\<forall>I. ideal I \<and> (\<exists>S. finite S \<and> ideal_generated S = I) \<longrightarrow> principal_ideal I

goal (1 subgoal):
 1. (\<And>d. ideal_generated {a, b} = ideal_generated {d} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis finite.emptyI finite_insert ideal_ideal_generated principal_ideal_def)
[PROOF STATE]
proof (state)
this:
ideal_generated {a, b} = ideal_generated {d}

goal (1 subgoal):
 1. \<And>a b. \<exists>p q d. p * a + q * b = d \<and> d dvd a \<and> d dvd b \<and> (\<forall>d'. d' dvd a \<and> d' dvd b \<longrightarrow> d' dvd d)
[PROOF STEP]
have a_in_d: "a \<in> ideal_generated {d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> ideal_generated {d}
[PROOF STEP]
using ideal_d ideal_generated_subset_generator
[PROOF STATE]
proof (prove)
using this:
ideal_generated {a, b} = ideal_generated {d}
ideal_generated ?A = ?I \<Longrightarrow> ?A \<subseteq> ?I

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

goal (1 subgoal):
 1. \<And>a b. \<exists>p q d. p * a + q * b = d \<and> d dvd a \<and> d dvd b \<and> (\<forall>d'. d' dvd a \<and> d' dvd b \<longrightarrow> d' dvd d)
[PROOF STEP]
have b_in_d: "b \<in> ideal_generated {d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in> ideal_generated {d}
[PROOF STEP]
using ideal_d ideal_generated_subset_generator
[PROOF STATE]
proof (prove)
using this:
ideal_generated {a, b} = ideal_generated {d}
ideal_generated ?A = ?I \<Longrightarrow> ?A \<subseteq> ?I

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

goal (1 subgoal):
 1. \<And>a b. \<exists>p q d. p * a + q * b = d \<and> d dvd a \<and> d dvd b \<and> (\<forall>d'. d' dvd a \<and> d' dvd b \<longrightarrow> d' dvd d)
[PROOF STEP]
have d_in_ab: "d \<in> ideal_generated {a,b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<in> ideal_generated {a, b}
[PROOF STEP]
using ideal_d ideal_generated_subset_generator
[PROOF STATE]
proof (prove)
using this:
ideal_generated {a, b} = ideal_generated {d}
ideal_generated ?A = ?I \<Longrightarrow> ?A \<subseteq> ?I

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. \<And>a b. \<exists>p q d. p * a + q * b = d \<and> d dvd a \<and> d dvd b \<and> (\<forall>d'. d' dvd a \<and> d' dvd b \<longrightarrow> d' dvd d)
[PROOF STEP]
obtain f where "(\<Sum>i\<in>{a,b}. f i * i) = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. (\<Sum>i\<in>{a, b}. f i * i) = d \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obtain_sum_ideal_generated[OF d_in_ab]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite {a, b}; \<And>f. (\<Sum>i\<in>{a, b}. f i * i) = d \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. \<And>a b. \<exists>p q d. p * a + q * b = d \<and> d dvd a \<and> d dvd b \<and> (\<forall>d'. d' dvd a \<and> d' dvd b \<longrightarrow> d' dvd d)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i\<in>{a, b}. f i * i) = d
[PROOF STEP]
obtain p q where d_eq: "d = p*a + q*b"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>{a, b}. f i * i) = d

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

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

goal (1 subgoal):
 1. \<And>a b. \<exists>p q d. p * a + q * b = d \<and> d dvd a \<and> d dvd b \<and> (\<forall>d'. d' dvd a \<and> d' dvd b \<longrightarrow> d' dvd d)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
d = p * a + q * b

goal (1 subgoal):
 1. \<And>a b. \<exists>p q d. p * a + q * b = d \<and> d dvd a \<and> d dvd b \<and> (\<forall>d'. d' dvd a \<and> d' dvd b \<longrightarrow> d' dvd d)
[PROOF STEP]
have d_dvd_a: "d dvd a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d dvd a
[PROOF STEP]
by (metis dvd_ideal_generated_singleton ideal_d ideal_generated_subset insert_commute
        subset_insertI)
[PROOF STATE]
proof (state)
this:
d dvd a

goal (1 subgoal):
 1. \<And>a b. \<exists>p q d. p * a + q * b = d \<and> d dvd a \<and> d dvd b \<and> (\<forall>d'. d' dvd a \<and> d' dvd b \<longrightarrow> d' dvd d)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
d dvd a

goal (1 subgoal):
 1. \<And>a b. \<exists>p q d. p * a + q * b = d \<and> d dvd a \<and> d dvd b \<and> (\<forall>d'. d' dvd a \<and> d' dvd b \<longrightarrow> d' dvd d)
[PROOF STEP]
have "d dvd b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d dvd b
[PROOF STEP]
by (metis dvd_ideal_generated_singleton ideal_d ideal_generated_subset subset_insertI)
[PROOF STATE]
proof (state)
this:
d dvd b

goal (1 subgoal):
 1. \<And>a b. \<exists>p q d. p * a + q * b = d \<and> d dvd a \<and> d dvd b \<and> (\<forall>d'. d' dvd a \<and> d' dvd b \<longrightarrow> d' dvd d)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
d dvd b

goal (1 subgoal):
 1. \<And>a b. \<exists>p q d. p * a + q * b = d \<and> d dvd a \<and> d dvd b \<and> (\<forall>d'. d' dvd a \<and> d' dvd b \<longrightarrow> d' dvd d)
[PROOF STEP]
have "d' dvd d" if d'_dvd: "d' dvd a \<and> d' dvd b" for 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 s1 s2 where s1_dvd: "a = s1*d'" and s2_dvd: "b = s2*d'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1 s2. \<lbrakk>a = s1 * d'; b = s2 * d'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using mult.commute d'_dvd
[PROOF STATE]
proof (prove)
using this:
?a * ?b = ?b * ?a
d' dvd a \<and> d' dvd b

goal (1 subgoal):
 1. (\<And>s1 s2. \<lbrakk>a = s1 * d'; b = s2 * d'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dvd_def
[PROOF STATE]
proof (prove)
using this:
?a * ?b = ?b * ?a
(\<exists>k. a = d' * k) \<and> (\<exists>k. b = d' * k)

goal (1 subgoal):
 1. (\<And>s1 s2. \<lbrakk>a = s1 * d'; b = s2 * d'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = s1 * d'
b = s2 * d'

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

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

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

goal (1 subgoal):
 1. d' dvd d
[PROOF STEP]
have "...= p * s1 * d' + q * s2 *d'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p * a + q * b = p * s1 * d' + q * s2 * d'
[PROOF STEP]
unfolding s1_dvd s2_dvd
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p * (s1 * d') + q * (s2 * d') = p * s1 * d' + q * s2 * d'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p * a + q * b = p * s1 * d' + q * s2 * d'

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

goal (1 subgoal):
 1. d' dvd d
[PROOF STEP]
have "... = (p * s1 + q * s2) * d'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p * s1 * d' + q * s2 * d' = (p * s1 + q * s2) * d'
[PROOF STEP]
by (simp add: ring_class.ring_distribs(2))
[PROOF STATE]
proof (state)
this:
p * s1 * d' + q * s2 * d' = (p * s1 + q * s2) * d'

goal (1 subgoal):
 1. d' dvd d
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
d = (p * s1 + q * s2) * d'
[PROOF STEP]
show "d' dvd d"
[PROOF STATE]
proof (prove)
using this:
d = (p * s1 + q * s2) * d'

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

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

goal (1 subgoal):
 1. \<exists>k. d = d' * k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d' dvd d

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?d' dvd a \<and> ?d' dvd b \<Longrightarrow> ?d' dvd d

goal (1 subgoal):
 1. \<And>a b. \<exists>p q d. p * a + q * b = d \<and> d dvd a \<and> d dvd b \<and> (\<forall>d'. d' dvd a \<and> d' dvd b \<longrightarrow> d' dvd d)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
d = p * a + q * b
d dvd a
d dvd b
?d' dvd a \<and> ?d' dvd b \<Longrightarrow> ?d' dvd d
[PROOF STEP]
show "\<exists>p q d. p * a + q * b = d \<and> d dvd a \<and> d dvd b
  \<and> (\<forall>d'. d' dvd a \<and> d' dvd b \<longrightarrow> d' dvd d)"
[PROOF STATE]
proof (prove)
using this:
d = p * a + q * b
d dvd a
d dvd b
?d' dvd a \<and> ?d' dvd b \<Longrightarrow> ?d' dvd d

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exists_bezout_extended:
  assumes S: "finite S" and ne: "S \<noteq> {}"
  shows "\<exists>f d. (\<Sum>a\<in>S. f a * a) = d \<and> (\<forall>a\<in>S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>S. d' dvd a) \<longrightarrow> d' dvd d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f d. (\<Sum>a\<in>S. f a * a) = d \<and> (\<forall>a\<in>S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
using S ne
[PROOF STATE]
proof (prove)
using this:
finite S
S \<noteq> {}

goal (1 subgoal):
 1. \<exists>f d. (\<Sum>a\<in>S. f a * a) = d \<and> (\<forall>a\<in>S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
proof (induct S)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {} \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>{}. f a * a) = d \<and> Ball {} ((dvd) d) \<and> (\<forall>d'. Ball {} ((dvd) d') \<longrightarrow> d' dvd d)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>F. f a * a) = d \<and> Ball F ((dvd) d) \<and> (\<forall>d'. Ball F ((dvd) d') \<longrightarrow> d' dvd d); insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x F. f a * a) = d \<and> Ball (insert x F) ((dvd) d) \<and> (\<forall>d'. Ball (insert x F) ((dvd) d') \<longrightarrow> d' dvd d)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
{} \<noteq> {}

goal (2 subgoals):
 1. {} \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>{}. f a * a) = d \<and> Ball {} ((dvd) d) \<and> (\<forall>d'. Ball {} ((dvd) d') \<longrightarrow> d' dvd d)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>F. f a * a) = d \<and> Ball F ((dvd) d) \<and> (\<forall>d'. Ball F ((dvd) d') \<longrightarrow> d' dvd d); insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x F. f a * a) = d \<and> Ball (insert x F) ((dvd) d) \<and> (\<forall>d'. Ball (insert x F) ((dvd) d') \<longrightarrow> d' dvd d)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{} \<noteq> {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
{} \<noteq> {}

goal (1 subgoal):
 1. \<exists>f d. (\<Sum>a\<in>{}. f a * a) = d \<and> (\<forall>a\<in>{}. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>{}. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>f d. (\<Sum>a\<in>{}. f a * a) = d \<and> (\<forall>a\<in>{}. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>{}. d' dvd a) \<longrightarrow> d' dvd d)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>F. f a * a) = d \<and> Ball F ((dvd) d) \<and> (\<forall>d'. Ball F ((dvd) d') \<longrightarrow> d' dvd d); insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x F. f a * a) = d \<and> Ball (insert x F) ((dvd) d) \<and> (\<forall>d'. Ball (insert x F) ((dvd) d') \<longrightarrow> d' dvd d)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>F. f a * a) = d \<and> Ball F ((dvd) d) \<and> (\<forall>d'. Ball F ((dvd) d') \<longrightarrow> d' dvd d); insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x F. f a * a) = d \<and> Ball (insert x F) ((dvd) d) \<and> (\<forall>d'. Ball (insert x F) ((dvd) d') \<longrightarrow> d' dvd d)
[PROOF STEP]
case (insert x S)
[PROOF STATE]
proof (state)
this:
finite S
x \<notin> S
S \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>S. f a * a) = d \<and> (\<forall>a\<in>S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>S. d' dvd a) \<longrightarrow> d' dvd d)
insert x S \<noteq> {}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>F. f a * a) = d \<and> Ball F ((dvd) d) \<and> (\<forall>d'. Ball F ((dvd) d') \<longrightarrow> d' dvd d); insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x F. f a * a) = d \<and> Ball (insert x F) ((dvd) d) \<and> (\<forall>d'. Ball (insert x F) ((dvd) d') \<longrightarrow> d' dvd d)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
proof (cases  "S={}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. S = {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
 2. S \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
S = {}

goal (2 subgoals):
 1. S = {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
 2. S \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
let ?f = "\<lambda>x. 1"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. S = {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
 2. S \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
by (rule exI[of _ ?f], insert True, auto)
[PROOF STATE]
proof (state)
this:
\<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
S \<noteq> {}

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
note ne = False
[PROOF STATE]
proof (state)
this:
S \<noteq> {}

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
note x_notin_S = insert.hyps(2)
[PROOF STATE]
proof (state)
this:
x \<notin> S

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
obtain f d where sum_eq_d: "(\<Sum>a\<in>S. f a * a) = d"
      and d_dvd_each_a: "(\<forall>a\<in>S. d dvd a)"
      and d_is_gcd: "(\<forall>d'. (\<forall>a\<in>S. d' dvd a) \<longrightarrow> d' dvd d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f d. \<lbrakk>(\<Sum>a\<in>S. f a * a) = d; \<forall>a\<in>S. d dvd a; \<forall>d'. (\<forall>a\<in>S. d' dvd a) \<longrightarrow> d' dvd d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using insert.hyps(3)[OF ne]
[PROOF STATE]
proof (prove)
using this:
\<exists>f d. (\<Sum>a\<in>S. f a * a) = d \<and> (\<forall>a\<in>S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>S. d' dvd a) \<longrightarrow> d' dvd d)

goal (1 subgoal):
 1. (\<And>f d. \<lbrakk>(\<Sum>a\<in>S. f a * a) = d; \<forall>a\<in>S. d dvd a; \<forall>d'. (\<forall>a\<in>S. d' dvd a) \<longrightarrow> d' dvd d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. f a * a) = d
\<forall>a\<in>S. d dvd a
\<forall>d'. (\<forall>a\<in>S. d' dvd a) \<longrightarrow> d' dvd d

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
have "\<exists>p q d'. p * d + q * x = d' \<and> d' dvd d \<and> d' dvd x \<and> (\<forall>c. c dvd d \<and> c dvd x \<longrightarrow> c dvd d')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p q d'. p * d + q * x = d' \<and> d' dvd d \<and> d' dvd x \<and> (\<forall>c. c dvd d \<and> c dvd x \<longrightarrow> c dvd d')
[PROOF STEP]
using exists_bezout
[PROOF STATE]
proof (prove)
using this:
\<exists>p q d. p * ?a + q * ?b = d \<and> d dvd ?a \<and> d dvd ?b \<and> (\<forall>d'. d' dvd ?a \<and> d' dvd ?b \<longrightarrow> d' dvd d)

goal (1 subgoal):
 1. \<exists>p q d'. p * d + q * x = d' \<and> d' dvd d \<and> d' dvd x \<and> (\<forall>c. c dvd d \<and> c dvd x \<longrightarrow> c dvd d')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>p q d'. p * d + q * x = d' \<and> d' dvd d \<and> d' dvd x \<and> (\<forall>c. c dvd d \<and> c dvd x \<longrightarrow> c dvd d')

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>p q d'. p * d + q * x = d' \<and> d' dvd d \<and> d' dvd x \<and> (\<forall>c. c dvd d \<and> c dvd x \<longrightarrow> c dvd d')
[PROOF STEP]
obtain p q d' where pd_qx_d': "p*d + q*x = d'"
      and d'_dvd_d: "d' dvd d" and d'_dvd_x: "d' dvd x"
      and d'_dvd: "\<forall>c. (c dvd d \<and> c dvd x) \<longrightarrow> c dvd d'"
[PROOF STATE]
proof (prove)
using this:
\<exists>p q d'. p * d + q * x = d' \<and> d' dvd d \<and> d' dvd x \<and> (\<forall>c. c dvd d \<and> c dvd x \<longrightarrow> c dvd d')

goal (1 subgoal):
 1. (\<And>p q d'. \<lbrakk>p * d + q * x = d'; d' dvd d; d' dvd x; \<forall>c. c dvd d \<and> c dvd x \<longrightarrow> c dvd d'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p * d + q * x = d'
d' dvd d
d' dvd x
\<forall>c. c dvd d \<and> c dvd x \<longrightarrow> c dvd d'

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
let ?f = "\<lambda>a. if a = x then q else p * f a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
have "(\<Sum>a\<in>insert x S. ?f a * a) = d'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>insert x S. (if a = x then q else p * f a) * a) = d'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>a\<in>insert x S. (if a = x then q else p * f a) * a) = d'
[PROOF STEP]
have "(\<Sum>a\<in>insert x S. ?f a * a) = (\<Sum>a\<in>S. ?f a * a) + ?f x * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>insert x S. (if a = x then q else p * f a) * a) = (\<Sum>a\<in>S. (if a = x then q else p * f a) * a) + (if x = x then q else p * f x) * x
[PROOF STEP]
by (simp add: add_commute insert.hyps(1) insert.hyps(2))
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>insert x S. (if a = x then q else p * f a) * a) = (\<Sum>a\<in>S. (if a = x then q else p * f a) * a) + (if x = x then q else p * f x) * x

goal (1 subgoal):
 1. (\<Sum>a\<in>insert x S. (if a = x then q else p * f a) * a) = d'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>insert x S. (if a = x then q else p * f a) * a) = (\<Sum>a\<in>S. (if a = x then q else p * f a) * a) + (if x = x then q else p * f x) * x

goal (1 subgoal):
 1. (\<Sum>a\<in>insert x S. (if a = x then q else p * f a) * a) = d'
[PROOF STEP]
have "... = p * (\<Sum>a\<in>S. f a * a) + q * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>S. (if a = x then q else p * f a) * a) + (if x = x then q else p * f x) * x = p * (\<Sum>a\<in>S. f a * a) + q * x
[PROOF STEP]
unfolding sum_distrib_left
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>S. (if a = x then q else p * f a) * a) + (if x = x then q else p * f x) * x = (\<Sum>n\<in>S. p * (f n * n)) + q * x
[PROOF STEP]
by (auto, rule sum.cong, insert x_notin_S,
            auto simp add: mult.semigroup_axioms semigroup.assoc)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. (if a = x then q else p * f a) * a) + (if x = x then q else p * f x) * x = p * (\<Sum>a\<in>S. f a * a) + q * x

goal (1 subgoal):
 1. (\<Sum>a\<in>insert x S. (if a = x then q else p * f a) * a) = d'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>a\<in>insert x S. (if a = x then q else p * f a) * a) = p * (\<Sum>a\<in>S. f a * a) + q * x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>a\<in>insert x S. (if a = x then q else p * f a) * a) = p * (\<Sum>a\<in>S. f a * a) + q * x

goal (1 subgoal):
 1. (\<Sum>a\<in>insert x S. (if a = x then q else p * f a) * a) = d'
[PROOF STEP]
using pd_qx_d' sum_eq_d
[PROOF STATE]
proof (prove)
using this:
(\<Sum>a\<in>insert x S. (if a = x then q else p * f a) * a) = p * (\<Sum>a\<in>S. f a * a) + q * x
p * d + q * x = d'
(\<Sum>a\<in>S. f a * a) = d

goal (1 subgoal):
 1. (\<Sum>a\<in>insert x S. (if a = x then q else p * f a) * a) = d'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>insert x S. (if a = x then q else p * f a) * a) = d'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>insert x S. (if a = x then q else p * f a) * a) = d'

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>insert x S. (if a = x then q else p * f a) * a) = d'

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
have "(\<forall>a\<in>insert x S. d' dvd a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>insert x S. d' dvd a
[PROOF STEP]
by (metis d'_dvd_d d'_dvd_x d_dvd_each_a insert_iff local.dvdE local.dvd_mult_left)
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>insert x S. d' dvd a

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>insert x S. d' dvd a

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
have " (\<forall>c. (\<forall>a\<in>insert x S. c dvd a) \<longrightarrow> c dvd d')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. (\<forall>a\<in>insert x S. c dvd a) \<longrightarrow> c dvd d'
[PROOF STEP]
by (simp add: d'_dvd d_is_gcd)
[PROOF STATE]
proof (state)
this:
\<forall>c. (\<forall>a\<in>insert x S. c dvd a) \<longrightarrow> c dvd d'

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>a\<in>insert x S. (if a = x then q else p * f a) * a) = d'
\<forall>a\<in>insert x S. d' dvd a
\<forall>c. (\<forall>a\<in>insert x S. c dvd a) \<longrightarrow> c dvd d'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>a\<in>insert x S. (if a = x then q else p * f a) * a) = d'
\<forall>a\<in>insert x S. d' dvd a
\<forall>c. (\<forall>a\<in>insert x S. c dvd a) \<longrightarrow> c dvd d'

goal (1 subgoal):
 1. \<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>f d. (\<Sum>a\<in>insert x S. f a * a) = d \<and> (\<forall>a\<in>insert x S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>insert x S. d' dvd a) \<longrightarrow> d' dvd d)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ideal_generated_empty: "ideal_generated {} = {0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated {} = {0::'a}
[PROOF STEP]
unfolding ideal_generated_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Inter> {I. ideal I \<and> {} \<subseteq> I} = {0::'a}
[PROOF STEP]
using ideal_generated_0
[PROOF STATE]
proof (prove)
using this:
ideal_generated {0::?'a} = {0::?'a}

goal (1 subgoal):
 1. \<Inter> {I. ideal I \<and> {} \<subseteq> I} = {0::'a}
[PROOF STEP]
by (metis empty_subsetI ideal_generated_def ideal_generated_subset ideal_ideal_generated
      ideal_not_empty subset_singletonD)


[STATEMENT]
lemma bezout_imp_all_fin_gen_ideals_are_principal:
  fixes I::"'a :: bezout_ring set"
  assumes fin: "finitely_generated_ideal I"
  shows "principal_ideal I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. principal_ideal I
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. principal_ideal I
[PROOF STEP]
obtain S where fin_S: "finite S" and ideal_gen_S: "ideal_generated S = I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>S. \<lbrakk>finite S; ideal_generated S = I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using fin
[PROOF STATE]
proof (prove)
using this:
finitely_generated_ideal I

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>finite S; ideal_generated S = I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding finitely_generated_ideal_def
[PROOF STATE]
proof (prove)
using this:
ideal I \<and> (\<exists>S. finite S \<and> ideal_generated S = I)

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>finite S; ideal_generated S = I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite S
ideal_generated S = I

goal (1 subgoal):
 1. principal_ideal I
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. principal_ideal I
[PROOF STEP]
proof (cases "S = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. S = {} \<Longrightarrow> principal_ideal I
 2. S \<noteq> {} \<Longrightarrow> principal_ideal I
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
S = {}

goal (2 subgoals):
 1. S = {} \<Longrightarrow> principal_ideal I
 2. S \<noteq> {} \<Longrightarrow> principal_ideal I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
S = {}

goal (1 subgoal):
 1. principal_ideal I
[PROOF STEP]
using ideal_gen_S
[PROOF STATE]
proof (prove)
using this:
S = {}
ideal_generated S = I

goal (1 subgoal):
 1. principal_ideal I
[PROOF STEP]
unfolding True
[PROOF STATE]
proof (prove)
using this:
{} = {}
ideal_generated {} = I

goal (1 subgoal):
 1. principal_ideal I
[PROOF STEP]
using ideal_generated_empty ideal_generated_0 principal_ideal_def
[PROOF STATE]
proof (prove)
using this:
{} = {}
ideal_generated {} = I
ideal_generated {} = {0::?'a}
ideal_generated {0::?'a} = {0::?'a}
principal_ideal ?S = (\<exists>a. ideal_generated {a} = ?S)

goal (1 subgoal):
 1. principal_ideal I
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
principal_ideal I

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> principal_ideal I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> principal_ideal I
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
S \<noteq> {}

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> principal_ideal I
[PROOF STEP]
note ne = False
[PROOF STATE]
proof (state)
this:
S \<noteq> {}

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> principal_ideal I
[PROOF STEP]
obtain d f where sum_S_d: "(\<Sum>i\<in>S. f i * i) = d"
    and d_dvd_a: "(\<forall>a\<in>S. d dvd a)" and d_is_gcd: "(\<forall>d'. (\<forall>a\<in>S. d' dvd a) \<longrightarrow> d' dvd d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f d. \<lbrakk>(\<Sum>i\<in>S. f i * i) = d; \<forall>a\<in>S. d dvd a; \<forall>d'. (\<forall>a\<in>S. d' dvd a) \<longrightarrow> d' dvd d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using exists_bezout_extended[OF fin_S ne]
[PROOF STATE]
proof (prove)
using this:
\<exists>f d. (\<Sum>a\<in>S. f a * a) = d \<and> (\<forall>a\<in>S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>S. d' dvd a) \<longrightarrow> d' dvd d)

goal (1 subgoal):
 1. (\<And>f d. \<lbrakk>(\<Sum>i\<in>S. f i * i) = d; \<forall>a\<in>S. d dvd a; \<forall>d'. (\<forall>a\<in>S. d' dvd a) \<longrightarrow> d' dvd d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>S. f i * i) = d
\<forall>a\<in>S. d dvd a
\<forall>d'. (\<forall>a\<in>S. d' dvd a) \<longrightarrow> d' dvd d

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> principal_ideal I
[PROOF STEP]
have d_in_S: "d \<in> ideal_generated S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<in> ideal_generated S
[PROOF STEP]
by (metis fin_S ideal_def ideal_generated_subset_generator
          ideal_ideal_generated sum_S_d sum_left_ideal)
[PROOF STATE]
proof (state)
this:
d \<in> ideal_generated S

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> principal_ideal I
[PROOF STEP]
have "ideal_generated {d} \<subseteq> ideal_generated S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated {d} \<subseteq> ideal_generated S
[PROOF STEP]
by (rule ideal_generated_singleton_subset[OF d_in_S fin_S])
[PROOF STATE]
proof (state)
this:
ideal_generated {d} \<subseteq> ideal_generated S

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> principal_ideal I
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ideal_generated {d} \<subseteq> ideal_generated S

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> principal_ideal I
[PROOF STEP]
have "ideal_generated S \<subseteq> ideal_generated {d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated S \<subseteq> ideal_generated {d}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated S \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated S \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
assume x_in_S: "x \<in> ideal_generated S"
[PROOF STATE]
proof (state)
this:
x \<in> ideal_generated S

goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated S \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
obtain f where sum_S_x: "(\<Sum>a\<in>S. f a * a) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. (\<Sum>a\<in>S. f a * a) = x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using fin_S obtain_sum_ideal_generated x_in_S
[PROOF STATE]
proof (prove)
using this:
finite S
\<lbrakk>?a \<in> ideal_generated ?A; finite ?A; \<And>f. (\<Sum>i\<in>?A. f i * i) = ?a \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
x \<in> ideal_generated S

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

goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated S \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
have d_dvd_each_a: "\<exists>k. a = k * d" if "a \<in> S" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. a = k * d
[PROOF STEP]
by (metis d_dvd_a dvdE mult.commute that)
[PROOF STATE]
proof (state)
this:
?a \<in> S \<Longrightarrow> \<exists>k. ?a = k * d

goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated S \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
let ?g = "\<lambda>a. SOME k. a = k*d"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated S \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
have "x = (\<Sum>a\<in>S. f a * a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = (\<Sum>a\<in>S. f a * a)
[PROOF STEP]
using sum_S_x
[PROOF STATE]
proof (prove)
using this:
(\<Sum>a\<in>S. f a * a) = x

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

goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated S \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x = (\<Sum>a\<in>S. f a * a)

goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated S \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
have "... = (\<Sum>a\<in>S. f a * (?g a * d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>S. f a * a) = (\<Sum>a\<in>S. f a * ((SOME k. a = k * d) * d))
[PROOF STEP]
proof (rule sum.cong)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. S = S
 2. \<And>x. x \<in> S \<Longrightarrow> f x * x = f x * ((SOME k. x = k * d) * d)
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. S = S
 2. \<And>x. x \<in> S \<Longrightarrow> f x * x = f x * ((SOME k. x = k * d) * d)
[PROOF STEP]
assume a_in_S: "a \<in> S"
[PROOF STATE]
proof (state)
this:
a \<in> S

goal (2 subgoals):
 1. S = S
 2. \<And>x. x \<in> S \<Longrightarrow> f x * x = f x * ((SOME k. x = k * d) * d)
[PROOF STEP]
obtain k where a_kd: "a = k * d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. a = k * d \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using d_dvd_each_a a_in_S
[PROOF STATE]
proof (prove)
using this:
?a \<in> S \<Longrightarrow> \<exists>k. ?a = k * d
a \<in> S

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

goal (2 subgoals):
 1. S = S
 2. \<And>x. x \<in> S \<Longrightarrow> f x * x = f x * ((SOME k. x = k * d) * d)
[PROOF STEP]
have "a = ((SOME k. a = k * d) * d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = (SOME k. a = k * d) * d
[PROOF STEP]
by (rule someI_ex, auto simp add: a_kd)
[PROOF STATE]
proof (state)
this:
a = (SOME k. a = k * d) * d

goal (2 subgoals):
 1. S = S
 2. \<And>x. x \<in> S \<Longrightarrow> f x * x = f x * ((SOME k. x = k * d) * d)
[PROOF STEP]
thus "f a * a = f a * ((SOME k. a = k * d) * d)"
[PROOF STATE]
proof (prove)
using this:
a = (SOME k. a = k * d) * d

goal (1 subgoal):
 1. f a * a = f a * ((SOME k. a = k * d) * d)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f a * a = f a * ((SOME k. a = k * d) * d)

goal (1 subgoal):
 1. S = S
[PROOF STEP]
qed (simp)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. f a * a) = (\<Sum>a\<in>S. f a * ((SOME k. a = k * d) * d))

goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated S \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. f a * a) = (\<Sum>a\<in>S. f a * ((SOME k. a = k * d) * d))

goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated S \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
have "... = (\<Sum>a\<in>S. f a * ?g a * d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>S. f a * ((SOME k. a = k * d) * d)) = (\<Sum>a\<in>S. f a * (SOME k. a = k * d) * d)
[PROOF STEP]
by (rule sum.cong, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. f a * ((SOME k. a = k * d) * d)) = (\<Sum>a\<in>S. f a * (SOME k. a = k * d) * d)

goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated S \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. f a * ((SOME k. a = k * d) * d)) = (\<Sum>a\<in>S. f a * (SOME k. a = k * d) * d)

goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated S \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
have "... = (\<Sum>a\<in>S. f a * ?g a)*d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>S. f a * (SOME k. a = k * d) * d) = (\<Sum>a\<in>S. f a * (SOME k. a = k * d)) * d
[PROOF STEP]
using sum_distrib_right[of _ S d]
[PROOF STATE]
proof (prove)
using this:
sum ?f S * d = (\<Sum>n\<in>S. ?f n * d)

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

goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated S \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x = (\<Sum>a\<in>S. f a * (SOME k. a = k * d)) * d
[PROOF STEP]
show "x \<in> ideal_generated {d}"
[PROOF STATE]
proof (prove)
using this:
x = (\<Sum>a\<in>S. f a * (SOME k. a = k * d)) * d

goal (1 subgoal):
 1. x \<in> ideal_generated {d}
[PROOF STEP]
by (meson contra_subsetD dvd_ideal_generated_singleton' dvd_triv_right
            ideal_generated_in singletonI)
[PROOF STATE]
proof (state)
this:
x \<in> ideal_generated {d}

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

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> principal_ideal I
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ideal_generated {d} \<subseteq> ideal_generated S
ideal_generated S \<subseteq> ideal_generated {d}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ideal_generated {d} \<subseteq> ideal_generated S
ideal_generated S \<subseteq> ideal_generated {d}

goal (1 subgoal):
 1. principal_ideal I
[PROOF STEP]
unfolding principal_ideal_def
[PROOF STATE]
proof (prove)
using this:
ideal_generated {d} \<subseteq> ideal_generated S
ideal_generated S \<subseteq> ideal_generated {d}

goal (1 subgoal):
 1. \<exists>a. ideal_generated {a} = I
[PROOF STEP]
using ideal_gen_S
[PROOF STATE]
proof (prove)
using this:
ideal_generated {d} \<subseteq> ideal_generated S
ideal_generated S \<subseteq> ideal_generated {d}
ideal_generated S = I

goal (1 subgoal):
 1. \<exists>a. ideal_generated {a} = I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
principal_ideal I

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bezout_imp_all_fin_gen_ideals_are_principal_unsatisfactory:
  assumes a1: "class.bezout_ring (*) (1::'b::comm_ring_1) (+) 0 (-) uminus" (*It is algo possible to prove it using OFCLASS*)
  shows "\<forall>I::'b set. finitely_generated_ideal I \<longrightarrow> principal_ideal I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I
[PROOF STEP]
using bezout_imp_all_fin_gen_ideals_are_principal[internalize_sort "'a::bezout_ring"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>class.bezout_ring (*) (1::?'a) (+) (0::?'a) (-) uminus; finitely_generated_ideal ?I\<rbrakk> \<Longrightarrow> principal_ideal ?I

goal (1 subgoal):
 1. \<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I
[PROOF STEP]
using a1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>class.bezout_ring (*) (1::?'a) (+) (0::?'a) (-) uminus; finitely_generated_ideal ?I\<rbrakk> \<Longrightarrow> principal_ideal ?I
class.bezout_ring (*) (1::'b) (+) (0::'b) (-) uminus

goal (1 subgoal):
 1. \<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I
[PROOF STEP]
by auto


[STATEMENT]
lemma OFCLASS_bezout_ring_imp_class_bezout_ring:
  assumes "OFCLASS('a::comm_ring_1,bezout_ring_class)"
  shows "class.bezout_ring ((*)::'a\<Rightarrow>'a\<Rightarrow>'a) 1 (+) 0 (-) uminus"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.bezout_ring (*) (1::'a) (+) (0::'a) (-) uminus
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
OFCLASS('a, bezout_ring_class)

goal (1 subgoal):
 1. class.bezout_ring (*) (1::'a) (+) (0::'a) (-) uminus
[PROOF STEP]
unfolding bezout_ring_class_def class.bezout_ring_def
[PROOF STATE]
proof (prove)
using this:
OFCLASS('a, comm_ring_1_class) &&& class.bezout_ring_axioms (*) (+)

goal (1 subgoal):
 1. class.comm_ring_1 (*) (1::'a) (+) (0::'a) (-) uminus \<and> class.bezout_ring_axioms (*) (+)
[PROOF STEP]
using conjunctionD2[of "OFCLASS('a, comm_ring_1_class)"
                         "class.bezout_ring_axioms ((*)::'a\<Rightarrow>'a\<Rightarrow>'a) (+)"]
[PROOF STATE]
proof (prove)
using this:
OFCLASS('a, comm_ring_1_class) &&& class.bezout_ring_axioms (*) (+)
OFCLASS('a, comm_ring_1_class) &&& class.bezout_ring_axioms (*) (+) \<Longrightarrow> class.bezout_ring_axioms (*) (+)

goal (1 subgoal):
 1. class.comm_ring_1 (*) (1::'a) (+) (0::'a) (-) uminus \<and> class.bezout_ring_axioms (*) (+)
[PROOF STEP]
by (auto, intro_locales)


[STATEMENT]
lemma bezout_ring_iff_fin_gen_principal_ideal:
    "(\<And>I::'a::comm_ring_1 set. finitely_generated_ideal I \<Longrightarrow> principal_ideal I)
    \<equiv> OFCLASS('a, bezout_ring_class)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>I. finitely_generated_ideal I \<Longrightarrow> principal_ideal I) \<equiv> OFCLASS('a, bezout_ring_class)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>I. finitely_generated_ideal I \<Longrightarrow> principal_ideal I) \<Longrightarrow> OFCLASS('a, bezout_ring_class)
 2. \<And>I. \<lbrakk>OFCLASS('a, bezout_ring_class); finitely_generated_ideal I\<rbrakk> \<Longrightarrow> principal_ideal I
[PROOF STEP]
show "(\<And>I::'a::comm_ring_1 set. finitely_generated_ideal I \<Longrightarrow> principal_ideal I)
    \<Longrightarrow> OFCLASS('a, bezout_ring_class)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>I. finitely_generated_ideal I \<Longrightarrow> principal_ideal I) \<Longrightarrow> OFCLASS('a, bezout_ring_class)
[PROOF STEP]
using all_fin_gen_ideals_are_principal_imp_bezout [where ?'a='a]
[PROOF STATE]
proof (prove)
using this:
\<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I \<Longrightarrow> OFCLASS('a, bezout_ring_class)

goal (1 subgoal):
 1. (\<And>I. finitely_generated_ideal I \<Longrightarrow> principal_ideal I) \<Longrightarrow> OFCLASS('a, bezout_ring_class)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<And>I. finitely_generated_ideal I \<Longrightarrow> principal_ideal I) \<Longrightarrow> OFCLASS('a, bezout_ring_class)

goal (1 subgoal):
 1. \<And>I. \<lbrakk>OFCLASS('a, bezout_ring_class); finitely_generated_ideal I\<rbrakk> \<Longrightarrow> principal_ideal I
[PROOF STEP]
show "\<And>I::'a::comm_ring_1 set. OFCLASS('a, bezout_ring_class)
    \<Longrightarrow> finitely_generated_ideal I \<Longrightarrow> principal_ideal I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>I. \<lbrakk>OFCLASS('a, bezout_ring_class); finitely_generated_ideal I\<rbrakk> \<Longrightarrow> principal_ideal I
[PROOF STEP]
using bezout_imp_all_fin_gen_ideals_are_principal_unsatisfactory[where ?'b='a]
[PROOF STATE]
proof (prove)
using this:
class.bezout_ring (*) (1::'a) (+) (0::'a) (-) uminus \<Longrightarrow> \<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I

goal (1 subgoal):
 1. \<And>I. \<lbrakk>OFCLASS('a, bezout_ring_class); finitely_generated_ideal I\<rbrakk> \<Longrightarrow> principal_ideal I
[PROOF STEP]
using OFCLASS_bezout_ring_imp_class_bezout_ring[where ?'a='a]
[PROOF STATE]
proof (prove)
using this:
class.bezout_ring (*) (1::'a) (+) (0::'a) (-) uminus \<Longrightarrow> \<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I
OFCLASS('a, bezout_ring_class) \<Longrightarrow> class.bezout_ring (*) (1::'a) (+) (0::'a) (-) uminus

goal (1 subgoal):
 1. \<And>I. \<lbrakk>OFCLASS('a, bezout_ring_class); finitely_generated_ideal I\<rbrakk> \<Longrightarrow> principal_ideal I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>OFCLASS('a, bezout_ring_class); finitely_generated_ideal ?I\<rbrakk> \<Longrightarrow> principal_ideal ?I

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bezout_ring_iff_fin_gen_principal_ideal2:
    "(\<forall>I::'a::comm_ring_1 set. finitely_generated_ideal I \<longrightarrow> principal_ideal I)
    = (class.bezout_ring ((*)::'a\<Rightarrow>'a\<Rightarrow>'a) 1 (+) 0 (-) uminus)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I) = class.bezout_ring (*) (1::'a) (+) (0::'a) (-) uminus
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I \<Longrightarrow> class.bezout_ring (*) (1::'a) (+) (0::'a) (-) uminus
 2. class.bezout_ring (*) (1::'a) (+) (0::'a) (-) uminus \<Longrightarrow> \<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I
[PROOF STEP]
show "\<forall>I::'a::comm_ring_1 set. finitely_generated_ideal I \<longrightarrow> principal_ideal I
      \<Longrightarrow> class.bezout_ring (*) 1 (+) (0::'a) (-) uminus"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I \<Longrightarrow> class.bezout_ring (*) (1::'a) (+) (0::'a) (-) uminus
[PROOF STEP]
using all_fin_gen_ideals_are_principal_imp_bezout[where ?'a='a]
[PROOF STATE]
proof (prove)
using this:
\<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I \<Longrightarrow> OFCLASS('a, bezout_ring_class)

goal (1 subgoal):
 1. \<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I \<Longrightarrow> class.bezout_ring (*) (1::'a) (+) (0::'a) (-) uminus
[PROOF STEP]
using OFCLASS_bezout_ring_imp_class_bezout_ring[where ?'a='a]
[PROOF STATE]
proof (prove)
using this:
\<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I \<Longrightarrow> OFCLASS('a, bezout_ring_class)
OFCLASS('a, bezout_ring_class) \<Longrightarrow> class.bezout_ring (*) (1::'a) (+) (0::'a) (-) uminus

goal (1 subgoal):
 1. \<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I \<Longrightarrow> class.bezout_ring (*) (1::'a) (+) (0::'a) (-) uminus
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I \<Longrightarrow> class.bezout_ring (*) (1::'a) (+) (0::'a) (-) uminus

goal (1 subgoal):
 1. class.bezout_ring (*) (1::'a) (+) (0::'a) (-) uminus \<Longrightarrow> \<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I
[PROOF STEP]
show "class.bezout_ring (*) 1 (+) (0::'a) (-) uminus \<Longrightarrow> \<forall>I::'a set.
    finitely_generated_ideal I \<longrightarrow> principal_ideal I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.bezout_ring (*) (1::'a) (+) (0::'a) (-) uminus \<Longrightarrow> \<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I
[PROOF STEP]
using bezout_imp_all_fin_gen_ideals_are_principal_unsatisfactory
[PROOF STATE]
proof (prove)
using this:
class.bezout_ring (*) (1::?'b) (+) (0::?'b) (-) uminus \<Longrightarrow> \<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I

goal (1 subgoal):
 1. class.bezout_ring (*) (1::'a) (+) (0::'a) (-) uminus \<Longrightarrow> \<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
class.bezout_ring (*) (1::'a) (+) (0::'a) (-) uminus \<Longrightarrow> \<forall>I. finitely_generated_ideal I \<longrightarrow> principal_ideal I

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma convergent_Cauchy_dist:
  fixes u v::"nat \<Rightarrow> ('a::metric_space)"
  assumes "Cauchy u" "Cauchy v"
  shows "convergent (\<lambda>n. dist (u n) (v n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convergent (\<lambda>n. dist (u n) (v n))
[PROOF STEP]
proof (rule real_Cauchy_convergent, intro CauchyI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
fix e::real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
assume "e > 0"
[PROOF STATE]
proof (state)
this:
0 < e

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
obtain Nu where Nu: "\<forall>n \<ge> Nu. \<forall>m \<ge> Nu. dist (u n) (u m) < e/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Nu. \<forall>n\<ge>Nu. \<forall>m\<ge>Nu. dist (u n) (u m) < e / 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
Cauchy u

goal (1 subgoal):
 1. (\<And>Nu. \<forall>n\<ge>Nu. \<forall>m\<ge>Nu. dist (u n) (u m) < e / 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis \<open>0 < e\<close> less_divide_eq_numeral1(1) metric_CauchyD mult_zero_left)
[PROOF STATE]
proof (state)
this:
\<forall>n\<ge>Nu. \<forall>m\<ge>Nu. dist (u n) (u m) < e / 2

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
obtain Nv where Nv: "\<forall>n \<ge> Nv. \<forall>m \<ge> Nv. dist (v n) (v m) < e/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Nv. \<forall>n\<ge>Nv. \<forall>m\<ge>Nv. dist (v n) (v m) < e / 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
Cauchy v

goal (1 subgoal):
 1. (\<And>Nv. \<forall>n\<ge>Nv. \<forall>m\<ge>Nv. dist (v n) (v m) < e / 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis \<open>0 < e\<close> less_divide_eq_numeral1(1) metric_CauchyD mult_zero_left)
[PROOF STATE]
proof (state)
this:
\<forall>n\<ge>Nv. \<forall>m\<ge>Nv. dist (v n) (v m) < e / 2

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
define M where "M = max Nu Nv"
[PROOF STATE]
proof (state)
this:
M = max Nu Nv

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
M = max Nu Nv

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
fix n m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
assume H: "n \<ge> M" "m \<ge> M"
[PROOF STATE]
proof (state)
this:
M \<le> n
M \<le> m

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
have *: "dist (u n) (u m) < e/2" "dist (v n) (v m) < e/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (u n) (u m) < e / 2 &&& dist (v n) (v m) < e / 2
[PROOF STEP]
using Nu Nv H
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<ge>Nu. \<forall>m\<ge>Nu. dist (u n) (u m) < e / 2
\<forall>n\<ge>Nv. \<forall>m\<ge>Nv. dist (v n) (v m) < e / 2
M \<le> n
M \<le> m

goal (1 subgoal):
 1. dist (u n) (u m) < e / 2 &&& dist (v n) (v m) < e / 2
[PROOF STEP]
unfolding M_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<ge>Nu. \<forall>m\<ge>Nu. dist (u n) (u m) < e / 2
\<forall>n\<ge>Nv. \<forall>m\<ge>Nv. dist (v n) (v m) < e / 2
max Nu Nv \<le> n
max Nu Nv \<le> m

goal (1 subgoal):
 1. dist (u n) (u m) < e / 2 &&& dist (v n) (v m) < e / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (u n) (u m) < e / 2
dist (v n) (v m) < e / 2

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
have "dist (u m) (v m) - dist (u n) (v n) \<le> dist (u m) (u n) + dist (v n) (v m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (u m) (v m) - dist (u n) (v n) \<le> dist (u m) (u n) + dist (v n) (v m)
[PROOF STEP]
by (simp add: algebra_simps) (metis add_le_cancel_left dist_commute dist_triangle2 dist_triangle_le)
[PROOF STATE]
proof (state)
this:
dist (u m) (v m) - dist (u n) (v n) \<le> dist (u m) (u n) + dist (v n) (v m)

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (u m) (v m) - dist (u n) (v n) \<le> dist (u m) (u n) + dist (v n) (v m)

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
have "... < e/2 + e/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (u m) (u n) + dist (v n) (v m) < e / 2 + e / 2
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
dist (u n) (u m) < e / 2
dist (v n) (v m) < e / 2

goal (1 subgoal):
 1. dist (u m) (u n) + dist (v n) (v m) < e / 2 + e / 2
[PROOF STEP]
by (simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
dist (u m) (u n) + dist (v n) (v m) < e / 2 + e / 2

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (u m) (v m) - dist (u n) (v n) < e / 2 + e / 2
[PROOF STEP]
have A: "dist (u m) (v m) - dist (u n) (v n) < e"
[PROOF STATE]
proof (prove)
using this:
dist (u m) (v m) - dist (u n) (v n) < e / 2 + e / 2

goal (1 subgoal):
 1. dist (u m) (v m) - dist (u n) (v n) < e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (u m) (v m) - dist (u n) (v n) < e

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
have "dist (u n) (v n) - dist (u m) (v m) \<le> dist (u m) (u n) + dist (v n) (v m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (u n) (v n) - dist (u m) (v m) \<le> dist (u m) (u n) + dist (v n) (v m)
[PROOF STEP]
by (simp add: algebra_simps) (metis add_le_cancel_left dist_commute dist_triangle2 dist_triangle_le)
[PROOF STATE]
proof (state)
this:
dist (u n) (v n) - dist (u m) (v m) \<le> dist (u m) (u n) + dist (v n) (v m)

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (u n) (v n) - dist (u m) (v m) \<le> dist (u m) (u n) + dist (v n) (v m)

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
have "... < e/2 + e/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (u m) (u n) + dist (v n) (v m) < e / 2 + e / 2
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
dist (u n) (u m) < e / 2
dist (v n) (v m) < e / 2

goal (1 subgoal):
 1. dist (u m) (u n) + dist (v n) (v m) < e / 2 + e / 2
[PROOF STEP]
by (simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
dist (u m) (u n) + dist (v n) (v m) < e / 2 + e / 2

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (u n) (v n) - dist (u m) (v m) < e / 2 + e / 2
[PROOF STEP]
have "dist (u n) (v n) - dist (u m) (v m) < e"
[PROOF STATE]
proof (prove)
using this:
dist (u n) (v n) - dist (u m) (v m) < e / 2 + e / 2

goal (1 subgoal):
 1. dist (u n) (v n) - dist (u m) (v m) < e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (u n) (v n) - dist (u m) (v m) < e

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist (u n) (v n) - dist (u m) (v m) < e
[PROOF STEP]
have "norm(dist (u m) (v m) - dist (u n) (v n)) < e"
[PROOF STATE]
proof (prove)
using this:
dist (u n) (v n) - dist (u m) (v m) < e

goal (1 subgoal):
 1. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
dist (u n) (v n) - dist (u m) (v m) < e
dist (u m) (v m) - dist (u n) (v n) < e

goal (1 subgoal):
 1. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
norm (dist (u m) (v m) - dist (u n) (v n)) < e

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>M \<le> ?n2; M \<le> ?m2\<rbrakk> \<Longrightarrow> norm (dist (u ?m2) (v ?m2) - dist (u ?n2) (v ?n2)) < e

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>M \<le> ?n2; M \<le> ?m2\<rbrakk> \<Longrightarrow> norm (dist (u ?m2) (v ?m2) - dist (u ?n2) (v ?n2)) < e
[PROOF STEP]
show "\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (dist (u m) (v m) - dist (u n) (v n)) < e"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>M \<le> ?n2; M \<le> ?m2\<rbrakk> \<Longrightarrow> norm (dist (u ?m2) (v ?m2) - dist (u ?n2) (v ?n2)) < e

goal (1 subgoal):
 1. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (dist (u m) (v m) - dist (u n) (v n)) < e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma convergent_add_null:
  fixes u v::"nat \<Rightarrow> ('a::real_normed_vector)"
  assumes "convergent u"
          "(\<lambda>n. v n - u n) \<longlonglongrightarrow> 0"
  shows "convergent v" "lim v = lim u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convergent v &&& lim v = lim u
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. convergent v
 2. lim v = lim u
[PROOF STEP]
have "(\<lambda>n. u n + (v n - u n)) \<longlonglongrightarrow> lim u + 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. u n + (v n - u n)) \<longlonglongrightarrow> lim u + (0::'a)
[PROOF STEP]
apply (rule tendsto_add)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. u \<longlonglongrightarrow> lim u
 2. (\<lambda>x. v x - u x) \<longlonglongrightarrow> (0::'a)
[PROOF STEP]
using assms convergent_LIMSEQ_iff
[PROOF STATE]
proof (prove)
using this:
convergent u
(\<lambda>n. v n - u n) \<longlonglongrightarrow> (0::'a)
convergent ?X = ?X \<longlonglongrightarrow> lim ?X

goal (2 subgoals):
 1. u \<longlonglongrightarrow> lim u
 2. (\<lambda>x. v x - u x) \<longlonglongrightarrow> (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. u n + (v n - u n)) \<longlonglongrightarrow> lim u + (0::'a)

goal (2 subgoals):
 1. convergent v
 2. lim v = lim u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. u n + (v n - u n)) \<longlonglongrightarrow> lim u + (0::'a)
[PROOF STEP]
have *: "v \<longlonglongrightarrow> lim u"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. u n + (v n - u n)) \<longlonglongrightarrow> lim u + (0::'a)

goal (1 subgoal):
 1. v \<longlonglongrightarrow> lim u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<longlonglongrightarrow> lim u

goal (2 subgoals):
 1. convergent v
 2. lim v = lim u
[PROOF STEP]
show "convergent v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convergent v
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
v \<longlonglongrightarrow> lim u

goal (1 subgoal):
 1. convergent v
[PROOF STEP]
by (simp add: Lim_def convergentI)
[PROOF STATE]
proof (state)
this:
convergent v

goal (1 subgoal):
 1. lim v = lim u
[PROOF STEP]
show "lim v = lim u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lim v = lim u
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
v \<longlonglongrightarrow> lim u

goal (1 subgoal):
 1. lim v = lim u
[PROOF STEP]
by (simp add: limI)
[PROOF STATE]
proof (state)
this:
lim v = lim u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dist_metric_completion_limit:
  fixes x y::"'a metric_completion"
  shows "(\<lambda>n. dist (rep_metric_completion x n) (rep_metric_completion y n)) \<longlonglongrightarrow> dist x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. dist (rep_metric_completion x n) (rep_metric_completion y n)) \<longlonglongrightarrow> dist x y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. dist (rep_metric_completion x n) (rep_metric_completion y n)) \<longlonglongrightarrow> dist x y
[PROOF STEP]
have C: "Cauchy (rep_metric_completion x)" "Cauchy (rep_metric_completion y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cauchy (rep_metric_completion x) &&& Cauchy (rep_metric_completion y)
[PROOF STEP]
using Quotient3_metric_completion Quotient3_rep_reflp
[PROOF STATE]
proof (prove)
using this:
Quotient3 (\<lambda>u v. Cauchy u \<and> Cauchy v \<and> (\<lambda>n. dist (u n) (v n)) \<longlonglongrightarrow> 0) abs_metric_completion rep_metric_completion
Quotient3 ?R ?Abs ?Rep \<Longrightarrow> ?R (?Rep ?a) (?Rep ?a)

goal (1 subgoal):
 1. Cauchy (rep_metric_completion x) &&& Cauchy (rep_metric_completion y)
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
Cauchy (rep_metric_completion x)
Cauchy (rep_metric_completion y)

goal (1 subgoal):
 1. (\<lambda>n. dist (rep_metric_completion x n) (rep_metric_completion y n)) \<longlonglongrightarrow> dist x y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. dist (rep_metric_completion x n) (rep_metric_completion y n)) \<longlonglongrightarrow> dist x y
[PROOF STEP]
unfolding dist_metric_completion_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. dist (rep_metric_completion x n) (rep_metric_completion y n)) \<longlonglongrightarrow> map_fun rep_metric_completion (map_fun rep_metric_completion id) (\<lambda>x y. lim (\<lambda>n. dist (x n) (y n))) x y
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
Cauchy (rep_metric_completion x)
Cauchy (rep_metric_completion y)

goal (1 subgoal):
 1. (\<lambda>n. dist (rep_metric_completion x n) (rep_metric_completion y n)) \<longlonglongrightarrow> map_fun rep_metric_completion (map_fun rep_metric_completion id) (\<lambda>x y. lim (\<lambda>n. dist (x n) (y n))) x y
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Cauchy (rep_metric_completion x); Cauchy (rep_metric_completion y)\<rbrakk> \<Longrightarrow> (\<lambda>n. dist (rep_metric_completion x n) (rep_metric_completion y n)) \<longlonglongrightarrow> lim (\<lambda>n. dist (rep_metric_completion x n) (rep_metric_completion y n))
[PROOF STEP]
using convergent_Cauchy_dist[OF C] convergent_LIMSEQ_iff
[PROOF STATE]
proof (prove)
using this:
convergent (\<lambda>n. dist (rep_metric_completion x n) (rep_metric_completion y n))
convergent ?X = ?X \<longlonglongrightarrow> lim ?X

goal (1 subgoal):
 1. \<lbrakk>Cauchy (rep_metric_completion x); Cauchy (rep_metric_completion y)\<rbrakk> \<Longrightarrow> (\<lambda>n. dist (rep_metric_completion x n) (rep_metric_completion y n)) \<longlonglongrightarrow> lim (\<lambda>n. dist (rep_metric_completion x n) (rep_metric_completion y n))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<lambda>n. dist (rep_metric_completion x n) (rep_metric_completion y n)) \<longlonglongrightarrow> dist x y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dist_metric_completion_limit':
  fixes x y::"nat \<Rightarrow> 'a"
  assumes "Cauchy x" "Cauchy y"
  shows "(\<lambda>n. dist (x n) (y n)) \<longlonglongrightarrow> dist (abs_metric_completion x) (abs_metric_completion y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. dist (x n) (y n)) \<longlonglongrightarrow> dist (abs_metric_completion x) (abs_metric_completion y)
[PROOF STEP]
apply (subst dist_metric_completion.abs_eq)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. Cauchy x \<and> Cauchy x \<and> (\<lambda>n. dist (x n) (x n)) \<longlonglongrightarrow> 0
 2. Cauchy y \<and> Cauchy y \<and> (\<lambda>n. dist (y n) (y n)) \<longlonglongrightarrow> 0
 3. (\<lambda>n. dist (x n) (y n)) \<longlonglongrightarrow> lim (\<lambda>n. dist (x n) (y n))
[PROOF STEP]
using assms convergent_Cauchy_dist[OF assms]
[PROOF STATE]
proof (prove)
using this:
Cauchy x
Cauchy y
convergent (\<lambda>n. dist (x n) (y n))

goal (3 subgoals):
 1. Cauchy x \<and> Cauchy x \<and> (\<lambda>n. dist (x n) (x n)) \<longlonglongrightarrow> 0
 2. Cauchy y \<and> Cauchy y \<and> (\<lambda>n. dist (y n) (y n)) \<longlonglongrightarrow> 0
 3. (\<lambda>n. dist (x n) (y n)) \<longlonglongrightarrow> lim (\<lambda>n. dist (x n) (y n))
[PROOF STEP]
by (auto simp add: convergent_LIMSEQ_iff)


[STATEMENT]
lemma to_metric_completion_isometry:
  "isometry_on UNIV to_metric_completion"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on UNIV to_metric_completion
[PROOF STEP]
proof (rule isometry_onI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV\<rbrakk> \<Longrightarrow> dist (to_metric_completion x) (to_metric_completion y) = dist x y
[PROOF STEP]
fix x y::'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV\<rbrakk> \<Longrightarrow> dist (to_metric_completion x) (to_metric_completion y) = dist x y
[PROOF STEP]
have "(\<lambda>n. dist (x) (y)) \<longlonglongrightarrow> dist (to_metric_completion x) (to_metric_completion y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. dist x y) \<longlonglongrightarrow> dist (to_metric_completion x) (to_metric_completion y)
[PROOF STEP]
unfolding to_metric_completion_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. dist x y) \<longlonglongrightarrow> dist (abs_metric_completion (\<lambda>n. x)) (abs_metric_completion (\<lambda>n. y))
[PROOF STEP]
apply (rule dist_metric_completion_limit')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Cauchy (\<lambda>n. x)
 2. Cauchy (\<lambda>n. y)
[PROOF STEP]
unfolding Cauchy_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist x x < e
 2. \<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist y y < e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. dist x y) \<longlonglongrightarrow> dist (to_metric_completion x) (to_metric_completion y)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV\<rbrakk> \<Longrightarrow> dist (to_metric_completion x) (to_metric_completion y) = dist x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. dist x y) \<longlonglongrightarrow> dist (to_metric_completion x) (to_metric_completion y)
[PROOF STEP]
show "dist (to_metric_completion x) (to_metric_completion y) = dist x y"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. dist x y) \<longlonglongrightarrow> dist (to_metric_completion x) (to_metric_completion y)

goal (1 subgoal):
 1. dist (to_metric_completion x) (to_metric_completion y) = dist x y
[PROOF STEP]
by (simp add: LIMSEQ_const_iff)
[PROOF STATE]
proof (state)
this:
dist (to_metric_completion x) (to_metric_completion y) = dist x y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma to_metric_completion_dense:
  assumes "open U" "U \<noteq> {}"
  shows "\<exists>x. to_metric_completion x \<in> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. to_metric_completion x \<in> U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. to_metric_completion x \<in> U
[PROOF STEP]
obtain y where "y \<in> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. y \<in> U \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>U \<noteq> {}\<close>
[PROOF STATE]
proof (prove)
using this:
U \<noteq> {}

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

goal (1 subgoal):
 1. \<exists>x. to_metric_completion x \<in> U
[PROOF STEP]
obtain e::real where e: "e > 0" "\<And>z. dist z y < e \<Longrightarrow> z \<in> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e. \<lbrakk>0 < e; \<And>z. dist z y < e \<Longrightarrow> z \<in> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>y \<in> U\<close> \<open>open U\<close>
[PROOF STATE]
proof (prove)
using this:
y \<in> U
open U

goal (1 subgoal):
 1. (\<And>e. \<lbrakk>0 < e; \<And>z. dist z y < e \<Longrightarrow> z \<in> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis open_dist)
[PROOF STATE]
proof (state)
this:
0 < e
dist ?z y < e \<Longrightarrow> ?z \<in> U

goal (1 subgoal):
 1. \<exists>x. to_metric_completion x \<in> U
[PROOF STEP]
have *: "Cauchy (rep_metric_completion y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cauchy (rep_metric_completion y)
[PROOF STEP]
using Quotient3_metric_completion Quotient3_rep_reflp
[PROOF STATE]
proof (prove)
using this:
Quotient3 (\<lambda>u v. Cauchy u \<and> Cauchy v \<and> (\<lambda>n. dist (u n) (v n)) \<longlonglongrightarrow> 0) abs_metric_completion rep_metric_completion
Quotient3 ?R ?Abs ?Rep \<Longrightarrow> ?R (?Rep ?a) (?Rep ?a)

goal (1 subgoal):
 1. Cauchy (rep_metric_completion y)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Cauchy (rep_metric_completion y)

goal (1 subgoal):
 1. \<exists>x. to_metric_completion x \<in> U
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cauchy (rep_metric_completion y)
[PROOF STEP]
obtain N where N: "\<forall>n \<ge> N. \<forall>m \<ge> N. dist (rep_metric_completion y n) (rep_metric_completion y m) < e/2"
[PROOF STATE]
proof (prove)
using this:
Cauchy (rep_metric_completion y)

goal (1 subgoal):
 1. (\<And>N. \<forall>n\<ge>N. \<forall>m\<ge>N. dist (rep_metric_completion y n) (rep_metric_completion y m) < e / 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>e > 0\<close>
[PROOF STATE]
proof (prove)
using this:
Cauchy (rep_metric_completion y)
0 < e

goal (1 subgoal):
 1. (\<And>N. \<forall>n\<ge>N. \<forall>m\<ge>N. dist (rep_metric_completion y n) (rep_metric_completion y m) < e / 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Cauchy_def
[PROOF STATE]
proof (prove)
using this:
\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (rep_metric_completion y m) (rep_metric_completion y n) < e
0 < e

goal (1 subgoal):
 1. (\<And>N. \<forall>n\<ge>N. \<forall>m\<ge>N. dist (rep_metric_completion y n) (rep_metric_completion y m) < e / 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson divide_pos_pos zero_less_numeral)
[PROOF STATE]
proof (state)
this:
\<forall>n\<ge>N. \<forall>m\<ge>N. dist (rep_metric_completion y n) (rep_metric_completion y m) < e / 2

goal (1 subgoal):
 1. \<exists>x. to_metric_completion x \<in> U
[PROOF STEP]
define x where "x = rep_metric_completion y N"
[PROOF STATE]
proof (state)
this:
x = rep_metric_completion y N

goal (1 subgoal):
 1. \<exists>x. to_metric_completion x \<in> U
[PROOF STEP]
have "(\<lambda>n. dist x (rep_metric_completion y n)) \<longlonglongrightarrow> dist (to_metric_completion x) (abs_metric_completion (rep_metric_completion y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. dist x (rep_metric_completion y n)) \<longlonglongrightarrow> dist (to_metric_completion x) (abs_metric_completion (rep_metric_completion y))
[PROOF STEP]
unfolding to_metric_completion_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. dist x (rep_metric_completion y n)) \<longlonglongrightarrow> dist (abs_metric_completion (\<lambda>n. x)) (abs_metric_completion (rep_metric_completion y))
[PROOF STEP]
apply (rule dist_metric_completion_limit')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Cauchy (\<lambda>n. x)
 2. Cauchy (rep_metric_completion y)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
Cauchy (rep_metric_completion y)

goal (2 subgoals):
 1. Cauchy (\<lambda>n. x)
 2. Cauchy (rep_metric_completion y)
[PROOF STEP]
unfolding Cauchy_def
[PROOF STATE]
proof (prove)
using this:
\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (rep_metric_completion y m) (rep_metric_completion y n) < e

goal (2 subgoals):
 1. \<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist x x < e
 2. \<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (rep_metric_completion y m) (rep_metric_completion y n) < e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. dist x (rep_metric_completion y n)) \<longlonglongrightarrow> dist (to_metric_completion x) (abs_metric_completion (rep_metric_completion y))

goal (1 subgoal):
 1. \<exists>x. to_metric_completion x \<in> U
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. dist x (rep_metric_completion y n)) \<longlonglongrightarrow> dist (to_metric_completion x) (abs_metric_completion (rep_metric_completion y))
[PROOF STEP]
have "(\<lambda>n. dist x (rep_metric_completion y n)) \<longlonglongrightarrow> dist (to_metric_completion x) y"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. dist x (rep_metric_completion y n)) \<longlonglongrightarrow> dist (to_metric_completion x) (abs_metric_completion (rep_metric_completion y))

goal (1 subgoal):
 1. (\<lambda>n. dist x (rep_metric_completion y n)) \<longlonglongrightarrow> dist (to_metric_completion x) y
[PROOF STEP]
unfolding Quotient3_abs_rep[OF Quotient3_metric_completion]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. dist x (rep_metric_completion y n)) \<longlonglongrightarrow> dist (to_metric_completion x) y

goal (1 subgoal):
 1. (\<lambda>n. dist x (rep_metric_completion y n)) \<longlonglongrightarrow> dist (to_metric_completion x) y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>n. dist x (rep_metric_completion y n)) \<longlonglongrightarrow> dist (to_metric_completion x) y

goal (1 subgoal):
 1. \<exists>x. to_metric_completion x \<in> U
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>n. dist x (rep_metric_completion y n)) \<longlonglongrightarrow> dist (to_metric_completion x) y

goal (1 subgoal):
 1. \<exists>x. to_metric_completion x \<in> U
[PROOF STEP]
have "eventually (\<lambda>n. dist x (rep_metric_completion y n) \<le> e/2) sequentially"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. dist x (rep_metric_completion y n) \<le> e / 2
[PROOF STEP]
unfolding eventually_sequentially x_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Na. \<forall>n\<ge>Na. dist (rep_metric_completion y N) (rep_metric_completion y n) \<le> e / 2
[PROOF STEP]
apply (rule exI[of _ N])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n\<ge>N. dist (rep_metric_completion y N) (rep_metric_completion y n) \<le> e / 2
[PROOF STEP]
using N less_imp_le
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<ge>N. \<forall>m\<ge>N. dist (rep_metric_completion y n) (rep_metric_completion y m) < e / 2
?x < ?y \<Longrightarrow> ?x \<le> ?y

goal (1 subgoal):
 1. \<forall>n\<ge>N. dist (rep_metric_completion y N) (rep_metric_completion y n) \<le> e / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. dist x (rep_metric_completion y n) \<le> e / 2

goal (1 subgoal):
 1. \<exists>x. to_metric_completion x \<in> U
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. dist x (rep_metric_completion y n)) \<longlonglongrightarrow> dist (to_metric_completion x) y
\<forall>\<^sub>F n in sequentially. dist x (rep_metric_completion y n) \<le> e / 2
[PROOF STEP]
have "dist (to_metric_completion x) y \<le> e/2"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. dist x (rep_metric_completion y n)) \<longlonglongrightarrow> dist (to_metric_completion x) y
\<forall>\<^sub>F n in sequentially. dist x (rep_metric_completion y n) \<le> e / 2

goal (1 subgoal):
 1. dist (to_metric_completion x) y \<le> e / 2
[PROOF STEP]
using LIMSEQ_le_const2
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. dist x (rep_metric_completion y n)) \<longlonglongrightarrow> dist (to_metric_completion x) y
\<forall>\<^sub>F n in sequentially. dist x (rep_metric_completion y n) \<le> e / 2
\<lbrakk>?X \<longlonglongrightarrow> ?x; \<exists>N. \<forall>n\<ge>N. ?X n \<le> ?a\<rbrakk> \<Longrightarrow> ?x \<le> ?a

goal (1 subgoal):
 1. dist (to_metric_completion x) y \<le> e / 2
[PROOF STEP]
unfolding eventually_sequentially
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. dist x (rep_metric_completion y n)) \<longlonglongrightarrow> dist (to_metric_completion x) y
\<exists>N. \<forall>n\<ge>N. dist x (rep_metric_completion y n) \<le> e / 2
\<lbrakk>?X \<longlonglongrightarrow> ?x; \<exists>N. \<forall>n\<ge>N. ?X n \<le> ?a\<rbrakk> \<Longrightarrow> ?x \<le> ?a

goal (1 subgoal):
 1. dist (to_metric_completion x) y \<le> e / 2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
dist (to_metric_completion x) y \<le> e / 2

goal (1 subgoal):
 1. \<exists>x. to_metric_completion x \<in> U
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist (to_metric_completion x) y \<le> e / 2
[PROOF STEP]
have "to_metric_completion x \<in> U"
[PROOF STATE]
proof (prove)
using this:
dist (to_metric_completion x) y \<le> e / 2

goal (1 subgoal):
 1. to_metric_completion x \<in> U
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
dist (to_metric_completion x) y \<le> e / 2
0 < e
dist ?z y < e \<Longrightarrow> ?z \<in> U

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

goal (1 subgoal):
 1. \<exists>x. to_metric_completion x \<in> U
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
to_metric_completion x \<in> U
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
to_metric_completion x \<in> U

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma to_metric_completion_dense':
  "closure (range to_metric_completion) = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (range to_metric_completion) = UNIV
[PROOF STEP]
apply (auto simp add: closure_iff_nhds_not_empty)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x A S. \<lbrakk>S \<subseteq> A; open S; x \<in> S; range to_metric_completion \<inter> A = {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using to_metric_completion_dense
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>open ?U; ?U \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>x. to_metric_completion x \<in> ?U

goal (1 subgoal):
 1. \<And>x A S. \<lbrakk>S \<subseteq> A; open S; x \<in> S; range to_metric_completion \<inter> A = {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by fastforce


[STATEMENT]
lemma lift_to_metric_completion:
  fixes f::"('a::metric_space) \<Rightarrow> ('b::complete_space)"
  assumes "uniformly_continuous_on UNIV f"
  shows "\<exists>g. (uniformly_continuous_on UNIV g)
            \<and> (f = g o to_metric_completion)
            \<and> (\<forall>x \<in> range to_metric_completion. g x = f (inv to_metric_completion x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g. isUCont g \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>g. isUCont g \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
define I::"'a metric_completion \<Rightarrow> 'a" where "I = inv to_metric_completion"
[PROOF STATE]
proof (state)
this:
I = inv to_metric_completion

goal (1 subgoal):
 1. \<exists>g. isUCont g \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
have "uniformly_continuous_on (range to_metric_completion) I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uniformly_continuous_on (range to_metric_completion) I
[PROOF STEP]
using isometry_on_uniformly_continuous[OF isometry_on_inverse(1)[OF to_metric_completion_isometry]] I_def
[PROOF STATE]
proof (prove)
using this:
uniformly_continuous_on (range to_metric_completion) (inv to_metric_completion)
I = inv to_metric_completion

goal (1 subgoal):
 1. uniformly_continuous_on (range to_metric_completion) I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
uniformly_continuous_on (range to_metric_completion) I

goal (1 subgoal):
 1. \<exists>g. isUCont g \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uniformly_continuous_on (range to_metric_completion) I
[PROOF STEP]
have UC: "uniformly_continuous_on (range to_metric_completion) (\<lambda>x. f (I x))"
[PROOF STATE]
proof (prove)
using this:
uniformly_continuous_on (range to_metric_completion) I

goal (1 subgoal):
 1. uniformly_continuous_on (range to_metric_completion) (\<lambda>x. f (I x))
[PROOF STEP]
using assms uniformly_continuous_on_compose
[PROOF STATE]
proof (prove)
using this:
uniformly_continuous_on (range to_metric_completion) I
isUCont f
\<lbrakk>uniformly_continuous_on ?s ?g; uniformly_continuous_on (?g ` ?s) ?f\<rbrakk> \<Longrightarrow> uniformly_continuous_on ?s (\<lambda>x. ?f (?g x))

goal (1 subgoal):
 1. uniformly_continuous_on (range to_metric_completion) (\<lambda>x. f (I x))
[PROOF STEP]
by (metis I_def bij_betw_imp_surj_on bij_betw_inv_into isometry_on_inverse(4) to_metric_completion_isometry)
[PROOF STATE]
proof (state)
this:
uniformly_continuous_on (range to_metric_completion) (\<lambda>x. f (I x))

goal (1 subgoal):
 1. \<exists>g. isUCont g \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
obtain g where g: "uniformly_continuous_on (closure(range to_metric_completion)) g"
                    "\<And>x. x \<in> range to_metric_completion \<Longrightarrow> f (I x) = g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>uniformly_continuous_on (closure (range to_metric_completion)) g; \<And>x. x \<in> range to_metric_completion \<Longrightarrow> f (I x) = g x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using uniformly_continuous_on_extension_on_closure[OF UC]
[PROOF STATE]
proof (prove)
using this:
(\<And>g. \<lbrakk>uniformly_continuous_on (closure (range to_metric_completion)) g; \<And>x. x \<in> range to_metric_completion \<Longrightarrow> f (I x) = g x; \<And>Y h x. \<lbrakk>range to_metric_completion \<subseteq> Y; Y \<subseteq> closure (range to_metric_completion); continuous_on Y h; \<And>x. x \<in> range to_metric_completion \<Longrightarrow> f (I x) = h x; x \<in> Y\<rbrakk> \<Longrightarrow> h x = g x\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>uniformly_continuous_on (closure (range to_metric_completion)) g; \<And>x. x \<in> range to_metric_completion \<Longrightarrow> f (I x) = g x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
uniformly_continuous_on (closure (range to_metric_completion)) g
?x \<in> range to_metric_completion \<Longrightarrow> f (I ?x) = g ?x

goal (1 subgoal):
 1. \<exists>g. isUCont g \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
have "uniformly_continuous_on UNIV g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isUCont g
[PROOF STEP]
using to_metric_completion_dense' g(1)
[PROOF STATE]
proof (prove)
using this:
closure (range to_metric_completion) = UNIV
uniformly_continuous_on (closure (range to_metric_completion)) g

goal (1 subgoal):
 1. isUCont g
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
isUCont g

goal (1 subgoal):
 1. \<exists>g. isUCont g \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
isUCont g

goal (1 subgoal):
 1. \<exists>g. isUCont g \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
have "f x = g (to_metric_completion x)" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x = g (to_metric_completion x)
[PROOF STEP]
using g(2)
[PROOF STATE]
proof (prove)
using this:
?x \<in> range to_metric_completion \<Longrightarrow> f (I ?x) = g ?x

goal (1 subgoal):
 1. f x = g (to_metric_completion x)
[PROOF STEP]
by (metis I_def UNIV_I isometry_on_inverse(2) range_eqI to_metric_completion_isometry)
[PROOF STATE]
proof (state)
this:
f ?x = g (to_metric_completion ?x)

goal (1 subgoal):
 1. \<exists>g. isUCont g \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f ?x = g (to_metric_completion ?x)

goal (1 subgoal):
 1. \<exists>g. isUCont g \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
have "g x = f (inv to_metric_completion x)" if "x \<in> range to_metric_completion" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g x = f (inv to_metric_completion x)
[PROOF STEP]
using I_def g(2) that
[PROOF STATE]
proof (prove)
using this:
I = inv to_metric_completion
?x \<in> range to_metric_completion \<Longrightarrow> f (I ?x) = g ?x
x \<in> range to_metric_completion

goal (1 subgoal):
 1. g x = f (inv to_metric_completion x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> range to_metric_completion \<Longrightarrow> g ?x = f (inv to_metric_completion ?x)

goal (1 subgoal):
 1. \<exists>g. isUCont g \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
isUCont g
f ?x = g (to_metric_completion ?x)
?x \<in> range to_metric_completion \<Longrightarrow> g ?x = f (inv to_metric_completion ?x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
isUCont g
f ?x = g (to_metric_completion ?x)
?x \<in> range to_metric_completion \<Longrightarrow> g ?x = f (inv to_metric_completion ?x)

goal (1 subgoal):
 1. \<exists>g. isUCont g \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
unfolding comp_def
[PROOF STATE]
proof (prove)
using this:
isUCont g
f ?x = g (to_metric_completion ?x)
?x \<in> range to_metric_completion \<Longrightarrow> g ?x = f (inv to_metric_completion ?x)

goal (1 subgoal):
 1. \<exists>g. isUCont g \<and> f = (\<lambda>x. g (to_metric_completion x)) \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>g. isUCont g \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))

goal:
No subgoals!
[PROOF STEP]
qed