# HG changeset patch # User nipkow # Date 971695261 -7200 # Node ID b9fd52525b692e1f3603fd586872c380d18ec8bb # Parent 7263c856787e3d80a5109a0482a2e3631205b547 *** empty log message *** diff -r 7263c856787e -r b9fd52525b69 doc-src/TutorialI/CTL/CTL.thy --- a/doc-src/TutorialI/CTL/CTL.thy Mon Oct 16 10:59:35 2000 +0200 +++ b/doc-src/TutorialI/CTL/CTL.thy Mon Oct 16 13:21:01 2000 +0200 @@ -107,22 +107,23 @@ "lfp(af A) \ {s. \ p \ Paths s. \ i. p i \ A}"; txt{*\noindent -The proof is again pointwise. Fixpoint induction on the premise @{prop"s \ lfp(af A)"} followed -by simplification and clarification +In contrast to the analogous property for @{term EF}, and just +for a change, we do not use fixpoint induction but a weaker theorem, +@{thm[source]lfp_lowerbound}: +@{thm[display]lfp_lowerbound[of _ "S",no_vars]} +The instance of the premise @{prop"f S \ S"} is proved pointwise, +starting with simplification and clarification: *}; - +apply(rule lfp_lowerbound); apply(rule subsetI); -apply(erule lfp_induct[OF _ mono_af]); apply(clarsimp simp add: af_def Paths_def); (*ML"Pretty.setmargin 70"; pr(latex xsymbols symbols);*) -txt{*\noindent -leads to the following somewhat involved proof state +txt{* \begin{isabelle} -\ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline -\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ \isadigit{0}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymand}\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}p{\isachardot}\ t\ {\isacharequal}\ p\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ {\isadigit{0}}\ {\isasymin}\ A\ {\isasymor}\isanewline +\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ {\isadigit{0}}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}p{\isachardot}\ t\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline \ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A @@ -144,8 +145,8 @@ txt{* \begin{isabelle} -\ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\ p\ \isadigit{1}\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharsemicolon}\isanewline -\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}pa{\isachardot}\ p\ \isadigit{1}\ {\isacharequal}\ pa\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}pa{\isachardot}\ p\ {\isadigit{1}}\ {\isacharequal}\ pa\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A \end{isabelle} @@ -158,6 +159,7 @@ apply blast; done; + text{* The opposite containment is proved by contradiction: if some state @{term s} is not in @{term"lfp(af A)"}, then we can construct an diff -r 7263c856787e -r b9fd52525b69 doc-src/TutorialI/CTL/document/CTL.tex --- a/doc-src/TutorialI/CTL/document/CTL.tex Mon Oct 16 10:59:35 2000 +0200 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Mon Oct 16 13:21:01 2000 +0200 @@ -59,20 +59,23 @@ \ \ {\isachardoublequote}lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}% \begin{isamarkuptxt}% \noindent -The proof is again pointwise. Fixpoint induction on the premise \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} followed -by simplification and clarification% +In contrast to the analogous property for \isa{EF}, and just +for a change, we do not use fixpoint induction but a weaker theorem, +\isa{lfp{\isacharunderscore}lowerbound}: +\begin{isabelle}% +\ \ \ \ \ f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S% +\end{isabelle} +The instance of the premise \isa{f\ S\ {\isasymsubseteq}\ S} is proved pointwise, +starting with simplification and clarification:% \end{isamarkuptxt}% +\isacommand{apply}{\isacharparenleft}rule\ lfp{\isacharunderscore}lowerbound{\isacharparenright}\isanewline \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}erule\ lfp{\isacharunderscore}induct{\isacharbrackleft}OF\ {\isacharunderscore}\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline \isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}% \begin{isamarkuptxt}% -\noindent -leads to the following somewhat involved proof state \begin{isabelle} -\ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline -\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ \isadigit{0}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymand}\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}p{\isachardot}\ t\ {\isacharequal}\ p\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ {\isadigit{0}}\ {\isasymin}\ A\ {\isasymor}\isanewline +\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ {\isadigit{0}}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}p{\isachardot}\ t\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline \ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A @@ -89,8 +92,8 @@ \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}% \begin{isamarkuptxt}% \begin{isabelle} -\ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\ p\ \isadigit{1}\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharsemicolon}\isanewline -\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}pa{\isachardot}\ p\ \isadigit{1}\ {\isacharequal}\ pa\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}pa{\isachardot}\ p\ {\isadigit{1}}\ {\isacharequal}\ pa\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A \end{isabelle} diff -r 7263c856787e -r b9fd52525b69 doc-src/TutorialI/Inductive/AB.thy --- a/doc-src/TutorialI/Inductive/AB.thy Mon Oct 16 10:59:35 2000 +0200 +++ b/doc-src/TutorialI/Inductive/AB.thy Mon Oct 16 13:21:01 2000 +0200 @@ -1,4 +1,6 @@ -theory AB = Main:; +(*<*)theory AB = Main:(*>*) + +section{*A context free grammar*} datatype alfa = a | b; @@ -118,4 +120,4 @@ apply(force simp add:min_less_iff_disj); by(force simp add:min_less_iff_disj split add: nat_diff_split); -end; +(*<*)end(*>*) diff -r 7263c856787e -r b9fd52525b69 doc-src/TutorialI/Inductive/ROOT.ML --- a/doc-src/TutorialI/Inductive/ROOT.ML Mon Oct 16 10:59:35 2000 +0200 +++ b/doc-src/TutorialI/Inductive/ROOT.ML Mon Oct 16 13:21:01 2000 +0200 @@ -1,3 +1,4 @@ use "../settings.ML"; +use_thy "Star"; use_thy "AB"; diff -r 7263c856787e -r b9fd52525b69 doc-src/TutorialI/Inductive/Star.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Inductive/Star.thy Mon Oct 16 13:21:01 2000 +0200 @@ -0,0 +1,56 @@ +(*<*)theory Star = Main:(*>*) + +section{*The transitive and reflexive closure*} + +text{* +A perfect example of an inductive definition is the transitive, reflexive +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 +fixpoint because at that point in the theory hierarchy +inductive definitions are not yet available. But now they are: +*} + +consts trc :: "('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*" + +lemma [intro]: "(x,y) : r \ (x,y) \ r*" +by(blast intro: trc_step); + +lemma step2[rule_format]: + "(y,z) \ r* \ (x,y) \ r \ (x,z) \ r*" +apply(erule trc.induct) + apply(blast); +apply(blast intro: trc_step); +done + +lemma trc_trans[rule_format]: + "(x,y) \ r* \ \z. (y,z) \ r* \ (x,z) \ r*" +apply(erule trc.induct) + apply blast; +apply(blast intro: step2); +done + +consts trc2 :: "('a \ 'a)set \ ('a \ 'a)set" +inductive "trc2 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" + + +lemma "((x,y) \ trc2 r) = ((x,y) \ r*)" +apply(rule iffI); + apply(erule trc2.induct); + apply(blast); + apply(blast); + apply(blast intro: trc_trans); +apply(erule trc.induct); + apply(blast intro: trc2.intros); +apply(blast intro: trc2.intros); +done + +(*<*)end(*>*) diff -r 7263c856787e -r b9fd52525b69 doc-src/TutorialI/Inductive/document/AB.tex --- a/doc-src/TutorialI/Inductive/document/AB.tex Mon Oct 16 10:59:35 2000 +0200 +++ b/doc-src/TutorialI/Inductive/document/AB.tex Mon Oct 16 13:21:01 2000 +0200 @@ -1,8 +1,8 @@ % \begin{isabellebody}% \def\isabellecontext{AB}% -\isacommand{theory}\ AB\ {\isacharequal}\ Main{\isacharcolon}\isanewline -\isanewline +% +\isamarkupsection{A context free grammar} \isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b\isanewline \isanewline \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isachartilde}{\isacharequal}\ a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ b{\isacharparenright}\ {\isacharampersand}\ {\isacharparenleft}x\ {\isachartilde}{\isacharequal}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ a{\isacharparenright}{\isachardoublequote}\isanewline @@ -120,8 +120,6 @@ \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline -\isanewline -\isacommand{end}\isanewline \end{isabellebody}% %%% Local Variables: %%% mode: latex diff -r 7263c856787e -r b9fd52525b69 doc-src/TutorialI/Inductive/document/Star.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Inductive/document/Star.tex Mon Oct 16 13:21:01 2000 +0200 @@ -0,0 +1,60 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Star}% +% +\isamarkupsection{The transitive and reflexive closure} +% +\begin{isamarkuptext}% +A perfect example of an inductive definition is the transitive, reflexive +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{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 +\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 +\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}blast{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isacharunderscore}step{\isacharparenright}\isanewline +\isacommand{done}\isanewline +\isanewline +\isacommand{lemma}\ trc{\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}\ 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 +\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 +\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{done}\isanewline +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r 7263c856787e -r b9fd52525b69 doc-src/TutorialI/Inductive/inductive.tex --- a/doc-src/TutorialI/Inductive/inductive.tex Mon Oct 16 10:59:35 2000 +0200 +++ b/doc-src/TutorialI/Inductive/inductive.tex Mon Oct 16 13:21:01 2000 +0200 @@ -1,3 +1,4 @@ \chapter{Inductively Defined Sets} +\input{Inductive/document/Star} \input{Inductive/document/AB} diff -r 7263c856787e -r b9fd52525b69 doc-src/TutorialI/IsaMakefile --- a/doc-src/TutorialI/IsaMakefile Mon Oct 16 10:59:35 2000 +0200 +++ b/doc-src/TutorialI/IsaMakefile Mon Oct 16 13:21:01 2000 +0200 @@ -114,7 +114,8 @@ HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz -$(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/AB.thy Inductive/ROOT.ML +$(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \ + Inductive/Star.thy Inductive/AB.thy @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Inductive @rm -f tutorial.dvi