# HG changeset patch # User paulson # Date 997275028 -7200 # Node ID 0fba0357c04c8fe29b7d378b2f6bd5c58b082b57 # Parent 697dcaaf478ff06cadf2dab76031024506e01754 Getting it working again with 1' instead of 1 diff -r 697dcaaf478f -r 0fba0357c04c doc-src/TutorialI/Recdef/document/examples.tex --- a/doc-src/TutorialI/Recdef/document/examples.tex Wed Aug 08 14:33:10 2001 +0200 +++ b/doc-src/TutorialI/Recdef/document/examples.tex Wed Aug 08 14:50:28 2001 +0200 @@ -8,7 +8,7 @@ \isacommand{consts}\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline \isacommand{recdef}\ fib\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline \ \ {\isachardoublequote}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline -\ \ {\isachardoublequote}fib\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}\isanewline +\ \ {\isachardoublequote}fib\ {\isadigit{1}}{\isacharprime}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}\isanewline \ \ {\isachardoublequote}fib\ {\isacharparenleft}Suc{\isacharparenleft}Suc\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ x\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ x{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent diff -r 697dcaaf478f -r 0fba0357c04c doc-src/TutorialI/Recdef/examples.thy --- a/doc-src/TutorialI/Recdef/examples.thy Wed Aug 08 14:33:10 2001 +0200 +++ b/doc-src/TutorialI/Recdef/examples.thy Wed Aug 08 14:50:28 2001 +0200 @@ -9,7 +9,7 @@ consts fib :: "nat \ nat"; recdef fib "measure(\n. n)" "fib 0 = 0" - "fib 1 = 1" + "fib 1' = 1" "fib (Suc(Suc x)) = fib x + fib (Suc x)"; text{*\noindent diff -r 697dcaaf478f -r 0fba0357c04c doc-src/TutorialI/Rules/Forward.thy --- a/doc-src/TutorialI/Rules/Forward.thy Wed Aug 08 14:33:10 2001 +0200 +++ b/doc-src/TutorialI/Rules/Forward.thy Wed Aug 08 14:50:28 2001 +0200 @@ -21,12 +21,12 @@ apply (simp add: is_gcd) done -lemma gcd_1 [simp]: "gcd(m,1) = 1" +lemma gcd_1 [simp]: "gcd(m,1') = 1'" apply simp done -lemma gcd_1_left [simp]: "gcd(1,m) = 1" -apply (simp add: gcd_commute [of 1]) +lemma gcd_1_left [simp]: "gcd(1',m) = 1'" +apply (simp add: gcd_commute [of "1'"]) done text{*\noindent diff -r 697dcaaf478f -r 0fba0357c04c doc-src/TutorialI/Rules/rules.tex --- a/doc-src/TutorialI/Rules/rules.tex Wed Aug 08 14:33:10 2001 +0200 +++ b/doc-src/TutorialI/Rules/rules.tex Wed Aug 08 14:50:28 2001 +0200 @@ -1819,7 +1819,7 @@ appearance from left to right. In this case, the variables are \isa{?k}, \isa{?m} and~\isa{?n}. So, the expression \hbox{\texttt{[of k 1]}} replaces \isa{?k} by~\isa{k} and \isa{?m} -by~\isa{1}. +by~\isa{1}.\REMARK{which 1 do we use?? (right the way down)} \begin{isabelle} \isacommand{lemmas}\ gcd_mult_0\ =\ gcd_mult_distrib2\ [of\ k\ 1] \end{isabelle} diff -r 697dcaaf478f -r 0fba0357c04c doc-src/TutorialI/Trie/document/Trie.tex --- a/doc-src/TutorialI/Trie/document/Trie.tex Wed Aug 08 14:33:10 2001 +0200 +++ b/doc-src/TutorialI/Trie/document/Trie.tex Wed Aug 08 14:50:28 2001 +0200 @@ -12,6 +12,7 @@ \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie\ {\isacharequal}\ Trie\ \ {\isachardoublequote}{\isacharprime}v\ option{\isachardoublequote}\ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie{\isacharparenright}list{\isachardoublequote}% \begin{isamarkuptext}% \noindent +\index{datatypes!and nested recursion}% The first component is the optional value, the second component the association list of subtries. This is an example of nested recursion involving products, which is fine because products are datatypes as well. @@ -90,11 +91,11 @@ \noindent Our plan is to induct on \isa{as}; hence the remaining variables are quantified. From the definitions it is clear that induction on either -\isa{as} or \isa{bs} is required. The choice of \isa{as} is merely +\isa{as} or \isa{bs} is required. The choice of \isa{as} is guided by the intuition that simplification of \isa{lookup} might be easier if \isa{update} has already been simplified, which can only happen if \isa{as} is instantiated. -The start of the proof is completely conventional:% +The start of the proof is conventional:% \end{isamarkuptxt}% \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ as{\isacharcomma}\ auto{\isacharparenright}% \begin{isamarkuptxt}% @@ -113,6 +114,7 @@ \isacommand{done}% \begin{isamarkuptext}% \noindent +\index{subgoal numbering}% All methods ending in \isa{tac} take an optional first argument that specifies the range of subgoals they are applied to, where \isa{{\isacharbrackleft}{\isacharbang}{\isacharbrackright}} means all subgoals, i.e.\ \isa{{\isacharbrackleft}{\isadigit{1}}{\isacharminus}{\isadigit{3}}{\isacharbrackright}} in our case. Individual subgoal numbers, @@ -123,8 +125,7 @@ proof states are invisible, and we rely on the (possibly brittle) magic of \isa{auto} (\isa{simp{\isacharunderscore}all} will not do --- try it) to split the subgoals of the induction up in such a way that case distinction on \isa{bs} makes -sense and solves the proof. Chapter~\ref{ch:Isar} shows you how to write readable -and stable proofs. +sense and solves the proof. \begin{exercise} Modify \isa{update} (and its type) such that it allows both insertion and diff -r 697dcaaf478f -r 0fba0357c04c doc-src/TutorialI/Types/Numbers.thy --- a/doc-src/TutorialI/Types/Numbers.thy Wed Aug 08 14:33:10 2001 +0200 +++ b/doc-src/TutorialI/Types/Numbers.thy Wed Aug 08 14:50:28 2001 +0200 @@ -83,8 +83,10 @@ *} -lemma "(n-1)*(n+1) = n*n - 1" -apply (simp split: nat_diff_split) +lemma "(n-#2)*(n+#2) = n*n - (#4::nat)" +apply (clarsimp split: nat_diff_split) + --{* @{subgoals[display,indent=0,margin=65]} *} +apply (subgoal_tac "n=0 | n=1", force, arith) done text{* diff -r 697dcaaf478f -r 0fba0357c04c doc-src/TutorialI/Types/document/Numbers.tex --- a/doc-src/TutorialI/Types/document/Numbers.tex Wed Aug 08 14:33:10 2001 +0200 +++ b/doc-src/TutorialI/Types/document/Numbers.tex Wed Aug 08 14:50:28 2001 +0200 @@ -113,8 +113,15 @@ \end{isabelle} \rulename{nat_diff_split}% \end{isamarkuptext}% -\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}n{\isacharminus}{\isadigit{1}}{\isacharparenright}{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}n\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequote}\isanewline -\isacommand{apply}\ {\isacharparenleft}simp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline +\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}n{\isacharminus}{\isacharhash}{\isadigit{2}}{\isacharparenright}{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isacharhash}{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}n\ {\isacharminus}\ {\isacharparenleft}{\isacharhash}{\isadigit{4}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline +\isacommand{apply}\ {\isacharparenleft}clarsimp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline +\ % +\isamarkupcmt{\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}d{\isachardot}\ {\isasymlbrakk}n\ {\isacharless}\ {\isacharhash}{\isadigit{2}}{\isacharsemicolon}\ n\ {\isacharasterisk}\ n\ {\isacharequal}\ {\isacharhash}{\isadigit{4}}\ {\isacharplus}\ d{\isasymrbrakk}\ {\isasymLongrightarrow}\ d\ {\isacharequal}\ {\isadigit{0}}% +\end{isabelle}% +} +\isanewline +\isacommand{apply}\ {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}n{\isacharequal}{\isadigit{0}}\ {\isacharbar}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}{\isacharcomma}\ force{\isacharcomma}\ arith{\isacharparenright}\isanewline \isacommand{done}% \begin{isamarkuptext}% \begin{isabelle}% diff -r 697dcaaf478f -r 0fba0357c04c doc-src/TutorialI/Types/numerics.tex --- a/doc-src/TutorialI/Types/numerics.tex Wed Aug 08 14:33:10 2001 +0200 +++ b/doc-src/TutorialI/Types/numerics.tex Wed Aug 08 14:50:28 2001 +0200 @@ -225,7 +225,7 @@ \rulename{nat_diff_split} \end{isabelle} For example, it proves the following fact, which lies outside the scope of -linear arithmetic: +linear arithmetic:\REMARK{replace by new example!} \begin{isabelle} \isacommand{lemma}\ "(n-1)*(n+1)\ =\ n*n\ -\ 1"\isanewline \isacommand{apply}\ (simp\ split:\ nat_diff_split)\isanewline