author  wenzelm 
Mon, 07 Oct 2013 21:24:44 +0200  
changeset 54313  da2e6282a4f5 
parent 53015  a1119cf551e8 
child 58774  d6435f0bf966 
permissions  rwrr 
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 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
48985
diff
changeset

72 
the predicate: its type should be \mbox{@{text"\<tau>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<tau>\<^sub>n \<Rightarrow> bool"}} 
35103  73 
rather than 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
48985
diff
changeset

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

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
48985
diff
changeset

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>\<^sub>1 \<Rightarrow> \<tau>\<^sub>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(*>*) 