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

author | paulson |

Fri, 29 Oct 2004 15:16:02 +0200 | |

changeset 15270 | 8b3f707a78a7 |

parent 15269 | f856f4f3258f |

child 15271 | 3c32a26510c4 |

fixed reference to renamed theorem

doc-src/TutorialI/Recdef/document/termination.tex | file | annotate | diff | comparison | revisions | |

doc-src/TutorialI/Recdef/termination.thy | file | annotate | diff | comparison | revisions |

--- a/doc-src/TutorialI/Recdef/document/termination.tex Thu Oct 28 19:40:22 2004 +0200 +++ b/doc-src/TutorialI/Recdef/document/termination.tex Fri Oct 29 15:16:02 2004 +0200 @@ -35,10 +35,9 @@ We can either prove this as a separate lemma, or try to figure out which existing lemmas may help. We opt for the second alternative. The theory of lists contains the simplification rule \isa{length\ {\isacharparenleft}filter\ P\ xs{\isacharparenright}\ {\isasymle}\ length\ xs}, -which is already -close to what we need, except that we still need to turn \mbox{\isa{{\isacharless}\ Suc}} +which is what we need, provided we turn \mbox{\isa{{\isacharless}\ Suc}} into -\isa{{\isasymle}} for the simplification rule to apply. Lemma +\isa{{\isasymle}} so that the rule applies. Lemma \isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} does just that: \isa{{\isacharparenleft}m\ {\isacharless}\ Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}m\ {\isasymle}\ n{\isacharparenright}}. Now we retry the above definition but supply the lemma(s) just found (or

--- a/doc-src/TutorialI/Recdef/termination.thy Thu Oct 28 19:40:22 2004 +0200 +++ b/doc-src/TutorialI/Recdef/termination.thy Fri Oct 29 15:16:02 2004 +0200 @@ -28,11 +28,10 @@ @{text[display]"length (filter ... xs) < Suc (length xs)"} We can either prove this as a separate lemma, or try to figure out which existing lemmas may help. We opt for the second alternative. The theory of -lists contains the simplification rule @{thm length_filter[no_vars]}, -which is already -close to what we need, except that we still need to turn \mbox{@{text"< Suc"}} +lists contains the simplification rule @{thm length_filter_le[no_vars]}, +which is what we need, provided we turn \mbox{@{text"< Suc"}} into -@{text"\<le>"} for the simplification rule to apply. Lemma +@{text"\<le>"} so that the rule applies. Lemma @{thm[source]less_Suc_eq_le} does just that: @{thm less_Suc_eq_le[no_vars]}. Now we retry the above definition but supply the lemma(s) just found (or