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"
apply (simp add:less_le)
done

lemma  zless_le_trans:"(i::int) < j; j  k  i < k"
apply (simp add:less_le)
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
         zadd_zle_mono[of "x" "x"], assumption+)
 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"
by (simp add:na_def)

lemma amult_an_an:"an (m * n) = (an m) * (an n)"
apply (simp add:an_def)
apply (simp add: of_nat_mult a_z_z)
done

definition
  adiv :: "[ant, ant]  ant" (infixl "adiv" 200) where
  "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],
       simp add:aless_zless)

lemma  amod_adiv_equality:
       "(ant a) = (a div b) *a (ant b) + ant (a mod b)"
apply (simp add:adiv_def tna_ant a_z_z a_zpz  asprod_mult)
done

lemma asp_z_Z:"z *a ant x  Z"
by (simp add:asprod_mult z_in_aug_inf)

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],
       simp del:ant_1 add:a_z_z,
       (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,
       erule disjE, simp add:ant_0, simp,
       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+,
       simp add:aminus_add_distrib[THEN sym, of "a" "b"],
       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"
by (simp add:amin_def)

lemma amin_le1:"(z::ant)  z'  (amin z w)  z'"
by (simp add:amin_def, simp add:aneg_le,
       rule impI, frule aless_le_trans[of "w" "z" "z'"],
       assumption+, simp add:aless_imp_le)

lemma amin_le2:"(z::ant)  z'  (amin w z)  z'"
by (simp add:amin_def, rule impI,
       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)"
by (simp add:Amin_geTr)

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",
       simp add:Abs_def, simp add:aadd_minus_inv)

apply (simp add:aneg_less,
       simp add:Abs_def, simp add:aneg_less[THEN sym, of "0" "x"],
       simp add:aneg_less[of "x" "0"], simp add:aadd_two_pos)
done

lemma  Abs_ge_self:"x  Abs x"
apply (simp add:Abs_def, rule impI,
       cut_tac ale_minus[of "x" "0"],
       simp add:aminus_0, simp add:aless_imp_le)
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"
by (simp add:an_def)

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 aadd_poss_less[of a 1],
       simp add:aadd_commute, assumption+)
apply (cut_tac zposs_aposss[of 1], simp)
done

lemma  gt_na_poss:"(na a) < m  0 < m"
apply (simp add:na_def)
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 add:asprod_amult a_z_z)
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,
        simp add:asprod_amult a_z_z)
 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"
apply (simp add:nset_def)
done

lemma nsetTr2:"j  nset (Suc a) (Suc b)  j - Suc 0  nset a b"
apply (simp add:nset_def, erule conjE,
       simp add:skip_im_Tr4[of "j" "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"
apply (simp add: not_le)
done

lemma nset_m_m:"nset m m = {m}"
by (simp add:nset_def,
       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)"
apply (simp add:nset_def, (erule conjE)+,
       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)}"
by (auto simp add:nset_def)

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,
       simp add:aless_zless,
       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,
        simp only:aadd_commute[of _ "x"])
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)))"
by (simp add:multi_inequalityTr0)

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
       aadd_le_mono, simp add:aadd_commute,
       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"
apply (simp add:m_maxTr)
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 "(jn. f j  Z)  (ln. f l = 0)", simp)
 apply (simp add:aadd_0_l, erule conjE,
        thin_tac "(jn. f j  Z)  (ln. 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 "jSuc 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 add:aadd_0_r)
 apply simp
 apply (simp add:nat_not_le_less[of j])
 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 "(jn. f j  Z)  (ln. f l = 0)")
 apply (thin_tac "jSuc n. f j  Z",
        thin_tac "l{h. h  Suc n} - {Suc n}. f l = 0", simp only:mp)
 apply (simp add:aadd_0_l)

 apply (thin_tac "(jn. f j  Z)  (ln. 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 "jSuc 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"
apply (simp add:eSum_singleTr)
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"
apply (simp add:Kronecker_delta_def)
apply (simp add:z_in_aug_inf Zero_in_aug_inf)
apply (simp add:asprod_n_0 Zero_in_aug_inf)
done

lemma Kdelta_in_Zinf1:"j  n; k  n   δ⇘j k Z"
apply (simp add:Kronecker_delta_def)
apply (simp add:z_in_aug_inf Zero_in_aug_inf)
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 (simp add:zmax_def)
 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)
 apply (simp add:zmax_def)
done

lemma m_zmax_gt_each:"(j  n. f j  Zset)  (j  n. (f j)  m_zmax n f)"
apply (simp add:m_zmax_gt_eachTr)
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 (simp add:transpos_def)
 apply (case_tac "k = j", simp, simp)
 apply (case_tac "k = n", simp)
 apply (simp add:n_notin_Nset_pred)
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 rKy) = (v x) + (v y)) 
    (x(carrier K). 0  (v x)  0  (v (1rK±Kx))) 
    (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"
by (simp add:valuation_def)

lemma (in Corps) value_in_aug_inf:"valuation K v; x  carrier K 
       v x  Z"
by (simp add:valuation_def, (erule conjE)+, simp add:funcset_mem)

lemma (in Corps) value_of_zero:"valuation K v   v (𝟬) = "
by (simp add:valuation_def)

lemma (in Corps) val_nonzero_noninf:"valuation K v; x  carrier K; x  𝟬
      (v x)  "
by (simp add:valuation_def)

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)"
by (simp add:amin_commute)

