Theory Padic_Field_Topology
theory Padic_Field_Topology
imports Padic_Fields
begin
section‹Topology of $p$-adic Fields›
text‹
In this section we develop some basic properties of the topology on the $p$-adics. Open and
closed sets are defined, convex subsets of the value group are characterized.
›
type_synonym padic_univ_poly = "nat ⇒ padic_number"
subsection‹$p$-adic Balls›
context padic_fields
begin
definition c_ball :: "int ⇒ padic_number ⇒ padic_number set" (‹B⇘_⇙[_]›) where
"c_ball n c = {x ∈ carrier Q⇩p. val (x ⊖ c) ≥ n}"
lemma c_ballI:
assumes "x ∈ carrier Q⇩p"
assumes " val (x ⊖ c) ≥ n"
shows "x ∈ c_ball n c"
using assms c_ball_def
by blast
lemma c_ballE:
assumes "x ∈ c_ball n c"
shows "x ∈ carrier Q⇩p"
" val (x ⊖ c) ≥ n"
using assms c_ball_def apply blast
using assms c_ball_def by blast
lemma c_ball_in_Qp:
"B⇘n⇙[c] ⊆ carrier Q⇩p"
unfolding c_ball_def
by blast
definition
q_ball :: "nat ⇒ int ⇒ int ⇒ padic_number ⇒ padic_number set" where
"q_ball n k m c = {x ∈ carrier Q⇩p. (ac n (x ⊖ c) = k ∧ (ord (x ⊖ c)) = m) }"
lemma q_ballI:
assumes "x ∈ carrier Q⇩p"
assumes "ac n (x ⊖ c) = k"
assumes "(ord (x ⊖ c)) = m"
shows "x ∈ q_ball n k m c"
using assms q_ball_def
by blast
lemma q_ballE:
assumes "x ∈ q_ball n k m c "
shows "x ∈ carrier Q⇩p"
using assms q_ball_def by blast
lemma q_ballE':
assumes "x ∈ q_ball n k m c "
shows "ac n (x ⊖ c) = k"
"(ord (x ⊖ c)) = m"
using assms q_ball_def apply blast
using assms q_ball_def by blast
lemma q_ball_in_Qp:
"q_ball n k m c ⊆ carrier Q⇩p"
unfolding q_ball_def by blast
lemma ac_ord_prop:
assumes "a ∈ nonzero Q⇩p"
assumes "b ∈ nonzero Q⇩p"
assumes "ord a = ord b"
assumes "ord a = n"
assumes "ac m a = ac m b"
assumes "m > 0"
shows "val (a ⊖ b) ≥ m + n "
proof-
have 0: "a = (𝔭[^]n) ⊗ ι (angular_component a)"
using angular_component_factors_x assms(1) assms(4) by blast
have 1: "b = (𝔭[^]n) ⊗ ι (angular_component b)"
using angular_component_factors_x assms(4) assms(2) assms(3)
by presburger
have 2: "a ⊖b = (𝔭[^]n) ⊗ ι (angular_component a) ⊖
(𝔭[^]n) ⊗ ι (angular_component b) "
using 0 1 by auto
have 3: "a ⊖b = (𝔭[^]n) ⊗( ι (angular_component a) ⊖ ι (angular_component b))"
proof-
have 30: "(𝔭[^]n) ∈ carrier Q⇩p"
by (simp add: p_intpow_closed(1))
have 31: " ι (angular_component a) ∈ carrier Q⇩p"
using Zp.nonzero_one_closed angular_component_closed assms(1) frac_closed local.inc_def
by presburger
have 32: " ι (angular_component b) ∈ carrier Q⇩p"
using Zp.nonzero_one_closed angular_component_closed assms(2) frac_closed local.inc_def
by presburger
show ?thesis
using 2 30 31 32 ring.ring_simprules(23)[of Q⇩p "(𝔭[^]n)"]
unfolding a_minus_def
by (metis Qp.domain_axioms cring.cring_simprules(25) cring.cring_simprules(29)
cring.cring_simprules(3) domain.axioms(1))
qed
have 4: "a ⊖b = (𝔭[^]n) ⊗( ι ((angular_component a) ⊖⇘Z⇩p⇙ (angular_component b)))"
using 3
by (simp add: angular_component_closed assms(1) assms(2) inc_of_diff)
have 5: "val_Zp ((angular_component a) ⊖⇘Z⇩p⇙ (angular_component b)) ≥ m "
proof-
have "((angular_component a) ⊖⇘Z⇩p⇙ (angular_component b)) m = 0"
using assms(5)
unfolding ac_def
using Q⇩p_def Qp.nonzero_memE(2) angular_component_closed assms(1) assms(2) residue_of_diff'
by auto
then show ?thesis
using Zp.minus_closed angular_component_closed assms(1) assms(2) ord_Zp_geq val_Zp_def val_ord_Zp
by auto
qed
have 6: "val (a ⊖ b) ≥ n + val ( ι (angular_component a) ⊖ ι (angular_component b))"
using 3 Qp.minus_closed angular_component_closed assms(1) assms(2) inc_closed
ord_p_pow_int p_intpow_closed(1) p_intpow_closed(2) val_mult val_ord
by simp
have 7: "n + val ( ι (angular_component a) ⊖ ι (angular_component b))
= n + val_Zp ((angular_component a) ⊖⇘Z⇩p⇙ (angular_component b))"
using Zp.minus_closed angular_component_closed assms(1) assms(2) inc_of_diff val_of_inc
by simp
have 8: "n + val_Zp ( (angular_component a) ⊖⇘Z⇩p⇙(angular_component b))
≥ n + m"
using 5
by (metis add_mono_thms_linordered_semiring(2) plus_eint_simps(1))
then have 9: "n + val ( ι (angular_component a) ⊖ ι (angular_component b))
≥ n + m"
using "7" by presburger
then show ?thesis
by (metis (no_types, opaque_lifting) "6" add.commute order_trans plus_eint_simps(1))
qed
lemma c_ball_q_ball:
assumes "b ∈ nonzero Q⇩p"
assumes "n > 0"
assumes "k = ac n b"
assumes "c ∈ carrier Q⇩p"
assumes "d ∈ q_ball n k m c"
shows "q_ball n k m c = c_ball (m + n) d"
proof
show "q_ball n k m c ⊆ B⇘m + int n⇙[d]"
proof
fix x
assume A0: "x ∈ q_ball n k m c"
show "x ∈ B⇘m + int n⇙[d]"
proof-
have A1: "(ac n (x ⊖ c) = k ∧ (ord (x ⊖ c)) = m)"
using A0 q_ball_def
by blast
have "val (x ⊖ d) ≥ m + n"
proof-
have A2: "(ac n (d ⊖ c) = k ∧ (ord (d ⊖ c)) = m)"
using assms(5) q_ball_def
by blast
have A3: "(x ⊖ c) ∈ nonzero Q⇩p"
proof-
have "k ≠0"
using A2 assms(1) assms(3) assms(5) ac_units[of b n]
by (metis One_nat_def Suc_le_eq assms(2) zero_not_in_residue_units)
then show ?thesis
by (smt (z3) A0 Qp.domain_axioms ac_def assms(4) cring.cring_simprules(4) domain.axioms(1)
mem_Collect_eq not_nonzero_Qp q_ball_def)
qed
have A4: "(d ⊖ c) ∈ nonzero Q⇩p"
proof-
have "k ≠0"
using A2 assms(1) assms(3) assms(5) ac_units[of b n]
by (metis One_nat_def Suc_le_eq assms(2) zero_not_in_residue_units)
then show ?thesis
by (metis (no_types, lifting) A2 Qp.domain_axioms ac_def assms(4) assms(5)
cring.cring_simprules(4) domain.axioms(1) mem_Collect_eq not_nonzero_Qp q_ball_def)
qed
then have " val ((x ⊖ c) ⊖(d ⊖ c)) ≥ n + m"
using ac_ord_prop[of "(x ⊖ c)" "(d ⊖ c)" m n ] A1 A2 assms A3
by simp
then show ?thesis
by (smt (z3) A0 Qp_diff_diff assms(4) assms(5) q_ballE)
qed
then show ?thesis
by (metis (no_types, lifting) A0 c_ball_def mem_Collect_eq q_ball_def)
qed
qed
show "B⇘m + int n⇙[d] ⊆ q_ball n k m c"
proof
fix x
assume A: "x ∈ B⇘m + int n⇙[d]"
show "x ∈ q_ball n k m c"
proof-
have A0: "val (x ⊖ d) ≥ m + n"
using A c_ball_def
by blast
have A1: "ord (d ⊖ c) = m"
using assms(5) q_ball_def
by blast
have A2: "ac n (d ⊖ c) = k"
using assms(5) q_ball_def
by blast
have A3: "(d ⊖ c) ≠ 𝟬"
using A2 assms
by (metis ac_def ac_units le_eq_less_or_eq le_neq_implies_less less_one nat_le_linear
padic_integers.zero_not_in_residue_units padic_integers_def prime zero_less_iff_neq_zero)
have A4: "val (d ⊖ c) =m"
by (simp add: A1 A3 val_def)
have A5: "val (x ⊖ d) > val (d ⊖ c)"
by (smt (z3) A0 A4 assms(2) eint_ord_code(4) eint_ord_simps(1) eint_ord_simps(2) of_nat_0_less_iff val_def)
have A6: "val ((x ⊖ d) ⊕ (d ⊖ c)) = m"
using A4 A0 A5
by (metis (mono_tags, opaque_lifting) A Qp.minus_closed assms(4) assms(5)
c_ballE(1) q_ballE val_ultrametric_noteq)
have A7: "val (x ⊖ c) = m"
proof-
have "(x ⊖ d) ⊕ (d ⊖ c) = ((x ⊖ d) ⊕ d) ⊖ c"
by (metis (no_types, lifting) A Qp.domain_axioms a_minus_def assms(4) assms(5)
c_ball_def cring.cring_simprules(3) cring.cring_simprules(4)
cring.cring_simprules(7) domain.axioms(1) mem_Collect_eq q_ball_def)
have "(x ⊖ d) ⊕ (d ⊖ c) = (x ⊕ (⊖ d ⊕ d)) ⊖ c"
by (metis (no_types, opaque_lifting) A Qp.add.l_cancel_one Qp.add.m_comm Qp.l_neg
Qp.minus_closed Qp.plus_diff_simp Qp.zero_closed assms(4) assms(5)
c_ballE(1) q_ballE)
then show ?thesis
by (metis (no_types, lifting) A A6 Qp.domain_axioms assms(5) c_ball_def
cring.cring_simprules(16) cring.cring_simprules(9) domain.axioms(1)
mem_Collect_eq q_ball_def)
qed
have A8: "ac n (x ⊖ c) = ac n (d ⊖ c)"
proof-
have A80: "(x ⊖ c) ∈ nonzero Q⇩p"
by (metis (no_types, lifting) A A4 A5 A7 Qp.domain_axioms
assms(4) cring.cring_simprules(4) domain.axioms(1)
mem_Collect_eq c_ball_def val_nonzero)
have A81: "(d ⊖ c) ∈ nonzero Q⇩p"
by (metis (no_types, lifting) A3 Qp.domain_axioms assms(4) assms(5)
cring.cring_simprules(4) domain.axioms(1) mem_Collect_eq not_nonzero_Qp q_ball_def)
have A82: "n + m= val (x ⊖ c) + n"
by (simp add: A7)
show ?thesis
using A0 A4 A7 ac_val[of "(x ⊖ c)" "(d ⊖ c)" n] A A80 A81 Qp_diff_diff assms(4) assms(5) c_ballE(1) q_ballE
by auto
qed
show ?thesis using A8 A3 A7 A2 q_ball_def[of n k m c] q_ballI[of x n c k m]
by (metis (no_types, lifting) A A4 A5 Qp.minus_closed assms(4) c_ballE(1) eint.inject val_nonzero val_ord)
qed
qed
qed
definition is_ball :: "padic_number set ⇒ bool" where
"is_ball B = (∃(m::int). ∃ c ∈ carrier Q⇩p. (B = B⇘m⇙[c]))"
lemma is_ball_imp_in_Qp:
assumes "is_ball B"
shows "B ⊆ carrier Q⇩p"
unfolding is_ball_def
using assms c_ball_in_Qp is_ball_def
by auto
lemma c_ball_centers:
assumes "is_ball B"
assumes "B = B⇘n⇙[c]"
assumes "d ∈ B"
assumes "c ∈ carrier Q⇩p"
shows "B = B⇘n⇙[d]"
proof
show "B ⊆ B⇘n⇙[d]"
proof
fix x
assume A0: "x ∈ B"
have "val (x ⊖ d) ≥ n"
proof-
have A00: "val (x ⊖ c) ≥ n"
using A0 assms(2) c_ballE(2) by blast
have A01: "val (d ⊖ c) ≥ n"
using assms(2) assms(3) c_ballE(2) by blast
then show ?thesis
using Qp_isosceles[of x c d "n"] assms A0 A00 c_ballE(1)
by blast
qed
then show "x ∈ B⇘n⇙[d]"
using A0 assms(1) c_ballI is_ball_imp_in_Qp
by blast
qed
show "B⇘n⇙[d] ⊆ B"
proof
fix x
assume "x ∈ B⇘n⇙[d]"
show "x ∈ B"
using Qp_isosceles[of x d c "n"]
assms
unfolding c_ball_def
by (metis (no_types, lifting) Qp.domain_axioms Qp_isosceles ‹x ∈ B⇘n⇙[d]›
a_minus_def assms(2) c_ballE(2) c_ballI cring.cring_simprules(17) domain.axioms(1)
c_ballE(1))
qed
qed
lemma c_ball_center_in:
assumes "is_ball B"
assumes "B = B⇘n⇙[c]"
assumes "c ∈ carrier Q⇩p"
shows "c ∈ B"
using assms unfolding c_ball_def
by (metis (no_types, lifting) Qp.r_right_minus_eq assms(2) c_ballI eint_ord_code(3) local.val_zero)
text ‹Every point a has a point b of distance exactly n away from it.›
lemma dist_nonempty:
assumes "a ∈ carrier Q⇩p"
shows "∃b ∈ carrier Q⇩p. val (b ⊖ a) = eint n"
proof-
obtain b where b_def: "b = (𝔭 [^] n) ⊕ a"
by simp
have "val (b ⊖a) = n"
using b_def assms
by (metis (no_types, lifting) Qp.domain_axioms a_minus_def cring.cring_simprules(16)
cring.cring_simprules(17) cring.cring_simprules(3) cring.cring_simprules(7)
domain.axioms(1) ord_p_pow_int p_intpow_closed(1) p_intpow_closed(2) val_ord)
then show ?thesis
by (metis Qp.domain_axioms assms b_def cring.cring_simprules(1) domain.axioms(1) p_intpow_closed(1))
qed
lemma dist_nonempty':
assumes "a ∈ carrier Q⇩p"
shows "∃b ∈ carrier Q⇩p. val (b ⊖ a) = α"
proof(cases "α = ∞")
case True
then have "val (a ⊖ a) = α"
using assms
by (metis Qp.r_right_minus_eq local.val_zero)
then show ?thesis
using assms
by blast
next
case False
then obtain n where n_def: "eint n = α"
by blast
then show ?thesis
using assms dist_nonempty[of a n]
by blast
qed
lemma ball_rad_0:
assumes "is_ball B"
assumes "B⇘m⇙[c] ⊆ B⇘n⇙[c]"
assumes "c ∈ carrier Q⇩p"
shows "n ≤ m"
proof-
obtain b where b_def: "b ∈ carrier Q⇩p ∧ val (b ⊖c) = m"
by (meson assms(3) dist_nonempty)
then have "b ∈ B⇘n⇙[c]"
using assms c_ballI
by auto
then have "m ≥ n"
using Q⇩p_def Zp_def b_def c_ballE(2) padic_integers_axioms
by force
then show ?thesis
by (simp )
qed
lemma ball_rad:
assumes "is_ball B"
assumes "B = B⇘n⇙[c]"
assumes "B = B⇘m⇙[c]"
assumes "c ∈ carrier Q⇩p"
shows "n = m"
proof-
have 0: "n ≥m"
using assms ball_rad_0
by (metis order_refl)
have 1: "m ≥n"
using assms ball_rad_0
by (metis order_refl)
show ?thesis
using 0 1
by auto
qed
definition radius :: "padic_number set ⇒ int" (‹rad›) where
"radius B = (SOME n. (∃c ∈ carrier Q⇩p . B = B⇘n⇙[c]))"
lemma radius_of_ball:
assumes "is_ball B"
assumes "c ∈ B"
shows "B = B⇘rad B⇙[c]"
proof-
obtain d m where d_m_def: "d ∈ carrier Q⇩p ∧ B = B⇘m⇙[d]"
using assms(1) is_ball_def
by blast
then have "B = B⇘m⇙[c]"
using assms(1) assms(2) c_ball_centers by blast
then have "rad B = m"
proof-
have "∃n. (∃c ∈ carrier Q⇩p . B = B⇘n⇙[c])"
using d_m_def by blast
then have "(∃c ∈ carrier Q⇩p . B = B⇘rad B⇙[c])"
using radius_def[of B]
by (smt (z3) someI_ex)
then show ?thesis
using radius_def ball_rad[of B m ]
by (metis (mono_tags, lifting) ‹B = B⇘m⇙[c]› assms(1) assms(2) c_ballE(1) c_ball_centers)
qed
then show ?thesis
using ‹B = B⇘m⇙[c]› by blast
qed
lemma ball_rad':
assumes "is_ball B"
assumes "B = B⇘n⇙[c]"
assumes "B = B⇘m⇙[d]"
assumes "c ∈ carrier Q⇩p"
assumes "d ∈ carrier Q⇩p"
shows "n = m"
by (metis assms(1) assms(2) assms(3) assms(4) assms(5) ball_rad c_ball_center_in c_ball_centers)
lemma nested_balls:
assumes "is_ball B"
assumes "B = B⇘n⇙[c]"
assumes "B' = B⇘m⇙[c]"
assumes "c ∈ carrier Q⇩p"
assumes "d ∈ carrier Q⇩p"
shows "n ≥m ⟷ B ⊆ B'"
proof
show "m ≤ n ⟹ B ⊆ B'"
proof
assume A0: "m ≤n"
then have A0': "m ≤ n"
by (simp add: )
fix x
assume A1: "x ∈ B"
show "x ∈ B'"
using assms c_ballI[of x m c] A0' A1 c_ballE(2)[of x n c] c_ball_in_Qp
by (meson c_ballE(1) dual_order.trans eint_ord_simps(1))
qed
show "B ⊆ B' ⟹ m ≤ n"
using assms(1) assms(2) assms(3) assms(4) ball_rad_0
by blast
qed
lemma nested_balls':
assumes "is_ball B"
assumes "is_ball B'"
assumes "B ∩ B' ≠ {}"
shows "B ⊆ B' ∨ B' ⊆ B"
proof-
obtain b where b_def: "b ∈ B ∩ B'"
using assms(3) by blast
show "B ⊆ B' ∨ B' ⊆ B"
proof-
have "¬ B ⊆ B' ⟹ B' ⊆ B"
proof-
assume A: "¬ B ⊆ B' "
have 0: "B = B⇘rad B⇙[b]"
using assms(1) b_def radius_of_ball by auto
have 1: "B' = B⇘rad B'⇙[b]"
using assms(2) b_def radius_of_ball by auto
show "B' ⊆ B" using 0 1 A nested_balls
by (smt (z3) IntD2 Q⇩p_def Zp_def assms(1) assms(2) b_def
c_ballE(1) padic_integers_axioms)
qed
then show ?thesis by blast
qed
qed
definition is_bounded:: "padic_number set ⇒ bool" where
"is_bounded S = (∃n. ∃c ∈ carrier Q⇩p. S ⊆ B⇘n⇙[c] )"
lemma empty_is_bounded:
"is_bounded {}"
unfolding is_bounded_def
by blast
subsection‹$p$-adic Open Sets›
definition is_open:: "padic_number set ⇒ bool" where
"is_open U ≡ (U ⊆ carrier Q⇩p) ∧ (∀c ∈ U. ∃n. B⇘n⇙[c]⊆ U )"
lemma is_openI:
assumes "U ⊆carrier Q⇩p"
assumes "⋀c. c ∈ U ⟹ ∃n. B⇘n⇙[c]⊆ U"
shows "is_open U"
by (simp add: assms(1) assms(2) is_open_def)
lemma ball_is_open:
assumes "is_ball B"
shows "is_open B"
by (metis (mono_tags, lifting) assms is_ball_imp_in_Qp is_open_def radius_of_ball subset_iff)
lemma is_open_imp_in_Qp:
assumes "is_open U"
shows "U ⊆ carrier Q⇩p"
using assms unfolding is_open_def
by linarith
lemma is_open_imp_in_Qp':
assumes "is_open U"
assumes " x ∈ U"
shows "x ∈ carrier Q⇩p"
using assms(1) assms(2) is_open_imp_in_Qp
by blast
text‹
Owing to the total disconnectedness of the $p$-adic field, every open set can be decomposed
into a disjoint union of balls which are maximal with respect to containment in that set.
This unique decomposition is occasionally useful.
›
definition is_max_ball_of ::"padic_number set ⇒ padic_number set ⇒ bool" where
"is_max_ball_of U B ≡ (is_ball B) ∧ (B ⊆ U) ∧ (∀B'. ((is_ball B') ∧ (B' ⊆ U) ∧ B ⊆ B') ⟶ B' ⊆ B)"
lemma is_max_ball_ofI:
assumes "U ⊆ carrier Q⇩p"
assumes "(B⇘m⇙[c]) ⊆ U"
assumes "c ∈ carrier Q⇩p"
assumes "∀m'. m' < m ⟶ ¬ B⇘m'⇙[c] ⊆ U"
shows "is_max_ball_of U (B⇘m⇙[c])"
proof(rule ccontr)
assume " ¬ is_max_ball_of U B⇘m⇙[c]"
then have "¬ (∀B'. is_ball B' ∧ B' ⊆ U ∧ B⇘m⇙[c] ⊆ B'⟶ B' ⊆ B⇘m⇙[c])"
using assms is_max_ball_of_def[of U "B⇘m⇙[c]" ]
unfolding is_ball_def
by blast
then obtain B' where B'_def: "is_ball B' ∧ B' ⊆ U ∧ B⇘m⇙[c] ⊆ B' ∧ ¬ B' ⊆ B⇘m⇙[c]"
by auto
obtain n where n_def: "B' = B⇘n⇙[c]"
by (meson B'_def assms(3) c_ball_center_in is_ball_def radius_of_ball subset_iff)
then show False
using assms
by (smt (z3) B'_def Q⇩p_def Zp_def ball_rad_0 padic_integers_axioms)
qed
lemma int_prop:
fixes P:: "int ⇒ bool"
assumes "P n"
assumes "∀m. m ≤N ⟶ ¬ P m"
shows "∃n. P n ∧ (∀n'. P n'⟶ n' ≥n)"
proof-
have "n > N"
by (meson assms(1) assms(2) not_less)
obtain k::nat where k_def: "k = nat (n - N)"
by blast
obtain l::nat where l_def: "l = (LEAST M. P (N + int M))"
by simp
have 0: " P (N + int l)"
by (metis (full_types) LeastI ‹N < n› assms(1) l_def zless_iff_Suc_zadd)
have 1: "l > 0"
using "0" assms(2) of_nat_0_less_iff by fastforce
have 2: "⋀M. M < l ⟶ ¬ P (N + M)"
by (metis Least_le l_def less_le_trans nat_less_le)
obtain n where n_def: "n = (N + int l)"
by simp
have "P n ∧ (∀n'. P n'⟶ n' ≥ n)"
proof-
have "P n"
by (simp add: "0" n_def)
have "(∀n'. P n'⟶ n' ≥ n)"
proof
fix n'
show "P n' ⟶ n ≤ n'"
proof
assume "P n'"
show "n ≤n'"
proof(rule ccontr)
assume " ¬ n ≤ n'"
then have C: "n' < n"
by auto
show "False"
proof(cases "n' ≥ N")
case True
obtain M where M_def: "nat (n' - N) = M"
by simp
then have M0: "n' = N + int M "
using True by linarith
have M1: "M < l"
using n_def C M0
by linarith
then show ?thesis using 2 M_def M0 M1
using ‹P n'› by auto
next
case False
then show ?thesis using assms
using ‹P n'› by auto
qed
qed
qed
qed
then show ?thesis
using ‹P n› by blast
qed
then show ?thesis by blast
qed
lemma open_max_ball:
assumes "is_open U"
assumes "U ≠ carrier Q⇩p"
assumes "c ∈ U"
shows "∃B. is_max_ball_of U B ∧ c ∈ B"
proof-
obtain B where B_def: "is_ball B ∧ B ⊆ U ∧ c ∈ B"
by (meson assms(1) assms(3) c_ball_center_in is_ball_def is_open_imp_in_Qp' is_open_def padic_integers_axioms)
show P: "∃B. is_max_ball_of U B ∧ c ∈ B"
proof(rule ccontr)
assume C: "∄B. is_max_ball_of U B ∧ c ∈ B"
show False
proof-
have C': "∀B. c ∈ B ⟶ ¬ is_max_ball_of U B "
using C
by auto
have C'': "∀N. ∃m <N. B⇘m⇙[c] ⊆ U "
proof
fix N
show "∃m<N. B⇘m⇙[c] ⊆ U"
proof(rule ccontr)
assume A: "¬ (∃m<N. B⇘m⇙[c] ⊆ U)"
obtain P where P_def: "P = (λ n. ∃m<n. B⇘m⇙[c] ⊆ U)"
by simp
have A0: "∃n. P n"
by (metis B_def P_def gt_ex radius_of_ball)
have A1: "∀m. m ≤N ⟶ ¬ P m"
using A P_def by auto
have A2: "∃n. P n ∧ (∀n'. P n'⟶ n' ≥n)"
using A0 A1 int_prop
by auto
obtain n where n_def: " P n ∧ (∀n'. P n'⟶ n' ≥n)"
using A2 by blast
have " B⇘n⇙[c] ⊆ U"
by (smt (z3) B_def P_def c_ball_def is_ball_def mem_Collect_eq n_def nested_balls order_trans)
obtain m where m_def: "m < n ∧B⇘m⇙[c] ⊆ U"
using P_def n_def by blast
have "m = n-1"
proof-
have "P (m +1)"
using P_def m_def
by auto
then have "m + 1 ≥ n"
using n_def by blast
then show ?thesis using m_def by auto
qed
have "∀m'. m' < m ⟶ ¬ B⇘m'⇙[c] ⊆ U"
proof
fix m'
show " m' < m ⟶ ¬ B⇘m'⇙[c] ⊆ U"
proof
assume "m' < m"
show "¬ B⇘m'⇙[c] ⊆ U"
proof
assume "B⇘m'⇙[c] ⊆ U"
then have "P (m' + 1)"
using P_def by auto
have "m'+ 1 < n"
using ‹m = n - 1› ‹m' < m› by linarith
then show False
using n_def ‹P (m' + 1)› by auto
qed
qed
qed
then have "is_max_ball_of U B⇘m⇙[c]"
using is_max_ball_ofI assms(1) assms(3) is_open_imp_in_Qp is_open_imp_in_Qp' m_def
by presburger
then show False
using C assms(1) assms(3) c_ball_center_in is_open_imp_in_Qp'
is_max_ball_of_def padic_integers_axioms
by blast
qed
qed
have "U = carrier Q⇩p"
proof
show "carrier Q⇩p ⊆ U"
proof
fix x
assume "x ∈ carrier Q⇩p"
show "x ∈ U"
proof(cases "x = c")
case True
then show ?thesis using assms by auto
next
case False
obtain m where m_def: "eint m = val(x ⊖ c)"
using False
by (metis (no_types, opaque_lifting) Qp_diff_diff Qp.domain_axioms ‹x ∈ carrier Q⇩p› a_minus_def
assms(1) assms(3) cring.cring_simprules(16) cring.cring_simprules(17)
cring.cring_simprules(4) domain.axioms(1) is_open_imp_in_Qp' val_def val_minus)
obtain m' where m'_def: "m' < m ∧ B⇘m'⇙[c] ⊆ U "
using C''
by blast
have "val (x ⊖ c) ≥ m'"
by (metis eint_ord_simps(1) less_imp_le m'_def m_def)
then have "x ∈ B⇘m'⇙[c]"
using ‹x ∈ carrier Q⇩p› c_ballI by blast
then show "x ∈ U"
using m'_def by blast
qed
qed
show "U ⊆ carrier Q⇩p "
using assms
by (simp add: is_open_imp_in_Qp)
qed
then show False using assms by auto
qed
qed
qed
definition interior where
"interior U = {a. ∃B. is_open B ∧ B ⊆ U ∧ a ∈ B}"
lemma interior_subset:
assumes "U ⊆ carrier Q⇩p"
shows "interior U ⊆ U"
proof
fix x
assume "x ∈ interior U"
show "x ∈ U"
proof-
obtain B where B_def: "is_open B ∧ B ⊆ U ∧ x ∈ B"
using ‹x ∈ interior U› interior_def
by auto
then show "x ∈ U"
by blast
qed
qed
lemma interior_open:
assumes "U ⊆ carrier Q⇩p"
shows "is_open (interior U)"
proof(rule is_openI)
show "interior U ⊆ carrier Q⇩p"
using assms interior_subset by blast
show "⋀c. c ∈ interior U ⟹ ∃n. B⇘n⇙[c] ⊆ interior U"
proof-
fix c
assume "c ∈ interior U"
show "∃n. B⇘n⇙[c] ⊆ interior U"
proof-
obtain B where B_def: "is_open B ∧ B ⊆ U ∧ c ∈ B"
using ‹c ∈ interior U› interior_def padic_integers_axioms
by auto
then show ?thesis
proof -
obtain ii :: "((nat ⇒ int) × (nat ⇒ int)) set ⇒ ((nat ⇒ int) × (nat ⇒ int)) set set ⇒ int"
where
"B⇘ii c B⇙[c] ⊆ B"
by (meson B_def is_open_def)
then show ?thesis
using B_def interior_def padic_integers_axioms by auto
qed
qed
qed
qed
lemma interiorI:
assumes "W ⊆ U"
assumes "is_open W"
shows "W ⊆ interior U"
using assms(1) assms(2) interior_def by blast
lemma max_ball_interior:
assumes "U ⊆ carrier Q⇩p"
assumes "is_max_ball_of (interior U) B"
shows "is_max_ball_of U B"
proof(rule ccontr)
assume C: " ¬ is_max_ball_of U B"
then obtain B' where B'_def: "is_ball B' ∧ B' ⊆ U ∧ B ⊆ B' ∧ B ≠ B'"
by (metis (no_types, lifting) assms(1) assms(2) dual_order.trans
interior_subset is_max_ball_of_def )
then have "B' ⊆ interior U"
using interior_def padic_integers_axioms ball_is_open
by auto
then show False using assms B'_def is_max_ball_of_def[of "interior U" "B"]
by blast
qed
lemma ball_in_max_ball:
assumes "U ⊆ carrier Q⇩p"
assumes "U ≠ carrier Q⇩p"
assumes "c ∈ U"
assumes "∃B. B ⊆ U ∧ is_ball B ∧ c ∈ B"
shows "∃B'. is_max_ball_of U B' ∧ c ∈ B'"
proof-
obtain B where " B ⊆ U ∧ is_ball B ∧ c ∈ B"
using assms(4)
by blast
then have 0: "B ⊆ interior U"
using ball_is_open interior_def by blast
have 1: "c ∈ interior U"
using "0" ‹B ⊆ U ∧ is_ball B ∧ c ∈ B› by blast
then have "∃B'. is_max_ball_of (interior U) B' ∧ c ∈ B'"
using open_max_ball[of "interior U" c] assms(1) assms(2) interior_open interior_subset
by blast
then show ?thesis
using assms(1) max_ball_interior
by blast
qed
lemma ball_in_max_ball':
assumes "U ⊆ carrier Q⇩p"
assumes "U ≠ carrier Q⇩p"
assumes "B ⊆ U ∧ is_ball B"
shows "∃B'. is_max_ball_of U B' ∧ B ⊆ B'"
proof-
obtain c where c_def: "c ∈ B"
by (metis assms(3) c_ball_center_in is_ball_def)
obtain B' where B'_def: " is_max_ball_of U B' ∧ c ∈ B'"
using assms ball_in_max_ball[of U c] c_def
by blast
then show ?thesis
by (meson assms(3) c_def disjoint_iff_not_equal nested_balls'
is_max_ball_of_def padic_integers_axioms)
qed
lemma max_balls_disjoint:
assumes "U ⊆ carrier Q⇩p"
assumes "is_max_ball_of U B"
assumes "is_max_ball_of U B'"
assumes "B ≠B'"
shows "B ∩ B' = {}"
by (meson assms(2) assms(3) assms(4) nested_balls' is_max_ball_of_def
padic_integers_axioms subset_antisym)
definition max_balls :: "padic_number set ⇒ padic_number set set" where
"max_balls U = {B. is_max_ball_of U B }"
lemma max_balls_interior:
assumes "U ⊆ carrier Q⇩p"
assumes "U ≠ carrier Q⇩p"
shows "interior U = {x ∈ carrier Q⇩p. (∃B ∈ (max_balls U). x ∈ B)}"
proof
show "interior U ⊆ {x ∈ carrier Q⇩p. ∃B∈max_balls U. x ∈ B}"
proof
fix x
assume A: " x ∈ interior U"
show "x ∈ {x ∈ carrier Q⇩p. ∃B∈max_balls U. x ∈ B}"
by (metis (mono_tags, lifting) A assms(1) assms(2) interior_open
interior_subset is_open_imp_in_Qp' max_ball_interior max_balls_def
mem_Collect_eq open_max_ball subset_antisym)
qed
show "{x ∈ carrier Q⇩p. ∃B∈max_balls U. x ∈ B} ⊆ interior U"
proof
fix x
assume A: " x ∈ {x ∈ carrier Q⇩p. ∃B∈max_balls U. x ∈ B} "
show "x ∈ interior U"
proof-
obtain B where B_def: "B∈max_balls U ∧ x ∈ B"
using A by blast
then have "B ⊆ interior U"
by (metis (no_types, lifting) interior_def is_max_ball_of_def mem_Collect_eq
ball_is_open max_balls_def subsetI)
then show ?thesis
using B_def by blast
qed
qed
qed
lemma max_balls_interior':
assumes "U ⊆ carrier Q⇩p"
assumes "U ≠ carrier Q⇩p"
assumes "B ∈ max_balls U"
shows "B ⊆ interior U"
using assms(1) assms(2) assms(3) is_max_ball_of_def max_balls_interior
max_balls_def padic_integers_axioms
by auto
lemma max_balls_interior'':
assumes "U ⊆ carrier Q⇩p"
assumes "U ≠ carrier Q⇩p"
assumes "a ∈ interior U"
shows "∃B ∈ max_balls U. a ∈ B"
using assms(1) assms(2) assms(3) max_balls_interior
by blast
lemma open_interior:
assumes "is_open U"
shows "interior U = U"
unfolding interior_def using assms
by blast
lemma interior_idempotent:
assumes "U ⊆ carrier Q⇩p"
shows "interior (interior U) = interior U"
using assms interior_open[of U] open_interior[of "interior U"]
by auto
subsection‹Convex Subsets of the Value Group›
text‹
The content of this section will be useful for defining and reasoning about $p$-adic cells in the
proof of Macintyre's theorem. It is proved that every convex set in the extended integers is
either an open ray, a closed ray, a closed interval, or a left-closed interval.›
definition is_convex :: "eint set ⇒ bool" where
"is_convex A = (∀ x ∈ A. ∀y ∈ A. ∀c. x ≤ c ∧ c ≤ y ⟶ c ∈ A)"
lemma is_convexI:
assumes "⋀x y c. x ∈ A ⟹ y ∈ A ⟹ x ≤ c ∧ c ≤y ⟹ c ∈ A"
shows "is_convex A"
unfolding is_convex_def
using assms
by blast
lemma is_convexE:
assumes "is_convex A"
assumes "x ∈ A"
assumes "y ∈ A"
assumes "x ≤ a"
assumes "a ≤ y"
shows "a ∈ A"
using assms is_convex_def
by blast
lemma empty_convex:
"is_convex {}"
apply(rule is_convexI)
by blast
lemma UNIV_convex:
"is_convex UNIV"
apply(rule is_convexI)
by blast
definition closed_interval (‹I[_ _]›) where
"closed_interval α β = {a . α ≤ a ∧ a ≤ β}"
lemma closed_interval_is_convex:
assumes "A = closed_interval α β"
shows "is_convex A"
apply(rule is_convexI)
using assms unfolding closed_interval_def
by auto
lemma empty_closed_interval:
"{} = closed_interval ∞ (eint 1)"
unfolding closed_interval_def
by auto
definition left_closed_interval where
"left_closed_interval α β = {a . α ≤ a ∧ a < β}"
lemma left_closed_interval_is_convex:
assumes "A = left_closed_interval α β"
shows "is_convex A"
apply(rule is_convexI)
using assms unfolding left_closed_interval_def
using leD order.trans by auto
definition closed_ray where
"closed_ray α β = {a . a ≤ β }"
lemma closed_ray_is_convex:
assumes "A = closed_ray α β"
shows "is_convex A"
apply(rule is_convexI)
using assms unfolding closed_ray_def
by auto
lemma UNIV_closed_ray:
"(UNIV::eint set)= closed_ray α ∞"
unfolding closed_ray_def
by simp
definition open_ray :: "eint ⇒ eint ⇒ eint set" where
"open_ray α β = {a . a < β }"
lemma open_ray_is_convex:
assumes "A = open_ray α β"
shows "is_convex A"
apply(rule is_convexI)
using assms unfolding open_ray_def
using leD by auto
lemma open_rayE:
assumes "a < β"
shows "a ∈ open_ray α β"
unfolding open_ray_def using assms
by blast
lemma value_group_is_open_ray:
"UNIV - {∞} = open_ray α ∞"
proof
show "UNIV - {∞} ⊆ open_ray α ∞"
using open_rayE[of _ α "∞"]
by (simp add: open_rayE subset_eq)
show "open_ray α ∞ ⊆ UNIV - {∞}"
unfolding open_ray_def
by blast
qed
text‹
This is a predicate which identifies a certain kind of set-valued function on the extended
integers. Convex conditions will be important in the definition of $p$-adic cells later, and
it will be proved that every convex set is induced by a convex condition.›
definition is_convex_condition :: "(eint ⇒ eint ⇒ eint set) ⇒ bool"
where "is_convex_condition I ≡
I = closed_interval ∨ I = left_closed_interval ∨ I = closed_ray ∨ I = open_ray"
lemma convex_condition_imp_convex:
assumes "is_convex_condition I"
shows "is_convex (I α β)"
using assms
unfolding is_convex_condition_def
by (meson closed_interval_is_convex closed_ray_is_convex left_closed_interval_is_convex open_ray_is_convex)
lemma bounded_order:
assumes "(a::eint) < ∞"
assumes "b ≤ a"
obtains k::nat where "a = b + k"
proof-
obtain m::int where m_def: "a = m"
using assms(1) less_infinityE by blast
obtain n::int where n_def: "b = n"
using assms(2) eint_ile m_def by blast
have 0: "a - b = eint (m - n)"
by (simp add: m_def n_def)
then have "a = b + nat (m - n)"
using assms m_def n_def
by simp
thus ?thesis
using that by blast
qed
text‹Every convex set is given by a convex condition›
lemma convex_imp_convex_condition:
assumes "is_convex A"
shows "∃ I α β. is_convex_condition I ∧ A = (I α β)"
proof(cases "∃ a ∈ A. ∀ b ∈ A. a ≤ b")
case True
then obtain α where alpha_def: "α ∈ A ∧ (∀ b ∈ A. α ≤ b)"
by blast
then show ?thesis
proof(cases "∃ a ∈ A. ∀ b ∈ A. b ≤ a")
case True
then obtain β where beta_def: "β ∈ A ∧ (∀ b ∈ A. b ≤ β)"
by blast
have "A = closed_interval α β"
unfolding closed_interval_def
using alpha_def beta_def assms is_convexE[of A α β]
by blast
then show ?thesis
using is_convex_condition_def
by blast
next
case False
have F0: "∀a. α ≤ a ∧ a < ∞ ⟶ a ∈ A"
proof(rule ccontr)
assume A: "¬ (∀a. a ≥ α ∧ a < ∞ ⟶ a ∈ A)"
then obtain a where a_def: " α ≤ a ∧ a < ∞ ∧ a ∉ A"
by blast
obtain n where n_def: "α = eint n"
using False alpha_def by force
obtain m where m_def: "a = eint m"
using a_def less_infinityE by blast
have "∀k::nat. ∃c. (α + eint (int k)) < c ∧ c ∈ A"
proof fix k
show "∃c>α + eint (int k). c ∈ A"
apply(induction k)
using False alpha_def le_less_linear zero_eint_def apply fastforce
proof- fix k
assume IH: "∃c>α + eint (int k). c ∈ A"
then obtain c where c_def: "c>α + eint (int k) ∧ c ∈ A"
by blast
then obtain c' where c'_def: "c' ∈ A ∧ c < c'"
using False
by (meson le_less_linear)
then have "(α + eint (int (Suc k))) ≤ c'"
proof-
have 0: "eint (int (Suc k)) = eint (int k) + eint 1"
by simp
have "α + eint (int k) ≤c'"
by (meson c'_def c_def le_less le_less_trans)
then have 1: "(α + eint (int k)) < c'"
using c'_def c_def le_less_trans
by auto
have 2: "α + eint (int k) + eint 1 = α + eint (int (Suc k))"
using 0
by (simp add: n_def)
then show "(α + eint (int (Suc k))) ≤ c'"
by (metis "1" ileI1 one_eint_def)
qed
then show "∃c>α + eint (int (Suc k)). c ∈ A"
using False c'_def not_less by fastforce
qed
qed
obtain k where k_def: "k = a - α"
using a_def n_def
by blast
hence "k ≥ 0"
using a_def n_def
by (metis alpha_def eint_minus_le le_less)
hence 0: "∃n::nat. k = n"
using a_def n_def k_def
by (metis eint.distinct(2) eint_0_iff(2) eint_add_cancel_fact eint_ord_simps(1) fromeint.cases m_def nonneg_int_cases plus_eint_simps(3))
have 1: "a = α + k"
using k_def a_def n_def
by simp
then obtain c where "c ∈ A ∧ a < c"
by (metis "0" ‹∀k. ∃c>α + eint (int k). c ∈ A› the_eint.simps)
then have "a ∈ A"
using is_convexE[of A α a c] a_def alpha_def assms is_convexE
by (meson linear not_less)
then show False
using a_def by blast
qed
have "A = closed_interval α ∞ ∨ A = left_closed_interval α ∞"
apply(cases "∞ ∈ A")
using False eint_ord_code(3) apply blast
proof-
assume A0: "∞ ∉ A "
have "A = left_closed_interval α ∞"
proof
show "A ⊆ left_closed_interval α ∞"
unfolding left_closed_interval_def
using alpha_def A0
by (metis (mono_tags, lifting) False eint_ord_code(3) le_less_linear less_le_trans mem_Collect_eq subsetI)
show "left_closed_interval α ∞ ⊆ A"
unfolding left_closed_interval_def
using alpha_def A0 F0
by blast
qed
then show ?thesis
by blast
qed
then show ?thesis
unfolding is_convex_condition_def
by blast
qed
next
case False
show ?thesis apply(cases "A = {}")
using empty_closed_interval is_convex_condition_def apply blast
proof-
assume A0: "A ≠ {}"
have "A ≠ {∞}"
using False
by blast
then obtain α where alpha_def: "α ∈ A ∧ α ≠∞"
using A0
by fastforce
have A1: "⋀k::nat. ∃ b ∈ A. b + eint (int k) ≤ α"
proof- fix k
show " ∃ b ∈ A. b + eint (int k) ≤ α"
proof(induction k)
case 0
then have "α + eint (int 0) = α"
by (simp add: zero_eint_def)
then show ?case
using alpha_def by auto
next
case (Suc k) fix k
assume IH: "∃b∈A. α ≥ b + eint (int k)"
show "∃b∈A. α ≥ b + eint (int (Suc k))"
proof-
obtain b where b_def: "b ∈ A ∧ α ≥ b + eint (int k)"
using IH by blast
then obtain c where c_def: "c ∈ A ∧ c < b"
using False le_less_linear by blast
have 0: "(c + eint (int (Suc k))) < (b + eint (int (Suc k)))"
using c_def
by simp
have 1: "b + eint (int (Suc k)) = (b + eint (int k)) + eint 1"
by simp
then show ?thesis
by (metis "0" b_def c_def eSuc_ile_mono ileI1 le_less one_eint_def)
qed
qed
qed
show ?thesis
proof(cases "∃ a ∈ A. ∀ b ∈ A. b ≤ a")
case True
then obtain β where beta_def: "β ∈ A ∧ (∀ b ∈ A. b ≤ β)"
by blast
have "A = closed_ray α β"
unfolding closed_ray_def
proof
show "A ⊆ {a. β ≥ a}"
using assms beta_def
by blast
show "{a. β ≥ a} ⊆ A"
proof fix x assume "x ∈ {a. β ≥ a}"
then have 0: "β ≥ x" by blast
show "x ∈ A"
proof(cases "x ≤ α")
case True
obtain n where n_def: "α= eint n"
using alpha_def
by blast
obtain m where m_def: "x = eint m"
using True eint_ile n_def by blast
have 1: "m ≤ n"
using True m_def n_def
by simp
have 2: "eint (int (nat (n - m))) = eint (n - m)"
by (simp add: "1")
then obtain b where b_def: "b ∈ A ∧ b + eint (n - m) ≤ α"
using A1[of "nat (n - m)"]
by (metis)
then have "b + eint (n - m) ≤ x + eint (n - m)"
using b_def
by (simp add: m_def n_def)
then have "b ≤ x"
by auto
then show ?thesis
using "0" assms b_def beta_def is_convex_def
by blast
next
case False
then show ?thesis
using "0" alpha_def assms beta_def is_convexE
by (meson linear)
qed
qed
qed
then show ?thesis
using is_convex_condition_def
by blast
next
case f: False
have F0: "∀a. α ≤ a ∧ a < ∞ ⟶ a ∈ A"
proof(rule ccontr)
assume A: "¬ (∀a. a ≥ α ∧ a < ∞ ⟶ a ∈ A)"
then obtain a where a_def: " α ≤ a ∧ a < ∞ ∧ a ∉ A"
by blast
obtain n where n_def: "α = eint n"
using alpha_def by blast
obtain m where m_def: "a = eint m"
using a_def less_infinityE by blast
have 0: "∀k::nat. ∃c. (α + eint (int k)) < c ∧ c ∈ A"
proof fix k
show "∃c>α + eint (int k). c ∈ A"
apply(induction k)
using alpha_def f le_less_linear apply fastforce
proof- fix k
assume IH: "∃c>α + eint (int k). c ∈ A"
then obtain c where c_def: "c>α + eint (int k) ∧ c ∈ A"
by blast
then obtain c' where c'_def: "c' ∈ A ∧ c < c'"
using False f le_less_linear by blast
then have "(α + eint (int (Suc k))) ≤ c'"
proof-
have 0: "eint (int (Suc k)) = eint (int k) + eint 1"
by simp
have "α + eint (int k) ≤c'"
using c_def c'_def dual_order.strict_trans le_less by blast
then have 1: "(α + eint (int k)) < c'"
using c'_def c_def le_less_trans by auto
have 2: "α + eint (int k) + eint 1 = α + eint (int (Suc k))"
using 0 by (simp add: n_def)
then show "(α + eint (int (Suc k))) ≤ c'"
by (metis "1" ileI1 one_eint_def)
qed
then show "∃c>α + eint (int (Suc k)). c ∈ A"
using False c'_def
by (smt (z3) c_def eSuc_eint iadd_Suc_right ileI1 le_less of_nat_Suc)
qed
qed
obtain k::nat where "a = α + eint (int k)"
using bounded_order a_def
by blast
then obtain c where "c ∈ A ∧ a <c"
using 0 by blast
then have "a ∈ A"
using is_convexE[of A α a c] a_def alpha_def assms is_convexE
by (meson linear not_less)
then show False
using a_def by blast
qed
have "A = UNIV - {∞}"
proof
show "A ⊆ UNIV - {∞}"
using f by auto
show "UNIV - {∞} ⊆ A"
proof fix x ::eint
assume A: "x ∈ UNIV - {∞}"
show "x ∈ A"
proof(cases "x ≤ α")
case True
obtain k::nat where k_def: "x + k = α"
by (metis True alpha_def bounded_order eint_ord_simps(4))
obtain c where c_def: "c ∈ A ∧ c + k = α"
by (metis A1 True add.commute alpha_def assms eint_add_left_cancel_le is_convexE k_def not_eint_eq)
have "x = c"
using k_def c_def
by auto
thus ?thesis
by (simp add: c_def)
next
case False
thus ?thesis
using A F0 by auto
qed
qed
qed
then show ?thesis
by (meson is_convex_condition_def value_group_is_open_ray)
qed
qed
qed
lemma ex_val_less:
shows "∃ (α::eint). α < β"
apply(induction β)
using eint_ord_simps(2) lt_ex apply blast
using eint_ord_simps(4) by blast
lemma ex_dist_less:
assumes "c ∈ carrier Q⇩p"
shows "∃ a ∈ carrier Q⇩p. val (a ⊖ c) < β"
using ex_val_less[of β] assms
by (metis dist_nonempty' ex_val_less)
end
end