author krauss Mon, 05 Nov 2007 14:26:41 +0100 changeset 25278 3026df96941d parent 25277 95128fcdd7e8 child 25279 5ff6fc338db1
changed "treemap" example to "mirror"
--- a/doc-src/IsarAdvanced/Functions/Thy/Functions.thy	Mon Nov 05 08:31:12 2007 +0100
+++ b/doc-src/IsarAdvanced/Functions/Thy/Functions.thy	Mon Nov 05 14:26:41 2007 +0100
@@ -27,7 +27,7 @@
and a set of defining recursive equations.
If we leave out the type, the most general type will be
inferred, which can sometimes lead to surprises: Since both @{term
-  "1::nat"} and @{text plus} are overloaded, we would end up
+  "1::nat"} and @{text "+"} are overloaded, we would end up
with @{text "fib :: nat \<Rightarrow> 'a::{one,plus}"}.
*}

@@ -1149,13 +1149,13 @@
| Branch "'a tree list"

-text {* \noindent We can define a map function for trees, using the predefined
-  map function for lists. *}
+text {* \noindent We can define a function which swaps the left and right subtrees recursively, using the
+  list functions @{const rev} and @{const map}: *}

-function treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
+function mirror :: "'a tree \<Rightarrow> 'a tree"
where
-  "treemap f (Leaf n) = Leaf (f n)"
-| "treemap f (Branch l) = Branch (map (treemap f) l)"
+  "mirror (Leaf n) = Leaf n"
+| "mirror (Branch l) = Branch (rev (map mirror l))"
by pat_completeness auto

text {*
@@ -1174,16 +1174,16 @@
@{subgoals[display,indent=0]}

So Isabelle seems to know that @{const map} behaves nicely and only
-  applies the recursive call @{term "treemap f"} to elements
+  applies the recursive call @{term "mirror"} to elements
of @{term "l"}. Before we discuss where this knowledge comes from,
let us finish the termination proof:
*}

-  show "wf (measure (size o snd))" by simp
+  show "wf (measure size)" by simp
next
fix f l and x :: "'a tree"
assume "x \<in> set l"
-  thus "((f, x), (f, Branch l)) \<in> measure (size o snd)"
+  thus "(x, Branch l) \<in> measure size"
apply simp
txt {*
Simplification returns the following subgoal:
@@ -1197,17 +1197,27 @@
*}
(*<*)oops(*>*)

-  lemma tree_list_size[simp]: "x \<in> set l \<Longrightarrow> size x < Suc (tree_list_size l)"
-    by (induct l) auto
+lemma tree_list_size[simp]:
+  "x \<in> set l \<Longrightarrow> size x < Suc (tree_list_size l)"
+by (induct l) auto

-  text {*
+text {*
Now the whole termination proof is automatic:
-    *}
+  *}
+
+termination
+  by lexicographic_order

-  termination
-    by lexicographic_order
-
-
+(*
+lemma "mirror (mirror t) = t"
+proof (induct t rule:mirror.induct)
+  case 1 show ?case by simp
+next
+  case (2 l)
+  thus "mirror (mirror (Branch l)) = Branch l"
+    by (induct l) (auto simp: rev_map)
+qed
+*)
subsection {* Congruence Rules *}

text {*
@@ -1302,36 +1312,4 @@
works well.
*}