lemma (in Corps) val_t2p:"valuation K v; x  carrier K; y  carrier K
                          v (x r y ) = v x + v y"
by (simp add:valuation_def)

lemma (in Corps) val_axiom4:"valuation K v; x  carrier K; 0  v x 
                      0  v (1r ± x)"
by (simp add:valuation_def)

lemma (in Corps) val_axiom5:"valuation K v 
                  x. x  carrier K  v x    v x  0"
by (simp add:valuation_def)

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  1r  𝟬"
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+,
       simp add:Ring.ring_times_0_x, simp add:value_of_zero)
done

lemma (in Corps) value_of_one:"valuation K v  v (1r) = 0"
apply (cut_tac field_is_ring, frule Ring.ring_one[of "K"])
apply (frule val_t2p[of v "1r" "1r"], assumption+,
       simp add:Ring.ring_l_one, frule val_field_1_neq_0[of v],
       frule val_nonzero_z[of v "1r"], assumption+,
       erule exE, simp add:a_zpz)
done

lemma (in Corps) has_val_one_neq_zero:"valuation K v  1r  𝟬"
by (frule value_of_one[of "v"],
       rule contrapos_pp, simp+, simp add:value_of_zero)

lemma (in Corps) val_minus_one:"valuation K v  v (-a 1r) = 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" "1r" "𝟬"], assumption+,
       simp add:Ring.ring_zero, assumption)
 apply (frule val_nonzero_z[of v "-a 1r"],
        rule aGroup.ag_mOp_closed, assumption+, simp add:aGroup.ag_inv_zero,
        erule exE, frule val_t2p [THEN sym, of v "-a 1r" "-a 1r"])
apply (simp add:aGroup.ag_mOp_closed[of "K" "1r"],
       simp add:aGroup.ag_mOp_closed[of "K" "1r"],
       frule Ring.ring_inv1_3[THEN sym, of "K" "1r" "1r"], assumption+,
       simp add:Ring.ring_l_one, simp add:value_of_one a_zpz)
done

lemma (in Corps) val_minus_eq:"valuation K v; x  carrier K 
                            v (-a x) = v x"
apply (cut_tac field_is_ring,
     simp add:Ring.ring_times_minusl[of K x],
     subst val_t2p[of v], assumption+,
     frule Ring.ring_is_ag[of "K"], rule aGroup.ag_mOp_closed, assumption+,
     simp add:Ring.ring_one, assumption, simp add:val_minus_one,
     simp add:aadd_0_l)
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+,
       simp+, simp add:value_of_one, simp add:a_inv)
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,
       induct_tac n, simp add:Ring.ring_r_one, simp add:value_of_one)
apply (drule sym, simp)
apply (subst val_t2p[of v _ x], assumption+,
       rule Ring.npClose, assumption+,
       frule val_nonzero_z[of v x], assumption+,
              erule exE, simp add:asprod_mult a_zpz,
       simp add: distrib_right)
done

text‹exponent in a field›
lemma (in Corps) val_exp:" valuation K v; x  carrier K; x  𝟬 
                        z *a (v x) = v (xK⇙⇗z)"
apply (simp add:npowf_def)
apply (case_tac "0  z",
       simp, frule val_exp_ring [of v x "nat z"], assumption+,
       simp, simp)
 apply (simp add:zle,
       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,
       simp add:asprod_mult aminus, 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+,
       simp add:val_t2p,
       simp add:value_of_inv[of v "x"],
       frule_tac x = "ant z" in ale_diff_pos[of _ "v y"],
       simp add:diff_ant_def)
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" "1r" "y r x⇗‐ K⇖"], assumption+,
       frule val_axiom4[of v "y r ( x⇗‐ K)"], assumption+)
apply (frule aadd_le_mono[of "0" "v (1r ± y r x⇗‐ K)" "v x"],
       simp add:aadd_0_l, simp add:aadd_commute[of _ "v x"],
       simp add:val_t2p[THEN sym, of v x],
       simp add:Ring.ring_distrib1 Ring.ring_r_one,
       simp add:Ring.ring_tOp_commute[of "K" "x"],
       simp add:Ring.ring_tOp_assoc, simp add:linvf,
       simp add:Ring.ring_r_one,
       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+,
       simp add:aGroup.ag_l_zero amin_def,
       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,
       erule disjE, simp add:amin_le_plusTr,
       frule_tac amin_le_plusTr[of v y x], assumption+,
       simp add:aGroup.ag_pOp_commute amin_commute)
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"],
       simp add: amin_def)
