Theory Valuation2

theory Valuation2
imports Valuation1
(**        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)"], tactic ‹CHANGED distinct_subgoals_tac›, 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) ≠ 𝟬")
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 x = "Suc 0" in bspec,
        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 x = "j - Suc 0" in bspec, 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 x = "j - Suc 0" in bspec, assumption+)
 apply (simp add:nset_def)
done

lemma (in Corps) val_1_nonzero:"⟦valuation K v; x ∈ carrier K; v x = 1⟧ ⟹
                               x ≠ 𝟬"
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: less_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 of_nat_0_less_iff[THEN sym]) 
apply (cut_tac a = "0 < m" and b = "0 < int m" in a_b_exchange, simp,
       assumption)
apply (thin_tac "(0 < m) = (0 < int m)",
      frule val_nonzero_z[of "vv 0" "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 ≠ 𝟬; 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 x = j in bspec, assumption) 
apply (frule Ostrowski_elem_nonzero[of "n" "vv" "x"], assumption+,
       frule val_nonzero_z[of "vv j" "x"], assumption+, erule exE, simp,
       frule_tac a = za and x = z in zmult_pos_bignumTr,
       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 ≠ 𝟬; 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 b = "Suc l" in max.cobounded1[of "2"],
       cut_tac b = "Suc l" in max.cobounded2[of _ "2"],
       cut_tac n = l in lessI,
       frule_tac x = l and y = "Suc l" and z = "max 2 (Suc l)" in 
         less_le_trans, assumption+,
       thin_tac "Suc l ≤ max 2 (Suc l)", thin_tac "l < Suc l",
       drule_tac a = "max 2 (Suc l)" in forall_spec, simp,
       drule_tac a = "max 2 (Suc l)" in forall_spec, assumption) 
 apply (subgoal_tac "(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 ∘ (τ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

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

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

lemma (in Corps) Ostrowski_base_hom:"vals_nonequiv K (Suc n) vv ⟹ 
      Ostrowski_base K vv (Suc n) ∈ {h. h ≤ (Suc n)} → carrier K"
apply (rule Pi_I, rename_tac l,
       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 ∘ τ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 del:Pi_I')

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 ≠ 𝟬"
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 ∘ τ0 j" in forall_spec, assumption,
       rule someI2_ex, blast) 
apply (thin_tac "∃x∈carrier K. Ostrowski_elem K (Suc n) (vv ∘ τ0 j) x",
       erule conjE)
apply (rule_tac vv = "vv ∘ τ0 j" and x = x in Ostrowski_elem_nonzero[of "n"],
       assumption+)
done

lemma (in Corps) Ostrowski_base_pos:"⟦vals_nonequiv K (Suc n) vv; 
      j ≤ Suc n; ja ≤ Suc n; ja ≠ j⟧ ⟹ 0 < ((vv j) ((ΩK vv (Suc n)) ja))"
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 ∘ τ0 ja" in forall_spec, assumption+) 
apply (rule someI2_ex, blast,
       thin_tac "∃x∈carrier K. Ostrowski_elem K (Suc n) (vv ∘ τ0 ja) x",
       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 x = ja in bspec, simp add:nset_def,
       cut_tac  transpos_ij_2[of "0" "Suc n" "ja"], simp, simp+) 
apply (frule_tac x = j in bspec, simp add:nset_def,
       cut_tac transpos_id[of "0" "Suc n" "ja" "j"], simp+) 
done

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

lemma (in Corps) Approzimation1_5P2:"⟦vals_nonequiv K (Suc n) vv;
           ∀l∈{h. h ≤ Suc n}. n_val K (vv l) = vv l; i ≤ Suc n; j ≤ Suc n⟧
          ⟹ vv i (App_base K vv (Suc n) j) = δi j "
apply (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 x = i in bspec, simp add:nset_def, assumption) 

apply (frule_tac j = j in transpos_vals_nonequiv[of "n" "vv"], simp,
       frule Approximation1_5P[of "n" "vv ∘ τ0 j"],
       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 x = j in bspec, 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 x = i in bspec, simp add:nset_def,
       cut_tac transpos_id[of 0 "Suc n" j i], simp+)
done

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

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

lemma (in Corps) Ostrowski_baseTr0:"⟦vals_nonequiv K (Suc n) vv; l ≤ (Suc n) ⟧
   ⟹   0 < ((vv l) (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 ∘ τ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 x = l in bspec, simp add:nset_def,
       simp add:transpos_ij_2,
       drule_tac x = m in bspec, 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) ≠ 𝟬"
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)" "𝟬" 
           "(Ω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) = 𝟬")
 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

abbreviation
  CHOOSE :: "[nat, nat] ⇒ nat"  ("(_C_)" [80, 81]80) where
  "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 = 𝟬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 of_nat_less_iff[THEN sym],
        frule_tac a = "0 < j" and b = "int 0 < int j" in a_b_exchange,
        assumption, thin_tac "0 < j", thin_tac "(0 < j) = (int 0 < int j)")
apply (simp del: of_nat_0_less_iff)

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

 apply(rule_tac x = "x^K j" and n = "Suc 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 of_nat_less_iff[THEN sym])
apply (        frule_tac a = "0 < j" and b = "int 0 < int j" in a_b_exchange, 
        assumption+, thin_tac "0 < j", thin_tac "(0 < j) = (int 0 < int j)",
        frule_tac z = "int 0" and z' = "int j" in zless_imp_zle,
        frule_tac i = "int 0" and j = "int j" and k = z in int_mult_le,
         assumption+, simp add:mult.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 ≠ 𝟬; 
     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 
        undefined" and n = n in aGroup.nsum_eq[of "K" _ _ "g"])
 apply (rule allI, rule impI, simp,
        rule allI, simp, rule allI, rule impI, simp, simp)

 apply (cut_tac a = "x (Suc n) ⋅r (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 undefined) n ± -a (x l) = 
         Σe K (λa. if a ≤ n then x a ⋅r (1r ± -a (b a)) else undefined) n ±
         -a (x l)", simp,
         rule aGroup.ag_pOp_add_r[of K _ _ "-a (x l)"], assumption+,
         rule aGroup.nsum_mem, assumption+,
         rule allI, rule impI, simp, 
         rule aGroup.nsum_mem, assumption+,
         rule allI, rule impI, simp,
         rule aGroup.ag_mOp_closed, assumption, simp,
         rule aGroup.nsum_eq, assumption+,
         rule allI, rule impI, simp, rule allI, rule impI) 
   apply simp
   apply (rule allI, rule impI, simp) 
done

lemma (in Corps) eSum_minus_x:"⟦∀j ≤ n. (x j) ∈ carrier K; 
       ∀j ≤ n. (b j) ∈ carrier K; l ≤ n; 
       ∀j∈({h. h ≤ n} -{l}). (g j = (x j) ⋅r (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 ± 
 -aK 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 ± -aK vv (Suc n)) l^K N)^K N) else (x j) ⋅r (1r ± -a (1r ± -aK 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 ∘ (λ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 ∘ (λ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) ∘ x" "m"])
 apply (subgoal_tac "∀ja ≤ (Suc n). (vv j ∘ 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 ± -aK 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 x = N in spec)
 apply (drule_tac a = j in forall_spec, assumption,
        thin_tac "∀ja≤Suc n. 1r ± -a (1r ± -aK 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 ± -aK vv (Suc n)) j^K N)^K N ∈ carrier K",
         thin_tac "-a (1r ± -aK 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 x = j in bspec, 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
 
definition
  app_lb :: "[_ , nat, nat ⇒ 'b ⇒ ant, nat ⇒ 'b, nat] ⇒ 
            (nat ⇒ nat)"   ("(5Ψ_ _ _ _ _)" [98,98,98,98,99]98) where
  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) ⋅rK (1rK ±K -aK
  (1rK ±K -aK ((ΩK vv n) j)^K N)^K N)) n ±K -aK (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

definition
  distinct_pds :: "[_, nat, nat ⇒ ('b ⇒ ant) set] ⇒ bool" where
  "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

definition
  ring_n_pd :: "[('b, 'm) Ring_scheme, nat ⇒ ('b ⇒ ant) set,
                             nat ] ⇒ ('b, 'm) Ring_scheme"
                 ("(3O_ _ _)" [98,98,99]98) where
  "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

definition
  prime_n_pd :: "[_, nat ⇒ ('b ⇒ ant) set,
                             nat, nat] ⇒ 'b set"
                 ("(4P_ _ _ _)" [98,98,98,99]98) where
  "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 ⟹ 
                               𝟬(OK P n) = 𝟬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 "𝟬(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 = 𝟬(OK P n)",
        simp add:zero_in_ring_n_pd_zero_K)
 apply (simp add:value_of_zero)
 apply (subgoal_tac "y = 𝟬", 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 (x‐K)))")
 apply (subgoal_tac "(y ⋅r (x‐K)) ∈ 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 (x‐K)"], 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 (x‐K)"], 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 x = j in spec, 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  
 
definition
  mI_gen :: "[_ , nat ⇒ ('r ⇒ ant) set, nat, 'r set] ⇒ 'r" where
  "mI_gen K P n I = (SOME x. x ∈ I ∧ 
                             (∀j ≤ n. (νK (P j)) x = LI K (νK (P j)) I))"

definition
  mL :: "[_, nat ⇒ ('r ⇒ ant) set, 'r set, nat] ⇒ int" where
  "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 ≠ {𝟬(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 ≠ {𝟬(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 ≠ {𝟬(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 "𝟬OK P n" "I"])
 apply (frule sets_not_eq[of "I" "{𝟬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 x = a in bspec, 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 ≠ {𝟬(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 ≠ {𝟬(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 ≠ {𝟬(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

definition
  KbaseP :: "[_, nat ⇒ ('r ⇒ ant) set, nat] ⇒ 
                                          (nat ⇒ 'r) ⇒ bool"  where
  "KbaseP K P n f ⟷ (∀j ≤ n. f j ∈ carrier K) ∧ 
     (∀j ≤ n. ∀l ≤ n. (νK (P j)) (f l) =  (δj l))"

definition
  Kbase :: "[_, nat, nat ⇒ ('r ⇒ ant) set] 
               ⇒ (nat ⇒ 'r)" ("(3Kb_ _ _)" [95,95,96]95) where
  "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 ≠ 𝟬"
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 - {𝟬}"
by(simp add:Kbase_nonzero Kbase_hom)

definition
  Zl_mI :: "[_, nat ⇒ ('b ⇒ ant) set, 'b set]
                         ⇒ nat ⇒ 'b" where
  "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 ≠ {𝟬(OK P n)}; j ≤ n⟧ ⟹  Zl_mI K P I j ≠ 𝟬"
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 "𝟬" "I"], 
        frule sets_not_eq[of "I" "{𝟬}"], 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

definition
  mprod_exp :: "[_, nat ⇒ int, nat ⇒ 'b, nat] 
              ⇒ 'b" where
  "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 (simp)
 apply (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+)
done 

lemma (in Corps) mprod_Suc:"⟦ ∀j≤(Suc n). e j ∈ Zset; 
                ∀j ≤ (Suc n). f j ∈ (carrier K - {𝟬})⟧ ⟹ 
 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) - {𝟬})) ⟶ 
       (mprod_exp K e f n) ∈ ((carrier K) - {𝟬})" 
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) - {𝟬})⟧ ⟹  (mprod_exp K e f n) ∈ ((carrier K) - {𝟬})"
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) - {𝟬})⟧ ⟹ 
              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)-{𝟬(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+,
         simp add:cmp_def,
         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,
        simp,
        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)-{𝟬(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 - {𝟬})) ⟶
 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 - {𝟬})⟧ ⟹ 
     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 ≠ {𝟬(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) *aK (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) *aj ja)) (Suc n)")
