author | wenzelm |
Sat, 05 Jan 2019 17:24:33 +0100 | |
changeset 69597 | ff784d5a5bfb |
parent 69505 | cc2d676d5395 |
permissions | -rw-r--r-- |
56820 | 1 |
(*<*) |
2 |
theory How_to_Prove_it |
|
3 |
imports Complex_Main |
|
4 |
begin |
|
5 |
(*>*) |
|
67406 | 6 |
text\<open> |
69597 | 7 |
\chapter{\<^theory>\<open>Main\<close>} |
56820 | 8 |
|
9 |
\section{Natural numbers} |
|
10 |
||
11 |
%Tobias Nipkow |
|
12 |
\paragraph{Induction rules}~\\ |
|
13 |
In addition to structural induction there is the induction rule |
|
14 |
@{thm[source] less_induct}: |
|
15 |
\begin{quote} |
|
16 |
@{thm less_induct} |
|
17 |
\end{quote} |
|
18 |
This is often called ``complete induction''. It is applied like this: |
|
19 |
\begin{quote} |
|
69505 | 20 |
(\<open>induction n rule: less_induct\<close>) |
56820 | 21 |
\end{quote} |
69597 | 22 |
In fact, it is not restricted to \<^typ>\<open>nat\<close> but works for any wellfounded |
69505 | 23 |
order \<open><\<close>. |
56820 | 24 |
|
25 |
There are many more special induction rules. You can find all of them |
|
26 |
via the Find button (in Isabelle/jedit) with the following search criteria: |
|
27 |
\begin{quote} |
|
28 |
\texttt{name: Nat name: induct} |
|
29 |
\end{quote} |
|
30 |
||
31 |
||
69597 | 32 |
\paragraph{How to convert numerals into \<^const>\<open>Suc\<close> terms}~\\ |
56820 | 33 |
Solution: simplify with the lemma @{thm[source] numeral_eq_Suc}. |
34 |
||
35 |
\noindent |
|
36 |
Example: |
|
67406 | 37 |
\<close> |
56820 | 38 |
|
39 |
lemma fixes x :: int shows "x ^ 3 = x * x * x" |
|
40 |
by (simp add: numeral_eq_Suc) |
|
41 |
||
69505 | 42 |
text\<open>This is a typical situation: function ``\<open>^\<close>'' is defined |
69597 | 43 |
by pattern matching on \<^const>\<open>Suc\<close> but is applied to a numeral. |
56820 | 44 |
|
45 |
Note: simplification with @{thm[source] numeral_eq_Suc} will convert all numerals. |
|
46 |
One can be more specific with the lemmas @{thm [source] numeral_2_eq_2} |
|
47 |
(@{thm numeral_2_eq_2}) and @{thm[source] numeral_3_eq_3} (@{thm numeral_3_eq_3}). |
|
48 |
||
49 |
||
50 |
\section{Lists} |
|
51 |
||
52 |
%Tobias Nipkow |
|
53 |
\paragraph{Induction rules}~\\ |
|
54 |
In addition to structural induction there are a few more induction rules |
|
55 |
that come in handy at times: |
|
56 |
\begin{itemize} |
|
57 |
\item |
|
58 |
Structural induction where the new element is appended to the end |
|
59 |
of the list (@{thm[source] rev_induct}): |
|
60 |
||
61 |
@{thm rev_induct} |
|
62 |
||
63 |
\item Induction on the length of a list (@{thm [source] length_induct}): |
|
64 |
||
65 |
@{thm length_induct} |
|
66 |
||
67 |
\item Simultaneous induction on two lists of the same length (@{thm [source] list_induct2}): |
|
68 |
||
69 |
@{thm[display,margin=60] list_induct2} |
|
70 |
||
71 |
\end{itemize} |
|
72 |
||
73 |
%Tobias Nipkow |
|
74 |
\section{Algebraic simplification} |
|
75 |
||
69597 | 76 |
On the numeric types \<^typ>\<open>nat\<close>, \<^typ>\<open>int\<close> and \<^typ>\<open>real\<close>, |
69505 | 77 |
proof method \<open>simp\<close> and friends can deal with a limited amount of linear |
78 |
arithmetic (no multiplication except by numerals) and method \<open>arith\<close> can |
|
69597 | 79 |
handle full linear arithmetic (on \<^typ>\<open>nat\<close>, \<^typ>\<open>int\<close> including quantifiers). |
56820 | 80 |
But what to do when proper multiplication is involved? |
81 |
At this point it can be helpful to simplify with the lemma list |
|
82 |
@{thm [source] algebra_simps}. Examples: |
|
67406 | 83 |
\<close> |
56820 | 84 |
|
85 |
lemma fixes x :: int |
|
86 |
shows "(x + y) * (y - z) = (y - z) * x + y * (y-z)" |
|
87 |
by(simp add: algebra_simps) |
|
88 |
||
89 |
lemma fixes x :: "'a :: comm_ring" |
|
90 |
shows "(x + y) * (y - z) = (y - z) * x + y * (y-z)" |
|
91 |
by(simp add: algebra_simps) |
|
92 |
||
67406 | 93 |
text\<open> |
56820 | 94 |
Rewriting with @{thm[source] algebra_simps} has the following effect: |
95 |
terms are rewritten into a normal form by multiplying out, |
|
96 |
rearranging sums and products into some canonical order. |
|
97 |
In the above lemma the normal form will be something like |
|
69597 | 98 |
\<^term>\<open>x*y + y*y - x*z - y*z\<close>. |
99 |
This works for concrete types like \<^typ>\<open>int\<close> as well as for classes like |
|
100 |
\<^class>\<open>comm_ring\<close> (commutative rings). For some classes (e.g.\ \<^class>\<open>ring\<close> |
|
101 |
and \<^class>\<open>comm_ring\<close>) this yields a decision procedure for equality. |
|
56820 | 102 |
|
103 |
Additional function and predicate symbols are not a problem either: |
|
67406 | 104 |
\<close> |
56820 | 105 |
|
106 |
lemma fixes f :: "int \<Rightarrow> int" shows "2 * f(x*y) - f(y*x) < f(y*x) + 1" |
|
107 |
by(simp add: algebra_simps) |
|
108 |
||
67406 | 109 |
text\<open>Here @{thm[source]algebra_simps} merely has the effect of rewriting |
69597 | 110 |
\<^term>\<open>y*x\<close> to \<^term>\<open>x*y\<close> (or the other way around). This yields |
111 |
a problem of the form \<^prop>\<open>2*t - t < t + (1::int)\<close> and we are back in the |
|
56820 | 112 |
realm of linear arithmetic. |
113 |
||
114 |
Because @{thm[source]algebra_simps} multiplies out, terms can explode. |
|
115 |
If one merely wants to bring sums or products into a canonical order |
|
67406 | 116 |
it suffices to rewrite with @{thm [source] ac_simps}:\<close> |
56820 | 117 |
|
118 |
lemma fixes f :: "int \<Rightarrow> int" shows "f(x*y*z) - f(z*x*y) = 0" |
|
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
56820
diff
changeset
|
119 |
by(simp add: ac_simps) |
56820 | 120 |
|
67406 | 121 |
text\<open>The lemmas @{thm[source]algebra_simps} take care of addition, subtraction |
56820 | 122 |
and multiplication (algebraic structures up to rings) but ignore division (fields). |
123 |
The lemmas @{thm[source]field_simps} also deal with division: |
|
67406 | 124 |
\<close> |
56820 | 125 |
|
126 |
lemma fixes x :: real shows "x+z \<noteq> 0 \<Longrightarrow> 1 + y/(x+z) = (x+y+z)/(x+z)" |
|
127 |
by(simp add: field_simps) |
|
128 |
||
67406 | 129 |
text\<open>Warning: @{thm[source]field_simps} can blow up your terms |
130 |
beyond recognition.\<close> |
|
56820 | 131 |
|
132 |
(*<*) |
|
133 |
end |
|
67399 | 134 |
(*>*) |