Theory Valuation3

theory Valuation3
imports Valuation2
(**        Valuation3  
                            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 9. completion 
      subsection Hensel's theorem
   **)

theory Valuation3 
imports Valuation2
begin

section "Completion"

text‹In this section we formalize "completion" of the ground field K›

definition
  limit :: "[_, 'b ⇒ ant, nat ⇒ 'b, 'b]
           ⇒ bool" ("(4lim _ _ _ _)" [90,90,90,91]90) where
  "limK v f b ⟷ (∀N. ∃M. (∀n. M < n ⟶ 
                ((f n) ±K (-aK b)) ∈ (vp K v) (Vr K v) (an N)))"

(* In this definition, f represents a sequence of elements of K, which is
   converging to b. Key lemmas of this section are n_value_x_1 and
   n_value_x_2 *) 


lemma not_in_singleton_noneq:"x ∉ {a} ⟹ x ≠ a"
apply simp
done   (* later move this lemma to Algebra1 *) 

lemma noneq_not_in_singleton:"x ≠ a ⟹ x ∉ {a}"
apply simp
done

lemma inf_neq_1[simp]:"∞ ≠ 1"
by (simp only:ant_1[THEN sym], rule z_neq_inf[THEN not_sym, of 1])

lemma a1_neq_0[simp]:"(1::ant) ≠ 0"
by (simp only:an_1[THEN sym], simp only:an_0[THEN sym],
    subst aneq_natneq[of 1 0], simp)

lemma a1_poss[simp]:"(0::ant) < 1"
by (cut_tac zposs_aposss[of 1], simp)

lemma a_p1_gt[simp]:"⟦a ≠ ∞; a ≠ -∞⟧  ⟹ a < a + 1"
apply (cut_tac aadd_poss_less[of a 1],
       simp add:aadd_commute, assumption+) 
apply simp
done

lemma (in Corps) vpr_pow_inter_zero:"valuation K v ⟹ 
      (⋂ {I. ∃n. I = (vp K v)(Vr K v) (an n)}) = {𝟬}"
apply (frule Vr_ring[of v], frule vp_ideal[of v])
apply (rule equalityI) 
defer
 apply (rule subsetI)
 apply simp
 apply (rule allI, rule impI, erule exE, simp)
 apply (cut_tac n = "an n" in vp_apow_ideal[of v], assumption+)
 apply simp
 apply (cut_tac I = "(vp K v) (Vr K v) (an n)" in  Ring.ideal_zero[of "Vr K v"],
        assumption+)
 apply (simp add:Vr_0_f_0)

apply (rule subsetI, simp) 
 apply (rule contrapos_pp, simp+)
 apply (subgoal_tac "x ∈ vp K v")
 prefer 2 
 apply (drule_tac x = "vp K v (Vr K v) (an 1)" in spec)
 apply (subgoal_tac "∃n. vp K v (Vr K v) (an (Suc 0)) = vp K v (Vr K v) (an n)", 
        simp,
        thin_tac " ∃n. vp K v (Vr K v) (an (Suc 0)) = vp K v (Vr K v) (an n)")
 apply (simp add:r_apow_def an_def) 
 apply (simp only:na_1)
  apply (simp only:Ring.idealpow_1_self[of "Vr K v" "vp K v"])

  apply blast

apply (frule n_val_valuation[of v])

apply (frule_tac x = x in val_nonzero_z[of "n_val K v"],
       frule_tac h = x in Ring.ideal_subset[of "Vr K v" "vp K v"],
       assumption+,
       simp add:Vr_mem_f_mem, assumption+) apply (
       frule_tac h = x in Ring.ideal_subset[of "Vr K v" "vp K v"],
       simp add:Vr_mem_f_mem, assumption+)
apply (cut_tac x = x in val_pos_mem_Vr[of v], assumption) apply(
       simp add:Vr_mem_f_mem, simp) 
       apply (frule_tac x = x in val_pos_n_val_pos[of v],
       simp add:Vr_mem_f_mem, simp)
apply (cut_tac x = "n_val K v x" and y = 1 in aadd_pos_poss, assumption+,
       simp) apply (frule_tac y = "n_val K v x + 1" in aless_imp_le[of 0])
apply (cut_tac x1 = x and n1 = "(n_val K v x) + 1" in n_val_n_pow[THEN sym, 
       of v], assumption+) 
apply (drule_tac a = "vp K v (Vr K v) (n_val K v x + 1)" in forall_spec)
apply (erule exE, simp)
apply (simp only:ant_1[THEN sym] a_zpz,
       cut_tac z = "z + 1" in z_neq_inf)
 apply (subst an_na[THEN sym], assumption+, blast)
 apply simp
 apply (cut_tac a = "n_val K v x" in a_p1_gt)
 apply (erule exE, simp only:ant_1[THEN sym], simp only:a_zpz z_neq_inf)
 apply (cut_tac i = "z + 1" and j = z in ale_zle, simp)
 apply (erule exE, simp add:z_neq_minf)
 apply (cut_tac y1 = "n_val K v x" and x1 = "n_val K v x + 1" in 
        aneg_le[THEN sym], simp)
done 

lemma (in Corps) limit_diff_n_val:"⟦b ∈ carrier K; ∀j. f j ∈ carrier K; 
      valuation K v⟧ ⟹  (limK v f b) = (∀N. ∃M. ∀n. M < n ⟶ 
       (an N) ≤ (n_val K v ((f n) ± (-a b))))" 
apply (rule iffI)
apply (rule allI)
apply (simp add:limit_def) apply (rotate_tac -1)
 apply (drule_tac x = N in spec)
 apply (erule exE)
apply (subgoal_tac "∀n>M. (an N) ≤ (n_val K v (f n ± (-a b)))")
apply blast
 apply (rule allI, rule impI) apply (rotate_tac -2)
 apply (drule_tac x = n in spec, simp) 
 apply (rule n_value_x_1[of v], assumption+,
        simp add:an_nat_pos, assumption)

apply (simp add:limit_def)
 apply (rule allI, rotate_tac -1, drule_tac x = N in spec)

 apply (erule exE)
 apply (subgoal_tac "∀n>M. f n ± (-a b) ∈ vp K v (Vr K v) (an N)")
 apply blast
apply (rule allI, rule impI)
apply (rotate_tac -2, drule_tac x = n in spec, simp)
 apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
 apply (rule_tac x = "f n ± -a b" and n = "an N" in n_value_x_2[of "v"],
        assumption+) 
 apply (subst val_pos_mem_Vr[THEN sym, of "v"], assumption+)
 apply (drule_tac x = n in spec)
 apply (rule aGroup.ag_pOp_closed[of "K"], assumption+)
 apply (simp add:aGroup.ag_mOp_closed)
 apply (subst val_pos_n_val_pos[of  "v"], assumption+)
 apply (rule aGroup.ag_pOp_closed, assumption+) apply simp
 apply (simp add:aGroup.ag_mOp_closed)
 apply (rule_tac j = "an N" and k = "n_val K v ( f n ± -a b)" in 
        ale_trans[of "0"], simp, assumption+)   
        apply simp 
done

lemma (in Corps) an_na_Lv:"valuation K v ⟹ an (na (Lv K v)) = Lv K v" 
apply (frule Lv_pos[of "v"])
apply (frule aless_imp_le[of "0" "Lv K v"])
apply (frule apos_neq_minf[of "Lv K v"])
apply (frule Lv_z[of "v"], erule exE)
apply (rule an_na)
 apply (rule contrapos_pp, simp+)
done

lemma (in Corps) limit_diff_val:"⟦b ∈ carrier K; ∀j. f j ∈ carrier K; 
      valuation K v⟧ ⟹  (limK v f b) = (∀N. ∃M. ∀n. M < n ⟶ 
             (an N) ≤ (v ((f n) ± (-a b))))" 
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
       simp add:limit_diff_n_val[of "b" "f" "v"])
apply (rule iffI)
 apply (rule allI,
   rotate_tac -1, drule_tac x = N in spec, erule exE) 
 apply (subgoal_tac "∀n > M. an N ≤ v( f n ± -a b)", blast)
 apply (rule allI, rule impI)
 apply (drule_tac x = n in spec,
        drule_tac x = n in spec, simp) 
 apply (frule aGroup.ag_mOp_closed[of "K" "b"], assumption+,
     frule_tac x = "f n" and y = "-a b" in aGroup.ag_pOp_closed, assumption+)
 apply (frule_tac x = "f n ± -a b" in n_val_le_val[of "v"], 
         assumption+)
 apply (cut_tac n = N in an_nat_pos)
 apply (frule_tac j = "an N" and k = "n_val K v ( f n ± -a b)" in 
                   ale_trans[of "0"], assumption+)
 apply (subst val_pos_n_val_pos, assumption+)
 apply (rule_tac i = "an N" and j = "n_val K v ( f n ± -a b)" and 
        k = "v ( f n ± -a b)" in ale_trans, assumption+)
 apply (rule allI)
 apply (rotate_tac 3, drule_tac x = "N * (na (Lv K v))" in spec)
 apply (erule exE)
 apply (subgoal_tac "∀n. M < n ⟶ (an N) ≤ n_val K v (f n ± -a b)", blast)
 apply (rule allI, rule impI)
 apply (rotate_tac -2, drule_tac x = n in spec, simp)

  apply (drule_tac x = n in spec)
  apply (frule aGroup.ag_mOp_closed[of "K" "b"], assumption+,
      frule_tac x = "f n" and y = "-a b" in aGroup.ag_pOp_closed, assumption+)
 apply (cut_tac n = "N * na (Lv K v)" in an_nat_pos)
 apply (frule_tac i = 0 and j = "an (N * na (Lv K v))" and 
                  k = "v ( f n ± -a b)" in ale_trans, assumption+)
 apply (simp add:amult_an_an, simp add:an_na_Lv)
 apply (frule Lv_pos[of "v"])
 apply (frule_tac x1 = "f n ± -a b" in n_val[THEN sym, of v], 
        assumption+, simp)
 apply (frule Lv_z[of v], erule exE, simp)
 apply (simp add:amult_pos_mono_r)
done

text‹uniqueness of the limit is derived from ‹vp_pow_inter_zero››
lemma (in Corps) limit_unique:"⟦b ∈ carrier K; ∀j. f j ∈ carrier K; 
      valuation K v;  c ∈ carrier K; limK v f b; limK v f c⟧ ⟹  b = c" 
apply (rule contrapos_pp, simp+, simp add:limit_def,
       cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
       simp add:aGroup.ag_neq_diffnonzero[of "K" "b" "c"], 
       frule vpr_pow_inter_zero[THEN sym, of v], 
       frule noneq_not_in_singleton[of "b ± -a c" "𝟬"])
apply simp
apply (rotate_tac -1, erule exE, erule conjE)
apply (erule exE, simp, thin_tac "x = (vp K v)(Vr K v) (an n)")
apply (rotate_tac 3, drule_tac x = n in spec,
       erule exE,
       drule_tac x = n in spec,
       erule exE)
apply (rename_tac x N M1 M2)
apply (subgoal_tac "M1 < Suc (max M1 M2)",
       subgoal_tac "M2 < Suc (max M1 M2)",
       drule_tac x = "Suc (max M1 M2)" in spec,
       drule_tac x = "Suc (max M1 M2)" in spec,
       drule_tac x = "Suc (max M1 M2)" in spec)
 apply simp

