Quelle Nested2.thy

Sprache: Isabelle

(*<*)
theory Nested2 imports Nested0 begin
(*>*)

lemma [simp]: "t ∈ set ts ⟶ size t < Suc(size_term_list ts)"
by(induct_tac ts, auto)
(*<*)
recdef trev "measure size"
"trev (Var x) = Var x"
"trev (App f ts) = App f (rev(map trev ts))"
(*>*)
text‹\noindent
making this theorem a simplification rule, \isacommand{recdef}
it automatically and the definition of @{term"trev"}
now. As a reward for our effort, we can now prove the desired
directly. We no longer need the verbose
schema for type ‹term› and can use the simpler one arising from
{term"trev"}:
›

lemma "trev(trev t) = t"
apply(induct_tac t rule: trev.induct)
txt‹
{subgoals[display,indent=0]}
the base case and the induction step fall to simplification:
›

by(simp_all add: rev_map sym[OF map_compose] cong: map_cong)

text‹\noindent
the proof of the induction step mystifies you, we recommend that you go through
chain of simplification steps in detail; you will probably need the help of
‹simp_trace›. Theorem @{thm[source]map_cong} is discussed below.
\begin{quote}
{term[display]"trev(trev(App f ts))"}\\
{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
{term[display]"App f (map trev (rev(rev(map trev ts))))"}\\
{term[display]"App f (map trev (map trev ts))"}\\
{term[display]"App f (map (trev o trev) ts)"}\\
{term[display]"App f (map (%x. x) ts)"}\\
{term[display]"App f ts"}
\end{quote}

definition of @{term"trev"} above is superior to the one in
S\ref{sec:nested-datatype} because it uses @{term"rev"}
lets us use existing facts such as \hbox{@{prop"rev(rev xs) = xs"}}.
this proof is a good example of an important principle:
begin{quote}
emph{Chose your definitions carefully\\
they determine the complexity of your proofs.}
end{quote}

us now return to the question of how \isacommand{recdef} can come up with
termination conditions in the presence of higher-order functions
@{term"map"}. For a start, if nothing were known about @{term"map"}, then
{term"map trev ts"} might apply @{term"trev"} to arbitrary terms, and thus
isacommand{recdef} would try to prove the unprovable @{term"size t < Suc
size_term_list ts)"}, without any assumption about @{term"t"}. Therefore
isacommand{recdef} has been supplied with the congruence theorem
{thm[source]map_cong}:
{thm[display,margin=50]"map_cong"[no_vars]}
second premise expresses that in @{term"map f xs"},
@{term"f"} is only applied to elements of list @{term"xs"}. Congruence
for other higher-order functions on lists are similar. If you get
a situation where you need to supply \isacommand{recdef} with new
rules, you can append a hint after the end of
recursion equations:\cmmdx{hints}
›
(*<*)
consts dummy :: "nat => nat"
recdef dummy "{}"
"dummy n = n"
(*>*)
(hints recdef_cong: map_cong)

text‹\noindent
you can declare them globally
giving them the \attrdx{recdef_cong} attribute:
›

declare map_cong[recdef_cong]

text‹
‹cong› and ‹recdef_cong› attributes are
kept apart because they control different activities, namely
and making recursive definitions.
The simplifier's congruence rules cannot be used by recdef.
For example the weak congruence rules for if and case would prevent
recdef from generating sensible termination conditions.
›
(*<*)end(*>*)

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet am 2026-06-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.