src/Doc/Tutorial/Inductive/Mutual.thy
author wenzelm
Mon, 07 Oct 2013 21:24:44 +0200
changeset 54313 da2e6282a4f5
parent 53015 a1119cf551e8
child 58774 d6435f0bf966
permissions -rw-r--r--
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17914
99ead7a7eb42 fix headers;
wenzelm
parents: 12815
diff changeset
     1
(*<*)theory Mutual imports Main begin(*>*)
10762
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
     2
10884
2995639c6a09 renaming of some files
paulson
parents: 10790
diff changeset
     3
subsection{*Mutually Inductive Definitions*}
10762
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
     4
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
     5
text{*
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
     6
Just as there are datatypes defined by mutual recursion, there are sets defined
10790
520dd8696927 *** empty log message ***
nipkow
parents: 10762
diff changeset
     7
by mutual induction. As a trivial example we consider the even and odd
520dd8696927 *** empty log message ***
nipkow
parents: 10762
diff changeset
     8
natural numbers:
10762
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
     9
*}
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    10
23733
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 19389
diff changeset
    11
inductive_set
25330
15bf0f47a87d added inductive
nipkow
parents: 23733
diff changeset
    12
  Even :: "nat set" and
15bf0f47a87d added inductive
nipkow
parents: 23733
diff changeset
    13
  Odd  :: "nat set"
23733
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 19389
diff changeset
    14
where
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 19389
diff changeset
    15
  zero:  "0 \<in> Even"
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 19389
diff changeset
    16
| EvenI: "n \<in> Odd \<Longrightarrow> Suc n \<in> Even"
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 19389
diff changeset
    17
| OddI:  "n \<in> Even \<Longrightarrow> Suc n \<in> Odd"
10762
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    18
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    19
text{*\noindent
10790
520dd8696927 *** empty log message ***
nipkow
parents: 10762
diff changeset
    20
The mutually inductive definition of multiple sets is no different from
520dd8696927 *** empty log message ***
nipkow
parents: 10762
diff changeset
    21
that of a single set, except for induction: just as for mutually recursive
520dd8696927 *** empty log message ***
nipkow
parents: 10762
diff changeset
    22
datatypes, induction needs to involve all the simultaneously defined sets. In
19389
0d57259fea82 Even/Odd: avoid clash with even/odd of Main HOL;
wenzelm
parents: 17914
diff changeset
    23
the above case, the induction rule is called @{thm[source]Even_Odd.induct}
10790
520dd8696927 *** empty log message ***
nipkow
parents: 10762
diff changeset
    24
(simply concatenate the names of the sets involved) and has the conclusion
19389
0d57259fea82 Even/Odd: avoid clash with even/odd of Main HOL;
wenzelm
parents: 17914
diff changeset
    25
@{text[display]"(?x \<in> Even \<longrightarrow> ?P ?x) \<and> (?y \<in> Odd \<longrightarrow> ?Q ?y)"}
10762
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    26
11494
23a118849801 revisions and indexing
paulson
parents: 10884
diff changeset
    27
If we want to prove that all even numbers are divisible by two, we have to
10790
520dd8696927 *** empty log message ***
nipkow
parents: 10762
diff changeset
    28
generalize the statement as follows:
10762
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    29
*}
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    30
19389
0d57259fea82 Even/Odd: avoid clash with even/odd of Main HOL;
wenzelm
parents: 17914
diff changeset
    31
lemma "(m \<in> Even \<longrightarrow> 2 dvd m) \<and> (n \<in> Odd \<longrightarrow> 2 dvd (Suc n))"
10762
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    32
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    33
txt{*\noindent
10790
520dd8696927 *** empty log message ***
nipkow
parents: 10762
diff changeset
    34
The proof is by rule induction. Because of the form of the induction theorem,
520dd8696927 *** empty log message ***
nipkow
parents: 10762
diff changeset
    35
it is applied by @{text rule} rather than @{text erule} as for ordinary
520dd8696927 *** empty log message ***
nipkow
parents: 10762
diff changeset
    36
inductive definitions:
10762
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    37
*}
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    38
19389
0d57259fea82 Even/Odd: avoid clash with even/odd of Main HOL;
wenzelm
parents: 17914
diff changeset
    39
apply(rule Even_Odd.induct)
10762
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    40
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    41
txt{*
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    42
@{subgoals[display,indent=0]}
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    43
The first two subgoals are proved by simplification and the final one can be
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    44
proved in the same manner as in \S\ref{sec:rule-induction}
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    45
where the same subgoal was encountered before.
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    46
We do not show the proof script.
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    47
*}
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    48
(*<*)
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    49
  apply simp
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    50
 apply simp
12815
wenzelm
parents: 11494
diff changeset
    51
apply(simp add: dvd_def)
10762
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    52
apply(clarify)
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    53
apply(rule_tac x = "Suc k" in exI)
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    54
apply simp
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    55
done
cd1a2bee5549 *** empty log message ***
nipkow
parents:
diff changeset
    56
(*>*)
25330
15bf0f47a87d added inductive
nipkow
parents: 23733
diff changeset
    57
15bf0f47a87d added inductive
nipkow
parents: 23733
diff changeset
    58
subsection{*Inductively Defined Predicates\label{sec:ind-predicates}*}
15bf0f47a87d added inductive
nipkow
parents: 23733
diff changeset
    59
15bf0f47a87d added inductive
nipkow
parents: 23733
diff changeset
    60
text{*\index{inductive predicates|(}
15bf0f47a87d added inductive
nipkow
parents: 23733
diff changeset
    61
Instead of a set of even numbers one can also define a predicate on @{typ nat}:
15bf0f47a87d added inductive
nipkow
parents: 23733
diff changeset
    62
*}
15bf0f47a87d added inductive
nipkow
parents: 23733
diff changeset
    63
15bf0f47a87d added inductive
nipkow
parents: 23733
diff changeset
    64
inductive evn :: "nat \<Rightarrow> bool" where
15bf0f47a87d added inductive
nipkow
parents: 23733
diff changeset
    65
zero: "evn 0" |
15bf0f47a87d added inductive
nipkow
parents: 23733
diff changeset
    66
step: "evn n \<Longrightarrow> evn(Suc(Suc n))"
15bf0f47a87d added inductive
nipkow
parents: 23733
diff changeset
    67
15bf0f47a87d added inductive
nipkow
parents: 23733
diff changeset
    68
text{*\noindent Everything works as before, except that
15bf0f47a87d added inductive
nipkow
parents: 23733
diff changeset
    69
you write \commdx{inductive} instead of \isacommand{inductive\_set} and
35103
d74fe18f01e9 inductive vs inductive_set explanation
nipkow
parents: 25330
diff changeset
    70
@{prop"evn n"} instead of @{prop"n : even"}.
d74fe18f01e9 inductive vs inductive_set explanation
nipkow
parents: 25330
diff changeset
    71
When defining an n-ary 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
d74fe18f01e9 inductive vs inductive_set explanation
nipkow
parents: 25330
diff changeset
    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
15bf0f47a87d added inductive
nipkow
parents: 23733
diff changeset
    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 well-typed 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
15bf0f47a87d added inductive
nipkow
parents: 23733
diff changeset
    77
\index{inductive predicates|)}
15bf0f47a87d added inductive
nipkow
parents: 23733
diff changeset
    78
*}
15bf0f47a87d added inductive
nipkow
parents: 23733
diff changeset
    79
10790
520dd8696927 *** empty log message ***
nipkow
parents: 10762
diff changeset
    80
(*<*)end(*>*)