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