# HG changeset patch # User nipkow # Date 971794742 -7200 # Node ID 875bf54b5d74fbff152694ed1e5c4f639f12e04e # Parent 7626cb4e14079ce70ce62dcf5d4995f5d802bef4 *** empty log message *** diff -r 7626cb4e1407 -r 875bf54b5d74 doc-src/TutorialI/CTL/CTL.thy --- a/doc-src/TutorialI/CTL/CTL.thy Tue Oct 17 13:28:57 2000 +0200 +++ b/doc-src/TutorialI/CTL/CTL.thy Tue Oct 17 16:59:02 2000 +0200 @@ -181,9 +181,9 @@ done; text{*\noindent -is proved by a variant of contraposition (@{thm[source]contrapos_np}: -@{thm contrapos_np[no_vars]}), i.e.\ assuming the negation of the conclusion -and proving @{term"s : lfp(af A)"}. Unfolding @{term lfp} once and +is proved by a variant of contraposition: +assume the negation of the conclusion and prove @{term"s : lfp(af A)"}. +Unfolding @{term lfp} once and simplifying with the definition of @{term af} finishes the proof. Now we iterate this process. The following construction of the desired @@ -333,8 +333,7 @@ "{s. \ p \ Paths s. \ i. p i \ A} \ lfp(af A)"; txt{*\noindent -The proof is again pointwise and then by contraposition (@{thm[source]contrapos_pp} is the rule -@{thm contrapos_pp}): +The proof is again pointwise and then by contraposition: *}; apply(rule subsetI); diff -r 7626cb4e1407 -r 875bf54b5d74 doc-src/TutorialI/CTL/document/CTL.tex --- a/doc-src/TutorialI/CTL/document/CTL.tex Tue Oct 17 13:28:57 2000 +0200 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Tue Oct 17 16:59:02 2000 +0200 @@ -117,15 +117,15 @@ \end{isamarkuptext}% \isacommand{lemma}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharcolon}\isanewline \ {\isachardoublequote}s\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ s\ {\isasymnotin}\ A\ {\isasymand}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}{\isasymin}M\ {\isasymand}\ t\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline -\isacommand{apply}{\isacharparenleft}erule\ swap{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}np{\isacharparenright}\isanewline \isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\isacharparenright}\isanewline \isacommand{done}% \begin{isamarkuptext}% \noindent -is proved by a variant of contraposition (\isa{swap}: -\isa{{\isasymlbrakk}{\isasymnot}\ Q{\isacharsemicolon}\ {\isasymnot}\ P\ {\isasymLongrightarrow}\ Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ P}), i.e.\ assuming the negation of the conclusion -and proving \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Unfolding \isa{lfp} once and +is proved by a variant of contraposition: +assume the negation of the conclusion and prove \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. +Unfolding \isa{lfp} once and simplifying with the definition of \isa{af} finishes the proof. Now we iterate this process. The following construction of the desired @@ -244,11 +244,10 @@ {\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptxt}% \noindent -The proof is again pointwise and then by contraposition (\isa{contrapos{\isadigit{2}}} is the rule -\isa{{\isasymlbrakk}{\isacharquery}Q{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P\ {\isasymLongrightarrow}\ {\isasymnot}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P}):% +The proof is again pointwise and then by contraposition:% \end{isamarkuptxt}% \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isadigit{2}}{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline \isacommand{apply}\ simp% \begin{isamarkuptxt}% \begin{isabelle} diff -r 7626cb4e1407 -r 875bf54b5d74 doc-src/TutorialI/Inductive/AB.thy --- a/doc-src/TutorialI/Inductive/AB.thy Tue Oct 17 13:28:57 2000 +0200 +++ b/doc-src/TutorialI/Inductive/AB.thy Tue Oct 17 16:59:02 2000 +0200 @@ -68,15 +68,14 @@ lemma correctness: "(w \ S \ size[x\w. x=a] = size[x\w. x=b]) \ - (w \ A \ size[x\w. x=a] = size[x\w. x=b] + 1) \ - (w \ B \ size[x\w. x=b] = size[x\w. x=a] + 1)" + (w \ A \ size[x\w. x=a] = size[x\w. x=b] + 1) \ + (w \ B \ size[x\w. x=b] = size[x\w. x=a] + 1)" txt{*\noindent These propositions are expressed with the help of the predefined @{term filter} function on lists, which has the convenient syntax @{term"[x\xs. P x]"}, the list of all elements @{term x} in @{term xs} such that @{prop"P x"} -holds. The length of a list is usually written @{term length}, and @{term -size} is merely a shorthand. +holds. Remember that on lists @{term size} and @{term length} are synonymous. The proof itself is by rule induction and afterwards automatic: *} @@ -193,8 +192,8 @@ theorem completeness: "(size[x\w. x=a] = size[x\w. x=b] \ w \ S) \ - (size[x\w. x=a] = size[x\w. x=b] + 1 \ w \ A) \ - (size[x\w. x=b] = size[x\w. x=a] + 1 \ w \ B)"; + (size[x\w. x=a] = size[x\w. x=b] + 1 \ w \ A) \ + (size[x\w. x=b] = size[x\w. x=a] + 1 \ w \ B)"; txt{*\noindent The proof is by induction on @{term w}. Structural induction would fail here diff -r 7626cb4e1407 -r 875bf54b5d74 doc-src/TutorialI/Inductive/Star.thy --- a/doc-src/TutorialI/Inductive/Star.thy Tue Oct 17 13:28:57 2000 +0200 +++ b/doc-src/TutorialI/Inductive/Star.thy Tue Oct 17 16:59:02 2000 +0200 @@ -1,9 +1,9 @@ (*<*)theory Star = Main:(*>*) -section{*The transitive and reflexive closure*} +section{*The reflexive transitive closure*} text{* -A perfect example of an inductive definition is the transitive, reflexive +A perfect example of an inductive definition is the reflexive transitive closure of a relation. This concept was already introduced in \S\ref{sec:rtrancl}, but it was not shown how it is defined. In fact, the operator @{text"^*"} is not defined inductively but via a least @@ -11,46 +11,52 @@ inductive definitions are not yet available. But now they are: *} -consts trc :: "('a \ 'a)set \ ('a \ 'a)set" ("_*" [1000] 999) +consts rtc :: "('a \ 'a)set \ ('a \ 'a)set" ("_*" [1000] 999) inductive "r*" intros -trc_refl[intro!]: "(x,x) \ r*" -trc_step: "\ (x,y) \ r*; (y,z) \ r \ \ (x,z) \ r*" +rtc_refl[intro!]: "(x,x) \ r*" +rtc_step: "\ (x,y) \ r*; (y,z) \ r \ \ (x,z) \ r*" lemma [intro]: "(x,y) : r \ (x,y) \ r*" -by(blast intro: trc_step); +by(blast intro: rtc_step); lemma step2[rule_format]: "(y,z) \ r* \ (x,y) \ r \ (x,z) \ r*" -apply(erule trc.induct) +apply(erule rtc.induct) apply(blast); -apply(blast intro: trc_step); +apply(blast intro: rtc_step); done -lemma trc_trans[rule_format]: +lemma rtc_trans[rule_format]: "(x,y) \ r* \ \z. (y,z) \ r* \ (x,z) \ r*" -apply(erule trc.induct) +apply(erule rtc.induct) apply blast; apply(blast intro: step2); done -consts trc2 :: "('a \ 'a)set \ ('a \ 'a)set" -inductive "trc2 r" +consts rtc2 :: "('a \ 'a)set \ ('a \ 'a)set" +inductive "rtc2 r" intros -"(x,y) \ r \ (x,y) \ trc2 r" -"(x,x) \ trc2 r" -"\ (x,y) \ trc2 r; (y,z) \ trc2 r \ \ (x,z) \ trc2 r" +"(x,y) \ r \ (x,y) \ rtc2 r" +"(x,x) \ rtc2 r" +"\ (x,y) \ rtc2 r; (y,z) \ rtc2 r \ \ (x,z) \ rtc2 r" +text{* +The equivalence of the two definitions is easily shown by the obvious rule +inductions: +*} -lemma "((x,y) \ trc2 r) = ((x,y) \ r*)" -apply(rule iffI); - apply(erule trc2.induct); - apply(blast); +lemma "(x,y) \ rtc2 r \ (x,y) \ r*" +apply(erule rtc2.induct); apply(blast); - apply(blast intro: trc_trans); -apply(erule trc.induct); - apply(blast intro: trc2.intros); -apply(blast intro: trc2.intros); + apply(blast); +apply(blast intro: rtc_trans); +done + +lemma "(x,y) \ r* \ (x,y) \ rtc2 r" +apply(erule rtc.induct); + apply(blast intro: rtc2.intros); +apply(blast intro: rtc2.intros); done (*<*)end(*>*) diff -r 7626cb4e1407 -r 875bf54b5d74 doc-src/TutorialI/Inductive/document/AB.tex --- a/doc-src/TutorialI/Inductive/document/AB.tex Tue Oct 17 13:28:57 2000 +0200 +++ b/doc-src/TutorialI/Inductive/document/AB.tex Tue Oct 17 16:59:02 2000 +0200 @@ -63,12 +63,12 @@ \end{isamarkuptext}% \isacommand{lemma}\ correctness{\isacharcolon}\isanewline \ \ {\isachardoublequote}{\isacharparenleft}w\ {\isasymin}\ S\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}{\isacharparenright}\ \ \ \ \ {\isasymand}\isanewline -\ \ \ \ {\isacharparenleft}w\ {\isasymin}\ A\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isasymand}\isanewline -\ \ \ \ {\isacharparenleft}w\ {\isasymin}\ B\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}% +\ \ \ {\isacharparenleft}w\ {\isasymin}\ A\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isasymand}\isanewline +\ \ \ {\isacharparenleft}w\ {\isasymin}\ B\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptxt}% \noindent These propositions are expressed with the help of the predefined \isa{filter} function on lists, which has the convenient syntax \isa{filter\ P\ xs}, the list of all elements \isa{x} in \isa{xs} such that \isa{P\ x} -holds. The length of a list is usually written \isa{size}, and \isa{size} is merely a shorthand. +holds. Remember that on lists \isa{size} and \isa{size} are synonymous. The proof itself is by rule induction and afterwards automatic:% \end{isamarkuptxt}% @@ -177,8 +177,8 @@ \end{isamarkuptext}% \isacommand{theorem}\ completeness{\isacharcolon}\isanewline \ \ {\isachardoublequote}{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ \ \ \ \ {\isasymlongrightarrow}\ w\ {\isasymin}\ S{\isacharparenright}\ {\isasymand}\isanewline -\ \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ A{\isacharparenright}\ {\isasymand}\isanewline -\ \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ B{\isacharparenright}{\isachardoublequote}% +\ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ A{\isacharparenright}\ {\isasymand}\isanewline +\ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ B{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptxt}% \noindent The proof is by induction on \isa{w}. Structural induction would fail here diff -r 7626cb4e1407 -r 875bf54b5d74 doc-src/TutorialI/Inductive/document/Star.tex --- a/doc-src/TutorialI/Inductive/document/Star.tex Tue Oct 17 13:28:57 2000 +0200 +++ b/doc-src/TutorialI/Inductive/document/Star.tex Tue Oct 17 16:59:02 2000 +0200 @@ -2,56 +2,60 @@ \begin{isabellebody}% \def\isabellecontext{Star}% % -\isamarkupsection{The transitive and reflexive closure} +\isamarkupsection{The reflexive transitive closure} % \begin{isamarkuptext}% -A perfect example of an inductive definition is the transitive, reflexive +A perfect example of an inductive definition is the reflexive transitive closure of a relation. This concept was already introduced in \S\ref{sec:rtrancl}, but it was not shown how it is defined. In fact, the operator \isa{{\isacharcircum}{\isacharasterisk}} is not defined inductively but via a least fixpoint because at that point in the theory hierarchy inductive definitions are not yet available. But now they are:% \end{isamarkuptext}% -\isacommand{consts}\ trc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\ \ {\isacharparenleft}{\isachardoublequote}{\isacharunderscore}{\isacharasterisk}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline +\isacommand{consts}\ rtc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\ \ {\isacharparenleft}{\isachardoublequote}{\isacharunderscore}{\isacharasterisk}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline \isacommand{inductive}\ {\isachardoublequote}r{\isacharasterisk}{\isachardoublequote}\isanewline \isakeyword{intros}\isanewline -trc{\isacharunderscore}refl{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline -trc{\isacharunderscore}step{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline +rtc{\isacharunderscore}refl{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline +rtc{\isacharunderscore}step{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline \isanewline \isacommand{lemma}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharcolon}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline -\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isacharunderscore}step{\isacharparenright}\isanewline +\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isanewline \isanewline \isacommand{lemma}\ step{\isadigit{2}}{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline \ \ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ \ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline -\isacommand{apply}{\isacharparenleft}erule\ trc{\isachardot}induct{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isacharunderscore}step{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isanewline \isacommand{done}\isanewline \isanewline -\isacommand{lemma}\ trc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline +\isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline \ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ \ {\isasymLongrightarrow}\ {\isasymforall}z{\isachardot}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline -\isacommand{apply}{\isacharparenleft}erule\ trc{\isachardot}induct{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline \ \isacommand{apply}\ blast\isanewline \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ step{\isadigit{2}}{\isacharparenright}\isanewline \isacommand{done}\isanewline \isanewline -\isacommand{consts}\ trc{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\isanewline -\isacommand{inductive}\ {\isachardoublequote}trc{\isadigit{2}}\ r{\isachardoublequote}\isanewline +\isacommand{consts}\ rtc{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\isanewline +\isacommand{inductive}\ {\isachardoublequote}rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline \isakeyword{intros}\isanewline -{\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ trc{\isadigit{2}}\ r{\isachardoublequote}\isanewline -{\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ trc{\isadigit{2}}\ r{\isachardoublequote}\isanewline -{\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ trc{\isadigit{2}}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ trc{\isadigit{2}}\ r\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ trc{\isadigit{2}}\ r{\isachardoublequote}\isanewline -\isanewline +{\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline +{\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline +{\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}% +\begin{isamarkuptext}% +The equivalence of the two definitions is easily shown by the obvious rule +inductions:% +\end{isamarkuptext}% +\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline +\isacommand{apply}{\isacharparenleft}erule\ rtc{\isadigit{2}}{\isachardot}induct{\isacharparenright}\isanewline +\ \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}trans{\isacharparenright}\isanewline +\isacommand{done}\isanewline \isanewline -\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ trc{\isadigit{2}}\ r{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharparenright}{\isachardoublequote}\isanewline -\isacommand{apply}{\isacharparenleft}rule\ iffI{\isacharparenright}\isanewline -\ \isacommand{apply}{\isacharparenleft}erule\ trc{\isadigit{2}}{\isachardot}induct{\isacharparenright}\isanewline -\ \ \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline -\ \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline -\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isacharunderscore}trans{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}erule\ trc{\isachardot}induct{\isacharparenright}\isanewline -\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline +\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline +\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline \isacommand{done}\isanewline \end{isabellebody}% %%% Local Variables: diff -r 7626cb4e1407 -r 875bf54b5d74 doc-src/TutorialI/fp.tex --- a/doc-src/TutorialI/fp.tex Tue Oct 17 13:28:57 2000 +0200 +++ b/doc-src/TutorialI/fp.tex Tue Oct 17 16:59:02 2000 +0200 @@ -188,11 +188,12 @@ Every datatype $t$ comes equipped with a \isa{size} function from $t$ into the natural numbers (see~\S\ref{sec:nat} below). For lists, \isa{size} is just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs + - 1}. In general, \isa{size} returns \isa{0} for all constructors that do -not have an argument of type $t$, and for all other constructors \isa{1 +} -the sum of the sizes of all arguments of type $t$. Note that because + 1}. In general, \isaindexbold{size} returns \isa{0} for all constructors +that do not have an argument of type $t$, and for all other constructors +\isa{1 +} the sum of the sizes of all arguments of type $t$. Note that because \isa{size} is defined on every datatype, it is overloaded; on lists -\isa{size} is also called \isa{length}, which is not overloaded. +\isa{size} is also called \isaindexbold{length}, which is not overloaded. +Isbelle will always show \isa{size} on lists as \isa{length}. \subsection{Primitive recursion} diff -r 7626cb4e1407 -r 875bf54b5d74 doc-src/TutorialI/todo.tobias --- a/doc-src/TutorialI/todo.tobias Tue Oct 17 13:28:57 2000 +0200 +++ b/doc-src/TutorialI/todo.tobias Tue Oct 17 16:59:02 2000 +0200 @@ -50,9 +50,6 @@ an example of induction: !y. A --> B --> C ?? -Advanced Ind expects rule_format incl (no_asm) (which it currently explains! -Where explained? - Appendix: Lexical: long ids. Warning: infixes automatically become reserved words! @@ -83,7 +80,8 @@ Mention that simp etc (big step tactics) insist on change? -Explain what "by" and "." really do, and introduce "done". +Rules: Introduce "by" (as a kind of shorthand for apply+done, except that it +does more.) A list of further useful commands (rules? tricks?) prefer, defer @@ -91,7 +89,11 @@ An overview of the automatic methods: simp, auto, fast, blast, force, clarify, clarsimp (intro, elim?) -explain rulify before induction section? +Advanced Ind expects rule_format incl (no_asm) (which it currently explains!) +Where explained? +Inductive also needs rule_format! + +Where is "simplified" explained? Needed by Inductive/AB.thy demonstrate x : set xs in Sets. Or Tricks chapter?