src/Doc/Tutorial/Inductive/Even.thy
author wenzelm
Mon, 07 Oct 2013 21:24:44 +0200
changeset 54313 da2e6282a4f5
parent 48985 5386df44a037
child 56059 2390391584c2
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:
48895
4cd4ef1ef4a4 prefer ML_file over old uses;
wenzelm
parents: 43564
diff changeset
     1
(*<*)theory Even imports Main begin
4cd4ef1ef4a4 prefer ML_file over old uses;
wenzelm
parents: 43564
diff changeset
     2
ML_file "../../antiquote_setup.ML" 
4cd4ef1ef4a4 prefer ML_file over old uses;
wenzelm
parents: 43564
diff changeset
     3
setup Antiquote_Setup.setup
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42637
diff changeset
     4
(*>*)
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
     5
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
     6
section{* The Set of Even Numbers *}
10314
5b36035e4dff even numbers example
paulson
parents:
diff changeset
     7
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
     8
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
     9
\index{even numbers!defining inductively|(}%
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    10
The set of even numbers can be inductively defined as the least set
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    11
containing 0 and closed under the operation $+2$.  Obviously,
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    12
\emph{even} can also be expressed using the divides relation (@{text dvd}). 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    13
We shall prove below that the two formulations coincide.  On the way we
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    14
shall examine the primary means of reasoning about inductively defined
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    15
sets: rule induction.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    16
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    17
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    18
subsection{* Making an Inductive Definition *}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    19
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    20
text {*
23928
efee34ff4764 Protected underscore in inductive_set.
berghofe
parents: 23842
diff changeset
    21
Using \commdx{inductive\protect\_set}, we declare the constant @{text even} to be
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    22
a set of natural numbers with the desired properties.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    23
*}
10314
5b36035e4dff even numbers example
paulson
parents:
diff changeset
    24
25330
15bf0f47a87d added inductive
nipkow
parents: 23928
diff changeset
    25
inductive_set even :: "nat set" where
15bf0f47a87d added inductive
nipkow
parents: 23928
diff changeset
    26
zero[intro!]: "0 \<in> even" |
15bf0f47a87d added inductive
nipkow
parents: 23928
diff changeset
    27
step[intro!]: "n \<in> even \<Longrightarrow> (Suc (Suc n)) \<in> even"
10314
5b36035e4dff even numbers example
paulson
parents:
diff changeset
    28
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    29
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    30
An inductive definition consists of introduction rules.  The first one
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    31
above states that 0 is even; the second states that if $n$ is even, then so
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    32
is~$n+2$.  Given this declaration, Isabelle generates a fixed point
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    33
definition for @{term even} and proves theorems about it,
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    34
thus following the definitional approach (see {\S}\ref{sec:definitional}).
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    35
These theorems
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    36
include the introduction rules specified in the declaration, an elimination
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    37
rule for case analysis and an induction rule.  We can refer to these
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    38
theorems by automatically-generated names.  Here are two examples:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    39
@{named_thms[display,indent=0] even.zero[no_vars] (even.zero) even.step[no_vars] (even.step)}
10314
5b36035e4dff even numbers example
paulson
parents:
diff changeset
    40
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    41
The introduction rules can be given attributes.  Here
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    42
both rules are specified as \isa{intro!},%
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    43
\index{intro"!@\isa {intro"!} (attribute)}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    44
directing the classical reasoner to 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    45
apply them aggressively. Obviously, regarding 0 as even is safe.  The
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    46
@{text step} rule is also safe because $n+2$ is even if and only if $n$ is
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    47
even.  We prove this equivalence later.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    48
*}
10314
5b36035e4dff even numbers example
paulson
parents:
diff changeset
    49
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    50
subsection{*Using Introduction Rules*}
10314
5b36035e4dff even numbers example
paulson
parents:
diff changeset
    51
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    52
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    53
Our first lemma states that numbers of the form $2\times k$ are even.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    54
Introduction rules are used to show that specific values belong to the
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    55
inductive set.  Such proofs typically involve 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    56
induction, perhaps over some other inductive set.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    57
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    58
11705
ac8ca15c556c fixed numerals;
wenzelm
parents: 10883
diff changeset
    59
lemma two_times_even[intro!]: "2*k \<in> even"
12328
7c4ec77a8715 *** empty log message ***
nipkow
parents: 11705
diff changeset
    60
