doc-src/HOL/HOL.tex
 changeset 7328 4265615b4206 parent 7325 01bb8abb5a91 child 7490 9a74b57740d1
equal inserted replaced
7327:596318fdb379 7328:4265615b4206
  1853
  1853
  1854 \item Standard conversions (selectors or updates applied to record constructor
  1854 \item Standard conversions (selectors or updates applied to record constructor
  1855   terms, make function definitions) are part of the standard simpset (via
  1855   terms, make function definitions) are part of the standard simpset (via
  1856   \texttt{addsimps}).
  1856   \texttt{addsimps}).
  1857
  1857

  1858 \item Selectors applied to updated records are automatically reduced by

  1859   simplification procedure \ttindex{record_simproc}, which is part of the

  1860   default simpset.

  1861
  1858 \item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x'  1862 \item Inject equations of a form analogous to$((x, y) = (x', y')) \equiv x=x'
  1859   \conj y=y'$are made part of the standard simpset and claset (via  1863 \conj y=y'$ are made part of the standard simpset and claset (via
  1860   \texttt{addIffs}).
  1864   \texttt{addIffs}).
  1861
  1865
  1862 \item A tactic for record field splitting (\ttindex{record_split_tac}) is made
  1866 \item A tactic for record field splitting (\ttindex{record_split_tac}) may be
  1863   part of the standard claset (via \texttt{addSWrapper}).  This tactic is
  1867   made part of the claset (via \texttt{addSWrapper}).  This tactic is based on
  1864   based on rules analogous to $(\All x PROP~P~x) \equiv (\All{a~b} PROP~P(a,  1868 rules analogous to$(\All x PROP~P~x) \equiv (\All{a~b} PROP~P(a, b))$for  1865 b))$ for any field.
  1869   any field.
  1866 \end{enumerate}
  1870 \end{enumerate}
  1867
  1871
  1868 The first two kinds of rules are stored within the theory as $t\dtt simps$ and
  1872 The first two kinds of rules are stored within the theory as $t\dtt simps$ and
  1869 $t\dtt iffs$, respectively.  In some situations it might be appropriate to
  1873 $t\dtt iffs$, respectively.  In some situations it might be appropriate to
  1870 expand the definitions of updates: $t\dtt updates$.  Following a new trend in
  1874 expand the definitions of updates: $t\dtt update_defs$.  Note that these names
  1871 Isabelle system architecture, these names are \emph{not} bound at the {\ML}
  1875 are \emph{not} bound at the {\ML} level.
  1872 level, though.

  1873
  1876
  1874 \medskip
  1877 \medskip
  1875
  1878
  1876 The example theory \texttt{HOL/ex/Points} demonstrates typical proofs
  1879 The example theory \texttt{HOL/ex/Points} demonstrates typical proofs
  1877 concerning records.  The basic idea is to make \ttindex{record_split_tac}
  1880 concerning records.  The basic idea is to make \ttindex{record_split_tac}
  1878 expand quantified record variables and then simplify by the conversion rules.
  1881 expand quantified record variables and then simplify by the conversion rules.
  1879 By using a combination of the simplifier and classical prover together with
  1882 By using a combination of the simplifier and classical prover together with
  1880 the default simpset and claset, record problems should be solved with a single
  1883 the default simpset and claset, record problems should be solved with a single
  1881 stroke of \texttt{Auto_tac} or \texttt{Force_tac}.
  1884 stroke of \texttt{Auto_tac} or \texttt{Force_tac}.  Most of the time, plain

  1885 \texttt{Simp_tac} should be sufficient, though.
  1882
  1886
  1883
  1887
  1884 \section{Datatype definitions}
  1888 \section{Datatype definitions}
  1885 \label{sec:HOL:datatype}
  1889 \label{sec:HOL:datatype}
  1886 \index{*datatype|(}
  1890 \index{*datatype|(}