# HG changeset patch # User wenzelm # Date 966878227 -7200 # Node ID 1b2d4f995b134148cfa2b9292d49d92c66b4fb06 # Parent 2c208c98f541e58c0b29bc06e9cc2f646cd80f63 updated; diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/CodeGen/document/CodeGen.tex --- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Mon Aug 21 19:17:07 2000 +0200 @@ -10,10 +10,10 @@ a fixed set of binary operations: instead the expression contains the appropriate function itself.% \end{isamarkuptext}% -\isacommand{types}\ 'v\ binop\ =\ {"}'v\ {\isasymRightarrow}\ 'v\ {\isasymRightarrow}\ 'v{"}\isanewline -\isacommand{datatype}\ ('a,'v)expr\ =\ Cex\ 'v\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Vex\ 'a\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Bex\ {"}'v\ binop{"}\ \ {"}('a,'v)expr{"}\ \ {"}('a,'v)expr{"}% +\isacommand{types}\ {\isacharprime}v\ binop\ {\isacharequal}\ {\isachardoublequote}{\isacharprime}v\ {\isasymRightarrow}\ {\isacharprime}v\ {\isasymRightarrow}\ {\isacharprime}v{\isachardoublequote}\isanewline +\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isacharequal}\ Cex\ {\isacharprime}v\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Vex\ {\isacharprime}a\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Bex\ {\isachardoublequote}{\isacharprime}v\ binop{\isachardoublequote}\ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr{\isachardoublequote}\ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr{\isachardoublequote}% \begin{isamarkuptext}% \noindent The three constructors represent constants, variables and the application of @@ -22,20 +22,20 @@ The value of an expression w.r.t.\ an environment that maps variables to values is easily defined:% \end{isamarkuptext}% -\isacommand{consts}\ value\ ::\ {"}('a,'v)expr\ {\isasymRightarrow}\ ('a\ {\isasymRightarrow}\ 'v)\ {\isasymRightarrow}\ 'v{"}\isanewline +\isacommand{consts}\ value\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}v{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}v{\isachardoublequote}\isanewline \isacommand{primrec}\isanewline -{"}value\ (Cex\ v)\ env\ =\ v{"}\isanewline -{"}value\ (Vex\ a)\ env\ =\ env\ a{"}\isanewline -{"}value\ (Bex\ f\ e1\ e2)\ env\ =\ f\ (value\ e1\ env)\ (value\ e2\ env){"}% +{\isachardoublequote}value\ {\isacharparenleft}Cex\ v{\isacharparenright}\ env\ {\isacharequal}\ v{\isachardoublequote}\isanewline +{\isachardoublequote}value\ {\isacharparenleft}Vex\ a{\isacharparenright}\ env\ {\isacharequal}\ env\ a{\isachardoublequote}\isanewline +{\isachardoublequote}value\ {\isacharparenleft}Bex\ f\ e\isadigit{1}\ e\isadigit{2}{\isacharparenright}\ env\ {\isacharequal}\ f\ {\isacharparenleft}value\ e\isadigit{1}\ env{\isacharparenright}\ {\isacharparenleft}value\ e\isadigit{2}\ env{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% The stack machine has three instructions: load a constant value onto the stack, load the contents of a certain address onto the stack, and apply a binary operation to the two topmost elements of the stack, replacing them by the result. As for \isa{expr}, addresses and values are type parameters:% \end{isamarkuptext}% -\isacommand{datatype}\ ('a,'v)\ instr\ =\ Const\ 'v\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Load\ 'a\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Apply\ {"}'v\ binop{"}% +\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}\ instr\ {\isacharequal}\ Const\ {\isacharprime}v\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Load\ {\isacharprime}a\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Apply\ {\isachardoublequote}{\isacharprime}v\ binop{\isachardoublequote}% \begin{isamarkuptext}% The execution of the stack machine is modelled by a function \isa{exec} that takes a list of instructions, a store (modelled as a @@ -44,13 +44,13 @@ and returns the stack at the end of the execution---the store remains unchanged:% \end{isamarkuptext}% -\isacommand{consts}\ exec\ ::\ {"}('a,'v)instr\ list\ {\isasymRightarrow}\ ('a{\isasymRightarrow}'v)\ {\isasymRightarrow}\ 'v\ list\ {\isasymRightarrow}\ 'v\ list{"}\isanewline +\isacommand{consts}\ exec\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isasymRightarrow}{\isacharprime}v{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}v\ list\ {\isasymRightarrow}\ {\isacharprime}v\ list{\isachardoublequote}\isanewline \isacommand{primrec}\isanewline -{"}exec\ []\ s\ vs\ =\ vs{"}\isanewline -{"}exec\ (i\#is)\ s\ vs\ =\ (case\ i\ of\isanewline -\ \ \ \ Const\ v\ \ {\isasymRightarrow}\ exec\ is\ s\ (v\#vs)\isanewline -\ \ |\ Load\ a\ \ \ {\isasymRightarrow}\ exec\ is\ s\ ((s\ a)\#vs)\isanewline -\ \ |\ Apply\ f\ \ {\isasymRightarrow}\ exec\ is\ s\ ((f\ (hd\ vs)\ (hd(tl\ vs)))\#(tl(tl\ vs)))){"}% +{\isachardoublequote}exec\ {\isacharbrackleft}{\isacharbrackright}\ s\ vs\ {\isacharequal}\ vs{\isachardoublequote}\isanewline +{\isachardoublequote}exec\ {\isacharparenleft}i{\isacharhash}is{\isacharparenright}\ s\ vs\ {\isacharequal}\ {\isacharparenleft}case\ i\ of\isanewline +\ \ \ \ Const\ v\ \ {\isasymRightarrow}\ exec\ is\ s\ {\isacharparenleft}v{\isacharhash}vs{\isacharparenright}\isanewline +\ \ {\isacharbar}\ Load\ a\ \ \ {\isasymRightarrow}\ exec\ is\ s\ {\isacharparenleft}{\isacharparenleft}s\ a{\isacharparenright}{\isacharhash}vs{\isacharparenright}\isanewline +\ \ {\isacharbar}\ Apply\ f\ \ {\isasymRightarrow}\ exec\ is\ s\ {\isacharparenleft}{\isacharparenleft}f\ {\isacharparenleft}hd\ vs{\isacharparenright}\ {\isacharparenleft}hd{\isacharparenleft}tl\ vs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharhash}{\isacharparenleft}tl{\isacharparenleft}tl\ vs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent Recall that \isa{hd} and \isa{tl} @@ -64,29 +64,29 @@ The compiler is a function from expressions to a list of instructions. Its definition is pretty much obvious:% \end{isamarkuptext}% -\isacommand{consts}\ comp\ ::\ {"}('a,'v)expr\ {\isasymRightarrow}\ ('a,'v)instr\ list{"}\isanewline +\isacommand{consts}\ comp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list{\isachardoublequote}\isanewline \isacommand{primrec}\isanewline -{"}comp\ (Cex\ v)\ \ \ \ \ \ \ =\ [Const\ v]{"}\isanewline -{"}comp\ (Vex\ a)\ \ \ \ \ \ \ =\ [Load\ a]{"}\isanewline -{"}comp\ (Bex\ f\ e1\ e2)\ =\ (comp\ e2)\ @\ (comp\ e1)\ @\ [Apply\ f]{"}% +{\isachardoublequote}comp\ {\isacharparenleft}Cex\ v{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Const\ v{\isacharbrackright}{\isachardoublequote}\isanewline +{\isachardoublequote}comp\ {\isacharparenleft}Vex\ a{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Load\ a{\isacharbrackright}{\isachardoublequote}\isanewline +{\isachardoublequote}comp\ {\isacharparenleft}Bex\ f\ e\isadigit{1}\ e\isadigit{2}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}comp\ e\isadigit{2}{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}comp\ e\isadigit{1}{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}Apply\ f{\isacharbrackright}{\isachardoublequote}% \begin{isamarkuptext}% Now we have to prove the correctness of the compiler, i.e.\ that the execution of a compiled expression results in the value of the expression:% \end{isamarkuptext}% -\isacommand{theorem}\ {"}exec\ (comp\ e)\ s\ []\ =\ [value\ e\ s]{"}% +\isacommand{theorem}\ {\isachardoublequote}exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}value\ e\ s{\isacharbrackright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent This theorem needs to be generalized to% \end{isamarkuptext}% -\isacommand{theorem}\ {"}{\isasymforall}vs.\ exec\ (comp\ e)\ s\ vs\ =\ (value\ e\ s)\ \#\ vs{"}% +\isacommand{theorem}\ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ vs\ {\isacharequal}\ {\isacharparenleft}value\ e\ s{\isacharparenright}\ {\isacharhash}\ vs{\isachardoublequote}% \begin{isamarkuptxt}% \noindent which is proved by induction on \isa{e} followed by simplification, once we have the following lemma about executing the concatenation of two instruction sequences:% \end{isamarkuptxt}% -\isacommand{lemma}\ exec\_app[simp]:\isanewline -\ \ {"}{\isasymforall}vs.\ exec\ (xs@ys)\ s\ vs\ =\ exec\ ys\ s\ (exec\ xs\ s\ vs){"}% +\isacommand{lemma}\ exec{\isacharunderscore}app{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}xs{\isacharat}ys{\isacharparenright}\ s\ vs\ {\isacharequal}\ exec\ ys\ s\ {\isacharparenleft}exec\ xs\ s\ vs{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptxt}% \noindent This requires induction on \isa{xs} and ordinary simplification for the @@ -94,14 +94,14 @@ that contains two \isa{case}-expressions over instructions. Thus we add automatic case splitting as well, which finishes the proof:% \end{isamarkuptxt}% -\isacommand{by}(induct\_tac\ xs,\ simp,\ simp\ split:\ instr.split)% +\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}% \begin{isamarkuptext}% \noindent Note that because \isaindex{auto} performs simplification, it can also be modified in the same way \isa{simp} can. Thus the proof can be rewritten as% \end{isamarkuptext}% -\isacommand{by}(induct\_tac\ xs,\ auto\ split:\ instr.split)% +\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ auto\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}% \begin{isamarkuptext}% \noindent Although this is more compact, it is less clear for the reader of the proof. diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Datatype/ROOT.ML --- a/doc-src/TutorialI/Datatype/ROOT.ML Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Datatype/ROOT.ML Mon Aug 21 19:17:07 2000 +0200 @@ -1,4 +1,3 @@ use_thy "ABexpr"; use_thy "unfoldnested"; -use_thy "Nested2"; use_thy "Fundata"; diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Datatype/document/ABexpr.tex --- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Mon Aug 21 19:17:07 2000 +0200 @@ -13,14 +13,14 @@ \end{itemize} In Isabelle this becomes% \end{isamarkuptext}% -\isacommand{datatype}\ 'a\ aexp\ =\ IF\ \ \ {"}'a\ bexp{"}\ {"}'a\ aexp{"}\ {"}'a\ aexp{"}\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Sum\ \ {"}'a\ aexp{"}\ {"}'a\ aexp{"}\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Diff\ {"}'a\ aexp{"}\ {"}'a\ aexp{"}\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Var\ 'a\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Num\ nat\isanewline -\isakeyword{and}\ \ \ \ \ \ 'a\ bexp\ =\ Less\ {"}'a\ aexp{"}\ {"}'a\ aexp{"}\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ And\ \ {"}'a\ bexp{"}\ {"}'a\ bexp{"}\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Neg\ \ {"}'a\ bexp{"}% +\isacommand{datatype}\ {\isacharprime}a\ aexp\ {\isacharequal}\ IF\ \ \ {\isachardoublequote}{\isacharprime}a\ bexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Sum\ \ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Diff\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Var\ {\isacharprime}a\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Num\ nat\isanewline +\isakeyword{and}\ \ \ \ \ \ {\isacharprime}a\ bexp\ {\isacharequal}\ Less\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ And\ \ {\isachardoublequote}{\isacharprime}a\ bexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ bexp{\isachardoublequote}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Neg\ \ {\isachardoublequote}{\isacharprime}a\ bexp{\isachardoublequote}% \begin{isamarkuptext}% \noindent Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler}, @@ -29,8 +29,8 @@ expressions can be arithmetic comparisons, conjunctions and negations. The semantics is fixed via two evaluation functions% \end{isamarkuptext}% -\isacommand{consts}\ \ evala\ ::\ {"}'a\ aexp\ {\isasymRightarrow}\ ('a\ {\isasymRightarrow}\ nat)\ {\isasymRightarrow}\ nat{"}\isanewline -\ \ \ \ \ \ \ \ evalb\ ::\ {"}'a\ bexp\ {\isasymRightarrow}\ ('a\ {\isasymRightarrow}\ nat)\ {\isasymRightarrow}\ bool{"}% +\isacommand{consts}\ \ evala\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ aexp\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline +\ \ \ \ \ \ \ \ evalb\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ bexp\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}% \begin{isamarkuptext}% \noindent that take an expression and an environment (a mapping from variables \isa{'a} to values @@ -40,22 +40,22 @@ section:% \end{isamarkuptext}% \isacommand{primrec}\isanewline -\ \ {"}evala\ (IF\ b\ a1\ a2)\ env\ =\isanewline -\ \ \ \ \ (if\ evalb\ b\ env\ then\ evala\ a1\ env\ else\ evala\ a2\ env){"}\isanewline -\ \ {"}evala\ (Sum\ a1\ a2)\ env\ =\ evala\ a1\ env\ +\ evala\ a2\ env{"}\isanewline -\ \ {"}evala\ (Diff\ a1\ a2)\ env\ =\ evala\ a1\ env\ -\ evala\ a2\ env{"}\isanewline -\ \ {"}evala\ (Var\ v)\ env\ =\ env\ v{"}\isanewline -\ \ {"}evala\ (Num\ n)\ env\ =\ n{"}\isanewline +\ \ {\isachardoublequote}evala\ {\isacharparenleft}IF\ b\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ env\ {\isacharequal}\isanewline +\ \ \ \ \ {\isacharparenleft}if\ evalb\ b\ env\ then\ evala\ a\isadigit{1}\ env\ else\ evala\ a\isadigit{2}\ env{\isacharparenright}{\isachardoublequote}\isanewline +\ \ {\isachardoublequote}evala\ {\isacharparenleft}Sum\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ env\ {\isacharequal}\ evala\ a\isadigit{1}\ env\ {\isacharplus}\ evala\ a\isadigit{2}\ env{\isachardoublequote}\isanewline +\ \ {\isachardoublequote}evala\ {\isacharparenleft}Diff\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ env\ {\isacharequal}\ evala\ a\isadigit{1}\ env\ {\isacharminus}\ evala\ a\isadigit{2}\ env{\isachardoublequote}\isanewline +\ \ {\isachardoublequote}evala\ {\isacharparenleft}Var\ v{\isacharparenright}\ env\ {\isacharequal}\ env\ v{\isachardoublequote}\isanewline +\ \ {\isachardoublequote}evala\ {\isacharparenleft}Num\ n{\isacharparenright}\ env\ {\isacharequal}\ n{\isachardoublequote}\isanewline \isanewline -\ \ {"}evalb\ (Less\ a1\ a2)\ env\ =\ (evala\ a1\ env\ <\ evala\ a2\ env){"}\isanewline -\ \ {"}evalb\ (And\ b1\ b2)\ env\ =\ (evalb\ b1\ env\ {\isasymand}\ evalb\ b2\ env){"}\isanewline -\ \ {"}evalb\ (Neg\ b)\ env\ =\ ({\isasymnot}\ evalb\ b\ env){"}% +\ \ {\isachardoublequote}evalb\ {\isacharparenleft}Less\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}evala\ a\isadigit{1}\ env\ {\isacharless}\ evala\ a\isadigit{2}\ env{\isacharparenright}{\isachardoublequote}\isanewline +\ \ {\isachardoublequote}evalb\ {\isacharparenleft}And\ b\isadigit{1}\ b\isadigit{2}{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}evalb\ b\isadigit{1}\ env\ {\isasymand}\ evalb\ b\isadigit{2}\ env{\isacharparenright}{\isachardoublequote}\isanewline +\ \ {\isachardoublequote}evalb\ {\isacharparenleft}Neg\ b{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ evalb\ b\ env{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent In the same fashion we also define two functions that perform substitution:% \end{isamarkuptext}% -\isacommand{consts}\ substa\ ::\ {"}('a\ {\isasymRightarrow}\ 'b\ aexp)\ {\isasymRightarrow}\ 'a\ aexp\ {\isasymRightarrow}\ 'b\ aexp{"}\isanewline -\ \ \ \ \ \ \ substb\ ::\ {"}('a\ {\isasymRightarrow}\ 'b\ aexp)\ {\isasymRightarrow}\ 'a\ bexp\ {\isasymRightarrow}\ 'b\ bexp{"}% +\isacommand{consts}\ substa\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ aexp{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ aexp\ {\isasymRightarrow}\ {\isacharprime}b\ aexp{\isachardoublequote}\isanewline +\ \ \ \ \ \ \ substb\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ aexp{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ bexp\ {\isasymRightarrow}\ {\isacharprime}b\ bexp{\isachardoublequote}% \begin{isamarkuptext}% \noindent The first argument is a function mapping variables to expressions, the @@ -64,16 +64,16 @@ to \isa{'b}. Note that there are only arithmetic and no boolean variables.% \end{isamarkuptext}% \isacommand{primrec}\isanewline -\ \ {"}substa\ s\ (IF\ b\ a1\ a2)\ =\isanewline -\ \ \ \ \ IF\ (substb\ s\ b)\ (substa\ s\ a1)\ (substa\ s\ a2){"}\isanewline -\ \ {"}substa\ s\ (Sum\ a1\ a2)\ =\ Sum\ (substa\ s\ a1)\ (substa\ s\ a2){"}\isanewline -\ \ {"}substa\ s\ (Diff\ a1\ a2)\ =\ Diff\ (substa\ s\ a1)\ (substa\ s\ a2){"}\isanewline -\ \ {"}substa\ s\ (Var\ v)\ =\ s\ v{"}\isanewline -\ \ {"}substa\ s\ (Num\ n)\ =\ Num\ n{"}\isanewline +\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}IF\ b\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ \ IF\ {\isacharparenleft}substb\ s\ b{\isacharparenright}\ {\isacharparenleft}substa\ s\ a\isadigit{1}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a\isadigit{2}{\isacharparenright}{\isachardoublequote}\isanewline +\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}Sum\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ {\isacharequal}\ Sum\ {\isacharparenleft}substa\ s\ a\isadigit{1}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a\isadigit{2}{\isacharparenright}{\isachardoublequote}\isanewline +\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}Diff\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ {\isacharequal}\ Diff\ {\isacharparenleft}substa\ s\ a\isadigit{1}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a\isadigit{2}{\isacharparenright}{\isachardoublequote}\isanewline +\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}Var\ v{\isacharparenright}\ {\isacharequal}\ s\ v{\isachardoublequote}\isanewline +\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}Num\ n{\isacharparenright}\ {\isacharequal}\ Num\ n{\isachardoublequote}\isanewline \isanewline -\ \ {"}substb\ s\ (Less\ a1\ a2)\ =\ Less\ (substa\ s\ a1)\ (substa\ s\ a2){"}\isanewline -\ \ {"}substb\ s\ (And\ b1\ b2)\ =\ And\ (substb\ s\ b1)\ (substb\ s\ b2){"}\isanewline -\ \ {"}substb\ s\ (Neg\ b)\ =\ Neg\ (substb\ s\ b){"}% +\ \ {\isachardoublequote}substb\ s\ {\isacharparenleft}Less\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ {\isacharequal}\ Less\ {\isacharparenleft}substa\ s\ a\isadigit{1}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a\isadigit{2}{\isacharparenright}{\isachardoublequote}\isanewline +\ \ {\isachardoublequote}substb\ s\ {\isacharparenleft}And\ b\isadigit{1}\ b\isadigit{2}{\isacharparenright}\ {\isacharequal}\ And\ {\isacharparenleft}substb\ s\ b\isadigit{1}{\isacharparenright}\ {\isacharparenleft}substb\ s\ b\isadigit{2}{\isacharparenright}{\isachardoublequote}\isanewline +\ \ {\isachardoublequote}substb\ s\ {\isacharparenleft}Neg\ b{\isacharparenright}\ {\isacharequal}\ Neg\ {\isacharparenleft}substb\ s\ b{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% Now we can prove a fundamental theorem about the interaction between evaluation and substitution: applying a substitution $s$ to an expression $a$ @@ -84,9 +84,9 @@ theorem in the induction step. Therefore you need to state and prove both theorems simultaneously:% \end{isamarkuptext}% -\isacommand{lemma}\ {"}evala\ (substa\ s\ a)\ env\ =\ evala\ a\ ({\isasymlambda}x.\ evala\ (s\ x)\ env)\ {\isasymand}\isanewline -\ \ \ \ \ \ \ \ evalb\ (substb\ s\ b)\ env\ =\ evalb\ b\ ({\isasymlambda}x.\ evala\ (s\ x)\ env){"}\isanewline -\isacommand{apply}(induct\_tac\ a\ \isakeyword{and}\ b)% +\isacommand{lemma}\ {\isachardoublequote}evala\ {\isacharparenleft}substa\ s\ a{\isacharparenright}\ env\ {\isacharequal}\ evala\ a\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ evala\ {\isacharparenleft}s\ x{\isacharparenright}\ env{\isacharparenright}\ {\isasymand}\isanewline +\ \ \ \ \ \ \ \ evalb\ {\isacharparenleft}substb\ s\ b{\isacharparenright}\ env\ {\isacharequal}\ evalb\ b\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ evala\ {\isacharparenleft}s\ x{\isacharparenright}\ env{\isacharparenright}{\isachardoublequote}\isanewline +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ a\ \isakeyword{and}\ b{\isacharparenright}% \begin{isamarkuptxt}% \noindent The resulting 8 goals (one for each constructor) are proved in one fell swoop:% @@ -102,7 +102,7 @@ \end{ttbox} \begin{exercise} - Define a function \isa{norma} of type \isa{\mbox{'a}\ aexp\ {\isasymRightarrow}\ \mbox{'a}\ aexp} that + Define a function \isa{norma} of type \isa{\mbox{{\isacharprime}a}\ aexp\ {\isasymRightarrow}\ \mbox{{\isacharprime}a}\ aexp} that replaces \isa{IF}s with complex boolean conditions by nested \isa{IF}s where each condition is a \isa{Less} --- \isa{And} and \isa{Neg} should be eliminated completely. Prove that \isa{norma} diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Datatype/document/Fundata.tex --- a/doc-src/TutorialI/Datatype/document/Fundata.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Mon Aug 21 19:17:07 2000 +0200 @@ -1,5 +1,5 @@ \begin{isabelle}% -\isacommand{datatype}\ ('a,'i)bigtree\ =\ Tip\ |\ Branch\ 'a\ {"}'i\ {\isasymRightarrow}\ ('a,'i)bigtree{"}% +\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isacharequal}\ Tip\ {\isacharbar}\ Branch\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}i\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}% \begin{isamarkuptext}% \noindent Parameter \isa{'a} is the type of values stored in the \isa{Branch}es of the tree, whereas \isa{'i} is the index @@ -11,33 +11,33 @@ \begin{quote} \begin{isabelle}% -Branch\ 0\ ({\isasymlambda}\mbox{i}.\ Branch\ \mbox{i}\ ({\isasymlambda}\mbox{n}.\ Tip)) +Branch\ \isadigit{0}\ {\isacharparenleft}{\isasymlambda}\mbox{i}{\isachardot}\ Branch\ \mbox{i}\ {\isacharparenleft}{\isasymlambda}\mbox{n}{\isachardot}\ Tip{\isacharparenright}{\isacharparenright} \end{isabelle}% \end{quote} -of type \isa{(nat,\ nat)\ bigtree} is the tree whose +of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose root is labeled with 0 and whose $i$th subtree is labeled with $i$ and has merely \isa{Tip}s as further subtrees. Function \isa{map_bt} applies a function to all labels in a \isa{bigtree}:% \end{isamarkuptext}% -\isacommand{consts}\ map\_bt\ ::\ {"}('a\ {\isasymRightarrow}\ 'b)\ {\isasymRightarrow}\ ('a,'i)bigtree\ {\isasymRightarrow}\ ('b,'i)bigtree{"}\isanewline +\isacommand{consts}\ map{\isacharunderscore}bt\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}\isanewline \isacommand{primrec}\isanewline -{"}map\_bt\ f\ Tip\ \ \ \ \ \ \ \ \ \ =\ Tip{"}\isanewline -{"}map\_bt\ f\ (Branch\ a\ F)\ =\ Branch\ (f\ a)\ ({\isasymlambda}i.\ map\_bt\ f\ (F\ i)){"}% +{\isachardoublequote}map{\isacharunderscore}bt\ f\ Tip\ \ \ \ \ \ \ \ \ \ {\isacharequal}\ Tip{\isachardoublequote}\isanewline +{\isachardoublequote}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent This is a valid \isacommand{primrec} definition because the recursive calls of \isa{map_bt} involve only subtrees obtained from \isa{F}, i.e.\ the left-hand side. Thus termination is assured. The -seasoned functional programmer might have written \isa{map\_bt\ \mbox{f}\ {\isasymcirc}\ \mbox{F}} -instead of \isa{{\isasymlambda}\mbox{i}.\ map\_bt\ \mbox{f}\ (\mbox{F}\ \mbox{i})}, but the former is not accepted by +seasoned functional programmer might have written \isa{map{\isacharunderscore}bt\ \mbox{f}\ {\isasymcirc}\ \mbox{F}} +instead of \isa{{\isasymlambda}\mbox{i}{\isachardot}\ map{\isacharunderscore}bt\ \mbox{f}\ {\isacharparenleft}\mbox{F}\ \mbox{i}{\isacharparenright}}, but the former is not accepted by Isabelle because the termination proof is not as obvious since \isa{map_bt} is only partially applied. The following lemma has a canonical proof% \end{isamarkuptext}% -\isacommand{lemma}\ {"}map\_bt\ (g\ o\ f)\ T\ =\ map\_bt\ g\ (map\_bt\ f\ T){"}\isanewline -\isacommand{by}(induct\_tac\ {"}T{"},\ auto)% +\isacommand{lemma}\ {\isachardoublequote}map{\isacharunderscore}bt\ {\isacharparenleft}g\ o\ f{\isacharparenright}\ T\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ T{\isacharparenright}{\isachardoublequote}\isanewline +\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ {\isachardoublequote}T{\isachardoublequote}{\isacharcomma}\ auto{\isacharparenright}% \begin{isamarkuptext}% \noindent but it is worth taking a look at the proof state after the induction step diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Datatype/document/unfoldnested.tex --- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex Mon Aug 21 19:17:07 2000 +0200 @@ -1,6 +1,6 @@ \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}% +\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}a\ {\isacharbar}\ App\ {\isacharprime}b\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\isanewline +\isakeyword{and}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list\ {\isacharequal}\ Nil\ {\isacharbar}\ Cons\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\end{isabelle}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Ifexpr/document/Ifexpr.tex --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Mon Aug 21 19:17:07 2000 +0200 @@ -7,15 +7,15 @@ constants by negation and conjunction. The following datatype serves exactly that purpose:% \end{isamarkuptext}% -\isacommand{datatype}\ boolex\ =\ Const\ bool\ |\ Var\ nat\ |\ Neg\ boolex\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ And\ boolex\ boolex% +\isacommand{datatype}\ boolex\ {\isacharequal}\ Const\ bool\ {\isacharbar}\ Var\ nat\ {\isacharbar}\ Neg\ boolex\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ And\ boolex\ boolex% \begin{isamarkuptext}% \noindent The two constants are represented by \isa{Const\ True} and \isa{Const\ False}. Variables are represented by terms of the form \isa{Var\ \mbox{n}}, where \isa{\mbox{n}} is a natural number (type \isa{nat}). For example, the formula $P@0 \land \neg P@1$ is represented by the term -\isa{And\ (Var\ 0)\ (Neg\ (Var\ 1))}. +\isa{And\ {\isacharparenleft}Var\ \isadigit{0}{\isacharparenright}\ {\isacharparenleft}Neg\ {\isacharparenleft}Var\ \isadigit{1}{\isacharparenright}{\isacharparenright}}. \subsubsection{What is the value of a boolean expression?} @@ -24,12 +24,12 @@ environment} of type \isa{nat\ {\isasymRightarrow}\ bool}, which maps variables to their values:% \end{isamarkuptext}% -\isacommand{consts}\ value\ ::\ {"}boolex\ {\isasymRightarrow}\ (nat\ {\isasymRightarrow}\ bool)\ {\isasymRightarrow}\ bool{"}\isanewline +\isacommand{consts}\ value\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}boolex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline \isacommand{primrec}\isanewline -{"}value\ (Const\ b)\ env\ =\ b{"}\isanewline -{"}value\ (Var\ x)\ \ \ env\ =\ env\ x{"}\isanewline -{"}value\ (Neg\ b)\ \ \ env\ =\ ({\isasymnot}\ value\ b\ env){"}\isanewline -{"}value\ (And\ b\ c)\ env\ =\ (value\ b\ env\ {\isasymand}\ value\ c\ env){"}% +{\isachardoublequote}value\ {\isacharparenleft}Const\ b{\isacharparenright}\ env\ {\isacharequal}\ b{\isachardoublequote}\isanewline +{\isachardoublequote}value\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequote}\isanewline +{\isachardoublequote}value\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ value\ b\ env{\isacharparenright}{\isachardoublequote}\isanewline +{\isachardoublequote}value\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}value\ b\ env\ {\isasymand}\ value\ c\ env{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent \subsubsection{If-expressions} @@ -39,17 +39,17 @@ from constants (\isa{CIF}), variables (\isa{VIF}) and conditionals (\isa{IF}):% \end{isamarkuptext}% -\isacommand{datatype}\ ifex\ =\ CIF\ bool\ |\ VIF\ nat\ |\ IF\ ifex\ ifex\ ifex% +\isacommand{datatype}\ ifex\ {\isacharequal}\ CIF\ bool\ {\isacharbar}\ VIF\ nat\ {\isacharbar}\ IF\ ifex\ ifex\ ifex% \begin{isamarkuptext}% \noindent The evaluation if If-expressions proceeds as for \isa{boolex}:% \end{isamarkuptext}% -\isacommand{consts}\ valif\ ::\ {"}ifex\ {\isasymRightarrow}\ (nat\ {\isasymRightarrow}\ bool)\ {\isasymRightarrow}\ bool{"}\isanewline +\isacommand{consts}\ valif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline \isacommand{primrec}\isanewline -{"}valif\ (CIF\ b)\ \ \ \ env\ =\ b{"}\isanewline -{"}valif\ (VIF\ x)\ \ \ \ env\ =\ env\ x{"}\isanewline -{"}valif\ (IF\ b\ t\ e)\ env\ =\ (if\ valif\ b\ env\ then\ valif\ t\ env\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env){"}% +{\isachardoublequote}valif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ b{\isachardoublequote}\isanewline +{\isachardoublequote}valif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequote}\isanewline +{\isachardoublequote}valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \subsubsection{Transformation into and of If-expressions} @@ -57,24 +57,24 @@ formulae, whereas \isa{ifex} is designed for efficiency. It is easy to translate from \isa{boolex} into \isa{ifex}:% \end{isamarkuptext}% -\isacommand{consts}\ bool2if\ ::\ {"}boolex\ {\isasymRightarrow}\ ifex{"}\isanewline +\isacommand{consts}\ bool\isadigit{2}if\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}boolex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline \isacommand{primrec}\isanewline -{"}bool2if\ (Const\ b)\ =\ CIF\ b{"}\isanewline -{"}bool2if\ (Var\ x)\ \ \ =\ VIF\ x{"}\isanewline -{"}bool2if\ (Neg\ b)\ \ \ =\ IF\ (bool2if\ b)\ (CIF\ False)\ (CIF\ True){"}\isanewline -{"}bool2if\ (And\ b\ c)\ =\ IF\ (bool2if\ b)\ (bool2if\ c)\ (CIF\ False){"}% +{\isachardoublequote}bool\isadigit{2}if\ {\isacharparenleft}Const\ b{\isacharparenright}\ {\isacharequal}\ CIF\ b{\isachardoublequote}\isanewline +{\isachardoublequote}bool\isadigit{2}if\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ {\isacharequal}\ VIF\ x{\isachardoublequote}\isanewline +{\isachardoublequote}bool\isadigit{2}if\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ {\isacharequal}\ IF\ {\isacharparenleft}bool\isadigit{2}if\ b{\isacharparenright}\ {\isacharparenleft}CIF\ False{\isacharparenright}\ {\isacharparenleft}CIF\ True{\isacharparenright}{\isachardoublequote}\isanewline +{\isachardoublequote}bool\isadigit{2}if\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ {\isacharequal}\ IF\ {\isacharparenleft}bool\isadigit{2}if\ b{\isacharparenright}\ {\isacharparenleft}bool\isadigit{2}if\ c{\isacharparenright}\ {\isacharparenleft}CIF\ False{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent At last, we have something we can verify: that \isa{bool2if} preserves the value of its argument:% \end{isamarkuptext}% -\isacommand{lemma}\ {"}valif\ (bool2if\ b)\ env\ =\ value\ b\ env{"}% +\isacommand{lemma}\ {\isachardoublequote}valif\ {\isacharparenleft}bool\isadigit{2}if\ b{\isacharparenright}\ env\ {\isacharequal}\ value\ b\ env{\isachardoublequote}% \begin{isamarkuptxt}% \noindent The proof is canonical:% \end{isamarkuptxt}% -\isacommand{apply}(induct\_tac\ b)\isanewline -\isacommand{by}(auto)% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ b{\isacharparenright}\isanewline +\isacommand{by}{\isacharparenleft}auto{\isacharparenright}% \begin{isamarkuptext}% \noindent In fact, all proofs in this case study look exactly like this. Hence we do @@ -83,35 +83,35 @@ More interesting is the transformation of If-expressions into a normal form where the first argument of \isa{IF} cannot be another \isa{IF} but must be a constant or variable. Such a normal form can be computed by -repeatedly replacing a subterm of the form \isa{IF\ (IF\ \mbox{b}\ \mbox{x}\ \mbox{y})\ \mbox{z}\ \mbox{u}} by -\isa{IF\ \mbox{b}\ (IF\ \mbox{x}\ \mbox{z}\ \mbox{u})\ (IF\ \mbox{y}\ \mbox{z}\ \mbox{u})}, which has the same value. The following +repeatedly replacing a subterm of the form \isa{IF\ {\isacharparenleft}IF\ \mbox{b}\ \mbox{x}\ \mbox{y}{\isacharparenright}\ \mbox{z}\ \mbox{u}} by +\isa{IF\ \mbox{b}\ {\isacharparenleft}IF\ \mbox{x}\ \mbox{z}\ \mbox{u}{\isacharparenright}\ {\isacharparenleft}IF\ \mbox{y}\ \mbox{z}\ \mbox{u}{\isacharparenright}}, which has the same value. The following primitive recursive functions perform this task:% \end{isamarkuptext}% -\isacommand{consts}\ normif\ ::\ {"}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{"}\isanewline +\isacommand{consts}\ normif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline \isacommand{primrec}\isanewline -{"}normif\ (CIF\ b)\ \ \ \ t\ e\ =\ IF\ (CIF\ b)\ t\ e{"}\isanewline -{"}normif\ (VIF\ x)\ \ \ \ t\ e\ =\ IF\ (VIF\ x)\ t\ e{"}\isanewline -{"}normif\ (IF\ b\ t\ e)\ u\ f\ =\ normif\ b\ (normif\ t\ u\ f)\ (normif\ e\ u\ f){"}\isanewline +{\isachardoublequote}normif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}CIF\ b{\isacharparenright}\ t\ e{\isachardoublequote}\isanewline +{\isachardoublequote}normif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}VIF\ x{\isacharparenright}\ t\ e{\isachardoublequote}\isanewline +{\isachardoublequote}normif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ u\ f\ {\isacharequal}\ normif\ b\ {\isacharparenleft}normif\ t\ u\ f{\isacharparenright}\ {\isacharparenleft}normif\ e\ u\ f{\isacharparenright}{\isachardoublequote}\isanewline \isanewline -\isacommand{consts}\ norm\ ::\ {"}ifex\ {\isasymRightarrow}\ ifex{"}\isanewline +\isacommand{consts}\ norm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline \isacommand{primrec}\isanewline -{"}norm\ (CIF\ b)\ \ \ \ =\ CIF\ b{"}\isanewline -{"}norm\ (VIF\ x)\ \ \ \ =\ VIF\ x{"}\isanewline -{"}norm\ (IF\ b\ t\ e)\ =\ normif\ b\ (norm\ t)\ (norm\ e){"}% +{\isachardoublequote}norm\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ {\isacharequal}\ CIF\ b{\isachardoublequote}\isanewline +{\isachardoublequote}norm\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ {\isacharequal}\ VIF\ x{\isachardoublequote}\isanewline +{\isachardoublequote}norm\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ normif\ b\ {\isacharparenleft}norm\ t{\isacharparenright}\ {\isacharparenleft}norm\ e{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent Their interplay is a bit tricky, and we leave it to the reader to develop an intuitive understanding. Fortunately, Isabelle can help us to verify that the transformation preserves the value of the expression:% \end{isamarkuptext}% -\isacommand{theorem}\ {"}valif\ (norm\ b)\ env\ =\ valif\ b\ env{"}% +\isacommand{theorem}\ {\isachardoublequote}valif\ {\isacharparenleft}norm\ b{\isacharparenright}\ env\ {\isacharequal}\ valif\ b\ env{\isachardoublequote}% \begin{isamarkuptext}% \noindent The proof is canonical, provided we first show the following simplification lemma (which also helps to understand what \isa{normif} does):% \end{isamarkuptext}% -\isacommand{lemma}\ [simp]:\isanewline -\ \ {"}{\isasymforall}t\ e.\ valif\ (normif\ b\ t\ e)\ env\ =\ valif\ (IF\ b\ t\ e)\ env{"}% +\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ valif\ {\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env{\isachardoublequote}% \begin{isamarkuptext}% \noindent Note that the lemma does not have a name, but is implicitly used in the proof @@ -120,18 +120,18 @@ But how can we be sure that \isa{norm} really produces a normal form in the above sense? We define a function that tests If-expressions for normality% \end{isamarkuptext}% -\isacommand{consts}\ normal\ ::\ {"}ifex\ {\isasymRightarrow}\ bool{"}\isanewline +\isacommand{consts}\ normal\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline \isacommand{primrec}\isanewline -{"}normal(CIF\ b)\ =\ True{"}\isanewline -{"}normal(VIF\ x)\ =\ True{"}\isanewline -{"}normal(IF\ b\ t\ e)\ =\ (normal\ t\ {\isasymand}\ normal\ e\ {\isasymand}\isanewline -\ \ \ \ \ (case\ b\ of\ CIF\ b\ {\isasymRightarrow}\ True\ |\ VIF\ x\ {\isasymRightarrow}\ True\ |\ IF\ x\ y\ z\ {\isasymRightarrow}\ False)){"}% +{\isachardoublequote}normal{\isacharparenleft}CIF\ b{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}\isanewline +{\isachardoublequote}normal{\isacharparenleft}VIF\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}\isanewline +{\isachardoublequote}normal{\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e\ {\isasymand}\isanewline +\ \ \ \ \ {\isacharparenleft}case\ b\ of\ CIF\ b\ {\isasymRightarrow}\ True\ {\isacharbar}\ VIF\ x\ {\isasymRightarrow}\ True\ {\isacharbar}\ IF\ x\ y\ z\ {\isasymRightarrow}\ False{\isacharparenright}{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent and prove \isa{normal(norm b)}. Of course, this requires a lemma about normality of \isa{normif}:% \end{isamarkuptext}% -\isacommand{lemma}[simp]:\ {"}{\isasymforall}t\ e.\ normal(normif\ b\ t\ e)\ =\ (normal\ t\ {\isasymand}\ normal\ e){"}\end{isabelle}% +\isacommand{lemma}{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}\end{isabelle}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/AdvancedInd.tex --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Mon Aug 21 19:17:07 2000 +0200 @@ -15,8 +15,8 @@ So far we have assumed that the theorem we want to prove is already in a form that is amenable to induction, but this is not always the case:% \end{isamarkuptext}% -\isacommand{lemma}\ {"}xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd(rev\ xs)\ =\ last\ xs{"}\isanewline -\isacommand{apply}(induct\_tac\ xs)% +\isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isanewline +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}% \begin{isamarkuptxt}% \noindent (where \isa{hd} and \isa{last} return the first and last element of a @@ -46,7 +46,7 @@ \end{quote} This means we should prove% \end{isamarkuptxt}% -\isacommand{lemma}\ hd\_rev:\ {"}xs\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd(rev\ xs)\ =\ last\ xs{"}% +\isacommand{lemma}\ hd{\isacharunderscore}rev{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}% \begin{isamarkuptext}% \noindent This time, induction leaves us with the following base case @@ -60,7 +60,7 @@ example because you want to apply it as an introduction rule, you need to derive it separately, by combining it with modus ponens:% \end{isamarkuptext}% -\isacommand{lemmas}\ hd\_revI\ =\ hd\_rev[THEN\ mp]% +\isacommand{lemmas}\ hd{\isacharunderscore}revI\ {\isacharequal}\ hd{\isacharunderscore}rev{\isacharbrackleft}THEN\ mp{\isacharbrackright}% \begin{isamarkuptext}% \noindent which yields the lemma we originally set out to prove. @@ -73,26 +73,26 @@ which can yield a fairly complex conclusion. Here is a simple example (which is proved by \isa{blast}):% \end{isamarkuptext}% -\isacommand{lemma}\ simple:\ {"}{\isasymforall}\ y.\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ \&\ A\ y{"}% +\isacommand{lemma}\ simple{\isacharcolon}\ {\isachardoublequote}{\isasymforall}\ y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isacharampersand}\ A\ y{\isachardoublequote}% \begin{isamarkuptext}% \noindent You can get the desired lemma by explicit application of modus ponens and \isa{spec}:% \end{isamarkuptext}% -\isacommand{lemmas}\ myrule\ =\ simple[THEN\ spec,\ THEN\ mp,\ THEN\ mp]% +\isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}THEN\ spec{\isacharcomma}\ THEN\ mp{\isacharcomma}\ THEN\ mp{\isacharbrackright}% \begin{isamarkuptext}% \noindent or the wholesale stripping of \isa{\isasymforall} and \isa{\isasymlongrightarrow} in the conclusion via \isa{rulify}% \end{isamarkuptext}% -\isacommand{lemmas}\ myrule\ =\ simple[rulify]% +\isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}rulify{\isacharbrackright}% \begin{isamarkuptext}% \noindent -yielding \isa{{\isasymlbrakk}\mbox{?A}\ \mbox{?y};\ \mbox{?B}\ \mbox{?y}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{?B}\ \mbox{?y}\ {\isasymand}\ \mbox{?A}\ \mbox{?y}}. +yielding \isa{{\isasymlbrakk}\mbox{{\isacharquery}A}\ \mbox{{\isacharquery}y}{\isacharsemicolon}\ \mbox{{\isacharquery}B}\ \mbox{{\isacharquery}y}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{{\isacharquery}B}\ \mbox{{\isacharquery}y}\ {\isasymand}\ \mbox{{\isacharquery}A}\ \mbox{{\isacharquery}y}}. You can go one step further and include these derivations already in the statement of your original lemma, thus avoiding the intermediate step:% \end{isamarkuptext}% -\isacommand{lemma}\ myrule[rulify]:\ \ {"}{\isasymforall}\ y.\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ \&\ A\ y{"}% +\isacommand{lemma}\ myrule{\isacharbrackleft}rulify{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isasymforall}\ y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isacharampersand}\ A\ y{\isachardoublequote}% \begin{isamarkuptext}% \bigskip @@ -121,14 +121,14 @@ \begin{quote} \begin{isabelle}% -({\isasymAnd}\mbox{n}.\ {\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ \mbox{?P}\ \mbox{m}\ {\isasymLongrightarrow}\ \mbox{?P}\ \mbox{n})\ {\isasymLongrightarrow}\ \mbox{?P}\ \mbox{?n} +{\isacharparenleft}{\isasymAnd}\mbox{n}{\isachardot}\ {\isasymforall}\mbox{m}{\isachardot}\ \mbox{m}\ {\isacharless}\ \mbox{n}\ {\isasymlongrightarrow}\ \mbox{{\isacharquery}P}\ \mbox{m}\ {\isasymLongrightarrow}\ \mbox{{\isacharquery}P}\ \mbox{n}{\isacharparenright}\ {\isasymLongrightarrow}\ \mbox{{\isacharquery}P}\ \mbox{{\isacharquery}n} \end{isabelle}% \end{quote} Here is an example of its application.% \end{isamarkuptext}% -\isacommand{consts}\ f\ ::\ {"}nat\ =>\ nat{"}\isanewline -\isacommand{axioms}\ f\_ax:\ {"}f(f(n))\ <\ f(Suc(n)){"}% +\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isacharequal}{\isachargreater}\ nat{\isachardoublequote}\isanewline +\isacommand{axioms}\ f{\isacharunderscore}ax{\isacharcolon}\ {\isachardoublequote}f{\isacharparenleft}f{\isacharparenleft}n{\isacharparenright}{\isacharparenright}\ {\isacharless}\ f{\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent From the above axiom\footnote{In general, the use of axioms is strongly @@ -139,14 +139,14 @@ be proved by induction on \isa{f\ \mbox{n}}. Following the recipy outlined above, we have to phrase the proposition as follows to allow induction:% \end{isamarkuptext}% -\isacommand{lemma}\ f\_incr\_lem:\ {"}{\isasymforall}i.\ k\ =\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{"}% +\isacommand{lemma}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}% \begin{isamarkuptxt}% \noindent To perform induction on \isa{k} using \isa{less\_induct}, we use the same general induction method as for recursion induction (see \S\ref{sec:recdef-induction}):% \end{isamarkuptxt}% -\isacommand{apply}(induct\_tac\ k\ rule:less\_induct)% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ k\ rule{\isacharcolon}less{\isacharunderscore}induct{\isacharparenright}% \begin{isamarkuptxt}% \noindent which leaves us with the following proof state: @@ -163,19 +163,19 @@ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i} \end{isabellepar}%% \end{isamarkuptxt}% -\isacommand{by}(blast\ intro!:\ f\_ax\ Suc\_leI\ intro:le\_less\_trans)% +\isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}% \begin{isamarkuptext}% \noindent It is not surprising if you find the last step puzzling. The proof goes like this (writing \isa{j} instead of \isa{nat}). -Since \isa{\mbox{i}\ =\ Suc\ \mbox{j}} it suffices to show -\isa{\mbox{j}\ <\ f\ (Suc\ \mbox{j})} (by \isa{Suc\_leI}: \isa{\mbox{?m}\ <\ \mbox{?n}\ {\isasymLongrightarrow}\ Suc\ \mbox{?m}\ {\isasymle}\ \mbox{?n}}). This is -proved as follows. From \isa{f\_ax} we have \isa{f\ (f\ \mbox{j})\ <\ f\ (Suc\ \mbox{j})} -(1) which implies \isa{f\ \mbox{j}\ {\isasymle}\ f\ (f\ \mbox{j})} (by the induction hypothesis). -Using (1) once more we obtain \isa{f\ \mbox{j}\ <\ f\ (Suc\ \mbox{j})} (2) by transitivity -(\isa{le_less_trans}: \isa{{\isasymlbrakk}\mbox{?i}\ {\isasymle}\ \mbox{?j};\ \mbox{?j}\ <\ \mbox{?k}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{?i}\ <\ \mbox{?k}}). +Since \isa{\mbox{i}\ {\isacharequal}\ Suc\ \mbox{j}} it suffices to show +\isa{\mbox{j}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ \mbox{j}{\isacharparenright}} (by \isa{Suc\_leI}: \isa{\mbox{{\isacharquery}m}\ {\isacharless}\ \mbox{{\isacharquery}n}\ {\isasymLongrightarrow}\ Suc\ \mbox{{\isacharquery}m}\ {\isasymle}\ \mbox{{\isacharquery}n}}). This is +proved as follows. From \isa{f\_ax} we have \isa{f\ {\isacharparenleft}f\ \mbox{j}{\isacharparenright}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ \mbox{j}{\isacharparenright}} +(1) which implies \isa{f\ \mbox{j}\ {\isasymle}\ f\ {\isacharparenleft}f\ \mbox{j}{\isacharparenright}} (by the induction hypothesis). +Using (1) once more we obtain \isa{f\ \mbox{j}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ \mbox{j}{\isacharparenright}} (2) by transitivity +(\isa{le_less_trans}: \isa{{\isasymlbrakk}\mbox{{\isacharquery}i}\ {\isasymle}\ \mbox{{\isacharquery}j}{\isacharsemicolon}\ \mbox{{\isacharquery}j}\ {\isacharless}\ \mbox{{\isacharquery}k}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{{\isacharquery}i}\ {\isacharless}\ \mbox{{\isacharquery}k}}). Using the induction hypothesis once more we obtain \isa{\mbox{j}\ {\isasymle}\ f\ \mbox{j}} -which, together with (2) yields \isa{\mbox{j}\ <\ f\ (Suc\ \mbox{j})} (again by +which, together with (2) yields \isa{\mbox{j}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ \mbox{j}{\isacharparenright}} (again by \isa{le_less_trans}). This last step shows both the power and the danger of automatic proofs: they @@ -186,12 +186,12 @@ We can now derive the desired \isa{\mbox{i}\ {\isasymle}\ f\ \mbox{i}} from \isa{f\_incr}:% \end{isamarkuptext}% -\isacommand{lemmas}\ f\_incr\ =\ f\_incr\_lem[rulify,\ OF\ refl]% +\isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rulify{\isacharcomma}\ OF\ refl{\isacharbrackright}% \begin{isamarkuptext}% The final \isa{refl} gets rid of the premise \isa{?k = f ?i}. Again, we could have included this derivation in the original statement of the lemma:% \end{isamarkuptext}% -\isacommand{lemma}\ f\_incr[rulify,\ OF\ refl]:\ {"}{\isasymforall}i.\ k\ =\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{"}% +\isacommand{lemma}\ f{\isacharunderscore}incr{\isacharbrackleft}rulify{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}% \begin{isamarkuptext}% \begin{exercise} From the above axiom and lemma for \isa{f} show that \isa{f} is the identity. @@ -216,7 +216,7 @@ \begin{quote} \begin{isabelle}% -{\isasymlbrakk}wf\ \mbox{?r};\ {\isasymAnd}\mbox{x}.\ {\isasymforall}\mbox{y}.\ (\mbox{y},\ \mbox{x})\ {\isasymin}\ \mbox{?r}\ {\isasymlongrightarrow}\ \mbox{?P}\ \mbox{y}\ {\isasymLongrightarrow}\ \mbox{?P}\ \mbox{x}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{?P}\ \mbox{?a} +{\isasymlbrakk}wf\ \mbox{{\isacharquery}r}{\isacharsemicolon}\ {\isasymAnd}\mbox{x}{\isachardot}\ {\isasymforall}\mbox{y}{\isachardot}\ {\isacharparenleft}\mbox{y}{\isacharcomma}\ \mbox{x}{\isacharparenright}\ {\isasymin}\ \mbox{{\isacharquery}r}\ {\isasymlongrightarrow}\ \mbox{{\isacharquery}P}\ \mbox{y}\ {\isasymLongrightarrow}\ \mbox{{\isacharquery}P}\ \mbox{x}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{{\isacharquery}P}\ \mbox{{\isacharquery}a} \end{isabelle}% \end{quote} diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/Itrev.tex --- a/doc-src/TutorialI/Misc/document/Itrev.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex Mon Aug 21 19:17:07 2000 +0200 @@ -7,10 +7,10 @@ \isa{rev} reqires an extra argument where the result is accumulated gradually, using only \isa{\#}:% \end{isamarkuptext}% -\isacommand{consts}\ itrev\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\isanewline +\isacommand{consts}\ itrev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline \isacommand{primrec}\isanewline -{"}itrev\ []\ \ \ \ \ ys\ =\ ys{"}\isanewline -{"}itrev\ (x\#xs)\ ys\ =\ itrev\ xs\ (x\#ys){"}% +{\isachardoublequote}itrev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ ys\ {\isacharequal}\ ys{\isachardoublequote}\isanewline +{\isachardoublequote}itrev\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ ys\ {\isacharequal}\ itrev\ xs\ {\isacharparenleft}x{\isacharhash}ys{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent The behaviour of \isa{itrev} is simple: it reverses its first argument by stacking its elements onto the second argument, @@ -21,12 +21,12 @@ Naturally, we would like to show that \isa{itrev} does indeed reverse its first argument provided the second one is empty:% \end{isamarkuptext}% -\isacommand{lemma}\ {"}itrev\ xs\ []\ =\ rev\ xs{"}% +\isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}% \begin{isamarkuptxt}% \noindent There is no choice as to the induction variable, and we immediately simplify:% \end{isamarkuptxt}% -\isacommand{apply}(induct\_tac\ xs,\ auto)% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ auto{\isacharparenright}% \begin{isamarkuptxt}% \noindent Unfortunately, this is not a complete success: @@ -43,7 +43,7 @@ Of course one cannot do this na\"{\i}vely: \isa{itrev xs ys = rev xs} is just not true---the correct generalization is% \end{isamarkuptxt}% -\isacommand{lemma}\ {"}itrev\ xs\ ys\ =\ rev\ xs\ @\ ys{"}% +\isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}% \begin{isamarkuptxt}% \noindent If \isa{ys} is replaced by \isa{[]}, the right-hand side simplifies to @@ -64,10 +64,10 @@ The induction hypothesis is still too weak, but this time it takes no intuition to generalize: the problem is that \isa{ys} is fixed throughout the subgoal, but the induction hypothesis needs to be applied with -\isa{\mbox{a}\ \#\ \mbox{ys}} instead of \isa{ys}. Hence we prove the theorem +\isa{\mbox{a}\ {\isacharhash}\ \mbox{ys}} instead of \isa{ys}. Hence we prove the theorem for all \isa{ys} instead of a fixed one:% \end{isamarkuptxt}% -\isacommand{lemma}\ {"}{\isasymforall}ys.\ itrev\ xs\ ys\ =\ rev\ xs\ @\ ys{"}% +\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}ys{\isachardot}\ itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}% \begin{isamarkuptxt}% \noindent This time induction on \isa{xs} followed by simplification succeeds. This diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/Tree.tex --- a/doc-src/TutorialI/Misc/document/Tree.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/Tree.tex Mon Aug 21 19:17:07 2000 +0200 @@ -4,19 +4,19 @@ \noindent Define the datatype of binary trees% \end{isamarkuptext}% -\isacommand{datatype}\ 'a\ tree\ =\ Tip\ |\ Node\ {"}'a\ tree{"}\ 'a\ {"}'a\ tree{"}% +\isacommand{datatype}\ {\isacharprime}a\ tree\ {\isacharequal}\ Tip\ {\isacharbar}\ Node\ {\isachardoublequote}{\isacharprime}a\ tree{\isachardoublequote}\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ tree{\isachardoublequote}% \begin{isamarkuptext}% \noindent and a function \isa{mirror} that mirrors a binary tree by swapping subtrees (recursively). Prove% \end{isamarkuptext}% -\isacommand{lemma}\ mirror\_mirror:\ {"}mirror(mirror\ t)\ =\ t{"}% +\isacommand{lemma}\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequote}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}% \begin{isamarkuptext}% \noindent Define a function \isa{flatten} that flattens a tree into a list by traversing it in infix order. Prove% \end{isamarkuptext}% -\isacommand{lemma}\ {"}flatten(mirror\ t)\ =\ rev(flatten\ t){"}\end{isabelle}% +\isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}\end{isabelle}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/Tree2.tex --- a/doc-src/TutorialI/Misc/document/Tree2.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/Tree2.tex Mon Aug 21 19:17:07 2000 +0200 @@ -7,11 +7,11 @@ A linear time version of \isa{flatten} again reqires an extra argument, the accumulator:% \end{isamarkuptext}% -\isacommand{consts}\ flatten2\ ::\ {"}'a\ tree\ =>\ 'a\ list\ =>\ 'a\ list{"}% +\isacommand{consts}\ flatten\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list{\isachardoublequote}% \begin{isamarkuptext}% \noindent Define \isa{flatten2} and prove% \end{isamarkuptext}% -\isacommand{lemma}\ {"}flatten2\ t\ []\ =\ flatten\ t{"}\end{isabelle}% +\isacommand{lemma}\ {\isachardoublequote}flatten\isadigit{2}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\end{isabelle}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/arith1.tex --- a/doc-src/TutorialI/Misc/document/arith1.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/arith1.tex Mon Aug 21 19:17:07 2000 +0200 @@ -1,5 +1,5 @@ \begin{isabelle}% -\isacommand{lemma}\ {"}{\isasymlbrakk}\ {\isasymnot}\ m\ <\ n;\ m\ <\ n+1\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ =\ n{"}\isanewline +\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline \end{isabelle}% %%% Local Variables: %%% mode: latex diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/arith2.tex --- a/doc-src/TutorialI/Misc/document/arith2.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/arith2.tex Mon Aug 21 19:17:07 2000 +0200 @@ -1,6 +1,6 @@ \begin{isabelle}% -\isacommand{lemma}\ {"}min\ i\ (max\ j\ (k*k))\ =\ max\ (min\ (k*k)\ i)\ (min\ i\ (j::nat)){"}\isanewline -\isacommand{by}(arith)\isanewline +\isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline +\isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline \end{isabelle}% %%% Local Variables: %%% mode: latex diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/arith3.tex --- a/doc-src/TutorialI/Misc/document/arith3.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/arith3.tex Mon Aug 21 19:17:07 2000 +0200 @@ -1,5 +1,5 @@ \begin{isabelle}% -\isacommand{lemma}\ {"}n*n\ =\ n\ {\isasymLongrightarrow}\ n=0\ {\isasymor}\ n=1{"}\isanewline +\isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}\isadigit{0}\ {\isasymor}\ n{\isacharequal}\isadigit{1}{\isachardoublequote}\isanewline \end{isabelle}% %%% Local Variables: %%% mode: latex diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/arith4.tex --- a/doc-src/TutorialI/Misc/document/arith4.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/arith4.tex Mon Aug 21 19:17:07 2000 +0200 @@ -1,5 +1,5 @@ \begin{isabelle}% -\isacommand{lemma}\ {"}{\isasymnot}\ m\ <\ n\ {\isasymand}\ m\ <\ n+1\ {\isasymLongrightarrow}\ m\ =\ n{"}\isanewline +\isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ m\ {\isacharless}\ n\ {\isasymand}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline \end{isabelle}% %%% Local Variables: %%% mode: latex diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/asm_simp.tex --- a/doc-src/TutorialI/Misc/document/asm_simp.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/asm_simp.tex Mon Aug 21 19:17:07 2000 +0200 @@ -4,27 +4,27 @@ By default, assumptions are part of the simplification process: they are used as simplification rules and are simplified themselves. For example:% \end{isamarkuptext}% -\isacommand{lemma}\ {"}{\isasymlbrakk}\ xs\ @\ zs\ =\ ys\ @\ xs;\ []\ @\ xs\ =\ []\ @\ []\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ ys\ =\ zs{"}\isanewline +\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ xs\ {\isacharat}\ zs\ {\isacharequal}\ ys\ {\isacharat}\ xs{\isacharsemicolon}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ ys\ {\isacharequal}\ zs{\isachardoublequote}\isanewline \isacommand{by}\ simp% \begin{isamarkuptext}% \noindent -The second assumption simplifies to \isa{\mbox{xs}\ =\ []}, which in turn -simplifies the first assumption to \isa{\mbox{zs}\ =\ \mbox{ys}}, thus reducing the -conclusion to \isa{\mbox{ys}\ =\ \mbox{ys}} and hence to \isa{True}. +The second assumption simplifies to \isa{\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}, which in turn +simplifies the first assumption to \isa{\mbox{zs}\ {\isacharequal}\ \mbox{ys}}, thus reducing the +conclusion to \isa{\mbox{ys}\ {\isacharequal}\ \mbox{ys}} and hence to \isa{True}. In some cases this may be too much of a good thing and may lead to nontermination:% \end{isamarkuptext}% -\isacommand{lemma}\ {"}{\isasymforall}x.\ f\ x\ =\ g\ (f\ (g\ x))\ {\isasymLongrightarrow}\ f\ []\ =\ f\ []\ @\ []{"}% +\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}% \begin{isamarkuptxt}% \noindent cannot be solved by an unmodified application of \isa{simp} because the -simplification rule \isa{\mbox{f}\ \mbox{x}\ =\ \mbox{g}\ (\mbox{f}\ (\mbox{g}\ \mbox{x}))} extracted from the assumption +simplification rule \isa{\mbox{f}\ \mbox{x}\ {\isacharequal}\ \mbox{g}\ {\isacharparenleft}\mbox{f}\ {\isacharparenleft}\mbox{g}\ \mbox{x}{\isacharparenright}{\isacharparenright}} extracted from the assumption does not terminate. Isabelle notices certain simple forms of nontermination but not this one. The problem can be circumvented by explicitly telling the simplifier to ignore the assumptions:% \end{isamarkuptxt}% -\isacommand{by}(simp\ (no\_asm))% +\isacommand{by}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}% \begin{isamarkuptext}% \noindent There are three options that influence the treatment of assumptions: diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/case_splits.tex --- a/doc-src/TutorialI/Misc/document/case_splits.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/case_splits.tex Mon Aug 21 19:17:07 2000 +0200 @@ -4,7 +4,7 @@ Goals containing \isaindex{if}-expressions are usually proved by case distinction on the condition of the \isa{if}. For example the goal% \end{isamarkuptext}% -\isacommand{lemma}\ {"}{\isasymforall}xs.\ if\ xs\ =\ []\ then\ rev\ xs\ =\ []\ else\ rev\ xs\ {\isasymnoteq}\ []{"}% +\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}xs{\isachardot}\ if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}% \begin{isamarkuptxt}% \noindent can be split into @@ -13,7 +13,7 @@ \end{isabellepar}% by a degenerate form of simplification% \end{isamarkuptxt}% -\isacommand{apply}(simp\ only:\ split:\ split\_if)% +\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}% \begin{isamarkuptext}% \noindent where no simplification rules are included (\isa{only:} is followed by the @@ -25,7 +25,7 @@ This splitting idea generalizes from \isa{if} to \isaindex{case}:% \end{isamarkuptext}% -\isacommand{lemma}\ {"}(case\ xs\ of\ []\ {\isasymRightarrow}\ zs\ |\ y\#ys\ {\isasymRightarrow}\ y\#(ys@zs))\ =\ xs@zs{"}% +\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ zs\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ y{\isacharhash}{\isacharparenleft}ys{\isacharat}zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}% \begin{isamarkuptxt}% \noindent becomes @@ -35,7 +35,7 @@ \end{isabellepar}% by typing% \end{isamarkuptxt}% -\isacommand{apply}(simp\ only:\ split:\ list.split)% +\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}% \begin{isamarkuptext}% \noindent In contrast to \isa{if}-expressions, the simplifier does not split @@ -43,7 +43,7 @@ in case of recursive datatypes. Again, if the \isa{only:} modifier is dropped, the above goal is solved,% \end{isamarkuptext}% -\isacommand{by}(simp\ split:\ list.split)% +\isacommand{by}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}% \begin{isamarkuptext}% \noindent% which \isacommand{apply}\isa{(simp)} alone will not do. @@ -52,18 +52,18 @@ \isa{$t$.split} which can be declared to be a \bfindex{split rule} either locally as above, or by giving it the \isa{split} attribute globally:% \end{isamarkuptext}% -\isacommand{lemmas}\ [split]\ =\ list.split% +\isacommand{lemmas}\ {\isacharbrackleft}split{\isacharbrackright}\ {\isacharequal}\ list{\isachardot}split% \begin{isamarkuptext}% \noindent The \isa{split} attribute can be removed with the \isa{del} modifier, either locally% \end{isamarkuptext}% -\isacommand{apply}(simp\ split\ del:\ split\_if)% +\isacommand{apply}{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}% \begin{isamarkuptext}% \noindent or globally:% \end{isamarkuptext}% -\isacommand{lemmas}\ [split\ del]\ =\ list.split\isanewline +\isacommand{lemmas}\ {\isacharbrackleft}split\ del{\isacharbrackright}\ {\isacharequal}\ list{\isachardot}split\isanewline \end{isabelle}% %%% Local Variables: %%% mode: latex diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/cases.tex --- a/doc-src/TutorialI/Misc/document/cases.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/cases.tex Mon Aug 21 19:17:07 2000 +0200 @@ -1,7 +1,7 @@ \begin{isabelle}% \isanewline -\isacommand{lemma}\ {"}(case\ xs\ of\ []\ {\isasymRightarrow}\ []\ |\ y\#ys\ {\isasymRightarrow}\ xs)\ =\ xs{"}\isanewline -\isacommand{apply}(case\_tac\ xs)% +\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline +\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharparenright}% \begin{isamarkuptxt}% \noindent results in the proof state @@ -11,7 +11,7 @@ \end{isabellepar}% which is solved automatically:% \end{isamarkuptxt}% -\isacommand{by}(auto)\isanewline +\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline \end{isabelle}% %%% Local Variables: %%% mode: latex diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/cond_rewr.tex --- a/doc-src/TutorialI/Misc/document/cond_rewr.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/cond_rewr.tex Mon Aug 21 19:17:07 2000 +0200 @@ -4,16 +4,16 @@ So far all examples of rewrite rules were equations. The simplifier also accepts \emph{conditional} equations, for example% \end{isamarkuptext}% -\isacommand{lemma}\ hd\_Cons\_tl[simp]:\ {"}xs\ {\isasymnoteq}\ []\ \ {\isasymLongrightarrow}\ \ hd\ xs\ \#\ tl\ xs\ =\ xs{"}\isanewline -\isacommand{by}(case\_tac\ xs,\ simp,\ simp)% +\isacommand{lemma}\ hd{\isacharunderscore}Cons{\isacharunderscore}tl{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ \ {\isasymLongrightarrow}\ \ hd\ xs\ {\isacharhash}\ tl\ xs\ {\isacharequal}\ xs{\isachardoublequote}\isanewline +\isacommand{by}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp{\isacharparenright}% \begin{isamarkuptext}% \noindent Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a sequence of methods. Assuming that the simplification rule -\isa{(rev\ \mbox{xs}\ =\ [])\ =\ (\mbox{xs}\ =\ [])} +\isa{{\isacharparenleft}rev\ \mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}} is present as well,% \end{isamarkuptext}% -\isacommand{lemma}\ {"}xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd(rev\ xs)\ \#\ tl(rev\ xs)\ =\ rev\ xs{"}% +\isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}% \begin{isamarkuptext}% \noindent is proved by plain simplification: diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/def_rewr.tex --- a/doc-src/TutorialI/Misc/document/def_rewr.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/def_rewr.tex Mon Aug 21 19:17:07 2000 +0200 @@ -9,19 +9,19 @@ enough lemmas that characterize the concept sufficiently for us to forget the original definition. For example, given% \end{isamarkuptext}% -\isacommand{constdefs}\ exor\ ::\ {"}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{"}\isanewline -\ \ \ \ \ \ \ \ \ {"}exor\ A\ B\ {\isasymequiv}\ (A\ {\isasymand}\ {\isasymnot}B)\ {\isasymor}\ ({\isasymnot}A\ {\isasymand}\ B){"}% +\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}% \begin{isamarkuptext}% \noindent we may want to prove% \end{isamarkuptext}% -\isacommand{lemma}\ {"}exor\ A\ ({\isasymnot}A){"}% +\isacommand{lemma}\ {\isachardoublequote}exor\ A\ {\isacharparenleft}{\isasymnot}A{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptxt}% \noindent There is a special method for \emph{unfolding} definitions, which we need to get started:\indexbold{*unfold}\indexbold{definition!unfolding}% \end{isamarkuptxt}% -\isacommand{apply}(unfold\ exor\_def)% +\isacommand{apply}{\isacharparenleft}unfold\ exor{\isacharunderscore}def{\isacharparenright}% \begin{isamarkuptxt}% \noindent It unfolds the given list of definitions (here merely one) in all subgoals: @@ -33,7 +33,7 @@ In case we want to expand a definition in the middle of a proof, we can simply include it locally:% \end{isamarkuptxt}% -\isacommand{apply}(simp\ add:\ exor\_def)% +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ exor{\isacharunderscore}def{\isacharparenright}% \begin{isamarkuptext}% \noindent In fact, this one command proves the above lemma directly. diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/fakenat.tex --- a/doc-src/TutorialI/Misc/document/fakenat.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/fakenat.tex Mon Aug 21 19:17:07 2000 +0200 @@ -5,7 +5,7 @@ The type \isaindexbold{nat}\index{*0|bold}\index{*Suc|bold} of natural numbers is predefined and behaves like% \end{isamarkuptext}% -\isacommand{datatype}\ nat\ =\ 0\ |\ Suc\ nat\end{isabelle}% +\isacommand{datatype}\ nat\ {\isacharequal}\ \isadigit{0}\ {\isacharbar}\ Suc\ nat\end{isabelle}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/let_rewr.tex --- a/doc-src/TutorialI/Misc/document/let_rewr.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/let_rewr.tex Mon Aug 21 19:17:07 2000 +0200 @@ -1,11 +1,11 @@ \begin{isabelle}% -\isacommand{lemma}\ {"}(let\ xs\ =\ []\ in\ xs@ys@xs)\ =\ ys{"}\isanewline -\isacommand{by}(simp\ add:\ Let\_def)% +\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequote}\isanewline +\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}% \begin{isamarkuptext}% If, in a particular context, there is no danger of a combinatorial explosion of nested \isa{let}s one could even add \isa{Let_def} permanently:% \end{isamarkuptext}% -\isacommand{lemmas}\ [simp]\ =\ Let\_def\end{isabelle}% +\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\end{isabelle}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/natsum.tex --- a/doc-src/TutorialI/Misc/document/natsum.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/natsum.tex Mon Aug 21 19:17:07 2000 +0200 @@ -6,22 +6,22 @@ \begin{quote} \begin{isabelle}% -case\ \mbox{n}\ of\ 0\ {\isasymRightarrow}\ 0\ |\ Suc\ \mbox{m}\ {\isasymRightarrow}\ \mbox{m} +case\ \mbox{n}\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ \mbox{m}\ {\isasymRightarrow}\ \mbox{m} \end{isabelle}% \end{quote} primitive recursion, for example% \end{isamarkuptext}% -\isacommand{consts}\ sum\ ::\ {"}nat\ {\isasymRightarrow}\ nat{"}\isanewline -\isacommand{primrec}\ {"}sum\ 0\ =\ 0{"}\isanewline -\ \ \ \ \ \ \ \ {"}sum\ (Suc\ n)\ =\ Suc\ n\ +\ sum\ n{"}% +\isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline +\isacommand{primrec}\ {\isachardoublequote}sum\ \isadigit{0}\ {\isacharequal}\ \isadigit{0}{\isachardoublequote}\isanewline +\ \ \ \ \ \ \ \ {\isachardoublequote}sum\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharplus}\ sum\ n{\isachardoublequote}% \begin{isamarkuptext}% \noindent and induction, for example% \end{isamarkuptext}% -\isacommand{lemma}\ {"}sum\ n\ +\ sum\ n\ =\ n*(Suc\ n){"}\isanewline -\isacommand{apply}(induct\_tac\ n)\isanewline -\isacommand{by}(auto)\isanewline +\isacommand{lemma}\ {\isachardoublequote}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\isanewline +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline +\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline \end{isabelle}% %%% Local Variables: %%% mode: latex diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/pairs.tex --- a/doc-src/TutorialI/Misc/document/pairs.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/pairs.tex Mon Aug 21 19:17:07 2000 +0200 @@ -15,8 +15,8 @@ In addition to explicit $\lambda$-abstractions, tuple patterns can be used in most variable binding constructs. Typical examples are \begin{quote} -\isa{let\ (\mbox{x},\ \mbox{y})\ =\ \mbox{f}\ \mbox{z}\ in\ (\mbox{y},\ \mbox{x})}\\ -\isa{case\ \mbox{xs}\ of\ []\ {\isasymRightarrow}\ 0\ |\ (\mbox{x},\ \mbox{y})\ \#\ \mbox{zs}\ {\isasymRightarrow}\ \mbox{x}\ +\ \mbox{y}} +\isa{let\ {\isacharparenleft}\mbox{x}{\isacharcomma}\ \mbox{y}{\isacharparenright}\ {\isacharequal}\ \mbox{f}\ \mbox{z}\ in\ {\isacharparenleft}\mbox{y}{\isacharcomma}\ \mbox{x}{\isacharparenright}}\\ +\isa{case\ \mbox{xs}\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ {\isacharparenleft}\mbox{x}{\isacharcomma}\ \mbox{y}{\isacharparenright}\ {\isacharhash}\ \mbox{zs}\ {\isasymRightarrow}\ \mbox{x}\ {\isacharplus}\ \mbox{y}} \end{quote} Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).% \end{isamarkuptext}% diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/prime_def.tex --- a/doc-src/TutorialI/Misc/document/prime_def.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/prime_def.tex Mon Aug 21 19:17:07 2000 +0200 @@ -1,6 +1,6 @@ \begin{isabelle}% \isanewline -\ \ \ \ {"}prime(p)\ {\isasymequiv}\ 1\ <\ p\ {\isasymand}\ (m\ dvd\ p\ {\isasymlongrightarrow}\ (m=1\ {\isasymor}\ m=p)){"}% +\ \ \ \ {\isachardoublequote}prime{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}m\ dvd\ p\ {\isasymlongrightarrow}\ {\isacharparenleft}m{\isacharequal}\isadigit{1}\ {\isasymor}\ m{\isacharequal}p{\isacharparenright}{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent\small where \isa{dvd} means ``divides''. @@ -8,7 +8,7 @@ right-hand side, which would introduce an inconsistency (why?). What you should have written is% \end{isamarkuptext}% -\ {"}prime(p)\ {\isasymequiv}\ 1\ <\ p\ {\isasymand}\ ({\isasymforall}m.\ m\ dvd\ p\ {\isasymlongrightarrow}\ (m=1\ {\isasymor}\ m=p)){"}\end{isabelle}% +\ {\isachardoublequote}prime{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ {\isacharparenleft}m{\isacharequal}\isadigit{1}\ {\isasymor}\ m{\isacharequal}p{\isacharparenright}{\isacharparenright}{\isachardoublequote}\end{isabelle}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/trace_simp.tex --- a/doc-src/TutorialI/Misc/document/trace_simp.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/trace_simp.tex Mon Aug 21 19:17:07 2000 +0200 @@ -5,9 +5,9 @@ \ttindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going on:% \end{isamarkuptext}% -\isacommand{ML}\ {"}set\ trace\_simp{"}\isanewline -\isacommand{lemma}\ {"}rev\ [a]\ =\ []{"}\isanewline -\isacommand{apply}(simp)% +\isacommand{ML}\ {\isachardoublequote}set\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline +\isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}% \begin{isamarkuptxt}% \noindent produces the trace @@ -35,7 +35,7 @@ invocations of the simplifier are often nested (e.g.\ when solving conditions of rewrite rules). Thus it is advisable to reset it:% \end{isamarkuptxt}% -\isacommand{ML}\ {"}reset\ trace\_simp{"}\isanewline +\isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline \end{isabelle}% %%% Local Variables: %%% mode: latex diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/types.tex --- a/doc-src/TutorialI/Misc/document/types.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/types.tex Mon Aug 21 19:17:07 2000 +0200 @@ -1,7 +1,7 @@ \begin{isabelle}% -\isacommand{types}\ number\ \ \ \ \ \ \ =\ nat\isanewline -\ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ =\ {"}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{"}\isanewline -\ \ \ \ \ \ ('a,'b)alist\ =\ {"}('a\ *\ 'b)list{"}% +\isacommand{types}\ number\ \ \ \ \ \ \ {\isacharequal}\ nat\isanewline +\ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline +\ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}% \begin{isamarkuptext}% \noindent\indexbold{*types}% Internally all synonyms are fully expanded. As a consequence Isabelle's @@ -9,8 +9,8 @@ readability of theories. Synonyms can be used just like any other type:% \end{isamarkuptext}% -\isacommand{consts}\ nand\ ::\ gate\isanewline -\ \ \ \ \ \ \ exor\ ::\ gate% +\isacommand{consts}\ nand\ {\isacharcolon}{\isacharcolon}\ gate\isanewline +\ \ \ \ \ \ \ exor\ {\isacharcolon}{\isacharcolon}\ gate% \begin{isamarkuptext}% \subsection{Constant definitions} \label{sec:ConstDefinitions} @@ -19,8 +19,8 @@ The above constants \isa{nand} and \isa{exor} are non-recursive and can therefore be defined directly by% \end{isamarkuptext}% -\isacommand{defs}\ nand\_def:\ {"}nand\ A\ B\ {\isasymequiv}\ {\isasymnot}(A\ {\isasymand}\ B){"}\isanewline -\ \ \ \ \ exor\_def:\ {"}exor\ A\ B\ {\isasymequiv}\ A\ {\isasymand}\ {\isasymnot}B\ {\isasymor}\ {\isasymnot}A\ {\isasymand}\ B{"}% +\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}% \begin{isamarkuptext}% \noindent% where \isacommand{defs}\indexbold{*defs} is a keyword and \isa{nand_def} and @@ -29,10 +29,10 @@ that must be used in constant definitions. Declarations and definitions can also be merged% \end{isamarkuptext}% -\isacommand{constdefs}\ nor\ ::\ gate\isanewline -\ \ \ \ \ \ \ \ \ {"}nor\ A\ B\ {\isasymequiv}\ {\isasymnot}(A\ {\isasymor}\ B){"}\isanewline -\ \ \ \ \ \ \ \ \ \ exor2\ ::\ gate\isanewline -\ \ \ \ \ \ \ \ \ {"}exor2\ A\ B\ {\isasymequiv}\ (A\ {\isasymor}\ B)\ {\isasymand}\ ({\isasymnot}A\ {\isasymor}\ {\isasymnot}B){"}% +\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}% \begin{isamarkuptext}% \noindent\indexbold{*constdefs}% in which case the default name of each definition is \isa{$f$_def}, where diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/fp.tex --- a/doc-src/TutorialI/fp.tex Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/fp.tex Mon Aug 21 19:17:07 2000 +0200 @@ -862,4 +862,4 @@ \label{sec:advanced-ind} \input{Misc/document/AdvancedInd.tex} -\input{Datatype/document/Nested2.tex} +%\input{Datatype/document/Nested2.tex} diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/isabelle.sty --- a/doc-src/TutorialI/isabelle.sty Mon Aug 21 19:03:58 2000 +0200 +++ b/doc-src/TutorialI/isabelle.sty Mon Aug 21 19:17:07 2000 +0200 @@ -8,34 +8,64 @@ % isabelle environments -\newcommand{\isabellestyle}{\small\tt\slshape} +\newcommand{\isastyle}{\small\tt\slshape} +\newcommand{\isastyleminor}{\small\tt\slshape} +\newcommand{\isastyletext}{\normalsize\rm} +\newcommand{\isastyletxt}{\rm} +\newcommand{\isastylecmt}{\rm} \newdimen\isa@parindent\newdimen\isa@parskip + \newenvironment{isabelle}{% \isa@parindent\parindent\parindent0pt% \isa@parskip\parskip\parskip0pt% -\isabellestyle}{} +\isastyle}{} -\newcommand{\isa}[1]{\emph{\isabellestyle #1}} - -\newenvironment{isabellequote}% -{\begin{quote}\begin{isabelle}\noindent}{\end{isabelle}\end{quote}} +\newcommand{\isa}[1]{\emph{\isastyleminor #1}} \newcommand{\isanewline}{\mbox{}\\\mbox{}} +\newcommand{\isadigit}[1]{#1} -\chardef\isabraceleft=`\{ -\chardef\isabraceright=`\} -\chardef\isatilde=`\~ -\chardef\isacircum=`\^ -\chardef\isabackslash=`\\ +\chardef\isacharbang=`\! +\chardef\isachardoublequote=`\" +\chardef\isacharhash=`\# +\chardef\isachardollar=`\$ +\chardef\isacharpercent=`\% +\chardef\isacharampersand=`\& +\chardef\isacharprime=`\' +\chardef\isacharparenleft=`\( +\chardef\isacharparenright=`\) +\chardef\isacharasterisk=`\* +\chardef\isacharplus=`\+ +\chardef\isacharcomma=`\, +\chardef\isacharminus=`\- +\chardef\isachardot=`\. +\chardef\isacharslash=`\/ +\chardef\isacharcolon=`\: +\chardef\isacharsemicolon=`\; +\chardef\isacharless=`\< +\chardef\isacharequal=`\= +\chardef\isachargreater=`\> +\chardef\isacharquery=`\? +\chardef\isacharat=`\@ +\chardef\isacharbrackleft=`\[ +\chardef\isacharbackslash=`\\ +\chardef\isacharbrackright=`\] +\chardef\isacharcircum=`\^ +\chardef\isacharunderscore=`\_ +\chardef\isacharbackquote=`\` +\chardef\isacharbraceleft=`\{ +\chardef\isacharbar=`\| +\chardef\isacharbraceright=`\} +\chardef\isachartilde=`\~ % keyword and section markup -\newcommand{\isacommand}[1]{\emph{\bf #1}} -\newcommand{\isakeyword}[1]{\emph{\bf #1}} -\newcommand{\isabeginblock}{\isakeyword{\{}} -\newcommand{\isaendblock}{\isakeyword{\}}} +\newcommand{\isakeyword}[1] +{\emph{\bf\def\isachardot{.}\def\isacharunderscore{-}% +\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}} +\newcommand{\isacommand}[1]{\isakeyword{#1}} \newcommand{\isamarkupheader}[1]{\section{#1}} \newcommand{\isamarkupchapter}[1]{\chapter{#1}} @@ -47,6 +77,48 @@ \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}} +\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}} +\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}} +\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}} + + +% alternative styles -- default is "tt" + +\newcommand{\isabellestyle}{} +\def\isabellestyle#1{\csname isabellestyle#1\endcsname} + +\newcommand{\isabellestyleit}{% +\renewcommand{\isastyle}{\small\it}% +\renewcommand{\isastyleminor}{\it}% +%\renewcommand{\isadigit}[1]{\emph{$##1$}} +\renewcommand{\isacharbang}{\emph{$!$}}% +\renewcommand{\isachardoublequote}{}% +\renewcommand{\isacharhash}{\emph{$\#$}}% +\renewcommand{\isachardollar}{\emph{$\$$}}% +\renewcommand{\isacharpercent}{\emph{$\%$}}% +\renewcommand{\isacharampersand}{\emph{$\&$}}% +\renewcommand{\isacharprime}{$\mskip2mu{'}\mskip-2mu$}% +\renewcommand{\isacharparenleft}{\emph{$($}}% +\renewcommand{\isacharparenright}{\emph{$)$}}% +\renewcommand{\isacharasterisk}{\emph{$*$}}% +\renewcommand{\isacharplus}{\emph{$+$}}% +\renewcommand{\isacharcomma}{\emph{$\mathord,$}}% +\renewcommand{\isacharminus}{\emph{$-$}}% +\renewcommand{\isachardot}{\emph{$\mathord.$}}% +\renewcommand{\isacharslash}{\emph{$/$}}% +\renewcommand{\isacharcolon}{\emph{$\mathord:$}}% +\renewcommand{\isacharsemicolon}{\emph{$\mathord;$}}% +\renewcommand{\isacharless}{\emph{$<$}}% +\renewcommand{\isacharequal}{\emph{$=$}}% +\renewcommand{\isachargreater}{\emph{$>$}}% +%\renewcommand{\isacharquery}{\emph{$\mathord?$}}% +\renewcommand{\isacharat}{\emph{$@$}}% +\renewcommand{\isacharbrackleft}{\emph{$[$}}% +\renewcommand{\isacharbrackright}{\emph{$]$}}% +\renewcommand{\isacharunderscore}{-}% +\renewcommand{\isacharbraceleft}{\emph{$\{$}}% +\renewcommand{\isacharbar}{\emph{$\mid$}}% +\renewcommand{\isacharbraceright}{\emph{$\}$}}% +} + +\newcommand{\isabellestylesl}{\isabellestyleit\renewcommand{\isastyle}{\small\slshape}}