Theory Valuation3

(**        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
  "lim⇘K vf b  (N. M. (n. M < n  
                ((f n) ±K(-aKb))  (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   (lim⇘K vf 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   (lim⇘K vf 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; lim⇘K vf b; lim⇘K vf 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; lim⇘K vf 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; lim⇘K vf 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; 
      lim⇘K vf 𝟬  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; 
      ¬ (lim⇘K vf 𝟬)  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; lim⇘K vf b; lim⇘K vg c
    lim⇘K 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  𝟬;
 lim⇘K vf b; lim⇘K vg c  lim⇘K 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;
      lim⇘K vf 𝟬; lim⇘K vg c  lim⇘K 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; lim⇘K vf b  lim⇘K 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  𝟬; lim⇘K vf b  
           lim⇘K 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
  "Cauchy⇘K vf  (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
  "Complete⇘vK  (f. (Cauchy⇘K vf)  
                           (b. b  (carrier K)  lim⇘K vf b))"

lemma (in Corps) has_limit_Cauchy:"valuation K v; j. f j  carrier K; 
      b  carrier K; lim⇘K vf b  Cauchy⇘K vf" 
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; Cauchy⇘K vf;
    ¬ (lim⇘K vf 𝟬)  
 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 vf 𝟬")
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; 
  Cauchy⇘K vf; ¬ (lim⇘K vf 𝟬)  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
  "Completion⇘v v'K K'  subfield K K' 
      Complete⇘v'K'  (x  carrier K. v x = v' x) 
      (x  carrier K'. (f. Cauchy⇘K vf  lim⇘K' 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'" "I⇘K⇙"], 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 "I⇘K aHom K K' 
     (xcarrier K. ycarrier K. I⇘K(x r y) = I⇘Kx rK'⇙ I⇘Ky) 
     I⇘K1r = 1rK'⇙")
apply (frule aHom_add[of "K" "K'" "I⇘K⇙" "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 "I⇘K aHom K K' 
     (xcarrier K. ycarrier K. I⇘K(x r y) = I⇘Kx rK'⇙ I⇘Ky) 
     I⇘K1r = 1rK'⇙")
apply (frule aHom_inv_inv[of "K" "K'" "I⇘K⇙" "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;  Completion⇘v 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'; 
 Completion⇘v 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'; Completion⇘v 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'; Completion⇘v 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';  Completion⇘v 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'" _ _ "I⇘K⇙"], 
                 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'" "I⇘K⇙"], assumption+, simp add:idmap_def)
done

lemma (in Corps) completion_vpr_sub:"Corps K'; valuation K v; valuation K' v';
      Completion⇘v 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'; Completion⇘v v'K K' 
   f. (Cauchy⇘K vf)  (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'; Complete⇘v'K'; j. f j  carrier K;  
      valuation K' v'; xcarrier K. v x = v' x; lim⇘K' v'f x  lim⇘K vf 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+, rul