Theory Valuation2

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

   chapter 1. elementary properties of a valuation
     section 8. approximation(continued)
    
   **)

theory Valuation2 
imports Valuation1
begin

lemma (in Corps) OstrowskiTr8:"valuation K v; x  carrier K; 
      0 < v (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
          xcarrier 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  
                        (xcarrier 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 "jnset (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 "jnset (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  (jnset (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  (jnset (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  
    xcarrier K. ((vv 0 x = 1)  (jnset (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. xcarrier 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. xcarrier K  (((vv  τ⇘0 j) 0 x 
                      = 1)  (knset (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 "xcarrier 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 "xcarrier 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 "xcarrier K.
            vv j x = 1  (janset (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 "xcarrier K. vv ((τ⇘0 j) 0) x = 1  
                     (janset (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)  
                      (jnset (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 "jnset (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
  "⇘n⇙C⇘i== n choose i"

lemma (in Ring) expansion_of_sum1:"x  carrier R  
                (1r ± x)^⇗R n= nsum R (λi.n⇙C⇘i⇙ ×⇘Rx^⇗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)⇙ ×⇘Rx^⇗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)⇙C⇘i⇙ ×⇘Rx^⇗R i) (Suc n)")
apply (subst aGroup.nsumTail[of R n "λi.(Suc n)⇙C⇘i⇙ ×⇘Rx^⇗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)⇙ ×⇘Rx^⇗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 n⇙C⇘Suc i⇙ ×⇘Rx^⇗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 n⇙C⇘Suc i⇙ ×⇘Rx^⇗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 ×⇘Kx)"
apply (cut_tac field_is_ring, induct_tac n, simp)  
apply (simp add:value_of_zero,
       simp,
       frule_tac y = "n ×⇘Kx" 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 n⇙C⇘Suc i⇙ ×⇘Kx^⇗K i) n)carrier (Vr K v)",
       frule Vr_mem_f_mem[of "v" "(nsum K (λi.Suc n⇙C⇘Suc i⇙ ×⇘Kx^⇗K i) n)"],
       assumption+,
       frule_tac x = x and y = "nsum K (λi.Suc n⇙C⇘Suc i⇙ ×⇘Kx^⇗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.(n⇙C⇘i+n⇙C⇘Suc i) ×⇘Kx^⇗K i) n"],
       frule aadd_le_mono[of "0" "v (nsum K (λi.(n⇙C⇘i+n⇙C⇘Suc i) ×⇘Kx^⇗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 n⇙C⇘Suc i⇙ ×⇘Kx^⇗K i⇖"], assumption, 
       rule allI, rule impI) apply (rule Ring.nsClose, assumption+) apply (simp add:Ring.npClose)

apply (rule allI, rule impI)
apply (cut_tac i = 0 and j = "v (x^⇗K j)" and k = "v (Suc n⇙C⇘Suc j⇙ ×⇘Kx^⇗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 n⇙C⇘Suc 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 ±