# Theory Valuation3

```(**        Valuation3
author Hidetsune Kobayashi
Group You Santo
Department of Mathematics
Nihon University
h_coba@math.cst.nihon-u.ac.jp
June 24, 2005
July 20, 2007

chapter 1. elementary properties of a valuation
section 9. completion
subsection Hensel's theorem
**)

theory Valuation3
imports Valuation2
begin

section "Completion"

text‹In this section we formalize "completion" of the ground field K›

definition
limit :: "[_, 'b ⇒ ant, nat ⇒ 'b, 'b]
⇒ bool" ("(4lim⇘ _ _ ⇙_ _)" [90,90,90,91]90) where
"lim⇘K v⇙ f b ⟷ (∀N. ∃M. (∀n. M < n ⟶
((f n) ±⇘K⇙ (-⇩a⇘K⇙ b)) ∈ (vp K v)⇗ (Vr K v) (an N)⇖))"

(* In this definition, f represents a sequence of elements of K, which is
converging to b. Key lemmas of this section are n_value_x_1 and
n_value_x_2 *)

lemma not_in_singleton_noneq:"x ∉ {a} ⟹ x ≠ a"
apply simp
done   (* later move this lemma to Algebra1 *)

lemma noneq_not_in_singleton:"x ≠ a ⟹ x ∉ {a}"
apply simp
done

lemma inf_neq_1[simp]:"∞ ≠ 1"
by (simp only:ant_1[THEN sym], rule z_neq_inf[THEN not_sym, of 1])

lemma a1_neq_0[simp]:"(1::ant) ≠ 0"
by (simp only:an_1[THEN sym], simp only:an_0[THEN sym],
subst aneq_natneq[of 1 0], simp)

lemma a1_poss[simp]:"(0::ant) < 1"
by (cut_tac zposs_aposss[of 1], simp)

lemma a_p1_gt[simp]:"⟦a ≠ ∞; a ≠ -∞⟧  ⟹ a < a + 1"
apply simp
done

lemma (in Corps) vpr_pow_inter_zero:"valuation K v ⟹
(⋂ {I. ∃n. I = (vp K v)⇗(Vr K v) (an n)⇖}) = {𝟬}"
apply (frule Vr_ring[of v], frule vp_ideal[of v])
apply (rule equalityI)
defer
apply (rule subsetI)
apply simp
apply (rule allI, rule impI, erule exE, simp)
apply (cut_tac n = "an n" in vp_apow_ideal[of v], assumption+)
apply simp
apply (cut_tac I = "(vp K v)⇗ (Vr K v) (an n)⇖" in  Ring.ideal_zero[of "Vr K v"],
assumption+)

apply (rule subsetI, simp)
apply (rule contrapos_pp, simp+)
apply (subgoal_tac "x ∈ vp K v")
prefer 2
apply (drule_tac x = "vp K v⇗ (Vr K v) (an 1)⇖" in spec)
apply (subgoal_tac "∃n. vp K v⇗ (Vr K v) (an (Suc 0))⇖ = vp K v⇗ (Vr K v) (an n)⇖",
simp,
thin_tac " ∃n. vp K v⇗ (Vr K v) (an (Suc 0))⇖ = vp K v⇗ (Vr K v) (an n)⇖")
apply (simp only:na_1)
apply (simp only:Ring.idealpow_1_self[of "Vr K v" "vp K v"])

apply blast

apply (frule n_val_valuation[of v])

apply (frule_tac x = x in val_nonzero_z[of "n_val K v"],
frule_tac h = x in Ring.ideal_subset[of "Vr K v" "vp K v"],
assumption+,
frule_tac h = x in Ring.ideal_subset[of "Vr K v" "vp K v"],
apply (cut_tac x = x in val_pos_mem_Vr[of v], assumption) apply(
apply (frule_tac x = x in val_pos_n_val_pos[of v],
apply (cut_tac x = "n_val K v x" and y = 1 in aadd_pos_poss, assumption+,
simp) apply (frule_tac y = "n_val K v x + 1" in aless_imp_le[of 0])
apply (cut_tac x1 = x and n1 = "(n_val K v x) + 1" in n_val_n_pow[THEN sym,
of v], assumption+)
apply (drule_tac a = "vp K v⇗ (Vr K v) (n_val K v x + 1)⇖" in forall_spec)
apply (erule exE, simp)
apply (simp only:ant_1[THEN sym] a_zpz,
cut_tac z = "z + 1" in z_neq_inf)
apply (subst an_na[THEN sym], assumption+, blast)
apply simp
apply (cut_tac a = "n_val K v x" in a_p1_gt)
apply (erule exE, simp only:ant_1[THEN sym], simp only:a_zpz z_neq_inf)
apply (cut_tac i = "z + 1" and j = z in ale_zle, simp)
apply (cut_tac y1 = "n_val K v x" and x1 = "n_val K v x + 1" in
aneg_le[THEN sym], simp)
done

lemma (in Corps) limit_diff_n_val:"⟦b ∈ carrier K; ∀j. f j ∈ carrier K;
valuation K v⟧ ⟹  (lim⇘K v⇙ f b) = (∀N. ∃M. ∀n. M < n ⟶
(an N) ≤ (n_val K v ((f n) ± (-⇩a b))))"
apply (rule iffI)
apply (rule allI)
apply (simp add:limit_def) apply (rotate_tac -1)
apply (drule_tac x = N in spec)
apply (erule exE)
apply (subgoal_tac "∀n>M. (an N) ≤ (n_val K v (f n ± (-⇩a b)))")
apply blast
apply (rule allI, rule impI) apply (rotate_tac -2)
apply (drule_tac x = n in spec, simp)
apply (rule n_value_x_1[of v], assumption+,

apply (rule allI, rotate_tac -1, drule_tac x = N in spec)

apply (erule exE)
apply (subgoal_tac "∀n>M. f n ± (-⇩a b) ∈ vp K v ⇗(Vr K v) (an N)⇖")
apply blast
apply (rule allI, rule impI)
apply (rotate_tac -2, drule_tac x = n in spec, simp)
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
apply (rule_tac x = "f n ± -⇩a b" and n = "an N" in n_value_x_2[of "v"],
assumption+)
apply (subst val_pos_mem_Vr[THEN sym, of "v"], assumption+)
apply (drule_tac x = n in spec)
apply (rule aGroup.ag_pOp_closed[of "K"], assumption+)
apply (subst val_pos_n_val_pos[of  "v"], assumption+)
apply (rule aGroup.ag_pOp_closed, assumption+) apply simp
apply (rule_tac j = "an N" and k = "n_val K v ( f n ± -⇩a b)" in
ale_trans[of "0"], simp, assumption+)
apply simp
done

lemma (in Corps) an_na_Lv:"valuation K v ⟹ an (na (Lv K v)) = Lv K v"
apply (frule Lv_pos[of "v"])
apply (frule aless_imp_le[of "0" "Lv K v"])
apply (frule apos_neq_minf[of "Lv K v"])
apply (frule Lv_z[of "v"], erule exE)
apply (rule an_na)
apply (rule contrapos_pp, simp+)
done

lemma (in Corps) limit_diff_val:"⟦b ∈ carrier K; ∀j. f j ∈ carrier K;
valuation K v⟧ ⟹  (lim⇘K v⇙ f b) = (∀N. ∃M. ∀n. M < n ⟶
(an N) ≤ (v ((f n) ± (-⇩a b))))"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
apply (rule iffI)
apply (rule allI,
rotate_tac -1, drule_tac x = N in spec, erule exE)
apply (subgoal_tac "∀n > M. an N ≤ v( f n ± -⇩a b)", blast)
apply (rule allI, rule impI)
apply (drule_tac x = n in spec,
drule_tac x = n in spec, simp)
apply (frule aGroup.ag_mOp_closed[of "K" "b"], assumption+,
frule_tac x = "f n" and y = "-⇩a b" in aGroup.ag_pOp_closed, assumption+)
apply (frule_tac x = "f n ± -⇩a b" in n_val_le_val[of "v"],
assumption+)
apply (cut_tac n = N in an_nat_pos)
apply (frule_tac j = "an N" and k = "n_val K v ( f n ± -⇩a b)" in
ale_trans[of "0"], assumption+)
apply (subst val_pos_n_val_pos, assumption+)
apply (rule_tac i = "an N" and j = "n_val K v ( f n ± -⇩a b)" and
k = "v ( f n ± -⇩a b)" in ale_trans, assumption+)
apply (rule allI)
apply (rotate_tac 3, drule_tac x = "N * (na (Lv K v))" in spec)
apply (erule exE)
apply (subgoal_tac "∀n. M < n ⟶ (an N) ≤ n_val K v (f n ± -⇩a b)", blast)
apply (rule allI, rule impI)
apply (rotate_tac -2, drule_tac x = n in spec, simp)

apply (drule_tac x = n in spec)
apply (frule aGroup.ag_mOp_closed[of "K" "b"], assumption+,
frule_tac x = "f n" and y = "-⇩a b" in aGroup.ag_pOp_closed, assumption+)
apply (cut_tac n = "N * na (Lv K v)" in an_nat_pos)
apply (frule_tac i = 0 and j = "an (N * na (Lv K v))" and
k = "v ( f n ± -⇩a b)" in ale_trans, assumption+)
apply (frule Lv_pos[of "v"])
apply (frule_tac x1 = "f n ± -⇩a b" in n_val[THEN sym, of v],
assumption+, simp)
apply (frule Lv_z[of v], erule exE, simp)
done

text‹uniqueness of the limit is derived from ‹vp_pow_inter_zero››
lemma (in Corps) limit_unique:"⟦b ∈ carrier K; ∀j. f j ∈ carrier K;
valuation K v;  c ∈ carrier K; lim⇘K v⇙ f b; lim⇘K v⇙ f c⟧ ⟹  b = c"
apply (rule contrapos_pp, simp+, simp add:limit_def,
cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
frule vpr_pow_inter_zero[THEN sym, of v],
frule noneq_not_in_singleton[of "b ± -⇩a c" "𝟬"])
apply simp
apply (rotate_tac -1, erule exE, erule conjE)
apply (erule exE, simp, thin_tac "x = (vp K v)⇗(Vr K v) (an n)⇖")
apply (rotate_tac 3, drule_tac x = n in spec,
erule exE,
drule_tac x = n in spec,
erule exE)
apply (rename_tac x N M1 M2)
apply (subgoal_tac "M1 < Suc (max M1 M2)",
subgoal_tac "M2 < Suc (max M1 M2)",
drule_tac x = "Suc (max M1 M2)" in spec,
drule_tac x = "Suc (max M1 M2)" in spec,
drule_tac x = "Suc (max M1 M2)" in spec)
apply simp

(* We see (f (Suc (max xb xc)) +⇩K -⇩K b) +⇩K (-⇩K (f (Suc (max xb xc)) +⇩K -⇩K c)) ∈ vpr K G a i v ⇗♢Vr K G a i v xa⇖" *)
apply (frule_tac n = "an N" in vp_apow_ideal[of "v"],
frule_tac x = "f (Suc (max M1 M2)) ± -⇩a b" and N = "an N" in
mem_vp_apow_mem_Vr[of "v"], simp,
frule Vr_ring[of "v"],  simp, simp)

apply (frule Vr_ring[of "v"],
frule_tac I = "vp K v⇗(Vr K v) (an N)⇖" and x = "f (Suc (max M1 M2)) ± -⇩a b"
in Ring.ideal_inv1_closed[of "Vr K v"], assumption+)
(** mOp of Vring and that of K is the same **)
apply (frule_tac I = "vp K v⇗(Vr K v) (an N)⇖" and h = "f (Suc (max M1 M2)) ± -⇩a b"
in Ring.ideal_subset[of "Vr K v"], assumption+)
cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
frule aGroup.ag_mOp_closed[of "K" "b"], assumption+,
(** addition of  -⇩K f (Suc (max xb xc)) +⇩K b  and f (Suc (max xb xc)) +⇩K -⇩K c
is included in vpr K G a i v ⇗♢(Vr K G a i v) xa⇖ **)
apply (frule_tac  I = "vp K v⇗(Vr K v) (an N)⇖" and x =
"-⇩a (f (Suc (max M1 M2))) ± b " and y = "f (Suc (max M1 M2)) ± (-⇩a c)" in
Ring.ideal_pOp_closed[of "Vr K v"], assumption+)
apply (frule_tac x = "f (Suc (max M1 M2)) ± -⇩a c" and N = "an N" in
mem_vp_apow_mem_Vr[of v], simp, assumption,
frule_tac x = "-⇩a (f (Suc (max M1 M2))) ± b" and N = "an N" in
mem_vp_apow_mem_Vr[of "v"], simp,
frule aGroup.ag_mOp_closed[of "K" "c"], assumption+,
frule_tac x = "f (Suc (max M1 M2))" in aGroup.ag_mOp_closed[of "K"],
assumption+,
frule_tac x = "f (Suc (max M1 M2))" and y = "-⇩a c" in
aGroup.ag_pOp_closed[of "K"], assumption+)

apply (simp add:aGroup.ag_pOp_assoc[of "K" _ "b" _],
simp add:aGroup.ag_pOp_assoc[THEN sym, of "K" "b" _ "-⇩a c"],
simp add:aGroup.ag_pOp_assoc[of "K" _ "b" "-⇩a c"],
frule aGroup.ag_pOp_closed[of "K" "b" "-⇩a c"], assumption+,
simp add:aGroup.ag_pOp_assoc[THEN sym, of "K" _ _ "b ± -⇩a c"],
apply (simp add:aGroup.ag_pOp_commute[of "K" _ "b"])
apply arith apply arith
done

(** The following lemma will be used to prove lemma limit_t. This lemma and
them next lemma show that the valuation v is continuous (see lemma
n_val **)
lemma (in Corps) limit_n_val:"⟦b ∈ carrier K; b ≠ 𝟬; valuation K v;
∀j. f j ∈ carrier K; lim⇘K v⇙ f b⟧ ⟹
∃N. (∀m. N < m ⟶ (n_val K v) (f m) = (n_val K v) b)"
apply (frule n_val_valuation[of "v"])
apply (frule val_nonzero_z[of "n_val K v" "b"], assumption+, erule exE,
rename_tac L)
apply (rotate_tac -3, drule_tac x = "nat (abs L + 1)" in spec)
apply (erule exE, rename_tac M)

(* |L| + 1 ≤ (n_val K v ( f n +⇩K -⇩K b)). *)
apply (subgoal_tac "∀n. M < n ⟶ n_val K v (f n) = n_val K v b", blast)
apply (rule allI, rule impI)
apply (rotate_tac -2,
drule_tac x = n in spec,
simp)
apply (frule_tac x = "f n ± -⇩a b" and n = "an (nat (¦L¦ + 1))" in
n_value_x_1[of "v"],
thin_tac "f n ± -⇩a b ∈ vp K v⇗(Vr K v) (an (nat (¦L¦ + 1)))⇖")
apply assumption

apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
apply (frule aGroup.ag_mOp_closed[of "K" "b"], assumption+)

apply (drule_tac x = n in spec,
frule_tac x = "f n" in aGroup.ag_pOp_closed[of "K" _ "-⇩a b"],
assumption+,
frule_tac x = "b" and y = "(f n) ± (-⇩a b)" in value_less_eq[of
"n_val K v"], assumption+)
apply simp
apply (rule_tac x = "ant L" and y = "an (nat (¦L¦ + 1))" and
z = "n_val K v ( f n ± -⇩a b)" in aless_le_trans)
apply (subst an_def)
apply (subst aless_zless) apply arith apply assumption+
done

lemma (in Corps) limit_val:"⟦b ∈ carrier K; b ≠ 𝟬; ∀j. f j ∈ carrier K;
valuation K v; lim⇘K v⇙ f b⟧ ⟹ ∃N. (∀n. N < n ⟶ v (f n) = v b)"
apply (frule limit_n_val[of "b" "v" "f"], assumption+)
apply (erule exE)
apply (subgoal_tac "∀m. N < m ⟶ v (f m) = v b")
apply blast
apply (rule allI, rule impI)
apply (drule_tac x = m in spec)
apply (drule_tac x = m in spec)
apply simp
apply (frule Lv_pos[of "v"])
apply (simp add:n_val[THEN sym, of "v"])
done

lemma (in Corps) limit_val_infinity:"⟦valuation K v; ∀j. f j ∈ carrier K;
lim⇘K v⇙ f 𝟬⟧ ⟹ ∀N.(∃M. (∀m. M < m ⟶ (an N) ≤ (n_val K v (f m))))"
apply (rule allI)
apply (drule_tac x = N in spec,
erule exE)

apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
simp only:aGroup.ag_inv_zero[of "K"], simp only:aGroup.ag_r_zero)
apply (subgoal_tac "∀n. M < n ⟶ an N ≤ n_val K v (f n)", blast)

apply (rule allI, rule impI)
apply (drule_tac x = n in spec,
drule_tac x = n in spec, simp)
done

lemma (in Corps) not_limit_zero:"⟦valuation K v; ∀j. f j ∈ carrier K;
¬ (lim⇘K v⇙ f 𝟬)⟧ ⟹ ∃N.(∀M. (∃m. (M < m) ∧
((n_val K v) (f m)) < (an N)))"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
apply (erule exE)
apply (case_tac "N = 0", simp add:r_apow_def)
apply (subgoal_tac "∀M. ∃n. M < n ∧ n_val K v (f n) < (an 0)") apply blast
apply (rule allI,
rotate_tac 4, frule_tac x = M in spec,
erule exE, erule conjE)
apply (frule_tac x1 = "f n" in val_pos_mem_Vr[THEN sym, of "v"]) apply simp
apply simp
apply (frule_tac x = "f n" in val_pos_n_val_pos[of "v"])
apply simp apply simp apply (thin_tac "¬ 0 ≤ v (f n)")

apply (simp)
apply (subgoal_tac "∀n. ((f n) ∈ vp K v⇗ (Vr K v) (an N)⇖) =
((an N) ≤ n_val K v (f n))")
apply simp
apply (thin_tac "∀n. (f n ∈ vp K v⇗ (Vr K v) (an N)⇖) = (an N ≤ n_val K v (f n))")

apply (rule allI)
apply (thin_tac "∀M. ∃n. M < n ∧ f n ∉ vp K v⇗ (Vr K v) (an N)⇖")
apply (rule iffI)
apply (frule_tac x1 = "f n" and n1 = "an N" in n_val_n_pow[THEN sym, of v])
apply (rule_tac N = "an N" and x = "f n" in mem_vp_apow_mem_Vr[of v],
assumption+, simp, assumption, simp, simp)
apply (frule_tac x = "f n" and n = "an N" in n_val_n_pow[of "v"])
apply (frule_tac x1 = "f n" in val_pos_mem_Vr[THEN sym, of "v"])
apply simp
apply (cut_tac n = N in an_nat_pos)
apply (frule_tac j = "an N" and k = "n_val K v (f n)" in ale_trans[of "0"],
assumption+)
apply (frule_tac x1 = "f n" in val_pos_n_val_pos[THEN sym, of "v"])
apply simp+
done

lemma (in Corps) limit_p:"⟦valuation K v; ∀j. f j  ∈ carrier K;
∀j. g j ∈ carrier K; b ∈ carrier K; c ∈ carrier K; lim⇘K v⇙ f b; lim⇘K v⇙ g c⟧
⟹ lim⇘K v⇙ (λj. (f j) ± (g j)) (b ± c)"
apply (rule allI) apply (rotate_tac 3,
drule_tac x = N in spec,
drule_tac x = N in spec,
(erule exE)+)
apply (frule_tac x = M and y = Ma in two_inequalities, simp,
subgoal_tac "∀n > (max M  Ma). (f n) ± (g n) ± -⇩a (b ± c)
∈ (vp K v)⇗(Vr K v) (an N)⇖")
apply (thin_tac "∀n. Ma < n ⟶
g n ± -⇩a c ∈ (vp K v)⇗(Vr K v) (an N)⇖",
thin_tac "∀n. M < n ⟶
f n ± -⇩a b ∈(vp K v)⇗(Vr K v) (an N)⇖", blast)
apply (frule Vr_ring[of v],
frule_tac n = "an N" in vp_apow_ideal[of v])
apply simp
apply (rule allI, rule impI)
apply (thin_tac "∀n>M. f n ± -⇩a b ∈ vp K v⇗ (Vr K v) (an N)⇖",
thin_tac "∀n>Ma. g n ± -⇩a c ∈ vp K v⇗ (Vr K v) (an N)⇖",
frule_tac I = "vp K v⇗(Vr K v) (an N)⇖" and x = "f n ± -⇩a b"
and y = "g n ± -⇩a c" in Ring.ideal_pOp_closed[of "Vr K v"],
assumption+, simp, simp)
apply (frule_tac I = "vp K v⇗(Vr K v) (an N)⇖" and h = "f n ± -⇩a b"
in Ring.ideal_subset[of "Vr K v"], assumption+, simp,
frule_tac I = "vp K v⇗(Vr K v) (an N)⇖" and h = "g n ± -⇩a c" in
Ring.ideal_subset[of "Vr K v"], assumption+, simp)
apply (thin_tac "f n ± -⇩a b ∈ carrier (Vr K v)",
thin_tac "g n ± -⇩a c ∈ carrier (Vr K v)")

apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
frule aGroup.ag_mOp_closed[of "K" "b"], assumption+,
frule aGroup.ag_mOp_closed[of "K" "c"], assumption+,
frule_tac a = "f n" and b = "-⇩a b" and c = "g n" and d = "-⇩a c" in
done

lemma (in Corps) Abs_ant_abs[simp]:"Abs (ant z) = ant (abs z)"
apply (simp only:ant_0[THEN sym], simp only:aless_zless)
done

lemma (in Corps) limit_t_nonzero:"⟦valuation K v; ∀(j::nat). (f j) ∈ carrier K; ∀(j::nat). g j ∈ carrier K;  b ∈ carrier K; c ∈ carrier K; b ≠ 𝟬; c ≠ 𝟬;
lim⇘K v⇙ f b; lim⇘K v⇙ g c⟧ ⟹ lim⇘K v⇙ (λj. (f j) ⋅⇩r (g j)) (b ⋅⇩r c)"
apply (cut_tac field_is_ring, simp add:limit_def, rule allI)
apply (subgoal_tac "∀j. (f j) ⋅⇩r (g j) ± -⇩a (b ⋅⇩r c) =
((f j) ⋅⇩r (g j) ± (f j) ⋅⇩r (-⇩a c)) ± ((f j) ⋅⇩r c ± -⇩a (b ⋅⇩r c))", simp,
thin_tac "∀j. f j ⋅⇩r g j ± -⇩a b ⋅⇩r c =
f j ⋅⇩r g j ± f j ⋅⇩r (-⇩a c) ± (f j ⋅⇩r c ± -⇩a b ⋅⇩r c)")
apply (frule limit_n_val[of  "b" "v" "f"], assumption+,
apply (frule n_val_valuation[of "v"])
apply (frule val_nonzero_z[of "n_val K v" "b"], assumption+,
rotate_tac -1, erule exE,
frule val_nonzero_z[of "n_val K v" "c"], assumption+,
rotate_tac -1, erule exE, rename_tac N bz cz)
apply (rotate_tac 5,
drule_tac x = "N + nat (abs cz)" in spec,
drule_tac x = "N + nat (abs bz)" in spec)
apply (erule exE)+
apply (rename_tac N bz cz M M1 M2)
(** three inequalities together **)
apply (subgoal_tac "∀n. (max (max M1 M2) M) < n ⟶
(f n) ⋅⇩r (g n) ± (f n) ⋅⇩r (-⇩a c) ± ((f n) ⋅⇩r c ± (-⇩a (b ⋅⇩r c)))
∈ vp K v ⇗(Vr K v) (an N)⇖",  blast)
apply (rule allI, rule impI) apply (simp, (erule conjE)+)
apply (rotate_tac 11, drule_tac x = n in spec,
drule_tac x = n in spec, simp,
drule_tac x = n in spec, simp)
apply (frule_tac b = "g n ± -⇩a c" and n = "an N" and x = "f n" in
convergenceTr1[of v])
apply simp apply simp apply (simp add:an_def a_zpz[THEN sym]) apply simp
apply (frule_tac b = "f n ± -⇩a b" and n = "an N" in convergenceTr1[of
"v" "c"], assumption+, simp) apply (simp add:an_def)
apply (simp add:a_zpz[THEN sym]) apply simp

apply (drule_tac x = n in spec,
drule_tac x = n in spec)
apply (simp add:Ring.ring_inv1_1[of "K" "b" "c"],
cut_tac Ring.ring_is_ag, frule aGroup.ag_mOp_closed[of "K" "c"],
assumption+,
frule aGroup.ag_mOp_closed[of "K" "b"], assumption+,
subst Ring.ring_tOp_commute[of "K" _ "c"], assumption+,
rule aGroup.ag_pOp_closed, assumption+)
apply (cut_tac n = N in an_nat_pos)
apply (frule_tac n = "an N" in vp_apow_ideal[of "v"], assumption+)
apply (frule Vr_ring[of "v"])

apply (frule_tac x = "(f n) ⋅⇩r (g n ± -⇩a c)" and y = "c ⋅⇩r (f n ± -⇩a b)"
and I = "vp K v⇗ (Vr K v) (an N)⇖" in Ring.ideal_pOp_closed[of "Vr K v"],
assumption+)
apply (frule_tac R = "Vr K v" and I = "vp K v⇗ (Vr K v) (an N)⇖" and
h = "(f n) ⋅⇩r (g n ± -⇩a c)" in Ring.ideal_subset, assumption+,
frule_tac R = "Vr K v" and I = "vp K v⇗ (Vr K v) (an N)⇖" and
h = "c ⋅⇩r (f n ± -⇩a b)" in Ring.ideal_subset, assumption+)
apply (rule allI)
apply (thin_tac "∀N. ∃M. ∀n>M. f n ± -⇩a b ∈ vp K v⇗ (Vr K v) (an N)⇖",
thin_tac "∀N. ∃M. ∀n>M. g n ± -⇩a c ∈ vp K v⇗ (Vr K v) (an N)⇖")
apply (drule_tac x = j in spec,
drule_tac x = j in spec,
cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
frule_tac x = "f j" and y = "g j" in Ring.ring_tOp_closed, assumption+,
frule_tac x = "b" and y = "c" in Ring.ring_tOp_closed, assumption+,
frule_tac x = "f j" and y = "c" in Ring.ring_tOp_closed, assumption+,
frule_tac x = c in aGroup.ag_mOp_closed[of "K"], assumption+,
frule_tac x = "f j" and y = "-⇩a c" in Ring.ring_tOp_closed, assumption+,
frule_tac x = "b ⋅⇩r c" in aGroup.ag_mOp_closed[of "K"], assumption+)
apply (subst aGroup.pOp_assocTr41[THEN sym, of "K"], assumption+,
subst aGroup.pOp_assocTr42[of "K"], assumption+,
subst Ring.ring_distrib1[THEN sym, of "K"], assumption+)
done

lemma an_npn[simp]:"an (n + m) = an n + an m"
by (simp add:an_def a_zpz) (** move **)

lemma Abs_noninf:"a ≠ -∞ ∧ a ≠ ∞ ⟹ Abs a ≠ ∞"
by (cut_tac mem_ant[of "a"], simp, erule exE, simp add:Abs_def,

lemma (in Corps) limit_t_zero:"⟦c ∈ carrier K; valuation K v;
∀(j::nat). f j ∈ carrier K; ∀(j::nat). g j ∈ carrier K;
lim⇘K v⇙ f 𝟬; lim⇘K v⇙ g c⟧ ⟹ lim⇘K v⇙ (λj. (f j) ⋅⇩r (g j)) 𝟬"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
apply (subgoal_tac "∀j. (f j) ⋅⇩r (g j) ∈ carrier K",
prefer 2 apply (rule allI, simp add:Ring.ring_tOp_closed)
apply (case_tac "c = 𝟬⇘K⇙")
apply (rule allI,
rotate_tac 4,
drule_tac x = N in spec,
drule_tac x = N in spec, (erule exE)+,
rename_tac N M1 M2)
apply (subgoal_tac "∀n>(max M1 M2). (f n) ⋅⇩r (g n) ∈ (vp K v)⇗(Vr K v) (an N)⇖",
blast)
apply (rule allI, rule impI)
apply (drule_tac x = M1 and y = M2 in two_inequalities, assumption+,
thin_tac "∀n>M2. g n ∈ vp K v⇗ (Vr K v) (an N)⇖")
apply (thin_tac "∀j. f j ⋅⇩r g j ∈ carrier K",
thin_tac "∀j. f j ∈ carrier K",
thin_tac "∀j. g j ∈ carrier K",
drule_tac x = n in spec, simp, erule conjE,
erule conjE,
frule Vr_ring[of v])
apply (cut_tac n = N in an_nat_pos)
apply (frule_tac x = "f n" in mem_vp_apow_mem_Vr[of  "v"], assumption+,
frule_tac x = "g n" in mem_vp_apow_mem_Vr[of  "v"], assumption+,
frule_tac n = "an N" in vp_apow_ideal[of  "v"], assumption+)
apply (frule_tac I = "vp K v⇗(Vr K v) (an N)⇖" and x = "g n" and
r = "f n" in Ring.ideal_ring_multiple[of "Vr K v"], assumption+,

(** case c ≠ 0⇩K **)
apply (rule allI)
apply (subgoal_tac "∀j. (f j) ⋅⇩r (g j) =
(f j) ⋅⇩r ((g j) ± (-⇩a c)) ± (f j) ⋅⇩r c", simp,
thin_tac "∀j. (f j) ⋅⇩r (g j) =
(f j) ⋅⇩r ((g j) ± (-⇩a c)) ± (f j) ⋅⇩r c",
thin_tac "∀j.  (f j) ⋅⇩r ( g j ± -⇩a c) ± (f j) ⋅⇩r c ∈ carrier K")
apply (rotate_tac 4,
drule_tac x = "N + na (Abs (n_val K v c))" in  spec,
drule_tac x = N in spec)
apply (erule exE)+ apply (rename_tac N M1 M2)
apply (subgoal_tac "∀n. (max M1 M2) < n ⟶ (f n) ⋅⇩r (g n ± -⇩a c) ±
(f n) ⋅⇩r  c ∈ vp K v⇗(Vr K v) (an N)⇖", blast)
apply (rule allI, rule impI, simp, erule conjE,
drule_tac x = n in spec,
drule_tac x = n in spec,
drule_tac x = n in spec)
apply (frule n_val_valuation[of "v"])
apply (frule value_in_aug_inf[of "n_val K v" "c"], assumption+,
apply (frule val_nonzero_noninf[of "n_val K v" "c"], assumption+)
apply (cut_tac Abs_noninf[of "n_val K v c"])
apply (cut_tac Abs_pos[of "n_val K v c"]) apply (simp add:an_na)

apply (drule_tac x = n in spec, simp)
apply (frule_tac b = "f n" and n = "an N" in convergenceTr1[of
"v" "c"], assumption+)
apply simp

apply (frule_tac x = "f n" and N = "an N + Abs (n_val K v c)" in
mem_vp_apow_mem_Vr[of "v"],
frule_tac n = "an N" in vp_apow_ideal[of "v"])
apply simp
apply (rule_tac x = "an N" and y = "Abs (n_val K v c)" in aadd_two_pos)
apply simp apply (simp add:Abs_pos) apply assumption

apply (frule_tac x = "g n ± (-⇩a c)" and N = "an N" in mem_vp_apow_mem_Vr[of
"v"], simp, assumption+) apply (
frule_tac x = "c ⋅⇩r (f n)" and N = "an N" in mem_vp_apow_mem_Vr[of
"v"], simp)  apply simp
apply (simp add:Ring.ring_tOp_commute[of "K" "c"]) apply (
frule Vr_ring[of  "v"],
frule_tac I = "(vp K v)⇗(Vr K v) (an N)⇖" and x = "g n ± (-⇩a c)"
and r = "f n" in Ring.ideal_ring_multiple[of "Vr K v"])
apply (frule_tac I = "vp K v⇗(Vr K v) (an N)⇖" and
x = "(f n) ⋅⇩r (g n ± -⇩a c)" and y = "(f n) ⋅⇩r c" in
Ring.ideal_pOp_closed[of "Vr K v"])
frule_tac x = "(f n) ⋅⇩r (g n ± -⇩a c)" and N = "an N" in mem_vp_apow_mem_Vr[of "v"], simp add:Vr_pOp_f_pOp, assumption+)
apply (frule_tac N = "an N" and x = "(f n) ⋅⇩r c" in mem_vp_apow_mem_Vr[of
"v"]) apply simp apply assumption

apply (thin_tac "∀N. ∃M. ∀n>M. f n ∈ vp K v⇗ (Vr K v) (an N)⇖",
thin_tac "∀N. ∃M. ∀n>M. g n ± -⇩a c ∈ vp K v⇗ (Vr K v) (an N)⇖",
rule allI)
apply (drule_tac x = j in spec,
drule_tac x = j in spec,
drule_tac x = j in spec,
frule  aGroup.ag_mOp_closed[of "K" "c"], assumption+,
frule_tac x = "f j" in Ring.ring_tOp_closed[of "K" _ "c"], assumption+,
frule_tac x = "f j" in Ring.ring_tOp_closed[of "K" _ "-⇩a c"], assumption+)
done

lemma (in Corps) limit_minus:"⟦valuation K v; ∀j. f j ∈ carrier K;
b ∈ carrier K; lim⇘K v⇙ f b⟧ ⟹ lim⇘K v⇙ (λj. (-⇩a (f j))) (-⇩a b)"
apply (rule allI,
rotate_tac -1, frule_tac x = N in spec,
thin_tac "∀N. ∃M. ∀n. M < n ⟶
f n ± -⇩a b ∈ (vp K v)⇗(Vr K v) (an N)⇖",
erule exE,
subgoal_tac "∀n. M < n ⟶
(-⇩a (f n)) ± (-⇩a (-⇩a b)) ∈ (vp K v)⇗(Vr K v) (an N)⇖",
blast)
apply (rule allI, rule impI,
frule_tac x = n in spec,
frule_tac x = n in spec, simp)

apply (frule Vr_ring[of "v"],
frule_tac n = "an N" in vp_apow_ideal[of "v"], simp)
apply (frule_tac x = "f n ± -⇩a b" and N = "an N" in
mem_vp_apow_mem_Vr[of "v"], simp+,
frule_tac I = "vp K v⇗(Vr K v) (an N)⇖" and x = "f n ± (-⇩a b)" in
Ring.ideal_inv1_closed[of "Vr K v"], assumption+, simp)
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
frule aGroup.ag_mOp_closed[of "K" "b"], assumption+)
done

lemma (in Corps) inv_diff:"⟦x ∈ carrier K; x ≠ 𝟬; y ∈ carrier K; y ≠ 𝟬⟧ ⟹
(x⇗‐K⇖) ± (-⇩a (y⇗‐K⇖)) = (x⇗‐K⇖) ⋅⇩r ( y⇗‐K⇖) ⋅⇩r (-⇩a (x ± (-⇩a y)))"
apply (cut_tac invf_closed1[of "x"], simp, erule conjE,
cut_tac invf_closed1[of y], simp, erule conjE,
cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
frule Ring.ring_tOp_closed[of "K" "x⇗‐K⇖" "y⇗‐K⇖"], assumption+,
frule aGroup.ag_mOp_closed[of "K" "x"], assumption+,
frule aGroup.ag_mOp_closed[of "K" "y"], assumption+,
frule aGroup.ag_mOp_closed[of "K" "x⇗‐K⇖"], assumption+,
frule aGroup.ag_mOp_closed[of "K" "y⇗‐K⇖"], assumption+,
frule aGroup.ag_pOp_closed[of "K" "x" "-⇩a y"], assumption+)

simp only:Ring.ring_distrib1[of "K" "(x⇗‐K⇖) ⋅⇩r (y⇗‐K⇖)" "x" "-⇩a y"],
simp only:Ring.ring_tOp_commute[of "K" _ x],
simp only:Ring.ring_inv1_2[THEN sym, of "K"],
simp only:Ring.ring_tOp_assoc[THEN sym],
simp only:Ring.ring_tOp_commute[of "K" "x"],
cut_tac linvf[of  "x"], simp+,
cut_tac linvf[of "y"], simp+,
simp only:Ring.ring_r_one)
rule aGroup.ag_pOp_commute[of "K" "x⇗‐K⇖" "-⇩a y⇗‐K⇖"], assumption+)
apply simp+
done

lemma times2plus:"(2::nat)*n = n + n"
by simp

lemma (in Corps) limit_inv:"⟦valuation K v; ∀j. f j ∈ carrier K;
b ∈ carrier K; b ≠ 𝟬; lim⇘K v⇙ f b⟧ ⟹
lim⇘K v⇙ (λj. if (f j) = 𝟬 then 𝟬 else (f j)⇗‐K⇖) (b⇗‐K⇖)"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
apply (frule limit_n_val[of "b" "v" "f"], assumption+)
apply (subst limit_def)
apply (rule allI, erule exE)
apply (subgoal_tac "∀m>Na. f m ≠ 𝟬")
prefer 2
apply (rule allI, rule impI, rotate_tac -2,
drule_tac x = m in spec, simp)
apply (frule n_val_valuation[of v])
apply (frule val_nonzero_noninf[of "n_val K v" b], assumption+)
apply (rule contrapos_pp, simp+, simp add:value_of_zero)
apply (unfold limit_def)
apply (rotate_tac 2,
frule_tac x = "N + 2*(na (Abs (n_val K v b)))" in
spec)
apply (erule exE)
apply (subgoal_tac "∀n>(max Na M).
(if f n = 𝟬 then 𝟬 else f n⇗‐K⇖) ± -⇩a b⇗‐K⇖ ∈ vp K v⇗(Vr K v) (an N)⇖",
blast)
apply (rule allI, rule impI)
apply (cut_tac x = "Na" and y = "max Na M" and z = n
in le_less_trans)
apply simp+
apply (thin_tac "∀N. ∃M. ∀n>M. f n ± -⇩a b ∈ vp K v⇗ (Vr K v) (an N)⇖")
apply (drule_tac x = n in spec,
drule_tac x = n in spec,
drule_tac x = n in spec,
drule_tac x = n in spec, simp)
apply (subst inv_diff, assumption+)
apply (cut_tac x = "f n" in invf_closed1, simp,
cut_tac x = b in invf_closed1, simp, simp, (erule conjE)+)
(* apply (frule field_is_idom[of "K"], frule field_iOp_closed[of "K" "b"],
simp, simp, erule conjE,
frule idom_tOp_nonzeros [of "K" "b⇗‐K⇖" "b⇗‐K⇖"], assumption+) *)
apply (frule_tac n = "an N + an (2 * na (Abs (n_val K v b)))" and
x = "f n ± -⇩a b" in n_value_x_1[of v])
apply (simp only:an_npn[THEN sym], rule an_nat_pos)
apply assumption
apply (rule_tac x = "f n⇗‐ K⇖ ⋅⇩r b⇗‐ K⇖ ⋅⇩r (-⇩a (f n ± -⇩a b))" and v = v and
n = "an N" in n_value_x_2, assumption+)
apply (frule n_val_valuation[of v])
apply (subst val_pos_mem_Vr[THEN sym, of "v"], assumption+)
apply (rule Ring.ring_tOp_closed, assumption+)+
apply (rule aGroup.ag_mOp_closed, assumption)
apply (rule aGroup.ag_pOp_closed, assumption+,
rule aGroup.ag_mOp_closed, assumption+)
apply (subst val_pos_n_val_pos[of v], assumption+,
rule Ring.ring_tOp_closed, assumption+,
rule Ring.ring_tOp_closed, assumption+,
rule aGroup.ag_mOp_closed, assumption+,
rule aGroup.ag_pOp_closed, assumption+,
rule aGroup.ag_mOp_closed, assumption+)
apply (subst val_t2p[of "n_val K v"], assumption+,
rule Ring.ring_tOp_closed, assumption+,
rule aGroup.ag_mOp_closed, assumption+,
rule aGroup.ag_pOp_closed, assumption+,
rule aGroup.ag_mOp_closed, assumption+,
subst val_minus_eq[of "n_val K v"], assumption+,
(rule aGroup.ag_pOp_closed, assumption+),
(rule aGroup.ag_mOp_closed, assumption+))
apply (subst val_t2p[of "n_val K v"], assumption+)
apply (frule_tac x = "an N + an (2 * na (Abs (n_val K v b)))" and y = "n_val K v (f n ± -⇩a b)" and z = "- n_val K v b + - n_val K v b" in aadd_le_mono)
apply (cut_tac z = "n_val K v b" in Abs_pos)
apply (frule val_nonzero_z[of "n_val K v" b], assumption+, erule exE)
apply (rotate_tac -1, drule sym, cut_tac z = z in z_neq_minf,
cut_tac z = z in z_neq_inf, simp,
cut_tac a = "(n_val K v b)" in Abs_noninf, simp)
apply (simp only:times2plus an_npn, simp add:an_na)
apply (rotate_tac -4, drule sym, simp)
apply (thin_tac "f n ± -⇩a b ∈ vp K v⇗ (Vr K v) (an N + (ant ¦z¦ + ant ¦z¦))⇖")
apply (rule_tac i = 0 and j = "ant (int N + 2 * ¦z¦ - 2 * z)" and
k = "n_val K v (f n ± -⇩a b) + ant (- (2 * z))" in ale_trans)
apply (subst ant_0[THEN sym])
apply (subst ale_zle, simp, assumption)

apply (frule n_val_valuation[of v])
apply (subst val_t2p[of "n_val K v"], assumption+)
apply (rule Ring.ring_tOp_closed, assumption+)+
apply (rule aGroup.ag_mOp_closed, assumption)
apply (rule aGroup.ag_pOp_closed, assumption+,
rule aGroup.ag_mOp_closed, assumption+)
apply (subst val_t2p[of "n_val K v"], assumption+)
apply (subst val_minus_eq[of "n_val K v"], assumption+,
rule aGroup.ag_pOp_closed, assumption+,
rule aGroup.ag_mOp_closed, assumption+)

apply (frule_tac x = "an N + an (2 * na (Abs (n_val K v b)))" and y = "n_val K v (f n ± -⇩a b)" and z = "- n_val K v b + - n_val K v b" in aadd_le_mono)
apply (cut_tac z = "n_val K v b" in Abs_pos)
apply (frule val_nonzero_z[of "n_val K v" b], assumption+, erule exE)
apply (rotate_tac -1, drule sym, cut_tac z = z in z_neq_minf,
cut_tac z = z in z_neq_inf, simp,
cut_tac a = "(n_val K v b)" in Abs_noninf, simp)
apply (simp only:times2plus an_npn, simp add:an_na)
apply (rotate_tac -4, drule sym, simp)
apply (thin_tac "f n ± -⇩a b ∈ vp K v⇗ (Vr K v) (an N + (ant ¦z¦ + ant ¦z¦))⇖")
apply (rule_tac i = "ant (int N)" and j = "ant (int N + 2 * ¦z¦ - 2 * z)"
and k = "n_val K v (f n ± -⇩a b) + ant (- (2 * z))" in ale_trans)
apply (subst ale_zle, simp, assumption)

apply simp
done

definition
Cauchy_seq :: "[_ , 'b ⇒ ant, nat ⇒ 'b]
⇒ bool" ("(3Cauchy⇘ _ _ ⇙_)" [90,90,91]90) where
"Cauchy⇘K v⇙ f ⟷ (∀n. (f n) ∈ carrier K) ∧ (
∀N. ∃M. (∀n m. M < n ∧ M < m ⟶
((f n) ±⇘K⇙ (-⇩a⇘K⇙ (f m))) ∈ (vp K v)⇗(Vr K v) (an N)⇖))"

definition
v_complete :: "['b ⇒ ant, _] ⇒ bool"
("(2Complete⇘_⇙ _)"  [90,91]90) where
"Complete⇘v⇙ K ⟷ (∀f. (Cauchy⇘K v⇙ f) ⟶
(∃b. b ∈ (carrier K) ∧ lim⇘K v⇙ f b))"

lemma (in Corps) has_limit_Cauchy:"⟦valuation K v; ∀j. f j ∈ carrier K;
b ∈ carrier K; lim⇘K v⇙ f b⟧ ⟹ Cauchy⇘K v⇙ f"
apply (rule allI)
apply (rotate_tac -1)
apply (drule_tac x = N in spec)
apply (erule exE)
apply (subgoal_tac "∀n m. M < n ∧ M < m ⟶
f n ± -⇩a (f m) ∈ vp K v⇗(Vr K v) (an N)⇖")
apply blast
apply ((rule allI)+, rule impI, erule conjE)
apply (frule_tac x = n in spec,
frule_tac x = m in spec,
thin_tac "∀j. f j ∈ carrier K",
frule_tac x = n in spec,
frule_tac x = m in spec,
thin_tac "∀n. M < n ⟶  f n ± -⇩a b ∈ vp K v⇗(Vr K v) (an N)⇖",
simp)
apply (frule_tac n = "an N" in vp_apow_ideal[of v], simp)
apply (frule Vr_ring[of "v"])
apply (frule_tac x = "f m ± -⇩a b" and I = "vp K v⇗(Vr K v) (an N)⇖" in
Ring.ideal_inv1_closed[of "Vr K v"], assumption+)
apply (frule_tac h = "f m ± -⇩a b" and I = "vp K v⇗(Vr K v) (an N)⇖" in
Ring.ideal_subset[of "Vr K v"], assumption+,
frule_tac h = "f n ± -⇩a b" and I = "vp K v⇗(Vr K v) (an N)⇖" in
Ring.ideal_subset[of "Vr K v"], assumption+)
apply (frule_tac h = "-⇩a⇘Vr K v⇙ (f m ± -⇩a b)" and I = "vp K v⇗(Vr K v) (an N)⇖" in         Ring.ideal_subset[of "Vr K v"], assumption+,
frule_tac h = "f n ± -⇩a b" and I = "vp K v⇗(Vr K v) (an N)⇖" in
Ring.ideal_subset[of "Vr K v"], assumption+)
apply (frule_tac I = "(vp K v)⇗ (Vr K v) (an N)⇖" and x = "f n ± -⇩a b" and
y = "-⇩a⇘(Vr K v)⇙ (f m ± -⇩a b)" in Ring.ideal_pOp_closed[of "Vr K v"],
assumption+)
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
apply (frule aGroup.ag_mOp_closed[of "K" "b"], assumption+)
apply (frule_tac x = "f m ± -⇩a b" in Vr_mem_f_mem[of "v"], assumption+)
apply (frule_tac x = "f m ± -⇩a b" in aGroup.ag_mOp_closed[of "K"],
assumption+)
apply (simp add:aGroup.ag_pOp_commute[of "K" "-⇩a b"])
apply (frule_tac x = "f m" in aGroup.ag_mOp_closed[of "K"], assumption+)
apply (simp add:aGroup.ag_pOp_assoc[of "K" _ "b" "-⇩a b"])
done

lemma (in Corps) no_limit_zero_Cauchy:"⟦valuation K v; Cauchy⇘K v⇙ f;
¬ (lim⇘K v⇙ f 𝟬)⟧ ⟹
∃N M. (∀m. N < m ⟶  ((n_val K v) (f M))  = ((n_val K v) (f m)))"
apply (frule not_limit_zero[of "v" "f"], thin_tac "¬ lim⇘ K v ⇙f 𝟬")
apply (simp add:Cauchy_seq_def, assumption) apply (erule exE)
apply (rename_tac L)
rotate_tac -1,
frule_tac x = L in spec, thin_tac "∀N. ∃M. ∀n m.
M < n ∧ M < m ⟶ f n ± -⇩a (f m) ∈ vp K v⇗(Vr K v) (an N)⇖")
apply (erule exE)
apply (drule_tac x = M in spec)
apply (erule exE, erule conjE)
apply (rotate_tac -3,
frule_tac x = m in spec)
apply (thin_tac "∀n m. M < n ∧ M < m ⟶
f n ± -⇩a (f m) ∈ (vp K v)⇗(Vr K v) (an L)⇖")
apply (subgoal_tac "M < m ∧ (∀ma. M < ma ⟶
n_val K v (f m) = n_val K v (f ma))")
apply blast
apply simp

apply (rule allI, rule impI)
apply (rotate_tac -2)
apply (drule_tac x = ma in spec)
apply simp
(** we have f ma ± -⇩a f m ∈ vpr K G a i v ⇗♢Vr K G a i v L⇖ as **)
apply (frule Vr_ring[of "v"],
frule_tac n = "an L" in vp_apow_ideal[of "v"], simp)
apply (frule_tac I = "vp K v⇗(Vr K v) (an L)⇖" and x = "f m ± -⇩a (f ma)"
in Ring.ideal_inv1_closed[of "Vr K v"], assumption+) apply (
frule_tac I = "vp K v⇗(Vr K v) (an L)⇖" and
h = "f m ± -⇩a (f ma)" in Ring.ideal_subset[of "Vr K v"],
apply (frule_tac x = m in spec,
drule_tac x = ma in spec)  apply (

cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
frule_tac x = "f ma" in aGroup.ag_mOp_closed[of "K"], assumption+,
frule_tac x = "f m" and y = "-⇩a (f ma)" in aGroup.ag_p_inv[of "K"],
assumption+, simp only:aGroup.ag_inv_inv,
frule_tac x = "f m" in aGroup.ag_mOp_closed[of "K"], assumption+,
thin_tac "-⇩a ( f m ± -⇩a (f ma)) =  f ma ± -⇩a (f m)",
thin_tac "f m ± -⇩a (f ma) ∈ vp K v⇗(Vr K v) (an L)⇖")
(** finally, by f ma = f m ± (f ma ± -⇩a (f m)) and value_less_eq
we have the conclusion **)
apply (frule_tac x = "f ma ± -⇩a (f m)" and n = "an L" in n_value_x_1[of
"v" ], simp) apply assumption apply (
frule n_val_valuation[of "v"],
frule_tac x = "f m" and y = "f ma ± -⇩a (f m)" in value_less_eq[of
"n_val K v"], assumption+) apply (simp add:aGroup.ag_pOp_closed)
apply (
rule_tac x = "n_val K v (f m)" and y = "an L" and
z = "n_val K v ( f ma ± -⇩a (f m))" in
aless_le_trans, assumption+)
apply (frule_tac x = "f ma ± -⇩a (f m)" in Vr_mem_f_mem[of "v"])
apply (frule_tac x = "f m" and y = "f ma ± -⇩a (f m)" in
aGroup.ag_pOp_commute[of "K"], assumption+)
done

lemma (in Corps) no_limit_zero_Cauchy1:"⟦valuation K v; ∀j. f j ∈ carrier K;
Cauchy⇘K v⇙ f; ¬ (lim⇘K v⇙ f 𝟬)⟧ ⟹ ∃N M. (∀m. N < m ⟶  v (f M) = v (f m))"
apply (frule no_limit_zero_Cauchy[of "v" "f"], assumption+)
apply (erule exE)+
apply (subgoal_tac "∀m. N < m ⟶ v (f M) = v (f m)") apply blast
apply (rule allI, rule impI)
apply (frule_tac x = M in spec,
drule_tac x = m in spec,
drule_tac x = m in spec, simp)
apply (simp add:n_val[THEN sym, of "v"])
done

definition
subfield :: "[_, ('b, 'm1) Ring_scheme] ⇒ bool" where
"subfield K K' ⟷ Corps K' ∧ carrier K ⊆ carrier K' ∧
idmap (carrier K) ∈ rHom K K'"

definition
v_completion :: "['b ⇒ ant, 'b ⇒ ant, _, ('b, 'm) Ring_scheme] ⇒ bool"
("(4Completion⇘_ _⇙ _ _)" [90,90,90,91]90) where
"Completion⇘v v'⇙ K K' ⟷ subfield K K' ∧
Complete⇘v'⇙ K' ∧ (∀x ∈ carrier K. v x = v' x) ∧
(∀x ∈ carrier K'. (∃f. Cauchy⇘K v⇙ f ∧ lim⇘K' v'⇙ f x))"

lemma (in Corps) subfield_zero:"⟦Corps K'; subfield K K'⟧ ⟹ 𝟬⇘K⇙ = 𝟬⇘K'⇙"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
frule Corps.field_is_ring[of "K'"], frule Ring.ring_is_ag[of "K'"])
apply (frule aHom_0_0[of "K" "K'" "I⇘K⇙"], assumption+)
apply (frule aGroup.ag_inc_zero[of "K"], simp add:idmap_def)
done

lemma (in Corps) subfield_pOp:"⟦Corps K'; subfield K K'; x ∈ carrier K;
y ∈ carrier K⟧ ⟹ x ± y = x ±⇘K'⇙ y"
apply (cut_tac field_is_ring, frule Corps.field_is_ring[of "K'"],
frule Ring.ring_is_ag[of "K"], frule Ring.ring_is_ag[of "K'"])
frule conjunct1)
apply (thin_tac "I⇘K⇙ ∈ aHom K K' ∧
(∀x∈carrier K. ∀y∈carrier K. I⇘K⇙ (x ⋅⇩r y) = I⇘K⇙ x ⋅⇩r⇘K'⇙ I⇘K⇙ y) ∧
I⇘K⇙ 1⇩r = 1⇩r⇘K'⇙")
apply (frule aHom_add[of "K" "K'" "I⇘K⇙" "x" "y"], assumption+,
frule aGroup.ag_pOp_closed[of "K" "x" "y"], assumption+,
done

lemma (in Corps) subfield_mOp:"⟦Corps K'; subfield K K'; x ∈ carrier K⟧ ⟹
-⇩a x = -⇩a⇘K'⇙ x"
apply (cut_tac field_is_ring, frule Corps.field_is_ring[of "K'"],
frule Ring.ring_is_ag[of "K"], frule Ring.ring_is_ag[of "K'"])
frule conjunct1)
apply (thin_tac "I⇘K⇙ ∈ aHom K K' ∧
(∀x∈carrier K. ∀y∈carrier K. I⇘K⇙ (x ⋅⇩r y) = I⇘K⇙ x ⋅⇩r⇘K'⇙ I⇘K⇙ y) ∧
I⇘K⇙ 1⇩r = 1⇩r⇘K'⇙")
apply (frule aHom_inv_inv[of "K" "K'" "I⇘K⇙" "x"], assumption+,
frule aGroup.ag_mOp_closed[of "K" "x"], assumption+)
done

lemma (in Corps) completion_val_eq:"⟦Corps K'; valuation K v; valuation K' v';
x ∈ carrier K;  Completion⇘v v'⇙ K K'⟧ ⟹ v x = v' x"
apply (unfold v_completion_def, (erule conjE)+)
apply simp
done

lemma (in Corps) completion_subset:"⟦Corps K'; valuation K v; valuation K' v';
Completion⇘v v'⇙ K K'⟧ ⟹  carrier K ⊆ carrier K'"
apply (unfold v_completion_def, (erule conjE)+)
done

lemma (in Corps) completion_subfield:"⟦Corps K'; valuation K v;
valuation K' v'; Completion⇘v v'⇙ K K'⟧ ⟹  subfield K K'"
done

lemma (in Corps) subfield_sub:"subfield K K' ⟹ carrier K ⊆ carrier K'"
done

lemma (in Corps) completion_Vring_sub:"⟦Corps K'; valuation K v;
valuation K' v'; Completion⇘v v'⇙ K K'⟧ ⟹
carrier (Vr K v) ⊆ carrier (Vr K' v')"
apply (rule subsetI,
frule completion_subset[of  "K'" "v" "v'"], assumption+,
frule_tac x = x in Vr_mem_f_mem[of "v"], assumption+,
frule_tac x = x in completion_val_eq[of "K'" "v" "v'"],
assumption+)
apply (frule_tac x1 = x in val_pos_mem_Vr[THEN sym, of  "v"],
assumption+, simp,
frule_tac c = x in subsetD[of "carrier K" "carrier K'"], assumption+,
done

lemma (in Corps) completion_idmap_rHom:"⟦Corps K'; valuation K v;
valuation K' v';  Completion⇘v v'⇙ K K'⟧ ⟹
I⇘(Vr K v)⇙ ∈ rHom (Vr K v) (Vr K' v')"
apply (frule completion_Vring_sub[of  "K'" "v" "v'"],
assumption+,
frule completion_subfield[of "K'" "v" "v'"],
assumption+,
frule Vr_ring[of "v"],
frule Ring.ring_is_ag[of "Vr K v"],
frule Corps.Vr_ring[of "K'" "v'"], assumption+,
frule Ring.ring_is_ag[of "Vr K' v'"])
apply (rule conjI)
rule conjI,
apply (rule conjI)
apply ((rule ballI)+) apply (
frule_tac x = a and y = b in aGroup.ag_pOp_closed, assumption+,
frule_tac c = a in subsetD[of "carrier (Vr K v)"
"carrier (Vr K' v')"], assumption+,
frule_tac c = b in subsetD[of "carrier (Vr K v)"
"carrier (Vr K' v')"], assumption+,
frule_tac x = a in Vr_mem_f_mem[of v], assumption,
frule_tac x = b in Vr_mem_f_mem[of v], assumption,
apply (rule conjI)
apply ((rule ballI)+,
frule_tac x = x and y = y in Ring.ring_tOp_closed, assumption+,
apply (frule_tac c = x in subsetD[of "carrier (Vr K v)"
"carrier (Vr K' v')"], assumption+,
frule_tac c = y in subsetD[of "carrier (Vr K v)"
"carrier (Vr K' v')"], assumption+)
apply (frule_tac x = x in Vr_mem_f_mem[of "v"], assumption+,
frule_tac x = y in Vr_mem_f_mem[of "v"], assumption+,
frule_tac x = x in Corps.Vr_mem_f_mem[of "K'" "v'"], assumption+,
frule_tac x = y in Corps.Vr_mem_f_mem[of "K'" "v'"], assumption+,
cut_tac field_is_ring, frule Corps.field_is_ring[of "K'"],
frule_tac x = x and y = y in Ring.ring_tOp_closed[of "K"], assumption+)
apply (frule_tac x = x and y = y in rHom_tOp[of "K" "K'" _ _ "I⇘K⇙"],
apply (frule Ring.ring_one[of "Vr K v"], simp add:idmap_def)
apply (cut_tac field_is_ring, frule Corps.field_is_ring[of "K'"],
frule Ring.ring_one[of "K"],
frule rHom_one[of "K" "K'" "I⇘K⇙"], assumption+, simp add:idmap_def)
done

lemma (in Corps) completion_vpr_sub:"⟦Corps K'; valuation K v; valuation K' v';
Completion⇘v v'⇙ K K'⟧ ⟹ vp K v ⊆ vp K' v'"
apply (rule subsetI,
frule completion_subset[of "K'" "v" "v'"], assumption+,
frule Vr_ring[of "v"], frule vp_ideal[of "v"],
frule_tac h = x in Ring.ideal_subset[of "Vr K v" "vp K v"],
assumption+,
frule_tac x = x in Vr_mem_f_mem[of  "v"], assumption+,
frule_tac x = x in completion_val_eq[of "K'" "v" "v'"],
assumption+)
apply (frule completion_subset[of "K'" "v" "v'"],
assumption+,
frule_tac c = x in subsetD[of "carrier K" "carrier K'"], assumption+,
done

lemma (in Corps) val_v_completion:"⟦Corps K'; valuation K v; valuation K' v';
x ∈ carrier K'; x ≠ 𝟬⇘K'⇙; Completion⇘v v'⇙ K K'⟧ ⟹
∃f. (Cauchy⇘K v⇙ f) ∧ (∃N. (∀m. N < m ⟶ v (f m) = v' x))"
apply (simp add:v_completion_def, erule conjE, (erule conjE)+)
apply (rotate_tac -1, drule_tac x = x in bspec, assumption+,
erule exE, erule conjE,
subgoal_tac "∃N. ∀m. N < m ⟶ v (f m) = v' x", blast)
thm Corps.limit_val
apply (frule_tac f = f and v = v' in  Corps.limit_val[of "K'" "x"],
assumption+,
unfold Cauchy_seq_def, frule conjunct1, fold Cauchy_seq_def)
apply (rule allI, drule_tac x = j in spec,
done

lemma (in Corps) v_completion_v_limit:"⟦Corps K'; valuation K v;
x ∈ carrier K; subfield K K'; Complete⇘v'⇙ K'; ∀j. f j ∈ carrier K;
valuation K' v'; ∀x∈carrier K. v x = v' x; lim⇘K' v' ⇙f x⟧ ⟹ lim⇘K v ⇙f x"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
frule Corps.field_is_ring[of K'], frule Ring.ring_is_ag[of "K'"],
subgoal_tac "∀j. f j ∈ carrier K'",
unfold subfield_def, frule conjunct2, fold subfield_def, erule conjE)
apply (frule subsetD[of "carrier K" "carrier K'" "x"], assumption+,
subgoal_tac "∀n. f n ±⇘K'⇙ -⇩a⇘K'⇙ x = f n ± -⇩a x")
apply (rule allI)
apply (rotate_tac 6, drule_tac x = N in spec,
erule exE)
apply (subgoal_tac "∀n>M. an N ≤ v'(f n ± -⇩a x)",
subgoal_tac "∀n. (v' (f n ± -⇩a x) = v (f n ± -⇩a x))", simp, blast)
apply (rule allI)
apply (frule_tac x = "f n ± -⇩a x" in bspec,
rule aGroup.ag_pOp_closed, assumption+, simp,
rule aGroup.ag_mOp_closed, assumption+) apply simp
apply (rule allI, rule impI)
apply (frule_tac v = v' and n = "an N" and x = "f n ± -⇩a x" in
Corps.n_value_x_1[of K'], assumption+, simp, simp)
apply (frule_tac v = v' and x = "f n ± -⇩a x" in Corps.n_val_le_val[of K'],
assumption+)
apply (cut_tac x = "f n" and y = "-⇩a x" in aGroup.ag_pOp_closed, assumption,
simp, rule aGroup.ag_mOp_closed, assumption+, simp add:subsetD)
apply (subst Corps.val_pos_n_val_pos[of K' v'], assumption+)
apply (cut_tac x = "f n" and y = "-⇩a x" in aGroup.ag_pOp_closed, assumption,
simp, rule aGroup.ag_mOp_closed, assumption+, simp add:subsetD)
apply (rule_tac i = 0 and j = "an N" and k = "n_val K' v' (f n ± -⇩a x)" in
ale_trans, simp+, rul```