# HG changeset patch
# User krauss
# Date 1194269201 -3600
# Node ID 3026df96941d25f26b3e3e95016e7a7a24c5910d
# Parent  95128fcdd7e855f529346c457bbf72042ae74d24
changed "treemap" example to "mirror"

diff -r 95128fcdd7e8 -r 3026df96941d doc-src/IsarAdvanced/Functions/Thy/Functions.thy
--- 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
diff -r 95128fcdd7e8 -r 3026df96941d doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex
--- 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
 %
 \isadelimproof
 %
@@ -1834,17 +1834,17 @@
 
   \begin{isabelle}%
 \ {\isadigit{1}}{\isachardot}\ wf\ {\isacharquery}R\isanewline
-\ {\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 @@
 %
 \endisadelimproof
 \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
 %
 \isadelimproof
-\ \ \ \ %
+%
 \endisadelimproof
 %
 \isatagproof
@@ -1897,11 +1898,11 @@
 Now the whole termination proof is automatic:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\ \ \isacommand{termination}\isamarkupfalse%
+\isacommand{termination}\isamarkupfalse%
 \ \isanewline
 %
 \isadelimproof
-\ \ \ \ %
+\ \ %
 \endisadelimproof
 %
 \isatagproof