(* $Id$ *)

theory pure

imports CPure

begin

chapter {* Basic language elements \label{ch:pure-syntax} *}

text {*

  Subsequently, we introduce the main part of Pure theory and proof

  commands, together with fundamental proof methods and attributes.

  \Chref{ch:gen-tools} describes further Isar elements provided by

  generic tools and packages (such as the Simplifier) that are either

  part of Pure Isabelle or pre-installed in most object logics.

  \Chref{ch:logics} refers to object-logic specific elements (mainly

  for HOL and ZF).

  \medskip Isar commands may be either \emph{proper} document

  constructors, or \emph{improper commands}.  Some proof methods and

  attributes introduced later are classified as improper as well.

  Improper Isar language elements, which are subsequently marked by

  ``@{text "\<^sup>*"}'', are often helpful when developing proof

  documents, while their use is discouraged for the final

  human-readable outcome.  Typical examples are diagnostic commands

  that print terms or theorems according to the current context; other

  commands emulate old-style tactical theorem proving.

*}

section {* Theory commands *}

subsection {* Defining theories \label{sec:begin-thy} *}

text {*

  \begin{matharray}{rcl}

    @{command_def "header"} & : & \isarkeep{toplevel} \\

    @{command_def "theory"} & : & \isartrans{toplevel}{theory} \\

    @{command_def "end"} & : & \isartrans{theory}{toplevel} \\

  \end{matharray}

  Isabelle/Isar theories are defined via theory, which contain both

  specifications and proofs; occasionally definitional mechanisms also

  require some explicit proof.

  The first ``real'' command of any theory has to be @{command

  "theory"}, which starts a new theory based on the merge of existing

  ones.  Just preceding the @{command "theory"} keyword, there may be

  an optional @{command "header"} declaration, which is relevant to

  document preparation only; it acts very much like a special

  pre-theory markup command (cf.\ \secref{sec:markup-thy} and

  \secref{sec:markup-thy}).  The @{command "end"} command concludes a

  theory development; it has to be the very last command of any theory

  file loaded in batch-mode.

  \begin{rail}

    'header' text

    ;

    'theory' name 'imports' (name +) uses? 'begin'

    ;

    uses: 'uses' ((name | parname) +);

  \end{rail}

  \begin{descr}

  \item [@{command "header"}~@{text "text"}] provides plain text

  markup just preceding the formal beginning of a theory.  In actual

  document preparation the corresponding {\LaTeX} macro @{verbatim

  "\\isamarkupheader"} may be redefined to produce chapter or section

  headings.  See also \secref{sec:markup-thy} and

  \secref{sec:markup-prf} for further markup commands.

  \item [@{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots>

  B\<^sub>n \<BEGIN>"}] starts a new theory @{text A} based on the

  merge of existing theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}.

  Due to inclusion of several ancestors, the overall theory structure

  emerging in an Isabelle session forms a directed acyclic graph

  (DAG).  Isabelle's theory loader ensures that the sources

  contributing to the development graph are always up-to-date.

  Changed files are automatically reloaded when processing theory

  headers.

  The optional @{keyword_def "uses"} specification declares additional

  dependencies on extra files (usually ML sources).  Files will be

  loaded immediately (as ML), unless the name is put in parentheses,

  which merely documents the dependency to be resolved later in the

  text (typically via explicit @{command_ref "use"} in the body text,

  see \secref{sec:ML}).

  \item [@{command "end"}] concludes the current theory definition or

  context switch.

  \end{descr}

*}

subsection {* Markup commands \label{sec:markup-thy} *}

text {*

  \begin{matharray}{rcl}

    @{command_def "chapter"} & : & \isarkeep{local{\dsh}theory} \\

    @{command_def "section"} & : & \isarkeep{local{\dsh}theory} \\

    @{command_def "subsection"} & : & \isarkeep{local{\dsh}theory} \\

    @{command_def "subsubsection"} & : & \isarkeep{local{\dsh}theory} \\

    @{command_def "text"} & : & \isarkeep{local{\dsh}theory} \\

    @{command_def "text_raw"} & : & \isarkeep{local{\dsh}theory} \\

  \end{matharray}

  Apart from formal comments (see \secref{sec:comments}), markup

  commands provide a structured way to insert text into the document

  generated from a theory (see \cite{isabelle-sys} for more

  information on Isabelle's document preparation tools).

  \begin{rail}

    ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text

    ;

    'text\_raw' text

    ;

  \end{rail}

  \begin{descr}

  \item [@{command "chapter"}, @{command "section"}, @{command

  "subsection"}, and @{command "subsubsection"}] mark chapter and

  section headings.

  \item [@{command "text"}] specifies paragraphs of plain text.

  \item [@{command "text_raw"}] inserts {\LaTeX} source into the

  output, without additional markup.  Thus the full range of document

  manipulations becomes available.

  \end{descr}

  The @{text "text"} argument of these markup commands (except for

  @{command "text_raw"}) may contain references to formal entities

  (``antiquotations'', see also \secref{sec:antiq}).  These are

  interpreted in the present theory context, or the named @{text

  "target"}.

  Any of these markup elements corresponds to a {\LaTeX} command with

  the name prefixed by @{verbatim "\\isamarkup"}.  For the sectioning

  commands this is a plain macro with a single argument, e.g.\

  @{verbatim "\\isamarkupchapter{"}@{text "\<dots>"}@{verbatim "}"} for

  @{command "chapter"}.  The @{command "text"} markup results in a

  {\LaTeX} environment @{verbatim "\\begin{isamarkuptext}"}~@{text

  "\<dots>"}~@{verbatim "\\end{isamarkuptext}"}, while @{command "text_raw"}

  causes the text to be inserted directly into the {\LaTeX} source.

  \medskip Additional markup commands are available for proofs (see

  \secref{sec:markup-prf}).  Also note that the @{command_ref

  "header"} declaration (see \secref{sec:begin-thy}) admits to insert

  section markup just preceding the actual theory definition.

*}

subsection {* Type classes and sorts \label{sec:classes} *}

text {*

  \begin{matharray}{rcll}

    @{command_def "classes"} & : & \isartrans{theory}{theory} \\

    @{command_def "classrel"} & : & \isartrans{theory}{theory} & (axiomatic!) \\

    @{command_def "defaultsort"} & : & \isartrans{theory}{theory} \\

    @{command_def "class_deps"} & : & \isarkeep{theory~|~proof} \\

  \end{matharray}

  \begin{rail}

    'classes' (classdecl +)

    ;

    'classrel' (nameref ('<' | subseteq) nameref + 'and')

    ;

    'defaultsort' sort

    ;

  \end{rail}

  \begin{descr}

  \item [@{command "classes"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n"}]

  declares class @{text c} to be a subclass of existing classes @{text

  "c\<^sub>1, \<dots>, c\<^sub>n"}.  Cyclic class structures are not permitted.

  \item [@{command "classrel"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"}] states

  subclass relations between existing classes @{text "c\<^sub>1"} and

  @{text "c\<^sub>2"}.  This is done axiomatically!  The @{command_ref

  "instance"} command (see \secref{sec:axclass}) provides a way to

  introduce proven class relations.

  \item [@{command "defaultsort"}~@{text s}] makes sort @{text s} the

  new default sort for any type variables given without sort

  constraints.  Usually, the default sort would be only changed when

  defining a new object-logic.

  \item [@{command "class_deps"}] visualizes the subclass relation,

  using Isabelle's graph browser tool (see also \cite{isabelle-sys}).

  \end{descr}

*}

subsection {* Primitive types and type abbreviations \label{sec:types-pure} *}

text {*

  \begin{matharray}{rcll}

    @{command_def "types"} & : & \isartrans{theory}{theory} \\

    @{command_def "typedecl"} & : & \isartrans{theory}{theory} \\

    @{command_def "nonterminals"} & : & \isartrans{theory}{theory} \\

    @{command_def "arities"} & : & \isartrans{theory}{theory} & (axiomatic!) \\

  \end{matharray}

  \begin{rail}

    'types' (typespec '=' type infix? +)

    ;

    'typedecl' typespec infix?

    ;

    'nonterminals' (name +)

    ;

    'arities' (nameref '::' arity +)

    ;

  \end{rail}

  \begin{descr}

  \item [@{command "types"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"}]

  introduces \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"}

  for existing type @{text "\<tau>"}.  Unlike actual type definitions, as

  are available in Isabelle/HOL for example, type synonyms are just

  purely syntactic abbreviations without any logical significance.

  Internally, type synonyms are fully expanded.

  \item [@{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"}]

  declares a new type constructor @{text t}, intended as an actual

  logical type (of the object-logic, if available).

  \item [@{command "nonterminals"}~@{text c}] declares type

  constructors @{text c} (without arguments) to act as purely

  syntactic types, i.e.\ nonterminal symbols of Isabelle's inner

  syntax of terms or types.

  \item [@{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)

  s"}] augments Isabelle's order-sorted signature of types by new type

  constructor arities.  This is done axiomatically!  The @{command_ref

  "instance"} command (see \S\ref{sec:axclass}) provides a way to

  introduce proven type arities.

  \end{descr}

*}

subsection {* Primitive constants and definitions \label{sec:consts} *}

text {*

  Definitions essentially express abbreviations within the logic.  The

  simplest form of a definition is @{text "c :: \<sigma> \<equiv> t"}, where @{text

  c} is a newly declared constant.  Isabelle also allows derived forms

  where the arguments of @{text c} appear on the left, abbreviating a

  prefix of @{text \<lambda>}-abstractions, e.g.\ @{text "c \<equiv> \<lambda>x y. t"} may be

  written more conveniently as @{text "c x y \<equiv> t"}.  Moreover,

  definitions may be weakened by adding arbitrary pre-conditions:

  @{text "A \<Longrightarrow> c x y \<equiv> t"}.

  \medskip The built-in well-formedness conditions for definitional

  specifications are:

  \begin{itemize}

  \item Arguments (on the left-hand side) must be distinct variables.

  \item All variables on the right-hand side must also appear on the

  left-hand side.

  \item All type variables on the right-hand side must also appear on

  the left-hand side; this prohibits @{text "0 :: nat \<equiv> length ([] ::

  \<alpha> list)"} for example.

  \item The definition must not be recursive.  Most object-logics

  provide definitional principles that can be used to express

  recursion safely.

  \end{itemize}

  Overloading means that a constant being declared as @{text "c :: \<alpha>

  decl"} may be defined separately on type instances @{text "c ::

  (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"} for each type constructor @{text

  t}.  The right-hand side may mention overloaded constants

  recursively at type instances corresponding to the immediate

  argument types @{text "\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n"}.  Incomplete

  specification patterns impose global constraints on all occurrences,

  e.g.\ @{text "d :: \<alpha> \<times> \<alpha>"} on the left-hand side means that all

  corresponding occurrences on some right-hand side need to be an

  instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed.

  \begin{matharray}{rcl}

    @{command_def "consts"} & : & \isartrans{theory}{theory} \\

    @{command_def "defs"} & : & \isartrans{theory}{theory} \\

    @{command_def "constdefs"} & : & \isartrans{theory}{theory} \\

  \end{matharray}

  \begin{rail}

    'consts' ((name '::' type mixfix?) +)

    ;

    'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)

    ;

  \end{rail}

  \begin{rail}

    'constdefs' structs? (constdecl? constdef +)

    ;

    structs: '(' 'structure' (vars + 'and') ')'

    ;

    constdecl:  ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'

    ;

    constdef: thmdecl? prop

    ;

  \end{rail}

  \begin{descr}

  \item [@{command "consts"}~@{text "c :: \<sigma>"}] declares constant

  @{text c} to have any instance of type scheme @{text \<sigma>}.  The

  optional mixfix annotations may attach concrete syntax to the

  constants declared.

  \item [@{command "defs"}~@{text "name: eqn"}] introduces @{text eqn}

  as a definitional axiom for some existing constant.

  The @{text "(unchecked)"} option disables global dependency checks

  for this definition, which is occasionally useful for exotic

  overloading.  It is at the discretion of the user to avoid malformed

  theory specifications!

  The @{text "(overloaded)"} option declares definitions to be

  potentially overloaded.  Unless this option is given, a warning

  message would be issued for any definitional equation with a more

  special type than that of the corresponding constant declaration.

  \item [@{command "constdefs"}] provides a streamlined combination of

  constants declarations and definitions: type-inference takes care of

  the most general typing of the given specification (the optional

  type constraint may refer to type-inference dummies ``@{verbatim

  _}'' as usual).  The resulting type declaration needs to agree with

  that of the specification; overloading is \emph{not} supported here!

  The constant name may be omitted altogether, if neither type nor

  syntax declarations are given.  The canonical name of the

  definitional axiom for constant @{text c} will be @{text c_def},

  unless specified otherwise.  Also note that the given list of

  specifications is processed in a strictly sequential manner, with

  type-checking being performed independently.

  An optional initial context of @{text "(structure)"} declarations

  admits use of indexed syntax, using the special symbol @{verbatim

  "\<index>"} (printed as ``@{text "\<index>"}'').  The latter concept is

  particularly useful with locales (see also \S\ref{sec:locale}).

  \end{descr}

*}

subsection {* Syntax and translations \label{sec:syn-trans} *}

text {*

  \begin{matharray}{rcl}

    @{command_def "syntax"} & : & \isartrans{theory}{theory} \\

    @{command_def "no_syntax"} & : & \isartrans{theory}{theory} \\

    @{command_def "translations"} & : & \isartrans{theory}{theory} \\

    @{command_def "no_translations"} & : & \isartrans{theory}{theory} \\

  \end{matharray}

  \railalias{rightleftharpoons}{\isasymrightleftharpoons}

  \railterm{rightleftharpoons}

  \railalias{rightharpoonup}{\isasymrightharpoonup}

  \railterm{rightharpoonup}

  \railalias{leftharpoondown}{\isasymleftharpoondown}

  \railterm{leftharpoondown}

  \begin{rail}

    ('syntax' | 'no\_syntax') mode? (constdecl +)

    ;

    ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)

    ;

    mode: ('(' ( name | 'output' | name 'output' ) ')')

    ;

    transpat: ('(' nameref ')')? string

    ;

  \end{rail}

  \begin{descr}

  \item [@{command "syntax"}~@{text "(mode) decls"}] is similar to

  @{command "consts"}~@{text decls}, except that the actual logical

  signature extension is omitted.  Thus the context free grammar of

  Isabelle's inner syntax may be augmented in arbitrary ways,

  independently of the logic.  The @{text mode} argument refers to the

  print mode that the grammar rules belong; unless the @{keyword_ref

  "output"} indicator is given, all productions are added both to the

  input and output grammar.

  \item [@{command "no_syntax"}~@{text "(mode) decls"}] removes

  grammar declarations (and translations) resulting from @{text

  decls}, which are interpreted in the same manner as for @{command

  "syntax"} above.

  \item [@{command "translations"}~@{text rules}] specifies syntactic

  translation rules (i.e.\ macros): parse~/ print rules (@{text "\<rightleftharpoons>"}),

  parse rules (@{text "\<rightharpoonup>"}), or print rules (@{text "\<leftharpoondown>"}).

  Translation patterns may be prefixed by the syntactic category to be

  used for parsing; the default is @{text logic}.

  \item [@{command "no_translations"}~@{text rules}] removes syntactic

  translation rules, which are interpreted in the same manner as for

  @{command "translations"} above.

  \end{descr}

*}

subsection {* Axioms and theorems \label{sec:axms-thms} *}

text {*

  \begin{matharray}{rcll}

    @{command_def "axioms"} & : & \isartrans{theory}{theory} & (axiomatic!) \\

    @{command_def "lemmas"} & : & \isarkeep{local{\dsh}theory} \\

    @{command_def "theorems"} & : & isarkeep{local{\dsh}theory} \\

  \end{matharray}

  \begin{rail}

    'axioms' (axmdecl prop +)

    ;

    ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')

    ;

  \end{rail}

  \begin{descr}

  \item [@{command "axioms"}~@{text "a: \<phi>"}] introduces arbitrary

  statements as axioms of the meta-logic.  In fact, axioms are

  ``axiomatic theorems'', and may be referred later just as any other

  theorem.

  Axioms are usually only introduced when declaring new logical

  systems.  Everyday work is typically done the hard way, with proper

  definitions and proven theorems.

  \item [@{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}]

  retrieves and stores existing facts in the theory context, or the

  specified target context (see also \secref{sec:target}).  Typical

  applications would also involve attributes, to declare Simplifier

  rules, for example.

  \item [@{command "theorems"}] is essentially the same as @{command

  "lemmas"}, but marks the result as a different kind of facts.

  \end{descr}

*}

subsection {* Name spaces *}

text {*

  \begin{matharray}{rcl}

    @{command_def "global"} & : & \isartrans{theory}{theory} \\

    @{command_def "local"} & : & \isartrans{theory}{theory} \\

    @{command_def "hide"} & : & \isartrans{theory}{theory} \\

  \end{matharray}

  \begin{rail}

    'hide' ('(open)')? name (nameref + )

    ;

  \end{rail}

  Isabelle organizes any kind of name declarations (of types,

  constants, theorems etc.) by separate hierarchically structured name

  spaces.  Normally the user does not have to control the behavior of

  name spaces by hand, yet the following commands provide some way to

  do so.

  \begin{descr}

  \item [@{command "global"} and @{command "local"}] change the

  current name declaration mode.  Initially, theories start in

  @{command "local"} mode, causing all names to be automatically

  qualified by the theory name.  Changing this to @{command "global"}

  causes all names to be declared without the theory prefix, until

  @{command "local"} is declared again.

  Note that global names are prone to get hidden accidently later,

  when qualified names of the same base name are introduced.

  \item [@{command "hide"}~@{text "space names"}] fully removes

  declarations from a given name space (which may be @{text "class"},

  @{text "type"}, @{text "const"}, or @{text "fact"}); with the @{text

  "(open)"} option, only the base name is hidden.  Global

  (unqualified) names may never be hidden.

  Note that hiding name space accesses has no impact on logical

  declarations -- they remain valid internally.  Entities that are no

  longer accessible to the user are printed with the special qualifier

  ``@{text "??"}'' prefixed to the full internal name.

  \end{descr}

*}

subsection {* Incorporating ML code \label{sec:ML} *}

text {*

  \begin{matharray}{rcl}

    @{command_def "use"} & : & \isarkeep{theory~|~local{\dsh}theory} \\

    @{command_def "ML"} & : & \isarkeep{theory~|~local{\dsh}theory} \\

    @{command_def "ML_val"} & : & \isartrans{\cdot}{\cdot} \\

    @{command_def "ML_command"} & : & \isartrans{\cdot}{\cdot} \\

    @{command_def "setup"} & : & \isartrans{theory}{theory} \\

    @{command_def "method_setup"} & : & \isartrans{theory}{theory} \\

  \end{matharray}

  \begin{rail}

    'use' name

    ;

    ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text

    ;

    'method\_setup' name '=' text text

    ;

  \end{rail}

  \begin{descr}

  \item [@{command "use"}~@{text "file"}] reads and executes ML

  commands from @{text "file"}.  The current theory context is passed

  down to the ML toplevel and may be modified, using @{ML

  "Context.>>"} or derived ML commands.  The file name is checked with

  the @{keyword_ref "uses"} dependency declaration given in the theory

  header (see also \secref{sec:begin-thy}).

  \item [@{command "ML"}~@{text "text"}] is similar to @{command

  "use"}, but executes ML commands directly from the given @{text

  "text"}.

  \item [@{command "ML_val"} and @{command "ML_command"}] are

  diagnostic versions of @{command "ML"}, which means that the context

  may not be updated.  @{command "ML_val"} echos the bindings produced

  at the ML toplevel, but @{command "ML_command"} is silent.

  \item [@{command "setup"}~@{text "text"}] changes the current theory

  context by applying @{text "text"}, which refers to an ML expression

  of type @{ML_type "theory -> theory"}.  This enables to initialize

  any object-logic specific tools and packages written in ML, for

  example.

  \item [@{command "method_setup"}~@{text "name = text description"}]

  defines a proof method in the current theory.  The given @{text

  "text"} has to be an ML expression of type @{ML_type "Args.src ->

  Proof.context -> Proof.method"}.  Parsing concrete method syntax

  from @{ML_type Args.src} input can be quite tedious in general.  The

  following simple examples are for methods without any explicit

  arguments, or a list of theorems, respectively.

%FIXME proper antiquotations

{\footnotesize

\begin{verbatim}

 Method.no_args (Method.METHOD (fn facts => foobar_tac))

 Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))

 Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))

 Method.thms_ctxt_args (fn thms => fn ctxt =>

    Method.METHOD (fn facts => foobar_tac))

\end{verbatim}

}

  Note that mere tactic emulations may ignore the @{text facts}

  parameter above.  Proper proof methods would do something

  appropriate with the list of current facts, though.  Single-rule

  methods usually do strict forward-chaining (e.g.\ by using @{ML

  Drule.multi_resolves}), while automatic ones just insert the facts

  using @{ML Method.insert_tac} before applying the main tactic.

  \end{descr}

*}

subsection {* Syntax translation functions *}

text {*

  \begin{matharray}{rcl}

    @{command_def "parse_ast_translation"} & : & \isartrans{theory}{theory} \\

    @{command_def "parse_translation"} & : & \isartrans{theory}{theory} \\

    @{command_def "print_translation"} & : & \isartrans{theory}{theory} \\

    @{command_def "typed_print_translation"} & : & \isartrans{theory}{theory} \\

    @{command_def "print_ast_translation"} & : & \isartrans{theory}{theory} \\

    @{command_def "token_translation"} & : & \isartrans{theory}{theory} \\

  \end{matharray}

  \begin{rail}

  ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |

    'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text

  ;

  'token\_translation' text

  ;

  \end{rail}

  Syntax translation functions written in ML admit almost arbitrary

  manipulations of Isabelle's inner syntax.  Any of the above commands

  have a single \railqtok{text} argument that refers to an ML

  expression of appropriate type, which are as follows by default:

%FIXME proper antiquotations

\begin{ttbox}

val parse_ast_translation   : (string * (ast list -> ast)) list

val parse_translation       : (string * (term list -> term)) list

val print_translation       : (string * (term list -> term)) list

val typed_print_translation :

  (string * (bool -> typ -> term list -> term)) list

val print_ast_translation   : (string * (ast list -> ast)) list

val token_translation       :

  (string * string * (string -> string * real)) list

\end{ttbox}

  If the @{text "(advanced)"} option is given, the corresponding

  translation functions may depend on the current theory or proof

  context.  This allows to implement advanced syntax mechanisms, as

  translations functions may refer to specific theory declarations or

  auxiliary proof data.

  See also \cite[\S8]{isabelle-ref} for more information on the

  general concept of syntax transformations in Isabelle.

%FIXME proper antiquotations

\begin{ttbox}

val parse_ast_translation:

  (string * (Context.generic -> ast list -> ast)) list

val parse_translation:

  (string * (Context.generic -> term list -> term)) list

val print_translation:

  (string * (Context.generic -> term list -> term)) list

val typed_print_translation:

  (string * (Context.generic -> bool -> typ -> term list -> term)) list

val print_ast_translation:

  (string * (Context.generic -> ast list -> ast)) list

\end{ttbox}

*}

subsection {* Oracles *}

text {*

  \begin{matharray}{rcl}

    @{command_def "oracle"} & : & \isartrans{theory}{theory} \\

  \end{matharray}

  The oracle interface promotes a given ML function @{ML_text

  "theory -> T -> term"} to @{ML_text "theory -> T -> thm"}, for some type

  @{ML_text T} given by the user.  This acts like an infinitary

  specification of axioms -- there is no internal check of the

  correctness of the results!  The inference kernel records oracle

  invocations within the internal derivation object of theorems, and

  the pretty printer attaches ``@{text "[!]"}'' to indicate results

  that are not fully checked by Isabelle inferences.

  \begin{rail}

    'oracle' name '(' type ')' '=' text

    ;

  \end{rail}

  \begin{descr}

  \item [@{command "oracle"}~@{text "name (type) = text"}] turns the

  given ML expression @{text "text"} of type @{ML_text "{theory

  ->"}~@{text "type"}~@{ML_text "-> term"} into an ML function

  @{ML_text name} of type @{ML_text "{theory ->"}~@{text

  "type"}~@{ML_text "-> thm"}.

  \end{descr}

*}

section {* Proof commands *}

text {*

  Proof commands perform transitions of Isar/VM machine

  configurations, which are block-structured, consisting of a stack of

  nodes with three main components: logical proof context, current

  facts, and open goals.  Isar/VM transitions are \emph{typed}

  according to the following three different modes of operation:

  \begin{descr}

  \item [@{text "proof(prove)"}] means that a new goal has just been

  stated that is now to be \emph{proven}; the next command may refine

  it by some proof method, and enter a sub-proof to establish the

  actual result.

  \item [@{text "proof(state)"}] is like a nested theory mode: the

  context may be augmented by \emph{stating} additional assumptions,

  intermediate results etc.

  \item [@{text "proof(chain)"}] is intermediate between @{text

  "proof(state)"} and @{text "proof(prove)"}: existing facts (i.e.\

  the contents of the special ``@{fact_ref this}'' register) have been

  just picked up in order to be used when refining the goal claimed

  next.

  \end{descr}

  The proof mode indicator may be read as a verb telling the writer

  what kind of operation may be performed next.  The corresponding

  typings of proof commands restricts the shape of well-formed proof

  texts to particular command sequences.  So dynamic arrangements of

  commands eventually turn out as static texts of a certain structure.

  \Appref{ap:refcard} gives a simplified grammar of the overall

  (extensible) language emerging that way.

*}

subsection {* Markup commands \label{sec:markup-prf} *}

text {*

  \begin{matharray}{rcl}

    @{command_def "sect"} & : & \isartrans{proof}{proof} \\

    @{command_def "subsect"} & : & \isartrans{proof}{proof} \\

    @{command_def "subsubsect"} & : & \isartrans{proof}{proof} \\

    @{command_def "txt"} & : & \isartrans{proof}{proof} \\

    @{command_def "txt_raw"} & : & \isartrans{proof}{proof} \\

  \end{matharray}

  These markup commands for proof mode closely correspond to the ones

  of theory mode (see \S\ref{sec:markup-thy}).

  \begin{rail}

    ('sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text

    ;

  \end{rail}

*}

subsection {* Context elements \label{sec:proof-context} *}

text {*

  \begin{matharray}{rcl}

    @{command_def "fix"} & : & \isartrans{proof(state)}{proof(state)} \\

    @{command_def "assume"} & : & \isartrans{proof(state)}{proof(state)} \\

    @{command_def "presume"} & : & \isartrans{proof(state)}{proof(state)} \\

    @{command_def "def"} & : & \isartrans{proof(state)}{proof(state)} \\

  \end{matharray}

  The logical proof context consists of fixed variables and

  assumptions.  The former closely correspond to Skolem constants, or

  meta-level universal quantification as provided by the Isabelle/Pure

  logical framework.  Introducing some \emph{arbitrary, but fixed}

  variable via ``@{command "fix"}~@{text x} results in a local value

  that may be used in the subsequent proof as any other variable or

  constant.  Furthermore, any result @{text "\<turnstile> \<phi>[x]"} exported from

  the context will be universally closed wrt.\ @{text x} at the

  outermost level: @{text "\<turnstile> \<And>x. \<phi>[x]"} (this is expressed in normal

  form using Isabelle's meta-variables).

  Similarly, introducing some assumption @{text \<chi>} has two effects.

  On the one hand, a local theorem is created that may be used as a

  fact in subsequent proof steps.  On the other hand, any result

  @{text "\<chi> \<turnstile> \<phi>"} exported from the context becomes conditional wrt.\

  the assumption: @{text "\<turnstile> \<chi> \<Longrightarrow> \<phi>"}.  Thus, solving an enclosing goal

  using such a result would basically introduce a new subgoal stemming

  from the assumption.  How this situation is handled depends on the

  version of assumption command used: while @{command "assume"}

  insists on solving the subgoal by unification with some premise of

  the goal, @{command "presume"} leaves the subgoal unchanged in order

  to be proved later by the user.

  Local definitions, introduced by ``@{command "def"}~@{text "x \<equiv>

  t"}'', are achieved by combining ``@{command "fix"}~@{text x}'' with

  another version of assumption that causes any hypothetical equation

  @{text "x \<equiv> t"} to be eliminated by the reflexivity rule.  Thus,

  exporting some result @{text "x \<equiv> t \<turnstile> \<phi>[x]"} yields @{text "\<turnstile>

  \<phi>[t]"}.

  \railalias{equiv}{\isasymequiv}

  \railterm{equiv}

  \begin{rail}

    'fix' (vars + 'and')

    ;

    ('assume' | 'presume') (props + 'and')

    ;

    'def' (def + 'and')

    ;

    def: thmdecl? \\ name ('==' | equiv) term termpat?

    ;

  \end{rail}

  \begin{descr}

  \item [@{command "fix"}~@{text x}] introduces a local variable

  @{text x} that is \emph{arbitrary, but fixed.}

  \item [@{command "assume"}~@{text "a: \<phi>"} and @{command

  "presume"}~@{text "a: \<phi>"}] introduce a local fact @{text "\<phi> \<turnstile> \<phi>"} by

  assumption.  Subsequent results applied to an enclosing goal (e.g.\

  by @{command_ref "show"}) are handled as follows: @{command

  "assume"} expects to be able to unify with existing premises in the

  goal, while @{command "presume"} leaves @{text \<phi>} as new subgoals.

  Several lists of assumptions may be given (separated by

  @{keyword_ref "and"}; the resulting list of current facts consists

  of all of these concatenated.

  \item [@{command "def"}~@{text "x \<equiv> t"}] introduces a local

  (non-polymorphic) definition.  In results exported from the context,

  @{text x} is replaced by @{text t}.  Basically, ``@{command

  "def"}~@{text "x \<equiv> t"}'' abbreviates ``@{command "fix"}~@{text

  x}~@{command "assume"}~@{text "x \<equiv> t"}'', with the resulting

  hypothetical equation solved by reflexivity.

  The default name for the definitional equation is @{text x_def}.

  Several simultaneous definitions may be given at the same time.

  \end{descr}

  The special name @{fact_ref prems} refers to all assumptions of the

  current context as a list of theorems.  This feature should be used

  with great care!  It is better avoided in final proof texts.

*}

subsection {* Facts and forward chaining *}

text {*

  \begin{matharray}{rcl}

    @{command_def "note"} & : & \isartrans{proof(state)}{proof(state)} \\

    @{command_def "then"} & : & \isartrans{proof(state)}{proof(chain)} \\

    @{command_def "from"} & : & \isartrans{proof(state)}{proof(chain)} \\

    @{command_def "with"} & : & \isartrans{proof(state)}{proof(chain)} \\

    @{command_def "using"} & : & \isartrans{proof(prove)}{proof(prove)} \\

    @{command_def "unfolding"} & : & \isartrans{proof(prove)}{proof(prove)} \\

  \end{matharray}

  New facts are established either by assumption or proof of local

  statements.  Any fact will usually be involved in further proofs,

  either as explicit arguments of proof methods, or when forward

  chaining towards the next goal via @{command "then"} (and variants);

  @{command "from"} and @{command "with"} are composite forms

  involving @{command "note"}.  The @{command "using"} elements

  augments the collection of used facts \emph{after} a goal has been

  stated.  Note that the special theorem name @{fact_ref this} refers

  to the most recently established facts, but only \emph{before}

  issuing a follow-up claim.

  \begin{rail}

    'note' (thmdef? thmrefs + 'and')

    ;

    ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')

    ;

  \end{rail}

  \begin{descr}

  \item [@{command "note"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}]

  recalls existing facts @{text "b\<^sub>1, \<dots>, b\<^sub>n"}, binding

  the result as @{text a}.  Note that attributes may be involved as

  well, both on the left and right hand sides.

  \item [@{command "then"}] indicates forward chaining by the current

  facts in order to establish the goal to be claimed next.  The

  initial proof method invoked to refine that will be offered the

  facts to do ``anything appropriate'' (see also

  \secref{sec:proof-steps}).  For example, method @{method_ref rule}

  (see \secref{sec:pure-meth-att}) would typically do an elimination

  rather than an introduction.  Automatic methods usually insert the

  facts into the goal state before operation.  This provides a simple

  scheme to control relevance of facts in automated proof search.

  \item [@{command "from"}~@{text b}] abbreviates ``@{command

  "note"}~@{text b}~@{command "then"}''; thus @{command "then"} is

  equivalent to ``@{command "from"}~@{text this}''.

  \item [@{command "with"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}]

  abbreviates ``@{command "from"}~@{text "b\<^sub>1 \<dots> b\<^sub>n \<AND>

  this"}''; thus the forward chaining is from earlier facts together

  with the current ones.

  \item [@{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}] augments

  the facts being currently indicated for use by a subsequent

  refinement step (such as @{command_ref "apply"} or @{command_ref

  "proof"}).

  \item [@{command "unfolding"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}] is

  structurally similar to @{command "using"}, but unfolds definitional

  equations @{text "b\<^sub>1, \<dots> b\<^sub>n"} throughout the goal state

  and facts.

  \end{descr}

  Forward chaining with an empty list of theorems is the same as not

  chaining at all.  Thus ``@{command "from"}~@{text nothing}'' has no

  effect apart from entering @{text "prove(chain)"} mode, since

  @{fact_ref nothing} is bound to the empty list of theorems.

  Basic proof methods (such as @{method_ref rule}) expect multiple

  facts to be given in their proper order, corresponding to a prefix

  of the premises of the rule involved.  Note that positions may be

  easily skipped using something like @{command "from"}~@{text "_

  \<AND> a \<AND> b"}, for example.  This involves the trivial rule

  @{text "PROP \<psi> \<Longrightarrow> PROP \<psi>"}, which is bound in Isabelle/Pure as

  ``@{fact_ref "_"}'' (underscore).

  Automated methods (such as @{method simp} or @{method auto}) just

  insert any given facts before their usual operation.  Depending on

  the kind of procedure involved, the order of facts is less

  significant here.

*}

subsection {* Goal statements \label{sec:goals} *}

text {*

  \begin{matharray}{rcl}

    \isarcmd{lemma} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\

    \isarcmd{theorem} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\

    \isarcmd{corollary} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\

    \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\

    \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\

    \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\

    \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\

    \isarcmd{print_statement}^* & : & \isarkeep{theory~|~proof} \\

  \end{matharray}

  From a theory context, proof mode is entered by an initial goal

  command such as @{command "lemma"}, @{command "theorem"}, or

  @{command "corollary"}.  Within a proof, new claims may be

  introduced locally as well; four variants are available here to

  indicate whether forward chaining of facts should be performed

  initially (via @{command_ref "then"}), and whether the final result

  is meant to solve some pending goal.

  Goals may consist of multiple statements, resulting in a list of

  facts eventually.  A pending multi-goal is internally represented as

  a meta-level conjunction (printed as @{text "&&"}), which is usually

  split into the corresponding number of sub-goals prior to an initial

  method application, via @{command_ref "proof"}

  (\secref{sec:proof-steps}) or @{command_ref "apply"}

  (\secref{sec:tactic-commands}).  The @{method_ref induct} method

  covered in \secref{sec:cases-induct} acts on multiple claims

  simultaneously.

  Claims at the theory level may be either in short or long form.  A

  short goal merely consists of several simultaneous propositions

  (often just one).  A long goal includes an explicit context

  specification for the subsequent conclusion, involving local

  parameters and assumptions.  Here the role of each part of the

  statement is explicitly marked by separate keywords (see also

  \secref{sec:locale}); the local assumptions being introduced here

  are available as @{fact_ref assms} in the proof.  Moreover, there

  are two kinds of conclusions: @{element_def "shows"} states several

  simultaneous propositions (essentially a big conjunction), while

  @{element_def "obtains"} claims several simultaneous simultaneous

  contexts of (essentially a big disjunction of eliminated parameters

  and assumptions, cf.\ \secref{sec:obtain}).

  \begin{rail}

    ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal)

    ;

    ('have' | 'show' | 'hence' | 'thus') goal

    ;

    'print\_statement' modes? thmrefs

    ;

    goal: (props + 'and')

    ;

    longgoal: thmdecl? (contextelem *) conclusion

    ;

    conclusion: 'shows' goal | 'obtains' (parname? case + '|')

    ;

    case: (vars + 'and') 'where' (props + 'and')

    ;

  \end{rail}

  \begin{descr}

  \item [@{command "lemma"}~@{text "a: \<phi>"}] enters proof mode with

  @{text \<phi>} as main goal, eventually resulting in some fact @{text "\<turnstile>

  \<phi>"} to be put back into the target context.  An additional

  \railnonterm{context} specification may build up an initial proof

  context for the subsequent claim; this includes local definitions

  and syntax as well, see the definition of @{syntax contextelem} in

  \secref{sec:locale}.

  \item [@{command "theorem"}~@{text "a: \<phi>"} and @{command

  "corollary"}~@{text "a: \<phi>"}] are essentially the same as @{command

  "lemma"}~@{text "a: \<phi>"}, but the facts are internally marked as

  being of a different kind.  This discrimination acts like a formal

  comment.