15 succeeds now. As a reward for our effort, we can now prove the desired |
15 succeeds now. As a reward for our effort, we can now prove the desired |
16 lemma directly. The key is the fact that we no longer need the verbose |
16 lemma directly. The key is the fact that we no longer need the verbose |
17 induction schema for type \isa{term} but the simpler one arising from |
17 induction schema for type \isa{term} but the simpler one arising from |
18 \isa{trev}:% |
18 \isa{trev}:% |
19 \end{isamarkuptext}% |
19 \end{isamarkuptext}% |
20 \isacommand{lemmas}\ {\isacharbrackleft}cong{\isacharbrackright}\ {\isacharequal}\ map{\isacharunderscore}cong\isanewline |
|
21 \isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline |
20 \isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline |
22 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}trev{\isachardot}induct{\isacharparenright}% |
21 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}trev{\isachardot}induct{\isacharparenright}% |
23 \begin{isamarkuptxt}% |
22 \begin{isamarkuptxt}% |
24 \noindent |
23 \noindent |
25 This leaves us with a trivial base case \isa{trev\ {\isacharparenleft}trev\ {\isacharparenleft}Var\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Var\ x} and the step case |
24 This leaves us with a trivial base case \isa{trev\ {\isacharparenleft}trev\ {\isacharparenleft}Var\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Var\ x} and the step case |
27 \ \ \ \ \ {\isasymforall}t{\isachardot}\ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t\ {\isasymLongrightarrow}\isanewline |
26 \ \ \ \ \ {\isasymforall}t{\isachardot}\ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t\ {\isasymLongrightarrow}\isanewline |
28 \ \ \ \ \ trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ f\ ts% |
27 \ \ \ \ \ trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ f\ ts% |
29 \end{isabelle} |
28 \end{isabelle} |
30 both of which are solved by simplification:% |
29 both of which are solved by simplification:% |
31 \end{isamarkuptxt}% |
30 \end{isamarkuptxt}% |
32 \isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}{\isacharparenright}% |
31 \isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ cong{\isacharcolon}map{\isacharunderscore}cong{\isacharparenright}% |
33 \begin{isamarkuptext}% |
32 \begin{isamarkuptext}% |
34 \noindent |
33 \noindent |
35 If the proof of the induction step mystifies you, we recommend to go through |
34 If the proof of the induction step mystifies you, we recommend to go through |
36 the chain of simplification steps in detail; you will probably need the help of |
35 the chain of simplification steps in detail; you will probably need the help of |
37 \isa{trace{\isacharunderscore}simp}. |
36 \isa{trace{\isacharunderscore}simp}. Theorem \isa{map{\isacharunderscore}cong} is discussed below. |
38 %\begin{quote} |
37 %\begin{quote} |
39 %{term[display]"trev(trev(App f ts))"}\\ |
38 %{term[display]"trev(trev(App f ts))"}\\ |
40 %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\ |
39 %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\ |
41 %{term[display]"App f (map trev (rev(rev(map trev ts))))"}\\ |
40 %{term[display]"App f (map trev (rev(rev(map trev ts))))"}\\ |
42 %{term[display]"App f (map trev (map trev ts))"}\\ |
41 %{term[display]"App f (map trev (map trev ts))"}\\ |
80 \end{ttbox} |
79 \end{ttbox} |
81 |
80 |
82 Note that \isacommand{recdef} feeds on exactly the same \emph{kind} of |
81 Note that \isacommand{recdef} feeds on exactly the same \emph{kind} of |
83 congruence rules as the simplifier (\S\ref{sec:simp-cong}) but that |
82 congruence rules as the simplifier (\S\ref{sec:simp-cong}) but that |
84 declaring a congruence rule for the simplifier does not make it |
83 declaring a congruence rule for the simplifier does not make it |
85 available to \isacommand{recdef}, and vice versa. This is intentional.% |
84 available to \isacommand{recdef}, and vice versa. This is intentional. |
|
85 %The simplifier's congruence rules cannot be used by recdef. |
|
86 %For example the weak congruence rules for if and case would prevent |
|
87 %recdef from generating sensible termination conditions.% |
86 \end{isamarkuptext}% |
88 \end{isamarkuptext}% |
87 \end{isabellebody}% |
89 \end{isabellebody}% |
88 %%% Local Variables: |
90 %%% Local Variables: |
89 %%% mode: latex |
91 %%% mode: latex |
90 %%% TeX-master: "root" |
92 %%% TeX-master: "root" |