doc-src/IsarRef/Thy/Outer_Syntax.thy
changeset 28754 6f2e67a3dfaa
parent 28753 b5926a48c943
child 28762 f5d79aeffd81
     1.1 --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu Nov 13 21:34:55 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu Nov 13 21:37:18 2008 +0100
     1.3 @@ -262,6 +262,51 @@
     1.4  *}
     1.5  
     1.6  
     1.7 +subsection {* Term patterns and declarations \label{sec:term-decls} *}
     1.8 +
     1.9 +text {*
    1.10 +  Wherever explicit propositions (or term fragments) occur in a proof
    1.11 +  text, casual binding of schematic term variables may be given
    1.12 +  specified via patterns of the form ``@{text "(\<IS> p\<^sub>1 \<dots>
    1.13 +  p\<^sub>n)"}''.  This works both for \railqtok{term} and \railqtok{prop}.
    1.14 +
    1.15 +  \indexouternonterm{termpat}\indexouternonterm{proppat}
    1.16 +  \begin{rail}
    1.17 +    termpat: '(' ('is' term +) ')'
    1.18 +    ;
    1.19 +    proppat: '(' ('is' prop +) ')'
    1.20 +    ;
    1.21 +  \end{rail}
    1.22 +
    1.23 +  \medskip Declarations of local variables @{text "x :: \<tau>"} and
    1.24 +  logical propositions @{text "a : \<phi>"} represent different views on
    1.25 +  the same principle of introducing a local scope.  In practice, one
    1.26 +  may usually omit the typing of \railnonterm{vars} (due to
    1.27 +  type-inference), and the naming of propositions (due to implicit
    1.28 +  references of current facts).  In any case, Isar proof elements
    1.29 +  usually admit to introduce multiple such items simultaneously.
    1.30 +
    1.31 +  \indexouternonterm{vars}\indexouternonterm{props}
    1.32 +  \begin{rail}
    1.33 +    vars: (name+) ('::' type)?
    1.34 +    ;
    1.35 +    props: thmdecl? (prop proppat? +)
    1.36 +    ;
    1.37 +  \end{rail}
    1.38 +
    1.39 +  The treatment of multiple declarations corresponds to the
    1.40 +  complementary focus of \railnonterm{vars} versus
    1.41 +  \railnonterm{props}.  In ``@{text "x\<^sub>1 \<dots> x\<^sub>n :: \<tau>"}''
    1.42 +  the typing refers to all variables, while in @{text "a: \<phi>\<^sub>1 \<dots>
    1.43 +  \<phi>\<^sub>n"} the naming refers to all propositions collectively.
    1.44 +  Isar language elements that refer to \railnonterm{vars} or
    1.45 +  \railnonterm{props} typically admit separate typings or namings via
    1.46 +  another level of iteration, with explicit @{keyword_ref "and"}
    1.47 +  separators; e.g.\ see @{command "fix"} and @{command "assume"} in
    1.48 +  \secref{sec:proof-context}.
    1.49 +*}
    1.50 +
    1.51 +
    1.52  subsection {* Mixfix annotations *}
    1.53  
    1.54  text {*
    1.55 @@ -314,7 +359,7 @@
    1.56    pattern.  Printing a nested application @{text "c t\<^sub>1 \<dots> t\<^sub>m"} for
    1.57    @{text "m > n"} works by attaching concrete notation only to the
    1.58    innermost part, essentially by printing @{text "(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m"}
    1.59 -  instead.  If a term has fewer argument than specified in the mixfix
    1.60 +  instead.  If a term has fewer arguments than specified in the mixfix
    1.61    template, the concrete syntax is ignored.
    1.62  
    1.63    \medskip A mixfix template may also contain additional directives
    1.64 @@ -366,69 +411,22 @@
    1.65    For example, the template @{text "(_ +/ _)"} specifies an infix
    1.66    operator.  There are two argument positions; the delimiter @{text
    1.67    "+"} is preceded by a space and followed by a space or line break;
    1.68 -  the entire phrase is a pretty printing block.  
    1.69 +  the entire phrase is a pretty printing block.
    1.70  
    1.71    The general idea of pretty printing with blocks and breaks is also
    1.72    described in \cite{paulson-ml2}.
    1.73  *}
    1.74  
    1.75  
    1.76 -subsection {* Proof methods \label{sec:syn-meth} *}
    1.77 -
    1.78 -text {*
    1.79 -  Proof methods are either basic ones, or expressions composed of
    1.80 -  methods via ``@{verbatim ","}'' (sequential composition),
    1.81 -  ``@{verbatim "|"}'' (alternative choices), ``@{verbatim "?"}'' 
    1.82 -  (try), ``@{verbatim "+"}'' (repeat at least once), ``@{verbatim
    1.83 -  "["}@{text n}@{verbatim "]"}'' (restriction to first @{text n}
    1.84 -  sub-goals, with default @{text "n = 1"}).  In practice, proof
    1.85 -  methods are usually just a comma separated list of
    1.86 -  \railqtok{nameref}~\railnonterm{args} specifications.  Note that
    1.87 -  parentheses may be dropped for single method specifications (with no
    1.88 -  arguments).
    1.89 -
    1.90 -  \indexouternonterm{method}
    1.91 -  \begin{rail}
    1.92 -    method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']')
    1.93 -    ;
    1.94 -    methods: (nameref args | method) + (',' | '|')
    1.95 -    ;
    1.96 -  \end{rail}
    1.97 -
    1.98 -  Proper Isar proof methods do \emph{not} admit arbitrary goal
    1.99 -  addressing, but refer either to the first sub-goal or all sub-goals
   1.100 -  uniformly.  The goal restriction operator ``@{text "[n]"}''
   1.101 -  evaluates a method expression within a sandbox consisting of the
   1.102 -  first @{text n} sub-goals (which need to exist).  For example, the
   1.103 -  method ``@{text "simp_all[3]"}'' simplifies the first three
   1.104 -  sub-goals, while ``@{text "(rule foo, simp_all)[]"}'' simplifies all
   1.105 -  new goals that emerge from applying rule @{text "foo"} to the
   1.106 -  originally first one.
   1.107 -
   1.108 -  Improper methods, notably tactic emulations, offer a separate
   1.109 -  low-level goal addressing scheme as explicit argument to the
   1.110 -  individual tactic being involved.  Here ``@{text "[!]"}'' refers to
   1.111 -  all goals, and ``@{text "[n-]"}'' to all goals starting from @{text
   1.112 -  "n"}.
   1.113 -
   1.114 -  \indexouternonterm{goalspec}
   1.115 -  \begin{rail}
   1.116 -    goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
   1.117 -    ;
   1.118 -  \end{rail}
   1.119 -*}
   1.120 -
   1.121 -
   1.122  subsection {* Attributes and theorems \label{sec:syn-att} *}
   1.123  
   1.124 -text {*
   1.125 -  Attributes (and proof methods, see \secref{sec:syn-meth}) have their
   1.126 -  own ``semi-inner'' syntax, in the sense that input conforming to
   1.127 -  \railnonterm{args} below is parsed by the attribute a second time.
   1.128 -  The attribute argument specifications may be any sequence of atomic
   1.129 -  entities (identifiers, strings etc.), or properly bracketed argument
   1.130 -  lists.  Below \railqtok{atom} refers to any atomic entity, including
   1.131 -  any \railtok{keyword} conforming to \railtok{symident}.
   1.132 +text {* Attributes have their own ``semi-inner'' syntax, in the sense
   1.133 +  that input conforming to \railnonterm{args} below is parsed by the
   1.134 +  attribute a second time.  The attribute argument specifications may
   1.135 +  be any sequence of atomic entities (identifiers, strings etc.), or
   1.136 +  properly bracketed argument lists.  Below \railqtok{atom} refers to
   1.137 +  any atomic entity, including any \railtok{keyword} conforming to
   1.138 +  \railtok{symident}.
   1.139  
   1.140    \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
   1.141    \begin{rail}
   1.142 @@ -459,7 +457,7 @@
   1.143  
   1.144    \item literal fact propositions using @{syntax_ref altstring} syntax
   1.145    @{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} (see also method
   1.146 -  @{method_ref fact} in \secref{sec:pure-meth-att}).
   1.147 +  @{method_ref fact}).
   1.148  
   1.149    \end{enumerate}
   1.150  
   1.151 @@ -498,49 +496,4 @@
   1.152    \end{rail}
   1.153  *}
   1.154  
   1.155 -
   1.156 -subsection {* Term patterns and declarations \label{sec:term-decls} *}
   1.157 -
   1.158 -text {*
   1.159 -  Wherever explicit propositions (or term fragments) occur in a proof
   1.160 -  text, casual binding of schematic term variables may be given
   1.161 -  specified via patterns of the form ``@{text "(\<IS> p\<^sub>1 \<dots>
   1.162 -  p\<^sub>n)"}''.  This works both for \railqtok{term} and \railqtok{prop}.
   1.163 -
   1.164 -  \indexouternonterm{termpat}\indexouternonterm{proppat}
   1.165 -  \begin{rail}
   1.166 -    termpat: '(' ('is' term +) ')'
   1.167 -    ;
   1.168 -    proppat: '(' ('is' prop +) ')'
   1.169 -    ;
   1.170 -  \end{rail}
   1.171 -
   1.172 -  \medskip Declarations of local variables @{text "x :: \<tau>"} and
   1.173 -  logical propositions @{text "a : \<phi>"} represent different views on
   1.174 -  the same principle of introducing a local scope.  In practice, one
   1.175 -  may usually omit the typing of \railnonterm{vars} (due to
   1.176 -  type-inference), and the naming of propositions (due to implicit
   1.177 -  references of current facts).  In any case, Isar proof elements
   1.178 -  usually admit to introduce multiple such items simultaneously.
   1.179 -
   1.180 -  \indexouternonterm{vars}\indexouternonterm{props}
   1.181 -  \begin{rail}
   1.182 -    vars: (name+) ('::' type)?
   1.183 -    ;
   1.184 -    props: thmdecl? (prop proppat? +)
   1.185 -    ;
   1.186 -  \end{rail}
   1.187 -
   1.188 -  The treatment of multiple declarations corresponds to the
   1.189 -  complementary focus of \railnonterm{vars} versus
   1.190 -  \railnonterm{props}.  In ``@{text "x\<^sub>1 \<dots> x\<^sub>n :: \<tau>"}''
   1.191 -  the typing refers to all variables, while in @{text "a: \<phi>\<^sub>1 \<dots>
   1.192 -  \<phi>\<^sub>n"} the naming refers to all propositions collectively.
   1.193 -  Isar language elements that refer to \railnonterm{vars} or
   1.194 -  \railnonterm{props} typically admit separate typings or namings via
   1.195 -  another level of iteration, with explicit @{keyword_ref "and"}
   1.196 -  separators; e.g.\ see @{command "fix"} and @{command "assume"} in
   1.197 -  \secref{sec:proof-context}.
   1.198 -*}
   1.199 -
   1.200  end