# HG changeset patch # User nipkow # Date 978696637 -3600 # Node ID ea48dd8b0232fe377ff1aee2dfeb4fe5dbd746ee # Parent f42353afd6d333d2b0bacbc930eff55f45c80384 *** empty log message *** diff -r f42353afd6d3 -r ea48dd8b0232 doc-src/TutorialI/Misc/consts.thy --- a/doc-src/TutorialI/Misc/consts.thy Fri Jan 05 10:19:32 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -(*<*)theory "consts" = Main:; -(*>*)consts nand :: gate - exor :: gate(*<*) -end -(*>*) diff -r f42353afd6d3 -r ea48dd8b0232 doc-src/TutorialI/Misc/document/natsum.tex --- a/doc-src/TutorialI/Misc/document/natsum.tex Fri Jan 05 10:19:32 2001 +0100 +++ b/doc-src/TutorialI/Misc/document/natsum.tex Fri Jan 05 13:10:37 2001 +0100 @@ -51,7 +51,7 @@ to prove the goal (although it may take you some time to realize what has happened if \isa{show{\isacharunderscore}types} is not set). In this particular example, you need to include an explicit type constraint, for example - \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x}. If there is enough contextual information this + \isa{x{\isacharplus}{\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}}. If there is enough contextual information this may not be necessary: \isa{Suc\ x\ {\isacharequal}\ x} automatically implies \isa{x{\isacharcolon}{\isacharcolon}nat} because \isa{Suc} is not overloaded. \end{warn} diff -r f42353afd6d3 -r ea48dd8b0232 doc-src/TutorialI/Misc/document/simp.tex --- a/doc-src/TutorialI/Misc/document/simp.tex Fri Jan 05 10:19:32 2001 +0100 +++ b/doc-src/TutorialI/Misc/document/simp.tex Fri Jan 05 13:10:37 2001 +0100 @@ -140,19 +140,19 @@ enough lemmas that characterize the concept sufficiently for us to forget the original definition. For example, given% \end{isamarkuptext}% -\isacommand{constdefs}\ exor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline -\ \ \ \ \ \ \ \ \ {\isachardoublequote}exor\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}% +\isacommand{constdefs}\ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline +\ \ \ \ \ \ \ \ \ {\isachardoublequote}xor\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent we may want to prove% \end{isamarkuptext}% -\isacommand{lemma}\ {\isachardoublequote}exor\ A\ {\isacharparenleft}{\isasymnot}A{\isacharparenright}{\isachardoublequote}% +\isacommand{lemma}\ {\isachardoublequote}xor\ A\ {\isacharparenleft}{\isasymnot}A{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptxt}% \noindent Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding}% \end{isamarkuptxt}% -\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}exor{\isacharunderscore}def{\isacharparenright}% +\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}xor{\isacharunderscore}def{\isacharparenright}% \begin{isamarkuptxt}% \noindent In this particular case, the resulting goal @@ -161,7 +161,7 @@ \end{isabelle} can be proved by simplification. Thus we could have proved the lemma outright by% \end{isamarkuptxt}% -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ exor{\isacharunderscore}def{\isacharparenright}% +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}% \begin{isamarkuptext}% \noindent Of course we can also unfold definitions in the middle of a proof. diff -r f42353afd6d3 -r ea48dd8b0232 doc-src/TutorialI/Misc/document/types.tex --- a/doc-src/TutorialI/Misc/document/types.tex Fri Jan 05 10:19:32 2001 +0100 +++ b/doc-src/TutorialI/Misc/document/types.tex Fri Jan 05 13:10:37 2001 +0100 @@ -12,29 +12,29 @@ type:% \end{isamarkuptext}% \isacommand{consts}\ nand\ {\isacharcolon}{\isacharcolon}\ gate\isanewline -\ \ \ \ \ \ \ exor\ {\isacharcolon}{\isacharcolon}\ gate% +\ \ \ \ \ \ \ xor\ \ {\isacharcolon}{\isacharcolon}\ gate% +\isamarkupsubsection{Constant definitions% +} +% \begin{isamarkuptext}% -\subsection{Constant definitions} -\label{sec:ConstDefinitions} -\indexbold{definition} - -The above constants \isa{nand} and \isa{exor} are non-recursive and can +\label{sec:ConstDefinitions}\indexbold{definition}% +The above constants \isa{nand} and \isa{xor} are non-recursive and can therefore be defined directly by% \end{isamarkuptext}% \isacommand{defs}\ nand{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}nand\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline -\ \ \ \ \ exor{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}exor\ A\ B\ {\isasymequiv}\ A\ {\isasymand}\ {\isasymnot}B\ {\isasymor}\ {\isasymnot}A\ {\isasymand}\ B{\isachardoublequote}% +\ \ \ \ \ xor{\isacharunderscore}def{\isacharcolon}\ \ {\isachardoublequote}xor\ A\ B\ \ {\isasymequiv}\ A\ {\isasymand}\ {\isasymnot}B\ {\isasymor}\ {\isasymnot}A\ {\isasymand}\ B{\isachardoublequote}% \begin{isamarkuptext}% \noindent% where \isacommand{defs}\indexbold{*defs} is a keyword and -\isa{nand{\isacharunderscore}def} and \isa{exor{\isacharunderscore}def} are user-supplied names. +\isa{nand{\isacharunderscore}def} and \isa{xor{\isacharunderscore}def} are user-supplied names. The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality that must be used in constant definitions. Declarations and definitions can also be merged% \end{isamarkuptext}% \isacommand{constdefs}\ nor\ {\isacharcolon}{\isacharcolon}\ gate\isanewline \ \ \ \ \ \ \ \ \ {\isachardoublequote}nor\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}{\isachardoublequote}\isanewline -\ \ \ \ \ \ \ \ \ \ exor{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ gate\isanewline -\ \ \ \ \ \ \ \ \ {\isachardoublequote}exor{\isadigit{2}}\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymnot}A\ {\isasymor}\ {\isasymnot}B{\isacharparenright}{\isachardoublequote}% +\ \ \ \ \ \ \ \ \ \ xor{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ gate\isanewline +\ \ \ \ \ \ \ \ \ {\isachardoublequote}xor{\isadigit{2}}\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymnot}A\ {\isasymor}\ {\isasymnot}B{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent\indexbold{*constdefs}% in which case the default name of each definition is $f$\isa{{\isacharunderscore}def}, where diff -r f42353afd6d3 -r ea48dd8b0232 doc-src/TutorialI/Misc/natsum.thy --- a/doc-src/TutorialI/Misc/natsum.thy Fri Jan 05 10:19:32 2001 +0100 +++ b/doc-src/TutorialI/Misc/natsum.thy Fri Jan 05 13:10:37 2001 +0100 @@ -49,7 +49,7 @@ to prove the goal (although it may take you some time to realize what has happened if @{text show_types} is not set). In this particular example, you need to include an explicit type constraint, for example - @{prop"x+0 = (x::nat)"}. If there is enough contextual information this + @{text"x+0 = (x::nat)"}. If there is enough contextual information this may not be necessary: @{prop"Suc x = x"} automatically implies @{text"x::nat"} because @{term Suc} is not overloaded. \end{warn} diff -r f42353afd6d3 -r ea48dd8b0232 doc-src/TutorialI/Misc/simp.thy --- a/doc-src/TutorialI/Misc/simp.thy Fri Jan 05 10:19:32 2001 +0100 +++ b/doc-src/TutorialI/Misc/simp.thy Fri Jan 05 13:10:37 2001 +0100 @@ -136,28 +136,28 @@ original definition. For example, given *} -constdefs exor :: "bool \ bool \ bool" - "exor A B \ (A \ \B) \ (\A \ B)"; +constdefs xor :: "bool \ bool \ bool" + "xor A B \ (A \ \B) \ (\A \ B)"; text{*\noindent we may want to prove *} -lemma "exor A (\A)"; +lemma "xor A (\A)"; txt{*\noindent Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding} *} -apply(simp only:exor_def); +apply(simp only:xor_def); txt{*\noindent In this particular case, the resulting goal @{subgoals[display,indent=0]} can be proved by simplification. Thus we could have proved the lemma outright by -*}(*<*)oops;lemma "exor A (\A)";(*>*) -apply(simp add: exor_def) +*}(*<*)oops;lemma "xor A (\A)";(*>*) +apply(simp add: xor_def) (*<*)done(*>*) text{*\noindent Of course we can also unfold definitions in the middle of a proof. diff -r f42353afd6d3 -r ea48dd8b0232 doc-src/TutorialI/Misc/types.thy --- a/doc-src/TutorialI/Misc/types.thy Fri Jan 05 10:19:32 2001 +0100 +++ b/doc-src/TutorialI/Misc/types.thy Fri Jan 05 13:10:37 2001 +0100 @@ -1,6 +1,5 @@ -(*<*) -theory "types" = Main:; -(*>*)types number = nat +(*<*)theory "types" = Main:(*>*) +types number = nat gate = "bool \ bool \ bool" ('a,'b)alist = "('a \ 'b)list"; @@ -12,23 +11,21 @@ *} consts nand :: gate - exor :: gate; + xor :: gate; -text{* -\subsection{Constant definitions} -\label{sec:ConstDefinitions} -\indexbold{definition} +subsection{*Constant definitions*} -The above constants @{term"nand"} and @{term"exor"} are non-recursive and can +text{*\label{sec:ConstDefinitions}\indexbold{definition}% +The above constants @{term"nand"} and @{term"xor"} are non-recursive and can therefore be defined directly by *} defs nand_def: "nand A B \ \(A \ B)" - exor_def: "exor A B \ A \ \B \ \A \ B"; + xor_def: "xor A B \ A \ \B \ \A \ B"; text{*\noindent% where \isacommand{defs}\indexbold{*defs} is a keyword and -@{thm[source]nand_def} and @{thm[source]exor_def} are user-supplied names. +@{thm[source]nand_def} and @{thm[source]xor_def} are user-supplied names. The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality that must be used in constant definitions. Declarations and definitions can also be merged @@ -36,11 +33,10 @@ constdefs nor :: gate "nor A B \ \(A \ B)" - exor2 :: gate - "exor2 A B \ (A \ B) \ (\A \ \B)"; + xor2 :: gate + "xor2 A B \ (A \ B) \ (\A \ \B)"; text{*\noindent\indexbold{*constdefs}% in which case the default name of each definition is $f$@{text"_def"}, where -$f$ is the name of the defined constant.*}(*<*) -end -(*>*) +$f$ is the name of the defined constant.*} +(*<*)end(*>*)