96 \isacommand{consts}\ find\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymtimes}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline |
96 \isacommand{consts}\ find\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymtimes}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline |
97 \isacommand{recdef}\ find\ {\isachardoublequote}same{\isacharunderscore}fst\ {\isacharparenleft}{\isasymlambda}f{\isachardot}\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}{\isacharparenright}\ step{\isadigit{1}}{\isachardoublequote}\isanewline |
97 \isacommand{recdef}\ find\ {\isachardoublequote}same{\isacharunderscore}fst\ {\isacharparenleft}{\isasymlambda}f{\isachardot}\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}{\isacharparenright}\ step{\isadigit{1}}{\isachardoublequote}\isanewline |
98 \ \ {\isachardoublequote}find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\isanewline |
98 \ \ {\isachardoublequote}find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\isanewline |
99 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ then\ if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find{\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}\isanewline |
99 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ then\ if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find{\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}\isanewline |
100 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ arbitrary{\isacharparenright}{\isachardoublequote}\isanewline |
100 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ arbitrary{\isacharparenright}{\isachardoublequote}\isanewline |
101 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}same{\isacharunderscore}fst{\isacharunderscore}def\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}% |
101 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}% |
102 \begin{isamarkuptext}% |
102 \begin{isamarkuptext}% |
103 \noindent |
103 \noindent |
104 The recursion equation itself should be clear enough: it is our aborted |
104 The recursion equation itself should be clear enough: it is our aborted |
105 first attempt augmented with a check that there are no non-trivial loops. |
105 first attempt augmented with a check that there are no non-trivial loops. |
106 To express the required well-founded relation we employ the |
106 To express the required well-founded relation we employ the |
121 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ P\ x\ {\isasymLongrightarrow}\ wf\ {\isacharparenleft}R\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ wf\ {\isacharparenleft}same{\isacharunderscore}fst\ P\ R{\isacharparenright}% |
121 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ P\ x\ {\isasymLongrightarrow}\ wf\ {\isacharparenleft}R\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ wf\ {\isacharparenleft}same{\isacharunderscore}fst\ P\ R{\isacharparenright}% |
122 \end{isabelle} |
122 \end{isabelle} |
123 is known to the well-foundedness prover of \isacommand{recdef}. Thus |
123 is known to the well-foundedness prover of \isacommand{recdef}. Thus |
124 well-foundedness of the relation given to \isacommand{recdef} is immediate. |
124 well-foundedness of the relation given to \isacommand{recdef} is immediate. |
125 Furthermore, each recursive call descends along that relation: the first |
125 Furthermore, each recursive call descends along that relation: the first |
126 argument stays unchanged and the second one descends along \isa{step{\isadigit{1}}\ f}. The proof merely requires unfolding of some definitions, as specified in |
126 argument stays unchanged and the second one descends along \isa{step{\isadigit{1}}\ f}. The proof requires unfolding the definition of \isa{step{\isadigit{1}}}, |
127 the \isacommand{hints} above. |
127 as specified in the \isacommand{hints} above. |
128 |
128 |
129 Normally you will then derive the following conditional variant of and from |
129 Normally you will then derive the following conditional variant of and from |
130 the recursion equation% |
130 the recursion equation% |
131 \end{isamarkuptext}% |
131 \end{isamarkuptext}% |
132 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline |
132 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline |