(** 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 (1r ± -a x)|] ==>
0 < (v (1r ± -a (x ·r ((1r ± x ·r (1r ± -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" "1r" " -a x"], assumption+,
frule OstrowskiTr32[of v x], assumption+)
apply (case_tac "x = 1rK", simp,
simp add:aGroup.ag_r_inv1, simp add:Ring.ring_times_x_0,
simp add:aGroup.ag_r_zero, cut_tac val_field_1_neq_0,
cut_tac invf_one, simp, simp add:Ring.ring_r_one,
simp add:aGroup.ag_r_inv1, assumption+)
apply (frule aGroup.ag_pOp_closed[of K "1r" "x ·r (1r ± -a x)"], assumption+,
rule Ring.ring_tOp_closed, assumption+)
apply (cut_tac invf_closed[of "1r ± x ·r (1r ± -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 "1r ± -a x ·r (1r ± x ·r (1r ± -a x)) K =
(1r ± -a x^K (Suc (Suc 0))) ·r (1r ± x ·r (1r ± -a x)) K",
subgoal_tac "1r ± -a x^K (Suc (Suc 0)) = (1r ± x) ·r (1r ± -a x)",
simp del:npow_suc,
thin_tac "1r ± -a x^K (Suc (Suc 0)) = (1r ± x) ·r (1r ± -a x)")
apply (subst val_t2p[of v], assumption+,
rule aGroup.ag_pOp_closed, assumption+,
subst value_of_inv[of v "1r ± x ·r (1r ± -a x)"], assumption+)
apply (rule contrapos_pp, simp+,
frule Ring.ring_tOp_closed[of K x "(1r ± -a x)"], assumption+,
simp add:aGroup.ag_pOp_commute[of K "1r"],
frule aGroup.ag_eq_diffzero[THEN sym, of K "x ·r (-a x ± 1r)" "-a 1r"],
assumption+, rule aGroup.ag_mOp_closed, assumption+)
apply (simp add:aGroup.ag_inv_inv[of K "1r"],
frule eq_elems_eq_val[of "x ·r (-a x ± 1r)" "-a 1r" v],
thin_tac "x ·r (-a x ± 1r) = -a 1r",
simp add:val_minus_eq value_of_one)
apply (simp add:val_t2p,
frule aadd_pos_poss[of "v x" "v (-a x ± 1r)"], assumption+,
simp,
subst value_less_eq[THEN sym, of v "1r" "x ·r (1r ± -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 (1r ± -a x)"], assumption+,
simp add:value_of_one,
cut_tac aadd_pos_poss[of "v (1r ± x)" "v (1r ± -a x)"],
simp add:aadd_0_r, rule val_axiom4, assumption+)
apply (subst Ring.ring_distrib2, assumption+, simp add:Ring.ring_l_one,
subst Ring.ring_distrib1, assumption+, simp add:Ring.ring_r_one,
subst aGroup.pOp_assocTr43, assumption+,
rule Ring.ring_tOp_closed, assumption+,
simp add:aGroup.ag_l_inv1 aGroup.ag_r_zero,
subst Ring.ring_inv1_2, assumption+, simp, assumption+)
apply simp
apply (rule contrapos_pp, simp+,
frule Ring.ring_tOp_closed[of K x "(1r ± -a x)"], assumption+,
simp add:aGroup.ag_pOp_commute[of K "1r"],
frule aGroup.ag_eq_diffzero[THEN sym, of K "x ·r (-a x ± 1r)" "-a 1r"],
assumption+, rule aGroup.ag_mOp_closed, assumption+)
apply (simp add:aGroup.ag_inv_inv[of K "1r"],
frule eq_elems_eq_val[of "x ·r (-a x ± 1r)" "-a 1r" v],
thin_tac "x ·r (-a x ± 1r) = -a 1r",
simp add:val_minus_eq value_of_one,
simp add:val_t2p,
frule aadd_pos_poss[of "v x" "v (-a x ± 1r)"], assumption+,
simp)
done
lemma (in Corps) OstrowskiTr9:"[|valuation K v; x ∈ carrier K; 0 < (v x)|] ==>
0 < (v (x ·r ((1r ± x ·r (1r ± -a x))K)))"
apply (subgoal_tac "1r ± x ·r (1r ± -a x) ≠ \<zero>")
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" "1r" "-a x"], assumption+,
subst val_t2p, assumption+,
cut_tac invf_closed1[of "1r ± x ·r (1r ± -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 "(1r ± -a x)"], assumption+) apply (
simp add:aGroup.ag_pOp_commute[of K "1r"],
frule aGroup.ag_eq_diffzero[THEN sym, of K "x ·r (-a x ± 1r)" "-a 1r"])
apply (rule Ring.ring_tOp_closed, assumption+,
rule aGroup.ag_mOp_closed, assumption+)
apply (simp add:aGroup.ag_inv_inv)
apply (frule eq_elems_eq_val[of "x ·r (-a x ± 1r)" "-a 1r" v],
thin_tac "x ·r (-a x ± 1r) = -a 1r",
simp add:val_minus_eq value_of_one,
simp add:val_t2p)
apply (simp add:aadd_commute[of "v x" "v (-a x ± 1r)"])
apply (cut_tac aadd_pos_poss[of "v (-a x ± 1r)" "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 (simp add:aless_imp_le, assumption) *)
apply (subst value_of_inv[of v "1r ± x ·r (1r ± -a x)"], assumption+,
rule aGroup.ag_pOp_closed, assumption+,
rule Ring.ring_tOp_closed, assumption+,
frule value_less_eq[THEN sym, of v "1r" "-a x"], assumption+,
simp add:value_of_one, simp add:val_minus_eq,
subst value_less_eq[THEN sym, of v "1r" "x ·r (1r ± -a x)"],
assumption+, rule Ring.ring_tOp_closed, assumption+,
simp add:value_of_one, subst val_t2p, assumption+,
subst aadd_commute,
rule aadd_pos_poss[of "v (1r ± -a x)" "v x"],
simp, assumption, simp add:value_of_one,
simp add:aadd_0_r)
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 "(1r ± -a x)"], assumption+,
rule aGroup.ag_pOp_closed, assumption+,
rule aGroup.ag_mOp_closed, assumption+,
frule aGroup.ag_mOp_closed[of K x], assumption+)
apply (simp add:aGroup.ag_pOp_commute[of K "1r"],
frule aGroup.ag_eq_diffzero[THEN sym, of K "x ·r (-a x ± 1r)" "-a 1r"],
simp add:aGroup.ag_pOp_commute,
rule aGroup.ag_mOp_closed, assumption+,
simp add:aGroup.ag_inv_inv,
frule eq_elems_eq_val[of "x ·r (-a x ± 1r)" "-a 1r" v],
thin_tac "x ·r (-a x ± 1r) = -a 1r",
simp add:val_minus_eq value_of_one,
frule_tac aGroup.ag_pOp_closed[of K "-a x" "1r"], assumption+,
simp add:val_t2p)
apply (simp add:aadd_commute[of "v x"],
cut_tac aadd_pos_poss[of "v (-a x ± 1r)" "v x"], simp,
subst aGroup.ag_pOp_commute, assumption+,
subst value_less_eq[THEN sym, of v "1r" "-a x"], assumption+,
simp add:value_of_one val_minus_eq, simp add:value_of_one)
apply assumption
done
lemma (in Corps) OstrowskiTr10:"[|valuation K v; x ∈ carrier K;
¬ 0 ≤ v x|] ==> 0 < (v (x ·r ((1r ± x ·r (1r ± -a x))K)))"
apply (frule OstrowskiTr6[of "v" "x"], assumption+,
cut_tac invf_closed1[of "1r ± x ·r (1r ± -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" "1r" "-a x"], assumption+,
subst val_t2p, assumption+)
apply (subst value_of_inv[of "v" "1r ± x ·r (1r ± -a x)"],
assumption+, subst aGroup.ag_pOp_commute[of "K" "1r"], assumption+,
rule Ring.ring_tOp_closed, assumption+,
subst value_less_eq[THEN sym, of v
"x ·r (1r ± -a x)" "1r"], assumption+)
apply (rule Ring.ring_tOp_closed, assumption+, simp add:value_of_one,
frule one_plus_x_nonzero[of "v" "-a x"], assumption,
simp add:val_minus_eq, erule conjE, simp,
subst val_t2p[of "v"], assumption+, simp add:aadd_two_negg)
apply (simp add:val_t2p,
frule value_less_eq[THEN sym, of "v" "-a x" "1r"], assumption+,
simp add:value_of_one, simp add:val_minus_eq,
simp add:val_minus_eq, simp add:aGroup.ag_pOp_commute[of "K" "-a x"],
frule val_nonzero_z[of "v" "x"], assumption+, erule exE,
simp add:a_zpz aminus, simp add:ant_0[THEN sym] aless_zless,
assumption)
done
lemma (in Corps) Ostrowski_first:"vals_nonequiv K (Suc 0) vv
==> ∃x∈carrier K. Ostrowski_elem K (Suc 0) vv x"
apply (simp add:vals_nonequiv_def,
cut_tac Nset_Suc0, (erule conjE)+,
simp add:valuations_def)
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+)
apply (simp add:less_ant_def, (erule conjE)+,
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 = "1r ± t ·r (1r ± -a t)" in invf_closed1,
frule_tac x = t and y = "(1r ± t ·r (1r ± -a t))K" in
Ring.ring_tOp_closed, assumption+, simp)
apply (subgoal_tac "Ostrowski_elem K (Suc (Suc n)) vv
(t ·r ((1r ± t ·r (1r ± (-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+)
apply (simp add:Ostrowski_elem_def, (erule conjE)+,
thin_tac "∀j∈nset (Suc 0) (Suc n).
0 < (compose {h. h ≤ (Suc n)} vv (skip 2) j t)",
simp add:compose_def skip_def,
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,
simp add:nset_def, simp add:Ostrowski_elem_def, (erule conjE)+)
(** case * * * **)
apply (case_tac "j = Suc 0", simp,
drule_tac b = "Suc 0" in forball_spec1,
simp add:nset_def,
simp add:compose_def skip_def,
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 b = "j - Suc 0" in forball_spec1, assumption+,
simp add:compose_def skip_def)
(** 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
OstrowskiTr9) apply (simp add:nset_def, assumption+)
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 ((1r ± s ·r (1r ± -a s))K) ∈ carrier K",
subgoal_tac "Ostrowski_elem K (Suc (Suc n)) vv
(s ·r ((1r ± s ·r (1r ± -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 = "1r ± s ·r (1r ± -a s)" in invf_closed1, simp,
simp add:Ostrowski_elem_def)
apply (rule conjI)
apply (rule_tac v = "vv 0" and x = s in OstrowskiTr8,
simp add:vals_nonequiv_valuation, assumption+)
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)",
simp add:compose_def skip_def, rule ballI)
(** case *** *** **)
apply (case_tac "j = Suc 0", simp,
rule_tac v = "vv (Suc 0)" and x = s in OstrowskiTr10,
simp add:vals_nonequiv_valuation, assumption+,
rule_tac v = "vv j" and x = s in OstrowskiTr9,
simp add:vals_nonequiv_valuation nset_def, assumption,
(erule conjE)+, simp add:compose_def skip_def,
frule_tac j = j in nset_Tr51, assumption+,
drule_tac b = "j - Suc 0" in forball_spec1, assumption+)
apply (simp add:nset_def)
done
lemma (in Corps) val_1_nonzero:"[|valuation K v; x ∈ carrier K; v x = 1|] ==>
x ≠ \<zero>"
apply (rule contrapos_pp, simp+,
simp add:value_of_zero,
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 ((1r ± -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" "1r" "-a x"], assumption+)
apply (subgoal_tac "0 < m",
frule_tac x = "a ·r (x^K m)" and y = "(1r ± -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+,
simp add:val_exp_ring[THEN sym], simp add:asprod_n_0 aadd_0_r)
apply (case_tac "x = 1rK", simp add:aGroup.ag_r_inv1,
frule_tac n = m in Ring.npZero_sub[of "K"], simp,
simp add:value_of_zero)
apply (cut_tac inf_ge_any[of "1"], simp add:aless_le)
apply (rotate_tac -1, drule not_sym,
frule aGroup.ag_neq_diffnonzero[of "K" "1r" "x"],
simp add:Ring.ring_one[of "K"], assumption+, simp,
simp add:val_exp_ring[THEN sym],
cut_tac n1 = m in zero_less_int_conv[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" "1r ± -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 ± (1r ± -a x)^K m) = vv 0 (a ·r x^K m)")
apply (simp add:val_t2p,
frule value_zero_nonzero[of "vv 0" "x"], assumption+,
simp add:val_exp_ring[THEN sym], simp add:asprod_n_0,
simp add:aadd_0_r,
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 ((1r ± -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" "1r" "-a x"], assumption+)
apply (simp add:aGroup.ag_mOp_closed, simp add:nset_def,
frule_tac m = j in vals_nonequiv_valuation[of "Suc n" "vv"],
simp,
frule_tac v1 = "vv j" and x1 = "1r ± -a x" and n1 = m in
val_exp_ring[THEN sym], assumption+)
apply (frule_tac v = "vv j" and x = "1r" and y = "-a x" in
value_less_eq, assumption+, simp add:aGroup.ag_mOp_closed)
apply(simp add:value_of_one, simp add:val_minus_eq,
simp add:Ostrowski_elem_def nset_def)
apply (simp add:value_of_one, rotate_tac -1, drule sym,
simp add:asprod_n_0)
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 ≠ \<zero>; 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],
assumption+, simp add:nset_def)
apply (frule_tac m = j in vals_nonequiv_valuation[of "Suc n" "vv"],
simp add:nset_def,
frule val_nonzero_z[of "vv j" "a"], assumption+, erule exE,
simp add:Ostrowski_elem_def,
frule conjunct2, fold Ostrowski_elem_def,
drule_tac b = j in forball_spec1, 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,
simp add:asprod_amult a_z_z a_zpz)
done
lemma (in Corps) Approximation1_5Tr6:"[|vals_nonequiv K (Suc n) vv;
a ∈ carrier K; a ≠ \<zero>; x ∈ carrier K;
Ostrowski_elem K (Suc n) vv x; j ∈ nset (Suc 0) (Suc n)|] ==>
∃l. ∀m. l < m --> vv j ((1r ± -a x)^K m ± a ·r (x^K m)) = 0"
apply (frule vals_nonequiv_valuation[of "Suc n" "vv" "j"],
simp add:nset_def,
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 ((1r ± -a x)^K m ± a ·r (x^K m)) =
vv j ((1r ± -a x)^K m)")
apply (simp add:Approximation1_5Tr3, blast)
apply (rule allI, rule impI,
drule_tac a = m in forall_spec, assumption,
frule_tac x = "(1r ± -a x)^K m" and y = "a ·r (x^K m)" in
value_less_eq[of "vv j"],
rule Ring.npClose, assumption+,
rule aGroup.ag_pOp_closed, assumption+, simp add:Ring.ring_one,
simp add:aGroup.ag_mOp_closed)
apply (rule Ring.ring_tOp_closed, assumption+,
rule Ring.npClose, assumption+,
simp add:Approximation1_5Tr3,
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 ((1r ± -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+,
simp add:nset_def)
apply (erule exE,
subgoal_tac "∀m. (max l la) < m --> (∀j∈nset (Suc 0) (Suc (Suc n)).
vv j ((1r ± -a x)^K m ± a ·r (x^K m)) = 0)",
blast,
simp add:nset_Suc)
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 y = "Suc l" in le_maxI1[of "2"],
cut_tac y = "Suc l" in le_maxI2[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 "(1r ± -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 aGroup.ag_pOp_closed, assumption+, simp add:Ring.ring_one,
simp add:aGroup.ag_mOp_closed, rule Ring.ring_tOp_closed, assumption+,
rule Ring.npClose, assumption+)
done
lemma K_gamma_hom:"k ≤ n ==> ∀j ≤ n. (λl. γk l) j ∈ Zset"
apply (simp add:Zset_def)
done
lemma transpos_eq:"(τ0 0) k = k"
by (simp add:transpos_def)
lemma (in Corps) transpos_vals_nonequiv:"[|vals_nonequiv K (Suc n) vv;
j ≤ (Suc n)|] ==> vals_nonequiv K (Suc n) (vv o (τ0 j))"
apply (simp add:vals_nonequiv_def)
apply (frule conjunct1, fold vals_nonequiv_def)
apply (simp add:valuations_def, rule conjI)
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,
simp add:vals_nonequiv_valuation)
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+)
apply (simp add:vals_nonequiv_valuation,
(rule allI, rule impI)+, rule impI)
apply (case_tac "j = 0", simp add:transpos_eq,
simp add:vals_nonequiv_def,
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)
apply (simp add:vals_nonequiv_def,
simp, assumption, rule not_sym, assumption)
done
constdefs (structure K)
Ostrowski_base::"[_, nat => 'b => ant, nat] => (nat => 'b)"
("(Ω_ _ _)" [90,90,91]90)
"Ostrowski_base K vv n == (λj∈{h. h ≤ n}. (SOME x. x∈carrier K ∧
(Ostrowski_elem K n (vv o (τ0 j)) x)))"
App_base::"[_, nat => 'b => ant, nat] => (nat => 'b)"
"App_base K vv n == (λj∈{h. h ≤ n}. (SOME x. x∈carrier K ∧ (((vv o τ0 j) 0 x
= 1) ∧ (∀k∈nset (Suc 0) n. ((vv o τ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 univar_func_test,
rule ballI, rename_tac l,
simp add:Ostrowski_base_def,
frule_tac j = l in transpos_vals_nonequiv[of n vv], simp,
cut_tac Ostrowski[of n])
apply (drule_tac a = "vv o τ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"],
simp add:funcset_mem)
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"
by (simp add:Ostrowski_base_mem)
lemma (in Corps) Ostrowski_base_nonzero:"[|vals_nonequiv K (Suc n) vv;
j ≤ Suc n|] ==> (ΩK vv (Suc n)) j ≠ \<zero>"
apply (simp add:Ostrowski_base_def,
frule_tac j = j in transpos_vals_nonequiv[of "n" "vv"],
assumption+,
cut_tac Ostrowski[of "n"],
drule_tac a = "vv o τ0 j" in forall_spec, assumption,
rule someI2_ex, blast)
apply (thin_tac "∃x∈carrier K. Ostrowski_elem K (Suc n) (vv o τ0 j) x",
erule conjE)
apply (rule_tac vv = "vv o τ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))"
apply (simp add:Ostrowski_base_def,
frule_tac j = ja in transpos_vals_nonequiv[of "n" "vv"],
assumption+,
cut_tac Ostrowski[of "n"],
drule_tac a = "vv o τ0 ja" in forall_spec, assumption+)
apply (rule someI2_ex, blast,
thin_tac "∃x∈carrier K. Ostrowski_elem K (Suc n) (vv o τ0 ja) x",
simp add:Ostrowski_elem_def, (erule conjE)+)
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 b = ja in forball_spec1, simp add:nset_def,
cut_tac transpos_ij_2[of "0" "Suc n" "ja"], simp, simp+)
apply (frule_tac b = j in forball_spec1, 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"],
simp add:nset_def,
frule_tac vv = "vv o τ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 (simp add:App_base_def)
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 b = i in forball_spec1, simp add:nset_def, assumption)
apply (frule_tac j = j in transpos_vals_nonequiv[of "n" "vv"], simp,
frule Approximation1_5P[of "n" "vv o τ0 j"],
simp add:cmp_def, simp add:transpos_ij_1[of 0 "Suc n" j])
apply (simp add:cmp_def,
case_tac "i = 0", simp add:transpos_eq,
simp add:transpos_ij_1, simp add:Kronecker_delta_def,
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 b = j in forball_spec1, simp add:nset_def,
simp add:transpos_ij_2)
apply (simp add:Kronecker_delta_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 b = i in forball_spec1, 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) (1r ± -a (Ostrowski_base K vv (Suc n) l))) ∧
(∀m∈{h. h ≤ (Suc n)} - {l}. 0 < ((vv m) (Ostrowski_base K vv (Suc n) l)))"
apply (simp add:Ostrowski_base_def,
frule_tac j = l in transpos_vals_nonequiv[of "n" "vv"], assumption,
cut_tac Ostrowski[of "n"],
drule_tac a = "vv o τ0 l" in forall_spec, assumption)
apply (erule bexE,
unfold Ostrowski_elem_def, frule conjunct1,
fold Ostrowski_elem_def,
rule conjI, simp add:Ostrowski_elem_def)
apply (case_tac "l = 0", simp, simp add:transpos_eq,
rule someI2_ex, blast, simp,
simp add:transpos_ij_1,
rule someI2_ex, blast, simp)
apply (simp add:Ostrowski_elem_def,
case_tac "l = 0", simp, simp add:transpos_eq,
rule someI2_ex, blast,
thin_tac "0 < vv 0 (1r ± -a x) ∧
(∀j∈nset (Suc 0) (Suc n). 0 < vv j x)",
rule ballI, simp add:nset_def)
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 b = l in forball_spec1, simp add:nset_def,
simp add:transpos_ij_2,
drule_tac b = m in forball_spec1, simp add:nset_def,
simp add:transpos_id)
done
lemma (in Corps) Ostrowski_baseTr1:"[|vals_nonequiv K (Suc n) vv; l ≤ (Suc n)|]
==> 0 < ((vv l) (1r ± -a (Ostrowski_base K vv (Suc n) l)))"
by (simp add:Ostrowski_baseTr0)
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|] ==>
1r ± -a ((ΩK vv (Suc n)) j^K N) ≠ \<zero>"
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" "1r" "-a ((ΩK vv (Suc n)) j^K N)"],
assumption+)
apply (frule aGroup.ag_pOp_add_r[of "K" "1r ± -a ((ΩK vv (Suc n)) j^K N)" "\<zero>"
"(ΩK vv (Suc n)) j^K N"], assumption+,
simp add:aGroup.ag_inc_zero, assumption+,
thin_tac "1r ± -a ((ΩK vv (Suc n)) j^K N) = \<zero>")
apply (simp add:aGroup.ag_pOp_assoc[of "K" "1r" "-a ((ΩK vv (Suc n)) j^K N)"])
apply (simp add:aGroup.ag_l_inv1, simp add:aGroup.ag_r_zero aGroup.ag_l_zero)
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 "1r" "(ΩK vv (Suc n)) j^K N"],
thin_tac "1r = (Ω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+,
simp add:Ostrowski_base_nonzero, simp, simp add:value_of_one)
apply (subgoal_tac "int N ≠ 0",
frule_tac x = "vv m ((ΩK vv (Suc n)) j)" in asprod_0[of "int N"],
assumption, simp add:less_ant_def, simp, simp,
rule allI, rule impI, rule impI,
rule Ostrowski_baseTr2, assumption+)
done
syntax
"@CHOOSE" :: "[nat, nat] => nat"
("(_C_)" [80, 81]80)
translations
"nCi" == "n choose i"
lemma (in Ring) expansion_of_sum1:"x ∈ carrier R ==>
(1r ± x)^R n = nsum R (λi. nCi ×R x^R i) n"
apply (cut_tac ring_one, frule npeSum2[of "1r" "x" "n"], assumption+,
simp add:npOne, subgoal_tac "∀(j::nat). (x^R j) ∈ carrier R")
apply (simp add:ring_l_one, rule allI, simp add:npClose)
done
lemma (in Ring) tail_of_expansion:"x ∈ carrier R ==> (1r ± x)^R (Suc n) =
(nsum R (λ i. ((Suc n)C(Suc i) ×R x^R (Suc i))) n) ± 1r"
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 "(1r ± x)^R (Suc n) = Σe R (λi. (Suc n)Ci ×R x^R i) (Suc n)")
apply (subst aGroup.nsumTail[of R n "λi. (Suc n)Ci ×R x^R i"], assumption,
rule allI, rule impI, rule nsClose, rule npClose, assumption)
apply (cut_tac ring_one,
simp del:nsum_suc binomial_Suc_Suc npow_suc add:aGroup.ag_l_zero)
done
lemma (in Ring) tail_of_expansion1:"x ∈ carrier R ==>
(1r ± x)^R (Suc n) = x ·r (nsum R (λ i. ((Suc n)C(Suc i) ×R x^R i)) n) ± 1r"
apply (frule tail_of_expansion[of "x" "n"],
simp del:nsum_suc binomial_Suc_Suc npow_suc,
subgoal_tac "∀i. Suc nCSuc 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" _ _ "1r"], 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 nCSuc 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)"
apply (simp add:nsum_in_VrTr)
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)
apply (simp add:value_of_zero,
simp,
frule_tac y = "n ×K x" in amin_le_plus[of "v" "x"], assumption+,
rule Ring.nsClose, assumption+)
apply (simp add:amin_def,
frule Ring.ring_is_ag[of K],
frule_tac n = n in Ring.nsClose[of K x], assumption+,
simp add:aGroup.ag_pOp_commute)
done
lemma (in Corps) ApproximationTr:"[|valuation K v; x ∈ carrier K; 0 ≤ (v x)|] ==>
v x ≤ (v (1r ± -a ((1r ± x)^K (Suc n))))"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
case_tac "x = \<zero>K",
simp, frule Ring.ring_one[of "K"], simp add:aGroup.ag_r_zero,
simp add:Ring.npOne, simp add:Ring.ring_l_one,simp add:aGroup.ag_r_inv1,
subst Ring.tail_of_expansion1[of "K" "x"], assumption+,
frule Ring.ring_one[of "K"])
apply (subgoal_tac "(nsum K (λi. Suc nCSuc i ×K x^K i) n)∈carrier (Vr K v)",
frule Vr_mem_f_mem[of "v" "(nsum K (λi. Suc nCSuc i ×K x^K i) n)"],
assumption+,
frule_tac x = x and y = "nsum K (λi. Suc nCSuc i ×K x^K i) n" in
Ring.ring_tOp_closed[of "K"], assumption+,
subst aGroup.ag_pOp_commute[of "K" _ "1r"], assumption+,
subst aGroup.ag_p_inv[of "K" "1r"], assumption+,
subst aGroup.ag_pOp_assoc[THEN sym], assumption+,
simp add:aGroup.ag_mOp_closed, rule aGroup.ag_mOp_closed, assumption+,
simp del:binomial_Suc_Suc add:aGroup.ag_r_inv1, subst aGroup.ag_l_zero,
assumption+,
rule aGroup.ag_mOp_closed, assumption+, simp add:val_minus_eq)
apply (subst val_t2p[of v], assumption+) apply (
simp add:val_pos_mem_Vr[THEN sym, of v
"nsum K (λi.(nCi + nCSuc i) ×K x^K i) n"],
frule aadd_le_mono[of "0" "v (nsum K (λi.(nCi + nCSuc i) ×K x^K i) n)"
"v x"], simp add:aadd_0_l, simp add:aadd_commute[of "v x"])
apply (rule nsum_mem_in_Vr[of v n "λi.Suc nCSuc 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 nCSuc j ×K x^K j)"
in ale_trans)
apply (case_tac "j = 0", simp add:value_of_one)
apply (simp add: val_exp_ring[THEN sym],
frule val_nonzero_z[of v x], assumption+,
erule exE,
cut_tac m1 = 0 and n1 = j in zless_int[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 nCSuc j" in
val_nscal_ge_selfTr[of v], assumption+,
simp add:Ring.npClose, simp add:val_exp_ring[THEN sym],
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 zless_int[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,
assumption+, simp add:zmult_commute )
apply assumption
done
lemma (in Corps) ApproximationTr0:"aa ∈ carrier K ==>
(1r ± -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_pOp_closed, assumption+, simp add:Ring.ring_one,
rule aGroup.ag_mOp_closed, assumption+, rule Ring.npClose, assumption+)
done
lemma (in Corps) ApproximationTr1:"aa ∈ carrier K ==>
1r ± -a ((1r ± -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 ≠ \<zero>;
0 ≤ (v aa)|] ==> (int N) *a(v aa) ≤ (v (1r ± -a ((1r ± -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 Ring.ring_one[of "K"], simp add:aGroup.ag_r_inv1,
simp add:value_of_zero)
apply (frule_tac n = N in Ring.npClose[of "K" "aa"], assumption+,
frule ApproximationTr[of v "-a (aa^K N)" "N - Suc 0"],
rule aGroup.ag_mOp_closed, assumption+, simp add:val_minus_eq,
subst val_exp_ring[THEN sym, of v], assumption+,
simp add:asprod_pos_pos)
apply (simp add:val_minus_eq, simp add:val_exp_ring[THEN sym])
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 (1r ± -a (b j)))) ∧
g l = (x l) ·r (-a (b l))
--> (nsum K (λj ∈ {h. h ≤ n}. (x j) ·r (1r ± -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+,
simp add:aGroup.ag_mOp_closed, simp add:Ring.ring_r_one,
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 (1r ± -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 (1r ± -a (b u)) else
arbitrary" 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 (1r ± -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_pOp_closed, assumption+, simp add:Ring.ring_one,
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,
simp add:aGroup.ag_mOp_closed,
simp add:Ring.ring_r_one) apply (
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 add:Ring.ring_tOp_closed aGroup.ag_mOp_closed,
simp) apply (
subst aGroup.ag_pOp_assoc[of "K"], assumption+,
rule Ring.ring_tOp_closed, assumption+, simp,
(simp add:aGroup.ag_mOp_closed)+,
subst aGroup.ag_r_inv1, assumption+, simp,
subst aGroup.ag_r_zero, assumption+,
simp add:Ring.ring_tOp_closed aGroup.ag_mOp_closed, simp,
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 (1r ± -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_pOp_closed, assumption+, simp add:Ring.ring_one,
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_pOp_closed, assumption+, simp add:Ring.ring_one,
rule aGroup.ag_mOp_closed, assumption, simp, simp,
rule Ring.ring_tOp_closed, assumption, simp,
rule aGroup.ag_pOp_closed, assumption+, simp add:Ring.ring_one,
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_pOp_closed, assumption+, simp add:Ring.ring_one,
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,
rule aGroup.ag_pOp_closed, assumption+, simp add:Ring.ring_one)
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_pOp_closed, assumption+, simp add:Ring.ring_one,
rule aGroup.ag_mOp_closed, assumption, simp)
apply (subgoal_tac "Σe K (λa. if a ≤ (Suc n) then x a ·r (1r ± -a (b a))
else arbitrary) n ± -a (x l) =
Σe K (λa. if a ≤ n then x a ·r (1r ± -a (b a)) else arbitrary) 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 (1r ± -a (b j)));
g l = (x l) ·r (-a (b l)) |] ==>
(nsum K (λj∈{h. h ≤ n}. (x j) ·r (1r ± -a (b j))) n) ± (-a (x l)) =
nsum K g n"
by (cut_tac eSum_tr[of "n" "x" "b" "l" "g"], simp)
lemma (in Ring) one_m_x_times:"x ∈ carrier R ==>
(1r ± -a x) ·r (nsum R (λj. x^R j) n) = 1r ± -a (x^R (Suc n))"
apply (cut_tac ring_one, cut_tac ring_is_ag,
frule aGroup.ag_mOp_closed[of "R" "x"], assumption+,
frule aGroup.ag_pOp_closed[of "R" "1r" "-a x"], assumption+)
apply (induct_tac n)
apply (simp add:ring_r_one ring_l_one)
apply (simp del:npow_suc,
frule_tac n = "Suc n" in npClose[of "x"],
subst ring_distrib1, assumption+)
apply (rule aGroup.nsum_mem, assumption, rule allI, rule impI,
simp add:npClose, rule npClose, assumption+,
simp del:npow_suc,
thin_tac "(1r ± -a x) ·r Σe R (npow R x) n = 1r ± -a (x^R (Suc n))")
apply (subst ring_distrib2, assumption+,
simp del:npow_suc add:ring_l_one,
subst aGroup.pOp_assocTr43[of R], assumption+,
rule_tac x = "x^R (Suc n)" in aGroup.ag_mOp_closed[of R], assumption+,
rule ring_tOp_closed, rule aGroup.ag_mOp_closed, assumption+)
apply (subst aGroup.ag_l_inv1, assumption+, simp del:npow_suc
add:aGroup.ag_r_zero,
frule_tac x = "-a x" and y = "x^R (Suc n)" in ring_tOp_closed,
assumption+)
apply (rule aGroup.ag_pOp_add_l[of R _ _ "1r"], assumption+,
rule aGroup.ag_mOp_closed, assumption+,
rule npClose, assumption+,
subst ring_inv1_1[THEN sym, of x], assumption,
rule npClose, assumption,
simp,
subst ring_tOp_commute[of x], assumption+, simp)
done
lemma (in Corps) x_pow_fSum_in_Vr:"[|valuation K v; x ∈ carrier (Vr K v)|] ==>
(nsum K (npow K x) n) ∈ carrier (Vr K v)"
apply (frule Vr_ring[of v])
apply (induct_tac n)
apply simp
apply (frule Ring.ring_one[of "Vr K v"])
apply (simp add:Vr_1_f_1)
apply (simp del:npow_suc)
apply (frule Ring.ring_is_ag[of "Vr K v"])
apply (subst Vr_pOp_f_pOp[THEN sym, of v], assumption+)
apply (subst Vr_exp_f_exp[THEN sym, of v], assumption+)
apply (rule Ring.npClose[of "Vr K v"], assumption+)
apply (rule aGroup.ag_pOp_closed[of "Vr K v"], assumption+)
apply (subst Vr_exp_f_exp[THEN sym, of v], assumption+)
apply (rule Ring.npClose[of "Vr K v"], assumption+)
done
lemma (in Corps) val_1mx_pos:"[|valuation K v; x ∈ carrier K;
0 < (v (1r ± -a x))|] ==> v x = 0"
apply (cut_tac field_is_ring, frule Ring.ring_one[of "K"],
frule Ring.ring_is_ag[of "K"])
apply (frule aGroup.ag_mOp_closed[of "K" "x"], assumption+)
apply (frule aGroup.ag_pOp_closed[of "K" "1r" "-a x"], assumption+)
apply (frule aGroup.ag_mOp_closed[of "K" "1r ± -a x"], assumption+)
apply (cut_tac x = x and y = "1r ± -a (1r ± -a x)" and f = v in
eq_elems_eq_val)
apply (subst aGroup.ag_p_inv, assumption+,
subst aGroup.ag_pOp_assoc[THEN sym], assumption+,
rule aGroup.ag_mOp_closed, assumption+,
subst aGroup.ag_inv_inv, assumption+,
subst aGroup.ag_r_inv1, assumption+,
subst aGroup.ag_l_zero, assumption+,
(simp add:aGroup.ag_inv_inv)+,
frule value_less_eq[of v "1r" "-a (1r ± -a x)"],
assumption+)
apply (simp add:val_minus_eq value_of_one,
simp add:value_of_one)
done
lemma (in Corps) val_1mx_pow:"[|valuation K v; x ∈ carrier K;
0 < (v (1r ± -a x))|] ==> 0 < (v (1r ± -a x^K (Suc n)))"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
apply (subst Ring.one_m_x_times[THEN sym, of K x n], assumption+)
apply (frule Ring.ring_one[of "K"],
frule x_pow_fSum_in_Vr[of v x n],
subst val_pos_mem_Vr[THEN sym], assumption+,
frule val_1mx_pos[of "v" "x"], assumption+,
simp)
apply (subst val_t2p, assumption+,
rule aGroup.ag_pOp_closed, assumption+,
simp add:aGroup.ag_mOp_closed, simp add:Vr_mem_f_mem,
frule val_pos_mem_Vr[THEN sym, of v "nsum K (npow K x) n"],
simp add:Vr_mem_f_mem, simp)
apply(frule aadd_le_mono[of "0" "v (nsum K (npow K x) n)" "v (1r ± -a x)"],
simp add:aadd_0_l, simp add:aadd_commute)
done
lemma (in Corps) ApproximationTr3:"[|vals_nonequiv K (Suc n) vv;
∀l ≤ (Suc n). x l ∈ carrier K; j ≤ (Suc n)|] ==>
∃L.(∀N. L < N --> (an m) ≤ (vv j ((Σe K (λk∈{h. h ≤ (Suc n)}.
(x k) ·r (1r ± -a ((1r ± -a (((ΩK vv (Suc n)) k)^K N))^K N)))
(Suc n)) ± -a (x j))))"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
apply (frule_tac vals_nonequiv_valuation[of "Suc n" "vv" j], assumption+)
apply (subgoal_tac "∀N. Σe K (λj∈{h. h ≤ (Suc n)}. (x j) ·r (1r ± -a (1r ±
-a ((ΩK vv (Suc n)) j)^K N)^K N)) (Suc n) ± -a (x j) =
Σe K (λl∈{h. h≤ (Suc n)}. (if l ≠ j then (x l) ·r (1r ± -a (1r ± -a
((ΩK vv (Suc n)) l)^K N)^K N) else (x j) ·r (1r ± -a (1r ±
-a ((ΩK vv (Suc n)) l)^K N)^K N ± -a 1r))) (Suc n)")
apply (simp del:nsum_suc)
apply (thin_tac "∀N. Σe K (λj∈{h. h ≤ (Suc n)}. (x j) ·r (1r ± -a (1r ±
-a (ΩK vv (Suc n)) j^K N)^K N)) (Suc n) ± -a (x j) = Σe K (λl∈{h. h ≤ (Suc n)}. if l ≠ j then (x l) ·r (1r ± -a (1r ± -a (ΩK vv (Suc n)) l^K N)^K N) else (x j) ·r (1r ± -a (1r ± -a (ΩK vv (Suc n)) l^K N)^K N ± -a 1r)) (Suc n)")
prefer 2 apply (rule allI)
apply (rule eSum_minus_x, assumption+)
apply (rule allI, rule impI) apply (rule ApproximationTr0)
apply (simp add:Ostrowski_base_mem) apply assumption
apply (rule ballI, simp)
apply simp
apply (frule Ring.ring_one[of "K"])
apply (cut_tac aa = "(ΩK vv (Suc n)) j" and N = N in
ApproximationTr0)
apply (simp add:Ostrowski_base_mem)
apply (subst aGroup.ag_pOp_assoc, assumption+)
apply (rule aGroup.ag_mOp_closed, assumption+)+
apply (subst aGroup.ag_pOp_commute[of "K" _ "-a 1r"], assumption+)
apply (rule aGroup.ag_mOp_closed, assumption+)+
apply (subst aGroup.ag_pOp_assoc[THEN sym], assumption+)
apply (rule aGroup.ag_mOp_closed, assumption+)+
apply (simp add:aGroup.ag_r_inv1)
apply (subst aGroup.ag_l_zero, assumption+) apply (simp add:aGroup.ag_mOp_closed)
apply simp (* subgoal 2 done **)
apply (subgoal_tac "∃L. ∀N. L < N -->
(∀ja ≤ (Suc n). (an m) ≤ ((vv j o (λl∈{h. h ≤ (Suc n)}. if l ≠ j then (x l) ·r (1r ± -a (1r ± -a ((ΩK vv (Suc n)) l)^K N)^K N) else (x j) ·r (1r ± -a (1r ± -a ((ΩK vv (Suc n)) l)^K N)^K N ± -a 1r))) ja))")
(*
apply (subgoal_tac "∃L. ∀N. L < N --> (an m) ≤ Amin (Suc n) (vv j o (λl∈Nset (Suc n). if l≠j then (x l) ·K (1K +K -K (1K +K -K ((ΩK vv (Suc n)) l)^K N)^K N)
else (x j) ·K (1K +K -K (1K +K -K ((ΩK vv (Suc n)) l)^K N)^K N
+K -K 1K)))")
apply (erule exE)
apply (subgoal_tac "∀N. L < N -->
((an m) ≤ ((vv j) (eΣ K (λl∈Nset (Suc n). (if l ≠ j then (x l) ·K
(1K +K -K (1K +K -K ((ΩK vv (Suc n)) l)^K N)^K N) else (x j) ·K (1K +K -K
(1K +K -K ((ΩK vv (Suc n)) l)^K N)^K N +K -K 1K))) (Suc n))))")
apply blast
*)
apply (erule exE)
apply (rename_tac M)
apply (subgoal_tac "∀N. M < (N::nat) -->
(an m) ≤ (vv j (Σe K (λl∈{h. h ≤ (Suc n)}. (if l ≠ j then
(x l) ·r (1r ± -a (1r ± -a ((ΩK vv (Suc n)) l)^K N)^K N)
else (x j) ·r (1r ± -a (1r ± -a ((ΩK vv (Suc n)) l)^K N)^K N
± -a 1r))) (Suc n)))")
apply blast
apply (rule allI, rule impI)
apply (drule_tac a = N in forall_spec, assumption)
apply (rule value_ge_add[of "vv j" "Suc n" _ "an m"], assumption+)
apply (rule allI, rule impI)
apply (frule Ring.ring_one[of "K"])
apply (case_tac "ja = j", simp)
apply (rule Ring.ring_tOp_closed, assumption+, simp)
apply (rule aGroup.ag_pOp_closed, assumption+)+
apply (rule aGroup.ag_mOp_closed, assumption+)
apply (rule Ring.npClose, assumption)
apply (rule aGroup.ag_pOp_closed, assumption+)
apply (rule aGroup.ag_mOp_closed, assumption)
apply (rule Ring.npClose, assumption)
apply (simp add:Ostrowski_base_mem)
apply (rule aGroup.ag_mOp_closed, assumption+)
apply simp
apply (rule Ring.ring_tOp_closed, assumption+, simp)
apply (rule aGroup.ag_pOp_closed, assumption+)+
apply (rule aGroup.ag_mOp_closed, assumption+)
apply (rule Ring.npClose, assumption)
apply (rule aGroup.ag_pOp_closed, assumption+)
apply (rule aGroup.ag_mOp_closed, assumption)
apply (rule Ring.npClose, assumption)
apply (simp add:Ostrowski_base_mem)
apply assumption
apply (subgoal_tac "∀N. ∀ja ≤ (Suc n). (1r ± -a (1r ± -a
((ΩK vv (Suc n)) ja)^K N)^K N) ∈ carrier K")
apply (subgoal_tac "∀N. (1r ± -a (1r ± -a ((ΩK vv (Suc n)) j)^K N)^K N
± -a 1r) ∈ carrier K")
apply (simp add:val_t2p)
apply (cut_tac multi_inequalityTr0[of "Suc n" "(vv j) o x" "m"])
apply (subgoal_tac "∀ja ≤ (Suc n). (vv j o x) ja ≠ - ∞", simp)
apply (erule exE)
apply (subgoal_tac "∀N. L < N --> (∀ja ≤ (Suc n). (ja ≠ j -->
an m ≤ vv j (x ja) + (vv j (1r ± -a (1r ± -a ((ΩK vv (Suc n)) ja)^K N)^K N)))
∧ (ja = j --> (an m) ≤ vv j (x j) + (vv j (1r ± -a (1r ±
-a ((ΩK vv (Suc n)) j)^K N)^K N ± -a (1r)))))")
apply blast
apply (rule allI, rule impI)+
apply (case_tac "ja = j", simp)
apply (thin_tac "∀N. 1r ± -a (1r ± -a (ΩK vv (Suc n)) j^K N)^K N ± -a 1r ∈
carrier K")
apply (thin_tac "∀l≤Suc n. x l ∈ carrier K")
apply (drule_tac m = N in nat_forall_spec)
apply (drule_tac a = j in forall_spec, assumption,
thin_tac "∀ja≤Suc n. 1r ± -a (1r ± -a (ΩK vv (Suc n)) ja^K N)^K N
∈ carrier K")
apply (cut_tac N = N in ApproximationTr0 [of "(ΩK vv (Suc n)) j"])
apply (simp add:Ostrowski_base_mem)
apply (frule Ring.ring_one[of "K"], frule aGroup.ag_mOp_closed[of "K" "1r"],
assumption) apply (
frule_tac x = "(1r ± -a ((ΩK vv (Suc n)) j)^K N)^K N" in
aGroup.ag_mOp_closed[of "K"], assumption+)
apply (simp only:aGroup.ag_pOp_assoc)
apply (simp only:aGroup.ag_pOp_commute[of "K" _ "-a 1r"])
apply (simp only:aGroup.ag_pOp_assoc[THEN sym])
apply (simp add:aGroup.ag_r_inv1)
apply (simp add:aGroup.ag_l_zero) apply (simp only:val_minus_eq)
apply (thin_tac "(1r ± -a (ΩK vv (Suc n)) j^K N)^K N ∈ carrier K",
thin_tac "-a (1r ± -a (ΩK vv (Suc n)) j^K N)^K N ∈ carrier K")
apply (subst val_exp_ring[THEN sym, of "vv j"], assumption+)
apply (rule aGroup.ag_pOp_closed[of "K"], assumption+)
apply (rule aGroup.ag_mOp_closed[of "K"], assumption)
apply (rule Ring.npClose, assumption+) apply (simp add:Ostrowski_base_mem)
apply (rule Ostrowski_base_npow_not_one) apply simp apply assumption+
apply (drule_tac a = N in forall_spec, assumption)
apply (drule_tac a = j in forall_spec, assumption)
apply (frule Ostrowski_baseTr1[of "n" "vv" "j"], assumption+)
apply (frule_tac n = "N - Suc 0" in val_1mx_pow[of "vv j" "(ΩK vv (Suc n)) j"])
apply (simp add:Ostrowski_base_mem) apply assumption
apply (thin_tac "vv j (x j) ≠ - ∞") apply (simp only:Suc_pred)
apply (thin_tac "0 < vv j (1r ± -a ((ΩK vv (Suc n)) j))")
apply (cut_tac b = "vv j (1r ± -a ((ΩK vv (Suc n)) j)^K N)" and N = N in
asprod_ge) apply assumption apply simp
apply (cut_tac x = "an N" and y = "int N *a vv j (1r ± -a ((ΩK vv (Suc n)) j)^K N)" in aadd_le_mono[of _ _ "vv j (x j)"], assumption)
apply (simp add:aadd_commute)
apply simp
apply (frule_tac aa = "(ΩK vv (Suc n)) ja" and N = N in
ApproximationTr2[of "vv j"])
apply (simp add:Ostrowski_base_mem)
apply (rule Ostrowski_base_nonzero, assumption+)
apply (frule_tac l = ja in Ostrowski_baseTr0[of "n" "vv"], assumption+,
erule conjE)
apply (rotate_tac -1, frule_tac a = j in forall_spec) apply assumption
apply (frule_tac b = j in forball_spec1, simp)
apply (rule aless_imp_le) apply blast
apply (rotate_tac -5,
drule_tac a = N in forall_spec, assumption)
apply (rotate_tac -2,
drule_tac a = ja in forall_spec, assumption) apply (
drule_tac a = ja in forall_spec, assumption)
apply (frule_tac l = ja in Ostrowski_baseTr0[of "n" "vv"], assumption+)
apply (erule conjE, rotate_tac -1,
frule_tac a = j in forall_spec, assumption+)
apply (thin_tac "vv j (x ja) ≠ - ∞")
apply (cut_tac b = "vv j ((ΩK vv (Suc n)) ja)" and N = N in asprod_ge)
apply simp apply simp
apply (frule_tac x = "an N" and y = "int N *a vv j ((ΩK vv (Suc n)) ja)" and
z = "vv j (x ja)" in aadd_le_mono)
apply (frule_tac x = "int N *a vv j ((ΩK vv (Suc n)) ja)" and y = "(vv j)
(1r ± -a (1r ± -a ((ΩK vv (Suc n)) ja)^K N)^K N)" and z = "vv j (x ja)"
in aadd_le_mono)
apply (frule_tac i = "an N + vv j (x ja)" and
j = "int N *a vv j ((ΩK vv (Suc n)) ja) + vv j (x ja)" and
k = "vv j (1r ± -a (1r ± -a ((ΩK vv (Suc n)) ja)^K N)^K N) +
vv j (x ja)" in ale_trans, assumption+)
apply (subst aadd_commute)
apply (frule_tac x = "an m" and y = "vv j (x ja) + an N" in aless_imp_le)
apply (rule_tac j = "vv j (x ja) + an N" in ale_trans[of "an m"],
assumption)
apply (simp add:aadd_commute)
apply (rule allI, rule impI, subst comp_def)
apply (frule_tac a = ja in forall_spec, assumption)
apply (frule_tac x = "x ja" in value_in_aug_inf[of "vv j"], assumption+)
apply (simp add:aug_inf_def)
apply (rule allI)
apply (rule aGroup.ag_pOp_closed, assumption+) apply blast
apply (rule aGroup.ag_mOp_closed, assumption, rule Ring.ring_one, assumption)
apply ((rule allI)+, rule impI)
apply (rule_tac aa = "(ΩK vv (Suc n)) ja" in ApproximationTr1,
simp add:Ostrowski_base_mem)
done
constdefs (structure K)
app_lb :: "[_ , nat, nat => 'b => ant, nat => 'b, nat] =>
(nat => nat)" ("(5Ψ_ _ _ _ _)" [98,98,98,98,99]98)
"ΨK n vv x m == λj∈{h. h ≤ n}. (SOME L. (∀N. L < N -->
(an m) ≤ (vv j (Σe K (λj∈{h. h ≤ n}. (x j) ·r (1r ± -a
(1r ± -a ((ΩK vv n) j)^K N)^K N)) n ± -a (x j)))))"
(** Approximation lower bound **)
lemma (in Corps) app_LB:"[|vals_nonequiv K (Suc n) vv;
∀l≤ (Suc n). x l ∈ carrier K; j ≤ (Suc n)|] ==>
∀N. (ΨK (Suc n) vv x m) j < N --> (an m) ≤
(vv j (Σe K (λj∈{h. h ≤ (Suc n)}. (x j) ·r (1r ± -a (1r ±
-a ((ΩK vv (Suc n)) j)^K N)^K N)) (Suc n) ± -a (x j)))"
apply (frule ApproximationTr3[of "n" "vv" "x" "j" "m"],
assumption+)
apply (simp del:nsum_suc add:app_lb_def) apply (rule allI)
apply (rule someI2_ex) apply assumption+
apply (rule impI) apply blast
done
lemma (in Corps) ApplicationTr4:"[|vals_nonequiv K (Suc n) vv;
∀j∈{h. h ≤ (Suc n)}. x j ∈ carrier K|] ==>
∃l. ∀N. l < N --> (∀j ≤ (Suc n). (an m) ≤
(vv j (Σe K (λj∈{h. h ≤ (Suc n)}. (x j) ·r (1r ± -a (1r ±
-a ((ΩK vv (Suc n)) j)^K N)^K N)) (Suc n) ± -a (x j))))"
apply (subgoal_tac "∀N. (m_max (Suc n) (ΨK (Suc n) vv x m)) < N -->
(∀j≤ (Suc n). (an m) ≤
(vv j (Σe K (λj∈{h. h ≤ (Suc n)}. (x j) ·r (1r ± -a (1r ±
-a ((ΩK vv (Suc n)) j)^K N)^K N)) (Suc n) ± -a (x j))))")
apply blast
apply (rule allI, rule impI)+
apply (frule_tac j = j in app_LB[of "n" "vv" "x" _ "m"],
simp, assumption,
subgoal_tac "(ΨK (Suc n) vv x m) j < N", blast)
apply (frule_tac l = j and n = "Suc n" and f = "ΨK (Suc n) vv x m" in m_max_gt,
frule_tac x = "(ΨK (Suc n) vv x m) j" and
y = "m_max (Suc n) (ΨK (Suc n) vv x m)" and z = N in le_less_trans,
assumption+)
done
theorem (in Corps) Approximation_thm:"[|vals_nonequiv K (Suc n) vv;
∀j≤ (Suc n). (x j) ∈ carrier K|] ==>
∃y∈carrier K. ∀j≤ (Suc n). (an m) ≤ (vv j (y ± -a (x j)))"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
apply (subgoal_tac "∃l. (∀N. l < N --> (∀j ≤ (Suc n). (an m) ≤ ((vv j) ((nsum K (λj∈{h. h ≤ (Suc n)}. (x j) ·r (1r ± -a (1r ± -a ((ΩK vv (Suc n)) j)^K N)^K N)) (Suc n)) ± -a (x j)))))")
apply (erule exE)
apply (rename_tac M)
apply (subgoal_tac "∀j≤ (Suc n). (an m) ≤
(vv j ( (Σe K (λj∈{h. h ≤ (Suc n)}. (x j) ·r (1r ± -a (1r ±
-a ((ΩK vv (Suc n)) j)^K (Suc M))^K (Suc M))) (Suc n)) ± -a (x j)))")
apply (subgoal_tac "Σe K (λj∈{h. h ≤ (Suc n)}. (x j) ·r (1r ±
-a (1r ± -a ((ΩK vv (Suc n)) j)^K (Suc M))^K (Suc M))) (Suc n) ∈ carrier K")
apply blast
apply (rule aGroup.nsum_mem[of "K" "Suc n"], assumption+)
apply (rule allI, rule impI, simp del:nsum_suc npow_suc)
apply (rule Ring.ring_tOp_closed, assumption+, simp,
rule ApproximationTr1, simp add:Ostrowski_base_mem)
apply (subgoal_tac "M < Suc M") apply blast
apply simp
apply (rule ApplicationTr4[of n vv x], assumption+)
apply simp
done
constdefs (structure K)
distinct_pds::"[_, nat, nat => ('b => ant) set] => bool"
"distinct_pds K n P == (∀j≤ n. P j ∈ Pds K) ∧
(∀l≤ n. ∀m≤ n. l ≠ m --> P l ≠ P m)"
(** pds --- prime divisors **)
lemma (in Corps) distinct_pds_restriction:"[|distinct_pds K (Suc n) P|] ==>
distinct_pds K n P"
apply (simp add:distinct_pds_def)
done
lemma (in Corps) ring_n_distinct_prime_divisors:"distinct_pds K n P ==>
Ring (Sr K {x. x∈carrier K ∧ (∀j≤ n. 0 ≤ ((ν K (P j)) x))})"
apply (simp add:distinct_pds_def) apply (erule conjE)
apply (cut_tac field_is_ring)
apply (rule Ring.Sr_ring, assumption+)
apply (subst sr_def)
apply (rule conjI)
apply (rule subsetI) apply simp
apply (rule conjI)
apply (simp add:Ring.ring_one)
apply (rule allI, rule impI)
apply (cut_tac P = "P j" in representative_of_pd_valuation, simp,
simp add:value_of_one)
apply (rule ballI)+
apply simp
apply (frule Ring.ring_is_ag[of "K"]) apply (erule conjE)+
apply (frule_tac x = y in aGroup.ag_mOp_closed[of "K"], assumption+)
apply (frule_tac x = x and y = "-a y" in aGroup.ag_pOp_closed[of "K"],
assumption+)
apply simp
apply (rule conjI)
apply (rule allI, rule impI)
apply (rotate_tac -4, frule_tac a = j in forall_spec, assumption,
rotate_tac -3,
drule_tac a = j in forall_spec, assumption)
apply (cut_tac P = "P j" in representative_of_pd_valuation, simp)
apply (frule_tac v = "νK (P j)" and x = x and y = "-a y" in amin_le_plus,
assumption+)
apply (simp add:val_minus_eq)
apply (frule_tac x = "(νK (P j)) x" and y = "(νK (P j)) y" in amin_ge1[of "0"])
apply simp
apply (rule_tac j = "amin ((νK (P j)) x) ((νK (P j)) y)" and k = "(νK (P j)) (x ± -a y)" in ale_trans[of "0"], assumption+)
apply (simp add:Ring.ring_tOp_closed)
apply (rule allI, rule impI,
cut_tac P = "P j" in representative_of_pd_valuation, simp,
subst val_t2p [where v="νK P j"], assumption+,
rule aadd_two_pos, simp+)
done
lemma (in Corps) distinct_pds_valuation:"[|j ≤ (Suc n);
distinct_pds K (Suc n) P|] ==> valuation K (νK (P j))"
apply (rule_tac P = "P j" in representative_of_pd_valuation)
apply (simp add:distinct_pds_def)
done
lemma (in Corps) distinct_pds_valuation1:"[|0 < n; j ≤ n; distinct_pds K n P|]
==> valuation K (νK (P j))"
apply (rule distinct_pds_valuation[of "j" "n - Suc 0" "P"])
apply simp+
done
lemma (in Corps) distinct_pds_valuation2:"[|j ≤ n; distinct_pds K n P|] ==>
valuation K (νK (P j))"
apply (case_tac "n = 0",
simp add:distinct_pds_def,
subgoal_tac "0 ∈ {0::nat}",
simp add:representative_of_pd_valuation[of "P 0"],
simp)
apply (simp add:distinct_pds_valuation1[of "n"])
done
constdefs
ring_n_pd ::"[('b, 'm) Ring_scheme, nat => ('b => ant) set,
nat ] => ('b, 'm) Ring_scheme"
("(3O_ _ _)" [98,98,99]98)
"OK P n == Sr K {x. x ∈ carrier K ∧
(∀j ≤ n. 0 ≤ ((νK (P j)) x))}"
(** ring defined by n prime divisors **)
lemma (in Corps) ring_n_pd:"distinct_pds K n P ==> Ring (OK P n)"
by (simp add:ring_n_pd_def, simp add:ring_n_distinct_prime_divisors)
lemma (in Corps) ring_n_pd_Suc:"distinct_pds K (Suc n) P ==>
carrier (O K P (Suc n)) ⊆ carrier (OK P n)"
apply (rule subsetI)
apply (simp add:ring_n_pd_def Sr_def)
done
lemma (in Corps) ring_n_pd_pOp_K_pOp:"[|distinct_pds K n P; x∈carrier (OK P n);
y ∈ carrier (OK P n)|] ==> x ±(OK P n) y = x ± y"
apply (simp add:ring_n_pd_def Sr_def)
done
lemma (in Corps) ring_n_pd_tOp_K_tOp:"[|distinct_pds K n P; x ∈carrier (OK P n);
y ∈ carrier (OK P n)|] ==> x ·r(OK P n) y = x ·r y"
apply (simp add:ring_n_pd_def Sr_def)
done
lemma (in Corps) ring_n_eSum_K_eSumTr:"distinct_pds K n P ==>
(∀j≤m. f j ∈ carrier (OK P n)) --> nsum (OK P n) f m = nsum K f m"
apply (induct_tac m)
apply (rule impI, simp)
apply (rule impI, simp,
subst ring_n_pd_pOp_K_pOp, assumption+,
frule_tac n = n in ring_n_pd[of _ "P"],
frule_tac Ring.ring_is_ag, drule sym, simp)
apply (rule aGroup.nsum_mem, assumption+, simp+)
done
lemma (in Corps) ring_n_eSum_K_eSum:"[|distinct_pds K n P;
∀j ≤ m. f j ∈ carrier (OK P n)|] ==> nsum (OK P n) f m = nsum K f m"
apply (simp add:ring_n_eSum_K_eSumTr)
done
lemma (in Corps) ideal_eSum_closed:"[|distinct_pds K n P; ideal (OK P n) I;
∀j ≤ m. f j ∈ I|] ==> nsum K f m ∈ I"
apply (frule ring_n_pd[of "n" "P"]) thm Ring.ideal_nsum_closed
apply (frule_tac n = m in
Ring.ideal_nsum_closed[of "(OK P n)" "I" _ "f"], assumption+)
apply (subst ring_n_eSum_K_eSum [THEN sym, of n P m f], assumption+,
rule allI, simp add:Ring.ideal_subset)
apply assumption
done
constdefs (structure K)
prime_n_pd ::"[_, nat => ('b => ant) set,
nat, nat] => 'b set"
("(4P_ _ _ _)" [98,98,98,99]98)
"PK P n j == {x. x ∈ (carrier (OK P n)) ∧ 0 < ((νK (P j)) x)}"
lemma (in Corps) zero_in_ring_n_pd_zero_K:"distinct_pds K n P ==>
\<zero>(OK P n) = \<zero>K"
apply (simp add:ring_n_pd_def Sr_def)
done
lemma (in Corps) one_in_ring_n_pd_one_K:"distinct_pds K n P ==>
1r(OK P n) = 1r"
apply (simp add:ring_n_pd_def Sr_def)
done
lemma (in Corps) mem_ring_n_pd_mem_K:"[|distinct_pds K n P; x ∈carrier (OK P n)|]
==> x ∈ carrier K"
apply (simp add:ring_n_pd_def Sr_def)
done
lemma (in Corps) ring_n_tOp_K_tOp:"[|distinct_pds K n P; x ∈ carrier (OK P n);
y ∈ carrier (OK P n)|] ==> x ·r(OK P n) y = x ·r y"
apply (simp add:ring_n_pd_def Sr_def)
done
lemma (in Corps) ring_n_exp_K_exp:"[|distinct_pds K n P; x ∈ carrier (OK P n)|]
==> x^K m = x^(OK P n) m"
apply (frule ring_n_pd[of "n" "P"])
apply (induct_tac m) apply simp
apply (simp add:one_in_ring_n_pd_one_K)
apply simp
apply (frule_tac n = na in Ring.npClose[of "OK P n" "x"], assumption+)
apply (simp add:ring_n_tOp_K_tOp)
done
lemma (in Corps) prime_n_pd_prime:"[|distinct_pds K n P; j ≤ n|] ==>
prime_ideal (OK P n) (PK P n j)"
apply (subst prime_ideal_def)
apply (rule conjI)
apply (simp add:ideal_def)
apply (rule conjI)
apply (rule aGroup.asubg_test)
apply (frule ring_n_pd[of "n" "P"], simp add:Ring.ring_is_ag)
apply (rule subsetI, simp add:prime_n_pd_def)
apply (subgoal_tac "\<zero>(OK P n) ∈ PK P n j")
apply blast
apply (simp add:zero_in_ring_n_pd_zero_K)
apply (simp add:prime_n_pd_def)
apply (simp add: ring_n_pd_def Sr_def)
apply (cut_tac field_is_ring, simp add:Ring.ring_zero)
apply (rule conjI) apply (rule allI, rule impI)
apply (cut_tac P = "P ja" in representative_of_pd_valuation,
simp add:distinct_pds_def, simp add:value_of_zero)
apply (cut_tac P = "P j" in representative_of_pd_valuation,
simp add:distinct_pds_def, simp add:value_of_zero)
apply (simp add:ant_0[THEN sym])
apply (rule ballI)+
apply (simp add:prime_n_pd_def) apply (erule conjE)+
apply (frule ring_n_pd [of "n" "P"], frule Ring.ring_is_ag[of "OK P n"])
apply (frule_tac x = b in aGroup.ag_mOp_closed[of "OK P n"], assumption+)
apply (simp add:aGroup.ag_pOp_closed)
apply (thin_tac "Ring (OK P n)") apply (thin_tac "aGroup (OK P n)")
apply (simp add:ring_n_pd_def Sr_def)
apply (erule conjE)+
apply (cut_tac v = "νK (P j)" and x = a and y = "-a b" in
amin_le_plus)
apply (rule_tac P = "P j" in representative_of_pd_valuation,
simp add:distinct_pds_def)
apply assumption+
apply (cut_tac P = "P j" in representative_of_pd_valuation)
apply (simp add:distinct_pds_def)
apply (frule_tac x = "(νK (P j)) a" and y = "(νK (P j)) (-a b)" in
amin_gt[of "0"])
apply (simp add:val_minus_eq)
apply (frule_tac y = "amin ((νK (P j)) a) ((νK (P j)) (-a b))" and
z = "(νK (P j)) ( a ± -a b)" in aless_le_trans[of "0"], assumption+)
apply (rule ballI)+
apply (frule ring_n_pd [of "n" "P"])
apply (frule_tac x = r and y = x in Ring.ring_tOp_closed[of "OK P n"],
assumption+)
apply (simp add:prime_n_pd_def)
apply (cut_tac P = "P j" in representative_of_pd_valuation,
simp add:distinct_pds_def)
apply (thin_tac "Ring (OK P n)")
apply (simp add:prime_n_pd_def ring_n_pd_def Sr_def, (erule conjE)+,
simp add:val_t2p)
apply (subgoal_tac "0 ≤ ((νK (P j)) r)")
apply (simp add:aadd_pos_poss, simp)
apply (rule conjI,
rule contrapos_pp, simp+,
simp add:prime_n_pd_def,
(erule conjE)+, simp add: one_in_ring_n_pd_one_K,
simp add:distinct_pds_def, (erule conjE)+,
cut_tac representative_of_pd_valuation[of "P j"],
simp add:value_of_one, simp)
apply ((rule ballI)+, rule impI)
apply (rule contrapos_pp, simp+, erule conjE,
simp add:prime_n_pd_def, (erule conjE)+,
simp add:ring_n_pd_def Sr_def, (erule conjE)+,
simp add:aneg_less,
frule_tac x = "(νK (P j)) x" in ale_antisym[of _ "0"], simp,
frule_tac x = "(νK (P j)) y" in ale_antisym[of _ "0"], simp)
apply (simp add:distinct_pds_def, (erule conjE)+,
cut_tac representative_of_pd_valuation[of "P j"],
simp add:val_t2p aadd_0_l,
simp)
done
lemma (in Corps) n_eq_val_eq_idealTr:
"[|distinct_pds K n P; x ∈ carrier (OK P n); y ∈ carrier (OK P n);
∀j ≤ n. ((νK (P j)) x) ≤ ((νK (P j)) y)|] ==> Rxa (OK P n) y ⊆ Rxa (OK P n) x"
apply (subgoal_tac "∀j ≤ n. valuation K (νK (P j))")
apply (case_tac "x = \<zero>(OK P n)",
simp add:zero_in_ring_n_pd_zero_K)
apply (simp add:value_of_zero)
apply (subgoal_tac "y = \<zero>", simp,
drule_tac a = n in forall_spec, simp,
drule_tac a=n in forall_spec, simp)
apply (cut_tac inf_ge_any[of "(νK (P n)) y"],
frule ale_antisym[of "(νK (P n)) y" "∞"], assumption+)
apply (rule value_inf_zero, assumption+)
apply (simp add:mem_ring_n_pd_mem_K, assumption)
apply (frule ring_n_pd[of n P])
apply (subgoal_tac "∀j≤n. 0 ≤ ((νK (P j)) (y ·r (xK)))")
apply (subgoal_tac "(y ·r (xK)) ∈ carrier (OK P n)")
apply (cut_tac field_frac_mul[of "y" "x"],
frule Ring.rxa_in_Rxa[of "OK P n" "x" "y ·r (xK)"], assumption+,
simp add:ring_n_pd_tOp_K_tOp[THEN sym],
frule Ring.principal_ideal[of "OK P n" "x"], assumption+)
apply (cut_tac Ring.ideal_cont_Rxa[of "OK P n" "(OK P n) ♦p x" "y"],
assumption+,
simp add:mem_ring_n_pd_mem_K,
simp add:mem_ring_n_pd_mem_K,
simp add:zero_in_ring_n_pd_zero_K)
apply (frule Ring.rxa_in_Rxa[of "OK P n" "x" "y ·r (xK)"], assumption+,
simp add:ring_n_pd_def Sr_def,
(erule conjE)+,
cut_tac field_is_ring, rule Ring.ring_tOp_closed, assumption+,
cut_tac invf_closed1[of x], simp, simp,
simp add:ring_n_pd_def Sr_def)
apply (cut_tac Ring.ring_tOp_closed, assumption+,
cut_tac field_is_ring, assumption+, simp+,
cut_tac invf_closed1[of x], simp, simp)
apply (rule allI, rule impI, drule_tac a = j in forall_spec, assumption+,
cut_tac invf_closed1[of x], simp, erule conjE)
apply (subst val_t2p [where v="νK P j"], simp,
rule mem_ring_n_pd_mem_K[of "n" "P" "y"], assumption+,
frule_tac a = j in forall_spec1, simp,
simp add:zero_in_ring_n_pd_zero_K)
apply (subst value_of_inv [where v="νK P j"], simp,
simp add:ring_n_pd_def Sr_def, assumption+)
apply (frule_tac x = "(νK (P j)) x" and y = "(νK (P j)) y" in ale_diff_pos,
simp add:diff_ant_def,
simp add:mem_ring_n_pd_mem_K[of "n" "P" "x"] zero_in_ring_n_pd_zero_K)
apply (rule allI, rule impI,
simp add:distinct_pds_def, (erule conjE)+,
rule_tac P = "P j" in representative_of_pd_valuation, simp)
done
lemma (in Corps) n_eq_val_eq_ideal:"[|distinct_pds K n P; x ∈ carrier (OK P n);
y ∈ carrier (OK P n); ∀j ≤ n.((νK (P j)) x) = ((νK (P j)) y)|] ==>
Rxa (OK P n) x = Rxa (OK P n) y"
apply (rule equalityI)
apply (subgoal_tac "∀j≤ n. (νK (P j)) y ≤ ((νK (P j)) x)")
apply (rule n_eq_val_eq_idealTr, assumption+)
apply (rule allI, rule impI, simp)
apply (subgoal_tac "∀j≤ n. (νK (P j)) x ≤ ((νK (P j)) y)")
apply (rule n_eq_val_eq_idealTr, assumption+)
apply (rule allI, rule impI)
apply simp
done
constdefs (structure K)
mI_gen :: "[_ , nat => ('r => ant) set, nat, 'r set] => 'r"
"mI_gen K P n I == SOME x. x ∈ I ∧
(∀j ≤ n. (νK (P j)) x = LI K (νK (P j)) I)"
constdefs (structure K)
mL :: "[_, nat => ('r => ant) set, 'r set, nat] => int"
"mL K P I j == tna (LI K (νK (P j)) I)"
lemma (in Corps) mI_vals_nonempty:"[|distinct_pds K n P; ideal (OK P n) I; j≤n|]
==> (νK (P j)) ` I ≠ {}"
apply (frule ring_n_pd[of "n" "P"])
apply (frule Ring.ideal_zero [of "OK P n" "I"], assumption+)
apply (simp add:image_def)
apply blast
done
lemma (in Corps) mI_vals_LB:"[|distinct_pds K n P; ideal (OK P n) I; j ≤ n|] ==>
((νK (P j)) `I) ⊆ LBset (ant 0)"
apply (rule subsetI)
apply (simp add:image_def, erule bexE)
apply (frule ring_n_pd[of "n" "P"])
apply (frule_tac h = xa in Ring.ideal_subset[of "OK P n" "I"], assumption+)
apply (thin_tac "ideal (OK P n) I")
apply (thin_tac "Ring (OK P n)")
apply (simp add: ring_n_pd_def Sr_def) apply (erule conjE)+
apply (drule_tac a = j in forall_spec, simp)
apply (simp add:LBset_def ant_0)
done
lemma (in Corps) mL_hom:"[|distinct_pds K n P; ideal (OK P n) I;
I ≠ {\<zero>(OK P n)}; I ≠ carrier (OK P n)|] ==>
∀j ≤ n. mL K P I j ∈ Zset"
apply (rule allI, rule impI)
apply (simp add:mL_def LI_def)
apply (simp add:Zset_def)
done
lemma (in Corps) ex_Zleast_in_mI:"[|distinct_pds K n P; ideal (OK P n) I; j ≤ n|]
==> ∃x∈I. (νK (P j)) x = LI K (νK (P j)) I"
apply (frule_tac j = j in mI_vals_nonempty[of "n" "P" "I"], assumption+)
apply (frule_tac j = j in mI_vals_LB[of "n" "P" "I"], assumption+)
apply (frule_tac A = "(νK (P j)) ` I" and z = 0 in AMin_mem, assumption+)
apply (simp add:LI_def)
apply (thin_tac "(νK (P j)) ` I ⊆ LBset (ant 0)")
apply (simp add:image_def, erule bexE)
apply (drule sym)
apply blast
done
lemma (in Corps) val_LI_pos:"[|distinct_pds K n P; ideal (OK P n) I;
I ≠ {\<zero>(OK P n)}; j ≤ n|] ==> 0 ≤ LI K (νK (P j)) I"
apply (frule_tac j = j in mI_vals_nonempty[of n P I], assumption+)
apply (frule_tac j = j in mI_vals_LB[of n P I], assumption+)
apply (frule_tac A = "(νK (P j)) ` I" and z = 0 in AMin_mem, assumption+)
apply (simp add:LI_def)
apply (frule subsetD[of "(νK (P j)) ` I" "LBset (ant 0)" "AMin ((νK (P j)) ` I)"], assumption+)
apply (simp add:LBset_def ant_0)
done
lemma (in Corps) val_LI_noninf:"[|distinct_pds K n P; ideal (OK P n) I;
I ≠ {\<zero>(OK P n)}; j ≤ n|] ==> LI K (νK (P j)) I ≠ ∞"
apply (frule_tac j = j in mI_vals_nonempty[of "n" "P" "I"], assumption+)
apply (frule_tac j = j in mI_vals_LB[of "n" "P" "I"], assumption+)
apply (frule_tac A = "(νK (P j)) ` I" and z = 0 in AMin, assumption+)
apply (thin_tac "(νK (P j)) ` I ⊆ LBset (ant 0)",
thin_tac "(νK (P j) ) ` I ≠ {}")
apply (frule ring_n_pd[of "n" "P"])
apply (frule Ring.ideal_zero[of "OK P n" "I"], assumption+)
apply (erule conjE, simp add:LI_def)
apply (frule singleton_sub[of "\<zero>OK P n" "I"])
apply (frule sets_not_eq[of "I" "{\<zero>OK P n}"],
assumption+, erule bexE)
apply (simp add:zero_in_ring_n_pd_zero_K)
apply (subgoal_tac "∃x∈I. AMin ((νK (P j)) ` I) = (νK (P j)) x",
erule bexE) apply simp
apply (drule_tac b = a in forball_spec1, assumption)
apply (thin_tac "AMin ((νK (P j)) ` I) = (νK (P j)) x")
apply (frule_tac h = a in Ring.ideal_subset[of "OK P n" "I"], assumption+)
apply (frule_tac x = a in mem_ring_n_pd_mem_K[of n P], assumption+)
apply (simp add:distinct_pds_def, (erule conjE)+)
apply (cut_tac representative_of_pd_valuation[of "P j"])
defer apply simp apply blast
apply (frule_tac x = a in val_nonzero_z[of "νK (P j)"], assumption+,
erule exE, simp)
apply (thin_tac "∀l ≤ n. ∀m ≤ n. l ≠ m --> P l ≠ P m",
thin_tac "(νK (P j)) a = ant z")
apply (rule contrapos_pp, simp+)
apply (cut_tac x = "ant z" in inf_ge_any)
apply (frule_tac x = "ant z" in ale_antisym[of _ "∞"], assumption+)
apply simp
done
lemma (in Corps) Zleast_in_mI_pos:"[|distinct_pds K n P; ideal (OK P n) I;
I ≠ {\<zero>(OK P n)}; j ≤ n|] ==> 0 ≤ mL K P I j"
apply (simp add:mL_def)
apply (frule ex_Zleast_in_mI[of "n" "P" "I" "j"], assumption+,
erule bexE, frule sym, thin_tac "(νK (P j)) x = LI K (νK (P j)) I")
apply (subgoal_tac "LI K (νK (P j)) I ≠ ∞", simp)
apply (thin_tac "LI K (νK (P j)) I = (νK (P j)) x")
apply (frule ring_n_pd[of "n" "P"])
apply (frule_tac h = x in Ring.ideal_subset[of "OK P n" "I"], assumption+)
apply (thin_tac "ideal (OK P n) I")
apply (thin_tac "Ring (OK P n)")
apply (simp add: ring_n_pd_def Sr_def) apply (erule conjE)
apply (drule_tac a = j in forall_spec, assumption)
apply (simp add:apos_tna_pos)
apply (rule val_LI_noninf, assumption+)
done
lemma (in Corps) Zleast_mL_I:"[|distinct_pds K n P; ideal (OK P n) I; j ≤ n;
I ≠ {\<zero>(OK P n)}; x ∈ I|] ==> ant (mL K P I j) ≤ ((νK (P j)) x)"
apply (frule val_LI_pos[of "n" "P" "I" "j"], assumption+)
apply (frule apos_neq_minf[of "LI K (νK (P j)) I"])
apply (frule val_LI_noninf[of "n" "P" "I" "j"], assumption+)
apply (simp add:mL_def LI_def)
apply (simp add:ant_tna)
apply (frule Zleast_in_mI_pos[of "n" "P" "I" "j"], assumption+)
apply (frule mI_vals_nonempty[of "n" "P" "I" "j"], assumption+)
apply (frule mI_vals_LB[of "n" "P" "I" "j"], assumption+)
apply (frule AMin[of "(νK (P j)) `I" "0"], assumption+)
apply (erule conjE)
apply (frule Zleast_in_mI_pos[of "n" "P" "I" "j"], assumption+)
apply (simp add:mL_def LI_def)
done
lemma (in Corps) Zleast_LI:"[|distinct_pds K n P; ideal (OK P n) I; j ≤ n;
I ≠ {\<zero>(OK P n)}; x ∈ I|] ==> (LI K (νK (P j)) I) ≤ ((νK (P j)) x)"
apply (frule mI_vals_nonempty[of "n" "P" "I" "j"], assumption+)
apply (frule mI_vals_LB[of "n" "P" "I" "j"], assumption+)
apply (frule AMin[of "(νK (P j)) `I" "0"], assumption+)
apply (erule conjE)
apply (simp add:LI_def)
done
lemma (in Corps) mpdiv_vals_nonequiv:"distinct_pds K n P ==>
vals_nonequiv K n (λj. νK (P j)) "
apply (simp add:vals_nonequiv_def)
apply (rule conjI)
apply (simp add:valuations_def)
apply (rule allI, rule impI)
apply (rule representative_of_pd_valuation,
simp add:distinct_pds_def)
apply ((rule allI, rule impI)+, rule impI)
apply (simp add:distinct_pds_def, erule conjE)
apply (rotate_tac 4) apply (
drule_tac a = j in forall_spec, assumption)
apply (rotate_tac -1,
drule_tac a = l in forall_spec, assumption, simp)
apply (simp add:distinct_p_divisors)
done
constdefs (structure K)
KbaseP ::"[_, nat => ('r => ant) set, nat] =>
(nat => 'r) => bool"
"KbaseP K P n f == (∀j ≤ n. f j ∈ carrier K) ∧
(∀j ≤ n. ∀l ≤ n. (νK (P j)) (f l) = (δj l))"
Kbase :: "[_, nat, nat => ('r => ant) set]
=> (nat => 'r)" ("(3Kb_ _ _)" [95,95,96]95)
"KbK n P == SOME f. KbaseP K P n f"
lemma (in Corps) KbaseTr:"distinct_pds K n P ==> ∃f. KbaseP K P n f"
apply (simp add: KbaseP_def)
apply (frule mpdiv_vals_nonequiv[of "n" "P"])
apply (case_tac "n = 0")
apply (simp add:vals_nonequiv_def valuations_def)
apply (simp add:distinct_pds_def)
apply (frule n_val_n_val1[of "P 0"])
apply (frule n_val_surj[of "νK (P 0)"])
apply (erule bexE)
apply (subgoal_tac " ((λj∈{0::nat}. x) (0::nat)) ∈ carrier K ∧
(νK (P 0)) ((λj∈{0::nat}. x) (0::nat)) = (δ0 0)")
apply blast
apply (rule conjI)
apply simp apply (simp add:Kronecker_delta_def)
apply (cut_tac Approximation1_5[of "n - Suc 0" "λj. νK (P j)"])
apply simp
apply simp+
apply (rule allI, rule impI)
apply (rule n_val_n_val1 )
apply (simp add:distinct_pds_def)
done
lemma (in Corps) KbaseTr1:"distinct_pds K n P ==> KbaseP K P n (KbK n P )"
apply (subst Kbase_def)
apply (frule KbaseTr[of n P])
apply (erule exE)
apply (simp add:someI)
done
lemma (in Corps) Kbase_hom:"distinct_pds K n P ==>
∀j ≤ n. (KbK n P) j ∈ carrier K"
apply (frule KbaseTr1[of "n" "P"])
apply (simp add:KbaseP_def)
done
lemma (in Corps) Kbase_Kronecker:"distinct_pds K n P ==>
∀j ≤ n. ∀l ≤ n. (νK (P j)) ((KbK n P) l) = δj l"
apply (frule KbaseTr1[of n P])
apply (simp add:KbaseP_def)
done
lemma (in Corps) Kbase_nonzero:"distinct_pds K n P ==>
∀j ≤ n. (KbK n P) j ≠ \<zero>"
apply (rule allI, rule impI)
apply (frule Kbase_Kronecker[of n P])
apply (subgoal_tac "(νK (P j)) ((KbK n P) j) = δj j")
apply (thin_tac "∀j≤n. (∀l≤n. ((νK P j) ((KbK n P) l)) = δj l)")
apply (simp add:Kronecker_delta_def)
apply (rule contrapos_pp, simp+)
apply (cut_tac P = "P j" in representative_of_pd_valuation)
apply (simp add:distinct_pds_def)
apply (simp only:value_of_zero, simp only:ant_1[THEN sym],
frule sym, thin_tac " ∞ = ant 1", simp del:ant_1)
apply simp
done
lemma (in Corps) Kbase_hom1:"distinct_pds K n P ==>
∀j ≤ n. (KbK n P) j ∈ carrier K - {\<zero>}"
apply (rule allI, rule impI)
apply (frule Kbase_hom[of n P])
apply (simp add:funcset_mem Kbase_nonzero)
done
constdefs (structure K)
Zl_mI ::"[_, nat => ('b => ant) set, 'b set]
=> nat => 'b"
"Zl_mI K P I j == SOME x. (x ∈ I ∧ ( (νK (P j)) x = LI K (νK (P j)) I))"
lemma (in Corps) value_Zl_mI:"[|distinct_pds K n P; ideal (OK P n) I; j ≤ n|]
==> (Zl_mI K P I j ∈ I) ∧ (νK (P j)) (Zl_mI K P I j) = LI K (νK (P j)) I"
apply (subgoal_tac "∃x. (x ∈ I ∧ ((νK (P j)) x = LI K (νK (P j)) I))")
apply (subst Zl_mI_def)+
apply (rule someI2_ex, assumption+)
apply (frule ex_Zleast_in_mI[of "n" "P" "I" "j"], assumption+)
apply (erule bexE, blast)
done
lemma (in Corps) Zl_mI_nonzero:"[|distinct_pds K n P; ideal (OK P n) I;
I ≠ {\<zero>(OK P n)}; j ≤ n|] ==> Zl_mI K P I j ≠ \<zero>"
apply (case_tac "n = 0")
apply (simp add:distinct_pds_def)
apply (frule representative_of_pd_valuation[of "P 0"])
apply (subgoal_tac "OK P 0 = Vr K (νK (P 0))")
apply (subgoal_tac "Zl_mI K P I 0 = Ig K (νK (P 0)) I")
apply simp apply (simp add:Ig_nonzero)
apply (simp add:Ig_def Zl_mI_def)
apply (simp add:ring_n_pd_def Vr_def)
apply (simp)
apply (frule value_Zl_mI[of n P I j], assumption+)
apply (erule conjE)
apply (rule contrapos_pp, simp+)
apply (frule distinct_pds_valuation1[of n j P], assumption+)
apply (simp add:value_of_zero)
apply (simp add:zero_in_ring_n_pd_zero_K)
apply (frule singleton_sub[of "\<zero>" "I"],
frule sets_not_eq[of "I" "{\<zero>}"], assumption,
erule bexE, simp)
apply (frule_tac x = a in Zleast_mL_I[of "n" "P" "I" "j"], assumption+)
apply (frule_tac x = a in val_nonzero_z[of "νK (P j)"])
apply (frule ring_n_pd[of "n" "P"])
apply (frule_tac h = a in Ring.ideal_subset[of "OK P n" "I"], assumption+)
apply (simp add:mem_ring_n_pd_mem_K) apply assumption
apply (simp add:zero_in_ring_n_pd_zero_K) apply assumption
apply (frule val_LI_noninf[THEN not_sym, of "n" "P" "I" "j"], assumption+)
apply (simp add:zero_in_ring_n_pd_zero_K) apply assumption
apply simp
done
lemma (in Corps) Zl_mI_mem_K:"[|distinct_pds K n P; ideal (OK P n) I; l ≤ n|]
==> (Zl_mI K P I l) ∈ carrier K"
apply (frule value_Zl_mI[of "n" "P" "I" "l"], assumption+)
apply (erule conjE)
apply (frule ring_n_pd[of "n" "P"])
apply (frule Ring.ideal_subset[of "OK P n" "I" "Zl_mI K P I l"], assumption+)
apply (simp add:mem_ring_n_pd_mem_K[of "n" "P" "Zl_mI K P I l"])
done
constdefs (structure K)
mprod_exp::"[_, nat => int, nat => 'b, nat]
=> 'b"
"mprod_exp K e f n == nprod K (λj. ((f j)K(e j))) n"
lemma (in Corps) mprod_expR_memTr:"(∀j≤n. f j ∈ carrier K) -->
mprod_expR K e f n ∈ carrier K"
apply (cut_tac field_is_ring)
apply (induct_tac n)
apply (rule impI, simp)
apply (simp add:mprod_expR_def)
apply (cut_tac Ring.npClose[of K "f 0" "e 0"], assumption+)
apply (rule impI)
apply simp
apply (subst Ring.mprodR_Suc, assumption+)
apply (rule univar_func_test, rule ballI, simp)
apply (rule univar_func_test, rule ballI, simp)
apply (rule Ring.ring_tOp_closed[of K], assumption+)
apply (rule Ring.npClose, assumption+)
apply simp
done
lemma (in Corps) mprod_expR_mem:"∀j ≤ n. f j ∈ carrier K ==>
mprod_expR K e f n ∈ carrier K"
apply (cut_tac field_is_ring)
apply (cut_tac Ring.mprod_expR_memTr[of K e n f])
apply simp
apply (subgoal_tac "f ∈ {j. j ≤ n} -> carrier K", simp+)
apply (rule univar_func_test, rule ballI, simp)
apply assumption
done
lemma (in Corps) mprod_Suc:"[| ∀j≤(Suc n). e j ∈ Zset;
∀j ≤ (Suc n). f j ∈ (carrier K - {\<zero>})|] ==>
mprod_exp K e f (Suc n) = (mprod_exp K e f n) ·r ((f (Suc n))K(e (Suc n)))"
apply (simp add:mprod_exp_def)
done
lemma (in Corps) mprod_memTr:"
(∀j ≤ n. e j ∈ Zset) ∧ (∀j ≤ n. f j ∈ ((carrier K) - {\<zero>})) -->
(mprod_exp K e f n) ∈ ((carrier K) - {\<zero>})"
apply (induct_tac n)
apply (simp, rule impI, (erule conjE)+,
simp add:mprod_exp_def, simp add:npowf_mem,
simp add:field_potent_nonzero1)
apply (rule impI, simp, erule conjE,
cut_tac field_is_ring, cut_tac field_is_idom,
erule conjE, simp add:mprod_Suc)
apply (rule conjI)
apply (rule Ring.ring_tOp_closed[of "K"], assumption+,
simp add:npowf_mem)
apply (rule Idomain.idom_tOp_nonzeros, assumption+,
simp add:npowf_mem, assumption,
simp add:field_potent_nonzero1)
done
lemma (in Corps) mprod_mem:"[|∀j ≤ n. e j ∈ Zset; ∀j ≤ n. f j ∈ ((carrier K) - {\<zero>})|] ==> (mprod_exp K e f n) ∈ ((carrier K) - {\<zero>})"
apply (cut_tac mprod_memTr[of n e f]) apply simp
done
lemma (in Corps) mprod_mprodR:"[|∀j ≤ n. e j ∈ Zset; ∀j ≤ n. 0 ≤ (e j);
∀j ≤ n. f j ∈ ((carrier K) - {\<zero>})|] ==>
mprod_exp K e f n = mprod_expR K (nat o e) f n"
apply (cut_tac field_is_ring)
apply (simp add:mprod_exp_def mprod_expR_def)
apply (rule Ring.nprod_eq, assumption+)
apply (rule allI, rule impI, simp add:npowf_mem)
apply (rule allI, rule impI, rule Ring.npClose, assumption+, simp)
apply (rule allI, rule impI)
apply (simp add:npowf_def)
done
subsection "representation of an ideal I as a product of prime ideals"
lemma (in Corps) ring_n_mprod_mprodRTr:"distinct_pds K n P ==>
(∀j ≤ m. e j ∈ Zset) ∧ (∀j ≤ m. 0 ≤ (e j)) ∧
(∀j ≤ m. f j ∈ carrier (OK P n)-{\<zero>(OK P n)}) -->
mprod_exp K e f m = mprod_expR (OK P n) (nat o e) f m"
apply (frule ring_n_pd[of n P])
apply (induct_tac m)
apply (rule impI, (erule conjE)+,
simp add:mprod_exp_def mprod_expR_def)
apply (erule conjE, simp add:npowf_def, simp add:ring_n_exp_K_exp)
apply (rule impI, (erule conjE)+, simp)
apply (subst mprod_Suc, assumption+,
rule allI, rule impI,
simp add:mem_ring_n_pd_mem_K,
simp add:zero_in_ring_n_pd_zero_K)
apply (subst Ring.mprodR_Suc, assumption+,
rule univar_func_test, rule ballI, simp add:cmp_def,
rule univar_func_test, rule ballI, simp)
apply (simp add:ring_n_pd, simp add:npowf_def,
simp add:ring_n_exp_K_exp)
apply (subst ring_n_tOp_K_tOp, assumption+,
rule Ring.mprod_expR_mem, simp add:ring_n_pd,
rule univar_func_test, rule ballI, simp,
rule univar_func_test, rule ballI, simp)
apply (rule Ring.npClose, simp add:ring_n_pd, simp, simp)
done
lemma (in Corps) ring_n_mprod_mprodR:"[|distinct_pds K n P; ∀j ≤ m. e j ∈ Zset;
∀j ≤ m. 0 ≤ (e j); ∀j ≤ m. f j ∈ carrier (OK P n)-{\<zero>(OK P n)}|]
==> mprod_exp K e f m = mprod_expR (OK P n) (nat o e) f m"
apply (simp add:ring_n_mprod_mprodRTr)
done
lemma (in Corps) value_mprod_expTr:"valuation K v ==>
(∀j ≤ n. e j ∈ Zset) ∧ (∀j ≤ n. f j ∈ (carrier K - {\<zero>})) -->
v (mprod_exp K e f n) = ASum (λj. (e j) *a (v (f j))) n"
apply (induct_tac n)
apply simp
apply (rule impI, erule conjE)
apply(simp add:mprod_exp_def val_exp)
apply (rule impI, erule conjE)
apply simp
apply (subst mprod_Suc, assumption+)
apply (rule allI, rule impI, simp)
apply (subst val_t2p[of v], assumption+)
apply (cut_tac n = "n" in mprod_mem[of _ e f],
(rule allI, rule impI, simp)+, simp)
apply (simp add:npowf_mem, simp add:field_potent_nonzero1)
apply (simp add:val_exp[THEN sym, of "v"])
done
lemma (in Corps) value_mprod_exp:"[|valuation K v; ∀j ≤ n. e j ∈ Zset;
∀j ≤ n. f j ∈ (carrier K - {\<zero>})|] ==>
v (mprod_exp K e f n) = ASum (λj. (e j) *a (v (f j))) n"
apply (simp add:value_mprod_expTr)
done
lemma (in Corps) mgenerator0_1:"[|distinct_pds K (Suc n) P;
ideal (OK P (Suc n)) I; I ≠ {\<zero>(OK P (Suc n))};
I ≠ carrier (OK P (Suc n)); j ≤ (Suc n)|] ==>
((νK (P j)) (mprod_exp K (mL K P I) (KbK (Suc n) P) (Suc n))) =
((νK (P j)) (Zl_mI K P I j))"
apply (frule distinct_pds_valuation[of j n P], assumption+)
apply (frule mL_hom[of "Suc n" "P" "I"], assumption+)
apply (frule Kbase_hom1[of "Suc n" "P"])
apply (frule value_mprod_exp[of "νK (P j)" "Suc n" "mL K P I"
"KbK (Suc n) P"], assumption+)
apply (simp del:ASum_Suc)
apply (thin_tac "(νK (P j)) (mprod_exp K (mL K P I) (KbK (Suc n) P) (Suc n)) =
ASum (λja. (mL K P I ja) *a (νK (P j)) ((KbK (Suc n) P) ja)) (Suc n)")
apply (subgoal_tac "ASum (λja. (mL K P I ja) *a
((νK (P j)) ((KbK (Suc n) P) ja))) (Suc n) =
ASum (λja. (mL K P I ja) *a (δj ja)) (Suc n)")
apply (simp del:ASum_Suc)
apply (subgoal_tac "∀h ≤ (Suc n). (λja. (mL K P I ja) *a (δj ja)) h ∈ Z∞")
apply (cut_tac eSum_single[of "Suc n" "λja. (mL K P I ja) *a (δj ja)" "j"])
apply simp
apply (simp add:Kronecker_delta_def asprod_n_0)
apply (rotate_tac -1, drule not_sym)
apply (simp add:mL_def[of "K" "P" "I" "j"])
apply (frule val_LI_noninf[of "Suc n" "P" "I" "j"], assumption+)
apply (rule not_sym, simp, simp)
apply (frule val_LI_pos[of "Suc n" "P" "I" "j"], assumption+,
rotate_tac -2, frule not_sym, simp, simp)
apply (frule apos_neq_minf[of "LI K (νK (P j)) I"])
apply (simp add:ant_tna)
apply (simp add:value_Zl_mI[of "Suc n" "P" "I" "j"])
apply (rule allI, rule impI)
apply (simp add:Kdelta_in_Zinf, simp)
apply (rule ballI, simp)
apply (simp add:Kronecker_delta_def, erule conjE)
apply (simp add:asprod_n_0)
apply (rule allI, rule impI)
apply (simp add:Kdelta_in_Zinf)
apply (frule Kbase_Kronecker[of "Suc n" "P"])
apply (rule ASum_eq,
rule allI, rule impI,
simp add:Kdelta_in_Zinf,
rule allI, rule impI,
simp add:Kdelta_in_Zinf)
apply (rule allI, rule impI) apply simp
done
lemma (in Corps) mgenerator0_2:"[| 0 < n; distinct_pds K n P; ideal (OK P n) I;
I ≠ {\<zero>(OK P n)}; I ≠ carrier (OK P n); j ≤ n|] ==>
((νK (P j)) (mprod_exp K (mL K P I) (KbK n P) n)) = ((νK (P j)) (Zl_mI K P I j))"
apply (cut_tac mgenerator0_1[of "n - Suc 0" "P" "I" "j"])
apply simp+
done
lemma (in Corps) mgenerator1:"[|distinct_pds K n P; ideal (OK P n) I;
I ≠ {\<zero>(OK P n)}; I ≠ carrier (OK P n); j ≤ n|] ==>
((νK (P j)) (mprod_exp K (mL K P I) (KbK n P) n)) = ((νK (P j)) (Zl_mI K P I j))"
apply (case_tac "n = 0",
frule value_Zl_mI[of "n" "P" "I" "j"], assumption+,
frule val_LI_noninf[of "n" "P" "I" "j"], assumption+,
frule val_LI_pos[of "n" "P" "I" "j"], assumption+,
frule apos_neq_minf[of "LI K (νK (P j)) I"],
simp add:distinct_pds_def, erule conjE)
apply (cut_tac representative_of_pd_valuation[of "P j"], simp+,
simp add:mprod_exp_def,
subst val_exp[THEN sym, of "νK (P 0)" "(KbK 0 P) 0"], assumption+,
cut_tac Kbase_hom[of "0" "P"], simp,
simp add:distinct_pds_def,
cut_tac Kbase_nonzero[of "0" "P"], simp+,
simp add:distinct_pds_def)
apply (cut_tac Kbase_nonzero[of "0" "P"], simp add:distinct_pds_def)
apply (cut_tac Kbase_Kronecker[of "0" "P"], simp add:distinct_pds_def)
apply (simp add:Kronecker_delta_def, simp add:mL_def, simp add:ant_tna)
apply (simp add:distinct_pds_def)+
apply (cut_tac mgenerator0_2[of "n" "P" "I" "j"], simp+)
apply (simp add:distinct_pds_def) apply simp+
done
lemma (in Corps) mgenerator2Tr1:"[|0 < n; j ≤ n; k ≤ n; distinct_pds K n P|] ==>
(νK (P j)) (mprod_exp K (λl. γk l ) (KbK n P) n) = (γk j) *a (δj j)"
apply (frule distinct_pds_valuation1[of "n" "j" "P"], assumption+)
apply (frule K_gamma_hom[of k n])
apply (subgoal_tac "∀j ≤ n. (KbK n P) j ∈ carrier K - {\<zero>}")
apply (simp add:value_mprod_exp[of "νK (P j)" n "K_gamma k" "(KbK n P)"])
apply (subgoal_tac "ASum (λja. (γk ja) *a (νK (P j)) ((KbK n P) ja)) n
= ASum (λja. (((γk ja) *a (δj ja)))) n")
apply simp
apply (subgoal_tac "∀j ≤ n. (λja. (γk ja) *a (δj ja)) j ∈ Z∞")
apply (cut_tac eSum_single[of n "λja. ((γk ja) *a (δj ja))" "j"], simp)
apply (rule allI, rule impI, simp add:Kronecker_delta_def,
rule impI, simp add:asprod_n_0 Zero_in_aug_inf, assumption+)
apply (rule ballI, simp)
apply (simp add:K_gamma_def, rule impI, simp add:Kronecker_delta_def)
apply (rule allI, rule impI)
apply (simp add:Kronecker_delta_def, simp add:K_gamma_def)
apply (simp add:ant_0 Zero_in_aug_inf)
apply (cut_tac z_in_aug_inf[of 1], simp add:ant_1)
apply (rule ASum_eq)
apply (rule allI, rule impI)
apply (simp add:K_gamma_def, simp add:Zero_in_aug_inf)
apply (rule impI, rule value_in_aug_inf, assumption+, simp)
apply (simp add:K_gamma_def Zero_in_aug_inf Kdelta_in_Zinf1)
apply (rule allI, rule impI)
apply (simp add:Kbase_Kronecker[of "n" "P"])
apply (rule Kbase_hom1, assumption+)
done
lemma (in Corps) mgenerator2Tr2:"[|0 < n; j ≤ n; k ≤ n; distinct_pds K n P|] ==>
(νK (P j)) ((mprod_exp K (λl. γk l ) (KbK n P) n)Km)= ant (m * (γk j))"
apply (frule K_gamma_hom[of k n])
apply (frule Kbase_hom1[of "n" "P"])
apply (frule mprod_mem[of n "K_gamma k" "KbK n P"], assumption+)
apply (frule distinct_pds_valuation1[of "n" "j" "P"], assumption+)
apply (simp, erule conjE)
apply (simp add:val_exp[THEN sym])
apply (simp add:mgenerator2Tr1)
apply (simp add:K_gamma_def Kronecker_delta_def)
apply (rule impI)
apply (simp add:asprod_def a_z_z)
done
lemma (in Corps) mgenerator2Tr3_1:"[|0 < n; j ≤ n; k ≤ n; j = k;
distinct_pds K n P|] ==>
(νK (P j)) ((mprod_exp K (λl. (γk l)) (KbK n P) n)Km) = 0"
apply (simp add:mgenerator2Tr2) apply (simp add:K_gamma_def)
done
lemma (in Corps) mgenerator2Tr3_2:"[|0 < n; j ≤ n; k ≤ n; j ≠ k;
distinct_pds K n P|] ==>
(νK (P j)) ((mprod_exp K (λl. (γk l)) (KbK n P) n)Km) = ant m"
apply (simp add:mgenerator2Tr2) apply (simp add:K_gamma_def)
done
lemma (in Corps) mgeneratorTr4:"[|0 < n; distinct_pds K n P; ideal (OK P n) I;
I ≠ {\<zero>OK P n}; I ≠ carrier (OK P n)|] ==>
mprod_exp K (mL K P I) (KbK n P) n ∈ carrier (OK P n)"
apply (subst ring_n_pd_def)
apply (simp add:Sr_def)
apply (frule mL_hom[of "n" "P" "I"], assumption+)
apply (frule mprod_mem[of n "mL K P I" "KbK n P"])
apply (rule Kbase_hom1, assumption+)
apply (simp add:mprod_mem)
apply (rule allI, rule impI)
apply (simp add:mgenerator1)
apply (simp add:value_Zl_mI)
apply (simp add:val_LI_pos)
done
constdefs (structure K)
m_zmax_pdsI_hom::"[_, nat => ('b => ant) set, 'b set] => nat => int"
"m_zmax_pdsI_hom K P I == λj. tna (AMin ((νK (P j)) ` I))"
m_zmax_pdsI ::"[_, nat, nat => ('b => ant) set, 'b set] => int"
"m_zmax_pdsI K n P I == (m_zmax n (m_zmax_pdsI_hom K P I)) + 1"
lemma (in Corps) value_Zl_mI_pos:"[|0 < n; distinct_pds K n P; ideal (OK P n) I;
I ≠ {\<zero>(OK P n)}; I ≠ carrier (OK P n); j ≤ n; l ≤ n|] ==>
0 ≤ ((νK (P j)) (Zl_mI K P I l))"
apply (frule value_Zl_mI[of "n" "P" "I" "l"], assumption+)
apply (erule conjE)
apply (frule ring_n_pd[of "n" "P"])
apply (frule Ring.ideal_subset[of "OK P n" "I" "Zl_mI K P I l"], assumption+)
apply (thin_tac "ideal (OK P n) I")
apply (thin_tac "I ≠ {\<zero>OK P n}")
apply (thin_tac "I ≠ carrier (OK P n)")
apply (thin_tac "Ring (OK P n)")
apply (simp add:ring_n_pd_def Sr_def)
done
lemma (in Corps) value_mI_genTr1:"[|0 < n; distinct_pds K n P; ideal (OK P n) I;
I ≠ {\<zero>OK P n}; I ≠ carrier (OK P n); j ≤ n|] ==>
(mprod_exp K (K_gamma j) (KbK n P) n)K(m_zmax_pdsI K n P I) ∈ carrier K"
apply (frule K_gamma_hom[of "j" "n"]) thm mprod_mem
apply (frule mprod_mem[of n "K_gamma j" "KbK n P"])
apply (rule Kbase_hom1, assumption+)
apply (rule npowf_mem)
apply simp+
done
lemma (in Corps) value_mI_genTr1_0:"[|0 < n; distinct_pds K n P;
ideal (OK P n) I; I ≠ {\<zero>OK P n}; I ≠ carrier (OK P n); j ≤ n|]
==> (mprod_exp K (K_gamma j) (KbK n P) n) ∈ carrier K"
apply (frule K_gamma_hom[of "j" "n"])
apply (frule mprod_mem[of n "K_gamma j" "KbK n P"])
apply (rule Kbase_hom1, assumption+)
apply simp
done
lemma (in Corps) value_mI_genTr2:"[|0 < n; distinct_pds K n P; ideal (OK P n) I;
I ≠ {\<zero>OK P n}; I ≠ carrier (OK P n); j ≤ n|] ==>
(mprod_exp K (K_gamma j) (KbK n P) n)K(m_zmax_pdsI K n P I) ≠ \<zero>"
apply (frule K_gamma_hom[of "j" "n"])
apply (frule mprod_mem[of n "K_gamma j" "KbK n P"])
apply (rule Kbase_hom1, assumption+) apply simp apply (erule conjE)
apply (simp add: field_potent_nonzero1)
done
lemma (in Corps) value_mI_genTr3:"[|0 < n; distinct_pds K n P; ideal (OK P n) I;
I ≠ {\<zero>OK P n}; I ≠ carrier (OK P n); j ≤ n|] ==>
(Zl_mI K P I j) ·r ((mprod_exp K (K_gamma j) (KbK n P) n)K(m_zmax_pdsI K n P I))
∈ carrier K"
apply (cut_tac field_is_ring)
apply (rule Ring.ring_tOp_closed, assumption+)
apply (simp add:Zl_mI_mem_K)
apply (simp add:value_mI_genTr1)
done
lemma (in Corps) value_mI_gen:"[|0 < n; distinct_pds K n P; ideal (OK P n) I;
I ≠ {\<zero>(OK P n)}; I ≠ carrier (OK P n); j ≤ n|] ==>
(νK (P j)) (nsum K (λk. ((Zl_mI K P I k) ·r ((mprod_exp K (λl. (γk l)) (KbK n P) n)K(m_zmax_pdsI K n P I)))) n) = LI K (νK (P j)) I"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
apply (case_tac "j = n", simp)
apply (cut_tac nsum_suc[of K "λk. Zl_mI K P I k ·r
mprod_exp K (K_gamma k) (KbK n P) nKm_zmax_pdsI K n P I" "n - Suc 0"],
simp,
thin_tac "Σe K (λk. Zl_mI K P I k ·r
mprod_exp K (K_gamma k) (KbK n P) nKm_zmax_pdsI K n P I) n =
Σe K (λk. Zl_mI K P I k ·r
mprod_exp K (K_gamma k) (KbK n P)
nKm_zmax_pdsI K n P I) (n - Suc 0) ±
Zl_mI K P I n ·r
mprod_exp K (K_gamma n) (KbK n P) nKm_zmax_pdsI K n P I")
apply (cut_tac distinct_pds_valuation[of "n" "n - Suc 0" "P"])
prefer 2 apply simp
prefer 2 apply simp
apply (subst value_less_eq1[THEN sym, of "νK (P n)"
"(Zl_mI K P I n)·r (mprod_exp K (K_gamma n) (KbK n P) nKm_zmax_pdsI K n P I)"
"nsum K (λk.(Zl_mI K P I k)·r (mprod_exp K (K_gamma k) (KbK n P) nKm_zmax_pdsI K n P I)) (n - Suc 0)"], assumption+)
apply (simp add:value_mI_genTr3)
apply (frule Ring.ring_is_ag[of K])
apply (rule aGroup.nsum_mem[of _ "n - Suc 0"], assumption+)
apply (rule allI, rule impI)
apply (simp add:value_mI_genTr3)
apply (subst val_t2p[of "νK (P n)"], assumption+)
apply (simp add:Zl_mI_mem_K)
apply (simp add:value_mI_genTr1)
apply (simp add:mgenerator2Tr3_1[of "n" "n" "n" "P"])
apply (simp add:aadd_0_r)
apply (frule value_Zl_mI[of "n" "P" "I" "n"], assumption+, simp)
apply (erule conjE)
apply (frule_tac f = "λk. (Zl_mI K P I k) ·r
(mprod_exp K (K_gamma k) (KbK n P) nKm_zmax_pdsI K n P I)" in
value_ge_add[of "νK (P n)" "n - Suc 0" _
"ant (m_zmax_pdsI K n P I)"])
apply (rule allI, rule impI)
apply (rule Ring.ring_tOp_closed, assumption+)
apply (simp add:Zl_mI_mem_K)
apply (simp add:value_mI_genTr1)
apply (rule allI, rule impI) apply (simp add:cmp_def)
apply (subst val_t2p [where v="νK P n"], assumption+)
apply (simp add:Zl_mI_mem_K)
apply (simp add:value_mI_genTr1)
apply (cut_tac e = "K_gamma ja" in mprod_mem[of n _ "KbK n P"])
apply (simp add:Zset_def) apply (rule Kbase_hom1, assumption+)
apply (subst val_exp[of "νK (P n)", THEN sym], assumption+)
apply simp+
apply (subst mgenerator2Tr1[of "n" "n" _ "P"], assumption+, simp, simp,
assumption+)
apply (simp add:K_gamma_def Kronecker_delta_def)
apply (frule_tac l = ja in value_Zl_mI_pos[of "n" "P" "I" "n"],
assumption+, simp, simp)
apply (simp add:Nset_preTr1)
apply (frule_tac y = "(νK (P n)) (Zl_mI K P I ja)" in
aadd_le_mono[of "0" _ "ant (m_zmax_pdsI K n P I)"]) apply (simp add:aadd_0_l)
apply (subgoal_tac "LI K (νK (P n)) I < ant (m_zmax_pdsI K n P I)")
apply simp
apply (rule aless_le_trans[of "LI K (νK (P n)) I"
"ant (m_zmax_pdsI K n P I)"])
apply (simp add:m_zmax_pdsI_def)
apply (cut_tac aless_zless[of "tna (LI K (νK (P n)) I)"
"m_zmax n (m_zmax_pdsI_hom K P I) + 1"])
apply (frule val_LI_noninf[of "n" "P" "I" "n"], assumption+, simp, simp)
apply (frule val_LI_pos[of "n" "P" "I" "n"], assumption+, simp,
frule apos_neq_minf[of "LI K (νK (P n)) I"], simp add:ant_tna)
apply (subst m_zmax_pdsI_hom_def)
apply (subst LI_def)
apply (cut_tac m_zmax_gt_each[of n "λu.(tna (AMin ((νK (P u)) ` I)))"])
apply simp
apply (rule allI, rule impI)
apply (simp add:Zset_def, simp)
apply (subst val_t2p[of "νK (P n)"], assumption+)
apply (rule Zl_mI_mem_K, assumption+, simp)
apply (simp add:value_mI_genTr1)
apply (simp add:mgenerator2Tr3_1[of "n" "n" "n" "P" "m_zmax_pdsI K n P I"])
apply (simp add:aadd_0_r)
apply (simp add:value_Zl_mI[of "n" "P" "I" "n"])
(*** case j = n done ***)
apply (frule aGroup.addition3[of "K" "n - Suc 0" "λk. (Zl_mI K P I k) ·r
((mprod_exp K (K_gamma k) (KbK n P) n)K(m_zmax_pdsI K n P I))" "j"])
apply simp
apply (rule allI, rule impI)
apply (simp add:value_mI_genTr3) apply simp+
apply (thin_tac "Σe K (λk. Zl_mI K P I k ·r
mprod_exp K (K_gamma k) (KbK n P) nKm_zmax_pdsI K n P I) n =
Σe K (cmp (λk. Zl_mI K P I k ·r
mprod_exp K (K_gamma k) (KbK n P) nKm_zmax_pdsI K n P I) (τj n)) n")
apply (cut_tac nsum_suc[of K "cmp (λk. Zl_mI K P I k ·r
mprod_exp K (K_gamma k) (KbK n P) nKm_zmax_pdsI K n P I) (τj n)" "n - Suc 0"])
apply (simp del:nsum_suc) apply (
thin_tac "Σe K (cmp (λk. Zl_mI K P I k ·r
mprod_exp K (K_gamma k) (KbK n P) nKm_zmax_pdsI K n P I) (τj n)) n =
Σe K (cmp (λk. Zl_mI K P I k ·r
mprod_exp K (K_gamma k) (KbK n P) nKm_zmax_pdsI K n P I) (τj n))
(n - Suc 0) ± (cmp (λk. Zl_mI K P I k ·r
mprod_exp K (K_gamma k) (KbK n P) nKm_zmax_pdsI K n P I) (τj n)) n")
apply (cut_tac distinct_pds_valuation[of "j" "n - Suc 0" "P"])
prefer 2 apply simp prefer 2 apply simp
apply (simp add:cmp_def)
apply (cut_tac n_in_Nsetn[of "n"])
apply (simp add:transpos_ij_2)
apply (subst value_less_eq1[THEN sym, of "νK (P j)"
"(Zl_mI K P I j) ·r (mprod_exp K (K_gamma j) (KbK n P)
nKm_zmax_pdsI K n P I)" "Σe K (λx.(Zl_mI K P I ((τj n) x)) ·r
(mprod_exp K (K_gamma ((τj n) x)) (KbK n P) nKm_zmax_pdsI K n P I)) (n - Suc 0)"], assumption+)
apply (simp add:value_mI_genTr3)
apply (rule aGroup.nsum_mem[of "K" "n - Suc 0"], assumption+)
apply (rule allI, rule impI)
apply (frule_tac l = ja in transpos_mem[of "j" "n" "n"], simp+)
apply (simp add:value_mI_genTr3)
apply (subst val_t2p[of "νK (P j)"], assumption+)
apply (simp add:Zl_mI_mem_K)
apply (simp add:value_mI_genTr1)
apply (simp add:mgenerator2Tr3_1[of "n" "j" "j" "P"])
apply (frule value_Zl_mI[of "n" "P" "I" "j"], assumption+)
apply (erule conjE)
apply (simp add:aadd_0_r)
apply (cut_tac f = "λx. (Zl_mI K P I ((τj n) x)) ·r
(mprod_exp K (K_gamma ((τj n) x)) (KbK n P) nKm_zmax_pdsI K n P I)" in
value_ge_add[of "νK (P j)"
"n - Suc 0" _ "ant (m_zmax_pdsI K n P I)"], assumption+)
apply (rule allI, rule impI)
apply (frule_tac l = ja in transpos_mem[of "j" "n" "n"], simp+)
apply (simp add:value_mI_genTr3)
apply (rule allI, rule impI) apply (simp add:cmp_def)
apply (frule_tac l = ja in transpos_mem[of "j" "n" "n"], simp+)
apply (subst val_t2p [where v="νK P j"], assumption+)
apply (simp add:Zl_mI_mem_K)
apply (simp add:value_mI_genTr1)
apply (cut_tac k = ja in transpos_noteqTr[of "n" _ "j"], simp+)
apply (subst mgenerator2Tr3_2[of "n" "j" _ "P"], simp+)
apply (cut_tac l = "(τj n) ja" in value_Zl_mI_pos[of "n" "P" "I" "j"],
simp+)
apply (frule_tac y = "(νK (P j)) (Zl_mI K P I ((τj n) ja))" in
aadd_le_mono[of "0" _ "ant (m_zmax_pdsI K n P I)"])
apply (simp add:aadd_0_l)
apply (subgoal_tac "LI K (νK (P j)) I < ant (m_zmax_pdsI K n P I)")
apply (rule aless_le_trans[of "LI K (νK (P j)) I"
"ant (m_zmax_pdsI K n P I)"], assumption+)
apply (simp add:m_zmax_pdsI_def)
apply (cut_tac aless_zless[of "tna (LI K (νK (P j)) I)"
"m_zmax n (m_zmax_pdsI_hom K P I) + 1"])
apply (frule val_LI_noninf[of "n" "P" "I" "j"], assumption+,
frule val_LI_pos[of "n" "P" "I" "j"], assumption+,
frule apos_neq_minf[of "LI K (νK (P j)) I"], simp add:ant_tna)
apply (subst m_zmax_pdsI_hom_def)
apply (subst LI_def)
apply (subgoal_tac "∀h ≤ n. (λu. (tna (AMin ((νK (P u)) ` I)))) h ∈ Zset")
apply (frule m_zmax_gt_each[of n "λu.(tna (AMin ((νK (P u)) ` I)))"])
apply simp
apply (rule allI, rule impI)
apply (simp add:Zset_def)
apply (subst val_t2p[of "νK (P j)"], assumption+)
apply (rule Zl_mI_mem_K, assumption+)
apply (simp add:value_mI_genTr1)
apply (simp add:mgenerator2Tr3_1[of "n" "j" "j" "P"
"m_zmax_pdsI K n P I"])
apply (simp add:aadd_0_r)
apply (simp add:value_Zl_mI[of "n" "P" "I" "j"])
done
lemma (in Corps) mI_gen_in_I:"[|0 < n; distinct_pds K n P; ideal (OK P n) I;
I ≠ {\<zero>(OK P n)}; I ≠ carrier (OK P n)|] ==>
(nsum K (λk. ((Zl_mI K P I k) ·r
((mprod_exp K (λl. (γk l)) (KbK n P) n)K(m_zmax_pdsI K n P I)))) n) ∈ I"
apply (cut_tac field_is_ring, frule ring_n_pd[of n P])
apply (rule ideal_eSum_closed[of n P I n], assumption+)
apply (rule allI, rule impI)
apply (frule_tac j = j in value_Zl_mI[of "n" "P" "I"], assumption+)
apply (erule conjE)
apply (thin_tac "(νK (P j)) (Zl_mI K P I j) = LI K (νK (P j)) I")
apply (subgoal_tac "(mprod_exp K (K_gamma j) (KbK n P) n)K(m_zmax_pdsI K n P I)
∈ carrier (OK P n)")
apply (frule_tac x = "Zl_mI K P I j" and
r = "(mprod_exp K (K_gamma j) (KbK n P) n)K(m_zmax_pdsI K n P I)"
in Ring.ideal_ring_multiple1[of "(OK P n)" "I"], assumption+)
apply (frule_tac h = "Zl_mI K P I j" in
Ring.ideal_subset[of "OK P n" "I"], assumption+)
apply (simp add:ring_n_pd_tOp_K_tOp[of "n" "P"])
apply (subst ring_n_pd_def) apply (simp add:Sr_def)
apply (simp add:value_mI_genTr1)
apply (rule allI, rule impI)
apply (case_tac "j = ja")
apply (simp add:mgenerator2Tr3_1)
apply (simp add:mgenerator2Tr3_2)
apply (simp add:m_zmax_pdsI_def) apply (simp add:m_zmax_pdsI_hom_def)
apply (simp only:ant_0[THEN sym])
apply (simp add:aless_zless)
apply (subgoal_tac "∀l ≤ n. (λj. tna (AMin ((νK (P j)) ` I))) l ∈ Zset")
apply (frule m_zmax_gt_each[of n "λj. tna (AMin ((νK (P j)) ` I))"])
apply (rotate_tac -1, drule_tac a = ja in forall_spec, simp+)
apply (frule_tac j = ja in val_LI_pos[of "n" "P" "I"], assumption+)
apply (cut_tac j = "tna (LI K (νK (P ja)) I)" in ale_zle[of "0"])
apply (frule_tac j = ja in val_LI_noninf[of "n" "P" "I"], assumption+,
frule_tac j = ja in val_LI_pos[of "n" "P" "I"], assumption+,
frule_tac a = "LI K (νK (P ja)) I" in apos_neq_minf, simp add:ant_tna,
simp add:ant_0) apply (unfold LI_def)
apply (frule_tac j = "tna (AMin (νK (P ja) ` I))" and k = "m_zmax n (λj. tna (AMin (νK (P j) ` I)))" in zle_trans[of "0"], assumption+)
apply (rule_tac j = "m_zmax n (λj. tna (AMin (νK (P j) ` I)))" and
k = "m_zmax n (λj. tna (AMin (νK (P j) ` I))) + 1" in zle_trans[of "0"],
assumption+) apply simp
apply (rule allI, rule impI) apply (simp add:Zset_def)
done
text{* We write the element
eΣ K (λk. (Zl_mI K P I k) ·K ((mprod_exp K (K_gamma k) (KbK n P)
n)K(m_zmax_pdsI K n P I))) n
as mIgK G a i n P I *}
constdefs (structure K)
mIg :: "[_, nat, nat => ('b => ant) set,
'b set] => 'b" ("(4mIg _ _ _ _)" [82,82,82,83]82)
"mIgK n P I == Σe K (λk. (Zl_mI K P I k) ·r
((mprod_exp K (K_gamma k) (KbK n P) n)K(m_zmax_pdsI K n P I))) n"
text{* We can rewrite above two lemmas by using mIgK G a i n P I *}
lemma (in Corps) value_mI_gen1:"[|0 < n; distinct_pds K n P; ideal (OK P n) I;
I ≠ {\<zero>(OK P n)}; I ≠ carrier (OK P n)|] ==>
∀j ≤ n.(νK (P j)) (mIgK n P I) = LI K (νK (P j)) I"
apply (rule allI, rule impI)
apply (simp add:mIg_def value_mI_gen)
done
lemma (in Corps) mI_gen_in_I1:"[|0 < n; distinct_pds K n P; ideal (OK P n) I;
I ≠ {\<zero>(OK P n)}; I ≠ carrier (OK P n)|] ==> (mIgK n P I) ∈ I"
apply (simp add:mIg_def mI_gen_in_I)
done
lemma (in Corps) mI_principalTr:"[|0 < n; distinct_pds K n P; ideal (OK P n) I;
I ≠ {\<zero>(OK P n)}; I ≠ carrier (OK P n); x ∈ I|] ==>
∀j ≤ n. ((νK (P j)) (mIgK n P I)) ≤ ((νK (P j)) x)"
apply (simp add:value_mI_gen1)
apply (rule allI, rule impI)
apply (rule Zleast_LI, assumption+)
done
lemma (in Corps) mI_principal:"[|0 < n; distinct_pds K n P; ideal (OK P n) I;
I ≠ {\<zero>(OK P n)}; I ≠ carrier (OK P n)|] ==>
I = Rxa (OK P n) (mIgK n P I)"
apply (frule ring_n_pd[of "n" "P"])
apply (rule equalityI)
apply (rule subsetI)
apply (frule_tac x = x in mI_principalTr[of "n" "P" "I"],
assumption+)
apply (frule_tac y = x in n_eq_val_eq_idealTr[of "n" "P" "mIgK n P I"])
apply (frule mI_gen_in_I1[of "n" "P" "I"], assumption+)
apply (simp add:Ring.ideal_subset)+
apply (thin_tac "∀j≤n. (νK (P j)) (mIg K n P I) ≤ (νK (P j)) x")
apply (frule_tac h = x in Ring.ideal_subset[of "OK P n" "I"], assumption+)
apply (frule_tac a = x in Ring.a_in_principal[of "OK P n"], assumption+)
apply (simp add:subsetD)
apply (rule Ring.ideal_cont_Rxa[of "OK P n" "I" "mIg K n P I"], assumption+)
apply (rule mI_gen_in_I1[of "n" "P" "I"], assumption+)
done
subsection "prime_n_pd"
lemma (in Corps) prime_n_pd_principal:"[|distinct_pds K n P; j ≤ n|] ==>
(PK P n j) = Rxa (OK P n) (((KbK n P) j))"
apply (frule ring_n_pd[of "n" "P"])
apply (frule prime_n_pd_prime[of "n" "P" "j"], assumption+)
apply (simp add:prime_ideal_def, frule conjunct1)
apply (fold prime_ideal_def)
apply (thin_tac "prime_ideal (OK P n) (PK P n j)")
apply (rule equalityI)
apply (rule subsetI)
apply (frule_tac y = x in n_eq_val_eq_idealTr[of n P "(KbK n P) j"])
apply (thin_tac "Ring (OK P n)", thin_tac "ideal (OK P n) (PK P n j)")
apply (simp add:ring_n_pd_def Sr_def)
apply (frule Kbase_hom[of "n" "P"], simp)
apply (rule allI, rule impI)
apply (frule Kbase_Kronecker[of "n" "P"])
apply (simp add:Kronecker_delta_def, rule impI)
apply (simp only:ant_0[THEN sym], simp only:ant_1[THEN sym])
apply (simp del:ant_1)
apply (simp add:prime_n_pd_def)
apply (rule allI, rule impI)
apply (frule Kbase_Kronecker[of "n" "P"])
apply simp
apply (thin_tac "∀j≤n. ∀l≤n. (νK (P j)) ((KbK n P) l) = δj l")
apply (case_tac "ja = j", simp add:Kronecker_delta_def)
apply (thin_tac "ideal (OK P n) (PK P n j)")
apply (simp add:prime_n_pd_def, erule conjE)
apply (frule_tac x = x in mem_ring_n_pd_mem_K[of "n" "P"],
assumption+)
apply (case_tac "x = \<zero>K")
apply (frule distinct_pds_valuation2[of "j" "n" "P"], assumption+)
apply (rule gt_a0_ge_1, assumption)+
apply (simp add:Kronecker_delta_def)
apply (frule_tac j = ja in distinct_pds_valuation2[of _ "n" "P"],
assumption+)
apply (simp add:prime_n_pd_def, erule conjE)
apply (thin_tac "ideal (OK P n) {x. x ∈ carrier (OK P n) ∧ 0 < (νK (P j)) x}")
apply (simp add:ring_n_pd_def Sr_def)
apply (cut_tac h = x in Ring.ideal_subset[of "OK P n" "PK P n j"])
apply (frule_tac a = x in Ring.a_in_principal[of "OK P n"])
apply (simp add:Ring.ideal_subset, assumption+)
apply (rule_tac c = x and A = "(OK P n) ♦p x" and B = "(OK P n) ♦p (KbK n P) j"
in subsetD, assumption+)
apply (simp add:Ring.a_in_principal)
apply (rule Ring.ideal_cont_Rxa[of "OK P n" "PK P n j" "(KbK n P) j"], assumption+)
apply (subst prime_n_pd_def, simp)
apply (frule Kbase_Kronecker[of "n" "P"])
apply (simp add:Kronecker_delta_def)
apply (simp only:ant_1[THEN sym], simp only:ant_0[THEN sym])
apply (simp del:ant_1 add:aless_zless)
apply (subst ring_n_pd_def, simp add:Sr_def)
apply (frule Kbase_hom[of "n" "P"])
apply simp
apply (rule allI)
apply (simp add:ant_0)
apply (rule impI)
apply (simp only:ant_1[THEN sym], simp only:ant_0[THEN sym])
apply (simp del:ant_1)
done
lemma (in Corps) ring_n_prod_primesTr:"[|0 < n; distinct_pds K n P;
ideal (OK P n) I; I ≠ {\<zero>OK P n}; I ≠ carrier (OK P n)|] ==>
∀j ≤ n.(νK (P j)) (mprod_exp K (mL K P I) (KbK n P) n) =
(νK (P j)) (mIgK n P I)"
apply (rule allI, rule impI)
apply (simp add:mgenerator1)
apply (simp add:value_mI_gen1)
apply (simp add:value_Zl_mI)
done
lemma (in Corps) ring_n_prod_primesTr1:"[|0 < n; distinct_pds K n P;
ideal (OK P n) I; I ≠ {\<zero>OK P n}; I ≠ carrier (OK P n)|] ==>
I = (OK P n) ♦p (mprod_exp K (mL K P I) (KbK n P) n)"
apply (frule ring_n_pd[of "n" "P"])
apply (subst n_eq_val_eq_ideal[of "n" "P" "mprod_exp K (mL K P I)
(KbK n P) n" "mIgK n P I"], assumption+)
apply (simp add:mgeneratorTr4)
apply (frule mI_gen_in_I1[of "n" "P" "I"], assumption+)
apply (simp add:Ring.ideal_subset)
apply (simp add:ring_n_prod_primesTr)
apply (simp add:mI_principal)
done
lemma (in Corps) ring_n_prod_primes:"[|0 < n; distinct_pds K n P;
ideal (OK P n) I; I ≠ {\<zero>OK P n}; I ≠ carrier (OK P n);
∀k ≤ n. J k = (PK P n k)♦(OK P n) (nat ((mL K P I) k))|] ==>
I = iΠ(OK P n),n J"
apply (simp add:prime_n_pd_principal[of "n" "P"])
apply (subst ring_n_prod_primesTr1[of "n" "P" "I"], assumption+)
apply (frule ring_n_pd[of "n" "P"])
apply (frule Ring.prod_n_principal_ideal[of "OK P n" "nat o (mL K P I)" "n"
"KbK n P" "J"])
apply (frule Kbase_hom[of "n" "P"])
apply (rule univar_func_test) apply (rule ballI) apply (simp add:nat_def)
apply (subst ring_n_pd_def) apply (simp add:Sr_def)
apply (rule univar_func_test, rule ballI, simp)
apply (simp add:Kbase_Kronecker[of "n" "P"])
apply (simp add:Kronecker_delta_def)
apply (simp only:ant_1[THEN sym], simp only:ant_0[THEN sym])
apply (simp del:ant_1)
apply (simp add:Kbase_hom) apply simp
apply simp
apply (frule ring_n_mprod_mprodR[of "n" "P" n "mL K P I" "KbK n P"])
apply (rule allI, rule impI, simp add:Zset_def)
apply (rule allI, rule impI)
apply (simp add: Zleast_in_mI_pos)
apply (rule allI, rule impI)
apply (subst ring_n_pd_def) apply (simp add:Sr_def)
apply (frule Kbase_hom1[of "n" "P"], simp)
apply (simp add:zero_in_ring_n_pd_zero_K)
apply (frule Kbase_Kronecker[of "n" "P"])
apply (simp add:Kronecker_delta_def)
apply (simp only:ant_1[THEN sym], simp only:ant_0[THEN sym])
apply (simp del:ant_1)
apply simp
done
end
lemma OstrowskiTr8:
[| valuation K v; x ∈ carrier K; 0 < v (1r ± -a x) |]
==> 0 < v (1r ± -a x ·r (1r ± x ·r (1r ± -a x)) K)
lemma OstrowskiTr9:
[| valuation K v; x ∈ carrier K; 0 < v x |]
==> 0 < v (x ·r (1r ± x ·r (1r ± -a x)) K)
lemma OstrowskiTr10:
[| valuation K v; x ∈ carrier K; ¬ 0 ≤ v x |]
==> 0 < v (x ·r (1r ± x ·r (1r ± -a x)) K)
lemma Ostrowski_first:
vals_nonequiv K (Suc 0) vv ==> ∃x∈carrier K. Ostrowski_elem K (Suc 0) vv x
lemma Ostrowski:
∀vv. vals_nonequiv K (Suc n) vv -->
(∃x∈carrier K. Ostrowski_elem K (Suc n) vv x)
lemma val_1_nonzero:
[| valuation K v; x ∈ carrier K; v x = 1 |] ==> x ≠ \<zero>
lemma 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. vv 0 ((1r ± -a x)^K m ± a ·r x^K m) = 1
lemma 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 ((1r ± -a x)^K m) = 0
lemma 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
lemma Approximation1_5Tr5:
[| vals_nonequiv K (Suc n) vv; a ∈ carrier K; a ≠ \<zero>; x ∈ carrier K;
Ostrowski_elem K (Suc n) vv x; j ∈ nset (Suc 0) (Suc n) |]
==> ∃l. ∀m>l. 0 < vv j (a ·r x^K m)
lemma Approximation1_5Tr6:
[| vals_nonequiv K (Suc n) vv; a ∈ carrier K; a ≠ \<zero>; x ∈ carrier K;
Ostrowski_elem K (Suc n) vv x; j ∈ nset (Suc 0) (Suc n) |]
==> ∃l. ∀m>l. vv j ((1r ± -a x)^K m ± a ·r x^K m) = 0
lemma 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. ∀j∈nset (Suc 0) (Suc n). vv j ((1r ± -a x)^K m ± a ·r x^K m) = 0)
lemma 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)
lemma K_gamma_hom:
k ≤ n ==> ∀j≤n. γk j ∈ Zset
lemma transpos_eq:
(τ0 0) k = k
lemma transpos_vals_nonequiv:
[| vals_nonequiv K (Suc n) vv; j ≤ Suc n |]
==> vals_nonequiv K (Suc n) (vv o τ0 j)
lemma Ostrowski_base_hom:
vals_nonequiv K (Suc n) vv ==> ΩK vv Suc n ∈ {h. h ≤ Suc n} -> carrier K
lemma Ostrowski_base_mem:
vals_nonequiv K (Suc n) vv ==> ∀j≤Suc n. (ΩK vv Suc n) j ∈ carrier K
lemma Ostrowski_base_mem_1:
[| vals_nonequiv K (Suc n) vv; j ≤ Suc n |] ==> (ΩK vv Suc n) j ∈ carrier K
lemma Ostrowski_base_nonzero:
[| vals_nonequiv K (Suc n) vv; j ≤ Suc n |] ==> (ΩK vv Suc n) j ≠ \<zero>
lemma 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)
lemma 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
lemma 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
lemma 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)
lemma Ostrowski_baseTr0:
[| vals_nonequiv K (Suc n) vv; l ≤ Suc n |]
==> 0 < vv l (1r ± -a (ΩK vv Suc n) l) ∧
(∀m∈{h. h ≤ Suc n} - {l}. 0 < vv m ((ΩK vv Suc n) l))
lemma Ostrowski_baseTr1:
[| vals_nonequiv K (Suc n) vv; l ≤ Suc n |]
==> 0 < vv l (1r ± -a (ΩK vv Suc n) l)
lemma Ostrowski_baseTr2:
[| vals_nonequiv K (Suc n) vv; l ≤ Suc n; m ≤ Suc n; l ≠ m |]
==> 0 < vv m ((ΩK vv Suc n) l)
lemma Nset_have_two:
j ∈ {h. h ≤ Suc n} ==> ∃m∈{h. h ≤ Suc n}. j ≠ m
lemma Ostrowski_base_npow_not_one:
[| 0 < N; j ≤ Suc n; vals_nonequiv K (Suc n) vv |]
==> 1r ± -a (ΩK vv Suc n) j^K N ≠ \<zero>
lemma expansion_of_sum1:
x ∈ carrier R ==> (1r ± x)^R n = Σe R (λi. nCi ×R x^R i) n
lemma tail_of_expansion:
x ∈ carrier R ==> (1r ± x)^R Suc n = Σe R (λi. Suc nCSuc i ×R x^R Suc i) n ± 1r
lemma tail_of_expansion1:
x ∈ carrier R
==> (1r ± x)^R Suc n = x ·r Σe R (λi. Suc nCSuc i ×R x^R i) n ± 1r
lemma nsum_in_VrTr:
valuation K v
==> (∀j≤n. f j ∈ carrier K) ∧ (∀j≤n. 0 ≤ v (f j)) -->
Σe K f n ∈ carrier (Vr K v)
lemma nsum_in_Vr:
[| valuation K v; ∀j≤n. f j ∈ carrier K; ∀j≤n. 0 ≤ v (f j) |]
==> Σe K f n ∈ carrier (Vr K v)
lemma nsum_mem_in_Vr:
[| valuation K v; ∀j≤n. f j ∈ carrier K; ∀j≤n. 0 ≤ v (f j) |]
==> Σe K f n ∈ carrier (Vr K v)
lemma val_nscal_ge_selfTr:
[| valuation K v; x ∈ carrier K; 0 ≤ v x |] ==> v x ≤ v ( n ×K x)
lemma ApproximationTr:
[| valuation K v; x ∈ carrier K; 0 ≤ v x |]
==> v x ≤ v (1r ± -a (1r ± x)^K Suc n)
lemma ApproximationTr0:
aa ∈ carrier K ==> (1r ± -a aa^K N)^K N ∈ carrier K
lemma ApproximationTr1:
aa ∈ carrier K ==> 1r ± -a (1r ± -a aa^K N)^K N ∈ carrier K
lemma ApproximationTr2:
[| valuation K v; aa ∈ carrier K; aa ≠ \<zero>; 0 ≤ v aa |]
==> int N *a v aa ≤ v (1r ± -a (1r ± -a aa^K N)^K N)
lemma 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 (1r ± -a b j)) ∧ g l = x l ·r (-a b l) -->
Σe K (λj∈{h. h ≤ n}. x j ·r (1r ± -a b j)) n ± -a x l = Σe K g n
lemma 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 (1r ± -a b j); g l = x l ·r (-a b l) |]
==> Σe K (λj∈{h. h ≤ n}. x j ·r (1r ± -a b j)) n ± -a x l = Σe K g n
lemma one_m_x_times:
x ∈ carrier R ==> (1r ± -a x) ·r Σe R npow R x n = 1r ± -a x^R Suc n
lemma x_pow_fSum_in_Vr:
[| valuation K v; x ∈ carrier (Vr K v) |] ==> Σe K npow K x n ∈ carrier (Vr K v)
lemma val_1mx_pos:
[| valuation K v; x ∈ carrier K; 0 < v (1r ± -a x) |] ==> v x = 0
lemma val_1mx_pow:
[| valuation K v; x ∈ carrier K; 0 < v (1r ± -a x) |]
==> 0 < v (1r ± -a x^K Suc n)
lemma ApproximationTr3:
[| vals_nonequiv K (Suc n) vv; ∀l≤Suc n. x l ∈ carrier K; j ≤ Suc n |]
==> ∃L. ∀N>L. an m
≤ vv j (Σe K (λk∈{h. h ≤ Suc n}.
x k ·r
(1r ±
-a (1r ± -a (ΩK vv Suc n) k^K N)^K N)) Suc n ±
-a x j)
lemma app_LB:
[| vals_nonequiv K (Suc n) vv; ∀l≤Suc n. x l ∈ carrier K; j ≤ Suc n |]
==> ∀N>(ΨK Suc n vv x m) j.
an m
≤ vv j (Σe K (λj∈{h. h ≤ Suc n}.
x j ·r
(1r ± -a (1r ± -a (ΩK vv Suc n) j^K N)^K N)) Suc n ±
-a x j)
lemma ApplicationTr4:
[| vals_nonequiv K (Suc n) vv; ∀j∈{h. h ≤ Suc n}. x j ∈ carrier K |]
==> ∃l. ∀N>l. ∀j≤Suc n.
an m
≤ vv j (Σe K (λj∈{h. h ≤ Suc n}.
x j ·r
(1r ±
-a (1r ±
-a (ΩK vv Suc n) j^K N)^K N)) Suc n ±
-a x j)
theorem Approximation_thm:
[| vals_nonequiv K (Suc n) vv; ∀j≤Suc n. x j ∈ carrier K |]
==> ∃y∈carrier K. ∀j≤Suc n. an m ≤ vv j (y ± -a x j)
lemma distinct_pds_restriction:
distinct_pds K (Suc n) P ==> distinct_pds K n P
lemma ring_n_distinct_prime_divisors:
distinct_pds K n P ==> Ring (Sr K {x : carrier K. ∀j≤n. 0 ≤ (νK P j) x})
lemma distinct_pds_valuation:
[| j ≤ Suc n; distinct_pds K (Suc n) P |] ==> valuation K (νK P j)
lemma distinct_pds_valuation1:
[| 0 < n; j ≤ n; distinct_pds K n P |] ==> valuation K (νK P j)
lemma distinct_pds_valuation2:
[| j ≤ n; distinct_pds K n P |] ==> valuation K (νK P j)
lemma ring_n_pd:
distinct_pds K n P ==> Ring (OK P n)
lemma ring_n_pd_Suc:
distinct_pds K (Suc n) P ==> carrier (OK P Suc n) ⊆ carrier (OK P n)
lemma ring_n_pd_pOp_K_pOp:
[| distinct_pds K n P; x ∈ carrier (OK P n); y ∈ carrier (OK P n) |]
==> x ±OK P n y = x ± y
lemma ring_n_pd_tOp_K_tOp:
[| distinct_pds K n P; x ∈ carrier (OK P n); y ∈ carrier (OK P n) |]
==> x ·rOK P n y = x ·r y
lemma ring_n_eSum_K_eSumTr:
distinct_pds K n P
==> (∀j≤m. f j ∈ carrier (OK P n)) --> Σe OK P n f m = Σe K f m
lemma ring_n_eSum_K_eSum:
[| distinct_pds K n P; ∀j≤m. f j ∈ carrier (OK P n) |]
==> Σe OK P n f m = Σe K f m
lemma ideal_eSum_closed:
[| distinct_pds K n P; ideal (OK P n) I; ∀j≤m. f j ∈ I |] ==> Σe K f m ∈ I
lemma zero_in_ring_n_pd_zero_K:
distinct_pds K n P ==> \<zero>OK P n = \<zero>
lemma one_in_ring_n_pd_one_K:
distinct_pds K n P ==> 1rOK P n = 1r
lemma mem_ring_n_pd_mem_K:
[| distinct_pds K n P; x ∈ carrier (OK P n) |] ==> x ∈ carrier K
lemma ring_n_tOp_K_tOp:
[| distinct_pds K n P; x ∈ carrier (OK P n); y ∈ carrier (OK P n) |]
==> x ·rOK P n y = x ·r y
lemma ring_n_exp_K_exp:
[| distinct_pds K n P; x ∈ carrier (OK P n) |] ==> x^K m = x^OK P n m
lemma prime_n_pd_prime:
[| distinct_pds K n P; j ≤ n |] ==> prime_ideal (OK P n) (PK P n j)
lemma n_eq_val_eq_idealTr:
[| distinct_pds K n P; x ∈ carrier (OK P n); y ∈ carrier (OK P n);
∀j≤n. (νK P j) x ≤ (νK P j) y |]
==> (OK P n) ♦p y ⊆ (OK P n) ♦p x
lemma n_eq_val_eq_ideal:
[| distinct_pds K n P; x ∈ carrier (OK P n); y ∈ carrier (OK P n);
∀j≤n. (νK P j) x = (νK P j) y |]
==> (OK P n) ♦p x = (OK P n) ♦p y
lemma mI_vals_nonempty:
[| distinct_pds K n P; ideal (OK P n) I; j ≤ n |] ==> νK P j ` I ≠ {}
lemma mI_vals_LB:
[| distinct_pds K n P; ideal (OK P n) I; j ≤ n |] ==> νK P j ` I ⊆ LBset (ant 0)
lemma mL_hom:
[| distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n};
I ≠ carrier (OK P n) |]
==> ∀j≤n. mL K P I j ∈ Zset
lemma ex_Zleast_in_mI:
[| distinct_pds K n P; ideal (OK P n) I; j ≤ n |]
==> ∃x∈I. (νK P j) x = LI K (νK P j) I
lemma val_LI_pos:
[| distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n}; j ≤ n |]
==> 0 ≤ LI K (νK P j) I
lemma val_LI_noninf:
[| distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n}; j ≤ n |]
==> LI K (νK P j) I ≠ ∞
lemma Zleast_in_mI_pos:
[| distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n}; j ≤ n |]
==> 0 ≤ mL K P I j
lemma Zleast_mL_I:
[| distinct_pds K n P; ideal (OK P n) I; j ≤ n; I ≠ {\<zero>OK P n}; x ∈ I |]
==> ant (mL K P I j) ≤ (νK P j) x
lemma Zleast_LI:
[| distinct_pds K n P; ideal (OK P n) I; j ≤ n; I ≠ {\<zero>OK P n}; x ∈ I |]
==> LI K (νK P j) I ≤ (νK P j) x
lemma mpdiv_vals_nonequiv:
distinct_pds K n P ==> vals_nonequiv K n (λj. νK P j)
lemma KbaseTr:
distinct_pds K n P ==> ∃f. KbaseP K P n f
lemma KbaseTr1:
distinct_pds K n P ==> KbaseP K P n (KbK n P)
lemma Kbase_hom:
distinct_pds K n P ==> ∀j≤n. (KbK n P) j ∈ carrier K
lemma Kbase_Kronecker:
distinct_pds K n P ==> ∀j≤n. ∀l≤n. (νK P j) ((KbK n P) l) = δj l
lemma Kbase_nonzero:
distinct_pds K n P ==> ∀j≤n. (KbK n P) j ≠ \<zero>
lemma Kbase_hom1:
distinct_pds K n P ==> ∀j≤n. (KbK n P) j ∈ carrier K - {\<zero>}
lemma value_Zl_mI:
[| distinct_pds K n P; ideal (OK P n) I; j ≤ n |]
==> Zl_mI K P I j ∈ I ∧ (νK P j) (Zl_mI K P I j) = LI K (νK P j) I
lemma Zl_mI_nonzero:
[| distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n}; j ≤ n |]
==> Zl_mI K P I j ≠ \<zero>
lemma Zl_mI_mem_K:
[| distinct_pds K n P; ideal (OK P n) I; l ≤ n |] ==> Zl_mI K P I l ∈ carrier K
lemma mprod_expR_memTr:
(∀j≤n. f j ∈ carrier K) --> mprod_expR K e f n ∈ carrier K
lemma mprod_expR_mem:
∀j≤n. f j ∈ carrier K ==> mprod_expR K e f n ∈ carrier K
lemma mprod_Suc:
[| ∀j≤Suc n. e j ∈ Zset; ∀j≤Suc n. f j ∈ carrier K - {\<zero>} |]
==> mprod_exp K e f (Suc n) = mprod_exp K e f n ·r f (Suc n)Ke (Suc n)
lemma mprod_memTr:
(∀j≤n. e j ∈ Zset) ∧ (∀j≤n. f j ∈ carrier K - {\<zero>}) -->
mprod_exp K e f n ∈ carrier K - {\<zero>}
lemma mprod_mem:
[| ∀j≤n. e j ∈ Zset; ∀j≤n. f j ∈ carrier K - {\<zero>} |]
==> mprod_exp K e f n ∈ carrier K - {\<zero>}
lemma mprod_mprodR:
[| ∀j≤n. e j ∈ Zset; ∀j≤n. 0 ≤ e j; ∀j≤n. f j ∈ carrier K - {\<zero>} |]
==> mprod_exp K e f n = mprod_expR K (nat o e) f n
lemma ring_n_mprod_mprodRTr:
distinct_pds K n P
==> (∀j≤m. e j ∈ Zset) ∧
(∀j≤m. 0 ≤ e j) ∧ (∀j≤m. f j ∈ carrier (OK P n) - {\<zero>OK P n}) -->
mprod_exp K e f m = mprod_expR (OK P n) (nat o e) f m
lemma ring_n_mprod_mprodR:
[| distinct_pds K n P; ∀j≤m. e j ∈ Zset; ∀j≤m. 0 ≤ e j;
∀j≤m. f j ∈ carrier (OK P n) - {\<zero>OK P n} |]
==> mprod_exp K e f m = mprod_expR (OK P n) (nat o e) f m
lemma value_mprod_expTr:
valuation K v
==> (∀j≤n. e j ∈ Zset) ∧ (∀j≤n. f j ∈ carrier K - {\<zero>}) -->
v (mprod_exp K e f n) = ASum (λj. e j *a v (f j)) n
lemma value_mprod_exp:
[| valuation K v; ∀j≤n. e j ∈ Zset; ∀j≤n. f j ∈ carrier K - {\<zero>} |]
==> v (mprod_exp K e f n) = ASum (λj. e j *a v (f j)) n
lemma mgenerator0_1:
[| distinct_pds K (Suc n) P; ideal (OK P Suc n) I; I ≠ {\<zero>OK P Suc n};
I ≠ carrier (OK P Suc n); j ≤ Suc n |]
==> (νK P j) (mprod_exp K (mL K P I) (KbK Suc n P) (Suc n)) =
(νK P j) (Zl_mI K P I j)
lemma mgenerator0_2:
[| 0 < n; distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n};
I ≠ carrier (OK P n); j ≤ n |]
==> (νK P j) (mprod_exp K (mL K P I) (KbK n P) n) = (νK P j) (Zl_mI K P I j)
lemma mgenerator1:
[| distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n};
I ≠ carrier (OK P n); j ≤ n |]
==> (νK P j) (mprod_exp K (mL K P I) (KbK n P) n) = (νK P j) (Zl_mI K P I j)
lemma mgenerator2Tr1:
[| 0 < n; j ≤ n; k ≤ n; distinct_pds K n P |]
==> (νK P j) (mprod_exp K (K_gamma k) (KbK n P) n) = (γk j) *a (δj j)
lemma mgenerator2Tr2:
[| 0 < n; j ≤ n; k ≤ n; distinct_pds K n P |]
==> (νK P j) (mprod_exp K (K_gamma k) (KbK n P) nKm) = ant (m * (γk j))
lemma mgenerator2Tr3_1:
[| 0 < n; j ≤ n; k ≤ n; j = k; distinct_pds K n P |]
==> (νK P j) (mprod_exp K (K_gamma k) (KbK n P) nKm) = 0
lemma mgenerator2Tr3_2:
[| 0 < n; j ≤ n; k ≤ n; j ≠ k; distinct_pds K n P |]
==> (νK P j) (mprod_exp K (K_gamma k) (KbK n P) nKm) = ant m
lemma mgeneratorTr4:
[| 0 < n; distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n};
I ≠ carrier (OK P n) |]
==> mprod_exp K (mL K P I) (KbK n P) n ∈ carrier (OK P n)
lemma value_Zl_mI_pos:
[| 0 < n; distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n};
I ≠ carrier (OK P n); j ≤ n; l ≤ n |]
==> 0 ≤ (νK P j) (Zl_mI K P I l)
lemma value_mI_genTr1:
[| 0 < n; distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n};
I ≠ carrier (OK P n); j ≤ n |]
==> mprod_exp K (K_gamma j) (KbK n P) nKm_zmax_pdsI K n P I ∈ carrier K
lemma value_mI_genTr1_0:
[| 0 < n; distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n};
I ≠ carrier (OK P n); j ≤ n |]
==> mprod_exp K (K_gamma j) (KbK n P) n ∈ carrier K
lemma value_mI_genTr2:
[| 0 < n; distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n};
I ≠ carrier (OK P n); j ≤ n |]
==> mprod_exp K (K_gamma j) (KbK n P) nKm_zmax_pdsI K n P I ≠ \<zero>
lemma value_mI_genTr3:
[| 0 < n; distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n};
I ≠ carrier (OK P n); j ≤ n |]
==> Zl_mI K P I j ·r mprod_exp K (K_gamma j) (KbK n P) nKm_zmax_pdsI K n P I
∈ carrier K
lemma value_mI_gen:
[| 0 < n; distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n};
I ≠ carrier (OK P n); j ≤ n |]
==> (νK P j)
(Σe K (λk. Zl_mI K P I k ·r
mprod_exp K (K_gamma k) (KbK n P) nKm_zmax_pdsI K n P I) n) =
LI K (νK P j) I
lemma mI_gen_in_I:
[| 0 < n; distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n};
I ≠ carrier (OK P n) |]
==> Σe K (λk. Zl_mI K P I k ·r
mprod_exp K (K_gamma k) (KbK n P) nKm_zmax_pdsI K n P I) n
∈ I
lemma value_mI_gen1:
[| 0 < n; distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n};
I ≠ carrier (OK P n) |]
==> ∀j≤n. (νK P j) (mIg K n P I) = LI K (νK P j) I
lemma mI_gen_in_I1:
[| 0 < n; distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n};
I ≠ carrier (OK P n) |]
==> mIg K n P I ∈ I
lemma mI_principalTr:
[| 0 < n; distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n};
I ≠ carrier (OK P n); x ∈ I |]
==> ∀j≤n. (νK P j) (mIg K n P I) ≤ (νK P j) x
lemma mI_principal:
[| 0 < n; distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n};
I ≠ carrier (OK P n) |]
==> I = (OK P n) ♦p (mIg K n P I)
lemma prime_n_pd_principal:
[| distinct_pds K n P; j ≤ n |] ==> PK P n j = (OK P n) ♦p (KbK n P) j
lemma ring_n_prod_primesTr:
[| 0 < n; distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n};
I ≠ carrier (OK P n) |]
==> ∀j≤n. (νK P j) (mprod_exp K (mL K P I) (KbK n P) n) = (νK P j) (mIg K n P I)
lemma ring_n_prod_primesTr1:
[| 0 < n; distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n};
I ≠ carrier (OK P n) |]
==> I = (OK P n) ♦p mprod_exp K (mL K P I) (KbK n P) n
lemma ring_n_prod_primes:
[| 0 < n; distinct_pds K n P; ideal (OK P n) I; I ≠ {\<zero>OK P n};
I ≠ carrier (OK P n); ∀k≤n. J k = (PK P n k) ♦(OK P n) nat (mL K P I k) |]
==> I = iΠOK P n,n J