apply (induct_tac k)
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    61
 apply auto
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    62
done
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    63
(*<*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    64
lemma "2*k \<in> even"
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    65
apply (induct_tac k)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    66
(*>*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    67
txt {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    68
\noindent
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    69
The first step is induction on the natural number @{text k}, which leaves
10883
2b9f87bf9113 updated for new version of even-examples.tex
paulson
parents: 10341
diff changeset
    70
two subgoals:
2b9f87bf9113 updated for new version of even-examples.tex
paulson
parents: 10341
diff changeset
    71
@{subgoals[display,indent=0,margin=65]}
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    72
Here @{text auto} simplifies both subgoals so that they match the introduction
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    73
rules, which are then applied automatically.
10314
5b36035e4dff even numbers example
paulson
parents:
diff changeset
    74
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    75
Our ultimate goal is to prove the equivalence between the traditional
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    76
definition of @{text even} (using the divides relation) and our inductive
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    77
definition.  One direction of this equivalence is immediate by the lemma
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    78
just proved, whose @{text "intro!"} attribute ensures it is applied automatically.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    79
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    80
(*<*)oops(*>*)
11705
ac8ca15c556c fixed numerals;
wenzelm
parents: 10883
diff changeset
    81
lemma dvd_imp_even: "2 dvd n \<Longrightarrow> n \<in> even"
10883
2b9f87bf9113 updated for new version of even-examples.tex
paulson
parents: 10341
diff changeset
    82
by (auto simp add: dvd_def)
10314
5b36035e4dff even numbers example
paulson
parents:
diff changeset
    83
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    84
subsection{* Rule Induction \label{sec:rule-induction} *}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    85
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    86
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    87
\index{rule induction|(}%
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    88
From the definition of the set
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    89
@{term even}, Isabelle has
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    90
generated an induction rule:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    91
@{named_thms [display,indent=0,margin=40] even.induct [no_vars] (even.induct)}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    92
A property @{term P} holds for every even number provided it
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    93
holds for~@{text 0} and is closed under the operation
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    94
\isa{Suc(Suc \(\cdot\))}.  Then @{term P} is closed under the introduction
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    95
rules for @{term even}, which is the least set closed under those rules. 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    96
This type of inductive argument is called \textbf{rule induction}. 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    97
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    98
Apart from the double application of @{term Suc}, the induction rule above
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    99
resembles the familiar mathematical induction, which indeed is an instance
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   100
of rule induction; the natural numbers can be defined inductively to be
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   101
the least set containing @{text 0} and closed under~@{term Suc}.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   102
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   103
Induction is the usual way of proving a property of the elements of an
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   104
inductively defined set.  Let us prove that all members of the set
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   105
@{term even} are multiples of two.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   106
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   107
11705
ac8ca15c556c fixed numerals;
wenzelm
parents: 10883
diff changeset
   108
lemma even_imp_dvd: "n \<in> even \<Longrightarrow> 2 dvd n"
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   109
txt {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   110
We begin by applying induction.  Note that @{text even.induct} has the form
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   111
of an elimination rule, so we use the method @{text erule}.  We get two
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   112
subgoals:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   113
*}
10314
5b36035e4dff even numbers example
paulson
parents:
diff changeset
   114
apply (erule even.induct)
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   115
txt {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   116
@{subgoals[display,indent=0]}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   117
We unfold the definition of @{text dvd} in both subgoals, proving the first
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   118
one and simplifying the second:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   119
*}
10883
2b9f87bf9113 updated for new version of even-examples.tex
paulson
parents: 10341
diff changeset
   120
apply (simp_all add: dvd_def)
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   121
txt {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   122
@{subgoals[display,indent=0]}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   123
The next command eliminates the existential quantifier from the assumption
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   124
and replaces @{text n} by @{text "2 * k"}.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   125
*}
10314
5b36035e4dff even numbers example
paulson
parents:
diff changeset
   126
apply clarify
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   127
txt {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   128
@{subgoals[display,indent=0]}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   129
To conclude, we tell Isabelle that the desired value is
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   130
@{term "Suc k"}.  With this hint, the subgoal falls to @{text simp}.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   131
*}
10883
2b9f87bf9113 updated for new version of even-examples.tex
paulson
parents: 10341
diff changeset
   132
apply (rule_tac x = "Suc k" in exI, simp)
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   133
(*<*)done(*>*)
10314
5b36035e4dff even numbers example
paulson
parents:
diff changeset
   134
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   135
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   136
Combining the previous two results yields our objective, the
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   137
equivalence relating @{term even} and @{text dvd}. 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   138
%
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   139
%we don't want [iff]: discuss?
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   140
*}
10314
5b36035e4dff even numbers example
paulson
parents:
diff changeset
   141
11705
ac8ca15c556c fixed numerals;
wenzelm
parents: 10883
diff changeset
   142
theorem even_iff_dvd: "(n \<in> even) = (2 dvd n)"
10883
2b9f87bf9113 updated for new version of even-examples.tex
paulson
parents: 10341
diff changeset
   143
by (blast intro: dvd_imp_even even_imp_dvd)
10314
5b36035e4dff even numbers example
paulson
parents:
diff changeset
   144
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   145
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   146
subsection{* Generalization and Rule Induction \label{sec:gen-rule-induction} *}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   147
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   148
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   149
\index{generalizing for induction}%
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   150
Before applying induction, we typically must generalize
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   151
the induction formula.  With rule induction, the required generalization
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   152
can be hard to find and sometimes requires a complete reformulation of the
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   153
problem.  In this  example, our first attempt uses the obvious statement of
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   154
the result.  It fails:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   155
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   156
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   157
lemma "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even"
10314
5b36035e4dff even numbers example
paulson
parents:
diff changeset
   158
apply (erule even.induct)
5b36035e4dff even numbers example
paulson
parents:
diff changeset
   159
oops
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   160
(*<*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   161
lemma "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even"
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   162
apply (erule even.induct)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   163
(*>*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   164
txt {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   165
Rule induction finds no occurrences of @{term "Suc(Suc n)"} in the
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   166
conclusion, which it therefore leaves unchanged.  (Look at
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   167
@{text even.induct} to see why this happens.)  We have these subgoals:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   168
@{subgoals[display,indent=0]}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   169
The first one is hopeless.  Rule induction on
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   170
a non-variable term discards information, and usually fails.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   171
How to deal with such situations
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   172
in general is described in {\S}\ref{sec:ind-var-in-prems} below.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   173
In the current case the solution is easy because
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   174
we have the necessary inverse, subtraction:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   175
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   176
(*<*)oops(*>*)
11705
ac8ca15c556c fixed numerals;
wenzelm
parents: 10883
diff changeset
   177
lemma even_imp_even_minus_2: "n \<in> even \<Longrightarrow> n - 2 \<in> even"
10314
5b36035e4dff even numbers example
paulson
parents:
diff changeset
   178
apply (erule even.induct)
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   179
 apply auto
10314
5b36035e4dff even numbers example
paulson
parents:
diff changeset
   180
done
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   181
(*<*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   182
lemma "n \<in>  even \<Longrightarrow> n - 2 \<in> even"
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   183
apply (erule even.induct)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   184
(*>*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   185
txt {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   186
This lemma is trivially inductive.  Here are the subgoals:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   187
@{subgoals[display,indent=0]}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   188
The first is trivial because @{text "0 - 2"} simplifies to @{text 0}, which is
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   189
even.  The second is trivial too: @{term "Suc (Suc n) - 2"} simplifies to
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   190
@{term n}, matching the assumption.%
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   191
\index{rule induction|)}  %the sequel isn't really about induction
10314
5b36035e4dff even numbers example
paulson
parents:
diff changeset
   192
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   193
\medskip
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   194
Using our lemma, we can easily prove the result we originally wanted:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   195
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   196
(*<*)oops(*>*)
10883
2b9f87bf9113 updated for new version of even-examples.tex
paulson
parents: 10341
diff changeset
   197
lemma Suc_Suc_even_imp_even: "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even"
2b9f87bf9113 updated for new version of even-examples.tex
paulson
parents: 10341
diff changeset
   198
by (drule even_imp_even_minus_2, simp)
10326
d4fe5ce8a5d5 minor tinkering
paulson
parents: 10314
diff changeset
   199
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   200
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   201
We have just proved the converse of the introduction rule @{text even.step}.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   202
This suggests proving the following equivalence.  We give it the
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   203
\attrdx{iff} attribute because of its obvious value for simplification.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   204
*}
10326
d4fe5ce8a5d5 minor tinkering
paulson
parents: 10314
diff changeset
   205
d4fe5ce8a5d5 minor tinkering
paulson
parents: 10314
diff changeset
   206
lemma [iff]: "((Suc (Suc n)) \<in> even) = (n \<in> even)"
10883
2b9f87bf9113 updated for new version of even-examples.tex
paulson
parents: 10341
diff changeset
   207
by (blast dest: Suc_Suc_even_imp_even)
10314
5b36035e4dff even numbers example
paulson
parents:
diff changeset
   208
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   209
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   210
subsection{* Rule Inversion \label{sec:rule-inversion} *}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   211
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   212
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   213
\index{rule inversion|(}%
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   214
Case analysis on an inductive definition is called \textbf{rule
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   215
inversion}.  It is frequently used in proofs about operational
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   216
semantics.  It can be highly effective when it is applied
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   217
automatically.  Let us look at how rule inversion is done in
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   218
Isabelle/HOL\@.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   219
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   220
Recall that @{term even} is the minimal set closed under these two rules:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   221
@{thm [display,indent=0] even.intros [no_vars]}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   222
Minimality means that @{term even} contains only the elements that these
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   223
rules force it to contain.  If we are told that @{term a}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   224
belongs to
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   225
@{term even} then there are only two possibilities.  Either @{term a} is @{text 0}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   226
or else @{term a} has the form @{term "Suc(Suc n)"}, for some suitable @{term n}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   227
that belongs to
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   228
@{term even}.  That is the gist of the @{term cases} rule, which Isabelle proves
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   229
for us when it accepts an inductive definition:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   230
@{named_thms [display,indent=0,margin=40] even.cases [no_vars] (even.cases)}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   231
This general rule is less useful than instances of it for
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   232
specific patterns.  For example, if @{term a} has the form
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   233
@{term "Suc(Suc n)"} then the first case becomes irrelevant, while the second
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   234
case tells us that @{term n} belongs to @{term even}.  Isabelle will generate
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   235
this instance for us:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   236
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   237
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   238
inductive_cases Suc_Suc_cases [elim!]: "Suc(Suc n) \<in> even"
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   239
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   240
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   241
The \commdx{inductive\protect\_cases} command generates an instance of
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   242
the @{text cases} rule for the supplied pattern and gives it the supplied name:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   243
@{named_thms [display,indent=0] Suc_Suc_cases [no_vars] (Suc_Suc_cases)}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   244
Applying this as an elimination rule yields one case where @{text even.cases}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   245
would yield two.  Rule inversion works well when the conclusions of the
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   246
introduction rules involve datatype constructors like @{term Suc} and @{text "#"}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   247
(list ``cons''); freeness reasoning discards all but one or two cases.
10314
5b36035e4dff even numbers example
paulson
parents:
diff changeset
   248
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   249
In the \isacommand{inductive\_cases} command we supplied an
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   250
attribute, @{text "elim!"},
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   251
\index{elim"!@\isa {elim"!} (attribute)}%
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   252
indicating that this elimination rule can be
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   253
applied aggressively.  The original
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   254
@{term cases} rule would loop if used in that manner because the
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   255
pattern~@{term a} matches everything.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   256
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   257
The rule @{text Suc_Suc_cases} is equivalent to the following implication:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   258
@{term [display,indent=0] "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even"}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   259
Just above we devoted some effort to reaching precisely
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   260
this result.  Yet we could have obtained it by a one-line declaration,
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   261
dispensing with the lemma @{text even_imp_even_minus_2}. 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   262
This example also justifies the terminology
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   263
\textbf{rule inversion}: the new rule inverts the introduction rule
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   264
@{text even.step}.  In general, a rule can be inverted when the set of elements
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   265
it introduces is disjoint from those of the other introduction rules.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   266
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   267
For one-off applications of rule inversion, use the \methdx{ind_cases} method. 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   268
Here is an example:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   269
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   270
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   271
(*<*)lemma "Suc(Suc n) \<in> even \<Longrightarrow> P"(*>*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   272
apply (ind_cases "Suc(Suc n) \<in> even")
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   273
(*<*)oops(*>*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   274
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   275
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   276
The specified instance of the @{text cases} rule is generated, then applied
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   277
as an elimination rule.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   278
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   279
To summarize, every inductive definition produces a @{text cases} rule.  The
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   280
\commdx{inductive\protect\_cases} command stores an instance of the
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   281
@{text cases} rule for a given pattern.  Within a proof, the
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   282
@{text ind_cases} method applies an instance of the @{text cases}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   283
rule.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   284
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   285
The even numbers example has shown how inductive definitions can be
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   286
used.  Later examples will show that they are actually worth using.%
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   287
\index{rule inversion|)}%
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   288
\index{even numbers!defining inductively|)}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   289
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   290
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   291
(*<*)end(*>*)