apply (frule amin_le_plus[of v "x ± y" "-a y"],
       rule aGroup.ag_pOp_closed, assumption+,
       rule aGroup.ag_mOp_closed, assumption+,
       simp add:val_minus_eq,
       frule aGroup.ag_mOp_closed[of "K" "y"], assumption+,
       simp add:aGroup.ag_pOp_assoc[of "K" "x" "y"],
       simp add:aGroup.ag_r_inv1, simp add:aGroup.ag_r_zero,
       simp add:amin_def)
 apply (case_tac "¬ (v (x ±Ky)  (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 (1r ± 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:aGroup.ag_r_zero, simp add:value_of_zero,
        simp add: aneg_le[of "0" "v x"],
        frule value_less_eq[of v x "1r"], assumption+,
        simp add:value_of_one)
apply (drule sym,
       simp add:aGroup.ag_pOp_commute[of "K" "x"])
done

lemma (in Corps) val_1mx:"valuation K v; x  carrier K;
                  0  (v (1r ± (-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"],
       simp add:aGroup.ag_mOp_closed, assumption, simp add:val_minus_eq)

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"
apply (simp add:Lv_def,
       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. (xacarrier K. x = v xa)  0 < x}  LBset 1",
       thin_tac "x. (xacarrier K. x = v xa)  0 < x",
       subgoal_tac "x  carrier K - {𝟬}", blast,
       frule AMin_z[of v],  erule exE, simp)
apply (simp add:image_def,
       thin_tac "AMin {x. (xacarrier K. x = v xa)  0 < x} = ant a",
       rule contrapos_pp, simp+, frule sym, thin_tac "v (𝟬) = ant a",
       simp add:value_of_zero)
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 
  wcarrier 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+,
       simp add:aug_inf_def,
       cut_tac a = "v w" in mem_ant, simp, erule exE,
       cut_tac a = z and b = a in amod_adiv_equality)
apply (case_tac "z mod a = 0", simp add:ant_0 aadd_0_r, blast,
       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 (kK⇙⇗(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 = "kK⇙⇗(z div a)⇖" in value_of_inv[THEN sym, of v], assumption+,
      simp add:diff_ant_def,
       thin_tac "- v (kK⇙⇗(z div a)) = v ((kK⇙⇗(z div a))⇗‐ K)",
       cut_tac x = "kK⇙⇗(z div a)⇖" in invf_closed1, simp,
       simp, erule conjE,
       frule_tac x1 = w and y1 = "(kK⇙⇗(z div a))⇗‐ K⇖"  in
        val_t2p[THEN sym, of  v], assumption+, simp,
       cut_tac field_is_ring,
       thin_tac "v w + v ((kK⇙⇗(z div a))⇗‐ K) = ant (z mod a)",
       thin_tac "v (kK⇙⇗(z div a)) + ant (z mod a) = v w",
       frule_tac x = w and y = "(kK⇙⇗(z div a))⇗‐ K⇖" in
                 Ring.ring_tOp_closed[of "K"], assumption+)
apply (frule valuation_map[of v],
       frule_tac a = "w r (kK⇙⇗(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 (kK⇙⇗(z div a))⇗‐ K)",
       drule_tac a = "v (w r (kK⇙⇗(z div a))⇗‐ K)" in forall_spec,
       simp add:image_def)
   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 - {𝟬}) 
             (wv ` 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)

 apply (simp add:Lv_def,
        frule AMin_z[of v], erule exE, simp,
        frule Lv_pos[of v], simp add:Lv_def,
        frule_tac m1 = a in a_i_pos[THEN sym], blast,
        simp add:Lv_pos)
done

lemma (in Corps) val_principalTr2:"valuation K v;
  c  v ` (carrier K - {𝟬})  (wv ` carrier K. a. w = a * c)  0 < c;
  d  v ` (carrier K - {𝟬})  (wv ` carrier K. a. w = a * d)  0 < d
        c = d"
apply ((erule conjE)+,
       drule_tac x = d in bspec,
       simp add:image_def, erule bexE, blast,
       drule_tac x = c in bspec,
       simp add:image_def, erule bexE, blast)

apply ((erule exE)+,
       drule sym, simp,
       simp add:image_def, (erule bexE)+, 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,
       (erule exE)+, simp add:a_z_z,
       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,
       simp add:pos_zmult_eq_1_iff,
       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,
             assumption+, simp add:mult.commute)
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],
      frule Lv_pos[of v], simp add:Lv_def,
      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 (
       erule exE, simp add:asprod_mult,
       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,
      erule exE, simp add:a_z_z,
      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,
       simp add:amult_0_l)
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,
       simp add:aug_inf_def)
apply (rule contrapos_pp, simp+)
apply (case_tac "x = 𝟬K⇙", simp,
       frule n_val[of v "𝟬"],
       simp add:value_of_zero, simp add:value_of_zero)

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+,
       simp add:a_z_z)
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,
       simp add:n_val_0)
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)"
apply (simp add:less_le,
       frule val_pos_n_val_pos[of v x], assumption+,
       rule iffI, erule conjE, simp,
       simp add:value_n0_n_val_n0[of v x])
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+,
       simp add:amult_one_l)
done

lemma (in Corps) n_val_valuationTr1:"valuation K v 
                           xcarrier 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_pos[of v], simp add:aug_inf_def,
      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"],
       simp add:val_t2p,
       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,
       simp add:amin_amult_pos, simp add:amult_pos_mono_l)
done

lemma (