doc-src/HOL/HOL.tex
changeset 7328 4265615b4206
parent 7325 01bb8abb5a91
child 7490 9a74b57740d1
equal deleted 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|(}