# Theory Valuation1

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

chapter 1. elementary properties of a valuation
section 1. definition of a valuation
section 2. the normal valuation of v
section 3. valuation ring
section 4. ideals in a valuation ring
section 5. pow of vp and n_value -- convergence --
section 6. equivalent valuations
section 7. prime divisors
section 8. approximation

**)

theory Valuation1
imports  "Group-Ring-Module.Algebra9"
begin

declare ex_image_cong_iff [simp del]

chapter "Preliminaries"

section "Int and ant (augmented integers)"

lemma int_less_mono:"(a::nat) < b ⟹ int a < int b"
apply simp
done

lemma zless_trans:"⟦(i::int) < j; j < k⟧ ⟹ i < k"
apply simp
done

lemma zmult_pos_bignumTr0:"∃L. ∀m. L < m ⟶ z < x + int m"
by (subgoal_tac "∀m. (nat((abs z) + (abs x))) < m ⟶ z < x + int m",
blast, rule allI, rule impI, arith)

lemma zle_less_trans:"⟦(i::int) ≤ j; j < k⟧ ⟹ i < k"
done

lemma  zless_le_trans:"⟦(i::int) < j; j ≤ k⟧ ⟹ i < k"
done

lemma zmult_pos_bignumTr:"0 < (a::int) ⟹
∃l. ∀m. l < m ⟶ z < x + (int m) * a"
apply (cut_tac zmult_pos_bignumTr0[of "z" "x"])
apply (erule exE)
apply (subgoal_tac "∀m. L < m ⟶ z < x + int m * a", blast)
apply (rule allI, rule impI)
apply (drule_tac a = m in forall_spec, assumption)
apply (subgoal_tac "0 ≤ int m")
apply (frule_tac a = "int m" and b = a in pos_zmult_pos, assumption)
apply (cut_tac order_refl[of "x"])
apply (frule_tac z' = "int m" and z = "int m * a" in
apply (rule_tac y = "x + int m" and z = "x + (int m)* a" in
less_le_trans[of "z"], assumption+)
apply simp
done

lemma  ale_shift:"⟦(x::ant)≤ y; y = z⟧ ⟹ x ≤ z"
by simp

lemma aneg_na_0[simp]:"a < 0 ⟹ na a = 0"

lemma amult_an_an:"an (m * n) = (an m) * (an n)"
done

definition
"x adiv y = ant ((tna x) div (tna y))"

definition
amod :: "[ant, ant] ⇒ ant" (infixl "amod" 200) where
"x amod y = ant ((tna x) mod (tna y))"

lemma apos_amod_conj:"0 < ant b ⟹
0 ≤ (ant a) amod (ant b) ∧ (ant a) amod (ant b) < (ant b)"
by (simp add:amod_def tna_ant, simp only:ant_0[THEN sym],

"(ant a) = (a div b) *⇩a (ant b) + ant (a mod b)"
done

lemma asp_z_Z:"z *⇩a ant x ∈ Z⇩∞"

lemma apos_in_aug_inf:"0 ≤ a ⟹ a ∈ Z⇩∞"
by (simp add:aug_inf_def, rule contrapos_pp, simp+,
cut_tac minf_le_any[of "0"], frule ale_antisym[of "0" "-∞"],
assumption+, simp)

lemma  amult_1_both:"⟦0 < (w::ant); x * w = 1⟧ ⟹ x = 1 ∧ w = 1"
apply (cut_tac mem_ant[of "x"], cut_tac mem_ant[of "w"],
(erule disjE)+, simp,
(frule sym, thin_tac "∞ = 1", simp only:ant_1[THEN sym],
simp del:ant_1))
apply (erule disjE, erule exE, simp,
(frule sym, thin_tac "-∞ = 1", simp only:ant_1[THEN sym],
simp del:ant_1), simp)
apply (frule sym, thin_tac "-∞ = 1", simp only:ant_1[THEN sym],
simp del:ant_1)
apply ((erule disjE)+, erule exE, simp,
frule_tac aless_imp_le[of "0" "-∞"],
cut_tac minf_le_any[of "0"],
frule ale_antisym[of "0" "-∞"], assumption+,
simp only:ant_0[THEN sym], simp,
frule sym, thin_tac "-∞ = 1", simp only:ant_1[THEN sym],
simp del:ant_1)
apply ((erule disjE)+, (erule exE)+, simp only:ant_1[THEN sym],
(cut_tac a = z and b = za in mult.commute, simp,
cut_tac z = za and z' = z in  times_1_both, assumption+),
simp)
apply (erule exE, simp,
cut_tac x = z and y = 0 in less_linear, erule disjE, simp,
frule sym, thin_tac "-∞ = 1", simp only:ant_1[THEN sym],
simp del:ant_1,
frule sym, thin_tac "∞ = 1", simp only:ant_1[THEN sym],
simp del:ant_1,
erule disjE, erule exE, simp,
frule sym, thin_tac "∞ = 1", simp only:ant_1[THEN sym],
simp del:ant_1, simp)
done

lemma poss_int_neq_0:"0 < (z::int) ⟹ z ≠ 0"
by simp

lemma aadd_neg_negg[simp]:"⟦a ≤ (0::ant); b < 0⟧ ⟹ a + b < 0"
apply (frule ale_minus[of "a" "0"], simp,
frule aless_minus[of "b" "0"], simp)
apply (frule aadd_pos_poss[of "-a" "-b"], assumption+,
frule aless_minus[of "0" "-(a + b)"], simp add:a_minus_minus)
done

lemma aadd_two_negg[simp]:"⟦a < (0::ant); b < 0⟧ ⟹ a + b < 0"
by auto

lemma amin_aminTr:"(z::ant) ≤ z' ⟹ amin z w ≤ amin z' w"

lemma amin_le1:"(z::ant) ≤ z' ⟹ (amin z w) ≤ z'"
rule impI, frule aless_le_trans[of "w" "z" "z'"],

lemma amin_le2:"(z::ant) ≤ z' ⟹ (amin w z) ≤ z'"
frule ale_trans[of "w" "z" "z'"], assumption+)

lemma  Amin_geTr:"(∀j ≤ n. f j ∈ Z⇩∞) ∧ (∀j ≤ n. z ≤ (f j)) ⟶
z ≤ (Amin n f)"
apply (induct_tac n)
apply (rule impI, erule conjE, simp)
apply (rule impI, (erule conjE)+,
cut_tac Nsetn_sub_mem1[of n], simp,
drule_tac x = "Suc n" in spec, simp,
rule_tac z = z and x = "Amin n f" and y = "f(Suc n)" in amin_ge1,
simp+)
done

lemma Amin_ge:"⟦∀j ≤ n. f j ∈ Z⇩∞; ∀j ≤ n. z ≤ (f j)⟧ ⟹
z ≤ (Amin n f)"

definition
Abs :: "ant ⇒ ant" where
"Abs z = (if z < 0 then -z else z)"

lemma Abs_pos:"0 ≤ Abs z"
by (simp add:Abs_def, rule conjI, rule impI,
cut_tac aless_minus[of "z" "0"], simp,
assumption,
rule impI, simp add:aneg_less[of "z" "0"])

lemma Abs_x_plus_x_pos:"0 ≤ (Abs x) + x"
apply (case_tac "x < 0",

done

lemma  Abs_ge_self:"x ≤ Abs x"
cut_tac ale_minus[of "x" "0"],
done

lemma  na_1:"na 1 = Suc 0"
apply (simp only:ant_1[THEN sym], simp only:na_def,
simp only:ant_0[THEN sym], simp only:aless_zless[of "1" "0"],
simp, subgoal_tac "∞ ≠ 1", simp)
apply (simp only:ant_1[THEN sym], simp only:tna_ant,
rule not_sym, simp only:ant_1[THEN sym], simp del:ant_1)
done

lemma ant_int:"ant (int n) = an n"

lemma int_nat:"0 < z ⟹ int (nat z) = z"
by arith

lemma int_ex_nat:"0 < z ⟹ ∃n. int n = z"
by (cut_tac int_nat[of z], blast, assumption)

lemma eq_nat_pos_ints:
"⟦nat (z::int) = nat (z'::int); 0 ≤ z; 0 ≤ z'⟧ ⟹ z = z'"
by simp

lemma a_p1_gt[simp]:"⟦a ≠ ∞; a ≠ -∞⟧  ⟹ a < a + 1"
apply (cut_tac zposs_aposss[of 1], simp)
done

lemma  gt_na_poss:"(na a) < m ⟹ 0 < m"
done

lemma azmult_less:"⟦a ≠ ∞; na a < m; 0 < x⟧
⟹ a < int m *⇩a x"
apply (cut_tac mem_ant[of "a"])
apply (erule disjE)
apply (case_tac "x = ∞") apply simp
apply (subst less_le[of "-∞" "∞"]) apply simp
apply (frule aless_imp_le[of "0" "x"], frule apos_neq_minf[of "x"])
apply (cut_tac mem_ant[of "x"], simp, erule exE, simp)
apply (simp, erule exE, simp)

apply (frule_tac a = "ant z" in gt_na_poss[of _ "m"])
apply (case_tac "x = ∞", simp)
apply (frule aless_imp_le[of "0" "x"])
apply (frule apos_neq_minf[of "x"])
apply (cut_tac mem_ant[of "x"], simp, erule exE,
apply (subst aless_zless)
apply (cut_tac a = "ant z" in gt_na_poss[of _ "m"], assumption)
apply (smt a0_less_int_conv aposs_na_poss int_less_mono int_nat na_def of_nat_0_le_iff pos_zmult_pos tna_ant z_neq_inf)
done

lemma  zmult_gt_one:"⟦2 ≤ m; 0 < xa⟧ ⟹ 1 < int m * xa"
by (metis ge2_zmult_pos mult.commute)

lemma zmult_pos:"⟦ 0 < m; 0 < (a::int)⟧ ⟹ 0 < (int m) * a"
by (frule zmult_zless_mono2[of "0" "a" "int m"], simp, simp)

lemma  ant_int_na:"⟦0 ≤ a; a ≠ ∞ ⟧ ⟹ ant (int (na a)) = a"
by (frule an_na[of "a"], assumption, simp add:an_def)

lemma zpos_nat:"0 ≤ (z::int) ⟹ ∃n. z = int n"
apply (subgoal_tac "z = int (nat z)")
apply blast apply simp
done

section "nsets"

lemma nsetTr1:"⟦j ∈ nset a b; j ≠ a⟧ ⟹ j ∈ nset (Suc a) b"
done

lemma nsetTr2:"j ∈ nset (Suc a) (Suc b) ⟹ j - Suc 0 ∈ nset a b"
done

lemma  nsetTr3:"⟦j ≠ Suc (Suc 0); j - Suc 0 ∈ nset (Suc 0) (Suc n)⟧
⟹  Suc 0 < j - Suc 0"
apply (simp add:nset_def, erule conjE, subgoal_tac "j ≠ 0",
rule contrapos_pp, simp+)
done

lemma Suc_leD1:"Suc m ≤ n ⟹ m < n"
apply (insert lessI[of "m"],
rule less_le_trans[of "m" "Suc m" "n"], assumption+)
done

lemma leI1:"n < m ⟹ ¬ ((m::nat) ≤ n)"
apply (rule contrapos_pp, simp+)
done

lemma neg_zle:"¬ (z::int) ≤ z' ⟹ z' < z"
done

lemma nset_m_m:"nset m m = {m}"
rule equalityI, rule subsetI, simp,
rule subsetI, simp)

lemma nset_Tr51:"⟦j ∈ nset (Suc 0) (Suc (Suc n)); j ≠ Suc 0⟧
⟹ j - Suc 0 ∈ nset (Suc 0) (Suc n)"
frule_tac m = j and n = "Suc (Suc n)" and l = "Suc 0" in diff_le_mono,
simp)
done

lemma nset_Tr52:"⟦j ≠ Suc (Suc 0); Suc 0 ≤ j - Suc 0⟧
⟹ ¬ j - Suc 0 ≤ Suc 0"
by auto

lemma nset_Suc:"nset (Suc 0) (Suc (Suc n)) =
nset (Suc 0) (Suc n) ∪ {Suc (Suc n)}"

lemma AinequalityTr0:"x ≠ -∞ ⟹ ∃L. (∀N. L < N ⟶
(an m) < (x + an N))"
apply (case_tac "x = ∞", simp add:an_def)
apply (cut_tac mem_ant[of "x"], simp, erule exE, simp add:an_def a_zpz,
cut_tac x = z in zmult_pos_bignumTr0[of "int m"], simp)
done

lemma AinequalityTr:"⟦0 < b ∧ b ≠ ∞; x ≠ -∞⟧ ⟹ ∃L. (∀N. L < N ⟶
(an m) < (x + (int N) *⇩a b))"
apply (frule_tac AinequalityTr0[of "x" "m"],
erule exE,
subgoal_tac "∀N. L < N ⟶ an m < x + (int N) *⇩a b",
blast, rule allI, rule impI)
apply (drule_tac a = N in forall_spec, assumption,
erule conjE,
cut_tac N = N in asprod_ge[of "b"], assumption,
thin_tac "x ≠ - ∞", thin_tac "b ≠ ∞", thin_tac "an m < x + an N",
simp)
apply (frule_tac x = "an N" and y = "int N *⇩a b" and z = x in aadd_le_mono,
done

lemma two_inequalities:"⟦∀(n::nat). x < n ⟶ P n; ∀(n::nat). y < n ⟶ Q n⟧
⟹  ∀n. (max x y) < n ⟶ (P n) ∧ (Q n)"
by auto

lemma multi_inequalityTr0:"(∀j ≤ (n::nat). (x j) ≠ -∞ ) ⟶
(∃L. (∀N. L < N ⟶  (∀l ≤ n. (an m) < (x l) + (an N))))"
apply (induct_tac n)
apply (rule impI, simp)
apply (rule AinequalityTr0[of "x 0" "m"], assumption)
(** n **)
apply (rule impI)
apply (subgoal_tac "∀l. l ≤ n ⟶ l ≤ (Suc n)", simp)
apply (erule exE)
apply (frule_tac a = "Suc n" in forall_spec, simp)

apply (frule_tac x = "x (Suc n)" in AinequalityTr0[of _ "m"])
apply (erule exE)
apply (subgoal_tac "∀N. (max L La) < N ⟶
(∀l ≤ (Suc n). an m < x l + an N)", blast)
apply (rule allI, rule impI, rule allI, rule impI)
apply (rotate_tac 1)
apply (case_tac "l = Suc n", simp,
drule_tac m = l and n = "Suc n" in noteq_le_less, assumption+,
drule_tac x = l and n = "Suc n" in less_le_diff, simp,
simp)
done

lemma multi_inequalityTr1:"⟦∀j ≤ (n::nat). (x j) ≠ - ∞⟧ ⟹
∃L. (∀N. L < N ⟶  (∀l ≤ n. (an m) < (x l) + (an N)))"

lemma gcoeff_multi_inequality:"⟦∀N. 0 < N ⟶ (∀j ≤ (n::nat). (x j) ≠ -∞ ∧
0 < (b N j) ∧ (b N j) ≠ ∞)⟧ ⟹
∃L. (∀N. L < N ⟶  (∀l ≤ n.(an m) < (x l) + (int N) *⇩a (b N l)))"
apply (subgoal_tac "∀j ≤ n. x j ≠ - ∞")
apply (frule  multi_inequalityTr1[of "n" "x" "m"])
apply (erule exE)
apply (subgoal_tac "∀N. L < N ⟶
(∀l ≤ n. an m < x l + (int N) *⇩a (b N l))")
apply blast

apply (rule allI, rule impI, rule allI, rule impI,
drule_tac a = N in forall_spec, simp,
drule_tac a = l in forall_spec, assumption,
drule_tac a = N in forall_spec, assumption,
drule_tac a = l in forall_spec, assumption,
drule_tac a = l in forall_spec, assumption)
apply (cut_tac b = "b N l" and N = N in asprod_ge, simp, simp,
(erule conjE)+, simp, thin_tac "x l ≠ - ∞", thin_tac "b N l ≠ ∞")
apply (frule_tac x = "an N" and y = "int N *⇩a b N l" and z = "x l" in
rule allI, rule impI,
cut_tac lessI[of "(0::nat)"],
drule_tac a = "Suc 0" in forall_spec, assumption)
apply simp
done

primrec m_max :: "[nat, nat ⇒ nat] ⇒ nat"
where
m_max_0: "m_max 0 f = f 0"
| m_max_Suc: "m_max (Suc n) f  = max (m_max n f) (f (Suc n))"

(** maximum value of f **)

lemma m_maxTr:"∀l ≤ n. (f l) ≤ m_max n f"
apply (induct_tac n)
apply simp

apply (rule allI, rule impI)
apply simp
apply (case_tac "l = Suc n", simp)
apply (cut_tac m = l and n = "Suc n" in noteq_le_less, assumption+,
thin_tac "l ≤ Suc n", thin_tac "l ≠ Suc n",
frule_tac x = l and n = "Suc n" in less_le_diff,
thin_tac "l < Suc n", simp)
apply (drule_tac a = l in forall_spec, assumption)
apply simp
done

lemma m_max_gt:"l ≤ n ⟹ (f l) ≤ m_max n f"
done

lemma ASum_zero:" (∀j ≤ n. f j ∈ Z⇩∞) ∧ (∀l ≤ n. f l = 0) ⟶ ASum f n = 0"
apply (induct_tac n)
apply (rule impI, erule conjE, simp)
apply (rule impI)
apply (subgoal_tac "(∀j≤n. f j ∈ Z⇩∞) ∧ (∀l≤n. f l = 0)", simp)
thin_tac "(∀j≤n. f j ∈ Z⇩∞) ∧ (∀l≤n. f l = 0) ⟶ ASum f n = 0")
apply (rule conjI)
apply (rule allI, rule impI,
drule_tac a = j in forall_spec, simp, assumption+)
apply (thin_tac "∀j≤Suc n. f j ∈ Z⇩∞")
apply (rule allI, rule impI,
drule_tac a = l in forall_spec, simp+)
done

lemma eSum_singleTr:"(∀j ≤ n. f j ∈ Z⇩∞) ∧ (j ≤ n ∧ (∀l ∈{h. h ≤ n} - {j}. f l = 0))  ⟶ ASum f n = f j"
apply (induct_tac n)
apply (simp, rule impI, (erule conjE)+)
apply (case_tac "j ≤ n")
apply simp
apply simp
apply (frule_tac m = n and n = j in Suc_leI)
apply (frule_tac m = j and n = "Suc n" in le_antisym, assumption+, simp)
apply (cut_tac n = n in ASum_zero [of _ "f"])
apply (subgoal_tac "(∀j≤n. f j ∈ Z⇩∞) ∧ (∀l≤n. f l = 0)")
apply (thin_tac "∀j≤Suc n. f j ∈ Z⇩∞",
thin_tac "∀l∈{h. h ≤ Suc n} - {Suc n}. f l = 0", simp only:mp)

apply (thin_tac "(∀j≤n. f j ∈ Z⇩∞) ∧ (∀l≤n. f l = 0) ⟶ ASum f n = 0")
apply (rule conjI,
thin_tac "∀l∈{h. h ≤ Suc n} - {Suc n}. f l = 0", simp)
apply (thin_tac "∀j≤Suc n. f j ∈ Z⇩∞", simp)
done

lemma eSum_single:"⟦∀j ≤ n. f j ∈ Z⇩∞ ; j ≤ n; ∀l ∈ {h. h ≤ n} - {j}. f l = 0⟧
⟹ ASum  f n = f j"
done

lemma ASum_eqTr:"(∀j ≤ n. f j ∈ Z⇩∞) ∧ (∀j ≤ n. g j ∈ Z⇩∞) ∧
(∀j ≤ n. f j = g j) ⟶ ASum f n = ASum g n"
apply (induct_tac n)
apply (rule impI, simp)

apply (rule impI, (erule conjE)+)
apply simp
done

lemma ASum_eq:"⟦∀j ≤ n. f j ∈ Z⇩∞; ∀j ≤ n. g j ∈ Z⇩∞; ∀j ≤ n. f j = g j⟧ ⟹
ASum f n = ASum g n"
by (cut_tac ASum_eqTr[of n f g], simp)

definition
Kronecker_delta :: "[nat, nat] ⇒ ant"
("(δ⇘_ _⇙)" [70,71]70) where
"δ⇘i j⇙ = (if i = j then 1 else 0)"

definition
K_gamma :: "[nat, nat] ⇒ int"
("(γ⇘_ _⇙)" [70,71]70) where
"γ⇘i j⇙ = (if i = j then 0 else 1)"

abbreviation
TRANSPOS  ("(τ⇘_ _⇙)" [90,91]90) where
"τ⇘i j⇙ == transpos i j"

lemma Kdelta_in_Zinf:"⟦j ≤ (Suc n); k ≤ (Suc n)⟧  ⟹
z *⇩a (δ⇘j k⇙) ∈ Z⇩∞"
done

lemma Kdelta_in_Zinf1:"⟦j ≤ n; k ≤ n⟧  ⟹ δ⇘j k⇙ ∈ Z⇩∞"
apply (rule impI)
apply (simp only:ant_1[THEN sym], simp del:ant_1 add:z_in_aug_inf)
done

primrec m_zmax :: "[nat, nat ⇒ int] ⇒ int"
where
m_zmax_0: "m_zmax 0 f = f 0"
| m_zmax_Suc: "m_zmax (Suc n) f = zmax (m_zmax n f) (f (Suc n))"

lemma m_zmax_gt_eachTr:
"(∀j ≤ n. f j ∈ Zset) ⟶ (∀j ≤ n. (f j) ≤ m_zmax n f)"
apply (induct_tac n)
apply (rule impI, rule allI, rule impI, simp)
apply (rule impI)
apply simp
apply (rule allI, rule impI)
apply (case_tac "j = Suc n", simp)
apply (drule_tac m = j and n = "Suc n" in noteq_le_less, assumption,
drule_tac x = j and n = "Suc n" in less_le_diff, simp)
apply (drule_tac a = j in forall_spec, assumption)
done

lemma m_zmax_gt_each:"(∀j ≤ n. f j ∈ Zset) ⟹ (∀j ≤ n. (f j) ≤ m_zmax n f)"
done

lemma n_notin_Nset_pred:" 0 < n ⟹ ¬ n ≤ (n - Suc 0)"
apply simp
done

lemma Nset_preTr:"⟦0 < n; j ≤ (n - Suc 0)⟧ ⟹ j ≤ n"
apply simp
done

lemma Nset_preTr1:"⟦0 < n; j ≤ (n - Suc 0)⟧ ⟹ j ≠ n"
apply simp
done

lemma transpos_noteqTr:"⟦0 < n; k ≤ (n - Suc 0); j ≤ n; j ≠ n⟧
⟹ j ≠ (τ⇘j n⇙) k"
apply (rule contrapos_pp, simp+)
apply (case_tac "k = j", simp, simp)
apply (case_tac "k = n", simp)
done

chapter "Elementary properties of a valuation"

section "Definition of a valuation"

definition
valuation :: "[('b, 'm) Ring_scheme, 'b ⇒ ant] ⇒ bool" where
"valuation K v ⟷
v ∈ extensional (carrier K) ∧
v ∈ carrier K → Z⇩∞  ∧
v (𝟬⇘K⇙) = ∞ ∧ (∀x∈((carrier K) - {𝟬⇘K⇙}). v x ≠ ∞) ∧
(∀x∈(carrier K). ∀y∈(carrier K). v (x ⋅⇩r⇘K⇙ y) = (v x) + (v y)) ∧
(∀x∈(carrier K). 0 ≤ (v x) ⟶ 0 ≤ (v (1⇩r⇘K⇙ ±⇘K⇙ x))) ∧
(∃x. x ∈ carrier K ∧ (v x) ≠ ∞ ∧ (v x) ≠ 0)"

lemma (in Corps) invf_closed:"x ∈ carrier K - {𝟬} ⟹ x⇗‐ K⇖ ∈ carrier K"
by (cut_tac invf_closed1[of x], simp, assumption)

lemma (in Corps) valuation_map:"valuation K v ⟹ v ∈ carrier K → Z⇩∞"

lemma (in Corps) value_in_aug_inf:"⟦valuation K v; x ∈ carrier K⟧ ⟹
v x ∈ Z⇩∞"

lemma (in Corps) value_of_zero:"valuation K v  ⟹ v (𝟬) = ∞"

lemma (in Corps) val_nonzero_noninf:"⟦valuation K v; x ∈ carrier K; x ≠ 𝟬⟧
⟹ (v x) ≠ ∞"

lemma (in Corps) value_inf_zero:"⟦valuation K v; x ∈ carrier K; v x = ∞⟧
⟹ x = 𝟬"
by (rule contrapos_pp, simp+,
frule val_nonzero_noninf[of v x], assumption+, simp)

lemma (in Corps) val_nonzero_z:"⟦valuation K v; x ∈ carrier K; x ≠ 𝟬⟧ ⟹
∃z. (v x) = ant z"
by (frule value_in_aug_inf[of v x], assumption+,
frule val_nonzero_noninf[of v x], assumption+,
cut_tac mem_ant[of "v x"],  simp add:aug_inf_def)

lemma (in Corps) val_nonzero_z_unique:"⟦valuation K v; x ∈ carrier K; x ≠ 𝟬⟧
⟹ ∃!z. (v x) = ant z"
by (rule ex_ex1I, simp add:val_nonzero_z, simp)

lemma (in Corps) value_noninf_nonzero:"⟦valuation K v; x ∈ carrier K; v x ≠ ∞⟧
⟹ x ≠ 𝟬"
by (rule contrapos_pp, simp+, simp add:value_of_zero)

lemma (in Corps) val1_neq_0:"⟦valuation K v; x ∈ carrier K; v x = 1⟧ ⟹
x ≠ 𝟬"
apply (rule contrapos_pp, simp+, simp add:value_of_zero)
apply (simp only:ant_1[THEN sym], cut_tac z_neq_inf[THEN not_sym, of 1], simp)
done

lemma (in Corps) val_Zmin_sym:"⟦valuation K v; x ∈ carrier K; y ∈ carrier K⟧
⟹  amin (v x) (v y) = amin (v y ) (v x)"

lemma (in Corps) val_t2p:"⟦valuation K v; x ∈ carrier K; y ∈ carrier K⟧
⟹ v (x ⋅⇩r y ) = v x + v y"

lemma (in Corps) val_axiom4:"⟦valuation K v; x ∈ carrier K; 0 ≤ v x⟧ ⟹
0 ≤ v (1⇩r ± x)"

lemma (in Corps) val_axiom5:"valuation K v ⟹
∃x. x ∈ carrier K ∧ v x ≠ ∞ ∧ v x ≠ 0"

lemma (in Corps) val_field_nonzero:"valuation K v ⟹ carrier K ≠ {𝟬}"
by (rule contrapos_pp, simp+,
frule val_axiom5[of v],
erule exE, (erule conjE)+, simp add:value_of_zero)

lemma (in Corps) val_field_1_neq_0:"valuation K v ⟹ 1⇩r ≠ 𝟬"
apply (rule contrapos_pp, simp+)
apply (frule val_axiom5[of v])
apply (erule exE, (erule conjE)+)
apply (cut_tac field_is_ring,
frule_tac t = x in  Ring.ring_l_one[THEN sym, of "K"], assumption+,
done

lemma (in Corps) value_of_one:"valuation K v ⟹ v (1⇩r) = 0"
apply (cut_tac field_is_ring, frule Ring.ring_one[of "K"])
apply (frule val_t2p[of v "1⇩r" "1⇩r"], assumption+,
frule val_nonzero_z[of v "1⇩r"], assumption+,
done

lemma (in Corps) has_val_one_neq_zero:"valuation K v ⟹ 1⇩r ≠ 𝟬"
by (frule value_of_one[of "v"],

lemma (in Corps) val_minus_one:"valuation K v ⟹ v (-⇩a 1⇩r) = 0"
apply (cut_tac field_is_ring, frule Ring.ring_one[of "K"],
frule Ring.ring_is_ag[of "K"],
frule val_field_1_neq_0[of v],
frule aGroup.ag_inv_inj[of "K" "1⇩r" "𝟬"], assumption+,
apply (frule val_nonzero_z[of v "-⇩a 1⇩r"],
erule exE, frule val_t2p [THEN sym, of v "-⇩a 1⇩r" "-⇩a 1⇩r"])
frule Ring.ring_inv1_3[THEN sym, of "K" "1⇩r" "1⇩r"], assumption+,
done

lemma (in Corps) val_minus_eq:"⟦valuation K v; x ∈ carrier K⟧ ⟹
v (-⇩a x) = v x"
apply (cut_tac field_is_ring,
subst val_t2p[of v], assumption+,
frule Ring.ring_is_ag[of "K"], rule aGroup.ag_mOp_closed, assumption+,
done

lemma (in Corps) value_of_inv:"⟦valuation K v; x ∈ carrier K; x ≠ 𝟬⟧ ⟹
v (x⇗‐K⇖) = - (v x)"
apply (cut_tac invf_inv[of x], erule conjE,
frule val_t2p[of v "x⇗‐K⇖" x], assumption+,
apply simp
done

lemma (in Corps) val_exp_ring:"⟦ valuation K v; x ∈ carrier K; x ≠ 𝟬⟧
⟹ (int n) *⇩a (v x) = v (x^⇗K n⇖)"
apply (cut_tac field_is_ring,
apply (drule sym, simp)
apply (subst val_t2p[of v _ x], assumption+,
rule Ring.npClose, assumption+,
frule val_nonzero_z[of v x], assumption+,
done

text‹exponent in a field›
lemma (in Corps) val_exp:"⟦ valuation K v; x ∈ carrier K; x ≠ 𝟬⟧ ⟹
z *⇩a (v x) = v (x⇘K⇙⇗z⇖)"
apply (case_tac "0 ≤ z",
simp, frule val_exp_ring [of v x "nat z"], assumption+,
simp, simp)
cut_tac invf_closed1[of x], simp,
cut_tac  val_exp_ring [THEN sym, of v "x⇗‐ K⇖" "nat (- z)"], simp,
thin_tac "v (x⇗‐ K⇖^⇗K (nat (- z))⇖) = (- z) *⇩a v (x⇗‐ K⇖)", erule conjE)
apply (subst value_of_inv[of v x], assumption+)
apply (frule val_nonzero_z[of v x], assumption+, erule exE, simp,
done

lemma (in Corps) value_zero_nonzero:"⟦valuation K v; x ∈ carrier K; v x = 0⟧
⟹ x ≠ 𝟬"
by (frule value_noninf_nonzero[of v x], assumption+, simp,
assumption)

lemma (in Corps) v_ale_diff:"⟦valuation K v; x ∈ carrier K; y ∈ carrier K;
x ≠ 𝟬; v x ≤ v y ⟧ ⟹ 0 ≤ v(y ⋅⇩r x⇗‐ K⇖)"
apply (frule value_in_aug_inf[of v x], simp+,
frule value_in_aug_inf[of v y], simp+,
frule val_nonzero_z[of v x], assumption+,
erule exE)
apply (cut_tac invf_closed[of x], simp+,
frule_tac x = "ant z" in ale_diff_pos[of _ "v y"],
apply simp
done

lemma (in Corps) amin_le_plusTr:"⟦valuation K v; x ∈ carrier K; y ∈ carrier K;
v x ≠ ∞; v y ≠ ∞; v x ≤ v y⟧ ⟹ amin (v x) (v y) ≤ v ( x ± y)"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag,
frule value_noninf_nonzero[of v x], assumption+,
frule v_ale_diff[of v x y], assumption+,
cut_tac invf_closed1[of x],
frule Ring.ring_tOp_closed[of K y "x⇗‐ K⇖"], assumption+, simp,
frule Ring.ring_one[of "K"],
frule aGroup.ag_pOp_closed[of "K" "1⇩r" "y ⋅⇩r x⇗‐ K⇖"], assumption+,
frule val_axiom4[of v "y ⋅⇩r ( x⇗‐ K⇖)"], assumption+)
apply (frule aadd_le_mono[of "0" "v (1⇩r ± y ⋅⇩r x⇗‐ K⇖)" "v x"],
simp add:val_t2p[THEN sym, of v x],
cut_tac amin_le_l[of "v x" "v y"],
rule ale_trans[of "amin (v x) (v y)" "v x" "v (x ± y)"], assumption+)
apply simp
done

lemma (in Corps) amin_le_plus:"⟦valuation K v; x ∈ carrier K; y ∈ carrier K⟧
⟹ (amin (v x) (v y)) ≤ (v (x ± y))"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag)
apply (case_tac "v x = ∞ ∨ v y = ∞")
apply (erule disjE, simp,
frule value_inf_zero[of v x], assumption+,
frule value_inf_zero[of v y], assumption+,
simp add:aGroup.ag_r_zero amin_def, simp, erule conjE)
apply (cut_tac z = "v x" and w = "v y" in ale_linear,
frule_tac amin_le_plusTr[of v y x], assumption+,
done

lemma (in Corps) value_less_eq:"⟦ valuation K v; x ∈ carrier K; y ∈ carrier K;
(v x) < (v y)⟧ ⟹ (v x) = (v (x ± y))"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
frule amin_le_plus[of v x y], assumption+,
frule aless_imp_le[of "v x" "v y"],
apply (frule amin_le_plus[of v "x ± y" "-⇩a y"],
rule aGroup.ag_pOp_closed, assumption+,
rule aGroup.ag_mOp_closed, assumption+,
frule aGroup.ag_mOp_closed[of "K" "y"], assumption+,
apply (case_tac "¬ (v (x ±⇘K⇙ y) ≤ (v y))", simp+)
done

lemma (in Corps) value_less_eq1:"⟦valuation K v; x ∈ carrier K; y ∈ carrier K;
(v x) < (v y)⟧ ⟹ v x =  v (y ± x)"
apply (cut_tac field_is_ring,
frule Ring.ring_is_ag[of "K"],
frule value_less_eq[of v x y], assumption+)
apply (subst aGroup.ag_pOp_commute, assumption+)
done

lemma (in Corps) val_1px:"⟦valuation K v; x ∈ carrier K; 0 ≤ (v (1⇩r ± x))⟧
⟹ 0 ≤ (v x)"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
frule Ring.ring_one[of "K"])
apply (rule contrapos_pp, simp+,
case_tac "x = 𝟬⇘K⇙",
simp add: aneg_le[of "0" "v x"],
frule value_less_eq[of v x "1⇩r"], assumption+,
apply (drule sym,
done

lemma (in Corps) val_1mx:"⟦valuation K v; x ∈ carrier K;
0 ≤ (v (1⇩r ± (-⇩a x)))⟧ ⟹ 0 ≤ (v x)"
by (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
frule val_1px[of v "-⇩a x"],

section "The normal valuation of v"

definition
Lv :: "[('r, 'm) Ring_scheme , 'r ⇒ ant] ⇒ ant" (* Least nonnegative value *) where
"Lv K v = AMin {x. x ∈ v ` carrier K ∧ 0 < x}"

definition
n_val :: "[('r, 'm) Ring_scheme, 'r ⇒ ant] ⇒ ('r ⇒ ant)" where
"n_val K v = (λx∈ carrier K.  (THE l. (l * (Lv K v)) = v x))"
(* normal valuation *)

definition
Pg :: "[('r, 'm) Ring_scheme, 'r ⇒ ant] ⇒ 'r" (* Positive generator *) where
"Pg K v = (SOME x. x ∈ carrier K - {𝟬⇘K⇙} ∧ v x = Lv K v)"

lemma (in Corps) vals_pos_nonempty:"valuation K v ⟹
{x. x ∈ v ` carrier K ∧ 0 < x} ≠ {}"
using val_axiom5[of v] value_noninf_nonzero[of v] value_of_inv[THEN sym, of v]
by (auto simp: ex_image_cong_iff) (metis Ring.ring_is_ag aGroup.ag_mOp_closed aGroup.ag_pOp_closed aGroup.ag_r_inv1 f_is_ring zero_lt_inf)

lemma (in Corps) vals_pos_LBset:"valuation K v ⟹
{x. x ∈ v ` carrier K ∧ 0 < x} ⊆ LBset 1"
by (rule subsetI, simp add:LBset_def, erule conjE,
rule_tac x = x in gt_a0_ge_1, assumption)

lemma (in Corps) Lv_pos:"valuation K v ⟹ 0 < Lv K v"
frule vals_pos_nonempty[of v],
frule vals_pos_LBset[of v],
simp only:ant_1[THEN sym],
frule AMin[of "{x. x ∈ v ` carrier K ∧ 0 < x}" "1"], assumption+,
erule conjE)
apply simp
done

lemma (in Corps) AMin_z:"valuation K v ⟹
∃a. AMin {x. x ∈ v ` carrier K ∧ 0 < x} = ant a"
apply (frule vals_pos_nonempty[of v],
frule vals_pos_LBset[of v],
simp only:ant_1[THEN sym],
frule AMin[of "{x. x ∈ v ` carrier K ∧ 0 < x}" "1"], assumption+,
erule conjE)
apply (frule val_axiom5[of v],
erule exE, (erule conjE)+,
cut_tac x = "v x" in aless_linear[of _ "0"], simp,
erule disjE,
frule_tac x = x in value_noninf_nonzero[of v], assumption+,
frule_tac x1 = x in value_of_inv[THEN sym, of v], assumption+)
apply (frule_tac x = "v x" in aless_minus[of _ "0"], simp,
cut_tac x = x in invf_closed1, simp, erule conjE,
frule valuation_map[of v],
frule_tac a = "x⇗‐ K⇖" in mem_in_image[of "v" "carrier K" "Z⇩∞"], simp)
apply (drule_tac a = "v (x⇗‐ K⇖)" in forall_spec, simp,
frule_tac x = "x⇗‐ K⇖" in val_nonzero_noninf[of v],
thin_tac "v (x⇗‐ K⇖) ∈ v ` carrier K",
thin_tac "{x ∈ v ` carrier K. 0 < x} ⊆ LBset 1",
thin_tac "AMin {x ∈ v ` carrier K. 0 < x} ∈ v ` carrier K",
thin_tac "0 < AMin {x ∈ v ` carrier K. 0 < x}", simp,
thin_tac "v (x⇗‐ K⇖) ∈ v ` carrier K",
thin_tac "{x ∈ v ` carrier K. 0 < x} ⊆ LBset 1",
thin_tac "AMin {x ∈ v ` carrier K. 0 < x} ∈ v ` carrier K",
thin_tac "0 < AMin {x ∈ v ` carrier K. 0 < x}", simp)
apply (rule noninf_mem_Z[of "AMin {x ∈ v ` carrier K. 0 < x}"],
frule image_sub[of v "carrier K" "Z⇩∞" "carrier K"],
rule subset_refl)
apply (rule subsetD[of "v ` carrier K" "Z⇩∞"
"AMin {x ∈ v ` carrier K. 0 < x}"], assumption+)
apply auto
by (metis (no_types, lifting) aneg_le aug_inf_noninf_is_z image_eqI value_in_aug_inf z_less_i)

lemma (in Corps) Lv_z:"valuation K v ⟹ ∃z. Lv K v = ant z"
by (simp add:Lv_def, rule AMin_z, assumption+)

lemma (in Corps) AMin_k:"valuation K v ⟹
∃k∈ carrier K - {𝟬}. AMin {x. x ∈ v ` carrier K ∧ 0 < x} = v k"

apply (frule vals_pos_nonempty[of v],
frule vals_pos_LBset[of v],
simp only:ant_1[THEN sym],
frule AMin[of "{x. x ∈ v ` carrier K ∧ 0 < x}" "1"], assumption+,
erule conjE)
apply (thin_tac "∀x∈{x. x ∈ v ` carrier K ∧ 0 < x}.
AMin {x. x ∈ v ` carrier K ∧ 0 < x} ≤ x")
apply (simp add:image_def, erule conjE, erule bexE,
thin_tac "{x. (∃xa∈carrier K. x = v xa) ∧ 0 < x} ⊆ LBset 1",
thin_tac "∃x. (∃xa∈carrier K. x = v xa) ∧ 0 < x",
subgoal_tac "x ∈ carrier K - {𝟬}", blast,
frule AMin_z[of v],  erule exE, simp)
thin_tac "AMin {x. (∃xa∈carrier K. x = v xa) ∧ 0 < x} = ant a",
rule contrapos_pp, simp+, frule sym, thin_tac "v (𝟬) = ant a",
done

lemma (in Corps) val_Pg:" valuation K v ⟹
Pg K v ∈ carrier K - {𝟬} ∧ v (Pg K v) = Lv K v"
apply (frule AMin_k[of v], unfold Lv_def, unfold Pg_def)
apply (rule someI2_ex)
apply (erule bexE, drule sym, unfold Lv_def, blast)
apply simp
done

lemma (in Corps) amin_generateTr:"valuation K v ⟹
∀w∈carrier K - {𝟬}. ∃z. v w = z *⇩a AMin {x. x ∈ v ` carrier K ∧ 0 < x}"
apply (frule vals_pos_nonempty[of v],
frule vals_pos_LBset[of v],
simp only:ant_1[THEN sym],
frule AMin[of "{x. x ∈ v ` carrier K ∧ 0 < x}" "1"], assumption+,
frule AMin_z[of v], erule exE, simp,
thin_tac "∃x. x ∈ v ` carrier K ∧ 0 < x",
(erule conjE)+, rule ballI, simp, erule conjE,
frule_tac x = w in val_nonzero_noninf[of v], assumption+,
frule_tac x = w in value_in_aug_inf[of v], assumption+,
cut_tac a = "v w" in mem_ant, simp, erule exE,
cut_tac a = z and b = a in amod_adiv_equality)
thin_tac "{x. x ∈ v ` carrier K ∧ 0 < x} ⊆ LBset 1",
thin_tac "v w ≠ ∞", thin_tac "v w ≠ - ∞")

apply (frule AMin_k[of v], erule bexE,
drule sym,
drule sym,
drule sym,
rotate_tac -1, drule sym)

apply (cut_tac z = z in z_in_aug_inf,
cut_tac z = "(z div a)" and x = a in asp_z_Z,
cut_tac z = "z mod a" in z_in_aug_inf,
frule_tac a = "ant z" and b = "(z div a) *⇩a ant a" and
c = "ant (z mod a)" in ant_sol, assumption+,
subst asprod_mult, simp, assumption, simp,
frule_tac x = k and z = "z div a" in val_exp[of v],
(erule conjE)+, assumption, simp, simp,
thin_tac "(z div a) *⇩a v k = v (k⇘K⇙⇗(z div a)⇖)",
erule conjE)
apply (frule_tac x = k and n = "z div a" in field_potent_nonzero1,
assumption+,
frule_tac a = k and n = "z div a" in npowf_mem, assumption,
frule_tac x1 = "k⇘K⇙⇗(z div a)⇖" in value_of_inv[THEN sym, of v], assumption+,
thin_tac "- v (k⇘K⇙⇗(z div a)⇖) = v ((k⇘K⇙⇗(z div a)⇖)⇗‐ K⇖)",
cut_tac x = "k⇘K⇙⇗(z div a)⇖" in invf_closed1, simp,
simp, erule conjE,
frule_tac x1 = w and y1 = "(k⇘K⇙⇗(z div a)⇖)⇗‐ K⇖"  in
val_t2p[THEN sym, of  v], assumption+, simp,
cut_tac field_is_ring,
thin_tac "v w + v ((k⇘K⇙⇗(z div a)⇖)⇗‐ K⇖) = ant (z mod a)",
thin_tac "v (k⇘K⇙⇗(z div a)⇖) + ant (z mod a) = v w",
frule_tac x = w and y = "(k⇘K⇙⇗(z div a)⇖)⇗‐ K⇖" in
Ring.ring_tOp_closed[of "K"], assumption+)
apply (frule valuation_map[of v],
frule_tac a = "w ⋅⇩r (k⇘K⇙⇗(z div a)⇖)⇗‐ K⇖" in mem_in_image[of "v"
"carrier K" "Z⇩∞"], assumption+, simp)
apply (thin_tac "AMin {x. x ∈ v ` carrier K ∧ 0 < x} = v k",
thin_tac "v ∈ carrier K → Z⇩∞",
subgoal_tac "0 < v (w ⋅⇩r (k⇘K⇙⇗(z div a)⇖)⇗‐ K⇖ )",
drule_tac a = "v (w ⋅⇩r (k⇘K⇙⇗(z div a)⇖)⇗‐ K⇖)" in forall_spec,
apply (drule sym, simp)

apply (frule_tac b = a and a = z in Divides.pos_mod_conj, erule conjE,
simp, simp,
frule_tac b = a and a = z in Divides.pos_mod_conj, erule conjE, simp)
done

lemma (in Corps) val_principalTr1:"⟦ valuation K v⟧  ⟹
Lv K v ∈ v ` (carrier K - {𝟬}) ∧
(∀w∈v ` carrier K. ∃a. w = a * Lv K v) ∧ 0 < Lv K v"
apply (rule conjI,
frule val_Pg[of v], erule conjE,
simp add:image_def, frule sym, thin_tac "v (Pg K v) = Lv K v",
erule conjE, blast)
apply (rule conjI,
rule ballI, simp add:image_def, erule bexE)

apply  (
frule_tac x = x in value_in_aug_inf[of v], assumption,
frule sym, thin_tac "w = v x", simp add:aug_inf_def,
cut_tac a = w in mem_ant, simp, erule disjE, erule exE,
frule_tac x = x in value_noninf_nonzero[of v], assumption+,
simp, frule amin_generateTr[of v])
apply (drule_tac x = x in bspec, simp,
erule exE,
frule AMin_z[of v], erule exE, simp add:Lv_def,
simp add:asprod_mult, frule sym, thin_tac "za * a = z",
simp, subst a_z_z[THEN sym], blast)

frule AMin_z[of v], erule exE, simp,
frule_tac m1 = a in a_i_pos[THEN sym], blast,
done

lemma (in Corps) val_principalTr2:"⟦valuation K v;
c ∈ v ` (carrier K - {𝟬}) ∧ (∀w∈v ` carrier K. ∃a. w = a * c) ∧ 0 < c;
d ∈ v ` (carrier K - {𝟬}) ∧ (∀w∈v ` carrier K. ∃a. w = a * d) ∧ 0 < d⟧
⟹ c = d"
apply ((erule conjE)+,
drule_tac x = d in bspec,
drule_tac x = c in bspec,

apply ((erule exE)+,
drule sym, simp,
(erule conjE)+,
frule_tac x = x in val_nonzero_z[of v], assumption+, erule exE,
frule_tac x = xa in val_nonzero_z[of v], assumption+, erule exE,
simp) apply (
subgoal_tac "a ≠ ∞ ∧ a ≠ -∞", subgoal_tac "aa ≠ ∞ ∧ aa ≠ -∞",
cut_tac a = a in mem_ant, cut_tac a = aa in mem_ant, simp,
thin_tac "c = ant z", frule sym, thin_tac "zb * z = za", simp)
apply (subgoal_tac "0 < zb",
cut_tac a = zc and b = zb in mult.commute, simp,
rule contrapos_pp, simp+,
cut_tac x = 0 and y = zb in less_linear, simp,
thin_tac "¬ 0 < zb",
erule disjE, simp,
frule_tac i = 0 and j = z and k = zb in zmult_zless_mono_neg,
apply (rule contrapos_pp, simp+, thin_tac "a ≠ ∞ ∧ a ≠ - ∞",
erule disjE, simp, rotate_tac 5, drule sym,
simp, simp, rotate_tac 5, drule sym, simp)
apply (rule contrapos_pp, simp+,
erule disjE, simp, rotate_tac 4,
drule sym, simp, simp,
rotate_tac 4, drule sym,
simp)
done

lemma (in Corps) val_principal:"valuation K v ⟹
∃!x0. x0 ∈ v ` (carrier K - {𝟬}) ∧
(∀w ∈ v ` (carrier K). ∃(a::ant). w = a * x0) ∧ 0 < x0"
by (rule ex_ex1I,
frule val_principalTr1[of v], blast,
rule_tac c = x0 and d = y in val_principalTr2[of v],
assumption+)

lemma (in Corps) n_val_defTr:"⟦valuation K v; w ∈ carrier K⟧ ⟹
∃!a. a * Lv K v = v w"
apply (rule ex_ex1I,
frule AMin_k[of v],
erule bexE,
frule_tac x = k in val_nonzero_z[of v], simp, simp,
erule exE, simp, (erule conjE)+)
apply (case_tac "w = 𝟬⇘K⇙", simp add:value_of_zero,
frule_tac m = z in a_i_pos, blast)
apply (frule amin_generateTr[of v],
drule_tac x = w in bspec, simp, simp)
apply (
subst a_z_z[THEN sym], blast)
apply (frule AMin_k[of v]) apply (erule bexE,
frule Lv_pos[of v], simp add:Lv_def) apply (
erule conjE,
frule_tac x = k in val_nonzero_z[of v], assumption+,
erule exE, simp) apply (
case_tac "w = 𝟬⇘K⇙", simp del:a_i_pos add:value_of_zero,
subgoal_tac "y = ∞", simp, rule contrapos_pp, simp+,
cut_tac a = a in mem_ant, simp,
erule disjE, simp, erule exE, simp add:a_z_z)
apply (rule contrapos_pp, simp+,
cut_tac a = y in mem_ant, simp, erule disjE, simp,
frule_tac x = w in val_nonzero_z[of v], assumption+,
erule exE, simp, cut_tac a = a in mem_ant,
erule disjE, simp, frule sym, thin_tac "- ∞ = ant za", simp,
erule disjE, erule exE, simp add:a_z_z)
apply (cut_tac a = y in mem_ant,
erule disjE, simp, rotate_tac 3, drule sym,
simp, erule disjE, erule exE, simp add:a_z_z, frule sym,
thin_tac "zb * z = za", simp, simp,
rotate_tac 3, drule sym,
simp, simp, frule sym, thin_tac "∞ = ant za", simp)
done

lemma (in Corps) n_valTr:"⟦ valuation K v; x ∈ carrier K⟧  ⟹
(THE l. (l * (Lv K v)) = v x)*(Lv K v) = v x"
by (rule theI', rule n_val_defTr, assumption+)

lemma (in Corps) n_val:"⟦valuation K v; x ∈ carrier K⟧  ⟹
(n_val K v x)*(Lv K v) = v x"
by (frule n_valTr[of v x], assumption+, simp add:n_val_def)

lemma (in Corps) val_pos_n_val_pos:"⟦valuation K v; x ∈ carrier K⟧  ⟹
(0 ≤ v x) = (0 ≤ n_val K v x)"
apply (frule n_val[of v x], assumption+,
drule sym,
frule Lv_pos[of v],
frule Lv_z[of v], erule exE, simp)
apply (frule_tac w = z and x = 0 and y = "n_val K v x" in amult_pos_mono_r,
done

lemma (in Corps) n_val_in_aug_inf:"⟦valuation K v; x ∈ carrier K⟧ ⟹
n_val K v x ∈ Z⇩∞"
apply (cut_tac field_is_ring, frule Ring.ring_zero[of "K"],
frule Lv_pos[of v],
frule Lv_z[of v], erule exE,
apply (rule contrapos_pp, simp+)
apply (case_tac "x = 𝟬⇘K⇙", simp,
frule n_val[of v "𝟬"],

apply (frule n_val[of v x], simp,
frule val_nonzero_z[of v x], assumption+,
erule exE, simp, rotate_tac -2, drule sym,
simp)
done

lemma (in Corps) n_val_0:"⟦valuation K v; x ∈ carrier K; v x = 0⟧
⟹  n_val K v x = 0"
by (frule Lv_z[of v], erule exE,
frule Lv_pos[of v],
frule n_val[of v x], simp, simp,
rule_tac z = z and a = "n_val K v x" in a_a_z_0, assumption+)

lemma (in Corps) value_n0_n_val_n0:"⟦valuation K v; x ∈ carrier K; v x ≠ 0⟧ ⟹
n_val K v x ≠ 0"
apply (frule n_val[of v x],
rule contrapos_pp, simp+, frule Lv_z[of v],
erule exE, simp, simp only:ant_0[THEN sym])
apply (rule contrapos_pp, simp+,
done

lemma (in Corps) val_0_n_val_0:"⟦valuation K v; x ∈ carrier K⟧ ⟹
(v x = 0) = (n_val K v x = 0)"
apply (rule iffI,
apply (rule contrapos_pp, simp+,
frule value_n0_n_val_n0[of v x], assumption+)
apply simp
done

lemma (in Corps) val_noninf_n_val_noninf:"⟦valuation K v; x ∈ carrier K⟧ ⟹
(v x ≠ ∞) = (n_val K v x ≠ ∞)"
by (frule Lv_z[of v], erule exE,
frule Lv_pos[of v], simp,
frule n_val[THEN sym, of v x],simp, simp,
thin_tac "v x = n_val K v x * ant z",
rule iffI, rule contrapos_pp, simp+,
cut_tac mem_ant[of "n_val K v x"], erule disjE, simp,
erule disjE, erule exE, simp add:a_z_z, simp, simp)

lemma (in Corps) val_inf_n_val_inf:"⟦valuation K v; x ∈ carrier K⟧ ⟹
(v x = ∞) = (n_val K v x = ∞)"
by (cut_tac val_noninf_n_val_noninf[of v x], simp, assumption+)

lemma (in Corps) val_eq_n_val_eq:"⟦valuation K v; x ∈ carrier K; y ∈ carrier K⟧
⟹  (v x = v y) = (n_val K v x = n_val K v y)"
apply (subst n_val[THEN sym, of v x], assumption+,
subst n_val[THEN sym, of v y], assumption+,
frule Lv_pos[of v], frule Lv_z[of v], erule exE, simp,
frule_tac s = z in zless_neq[THEN not_sym, of "0"])
apply (rule iffI)
apply (rule_tac z = z in amult_eq_eq_r[of _ "n_val K v x" "n_val K v y"],
assumption+)
apply simp
done

lemma (in Corps) val_poss_n_val_poss:"⟦valuation K v; x ∈ carrier K⟧  ⟹
(0 < v x) = (0 < n_val K v x)"
frule val_pos_n_val_pos[of v x], assumption+,
rule iffI, erule conjE, simp,
apply (drule sym,
erule conjE, simp,
frule_tac val_0_n_val_0[THEN sym, of v x], assumption+,
simp)
done

lemma (in Corps) n_val_Pg:"valuation K v ⟹ n_val K v (Pg K v) = 1"
apply (frule val_Pg[of v], simp, (erule conjE)+,
frule n_val[of v "Pg K v"], simp, frule Lv_z[of v], erule exE, simp,
frule Lv_pos[of v], simp, frule_tac i = 0 and j = z in zless_neq)
apply (rotate_tac -1, frule not_sym, thin_tac "0 ≠ z",
subgoal_tac "n_val K v (Pg K v) * ant z = 1 * ant z",
rule_tac z = z in adiv_eq[of _ "n_val K v (Pg K v)" "1"], assumption+,
done

lemma (in Corps) n_val_valuationTr1:"valuation K v ⟹
∀x∈carrier K. n_val K v x ∈ Z⇩∞"
by (rule ballI,
frule n_val[of v], assumption,
frule_tac x = x in value_in_aug_inf[of v], assumption,
frule Lv_z[of v], erule exE, simp,
rule contrapos_pp, simp+)

lemma (in Corps) n_val_t2p:"⟦valuation K v; x ∈ carrier K; y ∈ carrier K⟧ ⟹
n_val K v (x ⋅⇩r y) = n_val K v x + (n_val K v y)"
apply (cut_tac field_is_ring,
frule Ring.ring_tOp_closed[of K x y], assumption+,
frule n_val[of v "x ⋅⇩r y"], assumption+,
frule Lv_pos[of "v"],
frule n_val[THEN sym, of v x], assumption+,
frule n_val[THEN sym, of v y], assumption+, simp,
frule Lv_z[of v], erule exE, simp)
apply (subgoal_tac "ant z ≠ 0")
apply (frule_tac z1 = z in amult_distrib1[THEN sym, of _ "n_val K v x"
"n_val K v y"], simp,
thin_tac "n_val K v x * ant z + n_val K v y * ant z =
(n_val K v x + n_val K v y) * ant z",
rule_tac z = z and a = "n_val K v (x ⋅⇩r y)" and
b = "n_val K v x + n_val K v y" in adiv_eq, simp, assumption+, simp)
done

lemma (in Corps) n_val_valuationTr2:"⟦ valuation K v; x ∈ carrier K;
y ∈ carrier K⟧  ⟹
amin (n_val K v x) (n_val K v y) ≤ (n_val K v ( x ± y))"
apply (frule n_val[THEN sym, of v x], assumption+,
frule n_val[THEN sym, of v y], assumption+,
frule n_val[THEN sym, of v "x ± y"],
cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
rule aGroup.ag_pOp_closed, assumption+)
apply (frule amin_le_plus[of v x y], assumption+, simp,
simp add:amult_commute[of _ "Lv K v"],
frule Lv_z[of v], erule exE, simp,
frule Lv_pos[of v], simp,