# HG changeset patch
# User nipkow
# Date 1265874259 -3600
# Node ID d74fe18f01e97c24c38b713303a681efd96048b3
# Parent  53754ec7360b7b70dc7c81a46809d026f7b1c783
inductive vs inductive_set explanation

diff -r 53754ec7360b -r d74fe18f01e9 doc-src/TutorialI/Inductive/Mutual.thy
--- a/doc-src/TutorialI/Inductive/Mutual.thy	Wed Feb 10 19:37:34 2010 +0100
+++ b/doc-src/TutorialI/Inductive/Mutual.thy	Thu Feb 11 08:44:19 2010 +0100
@@ -67,13 +67,13 @@
 
 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.
+@{prop"evn n"} instead of @{prop"n : even"}.
+When defining an n-ary relation as a predicate, it is recommended to curry
+the predicate: its type should be \mbox{@{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.
 
-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.
+When should you choose sets and when predicates? If you intend to combine your notion with set theoretic notation, define it as an inductive set. If not, define it as an inductive predicate, thus avoiding the @{text"\<in>"} notation. But note that predicates of more than one argument cannot be combined with the usual set theoretic operators: @{term"P \<union> Q"} is not well-typed if @{text"P, Q :: \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2 \<Rightarrow> bool"}, you have to write @{term"%x y. P x y & Q x y"} instead.
 \index{inductive predicates|)}
 *}
 
diff -r 53754ec7360b -r d74fe18f01e9 doc-src/TutorialI/Inductive/document/Mutual.tex
--- a/doc-src/TutorialI/Inductive/document/Mutual.tex	Wed Feb 10 19:37:34 2010 +0100
+++ b/doc-src/TutorialI/Inductive/document/Mutual.tex	Thu Feb 11 08:44:19 2010 +0100
@@ -101,13 +101,13 @@
 \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.
+\isa{evn\ n} instead of \isa{n\ {\isasymin}\ even}.
+When defining an n-ary relation as a predicate, it is recommended to curry
+the predicate: its type should be \mbox{\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.
 
-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.
+When should you choose sets and when predicates? If you intend to combine your notion with set theoretic notation, define it as an inductive set. If not, define it as an inductive predicate, thus avoiding the \isa{{\isasymin}} notation. But note that predicates of more than one argument cannot be combined with the usual set theoretic operators: \isa{P\ {\isasymunion}\ Q} is not well-typed if \isa{P{\isacharcomma}\ Q\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlisub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymtau}\isactrlisub {\isadigit{2}}\ {\isasymRightarrow}\ bool}, you have to write \isa{{\isasymlambda}x\ y{\isachardot}\ P\ x\ y\ {\isasymand}\ Q\ x\ y} instead.
 \index{inductive predicates|)}%
 \end{isamarkuptext}%
 \isamarkuptrue%
diff -r 53754ec7360b -r d74fe18f01e9 doc-src/TutorialI/Types/document/Numbers.tex
--- a/doc-src/TutorialI/Types/document/Numbers.tex	Wed Feb 10 19:37:34 2010 +0100
+++ b/doc-src/TutorialI/Types/document/Numbers.tex	Thu Feb 11 08:44:19 2010 +0100
@@ -107,7 +107,7 @@
 \rulename{add_commute}
 
 \begin{isabelle}%
-a\ {\isacharplus}\ {\isacharparenleft}b\ {\isacharplus}\ c{\isacharparenright}\ {\isacharequal}\ b\ {\isacharplus}\ {\isacharparenleft}a\ {\isacharplus}\ c{\isacharparenright}%
+b\ {\isacharplus}\ {\isacharparenleft}a\ {\isacharplus}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharplus}\ {\isacharparenleft}b\ {\isacharplus}\ c{\isacharparenright}%
 \end{isabelle}
 \rulename{add_left_commute}