# Theory Valuation2

```(**        Valuation2
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 8. approximation(continued)

**)

theory Valuation2
imports Valuation1
begin

lemma (in Corps) OstrowskiTr8:"⟦valuation K v; x ∈ carrier K;
0 < v (1⇩r ± -⇩a x)⟧ ⟹
0 < (v (1⇩r ± -⇩a (x ⋅⇩r ((1⇩r ± x ⋅⇩r (1⇩r ± -⇩a x))⇗‐K⇖))))"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
apply (frule aGroup.ag_mOp_closed[of "K" "x"], assumption+,
frule Ring.ring_one[of "K"],
frule aGroup.ag_pOp_closed[of "K" "1⇩r" " -⇩a x"], assumption+,
frule OstrowskiTr32[of v x], assumption+)
apply (case_tac "x = 1⇩r⇘K⇙", simp,
apply (frule aGroup.ag_pOp_closed[of K "1⇩r" "x ⋅⇩r (1⇩r ± -⇩a x)"], assumption+,
rule Ring.ring_tOp_closed, assumption+)
apply (cut_tac invf_closed[of "1⇩r ± x ⋅⇩r (1⇩r ± -⇩a x)"])

apply (cut_tac field_one_plus_frac3[of x], simp del:npow_suc,
subst val_t2p[of v], assumption+)
apply (rule aGroup.ag_pOp_closed, assumption+,
rule aGroup.ag_mOp_closed, assumption+, rule Ring.npClose,
assumption+,
thin_tac "1⇩r ± -⇩a x ⋅⇩r (1⇩r ± x ⋅⇩r (1⇩r ± -⇩a x))⇗‐ K⇖ =
(1⇩r ± -⇩a x^⇗K (Suc (Suc 0))⇖) ⋅⇩r (1⇩r ± x ⋅⇩r (1⇩r ± -⇩a x))⇗‐ K⇖",
subgoal_tac "1⇩r ± -⇩a x^⇗K (Suc (Suc 0))⇖ = (1⇩r ± x) ⋅⇩r (1⇩r ± -⇩a x)",
simp del:npow_suc,
thin_tac "1⇩r ± -⇩a x^⇗K (Suc (Suc 0))⇖ = (1⇩r ± x) ⋅⇩r (1⇩r ± -⇩a x)")
apply (subst val_t2p[of v], assumption+,
rule aGroup.ag_pOp_closed, assumption+,
subst value_of_inv[of v "1⇩r ± x ⋅⇩r (1⇩r ± -⇩a x)"], tactic ‹CHANGED distinct_subgoals_tac›, assumption+)

apply (rule contrapos_pp, simp+,
frule Ring.ring_tOp_closed[of K x "(1⇩r ± -⇩a x)"], assumption+,
frule aGroup.ag_eq_diffzero[THEN sym, of K "x ⋅⇩r (-⇩a x ± 1⇩r)" "-⇩a 1⇩r"],
assumption+, rule aGroup.ag_mOp_closed, assumption+)
frule eq_elems_eq_val[of "x ⋅⇩r (-⇩a x ± 1⇩r)" "-⇩a 1⇩r" v],
thin_tac "x ⋅⇩r (-⇩a x ± 1⇩r) = -⇩a 1⇩r",
frule aadd_pos_poss[of "v x" "v (-⇩a x ± 1⇩r)"], assumption+,
simp,
subst value_less_eq[THEN sym, of v "1⇩r" "x ⋅⇩r (1⇩r ± -⇩a x)"],
assumption+,
rule Ring.ring_tOp_closed, assumption+,
simp add:value_of_one, subst val_t2p[of v], assumption+,
rule aadd_pos_poss[of "v x" "v (1⇩r ± -⇩a x)"], assumption+,
cut_tac aadd_pos_poss[of "v (1⇩r ± x)" "v (1⇩r ± -⇩a x)"],
apply (subst Ring.ring_distrib2, assumption+, simp add:Ring.ring_l_one,
subst aGroup.pOp_assocTr43, assumption+,
rule Ring.ring_tOp_closed, assumption+,
subst Ring.ring_inv1_2, assumption+, simp, assumption+)

apply simp

apply (rule contrapos_pp, simp+,
frule Ring.ring_tOp_closed[of K x "(1⇩r ± -⇩a x)"], assumption+,
frule aGroup.ag_eq_diffzero[THEN sym, of K "x ⋅⇩r (-⇩a x ± 1⇩r)" "-⇩a 1⇩r"],
assumption+, rule aGroup.ag_mOp_closed, assumption+)
frule eq_elems_eq_val[of "x ⋅⇩r (-⇩a x ± 1⇩r)" "-⇩a 1⇩r" v],
thin_tac "x ⋅⇩r (-⇩a x ± 1⇩r) = -⇩a 1⇩r",
frule aadd_pos_poss[of "v x" "v (-⇩a x ± 1⇩r)"], assumption+,
simp)
done

lemma (in Corps) OstrowskiTr9:"⟦valuation K v; x ∈ carrier K; 0 < (v x)⟧ ⟹
0 < (v (x ⋅⇩r ((1⇩r ± x ⋅⇩r (1⇩r ± -⇩a x))⇗‐K⇖)))"
apply (subgoal_tac "1⇩r ± x ⋅⇩r (1⇩r ± -⇩a x) ≠ 𝟬")
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
frule aGroup.ag_mOp_closed[of "K" "x"], assumption+,
frule Ring.ring_one[of "K"],
frule aGroup.ag_pOp_closed[of "K" "1⇩r" "-⇩a x"], assumption+,
subst val_t2p, assumption+,
cut_tac invf_closed1[of "1⇩r ± x ⋅⇩r (1⇩r ± -⇩a x)"], simp)
apply simp
apply (rule aGroup.ag_pOp_closed, assumption+,
rule Ring.ring_tOp_closed, assumption+)
(*
apply (rule contrapos_pp, simp+,
frule Ring.ring_tOp_closed[of K x "(1⇩r ± -⇩a x)"], assumption+) apply (
frule aGroup.ag_eq_diffzero[THEN sym, of K "x ⋅⇩r (-⇩a x ± 1⇩r)" "-⇩a 1⇩r"])
apply (rule Ring.ring_tOp_closed, assumption+,
rule aGroup.ag_mOp_closed, assumption+)
apply (frule eq_elems_eq_val[of "x ⋅⇩r (-⇩a x ± 1⇩r)" "-⇩a 1⇩r" v],
thin_tac "x ⋅⇩r (-⇩a x ± 1⇩r) = -⇩a 1⇩r",
apply (cut_tac aadd_pos_poss[of "v (-⇩a x ± 1⇩r)" "v x"], simp)
apply (simp add:val_minus_eq[THEN sym, of v x])
apply (subst aGroup.ag_pOp_commute, assumption+)
apply (rule val_axiom4[of v "-⇩a x"], assumption+)
apply (subst value_of_inv[of v "1⇩r ± x ⋅⇩r (1⇩r ± -⇩a x)"], assumption+,
rule aGroup.ag_pOp_closed, assumption+,
rule Ring.ring_tOp_closed, assumption+,
frule value_less_eq[THEN sym, of v "1⇩r" "-⇩a x"], assumption+,
subst value_less_eq[THEN sym, of v "1⇩r" "x ⋅⇩r (1⇩r ± -⇩a x)"],
assumption+, rule Ring.ring_tOp_closed, assumption+,
rule aadd_pos_poss[of "v (1⇩r ± -⇩a x)" "v x"],
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of K],
frule Ring.ring_one,
rule contrapos_pp, simp+,
frule Ring.ring_tOp_closed[of K x "(1⇩r ± -⇩a x)"], assumption+,
rule aGroup.ag_pOp_closed, assumption+,
rule aGroup.ag_mOp_closed, assumption+,
frule aGroup.ag_mOp_closed[of K x], assumption+)

frule aGroup.ag_eq_diffzero[THEN sym, of K "x ⋅⇩r (-⇩a x ± 1⇩r)" "-⇩a 1⇩r"],
rule aGroup.ag_mOp_closed, assumption+,
frule eq_elems_eq_val[of "x ⋅⇩r (-⇩a x ± 1⇩r)" "-⇩a 1⇩r" v],
thin_tac "x ⋅⇩r (-⇩a x ± 1⇩r) = -⇩a 1⇩r",
frule_tac aGroup.ag_pOp_closed[of K "-⇩a x" "1⇩r"], assumption+,
cut_tac aadd_pos_poss[of "v (-⇩a x ± 1⇩r)" "v x"], simp,
subst aGroup.ag_pOp_commute, assumption+,
subst value_less_eq[THEN sym, of v "1⇩r" "-⇩a x"], assumption+,

apply assumption
done

lemma (in Corps) OstrowskiTr10:"⟦valuation K v; x ∈ carrier K;
¬ 0 ≤ v x⟧ ⟹ 0 < (v (x ⋅⇩r ((1⇩r ± x ⋅⇩r (1⇩r ± -⇩a x))⇗‐K⇖)))"
apply (frule OstrowskiTr6[of "v" "x"], assumption+,
cut_tac invf_closed1[of "1⇩r ± x ⋅⇩r (1⇩r ± -⇩a x)"], simp,
erule conjE, simp add:aneg_le, frule val_neg_nonzero[of "v" "x"],
(erule conjE)+, assumption+, erule conjE)
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
frule aGroup.ag_mOp_closed[of "K" "x"], assumption+,
frule Ring.ring_one[of "K"],
frule aGroup.ag_pOp_closed[of "K" "1⇩r" "-⇩a x"], assumption+,
subst val_t2p, assumption+)
apply (subst value_of_inv[of "v" "1⇩r ± x ⋅⇩r (1⇩r ± -⇩a x)"],
assumption+, subst aGroup.ag_pOp_commute[of "K" "1⇩r"], assumption+,
rule Ring.ring_tOp_closed, assumption+,
subst value_less_eq[THEN sym, of v
"x ⋅⇩r (1⇩r ± -⇩a x)" "1⇩r"], assumption+)
apply (rule Ring.ring_tOp_closed, assumption+, simp add:value_of_one,
frule one_plus_x_nonzero[of "v" "-⇩a x"], assumption,

frule value_less_eq[THEN sym, of "v" "-⇩a x" "1⇩r"], assumption+,
frule val_nonzero_z[of "v" "x"], assumption+, erule exE,
assumption)
done

lemma (in Corps) Ostrowski_first:"vals_nonequiv K (Suc 0) vv
⟹ ∃x∈carrier K. Ostrowski_elem K (Suc 0) vv x"
cut_tac Nset_Suc0, (erule conjE)+,
apply (rotate_tac -1,
frule_tac a = 0 in forall_spec, simp,
rotate_tac -1,
drule_tac a = "Suc 0" in forall_spec, simp)
apply (drule_tac a = "Suc 0" in forall_spec, simp,
rotate_tac -1,
drule_tac a = 0 in forall_spec, simp, simp)
apply (frule_tac a = 0 in forall_spec, simp,
drule_tac a = "Suc 0" in forall_spec, simp,
frule_tac v = "vv 0" and v' = "vv (Suc 0)" in
nonequiv_ex_Ostrowski_elem, assumption+,
erule bexE)

apply (erule conjE,
frule_tac v = "vv (Suc 0)" and v' = "vv 0" in
nonequiv_ex_Ostrowski_elem, assumption+,
erule bexE,
thin_tac "¬ v_equiv K (vv (Suc 0)) (vv 0)",
thin_tac "¬ v_equiv K (vv 0) (vv (Suc 0))")

apply (rename_tac s t) (* we show s and t are non-zero in the following 4
lines *)
apply (erule conjE,
frule_tac x = t and v = "vv 0" in val_neg_nonzero, assumption+)
frule_tac x = s and v = "vv (Suc 0)" in val_neg_nonzero,
assumption+, unfold less_ant_def)
apply (rule conjI, assumption+)

apply (frule_tac s = s and t = t and v = "vv 0" in OstrowskiTr2,
assumption+, rule ale_neq_less, assumption+)
apply (frule_tac s = s and t = t and v = "vv (Suc 0)" in OstrowskiTr3,
assumption+, rule ale_neq_less, assumption+)
apply (subgoal_tac "t ⋅⇩r (( s ± t)⇗‐K⇖) ∈ carrier K",
simp only:Ostrowski_elem_def,
simp only: nset_m_m[of "Suc 0"], blast)
(* Here simp add:nset_m_m[of "Suc 0"] wouldn't work *)
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
rule Ring.ring_tOp_closed, assumption+,
frule_tac s = s and t = t and v = "vv 0" in OstrowskiTr1,
assumption+, rule ale_neq_less, assumption+,
frule_tac x = s and y = t in aGroup.ag_pOp_closed[of "K"], assumption+)
apply (cut_tac x = "s ± t" in invf_closed, blast)
apply assumption     (* in the above two lines, simp wouldn't work *)
done

(** subsection on inequality **)

lemma (in Corps) Ostrowski:"∀vv. vals_nonequiv K (Suc n) vv ⟶
(∃x∈carrier K. Ostrowski_elem K (Suc n) vv x)"
apply (induct_tac n,
rule allI, rule impI, simp add:Ostrowski_first)
(** case (Suc n) **)
apply (rule allI, rule impI,
frule_tac n = n and vv = vv in restrict_vals_nonequiv1,
frule_tac n = n and vv = vv in restrict_vals_nonequiv2,
frule_tac a = "compose {h. h ≤ Suc n} vv (skip 1)" in forall_spec,
assumption,
drule_tac a = "compose {h. h ≤ Suc n} vv (skip 2)" in forall_spec,
assumption+, (erule bexE)+)
apply (rename_tac n vv s t,
cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
(**  case * * *  **)
apply (frule_tac x = s and y = t in Ring.ring_tOp_closed[of "K"], assumption+,
case_tac "0 ≤ vv (Suc 0) s ∧ 0 ≤ vv (Suc (Suc 0)) t",
frule_tac vv = vv and s = s and t = t in OstrowskiTr5, assumption+)
apply blast

(** case * * * **)
apply (simp,
case_tac "0 ≤ (vv (Suc 0) s)", simp,
frule_tac n = "Suc (Suc n)" and m = "Suc (Suc 0)" and vv = vv in
vals_nonequiv_valuation,
simp,
frule_tac v = "vv (Suc (Suc 0))" and x = t in OstrowskiTr6,
assumption+,
frule_tac x = "1⇩r ± t ⋅⇩r (1⇩r ± -⇩a t)" in invf_closed1,
frule_tac x = t and y = "(1⇩r ± t ⋅⇩r (1⇩r ± -⇩a t))⇗‐K⇖" in
Ring.ring_tOp_closed, assumption+, simp)
apply (subgoal_tac "Ostrowski_elem K (Suc (Suc n)) vv
(t ⋅⇩r ((1⇩r ± t ⋅⇩r (1⇩r ± (-⇩a t)))⇗‐K⇖))",
blast)
apply (subst Ostrowski_elem_def,
rule conjI,
thin_tac "Ostrowski_elem K (Suc n)
(compose {h. h ≤ Suc n} vv (skip (Suc 0))) s",
thin_tac "vals_nonequiv K (Suc n)
(compose {h. h ≤ Suc n} vv (skip (Suc 0)))",
thin_tac "vals_nonequiv K (Suc n) (compose {h. h≤ Suc n} vv (skip 2))",
thin_tac "0 ≤ (vv (Suc 0) s)",
frule_tac n = "Suc (Suc n)" and vv = vv and m = 0 in
vals_nonequiv_valuation, simp,
rule_tac v = "vv 0" and x = t in
OstrowskiTr8, assumption+)

thin_tac "∀j∈nset (Suc 0) (Suc n).
0 < (compose {h. h ≤ (Suc n)} vv (skip 2) j t)",
rule ballI,
thin_tac "0 ≤ (vv (Suc 0) s)",
thin_tac "Ostrowski_elem K (Suc n)
(compose {h. h ≤ (Suc n)} vv (skip (Suc 0))) s",
frule_tac n = "Suc (Suc n)" and vv = vv and m = j in
vals_nonequiv_valuation,
(** case * * * **)
apply (case_tac "j = Suc 0", simp,
drule_tac x = "Suc 0" in bspec,
rule_tac v = "vv (Suc 0)" and x = t in
OstrowskiTr9, assumption+,
frule_tac j = j and n = n in nset_Tr51, assumption+,
drule_tac x = "j - Suc 0" in bspec, assumption+,
(** case * * * **)
apply (case_tac "j = Suc (Suc 0)", simp) apply (
rule_tac v = "vv (Suc (Suc 0))" and x = t in OstrowskiTr10,
assumption+) apply (
subgoal_tac "¬ j - Suc 0 ≤ Suc 0", simp add:nset_def) apply(
rule_tac v = "vv j" and x = t in
apply (simp add:nset_def, (erule conjE)+, rule nset_Tr52, assumption+,
thin_tac "vals_nonequiv K (Suc n)
(compose {h. h ≤ (Suc n)} vv (skip (Suc 0)))",
thin_tac "vals_nonequiv K (Suc n)
(compose {h. h ≤ (Suc n)} vv (skip 2))",
thin_tac "Ostrowski_elem K (Suc n)
(compose {h. h ≤(Suc n)} vv (skip 2)) t")
apply (subgoal_tac "s ⋅⇩r ((1⇩r ± s ⋅⇩r (1⇩r ± -⇩a s))⇗‐K⇖) ∈ carrier K",
subgoal_tac "Ostrowski_elem K (Suc (Suc n)) vv
(s ⋅⇩r ((1⇩r ± s ⋅⇩r (1⇩r ± -⇩a s))⇗‐K⇖))", blast)
prefer 2
apply (frule_tac n = "Suc (Suc n)" and m = "Suc 0" and vv = vv in
vals_nonequiv_valuation, simp,
frule_tac v = "vv (Suc 0)" and x = s in OstrowskiTr6, assumption+,
rule Ring.ring_tOp_closed, assumption+,
frule_tac x = "1⇩r ± s ⋅⇩r (1⇩r ± -⇩a s)" in invf_closed1, simp,
apply (rule conjI)
apply (rule_tac v = "vv 0" and x = s in OstrowskiTr8,
apply (
thin_tac "vals_nonequiv K (Suc (Suc n)) vv",
(erule conjE)+,
thin_tac "∀j∈nset (Suc 0) (Suc n).
0 < (compose {h. h ≤ (Suc n)} vv (skip (Suc 0)) j s)",
(** case *** *** **)
apply (case_tac "j = Suc 0", simp,
rule_tac v = "vv (Suc 0)" and x = s in OstrowskiTr10,
rule_tac v = "vv j" and x = s in OstrowskiTr9,
frule_tac j = j in nset_Tr51, assumption+,
drule_tac x = "j - Suc 0" in bspec, assumption+)
done

lemma (in Corps) val_1_nonzero:"⟦valuation K v; x ∈ carrier K; v x = 1⟧ ⟹
x ≠ 𝟬"
apply (rule contrapos_pp, simp+,
rotate_tac 3, drule sym, simp only:ant_1[THEN sym],
simp del:ant_1)
done

lemma (in Corps) Approximation1_5Tr1:"⟦vals_nonequiv K (Suc n) vv;
n_val K (vv 0) = vv 0; a ∈ carrier K; vv 0 a = 1; x ∈ carrier K;
Ostrowski_elem K (Suc n) vv x⟧  ⟹
∀m. 2 ≤ m ⟶ vv 0 ((1⇩r ± -⇩a x)^⇗K m⇖ ± a ⋅⇩r (x^⇗K m⇖)) = 1"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
frule Ring.ring_one[of "K"],
rule allI, rule impI,
frule vals_nonequiv_valuation[of "Suc n" "vv" "0"],
simp,
simp add:Ostrowski_elem_def, frule conjunct1, fold Ostrowski_elem_def,
frule val_1_nonzero[of "vv 0" "a"], assumption+)
apply (frule vals_nonequiv_valuation[of "Suc n" "vv" "0"], simp,
frule val_nonzero_noninf[of "vv 0" "a"], assumption+,
frule val_unit_cond[of "vv 0" "x"], assumption+,
frule_tac n = m in Ring.npClose[of "K" "x"], assumption+,
frule aGroup.ag_mOp_closed[of "K" "x"], assumption+,
frule aGroup.ag_pOp_closed[of "K" "1⇩r" "-⇩a x"], assumption+)
apply (subgoal_tac "0 < m",
frule_tac x = "a ⋅⇩r (x^⇗K m⇖)" and y = "(1⇩r ± -⇩a x)^⇗K m⇖" in
value_less_eq[of "vv 0"],
rule Ring.ring_tOp_closed, assumption+,
rule Ring.npClose, assumption+, simp add: val_t2p,
frule value_zero_nonzero[of "vv 0" "x"], assumption+,
apply (case_tac "x = 1⇩r⇘K⇙", simp add:aGroup.ag_r_inv1,
frule_tac n = m in Ring.npZero_sub[of "K"], simp,
apply (cut_tac inf_ge_any[of "1"], simp add: less_le)
apply (rotate_tac -1, drule not_sym,
frule aGroup.ag_neq_diffnonzero[of "K" "1⇩r" "x"],
cut_tac n1 = m in of_nat_0_less_iff[THEN sym])
apply (cut_tac a = "0 < m" and b = "0 < int m" in a_b_exchange, simp,
assumption)
apply (thin_tac "(0 < m) = (0 < int m)",
frule val_nonzero_z[of "vv 0" "1⇩r ± -⇩a x"], assumption+,
erule exE, simp, simp add:asprod_amult a_z_z,
simp only:ant_1[THEN sym], simp only:aless_zless, simp add:ge2_zmult_pos)

apply (subst aGroup.ag_pOp_commute[of "K"], assumption+,
rule Ring.npClose, assumption+, rule Ring.ring_tOp_closed[of "K"],
assumption+,
rotate_tac -1, drule sym, simp,
thin_tac "vv 0 (a ⋅⇩r x^⇗K m⇖ ± (1⇩r ± -⇩a x)^⇗K m⇖) = vv 0 (a ⋅⇩r x^⇗K m⇖)")
frule value_zero_nonzero[of "vv 0" "x"], assumption+,
cut_tac z = m in less_le_trans[of "0" "2"], simp, assumption+)
done

lemma (in Corps) Approximation1_5Tr3:"⟦vals_nonequiv K (Suc n) vv;
x ∈ carrier K; Ostrowski_elem K (Suc n) vv x; j ∈ nset (Suc 0) (Suc n)⟧
⟹  vv j ((1⇩r ± -⇩a x)^⇗K m⇖) = 0"
apply (frule Ostrowski_elem_not_one[of "n" "vv" "x"], assumption+,
cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
frule Ring.ring_one[of "K"],
frule aGroup.ag_pOp_closed[of "K" "1⇩r" "-⇩a x"], assumption+)
frule_tac m = j in vals_nonequiv_valuation[of "Suc n" "vv"],
simp,
frule_tac v1 = "vv j" and x1 = "1⇩r ± -⇩a x" and n1 = m in
val_exp_ring[THEN sym], assumption+)

apply (frule_tac v = "vv j" and x = "1⇩r" and  y = "-⇩a x" in
apply (simp add:value_of_one, rotate_tac -1, drule sym,
done

lemma (in Corps) Approximation1_5Tr4:"⟦vals_nonequiv K (Suc n) vv;
aa ∈ carrier K; x ∈ carrier K;
Ostrowski_elem K (Suc n) vv x; j ≤ (Suc n)⟧ ⟹
vv j (aa ⋅⇩r (x^⇗K m⇖)) = vv j aa + (int m) *⇩a (vv j  x)"
apply (frule Ostrowski_elem_nonzero[of "n" "vv" "x"],
assumption+,
cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
apply (frule_tac m = j in vals_nonequiv_valuation[of "Suc n" "vv"], assumption)
apply (subst val_t2p[of "vv j"], assumption+,
rule Ring.npClose, assumption+,
cut_tac field_is_idom,
frule_tac v1 = "vv j" and x1 = x and n1 = m in
val_exp_ring[THEN sym], assumption+, simp)
done

lemma (in Corps) Approximation1_5Tr5:"⟦vals_nonequiv K (Suc n) vv;
a ∈ carrier K; a ≠ 𝟬; x ∈ carrier K;
Ostrowski_elem K (Suc n) vv x; j ∈ nset (Suc 0) (Suc n)⟧ ⟹
∃l. ∀m. l < m ⟶ 0 < (vv j (a ⋅⇩r (x^⇗K m⇖)))"
apply (frule Ostrowski_elem_nonzero[of "n" "vv" "x"], assumption+,
subgoal_tac "∀n. vv j (a ⋅⇩r (x^⇗K n⇖)) = vv j a + (int n) *⇩a (vv j  x)",
simp,
thin_tac "∀n. vv j (a ⋅⇩r x^⇗K n⇖) = vv j a + int n *⇩a vv j x")
prefer 2
apply (rule allI, rule Approximation1_5Tr4[of _ vv a x j],
apply (frule_tac m = j in vals_nonequiv_valuation[of "Suc n" "vv"],
frule val_nonzero_z[of "vv j" "a"], assumption+, erule exE,
frule conjunct2, fold Ostrowski_elem_def,
drule_tac x = j in bspec, assumption)
apply (frule Ostrowski_elem_nonzero[of "n" "vv" "x"], assumption+,
frule val_nonzero_z[of "vv j" "x"], assumption+, erule exE, simp,
frule_tac a = za and x = z in zmult_pos_bignumTr,
done

lemma (in Corps) Approximation1_5Tr6:"⟦vals_nonequiv K (Suc n) vv;
a ∈ carrier K; a ≠ 𝟬; x ∈ carrier K;
Ostrowski_elem K (Suc n) vv x; j ∈ nset (Suc 0) (Suc n)⟧ ⟹
∃l. ∀m. l < m ⟶ vv j ((1⇩r ± -⇩a x)^⇗K m⇖ ± a ⋅⇩r (x^⇗K m⇖)) = 0"
apply (frule vals_nonequiv_valuation[of "Suc n" "vv" "j"],
frule Approximation1_5Tr5[of "n" "vv" "a" "x" "j"],
assumption+, erule exE,
cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
subgoal_tac "∀m. l < m ⟶ vv j ((1⇩r ± -⇩a x)^⇗K m⇖ ± a ⋅⇩r (x^⇗K m⇖)) =
vv j ((1⇩r ± -⇩a x)^⇗K m⇖)")
apply (rule allI, rule impI,
drule_tac a = m in forall_spec, assumption,
frule_tac x = "(1⇩r ± -⇩a x)^⇗K m⇖" and y = "a ⋅⇩r (x^⇗K m⇖)" in
value_less_eq[of "vv j"],
rule Ring.npClose, assumption+,
apply (rule Ring.ring_tOp_closed, assumption+,
rule Ring.npClose, assumption+,
frule sym, assumption)
done

lemma (in Corps) Approximation1_5Tr7:"⟦a ∈ carrier K; vv 0 a = 1;
x ∈ carrier K⟧ ⟹
vals_nonequiv K (Suc n) vv  ∧ Ostrowski_elem K (Suc n) vv x ⟶
(∃l. ∀m. l < m ⟶ (∀j∈nset (Suc 0) (Suc n).
(vv j ((1⇩r ± -⇩a x)^⇗K m⇖ ± a ⋅⇩r (x^⇗K m⇖)) = 0)))"
apply (induct_tac n,
rule impI, erule conjE, simp add:nset_m_m[of "Suc 0"],
frule vals_nonequiv_valuation[of "Suc 0" "vv" "Suc 0"], simp,
frule Approximation1_5Tr6[of "0" "vv" "a" "x" "Suc 0"], assumption+)
apply (frule vals_nonequiv_valuation[of "Suc 0" "vv" "0"], simp,
frule val_1_nonzero[of "vv 0" "a"], assumption+, simp add:nset_def,
assumption)
(** case n **)
apply (rule impI, erule conjE,
frule_tac n = n in  restrict_vals_nonequiv[of _ "vv"],
frule_tac n = n in restrict_Ostrowski_elem[of "x"  _ "vv"],
assumption, simp,
erule exE,
frule_tac n = "Suc n" and j = "Suc (Suc n)" in Approximation1_5Tr6
[of _ "vv" "a" "x"], assumption+,
frule_tac n = "Suc (Suc n)" in vals_nonequiv_valuation[of _ "vv"
"0"],simp,
rule val_1_nonzero[of "vv 0" "a"], assumption+,
apply (erule exE,
subgoal_tac "∀m. (max l la) < m ⟶ (∀j∈nset (Suc 0) (Suc (Suc n)).
vv j ((1⇩r ± -⇩a x)^⇗K m⇖ ± a ⋅⇩r (x^⇗K m⇖)) = 0)",
blast,
done

lemma (in Corps) Approximation1_5P:"⟦vals_nonequiv K (Suc n) vv;
n_val K (vv 0) = vv 0⟧ ⟹
∃x∈carrier K. ((vv 0 x = 1) ∧ (∀j∈nset (Suc 0) (Suc n). (vv j x) = 0))"
apply (frule vals_nonequiv_valuation[of "Suc n" "vv" "0"], simp) apply (
frule n_val_surj[of "vv 0"], erule bexE) apply (
rename_tac aa) apply (
cut_tac n = n in Ostrowski) apply (
drule_tac a = vv in forall_spec[of "vals_nonequiv K (Suc n)"], simp)
apply (
erule bexE,
frule_tac a = aa and x = x in Approximation1_5Tr1[of "n" "vv"],
assumption+,
simp, assumption+)
apply (frule_tac a = aa and x = x in Approximation1_5Tr7[of _ "vv" _ "n"],
simp, assumption,
simp, erule exE,
cut_tac b = "Suc l" in max.cobounded1[of "2"],
cut_tac b = "Suc l" in max.cobounded2[of _ "2"],
cut_tac n = l in lessI,
frule_tac x = l and y = "Suc l" and z = "max 2 (Suc l)" in
less_le_trans, assumption+,
thin_tac "Suc l ≤ max 2 (Suc l)", thin_tac "l < Suc l",
drule_tac a = "max 2 (Suc l)" in forall_spec, simp,
drule_tac a = "max 2 (Suc l)" in forall_spec, assumption)
apply (subgoal_tac "(1⇩r ± -⇩a x)^⇗K (max 2 (Suc l))⇖ ± aa ⋅⇩r (x^⇗K (max 2 (Suc l))⇖) ∈
carrier K",
blast,
cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
rule aGroup.ag_pOp_closed, assumption+, rule Ring.npClose, assumption+,
rule Ring.npClose, assumption+)
done

lemma K_gamma_hom:"k ≤ n ⟹ ∀j ≤ n. (λl. γ⇘k l⇙) j ∈ Zset"
done

lemma transpos_eq:"(τ⇘0 0⇙) k = k"

lemma (in Corps) transpos_vals_nonequiv:"⟦vals_nonequiv K (Suc n) vv;
j ≤ (Suc n)⟧ ⟹ vals_nonequiv K (Suc n) (vv ∘ (τ⇘0 j⇙))"
apply (frule conjunct1, fold vals_nonequiv_def)
apply (rule allI, rule impI)
apply (case_tac "ja = 0", simp,
case_tac "j = 0", simp add:transpos_eq)
apply (subst transpos_ij_1[of "0" "Suc n" "j"], simp, assumption+,
rule not_sym, assumption, simp)

apply (case_tac "ja = j", simp)
apply (subst transpos_ij_2[of "0" "Suc n" "j"], simp, assumption, simp,
apply (case_tac "j = 0", simp add:transpos_eq)
apply (cut_tac x = ja in transpos_id_1[of 0 "Suc n" j], simp, assumption+,
rule not_sym, assumption+)
(rule allI, rule impI)+, rule impI)
apply (case_tac "j = 0", simp add:transpos_eq,
cut_tac transpos_inj[of "0" "Suc n" "j"], simp)
apply (frule_tac x = ja and y = l in injective[of "transpos 0 j"
"{j. j ≤ (Suc n)}"], simp, simp, assumption+)
apply (cut_tac l = ja in transpos_mem[of "0" "Suc n" "j"], simp, assumption+,
simp, assumption,
cut_tac l = l in transpos_mem[of "0" "Suc n" "j"], simp, assumption+,
simp, assumption)
simp, assumption, rule not_sym, assumption)
done

definition
Ostrowski_base :: "[_, nat ⇒ 'b ⇒ ant, nat] ⇒ (nat ⇒ 'b)"
("(Ω⇘_ _ _⇙)" [90,90,91]90) where
"Ostrowski_base K vv n = (λj∈{h. h ≤ n}. (SOME x. x∈carrier K ∧
(Ostrowski_elem K n (vv ∘ (τ⇘0 j⇙)) x)))"

definition
App_base :: "[_, nat ⇒ 'b ⇒ ant, nat] ⇒ (nat ⇒ 'b)" where
"App_base K vv n = (λj∈{h. h ≤ n}. (SOME x. x∈carrier K ∧ (((vv ∘ τ⇘0 j⇙) 0 x
= 1) ∧ (∀k∈nset (Suc 0) n. ((vv ∘ τ⇘0 j⇙) k x) = 0))))"
(* Approximation base. *)

lemma (in Corps) Ostrowski_base_hom:"vals_nonequiv K (Suc n) vv ⟹
Ostrowski_base K vv (Suc n) ∈ {h. h ≤ (Suc n)} → carrier K"
apply (rule Pi_I, rename_tac l,
frule_tac j = l in transpos_vals_nonequiv[of n vv], simp,
cut_tac Ostrowski[of n])
apply (drule_tac a = "vv ∘ τ⇘0 l⇙" in forall_spec, simp,
rule someI2_ex, blast, simp)
done

lemma (in Corps) Ostrowski_base_mem:"vals_nonequiv K (Suc n) vv ⟹
∀j ≤ (Suc n). Ostrowski_base K vv (Suc n) j ∈ carrier K"
by (rule allI, rule impI,
frule Ostrowski_base_hom[of "n" "vv"],

lemma (in Corps)  Ostrowski_base_mem_1:"⟦vals_nonequiv K (Suc n) vv;
j ≤ (Suc n)⟧ ⟹ Ostrowski_base K vv (Suc n) j ∈ carrier K"

lemma (in Corps) Ostrowski_base_nonzero:"⟦vals_nonequiv K (Suc n) vv;
j ≤ Suc n⟧  ⟹ (Ω⇘K vv (Suc n)⇙) j ≠ 𝟬"
frule_tac j = j in transpos_vals_nonequiv[of "n" "vv"],
assumption+,
cut_tac Ostrowski[of "n"],
drule_tac a = "vv ∘ τ⇘0 j⇙" in forall_spec, assumption,
rule someI2_ex, blast)
apply (thin_tac "∃x∈carrier K. Ostrowski_elem K (Suc n) (vv ∘ τ⇘0 j⇙) x",
erule conjE)
apply (rule_tac vv = "vv ∘ τ⇘0 j⇙" and x = x in Ostrowski_elem_nonzero[of "n"],
assumption+)
done

lemma (in Corps) Ostrowski_base_pos:"⟦vals_nonequiv K (Suc n) vv;
j ≤ Suc n; ja ≤ Suc n; ja ≠ j⟧ ⟹ 0 < ((vv j) ((Ω⇘K vv (Suc n)⇙) ja))"
frule_tac j = ja in transpos_vals_nonequiv[of "n" "vv"],
assumption+,
cut_tac Ostrowski[of "n"],
drule_tac a = "vv ∘ τ⇘0 ja⇙" in forall_spec, assumption+)
apply (rule someI2_ex, blast,
thin_tac "∃x∈carrier K. Ostrowski_elem K (Suc n) (vv ∘ τ⇘0 ja⇙) x",
apply (case_tac "ja = 0", simp, cut_tac transpos_eq[of "j"],
simp add:nset_def, frule Suc_leI[of "0" "j"],
frule_tac a = j in forall_spec, simp, simp)
apply (case_tac "j = 0", simp,
frule_tac x = ja in bspec, simp add:nset_def,
cut_tac  transpos_ij_2[of "0" "Suc n" "ja"], simp, simp+)
apply (frule_tac x = j in bspec, simp add:nset_def,
cut_tac transpos_id[of "0" "Suc n" "ja" "j"], simp+)
done

lemma (in Corps) App_base_hom:"⟦vals_nonequiv K (Suc n) vv;
∀j ≤ (Suc n). n_val K (vv j) = vv j⟧ ⟹
∀j ≤ (Suc n). App_base K vv (Suc n) j ∈ carrier K"
apply (rule allI, rule impI,
rename_tac k,
subst App_base_def)
apply (case_tac "k = 0", simp, simp add:transpos_eq,
frule Approximation1_5P[of "n" "vv"], simp,
rule someI2_ex, blast, simp)
apply (frule_tac j = k in transpos_vals_nonequiv[of "n" "vv"],
frule_tac vv = "vv ∘ τ⇘0 k⇙" in Approximation1_5P[of "n"])
apply (simp add:cmp_def, subst transpos_ij_1[of "0" "Suc n"], simp+,
subst transpos_ij_1[of 0 "Suc n" k], simp+)
apply (rule someI2_ex, blast, simp)
done

lemma (in Corps) Approzimation1_5P2:"⟦vals_nonequiv K (Suc n) vv;
∀l∈{h. h ≤ Suc n}. n_val K (vv l) = vv l; i ≤ Suc n; j ≤ Suc n⟧
⟹ vv i (App_base K vv (Suc n) j) = δ⇘i j⇙ "
apply (case_tac "j = 0", simp add:transpos_eq,
rule someI2_ex,
frule Approximation1_5P[of "n" "vv"], simp , blast,
simp add:Kronecker_delta_def, rule impI, (erule conjE)+,
frule_tac x = i in bspec, simp add:nset_def, assumption)

apply (frule_tac j = j in transpos_vals_nonequiv[of "n" "vv"], simp,
frule Approximation1_5P[of "n" "vv ∘ τ⇘0 j⇙"],

case_tac "i = 0", simp add:transpos_eq,
rule someI2_ex, blast,
thin_tac "∃x∈carrier K.
vv j x = 1 ∧ (∀ja∈nset (Suc 0) (Suc n). vv ((τ⇘0 j⇙) ja) x = 0)",
(erule conjE)+,
drule_tac x = j in bspec, simp add:nset_def,

case_tac "i = j", simp add:transpos_ij_1, rule someI2_ex, blast, simp)

apply (simp, rule someI2_ex, blast,
thin_tac "∃x∈carrier K. vv ((τ⇘0 j⇙) 0) x = 1 ∧
(∀ja∈nset (Suc 0) (Suc n). vv ((τ⇘0 j⇙) ja) x = 0)",
(erule conjE)+,
drule_tac x = i in bspec, simp add:nset_def,
cut_tac transpos_id[of 0 "Suc n" j i], simp+)
done

(*
lemma (in Corps) Approximation1_5:"⟦vals_nonequiv K (Suc n) vv;
∀j ≤ (Suc n)}. n_val K (vv j) = vv j⟧ ⟹
∃x∈{h. h ≤ (Suc n)} → carrier K. ∀i ≤ (Suc n). ∀j ≤ (Suc n).
((vv i)  (x j) = δ⇘i j⇙)" *)

lemma (in Corps) Approximation1_5:"⟦vals_nonequiv K (Suc n) vv;
∀j ≤ (Suc n). n_val K (vv j) = vv j⟧ ⟹
∃x. (∀j ≤ (Suc n). x j ∈ carrier K) ∧ (∀i ≤ (Suc n). ∀j ≤ (Suc n).
((vv i)  (x j) = δ⇘i j⇙))"
apply (frule App_base_hom[of n vv], rule allI, simp)
apply (subgoal_tac "(∀i ≤ (Suc n). ∀j ≤ (Suc n).
(vv i) ((App_base K vv (Suc n)) j)  = (δ⇘i j⇙))",
blast)
apply (rule allI, rule impI)+
apply (rule Approzimation1_5P2, assumption+, simp+)
done

lemma (in Corps) Ostrowski_baseTr0:"⟦vals_nonequiv K (Suc n) vv; l ≤ (Suc n) ⟧
⟹   0 < ((vv l) (1⇩r ± -⇩a (Ostrowski_base K vv (Suc n) l))) ∧
(∀m∈{h. h ≤ (Suc n)} - {l}. 0 < ((vv m) (Ostrowski_base K vv (Suc n) l)))"
frule_tac j = l in transpos_vals_nonequiv[of "n" "vv"], assumption,
cut_tac Ostrowski[of "n"],
drule_tac a = "vv ∘ τ⇘0 l⇙" in forall_spec, assumption)
apply (erule bexE,
unfold Ostrowski_elem_def, frule conjunct1,
fold Ostrowski_elem_def,
apply (case_tac "l = 0", simp, simp add:transpos_eq,
rule someI2_ex, blast, simp,
rule someI2_ex, blast, simp)

case_tac "l = 0", simp, simp add:transpos_eq,
rule someI2_ex, blast,
thin_tac "0 < vv 0 (1⇩r ± -⇩a x) ∧
(∀j∈nset (Suc 0) (Suc n). 0 < vv j x)",

apply (rule ballI, erule conjE,
rule someI2_ex, blast,
thin_tac "∀j∈nset (Suc 0) (Suc n). 0 < vv ((τ⇘0 l⇙) j) x",
(erule conjE)+)

apply (case_tac "m = 0", simp,
drule_tac x = l in bspec, simp add:nset_def,
drule_tac x = m in bspec, simp add:nset_def,
done

lemma (in Corps) Ostrowski_baseTr1:"⟦vals_nonequiv K (Suc n) vv; l ≤ (Suc n)⟧
⟹ 0 < ((vv l) (1⇩r ± -⇩a (Ostrowski_base K vv (Suc n) l)))"

lemma (in Corps) Ostrowski_baseTr2:"⟦vals_nonequiv K (Suc n) vv;
l ≤ (Suc n); m ≤ (Suc n); l ≠ m⟧ ⟹
0 < ((vv m) (Ostrowski_base K vv (Suc n) l))"
apply (frule Ostrowski_baseTr0[of "n" "vv" "l"], assumption+)
apply simp
done

lemma Nset_have_two:"j ∈{h. h ≤ (Suc n)} ⟹ ∃m ∈ {h. h ≤ (Suc n)}. j ≠ m"
apply (rule contrapos_pp, simp+,
case_tac "j = Suc n", simp,
drule_tac a = 0 in forall_spec, simp, arith)
apply (drule_tac a = "Suc n" in forall_spec, simp, simp)
done

lemma (in Corps) Ostrowski_base_npow_not_one:"⟦0 < N; j ≤ Suc n;
vals_nonequiv K (Suc n) vv⟧  ⟹
1⇩r ± -⇩a ((Ω⇘K vv (Suc n)⇙) j^⇗K N⇖) ≠ 𝟬"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
rule contrapos_pp, simp+,
frule Ostrowski_base_mem_1[of "n" "vv" "j"], assumption,
frule Ring.npClose[of "K" "(Ω⇘K vv (Suc n)⇙) j" "N"], assumption+,
frule Ring.ring_one[of "K"],
frule aGroup.ag_mOp_closed[of K "(Ω⇘K vv (Suc n)⇙) j^⇗K N⇖"], assumption+,
frule aGroup.ag_pOp_closed[of "K" "1⇩r" "-⇩a ((Ω⇘K  vv (Suc n)⇙) j^⇗K N⇖)"],
assumption+)
apply (frule  aGroup.ag_pOp_add_r[of "K" "1⇩r ± -⇩a ((Ω⇘K vv (Suc n)⇙) j^⇗K N⇖)" "𝟬"
"(Ω⇘K  vv  (Suc n)⇙) j^⇗K N⇖"], assumption+,
thin_tac "1⇩r ± -⇩a ((Ω⇘K vv (Suc n)⇙) j^⇗K N⇖) = 𝟬")
apply (simp add:aGroup.ag_pOp_assoc[of "K" "1⇩r" "-⇩a ((Ω⇘K vv (Suc n)⇙) j^⇗K N⇖)"])
apply (subgoal_tac "∀m ≤ (Suc n). (j ≠ m ⟶
0 < (vv m ((Ω⇘K vv (Suc n)⇙) j)))")
apply (cut_tac Nset_have_two[of "j" "n"],
erule bexE, drule_tac a = m in forall_spec, simp,
thin_tac "(Ω⇘K vv (Suc n)⇙) j^⇗K N⇖ ± -⇩a ((Ω⇘K vv (Suc n)⇙) j^⇗K N⇖) ∈ carrier K",
frule_tac f = "vv m" in eq_elems_eq_val[of "1⇩r" "(Ω⇘K vv (Suc n)⇙) j^⇗K N⇖"],
thin_tac "1⇩r = (Ω⇘K vv (Suc n)⇙) j^⇗K N⇖", simp)
apply (frule_tac m = m in vals_nonequiv_valuation[of "Suc n" "vv"],
assumption+,
frule_tac v1 = "vv m" and n1 = N in val_exp_ring[THEN sym,
of  _ "(Ω⇘K vv (Suc n)⇙) j"], assumption+,
apply (subgoal_tac "int N ≠ 0",
frule_tac x = "vv m ((Ω⇘K vv (Suc n)⇙) j)" in asprod_0[of "int N"],
rule allI, rule impI, rule impI,
rule Ostrowski_baseTr2, assumption+)
done

abbreviation
CHOOSE :: "[nat, nat] ⇒ nat"  ("(⇘_⇙C⇘_⇙)" [80, 81]80) where
"⇘n⇙C⇘i⇙ == n choose i"

lemma (in Ring) expansion_of_sum1:"x ∈ carrier R ⟹
(1⇩r ± x)^⇗R n⇖ = nsum R (λi. ⇘n⇙C⇘i⇙ ×⇘R⇙ x^⇗R i⇖) n"
apply (cut_tac ring_one, frule npeSum2[of "1⇩r" "x" "n"], assumption+,
simp add:npOne, subgoal_tac "∀(j::nat). (x^⇗R j⇖) ∈ carrier R")
done

lemma (in Ring) tail_of_expansion:"x ∈ carrier R ⟹ (1⇩r ± x)^⇗R (Suc n)⇖ =
(nsum R (λ i. (⇘(Suc n)⇙C⇘(Suc i)⇙ ×⇘R⇙ x^⇗R (Suc i)⇖)) n) ± 1⇩r"
apply (cut_tac ring_is_ag)
apply (frule expansion_of_sum1[of "x" "Suc n"],
simp del:nsum_suc binomial_Suc_Suc npow_suc,
thin_tac "(1⇩r ± x)^⇗R (Suc n)⇖ = Σ⇩e R (λi. ⇘(Suc n)⇙C⇘i⇙ ×⇘R⇙ x^⇗R i⇖) (Suc n)")
apply (subst aGroup.nsumTail[of R n "λi. ⇘(Suc n)⇙C⇘i⇙ ×⇘R⇙ x^⇗R i⇖"], assumption,
rule allI, rule impI, rule nsClose, rule npClose, assumption)
apply (cut_tac ring_one,
done

lemma (in Ring) tail_of_expansion1:"x ∈ carrier R ⟹
(1⇩r ± x)^⇗R (Suc n)⇖  = x ⋅⇩r (nsum R (λ i. (⇘(Suc n)⇙C⇘(Suc i)⇙ ×⇘R⇙ x^⇗R i⇖)) n) ± 1⇩r"
apply (frule tail_of_expansion[of "x" "n"],
simp del:nsum_suc binomial_Suc_Suc npow_suc,
subgoal_tac "∀i.  ⇘Suc n⇙C⇘Suc i⇙ ×⇘R⇙ x^⇗R i⇖ ∈ carrier R",
cut_tac ring_one, cut_tac ring_is_ag)
prefer 2  apply(simp add: nsClose npClose)
apply (rule aGroup.ag_pOp_add_r[of "R" _ _ "1⇩r"], assumption+,
rule aGroup.nsum_mem, assumption+, rule allI, rule impI,
rule nsClose, rule npClose, assumption)
apply (rule ring_tOp_closed, assumption+,
rule aGroup.nsum_mem, assumption+, blast, simp add:ring_one)
apply (subst nsumMulEleL[of "λi. ⇘Suc n⇙C⇘Suc i⇙ ×⇘R⇙ x^⇗R i⇖" "x"], assumption+)
apply (rule aGroup.nsum_eq, assumption, rule allI, rule impI, rule nsClose,
rule npClose, assumption, rule allI, rule impI,
rule ring_tOp_closed, assumption+, rule nsClose, rule npClose,
assumption)
apply (rule allI, rule impI)
apply (subst nsMulDistrL, assumption, simp add:npClose,
frule_tac n = j in npClose[of x], simp add:ring_tOp_commute[of x])
done

lemma (in Corps) nsum_in_VrTr:"valuation K v ⟹
(∀j ≤ n. f j ∈ carrier K) ∧ (∀j ≤ n.
0 ≤ (v (f j))) ⟶ (nsum K f n) ∈ carrier (Vr K v)"
apply (induct_tac n)
apply (rule impI, erule conjE, simp add:val_pos_mem_Vr)
apply (rule impI, erule conjE)
apply (frule Vr_ring[of v], frule Ring.ring_is_ag[of "Vr K v"],
frule_tac  x = "f (Suc n)" and y = "nsum K f n" in
aGroup.ag_pOp_closed[of "Vr K v"],
subst val_pos_mem_Vr[THEN sym, of  "v"], assumption+,
simp, simp, simp)
apply (simp, subst Vr_pOp_f_pOp[of "v", THEN sym], assumption+,
subst val_pos_mem_Vr[THEN sym, of v], assumption+,
simp+)
apply (subst aGroup.ag_pOp_commute, assumption+, simp add:val_pos_mem_Vr,
assumption)
done

lemma (in Corps) nsum_in_Vr:"⟦valuation K v; ∀j ≤ n. f j ∈ carrier K;
∀j ≤ n.  0 ≤ (v (f j))⟧ ⟹ (nsum K f n) ∈ carrier (Vr K v)"
done

lemma (in Corps) nsum_mem_in_Vr:"⟦valuation K v;
∀j ≤ n. (f j) ∈ carrier K; ∀j ≤ n. 0 ≤ (v (f j))⟧ ⟹
(nsum K f n) ∈ carrier (Vr K v)"
by (rule nsum_in_Vr)

lemma (in Corps) val_nscal_ge_selfTr:"⟦valuation K v; x ∈ carrier K; 0 ≤ v x⟧
⟹  v x ≤  v (n ×⇘K⇙ x)"
apply (cut_tac field_is_ring, induct_tac n, simp)
simp,
frule_tac y = "n ×⇘K⇙ x" in amin_le_plus[of "v" "x"], assumption+,
rule Ring.nsClose, assumption+)
frule Ring.ring_is_ag[of K],
frule_tac n = n in Ring.nsClose[of K x], assumption+,
done

lemma (in Corps) ApproximationTr:"⟦valuation K v; x ∈ carrier K; 0 ≤ (v x)⟧ ⟹
v x ≤ (v (1⇩r ± -⇩a ((1⇩r ± x)^⇗K (Suc n)⇖)))"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
case_tac "x = 𝟬⇘K⇙",
simp, frule Ring.ring_one[of "K"], simp add:aGroup.ag_r_zero,
subst Ring.tail_of_expansion1[of "K" "x"], assumption+,
frule Ring.ring_one[of "K"])
apply (subgoal_tac "(nsum K (λi. ⇘Suc n⇙C⇘Suc i⇙ ×⇘K⇙ x^⇗K i⇖) n)∈carrier (Vr K v)",
frule Vr_mem_f_mem[of "v" "(nsum K (λi. ⇘Suc n⇙C⇘Suc i⇙ ×⇘K⇙ x^⇗K i⇖) n)"],
assumption+,
frule_tac x = x and y = "nsum K (λi. ⇘Suc n⇙C⇘Suc i⇙ ×⇘K⇙ x^⇗K i⇖) n" in
Ring.ring_tOp_closed[of "K"], assumption+,
subst aGroup.ag_pOp_commute[of "K" _ "1⇩r"], assumption+,
subst aGroup.ag_p_inv[of "K" "1⇩r"], assumption+,
subst aGroup.ag_pOp_assoc[THEN sym], assumption+,
assumption+,

apply (subst val_t2p[of v], assumption+) apply (
"nsum K (λi.(⇘n⇙C⇘i⇙ + ⇘n⇙C⇘Suc i⇙) ×⇘K⇙ x^⇗K i⇖) n"],
frule aadd_le_mono[of "0" "v (nsum K (λi.(⇘n⇙C⇘i⇙ + ⇘n⇙C⇘Suc i⇙) ×⇘K⇙ x^⇗K i⇖) n)"

apply (rule nsum_mem_in_Vr[of v n "λi.⇘Suc n⇙C⇘Suc i⇙ ×⇘K⇙ x^⇗K i⇖"], assumption,
rule allI, rule impI) apply (rule Ring.nsClose, assumption+) apply (simp add:Ring.npClose)

apply (rule allI, rule impI)
apply (cut_tac i = 0 and j = "v (x^⇗K j⇖)" and k = "v (⇘Suc n⇙C⇘Suc j⇙ ×⇘K⇙ x^⇗K j⇖)"
in ale_trans)
apply (case_tac "j = 0", simp add:value_of_one)
frule val_nonzero_z[of v x], assumption+,
erule exE,
cut_tac m1 = 0 and n1 = j in of_nat_less_iff[THEN sym],
frule_tac a = "0 < j" and b = "int 0 < int j" in a_b_exchange,
assumption, thin_tac "0 < j", thin_tac "(0 < j) = (int 0 < int j)")
apply (simp del: of_nat_0_less_iff)

apply (frule_tac w1 = "int j" and x1 = 0 and y1 = "ant z" in
asprod_pos_mono[THEN sym],
simp only:asprod_n_0)

apply(rule_tac x = "x^⇗K j⇖" and n = "⇘Suc n⇙C⇘Suc j⇙" in
val_nscal_ge_selfTr[of v], assumption+,
frule val_nonzero_z[of "v" "x"], assumption+, erule exE, simp)
apply (case_tac "j = 0", simp)
apply (subst asprod_amult, simp, simp add:a_z_z)
apply(
simp only:ant_0[THEN sym], simp only:ale_zle,
cut_tac m1 = 0 and n1 = j in of_nat_less_iff[THEN sym])
apply (        frule_tac a = "0 < j" and b = "int 0 < int j" in a_b_exchange,
assumption+, thin_tac "0 < j", thin_tac "(0 < j) = (int 0 < int j)",
frule_tac z = "int 0" and z' = "int j" in zless_imp_zle,
frule_tac i = "int 0" and j = "int j" and k = z in int_mult_le,
apply assumption
done

lemma (in Corps) ApproximationTr0:"aa ∈ carrier K ⟹
(1⇩r ± -⇩a (aa^⇗K N⇖))^⇗K N⇖ ∈ carrier K"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
rule Ring.npClose, assumption+,
rule aGroup.ag_mOp_closed, assumption+, rule Ring.npClose, assumption+)
done

lemma (in Corps) ApproximationTr1:"aa ∈ carrier K ⟹
1⇩r ± -⇩a ((1⇩r ± -⇩a (aa^⇗K N⇖))^⇗K N⇖) ∈ carrier K"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
frule ApproximationTr0[of aa N],
frule Ring.ring_one[of "K"], rule aGroup.ag_pOp_closed, assumption+,
rule aGroup.ag_mOp_closed, assumption+)
done

lemma (in Corps) ApproximationTr2:"⟦valuation K v; aa ∈ carrier K; aa ≠ 𝟬;
0 ≤ (v aa)⟧ ⟹ (int N) *⇩a(v aa) ≤ (v (1⇩r ± -⇩a ((1⇩r ± -⇩a (aa^⇗K N⇖))^⇗K N⇖)))"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
case_tac "N = 0",
frule val_nonzero_z[of v "aa"], assumption+, erule exE, simp)

apply (frule_tac n = N in Ring.npClose[of "K" "aa"], assumption+,
frule ApproximationTr[of v "-⇩a (aa^⇗K N⇖)" "N - Suc 0"],
subst val_exp_ring[THEN sym, of v], assumption+,
done

lemma (in Corps) eSum_tr:"
( ∀j ≤ n. (x j) ∈ carrier K) ∧
( ∀j ≤ n. (b j) ∈ carrier K) ∧ l ≤ n ∧
( ∀j∈({h. h ≤ n} -{l}). (g j = (x j) ⋅⇩r (1⇩r ± -⇩a (b j)))) ∧
g l = (x l) ⋅⇩r (-⇩a (b l))
⟶ (nsum K (λj ∈ {h. h ≤ n}. (x j) ⋅⇩r (1⇩r ± -⇩a (b j))) n) ± (-⇩a (x l)) =
nsum K g n"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
apply (induct_tac n)
apply (simp, rule impI, (erule conjE)+,
simp, frule Ring.ring_one[of "K"], subst Ring.ring_distrib1,
assumption+,
frule aGroup.ag_mOp_closed[of K "b 0"], assumption+,
frule Ring.ring_tOp_closed[of "K" "x 0" "-⇩a (b 0)"], assumption+,
subst aGroup.ag_pOp_commute[of "K" "x 0" _], assumption+,
subst aGroup.ag_pOp_assoc, assumption+,
frule aGroup.ag_mOp_closed[of "K"],
assumption+)
apply (simp add:aGroup.ag_r_inv1, subst aGroup.ag_r_zero, assumption+, simp)
apply (rule impI, (erule conjE)+)
apply (subgoal_tac "∀j ≤ (Suc n).  ((x j) ⋅⇩r (1⇩r ± -⇩a (b j))) ∈ carrier K")
apply (case_tac "l = Suc n", simp)
apply (subgoal_tac "Σ⇩e K g n ∈ carrier K",
subgoal_tac "{h. h ≤ (Suc n)} - {Suc n} = {h. h ≤ n}", simp,
subgoal_tac "∀j. j ≤ n ⟶ j ≤ (Suc n)",
frule_tac f = "λu. if u ≤ Suc n then (x u) ⋅⇩r (1⇩r ± -⇩a (b u)) else
undefined" and n = n in aGroup.nsum_eq[of "K" _ _ "g"])
apply (rule allI, rule impI, simp,
rule allI, simp, rule allI, rule impI, simp, simp)

apply (cut_tac a = "x (Suc n) ⋅⇩r (1⇩r ± -⇩a (b (Suc n))) ± -⇩a (x (Suc n))" and
b = "x (Suc n) ⋅⇩r (-⇩a (b (Suc n)))" and
c = "Σ⇩e K g n" in aGroup.ag_pOp_add_l[of K], assumption)
apply (rule aGroup.ag_pOp_closed, assumption+,
rule Ring.ring_tOp_closed, assumption+, simp,
rule aGroup.ag_mOp_closed, assumption, simp,
rule aGroup.ag_mOp_closed, assumption, simp,
rule Ring.ring_tOp_closed, assumption+, simp,
rule aGroup.ag_mOp_closed, assumption+, simp, assumption)

apply (subst Ring.ring_distrib1, assumption+, simp, simp add:Ring.ring_one,
frule_tac x = "x (Suc n)" and y = "x (Suc n) ⋅⇩r (-⇩a (b (Suc n)))" in
aGroup.ag_pOp_commute [of "K"], simp,
simp) apply (
subst aGroup.ag_pOp_assoc[of "K"], assumption+,
rule Ring.ring_tOp_closed, assumption+, simp,
subst aGroup.ag_r_inv1, assumption+, simp,
subst aGroup.ag_r_zero, assumption+,
rotate_tac -1, drule sym, simp) apply (
thin_tac "Σ⇩e K g n ± x (Suc n) ⋅⇩r (-⇩a (b (Suc n))) =
Σ⇩e K g n ± (x (Suc n) ⋅⇩r (1⇩r ± -⇩a (b (Suc n))) ± -⇩a (x (Suc n)))")
apply (subst aGroup.ag_pOp_assoc[THEN sym], assumption+,
rule Ring.ring_tOp_closed, assumption+, simp,
rule aGroup.ag_mOp_closed, assumption+, simp,
rule aGroup.ag_mOp_closed, assumption+, simp, simp,
simp, rule equalityI, rule subsetI, simp, rule subsetI, simp)
apply (rule aGroup.nsum_mem, assumption+,
rule allI, rule impI, simp)
defer
apply (rule allI, rule impI)
apply (case_tac "j = l", simp,
rule Ring.ring_tOp_closed, assumption, simp,
rule aGroup.ag_mOp_closed, assumption, simp, simp,
rule Ring.ring_tOp_closed, assumption, simp,
rule aGroup.ag_mOp_closed, assumption, simp, simp) (* end defer *)

apply (subst aGroup.ag_pOp_assoc, assumption+,
rule aGroup.nsum_mem, assumption+,
rule allI, simp, rule Ring.ring_tOp_closed, assumption+, simp,
rule aGroup.ag_mOp_closed, assumption, simp,
rule aGroup.ag_mOp_closed, assumption, simp,
subst aGroup.ag_pOp_commute[of K _ "-⇩a (x l)"], assumption+,
rule Ring.ring_tOp_closed, assumption, simp,
apply (rule aGroup.ag_mOp_closed, assumption+, simp,
rule aGroup.ag_mOp_closed, assumption+, simp,
subst aGroup.ag_pOp_assoc[THEN sym], assumption+,
rule aGroup.nsum_mem, assumption+,
rule allI, rule impI, simp,
rule aGroup.ag_mOp_closed, assumption, simp,
rule Ring.ring_tOp_closed, assumption, simp,
rule aGroup.ag_mOp_closed, assumption, simp)
apply (subgoal_tac "Σ⇩e K (λa. if a ≤ (Suc n) then x a ⋅⇩r (1⇩r ± -⇩a (b a))
else undefined) n ± -⇩a (x l) =
Σ⇩e K (λa. if a ≤ n then x a ⋅⇩r (1⇩r ± -⇩a (b a)) else undefined) n ±
-⇩a (x l)", simp,
rule aGroup.ag_pOp_add_r[of K _ _ "-⇩a (x l)"], assumption+,
rule aGroup.nsum_mem, assumption+,
rule allI, rule impI, simp,
rule aGroup.nsum_mem, assumption+,
rule allI, rule impI, simp,
rule aGroup.ag_mOp_closed, assumption, simp,
rule aGroup.nsum_eq, assumption+,
rule allI, rule impI, simp, rule allI, rule impI)
apply simp
apply (rule allI, rule impI, simp)
done

lemma (in Corps) eSum_minus_x:"⟦∀j ≤ n. (x j) ∈ carrier K;
∀j ≤ n. (b j) ∈ carrier K; l ≤ n;
∀j∈({h. h ≤ n} -{l}). (g j = (x j) ⋅⇩r (1⇩r ± ```