clarified current 'primrec' vs. old 'recdef';
updated examples from src/HOL/Induct;
1.1 --- a/doc-src/HOL/HOL.tex Thu May 26 14:24:26 2011 +0200
1.2 +++ b/doc-src/HOL/HOL.tex Thu May 26 15:56:39 2011 +0200
1.3 @@ -1589,7 +1589,7 @@
1.4 \texttt{split_if} (see~{\S}\ref{subsec:HOL:case:splitting}).
1.5
1.6 \texttt{List} provides a basic library of list processing functions defined by
1.7 -primitive recursion (see~{\S}\ref{sec:HOL:primrec}). The recursion equations
1.8 +primitive recursion. The recursion equations
1.9 are shown in Figs.\ts\ref{fig:HOL:list-simps} and~\ref{fig:HOL:list-simps2}.
1.10
1.11 \index{list@{\textit{list}} type|)}
1.12 @@ -1938,229 +1938,21 @@
1.13 and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$.
1.14
1.15
1.16 -\section{Recursive function definitions}\label{sec:HOL:recursive}
1.17 -\index{recursive functions|see{recursion}}
1.18 -
1.19 -Isabelle/HOL provides two main mechanisms of defining recursive functions.
1.20 -\begin{enumerate}
1.21 -\item \textbf{Primitive recursion} is available only for datatypes, and it is
1.22 - somewhat restrictive. Recursive calls are only allowed on the argument's
1.23 - immediate constituents. On the other hand, it is the form of recursion most
1.24 - often wanted, and it is easy to use.
1.25 -
1.26 -\item \textbf{Well-founded recursion} requires that you supply a well-founded
1.27 - relation that governs the recursion. Recursive calls are only allowed if
1.28 - they make the argument decrease under the relation. Complicated recursion
1.29 - forms, such as nested recursion, can be dealt with. Termination can even be
1.30 - proved at a later time, though having unsolved termination conditions around
1.31 - can make work difficult.%
1.32 - \footnote{This facility is based on Konrad Slind's TFL
1.33 - package~\cite{slind-tfl}. Thanks are due to Konrad for implementing TFL
1.34 - and assisting with its installation.}
1.35 -\end{enumerate}
1.36 -
1.37 -Following good HOL tradition, these declarations do not assert arbitrary
1.38 -axioms. Instead, they define the function using a recursion operator. Both
1.39 -HOL and ZF derive the theory of well-founded recursion from first
1.40 -principles~\cite{paulson-set-II}. Primitive recursion over some datatype
1.41 -relies on the recursion operator provided by the datatype package. With
1.42 -either form of function definition, Isabelle proves the desired recursion
1.43 -equations as theorems.
1.44 -
1.45 -
1.46 -\subsection{Primitive recursive functions}
1.47 -\label{sec:HOL:primrec}
1.48 -\index{recursion!primitive|(}
1.49 -\index{*primrec|(}
1.50 -
1.51 -Datatypes come with a uniform way of defining functions, {\bf primitive
1.52 - recursion}. In principle, one could introduce primitive recursive functions
1.53 -by asserting their reduction rules as new axioms, but this is not recommended:
1.54 -\begin{ttbox}\slshape
1.55 -Append = Main +
1.56 -consts app :: ['a list, 'a list] => 'a list
1.57 -rules
1.58 - app_Nil "app [] ys = ys"
1.59 - app_Cons "app (x#xs) ys = x#app xs ys"
1.60 -end
1.61 -\end{ttbox}
1.62 -Asserting axioms brings the danger of accidentally asserting nonsense, as
1.63 -in \verb$app [] ys = us$.
1.64 -
1.65 -The \ttindex{primrec} declaration is a safe means of defining primitive
1.66 -recursive functions on datatypes:
1.67 -\begin{ttbox}
1.68 -Append = Main +
1.69 -consts app :: ['a list, 'a list] => 'a list
1.70 -primrec
1.71 - "app [] ys = ys"
1.72 - "app (x#xs) ys = x#app xs ys"
1.73 -end
1.74 -\end{ttbox}
1.75 -Isabelle will now check that the two rules do indeed form a primitive
1.76 -recursive definition. For example
1.77 -\begin{ttbox}
1.78 -primrec
1.79 - "app [] ys = us"
1.80 -\end{ttbox}
1.81 -is rejected with an error message ``\texttt{Extra variables on rhs}''.
1.82 -
1.83 -\bigskip
1.84 -
1.85 -The general form of a primitive recursive definition is
1.86 -\begin{ttbox}
1.87 -primrec
1.88 - {\it reduction rules}
1.89 -\end{ttbox}
1.90 -where \textit{reduction rules} specify one or more equations of the form
1.91 -\[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \,
1.92 -\dots \, z@n = r \] such that $C$ is a constructor of the datatype, $r$
1.93 -contains only the free variables on the left-hand side, and all recursive
1.94 -calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. There
1.95 -must be at most one reduction rule for each constructor. The order is
1.96 -immaterial. For missing constructors, the function is defined to return a
1.97 -default value.
1.98 -
1.99 -If you would like to refer to some rule by name, then you must prefix
1.100 -the rule with an identifier. These identifiers, like those in the
1.101 -\texttt{rules} section of a theory, will be visible at the \ML\ level.
1.102 -
1.103 -The primitive recursive function can have infix or mixfix syntax:
1.104 -\begin{ttbox}\underscoreon
1.105 -consts "@" :: ['a list, 'a list] => 'a list (infixr 60)
1.106 -primrec
1.107 - "[] @ ys = ys"
1.108 - "(x#xs) @ ys = x#(xs @ ys)"
1.109 -\end{ttbox}
1.110 -
1.111 -The reduction rules become part of the default simpset, which
1.112 -leads to short proof scripts:
1.113 -\begin{ttbox}\underscoreon
1.114 -Goal "(xs @ ys) @ zs = xs @ (ys @ zs)";
1.115 -by (induct\_tac "xs" 1);
1.116 -by (ALLGOALS Asm\_simp\_tac);
1.117 -\end{ttbox}
1.118 -
1.119 -\subsubsection{Example: Evaluation of expressions}
1.120 -Using mutual primitive recursion, we can define evaluation functions \texttt{evala}
1.121 -and \texttt{eval_bexp} for the datatypes of arithmetic and boolean expressions mentioned in
1.122 -{\S}\ref{subsec:datatype:basics}:
1.123 -\begin{ttbox}
1.124 -consts
1.125 - evala :: "['a => nat, 'a aexp] => nat"
1.126 - evalb :: "['a => nat, 'a bexp] => bool"
1.127 -
1.128 -primrec
1.129 - "evala env (If_then_else b a1 a2) =
1.130 - (if evalb env b then evala env a1 else evala env a2)"
1.131 - "evala env (Sum a1 a2) = evala env a1 + evala env a2"
1.132 - "evala env (Diff a1 a2) = evala env a1 - evala env a2"
1.133 - "evala env (Var v) = env v"
1.134 - "evala env (Num n) = n"
1.135 -
1.136 - "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
1.137 - "evalb env (And b1 b2) = (evalb env b1 & evalb env b2)"
1.138 - "evalb env (Or b1 b2) = (evalb env b1 & evalb env b2)"
1.139 -\end{ttbox}
1.140 -Since the value of an expression depends on the value of its variables,
1.141 -the functions \texttt{evala} and \texttt{evalb} take an additional
1.142 -parameter, an {\em environment} of type \texttt{'a => nat}, which maps
1.143 -variables to their values.
1.144 -
1.145 -Similarly, we may define substitution functions \texttt{substa}
1.146 -and \texttt{substb} for expressions: The mapping \texttt{f} of type
1.147 -\texttt{'a => 'a aexp} given as a parameter is lifted canonically
1.148 -on the types \texttt{'a aexp} and \texttt{'a bexp}:
1.149 -\begin{ttbox}
1.150 -consts
1.151 - substa :: "['a => 'b aexp, 'a aexp] => 'b aexp"
1.152 - substb :: "['a => 'b aexp, 'a bexp] => 'b bexp"
1.153 -
1.154 -primrec
1.155 - "substa f (If_then_else b a1 a2) =
1.156 - If_then_else (substb f b) (substa f a1) (substa f a2)"
1.157 - "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
1.158 - "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
1.159 - "substa f (Var v) = f v"
1.160 - "substa f (Num n) = Num n"
1.161 -
1.162 - "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
1.163 - "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
1.164 - "substb f (Or b1 b2) = Or (substb f b1) (substb f b2)"
1.165 -\end{ttbox}
1.166 -In textbooks about semantics one often finds {\em substitution theorems},
1.167 -which express the relationship between substitution and evaluation. For
1.168 -\texttt{'a aexp} and \texttt{'a bexp}, we can prove such a theorem by mutual
1.169 -induction, followed by simplification:
1.170 -\begin{ttbox}
1.171 -Goal
1.172 - "evala env (substa (Var(v := a')) a) =
1.173 - evala (env(v := evala env a')) a &
1.174 - evalb env (substb (Var(v := a')) b) =
1.175 - evalb (env(v := evala env a')) b";
1.176 -by (induct_tac "a b" 1);
1.177 -by (ALLGOALS Asm_full_simp_tac);
1.178 -\end{ttbox}
1.179 -
1.180 -\subsubsection{Example: A substitution function for terms}
1.181 -Functions on datatypes with nested recursion, such as the type
1.182 -\texttt{term} mentioned in {\S}\ref{subsec:datatype:basics}, are
1.183 -also defined by mutual primitive recursion. A substitution
1.184 -function \texttt{subst_term} on type \texttt{term}, similar to the functions
1.185 -\texttt{substa} and \texttt{substb} described above, can
1.186 -be defined as follows:
1.187 -\begin{ttbox}
1.188 -consts
1.189 - subst_term :: "['a => ('a,'b) term, ('a,'b) term] => ('a,'b) term"
1.190 - subst_term_list ::
1.191 - "['a => ('a,'b) term, ('a,'b) term list] => ('a,'b) term list"
1.192 -
1.193 -primrec
1.194 - "subst_term f (Var a) = f a"
1.195 - "subst_term f (App b ts) = App b (subst_term_list f ts)"
1.196 -
1.197 - "subst_term_list f [] = []"
1.198 - "subst_term_list f (t # ts) =
1.199 - subst_term f t # subst_term_list f ts"
1.200 -\end{ttbox}
1.201 -The recursion scheme follows the structure of the unfolded definition of type
1.202 -\texttt{term} shown in {\S}\ref{subsec:datatype:basics}. To prove properties of
1.203 -this substitution function, mutual induction is needed:
1.204 -\begin{ttbox}
1.205 -Goal
1.206 - "(subst_term ((subst_term f1) o f2) t) =
1.207 - (subst_term f1 (subst_term f2 t)) &
1.208 - (subst_term_list ((subst_term f1) o f2) ts) =
1.209 - (subst_term_list f1 (subst_term_list f2 ts))";
1.210 -by (induct_tac "t ts" 1);
1.211 -by (ALLGOALS Asm_full_simp_tac);
1.212 -\end{ttbox}
1.213 -
1.214 -\subsubsection{Example: A map function for infinitely branching trees}
1.215 -Defining functions on infinitely branching datatypes by primitive
1.216 -recursion is just as easy. For example, we can define a function
1.217 -\texttt{map_tree} on \texttt{'a tree} as follows:
1.218 -\begin{ttbox}
1.219 -consts
1.220 - map_tree :: "('a => 'b) => 'a tree => 'b tree"
1.221 -
1.222 -primrec
1.223 - "map_tree f (Atom a) = Atom (f a)"
1.224 - "map_tree f (Branch ts) = Branch (\%x. map_tree f (ts x))"
1.225 -\end{ttbox}
1.226 -Note that all occurrences of functions such as \texttt{ts} in the
1.227 -\texttt{primrec} clauses must be applied to an argument. In particular,
1.228 -\texttt{map_tree f o ts} is not allowed.
1.229 -
1.230 -\index{recursion!primitive|)}
1.231 -\index{*primrec|)}
1.232 -
1.233 -
1.234 -\subsection{General recursive functions}
1.235 -\label{sec:HOL:recdef}
1.236 +\section{Old-style recursive function definitions}\label{sec:HOL:recursive}
1.237 \index{recursion!general|(}
1.238 \index{*recdef|(}
1.239
1.240 +Old-style recursive definitions via \texttt{recdef} requires that you
1.241 +supply a well-founded relation that governs the recursion. Recursive
1.242 +calls are only allowed if they make the argument decrease under the
1.243 +relation. Complicated recursion forms, such as nested recursion, can
1.244 +be dealt with. Termination can even be proved at a later time, though
1.245 +having unsolved termination conditions around can make work
1.246 +difficult.%
1.247 +\footnote{This facility is based on Konrad Slind's TFL
1.248 + package~\cite{slind-tfl}. Thanks are due to Konrad for implementing
1.249 + TFL and assisting with its installation.}
1.250 +
1.251 Using \texttt{recdef}, you can declare functions involving nested recursion
1.252 and pattern-matching. Recursion need not involve datatypes and there are few
1.253 syntactic restrictions. Termination is proved by showing that each recursive
2.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu May 26 14:24:26 2011 +0200
2.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu May 26 15:56:39 2011 +0200
2.3 @@ -171,7 +171,30 @@
2.4 \begin{description}
2.5
2.6 \item @{command (HOL) "primrec"} defines primitive recursive
2.7 - functions over datatypes, see also \cite{isabelle-HOL}.
2.8 + functions over datatypes (see also @{command_ref (HOL) datatype} and
2.9 + @{command_ref (HOL) rep_datatype}). The given @{text equations}
2.10 + specify reduction rules that are produced by instantiating the
2.11 + generic combinator for primitive recursion that is available for
2.12 + each datatype.
2.13 +
2.14 + Each equation needs to be of the form:
2.15 +
2.16 + @{text [display] "f x\<^sub>1 \<dots> x\<^sub>m (C y\<^sub>1 \<dots> y\<^sub>k) z\<^sub>1 \<dots> z\<^sub>n = rhs"}
2.17 +
2.18 + such that @{text C} is a datatype constructor, @{text rhs} contains
2.19 + only the free variables on the left-hand side (or from the context),
2.20 + and all recursive occurrences of @{text "f"} in @{text "rhs"} are of
2.21 + the form @{text "f \<dots> y\<^sub>i \<dots>"} for some @{text i}. At most one
2.22 + reduction rule for each constructor can be given. The order does
2.23 + not matter. For missing constructors, the function is defined to
2.24 + return a default value, but this equation is made difficult to
2.25 + access for users.
2.26 +
2.27 + The reduction rules are declared as @{attribute simp} by default,
2.28 + which enables standard proof methods like @{method simp} and
2.29 + @{method auto} to normalize expressions of @{text "f"} applied to
2.30 + datatype constructions, by simulating symbolic computation via
2.31 + rewriting.
2.32
2.33 \item @{command (HOL) "function"} defines functions by general
2.34 wellfounded recursion. A detailed description with examples can be
2.35 @@ -200,15 +223,12 @@
2.36 \end{description}
2.37
2.38 Recursive definitions introduced by the @{command (HOL) "function"}
2.39 - command accommodate
2.40 - reasoning by induction (cf.\ \secref{sec:cases-induct}): rule @{text
2.41 - "c.induct"} (where @{text c} is the name of the function definition)
2.42 - refers to a specific induction rule, with parameters named according
2.43 - to the user-specified equations. Cases are numbered (starting from 1).
2.44 -
2.45 - For @{command (HOL) "primrec"}, the induction principle coincides
2.46 - with structural recursion on the datatype the recursion is carried
2.47 - out.
2.48 + command accommodate reasoning by induction (cf.\ @{method induct}):
2.49 + rule @{text "f.induct"} refers to a specific induction rule, with
2.50 + parameters named according to the user-specified equations. Cases
2.51 + are numbered starting from 1. For @{command (HOL) "primrec"}, the
2.52 + induction principle coincides with structural recursion on the
2.53 + datatype where the recursion is carried out.
2.54
2.55 The equations provided by these packages may be referred later as
2.56 theorem list @{text "f.simps"}, where @{text f} is the (collective)
2.57 @@ -237,6 +257,129 @@
2.58 \end{description}
2.59 *}
2.60
2.61 +subsubsection {* Example: evaluation of expressions *}
2.62 +
2.63 +text {* Subsequently, we define mutual datatypes for arithmetic and
2.64 + boolean expressions, and use @{command primrec} for evaluation
2.65 + functions that follow the same recursive structure. *}
2.66 +
2.67 +datatype 'a aexp =
2.68 + IF "'a bexp" "'a aexp" "'a aexp"
2.69 + | Sum "'a aexp" "'a aexp"
2.70 + | Diff "'a aexp" "'a aexp"
2.71 + | Var 'a
2.72 + | Num nat
2.73 +and 'a bexp =
2.74 + Less "'a aexp" "'a aexp"
2.75 + | And "'a bexp" "'a bexp"
2.76 + | Neg "'a bexp"
2.77 +
2.78 +
2.79 +text {* \medskip Evaluation of arithmetic and boolean expressions *}
2.80 +
2.81 +primrec evala :: "('a \<Rightarrow> nat) \<Rightarrow> 'a aexp \<Rightarrow> nat"
2.82 + and evalb :: "('a \<Rightarrow> nat) \<Rightarrow> 'a bexp \<Rightarrow> bool"
2.83 +where
2.84 + "evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)"
2.85 +| "evala env (Sum a1 a2) = evala env a1 + evala env a2"
2.86 +| "evala env (Diff a1 a2) = evala env a1 - evala env a2"
2.87 +| "evala env (Var v) = env v"
2.88 +| "evala env (Num n) = n"
2.89 +| "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
2.90 +| "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"
2.91 +| "evalb env (Neg b) = (\<not> evalb env b)"
2.92 +
2.93 +text {* Since the value of an expression depends on the value of its
2.94 + variables, the functions @{const evala} and @{const evalb} take an
2.95 + additional parameter, an \emph{environment} that maps variables to
2.96 + their values.
2.97 +
2.98 + \medskip Substitution on expressions can be defined similarly. The
2.99 + mapping @{text f} of type @{typ "'a \<Rightarrow> 'a aexp"} given as a
2.100 + parameter is lifted canonically on the types @{typ "'a aexp"} and
2.101 + @{typ "'a bexp"}, respectively.
2.102 +*}
2.103 +
2.104 +primrec substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp"
2.105 + and substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp"
2.106 +where
2.107 + "substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)"
2.108 +| "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
2.109 +| "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
2.110 +| "substa f (Var v) = f v"
2.111 +| "substa f (Num n) = Num n"
2.112 +| "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
2.113 +| "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
2.114 +| "substb f (Neg b) = Neg (substb f b)"
2.115 +
2.116 +text {* In textbooks about semantics one often finds substitution
2.117 + theorems, which express the relationship between substitution and
2.118 + evaluation. For @{typ "'a aexp"} and @{typ "'a bexp"}, we can prove
2.119 + such a theorem by mutual induction, followed by simplification.
2.120 +*}
2.121 +
2.122 +lemma subst_one:
2.123 + "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a"
2.124 + "evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
2.125 + by (induct a and b) simp_all
2.126 +
2.127 +lemma subst_all:
2.128 + "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a"
2.129 + "evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
2.130 + by (induct a and b) simp_all
2.131 +
2.132 +
2.133 +subsubsection {* Example: a substitution function for terms *}
2.134 +
2.135 +text {* Functions on datatypes with nested recursion are also defined
2.136 + by mutual primitive recursion. *}
2.137 +
2.138 +datatype ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list"
2.139 +
2.140 +text {* A substitution function on type @{typ "('a, 'b) term"} can be
2.141 + defined as follows, by working simultaneously on @{typ "('a, 'b)
2.142 + term list"}: *}
2.143 +
2.144 +primrec subst_term :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term \<Rightarrow> ('a, 'b) term" and
2.145 + subst_term_list :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term list \<Rightarrow> ('a, 'b) term list"
2.146 +where
2.147 + "subst_term f (Var a) = f a"
2.148 +| "subst_term f (App b ts) = App b (subst_term_list f ts)"
2.149 +| "subst_term_list f [] = []"
2.150 +| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
2.151 +
2.152 +text {* The recursion scheme follows the structure of the unfolded
2.153 + definition of type @{typ "('a, 'b) term"}. To prove properties of this
2.154 + substitution function, mutual induction is needed:
2.155 +*}
2.156 +
2.157 +lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)" and
2.158 + "subst_term_list (subst_term f1 \<circ> f2) ts = subst_term_list f1 (subst_term_list f2 ts)"
2.159 + by (induct t and ts) simp_all
2.160 +
2.161 +
2.162 +subsubsection {* Example: a map function for infinitely branching trees *}
2.163 +
2.164 +text {* Defining functions on infinitely branching datatypes by
2.165 + primitive recursion is just as easy.
2.166 +*}
2.167 +
2.168 +datatype 'a tree = Atom 'a | Branch "nat \<Rightarrow> 'a tree"
2.169 +
2.170 +primrec map_tree :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a tree \<Rightarrow> 'b tree"
2.171 +where
2.172 + "map_tree f (Atom a) = Atom (f a)"
2.173 +| "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
2.174 +
2.175 +text {* Note that all occurrences of functions such as @{text ts}
2.176 + above must be applied to an argument. In particular, @{term
2.177 + "map_tree f \<circ> ts"} is not allowed here. *}
2.178 +
2.179 +text {* Here is a simple composition lemma for @{term map_tree}: *}
2.180 +
2.181 +lemma "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
2.182 + by (induct t) simp_all
2.183 +
2.184
2.185 subsection {* Proof methods related to recursive definitions *}
2.186
3.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 26 14:24:26 2011 +0200
3.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 26 15:56:39 2011 +0200
3.3 @@ -288,7 +288,32 @@
3.4 \begin{description}
3.5
3.6 \item \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} defines primitive recursive
3.7 - functions over datatypes, see also \cite{isabelle-HOL}.
3.8 + functions over datatypes (see also \indexref{HOL}{command}{datatype}\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} and
3.9 + \indexref{HOL}{command}{rep\_datatype}\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}). The given \isa{equations}
3.10 + specify reduction rules that are produced by instantiating the
3.11 + generic combinator for primitive recursion that is available for
3.12 + each datatype.
3.13 +
3.14 + Each equation needs to be of the form:
3.15 +
3.16 + \begin{isabelle}%
3.17 +{\isaliteral{22}{\isachardoublequote}}f\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{28}{\isacharparenleft}}C\ y\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ y\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{29}{\isacharparenright}}\ z\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ z\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3D}{\isacharequal}}\ rhs{\isaliteral{22}{\isachardoublequote}}%
3.18 +\end{isabelle}
3.19 +
3.20 + such that \isa{C} is a datatype constructor, \isa{rhs} contains
3.21 + only the free variables on the left-hand side (or from the context),
3.22 + and all recursive occurrences of \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}} in \isa{{\isaliteral{22}{\isachardoublequote}}rhs{\isaliteral{22}{\isachardoublequote}}} are of
3.23 + the form \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ y\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} for some \isa{i}. At most one
3.24 + reduction rule for each constructor can be given. The order does
3.25 + not matter. For missing constructors, the function is defined to
3.26 + return a default value, but this equation is made difficult to
3.27 + access for users.
3.28 +
3.29 + The reduction rules are declared as \hyperlink{attribute.simp}{\mbox{\isa{simp}}} by default,
3.30 + which enables standard proof methods like \hyperlink{method.simp}{\mbox{\isa{simp}}} and
3.31 + \hyperlink{method.auto}{\mbox{\isa{auto}}} to normalize expressions of \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}} applied to
3.32 + datatype constructions, by simulating symbolic computation via
3.33 + rewriting.
3.34
3.35 \item \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} defines functions by general
3.36 wellfounded recursion. A detailed description with examples can be
3.37 @@ -316,14 +341,12 @@
3.38 \end{description}
3.39
3.40 Recursive definitions introduced by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}
3.41 - command accommodate
3.42 - reasoning by induction (cf.\ \secref{sec:cases-induct}): rule \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{2E}{\isachardot}}induct{\isaliteral{22}{\isachardoublequote}}} (where \isa{c} is the name of the function definition)
3.43 - refers to a specific induction rule, with parameters named according
3.44 - to the user-specified equations. Cases are numbered (starting from 1).
3.45 -
3.46 - For \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}, the induction principle coincides
3.47 - with structural recursion on the datatype the recursion is carried
3.48 - out.
3.49 + command accommodate reasoning by induction (cf.\ \hyperlink{method.induct}{\mbox{\isa{induct}}}):
3.50 + rule \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}induct{\isaliteral{22}{\isachardoublequote}}} refers to a specific induction rule, with
3.51 + parameters named according to the user-specified equations. Cases
3.52 + are numbered starting from 1. For \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}, the
3.53 + induction principle coincides with structural recursion on the
3.54 + datatype where the recursion is carried out.
3.55
3.56 The equations provided by these packages may be referred later as
3.57 theorem list \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}simps{\isaliteral{22}{\isachardoublequote}}}, where \isa{f} is the (collective)
3.58 @@ -353,6 +376,205 @@
3.59 \end{isamarkuptext}%
3.60 \isamarkuptrue%
3.61 %
3.62 +\isamarkupsubsubsection{Example: evaluation of expressions%
3.63 +}
3.64 +\isamarkuptrue%
3.65 +%
3.66 +\begin{isamarkuptext}%
3.67 +Subsequently, we define mutual datatypes for arithmetic and
3.68 + boolean expressions, and use \hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}} for evaluation
3.69 + functions that follow the same recursive structure.%
3.70 +\end{isamarkuptext}%
3.71 +\isamarkuptrue%
3.72 +\isacommand{datatype}\isamarkupfalse%
3.73 +\ {\isaliteral{27}{\isacharprime}}a\ aexp\ {\isaliteral{3D}{\isacharequal}}\isanewline
3.74 +\ \ \ \ IF\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.75 +\ \ {\isaliteral{7C}{\isacharbar}}\ Sum\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.76 +\ \ {\isaliteral{7C}{\isacharbar}}\ Diff\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.77 +\ \ {\isaliteral{7C}{\isacharbar}}\ Var\ {\isaliteral{27}{\isacharprime}}a\isanewline
3.78 +\ \ {\isaliteral{7C}{\isacharbar}}\ Num\ nat\isanewline
3.79 +\isakeyword{and}\ {\isaliteral{27}{\isacharprime}}a\ bexp\ {\isaliteral{3D}{\isacharequal}}\isanewline
3.80 +\ \ \ \ Less\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.81 +\ \ {\isaliteral{7C}{\isacharbar}}\ And\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.82 +\ \ {\isaliteral{7C}{\isacharbar}}\ Neg\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}%
3.83 +\begin{isamarkuptext}%
3.84 +\medskip Evaluation of arithmetic and boolean expressions%
3.85 +\end{isamarkuptext}%
3.86 +\isamarkuptrue%
3.87 +\isacommand{primrec}\isamarkupfalse%
3.88 +\ evala\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ aexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.89 +\ \ \isakeyword{and}\ evalb\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ bexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.90 +\isakeyword{where}\isanewline
3.91 +\ \ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}IF\ b\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ evalb\ env\ b\ then\ evala\ env\ a{\isadigit{1}}\ else\ evala\ env\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.92 +{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}Sum\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ evala\ env\ a{\isadigit{1}}\ {\isaliteral{2B}{\isacharplus}}\ evala\ env\ a{\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.93 +{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}Diff\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ evala\ env\ a{\isadigit{1}}\ {\isaliteral{2D}{\isacharminus}}\ evala\ env\ a{\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.94 +{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}Var\ v{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ env\ v{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.95 +{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}Num\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.96 +{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evalb\ env\ {\isaliteral{28}{\isacharparenleft}}Less\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}evala\ env\ a{\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ evala\ env\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.97 +{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evalb\ env\ {\isaliteral{28}{\isacharparenleft}}And\ b{\isadigit{1}}\ b{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}evalb\ env\ b{\isadigit{1}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ evalb\ env\ b{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.98 +{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evalb\ env\ {\isaliteral{28}{\isacharparenleft}}Neg\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ evalb\ env\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
3.99 +\begin{isamarkuptext}%
3.100 +Since the value of an expression depends on the value of its
3.101 + variables, the functions \isa{evala} and \isa{evalb} take an
3.102 + additional parameter, an \emph{environment} that maps variables to
3.103 + their values.
3.104 +
3.105 + \medskip Substitution on expressions can be defined similarly. The
3.106 + mapping \isa{f} of type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequote}}} given as a
3.107 + parameter is lifted canonically on the types \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequote}}} and
3.108 + \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequote}}}, respectively.%
3.109 +\end{isamarkuptext}%
3.110 +\isamarkuptrue%
3.111 +\isacommand{primrec}\isamarkupfalse%
3.112 +\ substa\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ aexp{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ aexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.113 +\ \ \isakeyword{and}\ substb\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ aexp{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ bexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ bexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.114 +\isakeyword{where}\isanewline
3.115 +\ \ {\isaliteral{22}{\isachardoublequoteopen}}substa\ f\ {\isaliteral{28}{\isacharparenleft}}IF\ b\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ IF\ {\isaliteral{28}{\isacharparenleft}}substb\ f\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.116 +{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substa\ f\ {\isaliteral{28}{\isacharparenleft}}Sum\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Sum\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.117 +{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substa\ f\ {\isaliteral{28}{\isacharparenleft}}Diff\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Diff\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.118 +{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substa\ f\ {\isaliteral{28}{\isacharparenleft}}Var\ v{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ v{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.119 +{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substa\ f\ {\isaliteral{28}{\isacharparenleft}}Num\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Num\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.120 +{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substb\ f\ {\isaliteral{28}{\isacharparenleft}}Less\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Less\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.121 +{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substb\ f\ {\isaliteral{28}{\isacharparenleft}}And\ b{\isadigit{1}}\ b{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ And\ {\isaliteral{28}{\isacharparenleft}}substb\ f\ b{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substb\ f\ b{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.122 +{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substb\ f\ {\isaliteral{28}{\isacharparenleft}}Neg\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Neg\ {\isaliteral{28}{\isacharparenleft}}substb\ f\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
3.123 +\begin{isamarkuptext}%
3.124 +In textbooks about semantics one often finds substitution
3.125 + theorems, which express the relationship between substitution and
3.126 + evaluation. For \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequote}}}, we can prove
3.127 + such a theorem by mutual induction, followed by simplification.%
3.128 +\end{isamarkuptext}%
3.129 +\isamarkuptrue%
3.130 +\isacommand{lemma}\isamarkupfalse%
3.131 +\ subst{\isaliteral{5F}{\isacharunderscore}}one{\isaliteral{3A}{\isacharcolon}}\isanewline
3.132 +\ \ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}substa\ {\isaliteral{28}{\isacharparenleft}}Var\ {\isaliteral{28}{\isacharparenleft}}v\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ evala\ {\isaliteral{28}{\isacharparenleft}}env\ {\isaliteral{28}{\isacharparenleft}}v\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ evala\ env\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.133 +\ \ {\isaliteral{22}{\isachardoublequoteopen}}evalb\ env\ {\isaliteral{28}{\isacharparenleft}}substb\ {\isaliteral{28}{\isacharparenleft}}Var\ {\isaliteral{28}{\isacharparenleft}}v\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ evalb\ {\isaliteral{28}{\isacharparenleft}}env\ {\isaliteral{28}{\isacharparenleft}}v\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ evala\ env\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.134 +%
3.135 +\isadelimproof
3.136 +\ \ %
3.137 +\endisadelimproof
3.138 +%
3.139 +\isatagproof
3.140 +\isacommand{by}\isamarkupfalse%
3.141 +\ {\isaliteral{28}{\isacharparenleft}}induct\ a\ \isakeyword{and}\ b{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all%
3.142 +\endisatagproof
3.143 +{\isafoldproof}%
3.144 +%
3.145 +\isadelimproof
3.146 +\isanewline
3.147 +%
3.148 +\endisadelimproof
3.149 +\isanewline
3.150 +\isacommand{lemma}\isamarkupfalse%
3.151 +\ subst{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{3A}{\isacharcolon}}\isanewline
3.152 +\ \ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ evala\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ evala\ env\ {\isaliteral{28}{\isacharparenleft}}s\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.153 +\ \ {\isaliteral{22}{\isachardoublequoteopen}}evalb\ env\ {\isaliteral{28}{\isacharparenleft}}substb\ s\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ evalb\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ evala\ env\ {\isaliteral{28}{\isacharparenleft}}s\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.154 +%
3.155 +\isadelimproof
3.156 +\ \ %
3.157 +\endisadelimproof
3.158 +%
3.159 +\isatagproof
3.160 +\isacommand{by}\isamarkupfalse%
3.161 +\ {\isaliteral{28}{\isacharparenleft}}induct\ a\ \isakeyword{and}\ b{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all%
3.162 +\endisatagproof
3.163 +{\isafoldproof}%
3.164 +%
3.165 +\isadelimproof
3.166 +%
3.167 +\endisadelimproof
3.168 +%
3.169 +\isamarkupsubsubsection{Example: a substitution function for terms%
3.170 +}
3.171 +\isamarkuptrue%
3.172 +%
3.173 +\begin{isamarkuptext}%
3.174 +Functions on datatypes with nested recursion are also defined
3.175 + by mutual primitive recursion.%
3.176 +\end{isamarkuptext}%
3.177 +\isamarkuptrue%
3.178 +\isacommand{datatype}\isamarkupfalse%
3.179 +\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{22}{\isachardoublequoteopen}}term{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{3D}{\isacharequal}}\ Var\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{7C}{\isacharbar}}\ App\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term\ list{\isaliteral{22}{\isachardoublequoteclose}}%
3.180 +\begin{isamarkuptext}%
3.181 +A substitution function on type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term{\isaliteral{22}{\isachardoublequote}}} can be
3.182 + defined as follows, by working simultaneously on \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term\ list{\isaliteral{22}{\isachardoublequote}}}:%
3.183 +\end{isamarkuptext}%
3.184 +\isamarkuptrue%
3.185 +\isacommand{primrec}\isamarkupfalse%
3.186 +\ subst{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
3.187 +\ \ subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term\ list{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.188 +\isakeyword{where}\isanewline
3.189 +\ \ {\isaliteral{22}{\isachardoublequoteopen}}subst{\isaliteral{5F}{\isacharunderscore}}term\ f\ {\isaliteral{28}{\isacharparenleft}}Var\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.190 +{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}subst{\isaliteral{5F}{\isacharunderscore}}term\ f\ {\isaliteral{28}{\isacharparenleft}}App\ b\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ App\ b\ {\isaliteral{28}{\isacharparenleft}}subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ f\ ts{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.191 +{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.192 +{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ f\ {\isaliteral{28}{\isacharparenleft}}t\ {\isaliteral{23}{\isacharhash}}\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ subst{\isaliteral{5F}{\isacharunderscore}}term\ f\ t\ {\isaliteral{23}{\isacharhash}}\ subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ f\ ts{\isaliteral{22}{\isachardoublequoteclose}}%
3.193 +\begin{isamarkuptext}%
3.194 +The recursion scheme follows the structure of the unfolded
3.195 + definition of type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term{\isaliteral{22}{\isachardoublequote}}}. To prove properties of this
3.196 + substitution function, mutual induction is needed:%
3.197 +\end{isamarkuptext}%
3.198 +\isamarkuptrue%
3.199 +\isacommand{lemma}\isamarkupfalse%
3.200 +\ {\isaliteral{22}{\isachardoublequoteopen}}subst{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{28}{\isacharparenleft}}subst{\isaliteral{5F}{\isacharunderscore}}term\ f{\isadigit{1}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ f{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ subst{\isaliteral{5F}{\isacharunderscore}}term\ f{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}subst{\isaliteral{5F}{\isacharunderscore}}term\ f{\isadigit{2}}\ t{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
3.201 +\ \ {\isaliteral{22}{\isachardoublequoteopen}}subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ {\isaliteral{28}{\isacharparenleft}}subst{\isaliteral{5F}{\isacharunderscore}}term\ f{\isadigit{1}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ f{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ ts\ {\isaliteral{3D}{\isacharequal}}\ subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ f{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ f{\isadigit{2}}\ ts{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.202 +%
3.203 +\isadelimproof
3.204 +\ \ %
3.205 +\endisadelimproof
3.206 +%
3.207 +\isatagproof
3.208 +\isacommand{by}\isamarkupfalse%
3.209 +\ {\isaliteral{28}{\isacharparenleft}}induct\ t\ \isakeyword{and}\ ts{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all%
3.210 +\endisatagproof
3.211 +{\isafoldproof}%
3.212 +%
3.213 +\isadelimproof
3.214 +%
3.215 +\endisadelimproof
3.216 +%
3.217 +\isamarkupsubsubsection{Example: a map function for infinitely branching trees%
3.218 +}
3.219 +\isamarkuptrue%
3.220 +%
3.221 +\begin{isamarkuptext}%
3.222 +Defining functions on infinitely branching datatypes by
3.223 + primitive recursion is just as easy.%
3.224 +\end{isamarkuptext}%
3.225 +\isamarkuptrue%
3.226 +\isacommand{datatype}\isamarkupfalse%
3.227 +\ {\isaliteral{27}{\isacharprime}}a\ tree\ {\isaliteral{3D}{\isacharequal}}\ Atom\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{7C}{\isacharbar}}\ Branch\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.228 +\isanewline
3.229 +\isacommand{primrec}\isamarkupfalse%
3.230 +\ map{\isaliteral{5F}{\isacharunderscore}}tree\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ tree\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ tree{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.231 +\isakeyword{where}\isanewline
3.232 +\ \ {\isaliteral{22}{\isachardoublequoteopen}}map{\isaliteral{5F}{\isacharunderscore}}tree\ f\ {\isaliteral{28}{\isacharparenleft}}Atom\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Atom\ {\isaliteral{28}{\isacharparenleft}}f\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.233 +{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}map{\isaliteral{5F}{\isacharunderscore}}tree\ f\ {\isaliteral{28}{\isacharparenleft}}Branch\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Branch\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ map{\isaliteral{5F}{\isacharunderscore}}tree\ f\ {\isaliteral{28}{\isacharparenleft}}ts\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
3.234 +\begin{isamarkuptext}%
3.235 +Note that all occurrences of functions such as \isa{ts}
3.236 + above must be applied to an argument. In particular, \isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{5F}{\isacharunderscore}}tree\ f\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ ts{\isaliteral{22}{\isachardoublequote}}} is not allowed here.%
3.237 +\end{isamarkuptext}%
3.238 +\isamarkuptrue%
3.239 +%
3.240 +\begin{isamarkuptext}%
3.241 +Here is a simple composition lemma for \isa{map{\isaliteral{5F}{\isacharunderscore}}tree}:%
3.242 +\end{isamarkuptext}%
3.243 +\isamarkuptrue%
3.244 +\isacommand{lemma}\isamarkupfalse%
3.245 +\ {\isaliteral{22}{\isachardoublequoteopen}}map{\isaliteral{5F}{\isacharunderscore}}tree\ g\ {\isaliteral{28}{\isacharparenleft}}map{\isaliteral{5F}{\isacharunderscore}}tree\ f\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ map{\isaliteral{5F}{\isacharunderscore}}tree\ {\isaliteral{28}{\isacharparenleft}}g\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ f{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.246 +%
3.247 +\isadelimproof
3.248 +\ \ %
3.249 +\endisadelimproof
3.250 +%
3.251 +\isatagproof
3.252 +\isacommand{by}\isamarkupfalse%
3.253 +\ {\isaliteral{28}{\isacharparenleft}}induct\ t{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all%
3.254 +\endisatagproof
3.255 +{\isafoldproof}%
3.256 +%
3.257 +\isadelimproof
3.258 +%
3.259 +\endisadelimproof
3.260 +%
3.261 \isamarkupsubsection{Proof methods related to recursive definitions%
3.262 }
3.263 \isamarkuptrue%