--- a/doc-src/TutorialI/Inductive/AB.thy Wed Nov 07 16:43:01 2007 +0100
+++ b/doc-src/TutorialI/Inductive/AB.thy Wed Nov 07 18:19:04 2007 +0100
@@ -41,9 +41,9 @@
*}
inductive_set
- S :: "alfa list set"
- and A :: "alfa list set"
- and B :: "alfa list set"
+ S :: "alfa list set" and
+ A :: "alfa list set" and
+ B :: "alfa list set"
where
"[] \<in> S"
| "w \<in> A \<Longrightarrow> b#w \<in> S"
--- a/doc-src/TutorialI/Inductive/Even.thy Wed Nov 07 16:43:01 2007 +0100
+++ b/doc-src/TutorialI/Inductive/Even.thy Wed Nov 07 18:19:04 2007 +0100
@@ -20,10 +20,9 @@
a set of natural numbers with the desired properties.
*}
-inductive_set even :: "nat set"
-where
- zero[intro!]: "0 \<in> even"
-| step[intro!]: "n \<in> even \<Longrightarrow> (Suc (Suc n)) \<in> even"
+inductive_set even :: "nat set" where
+zero[intro!]: "0 \<in> even" |
+step[intro!]: "n \<in> even \<Longrightarrow> (Suc (Suc n)) \<in> even"
text {*
An inductive definition consists of introduction rules. The first one
--- a/doc-src/TutorialI/Inductive/Mutual.thy Wed Nov 07 16:43:01 2007 +0100
+++ b/doc-src/TutorialI/Inductive/Mutual.thy Wed Nov 07 18:19:04 2007 +0100
@@ -9,8 +9,8 @@
*}
inductive_set
- Even :: "nat set"
- and Odd :: "nat set"
+ Even :: "nat set" and
+ Odd :: "nat set"
where
zero: "0 \<in> Even"
| EvenI: "n \<in> Odd \<Longrightarrow> Suc n \<in> Even"
@@ -54,7 +54,27 @@
apply simp
done
(*>*)
-(*
-Exercise: 1 : odd
-*)
+
+subsection{*Inductively Defined Predicates\label{sec:ind-predicates}*}
+
+text{*\index{inductive predicates|(}
+Instead of a set of even numbers one can also define a predicate on @{typ nat}:
+*}
+
+inductive evn :: "nat \<Rightarrow> bool" where
+zero: "evn 0" |
+step: "evn n \<Longrightarrow> evn(Suc(Suc n))"
+
+text{*\noindent Everything works as before, except that
+you write \commdx{inductive} instead of \isacommand{inductive\_set} and
+@{prop"evn n"} instead of @{prop"n : even"}. The notation is more
+lightweight but the usual set-theoretic operations, e.g. @{term"Even \<union> Odd"},
+are not directly available on predicates.
+
+When defining an n-ary relation as a predicate it is recommended to curry
+the predicate: its type should be @{text"\<tau>\<^isub>1 \<Rightarrow> \<dots> \<Rightarrow> \<tau>\<^isub>n \<Rightarrow> bool"} rather than
+@{text"\<tau>\<^isub>1 \<times> \<dots> \<times> \<tau>\<^isub>n \<Rightarrow> bool"}. The curried version facilitates inductions.
+\index{inductive predicates|)}
+*}
+
(*<*)end(*>*)
--- a/doc-src/TutorialI/Inductive/document/AB.tex Wed Nov 07 16:43:01 2007 +0100
+++ b/doc-src/TutorialI/Inductive/document/AB.tex Wed Nov 07 18:19:04 2007 +0100
@@ -76,9 +76,9 @@
\isamarkuptrue%
\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse%
\isanewline
-\ \ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{and}\ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{and}\ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\isanewline
+\ \ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
+\ \ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
+\ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\isanewline
\isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isasymin}\ S{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}w\ {\isasymin}\ A\ {\isasymLongrightarrow}\ b{\isacharhash}w\ {\isasymin}\ S{\isachardoublequoteclose}\isanewline
--- a/doc-src/TutorialI/Inductive/document/Even.tex Wed Nov 07 16:43:01 2007 +0100
+++ b/doc-src/TutorialI/Inductive/document/Even.tex Wed Nov 07 18:19:04 2007 +0100
@@ -40,10 +40,9 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse%
-\ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
-\isakeyword{where}\isanewline
-\ \ zero{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymin}\ even{\isachardoublequoteclose}\isanewline
-{\isacharbar}\ step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isasymin}\ even{\isachardoublequoteclose}%
+\ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+zero{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymin}\ even{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isasymin}\ even{\isachardoublequoteclose}%
\begin{isamarkuptext}%
An inductive definition consists of introduction rules. The first one
above states that 0 is even; the second states that if $n$ is even, then so
--- a/doc-src/TutorialI/Inductive/document/Mutual.tex Wed Nov 07 16:43:01 2007 +0100
+++ b/doc-src/TutorialI/Inductive/document/Mutual.tex Wed Nov 07 18:19:04 2007 +0100
@@ -27,8 +27,8 @@
\isamarkuptrue%
\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse%
\isanewline
-\ \ Even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{and}\ Odd\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
+\ \ Even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
+\ \ Odd\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
\isakeyword{where}\isanewline
\ \ zero{\isacharcolon}\ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymin}\ Even{\isachardoublequoteclose}\isanewline
{\isacharbar}\ EvenI{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ Odd\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ Even{\isachardoublequoteclose}\isanewline
@@ -85,6 +85,33 @@
%
\endisadelimproof
%
+\isamarkupsubsection{Inductively Defined Predicates\label{sec:ind-predicates}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\index{inductive predicates|(}
+Instead of a set of even numbers one can also define a predicate on \isa{nat}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{inductive}\isamarkupfalse%
+\ evn\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+zero{\isacharcolon}\ {\isachardoublequoteopen}evn\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+step{\isacharcolon}\ {\isachardoublequoteopen}evn\ n\ {\isasymLongrightarrow}\ evn{\isacharparenleft}Suc{\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent Everything works as before, except that
+you write \commdx{inductive} instead of \isacommand{inductive\_set} and
+\isa{evn\ n} instead of \isa{n\ {\isasymin}\ even}. The notation is more
+lightweight but the usual set-theoretic operations, e.g. \isa{Even\ {\isasymunion}\ Odd},
+are not directly available on predicates.
+
+When defining an n-ary relation as a predicate it is recommended to curry
+the predicate: its type should be \isa{{\isasymtau}\isactrlisub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymtau}\isactrlisub n\ {\isasymRightarrow}\ bool} rather than
+\isa{{\isasymtau}\isactrlisub {\isadigit{1}}\ {\isasymtimes}\ {\isasymdots}\ {\isasymtimes}\ {\isasymtau}\isactrlisub n\ {\isasymRightarrow}\ bool}. The curried version facilitates inductions.
+\index{inductive predicates|)}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isadelimtheory
%
\endisadelimtheory
--- a/doc-src/TutorialI/Inductive/inductive.tex Wed Nov 07 16:43:01 2007 +0100
+++ b/doc-src/TutorialI/Inductive/inductive.tex Wed Nov 07 18:19:04 2007 +0100
@@ -13,6 +13,11 @@
context-free grammars. The first two sections are required reading for anybody
interested in mathematical modelling.
+\begin{warn}
+Predicates can also be defined inductively.
+See {\S}\ref{sec:ind-predicates}.
+\end{warn}
+
\input{Inductive/document/Even}
\input{Inductive/document/Mutual}
\input{Inductive/document/Star}