equal
deleted
inserted
replaced
68 \[ A@1 \longrightarrow \cdots A@n \longrightarrow C. \] |
68 \[ A@1 \longrightarrow \cdots A@n \longrightarrow C. \] |
69 Additionally, you may also have to universally quantify some other variables, |
69 Additionally, you may also have to universally quantify some other variables, |
70 which can yield a fairly complex conclusion. However, @{text rule_format} |
70 which can yield a fairly complex conclusion. However, @{text rule_format} |
71 can remove any number of occurrences of @{text"\<forall>"} and |
71 can remove any number of occurrences of @{text"\<forall>"} and |
72 @{text"\<longrightarrow>"}. |
72 @{text"\<longrightarrow>"}. |
73 *} |
73 |
74 |
|
75 (*<*) |
|
76 by auto; |
|
77 (*>*) |
|
78 (* |
|
79 Here is a simple example (which is proved by @{text"blast"}): |
|
80 lemma simple[rule_format]: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y \<and> A y"; |
|
81 by blast; |
|
82 *) |
|
83 |
|
84 text{* |
|
85 \index{induction!on a term}% |
74 \index{induction!on a term}% |
86 A second reason why your proposition may not be amenable to induction is that |
75 A second reason why your proposition may not be amenable to induction is that |
87 you want to induct on a complex term, rather than a variable. In |
76 you want to induct on a complex term, rather than a variable. In |
88 general, induction on a term~$t$ requires rephrasing the conclusion~$C$ |
77 general, induction on a term~$t$ requires rephrasing the conclusion~$C$ |
89 as |
78 as |
120 $C$ on the free variables of $t$ has been made explicit. |
109 $C$ on the free variables of $t$ has been made explicit. |
121 Unfortunately, this induction schema cannot be expressed as a |
110 Unfortunately, this induction schema cannot be expressed as a |
122 single theorem because it depends on the number of free variables in $t$ --- |
111 single theorem because it depends on the number of free variables in $t$ --- |
123 the notation $\overline{y}$ is merely an informal device. |
112 the notation $\overline{y}$ is merely an informal device. |
124 *} |
113 *} |
|
114 (*<*)by auto(*>*) |
125 |
115 |
126 subsection{*Beyond Structural and Recursion Induction*}; |
116 subsection{*Beyond Structural and Recursion Induction*}; |
127 |
117 |
128 text{*\label{sec:complete-ind} |
118 text{*\label{sec:complete-ind} |
129 So far, inductive proofs were by structural induction for |
119 So far, inductive proofs were by structural induction for |