summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Tue, 28 Nov 2000 16:21:51 +0100 | |

changeset 10534 | f3a17e35d976 |

parent 10533 | 909c473542f9 |

child 10535 | c00b1d0d46ac |

added a reference to {sec:products} for ordered pair reasoning

--- a/doc-src/TutorialI/Sets/sets.tex Tue Nov 28 01:48:07 2000 +0100 +++ b/doc-src/TutorialI/Sets/sets.tex Tue Nov 28 16:21:51 2000 +0100 @@ -841,13 +841,11 @@ \isacommand{done} \end{isabelle} -Note one detail. The {\isa{auto}} method can prove this but -{\isa{blast}} cannot. \REMARK{move to a later section?} -This is because the -lemmas we have proved only apply to ordered pairs. {\isa{Auto}} can -convert a bound variable of a product type into a pair of bound variables, -allowing the lemmas to be applied. A toy example demonstrates this -point: +Note one detail. The {\isa{auto}} method can prove this theorem, but +{\isa{blast}} cannot. +The lemmas we have proved apply only to ordered pairs, but {\isa{Auto}} +replaces a bound variable of product type by a pair of bound variables, +allowing the lemmas to be applied. A toy example demonstrates this point: \begin{isabelle} \isacommand{lemma}\ "A\ \isasymsubseteq\ Id"\isanewline \isacommand{apply}\ (rule\ subsetI)\isanewline @@ -861,15 +859,15 @@ \end{isabelle} The \isa{simp} and \isa{blast} methods can do nothing here. However, \isa{x} is of product type and therefore denotes an ordered pair. The -\isa{auto} method (and some others, including \isa{clarify}) -can replace +\isa{auto} method (and some others, including \isa{clarify}) replace \isa{x} by a pair, which then allows the further simplification from \isa{(a,b)\ \isasymin\ A} to \isa{a\ =\ b}. \begin{isabelle} A\ \isasymsubseteq\ Id\isanewline \ 1.\ {\isasymAnd}a\ b.\ (a,b)\ \isasymin\ A\ \isasymLongrightarrow\ a\ =\ b \end{isabelle} - +Section~\ref{sec:products} will discuss proof techniques for ordered pairs +in more detail. \section{Well-founded relations and induction}