Theory AxEField

(*
  Mike Stannett
  Feb 2023
*)

section ‹ AXIOM: AxEField ›

text ‹This theory defines the axiom AxEField, which states that 
the linearly ordered field of quantities is Euclidean, i.e. that
all non-negative values have square roots in the field. ›

theory AxEField
  imports Sorts
begin

class axEField = Quantities
begin
  abbreviation axEField :: "'a ⇒ bool"
    where "axEField x ≡ (x ≥ 0) ⟶ hasRoot x"
end (* of class axEField *)


class AxEField = axEField +
  assumes AxEField: "∀ x . axEField x"
begin
end (* of class AxEField *)


end (* of theory AxEField *)