src/Doc/Implementation/Logic.thy

 
 chapter \<open>Primitive logic \label{ch:logic}\<close>
 
 text \<open>
   The logical foundations of Isabelle/Isar are that of the Pure logic, which
-  has been introduced as a Natural Deduction framework in @{cite paulson700}.
+  has been introduced as a Natural Deduction framework in \<^cite>\<open>paulson700\<close>.
   This is essentially the same logic as ``\<open>\<lambda>HOL\<close>'' in the more abstract
-  setting of Pure Type Systems (PTS) @{cite "Barendregt-Geuvers:2001"},
+  setting of Pure Type Systems (PTS) \<^cite>\<open>"Barendregt-Geuvers:2001"\<close>,
   although there are some key differences in the specific treatment of simple
   types in Isabelle/Pure.
 
   Following type-theoretic parlance, the Pure logic consists of three levels
   of \<open>\<lambda>\<close>-calculus with corresponding arrows, \<open>\<Rightarrow>\<close> for syntactic function space

   constraints can be solved in a most general fashion: for each type
   constructor \<open>\<kappa>\<close> and sort \<open>s\<close> there is a most general vector of argument
   sorts \<open>(s\<^sub>1, \<dots>, s\<^sub>k)\<close> such that a type scheme \<open>(\<alpha>\<^bsub>s\<^sub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^sub>k\<^esub>)\<kappa>\<close> is of
   sort \<open>s\<close>. Consequently, type unification has most general solutions (modulo
   equivalence of sorts), so type-inference produces primary types as expected
-  @{cite "nipkow-prehofer"}.
+  \<^cite>\<open>"nipkow-prehofer"\<close>.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML_type class = string} \\

 
 section \<open>Terms \label{sec:terms}\<close>
 
 text \<open>
   The language of terms is that of simply-typed \<open>\<lambda>\<close>-calculus with de-Bruijn
-  indices for bound variables (cf.\ @{cite debruijn72} or @{cite
-  "paulson-ml2"}), with the types being determined by the corresponding
+  indices for bound variables (cf.\ \<^cite>\<open>debruijn72\<close> or \<^cite>\<open>"paulson-ml2"\<close>), with the types being determined by the corresponding
   binders. In contrast, free variables and constants have an explicit name and
   type in each occurrence.
 
   \<^medskip>
   A \<^emph>\<open>bound variable\<close> is a natural number \<open>b\<close>, which accounts for the number

   formation of dependently typed \<open>\<lambda>\<close>-terms representing the underlying proof
   objects. Proof terms are irrelevant in the Pure logic, though; they cannot
   occur within propositions. The system provides a runtime option to record
   explicit proof terms for primitive inferences, see also
   \secref{sec:proof-terms}. Thus all three levels of \<open>\<lambda>\<close>-calculus become
-  explicit: \<open>\<Rightarrow>\<close> for terms, and \<open>\<And>/\<Longrightarrow>\<close> for proofs (cf.\ @{cite
-  "Berghofer-Nipkow:2000:TPHOL"}).
+  explicit: \<open>\<Rightarrow>\<close> for terms, and \<open>\<And>/\<Longrightarrow>\<close> for proofs (cf.\ \<^cite>\<open>"Berghofer-Nipkow:2000:TPHOL"\<close>).
 
   Observe that locally fixed parameters (as in \<open>\<And>\<hyphen>intro\<close>) need not be recorded
   in the hypotheses, because the simple syntactic types of Pure are always
   inhabitable. ``Assumptions'' \<open>x :: \<tau>\<close> for type-membership are only present
   as long as some \<open>x\<^sub>\<tau>\<close> occurs in the statement body.\<^footnote>\<open>This is the key
-  difference to ``\<open>\<lambda>HOL\<close>'' in the PTS framework @{cite
-  "Barendregt-Geuvers:2001"}, where hypotheses \<open>x : A\<close> are treated uniformly
+  difference to ``\<open>\<lambda>HOL\<close>'' in the PTS framework \<^cite>\<open>"Barendregt-Geuvers:2001"\<close>, where hypotheses \<open>x : A\<close> are treated uniformly
   for propositions and types.\<close>
 
   \<^medskip>
   The axiomatization of a theory is implicitly closed by forming all instances
   of type and term variables: \<open>\<turnstile> A\<vartheta>\<close> holds for any substitution

   constant, with zero or one equations \<open>c((\<^vec>\<alpha>)\<kappa>) \<equiv> t\<close> for each type
   constructor \<open>\<kappa>\<close> (for distinct variables \<open>\<^vec>\<alpha>\<close>). The RHS may mention
   previously defined constants as above, or arbitrary constants \<open>d(\<alpha>\<^sub>i)\<close> for
   some \<open>\<alpha>\<^sub>i\<close> projected from \<open>\<^vec>\<alpha>\<close>. Thus overloaded definitions
   essentially work by primitive recursion over the syntactic structure of a
