--- a/doc-src/TutorialI/CTL/Base.thy Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/CTL/Base.thy Thu May 29 22:45:33 2008 +0200
@@ -72,7 +72,7 @@
consts M :: "(state \<times> state)set";
text{*\noindent
-Again, we could have made @{term M} a parameter of everything.
+This is Isabelle's way of declaring a constant without defining it.
Finally we introduce a type of atomic propositions
*}
--- a/doc-src/TutorialI/CTL/CTL.thy Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy Thu May 29 22:45:33 2008 +0200
@@ -24,8 +24,8 @@
in HOL: it is simply a function from @{typ nat} to @{typ state}.
*};
-constdefs Paths :: "state \<Rightarrow> (nat \<Rightarrow> state)set"
- "Paths s \<equiv> {p. s = p 0 \<and> (\<forall>i. (p i, p(i+1)) \<in> M)}";
+definition Paths :: "state \<Rightarrow> (nat \<Rightarrow> state)set" where
+"Paths s \<equiv> {p. s = p 0 \<and> (\<forall>i. (p i, p(i+1)) \<in> M)}"
text{*\noindent
This definition allows a succinct statement of the semantics of @{const AF}:
@@ -35,37 +35,34 @@
a new datatype and a new function.}
*};
(*<*)
-consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80);
-
-primrec
-"s \<Turnstile> Atom a = (a \<in> L s)"
-"s \<Turnstile> Neg f = (~(s \<Turnstile> f))"
-"s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)"
-"s \<Turnstile> AX f = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)"
-"s \<Turnstile> EF f = (\<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<Turnstile> f)"
+primrec valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80) where
+"s \<Turnstile> Atom a = (a \<in> L s)" |
+"s \<Turnstile> Neg f = (~(s \<Turnstile> f))" |
+"s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)" |
+"s \<Turnstile> AX f = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)" |
+"s \<Turnstile> EF f = (\<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<Turnstile> f)" |
(*>*)
-"s \<Turnstile> AF f = (\<forall>p \<in> Paths s. \<exists>i. p i \<Turnstile> f)";
+"s \<Turnstile> AF f = (\<forall>p \<in> Paths s. \<exists>i. p i \<Turnstile> f)"
text{*\noindent
Model checking @{const AF} involves a function which
is just complicated enough to warrant a separate definition:
*};
-constdefs af :: "state set \<Rightarrow> state set \<Rightarrow> state set"
- "af A T \<equiv> A \<union> {s. \<forall>t. (s, t) \<in> M \<longrightarrow> t \<in> T}";
+definition af :: "state set \<Rightarrow> state set \<Rightarrow> state set" where
+"af A T \<equiv> A \<union> {s. \<forall>t. (s, t) \<in> M \<longrightarrow> t \<in> T}"
text{*\noindent
Now we define @{term "mc(AF f)"} as the least set @{term T} that includes
@{term"mc f"} and all states all of whose direct successors are in @{term T}:
*};
(*<*)
-consts mc :: "formula \<Rightarrow> state set";
-primrec
-"mc(Atom a) = {s. a \<in> L s}"
-"mc(Neg f) = -mc f"
-"mc(And f g) = mc f \<inter> mc g"
-"mc(AX f) = {s. \<forall>t. (s,t) \<in> M \<longrightarrow> t \<in> mc f}"
-"mc(EF f) = lfp(\<lambda>T. mc f \<union> M\<inverse> `` T)"(*>*)
+primrec mc :: "formula \<Rightarrow> state set" where
+"mc(Atom a) = {s. a \<in> L s}" |
+"mc(Neg f) = -mc f" |
+"mc(And f g) = mc f \<inter> mc g" |
+"mc(AX f) = {s. \<forall>t. (s,t) \<in> M \<longrightarrow> t \<in> mc f}" |
+"mc(EF f) = lfp(\<lambda>T. mc f \<union> M\<inverse> `` T)"|(*>*)
"mc(AF f) = lfp(af(mc f))";
text{*\noindent
@@ -106,8 +103,7 @@
with the easy one:
*};
-theorem AF_lemma1:
- "lfp(af A) \<subseteq> {s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A}";
+theorem AF_lemma1: "lfp(af A) \<subseteq> {s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A}"
txt{*\noindent
In contrast to the analogous proof for @{const EF}, and just
@@ -165,10 +161,9 @@
path is parameterized by a predicate @{term Q} that should hold along the path:
*};
-consts path :: "state \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> (nat \<Rightarrow> state)";
-primrec
-"path s Q 0 = s"
-"path s Q (Suc n) = (SOME t. (path s Q n,t) \<in> M \<and> Q t)";
+primrec path :: "state \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> (nat \<Rightarrow> state)" where
+"path s Q 0 = s" |
+"path s Q (Suc n) = (SOME t. (path s Q n,t) \<in> M \<and> Q t)"
text{*\noindent
Element @{term"n+1::nat"} on this path is some arbitrary successor
--- a/doc-src/TutorialI/CTL/PDL.thy Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/CTL/PDL.thy Thu May 29 22:45:33 2008 +0200
@@ -21,23 +21,17 @@
text{*\noindent
This resembles the boolean expression case study in
\S\ref{sec:boolex}.
-A validity relation between
-states and formulae specifies the semantics:
+A validity relation between states and formulae specifies the semantics.
+The syntax annotation allows us to write @{text"s \<Turnstile> f"} instead of
+\hbox{@{text"valid s f"}}. The definition is by recursion over the syntax:
*}
-consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80)
-
-text{*\noindent
-The syntax annotation allows us to write @{term"s \<Turnstile> f"} instead of
-\hbox{@{text"valid s f"}}.
-The definition of @{text"\<Turnstile>"} is by recursion over the syntax:
-*}
-
-primrec
-"s \<Turnstile> Atom a = (a \<in> L s)"
-"s \<Turnstile> Neg f = (\<not>(s \<Turnstile> f))"
-"s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)"
-"s \<Turnstile> AX f = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)"
+primrec valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80)
+where
+"s \<Turnstile> Atom a = (a \<in> L s)" |
+"s \<Turnstile> Neg f = (\<not>(s \<Turnstile> f))" |
+"s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)" |
+"s \<Turnstile> AX f = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)" |
"s \<Turnstile> EF f = (\<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<Turnstile> f)"
text{*\noindent
@@ -47,16 +41,15 @@
true. The future is expressed via @{text"\<^sup>*"}, the reflexive transitive
closure. Because of reflexivity, the future includes the present.
-Now we come to the model checker itself. It maps a formula into the set of
-states where the formula is true. It too is defined by recursion over the syntax:
-*}
+Now we come to the model checker itself. It maps a formula into the
+set of states where the formula is true. It too is defined by
+recursion over the syntax: *}
-consts mc :: "formula \<Rightarrow> state set"
-primrec
-"mc(Atom a) = {s. a \<in> L s}"
-"mc(Neg f) = -mc f"
-"mc(And f g) = mc f \<inter> mc g"
-"mc(AX f) = {s. \<forall>t. (s,t) \<in> M \<longrightarrow> t \<in> mc f}"
+primrec mc :: "formula \<Rightarrow> state set" where
+"mc(Atom a) = {s. a \<in> L s}" |
+"mc(Neg f) = -mc f" |
+"mc(And f g) = mc f \<inter> mc g" |
+"mc(AX f) = {s. \<forall>t. (s,t) \<in> M \<longrightarrow> t \<in> mc f}" |
"mc(EF f) = lfp(\<lambda>T. mc f \<union> (M\<inverse> `` T))"
text{*\noindent
--- a/doc-src/TutorialI/CTL/document/Base.tex Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/CTL/document/Base.tex Thu May 29 22:45:33 2008 +0200
@@ -92,7 +92,7 @@
\ M\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}state\ {\isasymtimes}\ state{\isacharparenright}set{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
-Again, we could have made \isa{M} a parameter of everything.
+This is Isabelle's way of declaring a constant without defining it.
Finally we introduce a type of atomic propositions%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/TutorialI/CTL/document/CTL.tex Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Thu May 29 22:45:33 2008 +0200
@@ -37,9 +37,9 @@
in HOL: it is simply a function from \isa{nat} to \isa{state}.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{constdefs}\isamarkupfalse%
-\ Paths\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}set{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}Paths\ s\ {\isasymequiv}\ {\isacharbraceleft}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}%
+\isacommand{definition}\isamarkupfalse%
+\ Paths\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}Paths\ s\ {\isasymequiv}\ {\isacharbraceleft}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
This definition allows a succinct statement of the semantics of \isa{AF}:
@@ -56,9 +56,9 @@
is just complicated enough to warrant a separate definition:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{constdefs}\isamarkupfalse%
-\ af\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}af\ A\ T\ {\isasymequiv}\ A\ {\isasymunion}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\ t\ {\isasymin}\ T{\isacharbraceright}{\isachardoublequoteclose}%
+\isacommand{definition}\isamarkupfalse%
+\ af\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}af\ A\ T\ {\isasymequiv}\ A\ {\isasymunion}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\ t\ {\isasymin}\ T{\isacharbraceright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
Now we define \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}} as the least set \isa{T} that includes
@@ -127,8 +127,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\isamarkupfalse%
-\ AF{\isacharunderscore}lemma{\isadigit{1}}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequoteclose}%
+\ AF{\isacharunderscore}lemma{\isadigit{1}}{\isacharcolon}\ {\isachardoublequoteopen}lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequoteclose}%
\isadelimproof
%
\endisadelimproof
@@ -225,11 +224,9 @@
path is parameterized by a predicate \isa{Q} that should hold along the path:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ path\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ {\isasymRightarrow}\ {\isacharparenleft}state\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
-\isanewline
-{\isachardoublequoteopen}path\ s\ Q\ {\isadigit{0}}\ {\isacharequal}\ s{\isachardoublequoteclose}\isanewline
+\ path\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ {\isasymRightarrow}\ {\isacharparenleft}state\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}path\ s\ Q\ {\isadigit{0}}\ {\isacharequal}\ s{\isachardoublequoteclose}\ {\isacharbar}\isanewline
{\isachardoublequoteopen}path\ s\ Q\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ Q\ n{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
--- a/doc-src/TutorialI/CTL/document/PDL.tex Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/CTL/document/PDL.tex Thu May 29 22:45:33 2008 +0200
@@ -40,25 +40,18 @@
\noindent
This resembles the boolean expression case study in
\S\ref{sec:boolex}.
-A validity relation between
-states and formulae specifies the semantics:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ valid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ {\isasymRightarrow}\ formula\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}\ {\isasymTurnstile}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{8}}{\isadigit{0}}{\isacharcomma}{\isadigit{8}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{8}}{\isadigit{0}}{\isacharparenright}%
-\begin{isamarkuptext}%
-\noindent
+A validity relation between states and formulae specifies the semantics.
The syntax annotation allows us to write \isa{s\ {\isasymTurnstile}\ f} instead of
-\hbox{\isa{valid\ s\ f}}.
-The definition of \isa{{\isasymTurnstile}} is by recursion over the syntax:%
+\hbox{\isa{valid\ s\ f}}. The definition is by recursion over the syntax:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{primrec}\isamarkupfalse%
-\isanewline
-{\isachardoublequoteopen}s\ {\isasymTurnstile}\ Atom\ a\ \ {\isacharequal}\ {\isacharparenleft}a\ {\isasymin}\ L\ s{\isacharparenright}{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}s\ {\isasymTurnstile}\ Neg\ f\ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymnot}{\isacharparenleft}s\ {\isasymTurnstile}\ f{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}s\ {\isasymTurnstile}\ And\ f\ g\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymTurnstile}\ f\ {\isasymand}\ s\ {\isasymTurnstile}\ g{\isacharparenright}{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}s\ {\isasymTurnstile}\ AX\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\ t\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ valid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ {\isasymRightarrow}\ formula\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}\ {\isasymTurnstile}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{8}}{\isadigit{0}}{\isacharcomma}{\isadigit{8}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{8}}{\isadigit{0}}{\isacharparenright}\isanewline
+\isakeyword{where}\isanewline
+{\isachardoublequoteopen}s\ {\isasymTurnstile}\ Atom\ a\ \ {\isacharequal}\ {\isacharparenleft}a\ {\isasymin}\ L\ s{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}s\ {\isasymTurnstile}\ Neg\ f\ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymnot}{\isacharparenleft}s\ {\isasymTurnstile}\ f{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}s\ {\isasymTurnstile}\ And\ f\ g\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymTurnstile}\ f\ {\isasymand}\ s\ {\isasymTurnstile}\ g{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}s\ {\isasymTurnstile}\ AX\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\ t\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
{\isachardoublequoteopen}s\ {\isasymTurnstile}\ EF\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
@@ -68,18 +61,17 @@
true. The future is expressed via \isa{\isactrlsup {\isacharasterisk}}, the reflexive transitive
closure. Because of reflexivity, the future includes the present.
-Now we come to the model checker itself. It maps a formula into the set of
-states where the formula is true. It too is defined by recursion over the syntax:%
+Now we come to the model checker itself. It maps a formula into the
+set of states where the formula is true. It too is defined by
+recursion over the syntax:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ mc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}formula\ {\isasymRightarrow}\ state\ set{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
-\isanewline
-{\isachardoublequoteopen}mc{\isacharparenleft}Atom\ a{\isacharparenright}\ \ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ a\ {\isasymin}\ L\ s{\isacharbraceright}{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}mc{\isacharparenleft}Neg\ f{\isacharparenright}\ \ \ {\isacharequal}\ {\isacharminus}mc\ f{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}mc{\isacharparenleft}And\ f\ g{\isacharparenright}\ {\isacharequal}\ mc\ f\ {\isasyminter}\ mc\ g{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}mc{\isacharparenleft}AX\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ \ {\isasymlongrightarrow}\ t\ {\isasymin}\ mc\ f{\isacharbraceright}{\isachardoublequoteclose}\isanewline
+\ mc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}formula\ {\isasymRightarrow}\ state\ set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}mc{\isacharparenleft}Atom\ a{\isacharparenright}\ \ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ a\ {\isasymin}\ L\ s{\isacharbraceright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}mc{\isacharparenleft}Neg\ f{\isacharparenright}\ \ \ {\isacharequal}\ {\isacharminus}mc\ f{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}mc{\isacharparenleft}And\ f\ g{\isacharparenright}\ {\isacharequal}\ mc\ f\ {\isasyminter}\ mc\ g{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}mc{\isacharparenleft}AX\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ \ {\isasymlongrightarrow}\ t\ {\isasymin}\ mc\ f{\isacharbraceright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
{\isachardoublequoteopen}mc{\isacharparenleft}EF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
--- a/doc-src/TutorialI/CodeGen/CodeGen.thy Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/CodeGen/CodeGen.thy Thu May 29 22:45:33 2008 +0200
@@ -28,11 +28,10 @@
values is easily defined:
*}
-consts "value" :: "('a,'v)expr \<Rightarrow> ('a \<Rightarrow> 'v) \<Rightarrow> 'v";
-primrec
-"value (Cex v) env = v"
-"value (Vex a) env = env a"
-"value (Bex f e1 e2) env = f (value e1 env) (value e2 env)";
+primrec "value" :: "('a,'v)expr \<Rightarrow> ('a \<Rightarrow> 'v) \<Rightarrow> 'v" where
+"value (Cex v) env = v" |
+"value (Vex a) env = env a" |
+"value (Bex f e1 e2) env = f (value e1 env) (value e2 env)"
text{*
The stack machine has three instructions: load a constant value onto the
@@ -54,13 +53,13 @@
unchanged:
*}
-consts exec :: "('a,'v)instr list \<Rightarrow> ('a\<Rightarrow>'v) \<Rightarrow> 'v list \<Rightarrow> 'v list";
-primrec
-"exec [] s vs = vs"
+primrec exec :: "('a,'v)instr list \<Rightarrow> ('a\<Rightarrow>'v) \<Rightarrow> 'v list \<Rightarrow> 'v list"
+where
+"exec [] s vs = vs" |
"exec (i#is) s vs = (case i of
Const v \<Rightarrow> exec is s (v#vs)
| Load a \<Rightarrow> exec is s ((s a)#vs)
- | Apply f \<Rightarrow> exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))";
+ | Apply f \<Rightarrow> exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))"
text{*\noindent
Recall that @{term"hd"} and @{term"tl"}
@@ -75,10 +74,9 @@
definition is obvious:
*}
-consts compile :: "('a,'v)expr \<Rightarrow> ('a,'v)instr list"
-primrec
-"compile (Cex v) = [Const v]"
-"compile (Vex a) = [Load a]"
+primrec compile :: "('a,'v)expr \<Rightarrow> ('a,'v)instr list" where
+"compile (Cex v) = [Const v]" |
+"compile (Vex a) = [Load a]" |
"compile (Bex f e1 e2) = (compile e2) @ (compile e1) @ [Apply f]"
text{*
--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Thu May 29 22:45:33 2008 +0200
@@ -46,12 +46,10 @@
values is easily defined:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ {\isachardoublequoteopen}value{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}v{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}v{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
-\isanewline
-{\isachardoublequoteopen}value\ {\isacharparenleft}Cex\ v{\isacharparenright}\ env\ {\isacharequal}\ v{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}value\ {\isacharparenleft}Vex\ a{\isacharparenright}\ env\ {\isacharequal}\ env\ a{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}value{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}v{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}v{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}value\ {\isacharparenleft}Cex\ v{\isacharparenright}\ env\ {\isacharequal}\ v{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}value\ {\isacharparenleft}Vex\ a{\isacharparenright}\ env\ {\isacharequal}\ env\ a{\isachardoublequoteclose}\ {\isacharbar}\isanewline
{\isachardoublequoteopen}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}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
The stack machine has three instructions: load a constant value onto the
@@ -73,11 +71,10 @@
unchanged:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
+\isacommand{primrec}\isamarkupfalse%
\ exec\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\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{\isachardoublequoteclose}\isanewline
-\isacommand{primrec}\isamarkupfalse%
-\isanewline
-{\isachardoublequoteopen}exec\ {\isacharbrackleft}{\isacharbrackright}\ s\ vs\ {\isacharequal}\ vs{\isachardoublequoteclose}\isanewline
+\isakeyword{where}\isanewline
+{\isachardoublequoteopen}exec\ {\isacharbrackleft}{\isacharbrackright}\ s\ vs\ {\isacharequal}\ vs{\isachardoublequoteclose}\ {\isacharbar}\isanewline
{\isachardoublequoteopen}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
@@ -96,12 +93,10 @@
definition is obvious:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ compile\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
-\isanewline
-{\isachardoublequoteopen}compile\ {\isacharparenleft}Cex\ v{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Const\ v{\isacharbrackright}{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}compile\ {\isacharparenleft}Vex\ a{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Load\ a{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ compile\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}compile\ {\isacharparenleft}Cex\ v{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Const\ v{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}compile\ {\isacharparenleft}Vex\ a{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Load\ a{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
{\isachardoublequoteopen}compile\ {\isacharparenleft}Bex\ f\ e{\isadigit{1}}\ e{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}compile\ e{\isadigit{2}}{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}compile\ e{\isadigit{1}}{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}Apply\ f{\isacharbrackright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
Now we have to prove the correctness of the compiler, i.e.\ that the
--- a/doc-src/TutorialI/Datatype/ABexpr.thy Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Datatype/ABexpr.thy Thu May 29 22:45:33 2008 +0200
@@ -35,56 +35,52 @@
The semantics is given by two evaluation functions:
*}
-consts evala :: "'a aexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"
- evalb :: "'a bexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool";
+primrec evala :: "'a aexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat" and
+ evalb :: "'a bexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool" where
+"evala (IF b a1 a2) env =
+ (if evalb b env then evala a1 env else evala a2 env)" |
+"evala (Sum a1 a2) env = evala a1 env + evala a2 env" |
+"evala (Diff a1 a2) env = evala a1 env - evala a2 env" |
+"evala (Var v) env = env v" |
+"evala (Num n) env = n" |
+
+"evalb (Less a1 a2) env = (evala a1 env < evala a2 env)" |
+"evalb (And b1 b2) env = (evalb b1 env \<and> evalb b2 env)" |
+"evalb (Neg b) env = (\<not> evalb b env)"
text{*\noindent
-Both take an expression and an environment (a mapping from variables @{typ"'a"} to values
-@{typ"nat"}) and return its arithmetic/boolean
-value. Since the datatypes are mutually recursive, so are functions that
-operate on them. Hence they need to be defined in a single \isacommand{primrec}
-section:
-*}
-primrec
- "evala (IF b a1 a2) env =
- (if evalb b env then evala a1 env else evala a2 env)"
- "evala (Sum a1 a2) env = evala a1 env + evala a2 env"
- "evala (Diff a1 a2) env = evala a1 env - evala a2 env"
- "evala (Var v) env = env v"
- "evala (Num n) env = n"
+Both take an expression and an environment (a mapping from variables
+@{typ"'a"} to values @{typ"nat"}) and return its arithmetic/boolean
+value. Since the datatypes are mutually recursive, so are functions
+that operate on them. Hence they need to be defined in a single
+\isacommand{primrec} section. Notice the \isakeyword{and} separating
+the declarations of @{const evala} and @{const evalb}. Their defining
+equations need not be split into two groups;
+the empty line is purely for readability.
- "evalb (Less a1 a2) env = (evala a1 env < evala a2 env)"
- "evalb (And b1 b2) env = (evalb b1 env \<and> evalb b2 env)"
- "evalb (Neg b) env = (\<not> evalb b env)"
-
-text{*\noindent
In the same fashion we also define two functions that perform substitution:
*}
-consts substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp"
- substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp";
+primrec substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp" and
+ substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp" where
+"substa s (IF b a1 a2) =
+ IF (substb s b) (substa s a1) (substa s a2)" |
+"substa s (Sum a1 a2) = Sum (substa s a1) (substa s a2)" |
+"substa s (Diff a1 a2) = Diff (substa s a1) (substa s a2)" |
+"substa s (Var v) = s v" |
+"substa s (Num n) = Num n" |
+
+"substb s (Less a1 a2) = Less (substa s a1) (substa s a2)" |
+"substb s (And b1 b2) = And (substb s b1) (substb s b2)" |
+"substb s (Neg b) = Neg (substb s b)"
text{*\noindent
-The first argument is a function mapping variables to expressions, the
+Their first argument is a function mapping variables to expressions, the
substitution. It is applied to all variables in the second argument. As a
result, the type of variables in the expression may change from @{typ"'a"}
to @{typ"'b"}. Note that there are only arithmetic and no boolean variables.
-*}
-primrec
- "substa s (IF b a1 a2) =
- IF (substb s b) (substa s a1) (substa s a2)"
- "substa s (Sum a1 a2) = Sum (substa s a1) (substa s a2)"
- "substa s (Diff a1 a2) = Diff (substa s a1) (substa s a2)"
- "substa s (Var v) = s v"
- "substa s (Num n) = Num n"
-
- "substb s (Less a1 a2) = Less (substa s a1) (substa s a2)"
- "substb s (And b1 b2) = And (substb s b1) (substb s b2)"
- "substb s (Neg b) = Neg (substb s b)";
-
-text{*
Now we can prove a fundamental theorem about the interaction between
evaluation and substitution: applying a substitution $s$ to an expression $a$
and evaluating the result in an environment $env$ yields the same result as
@@ -128,18 +124,16 @@
\end{exercise}
*}
(*<*)
-consts norma :: "'a aexp \<Rightarrow> 'a aexp"
- normb :: "'a bexp \<Rightarrow> 'a aexp \<Rightarrow> 'a aexp \<Rightarrow> 'a aexp"
-
-primrec
-"norma (IF b t e) = (normb b (norma t) (norma e))"
-"norma (Sum a1 a2) = Sum (norma a1) (norma a2)"
-"norma (Diff a1 a2) = Diff (norma a1) (norma a2)"
-"norma (Var v) = Var v"
-"norma (Num n) = Num n"
+primrec norma :: "'a aexp \<Rightarrow> 'a aexp" and
+ normb :: "'a bexp \<Rightarrow> 'a aexp \<Rightarrow> 'a aexp \<Rightarrow> 'a aexp" where
+"norma (IF b t e) = (normb b (norma t) (norma e))" |
+"norma (Sum a1 a2) = Sum (norma a1) (norma a2)" |
+"norma (Diff a1 a2) = Diff (norma a1) (norma a2)" |
+"norma (Var v) = Var v" |
+"norma (Num n) = Num n" |
-"normb (Less a1 a2) t e = IF (Less (norma a1) (norma a2)) t e"
-"normb (And b1 b2) t e = normb b1 (normb b2 t e) e"
+"normb (Less a1 a2) t e = IF (Less (norma a1) (norma a2)) t e" |
+"normb (And b1 b2) t e = normb b1 (normb b2 t e) e" |
"normb (Neg b) t e = normb b e t"
lemma " evala (norma a) env = evala a env
@@ -148,18 +142,16 @@
apply (simp_all)
done
-consts normala :: "'a aexp \<Rightarrow> bool"
- normalb :: "'b bexp \<Rightarrow> bool"
+primrec normala :: "'a aexp \<Rightarrow> bool" and
+ normalb :: "'a bexp \<Rightarrow> bool" where
+"normala (IF b t e) = (normalb b \<and> normala t \<and> normala e)" |
+"normala (Sum a1 a2) = (normala a1 \<and> normala a2)" |
+"normala (Diff a1 a2) = (normala a1 \<and> normala a2)" |
+"normala (Var v) = True" |
+"normala (Num n) = True" |
-primrec
-"normala (IF b t e) = (normalb b \<and> normala t \<and> normala e)"
-"normala (Sum a1 a2) = (normala a1 \<and> normala a2)"
-"normala (Diff a1 a2) = (normala a1 \<and> normala a2)"
-"normala (Var v) = True"
-"normala (Num n) = True"
-
-"normalb (Less a1 a2) = (normala a1 \<and> normala a2)"
-"normalb (And b1 b2) = False"
+"normalb (Less a1 a2) = (normala a1 \<and> normala a2)" |
+"normalb (And b1 b2) = False" |
"normalb (Neg b) = False"
lemma "normala (norma (a::'a aexp)) \<and>
--- a/doc-src/TutorialI/Datatype/Fundata.thy Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Datatype/Fundata.thy Thu May 29 22:45:33 2008 +0200
@@ -19,9 +19,9 @@
Function @{term"map_bt"} applies a function to all labels in a @{text"bigtree"}:
*}
-consts map_bt :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a,'i)bigtree \<Rightarrow> ('b,'i)bigtree"
-primrec
-"map_bt f Tip = Tip"
+primrec map_bt :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a,'i)bigtree \<Rightarrow> ('b,'i)bigtree"
+where
+"map_bt f Tip = Tip" |
"map_bt f (Br a F) = Br (f a) (\<lambda>i. map_bt f (F i))"
text{*\noindent This is a valid \isacommand{primrec} definition because the
--- a/doc-src/TutorialI/Datatype/Nested.thy Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy Thu May 29 22:45:33 2008 +0200
@@ -43,17 +43,16 @@
lists, we need to define two substitution functions simultaneously:
*}
-consts
-subst :: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term \<Rightarrow> ('v,'f)term"
-substs:: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term list \<Rightarrow> ('v,'f)term list";
+primrec
+subst :: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term \<Rightarrow> ('v,'f)term" and
+substs:: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term list \<Rightarrow> ('v,'f)term list"
+where
+"subst s (Var x) = s x" |
+ subst_App:
+"subst s (App f ts) = App f (substs s ts)" |
-primrec
- "subst s (Var x) = s x"
- subst_App:
- "subst s (App f ts) = App f (substs s ts)"
-
- "substs s [] = []"
- "substs s (t # ts) = subst s t # substs s ts";
+"substs s [] = []" |
+"substs s (t # ts) = subst s t # substs s ts"
text{*\noindent
Individual equations in a \commdx{primrec} definition may be
--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Thu May 29 22:45:33 2008 +0200
@@ -49,59 +49,54 @@
The semantics is given by two evaluation functions:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ \ evala\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ aexp\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ evalb\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ bexp\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}%
+\isacommand{primrec}\isamarkupfalse%
+\ evala\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ aexp\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
+\ \ \ \ \ \ \ \ \ evalb\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ bexp\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}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}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}evala\ {\isacharparenleft}Sum\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ evala\ a{\isadigit{1}}\ env\ {\isacharplus}\ evala\ a{\isadigit{2}}\ env{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}evala\ {\isacharparenleft}Diff\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ evala\ a{\isadigit{1}}\ env\ {\isacharminus}\ evala\ a{\isadigit{2}}\ env{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}evala\ {\isacharparenleft}Var\ v{\isacharparenright}\ env\ {\isacharequal}\ env\ v{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}evala\ {\isacharparenleft}Num\ n{\isacharparenright}\ env\ {\isacharequal}\ n{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+\isanewline
+{\isachardoublequoteopen}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}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}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}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}evalb\ {\isacharparenleft}Neg\ b{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ evalb\ b\ env{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
-Both take an expression and an environment (a mapping from variables \isa{{\isacharprime}a} to values
-\isa{nat}) and return its arithmetic/boolean
-value. Since the datatypes are mutually recursive, so are functions that
-operate on them. Hence they need to be defined in a single \isacommand{primrec}
-section:%
+
+Both take an expression and an environment (a mapping from variables
+\isa{{\isacharprime}a} to values \isa{nat}) and return its arithmetic/boolean
+value. Since the datatypes are mutually recursive, so are functions
+that operate on them. Hence they need to be defined in a single
+\isacommand{primrec} section. Notice the \isakeyword{and} separating
+the declarations of \isa{evala} and \isa{evalb}. Their defining
+equations need not be split into two groups;
+the empty line is purely for readability.
+
+In the same fashion we also define two functions that perform substitution:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{primrec}\isamarkupfalse%
+\ substa\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ aexp{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ aexp\ {\isasymRightarrow}\ {\isacharprime}b\ aexp{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
+\ \ \ \ \ \ \ \ \ substb\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ aexp{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ bexp\ {\isasymRightarrow}\ {\isacharprime}b\ bexp{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}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}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}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}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}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}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}substa\ s\ {\isacharparenleft}Var\ v{\isacharparenright}\ {\isacharequal}\ s\ v{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}substa\ s\ {\isacharparenleft}Num\ n{\isacharparenright}\ {\isacharequal}\ Num\ n{\isachardoublequoteclose}\ {\isacharbar}\isanewline
\isanewline
-\ \ {\isachardoublequoteopen}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}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}evala\ {\isacharparenleft}Sum\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ evala\ a{\isadigit{1}}\ env\ {\isacharplus}\ evala\ a{\isadigit{2}}\ env{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}evala\ {\isacharparenleft}Diff\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ evala\ a{\isadigit{1}}\ env\ {\isacharminus}\ evala\ a{\isadigit{2}}\ env{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}evala\ {\isacharparenleft}Var\ v{\isacharparenright}\ env\ {\isacharequal}\ env\ v{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}evala\ {\isacharparenleft}Num\ n{\isacharparenright}\ env\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
-\isanewline
-\ \ {\isachardoublequoteopen}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}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}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}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}evalb\ {\isacharparenleft}Neg\ b{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ evalb\ b\ env{\isacharparenright}{\isachardoublequoteclose}%
+{\isachardoublequoteopen}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}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}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}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}substb\ s\ {\isacharparenleft}Neg\ b{\isacharparenright}\ {\isacharequal}\ Neg\ {\isacharparenleft}substb\ s\ b{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
-In the same fashion we also define two functions that perform substitution:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ substa\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ aexp{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ aexp\ {\isasymRightarrow}\ {\isacharprime}b\ aexp{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ substb\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ aexp{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ bexp\ {\isasymRightarrow}\ {\isacharprime}b\ bexp{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent
-The first argument is a function mapping variables to expressions, the
+Their first argument is a function mapping variables to expressions, the
substitution. It is applied to all variables in the second argument. As a
result, the type of variables in the expression may change from \isa{{\isacharprime}a}
-to \isa{{\isacharprime}b}. Note that there are only arithmetic and no boolean variables.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{primrec}\isamarkupfalse%
-\isanewline
-\ \ {\isachardoublequoteopen}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}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}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}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}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}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}substa\ s\ {\isacharparenleft}Var\ v{\isacharparenright}\ {\isacharequal}\ s\ v{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}substa\ s\ {\isacharparenleft}Num\ n{\isacharparenright}\ {\isacharequal}\ Num\ n{\isachardoublequoteclose}\isanewline
-\isanewline
-\ \ {\isachardoublequoteopen}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}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}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}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}substb\ s\ {\isacharparenleft}Neg\ b{\isacharparenright}\ {\isacharequal}\ Neg\ {\isacharparenleft}substb\ s\ b{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
+to \isa{{\isacharprime}b}. Note that there are only arithmetic and no boolean variables.
+
Now we can prove a fundamental theorem about the interaction between
evaluation and substitution: applying a substitution $s$ to an expression $a$
and evaluating the result in an environment $env$ yields the same result as
--- a/doc-src/TutorialI/Datatype/document/Fundata.tex Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Thu May 29 22:45:33 2008 +0200
@@ -35,11 +35,10 @@
Function \isa{map{\isacharunderscore}bt} applies a function to all labels in a \isa{bigtree}:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
+\isacommand{primrec}\isamarkupfalse%
\ map{\isacharunderscore}bt\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\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{\isachardoublequoteclose}\isanewline
-\isacommand{primrec}\isamarkupfalse%
-\isanewline
-{\isachardoublequoteopen}map{\isacharunderscore}bt\ f\ Tip\ \ \ \ \ \ {\isacharequal}\ Tip{\isachardoublequoteclose}\isanewline
+\isakeyword{where}\isanewline
+{\isachardoublequoteopen}map{\isacharunderscore}bt\ f\ Tip\ \ \ \ \ \ {\isacharequal}\ Tip{\isachardoublequoteclose}\ {\isacharbar}\isanewline
{\isachardoublequoteopen}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Br\ a\ F{\isacharparenright}\ {\isacharequal}\ Br\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ i{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent This is a valid \isacommand{primrec} definition because the
--- a/doc-src/TutorialI/Datatype/document/Nested.tex Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex Thu May 29 22:45:33 2008 +0200
@@ -56,19 +56,17 @@
lists, we need to define two substitution functions simultaneously:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\isanewline
-subst\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}v{\isasymRightarrow}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ \ \ \ \ \ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isachardoublequoteclose}\isanewline
-substs{\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}v{\isasymRightarrow}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isachardoublequoteclose}\isanewline
-\isanewline
\isacommand{primrec}\isamarkupfalse%
\isanewline
-\ \ {\isachardoublequoteopen}subst\ s\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ s\ x{\isachardoublequoteclose}\isanewline
+subst\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}v{\isasymRightarrow}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ \ \ \ \ \ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
+substs{\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}v{\isasymRightarrow}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isachardoublequoteclose}\isanewline
+\isakeyword{where}\isanewline
+{\isachardoublequoteopen}subst\ s\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ s\ x{\isachardoublequoteclose}\ {\isacharbar}\isanewline
\ \ subst{\isacharunderscore}App{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}substs\ s\ ts{\isacharparenright}{\isachardoublequoteclose}\isanewline
+{\isachardoublequoteopen}subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}substs\ s\ ts{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
\isanewline
-\ \ {\isachardoublequoteopen}substs\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}substs\ s\ {\isacharparenleft}t\ {\isacharhash}\ ts{\isacharparenright}\ {\isacharequal}\ subst\ s\ t\ {\isacharhash}\ substs\ s\ ts{\isachardoublequoteclose}%
+{\isachardoublequoteopen}substs\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}substs\ s\ {\isacharparenleft}t\ {\isacharhash}\ ts{\isacharparenright}\ {\isacharequal}\ subst\ s\ t\ {\isacharhash}\ substs\ s\ ts{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
Individual equations in a \commdx{primrec} definition may be
--- a/doc-src/TutorialI/Documents/Documents.thy Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy Thu May 29 22:45:33 2008 +0200
@@ -26,7 +26,7 @@
text {*
Syntax annotations may be included wherever constants are declared,
- such as \isacommand{consts} and \isacommand{constdefs} --- and also
+ such as \isacommand{definition} and \isacommand{primrec} --- and also
\isacommand{datatype}, which declares constructor operations.
Type-constructors may be annotated as well, although this is less
frequently encountered in practice (the infix type @{text "\<times>"} comes
@@ -37,9 +37,8 @@
operation on boolean values illustrates typical infix declarations.
*}
-constdefs
- xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "[+]" 60)
- "A [+] B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
+definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "[+]" 60)
+where "A [+] B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
text {*
\noindent Now @{text "xor A B"} and @{text "A [+] B"} refer to the
@@ -142,9 +141,8 @@
hide const xor
setup {* Sign.add_path "version1" *}
(*>*)
-constdefs
- xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<oplus>" 60)
- "A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
+definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<oplus>" 60)
+where "A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
(*<*)
local
(*>*)
@@ -166,18 +164,18 @@
hide const xor
setup {* Sign.add_path "version2" *}
(*>*)
-constdefs
- xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "[+]\<ignore>" 60)
- "A [+]\<ignore> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
+definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "[+]\<ignore>" 60)
+where "A [+]\<ignore> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
notation (xsymbols) xor (infixl "\<oplus>\<ignore>" 60)
(*<*)
local
(*>*)
-text {*The \commdx{notation} command associates a mixfix
-annotation with a known constant. The print mode specification of
-\isakeyword{syntax}, here @{text "(xsymbols)"}, is optional.
+text {*\noindent
+The \commdx{notation} command associates a mixfix
+annotation with a known constant. The print mode specification,
+here @{text "(xsymbols)"}, is optional.
We may now write @{text "A [+] B"} or @{text "A \<oplus> B"} in input, while
output uses the nicer syntax of $xsymbols$ whenever that print mode is
@@ -212,8 +210,7 @@
achieves conformance with notational standards of the European
Commission.
- Prefix syntax works the same way for \isakeyword{consts} or
- \isakeyword{constdefs}.
+ Prefix syntax works the same way for other commands that introduce new constants, e.g. \isakeyword{primrec}.
*}
@@ -232,10 +229,9 @@
A typical use of abbreviations is to introduce relational notation for
membership in a set of pairs, replacing @{text "(x, y) \<in> sim"} by
-@{text "x \<approx> y"}. *}
-
-consts sim :: "('a \<times> 'a) set"
-
+@{text "x \<approx> y"}. We assume that a constant @{text sim } of type
+@{typ"('a \<times> 'a) set"} has been introduced at this point. *}
+(*<*)consts sim :: "('a \<times> 'a) set"(*>*)
abbreviation sim2 :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<approx>" 50)
where "x \<approx> y \<equiv> (x, y) \<in> sim"
@@ -259,7 +255,7 @@
text {* \noindent The notation @{text \<noteq>} is introduced separately to restrict it
to the \emph{xsymbols} mode.
- Abbreviations are appropriate when the defined concept is a
+Abbreviations are appropriate when the defined concept is a
simple variation on an existing one. But because of the automatic
folding and unfolding of abbreviations, they do not scale up well to
large hierarchies of concepts. Abbreviations do not replace
--- a/doc-src/TutorialI/Documents/document/Documents.tex Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Thu May 29 22:45:33 2008 +0200
@@ -43,7 +43,7 @@
%
\begin{isamarkuptext}%
Syntax annotations may be included wherever constants are declared,
- such as \isacommand{consts} and \isacommand{constdefs} --- and also
+ such as \isacommand{definition} and \isacommand{primrec} --- and also
\isacommand{datatype}, which declares constructor operations.
Type-constructors may be annotated as well, although this is less
frequently encountered in practice (the infix type \isa{{\isasymtimes}} comes
@@ -54,10 +54,9 @@
operation on boolean values illustrates typical infix declarations.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{constdefs}\isamarkupfalse%
-\isanewline
-\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ {\isachardoublequoteopen}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}%
+\isacommand{definition}\isamarkupfalse%
+\ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
+\isakeyword{where}\ {\isachardoublequoteopen}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent Now \isa{xor\ A\ B} and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} refer to the
same expression internally. Any curried function with at least two
@@ -166,10 +165,9 @@
\isadelimML
%
\endisadelimML
-\isacommand{constdefs}\isamarkupfalse%
-\isanewline
-\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ {\isachardoublequoteopen}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}%
+\isacommand{definition}\isamarkupfalse%
+\ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
+\isakeyword{where}\ {\isachardoublequoteopen}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent The X-Symbol package within Proof~General provides several
input methods to enter \isa{{\isasymoplus}} in the text. If all fails one may
@@ -196,17 +194,17 @@
\isadelimML
%
\endisadelimML
-\isacommand{constdefs}\isamarkupfalse%
-\isanewline
-\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ {\isachardoublequoteopen}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
+\isakeyword{where}\ {\isachardoublequoteopen}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{notation}\isamarkupfalse%
\ {\isacharparenleft}xsymbols{\isacharparenright}\ xor\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}%
\begin{isamarkuptext}%
+\noindent
The \commdx{notation} command associates a mixfix
-annotation with a known constant. The print mode specification of
-\isakeyword{syntax}, here \isa{{\isacharparenleft}xsymbols{\isacharparenright}}, is optional.
+annotation with a known constant. The print mode specification,
+here \isa{{\isacharparenleft}xsymbols{\isacharparenright}}, is optional.
We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in input, while
output uses the nicer syntax of $xsymbols$ whenever that print mode is
@@ -243,8 +241,7 @@
achieves conformance with notational standards of the European
Commission.
- Prefix syntax works the same way for \isakeyword{consts} or
- \isakeyword{constdefs}.%
+ Prefix syntax works the same way for other commands that introduce new constants, e.g. \isakeyword{primrec}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -266,12 +263,10 @@
A typical use of abbreviations is to introduce relational notation for
membership in a set of pairs, replacing \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} by
-\isa{x\ {\isasymapprox}\ y}.%
+\isa{x\ {\isasymapprox}\ y}. We assume that a constant \isa{sim} of type
+\isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set} has been introduced at this point.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ sim\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequoteclose}\isanewline
-\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ sim{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequoteopen}{\isasymapprox}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
\isakeyword{where}\ {\isachardoublequoteopen}x\ {\isasymapprox}\ y\ \ {\isasymequiv}\ \ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim{\isachardoublequoteclose}%
@@ -297,7 +292,7 @@
\noindent The notation \isa{{\isasymnoteq}} is introduced separately to restrict it
to the \emph{xsymbols} mode.
- Abbreviations are appropriate when the defined concept is a
+Abbreviations are appropriate when the defined concept is a
simple variation on an existing one. But because of the automatic
folding and unfolding of abbreviations, they do not scale up well to
large hierarchies of concepts. Abbreviations do not replace
--- a/doc-src/TutorialI/Fun/document/fun0.tex Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Fun/document/fun0.tex Thu May 29 22:45:33 2008 +0200
@@ -24,9 +24,9 @@
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
-\ \ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
-\ \ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc{\isacharparenleft}Suc\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ x\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ x{\isacharparenright}{\isachardoublequoteclose}%
+{\isachardoublequoteopen}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}fib\ {\isacharparenleft}Suc{\isacharparenleft}Suc\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ x\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ x{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
This resembles ordinary functional programming languages. Note the obligatory
@@ -40,9 +40,9 @@
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ sep\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}sep\ a\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
-\ \ {\isachardoublequoteopen}sep\ a\ {\isacharbrackleft}x{\isacharbrackright}\ \ \ \ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
-\ \ {\isachardoublequoteopen}sep\ a\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\ a\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequoteclose}%
+{\isachardoublequoteopen}sep\ a\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}sep\ a\ {\isacharbrackleft}x{\isacharbrackright}\ \ \ \ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}sep\ a\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\ a\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
This time the length of the list decreases with the
@@ -54,8 +54,8 @@
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ last\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}last\ {\isacharbrackleft}x{\isacharbrackright}\ \ \ \ \ \ {\isacharequal}\ x{\isachardoublequoteclose}\ {\isacharbar}\isanewline
-\ \ {\isachardoublequoteopen}last\ {\isacharparenleft}{\isacharunderscore}{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ last\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequoteclose}%
+{\isachardoublequoteopen}last\ {\isacharbrackleft}x{\isacharbrackright}\ \ \ \ \ \ {\isacharequal}\ x{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}last\ {\isacharparenleft}{\isacharunderscore}{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ last\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
Overlapping patterns are disambiguated by taking the order of equations into
account, just as in functional programming:%
@@ -63,8 +63,8 @@
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ sep{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}sep{\isadigit{1}}\ a\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isadigit{1}}\ a\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
-\ \ {\isachardoublequoteopen}sep{\isadigit{1}}\ {\isacharunderscore}\ xs\ \ \ \ \ \ \ {\isacharequal}\ xs{\isachardoublequoteclose}%
+{\isachardoublequoteopen}sep{\isadigit{1}}\ a\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isadigit{1}}\ a\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}sep{\isadigit{1}}\ {\isacharunderscore}\ xs\ \ \ \ \ \ \ {\isacharequal}\ xs{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
To guarantee that the second equation can only be applied if the first
@@ -79,8 +79,8 @@
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ swap{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}swap{\isadigit{1}}{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ y{\isacharhash}x{\isacharhash}zs{\isachardoublequoteclose}\ {\isacharbar}\isanewline
-\ \ {\isachardoublequoteopen}swap{\isadigit{1}}{\isadigit{2}}\ zs\ \ \ \ \ \ \ {\isacharequal}\ zs{\isachardoublequoteclose}%
+{\isachardoublequoteopen}swap{\isadigit{1}}{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ y{\isacharhash}x{\isacharhash}zs{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}swap{\isadigit{1}}{\isadigit{2}}\ zs\ \ \ \ \ \ \ {\isacharequal}\ zs{\isachardoublequoteclose}%
\begin{isamarkuptext}%
After a function~$f$ has been defined via \isacommand{fun},
its defining equations (or variants derived from them) are available
@@ -108,9 +108,9 @@
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ ack{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}ack{\isadigit{2}}\ n\ {\isadigit{0}}\ {\isacharequal}\ Suc\ n{\isachardoublequoteclose}\ {\isacharbar}\isanewline
-\ \ {\isachardoublequoteopen}ack{\isadigit{2}}\ {\isadigit{0}}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ ack{\isadigit{2}}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ m{\isachardoublequoteclose}\ {\isacharbar}\isanewline
-\ \ {\isachardoublequoteopen}ack{\isadigit{2}}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ ack{\isadigit{2}}\ {\isacharparenleft}ack{\isadigit{2}}\ n\ {\isacharparenleft}Suc\ m{\isacharparenright}{\isacharparenright}\ m{\isachardoublequoteclose}%
+{\isachardoublequoteopen}ack{\isadigit{2}}\ n\ {\isadigit{0}}\ {\isacharequal}\ Suc\ n{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}ack{\isadigit{2}}\ {\isadigit{0}}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ ack{\isadigit{2}}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ m{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}ack{\isadigit{2}}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ ack{\isadigit{2}}\ {\isacharparenleft}ack{\isadigit{2}}\ n\ {\isacharparenleft}Suc\ m{\isacharparenright}{\isacharparenright}\ m{\isachardoublequoteclose}%
\begin{isamarkuptext}%
The order of arguments has no influence on whether
\isacommand{fun} can prove termination of a function. For more details
@@ -130,7 +130,7 @@
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ gcd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}gcd\ m\ n\ {\isacharequal}\ {\isacharparenleft}if\ n{\isacharequal}{\isadigit{0}}\ then\ m\ else\ gcd\ n\ {\isacharparenleft}m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
+{\isachardoublequoteopen}gcd\ m\ n\ {\isacharequal}\ {\isacharparenleft}if\ n{\isacharequal}{\isadigit{0}}\ then\ m\ else\ gcd\ n\ {\isacharparenleft}m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
The second argument decreases with each recursive call.
@@ -176,8 +176,8 @@
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ gcd{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}gcd{\isadigit{1}}\ m\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\ {\isacharbar}\isanewline
-\ \ {\isachardoublequoteopen}gcd{\isadigit{1}}\ m\ n\ {\isacharequal}\ gcd{\isadigit{1}}\ n\ {\isacharparenleft}m\ mod\ n{\isacharparenright}{\isachardoublequoteclose}%
+{\isachardoublequoteopen}gcd{\isadigit{1}}\ m\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}gcd{\isadigit{1}}\ m\ n\ {\isacharequal}\ gcd{\isadigit{1}}\ n\ {\isacharparenleft}m\ mod\ n{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
The order of equations is important: it hides the side condition
@@ -190,7 +190,7 @@
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ gcd{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}gcd{\isadigit{2}}\ m\ n\ {\isacharequal}\ {\isacharparenleft}case\ n{\isacharequal}{\isadigit{0}}\ of\ True\ {\isasymRightarrow}\ m\ {\isacharbar}\ False\ {\isasymRightarrow}\ gcd{\isadigit{2}}\ n\ {\isacharparenleft}m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
+{\isachardoublequoteopen}gcd{\isadigit{2}}\ m\ n\ {\isacharequal}\ {\isacharparenleft}case\ n{\isacharequal}{\isadigit{0}}\ of\ True\ {\isasymRightarrow}\ m\ {\isacharbar}\ False\ {\isasymRightarrow}\ gcd{\isadigit{2}}\ n\ {\isacharparenleft}m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
This is probably the neatest solution next to pattern matching, and it is
--- a/doc-src/TutorialI/Fun/fun0.thy Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Fun/fun0.thy Thu May 29 22:45:33 2008 +0200
@@ -10,9 +10,9 @@
*}
fun fib :: "nat \<Rightarrow> nat" where
- "fib 0 = 0" |
- "fib (Suc 0) = 1" |
- "fib (Suc(Suc x)) = fib x + fib (Suc x)"
+"fib 0 = 0" |
+"fib (Suc 0) = 1" |
+"fib (Suc(Suc x)) = fib x + fib (Suc x)"
text{*\noindent
This resembles ordinary functional programming languages. Note the obligatory
@@ -25,9 +25,9 @@
*}
fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "sep a [] = []" |
- "sep a [x] = [x]" |
- "sep a (x#y#zs) = x # a # sep a (y#zs)";
+"sep a [] = []" |
+"sep a [x] = [x]" |
+"sep a (x#y#zs) = x # a # sep a (y#zs)";
text{*\noindent
This time the length of the list decreases with the
@@ -38,8 +38,8 @@
*}
fun last :: "'a list \<Rightarrow> 'a" where
- "last [x] = x" |
- "last (_#y#zs) = last (y#zs)"
+"last [x] = x" |
+"last (_#y#zs) = last (y#zs)"
text{*
Overlapping patterns are disambiguated by taking the order of equations into
@@ -47,8 +47,8 @@
*}
fun sep1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "sep1 a (x#y#zs) = x # a # sep1 a (y#zs)" |
- "sep1 _ xs = xs"
+"sep1 a (x#y#zs) = x # a # sep1 a (y#zs)" |
+"sep1 _ xs = xs"
text{*\noindent
To guarantee that the second equation can only be applied if the first
@@ -62,8 +62,8 @@
*}
fun swap12 :: "'a list \<Rightarrow> 'a list" where
- "swap12 (x#y#zs) = y#x#zs" |
- "swap12 zs = zs"
+"swap12 (x#y#zs) = y#x#zs" |
+"swap12 zs = zs"
text{*
After a function~$f$ has been defined via \isacommand{fun},
@@ -90,9 +90,9 @@
function} is accepted: *}
fun ack2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
- "ack2 n 0 = Suc n" |
- "ack2 0 (Suc m) = ack2 (Suc 0) m" |
- "ack2 (Suc n) (Suc m) = ack2 (ack2 n (Suc m)) m"
+"ack2 n 0 = Suc n" |
+"ack2 0 (Suc m) = ack2 (Suc 0) m" |
+"ack2 (Suc n) (Suc m) = ack2 (ack2 n (Suc m)) m"
text{* The order of arguments has no influence on whether
\isacommand{fun} can prove termination of a function. For more details
@@ -111,7 +111,7 @@
*}
fun gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
- "gcd m n = (if n=0 then m else gcd n (m mod n))"
+"gcd m n = (if n=0 then m else gcd n (m mod n))"
text{*\noindent
The second argument decreases with each recursive call.
@@ -148,8 +148,8 @@
*}
fun gcd1 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
- "gcd1 m 0 = m" |
- "gcd1 m n = gcd1 n (m mod n)"
+"gcd1 m 0 = m" |
+"gcd1 m n = gcd1 n (m mod n)"
text{*\noindent
The order of equations is important: it hides the side condition
@@ -161,7 +161,7 @@
*}
fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
- "gcd2 m n = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2 n (m mod n))"
+"gcd2 m n = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2 n (m mod n))"
text{*\noindent
This is probably the neatest solution next to pattern matching, and it is
--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Thu May 29 22:45:33 2008 +0200
@@ -36,12 +36,11 @@
values:
*}
-consts "value" :: "boolex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool";
-primrec
-"value (Const b) env = b"
-"value (Var x) env = env x"
-"value (Neg b) env = (\<not> value b env)"
-"value (And b c) env = (value b env \<and> value c env)";
+primrec "value" :: "boolex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where
+"value (Const b) env = b" |
+"value (Var x) env = env x" |
+"value (Neg b) env = (\<not> value b env)" |
+"value (And b c) env = (value b env \<and> value c env)"
text{*\noindent
\subsubsection{If-Expressions}
@@ -58,12 +57,11 @@
The evaluation of If-expressions proceeds as for @{typ"boolex"}:
*}
-consts valif :: "ifex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool";
-primrec
-"valif (CIF b) env = b"
-"valif (VIF x) env = env x"
+primrec valif :: "ifex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where
+"valif (CIF b) env = b" |
+"valif (VIF x) env = env x" |
"valif (IF b t e) env = (if valif b env then valif t env
- else valif e env)";
+ else valif e env)"
text{*
\subsubsection{Converting Boolean and If-Expressions}
@@ -73,12 +71,11 @@
translate from @{typ"boolex"} into @{typ"ifex"}:
*}
-consts bool2if :: "boolex \<Rightarrow> ifex";
-primrec
-"bool2if (Const b) = CIF b"
-"bool2if (Var x) = VIF x"
-"bool2if (Neg b) = IF (bool2if b) (CIF False) (CIF True)"
-"bool2if (And b c) = IF (bool2if b) (bool2if c) (CIF False)";
+primrec bool2if :: "boolex \<Rightarrow> ifex" where
+"bool2if (Const b) = CIF b" |
+"bool2if (Var x) = VIF x" |
+"bool2if (Neg b) = IF (bool2if b) (CIF False) (CIF True)" |
+"bool2if (And b c) = IF (bool2if b) (bool2if c) (CIF False)"
text{*\noindent
At last, we have something we can verify: that @{term"bool2if"} preserves the
@@ -107,17 +104,15 @@
primitive recursive functions perform this task:
*}
-consts normif :: "ifex \<Rightarrow> ifex \<Rightarrow> ifex \<Rightarrow> ifex";
-primrec
-"normif (CIF b) t e = IF (CIF b) t e"
-"normif (VIF x) t e = IF (VIF x) t e"
-"normif (IF b t e) u f = normif b (normif t u f) (normif e u f)";
+primrec normif :: "ifex \<Rightarrow> ifex \<Rightarrow> ifex \<Rightarrow> ifex" where
+"normif (CIF b) t e = IF (CIF b) t e" |
+"normif (VIF x) t e = IF (VIF x) t e" |
+"normif (IF b t e) u f = normif b (normif t u f) (normif e u f)"
-consts norm :: "ifex \<Rightarrow> ifex";
-primrec
-"norm (CIF b) = CIF b"
-"norm (VIF x) = VIF x"
-"norm (IF b t e) = normif b (norm t) (norm e)";
+primrec norm :: "ifex \<Rightarrow> ifex" where
+"norm (CIF b) = CIF b" |
+"norm (VIF x) = VIF x" |
+"norm (IF b t e) = normif b (norm t) (norm e)"
text{*\noindent
Their interplay is tricky; we leave it to you to develop an
@@ -150,12 +145,11 @@
the above sense? We define a function that tests If-expressions for normality:
*}
-consts normal :: "ifex \<Rightarrow> bool";
-primrec
-"normal(CIF b) = True"
-"normal(VIF x) = True"
+primrec normal :: "ifex \<Rightarrow> bool" where
+"normal(CIF b) = True" |
+"normal(VIF x) = True" |
"normal(IF b t e) = (normal t \<and> normal e \<and>
- (case b of CIF b \<Rightarrow> True | VIF x \<Rightarrow> True | IF x y z \<Rightarrow> False))";
+ (case b of CIF b \<Rightarrow> True | VIF x \<Rightarrow> True | IF x y z \<Rightarrow> False))"
text{*\noindent
Now we prove @{term"normal(norm b)"}. Of course, this requires a lemma about
@@ -190,26 +184,22 @@
*}
(*<*)
-consts normif2 :: "ifex => ifex => ifex => ifex"
-primrec
-"normif2 (CIF b) t e = (if b then t else e)"
-"normif2 (VIF x) t e = IF (VIF x) t e"
+primrec normif2 :: "ifex => ifex => ifex => ifex" where
+"normif2 (CIF b) t e = (if b then t else e)" |
+"normif2 (VIF x) t e = IF (VIF x) t e" |
"normif2 (IF b t e) u f = normif2 b (normif2 t u f) (normif2 e u f)"
-consts norm2 :: "ifex => ifex"
-primrec
-"norm2 (CIF b) = CIF b"
-"norm2 (VIF x) = VIF x"
+primrec norm2 :: "ifex => ifex" where
+"norm2 (CIF b) = CIF b" |
+"norm2 (VIF x) = VIF x" |
"norm2 (IF b t e) = normif2 b (norm2 t) (norm2 e)"
-consts normal2 :: "ifex => bool"
-primrec
-"normal2(CIF b) = True"
-"normal2(VIF x) = True"
+primrec normal2 :: "ifex => bool" where
+"normal2(CIF b) = True" |
+"normal2(VIF x) = True" |
"normal2(IF b t e) = (normal2 t & normal2 e &
(case b of CIF b => False | VIF x => True | IF x y z => False))"
-
lemma [simp]:
"ALL t e. valif (normif2 b t e) env = valif (IF b t e) env"
apply(induct b)
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Thu May 29 22:45:33 2008 +0200
@@ -56,13 +56,11 @@
values:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ {\isachardoublequoteopen}value{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}boolex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
-\isanewline
-{\isachardoublequoteopen}value\ {\isacharparenleft}Const\ b{\isacharparenright}\ env\ {\isacharequal}\ b{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}value\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}value\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ value\ b\ env{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}value{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}boolex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}value\ {\isacharparenleft}Const\ b{\isacharparenright}\ env\ {\isacharequal}\ b{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}value\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}value\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ value\ b\ env{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
{\isachardoublequoteopen}value\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}value\ b\ env\ {\isasymand}\ value\ c\ env{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
@@ -81,12 +79,10 @@
The evaluation of If-expressions proceeds as for \isa{boolex}:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ valif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
-\isanewline
-{\isachardoublequoteopen}valif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ b{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}valif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequoteclose}\isanewline
+\ valif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}valif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ b{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}valif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequoteclose}\ {\isacharbar}\isanewline
{\isachardoublequoteopen}valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
@@ -97,13 +93,11 @@
translate from \isa{boolex} into \isa{ifex}:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ bool{\isadigit{2}}if\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}boolex\ {\isasymRightarrow}\ ifex{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
-\isanewline
-{\isachardoublequoteopen}bool{\isadigit{2}}if\ {\isacharparenleft}Const\ b{\isacharparenright}\ {\isacharequal}\ CIF\ b{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}bool{\isadigit{2}}if\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ {\isacharequal}\ VIF\ x{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}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}{\isachardoublequoteclose}\isanewline
+\ bool{\isadigit{2}}if\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}boolex\ {\isasymRightarrow}\ ifex{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}bool{\isadigit{2}}if\ {\isacharparenleft}Const\ b{\isacharparenright}\ {\isacharequal}\ CIF\ b{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}bool{\isadigit{2}}if\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ {\isacharequal}\ VIF\ x{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}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}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
{\isachardoublequoteopen}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}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
@@ -150,20 +144,16 @@
primitive recursive functions perform this task:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ normif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
-\isanewline
-{\isachardoublequoteopen}normif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}CIF\ b{\isacharparenright}\ t\ e{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}normif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}VIF\ x{\isacharparenright}\ t\ e{\isachardoublequoteclose}\isanewline
+\ normif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}normif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}CIF\ b{\isacharparenright}\ t\ e{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}normif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}VIF\ x{\isacharparenright}\ t\ e{\isachardoublequoteclose}\ {\isacharbar}\isanewline
{\isachardoublequoteopen}normif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ u\ f\ {\isacharequal}\ normif\ b\ {\isacharparenleft}normif\ t\ u\ f{\isacharparenright}\ {\isacharparenleft}normif\ e\ u\ f{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
-\isacommand{consts}\isamarkupfalse%
-\ norm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ ifex{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
-\isanewline
-{\isachardoublequoteopen}norm\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ {\isacharequal}\ CIF\ b{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}norm\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ {\isacharequal}\ VIF\ x{\isachardoublequoteclose}\isanewline
+\ norm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ ifex{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}norm\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ {\isacharequal}\ CIF\ b{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}norm\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ {\isacharequal}\ VIF\ x{\isachardoublequoteclose}\ {\isacharbar}\isanewline
{\isachardoublequoteopen}norm\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ normif\ b\ {\isacharparenleft}norm\ t{\isacharparenright}\ {\isacharparenleft}norm\ e{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
@@ -231,12 +221,10 @@
the above sense? We define a function that tests If-expressions for normality:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ normal\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
-\isanewline
-{\isachardoublequoteopen}normal{\isacharparenleft}CIF\ b{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}normal{\isacharparenleft}VIF\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}\isanewline
+\ normal\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}normal{\isacharparenleft}CIF\ b{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}normal{\isacharparenleft}VIF\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}\ {\isacharbar}\isanewline
{\isachardoublequoteopen}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}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
--- a/doc-src/TutorialI/Misc/Itrev.thy Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy Thu May 29 22:45:33 2008 +0200
@@ -45,10 +45,9 @@
gradually, using only~@{text"#"}:
*}
-consts itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list";
-primrec
-"itrev [] ys = ys"
-"itrev (x#xs) ys = itrev xs (x#ys)";
+primrec itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"itrev [] ys = ys" |
+"itrev (x#xs) ys = itrev xs (x#ys)"
text{*\noindent
The behaviour of \cdx{itrev} is simple: it reverses
--- a/doc-src/TutorialI/Misc/Plus.thy Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Misc/Plus.thy Thu May 29 22:45:33 2008 +0200
@@ -4,9 +4,8 @@
text{*\noindent Define the following addition function *}
-consts add :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-primrec
-"add m 0 = m"
+primrec add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+"add m 0 = m" |
"add m (Suc n) = add (Suc m) n"
text{*\noindent and prove*}
--- a/doc-src/TutorialI/Misc/Tree.thy Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Misc/Tree.thy Thu May 29 22:45:33 2008 +0200
@@ -8,9 +8,8 @@
datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*)
-consts mirror :: "'a tree \<Rightarrow> 'a tree";
-primrec
-"mirror Tip = Tip"
+primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
+"mirror Tip = Tip" |
"mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*)
text{*\noindent
@@ -23,9 +22,8 @@
apply(induct_tac t);
by(auto);
-consts flatten :: "'a tree => 'a list"
-primrec
-"flatten Tip = []"
+primrec flatten :: "'a tree => 'a list" where
+"flatten Tip = []" |
"flatten (Node l x r) = flatten l @ [x] @ flatten r";
(*>*)
--- a/doc-src/TutorialI/Misc/Tree2.thy Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Misc/Tree2.thy Thu May 29 22:45:33 2008 +0200
@@ -6,25 +6,21 @@
@{term"flatten"} from trees to lists. The straightforward version of
@{term"flatten"} is based on @{text"@"} and is thus, like @{term"rev"},
quadratic. A linear time version of @{term"flatten"} again reqires an extra
-argument, the accumulator: *}
-
-consts flatten2 :: "'a tree \<Rightarrow> 'a list \<Rightarrow> 'a list"
-(*<*)
-primrec
-"flatten2 Tip xs = xs"
+argument, the accumulator. Define *}
+(*<*)primrec(*>*)flatten2 :: "'a tree \<Rightarrow> 'a list \<Rightarrow> 'a list"(*<*)where
+"flatten2 Tip xs = xs" |
"flatten2 (Node l x r) xs = flatten2 l (x#(flatten2 r xs))"
(*>*)
-text{*\noindent Define @{term"flatten2"} and prove
-*}
+text{*\noindent and prove*}
(*<*)
-lemma [simp]: "!xs. flatten2 t xs = flatten t @ xs";
-apply(induct_tac t);
+lemma [simp]: "!xs. flatten2 t xs = flatten t @ xs"
+apply(induct_tac t)
by(auto);
(*>*)
-lemma "flatten2 t [] = flatten t";
+lemma "flatten2 t [] = flatten t"
(*<*)
-by(simp);
+by(simp)
end
(*>*)
--- a/doc-src/TutorialI/Misc/document/Itrev.tex Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Thu May 29 22:45:33 2008 +0200
@@ -71,11 +71,9 @@
gradually, using only~\isa{{\isacharhash}}:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ itrev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
-\isanewline
-{\isachardoublequoteopen}itrev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ ys\ {\isacharequal}\ ys{\isachardoublequoteclose}\isanewline
+\ itrev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}itrev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ ys\ {\isacharequal}\ ys{\isachardoublequoteclose}\ {\isacharbar}\isanewline
{\isachardoublequoteopen}itrev\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ ys\ {\isacharequal}\ itrev\ xs\ {\isacharparenleft}x{\isacharhash}ys{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
--- a/doc-src/TutorialI/Misc/document/Plus.tex Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Misc/document/Plus.tex Thu May 29 22:45:33 2008 +0200
@@ -19,11 +19,9 @@
\noindent Define the following addition function%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ add\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
-\isanewline
-{\isachardoublequoteopen}add\ m\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
+\ add\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}add\ m\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\ {\isacharbar}\isanewline
{\isachardoublequoteopen}add\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ add\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent and prove%
--- a/doc-src/TutorialI/Misc/document/Tree2.tex Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree2.tex Thu May 29 22:45:33 2008 +0200
@@ -20,13 +20,12 @@
\isa{flatten} from trees to lists. The straightforward version of
\isa{flatten} is based on \isa{{\isacharat}} and is thus, like \isa{rev},
quadratic. A linear time version of \isa{flatten} again reqires an extra
-argument, the accumulator:%
+argument, the accumulator. Define%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}%
+flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-\noindent Define \isa{flatten{\isadigit{2}}} and prove%
+\noindent and prove%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/TutorialI/Misc/document/natsum.tex Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Thu May 29 22:45:33 2008 +0200
@@ -24,11 +24,10 @@
primitive recursion, for example%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
-\ {\isachardoublequoteopen}sum\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ {\isachardoublequoteopen}sum\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharplus}\ sum\ n{\isachardoublequoteclose}%
+\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}sum\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}sum\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharplus}\ sum\ n{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
and induction, for example%
--- a/doc-src/TutorialI/Misc/document/types.tex Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Misc/document/types.tex Thu May 29 22:45:33 2008 +0200
@@ -23,49 +23,33 @@
Internally all synonyms are fully expanded. As a consequence Isabelle's
output never contains synonyms. Their main purpose is to improve the
readability of theories. Synonyms can be used just like any other
-type. Here, we declare two constants of type \isa{gate}:%
+type.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ nand\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
-\ \ \ \ \ \ \ xor\ \ {\isacharcolon}{\isacharcolon}\ gate%
+%
\isamarkupsubsection{Constant Definitions%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\label{sec:ConstDefinitions}\indexbold{definitions}%
-The constants \isa{nand} and \isa{xor} above are non-recursive and can
-be defined directly:%
+Nonrecursive definitions can be made with the \commdx{definition}
+command, for example \isa{nand} and \isa{xor} gates
+(based on type \isa{gate} above):%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{defs}\isamarkupfalse%
-\ nand{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}nand\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ xor{\isacharunderscore}def{\isacharcolon}\ \ {\isachardoublequoteopen}xor\ A\ B\ \ {\isasymequiv}\ A\ {\isasymand}\ {\isasymnot}B\ {\isasymor}\ {\isasymnot}A\ {\isasymand}\ B{\isachardoublequoteclose}%
+\isacommand{definition}\isamarkupfalse%
+\ nand\ {\isacharcolon}{\isacharcolon}\ gate\ \isakeyword{where}\ {\isachardoublequoteopen}nand\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ xor\ \ {\isacharcolon}{\isacharcolon}\ gate\ \isakeyword{where}\ {\isachardoublequoteopen}xor\ \ A\ B\ {\isasymequiv}\ A\ {\isasymand}\ {\isasymnot}B\ {\isasymor}\ {\isasymnot}A\ {\isasymand}\ B{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent%
-Here \commdx{defs} is a keyword and
-\isa{nand{\isacharunderscore}def} and \isa{xor{\isacharunderscore}def} are user-supplied names.
The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
that must be used in constant definitions.
Pattern-matching is not allowed: each definition must be of
the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
Section~\ref{sec:Simp-with-Defs} explains how definitions are used
-in proofs.
-
-A \commdx{constdefs} command combines the effects of \isacommand{consts} and
-\isacommand{defs}. For instance, we can introduce \isa{nand} and \isa{xor} by a
-single command:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{constdefs}\isamarkupfalse%
-\ nor\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
-\ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}nor\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \ \ xor{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
-\ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}xor{\isadigit{2}}\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymnot}A\ {\isasymor}\ {\isasymnot}B{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent
-The default name of each definition is $f$\isa{{\isacharunderscore}def}, where
+in proofs. The default name of each definition is $f$\isa{{\isacharunderscore}def}, where
$f$ is the name of the defined constant.%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/TutorialI/Misc/natsum.thy Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy Thu May 29 22:45:33 2008 +0200
@@ -7,9 +7,9 @@
primitive recursion, for example
*}
-consts sum :: "nat \<Rightarrow> nat"
-primrec "sum 0 = 0"
- "sum (Suc n) = Suc n + sum n"
+primrec sum :: "nat \<Rightarrow> nat" where
+"sum 0 = 0" |
+"sum (Suc n) = Suc n + sum n"
text{*\noindent
and induction, for example
--- a/doc-src/TutorialI/Misc/types.thy Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Misc/types.thy Thu May 29 22:45:33 2008 +0200
@@ -7,43 +7,26 @@
Internally all synonyms are fully expanded. As a consequence Isabelle's
output never contains synonyms. Their main purpose is to improve the
readability of theories. Synonyms can be used just like any other
-type. Here, we declare two constants of type \isa{gate}:
+type.
*}
-consts nand :: gate
- xor :: gate
-
subsection{*Constant Definitions*}
text{*\label{sec:ConstDefinitions}\indexbold{definitions}%
-The constants @{term"nand"} and @{term"xor"} above are non-recursive and can
-be defined directly:
+Nonrecursive definitions can be made with the \commdx{definition}
+command, for example @{text nand} and @{text xor} gates
+(based on type @{typ gate} above):
*}
-defs nand_def: "nand A B \<equiv> \<not>(A \<and> B)"
- xor_def: "xor A B \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B"
+definition nand :: gate where "nand A B \<equiv> \<not>(A \<and> B)"
+definition xor :: gate where "xor A B \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B"
text{*\noindent%
-Here \commdx{defs} is a keyword and
-@{thm[source]nand_def} and @{thm[source]xor_def} are user-supplied names.
The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
that must be used in constant definitions.
Pattern-matching is not allowed: each definition must be of
the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
Section~\ref{sec:Simp-with-Defs} explains how definitions are used
-in proofs.
-
-A \commdx{constdefs} command combines the effects of \isacommand{consts} and
-\isacommand{defs}. For instance, we can introduce @{term"nand"} and @{term"xor"} by a
-single command:
-*}
-
-constdefs nor :: gate
- "nor A B \<equiv> \<not>(A \<or> B)"
- xor2 :: gate
- "xor2 A B \<equiv> (A \<or> B) \<and> (\<not>A \<or> \<not>B)"
-
-text{*\noindent
-The default name of each definition is $f$@{text"_def"}, where
+in proofs. The default name of each definition is $f$@{text"_def"}, where
$f$ is the name of the defined constant.*}
(*<*)end(*>*)
--- a/doc-src/TutorialI/ToyList/ToyList.thy Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy Thu May 29 22:45:33 2008 +0200
@@ -38,38 +38,34 @@
Syntax annotations can be powerful, but they are difficult to master and
are never necessary. You
could drop them from theory @{text"ToyList"} and go back to the identifiers
- @{term[source]Nil} and @{term[source]Cons}.
- Novices should avoid using
+ @{term[source]Nil} and @{term[source]Cons}. Novices should avoid using
syntax annotations in their own theories.
\end{warn}
-Next, two functions @{text"app"} and \cdx{rev} are declared:
+Next, two functions @{text"app"} and \cdx{rev} are defined recursively,
+in this order, because Isabelle insists on definition before use:
*}
-consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65)
- rev :: "'a list \<Rightarrow> 'a list";
+primrec app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where
+"[] @ ys = ys" |
+"(x # xs) @ ys = x # (xs @ ys)"
+
+primrec rev :: "'a list \<Rightarrow> 'a list" where
+"rev [] = []" |
+"rev (x # xs) = (rev xs) @ (x # [])"
-text{*
-\noindent
-In contrast to many functional programming languages,
-Isabelle insists on explicit declarations of all functions
-(keyword \commdx{consts}). Apart from the declaration-before-use
-restriction, the order of items in a theory file is unconstrained. Function
-@{text"app"} is annotated with concrete syntax too. Instead of the
+text{*\noindent
+Each function definition is of the form
+\begin{center}
+\isacommand{primrec} \textit{name} @{text"::"} \textit{type} \textit{(optional syntax)} \isakeyword{where} \textit{equations}
+\end{center}
+The equations must be separated by @{text"|"}.
+%
+Function @{text"app"} is annotated with concrete syntax. Instead of the
prefix syntax @{text"app xs ys"} the infix
@{term"xs @ ys"}\index{$HOL2list@\isa{\at}|bold} becomes the preferred
-form. Both functions are defined recursively:
-*}
-
-primrec
-"[] @ ys = ys"
-"(x # xs) @ ys = x # (xs @ ys)";
+form.
-primrec
-"rev [] = []"
-"rev (x # xs) = (rev xs) @ (x # [])";
-
-text{*
-\noindent\index{*rev (constant)|(}\index{append function|(}
+\index{*rev (constant)|(}\index{append function|(}
The equations for @{text"app"} and @{term"rev"} hardly need comments:
@{text"app"} appends two lists and @{term"rev"} reverses a list. The
keyword \commdx{primrec} indicates that the recursion is
@@ -104,12 +100,8 @@
HOL-specific (terms and types) should be enclosed in
\texttt{"}\dots\texttt{"}.
To lessen this burden, quotation marks around a single identifier can be
-dropped, unless the identifier happens to be a keyword, as in
-*}
-
-consts "end" :: "'a list \<Rightarrow> 'a"
-
-text{*\noindent
+dropped, unless the identifier happens to be a keyword, for example
+\isa{"end"}.
When Isabelle prints a syntax error message, it refers to the HOL syntax as
the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
@@ -141,8 +133,6 @@
normal_form "rev (a # b # c # xs)"
text{*
-\noindent Chances are that the result will at first puzzle you.
-
\section{An Introductory Proof}
\label{sec:intro-proof}
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Thu May 29 22:45:33 2008 +0200
@@ -56,39 +56,36 @@
Syntax annotations can be powerful, but they are difficult to master and
are never necessary. You
could drop them from theory \isa{ToyList} and go back to the identifiers
- \isa{Nil} and \isa{Cons}.
- Novices should avoid using
+ \isa{Nil} and \isa{Cons}. Novices should avoid using
syntax annotations in their own theories.
\end{warn}
-Next, two functions \isa{app} and \cdx{rev} are declared:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ app\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequoteopen}{\isacharat}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}\isanewline
-\ \ \ \ \ \ \ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent
-In contrast to many functional programming languages,
-Isabelle insists on explicit declarations of all functions
-(keyword \commdx{consts}). Apart from the declaration-before-use
-restriction, the order of items in a theory file is unconstrained. Function
-\isa{app} is annotated with concrete syntax too. Instead of the
-prefix syntax \isa{app\ xs\ ys} the infix
-\isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\isa{\at}|bold} becomes the preferred
-form. Both functions are defined recursively:%
+Next, two functions \isa{app} and \cdx{rev} are defined recursively,
+in this order, because Isabelle insists on definition before use:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{primrec}\isamarkupfalse%
-\isanewline
-{\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ ys\ \ \ \ \ \ \ {\isacharequal}\ ys{\isachardoublequoteclose}\isanewline
+\ app\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequoteopen}{\isacharat}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ ys\ \ \ \ \ \ \ {\isacharequal}\ ys{\isachardoublequoteclose}\ {\isacharbar}\isanewline
{\isachardoublequoteopen}{\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharat}\ ys\ {\isacharequal}\ x\ {\isacharhash}\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{primrec}\isamarkupfalse%
-\isanewline
-{\isachardoublequoteopen}rev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}rev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
{\isachardoublequoteopen}rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ \ {\isacharequal}\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}x\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-\noindent\index{*rev (constant)|(}\index{append function|(}
+\noindent
+Each function definition is of the form
+\begin{center}
+\isacommand{primrec} \textit{name} \isa{{\isacharcolon}{\isacharcolon}} \textit{type} \textit{(optional syntax)} \isakeyword{where} \textit{equations}
+\end{center}
+The equations must be separated by \isa{{\isacharbar}}.
+%
+Function \isa{app} is annotated with concrete syntax. Instead of the
+prefix syntax \isa{app\ xs\ ys} the infix
+\isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\isa{\at}|bold} becomes the preferred
+form.
+
+\index{*rev (constant)|(}\index{append function|(}
The equations for \isa{app} and \isa{rev} hardly need comments:
\isa{app} appends two lists and \isa{rev} reverses a list. The
keyword \commdx{primrec} indicates that the recursion is
@@ -123,13 +120,8 @@
HOL-specific (terms and types) should be enclosed in
\texttt{"}\dots\texttt{"}.
To lessen this burden, quotation marks around a single identifier can be
-dropped, unless the identifier happens to be a keyword, as in%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ {\isachardoublequoteopen}end{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent
+dropped, unless the identifier happens to be a keyword, for example
+\isa{"end"}.
When Isabelle prints a syntax error message, it refers to the HOL syntax as
the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
@@ -164,8 +156,6 @@
\isacommand{normal{\isacharunderscore}form}\isamarkupfalse%
\ {\isachardoublequoteopen}rev\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ c\ {\isacharhash}\ xs{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-\noindent Chances are that the result will at first puzzle you.
-
\section{An Introductory Proof}
\label{sec:intro-proof}
--- a/doc-src/TutorialI/ToyList2/ToyList1 Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/ToyList2/ToyList1 Thu May 29 22:45:33 2008 +0200
@@ -5,13 +5,11 @@
datatype 'a list = Nil ("[]")
| Cons 'a "'a list" (infixr "#" 65)
-consts app :: "'a list => 'a list => 'a list" (infixr "@" 65)
- rev :: "'a list => 'a list"
-
-primrec
-"[] @ ys = ys"
+primrec app :: "'a list => 'a list => 'a list" (infixr "@" 65)
+where
+"[] @ ys = ys" |
"(x # xs) @ ys = x # (xs @ ys)"
-primrec
-"rev [] = []"
+primrec rev :: "'a list => 'a list" where
+"rev [] = []" |
"rev (x # xs) = (rev xs) @ (x # [])"
--- a/doc-src/TutorialI/Trie/Trie.thy Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Trie/Trie.thy Thu May 29 22:45:33 2008 +0200
@@ -19,20 +19,20 @@
We define two selector functions:
*};
-consts "value" :: "('a,'v)trie \<Rightarrow> 'v option"
- alist :: "('a,'v)trie \<Rightarrow> ('a * ('a,'v)trie)list";
-primrec "value(Trie ov al) = ov";
-primrec "alist(Trie ov al) = al";
+primrec "value" :: "('a,'v)trie \<Rightarrow> 'v option" where
+"value(Trie ov al) = ov"
+primrec alist :: "('a,'v)trie \<Rightarrow> ('a * ('a,'v)trie)list" where
+"alist(Trie ov al) = al"
text{*\noindent
Association lists come with a generic lookup function. Its result
involves type @{text option} because a lookup can fail:
*};
-consts assoc :: "('key * 'val)list \<Rightarrow> 'key \<Rightarrow> 'val option";
-primrec "assoc [] x = None"
- "assoc (p#ps) x =
- (let (a,b) = p in if a=x then Some b else assoc ps x)";
+primrec assoc :: "('key * 'val)list \<Rightarrow> 'key \<Rightarrow> 'val option" where
+"assoc [] x = None" |
+"assoc (p#ps) x =
+ (let (a,b) = p in if a=x then Some b else assoc ps x)"
text{*
Now we can define the lookup function for tries. It descends into the trie
@@ -41,11 +41,11 @@
recursion on the search string argument:
*};
-consts lookup :: "('a,'v)trie \<Rightarrow> 'a list \<Rightarrow> 'v option";
-primrec "lookup t [] = value t"
- "lookup t (a#as) = (case assoc (alist t) a of
- None \<Rightarrow> None
- | Some at \<Rightarrow> lookup at as)";
+primrec lookup :: "('a,'v)trie \<Rightarrow> 'a list \<Rightarrow> 'v option" where
+"lookup t [] = value t" |
+"lookup t (a#as) = (case assoc (alist t) a of
+ None \<Rightarrow> None
+ | Some at \<Rightarrow> lookup at as)"
text{*
As a first simple property we prove that looking up a string in the empty
@@ -63,13 +63,12 @@
associated with that string:
*};
-consts update :: "('a,'v)trie \<Rightarrow> 'a list \<Rightarrow> 'v \<Rightarrow> ('a,'v)trie";
-primrec
- "update t [] v = Trie (Some v) (alist t)"
- "update t (a#as) v =
- (let tt = (case assoc (alist t) a of
- None \<Rightarrow> Trie None [] | Some at \<Rightarrow> at)
- in Trie (value t) ((a,update tt as v) # alist t))";
+primrec update:: "('a,'v)trie \<Rightarrow> 'a list \<Rightarrow> 'v \<Rightarrow> ('a,'v)trie" where
+"update t [] v = Trie (Some v) (alist t)" |
+"update t (a#as) v =
+ (let tt = (case assoc (alist t) a of
+ None \<Rightarrow> Trie None [] | Some at \<Rightarrow> at)
+ in Trie (value t) ((a,update tt as v) # alist t))"
text{*\noindent
The base case is obvious. In the recursive case the subtrie
@@ -165,9 +164,9 @@
(* Exercise 1. Solution by Getrud Bauer *)
-consts update1 :: "('a, 'v) trie \<Rightarrow> 'a list \<Rightarrow> 'v option \<Rightarrow> ('a, 'v) trie"
-primrec
- "update1 t [] vo = Trie vo (alist t)"
+primrec update1 :: "('a, 'v) trie \<Rightarrow> 'a list \<Rightarrow> 'v option \<Rightarrow> ('a, 'v) trie"
+where
+ "update1 t [] vo = Trie vo (alist t)" |
"update1 t (a#as) vo =
(let tt = (case assoc (alist t) a of
None \<Rightarrow> Trie None []
@@ -183,19 +182,18 @@
(* Exercise 2. Solution by Getrud Bauer *)
-consts overwrite :: "'a \<Rightarrow> 'b \<Rightarrow> ('a * 'b) list \<Rightarrow> ('a * 'b) list"
-primrec
- "overwrite a v [] = [(a,v)]"
- "overwrite a v (p#ps) = (if a = fst p then (a,v)#ps else p # overwrite a v ps)"
+primrec overwrite :: "'a \<Rightarrow> 'b \<Rightarrow> ('a * 'b) list \<Rightarrow> ('a * 'b) list" where
+"overwrite a v [] = [(a,v)]" |
+"overwrite a v (p#ps) = (if a = fst p then (a,v)#ps else p # overwrite a v ps)"
lemma [simp]: "\<forall> a v b. assoc (overwrite a v ps) b = assoc ((a,v)#ps) b"
apply (induct_tac ps, auto)
apply (case_tac[!] a)
done
-consts update2 :: "('a, 'v) trie \<Rightarrow> 'a list \<Rightarrow> 'v option \<Rightarrow> ('a, 'v) trie";
-primrec
- "update2 t [] vo = Trie vo (alist t)"
+primrec update2 :: "('a, 'v) trie \<Rightarrow> 'a list \<Rightarrow> 'v option \<Rightarrow> ('a, 'v) trie"
+where
+ "update2 t [] vo = Trie vo (alist t)" |
"update2 t (a#as) vo =
(let tt = (case assoc (alist t) a of
None \<Rightarrow> Trie None []
@@ -212,15 +210,14 @@
(* Exercise 3. Solution by Getrud Bauer *)
datatype ('a,'v) triem = Triem "'v option" "'a \<Rightarrow> ('a,'v) triem option";
-consts valuem :: "('a, 'v) triem \<Rightarrow> 'v option"
-primrec "valuem (Triem ov m) = ov";
+primrec valuem :: "('a, 'v) triem \<Rightarrow> 'v option" where
+"valuem (Triem ov m) = ov"
-consts mapping :: "('a,'v) triem \<Rightarrow> 'a \<Rightarrow> ('a, 'v) triem option";
-primrec "mapping (Triem ov m) = m";
+primrec mapping :: "('a,'v) triem \<Rightarrow> 'a \<Rightarrow> ('a, 'v) triem option" where
+"mapping (Triem ov m) = m"
-consts lookupm :: "('a,'v) triem \<Rightarrow> 'a list \<Rightarrow> 'v option"
-primrec
- "lookupm t [] = valuem t"
+primrec lookupm :: "('a,'v) triem \<Rightarrow> 'a list \<Rightarrow> 'v option" where
+ "lookupm t [] = valuem t" |
"lookupm t (a#as) = (case mapping t a of
None \<Rightarrow> None
| Some at \<Rightarrow> lookupm at as)";
@@ -229,9 +226,8 @@
apply (case_tac as, simp_all);
done
-consts updatem :: "('a,'v)triem \<Rightarrow> 'a list \<Rightarrow> 'v \<Rightarrow> ('a,'v)triem"
-primrec
- "updatem t [] v = Triem (Some v) (mapping t)"
+primrec updatem :: "('a,'v)triem \<Rightarrow> 'a list \<Rightarrow> 'v \<Rightarrow> ('a,'v)triem" where
+ "updatem t [] v = Triem (Some v) (mapping t)" |
"updatem t (a#as) v =
(let tt = (case mapping t a of
None \<Rightarrow> Triem None (\<lambda>c. None)
--- a/doc-src/TutorialI/Trie/document/Trie.tex Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex Thu May 29 22:45:33 2008 +0200
@@ -34,25 +34,23 @@
We define two selector functions:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ {\isachardoublequoteopen}value{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie\ {\isasymRightarrow}\ {\isacharprime}v\ option{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ alist\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie{\isacharparenright}list{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
-\ {\isachardoublequoteopen}value{\isacharparenleft}Trie\ ov\ al{\isacharparenright}\ {\isacharequal}\ ov{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}value{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie\ {\isasymRightarrow}\ {\isacharprime}v\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}value{\isacharparenleft}Trie\ ov\ al{\isacharparenright}\ {\isacharequal}\ ov{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
-\ {\isachardoublequoteopen}alist{\isacharparenleft}Trie\ ov\ al{\isacharparenright}\ {\isacharequal}\ al{\isachardoublequoteclose}%
+\ alist\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie{\isacharparenright}list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}alist{\isacharparenleft}Trie\ ov\ al{\isacharparenright}\ {\isacharequal}\ al{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
Association lists come with a generic lookup function. Its result
involves type \isa{option} because a lookup can fail:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ \ \ assoc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}key\ {\isacharasterisk}\ {\isacharprime}val{\isacharparenright}list\ {\isasymRightarrow}\ {\isacharprime}key\ {\isasymRightarrow}\ {\isacharprime}val\ option{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
-\ {\isachardoublequoteopen}assoc\ {\isacharbrackleft}{\isacharbrackright}\ x\ {\isacharequal}\ None{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ {\isachardoublequoteopen}assoc\ {\isacharparenleft}p{\isacharhash}ps{\isacharparenright}\ x\ {\isacharequal}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}let\ {\isacharparenleft}a{\isacharcomma}b{\isacharparenright}\ {\isacharequal}\ p\ in\ if\ a{\isacharequal}x\ then\ Some\ b\ else\ assoc\ ps\ x{\isacharparenright}{\isachardoublequoteclose}%
+\ assoc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}key\ {\isacharasterisk}\ {\isacharprime}val{\isacharparenright}list\ {\isasymRightarrow}\ {\isacharprime}key\ {\isasymRightarrow}\ {\isacharprime}val\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}assoc\ {\isacharbrackleft}{\isacharbrackright}\ x\ {\isacharequal}\ None{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}assoc\ {\isacharparenleft}p{\isacharhash}ps{\isacharparenright}\ x\ {\isacharequal}\isanewline
+\ \ \ {\isacharparenleft}let\ {\isacharparenleft}a{\isacharcomma}b{\isacharparenright}\ {\isacharequal}\ p\ in\ if\ a{\isacharequal}x\ then\ Some\ b\ else\ assoc\ ps\ x{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
Now we can define the lookup function for tries. It descends into the trie
examining the letters of the search string one by one. As
@@ -60,13 +58,12 @@
recursion on the search string argument:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ \ \ lookup\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}v\ option{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
-\ {\isachardoublequoteopen}lookup\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ value\ t{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ {\isachardoublequoteopen}lookup\ t\ {\isacharparenleft}a{\isacharhash}as{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}case\ assoc\ {\isacharparenleft}alist\ t{\isacharparenright}\ a\ of\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ None\ {\isasymRightarrow}\ None\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Some\ at\ {\isasymRightarrow}\ lookup\ at\ as{\isacharparenright}{\isachardoublequoteclose}%
+\ lookup\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}v\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}lookup\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ value\ t{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}lookup\ t\ {\isacharparenleft}a{\isacharhash}as{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}case\ assoc\ {\isacharparenleft}alist\ t{\isacharparenright}\ a\ of\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ None\ {\isasymRightarrow}\ None\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Some\ at\ {\isasymRightarrow}\ lookup\ at\ as{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
As a first simple property we prove that looking up a string in the empty
trie \isa{Trie\ None\ {\isacharbrackleft}{\isacharbrackright}} always returns \isa{None}. The proof merely
@@ -98,15 +95,13 @@
associated with that string:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ update\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}v\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
-\isanewline
-\ \ {\isachardoublequoteopen}update\ t\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ v\ {\isacharequal}\ Trie\ {\isacharparenleft}Some\ v{\isacharparenright}\ {\isacharparenleft}alist\ t{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}update\ t\ {\isacharparenleft}a{\isacharhash}as{\isacharparenright}\ v\ {\isacharequal}\isanewline
-\ \ \ \ \ {\isacharparenleft}let\ tt\ {\isacharequal}\ {\isacharparenleft}case\ assoc\ {\isacharparenleft}alist\ t{\isacharparenright}\ a\ of\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ None\ {\isasymRightarrow}\ Trie\ None\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ Some\ at\ {\isasymRightarrow}\ at{\isacharparenright}\isanewline
-\ \ \ \ \ \ in\ Trie\ {\isacharparenleft}value\ t{\isacharparenright}\ {\isacharparenleft}{\isacharparenleft}a{\isacharcomma}update\ tt\ as\ v{\isacharparenright}\ {\isacharhash}\ alist\ t{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
+\ update{\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}v\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}update\ t\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ v\ {\isacharequal}\ Trie\ {\isacharparenleft}Some\ v{\isacharparenright}\ {\isacharparenleft}alist\ t{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}update\ t\ {\isacharparenleft}a{\isacharhash}as{\isacharparenright}\ v\ {\isacharequal}\isanewline
+\ \ \ {\isacharparenleft}let\ tt\ {\isacharequal}\ {\isacharparenleft}case\ assoc\ {\isacharparenleft}alist\ t{\isacharparenright}\ a\ of\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ None\ {\isasymRightarrow}\ Trie\ None\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ Some\ at\ {\isasymRightarrow}\ at{\isacharparenright}\isanewline
+\ \ \ \ in\ Trie\ {\isacharparenleft}value\ t{\isacharparenright}\ {\isacharparenleft}{\isacharparenleft}a{\isacharcomma}update\ tt\ as\ v{\isacharparenright}\ {\isacharhash}\ alist\ t{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
The base case is obvious. In the recursive case the subtrie
--- a/doc-src/TutorialI/Types/Records.thy Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Types/Records.thy Thu May 29 22:45:33 2008 +0200
@@ -44,26 +44,24 @@
Xcoord :: int
Ycoord :: int
-text {*
+text {*\noindent
Records of type @{typ point} have two fields named @{const Xcoord}
and @{const Ycoord}, both of type~@{typ int}. We now define a
constant of type @{typ point}:
*}
-constdefs
- pt1 :: point
- "pt1 \<equiv> (| Xcoord = 999, Ycoord = 23 |)"
+definition pt1 :: point where
+"pt1 \<equiv> (| Xcoord = 999, Ycoord = 23 |)"
-text {*
+text {*\noindent
We see above the ASCII notation for record brackets. You can also
use the symbolic brackets @{text \<lparr>} and @{text \<rparr>}. Record type
expressions can be also written directly with individual fields.
The type name above is merely an abbreviation.
*}
-constdefs
- pt2 :: "\<lparr>Xcoord :: int, Ycoord :: int\<rparr>"
- "pt2 \<equiv> \<lparr>Xcoord = -45, Ycoord = 97\<rparr>"
+definition pt2 :: "\<lparr>Xcoord :: int, Ycoord :: int\<rparr>" where
+"pt2 \<equiv> \<lparr>Xcoord = -45, Ycoord = 97\<rparr>"
text {*
For each field, there is a \emph{selector}\index{selector!record}
@@ -84,7 +82,7 @@
*}
lemma "\<lparr>Xcoord = a, Ycoord = b\<rparr>\<lparr>Xcoord := 0\<rparr> =
- \<lparr>Xcoord = 0, Ycoord = b\<rparr>"
+ \<lparr>Xcoord = 0, Ycoord = b\<rparr>"
by simp
text {*
@@ -110,17 +108,16 @@
record cpoint = point +
col :: colour
-text {*
+text {*\noindent
The fields of this new type are @{const Xcoord}, @{text Ycoord} and
@{text col}, in that order.
*}
-constdefs
- cpt1 :: cpoint
- "cpt1 \<equiv> \<lparr>Xcoord = 999, Ycoord = 23, col = Green\<rparr>"
+definition cpt1 :: cpoint where
+"cpt1 \<equiv> \<lparr>Xcoord = 999, Ycoord = 23, col = Green\<rparr>"
text {*
- \medskip We can define generic operations that work on arbitrary
+ We can define generic operations that work on arbitrary
instances of a record scheme, e.g.\ covering @{typ point}, @{typ
cpoint}, and any further extensions. Every record structure has an
implicit pseudo-field, \cdx{more}, that keeps the extension as an
@@ -150,7 +147,7 @@
lemma "point.more cpt1 = \<lparr>col = Green\<rparr>"
by (simp add: cpt1_def)
-text {*
+text {*\noindent
We see that the colour part attached to this @{typ point} is a
rudimentary record in its own right, namely @{text "\<lparr>col =
Green\<rparr>"}. In order to select or update @{text col}, this fragment
@@ -163,11 +160,12 @@
\medskip
\begin{tabular}{l}
- @{typ point}~@{text "="}~@{typ "\<lparr>Xcoord :: int, Ycoord :: int\<rparr>"} \\
- @{typ "'a point_scheme"}~@{text "="}~@{typ "\<lparr>Xcoord :: int, Ycoord :: int, \<dots> :: 'a\<rparr>"} \\
+ @{typ point}~@{text "="}~@{text "\<lparr>Xcoord :: int, Ycoord :: int\<rparr>"} \\
+ @{typ "'a point_scheme"}~@{text "="}~@{text "\<lparr>Xcoord :: int, Ycoord :: int, \<dots> :: 'a\<rparr>"} \\
\end{tabular}
\medskip
-
+
+\noindent
Type @{typ point} is for fixed records having exactly the two fields
@{const Xcoord} and~@{text Ycoord}, while the polymorphic type @{typ
"'a point_scheme"} comprises all possible extensions to those two
@@ -180,11 +178,10 @@
Xcoord} field.
*}
-constdefs
- getX :: "'a point_scheme \<Rightarrow> int"
- "getX r \<equiv> Xcoord r"
- setX :: "'a point_scheme \<Rightarrow> int \<Rightarrow> 'a point_scheme"
- "setX r a \<equiv> r\<lparr>Xcoord := a\<rparr>"
+definition getX :: "'a point_scheme \<Rightarrow> int" where
+"getX r \<equiv> Xcoord r"
+definition setX :: "'a point_scheme \<Rightarrow> int \<Rightarrow> 'a point_scheme" where
+"setX r a \<equiv> r\<lparr>Xcoord := a\<rparr>"
text {*
Here is a generic method that modifies a point, incrementing its
@@ -193,10 +190,9 @@
@{typ point} (including @{typ cpoint} etc.):
*}
-constdefs
- incX :: "'a point_scheme \<Rightarrow> 'a point_scheme"
- "incX r \<equiv>
- \<lparr>Xcoord = Xcoord r + 1, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
+definition incX :: "'a point_scheme \<Rightarrow> 'a point_scheme" where
+"incX r \<equiv>
+ \<lparr>Xcoord = Xcoord r + 1, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
text {*
Generic theorems can be proved about generic methods. This trivial
@@ -238,12 +234,12 @@
lemma "r\<lparr>Xcoord := a, Ycoord := b\<rparr> = r\<lparr>Ycoord := b, Xcoord := a\<rparr>"
by simp
-text {*
+text {*\noindent
We see above the syntax for iterated updates. We could equivalently
have written the left-hand side as @{text "r\<lparr>Xcoord := a\<rparr>\<lparr>Ycoord :=
b\<rparr>"}.
- \medskip Record equality is \emph{extensional}:
+ Record equality is \emph{extensional}:
\index{extensionality!for records} a record is determined entirely
by the values of its fields.
*}
@@ -251,7 +247,7 @@
lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r\<rparr>"
by simp
-text {*
+text {*\noindent
The generic version of this equality includes the pseudo-field
@{text more}:
*}
@@ -260,7 +256,7 @@
by simp
text {*
- \medskip The simplifier can prove many record equalities
+ The simplifier can prove many record equalities
automatically, but general equality reasoning can be tricky.
Consider proving this obvious fact:
*}
@@ -269,7 +265,7 @@
apply simp?
oops
-text {*
+text {*\noindent
Here the simplifier can do nothing, since general record equality is
not eliminated automatically. One way to proceed is by an explicit
forward step that applies the selector @{const Xcoord} to both sides
@@ -344,23 +340,19 @@
any additional fields.
\end{itemize}
-
These functions provide useful abbreviations for standard
record expressions involving constructors and selectors. The
definitions, which are \emph{not} unfolded by default, are made
available by the collective name of @{text defs} (@{text
point.defs}, @{text cpoint.defs}, etc.).
-
For example, here are the versions of those functions generated for
record @{typ point}. We omit @{text point.fields}, which happens to
be the same as @{text point.make}.
@{thm [display, indent = 0, margin = 65] point.make_def [no_vars]
point.extend_def [no_vars] point.truncate_def [no_vars]}
-
Contrast those with the corresponding functions for record @{typ
cpoint}. Observe @{text cpoint.fields} in particular.
-
@{thm [display, indent = 0, margin = 65] cpoint.make_def [no_vars]
cpoint.fields_def [no_vars] cpoint.extend_def [no_vars]
cpoint.truncate_def [no_vars]}
@@ -371,9 +363,8 @@
appropriate record fragment by @{text cpoint.fields}.
*}
-constdefs
- cpt2 :: cpoint
- "cpt2 \<equiv> point.extend pt1 (cpoint.fields Green)"
+definition cpt2 :: cpoint where
+"cpt2 \<equiv> point.extend pt1 (cpoint.fields Green)"
text {*
The coloured points @{const cpt1} and @{text cpt2} are equal. The
--- a/doc-src/TutorialI/Types/document/Records.tex Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Types/document/Records.tex Thu May 29 22:45:33 2008 +0200
@@ -61,26 +61,26 @@
\ \ Xcoord\ {\isacharcolon}{\isacharcolon}\ int\isanewline
\ \ Ycoord\ {\isacharcolon}{\isacharcolon}\ int%
\begin{isamarkuptext}%
-Records of type \isa{point} have two fields named \isa{Xcoord}
+\noindent
+ Records of type \isa{point} have two fields named \isa{Xcoord}
and \isa{Ycoord}, both of type~\isa{int}. We now define a
constant of type \isa{point}:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{constdefs}\isamarkupfalse%
-\isanewline
-\ \ pt{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ point\isanewline
-\ \ {\isachardoublequoteopen}pt{\isadigit{1}}\ {\isasymequiv}\ {\isacharparenleft}{\isacharbar}\ Xcoord\ {\isacharequal}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isadigit{2}}{\isadigit{3}}\ {\isacharbar}{\isacharparenright}{\isachardoublequoteclose}%
+\isacommand{definition}\isamarkupfalse%
+\ pt{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ point\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}pt{\isadigit{1}}\ {\isasymequiv}\ {\isacharparenleft}{\isacharbar}\ Xcoord\ {\isacharequal}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isadigit{2}}{\isadigit{3}}\ {\isacharbar}{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-We see above the ASCII notation for record brackets. You can also
+\noindent
+ We see above the ASCII notation for record brackets. You can also
use the symbolic brackets \isa{{\isasymlparr}} and \isa{{\isasymrparr}}. Record type
expressions can be also written directly with individual fields.
The type name above is merely an abbreviation.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{constdefs}\isamarkupfalse%
-\isanewline
-\ \ pt{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isasymrparr}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}pt{\isadigit{2}}\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isacharminus}{\isadigit{4}}{\isadigit{5}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isadigit{9}}{\isadigit{7}}{\isasymrparr}{\isachardoublequoteclose}%
+\isacommand{definition}\isamarkupfalse%
+\ pt{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isasymrparr}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}pt{\isadigit{2}}\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isacharminus}{\isadigit{4}}{\isadigit{5}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isadigit{9}}{\isadigit{7}}{\isasymrparr}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
For each field, there is a \emph{selector}\index{selector!record}
function of the same name. For example, if \isa{p} has type \isa{point} then \isa{Xcoord\ p} denotes the value of the \isa{Xcoord} field of~\isa{p}. Expressions involving field selection
@@ -112,7 +112,7 @@
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}\ {\isacharequal}\isanewline
-\ \ \ \ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isadigit{0}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \ \ \ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isadigit{0}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
@@ -155,16 +155,16 @@
\ cpoint\ {\isacharequal}\ point\ {\isacharplus}\isanewline
\ \ col\ {\isacharcolon}{\isacharcolon}\ colour%
\begin{isamarkuptext}%
-The fields of this new type are \isa{Xcoord}, \isa{Ycoord} and
+\noindent
+ The fields of this new type are \isa{Xcoord}, \isa{Ycoord} and
\isa{col}, in that order.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{constdefs}\isamarkupfalse%
-\isanewline
-\ \ cpt{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ cpoint\isanewline
-\ \ {\isachardoublequoteopen}cpt{\isadigit{1}}\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isadigit{2}}{\isadigit{3}}{\isacharcomma}\ col\ {\isacharequal}\ Green{\isasymrparr}{\isachardoublequoteclose}%
+\isacommand{definition}\isamarkupfalse%
+\ cpt{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ cpoint\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}cpt{\isadigit{1}}\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isadigit{2}}{\isadigit{3}}{\isacharcomma}\ col\ {\isacharequal}\ Green{\isasymrparr}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-\medskip We can define generic operations that work on arbitrary
+We can define generic operations that work on arbitrary
instances of a record scheme, e.g.\ covering \isa{point}, \isa{cpoint}, and any further extensions. Every record structure has an
implicit pseudo-field, \cdx{more}, that keeps the extension as an
explicit value. Its type is declared as completely
@@ -219,7 +219,8 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-We see that the colour part attached to this \isa{point} is a
+\noindent
+ We see that the colour part attached to this \isa{point} is a
rudimentary record in its own right, namely \isa{{\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}}. In order to select or update \isa{col}, this fragment
needs to be put back into the context of the parent type scheme, say
as \isa{more} part of another \isa{point}.
@@ -230,11 +231,12 @@
\medskip
\begin{tabular}{l}
- \isa{point}~\isa{{\isacharequal}}~\isa{point} \\
- \isa{{\isacharprime}a\ point{\isacharunderscore}scheme}~\isa{{\isacharequal}}~\isa{{\isacharprime}a\ point{\isacharunderscore}scheme} \\
+ \isa{point}~\isa{{\isacharequal}}~\isa{{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isasymrparr}} \\
+ \isa{{\isacharprime}a\ point{\isacharunderscore}scheme}~\isa{{\isacharequal}}~\isa{{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a{\isasymrparr}} \\
\end{tabular}
\medskip
-
+
+\noindent
Type \isa{point} is for fixed records having exactly the two fields
\isa{Xcoord} and~\isa{Ycoord}, while the polymorphic type \isa{{\isacharprime}a\ point{\isacharunderscore}scheme} comprises all possible extensions to those two
fields. Note that \isa{unit\ point{\isacharunderscore}scheme} coincides with \isa{point}, and \isa{{\isasymlparr}col\ {\isacharcolon}{\isacharcolon}\ colour{\isasymrparr}\ point{\isacharunderscore}scheme} with \isa{cpoint}.
@@ -243,12 +245,12 @@
regard records as objects --- to get and set any point's \isa{Xcoord} field.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{constdefs}\isamarkupfalse%
-\isanewline
-\ \ getX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}getX\ r\ {\isasymequiv}\ Xcoord\ r{\isachardoublequoteclose}\isanewline
-\ \ setX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ {\isacharprime}a\ point{\isacharunderscore}scheme{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}setX\ r\ a\ {\isasymequiv}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isachardoublequoteclose}%
+\isacommand{definition}\isamarkupfalse%
+\ getX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}getX\ r\ {\isasymequiv}\ Xcoord\ r{\isachardoublequoteclose}\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ setX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ {\isacharprime}a\ point{\isacharunderscore}scheme{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}setX\ r\ a\ {\isasymequiv}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
Here is a generic method that modifies a point, incrementing its
\isa{Xcoord} field. The \isa{Ycoord} and \isa{more} fields
@@ -256,11 +258,10 @@
\isa{point} (including \isa{cpoint} etc.):%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{constdefs}\isamarkupfalse%
-\isanewline
-\ \ incX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ {\isacharprime}a\ point{\isacharunderscore}scheme{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}incX\ r\ {\isasymequiv}\isanewline
-\ \ \ \ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r\ {\isacharplus}\ {\isadigit{1}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ point{\isachardot}more\ r{\isasymrparr}{\isachardoublequoteclose}%
+\isacommand{definition}\isamarkupfalse%
+\ incX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ {\isacharprime}a\ point{\isacharunderscore}scheme{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}incX\ r\ {\isasymequiv}\isanewline
+\ \ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r\ {\isacharplus}\ {\isadigit{1}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ point{\isachardot}more\ r{\isasymrparr}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
Generic theorems can be proved about generic methods. This trivial
lemma relates \isa{incX} to \isa{getX} and \isa{setX}:%
@@ -346,10 +347,11 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-We see above the syntax for iterated updates. We could equivalently
+\noindent
+ We see above the syntax for iterated updates. We could equivalently
have written the left-hand side as \isa{r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isasymlparr}Ycoord\ {\isacharcolon}{\isacharequal}\ b{\isasymrparr}}.
- \medskip Record equality is \emph{extensional}:
+ Record equality is \emph{extensional}:
\index{extensionality!for records} a record is determined entirely
by the values of its fields.%
\end{isamarkuptext}%
@@ -372,7 +374,8 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-The generic version of this equality includes the pseudo-field
+\noindent
+ The generic version of this equality includes the pseudo-field
\isa{more}:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -394,7 +397,7 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-\medskip The simplifier can prove many record equalities
+The simplifier can prove many record equalities
automatically, but general equality reasoning can be tricky.
Consider proving this obvious fact:%
\end{isamarkuptext}%
@@ -419,7 +422,8 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-Here the simplifier can do nothing, since general record equality is
+\noindent
+ Here the simplifier can do nothing, since general record equality is
not eliminated automatically. One way to proceed is by an explicit
forward step that applies the selector \isa{Xcoord} to both sides
of the assumed record equality:%
@@ -536,12 +540,10 @@
any additional fields.
\end{itemize}
-
These functions provide useful abbreviations for standard
record expressions involving constructors and selectors. The
definitions, which are \emph{not} unfolded by default, are made
available by the collective name of \isa{defs} (\isa{point{\isachardot}defs}, \isa{cpoint{\isachardot}defs}, etc.).
-
For example, here are the versions of those functions generated for
record \isa{point}. We omit \isa{point{\isachardot}fields}, which happens to
be the same as \isa{point{\isachardot}make}.
@@ -552,9 +554,7 @@
{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isasep\isanewline%
point{\isachardot}truncate\ r\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isasymrparr}%
\end{isabelle}
-
Contrast those with the corresponding functions for record \isa{cpoint}. Observe \isa{cpoint{\isachardot}fields} in particular.
-
\begin{isabelle}%
cpoint{\isachardot}make\ Xcoord\ Ycoord\ col\ {\isasymequiv}\isanewline
{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ col\ {\isacharequal}\ col{\isasymrparr}\isasep\isanewline%
@@ -571,10 +571,9 @@
appropriate record fragment by \isa{cpoint{\isachardot}fields}.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{constdefs}\isamarkupfalse%
-\isanewline
-\ \ cpt{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ cpoint\isanewline
-\ \ {\isachardoublequoteopen}cpt{\isadigit{2}}\ {\isasymequiv}\ point{\isachardot}extend\ pt{\isadigit{1}}\ {\isacharparenleft}cpoint{\isachardot}fields\ Green{\isacharparenright}{\isachardoublequoteclose}%
+\isacommand{definition}\isamarkupfalse%
+\ cpt{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ cpoint\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}cpt{\isadigit{2}}\ {\isasymequiv}\ point{\isachardot}extend\ pt{\isadigit{1}}\ {\isacharparenleft}cpoint{\isachardot}fields\ Green{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
The coloured points \isa{cpt{\isadigit{1}}} and \isa{cpt{\isadigit{2}}} are equal. The
proof is trivial, by unfolding all the definitions. We deliberately
--- a/doc-src/TutorialI/fp.tex Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/fp.tex Thu May 29 22:45:33 2008 +0200
@@ -169,10 +169,9 @@
\isa{size [] = 0} and \isa{size(x \# xs) = size xs + 1}. In general,
\cdx{size} returns
\begin{itemize}
-\item zero for all constructors
-that do not have an argument of type $t$\\
+\item zero for all constructors that do not have an argument of type $t$,
\item one plus the sum of the sizes of all arguments of type~$t$,
-for all other constructors
+for all other constructors.
\end{itemize}
Note that because
\isa{size} is defined on every datatype, it is overloaded; on lists
@@ -184,11 +183,10 @@
\index{recursion!primitive}%
Functions on datatypes are usually defined by recursion. In fact, most of the
-time they are defined by what is called \textbf{primitive recursion}.
-The keyword \commdx{primrec} is followed by a list of
-equations
+time they are defined by what is called \textbf{primitive recursion} over some
+datatype $t$. This means that the recursion equations must be of the form
\[ f \, x@1 \, \dots \, (C \, y@1 \, \dots \, y@k)\, \dots \, x@n = r \]
-such that $C$ is a constructor of the datatype $t$ and all recursive calls of
+such that $C$ is a constructor of $t$ and all recursive calls of
$f$ in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. Thus
Isabelle immediately sees that $f$ terminates because one (fixed!) argument
becomes smaller with every recursive call. There must be at most one equation