-(*
-text {*
-Since the structure of
-  congruence rules is a little unintuitive, here are some exercises:
-*}
-
-fun mapeven :: "(nat \<Rightarrow> nat) \<Rightarrow> nat list \<Rightarrow> nat list"
-where
-  "mapeven f [] = []"
-| "mapeven f (x#xs) = (if x mod 2 = 0 then f x # mapeven f xs else x #
-  mapeven f xs)"
-
-
-text {*
-
-  \begin{exercise}
-    Find a suitable congruence rule for the following function which
-  maps only over the even numbers in a list:
-
-  @{thm[display] mapeven.simps}
-  \end{exercise}
-
-  \begin{exercise}
-  Try what happens if the congruence rule for @{const If} is
-  disabled by declaring @{text "if_cong[fundef_cong del]"}?
-  \end{exercise}
-
-  Note that in some cases there is no \qt{best} congruence rule.
-  \fixme{}
-
-*}
-*)
end
--- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Mon Nov 05 08:31:12 2007 +0100
+++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Mon Nov 05 14:26:41 2007 +0100
@@ -39,7 +39,7 @@
giving its name, its type,
and a set of defining recursive equations.
If we leave out the type, the most general type will be
-  inferred, which can sometimes lead to surprises: Since both \isa{{\isadigit{1}}} and \isa{plus} are overloaded, we would end up
+  inferred, which can sometimes lead to surprises: Since both \isa{{\isadigit{1}}} and \isa{{\isacharplus}} are overloaded, we would end up
with \isa{fib\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ {\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}one{\isacharcomma}plus{\isacharbraceright}}.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -1788,15 +1788,15 @@
\ \ Leaf\ {\isacharprime}a\ \isanewline
{\isacharbar}\ Branch\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ list{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-\noindent We can define a map function for trees, using the predefined
-  map function for lists.%
+\noindent We can define a function which swaps the left and right subtrees recursively, using the
+  list functions \isa{rev} and \isa{map}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{function}\isamarkupfalse%
-\ treemap\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ tree{\isachardoublequoteclose}\isanewline
+\ mirror\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ tree{\isachardoublequoteclose}\isanewline
\isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}treemap\ f\ {\isacharparenleft}Leaf\ n{\isacharparenright}\ {\isacharequal}\ Leaf\ {\isacharparenleft}f\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
-{\isacharbar}\ {\isachardoublequoteopen}treemap\ f\ {\isacharparenleft}Branch\ l{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}map\ {\isacharparenleft}treemap\ f{\isacharparenright}\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Leaf\ n{\isacharparenright}\ {\isacharequal}\ Leaf\ n{\isachardoublequoteclose}\isanewline
+{\isacharbar}\ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Branch\ l{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}rev\ {\isacharparenleft}map\ mirror\ l{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
%
@@ -1834,17 +1834,17 @@

\begin{isabelle}%
-\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}f\ l\ x{\isachardot}\ x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}{\isacharcomma}\ f{\isacharcomma}\ Branch\ l{\isacharparenright}\ {\isasymin}\ {\isacharquery}R%
+\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}l\ x{\isachardot}\ x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ Branch\ l{\isacharparenright}\ {\isasymin}\ {\isacharquery}R%
\end{isabelle}

So Isabelle seems to know that \isa{map} behaves nicely and only
-  applies the recursive call \isa{treemap\ f} to elements
+  applies the recursive call \isa{mirror} to elements
of \isa{l}. Before we discuss where this knowledge comes from,
let us finish the termination proof:%
\end{isamarkuptxt}%
\isamarkuptrue%
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}wf\ {\isacharparenleft}measure\ {\isacharparenleft}size\ o\ snd{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isachardoublequoteopen}wf\ {\isacharparenleft}measure\ size{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
@@ -1853,7 +1853,7 @@
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ l{\isachardoublequoteclose}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}f{\isacharcomma}\ Branch\ l{\isacharparenright}{\isacharparenright}\ {\isasymin}\ measure\ {\isacharparenleft}size\ o\ snd{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}\ Branch\ l{\isacharparenright}\ {\isasymin}\ measure\ size{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ simp%
\begin{isamarkuptxt}%
@@ -1876,11 +1876,12 @@
%
\isanewline
-\ \ \isacommand{lemma}\isamarkupfalse%
-\ tree{\isacharunderscore}list{\isacharunderscore}size{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ size\ x\ {\isacharless}\ Suc\ {\isacharparenleft}tree{\isacharunderscore}list{\isacharunderscore}size\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ tree{\isacharunderscore}list{\isacharunderscore}size{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ \isanewline
+\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ size\ x\ {\isacharless}\ Suc\ {\isacharparenleft}tree{\isacharunderscore}list{\isacharunderscore}size\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
-\ \ \ \ %
+%
%
\isatagproof
@@ -1897,11 +1898,11 @@
Now the whole termination proof is automatic:%
\end{isamarkuptext}%
\isamarkuptrue%
-\ \ \isacommand{termination}\isamarkupfalse%
+\isacommand{termination}\isamarkupfalse%
\ \isanewline
%
\isatagproof