19 for all recursive calls on the right-hand side. Here is a simple example |
19 for all recursive calls on the right-hand side. Here is a simple example |
20 involving the predefined \isa{map} functional on lists:% |
20 involving the predefined \isa{map} functional on lists:% |
21 \end{isamarkuptext}% |
21 \end{isamarkuptext}% |
22 \isamarkuptrue% |
22 \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% |
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 % |
|
25 \begin{isamarkuptxt}% |
|
26 \noindent |
|
27 Note that \isa{map\ f\ xs} |
|
28 is the result of applying \isa{f} to all elements of \isa{xs}. We prove |
|
29 this lemma by recursion induction over \isa{sep}:% |
|
30 \end{isamarkuptxt}% |
|
31 \isamarkuptrue% |
24 \isamarkuptrue% |
32 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}\isamarkupfalse% |
25 \isamarkupfalse% |
33 % |
|
34 \begin{isamarkuptxt}% |
|
35 \noindent |
|
36 The resulting proof state has three subgoals corresponding to the three |
|
37 clauses for \isa{sep}: |
|
38 \begin{isabelle}% |
|
39 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a{\isachardot}\ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline |
|
40 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ x{\isachardot}\ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\isanewline |
|
41 \ {\isadigit{3}}{\isachardot}\ {\isasymAnd}a\ x\ y\ zs{\isachardot}\isanewline |
|
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 |
|
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}% |
|
44 \end{isabelle} |
|
45 The rest is pure simplification:% |
|
46 \end{isamarkuptxt}% |
|
47 \isamarkuptrue% |
26 \isamarkuptrue% |
48 \isacommand{apply}\ simp{\isacharunderscore}all\isanewline |
|
49 \isamarkupfalse% |
27 \isamarkupfalse% |
50 \isacommand{done}\isamarkupfalse% |
28 \isamarkupfalse% |
51 % |
29 % |
52 \begin{isamarkuptext}% |
30 \begin{isamarkuptext}% |
53 Try proving the above lemma by structural induction, and you find that you |
31 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 |
32 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 |
33 are invented by Isabelle and have nothing to do with the names in the |