src/Doc/Datatypes/Datatypes.thy
changeset 62336 4a8d2f0d7fdd
parent 62333 e4e09a6e3922
child 62384 54512bd12a5e
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Wed Feb 17 16:26:50 2016 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Wed Feb 17 17:21:43 2016 +0100
     1.3 @@ -1429,16 +1429,7 @@
     1.4  
     1.5  text \<open>
     1.6  \noindent
     1.7 -For convenience, the predicator can be used instead of the map function,
     1.8 -typically when defining predicates. For example:
     1.9 -\<close>
    1.10 -
    1.11 -primrec increasing_tree :: "int \<Rightarrow> int tree\<^sub>f\<^sub>f \<Rightarrow> bool" where
    1.12 -  "increasing_tree m (Node\<^sub>f\<^sub>f n ts) \<longleftrightarrow> n \<ge> m \<and> list_all (increasing_tree (n + 1)) ts"
    1.13 -
    1.14 -text \<open>
    1.15 -\noindent
    1.16 -Also for convenience, recursion through functions can also be expressed using
    1.17 +For convenience, recursion through functions can also be expressed using
    1.18  $\lambda$-abstractions and function application rather than through composition.
    1.19  For example:
    1.20  \<close>
    1.21 @@ -1478,6 +1469,14 @@
    1.22      primrec (nonexhaustive) subtree_ft2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
    1.23        "subtree_ft2 x y (FTNode2 g) = g x y"
    1.24  
    1.25 +text \<open>
    1.26 +For any datatype featuring nesting, the predicator can be used instead of the
    1.27 +map function, typically when defining predicates. For example:
    1.28 +\<close>
    1.29 +
    1.30 +    primrec increasing_tree :: "int \<Rightarrow> int tree\<^sub>f\<^sub>f \<Rightarrow> bool" where
    1.31 +      "increasing_tree m (Node\<^sub>f\<^sub>f n ts) \<longleftrightarrow> n \<ge> m \<and> list_all (increasing_tree (n + 1)) ts"
    1.32 +
    1.33  
    1.34  subsubsection \<open> Nested-as-Mutual Recursion
    1.35    \label{sssec:primrec-nested-as-mutual-recursion} \<close>