equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Induction}% |
3 \def\isabellecontext{Induction}% |
4 \isamarkupfalse% |
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 \isamarkuptrue% |
5 % |
18 % |
6 \begin{isamarkuptext}% |
19 \begin{isamarkuptext}% |
7 Assuming we have defined our function such that Isabelle could prove |
20 Assuming we have defined our function such that Isabelle could prove |
8 termination and that the recursion equations (or some suitable derived |
21 termination and that the recursion equations (or some suitable derived |
9 equations) are simplification rules, we might like to prove something about |
22 equations) are simplification rules, we might like to prove something about |
17 requires you to prove for each \isacommand{recdef} equation that the property |
30 requires you to prove for each \isacommand{recdef} equation that the property |
18 you are trying to establish holds for the left-hand side provided it holds |
31 you are trying to establish holds for the left-hand side provided it holds |
19 for all recursive calls on the right-hand side. Here is a simple example |
32 for all recursive calls on the right-hand side. Here is a simple example |
20 involving the predefined \isa{map} functional on lists:% |
33 involving the predefined \isa{map} functional on lists:% |
21 \end{isamarkuptext}% |
34 \end{isamarkuptext}% |
|
35 \isamarkupfalse% |
|
36 \isacommand{lemma}\ {\isachardoublequote}map\ f\ {\isacharparenleft}sep{\isacharparenleft}x{\isacharcomma}xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep{\isacharparenleft}f\ x{\isacharcomma}\ map\ f\ xs{\isacharparenright}{\isachardoublequote}% |
|
37 \isadelimproof |
|
38 % |
|
39 \endisadelimproof |
|
40 % |
|
41 \isatagproof |
22 \isamarkuptrue% |
42 \isamarkuptrue% |
23 \isacommand{lemma}\ {\isachardoublequote}map\ f\ {\isacharparenleft}sep{\isacharparenleft}x{\isacharcomma}xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep{\isacharparenleft}f\ x{\isacharcomma}\ map\ f\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
24 % |
43 % |
25 \begin{isamarkuptxt}% |
44 \begin{isamarkuptxt}% |
26 \noindent |
45 \noindent |
27 Note that \isa{map\ f\ xs} |
46 Note that \isa{map\ f\ xs} |
28 is the result of applying \isa{f} to all elements of \isa{xs}. We prove |
47 is the result of applying \isa{f} to all elements of \isa{xs}. We prove |
29 this lemma by recursion induction over \isa{sep}:% |
48 this lemma by recursion induction over \isa{sep}:% |
30 \end{isamarkuptxt}% |
49 \end{isamarkuptxt}% |
31 \isamarkuptrue% |
50 \isamarkupfalse% |
32 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}\isamarkupfalse% |
51 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}\isamarkuptrue% |
33 % |
52 % |
34 \begin{isamarkuptxt}% |
53 \begin{isamarkuptxt}% |
35 \noindent |
54 \noindent |
36 The resulting proof state has three subgoals corresponding to the three |
55 The resulting proof state has three subgoals corresponding to the three |
37 clauses for \isa{sep}: |
56 clauses for \isa{sep}: |
42 \isaindent{\ {\isadigit{3}}{\isachardot}\ \ \ \ }map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline |
61 \isaindent{\ {\isadigit{3}}{\isachardot}\ \ \ \ }map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline |
43 \isaindent{\ {\isadigit{3}}{\isachardot}\ \ \ \ }map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}% |
62 \isaindent{\ {\isadigit{3}}{\isachardot}\ \ \ \ }map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}% |
44 \end{isabelle} |
63 \end{isabelle} |
45 The rest is pure simplification:% |
64 The rest is pure simplification:% |
46 \end{isamarkuptxt}% |
65 \end{isamarkuptxt}% |
47 \isamarkuptrue% |
66 \isamarkupfalse% |
48 \isacommand{apply}\ simp{\isacharunderscore}all\isanewline |
67 \isacommand{apply}\ simp{\isacharunderscore}all\isanewline |
49 \isamarkupfalse% |
68 \isamarkupfalse% |
50 \isacommand{done}\isamarkupfalse% |
69 \isacommand{done}% |
|
70 \endisatagproof |
|
71 {\isafoldproof}% |
|
72 % |
|
73 \isadelimproof |
|
74 % |
|
75 \endisadelimproof |
|
76 \isamarkuptrue% |
51 % |
77 % |
52 \begin{isamarkuptext}% |
78 \begin{isamarkuptext}% |
53 Try proving the above lemma by structural induction, and you find that you |
79 Try proving the above lemma by structural induction, and you find that you |
54 need an additional case distinction. What is worse, the names of variables |
80 need an additional case distinction. What is worse, the names of variables |
55 are invented by Isabelle and have nothing to do with the names in the |
81 are invented by Isabelle and have nothing to do with the names in the |
73 \isa{v} you need to prove it for the three cases where \isa{v} is the |
99 \isa{v} you need to prove it for the three cases where \isa{v} is the |
74 empty list, the singleton list, and the list with at least two elements. |
100 empty list, the singleton list, and the list with at least two elements. |
75 The final case has an induction hypothesis: you may assume that \isa{P} |
101 The final case has an induction hypothesis: you may assume that \isa{P} |
76 holds for the tail of that list.% |
102 holds for the tail of that list.% |
77 \end{isamarkuptext}% |
103 \end{isamarkuptext}% |
78 \isamarkuptrue% |
104 % |
79 \isamarkupfalse% |
105 \isadelimtheory |
|
106 % |
|
107 \endisadelimtheory |
|
108 % |
|
109 \isatagtheory |
|
110 % |
|
111 \endisatagtheory |
|
112 {\isafoldtheory}% |
|
113 % |
|
114 \isadelimtheory |
|
115 % |
|
116 \endisadelimtheory |
80 \end{isabellebody}% |
117 \end{isabellebody}% |
81 %%% Local Variables: |
118 %%% Local Variables: |
82 %%% mode: latex |
119 %%% mode: latex |
83 %%% TeX-master: "root" |
120 %%% TeX-master: "root" |
84 %%% End: |
121 %%% End: |