*** empty log message ***
authornipkow
Wed Apr 19 13:40:42 2000 +0200 (2000-04-19)
changeset 87519ed0548177fb
parent 8750 36b165788421
child 8752 4c1a120647b8
*** empty log message ***
doc-src/TutorialI/Datatype/Nested.thy
doc-src/TutorialI/Datatype/ROOT.ML
doc-src/TutorialI/Datatype/document/Nested.tex
doc-src/TutorialI/Datatype/document/unfoldnested.tex
doc-src/TutorialI/Datatype/unfoldnested.thy
doc-src/TutorialI/IsaMakefile
doc-src/TutorialI/ToyList2/ToyList1
doc-src/TutorialI/ToyList2/ToyList2
doc-src/TutorialI/isabelle.sty
doc-src/TutorialI/isabellesym.sty
doc-src/TutorialI/pdfsetup.sty
     1.1 --- a/doc-src/TutorialI/Datatype/Nested.thy	Wed Apr 19 13:20:16 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Datatype/Nested.thy	Wed Apr 19 13:40:42 2000 +0200
     1.3 @@ -25,8 +25,12 @@
     1.4  nested recursion can be eliminated in favour of mutual recursion by unfolding
     1.5  the offending datatypes, here \isa{list}. The result for \isa{term}
     1.6  would be something like
     1.7 -\begin{ttbox}
     1.8 -\input{Datatype/tunfoldeddata}\end{ttbox}
     1.9 +\medskip
    1.10 +
    1.11 +\input{Datatype/document/unfoldnested.tex}
    1.12 +\medskip
    1.13 +
    1.14 +\noindent
    1.15  Although we do not recommend this unfolding to the user, it shows how to
    1.16  simulate nested recursion by mutual recursion.
    1.17  Now we return to the initial definition of \isa{term} using
     2.1 --- a/doc-src/TutorialI/Datatype/ROOT.ML	Wed Apr 19 13:20:16 2000 +0200
     2.2 +++ b/doc-src/TutorialI/Datatype/ROOT.ML	Wed Apr 19 13:40:42 2000 +0200
     2.3 @@ -1,3 +1,4 @@
     2.4  use_thy "ABexpr";
     2.5 +use_thy "unfoldnested";
     2.6  use_thy "Nested";
     2.7  use_thy "Fundata";
     3.1 --- a/doc-src/TutorialI/Datatype/document/Nested.tex	Wed Apr 19 13:20:16 2000 +0200
     3.2 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Wed Apr 19 13:40:42 2000 +0200
     3.3 @@ -22,8 +22,12 @@
     3.4  nested recursion can be eliminated in favour of mutual recursion by unfolding
     3.5  the offending datatypes, here \isa{list}. The result for \isa{term}
     3.6  would be something like
     3.7 -\begin{ttbox}
     3.8 -\input{Datatype/tunfoldeddata}\end{ttbox}
     3.9 +\medskip
    3.10 +
    3.11 +\input{Datatype/document/unfoldnested.tex}
    3.12 +\medskip
    3.13 +
    3.14 +\noindent
    3.15  Although we do not recommend this unfolding to the user, it shows how to
    3.16  simulate nested recursion by mutual recursion.
    3.17  Now we return to the initial definition of \isa{term} using
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex	Wed Apr 19 13:40:42 2000 +0200
     4.3 @@ -0,0 +1,3 @@
     4.4 +\begin{isabelle}%
     4.5 +\isacommand{datatype}~('a,'b){"}term{"}~=~Var~'a~|~App~'b~{"}('a,'b)term\_list{"}\isanewline
     4.6 +\isakeyword{and}~('a,'b)term\_list~=~Nil~|~Cons~{"}('a,'b)term{"}~{"}('a,'b)term\_list{"}\end{isabelle}%
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/doc-src/TutorialI/Datatype/unfoldnested.thy	Wed Apr 19 13:40:42 2000 +0200
     5.3 @@ -0,0 +1,8 @@
     5.4 +(*<*)
     5.5 +theory unfoldnested = Main:;
     5.6 +(*>*)
     5.7 +datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term_list"
     5.8 +and ('a,'b)term_list = Nil | Cons "('a,'b)term" "('a,'b)term_list"
     5.9 +(*<*)
    5.10 +end
    5.11 +(*>*)
     6.1 --- a/doc-src/TutorialI/IsaMakefile	Wed Apr 19 13:20:16 2000 +0200
     6.2 +++ b/doc-src/TutorialI/IsaMakefile	Wed Apr 19 13:40:42 2000 +0200
     6.3 @@ -64,8 +64,8 @@
     6.4  
     6.5  HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz
     6.6  
     6.7 -$(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy Datatype/Nested.thy \
     6.8 -  Datatype/Fundata.thy
     6.9 +$(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \
    6.10 +  Datatype/Nested.thy Datatype/unfoldnested.thy Datatype/Fundata.thy
    6.11  	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Datatype
    6.12  
    6.13  
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/doc-src/TutorialI/ToyList2/ToyList1	Wed Apr 19 13:40:42 2000 +0200
     7.3 @@ -0,0 +1,15 @@
     7.4 +theory ToyList = PreList:
     7.5 +
     7.6 +datatype 'a list = Nil                          ("[]")
     7.7 +                 | Cons 'a "'a list"            (infixr "#" 65);
     7.8 +
     7.9 +consts app :: "'a list => 'a list => 'a list"   (infixr "@" 65)
    7.10 +       rev :: "'a list => 'a list";
    7.11 +
    7.12 +primrec
    7.13 +"[] @ ys       = ys"
    7.14 +"(x # xs) @ ys = x # (xs @ ys)";
    7.15 +
    7.16 +primrec
    7.17 +"rev []        = []"
    7.18 +"rev (x # xs)  = (rev xs) @ (x # [])";
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/doc-src/TutorialI/ToyList2/ToyList2	Wed Apr 19 13:40:42 2000 +0200
     8.3 @@ -0,0 +1,17 @@
     8.4 +lemma app_Nil2 [simp]: "xs @ [] = xs";
     8.5 +apply(induct_tac xs);
     8.6 +apply(auto).;
     8.7 +
     8.8 +lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
     8.9 +apply(induct_tac xs);
    8.10 +apply(auto).;
    8.11 +
    8.12 +lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
    8.13 +apply(induct_tac xs);
    8.14 +apply(auto).;
    8.15 +
    8.16 +theorem rev_rev [simp]: "rev(rev xs) = xs";
    8.17 +apply(induct_tac xs);
    8.18 +apply(auto).;
    8.19 +
    8.20 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/doc-src/TutorialI/isabelle.sty	Wed Apr 19 13:40:42 2000 +0200
     9.3 @@ -0,0 +1,50 @@
     9.4 +%%
     9.5 +%% $Id$
     9.6 +%%
     9.7 +%% macros for Isabelle generated LaTeX output
     9.8 +%%
     9.9 +
    9.10 +%%% Simple document preparation (based on theory token language)
    9.11 +
    9.12 +% isabelle environments
    9.13 +
    9.14 +\newcommand{\isabelledefaultstyle}{\small\tt\slshape}
    9.15 +\newcommand{\isabellestyle}{}
    9.16 +
    9.17 +\newdimen\isa@parindent\newdimen\isa@parskip
    9.18 +\newenvironment{isabelle}{%
    9.19 +\isa@parindent\parindent\parindent0pt%
    9.20 +\isa@parskip\parskip\parskip0pt%
    9.21 +\isabelledefaultstyle\isabellestyle}{}
    9.22 +
    9.23 +\newcommand{\isa}[1]{\emph{\isabelledefaultstyle\isabellestyle #1}}
    9.24 +
    9.25 +\newcommand{\isanewline}{\mbox{}\\\mbox{}}
    9.26 +
    9.27 +\chardef\isabraceleft=`\{
    9.28 +\chardef\isabraceright=`\}
    9.29 +\chardef\isatilde=`\~
    9.30 +\chardef\isacircum=`\^
    9.31 +\chardef\isabackslash=`\\
    9.32 +
    9.33 +
    9.34 +% keyword and section markup
    9.35 +
    9.36 +\newcommand{\isacommand}[1]{\emph{\bf #1}}
    9.37 +\newcommand{\isakeyword}[1]{\emph{\bf #1}}
    9.38 +\newcommand{\isabeginblock}{\isakeyword{\{}}
    9.39 +\newcommand{\isaendblock}{\isakeyword{\}}}
    9.40 +
    9.41 +\newcommand{\isamarkupheader}[1]{\section{#1}}
    9.42 +\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
    9.43 +\newcommand{\isamarkupsection}[1]{\section{#1}}
    9.44 +\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
    9.45 +\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
    9.46 +\newcommand{\isamarkupsect}[1]{\section{#1}}
    9.47 +\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
    9.48 +\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
    9.49 +
    9.50 +\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\par\medskip}{\par\smallskip}
    9.51 +\newenvironment{isamarkuptext}{\normalsize\rm\begin{isapar}}{\end{isapar}}
    9.52 +\newenvironment{isamarkuptxt}{\rm\begin{isapar}}{\end{isapar}}
    9.53 +\newcommand{\isamarkupcmt}[1]{{\rm--- #1}}
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/doc-src/TutorialI/isabellesym.sty	Wed Apr 19 13:40:42 2000 +0200
    10.3 @@ -0,0 +1,152 @@
    10.4 +%%
    10.5 +%% $Id$
    10.6 +%%
    10.7 +%% definitions of many Isabelle symbols
    10.8 +%%
    10.9 +
   10.10 +\usepackage{latexsym}
   10.11 +%\usepackage[latin1]{inputenc}
   10.12 +
   10.13 +\newcommand{\bigsqcap}{\overline{|\,\,|}}  %just a hack
   10.14 +%\def\textbrokenbar??? etc
   10.15 +
   10.16 +\newcommand{\isasymspacespace}{~~}
   10.17 +\newcommand{\isasymGamma}{$\Gamma$}
   10.18 +\newcommand{\isasymDelta}{$\Delta$}
   10.19 +\newcommand{\isasymTheta}{$\Theta$}
   10.20 +\newcommand{\isasymLambda}{$\Lambda$}
   10.21 +\newcommand{\isasymPi}{$\Pi$}
   10.22 +\newcommand{\isasymSigma}{$\Sigma$}
   10.23 +\newcommand{\isasymPhi}{$\Phi$}
   10.24 +\newcommand{\isasymPsi}{$\Psi$}
   10.25 +\newcommand{\isasymOmega}{$\Omega$}
   10.26 +\newcommand{\isasymalpha}{$\alpha$}
   10.27 +\newcommand{\isasymbeta}{$\beta$}
   10.28 +\newcommand{\isasymgamma}{$\gamma$}
   10.29 +\newcommand{\isasymdelta}{$\delta$}
   10.30 +\newcommand{\isasymepsilon}{$\varepsilon$}
   10.31 +\newcommand{\isasymzeta}{$\zeta$}
   10.32 +\newcommand{\isasymeta}{$\eta$}
   10.33 +\newcommand{\isasymtheta}{$\vartheta$}
   10.34 +\newcommand{\isasymkappa}{$\kappa$}
   10.35 +\newcommand{\isasymlambda}{$\lambda$}
   10.36 +\newcommand{\isasymmu}{$\mu$}
   10.37 +\newcommand{\isasymnu}{$\nu$}
   10.38 +\newcommand{\isasymxi}{$\xi$}
   10.39 +\newcommand{\isasympi}{$\pi$}
   10.40 +\newcommand{\isasymrho}{$\rho$}
   10.41 +\newcommand{\isasymsigma}{$\sigma$}
   10.42 +\newcommand{\isasymtau}{$\tau$}
   10.43 +\newcommand{\isasymphi}{$\varphi$}
   10.44 +\newcommand{\isasymchi}{$\chi$}
   10.45 +\newcommand{\isasympsi}{$\psi$}
   10.46 +\newcommand{\isasymomega}{$\omega$}
   10.47 +\newcommand{\isasymnot}{\emph{$\neg$}}
   10.48 +\newcommand{\isasymand}{\emph{$\wedge$}}
   10.49 +\newcommand{\isasymor}{\emph{$\vee$}}
   10.50 +\newcommand{\isasymforall}{\emph{$\forall\,$}}
   10.51 +\newcommand{\isasymexists}{\emph{$\exists\,$}}
   10.52 +\newcommand{\isasymAnd}{\emph{$\bigwedge\,$}}
   10.53 +\newcommand{\isasymlceil}{\emph{$\lceil$}}
   10.54 +\newcommand{\isasymrceil}{\emph{$\rceil$}}
   10.55 +\newcommand{\isasymlfloor}{\emph{$\lfloor$}}
   10.56 +\newcommand{\isasymrfloor}{\emph{$\rfloor$}}
   10.57 +\newcommand{\isasymturnstile}{\emph{$\vdash$}}
   10.58 +\newcommand{\isasymTurnstile}{\emph{$\models$}}
   10.59 +\newcommand{\isasymlbrakk}{\emph{$\mathopen{\lbrack\mkern-3mu\lbrack}$}}
   10.60 +\newcommand{\isasymrbrakk}{\emph{$\mathclose{\rbrack\mkern-3mu\rbrack}$}}
   10.61 +\newcommand{\isasymcdot}{\emph{$\cdot$}}
   10.62 +\newcommand{\isasymin}{\emph{$\in$}}
   10.63 +\newcommand{\isasymsubseteq}{\emph{$\subseteq$}}
   10.64 +\newcommand{\isasyminter}{\emph{$\cap$}}
   10.65 +\newcommand{\isasymunion}{\emph{$\cup$}}
   10.66 +\newcommand{\isasymInter}{\emph{$\bigcap\,$}}
   10.67 +\newcommand{\isasymUnion}{\emph{$\bigcup\,$}}
   10.68 +\newcommand{\isasymsqinter}{\emph{$\sqcap$}}
   10.69 +\newcommand{\isasymsqunion}{\emph{$\sqcup$}}
   10.70 +\newcommand{\isasymSqinter}{\emph{$\bigsqcap\,$}}
   10.71 +\newcommand{\isasymSqunion}{\emph{$\bigsqcup\,$}}
   10.72 +\newcommand{\isasymbottom}{\emph{$\bot$}}
   10.73 +\newcommand{\isasymdoteq}{\emph{$\doteq$}}
   10.74 +\newcommand{\isasymequiv}{\emph{$\equiv$}}
   10.75 +\newcommand{\isasymnoteq}{\emph{$\not=$}}
   10.76 +\newcommand{\isasymsqsubset}{\emph{$\sqsubset$}}
   10.77 +\newcommand{\isasymsqsubseteq}{\emph{$\sqsubseteq$}}
   10.78 +\newcommand{\isasymprec}{\emph{$\prec$}}
   10.79 +\newcommand{\isasympreceq}{\emph{$\preceq$}}
   10.80 +\newcommand{\isasymsucc}{\emph{$\succ$}}
   10.81 +\newcommand{\isasymapprox}{\emph{$\approx$}}
   10.82 +\newcommand{\isasymsim}{\emph{$\sim$}}
   10.83 +\newcommand{\isasymsimeq}{\emph{$\simeq$}}
   10.84 +\newcommand{\isasymle}{\emph{$\le$}}
   10.85 +\newcommand{\isasymColon}{\emph{$\mathrel{::}$}}
   10.86 +\newcommand{\isasymleftarrow}{\emph{$\leftarrow$}}
   10.87 +\newcommand{\isasymmidarrow}{\emph{$-$}}%deprecated
   10.88 +\newcommand{\isasymrightarrow}{\emph{$\rightarrow$}}
   10.89 +\newcommand{\isasymLeftarrow}{\emph{$\Leftarrow$}}
   10.90 +\newcommand{\isasymMidarrow}{\emph{$=$}}%deprecated
   10.91 +\newcommand{\isasymRightarrow}{\emph{$\Rightarrow$}}
   10.92 +\newcommand{\isasymbow}{\emph{$\frown$}}
   10.93 +\newcommand{\isasymmapsto}{\emph{$\mapsto$}}
   10.94 +\newcommand{\isasymleadsto}{\emph{$\leadsto$}}
   10.95 +\newcommand{\isasymup}{\emph{$\uparrow$}}
   10.96 +\newcommand{\isasymdown}{\emph{$\downarrow$}}
   10.97 +\newcommand{\isasymnotin}{\emph{$\notin$}}
   10.98 +\newcommand{\isasymtimes}{\emph{$\times$}}
   10.99 +\newcommand{\isasymoplus}{\emph{$\oplus$}}
  10.100 +\newcommand{\isasymominus}{\emph{$\ominus$}}
  10.101 +\newcommand{\isasymotimes}{\emph{$\otimes$}}
  10.102 +\newcommand{\isasymoslash}{\emph{$\oslash$}}
  10.103 +\newcommand{\isasymsubset}{\emph{$\subset$}}
  10.104 +\newcommand{\isasyminfinity}{\emph{$\infty$}}
  10.105 +\newcommand{\isasymbox}{\emph{$\Box$}}
  10.106 +\newcommand{\isasymdiamond}{\emph{$\Diamond$}}
  10.107 +\newcommand{\isasymcirc}{\emph{$\circ$}}
  10.108 +\newcommand{\isasymbullet}{\emph{$\bullet$}}
  10.109 +\newcommand{\isasymparallel}{\emph{$\parallel$}}
  10.110 +\newcommand{\isasymsurd}{\emph{$\surd$}}
  10.111 +\newcommand{\isasymcopyright}{\emph{\copyright}}
  10.112 +
  10.113 +\newcommand{\isasymplusminus}{\emph{$\pm$}}
  10.114 +\newcommand{\isasymdiv}{\emph{$\div$}}
  10.115 +\newcommand{\isasymlongrightarrow}{\emph{$\longrightarrow$}}
  10.116 +\newcommand{\isasymlongleftarrow}{\emph{$\longleftarrow$}}
  10.117 +\newcommand{\isasymlongleftrightarrow}{\emph{$\longleftrightarrow$}}
  10.118 +\newcommand{\isasymLongrightarrow}{\emph{$\Longrightarrow$}}
  10.119 +\newcommand{\isasymLongleftarrow}{\emph{$\Longleftarrow$}}
  10.120 +\newcommand{\isasymLongleftrightarrow}{\emph{$\Longleftrightarrow$}}
  10.121 +%requires OT1 encoding:
  10.122 +\newcommand{\isasymbrokenbar}{\emph{\textbrokenbar}}
  10.123 +\newcommand{\isasymhyphen}{-}
  10.124 +\newcommand{\isasymmacron}{\={}}
  10.125 +\newcommand{\isasymexclamdown}{\emph{\textexclamdown}}
  10.126 +\newcommand{\isasymquestiondown}{\emph{\textquestiondown}}
  10.127 +%requires OT1 encoding:
  10.128 +\newcommand{\isasymguillemotleft}{\emph{\guillemotleft}}
  10.129 +%requires OT1 encoding:
  10.130 +\newcommand{\isasymguillemotright}{\emph{\guillemotright}}
  10.131 +%should be available (?):
  10.132 +\newcommand{\isasymdegree}{\emph{\textdegree}}
  10.133 +\newcommand{\isasymonesuperior}{\emph{$\mathonesuperior$}}
  10.134 +\newcommand{\isasymonequarter}{\emph{\textonequarter}}
  10.135 +\newcommand{\isasymtwosuperior}{\emph{$\mathtwosuperior$}}
  10.136 +\newcommand{\isasymonehalf}{\emph{\textonehalf}}
  10.137 +\newcommand{\isasymthreesuperior}{\emph{$\maththreesuperior$}}
  10.138 +\newcommand{\isasymthreequarters}{\emph{\textthreequarters}}
  10.139 +\newcommand{\isasymparagraph}{\emph{\P}}
  10.140 +\newcommand{\isasymregistered}{\emph{\textregistered}}
  10.141 +%should be available (?):
  10.142 +\newcommand{\isasymordfeminine}{\emph{\textordfeminine}}
  10.143 +%should be available (?):
  10.144 +\newcommand{\isasymordmasculine}{\emph{\textordmasculine}}
  10.145 +\newcommand{\isasymsection}{\S}
  10.146 +\newcommand{\isasympounds}{\emph{$\pounds$}}
  10.147 +%requires OT1 encoding:
  10.148 +\newcommand{\isasymyen}{\emph{\textyen}}
  10.149 +%requires OT1 encoding:
  10.150 +\newcommand{\isasymcent}{\emph{\textcent}}
  10.151 +%requires OT1 encoding:
  10.152 +\newcommand{\isasymcurrency}{\emph{\textcurrency}}
  10.153 +\newcommand{\isasymlbrace}{\emph{$\mathopen{\lbrace\mkern-4.5mu\mid}$}}
  10.154 +\newcommand{\isasymrbrace}{\emph{$\mathclose{\mid\mkern-4.5mu\rbrace}$}}
  10.155 +\newcommand{\isasymtop}{\emph{$\top$}}
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/doc-src/TutorialI/pdfsetup.sty	Wed Apr 19 13:40:42 2000 +0200
    11.3 @@ -0,0 +1,9 @@
    11.4 +%%
    11.5 +%% $Id$
    11.6 +%%
    11.7 +%% conditional url/hyperref setup
    11.8 +%%
    11.9 +
   11.10 +\@ifundefined{pdfoutput}{\usepackage{url}}
   11.11 +{\usepackage[pdftex,a4paper,colorlinks=true]{hyperref}
   11.12 +  \IfFileExists{thumbpdf.sty}{\usepackage{thumbpdf}}{}}