\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym, amsmath, amssymb, amsfonts}

% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed

%\usepackage{amssymb}
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
  %\<triangleq>, \<yen>, \<lozenge>

%\usepackage{eurosym}
  %for \<euro>

%\usepackage[only,bigsqcap]{stmaryrd}
  %for \<Sqinter>

%\usepackage{eufrak}
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)

%\usepackage{textcomp}
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
  %\<currency>

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}


\begin{document}

\title{$p$-adic Fields}
\author{Aaron Crighton}
\maketitle

\tableofcontents

% sane default for proof documents
\parindent 0pt\parskip 0.5ex


\begin{abstract}
We formalize the fields $\mathbb{Q}_p$ of $p$-adic numbers within the framework of the HOL-Algebra library. The $p$-adic field is defined simply as the fraction field of the ring of $p$-adic integers. The valuation, and basic topological properties of $\mathbb{Q}_p$ are developed, including deducing Hensel's Lemma for $\mathbb{Q}_p$ from the same theorem for $\mathbb{Z}_p$. The theory of semialgebraic subsets of $\mathbb{Q}_p^n$ and semialgebraic functions is also developed, as outlined in \cite{denef1986}. In order to formulate these results, general theory about multivariable polynomial rings and cartesian powers of a ring must also be developed. This work is done with a view to formalizing the proof in \cite{denef1986} of Macintyre's quantifier elimination theorem for semialgebraic subsets of $\mathbb{Q}_p^n$. 
\end{abstract}
% generated text of all theories

\input{session}

% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
