17914

1 
(*<*)theory Mutual imports Main begin(*>*)

10762

2 

10884

3 
subsection{*Mutually Inductive Definitions*}

10762

4 


5 
text{*


6 
Just as there are datatypes defined by mutual recursion, there are sets defined

10790

7 
by mutual induction. As a trivial example we consider the even and odd


8 
natural numbers:

10762

9 
*}


10 

23733

11 
inductive_set

25330

12 
Even :: "nat set" and


13 
Odd :: "nat set"

23733

14 
where


15 
zero: "0 \<in> Even"


16 
 EvenI: "n \<in> Odd \<Longrightarrow> Suc n \<in> Even"


17 
 OddI: "n \<in> Even \<Longrightarrow> Suc n \<in> Odd"

10762

18 


19 
text{*\noindent

10790

20 
The mutually inductive definition of multiple sets is no different from


21 
that of a single set, except for induction: just as for mutually recursive


22 
datatypes, induction needs to involve all the simultaneously defined sets. In

19389

23 
the above case, the induction rule is called @{thm[source]Even_Odd.induct}

10790

24 
(simply concatenate the names of the sets involved) and has the conclusion

19389

25 
@{text[display]"(?x \<in> Even \<longrightarrow> ?P ?x) \<and> (?y \<in> Odd \<longrightarrow> ?Q ?y)"}

10762

26 

11494

27 
If we want to prove that all even numbers are divisible by two, we have to

10790

28 
generalize the statement as follows:

10762

29 
*}


30 

19389

31 
lemma "(m \<in> Even \<longrightarrow> 2 dvd m) \<and> (n \<in> Odd \<longrightarrow> 2 dvd (Suc n))"

10762

32 


33 
txt{*\noindent

10790

34 
The proof is by rule induction. Because of the form of the induction theorem,


35 
it is applied by @{text rule} rather than @{text erule} as for ordinary


36 
inductive definitions:

10762

37 
*}


38 

19389

39 
apply(rule Even_Odd.induct)

10762

40 


41 
txt{*


42 
@{subgoals[display,indent=0]}


43 
The first two subgoals are proved by simplification and the final one can be


44 
proved in the same manner as in \S\ref{sec:ruleinduction}


45 
where the same subgoal was encountered before.


46 
We do not show the proof script.


47 
*}


48 
(*<*)


49 
apply simp


50 
apply simp

12815

51 
apply(simp add: dvd_def)

10762

52 
apply(clarify)


53 
apply(rule_tac x = "Suc k" in exI)


54 
apply simp


55 
done


56 
(*>*)

25330

57 


58 
subsection{*Inductively Defined Predicates\label{sec:indpredicates}*}


59 


60 
text{*\index{inductive predicates(}


61 
Instead of a set of even numbers one can also define a predicate on @{typ nat}:


62 
*}


63 


64 
inductive evn :: "nat \<Rightarrow> bool" where


65 
zero: "evn 0" 


66 
step: "evn n \<Longrightarrow> evn(Suc(Suc n))"


67 


68 
text{*\noindent Everything works as before, except that


69 
you write \commdx{inductive} instead of \isacommand{inductive\_set} and

35103

70 
@{prop"evn n"} instead of @{prop"n : even"}.


71 
When defining an nary relation as a predicate, it is recommended to curry


72 
the predicate: its type should be \mbox{@{text"\<tau>\<^isub>1 \<Rightarrow> \<dots> \<Rightarrow> \<tau>\<^isub>n \<Rightarrow> bool"}}


73 
rather than


74 
@{text"\<tau>\<^isub>1 \<times> \<dots> \<times> \<tau>\<^isub>n \<Rightarrow> bool"}. The curried version facilitates inductions.

25330

75 

35103

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 @{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 welltyped 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.

25330

77 
\index{inductive predicates)}


78 
*}


79 

10790

80 
(*<*)end(*>*)