apply (simp del:ASum_Suc)
apply (subgoal_tac "∀h ≤ (Suc n). (λja. (mL K P I ja) *aj ja)) h ∈ Z")
apply (cut_tac eSum_single[of "Suc n" "λja. (mL K P I ja) *aj 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 ≠ {𝟬(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 ≠ {𝟬(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) *aj 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 - {𝟬}")
apply (simp add:value_mprod_exp[of K (P j)" n "K_gamma k" "(KbK n P)"])
apply (subgoal_tac "ASum (λja. (γk ja) *aK (P j)) ((KbK n P) ja)) n
       = ASum (λja. (((γk ja) *aj ja)))) n")
 apply simp
 apply (subgoal_tac "∀j ≤ n. (λja. (γk ja) *aj ja)) j ∈ Z")
 apply (cut_tac eSum_single[of n "λja. ((γk ja) *aj 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 ≠ {𝟬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

definition
  m_zmax_pdsI_hom :: "[_, nat ⇒ ('b ⇒ ant) set, 'b set] ⇒ nat ⇒ int" where
  "m_zmax_pdsI_hom K P I = (λj. tna (AMin ((νK (P j)) ` I)))"

definition
  m_zmax_pdsI :: "[_, nat, nat ⇒ ('b ⇒ ant) set, 'b set] ⇒ int" where
  "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 ≠ {𝟬(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 ≠ {𝟬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 ≠ {𝟬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"])
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 ≠ {𝟬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 ≠ {𝟬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) ≠ 𝟬"
 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 ≠ {𝟬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 ≠ {𝟬(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 ≠ {𝟬(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 y = "tna (AMin (νK (P ja) ` I))" and z = "m_zmax n (λj. tna (AMin (νK (P j) ` I)))" in order_trans[of "0"], assumption+)
 apply (rule_tac y = "m_zmax n (λj. tna (AMin (νK (P j) ` I)))" and 
        z = "m_zmax n (λj. tna (AMin (νK (P j) ` I))) + 1" in order_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››

definition
  mIg :: "[_, nat, nat ⇒ ('b ⇒ ant) set,
             'b set] ⇒ 'b" ("(4mIg _ _ _ _)" [82,82,82,83]82) where
  "mIgK n P I = Σe K (λk. (Zl_mI K P I k) ⋅rK
             ((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 ≠ {𝟬(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 ≠ {𝟬(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 ≠ {𝟬(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 ≠ {𝟬(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 = 𝟬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 ≠ {𝟬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 ≠ {𝟬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 ≠ {𝟬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 (simp add:nat_def)
 apply (subst ring_n_pd_def) apply (simp add:Sr_def) 
 apply (rule Pi_I, 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"])
 </