56 (*>*) |
56 (*>*) |
57 |
57 |
58 subsection\<open>Inductively Defined Predicates\label{sec:ind-predicates}\<close> |
58 subsection\<open>Inductively Defined Predicates\label{sec:ind-predicates}\<close> |
59 |
59 |
60 text\<open>\index{inductive predicates|(} |
60 text\<open>\index{inductive predicates|(} |
61 Instead of a set of even numbers one can also define a predicate on @{typ nat}: |
61 Instead of a set of even numbers one can also define a predicate on \<^typ>\<open>nat\<close>: |
62 \<close> |
62 \<close> |
63 |
63 |
64 inductive evn :: "nat \<Rightarrow> bool" where |
64 inductive evn :: "nat \<Rightarrow> bool" where |
65 zero: "evn 0" | |
65 zero: "evn 0" | |
66 step: "evn n \<Longrightarrow> evn(Suc(Suc n))" |
66 step: "evn n \<Longrightarrow> evn(Suc(Suc n))" |
67 |
67 |
68 text\<open>\noindent Everything works as before, except that |
68 text\<open>\noindent Everything works as before, except that |
69 you write \commdx{inductive} instead of \isacommand{inductive\_set} and |
69 you write \commdx{inductive} instead of \isacommand{inductive\_set} and |
70 @{prop"evn n"} instead of @{prop"n \<in> Even"}. |
70 \<^prop>\<open>evn n\<close> instead of \<^prop>\<open>n \<in> Even\<close>. |
71 When defining an n-ary relation as a predicate, it is recommended to curry |
71 When defining an n-ary relation as a predicate, it is recommended to curry |
72 the predicate: its type should be \mbox{\<open>\<tau>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<tau>\<^sub>n \<Rightarrow> bool\<close>} |
72 the predicate: its type should be \mbox{\<open>\<tau>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<tau>\<^sub>n \<Rightarrow> bool\<close>} |
73 rather than |
73 rather than |
74 \<open>\<tau>\<^sub>1 \<times> \<dots> \<times> \<tau>\<^sub>n \<Rightarrow> bool\<close>. The curried version facilitates inductions. |
74 \<open>\<tau>\<^sub>1 \<times> \<dots> \<times> \<tau>\<^sub>n \<Rightarrow> bool\<close>. The curried version facilitates inductions. |
75 |
75 |
76 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 \<open>\<in>\<close> 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 \<open>P, Q :: \<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> bool\<close>, you have to write @{term"%x y. P x y & Q x y"} instead. |
76 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 \<open>\<in>\<close> notation. But note that predicates of more than one argument cannot be combined with the usual set theoretic operators: \<^term>\<open>P \<union> Q\<close> is not well-typed if \<open>P, Q :: \<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> bool\<close>, you have to write \<^term>\<open>%x y. P x y & Q x y\<close> instead. |
77 \index{inductive predicates|)} |
77 \index{inductive predicates|)} |
78 \<close> |
78 \<close> |
79 |
79 |
80 (*<*)end(*>*) |
80 (*<*)end(*>*) |