-  single type argument. See also @{cite \<open>\S4.3\<close>
-  "Haftmann-Wenzel:2006:classes"}.
+  single type argument. See also \<^cite>\<open>\<open>\S4.3\<close> in
+  "Haftmann-Wenzel:2006:classes"\<close>.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML Logic.all: "term -> term -> term"} \\

 
 subsection \<open>Hereditary Harrop Formulae\<close>
 
 text \<open>
   The idea of object-level rules is to model Natural Deduction inferences in
-  the style of Gentzen @{cite "Gentzen:1935"}, but we allow arbitrary nesting
-  similar to @{cite "Schroeder-Heister:1984"}. The most basic rule format is
+  the style of Gentzen \<^cite>\<open>"Gentzen:1935"\<close>, but we allow arbitrary nesting
+  similar to \<^cite>\<open>"Schroeder-Heister:1984"\<close>. The most basic rule format is
   that of a \<^emph>\<open>Horn Clause\<close>:
   \[
   \infer{\<open>A\<close>}{\<open>A\<^sub>1\<close> & \<open>\<dots>\<close> & \<open>A\<^sub>n\<close>}
   \]
   where \<open>A, A\<^sub>1, \<dots>, A\<^sub>n\<close> are atomic propositions of the framework, usually of

   \<open>\<And>x\<^sub>1 \<dots> x\<^sub>m. A\<^sub>1 x\<^sub>1 \<dots> x\<^sub>m \<Longrightarrow> \<dots> A\<^sub>n x\<^sub>1 \<dots> x\<^sub>m \<Longrightarrow> A x\<^sub>1 \<dots> x\<^sub>m\<close>
   \]
 
   Nesting of rules means that the positions of \<open>A\<^sub>i\<close> may again hold compound
   rules, not just atomic propositions. Propositions of this format are called
-  \<^emph>\<open>Hereditary Harrop Formulae\<close> in the literature @{cite "Miller:1991"}. Here
+  \<^emph>\<open>Hereditary Harrop Formulae\<close> in the literature \<^cite>\<open>"Miller:1991"\<close>. Here
   we give an inductive characterization as follows:
 
   \<^medskip>
   \begin{tabular}{ll}
   \<open>\<^bold>x\<close> & set of variables \\

   represented by a datatype similar to the one for terms described in
   \secref{sec:terms}. On top of these syntactic terms, two more layers of
   \<open>\<lambda>\<close>-calculus are added, which correspond to \<open>\<And>x :: \<alpha>. B x\<close> and \<open>A \<Longrightarrow> B\<close>
   according to the propositions-as-types principle. The resulting 3-level
   \<open>\<lambda>\<close>-calculus resembles ``\<open>\<lambda>HOL\<close>'' in the more abstract setting of Pure Type
-  Systems (PTS) @{cite "Barendregt-Geuvers:2001"}, if some fine points like
+  Systems (PTS) \<^cite>\<open>"Barendregt-Geuvers:2001"\<close>, if some fine points like
   schematic polymorphism and type classes are ignored.
 
   \<^medskip>
   \<^emph>\<open>Proof abstractions\<close> of the form \<open>\<^bold>\<lambda>x :: \<alpha>. prf\<close> or \<open>\<^bold>\<lambda>p : A. prf\<close>
   correspond to introduction of \<open>\<And>\<close>/\<open>\<Longrightarrow>\<close>, and \<^emph>\<open>proof applications\<close> of the form

   Isabelle/Pure inference kernel records only \<^emph>\<open>implicit\<close> proof terms, by
   omitting all typing information in terms, all term and type labels of proof
   abstractions, and some argument terms of applications \<open>p \<cdot> t\<close> (if possible).
 
   There are separate operations to reconstruct the full proof term later on,
-  using \<^emph>\<open>higher-order pattern unification\<close> @{cite "nipkow-patterns" and
-  "Berghofer-Nipkow:2000:TPHOL"}.
+  using \<^emph>\<open>higher-order pattern unification\<close> \<^cite>\<open>"nipkow-patterns" and
+  "Berghofer-Nipkow:2000:TPHOL"\<close>.
 
   The \<^emph>\<open>proof checker\<close> expects a fully reconstructed proof term, and can turn
   it into a theorem by replaying its primitive inferences within the kernel.
 \<close>
 
 
 subsection \<open>Concrete syntax of proof terms\<close>
 
 text \<open>
   The concrete syntax of proof terms is a slight extension of the regular
-  inner syntax of Isabelle/Pure @{cite "isabelle-isar-ref"}. Its main
+  inner syntax of Isabelle/Pure \<^cite>\<open>"isabelle-isar-ref"\<close>. Its main
   syntactic category @{syntax (inner) proof} is defined as follows:
 
   \begin{center}
   \begin{supertabular}{rclr}