equal
deleted
inserted
replaced
4 |
4 |
5 text{*\noindent |
5 text{*\noindent |
6 Now that we have learned about rules and logic, we take another look at the |
6 Now that we have learned about rules and logic, we take another look at the |
7 finer points of induction. The two questions we answer are: what to do if the |
7 finer points of induction. The two questions we answer are: what to do if the |
8 proposition to be proved is not directly amenable to induction, and how to |
8 proposition to be proved is not directly amenable to induction, and how to |
9 utilize and even derive new induction schemas. |
9 utilize and even derive new induction schemas. We conclude with some slightly subtle |
|
10 examples of induction. |
10 *}; |
11 *}; |
11 |
12 |
12 subsection{*Massaging the proposition*}; |
13 subsection{*Massaging the proposition*}; |
13 |
14 |
14 text{*\label{sec:ind-var-in-prems} |
15 text{*\label{sec:ind-var-in-prems} |
80 Additionally, you may also have to universally quantify some other variables, |
81 Additionally, you may also have to universally quantify some other variables, |
81 which can yield a fairly complex conclusion. |
82 which can yield a fairly complex conclusion. |
82 Here is a simple example (which is proved by @{text"blast"}): |
83 Here is a simple example (which is proved by @{text"blast"}): |
83 *}; |
84 *}; |
84 |
85 |
85 lemma simple: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y"; |
86 lemma simple: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y \<and> A y"; |
86 (*<*)by blast;(*>*) |
87 (*<*)by blast;(*>*) |
87 |
88 |
88 text{*\noindent |
89 text{*\noindent |
89 You can get the desired lemma by explicit |
90 You can get the desired lemma by explicit |
90 application of modus ponens and @{thm[source]spec}: |
91 application of modus ponens and @{thm[source]spec}: |
103 yielding @{thm"myrule"[no_vars]}. |
104 yielding @{thm"myrule"[no_vars]}. |
104 You can go one step further and include these derivations already in the |
105 You can go one step further and include these derivations already in the |
105 statement of your original lemma, thus avoiding the intermediate step: |
106 statement of your original lemma, thus avoiding the intermediate step: |
106 *}; |
107 *}; |
107 |
108 |
108 lemma myrule[rule_format]: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y"; |
109 lemma myrule[rule_format]: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y \<and> A y"; |
109 (*<*) |
110 (*<*) |
110 by blast; |
111 by blast; |
111 (*>*) |
112 (*>*) |
112 |
113 |
113 text{* |
114 text{* |
127 some inductively defined set and the $x@i$ are variables. If instead we have |
128 some inductively defined set and the $x@i$ are variables. If instead we have |
128 a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we |
129 a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we |
129 replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as |
130 replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as |
130 \[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C \] |
131 \[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C \] |
131 For an example see \S\ref{sec:CTL-revisited} below. |
132 For an example see \S\ref{sec:CTL-revisited} below. |
|
133 |
|
134 Of course, all premises that share free variables with $t$ need to be pulled into |
|
135 the conclusion as well, under the @{text"\<forall>"}, again using @{text"\<longrightarrow>"} as shown above. |
132 *}; |
136 *}; |
133 |
137 |
134 subsection{*Beyond structural and recursion induction*}; |
138 subsection{*Beyond structural and recursion induction*}; |
135 |
139 |
136 text{*\label{sec:complete-ind} |
140 text{*\label{sec:complete-ind} |
147 holds for all $m<n$. In Isabelle, this is the theorem @{thm[source]nat_less_induct}: |
151 holds for all $m<n$. In Isabelle, this is the theorem @{thm[source]nat_less_induct}: |
148 @{thm[display]"nat_less_induct"[no_vars]} |
152 @{thm[display]"nat_less_induct"[no_vars]} |
149 Here is an example of its application. |
153 Here is an example of its application. |
150 *}; |
154 *}; |
151 |
155 |
152 consts f :: "nat => nat"; |
156 consts f :: "nat \<Rightarrow> nat"; |
153 axioms f_ax: "f(f(n)) < f(Suc(n))"; |
157 axioms f_ax: "f(f(n)) < f(Suc(n))"; |
154 |
158 |
155 text{*\noindent |
159 text{*\noindent |
156 From the above axiom\footnote{In general, the use of axioms is strongly |
160 From the above axiom\footnote{In general, the use of axioms is strongly |
157 discouraged, because of the danger of inconsistencies. The above axiom does |
161 discouraged, because of the danger of inconsistencies. The above axiom does |
287 |
291 |
288 theorem nat_less_induct: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> P n"; |
292 theorem nat_less_induct: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> P n"; |
289 by(insert induct_lem, blast); |
293 by(insert induct_lem, blast); |
290 |
294 |
291 text{* |
295 text{* |
292 |
|
293 Finally we should mention that HOL already provides the mother of all |
296 Finally we should mention that HOL already provides the mother of all |
294 inductions, \textbf{well-founded |
297 inductions, \textbf{well-founded |
295 induction}\indexbold{induction!well-founded}\index{well-founded |
298 induction}\indexbold{induction!well-founded}\index{well-founded |
296 induction|see{induction, well-founded}} (@{thm[source]wf_induct}): |
299 induction|see{induction, well-founded}} (@{thm[source]wf_induct}): |
297 @{thm[display]wf_induct[no_vars]} |
300 @{thm[display]wf_induct[no_vars]} |