# HG changeset patch # User nipkow # Date 956144442 -7200 # Node ID 9ed0548177fbdfcd464fff27fe1280c300293582 # Parent 36b1657884210f56994ce41582c3e569a538aa0b *** empty log message *** diff -r 36b165788421 -r 9ed0548177fb doc-src/TutorialI/Datatype/Nested.thy --- a/doc-src/TutorialI/Datatype/Nested.thy Wed Apr 19 13:20:16 2000 +0200 +++ b/doc-src/TutorialI/Datatype/Nested.thy Wed Apr 19 13:40:42 2000 +0200 @@ -25,8 +25,12 @@ nested recursion can be eliminated in favour of mutual recursion by unfolding the offending datatypes, here \isa{list}. The result for \isa{term} would be something like -\begin{ttbox} -\input{Datatype/tunfoldeddata}\end{ttbox} +\medskip + +\input{Datatype/document/unfoldnested.tex} +\medskip + +\noindent Although we do not recommend this unfolding to the user, it shows how to simulate nested recursion by mutual recursion. Now we return to the initial definition of \isa{term} using diff -r 36b165788421 -r 9ed0548177fb doc-src/TutorialI/Datatype/ROOT.ML --- a/doc-src/TutorialI/Datatype/ROOT.ML Wed Apr 19 13:20:16 2000 +0200 +++ b/doc-src/TutorialI/Datatype/ROOT.ML Wed Apr 19 13:40:42 2000 +0200 @@ -1,3 +1,4 @@ use_thy "ABexpr"; +use_thy "unfoldnested"; use_thy "Nested"; use_thy "Fundata"; diff -r 36b165788421 -r 9ed0548177fb doc-src/TutorialI/Datatype/document/Nested.tex --- a/doc-src/TutorialI/Datatype/document/Nested.tex Wed Apr 19 13:20:16 2000 +0200 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex Wed Apr 19 13:40:42 2000 +0200 @@ -22,8 +22,12 @@ nested recursion can be eliminated in favour of mutual recursion by unfolding the offending datatypes, here \isa{list}. The result for \isa{term} would be something like -\begin{ttbox} -\input{Datatype/tunfoldeddata}\end{ttbox} +\medskip + +\input{Datatype/document/unfoldnested.tex} +\medskip + +\noindent Although we do not recommend this unfolding to the user, it shows how to simulate nested recursion by mutual recursion. Now we return to the initial definition of \isa{term} using diff -r 36b165788421 -r 9ed0548177fb doc-src/TutorialI/Datatype/document/unfoldnested.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex Wed Apr 19 13:40:42 2000 +0200 @@ -0,0 +1,3 @@ +\begin{isabelle}% +\isacommand{datatype}~('a,'b){"}term{"}~=~Var~'a~|~App~'b~{"}('a,'b)term\_list{"}\isanewline +\isakeyword{and}~('a,'b)term\_list~=~Nil~|~Cons~{"}('a,'b)term{"}~{"}('a,'b)term\_list{"}\end{isabelle}% diff -r 36b165788421 -r 9ed0548177fb doc-src/TutorialI/Datatype/unfoldnested.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Datatype/unfoldnested.thy Wed Apr 19 13:40:42 2000 +0200 @@ -0,0 +1,8 @@ +(*<*) +theory unfoldnested = Main:; +(*>*) +datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term_list" +and ('a,'b)term_list = Nil | Cons "('a,'b)term" "('a,'b)term_list" +(*<*) +end +(*>*) diff -r 36b165788421 -r 9ed0548177fb doc-src/TutorialI/IsaMakefile --- a/doc-src/TutorialI/IsaMakefile Wed Apr 19 13:20:16 2000 +0200 +++ b/doc-src/TutorialI/IsaMakefile Wed Apr 19 13:40:42 2000 +0200 @@ -64,8 +64,8 @@ HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz -$(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy Datatype/Nested.thy \ - Datatype/Fundata.thy +$(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \ + Datatype/Nested.thy Datatype/unfoldnested.thy Datatype/Fundata.thy @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Datatype diff -r 36b165788421 -r 9ed0548177fb doc-src/TutorialI/ToyList2/ToyList1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/ToyList2/ToyList1 Wed Apr 19 13:40:42 2000 +0200 @@ -0,0 +1,15 @@ +theory ToyList = PreList: + +datatype 'a list = Nil ("[]") + | Cons 'a "'a list" (infixr "#" 65); + +consts app :: "'a list => 'a list => 'a list" (infixr "@" 65) + rev :: "'a list => 'a list"; + +primrec +"[] @ ys = ys" +"(x # xs) @ ys = x # (xs @ ys)"; + +primrec +"rev [] = []" +"rev (x # xs) = (rev xs) @ (x # [])"; diff -r 36b165788421 -r 9ed0548177fb doc-src/TutorialI/ToyList2/ToyList2 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/ToyList2/ToyList2 Wed Apr 19 13:40:42 2000 +0200 @@ -0,0 +1,17 @@ +lemma app_Nil2 [simp]: "xs @ [] = xs"; +apply(induct_tac xs); +apply(auto).; + +lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"; +apply(induct_tac xs); +apply(auto).; + +lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"; +apply(induct_tac xs); +apply(auto).; + +theorem rev_rev [simp]: "rev(rev xs) = xs"; +apply(induct_tac xs); +apply(auto).; + +end diff -r 36b165788421 -r 9ed0548177fb doc-src/TutorialI/isabelle.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/isabelle.sty Wed Apr 19 13:40:42 2000 +0200 @@ -0,0 +1,50 @@ +%% +%% $Id$ +%% +%% macros for Isabelle generated LaTeX output +%% + +%%% Simple document preparation (based on theory token language) + +% isabelle environments + +\newcommand{\isabelledefaultstyle}{\small\tt\slshape} +\newcommand{\isabellestyle}{} + +\newdimen\isa@parindent\newdimen\isa@parskip +\newenvironment{isabelle}{% +\isa@parindent\parindent\parindent0pt% +\isa@parskip\parskip\parskip0pt% +\isabelledefaultstyle\isabellestyle}{} + +\newcommand{\isa}[1]{\emph{\isabelledefaultstyle\isabellestyle #1}} + +\newcommand{\isanewline}{\mbox{}\\\mbox{}} + +\chardef\isabraceleft=`\{ +\chardef\isabraceright=`\} +\chardef\isatilde=`\~ +\chardef\isacircum=`\^ +\chardef\isabackslash=`\\ + + +% keyword and section markup + +\newcommand{\isacommand}[1]{\emph{\bf #1}} +\newcommand{\isakeyword}[1]{\emph{\bf #1}} +\newcommand{\isabeginblock}{\isakeyword{\{}} +\newcommand{\isaendblock}{\isakeyword{\}}} + +\newcommand{\isamarkupheader}[1]{\section{#1}} +\newcommand{\isamarkupchapter}[1]{\chapter{#1}} +\newcommand{\isamarkupsection}[1]{\section{#1}} +\newcommand{\isamarkupsubsection}[1]{\subsection{#1}} +\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}} +\newcommand{\isamarkupsect}[1]{\section{#1}} +\newcommand{\isamarkupsubsect}[1]{\subsection{#1}} +\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}} + +\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\par\medskip}{\par\smallskip} +\newenvironment{isamarkuptext}{\normalsize\rm\begin{isapar}}{\end{isapar}} +\newenvironment{isamarkuptxt}{\rm\begin{isapar}}{\end{isapar}} +\newcommand{\isamarkupcmt}[1]{{\rm--- #1}} diff -r 36b165788421 -r 9ed0548177fb doc-src/TutorialI/isabellesym.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/isabellesym.sty Wed Apr 19 13:40:42 2000 +0200 @@ -0,0 +1,152 @@ +%% +%% $Id$ +%% +%% definitions of many Isabelle symbols +%% + +\usepackage{latexsym} +%\usepackage[latin1]{inputenc} + +\newcommand{\bigsqcap}{\overline{|\,\,|}} %just a hack +%\def\textbrokenbar??? etc + +\newcommand{\isasymspacespace}{~~} +\newcommand{\isasymGamma}{$\Gamma$} +\newcommand{\isasymDelta}{$\Delta$} +\newcommand{\isasymTheta}{$\Theta$} +\newcommand{\isasymLambda}{$\Lambda$} +\newcommand{\isasymPi}{$\Pi$} +\newcommand{\isasymSigma}{$\Sigma$} +\newcommand{\isasymPhi}{$\Phi$} +\newcommand{\isasymPsi}{$\Psi$} +\newcommand{\isasymOmega}{$\Omega$} +\newcommand{\isasymalpha}{$\alpha$} +\newcommand{\isasymbeta}{$\beta$} +\newcommand{\isasymgamma}{$\gamma$} +\newcommand{\isasymdelta}{$\delta$} +\newcommand{\isasymepsilon}{$\varepsilon$} +\newcommand{\isasymzeta}{$\zeta$} +\newcommand{\isasymeta}{$\eta$} +\newcommand{\isasymtheta}{$\vartheta$} +\newcommand{\isasymkappa}{$\kappa$} +\newcommand{\isasymlambda}{$\lambda$} +\newcommand{\isasymmu}{$\mu$} +\newcommand{\isasymnu}{$\nu$} +\newcommand{\isasymxi}{$\xi$} +\newcommand{\isasympi}{$\pi$} +\newcommand{\isasymrho}{$\rho$} +\newcommand{\isasymsigma}{$\sigma$} +\newcommand{\isasymtau}{$\tau$} +\newcommand{\isasymphi}{$\varphi$} +\newcommand{\isasymchi}{$\chi$} +\newcommand{\isasympsi}{$\psi$} +\newcommand{\isasymomega}{$\omega$} +\newcommand{\isasymnot}{\emph{$\neg$}} +\newcommand{\isasymand}{\emph{$\wedge$}} +\newcommand{\isasymor}{\emph{$\vee$}} +\newcommand{\isasymforall}{\emph{$\forall\,$}} +\newcommand{\isasymexists}{\emph{$\exists\,$}} +\newcommand{\isasymAnd}{\emph{$\bigwedge\,$}} +\newcommand{\isasymlceil}{\emph{$\lceil$}} +\newcommand{\isasymrceil}{\emph{$\rceil$}} +\newcommand{\isasymlfloor}{\emph{$\lfloor$}} +\newcommand{\isasymrfloor}{\emph{$\rfloor$}} +\newcommand{\isasymturnstile}{\emph{$\vdash$}} +\newcommand{\isasymTurnstile}{\emph{$\models$}} +\newcommand{\isasymlbrakk}{\emph{$\mathopen{\lbrack\mkern-3mu\lbrack}$}} +\newcommand{\isasymrbrakk}{\emph{$\mathclose{\rbrack\mkern-3mu\rbrack}$}} +\newcommand{\isasymcdot}{\emph{$\cdot$}} +\newcommand{\isasymin}{\emph{$\in$}} +\newcommand{\isasymsubseteq}{\emph{$\subseteq$}} +\newcommand{\isasyminter}{\emph{$\cap$}} +\newcommand{\isasymunion}{\emph{$\cup$}} +\newcommand{\isasymInter}{\emph{$\bigcap\,$}} +\newcommand{\isasymUnion}{\emph{$\bigcup\,$}} +\newcommand{\isasymsqinter}{\emph{$\sqcap$}} +\newcommand{\isasymsqunion}{\emph{$\sqcup$}} +\newcommand{\isasymSqinter}{\emph{$\bigsqcap\,$}} +\newcommand{\isasymSqunion}{\emph{$\bigsqcup\,$}} +\newcommand{\isasymbottom}{\emph{$\bot$}} +\newcommand{\isasymdoteq}{\emph{$\doteq$}} +\newcommand{\isasymequiv}{\emph{$\equiv$}} +\newcommand{\isasymnoteq}{\emph{$\not=$}} +\newcommand{\isasymsqsubset}{\emph{$\sqsubset$}} +\newcommand{\isasymsqsubseteq}{\emph{$\sqsubseteq$}} +\newcommand{\isasymprec}{\emph{$\prec$}} +\newcommand{\isasympreceq}{\emph{$\preceq$}} +\newcommand{\isasymsucc}{\emph{$\succ$}} +\newcommand{\isasymapprox}{\emph{$\approx$}} +\newcommand{\isasymsim}{\emph{$\sim$}} +\newcommand{\isasymsimeq}{\emph{$\simeq$}} +\newcommand{\isasymle}{\emph{$\le$}} +\newcommand{\isasymColon}{\emph{$\mathrel{::}$}} +\newcommand{\isasymleftarrow}{\emph{$\leftarrow$}} +\newcommand{\isasymmidarrow}{\emph{$-$}}%deprecated +\newcommand{\isasymrightarrow}{\emph{$\rightarrow$}} +\newcommand{\isasymLeftarrow}{\emph{$\Leftarrow$}} +\newcommand{\isasymMidarrow}{\emph{$=$}}%deprecated +\newcommand{\isasymRightarrow}{\emph{$\Rightarrow$}} +\newcommand{\isasymbow}{\emph{$\frown$}} +\newcommand{\isasymmapsto}{\emph{$\mapsto$}} +\newcommand{\isasymleadsto}{\emph{$\leadsto$}} +\newcommand{\isasymup}{\emph{$\uparrow$}} +\newcommand{\isasymdown}{\emph{$\downarrow$}} +\newcommand{\isasymnotin}{\emph{$\notin$}} +\newcommand{\isasymtimes}{\emph{$\times$}} +\newcommand{\isasymoplus}{\emph{$\oplus$}} +\newcommand{\isasymominus}{\emph{$\ominus$}} +\newcommand{\isasymotimes}{\emph{$\otimes$}} +\newcommand{\isasymoslash}{\emph{$\oslash$}} +\newcommand{\isasymsubset}{\emph{$\subset$}} +\newcommand{\isasyminfinity}{\emph{$\infty$}} +\newcommand{\isasymbox}{\emph{$\Box$}} +\newcommand{\isasymdiamond}{\emph{$\Diamond$}} +\newcommand{\isasymcirc}{\emph{$\circ$}} +\newcommand{\isasymbullet}{\emph{$\bullet$}} +\newcommand{\isasymparallel}{\emph{$\parallel$}} +\newcommand{\isasymsurd}{\emph{$\surd$}} +\newcommand{\isasymcopyright}{\emph{\copyright}} + +\newcommand{\isasymplusminus}{\emph{$\pm$}} +\newcommand{\isasymdiv}{\emph{$\div$}} +\newcommand{\isasymlongrightarrow}{\emph{$\longrightarrow$}} +\newcommand{\isasymlongleftarrow}{\emph{$\longleftarrow$}} +\newcommand{\isasymlongleftrightarrow}{\emph{$\longleftrightarrow$}} +\newcommand{\isasymLongrightarrow}{\emph{$\Longrightarrow$}} +\newcommand{\isasymLongleftarrow}{\emph{$\Longleftarrow$}} +\newcommand{\isasymLongleftrightarrow}{\emph{$\Longleftrightarrow$}} +%requires OT1 encoding: +\newcommand{\isasymbrokenbar}{\emph{\textbrokenbar}} +\newcommand{\isasymhyphen}{-} +\newcommand{\isasymmacron}{\={}} +\newcommand{\isasymexclamdown}{\emph{\textexclamdown}} +\newcommand{\isasymquestiondown}{\emph{\textquestiondown}} +%requires OT1 encoding: +\newcommand{\isasymguillemotleft}{\emph{\guillemotleft}} +%requires OT1 encoding: +\newcommand{\isasymguillemotright}{\emph{\guillemotright}} +%should be available (?): +\newcommand{\isasymdegree}{\emph{\textdegree}} +\newcommand{\isasymonesuperior}{\emph{$\mathonesuperior$}} +\newcommand{\isasymonequarter}{\emph{\textonequarter}} +\newcommand{\isasymtwosuperior}{\emph{$\mathtwosuperior$}} +\newcommand{\isasymonehalf}{\emph{\textonehalf}} +\newcommand{\isasymthreesuperior}{\emph{$\maththreesuperior$}} +\newcommand{\isasymthreequarters}{\emph{\textthreequarters}} +\newcommand{\isasymparagraph}{\emph{\P}} +\newcommand{\isasymregistered}{\emph{\textregistered}} +%should be available (?): +\newcommand{\isasymordfeminine}{\emph{\textordfeminine}} +%should be available (?): +\newcommand{\isasymordmasculine}{\emph{\textordmasculine}} +\newcommand{\isasymsection}{\S} +\newcommand{\isasympounds}{\emph{$\pounds$}} +%requires OT1 encoding: +\newcommand{\isasymyen}{\emph{\textyen}} +%requires OT1 encoding: +\newcommand{\isasymcent}{\emph{\textcent}} +%requires OT1 encoding: +\newcommand{\isasymcurrency}{\emph{\textcurrency}} +\newcommand{\isasymlbrace}{\emph{$\mathopen{\lbrace\mkern-4.5mu\mid}$}} +\newcommand{\isasymrbrace}{\emph{$\mathclose{\mid\mkern-4.5mu\rbrace}$}} +\newcommand{\isasymtop}{\emph{$\top$}} diff -r 36b165788421 -r 9ed0548177fb doc-src/TutorialI/pdfsetup.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/pdfsetup.sty Wed Apr 19 13:40:42 2000 +0200 @@ -0,0 +1,9 @@ +%% +%% $Id$ +%% +%% conditional url/hyperref setup +%% + +\@ifundefined{pdfoutput}{\usepackage{url}} +{\usepackage[pdftex,a4paper,colorlinks=true]{hyperref} + \IfFileExists{thumbpdf.sty}{\usepackage{thumbpdf}}{}}