# HG changeset patch
# User nipkow
# Date 1194455944 -3600
# Node ID 15bf0f47a87d8fc2115707b004fff6ae484fa839
# Parent  63e8de11c8e9d3c57b804c5c22a82be3e8ee4a9e
added inductive

diff -r 63e8de11c8e9 -r 15bf0f47a87d doc-src/TutorialI/Inductive/AB.thy
--- 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"
diff -r 63e8de11c8e9 -r 15bf0f47a87d doc-src/TutorialI/Inductive/Even.thy
--- 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
diff -r 63e8de11c8e9 -r 15bf0f47a87d doc-src/TutorialI/Inductive/Mutual.thy
--- 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(*>*)
diff -r 63e8de11c8e9 -r 15bf0f47a87d doc-src/TutorialI/Inductive/document/AB.tex
--- 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
diff -r 63e8de11c8e9 -r 15bf0f47a87d doc-src/TutorialI/Inductive/document/Even.tex
--- 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
diff -r 63e8de11c8e9 -r 15bf0f47a87d doc-src/TutorialI/Inductive/document/Mutual.tex
--- 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
diff -r 63e8de11c8e9 -r 15bf0f47a87d doc-src/TutorialI/Inductive/inductive.tex
--- 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}