(* We see (f (Suc (max xb xc)) +K -K b) +K (-K (f (Suc (max xb xc)) +K -K c)) ∈ vpr K G a i v ♢Vr K G a i v xa" *) 
 apply (frule_tac n = "an N" in vp_apow_ideal[of "v"], 
       frule_tac x = "f (Suc (max M1 M2)) ± -a b" and N = "an N" in 
       mem_vp_apow_mem_Vr[of "v"], simp,
       frule Vr_ring[of "v"],  simp, simp)
      
apply (frule Vr_ring[of "v"], 
       frule_tac I = "vp K v(Vr K v) (an N)" and x = "f (Suc (max M1 M2)) ± -a b"
       in Ring.ideal_inv1_closed[of "Vr K v"], assumption+)
 (** mOp of Vring and that of K is the same **)
apply (frule_tac I = "vp K v(Vr K v) (an N)" and h = "f (Suc (max M1 M2)) ± -a b"
 in Ring.ideal_subset[of "Vr K v"], assumption+)
 apply (simp add:Vr_mOp_f_mOp,
        cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
        frule aGroup.ag_mOp_closed[of "K" "b"], assumption+,
        simp add:aGroup.ag_p_inv, simp add:aGroup.ag_inv_inv)
 (** addition of  -K f (Suc (max xb xc)) +K b  and f (Suc (max xb xc)) +K -K c
    is included in vpr K G a i v ♢(Vr K G a i v) xa **)
 apply (frule_tac  I = "vp K v(Vr K v) (an N)" and x = 
 "-a (f (Suc (max M1 M2))) ± b " and y = "f (Suc (max M1 M2)) ± (-a c)" in 
  Ring.ideal_pOp_closed[of "Vr K v"], assumption+)
 apply (frule_tac x = "f (Suc (max M1 M2)) ± -a c" and N = "an N" in 
        mem_vp_apow_mem_Vr[of v], simp, assumption,
        frule_tac x = "-a (f (Suc (max M1 M2))) ± b" and N = "an N" in 
        mem_vp_apow_mem_Vr[of "v"], simp,
        simp add:Vr_pOp_f_pOp, simp add:Vr_pOp_f_pOp,
   frule aGroup.ag_mOp_closed[of "K" "c"], assumption+,
   frule_tac x = "f (Suc (max M1 M2))" in aGroup.ag_mOp_closed[of "K"], 
      assumption+,
   frule_tac x = "f (Suc (max M1 M2))" and y = "-a c" in 
      aGroup.ag_pOp_closed[of "K"], assumption+) 

apply (simp add:aGroup.ag_pOp_assoc[of "K" _ "b" _],
       simp add:aGroup.ag_pOp_assoc[THEN sym, of "K" "b" _ "-a c"],
       simp add:aGroup.ag_pOp_commute[of "K" "b"],
       simp add:aGroup.ag_pOp_assoc[of "K" _ "b" "-a c"],
       frule aGroup.ag_pOp_closed[of "K" "b" "-a c"], assumption+,
       simp add:aGroup.ag_pOp_assoc[THEN sym, of "K" _ _ "b ± -a c"],
       simp add:aGroup.ag_l_inv1, simp add:aGroup.ag_l_zero)
apply (simp add:aGroup.ag_pOp_commute[of "K" _ "b"])
apply arith apply arith
done


(** The following lemma will be used to prove lemma limit_t. This lemma and
 them next lemma show that the valuation v is continuous (see lemma 
 n_val **) 
lemma (in Corps) limit_n_val:"⟦b ∈ carrier K; b ≠ 𝟬; valuation K v; 
       ∀j. f j ∈ carrier K; limK v f b⟧ ⟹
       ∃N. (∀m. N < m ⟶ (n_val K v) (f m) = (n_val K v) b)"
apply (simp add:limit_def)
apply (frule n_val_valuation[of "v"])
apply (frule val_nonzero_z[of "n_val K v" "b"], assumption+, erule exE,
       rename_tac L)
apply (rotate_tac -3, drule_tac x = "nat (abs L + 1)" in spec)
apply (erule exE, rename_tac M)

    (* |L| + 1 ≤ (n_val K v ( f n +K -K b)). *) 
 apply (subgoal_tac "∀n. M < n ⟶ n_val K v (f n) = n_val K v b", blast)
 apply (rule allI, rule impI) 
 apply (rotate_tac -2, 
        drule_tac x = n in spec,
        simp)
apply (frule_tac x = "f n ± -a b" and n = "an (nat (¦L¦ + 1))" in 
       n_value_x_1[of "v"],
       thin_tac "f n ± -a b ∈ vp K v(Vr K v) (an (nat (¦L¦ + 1)))")
apply (simp add:an_def) 
 apply (simp add: zpos_apos [symmetric])
 apply assumption

 apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
 apply (frule aGroup.ag_mOp_closed[of "K" "b"], assumption+)
 
 apply (drule_tac x = n in spec, 
        frule_tac x = "f n" in aGroup.ag_pOp_closed[of "K" _ "-a b"], 
        assumption+,  
        frule_tac x = "b" and y = "(f n) ± (-a b)" in value_less_eq[of 
        "n_val K v"], assumption+)
 apply simp 
 apply (rule_tac x = "ant L" and y = "an (nat (¦L¦ + 1))" and 
        z = "n_val K v ( f n ± -a b)" in aless_le_trans)
 apply (subst an_def)
 apply (subst aless_zless) apply arith apply assumption+
 apply (simp add:aGroup.ag_pOp_commute[of "K" "b"])
 apply (simp add:aGroup.ag_pOp_assoc) apply (simp add:aGroup.ag_l_inv1)
 apply (simp add:aGroup.ag_r_zero)
done 

lemma (in Corps) limit_val:"⟦b ∈ carrier K; b ≠ 𝟬; ∀j. f j ∈ carrier K; 
      valuation K v; limK v f b⟧ ⟹ ∃N. (∀n. N < n ⟶ v (f n) = v b)"
apply (frule limit_n_val[of "b" "v" "f"], assumption+)
 apply (erule exE)
 apply (subgoal_tac "∀m. N < m ⟶ v (f m) = v b")
 apply blast
apply (rule allI, rule impI)
 apply (drule_tac x = m in spec)
 apply (drule_tac x = m in spec)
  apply simp
 apply (frule Lv_pos[of "v"])
 apply (simp add:n_val[THEN sym, of "v"])
done

lemma (in Corps) limit_val_infinity:"⟦valuation K v; ∀j. f j ∈ carrier K; 
      limK v f 𝟬⟧ ⟹ ∀N.(∃M. (∀m. M < m ⟶ (an N) ≤ (n_val K v (f m))))"
apply (simp add:limit_def)
 apply (rule allI)
 apply (drule_tac x = N in spec, 
        erule exE)
       
 apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
        simp only:aGroup.ag_inv_zero[of "K"], simp only:aGroup.ag_r_zero)
apply (subgoal_tac "∀n. M < n ⟶ an N ≤ n_val K v (f n)", blast)

 apply (rule allI, rule impI)
 apply (drule_tac x = n in spec,
        drule_tac x = n in spec, simp)
 apply (simp add:n_value_x_1)
done

lemma (in Corps) not_limit_zero:"⟦valuation K v; ∀j. f j ∈ carrier K; 
      ¬ (limK v f 𝟬)⟧ ⟹ ∃N.(∀M. (∃m. (M < m) ∧ 
                                    ((n_val K v) (f m)) < (an N)))"
apply (simp add:limit_def)
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
apply (simp add:aGroup.ag_inv_zero aGroup.ag_r_zero)
apply (erule exE)
 apply (case_tac "N = 0", simp add:r_apow_def) 
 apply (subgoal_tac "∀M. ∃n. M < n ∧ n_val K v (f n) < (an 0)") apply blast
 apply (rule allI, 
        rotate_tac 4, frule_tac x = M in spec,
        erule exE, erule conjE)
 apply (frule_tac x1 = "f n" in val_pos_mem_Vr[THEN sym, of "v"]) apply simp 
 apply simp
 apply (frule_tac x = "f n" in val_pos_n_val_pos[of "v"])
 apply simp apply simp apply (thin_tac "¬ 0 ≤ v (f n)")
 apply (simp add:aneg_le) apply blast

apply (simp)
 apply (subgoal_tac "∀n. ((f n) ∈ vp K v (Vr K v) (an N)) = 
                                ((an N) ≤ n_val K v (f n))")
 apply simp
 apply (thin_tac "∀n. (f n ∈ vp K v (Vr K v) (an N)) = (an N ≤ n_val K v (f n))")
 apply (simp add:aneg_le) apply blast

apply (rule allI)
 apply (thin_tac "∀M. ∃n. M < n ∧ f n ∉ vp K v (Vr K v) (an N)")
 apply (rule iffI)
 apply (frule_tac x1 = "f n" and n1 = "an N" in n_val_n_pow[THEN sym, of v])
 apply (rule_tac N = "an N" and x = "f n" in mem_vp_apow_mem_Vr[of v],
        assumption+, simp, assumption, simp, simp)
 apply (frule_tac x = "f n" and n = "an N" in n_val_n_pow[of "v"])
 apply (frule_tac x1 = "f n" in val_pos_mem_Vr[THEN sym, of "v"])
 apply simp
 apply (cut_tac n = N in an_nat_pos) 
 apply (frule_tac j = "an N" and k = "n_val K v (f n)" in ale_trans[of "0"],
         assumption+)
 apply (frule_tac x1 = "f n" in val_pos_n_val_pos[THEN sym, of "v"]) 
 apply simp+ 
done

lemma (in Corps) limit_p:"⟦valuation K v; ∀j. f j  ∈ carrier K; 
   ∀j. g j ∈ carrier K; b ∈ carrier K; c ∈ carrier K; limK v f b; limK v g c⟧
   ⟹ limK v (λj. (f j) ± (g j)) (b ± c)"
apply (simp add:limit_def)
 apply (rule allI) apply (rotate_tac 3,
       drule_tac x = N in spec,
       drule_tac x = N in spec,
       (erule exE)+) 
 apply (frule_tac x = M and y = Ma in two_inequalities, simp,
        subgoal_tac "∀n > (max M  Ma). (f n) ± (g n) ± -a (b ± c)
        ∈ (vp K v)(Vr K v) (an N)")
 apply (thin_tac "∀n. Ma < n ⟶ 
                     g n ± -a c ∈ (vp K v)(Vr K v) (an N)",
        thin_tac "∀n. M < n ⟶ 
                      f n ± -a b ∈(vp K v)(Vr K v) (an N)", blast)
 apply (frule Vr_ring[of v], 
        frule_tac n = "an N" in vp_apow_ideal[of v])
apply simp 
 apply (rule allI, rule impI)
 apply (thin_tac "∀n>M. f n ± -a b ∈ vp K v (Vr K v) (an N)",
        thin_tac "∀n>Ma. g n ± -a c ∈ vp K v (Vr K v) (an N)",
        frule_tac I = "vp K v(Vr K v) (an N)" and x = "f n ± -a b" 
        and y = "g n ± -a c" in Ring.ideal_pOp_closed[of "Vr K v"], 
        assumption+, simp, simp) 
apply (frule_tac I = "vp K v(Vr K v) (an N)" and h = "f n ± -a b" 
        in Ring.ideal_subset[of "Vr K v"], assumption+, simp,
        frule_tac I = "vp K v(Vr K v) (an N)" and h = "g n ± -a c" in
                   Ring.ideal_subset[of "Vr K v"], assumption+, simp)
 apply (simp add:Vr_pOp_f_pOp) 
 apply (thin_tac "f n ± -a b ∈ carrier (Vr K v)",
        thin_tac "g n ± -a c ∈ carrier (Vr K v)")

 apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
        frule aGroup.ag_mOp_closed[of "K" "b"], assumption+,
        frule aGroup.ag_mOp_closed[of "K" "c"], assumption+,
        frule_tac a = "f n" and b = "-a b" and c = "g n" and d = "-a c" in 
                  aGroup.ag_add4_rel[of "K"], simp+)
 apply (simp add:aGroup.ag_p_inv[THEN sym]) 
done

lemma (in Corps) Abs_ant_abs[simp]:"Abs (ant z) = ant (abs z)"
apply (simp add:Abs_def, simp add:aminus)
apply (simp only:ant_0[THEN sym], simp only:aless_zless)
apply (simp add:zabs_def)
done

lemma (in Corps) limit_t_nonzero:"⟦valuation K v; ∀(j::nat). (f j) ∈ carrier K; ∀(j::nat). g j ∈ carrier K;  b ∈ carrier K; c ∈ carrier K; b ≠ 𝟬; c ≠ 𝟬;
 limK v f b; limK v g c⟧ ⟹ limK v (λj. (f j) ⋅r (g j)) (b ⋅r c)"
apply (cut_tac field_is_ring, simp add:limit_def, rule allI) 
 apply (subgoal_tac "∀j. (f j) ⋅r (g j) ± -a (b ⋅r c) = 
 ((f j) ⋅r (g j) ± (f j) ⋅r (-a c)) ± ((f j) ⋅r c ± -a (b ⋅r c))", simp,
 thin_tac "∀j. f j ⋅r g j ± -a b ⋅r c =
             f j ⋅r g j ± f j ⋅r (-a c) ± (f j ⋅r c ± -a b ⋅r c)")
 apply (frule limit_n_val[of  "b" "v" "f"], assumption+,
        simp add:limit_def)
 apply (frule n_val_valuation[of "v"])
 apply (frule val_nonzero_z[of "n_val K v" "b"], assumption+, 
        rotate_tac -1, erule exE,
        frule val_nonzero_z[of "n_val K v" "c"], assumption+,
        rotate_tac -1, erule exE, rename_tac N bz cz)
 apply (rotate_tac 5, 
  drule_tac x = "N + nat (abs cz)" in spec, 
  drule_tac x = "N + nat (abs bz)" in spec)
  apply (erule exE)+ 
  apply (rename_tac N bz cz M M1 M2)
(** three inequalities together **)
apply (subgoal_tac "∀n. (max (max M1 M2) M) < n ⟶
 (f n) ⋅r (g n) ± (f n) ⋅r (-a c) ± ((f n) ⋅r c ± (-a (b ⋅r c)))
                  ∈ vp K v (Vr K v) (an N)",  blast)
apply (rule allI, rule impI) apply (simp, (erule conjE)+) 
 apply (rotate_tac 11, drule_tac x = n in spec,
      drule_tac x = n in spec, simp,
      drule_tac x = n in spec, simp)
 apply (frule_tac b = "g n ± -a c" and n = "an N" and x = "f n" in 
        convergenceTr1[of v])
 apply simp apply simp apply (simp add:an_def a_zpz[THEN sym]) apply simp
 apply (frule_tac b = "f n ± -a b" and n = "an N" in convergenceTr1[of  
  "v" "c"], assumption+, simp) apply (simp add:an_def)
   apply (simp add:a_zpz[THEN sym]) apply simp

 apply (drule_tac x = n in spec, 
        drule_tac x = n in spec)
 apply (simp add:Ring.ring_inv1_1[of "K" "b" "c"],
        cut_tac Ring.ring_is_ag, frule aGroup.ag_mOp_closed[of "K" "c"], 
        assumption+,
        simp add:Ring.ring_distrib1[THEN sym],
        frule aGroup.ag_mOp_closed[of "K" "b"], assumption+,
        simp add:Ring.ring_distrib2[THEN sym],
        subst Ring.ring_tOp_commute[of "K" _ "c"], assumption+,
        rule aGroup.ag_pOp_closed, assumption+) 
apply (cut_tac n = N in an_nat_pos)
apply (frule_tac n = "an N" in vp_apow_ideal[of "v"], assumption+)
apply (frule Vr_ring[of "v"]) 

apply (frule_tac x = "(f n) ⋅r (g n ± -a c)" and y = "c ⋅r (f n ± -a b)"
   and I = "vp K v (Vr K v) (an N)" in Ring.ideal_pOp_closed[of "Vr K v"], 
   assumption+)
apply (frule_tac R = "Vr K v" and I = "vp K v (Vr K v) (an N)" and 
       h = "(f n) ⋅r (g n ± -a c)" in Ring.ideal_subset, assumption+,
       frule_tac R = "Vr K v" and I = "vp K v (Vr K v) (an N)" and 
       h = "c ⋅r (f n ± -a b)" in Ring.ideal_subset, assumption+) 
apply (simp add:Vr_pOp_f_pOp, assumption+)
apply (rule allI)
 apply (thin_tac "∀N. ∃M. ∀n>M. f n ± -a b ∈ vp K v (Vr K v) (an N)",
        thin_tac "∀N. ∃M. ∀n>M. g n ± -a c ∈ vp K v (Vr K v) (an N)")
 apply (drule_tac x = j in spec,
        drule_tac x = j in spec,
        cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
       frule_tac x = "f j" and y = "g j" in Ring.ring_tOp_closed, assumption+,
       frule_tac x = "b" and y = "c" in Ring.ring_tOp_closed, assumption+,
       frule_tac x = "f j" and y = "c" in Ring.ring_tOp_closed, assumption+,
       frule_tac x = c in aGroup.ag_mOp_closed[of "K"], assumption+,
       frule_tac x = "f j" and y = "-a c" in Ring.ring_tOp_closed, assumption+,
       frule_tac x = "b ⋅r c" in aGroup.ag_mOp_closed[of "K"], assumption+)
 apply (subst aGroup.pOp_assocTr41[THEN sym, of "K"], assumption+,
        subst aGroup.pOp_assocTr42[of "K"], assumption+,
        subst Ring.ring_distrib1[THEN sym, of "K"], assumption+)
 apply (simp add:aGroup.ag_l_inv1, simp add:Ring.ring_times_x_0, 
        simp add:aGroup.ag_r_zero)
done

lemma an_npn[simp]:"an (n + m) = an n + an m"
by (simp add:an_def a_zpz) (** move **) 

lemma Abs_noninf:"a ≠ -∞ ∧ a ≠ ∞ ⟹ Abs a ≠ ∞"
by (cut_tac mem_ant[of "a"], simp, erule exE, simp add:Abs_def,
       simp add:aminus)

lemma (in Corps) limit_t_zero:"⟦c ∈ carrier K; valuation K v; 
      ∀(j::nat). f j ∈ carrier K; ∀(j::nat). g j ∈ carrier K;
      limK v f 𝟬; limK v g c⟧ ⟹ limK v (λj. (f j) ⋅r (g j)) 𝟬"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"], 
       simp add:limit_def, simp add:aGroup.ag_inv_zero, simp add:aGroup.ag_r_zero)
apply (subgoal_tac "∀j. (f j) ⋅r (g j) ∈ carrier K",
       simp add:aGroup.ag_r_zero)
 prefer 2 apply (rule allI, simp add:Ring.ring_tOp_closed)
apply (case_tac "c = 𝟬K")
 apply (simp add:aGroup.ag_inv_zero, simp add:aGroup.ag_r_zero)
 apply (rule allI,
        rotate_tac 4,
        drule_tac x = N in spec,
        drule_tac x = N in spec, (erule exE)+,
        rename_tac N M1 M2)
 apply (subgoal_tac "∀n>(max M1 M2). (f n) ⋅r (g n) ∈ (vp K v)(Vr K v) (an N)", 
        blast) 
 apply (rule allI, rule impI)
 apply (drule_tac x = M1 and y = M2 in two_inequalities, assumption+,
        thin_tac "∀n>M2. g n ∈ vp K v (Vr K v) (an N)")
apply (thin_tac "∀j. f j ⋅r g j ∈ carrier K",
       thin_tac "∀j. f j ∈ carrier K",
       thin_tac "∀j. g j ∈ carrier K",
       drule_tac x = n in spec, simp, erule conjE,
       erule conjE,
       frule Vr_ring[of v])
 apply (cut_tac n = N in an_nat_pos) 
 apply (frule_tac x = "f n" in mem_vp_apow_mem_Vr[of  "v"], assumption+,
        frule_tac x = "g n" in mem_vp_apow_mem_Vr[of  "v"], assumption+,
       frule_tac n = "an N" in vp_apow_ideal[of  "v"], assumption+)
 apply (frule_tac I = "vp K v(Vr K v) (an N)" and x = "g n" and 
        r = "f n" in Ring.ideal_ring_multiple[of "Vr K v"], assumption+,
        simp add:Vr_tOp_f_tOp)


 (** case c ≠ 0K **)
 apply (rule allI)
 apply (subgoal_tac "∀j. (f j) ⋅r (g j) = 
        (f j) ⋅r ((g j) ± (-a c)) ± (f j) ⋅r c", simp,
        thin_tac "∀j. (f j) ⋅r (g j) = 
        (f j) ⋅r ((g j) ± (-a c)) ± (f j) ⋅r c",
        thin_tac "∀j.  (f j) ⋅r ( g j ± -a c) ± (f j) ⋅r c ∈ carrier K")
apply (rotate_tac 4,
       drule_tac x = "N + na (Abs (n_val K v c))" in  spec,
       drule_tac x = N in spec)
 apply (erule exE)+ apply (rename_tac N M1 M2)
apply (subgoal_tac "∀n. (max M1 M2) < n ⟶ (f n) ⋅r (g n ± -a c) ± 
                     (f n) ⋅r  c ∈ vp K v(Vr K v) (an N)", blast)
apply (rule allI, rule impI, simp, erule conjE,
      drule_tac x = n in spec,
      drule_tac x = n in spec,
      drule_tac x = n in spec) 
apply (frule n_val_valuation[of "v"])
apply (frule value_in_aug_inf[of "n_val K v" "c"], assumption+, 
       simp add:aug_inf_def)
apply (frule val_nonzero_noninf[of "n_val K v" "c"], assumption+)
apply (cut_tac Abs_noninf[of "n_val K v c"])
apply (cut_tac Abs_pos[of "n_val K v c"]) apply (simp add:an_na)

apply (drule_tac x = n in spec, simp)
 apply (frule_tac b = "f n" and n = "an N" in convergenceTr1[of 
                                   "v" "c"], assumption+)
 apply simp

apply (frule_tac x = "f n" and N = "an N + Abs (n_val K v c)" in 
       mem_vp_apow_mem_Vr[of "v"], 
       frule_tac n = "an N" in vp_apow_ideal[of "v"])
      apply simp
apply (rule_tac x = "an N" and y = "Abs (n_val K v c)" in aadd_two_pos)
    apply simp apply (simp add:Abs_pos) apply assumption
   
apply (frule_tac x = "g n ± (-a c)" and N = "an N" in mem_vp_apow_mem_Vr[of 
       "v"], simp, assumption+) apply (
       frule_tac x = "c ⋅r (f n)" and N = "an N" in mem_vp_apow_mem_Vr[of 
       "v"], simp)  apply simp  
apply (simp add:Ring.ring_tOp_commute[of "K" "c"]) apply (
       frule Vr_ring[of  "v"], 
       frule_tac I = "(vp K v)(Vr K v) (an N)" and x = "g n ± (-a c)" 
       and r = "f n" in Ring.ideal_ring_multiple[of "Vr K v"]) 
apply (simp add:vp_apow_ideal) apply assumption+
apply (frule_tac I = "vp K v(Vr K v) (an N)" and 
       x = "(f n) ⋅r (g n ± -a c)" and y = "(f n) ⋅r c" in 
                      Ring.ideal_pOp_closed[of "Vr K v"])
    apply (simp add:vp_apow_ideal)
 apply (simp add:Vr_tOp_f_tOp,  assumption)
 apply (simp add:Vr_tOp_f_tOp Vr_pOp_f_pOp,
       frule_tac x = "(f n) ⋅r (g n ± -a c)" and N = "an N" in mem_vp_apow_mem_Vr[of "v"], simp add:Vr_pOp_f_pOp, assumption+)
 apply (frule_tac N = "an N" and x = "(f n) ⋅r c" in mem_vp_apow_mem_Vr[of 
        "v"]) apply simp apply assumption
 apply (simp add:Vr_pOp_f_pOp) apply simp

 apply (thin_tac "∀N. ∃M. ∀n>M. f n ∈ vp K v (Vr K v) (an N)",
        thin_tac "∀N. ∃M. ∀n>M. g n ± -a c ∈ vp K v (Vr K v) (an N)",
        rule allI)
 apply (drule_tac x = j in spec, 
    drule_tac x = j in spec,
    drule_tac x = j in spec,
    frule  aGroup.ag_mOp_closed[of "K" "c"], assumption+,
    frule_tac x = "f j" in Ring.ring_tOp_closed[of "K" _ "c"], assumption+,
    frule_tac x = "f j" in Ring.ring_tOp_closed[of "K" _ "-a c"], assumption+)
 apply (simp add:Ring.ring_distrib1, simp add:aGroup.ag_pOp_assoc, 
        simp add:Ring.ring_distrib1[THEN sym],
        simp add:aGroup.ag_l_inv1, simp add:Ring.ring_times_x_0, 
        simp add:aGroup.ag_r_zero)
done

lemma (in Corps) limit_minus:"⟦valuation K v; ∀j. f j ∈ carrier K; 
      b ∈ carrier K; limK v f b⟧ ⟹ limK v (λj. (-a (f j))) (-a b)"
apply (simp add:limit_def)
 apply (rule allI,
       rotate_tac -1, frule_tac x = N in spec,
        thin_tac "∀N. ∃M. ∀n. M < n ⟶  
                   f n ± -a b ∈ (vp K v)(Vr K v) (an N)",
       erule exE,
       subgoal_tac "∀n. M < n ⟶ 
           (-a (f n)) ± (-a (-a b)) ∈ (vp K v)(Vr K v) (an N)",
      blast) 
 apply (rule allI, rule impI,
        frule_tac x = n in spec,
        frule_tac x = n in spec, simp) 

apply (frule Vr_ring[of "v"],
       frule_tac n = "an N" in vp_apow_ideal[of "v"], simp)
apply (frule_tac x = "f n ± -a b" and N = "an N" in 
       mem_vp_apow_mem_Vr[of "v"], simp+,
       frule_tac I = "vp K v(Vr K v) (an N)" and x = "f n ± (-a b)" in 
       Ring.ideal_inv1_closed[of "Vr K v"], assumption+, simp) 
 apply (simp add:Vr_mOp_f_mOp) 
 apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
        frule aGroup.ag_mOp_closed[of "K" "b"], assumption+)
 apply (simp add:aGroup.ag_p_inv[of "K"])
done

lemma (in Corps) inv_diff:"⟦x ∈ carrier K; x ≠ 𝟬; y ∈ carrier K; y ≠ 𝟬⟧ ⟹
                (x‐K) ± (-a (y‐K)) = (x‐K) ⋅r ( y‐K) ⋅r (-a (x ± (-a y)))"
apply (cut_tac invf_closed1[of "x"], simp, erule conjE,
       cut_tac invf_closed1[of y], simp, erule conjE,
       cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
       frule Ring.ring_tOp_closed[of "K" "x‐K" "y‐K"], assumption+,
       frule aGroup.ag_mOp_closed[of "K" "x"], assumption+,
       frule aGroup.ag_mOp_closed[of "K" "y"], assumption+,
       frule aGroup.ag_mOp_closed[of "K" "x‐K"], assumption+,
       frule aGroup.ag_mOp_closed[of "K" "y‐K"], assumption+,
       frule aGroup.ag_pOp_closed[of "K" "x" "-a y"], assumption+) 
                                    
apply (simp add:Ring.ring_inv1_2[THEN sym],
       simp only:Ring.ring_distrib1[of "K" "(x‐K) ⋅r (y‐K)" "x" "-a y"],
       simp only:Ring.ring_tOp_commute[of "K" _ x],
       simp only:Ring.ring_inv1_2[THEN sym, of "K"], 
       simp only:Ring.ring_tOp_assoc[THEN sym],
       simp only:Ring.ring_tOp_commute[of "K" "x"],
       cut_tac linvf[of  "x"], simp+,
       simp add:Ring.ring_l_one, simp only:Ring.ring_tOp_assoc,
       cut_tac linvf[of "y"], simp+, 
       simp only:Ring.ring_r_one) 
apply (simp add:aGroup.ag_p_inv[of "K"], simp add:aGroup.ag_inv_inv,
       rule aGroup.ag_pOp_commute[of "K" "x‐K" "-a y‐K"], assumption+)
apply simp+
done

lemma times2plus:"(2::nat)*n = n + n"
by simp

lemma (in Corps) limit_inv:"⟦valuation K v; ∀j. f j ∈ carrier K; 
      b ∈ carrier K; b ≠ 𝟬; limK v f b⟧ ⟹ 
           limK v (λj. if (f j) = 𝟬 then 𝟬 else (f j)‐K) (b‐K)"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
apply (frule limit_n_val[of "b" "v" "f"], assumption+) 
apply (subst limit_def)
 apply (rule allI, erule exE)
 apply (subgoal_tac "∀m>Na. f m ≠ 𝟬") 
 prefer 2
 apply (rule allI, rule impI, rotate_tac -2,
        drule_tac x = m in spec, simp)
 apply (frule n_val_valuation[of v]) 
 apply (frule val_nonzero_noninf[of "n_val K v" b], assumption+)
 apply (rule contrapos_pp, simp+, simp add:value_of_zero)
 apply (unfold limit_def)
  apply (rotate_tac 2,
         frule_tac x = "N + 2*(na (Abs (n_val K v b)))" in 
         spec)
  apply (erule exE)
  apply (subgoal_tac "∀n>(max Na M).
          (if f n = 𝟬 then 𝟬 else f n‐K) ± -a b‐K ∈ vp K v(Vr K v) (an N)", 
         blast) 
  apply (rule allI, rule impI)
  apply (cut_tac x = "Na" and y = "max Na M" and z = n
         in le_less_trans)
  apply simp+
  apply (thin_tac "∀N. ∃M. ∀n>M. f n ± -a b ∈ vp K v (Vr K v) (an N)")
 apply (drule_tac x = n in spec,
        drule_tac x = n in spec,
        drule_tac x = n in spec,
        drule_tac x = n in spec, simp)
 apply (subst inv_diff, assumption+)
 apply (cut_tac x = "f n" in invf_closed1, simp,
        cut_tac x = b in invf_closed1, simp, simp, (erule conjE)+)
(* apply (frule field_is_idom[of "K"], frule field_iOp_closed[of "K" "b"], 
                                                 simp, simp, erule conjE,
        frule idom_tOp_nonzeros [of "K" "b‐K" "b‐K"], assumption+) *)
 apply (frule_tac n = "an N + an (2 * na (Abs (n_val K v b)))" and 
        x = "f n ± -a b" in n_value_x_1[of v])
 apply (simp only:an_npn[THEN sym], rule an_nat_pos) 
 apply assumption
 apply (rule_tac x = "f n‐ Kr b‐ Kr (-a (f n ± -a b))" and v = v and 
        n = "an N" in n_value_x_2, assumption+)
 apply (frule n_val_valuation[of v])
 apply (subst val_pos_mem_Vr[THEN sym, of "v"], assumption+)
  apply (rule Ring.ring_tOp_closed, assumption+)+
  apply (rule aGroup.ag_mOp_closed, assumption)
  apply (rule aGroup.ag_pOp_closed, assumption+,
         rule aGroup.ag_mOp_closed, assumption+)
  apply (subst val_pos_n_val_pos[of v], assumption+,
         rule Ring.ring_tOp_closed, assumption+,
         rule Ring.ring_tOp_closed, assumption+,
         rule aGroup.ag_mOp_closed, assumption+,
         rule aGroup.ag_pOp_closed, assumption+,
         rule aGroup.ag_mOp_closed, assumption+)
  apply (subst val_t2p[of "n_val K v"], assumption+,
         rule Ring.ring_tOp_closed, assumption+,
         rule aGroup.ag_mOp_closed, assumption+,
         rule aGroup.ag_pOp_closed, assumption+,
         rule aGroup.ag_mOp_closed, assumption+,
         subst val_minus_eq[of "n_val K v"], assumption+,
          (rule aGroup.ag_pOp_closed, assumption+),
          (rule aGroup.ag_mOp_closed, assumption+))
  apply (subst val_t2p[of "n_val K v"], assumption+)
  apply (simp add:value_of_inv)
  apply (frule_tac x = "an N + an (2 * na (Abs (n_val K v b)))" and y = "n_val K v (f n ± -a b)" and z = "- n_val K v b + - n_val K v b" in aadd_le_mono)
  apply (cut_tac z = "n_val K v b" in Abs_pos)
  apply (frule val_nonzero_z[of "n_val K v" b], assumption+, erule exE)
  apply (rotate_tac -1, drule sym, cut_tac z = z in z_neq_minf,
         cut_tac z = z in z_neq_inf, simp,
         cut_tac a = "(n_val K v b)" in Abs_noninf, simp)
  apply (simp only:times2plus an_npn, simp add:an_na)
  apply (rotate_tac -4, drule sym, simp)
  apply (thin_tac "f n ± -a b ∈ vp K v (Vr K v) (an N + (ant ¦z¦ + ant ¦z¦))")
  apply (simp add:an_def, simp add:aminus, (simp add:a_zpz)+)
  apply (subst aadd_commute)
  apply (rule_tac i = 0 and j = "ant (int N + 2 * ¦z¦ - 2 * z)" and 
         k = "n_val K v (f n ± -a b) + ant (- (2 * z))" in ale_trans)
  apply (subst ant_0[THEN sym])
  apply (subst ale_zle, simp, assumption)

  apply (frule n_val_valuation[of v])
  apply (subst val_t2p[of "n_val K v"], assumption+)
  apply (rule Ring.ring_tOp_closed, assumption+)+
  apply (rule aGroup.ag_mOp_closed, assumption)
  apply (rule aGroup.ag_pOp_closed, assumption+,
         rule aGroup.ag_mOp_closed, assumption+)
  apply (subst val_t2p[of "n_val K v"], assumption+) 
  apply (subst val_minus_eq[of "n_val K v"], assumption+,
         rule aGroup.ag_pOp_closed, assumption+,
         rule aGroup.ag_mOp_closed, assumption+)

  apply (simp add:value_of_inv)
  apply (frule_tac x = "an N + an (2 * na (Abs (n_val K v b)))" and y = "n_val K v (f n ± -a b)" and z = "- n_val K v b + - n_val K v b" in aadd_le_mono)
  apply (cut_tac z = "n_val K v b" in Abs_pos)
  apply (frule val_nonzero_z[of "n_val K v" b], assumption+, erule exE)
  apply (rotate_tac -1, drule sym, cut_tac z = z in z_neq_minf,
         cut_tac z = z in z_neq_inf, simp,
         cut_tac a = "(n_val K v b)" in Abs_noninf, simp)
  apply (simp only:times2plus an_npn, simp add:an_na)
  apply (rotate_tac -4, drule sym, simp)
  apply (thin_tac "f n ± -a b ∈ vp K v (Vr K v) (an N + (ant ¦z¦ + ant ¦z¦))")
  apply (simp add:an_def, simp add:aminus, (simp add:a_zpz)+)
  apply (subst aadd_commute)
  apply (rule_tac i = "ant (int N)" and j = "ant (int N + 2 * ¦z¦ - 2 * z)" 
        and k = "n_val K v (f n ± -a b) + ant (- (2 * z))" in ale_trans)
  apply (subst ale_zle, simp, assumption)
 
  apply simp
done

definition
  Cauchy_seq :: "[_ , 'b ⇒ ant, nat ⇒ 'b]
           ⇒ bool" ("(3Cauchy _ _ _)" [90,90,91]90) where
  "CauchyK v f ⟷ (∀n. (f n) ∈ carrier K) ∧ (
  ∀N. ∃M. (∀n m. M < n ∧ M < m ⟶ 
                ((f n) ±K (-aK (f m))) ∈ (vp K v)(Vr K v) (an N)))"

definition
  v_complete :: "['b ⇒ ant, _] ⇒ bool"
                    ("(2Complete_ _)"  [90,91]90) where
  "Completev K ⟷ (∀f. (CauchyK v f) ⟶ 
                           (∃b. b ∈ (carrier K) ∧ limK v f b))"

lemma (in Corps) has_limit_Cauchy:"⟦valuation K v; ∀j. f j ∈ carrier K; 
      b ∈ carrier K; limK v f b⟧ ⟹ CauchyK v f" 
apply (simp add:Cauchy_seq_def)
apply (rule allI)
apply (simp add:limit_def)
 apply (rotate_tac -1)
 apply (drule_tac x = N in spec)
 apply (erule exE)
 apply (subgoal_tac "∀n m. M < n ∧ M < m ⟶
                        f n ± -a (f m) ∈ vp K v(Vr K v) (an N)")
 apply blast
 apply ((rule allI)+, rule impI, erule conjE)
 apply (frule_tac x = n in spec,
        frule_tac x = m in spec,
        thin_tac "∀j. f j ∈ carrier K",
        frule_tac x = n in spec,
        frule_tac x = m in spec,
        thin_tac "∀n. M < n ⟶  f n ± -a b ∈ vp K v(Vr K v) (an N)",
        simp)
 apply (frule_tac n = "an N" in vp_apow_ideal[of v], simp)
 apply (frule Vr_ring[of "v"])
 apply (frule_tac x = "f m ± -a b" and I = "vp K v(Vr K v) (an N)" in 
           Ring.ideal_inv1_closed[of "Vr K v"], assumption+)
 apply (frule_tac h = "f m ± -a b" and I = "vp K v(Vr K v) (an N)" in 
           Ring.ideal_subset[of "Vr K v"], assumption+,
        frule_tac h = "f n ± -a b" and I = "vp K v(Vr K v) (an N)" in 
           Ring.ideal_subset[of "Vr K v"], assumption+)  
apply (frule_tac h = "-aVr K v (f m ± -a b)" and I = "vp K v(Vr K v) (an N)" in         Ring.ideal_subset[of "Vr K v"], assumption+,
       frule_tac h = "f n ± -a b" and I = "vp K v(Vr K v) (an N)" in 
        Ring.ideal_subset[of "Vr K v"], assumption+) 
apply (frule_tac I = "(vp K v) (Vr K v) (an N)" and x = "f n ± -a b" and
       y = "-a(Vr K v) (f m ± -a b)" in Ring.ideal_pOp_closed[of "Vr K v"],
       assumption+)
apply (simp add:Vr_pOp_f_pOp) apply (simp add:Vr_mOp_f_mOp)
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
 apply (frule aGroup.ag_mOp_closed[of "K" "b"], assumption+)
 apply (frule_tac x = "f m ± -a b" in Vr_mem_f_mem[of "v"], assumption+)
 apply (frule_tac x = "f m ± -a b" in aGroup.ag_mOp_closed[of "K"], 
         assumption+)
 apply (simp add:aGroup.ag_pOp_assoc)
 apply (simp add:aGroup.ag_pOp_commute[of "K" "-a b"])
 apply (simp add:aGroup.ag_p_inv[of "K"])
 apply (frule_tac x = "f m" in aGroup.ag_mOp_closed[of "K"], assumption+)
 apply (simp add:aGroup.ag_inv_inv)
 apply (simp add:aGroup.ag_pOp_assoc[of "K" _ "b" "-a b"])
 apply (simp add:aGroup.ag_r_inv1[of "K"], simp add:aGroup.ag_r_zero)
done

lemma (in Corps) no_limit_zero_Cauchy:"⟦valuation K v; CauchyK v f;
    ¬ (limK v f 𝟬)⟧ ⟹ 
 ∃N M. (∀m. N < m ⟶  ((n_val K v) (f M))  = ((n_val K v) (f m)))"
apply (frule not_limit_zero[of "v" "f"], thin_tac "¬ lim K v f 𝟬")
apply (simp add:Cauchy_seq_def, assumption) apply (erule exE)
apply (rename_tac L)
apply (simp add:Cauchy_seq_def, erule conjE,
       rotate_tac -1,
       frule_tac x = L in spec, thin_tac "∀N. ∃M. ∀n m. 
       M < n ∧ M < m ⟶ f n ± -a (f m) ∈ vp K v(Vr K v) (an N)")
apply (erule exE)
apply (drule_tac x = M in spec)
apply (erule exE, erule conjE)
apply (rotate_tac -3,
       frule_tac x = m in spec)
    apply (thin_tac "∀n m. M < n ∧ M < m ⟶
               f n ± -a (f m) ∈ (vp K v)(Vr K v) (an L)")
   apply (subgoal_tac "M < m ∧ (∀ma. M < ma ⟶ 
                             n_val K v (f m) = n_val K v (f ma))")
   apply blast
  apply simp
 
 apply (rule allI, rule impI)
 apply (rotate_tac -2)
 apply (drule_tac x = ma in spec)
 apply simp
 (** we have f ma ± -a f m ∈ vpr K G a i v ♢Vr K G a i v L as **) 
 apply (frule Vr_ring[of "v"], 
        frule_tac n = "an L" in vp_apow_ideal[of "v"], simp)
apply (frule_tac I = "vp K v(Vr K v) (an L)" and x = "f m ± -a (f ma)"
        in Ring.ideal_inv1_closed[of "Vr K v"], assumption+) apply (
        frule_tac I = "vp K v(Vr K v) (an L)" and 
        h = "f m ± -a (f ma)" in Ring.ideal_subset[of "Vr K v"], 
        assumption+, simp add:Vr_mOp_f_mOp)
   apply (frule_tac x = m in spec,
          drule_tac x = ma in spec)  apply (
         
          cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
          frule_tac x = "f ma" in aGroup.ag_mOp_closed[of "K"], assumption+,
          frule_tac x = "f m" and y = "-a (f ma)" in aGroup.ag_p_inv[of "K"],
          assumption+, simp only:aGroup.ag_inv_inv,
          frule_tac x = "f m" in aGroup.ag_mOp_closed[of "K"], assumption+,
          simp add:aGroup.ag_pOp_commute,
          thin_tac "-a ( f m ± -a (f ma)) =  f ma ± -a (f m)",
          thin_tac "f m ± -a (f ma) ∈ vp K v(Vr K v) (an L)")
  (** finally, by f ma = f m ± (f ma ± -a (f m)) and value_less_eq 
      we have the conclusion **)
   apply (frule_tac x = "f ma ± -a (f m)" and n = "an L" in n_value_x_1[of 
         "v" ], simp) apply assumption apply (
         frule n_val_valuation[of "v"], 
         frule_tac x = "f m" and y = "f ma ± -a (f m)" in value_less_eq[of 
         "n_val K v"], assumption+) apply (simp add:aGroup.ag_pOp_closed) 
  apply (
         rule_tac x = "n_val K v (f m)" and y = "an L" and
         z = "n_val K v ( f ma ± -a (f m))" in  
         aless_le_trans, assumption+) 
  apply (frule_tac x = "f ma ± -a (f m)" in Vr_mem_f_mem[of "v"])
  apply (simp add:Ring.ideal_subset)
  apply (frule_tac x = "f m" and y = "f ma ± -a (f m)" in 
         aGroup.ag_pOp_commute[of "K"], assumption+) 
  apply (simp add:aGroup.ag_pOp_assoc,
         simp add:aGroup.ag_l_inv1, simp add:aGroup.ag_r_zero)
done 

lemma (in Corps) no_limit_zero_Cauchy1:"⟦valuation K v; ∀j. f j ∈ carrier K; 
  CauchyK v f; ¬ (limK v f 𝟬)⟧ ⟹ ∃N M. (∀m. N < m ⟶  v (f M) = v (f m))"
apply (frule no_limit_zero_Cauchy[of "v" "f"], assumption+)
 apply (erule exE)+
 apply (subgoal_tac "∀m. N < m ⟶ v (f M) = v (f m)") apply blast
 apply (rule allI, rule impI)
 apply (frule_tac x = M in spec,
        drule_tac x = m in spec,
        drule_tac x = m in spec, simp)
 apply (simp add:n_val[THEN sym, of "v"])
done
 
definition
  subfield :: "[_, ('b, 'm1) Ring_scheme] ⇒ bool" where
  "subfield K K' ⟷ Corps K' ∧ carrier K ⊆ carrier K' ∧ 
                   idmap (carrier K) ∈ rHom K K'"

definition
  v_completion :: "['b ⇒ ant, 'b ⇒ ant, _, ('b, 'm) Ring_scheme] ⇒ bool" 
               ("(4Completion_ _ _ _)" [90,90,90,91]90) where
  "Completionv v' K K' ⟷ subfield K K' ∧
      Completev' K' ∧ (∀x ∈ carrier K. v x = v' x) ∧
      (∀x ∈ carrier K'. (∃f. CauchyK v f ∧ limK' v' f x))"

lemma (in Corps) subfield_zero:"⟦Corps K'; subfield K K'⟧ ⟹ 𝟬K = 𝟬K'"
apply (simp add:subfield_def, (erule conjE)+)
apply (simp add:rHom_def, (erule conjE)+)
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
       frule Corps.field_is_ring[of "K'"], frule Ring.ring_is_ag[of "K'"])
apply (frule aHom_0_0[of "K" "K'" "IK"], assumption+)
apply (frule aGroup.ag_inc_zero[of "K"], simp add:idmap_def)
done

lemma (in Corps) subfield_pOp:"⟦Corps K'; subfield K K'; x ∈ carrier K;
      y ∈ carrier K⟧ ⟹ x ± y = x ±K' y"
apply (cut_tac field_is_ring, frule Corps.field_is_ring[of "K'"],
       frule Ring.ring_is_ag[of "K"], frule Ring.ring_is_ag[of "K'"])
apply (simp add:subfield_def, erule conjE, simp add:rHom_def,
       frule conjunct1)
apply (thin_tac "IK ∈ aHom K K' ∧
     (∀x∈carrier K. ∀y∈carrier K. IK (x ⋅r y) = IK x ⋅rK' IK y) ∧
     IK 1r = 1rK'")
apply (frule aHom_add[of "K" "K'" "IK" "x" "y"], assumption+,
       frule aGroup.ag_pOp_closed[of "K" "x" "y"], assumption+, 
       simp add:idmap_def)
done

lemma (in Corps) subfield_mOp:"⟦Corps K'; subfield K K'; x ∈ carrier K⟧ ⟹ 
                     -a x = -aK' x"
apply (cut_tac field_is_ring, frule Corps.field_is_ring[of "K'"],
       frule Ring.ring_is_ag[of "K"], frule Ring.ring_is_ag[of "K'"])
apply (simp add:subfield_def, erule conjE, simp add:rHom_def,
       frule conjunct1)
apply (thin_tac "IK ∈ aHom K K' ∧
     (∀x∈carrier K. ∀y∈carrier K. IK (x ⋅r y) = IK x ⋅rK' IK y) ∧
     IK 1r = 1rK'")
apply (frule aHom_inv_inv[of "K" "K'" "IK" "x"], assumption+,
       frule aGroup.ag_mOp_closed[of "K" "x"], assumption+)
apply (simp add:idmap_def)
done

lemma (in Corps) completion_val_eq:"⟦Corps K'; valuation K v; valuation K' v'; 
 x ∈ carrier K;  Completionv v' K K'⟧ ⟹ v x = v' x"
apply (unfold v_completion_def, (erule conjE)+)
apply simp
done

lemma (in Corps) completion_subset:"⟦Corps K'; valuation K v; valuation K' v'; 
 Completionv v' K K'⟧ ⟹  carrier K ⊆ carrier K'"
apply (unfold v_completion_def, (erule conjE)+)
apply (simp add:subfield_def)
done

lemma (in Corps) completion_subfield:"⟦Corps K'; valuation K v; 
       valuation K' v'; Completionv v' K K'⟧ ⟹  subfield K K'"
apply (simp add:v_completion_def)
done

lemma (in Corps) subfield_sub:"subfield K K' ⟹ carrier K ⊆ carrier K'"
apply (simp add:subfield_def)
done

lemma (in Corps) completion_Vring_sub:"⟦Corps K'; valuation K v; 
  valuation K' v'; Completionv v' K K'⟧ ⟹ 
                     carrier (Vr K v) ⊆ carrier (Vr K' v')"
apply (rule subsetI,
      frule completion_subset[of  "K'" "v" "v'"], assumption+,
      frule_tac x = x in Vr_mem_f_mem[of "v"], assumption+,
      frule_tac x = x in completion_val_eq[of "K'" "v" "v'"],
        assumption+)
apply (frule_tac x1 = x in val_pos_mem_Vr[THEN sym, of  "v"],
       assumption+, simp,
       frule_tac c = x in subsetD[of "carrier K" "carrier K'"], assumption+,
      simp add:Corps.val_pos_mem_Vr[of "K'" "v'"])
done

lemma (in Corps) completion_idmap_rHom:"⟦Corps K'; valuation K v; 
  valuation K' v';  Completionv v' K K'⟧ ⟹ 
             I(Vr K v) ∈ rHom (Vr K v) (Vr K' v')"
apply (frule completion_Vring_sub[of  "K'" "v" "v'"],
         assumption+,
       frule completion_subfield[of "K'" "v" "v'"], 
         assumption+,
       frule Vr_ring[of "v"],
        frule Ring.ring_is_ag[of "Vr K v"],
       frule Corps.Vr_ring[of "K'" "v'"], assumption+,
       frule Ring.ring_is_ag[of "Vr K' v'"])
apply (simp add:rHom_def)
apply (rule conjI) 
 apply (simp add:aHom_def,
        rule conjI,
        simp add:idmap_def, simp add:subsetD)
apply (rule conjI)
 apply (simp add:idmap_def extensional_def)
 apply ((rule ballI)+) apply (
        frule_tac x = a and y = b in aGroup.ag_pOp_closed, assumption+,
        simp add:idmap_def, 
   frule_tac c = a in subsetD[of "carrier (Vr K v)" 
                         "carrier (Vr K' v')"], assumption+,
   frule_tac c = b in subsetD[of "carrier (Vr K v)" 
                         "carrier (Vr K' v')"], assumption+,
   simp add:Vr_pOp_f_pOp,
   frule_tac x = a in Vr_mem_f_mem[of v], assumption,
   frule_tac x = b in Vr_mem_f_mem[of v], assumption,
   simp add:Corps.Vr_pOp_f_pOp,
   simp add:subfield_pOp)
apply (rule conjI)
 apply ((rule ballI)+, 
        frule_tac x = x and y = y in Ring.ring_tOp_closed, assumption+,
        simp add:idmap_def, simp add:subfield_def, erule conjE)
 apply (frule_tac c = x in subsetD[of "carrier (Vr K v)" 
            "carrier (Vr K' v')"], assumption+,
        frule_tac c = y in subsetD[of "carrier (Vr K v)" 
            "carrier (Vr K' v')"], assumption+)
 apply (simp add:Vr_tOp_f_tOp Corps.Vr_tOp_f_tOp)
apply (frule_tac x = x in Vr_mem_f_mem[of "v"], assumption+,
       frule_tac x = y in Vr_mem_f_mem[of "v"], assumption+,
     frule_tac x = x in Corps.Vr_mem_f_mem[of "K'" "v'"], assumption+,
     frule_tac x = y in Corps.Vr_mem_f_mem[of "K'" "v'"], assumption+,
       cut_tac field_is_ring, frule Corps.field_is_ring[of "K'"],
       frule_tac x = x and y = y in Ring.ring_tOp_closed[of "K"], assumption+)
apply (frule_tac x = x and y = y in rHom_tOp[of "K" "K'" _ _ "IK"], 
                 assumption+, simp add:idmap_def)
apply (frule Ring.ring_one[of "Vr K v"], simp add:idmap_def)
apply (simp add:Vr_1_f_1 Corps.Vr_1_f_1)
apply (simp add:subfield_def, (erule conjE)+)
apply (cut_tac field_is_ring, frule Corps.field_is_ring[of "K'"],
       frule Ring.ring_one[of "K"],
       frule rHom_one[of "K" "K'" "IK"], assumption+, simp add:idmap_def)
done

lemma (in Corps) completion_vpr_sub:"⟦Corps K'; valuation K v; valuation K' v';
      Completionv v' K K'⟧ ⟹ vp K v ⊆ vp K' v'"
apply (rule subsetI,
      frule completion_subset[of "K'" "v" "v'"], assumption+,
      frule Vr_ring[of "v"], frule vp_ideal[of "v"],
        frule_tac h = x in Ring.ideal_subset[of "Vr K v" "vp K v"],
        assumption+,
      frule_tac x = x in Vr_mem_f_mem[of  "v"], assumption+,
      frule_tac x = x in completion_val_eq[of "K'" "v" "v'"],
        assumption+)
apply (frule completion_subset[of "K'" "v" "v'"],
        assumption+,
       frule_tac c = x in subsetD[of "carrier K" "carrier K'"], assumption+,
       simp add:Corps.vp_mem_val_poss vp_mem_val_poss)
done

lemma (in Corps) val_v_completion:"⟦Corps K'; valuation K v; valuation K' v'; 
      x ∈ carrier K'; x ≠ 𝟬K'; Completionv v' K K'⟧ ⟹
   ∃f. (CauchyK v f) ∧ (∃N. (∀m. N < m ⟶ v (f m) = v' x))"
apply (simp add:v_completion_def, erule conjE, (erule conjE)+)
 apply (rotate_tac -1, drule_tac x = x in bspec, assumption+,
        erule exE, erule conjE,
        subgoal_tac "∃N. ∀m. N < m ⟶ v (f m) = v' x", blast) 
    thm Corps.limit_val
 apply (frule_tac f = f and v = v' in  Corps.limit_val[of "K'" "x"],
        assumption+,
        unfold Cauchy_seq_def, frule conjunct1, fold Cauchy_seq_def) 
apply (rule allI, drule_tac x = j in spec,
       simp add:subfield_def, erule conjE, simp add:subsetD, assumption+)
 apply (simp add:Cauchy_seq_def)
done

lemma (in Corps) v_completion_v_limit:"⟦Corps K'; valuation K v; 
      x ∈ carrier K; subfield K K'; Completev' K'; ∀j. f j ∈ carrier K;  
      valuation K' v'; ∀x∈carrier K. v x = v' x; limK' v' f x⟧ ⟹ limK v f x"
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
       frule Corps.field_is_ring[of K'], frule Ring.ring_is_ag[of "K'"],
       subgoal_tac "∀j. f j ∈ carrier K'",
       unfold subfield_def, frule conjunct2, fold subfield_def, erule conjE)
apply (frule subsetD[of "carrier K" "carrier K'" "x"], assumption+,
       simp add:limit_diff_val[of "x" "f"],
       subgoal_tac "∀n. f n ±K' -aK' x = f n ± -a x")
 apply (rule allI)
 apply (simp add:limit_def)
 apply (rotate_tac 6, drule_tac x = N in spec,
        erule exE)
 apply (subgoal_tac "∀n>M. an N ≤ v'(f n ± -a x)",
        subgoal_tac "∀n. (v' (f n ± -a x) = v (f n ± -a x))", simp, blast)
 apply (rule allI)
 apply (frule_tac x = "f n ± -a x" in bspec,
        rule aGroup.ag_pOp_closed, assumption+, simp,
        rule aGroup.ag_mOp_closed, assumption+) apply simp
 apply (rule allI, rule impI)
 apply (frule_tac v = v' and n = "an N" and x = "f n ± -a x" in 
         Corps.n_value_x_1[of K'], assumption+, simp, simp)
 apply (frule_tac v = v' and x = "f n ± -a x" in Corps.n_val_le_val[of K'],
         assumption+) 
 apply (cut_tac x = "f n" and y = "-a x" in aGroup.ag_pOp_closed, assumption,
        simp, rule aGroup.ag_mOp_closed, assumption+, simp add:subsetD)
 apply (subst Corps.val_pos_n_val_pos[of K' v'], assumption+)
   apply (cut_tac x = "f n" and y = "-a x" in aGroup.ag_pOp_closed, assumption,
        simp, rule aGroup.ag_mOp_closed, assumption+, simp add:subsetD)
apply (rule_tac i = 0 and j = "an N" and k = "n_val K' v' (f n ± -a x)" in 
       ale_trans, simp+, rule allI)
 apply (subst subfield_pOp[of K'], assumption+, simp+,
        rule aGroup.ag_mOp_closed, assumption+)
 apply (simp add:subfield_mOp[of K'])
 apply (cut_tac subfield_sub[of K'], simp add:subsetD, assumption+)
done
    
lemma (in Corps) Vr_idmap_aHom:"⟦Corps K'; valuation K v; valuation K' v'; 
      subfield K K'; ∀x∈carrier K. v x = v' x⟧ ⟹ 
                              I(Vr K v) ∈ aHom (Vr K v) (Vr K' v')"
apply (simp add:aHom_def)
apply (subgoal_tac "I(Vr K v) ∈ carrier (Vr K v) → carrier (Vr K' v')")
apply simp
apply (rule conjI)
 apply (simp add:idmap_def)
apply (rule ballI)+
 apply (frule Vr_ring[of "v"],
        frule Ring.ring_is_ag[of "Vr K v"],
        frule Corps.Vr_ring[of "K'" "v'"], assumption+,
        frule Ring.ring_is_ag[of "Vr K' v'"]) 
 apply (frule_tac x = a and y = b in aGroup.ag_pOp_closed[of "Vr K v"],
               assumption+,
        frule_tac x = a in funcset_mem[of "I(Vr K v)" 
        "carrier (Vr K v)" "carrier (Vr K' v')"], assumption+,
        frule_tac x = b in funcset_mem[of "I(Vr K v)" 
        "carrier (Vr K v)" "carrier (Vr K' v')"], assumption+,
        frule_tac x = "(I(Vr K v)) a" and y = "(I(Vr K v)) b" in 
        aGroup.ag_pOp_closed[of "Vr K' v'"], assumption+, 
        simp add:Vr_pOp_f_pOp)
 apply (simp add:idmap_def, simp add:subfield_def, erule conjE,
        simp add:rHom_def, frule conjunct1,
        thin_tac "IK ∈ aHom K K' ∧
           (∀x∈carrier K. ∀y∈carrier K. IK (x ⋅r y) = IK x ⋅rK' IK y) ∧
           IK 1r = 1rK'")
  apply (simp add:Corps.Vr_pOp_f_pOp[of K' v'])
  apply (frule_tac x = a in Vr_mem_f_mem[of v], assumption+,
         frule_tac x = b in Vr_mem_f_mem[of v], assumption+)
  apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of K],
         frule Corps.field_is_ring[of K'], frule Ring.ring_is_ag[of K']) 
  apply (frule_tac a = a and b = b in aHom_add[of K K' "IK"], assumption+,
         frule_tac x = a and y = b in aGroup.ag_pOp_closed[of K], assumption+,
         simp add:idmap_def)
apply (rule Pi_I,
       drule_tac x = x in bspec, simp add:Vr_mem_f_mem)
apply (simp add:idmap_def)
 apply (frule_tac x1 = x in val_pos_mem_Vr[THEN sym, of v],
         simp add:Vr_mem_f_mem, simp)
 apply (subst Corps.val_pos_mem_Vr[THEN sym, of K' v'], assumption+,
        frule_tac x = x in Vr_mem_f_mem[of v], assumption+,
        frule subfield_sub[of K'], simp add:subsetD)
 apply assumption
done

lemma amult_pos_pos:"0 ≤ a ⟹ 0 ≤ a * an N"
apply (case_tac "N = 0", simp add:an_0)
 apply (case_tac "a = ∞", simp) 
 apply (frule apos_neq_minf[of a])
 apply (subst ant_tna[THEN sym, of a], simp)
 apply (subst amult_0_r, simp)
apply (case_tac "a = ∞", simp add:an_def) 
 apply (frule apos_neq_minf[of a])
 apply (subst ant_tna[THEN sym, of a], simp)
 apply (case_tac "a = 0", simp)
 apply (simp add:ant_0 an_def amult_0_l)
apply (cut_tac amult_pos1[of "tna a" "an N"]) 
 apply (simp add:ant_tna)
 apply (rule_tac ale_trans[of 0 "an N" "a * an N"], simp+)
 apply (frule ale_neq_less[of 0 a], rule not_sym, assumption)
 apply (subst aless_zless[THEN sym, of 0 "tna a"], simp add:ant_tna ant_0)
 apply simp
done

lemma (in Corps) Cauchy_down:"⟦Corps K'; valuation K v; valuation K' v'; 
  subfield K K'; ∀x∈carrier K. v x = v' x; ∀j. f j ∈ carrier K; CauchyK' v' f⟧ 
  ⟹  CauchyK v f" 
apply (simp add:Cauchy_seq_def, rule allI, erule conjE) 
apply (rotate_tac -1, drule_tac 
  x = "na (Lv K v) * N" in spec,
  erule exE,
  subgoal_tac "∀n m. M < n ∧ M < m ⟶
      f n ± (-a (f m)) ∈ vp K v(Vr K v) (an N)", blast)
 apply (simp add:amult_an_an) apply (simp add:an_na_Lv)
 apply ((rule allI)+, rule impI, erule conjE) apply (
      rotate_tac -3, drule_tac x = n in spec,
      rotate_tac -1, drule_tac x = m in spec,
      simp)
 apply (rotate_tac 7,
        frule_tac x = n in spec,
        drule_tac x = m in spec)
 apply (simp add:subfield_mOp[THEN sym],
        cut_tac field_is_ring, frule Ring.ring_is_ag[of K],
        frule_tac x = "f m" in aGroup.ag_mOp_closed[of K], assumption+)
 apply (simp add:subfield_pOp[THEN sym])
 apply (frule_tac x = "f n" and y = "-a f m" in aGroup.ag_pOp_closed, 
        assumption+,
        frule subfield_sub[of K'],
        frule_tac c = "f n ± -a f m" in subsetD[of "carrier K" "carrier K'"], 
        assumption+)
 apply (frule Lv_pos[of v],
        frule aless_imp_le[of 0 "Lv K v"])
 apply (frule_tac N = N in amult_pos_pos[of "Lv K v"])
 apply (frule_tac n = "(Lv K v) * an N" and x = "f n ± -a f m" in 
        Corps.n_value_x_1[of K' v'], assumption+)
 apply (frule_tac x = "f n ± -a f m" in Corps.n_val_le_val[of K' v'],
        assumption+,
        frule_tac j = "Lv K v * an N" and k = "n_val K' v' (f n ± -a f m)" in
         ale_trans[of 0], assumption+, simp add:Corps.val_pos_n_val_pos)
 apply (frule_tac i = "Lv K v * an N" and j = "n_val K' v' (f n ± -a f m)" 
        and k = "v' (f n ± -a f m)" in ale_trans, assumption+,
        thin_tac "n_val K' v' (f n ± -a f m) ≤ v' (f n ± -a f m)",
        thin_tac "Lv K v * an N ≤ n_val K' v' (f n ± -a f m)")
 apply (rotate_tac 1,
        drule_tac x = "f n ± -a f m" in bspec, assumption,
        rotate_tac -1, drule sym, simp)
 apply (frule_tac v1 = v and x1 = "f n ± -a f m" in n_val[THEN sym],
        assumption)
 apply simp
 apply (simp only:amult_commute[of _ "Lv K v"])
apply (frule Lv_z[of v], erule exE)
 
apply (cut_tac w = z and x = "an N" and y = "n_val K v (f n ± -a f m)" in
       amult_pos_mono_l,
       cut_tac m = 0 and n = z in aless_zless, simp add:ant_0)
 apply simp
 apply (rule_tac x="f n ± -a (f m)" and n = "an N" in n_value_x_2[of v], 
        assumption+) 
 apply (subst val_pos_mem_Vr[THEN sym, of v], assumption+)
 apply (subst val_pos_n_val_pos[of v], assumption+)
 apply (rule_tac j = "an N" and k = "n_val K v (f n ± -a f m)" in 
        ale_trans[of 0], simp, assumption+)
 apply simp
done

lemma (in Corps) Cauchy_up:"⟦Corps K'; valuation K v; valuation K' v'; 
      Completionv v' K K'; Cauchy K v f⟧ ⟹ Cauchy K' v' f" 
apply (simp add:Cauchy_seq_def,
       erule conjE,
       rule conjI, unfold v_completion_def, frule conjunct1,
       fold v_completion_def, rule allI, frule subfield_sub[of K'])
apply (simp add:subsetD) 

apply (rule allI)
apply (rotate_tac -1, drule_tac x = "na (Lv K' v') * N" 
      in spec, erule exE) 
apply (subgoal_tac "∀n m. M < n ∧ M < m ⟶
         f n ±K' (-aK' (f m)) ∈ vp K' v'(Vr K' v') (an N)", blast,
       (rule allI)+, rule impI, erule conjE)
apply (rotate_tac -3, drule_tac x = n in spec,
       rotate_tac -1, 
       drule_tac x = m in spec, simp,
       frule_tac x = n in spec,
       drule_tac x = m in spec)
 apply(unfold v_completion_def, frule conjunct1, fold v_completion_def,
       cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
       frule_tac x = "f m" in aGroup.ag_mOp_closed[of "K"], assumption+,
       frule_tac x = "f n" and y = "-a (f m)" in aGroup.ag_pOp_closed[of "K"],
       assumption+)
 apply (simp add:amult_an_an) apply (simp add:Corps.an_na_Lv)
apply (simp add:subfield_mOp, simp add:subfield_pOp) apply (
       frule_tac x = "f n  ±K' -aK' f m" and n = "(Lv K' v') * (an N)"
       in n_value_x_1[of v]) (*apply (
  thin_tac "f n ±' (-a' (f m)) ∈ vp K v(Vr K v) ( (Lv K' v') * (an N))",
   simp add:v_completion_def, (erule conjE)+) *) 
apply (frule Corps.Lv_pos[of "K'" "v'"], assumption+, 
       frule Corps.Lv_z[of "K'" "v'"],
       assumption, erule exE, simp, 
       cut_tac n = N in an_nat_pos,
       frule_tac w1 = z and x1 = 0 and y1 = "an N" in 
             amult_pos_mono_l[THEN sym], simp, simp add:amult_0_r)
apply assumption
apply (frule_tac x = "f n ±K' -aK' f m " in n_val_le_val[of v],
        assumption+)
apply (subst n_val[THEN sym, of "v"], assumption+)
apply (frule Lv_pos[of "v"], frule Lv_z[of v], erule exE, simp)
apply (frule Corps.Lv_pos[of "K'" "v'"], assumption+, 
       frule Corps.Lv_z[of "K'" "v'"],   assumption, erule exE, simp, 
       cut_tac n = N in an_nat_pos,
       frule_tac w1 = za and x1 = 0 and y1 = "an N" in 
             amult_pos_mono_l[THEN sym], simp, simp add:amult_0_r)
apply (frule_tac j = "ant za * an N" and k = "n_val K v (f n ±K' -aK' (f m))"
       in ale_trans[of "0"], assumption+)
apply (frule_tac w1 = z and x1 = 0 and y1 = "n_val K v ( f n ±K' -aK' (f m))"
       in amult_pos_mono_r[THEN sym], simp, simp add:amult_0_l)
apply (frule_tac i = "Lv K' v' * an N" and j ="n_val K v ( f n ±K' -aK' (f m))"
       and k = "v ( f n ±K' -aK' (f m))" in ale_trans, assumption+)
apply (thin_tac "f n ±K' -aK' (f m) ∈ vp K v (Vr K v) (Lv K' v') * (an N)",
       thin_tac "Lv K' v' * an N ≤ n_val K v ( f n ±K' -aK' (f m))",
       thin_tac "n_val K v ( f n ±K' -aK' (f m)) ≤ v ( f n ±K' -aK' (f m))")

apply (simp add:v_completion_def, (erule conjE)+)
 apply (thin_tac "∀x∈carrier K. v x = v' x",
        thin_tac "∀x∈carrier K'. ∃f. Cauchy K v f ∧ lim K' v' f x")
 apply (frule subfield_sub[of K'],
        frule_tac c = "f n ±K' -aK' (f m)" in 
                  subsetD[of "carrier K" "carrier K'"], assumption+)
apply (simp add:Corps.n_val[THEN sym, of "K'" "v'"])
apply (simp add:amult_commute[of _ "Lv K' v'"])
apply (frule Corps.Lv_pos[of "K'" "v'"], assumption, 
       frule Corps.Lv_z[of "K'" "v'"], assumption+, erule exE, simp)
apply (simp add:amult_pos_mono_l)

apply (rule_tac x = "f n ±K' -aK' (f m)" and n = "an N" in 
       Corps.n_value_x_2[of "K'" "v'"], assumption+)
apply (cut_tac n = N in an_nat_pos)
 apply (frule_tac j = "an N" and k = "n_val K' v' (f n ±K' -aK' (f m))" in 
        ale_trans[of "0"], assumption+)
 apply (simp add:Corps.val_pos_n_val_pos[THEN sym, of "K'" "v'"])
 apply (simp add:Corps.val_pos_mem_Vr) apply assumption apply simp
done

lemma max_gtTr:"(n::nat) < max (Suc n) (Suc m) ∧ m < max (Suc n) (Suc m)"
by (simp add:max_def)

lemma (in Corps) completion_approx:"⟦Corps K'; valuation K v; valuation K' v'; 
      Completionv v' K K'; x ∈ carrier (Vr K' v')⟧ ⟹ 
               ∃y∈carrier (Vr K v). (y ±K' -aK' x) ∈ (vp K' v')"
(** show an element y near by x is included in (Vr K v) **) 
apply (frule Corps.Vr_mem_f_mem [of "K'" "v'" "x"], assumption+,
       frule Corps.val_pos_mem_Vr[THEN sym, of "K'" "v'" "x"], assumption+,
       simp add:v_completion_def, (erule conjE)+,
       rotate_tac -1, drule_tac x = x in bspec, assumption+, 
       erule exE, erule conjE)
apply (unfold Cauchy_seq_def, frule conjunct1, fold Cauchy_seq_def)
apply (case_tac "x = 𝟬K'", 
       simp, frule Corps.field_is_ring[of "K'"], 
       frule Ring.ring_is_ag[of "K'"],
       subgoal_tac " 𝟬K' ∈ carrier (Vr K v)",
       subgoal_tac " (𝟬K' ±K' -aK' 𝟬K')∈ vp K' v'", blast,
       frule aGroup.ag_inc_zero[of "K'"], simp add:aGroup.ag_r_inv1,
       simp add:Corps.Vr_0_f_0[THEN sym, of "K'" "v'"],
       frule Corps.Vr_ring[of "K'" "v'"], assumption+,
       frule Corps.vp_ideal[of "K'" "v'"], assumption+,
       simp add:Ring.ideal_zero,
       simp add:subfield_zero[THEN sym, of  "K'"],
       cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
       frule aGroup.ag_inc_zero[of "K"],
       simp add:Vr_0_f_0[THEN sym, of "v"],
       frule Vr_ring[of "v"],simp add:Ring.ring_zero)
      apply (frule_tac f = f in Corps.limit_val[of "K'" "x" _ "v'"], 
                         assumption+)
      apply (rule allI, rotate_tac -2, frule_tac x = j in spec,
             frule subfield_sub[of K'], simp add:subsetD, assumption+)
apply (erule exE)
 apply (simp add:limit_def,
        frule Corps.Vr_ring[of K' v'], assumption+,
        rotate_tac 10,
              drule_tac x = "Suc 0" in spec, erule exE,
       rotate_tac 1,
              frule_tac x = N and y = M in two_inequalities, assumption+,
              thin_tac "∀n>N. v' (f n) = v' x",
              thin_tac "∀n>M. f n ±K' -aK' x ∈ vp K' v' (Vr K' v') (an (Suc 0))")
       apply (frule Corps.vp_ideal[of K' v'], assumption+,
              simp add:Ring.r_apow_Suc[of "Vr K' v'" "vp K' v'"])
       apply (drule_tac x = "N + M + 1" in spec, simp,
              drule_tac x = "N + M + 1" in spec, simp,
              erule conjE)
 apply (drule_tac x = "f (Suc (N + M))" in bspec, assumption+)
 apply simp 
 apply (cut_tac x = "f (Suc (N + M))" in val_pos_mem_Vr[of v], assumption+)
 apply simp apply blast
done

lemma (in Corps) res_v_completion_surj:"⟦ Corps K'; valuation K v; 
      valuation K' v'; Completionv v' K K'⟧ ⟹ 
      surjec(Vr K v),(qring (Vr K' v') (vp K' v')) 
            (compos (Vr K v) (pj (Vr K' v') (vp K' v')) (I(Vr K v)))"
apply (frule Vr_ring[of "v"], 
       frule Ring.ring_is_ag[of "Vr K v"],
       frule Corps.Vr_ring[of "K'" "v'"], assumption+,
       frule Ring.ring_is_ag[of "Vr K' v'"],
       frule Ring.ring_is_ag[of "Vr K v"])
apply (frule Corps.vp_ideal[of "K'" "v'"], assumption+, 
       frule Ring.qring_ring[of "Vr K' v'" "vp K' v'"], assumption+)
apply (simp add:surjec_def)
apply (frule aHom_compos[of "Vr K v" "Vr K' v'" 
      "qring (Vr K' v') (vp K' v')" "I(Vr K v)" 
      "pj (Vr K' v') (vp K' v')"], assumption+, simp add:Ring.ring_is_ag)
apply (rule Vr_idmap_aHom, assumption+) apply (simp add:completion_subfield,
      simp add:v_completion_def) apply (
      frule pj_Hom[of "Vr K' v'" "vp K' v'"], assumption+) apply ( 
      simp add:rHom_def, simp)
apply (rule surj_to_test)
 apply (simp add:aHom_def)
apply (rule ballI) 
 apply (thin_tac "Ring (Vr K' v' /r vp K' v')",
  thin_tac "compos (Vr K v) (pj (Vr K' v') (vp K' v')) (I(Vr K v)) ∈ 
               aHom (Vr K v) (Vr K' v' /r vp K' v')")
 apply (simp add:Ring.qring_carrier)
 apply (erule bexE)
 apply (frule_tac x = a in completion_approx[of "K'" "v" "v'"], 
       assumption+, erule bexE)
 apply (subgoal_tac "compos (Vr K v) (pj (Vr K' v') 
                     (vp K' v')) ((I(Vr K v))) y = b", blast)
 apply (simp add:compos_def compose_def idmap_def)
 apply (frule completion_Vring_sub[of "K'" "v" "v'"], assumption+)
 apply (frule_tac c = y in subsetD[of "carrier (Vr K v)" "carrier (Vr K' v')"],
         assumption+)
 apply (frule_tac x = y in pj_mem[of "Vr K' v'" "vp K' v'"], assumption+, simp,
        thin_tac "pj (Vr K' v') (vp K' v') y = y ⊎(Vr K' v') (vp K' v')")
 apply (rotate_tac -5, frule sym, thin_tac "a ⊎(Vr K' v') (vp K' v') = b", 
       simp)
 apply (rule_tac b1 = y and a1 = a in Ring.ar_coset_same1[THEN sym, 
        of "Vr K' v'" "vp K' v'"], assumption+)
 apply (frule Ring.ring_is_ag[of "Vr K' v'"], 
        frule_tac x = a in aGroup.ag_mOp_closed[of "Vr K' v'"],
        assumption+)
 apply (simp add:Corps.Vr_mOp_f_mOp, simp add:Corps.Vr_pOp_f_pOp)
done

lemma (in Corps) res_v_completion_ker:"⟦Corps K'; valuation K v; 
      valuation K' v'; Completionv v' K K'⟧ ⟹ 
  ker(Vr K v), (qring (Vr K' v') (vp K' v')) 
  (compos (Vr K v) (pj (Vr K' v') (vp K' v')) (I(Vr K v))) = vp K v"
apply (rule equalityI)
 apply (rule subsetI)
 apply (simp add:ker_def, (erule conjE)+)
 apply (frule Corps.Vr_ring[of "K'" "v'"], assumption+,
        frule Corps.vp_ideal[of "K'" "v'"], assumption+,
        frule Ring.qring_ring[of "Vr K' v'" "vp K' v'"], assumption+,
        simp add:Ring.qring_zero)
 apply (simp add:compos_def, simp add:compose_def, simp add:idmap_def)
 apply (frule completion_Vring_sub[of "K'" "v" "v'"], assumption+)
 apply (frule_tac c = x in subsetD[of "carrier (Vr K v)" "carrier (Vr K' v')"],
        assumption+)
 apply (simp add:pj_mem)
 apply (frule_tac a = x in Ring.qring_zero_1[of "Vr K' v'" _  "vp K' v'"], 
        assumption+)
 apply (subst vp_mem_val_poss[of v], assumption+) 
 apply (simp add:Vr_mem_f_mem)
 apply (frule_tac x = x in Corps.vp_mem_val_poss[of "K'" "v'"],
        assumption+, simp add:Corps.Vr_mem_f_mem, simp)
apply (frule_tac x = x in Vr_mem_f_mem[of v], assumption+)
 apply (frule_tac x = x in completion_val_eq[of "K'" "v" "v'"],
         assumption+, simp)
apply (rule subsetI)
 apply (simp add:ker_def)
 apply (frule Vr_ring[of  "v"])
 apply (frule vp_ideal[of "v"])
 apply (frule_tac h = x in Ring.ideal_subset[of "Vr K v" "vp K v"],
         assumption+, simp)
 apply (frule Corps.Vr_ring[of "K'" "v'"], assumption+,
        frule Corps.vp_ideal[of "K'" "v'"], assumption+, 
        simp add:Ring.qring_zero)
 apply (simp add:compos_def compose_def idmap_def)
 apply (frule completion_Vring_sub[of "K'" "v" "v'"],
        assumption+, frule_tac c = x in subsetD[of "carrier (Vr K v)"
        "carrier (Vr K' v')"], assumption+)
 apply (simp add:pj_mem)
 apply (frule completion_vpr_sub[of "K'" "v" "v'"], assumption+,
        frule_tac c = x in subsetD[of "vp K v" "vp K' v'"], assumption+)
 apply (simp add:Ring.ar_coset_same4[of "Vr K' v'" "vp K' v'"])
done 

lemma (in Corps) completion_res_qring_isom:"⟦Corps K'; valuation K v; 
  valuation K' v'; Completionv v' K K'⟧  ⟹ 
   r_isom ((Vr K v) /r (vp K v)) ((Vr K' v') /r (vp K' v'))"
apply (subst r_isom_def)
apply (frule res_v_completion_surj[of "K'" "v" "v'"], assumption+)
apply (frule Vr_ring[of "v"],
       frule Corps.Vr_ring[of "K'" "v'"], assumption+,
       frule Corps.vp_ideal[of "K'" "v'"], assumption+,
       frule Ring.qring_ring[of "Vr K' v'" "vp K' v'"], assumption+)
apply (frule rHom_compos[of "Vr K v" "Vr K' v'" "(Vr K' v' /r vp K' v')" 
       "(I(Vr K v))" "pj (Vr K' v') (vp K' v')"], assumption+)
apply (simp add:completion_idmap_rHom)
apply (simp add:pj_Hom) 
apply (frule surjec_ind_bijec [of "Vr K v" "(Vr K' v' /r vp K' v')" 
      "compos (Vr K v) (pj (Vr K' v') (vp K' v')) (I(Vr K v))"], assumption+)
apply (frule ind_hom_rhom[of "Vr K v" "(Vr K' v' /r vp K' v')" 
       "compos (Vr K v) (pj (Vr K' v') (vp K' v')) (I(Vr K v))"], assumption+)
apply (simp add:res_v_completion_ker) apply blast
done

text‹expansion of x in a complete field K, with normal valuation v. Here
we suppose t is an element of K satisfying the equation ‹v t = 1›.›

definition
  Kxa :: "[_, 'b ⇒ ant, 'b] ⇒ 'b set" where
  "Kxa K v x = {y. ∃k∈carrier (Vr K v). y = x ⋅rK k}"
    (**  x *r carrier (Vr K v) **)

primrec 
  partial_sum :: "[('b, 'm) Ring_scheme, 'b, 'b ⇒ ant, 'b] 
                                   ⇒ nat ⇒ 'b"
        ("(5psum _ _ _ _ _)" [96,96,96,96,97]96)
where
  psum_0: "psum K x v t 0 = (csrp_fn (Vr K v) (vp K v) 
     (pj (Vr K v) (vp K v) (x ⋅rK tK-(tna (v x))))) ⋅rK (tK(tna (v x)))"
| psum_Suc: "psum K x v t (Suc n) = (psum K x v t n) ±K 
  ((csrp_fn (Vr K v) (vp K v) (pj (Vr K v) (vp K v)  
   ((x ±K -aK (psum K x v t n)) ⋅rK (tK- (tna (v x) + int (Suc n)))))) ⋅rK 
         (tK(tna (v x) + int (Suc n))))" 

definition
  expand_coeff :: "[_ , 'b ⇒ ant, 'b, 'b] 
                      ⇒ nat ⇒ 'b"
                   ("(5ecf_ _ _ _ _)" [96,96,96,96,97]96) where
  "ecfK v t x n = (if n = 0 then  csrp_fn (Vr K v) (vp K v) 
     (pj (Vr K v) (vp K v) (x ⋅rK tK(-(tna (v x)))))
     else csrp_fn (Vr K v) (vp K v) (pj (Vr K v) 
  (vp K v) ((x ±K -aK (psum K x v t (n - 1))) ⋅rK (tK(- (tna (v x) + int n))))))" 

definition
  expand_term :: "[_, 'b ⇒ ant, 'b, 'b] 
                      ⇒ nat ⇒ 'b"
                   ("(5etm _ _ _ _ _)" [96,96,96,96,97]96) where
        
  "etmK v t x n = (ecfK v t x n)⋅rK (tK(tna (v x) + int n))"



(*** Let O be the valuation ring with respect to the valuation v and let P
be the maximal ideal of O. Let j be the value of x (∈ O), and  a0 be an 
element of the complete set of representatives such that a0 = x t-j mod P.
 We see that (a0 - x t-j)/t is an element of O, and then we choose a1 an 
element of the complete set of representatives which is equal to (a0 - x t-j)/tmodulo P. We see x - (a0tj + a1t(j+1) + … + ast(j+s)) ∈ (t(j+s+1)). 
"psum G a i K v t x s" is the partial sum a0tj + a1t(j+1) + … + ast(j+s) ***)  

lemma (in Corps) Kxa_val_ge:"⟦valuation K v; t ∈ carrier K; v t = 1⟧ 
 ⟹  Kxa K v (tKj) = {x. x ∈ carrier K ∧ (ant j) ≤ (v x)}"
apply (frule val1_neq_0[of v t], assumption+)
apply (cut_tac field_is_ring) 
apply (rule equalityI)
 apply (rule subsetI,
        simp add:Kxa_def, erule bexE,
        frule_tac x = k in Vr_mem_f_mem[of "v"], assumption+,
        frule npowf_mem[of "t" "j"], simp, 
        simp add:Ring.ring_tOp_closed)
 apply (simp add:val_t2p) apply (simp add:val_exp[THEN sym]) 
 apply (simp add:val_pos_mem_Vr[THEN sym, of "v"])
 apply (frule_tac x = 0 and y = "v k" in aadd_le_mono[of _ _ "ant j"])
 apply (simp add:aadd_0_l aadd_commute)
apply (rule subsetI, simp, erule conjE)
 apply (simp add:Kxa_def)
 apply (case_tac "x = 𝟬K")
 apply (frule Vr_ring[of "v"], 
        frule Ring.ring_zero[of "Vr K v"],
        simp add:Vr_0_f_0,
        frule_tac x1 = "tKj" in Ring.ring_times_x_0[THEN sym, of "K"],
        simp add:npowf_mem, blast)
 apply (frule val_exp[of "v" "t" "j"], assumption+, simp) 
 apply (frule field_potent_nonzero1[of "t" "j"], 
        frule npowf_mem[of "t" "j"], assumption+)
 apply (frule_tac y = "v x" in ale_diff_pos[of "v (tKj)"], 
        simp add:diff_ant_def)
apply (cut_tac npowf_mem[of t j]) 
 defer 
 apply assumption apply simp
apply (frule value_of_inv[THEN sym, of "v" "tKj"], assumption+) 
 
 apply (cut_tac invf_closed1[of "tKj"], simp, erule conjE)
 apply (frule_tac x1 = x in val_t2p[THEN sym, of "v" _ "(tKj)‐K"], 
        assumption+, simp)
 apply (frule_tac x = "(tKj)‐K" and y = x in Ring.ring_tOp_closed[of "K"], 
          assumption+)
 apply (simp add:Ring.ring_tOp_commute[of "K" _ "(tKj)‐K"])
 apply (frule_tac x = "((tKj)‐K) ⋅r x" in val_pos_mem_Vr[of v], assumption+, 
        simp)
 apply (frule_tac z = x in Ring.ring_tOp_assoc[of "K" "tKj" "(tKj)‐K"], 
         assumption+) 
 apply (simp add:Ring.ring_tOp_commute[of K "tKj" "(tKj)‐ K"] linvf,
        simp add:Ring.ring_l_one, blast) 
 apply simp
done

lemma (in Corps) Kxa_pow_vpr:"⟦ valuation K v; t ∈ carrier K; v t = 1;
    (0::int) ≤ j⟧ ⟹ Kxa K v (tKj) = (vp K v)(Vr K v) (ant j)"
apply (frule val_surj_n_val[of v], blast) 
apply (simp add:Kxa_val_ge) 
apply (rule equalityI)
 apply (rule subsetI, simp, erule conjE)
 apply (rule_tac x = x in n_value_x_2[of "v" _ "(ant j)"],
            assumption+)
 apply (cut_tac ale_zle[THEN sym, of "0" "j"]) 
 apply (frule_tac a = "0 ≤ j" and b = "ant 0 ≤ ant j" in a_b_exchange,
         assumption+) 
 apply (thin_tac "(0 ≤ j) = (ant 0 ≤ ant j)", simp add:ant_0)
 apply (frule_tac k = "v x" in ale_trans[of "0" "ant j"], assumption+)
 apply (simp add:val_pos_mem_Vr) apply simp
 apply (simp only:ale_zle[THEN sym, of "0" "j"], simp add:ant_0)
apply (rule subsetI)
 apply simp 
 apply (frule_tac x = x in mem_vp_apow_mem_Vr[of "v" "ant j"]) 
 apply (simp only:ale_zle[THEN sym, of "0" "j"], simp add:ant_0) 
 apply assumption
apply (simp add:Vr_mem_f_mem[of "v"])
apply (frule_tac x = x in n_value_x_1[of "v" "ant j" _ ])
 apply (simp only:ale_zle[THEN sym, of "0" "j"], simp add:ant_0) 
 apply assumption apply simp
done  

lemma (in Corps) field_distribTr:"⟦a ∈ carrier K; b ∈ carrier K; 
      x ∈ carrier K; x ≠ 𝟬⟧ ⟹ a ± (-a (b ⋅r x)) = (a ⋅r (x‐K) ± (-a b)) ⋅r x"
apply (cut_tac field_is_ring,
       cut_tac invf_closed1[of x], simp, erule conjE) apply (
       simp add:Ring.ring_inv1_1[of "K" "b" "x"],
       frule Ring.ring_is_ag[of "K"],
       frule aGroup.ag_mOp_closed[of "K" "b"], assumption+)
apply (frule Ring.ring_tOp_closed[of "K" "a" "x‐K"], assumption+,
       simp add:Ring.ring_distrib2, simp add:Ring.ring_tOp_assoc, 
       simp add:linvf,
       simp add:Ring.ring_r_one)
apply simp
done

lemma a0_le_1[simp]:"(0::ant) ≤ 1"
by (cut_tac a0_less_1, simp add:aless_imp_le)

lemma (in Corps) vp_mem_times_t:"⟦valuation K v; t ∈ carrier K; t ≠ 𝟬; 
       v t = 1; x ∈ vp K v⟧ ⟹ ∃a∈carrier (Vr K v). x = a ⋅r t" 
apply (frule Vr_ring[of v],
       frule vp_ideal[of v]) 
 apply (frule val_surj_n_val[of v], blast)
 apply (frule vp_mem_val_poss[of v x],
        frule_tac h = x in Ring.ideal_subset[of "Vr K v" "vp K v"], 
        assumption+, simp add:Vr_mem_f_mem, simp) 
 apply (frule gt_a0_ge_1[of "v x"])
 apply (subgoal_tac "v t ≤ v x") 
 apply (thin_tac "1 ≤ v x")
 apply (frule val_Rxa_gt_a_1[of "v" "t" "x"])
 apply (subst val_pos_mem_Vr[THEN sym, of "v" "t"], assumption+)
 apply simp 
 apply (simp add:vp_mem_Vr_mem) apply assumption+
 apply (simp add:Rxa_def, erule bexE) 
 apply (cut_tac a0_less_1) 
 apply (subgoal_tac "0 ≤ v t")
 apply (frule val_pos_mem_Vr[of "v" "t"], assumption+)
 apply (simp, simp add:Vr_tOp_f_tOp, blast, simp+)
done

lemma (in Corps) psum_diff_mem_Kxa:"⟦valuation K v; t ∈ carrier K; 
      v t = 1; x ∈ carrier K; x ≠ 𝟬⟧ ⟹ 
     (psum K x v t n) ∈ carrier K ∧ 
     ( x ± (-a (psum K x v t n))) ∈ Kxa K v (tK((tna (v x)) + (1 + int n)))"
apply (frule val1_neq_0[of v t], assumption+)
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
       frule Vr_ring[of v], frule vp_ideal[of v])
apply (induct_tac n)
apply (subgoal_tac "x ⋅r (tK- tna (v x)) ∈ carrier (Vr K v)",
       rule conjI, simp, rule Ring.ring_tOp_closed[of "K"], assumption+,
       frule Ring.csrp_fn_mem[of "Vr K v" "vp K v" 
       "pj (Vr K v) (vp K v) (x ⋅r (tK- tna (v x)))"], 
       assumption+,
       simp add:pj_mem Ring.qring_carrier, blast,
       simp add:Vr_mem_f_mem, simp add:npowf_mem)
apply (simp, 
     frule npowf_mem[of "t" "tna (v x)"], assumption+,
     frule field_potent_nonzero1[of "t" "tna (v x)"], assumption+,
     subst field_distribTr[of "x" _ "tK(tna (v x))"], assumption+,
     frule Ring.csrp_fn_mem[of "Vr K v" "vp K v" 
     "pj (Vr K v) (vp K v) (x ⋅r (tK- tna (v x)))"], 
     assumption+,
     simp add:pj_mem Ring.qring_carrier, blast, simp add:Vr_mem_f_mem,
     simp add:npowf_mem, assumption) 
apply (frule Ring.csrp_diff_in_vpr[of "Vr K v" "vp K v" 
       "x ⋅r ((tK(tna (v x)))‐K)"], assumption+) 
      apply (simp add:npowf_minus)
 
 apply (simp add:npowf_minus)
 apply (frule pj_Hom[of "Vr K v" "vp K v"], assumption+)
 apply (frule rHom_mem[of "pj (Vr K v) (vp K v)" "Vr K v" "Vr K v /r vp K v" 
        "x ⋅r (tK- tna (v x))"], assumption+)
 apply (frule Ring.csrp_fn_mem[of "Vr K v" "vp K v" 
         "pj (Vr K v) (vp K v) (x ⋅r (tK- tna (v x)))"], assumption+)
 apply (frule Ring.ring_is_ag[of "Vr K v"], 
        frule_tac x = "csrp_fn (Vr K v) (vp K v) (pj (Vr K v) (vp K v) 
       (x ⋅r (tK- tna (v x))))" in aGroup.ag_mOp_closed[of "Vr K v"], assumption+)
 apply (simp add:Vr_pOp_f_pOp) apply (simp add:Vr_mOp_f_mOp)
apply (frule_tac x = "x ⋅r (tK- tna (v x)) ± -a (csrp_fn (Vr K v) (vp K v)
      (pj (Vr K v) (vp K v) (x ⋅r (tK- tna (v x)))))" in 
      vp_mem_times_t[of "v" "t"], assumption+, erule bexE, simp)
apply (frule_tac x = a in Vr_mem_f_mem[of  "v"], assumption+)
apply (simp add:Ring.ring_tOp_assoc[of "K"])
 apply (simp add:npowf_exp_1_add[THEN sym, of "t" "tna (v x)"]) 
 apply (simp add:add.commute)
apply (simp add:Kxa_def) 
apply (frule npowf_mem[of "t" "1 + tna (v x)"], assumption+)
apply (simp add:Ring.ring_tOp_commute[of "K" _ "tK(1 + tna (v x))"])
 apply blast
 apply (frule npowf_mem[of  "t" "- tna (v x)"], assumption+)
 apply (frule Ring.ring_tOp_closed[of "K" "x" "tK- tna (v x)"], assumption+)
apply (subst val_pos_mem_Vr[THEN sym, of v], assumption+)
 apply (simp add:val_t2p) apply (simp add:val_exp[THEN sym, of "v" "t"])
 apply (simp add:aminus[THEN sym])
 apply (frule value_in_aug_inf[of "v" "x"], assumption+, 
        simp add:aug_inf_def)
 apply (frule val_nonzero_noninf[of "v" "x"], assumption+,
         simp add:ant_tna)
 apply (simp add:aadd_minus_r)

apply (erule conjE)
 apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
 apply (rule conjI)
 apply simp
 apply (rule aGroup.ag_pOp_closed, assumption+)
 apply (rule Ring.ring_tOp_closed[of "K"], assumption+)
 apply (simp add:Kxa_def, erule bexE, simp)
 apply (subst Ring.ring_tOp_commute, assumption+)
 apply (rule npowf_mem, assumption+) apply (simp add:Vr_mem_f_mem)
 apply (frule_tac n = "tna (v x) + (1 + int n)" in npowf_mem[of t ], 
        assumption,
        frule_tac n = "- tna (v x) + (-1 - int n)" in npowf_mem[of t ], 
        assumption,
        frule_tac x = k in Vr_mem_f_mem[of v], assumption+)
 apply (simp add:Ring.ring_tOp_assoc npowf_exp_add[THEN sym, of t])
  apply (simp add:field_npowf_exp_zero) 
  apply (simp add:Ring.ring_r_one)

 apply (frule pj_Hom[of "Vr K v" "vp K v"], assumption+)
 apply (frule_tac a = k in rHom_mem[of "pj (Vr K v) (vp K v)" "Vr K v" 
        "Vr K v /r vp K v"], assumption+)
 apply (frule_tac x = "pj (Vr K v) (vp K v) k" in Ring.csrp_fn_mem[of "Vr K v" 
        "vp K v"], assumption+)
 apply (simp add:Vr_mem_f_mem)
 apply (rule npowf_mem, assumption+)

apply (simp add:Kxa_def) apply (erule bexE, simp)
apply (frule_tac x = k in Vr_mem_f_mem[of "v"], assumption+)
apply (frule_tac n = "tna (v x) + (1 + int n)" in npowf_mem[of "t"], 
       assumption+)
apply (frule_tac n = "- tna (v x) + (- 1 - int n)" in npowf_mem[of "t"], 
       assumption+)
apply (frule_tac x = "tK(tna (v x) + (1 + int n))" and y = k in 
      Ring.ring_tOp_commute[of "K"], assumption+) apply simp
apply (simp add:Ring.ring_tOp_assoc, simp add:npowf_exp_add[THEN sym])
   apply (simp add:field_npowf_exp_zero) 
   apply (simp add:Ring.ring_r_one)
   apply (thin_tac "(tK(tna (v x) + (1 + int n))) ⋅r k =
            k ⋅r (tK(tna (v x) + (1 + int n)))")
apply (frule pj_Hom[of "Vr K v" "vp K v"], assumption+)
apply (frule_tac a = k in rHom_mem[of "pj (Vr K v) (vp K v)" "Vr K v" 
        "Vr K v /r vp K v"], assumption+)
 apply (frule_tac x = "pj (Vr K v) (vp K v) k" in Ring.csrp_fn_mem[of "Vr K v" 
        "vp K v"], assumption+)
 apply (frule_tac x = "csrp_fn (Vr K v) (vp K v) (pj (Vr K v) (vp K v) k)" in 
        Vr_mem_f_mem[of v], assumption+)
 apply (frule_tac x = "csrp_fn (Vr K v) (vp K v) (pj (Vr K v) (vp K v) k)" and
 y = "tK(tna (v x) + (1 + int n))" in Ring.ring_tOp_closed[of "K"], assumption+)
 apply (simp add:aGroup.ag_p_inv[of "K"])
 apply (frule_tac x = "psum K x v t n" in aGroup.ag_mOp_closed[of "K"], 
          assumption+)
 apply (frule_tac x = "(csrp_fn (Vr K v) (vp K v)(pj (Vr K v) (vp K v) k)) ⋅r
       (tK(tna (v x) + (1 + int n)))" in aGroup.ag_mOp_closed[of "K"], assumption+)
 apply (subst aGroup.ag_pOp_assoc[THEN sym], assumption+)
 apply simp
 apply (simp add:Ring.ring_inv1_1)
 apply (subst Ring.ring_distrib2[THEN sym, of "K"], assumption+)
 apply (rule aGroup.ag_mOp_closed, assumption+)
 apply (frule_tac x = k in  Ring.csrp_diff_in_vpr[of "Vr K v" "vp K v"]
     , assumption+)
 apply (frule Ring.ring_is_ag[of "Vr K v"])
 apply (frule_tac x = "csrp_fn (Vr K v) (vp K v) (pj (Vr K v) (vp K v) k)" in 
        aGroup.ag_mOp_closed[of "Vr K v"], assumption+)
 apply (simp add:Vr_pOp_f_pOp) apply (simp add:Vr_mOp_f_mOp)
 apply (frule_tac x = "k ± -a (csrp_fn (Vr K v) (vp K v) (pj (Vr K v) (vp K v)
 k))" in vp_mem_times_t[of "v" "t"], assumption+, erule bexE, simp)
 apply (frule_tac x = a in Vr_mem_f_mem[of v], assumption+)
 apply (simp add:Ring.ring_tOp_assoc[of "K"])
 apply (simp add:npowf_exp_1_add[THEN sym, of "t"])
 apply (simp add:add.commute[of "2"])
 apply (simp add:add.assoc)
 apply (subst Ring.ring_tOp_commute, assumption+)
 apply (rule npowf_mem, assumption+) apply blast
done

lemma Suc_diff_int:"0 < n ⟹ int (n - Suc 0) = int n - 1" 
by (cut_tac of_nat_Suc[of "n - Suc 0"], simp)

lemma (in Corps) ecf_mem:"⟦valuation K v; t ∈ carrier K; v t = 1; 
      x ∈ carrier K; x ≠ 𝟬 ⟧ ⟹  ecfK v t x n ∈ carrier K"
apply (frule val1_neq_0[of v t], assumption+)
apply (cut_tac field_is_ring,
       frule Vr_ring[of v], frule vp_ideal[of v])
apply (case_tac "n = 0")
 apply (simp add:expand_coeff_def)
 apply (rule Vr_mem_f_mem[of v], assumption+)
 apply (rule Ring.csrp_fn_mem, assumption+)
 apply (subgoal_tac "x ⋅r (tK- tna (v x)) ∈ carrier (Vr K v)")
 apply (simp add:pj_mem Ring.qring_carrier, blast)
apply (frule npowf_mem[of  "t" "- tna (v x)"], assumption+,
       subst val_pos_mem_Vr[THEN sym, of v "x ⋅r (tK(- tna(v x)))"], 
       assumption+,
       rule Ring.ring_tOp_closed, assumption+) 
apply (simp add:val_t2p,
       simp add:val_exp[THEN sym, of  "v" "t" "- tna (v x)"]) 
apply (frule value_in_aug_inf[of  "v" "x"], assumption+,
       simp add:aug_inf_def)
      apply (frule val_nonzero_noninf[of  "v" "x"], assumption+)
  apply (simp add:aminus[THEN sym], simp add:ant_tna)
  apply (simp add:aadd_minus_r)

apply (simp add:expand_coeff_def) 
apply (frule psum_diff_mem_Kxa[of  "v" "t" "x" "n - 1"],
                   assumption+, erule conjE)
apply (simp add:Kxa_def, erule bexE,
       frule_tac x = k in Vr_mem_f_mem[of v], assumption+,
     frule npowf_mem[of  "t" "tna (v x) + (1 + int (n - Suc 0))"], 
     assumption+,
   frule npowf_mem[of  "t" "-tna (v x) - int n"], assumption+)
  apply simp
  apply (thin_tac "x ± -a psum K x v t (n - Suc 0) =
          (tK(tna (v x) + (1 + int (n - Suc 0)))) ⋅r k")
apply(simp add:Ring.ring_tOp_commute[of "K" "tK(tna (v x) + (1 + int (n - Suc 0)))"])
 apply (simp add:Ring.ring_tOp_assoc, simp add:npowf_exp_add[THEN sym])
 apply (thin_tac "tK(tna (v x) + (1 + int (n - Suc 0))) ∈ carrier K",
        thin_tac "tK(- tna (v x) - int n) ∈ carrier K")
 apply (simp add:Suc_diff_int[of "n"])
 apply (simp add:npowf_def, simp add:Ring.ring_r_one)
apply (rule Vr_mem_f_mem, assumption+)
 apply (rule Ring.csrp_fn_mem, assumption+)
 apply (simp add:pj_mem Ring.qring_carrier, blast)
done

lemma (in Corps) etm_mem:"⟦valuation K v; t ∈ carrier K; v t = 1; 
     x ∈ carrier K; x ≠ 𝟬⟧ ⟹ etmK v t x n ∈ carrier K"
apply (frule val1_neq_0[of v t], assumption+)
apply (simp add:expand_term_def)
apply (cut_tac field_is_ring,
       rule Ring.ring_tOp_closed[of "K"], assumption)
apply (simp add:ecf_mem)
apply (simp add:npowf_mem)
done

lemma (in Corps) psum_sum_etm:"⟦valuation K v; t ∈ carrier K; v t = 1; 
      x ∈ carrier K; x ≠ 𝟬⟧ ⟹ 
 psumK x v t n = nsum K (λj. (ecfK v t x j)⋅r (tK(tna (v x) + (int j)))) n" 
apply (frule val1_neq_0[of v t], assumption+)
apply (induct_tac "n")
 apply (simp add:expand_coeff_def)
apply (rotate_tac -1, drule sym)
apply simp
 apply (thin_tac e K (λj. ecfK v t x j ⋅r tK(tna (v x) + int j)) n =
         psum K x v t n")
 apply (simp add:expand_coeff_def)
done

lemma zabs_pos:"0 ≤ (abs (z::int))"
by (simp add:zabs_def)

lemma abs_p_self_pos:"0 ≤ z + (abs (z::int))"
by (simp add:zabs_def)

lemma zadd_right_mono:"(i::int) ≤ j ⟹ i  + k ≤ j  + k"
by simp

theorem (in Corps) expansion_thm:"⟦valuation K v; t ∈ carrier K; 
       v t = 1; x ∈ carrier K; x ≠ 𝟬⟧  ⟹ limK v (partial_sum K x v t) x" 
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
apply (simp add:limit_def)
 apply (rule allI)
 apply (subgoal_tac "∀n. (N + na (Abs (v x))) < n ⟶
                     psumK x v t n ± -a x ∈ vp K v(Vr K v) (an N)")
 apply blast
apply (rule allI, rule impI)
apply (frule_tac n = n in psum_diff_mem_Kxa[of "v" "t" "x"],
          assumption+, erule conjE) 
apply (frule_tac j = "tna (v x) + (1 + int n)" in  Kxa_val_ge[of "v" "t"], 
       assumption+)
 apply simp
 apply (thin_tac "Kxa K v (tK(tna (v x) + (1 + int n))) =
           {xa ∈ carrier K. ant (tna (v x) + (1 + int n)) ≤ v xa}")
 apply (erule conjE)
 apply (simp add:a_zpz[THEN sym])

apply (subgoal_tac "(an N) ≤ v (psum K x v t n ± -a x)")
 
 apply (frule value_in_aug_inf[of v x], assumption+,
       simp add:aug_inf_def)
      apply (frule val_nonzero_noninf[of v x], assumption+)
  apply (simp add:ant_tna)
 apply (frule val_surj_n_val[of v], blast)
apply (rule_tac x = "psumK x v t n ± -a x" and n = "an N" in 
                     n_value_x_2[of  "v"], assumption+) 
apply (subst val_pos_mem_Vr[THEN sym, of v], assumption+)
apply (rule aGroup.ag_pOp_closed[of "K"], assumption+)
apply (simp add:aGroup.ag_mOp_closed)

apply (cut_tac n = N in an_nat_pos)
apply (rule_tac i = 0 and j = "an N" and k = "v (psum K x v t n ± -a x)" in 
       ale_trans, assumption+)
apply simp
apply simp

apply (frule_tac x1 = "x ± (-a psumK x v t n)" in val_minus_eq[THEN sym,
      of v], assumption+, simp,
      thin_tac "v ( x ± -a psum K x v t n) = v (-a ( x ± -a psum K x v t n))")
 apply (frule_tac x = "psum K x v t n" in aGroup.ag_mOp_closed[of "K"],
        assumption+, simp add:aGroup.ag_p_inv, simp add:aGroup.ag_inv_inv)
 apply (frule aGroup.ag_mOp_closed[of "K" "x"], assumption+)
 apply (simp add:aGroup.ag_pOp_commute[of "K" "-a x"])

apply (cut_tac Abs_pos[of "v x"])
apply (frule val_nonzero_z[of v x], assumption+, erule exE, simp) 
apply (simp add:na_def) 
apply (cut_tac aneg_less[THEN sym, of "0" "Abs (v x)"], simp)
apply (frule val_nonzero_noninf[of v x], assumption+)
apply (simp add:tna_ant)
apply (simp only:ant_1[THEN sym], simp del:ant_1 add:a_zpz)
apply (simp add:add.assoc[THEN sym])
apply (cut_tac m1 = "N + nat ¦z¦" and n1 = n in of_nat_less_iff [where ?'a = int, THEN sym], simp)
apply (frule_tac a = "int N + abs z" and b = "int n" and c = "z + 1" in 
       add_strict_right_mono, simp only:add.commute)
apply (simp only:add.assoc[of _ "1"])
apply (simp only:add.assoc[THEN sym, of "1"])
apply (simp only:add.commute[of "1"])
apply (simp only:add.assoc[of _ "1"])
apply (cut_tac ?a1 = z and ?b1 = "abs z" and ?c1 = "1 + int N" in 
       add.assoc[THEN sym])
apply (thin_tac "¦z¦ + int N < int n")
apply (frule_tac a = "z + (¦z¦ + (1 + int N))" and b = "z + ¦z¦ + (1 + int N)" and c = "int n + (z + 1)" in ineq_conv1, assumption+)
apply (thin_tac "z + (¦z¦ + (1 + int N)) < int n + (z + 1)",
       thin_tac "z + (¦z¦ + (1 + int N)) = z + ¦z¦ + (1 + int N)",
       thin_tac "N + nat ¦z¦ < n")
apply (cut_tac z = z in abs_p_self_pos)
apply (frule_tac i = 0 and j = "z + abs z" and k = "1 + int N" in 
        zadd_right_mono) 
apply (simp only:add_0)
apply (frule_tac i = "1 + int N" and j = "z + ¦z¦ + (1 + int N)" and 
       k = "int n + (z + 1)" in zle_zless_trans, assumption+) 
apply (thin_tac "z + ¦z¦ + (1 + int N) < int n + (z + 1)",
       thin_tac "0 ≤ z + ¦z¦",
       thin_tac "1 + int N ≤ z + ¦z¦ + (1 + int N)")
apply (cut_tac m1 = "1 + int N" and n1 = "int n + (z + 1)" in 
       aless_zless[THEN sym], simp)

apply (frule_tac x = "ant (1 + int N)" and y = "ant (int n + (z + 1))"
       and z = "v ( psum K x v t n ± -a x)" in aless_le_trans, assumption+)
apply (thin_tac "ant (1 + int N) < ant (int n + (z + 1))")

apply (simp add:a_zpz[THEN sym])
apply (frule_tac x = "1 + ant (int N)" and y = "v ( psum K x v t n ± -a x)" in 
       aless_imp_le, thin_tac "1 + ant (int N) < v ( psum K x v t n ± -a x)")
apply (cut_tac a0_less_1, frule aless_imp_le[of "0" "1"])
apply (frule_tac b = "ant (int N)" in aadd_pos_le[of "1"])
apply (subst an_def)
apply (rule_tac i = "ant (int N)" and j = "1 + ant (int N)" and 
       k = "v ( psum K x v t n ± -a x)" in ale_trans, assumption+)
done

subsection "Hensel's theorem"

definition
(*** Cauchy sequence of polynomials in (Vr K v)[X] ***)
  pol_Cauchy_seq :: "[('b, 'm) Ring_scheme, 'b, _, 'b ⇒ ant, 
         nat ⇒ 'b] ⇒ bool" ("(5PCauchy _ _ _ _ _)" [90,90,90,90,91]90) where
  "PCauchyR X K v F ⟷ (∀n. (F n) ∈ carrier R) ∧ 
    (∃d. (∀n. deg R (Vr K v) X (F n) ≤ (an d))) ∧
    (∀N. ∃M. (∀n m. M < n ∧ M < m ⟶  
        P_mod R (Vr K v) X ((vp K v)(Vr K v) (an N)) (F n ±R -aR (F m))))"

definition
  pol_limit :: "[('b, 'm) Ring_scheme, 'b, _, 'b ⇒ ant, 
             nat ⇒ 'b, 'b] ⇒ bool" 
             ("(6Plimit _ _ _ _ _ _)" [90,90,90,90,90,91]90) where
  "PlimitR X K v F p ⟷ (∀n. (F n) ∈ carrier R) ∧ 
    (∀N. ∃M. (∀m. M < m ⟶  
        P_mod R (Vr K v) X ((vp K v)(Vr K v) (an N)) ((F m) ±R -aR p)))"

definition
  Pseql :: "[('b, 'm) Ring_scheme, 'b, _, 'b ⇒ ant, nat, 
             nat ⇒ 'b] ⇒ nat ⇒ 'b" 
            ("(6Pseql_  _ _ _ _ _)" [90,90,90,90,90,91]90) where
  "PseqlR X K v d F = (λn. (ldeg_p R (Vr K v) X d (F n)))"

   (** deg R (Vr K v) X (F n) ≤ an (Suc d) **)

definition
  Pseqh :: "[('b, 'm) Ring_scheme, 'b, _, 'b ⇒ ant, nat, nat ⇒ 'b] ⇒  
        nat ⇒ 'b" 
           ("(6Pseqh _ _ _ _ _ _)" [90,90,90,90,90,91]90) where
  "PseqhR X K v d F = (λn. (hdeg_p R (Vr K v) X (Suc d) (F n)))"

    (** deg R (Vr K v) X (F n) ≤ an (Suc d) **)

lemma an_neq_minf[simp]:"∀n. -∞ ≠ an n"
apply (rule allI)
apply (simp add:an_def) apply (rule not_sym) apply simp
done

lemma an_neq_minf1[simp]:"∀n. an n ≠ -∞" 
apply (rule allI) apply (simp add:an_def)
done

lemma (in Corps) Pseql_mem:"⟦valuation K v; PolynRg R (Vr K v) X;
      F n ∈ carrier R; ∀n. deg R (Vr K v) X (F n) ≤ an (Suc d)⟧ ⟹
                     (PseqlR X K v d F) n ∈ carrier R"
apply (frule PolynRg.is_Ring)
apply (simp add:Pseql_def)
apply (frule Vr_ring[of "v"], 
       rule PolynRg.ldeg_p_mem, assumption+, simp)
done

lemma (in Corps) Pseqh_mem:"⟦valuation K v; PolynRg R (Vr K v) X;
      F n ∈ carrier R; ∀n. deg R (Vr K v) X (F n) ≤ an (Suc d)⟧ ⟹
                     (PseqhR X K v d F) n ∈ carrier R"
apply (frule PolynRg.is_Ring)
apply (frule Vr_ring[of "v"]) 
apply (frule PolynRg.subring[of "R" "Vr K v" "X"])
apply (frule PolynRg.X_mem_R[of "R" "Vr K v" "X"])
apply (simp del:npow_suc add:Pseqh_def)
apply (rule PolynRg.hdeg_p_mem, assumption+, simp)
done

lemma (in Corps) PCauchy_lTr:"⟦valuation K v; PolynRg R (Vr K v) X;
    p ∈ carrier R; deg R (Vr K v) X p ≤ an (Suc d); 
    P_mod R (Vr K v) X (vp K v(Vr K v) (an N)) p⟧ ⟹
    P_mod R (Vr K v) X (vp K v(Vr K v) (an N)) (ldeg_p R (Vr K v) X d p)"
apply (frule PolynRg.is_Ring)
apply (simp add:ldeg_p_def)
apply (frule Vr_ring[of v])
apply (frule PolynRg.scf_d_pol[of "R" "Vr K v" "X" "p" "Suc d"], assumption+,
       (erule conjE)+)
apply (frule_tac n = "an N" in vp_apow_ideal[of v], simp)
apply (frule PolynRg.P_mod_mod[THEN sym, of R "Vr K v" X "vp K v (Vr K v) (an N)"
       p "scf_d R (Vr K v) X p (Suc d)"], assumption+, simp)
apply (subst PolynRg.polyn_expr_short[of R "Vr K v" X 
             "scf_d R (Vr K v) X p (Suc d)" d], assumption+, simp)
apply (subst PolynRg.P_mod_mod[THEN sym, of R "Vr K v" X "vp K v (Vr K v) (an N)"
       "polyn_expr R X d (d, snd (scf_d R (Vr K v) X p (Suc d)))" 
       "(d, snd (scf_d R (Vr K v) X p (Suc d)))"], assumption+)
apply (subst PolynRg.polyn_expr_short[THEN sym], simp+,
       simp add:PolynRg.polyn_mem)
apply (subst pol_coeff_def, rule allI, rule impI, 
       simp add:PolynRg.pol_coeff_mem)
apply simp+
done

lemma (in Corps) PCauchy_hTr:"⟦valuation K v; PolynRg R (Vr K v) X;
      p ∈ carrier R; deg R (Vr K v) X p ≤ an (Suc d); 
      P_mod R (Vr K v) X (vp K v(Vr K v) (an N)) p⟧
  ⟹ P_mod R (Vr K v) X (vp K v(Vr K v) (an N)) (hdeg_p R (Vr K v) X (Suc d) p)"
apply (frule PolynRg.is_Ring)
apply (cut_tac Vr_ring[of v])
apply (frule PolynRg.scf_d_pol[of R "Vr K v" X p "Suc d"], assumption+)
apply (frule_tac n = "an N" in vp_apow_ideal[of v], simp)
apply (frule PolynRg.P_mod_mod[THEN sym, of "R" "Vr K v" "X" 
       "vp K v (Vr K v) (an N)" p "scf_d R (Vr K v) X p (Suc d)"], assumption+,
       simp+)
apply (subst hdeg_p_def) 
apply (subst PolynRg.monomial_P_mod_mod[THEN sym, of "R" "Vr K v" "X" 
       "vp K v (Vr K v) (an N)" "snd (scf_d R (Vr K v) X p (Suc d)) (Suc d)" 
       "(snd (scf_d R (Vr K v) X p (Suc d)) (Suc d)) ⋅rR (X^R (Suc d))" 
       "Suc d"], 
       assumption+)
apply (rule PolynRg.pol_coeff_mem[of R "Vr K v" X 
       "scf_d R (Vr K v) X p (Suc d)" "Suc d"], assumption+, simp+)
done
 
lemma (in Corps) v_ldeg_p_pOp:"⟦valuation K v; PolynRg R (Vr K v) X; 
      p ∈ carrier R; q ∈ carrier R; deg R (Vr K v) X p ≤ an (Suc d); 
      deg R (Vr K v) X q ≤ an (Suc d)⟧ ⟹
      (ldeg_p R (Vr K v) X d p) ±R (ldeg_p R (Vr K v) X d q) =
                              ldeg_p R (Vr K v) X d (p ±R q)"
by (simp add:PolynRg.ldeg_p_pOp[of R "Vr K v" X p q d]) 

lemma (in Corps) v_hdeg_p_pOp:"⟦valuation K v; PolynRg R (Vr K v) X; 
      p ∈ carrier R; q ∈ carrier R; deg R (Vr K v) X p ≤ an (Suc d); 
      deg R (Vr K v) X q ≤ an (Suc d)⟧ ⟹ (hdeg_p R (Vr K v) X (Suc d) p) ±R 
      (hdeg_p R (Vr K v) X (Suc d) q) = hdeg_p R (Vr K v) X (Suc d) (p ±R q)"
by (simp add:PolynRg.hdeg_p_pOp[of R "Vr K v" X p q d])

lemma (in Corps) v_ldeg_p_mOp:"⟦valuation K v; PolynRg R (Vr K v) X; 
       p ∈ carrier R;deg R (Vr K v) X p ≤ an (Suc d)⟧ ⟹ 
       -aR (ldeg_p R (Vr K v) X d p) = ldeg_p R (Vr K v) X d (-aR p)"
by (simp add:PolynRg.ldeg_p_mOp)


lemma (in Corps) v_hdeg_p_mOp:"⟦valuation K v; PolynRg R (Vr K v) X; 
    p ∈ carrier R;deg R (Vr K v) X p ≤ an (Suc d)⟧ ⟹
   -aR (hdeg_p R (Vr K v) X (Suc d) p) = hdeg_p R (Vr K v) X (Suc d) (-aR p)"
by (simp add:PolynRg.hdeg_p_mOp)

lemma (in Corps) PCauchy_lPCauchy:"⟦valuation K v; PolynRg R (Vr K v) X; 
      ∀n. F n ∈ carrier R;  ∀n. deg R (Vr K v) X (F n) ≤ an (Suc d); 
      P_mod R (Vr K v) X (vp K v(Vr K v) (an N)) (F n ±R -aR (F m))⟧
      ⟹ P_mod R (Vr K v) X (vp K v(Vr K v) (an N))
                     (((PseqlR X K v d F) n) ±R -aR ((PseqlR X K v d F) m))"
apply (frule PolynRg.is_Ring)
apply (cut_tac Vr_ring[of v],
       frule Ring.ring_is_ag[of "R"],
       frule PolynRg.subring[of "R" "Vr K v" "X"])
apply (simp add:Pseql_def)
apply (subst v_ldeg_p_mOp[of "v" "R" "X" _ "d"], assumption+,
       simp, simp)
apply (subst v_ldeg_p_pOp[of v R X "F n" "-aR (F m)"], assumption+,
       simp, rule aGroup.ag_mOp_closed, assumption, simp, simp,
       simp add:PolynRg.deg_minus_eq1)
apply (rule PCauchy_lTr[of v R X "F n ±R -aR (F m)" "d" "N"],
       assumption+,
       rule aGroup.ag_pOp_closed[of "R" "F n" "-aR (F m)"], assumption+,
       simp, rule aGroup.ag_mOp_closed, assumption+, simp)
apply (frule PolynRg.deg_minus_eq1 [of "R" "Vr K v" "X" "F m"], simp)
apply (rule PolynRg.polyn_deg_add4[of "R" "Vr K v" "X" "F n" 
       "-aR (F m)" "Suc d"], assumption+, simp,
       rule aGroup.ag_mOp_closed, assumption, simp+)
done

lemma (in Corps) PCauchy_hPCauchy:"⟦valuation K v; PolynRg R (Vr K v) X;
      ∀n. F n ∈ carrier R; ∀n. deg R (Vr K v) X (F n) ≤ an (Suc d); 
      P_mod R (Vr K v) X (vp K v(Vr K v) (an N)) (F n ±R -aR (F m))⟧
      ⟹ P_mod R (Vr K v) X (vp K v(Vr K v) (an N))
                     (((PseqhR X K v d F) n) ±R -aR ((PseqhR X K v d F) m))"
apply (frule PolynRg.is_Ring)
apply (frule Vr_ring[of v], frule Ring.ring_is_ag[of "R"],
       frule PolynRg.subring[of "R" "Vr K v" "X"], 
       frule vp_apow_ideal[of v "an N"], simp) 

apply (simp add:Pseqh_def,
       subst v_hdeg_p_mOp[of v R X "F m" "d"], assumption+,
       simp+)

apply (subst v_hdeg_p_pOp[of v R X "F n" "-aR (F m)"], assumption+,
       simp, rule aGroup.ag_mOp_closed, assumption, simp, simp,
       frule PolynRg.deg_minus_eq1 [of "R" "Vr K v" "X" "F m"],
       simp+ )
apply (frule PCauchy_hTr[of "v" "R" "X" "F n ±R -aR (F m)" "d" "N"],
    assumption+,
    rule aGroup.ag_pOp_closed[of "R" "F n" "-aR (F m)"], assumption+,
    simp, rule aGroup.ag_mOp_closed, assumption+, simp)
apply (frule PolynRg.deg_minus_eq1 [of "R" "Vr K v" "X" "F m"], simp+)
apply (rule PolynRg.polyn_deg_add4[of "R" "Vr K v" "X" "F n" "-aR (F m)" 
       "Suc d"], assumption+,
       simp, rule aGroup.ag_mOp_closed, assumption, simp+)
done

(** Don't forget  t_vp_apow  ***)
 
lemma (in Corps) Pseq_decompos:"⟦valuation K v; PolynRg R (Vr K v) X;
      F n ∈ carrier R; deg R (Vr K v) X (F n) ≤ an (Suc d)⟧
      ⟹ F n = ((PseqlR X K v d F) n) ±R ((PseqhR X K v d F) n)"
apply (frule PolynRg.is_Ring)
apply (simp del:npow_suc add:Pseql_def Pseqh_def)
apply (frule Vr_ring[of v])
apply (frule PolynRg.subring[of "R" "Vr K v" "X"])
apply (rule PolynRg.decompos_p[of "R" "Vr K v" "X" "F n" "d"], assumption+)
done

lemma (in Corps) deg_0_const:"⟦valuation K v; PolynRg R (Vr K v) X;
      p ∈ carrier R; deg R (Vr K v) X p ≤ 0⟧ ⟹ p ∈ carrier (Vr K v)"
apply (frule Vr_ring[of v])
apply (frule PolynRg.subring)
apply (frule PolynRg.is_Ring)
apply (case_tac "p = 𝟬R", simp,
       simp add:Ring.Subring_zero_ring_zero[THEN sym],
       simp add:Ring.ring_zero)
apply (subst PolynRg.pol_of_deg0[THEN sym, of "R" "Vr K v" "X" "p"], 
        assumption+)
apply (simp add:PolynRg.deg_an, simp only:an_0[THEN sym])
apply (simp only:ale_nat_le[of "deg_n R (Vr K v) X p" "0"])
done

lemma (in Corps) monomial_P_limt:"⟦valuation K v; Completev K; 
     PolynRg R (Vr K v) X; ∀n. f n ∈ carrier (Vr K v);
     ∀n. F n = (f n) ⋅rR (X^R d);  ∀N. ∃M. ∀n m. M < n ∧ M < m ⟶
     P_mod R (Vr K v) X (vp K v(Vr K v) (an N)) (F n ±R -aR (F m))⟧ ⟹ 
        ∃b∈carrier (Vr K v). Plimit R X K v F (b ⋅rR (X^R d))"
apply (frule PolynRg.is_Ring)
apply (frule Vr_ring[of v])
apply (frule PolynRg.subring[of "R" "Vr K v" "X"])
apply simp

apply (subgoal_tac "Cauchy K v f")
 apply (simp add:v_complete_def)
 apply (drule_tac a = f in forall_spec)
 apply (thin_tac "∀N. ∃M. ∀n m. M < n ∧ M < m ⟶
        P_mod R (Vr K v) X (vp K v(Vr K v) (an N))
        ((f n) ⋅rR (X^R d) ±R -aR (f m) ⋅rR (X^R d))", assumption)
 apply (erule exE, erule conjE)
 apply (subgoal_tac "b ∈ carrier (Vr K v)")
 apply (subgoal_tac "Plimit R X K v F (b ⋅rR (X^R d))", blast)
 
(******* b ∈ carrier (Vr K v) ***********)
apply (simp add:pol_limit_def)
apply (rule conjI)
 apply (rule allI)
 apply (rule Ring.ring_tOp_closed[of "R"], assumption)
 apply (frule PolynRg.subring[of "R" "Vr K v" "X"])
 apply (rule Ring.mem_subring_mem_ring[of "R" "Vr K v"], assumption+) 
 apply simp
 
 apply (frule PolynRg.X_mem_R[of "R" "Vr K v" "X"])
 apply (simp add:Ring.npClose)
apply (thin_tac "∀n. F n = f n ⋅rR X^R d") 
apply (simp add:limit_def)
 apply (rule allI)
(* apply (simp add:t_vp_apow[of "K" "v" "t"]) *) 
 apply (rotate_tac -2, drule_tac x = N in spec) 
 apply (erule exE)
 apply (subgoal_tac "∀n> M. P_mod R (Vr K v) X (vp K v (Vr K v) (an N))
                   ((f n)⋅rR (X^R d) ±R -aR (b ⋅rR (X^R d)))", blast) 
 apply (rule allI, rule impI)
 apply (rotate_tac -2, drule_tac x = n in spec, simp)
 apply (drule_tac x = n in spec)

apply (frule_tac x = "f n" in Ring.mem_subring_mem_ring[of "R" "Vr K v"], 
       assumption+,
       frule_tac x = b in Ring.mem_subring_mem_ring[of "R" "Vr K v"], 
       assumption+)
apply (frule PolynRg.X_mem_R[of "R" "Vr K v" "X"])
 apply (frule Ring.npClose[of "R" "X" "d"], assumption+)
 apply (simp add:Ring.ring_inv1_1)
 apply (frule Ring.ring_is_ag[of "R"],
        frule_tac x = b in aGroup.ag_mOp_closed[of "R"], assumption+)
 apply (subst Ring.ring_distrib2[THEN sym, of "R" "X^R d"], assumption+)

 apply (frule_tac n = "an N" in vp_apow_ideal[of v], simp) 
 apply (frule_tac I = "vp K v (Vr K v) (an N)" and c = "f n ±R -aR b" and 
        p = "(f n ±R -aR b) ⋅rR (X^R d)" in  
        PolynRg.monomial_P_mod_mod[of "R" "Vr K v" "X" _ _ _ "d"], assumption+)
 apply (simp add:Ring.Subring_minus_ring_minus[THEN sym])
 apply (frule Ring.ring_is_ag[of "Vr K v"])
 apply (frule_tac x = b in aGroup.ag_mOp_closed[of "Vr K v"], assumption+)
 apply (simp only:Ring.Subring_pOp_ring_pOp[THEN sym])
 apply (rule aGroup.ag_pOp_closed, assumption+) apply simp
 apply (frule_tac I1 = "vp K v (Vr K v) (an N)" and c1 = "f n ±R -aR b" and 
     p1 = "(f n ±R -aR b) ⋅rR (X^R d)" in PolynRg.monomial_P_mod_mod[THEN sym, 
     of "R" "Vr K v" "X" _ _ _ "d"], assumption+)
 apply (frule Ring.ring_is_ag[of "Vr K v"])
 apply (frule_tac x = b in aGroup.ag_mOp_closed[of "Vr K v"], assumption+)
 apply (simp only:Ring.Subring_minus_ring_minus[THEN sym])
 apply (simp only:Ring.Subring_pOp_ring_pOp[THEN sym])
 apply (rule aGroup.ag_pOp_closed, assumption+) apply simp apply simp
 apply (simp only:Vr_mOp_f_mOp[THEN sym])
 apply (frule Ring.ring_is_ag[of "Vr K v"])
 apply (frule_tac x = b in aGroup.ag_mOp_closed[of "Vr K v"], assumption+)
 apply (simp add:Vr_pOp_f_pOp[THEN sym])
 apply (simp add:Ring.Subring_pOp_ring_pOp)
 apply (simp add:Ring.Subring_minus_ring_minus)

 apply (case_tac "b = 𝟬K", simp add:Vr_0_f_0[THEN sym], 
        simp add:Ring.ring_zero)
 apply (frule_tac b = b in limit_val[of  _ "f" "v"], assumption+,
        rule allI,
        frule_tac x = j in spec, simp add:Vr_mem_f_mem,
        assumption+, erule exE)
 apply (thin_tac "∀n. F n = f n ⋅rR X^R d",
        thin_tac "∀N. ∃M. ∀n m. M < n ∧ M < m ⟶
                         P_mod R (Vr K v) X (vp K v (Vr K v) (an N))
                          (f n ⋅rR X^R d ±R -aR f m ⋅rR X^R d)")  
 apply (rotate_tac -1, drule_tac x = "Suc N" in spec, simp)
 apply (drule_tac x = "Suc N" in spec)
 apply (frule_tac x1 = "f (Suc N)" in val_pos_mem_Vr[THEN sym, of v],
        simp add:Vr_mem_f_mem, simp, simp add:val_pos_mem_Vr[of v]) 

apply (simp add:Cauchy_seq_def)
 apply (simp add:Vr_mem_f_mem)
 apply (rule allI)
 apply (rotate_tac -3, frule_tac x = N in spec)

 apply (thin_tac "∀n. F n = f n ⋅rR X^R d")
 (*apply (simp add:t_vp_apow[of "K" "v" "t"]) *) 
 apply (frule_tac n = "an N" in vp_apow_ideal[of "v"], simp)
 apply (drule_tac x = N in spec, erule exE) 
 apply (subgoal_tac "∀n m. M < n ∧ M < m ⟶
                      f n ± -a (f m) ∈ vp K v (Vr K v) (an N)", blast)
 apply (rule allI)+
 apply (rule impI, erule conjE)
 apply (frule_tac I = "vp K v (Vr K v) (an N)" and c = "f n ± -a (f m)" and 
   p = "(f n ± -a (f m)) ⋅rR (X^R d)" in
   PolynRg.monomial_P_mod_mod[of "R" "Vr K v" "X" _ _ _ "d"], assumption+)
 
 apply (frule_tac x = n in spec,
        drule_tac x = m in spec)
 apply (frule Ring.ring_is_ag[of "Vr K v"],
        simp add:Vr_mOp_f_mOp[THEN sym],
        frule_tac x = "f m" in aGroup.ag_mOp_closed[of "Vr K v"], assumption+,
        simp add:Vr_pOp_f_pOp[THEN sym])
 apply (rule aGroup.ag_pOp_closed, assumption+, simp)
 apply simp 
 apply (thin_tac "(f n ± -a f m ∈ vp K v (Vr K v) (an N)) =
        P_mod R (Vr K v) X (vp K v (Vr K v) (an N)) ((f n ± -a f m) ⋅rR X^R d)")
 apply (rotate_tac -3, drule_tac x = n in spec,
        rotate_tac -1, drule_tac x = m in spec, simp)
 apply (frule_tac x = n in spec,
        drule_tac x = m in spec)
 apply (frule_tac x = "f n" in Ring.mem_subring_mem_ring[of R "Vr K v"],
         assumption+,
        frule_tac x = "f m" in Ring.mem_subring_mem_ring[of R "Vr K v"],
         assumption+,
        frule Ring.ring_is_ag[of R],
        frule_tac x = "f m" in aGroup.ag_mOp_closed[of R], assumption+,
        frule PolynRg.X_mem_R[of R "Vr K v" X],
        frule Ring.npClose[of R X d], assumption)
 apply (simp add:Ring.ring_inv1_1[of R],
        frule_tac y1 = "f n" and z1 = "-aR f m" in Ring.ring_distrib2[
        THEN sym, of R "X^R d"], assumption+, simp,
        thin_tac "f n ⋅rR X^R d ±R (-aR f m) ⋅rR X^R d =
                                           (f n ±R -aR f m) ⋅rR X^R d")
 apply (simp only:Ring.Subring_minus_ring_minus[THEN sym,of R "Vr K v"])
 apply (frule Ring.subring_Ring[of R "Vr K v"], assumption,
        frule Ring.ring_is_ag[of "Vr K v"],
        frule_tac x = "f m" in aGroup.ag_mOp_closed[of "Vr K v"], assumption+)
 apply (simp add:Ring.Subring_pOp_ring_pOp[THEN sym, of R "Vr K v"],
        simp add:Vr_pOp_f_pOp, simp add:Vr_mOp_f_mOp)
done

lemma (in Corps) mPlimit_uniqueTr:"⟦valuation K v; 
     PolynRg R (Vr K v) X; ∀n. f n ∈ carrier (Vr K v);
     ∀n. F n = (f n) ⋅rR (X^R d); c ∈ carrier (Vr K v);
     Plimit R X K v F (c ⋅rR (X^R d))⟧  ⟹ lim K v f c" 
apply (frule PolynRg.is_Ring,
       simp add:pol_limit_def limit_def,
       rule allI,
       erule conjE,
       rotate_tac -1, drule_tac x = N in spec,
       erule exE)
apply (subgoal_tac "∀n. M < n ⟶ f n ± -a c ∈ vp K v (Vr K v) (an N)", blast)
apply (rule allI, rule impI,
       rotate_tac -2, drule_tac x = n in spec, simp,
       drule_tac x = n in spec,
       drule_tac x = n in spec,
       thin_tac "∀n. f n ⋅rR X^R d ∈ carrier R")
apply (frule Vr_ring[of v],
       frule PolynRg.X_mem_R[of "R" "Vr K v" "X"],
       frule Ring.npClose[of "R" "X" "d"], assumption+,
       frule PolynRg.subring[of "R" "Vr K v" "X"])
apply (frule_tac x = c in Ring.mem_subring_mem_ring[of "R" "Vr K v"], 
       assumption+,
      frule_tac x = "f n" in Ring.mem_subring_mem_ring[of "R" "Vr K v"], 
       assumption+)
apply (simp add:Ring.ring_inv1_1,
       frule Ring.ring_is_ag[of "R"], 
       frule aGroup.ag_mOp_closed[of "R" "c"], assumption+)
apply (simp add:Ring.ring_distrib2[THEN sym, of "R" "X^R d" _ "-aR c"],
       simp add:Ring.Subring_minus_ring_minus[THEN sym],
       frule Ring.ring_is_ag[of "Vr K v"],
       frule aGroup.ag_mOp_closed[of "Vr K v" "c"], assumption+)
apply (simp add:Ring.Subring_pOp_ring_pOp[THEN sym],
       frule_tac x = "f n" in aGroup.ag_pOp_closed[of "Vr K v" _ 
        "-a(Vr K v) c"], assumption+,
       frule_tac n = "an N" in vp_apow_ideal[of "v"], simp,
       frule_tac I1 = "vp K v (Vr K v) (an N)" and 
        c1 = "f n ±(Vr K v) -a(Vr K v) c" and p1 = "(f n ±(Vr K v) -a(Vr K v) c)
       ⋅rR (X^R d)" in PolynRg.monomial_P_mod_mod[THEN sym, of R "Vr K v" 
        X _ _ _ d], assumption+, simp, simp)
 apply (simp add:Vr_pOp_f_pOp, simp add:Vr_mOp_f_mOp)
done

lemma (in Corps) mono_P_limt_unique:"⟦valuation K v; 
  PolynRg R (Vr K v) X; ∀n. f n ∈ carrier (Vr K v); 
  ∀n. F n = (f n) ⋅rR (X^R d); b ∈ carrier (Vr K v); c ∈ carrier (Vr K v);
  Plimit R X K v F (b ⋅rR (X^R d)); Plimit R X K v F (c ⋅rR (X^R d))⟧ ⟹ 
        b  ⋅rR (X^R d) = c ⋅rR (X^R d)" 
apply (frule PolynRg.is_Ring)
apply (frule_tac mPlimit_uniqueTr[of v R X f F d b], assumption+,
       frule_tac mPlimit_uniqueTr[of v R X f F d c], assumption+)
apply (frule Vr_ring[of v],
       frule PolynRg.subring[of "R" "Vr K v" "X"],
       frule Vr_mem_f_mem[of v b], assumption+,
       frule Vr_mem_f_mem[of v c], assumption+,
       frule limit_unique[of b f v c])
apply (rule allI, simp add:Vr_mem_f_mem, assumption+, simp)
done 

lemma (in Corps) Plimit_deg:"⟦valuation K v; PolynRg R (Vr K v) X; 
  ∀n. F n ∈ carrier R; ∀n. deg R (Vr K v) X (F n) ≤ (an d); 
  p ∈ carrier R; Plimit R X K v F p⟧ ⟹  deg R (Vr K v) X p ≤ (an d)"
apply (frule PolynRg.is_Ring, frule Vr_ring[of v])
apply (case_tac "p = 𝟬R", simp add:deg_def)
apply (rule contrapos_pp, simp+,
       simp add:aneg_le,
       frule PolynRg.s_cf_expr[of R "Vr K v" X p], assumption+, (erule conjE)+,
       frule PolynRg.s_cf_deg[of R "Vr K v" X p], assumption+,
       frule PolynRg.pol_coeff_mem[of R "Vr K v" X "s_cf R (Vr K v) X p" 
        "fst (s_cf R (Vr K v) X p)"], assumption+, simp,
       frule Vr_mem_f_mem[of v "snd (s_cf R (Vr K v) X p) 
            (fst (s_cf R (Vr K v) X p))"], assumption+)
(* show the value of the leading coefficient is noninf *)
apply (frule val_nonzero_noninf[of "v" 
       "snd (s_cf R (Vr K v) X p) (fst (s_cf R (Vr K v) X p))"], assumption,
       simp add:Vr_0_f_0,
       frule val_pos_mem_Vr[THEN sym, of v "snd (s_cf R (Vr K v) X p) 
         (fst (s_cf R (Vr K v) X p))"], assumption+, simp,
       frule value_in_aug_inf[of "v" "snd (s_cf R (Vr K v) X p) 
          (fst (s_cf R (Vr K v) X p))"], assumption+,
       cut_tac mem_ant[of "v (snd (s_cf R (Vr K v) X p) 
       (fst (s_cf R (Vr K v) X p)))"], simp add:aug_inf_def,
       erule exE, simp, simp only:ant_0[THEN sym], simp only:ale_zle,
       frule_tac z = z in zpos_nat, erule exE, simp,
       thin_tac "z = int n")

(* show that the leading coefficient of p shoule be 0. contradiction *)
apply (simp add:pol_limit_def)
apply (rotate_tac 5, drule_tac x = "Suc n" in spec) 
apply (erule exE)
apply (rotate_tac -1, 
       drule_tac x = "Suc M" in spec, simp del:npow_suc,
       drule_tac x = "Suc M" in spec, 
       drule_tac x = "Suc M" in spec)

  (**** Only formula manipulation to obtain
        P_mod R (Vr K v) X (vp K v Vr K v an (Suc n))
         (polyn_expr R X (fst (s_cf R (Vr K v) X p))
           (add_cf (Vr K v) f
             (fst (s_cf R (Vr K v) X p),
              λj. -aVr K v snd (s_cf R (Vr K v) X p) j))) *****)
apply (frule PolynRg.polyn_minus[of R "Vr K v" X "s_cf R (Vr K v) X p" 
       "fst (s_cf R (Vr K v) X p)"], assumption+, simp,
   frule PolynRg.minus_pol_coeff[of R "Vr K v" X "s_cf R (Vr K v) X p"],
        assumption+, drule sym,
   frule_tac x = "deg R (Vr K v) X (F (Suc M))" in ale_less_trans[of _ 
       "an d" "deg R (Vr K v) X p"], assumption+,
   frule_tac p = "F (Suc M)" and d = "deg_n R (Vr K v) X p" in 
            PolynRg.pol_expr_edeg[of "R" "Vr K v" "X"], assumption+,
   frule_tac x = "deg R (Vr K v) X (F (Suc M))" and 
         y = "deg R (Vr K v) X p" in aless_imp_le,
      subst PolynRg.deg_an[THEN sym, of "R" "Vr K v" "X" "p"], assumption+,
      erule exE, (erule conjE)+,
   frule_tac c = f in PolynRg.polyn_add1[of "R" "Vr K v" "X" _ 
    "(fst (s_cf R (Vr K v) X p), λj. -aVr K v snd (s_cf R (Vr K v) X p) j)"],
    assumption+, simp,
   thin_tac "-aR p = polyn_expr R X (fst (s_cf R (Vr K v) X p))
    (fst (s_cf R (Vr K v) X p), λj. -aVr K v snd (s_cf R (Vr K v) X p) j)",
   thin_tac "polyn_expr R X (fst (s_cf R (Vr K v) X p))
             (s_cf R (Vr K v) X p) = p",
   thin_tac "F (Suc M) = polyn_expr R X (fst (s_cf R (Vr K v) X p)) f",
   thin_tac "polyn_expr R X (fst (s_cf R (Vr K v) X p)) f ±R
       polyn_expr R X (fst (s_cf R (Vr K v) X p))
        (fst (s_cf R (Vr K v) X p), λj. -aVr K v snd (s_cf R (Vr K v) X p) j) =
       polyn_expr R X (fst (s_cf R (Vr K v) X p)) (add_cf (Vr K v) f
       (fst (s_cf R (Vr K v) X p), λj. -aVr K v snd (s_cf R (Vr K v) X p) j))")

(** apply P_mod_mod to obtain a condition of coefficients **) 
 apply (frule_tac n = "an (Suc n)" in vp_apow_ideal[of "v"], simp,
   frule_tac p1 = "polyn_expr R X (fst (s_cf R (Vr K v) X p))(add_cf (Vr K v) f
   (fst (s_cf R (Vr K v) X p), λj. -aVr K v snd (s_cf R (Vr K v) X p) j))" and
  I1= "vp K v (Vr K v) (an (Suc n))" and c1 = "add_cf (Vr K v) f (fst 
   (s_cf R (Vr K v) X p), λj. -aVr K v snd (s_cf R (Vr K v) X p) j)" in 
  PolynRg.P_mod_mod[THEN sym, of R "Vr K v" X], assumption+,
  rule PolynRg.polyn_mem[of R "Vr K v" X], assumption+,
  rule PolynRg.add_cf_pol_coeff[of R "Vr K v" X], assumption+,
  simp add:PolynRg.add_cf_len,
  rule PolynRg.add_cf_pol_coeff[of R "Vr K v" X], assumption+,
  simp add:PolynRg.add_cf_len,
  simp add:PolynRg.add_cf_len)
 apply (drule_tac x = "fst (s_cf R (Vr K v) X p)" in spec, simp,
        thin_tac "P_mod R (Vr K v) X (vp K v (Vr K v) (an (Suc n)))
         (polyn_expr R X (fst (s_cf R (Vr K v) X p)) (add_cf (Vr K v) f
      (fst (s_cf R (Vr K v) X p), λj. -aVr K v snd (s_cf R (Vr K v) X p) j)))",
      simp add:add_cf_def)
 (**** we obtained snd (add_cf (Vr K v) f (fst (s_cf R (Vr K v) X p),
     λj. -aVr K v snd (s_cf R (Vr K v) X p) j)) (fst (s_cf R (Vr K v) X p))
           ∈ vp K v Vr K v an (Suc n)   ***)
 apply (frule_tac p = "polyn_expr R X (fst (s_cf R (Vr K v) X p)) f" and 
       c = f and j = "fst f" in PolynRg.pol_len_gt_deg[of R "Vr K v" X],
       assumption+, simp, drule sym, simp add:PolynRg.deg_an) apply simp
 apply (rotate_tac -4, drule sym, simp)
 apply (frule Ring.ring_is_ag[of "Vr K v"],
        frule_tac x = "snd (s_cf R (Vr K v) X p) (fst f)" in 
        aGroup.ag_mOp_closed[of "Vr K v"], assumption+,
        simp add:aGroup.ag_l_zero) 
 apply (frule_tac I = "vp K v (Vr K v) (an (Suc n))" and 
        x = "-aVr K v snd (s_cf R (Vr K v) X p) (fst f)" in 
        Ring.ideal_inv1_closed[of "Vr K v"], assumption+)
 apply (simp add:aGroup.ag_inv_inv)
 apply (frule_tac n = "an (Suc n)" and x = "snd (s_cf R (Vr K v) X p) (fst f)"
         in n_value_x_1[of v], simp+)    
 apply (frule_tac x = "snd (s_cf R (Vr K v) X p) (fst f)" in 
         n_val_le_val[of v], assumption+, simp add:ant_int) 
 apply (drule_tac i = "an (Suc n)" and 
        j = "n_val K v (snd (s_cf R (Vr K v) X p) (fst f))" and
        k = "v (snd (s_cf R (Vr K v) X p) (fst f))" in ale_trans,
        assumption+)
 apply (simp add:ant_int ale_natle)
done

lemma (in Corps) Plimit_deg1:"⟦valuation K v; Ring R; PolynRg R (Vr K v) X; 
  ∀n. F n ∈ carrier R; ∀n. deg R (Vr K v) X (F n) ≤ ad; 
  p ∈ carrier R; Plimit R X K v F p⟧ ⟹  deg R (Vr K v) X p ≤ ad"
apply (frule Vr_ring[of v])
apply (case_tac "∀n. F n = 𝟬R")
apply (frule Plimit_deg[of v R X F 0 p], assumption+,
       rule allI, simp add:deg_def, assumption+)
apply (case_tac "p = 𝟬R", simp add:deg_def,
       frule PolynRg.nonzero_deg_pos[of R "Vr K v" X p], assumption+,
       simp,
       frule PolynRg.pols_const[of "R" "Vr K v" "X" "p"], assumption+,
       simp,
       frule PolynRg.pols_const[of "R" "Vr K v" "X" "p"], assumption+,
       simp add:ale_refl)
 apply (subgoal_tac "p = 𝟬R", simp)
 apply (thin_tac "p ≠ 𝟬R")
 apply (rule contrapos_pp, simp+)

apply (frule n_val_valuation[of v])
apply (frule val_nonzero_z[of "n_val K v" "p"])
 apply (simp add:Vr_mem_f_mem)
 apply (frule PolynRg.subring[of "R" "Vr K v" "X"])
 apply (simp only:Ring.Subring_zero_ring_zero[THEN sym, of "R" "Vr K v"])
 apply (simp add:Vr_0_f_0, erule exE)
 apply (frule val_pos_mem_Vr[THEN sym, of "v" "p"])
 apply (simp add:Vr_mem_f_mem, simp)
 apply (frule val_pos_n_val_pos[of "v" "p"])
 apply (simp add:Vr_mem_f_mem, simp)
 apply (simp add:ant_0[THEN sym])
apply (frule_tac z = z in zpos_nat, erule exE)
apply (unfold pol_limit_def, erule conjE)
 apply (rotate_tac -1, drule_tac x = "Suc n" in spec)
 apply (subgoal_tac "¬ (∃M. ∀m. M < m ⟶
             P_mod R (Vr K v) X (vp K v (Vr K v) (an (Suc n))) ( F m ±R -aR p))")
 apply blast
 apply (thin_tac "∃M. ∀m. M < m ⟶
           P_mod R (Vr K v) X (vp K v (Vr K v) (an (Suc n))) (F m ±R -aR p)")
 apply simp
 apply (subgoal_tac "M < (Suc M) ∧
       ¬ P_mod R (Vr K v) X (vp K v (Vr K v) (an (Suc n))) (𝟬R ±R -aR p)")
 apply blast
 apply simp
 apply (frule Ring.ring_is_ag[of "R"])
 apply (frule aGroup.ag_mOp_closed[of "R" "p"], assumption) 
 apply (simp add:aGroup.ag_l_zero)
 apply (frule Ring.ring_is_ag[of "Vr K v"])
 apply (frule aGroup.ag_mOp_closed[of "Vr K v" "p"], assumption) 
 apply (frule_tac n = "an (Suc n)" in vp_apow_ideal[of v], simp)
 apply (frule PolynRg.subring[of "R" "Vr K v" "X"])
 apply (simp add:Ring.Subring_minus_ring_minus[THEN sym, of "R" "Vr K v"])
 apply (simp add:PolynRg.P_mod_coeffTr[of "R" "Vr K v" "X" _ "-a(Vr K v) p"])
 apply (rule contrapos_pp, simp+)

 apply (frule_tac I = "vp K v (Vr K v) (an (Suc n))" in 
        Ring.ideal_inv1_closed[of "Vr K v" _ "-a(Vr K v) p"], assumption+)
 apply (simp add:aGroup.ag_inv_inv)
 apply (frule_tac n = "an (Suc n)" in n_value_x_1[of "v" _ "p"], simp)   
 apply assumption
 apply simp
 apply (simp add:ant_int, simp add:ale_natle)

apply (fold pol_limit_def) 
apply (case_tac "ad = ∞", simp)
apply simp apply (erule exE)
apply (subgoal_tac "0 ≤ ad")
apply (frule Plimit_deg[of "v" "R" "X" "F" "na ad" "p"], assumption+)
 apply (simp add:an_na)+
apply (drule_tac x = n in spec,
       drule_tac x = n in spec)

apply (frule_tac p = "F n" in PolynRg.nonzero_deg_pos[of "R" "Vr K v" "X"],
           assumption+)
apply (rule_tac j = "deg R (Vr K v) X (F n)" in ale_trans[of "0" _ "ad"],
           assumption+)
done

lemma (in Corps) Plimit_ldeg:"⟦valuation K v; PolynRg R (Vr K v) X;
     ∀n. F n ∈ carrier R; p ∈ carrier R; 
     ∀n. deg R (Vr K v) X (F n) ≤ an (Suc d); 
      Plimit R X K v F p⟧  ⟹  Plimit R X K v (Pseql R X K v d F) 
                                             (ldeg_p R (Vr K v) X d p)"
apply (frule Vr_ring[of v], frule PolynRg.is_Ring,
       frule Ring.ring_is_ag[of "R"])
apply (frule Plimit_deg[of v R X F "Suc d" p], assumption+)
apply (simp add:Pseql_def, simp add:pol_limit_def)
apply (rule conjI, rule allI)
 apply (rule PolynRg.ldeg_p_mem, assumption+, simp+)
 apply (rule allI)
 apply (rotate_tac -5, drule_tac x = N in spec, erule exE)
 apply (subgoal_tac "∀m > M. P_mod R (Vr K v) X (vp K v (Vr K v) (an N))
              (ldeg_p R (Vr K v) X d (F m) ±R -aR (ldeg_p R (Vr K v) X d p))",
        blast)
 apply (rule allI, rule impI)
 apply (rotate_tac -2, 
        frule_tac x = m in spec,
        thin_tac "∀m. M < m ⟶
            P_mod R (Vr K v) X (vp K v (Vr K v) (an N)) ( F m ±R -aR p)",
        simp)
 apply (subst v_ldeg_p_mOp[of v R X _ d], assumption+)
 apply (subst v_ldeg_p_pOp[of v R X _ "-aR p"], assumption+)
 apply (simp, rule aGroup.ag_mOp_closed, assumption, simp, simp)
 apply (frule PolynRg.deg_minus_eq1 [THEN sym, of "R" "Vr K v" "X" "p"], 
        assumption+)
 apply simp 
apply (rule_tac p = "F m ±R -aR p" and N = N in PCauchy_lTr[of  "v"  
       "R" "X" _ "d" ], assumption+)
 apply (rule_tac x = "F m" in aGroup.ag_pOp_closed[of "R" _ "-aR p"], 
       assumption+)
 apply (simp, rule aGroup.ag_mOp_closed, assumption+)
apply (frule PolynRg.deg_minus_eq1 [of