1.1 --- a/doc-src/TutorialI/Inductive/AB.thy Wed Nov 07 16:43:01 2007 +0100
1.2 +++ b/doc-src/TutorialI/Inductive/AB.thy Wed Nov 07 18:19:04 2007 +0100
1.3 @@ -41,9 +41,9 @@
1.4 *}
1.5
1.6 inductive_set
1.7 - S :: "alfa list set"
1.8 - and A :: "alfa list set"
1.9 - and B :: "alfa list set"
1.10 + S :: "alfa list set" and
1.11 + A :: "alfa list set" and
1.12 + B :: "alfa list set"
1.13 where
1.14 "[] \<in> S"
1.15 | "w \<in> A \<Longrightarrow> b#w \<in> S"
2.1 --- a/doc-src/TutorialI/Inductive/Even.thy Wed Nov 07 16:43:01 2007 +0100
2.2 +++ b/doc-src/TutorialI/Inductive/Even.thy Wed Nov 07 18:19:04 2007 +0100
2.3 @@ -20,10 +20,9 @@
2.4 a set of natural numbers with the desired properties.
2.5 *}
2.6
2.7 -inductive_set even :: "nat set"
2.8 -where
2.9 - zero[intro!]: "0 \<in> even"
2.10 -| step[intro!]: "n \<in> even \<Longrightarrow> (Suc (Suc n)) \<in> even"
2.11 +inductive_set even :: "nat set" where
2.12 +zero[intro!]: "0 \<in> even" |
2.13 +step[intro!]: "n \<in> even \<Longrightarrow> (Suc (Suc n)) \<in> even"
2.14
2.15 text {*
2.16 An inductive definition consists of introduction rules. The first one
3.1 --- a/doc-src/TutorialI/Inductive/Mutual.thy Wed Nov 07 16:43:01 2007 +0100
3.2 +++ b/doc-src/TutorialI/Inductive/Mutual.thy Wed Nov 07 18:19:04 2007 +0100
3.3 @@ -9,8 +9,8 @@
3.4 *}
3.5
3.6 inductive_set
3.7 - Even :: "nat set"
3.8 - and Odd :: "nat set"
3.9 + Even :: "nat set" and
3.10 + Odd :: "nat set"
3.11 where
3.12 zero: "0 \<in> Even"
3.13 | EvenI: "n \<in> Odd \<Longrightarrow> Suc n \<in> Even"
3.14 @@ -54,7 +54,27 @@
3.15 apply simp
3.16 done
3.17 (*>*)
3.18 -(*
3.19 -Exercise: 1 : odd
3.20 -*)
3.21 +
3.22 +subsection{*Inductively Defined Predicates\label{sec:ind-predicates}*}
3.23 +
3.24 +text{*\index{inductive predicates|(}
3.25 +Instead of a set of even numbers one can also define a predicate on @{typ nat}:
3.26 +*}
3.27 +
3.28 +inductive evn :: "nat \<Rightarrow> bool" where
3.29 +zero: "evn 0" |
3.30 +step: "evn n \<Longrightarrow> evn(Suc(Suc n))"
3.31 +
3.32 +text{*\noindent Everything works as before, except that
3.33 +you write \commdx{inductive} instead of \isacommand{inductive\_set} and
3.34 +@{prop"evn n"} instead of @{prop"n : even"}. The notation is more
3.35 +lightweight but the usual set-theoretic operations, e.g. @{term"Even \<union> Odd"},
3.36 +are not directly available on predicates.
3.37 +
3.38 +When defining an n-ary relation as a predicate it is recommended to curry
3.39 +the predicate: its type should be @{text"\<tau>\<^isub>1 \<Rightarrow> \<dots> \<Rightarrow> \<tau>\<^isub>n \<Rightarrow> bool"} rather than
3.40 +@{text"\<tau>\<^isub>1 \<times> \<dots> \<times> \<tau>\<^isub>n \<Rightarrow> bool"}. The curried version facilitates inductions.
3.41 +\index{inductive predicates|)}
3.42 +*}
3.43 +
3.44 (*<*)end(*>*)
4.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex Wed Nov 07 16:43:01 2007 +0100
4.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex Wed Nov 07 18:19:04 2007 +0100
4.3 @@ -76,9 +76,9 @@
4.4 \isamarkuptrue%
4.5 \isacommand{inductive{\isacharunderscore}set}\isamarkupfalse%
4.6 \isanewline
4.7 -\ \ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\isanewline
4.8 -\ \ \isakeyword{and}\ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\isanewline
4.9 -\ \ \isakeyword{and}\ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\isanewline
4.10 +\ \ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
4.11 +\ \ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
4.12 +\ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\isanewline
4.13 \isakeyword{where}\isanewline
4.14 \ \ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isasymin}\ S{\isachardoublequoteclose}\isanewline
4.15 {\isacharbar}\ {\isachardoublequoteopen}w\ {\isasymin}\ A\ {\isasymLongrightarrow}\ b{\isacharhash}w\ {\isasymin}\ S{\isachardoublequoteclose}\isanewline
5.1 --- a/doc-src/TutorialI/Inductive/document/Even.tex Wed Nov 07 16:43:01 2007 +0100
5.2 +++ b/doc-src/TutorialI/Inductive/document/Even.tex Wed Nov 07 18:19:04 2007 +0100
5.3 @@ -40,10 +40,9 @@
5.4 \end{isamarkuptext}%
5.5 \isamarkuptrue%
5.6 \isacommand{inductive{\isacharunderscore}set}\isamarkupfalse%
5.7 -\ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
5.8 -\isakeyword{where}\isanewline
5.9 -\ \ zero{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymin}\ even{\isachardoublequoteclose}\isanewline
5.10 -{\isacharbar}\ step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isasymin}\ even{\isachardoublequoteclose}%
5.11 +\ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
5.12 +zero{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymin}\ even{\isachardoublequoteclose}\ {\isacharbar}\isanewline
5.13 +step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isasymin}\ even{\isachardoublequoteclose}%
5.14 \begin{isamarkuptext}%
5.15 An inductive definition consists of introduction rules. The first one
5.16 above states that 0 is even; the second states that if $n$ is even, then so
6.1 --- a/doc-src/TutorialI/Inductive/document/Mutual.tex Wed Nov 07 16:43:01 2007 +0100
6.2 +++ b/doc-src/TutorialI/Inductive/document/Mutual.tex Wed Nov 07 18:19:04 2007 +0100
6.3 @@ -27,8 +27,8 @@
6.4 \isamarkuptrue%
6.5 \isacommand{inductive{\isacharunderscore}set}\isamarkupfalse%
6.6 \isanewline
6.7 -\ \ Even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
6.8 -\ \ \isakeyword{and}\ Odd\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
6.9 +\ \ Even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
6.10 +\ \ Odd\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
6.11 \isakeyword{where}\isanewline
6.12 \ \ zero{\isacharcolon}\ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymin}\ Even{\isachardoublequoteclose}\isanewline
6.13 {\isacharbar}\ EvenI{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ Odd\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ Even{\isachardoublequoteclose}\isanewline
6.14 @@ -85,6 +85,33 @@
6.15 %
6.16 \endisadelimproof
6.17 %
6.18 +\isamarkupsubsection{Inductively Defined Predicates\label{sec:ind-predicates}%
6.19 +}
6.20 +\isamarkuptrue%
6.21 +%
6.22 +\begin{isamarkuptext}%
6.23 +\index{inductive predicates|(}
6.24 +Instead of a set of even numbers one can also define a predicate on \isa{nat}:%
6.25 +\end{isamarkuptext}%
6.26 +\isamarkuptrue%
6.27 +\isacommand{inductive}\isamarkupfalse%
6.28 +\ evn\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
6.29 +zero{\isacharcolon}\ {\isachardoublequoteopen}evn\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
6.30 +step{\isacharcolon}\ {\isachardoublequoteopen}evn\ n\ {\isasymLongrightarrow}\ evn{\isacharparenleft}Suc{\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
6.31 +\begin{isamarkuptext}%
6.32 +\noindent Everything works as before, except that
6.33 +you write \commdx{inductive} instead of \isacommand{inductive\_set} and
6.34 +\isa{evn\ n} instead of \isa{n\ {\isasymin}\ even}. The notation is more
6.35 +lightweight but the usual set-theoretic operations, e.g. \isa{Even\ {\isasymunion}\ Odd},
6.36 +are not directly available on predicates.
6.37 +
6.38 +When defining an n-ary relation as a predicate it is recommended to curry
6.39 +the predicate: its type should be \isa{{\isasymtau}\isactrlisub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymtau}\isactrlisub n\ {\isasymRightarrow}\ bool} rather than
6.40 +\isa{{\isasymtau}\isactrlisub {\isadigit{1}}\ {\isasymtimes}\ {\isasymdots}\ {\isasymtimes}\ {\isasymtau}\isactrlisub n\ {\isasymRightarrow}\ bool}. The curried version facilitates inductions.
6.41 +\index{inductive predicates|)}%
6.42 +\end{isamarkuptext}%
6.43 +\isamarkuptrue%
6.44 +%
6.45 \isadelimtheory
6.46 %
6.47 \endisadelimtheory
7.1 --- a/doc-src/TutorialI/Inductive/inductive.tex Wed Nov 07 16:43:01 2007 +0100
7.2 +++ b/doc-src/TutorialI/Inductive/inductive.tex Wed Nov 07 18:19:04 2007 +0100
7.3 @@ -13,6 +13,11 @@
7.4 context-free grammars. The first two sections are required reading for anybody
7.5 interested in mathematical modelling.
7.6
7.7 +\begin{warn}
7.8 +Predicates can also be defined inductively.
7.9 +See {\S}\ref{sec:ind-predicates}.
7.10 +\end{warn}
7.11 +
7.12 \input{Inductive/document/Even}
7.13 \input{Inductive/document/Mutual}
7.14 \input{Inductive/document/Star}