# HG changeset patch # User krauss # Date 1179435827 -7200 # Node ID 4b0bf04a4d6876cf058cb202dd383980860e7059 # Parent b469cf6dc5313fd651fd6d7fb64961448f35a3d6 updated diff -r b469cf6dc531 -r 4b0bf04a4d68 doc-src/IsarAdvanced/Functions/Thy/Functions.thy --- a/doc-src/IsarAdvanced/Functions/Thy/Functions.thy Thu May 17 23:00:06 2007 +0200 +++ b/doc-src/IsarAdvanced/Functions/Thy/Functions.thy Thu May 17 23:03:47 2007 +0200 @@ -9,13 +9,14 @@ imports Main begin -chapter {* Defining Recursive Functions in Isabelle/HOL *} - section {* Function Definition for Dummies *} text {* In most cases, defining a recursive function is just as simple as other definitions: - *} + + Like in functional programming, a function definition consists of a + +*} fun fib :: "nat \ nat" where @@ -24,11 +25,21 @@ | "fib (Suc (Suc n)) = fib n + fib (Suc n)" text {* - The function always terminates, since the argument of gets smaller in every - recursive call. Termination is an - important requirement, since it prevents inconsistencies: From - the "definition" @{text "f(n) = f(n) + 1"} we could prove - @{text "0 = 1"} by subtracting @{text "f(n)"} on both sides. + The syntax is rather self-explanatory: We introduce a function by + giving its name, its type and a set of defining recursive + equations. +*} + + + + + +text {* + The function always terminates, since its argument gets smaller in + every recursive call. Termination is an important requirement, since + it prevents inconsistencies: From the "definition" @{text "f(n) = + f(n) + 1"} we could prove @{text "0 = 1"} by subtracting @{text + "f(n)"} on both sides. Isabelle tries to prove termination automatically when a function is defined. We will later look at cases where this fails and see what to @@ -38,8 +49,8 @@ subsection {* Pattern matching *} text {* \label{patmatch} - Like in functional programming, functions can be defined by pattern - matching. At the moment we will only consider \emph{datatype + Like in functional programming, we can use pattern matching to + define functions. At the moment we will only consider \emph{constructor patterns}, which only consist of datatype constructors and variables. @@ -72,8 +83,6 @@ lemma "sep (0::nat) [1, 2, 3] = [1, 0, 2, 0, 3]" by simp - - subsection {* Induction *} text {* @@ -178,10 +187,14 @@ We can use this expression as a measure function suitable to prove termination. *} -termination +termination sum by (relation "measure (\(i,N). N + 1 - i)") auto text {* + The \cmd{termination} command sets up the termination goal for the + specified function @{text "sum"}. If the function name is omitted it + implicitly refers to the last function definition. + The @{text relation} method takes a relation of type @{typ "('a \ 'a) set"}, where @{typ "'a"} is the argument type of the function. If the function has multiple curried arguments, then @@ -223,6 +236,32 @@ termination by (relation "measures [\(i, N). N, \(i,N). N + 1 - i]") auto +subsection {* Manual Termination Proofs *} + +text {* + The @{text relation} method is often useful, but not + necessary. Since termination proofs are just normal Isabelle proofs, + they can also be carried out manually: +*} + +function id :: "nat \ nat" +where + "id 0 = 0" +| "id (Suc n) = Suc (id n)" +by pat_completeness auto + +termination +proof + show "wf less_than" .. +next + fix n show "(n, Suc n) \ less_than" by simp +qed + +text {* + Of course this is just a trivial example, but manual proofs can + sometimes be the only choice if faced with very hard termination problems. +*} + section {* Mutual Recursion *} @@ -334,8 +373,8 @@ shows the problem: Suppose we are modelling incomplete knowledge about the world by a - three-valued datatype, which has values for @{term "T"}, @{term "F"} - and @{term "X"} for true, false and uncertain propositions. + three-valued datatype, which has values @{term "T"}, @{term "F"} + and @{term "X"} for true, false and uncertain propositions, respectively. *} datatype P3 = T | F | X @@ -345,10 +384,10 @@ fun And :: "P3 \ P3 \ P3" where "And T p = p" - "And p T = p" - "And p F = F" - "And F p = F" - "And X X = X" +| "And p T = p" +| "And p F = F" +| "And F p = F" +| "And X X = X" text {* @@ -365,15 +404,15 @@ @{thm[indent=4] And.simps} \vspace*{1em} - \noindent There are several problems with this approach: + \noindent There are several problems with this: \begin{enumerate} \item When datatypes have many constructors, there can be an explosion of equations. For @{const "And"}, we get seven instead of - five equation, which can be tolerated, but this is just a small + five equations, which can be tolerated, but this is just a small example. - \item Since splitting makes the equations "more special", they + \item Since splitting makes the equations "less general", they do not always match in rewriting. While the term @{term "And x F"} can be simplified to @{term "F"} by the original specification, a (manual) case split on @{term "x"} is now necessary. @@ -390,17 +429,17 @@ both @{term "f x = True"} and @{term "f x = False"} is a bad idea. So if we don't want Isabelle to mangle our definitions, we will have to prove that this is not necessary. By using the full - definition form withour the \cmd{sequential} option, we get this + definition form without the \cmd{sequential} option, we get this behaviour: *} function And2 :: "P3 \ P3 \ P3" where "And2 T p = p" - "And2 p T = p" - "And2 p F = F" - "And2 F p = F" - "And2 X X = X" +| "And2 p T = p" +| "And2 p F = F" +| "And2 F p = F" +| "And2 X X = X" txt {* Now it is also time to look at the subgoals generated by a @@ -436,13 +475,6 @@ text {* FIXME *} -subsection {* Non-constructor patterns *} - -text {* FIXME *} - - - - section {* Partiality *} @@ -451,23 +483,672 @@ In HOL, all functions are total. A function @{term "f"} applied to @{term "x"} always has a value @{term "f x"}, and there is no notion of undefinedness. + + This property of HOL is the reason why we have to do termination + proofs when defining functions: The termination proof justifies the + definition of the function by wellfounded recursion. - FIXME + However, the \cmd{function} package still supports partiality. Let's + look at the following function which searches for a zero in the + function f. +*} + +function (*<*)(domintros, tailrec)(*>*)findzero :: "(nat \ nat) \ nat \ nat" +where + "findzero f n = (if f n = 0 then n else findzero f (Suc n))" +by pat_completeness auto +(*<*)declare findzero.simps[simp del](*>*) + +text {* + Clearly, any attempt of a termination proof must fail. And without + that, we do not get the usual rules @{text "findzero.simp"} and + @{text "findzero.induct"}. So what was the definition good for at all? +*} + +subsection {* Domain predicates *} + +text {* + The trick is that Isabelle has not only defined the function @{const findzero}, but also + a predicate @{term "findzero_dom"} that characterizes the values where the function + terminates: the \emph{domain} of the function. In Isabelle/HOL, a + partial function is just a total function with an additional domain + predicate. Like with total functions, we get simplification and + induction rules, but they are guarded by the domain conditions and + called @{text psimps} and @{text pinduct}: +*} + +thm findzero.psimps + +text {* + @{thm[display] findzero.psimps} +*} + +thm findzero.pinduct + +text {* + @{thm[display] findzero.pinduct} +*} + +text {* + As already mentioned, HOL does not support true partiality. All we + are doing here is using some tricks to make a total function appear + as if it was partial. We can still write the term @{term "findzero + (\x. 1) 0"} and like any other term of type @{typ nat} it is equal + to some natural number, although we might not be able to find out + which one (we will discuss this further in \S\ref{default}). The + function is \emph{underdefined}. + + But it is enough defined to prove something about it. We can prove + that if @{term "findzero f n"} + it terminates, it indeed returns a zero of @{term f}: +*} + +lemma findzero_zero: "findzero_dom (f, n) \ f (findzero f n) = 0" + +txt {* We apply induction as usual, but using the partial induction + rule: *} + +apply (induct f n rule: findzero.pinduct) + +txt {* This gives the following subgoals: + + @{subgoals[display,indent=0]} + + The premise in our lemma was used to satisfy the first premise in + the induction rule. However, now we can also use @{term + "findzero_dom (f, n)"} as an assumption in the induction step. This + allows to unfold @{term "findzero f n"} using the @{text psimps} + rule, and the rest is trivial. Since @{text psimps} rules carry the + @{text "[simp]"} attribute by default, we just need a single step: + *} +apply simp +done + +text {* + Proofs about partial functions are often not harder than for total + functions. Fig.~\ref{findzero_isar} shows a slightly more + complicated proof written in Isar. It is verbose enough to show how + partiality comes into play: From the partial induction, we get an + additional domain condition hypothesis. Observe how this condition + is applied when calls to @{term findzero} are unfolded. +*} + +text_raw {* +\begin{figure} +\begin{center} +\begin{minipage}{0.8\textwidth} +\isabellestyle{it} +\isastyle\isamarkuptrue +*} +lemma "\findzero_dom (f, n); x \ {n ..< findzero f n}\ \ f x \ 0" +proof (induct rule: findzero.pinduct) + fix f n assume dom: "findzero_dom (f, n)" + and IH: "\f n \ 0; x \ {Suc n.. + \ f x \ 0" + and x_range: "x \ {n.. 0" + proof + assume "f n = 0" + with dom have "findzero f n = n" by simp + with x_range show False by auto + qed + + from x_range have "x = n \ x \ {Suc n ..< findzero f n}" by auto + thus "f x \ 0" + proof + assume "x = n" + with `f n \ 0` show ?thesis by simp + next + assume "x \ {Suc n.. 0` have "x \ {Suc n ..< findzero f (Suc n)}" + by simp + with IH and `f n \ 0` + show ?thesis by simp + qed +qed +text_raw {* +\isamarkupfalse\isabellestyle{tt} +\end{minipage}\end{center} +\caption{A proof about a partial function}\label{findzero_isar} +\end{figure} +*} + +subsection {* Partial termination proofs *} + +text {* + Now that we have proved some interesting properties about our + function, we should turn to the domain predicate and see if it is + actually true for some values. Otherwise we would have just proved + lemmas with @{term False} as a premise. + + Essentially, we need some introduction rules for @{text + findzero_dom}. The function package can prove such domain + introduction rules automatically. But since they are not used very + often (they are almost never needed if the function is total), they + are disabled by default for efficiency reasons. So we have to go + back and ask for them explicitly by passing the @{text + "(domintros)"} option to the function package: + +\noindent\cmd{function} @{text "(domintros) findzero :: \"(nat \ nat) \ nat \ nat\""}\\% +\cmd{where}\isanewline% +\ \ \ldots\\ +\cmd{by} @{text "pat_completeness auto"}\\% + + + Now the package has proved an introduction rule for @{text findzero_dom}: +*} + +thm findzero.domintros + +text {* + @{thm[display] findzero.domintros} + + Domain introduction rules allow to show that a given value lies in the + domain of a function, if the arguments of all recursive calls + are in the domain as well. They allow to do a \qt{single step} in a + termination proof. Usually, you want to combine them with a suitable + induction principle. + + Since our function increases its argument at recursive calls, we + need an induction principle which works \qt{backwards}. We will use + @{text inc_induct}, which allows to do induction from a fixed number + \qt{downwards}: + + @{thm[display] inc_induct} + + Fig.~\ref{findzero_term} gives a detailed Isar proof of the fact + that @{text findzero} terminates if there is a zero which is greater + or equal to @{term n}. First we derive two useful rules which will + solve the base case and the step case of the induction. The + induction is then straightforward, except for the unusal induction + principle. + +*} + +text_raw {* +\begin{figure} +\begin{center} +\begin{minipage}{0.8\textwidth} +\isabellestyle{it} +\isastyle\isamarkuptrue +*} +lemma findzero_termination: + assumes "x >= n" + assumes "f x = 0" + shows "findzero_dom (f, n)" +proof - + have base: "findzero_dom (f, x)" + by (rule findzero.domintros) (simp add:`f x = 0`) + + have step: "\i. findzero_dom (f, Suc i) + \ findzero_dom (f, i)" + by (rule findzero.domintros) simp + + from `x \ n` + show ?thesis + proof (induct rule:inc_induct) + show "findzero_dom (f, x)" + by (rule base) + next + fix i assume "findzero_dom (f, Suc i)" + thus "findzero_dom (f, i)" + by (rule step) + qed +qed +text_raw {* +\isamarkupfalse\isabellestyle{tt} +\end{minipage}\end{center} +\caption{Termination proof for @{text findzero}}\label{findzero_term} +\end{figure} +*} + +text {* + Again, the proof given in Fig.~\ref{findzero_term} has a lot of + detail in order to explain the principles. Using more automation, we + can also have a short proof: +*} + +lemma findzero_termination_short: + assumes zero: "x >= n" + assumes [simp]: "f x = 0" + shows "findzero_dom (f, n)" + using zero + by (induct rule:inc_induct) (auto intro: findzero.domintros) + +text {* + It is simple to combine the partial correctness result with the + termination lemma: +*} + +lemma findzero_total_correctness: + "f x = 0 \ f (findzero f 0) = 0" +by (blast intro: findzero_zero findzero_termination) + +subsection {* Definition of the domain predicate *} + +text {* + Sometimes it is useful to know what the definition of the domain + predicate actually is. Actually, @{text findzero_dom} is just an + abbreviation: + + @{abbrev[display] findzero_dom} + + The domain predicate is the accessible part of a relation @{const + findzero_rel}, which was also created internally by the function + package. @{const findzero_rel} is just a normal + inductively defined predicate, so we can inspect its definition by + looking at the introduction rules @{text findzero_rel.intros}. + In our case there is just a single rule: + + @{thm[display] findzero_rel.intros} + + The relation @{const findzero_rel}, expressed as a binary predicate, + describes the \emph{recursion relation} of the function + definition. The recursion relation is a binary relation on + the arguments of the function that relates each argument to its + recursive calls. In general, there is one introduction rule for each + recursive call. + + The predicate @{term "acc findzero_rel"} is the \emph{accessible part} of + that relation. An argument belongs to the accessible part, if it can + be reached in a finite number of steps. + + Since the domain predicate is just an abbreviation, you can use + lemmas for @{const acc} and @{const findzero_rel} directly. Some + lemmas which are occasionally useful are @{text accI}, @{text + acc_downward}, and of course the introduction and elimination rules + for the recursion relation @{text "findzero.intros"} and @{text "findzero.cases"}. +*} + +(*lemma findzero_nicer_domintros: + "f x = 0 \ findzero_dom (f, x)" + "findzero_dom (f, Suc x) \ findzero_dom (f, x)" +by (rule accI, erule findzero_rel.cases, auto)+ +*) + +subsection {* A Useful Special Case: Tail recursion *} + +text {* + The domain predicate is our trick that allows us to model partiality + in a world of total functions. The downside of this is that we have + to carry it around all the time. The termination proof above allowed + us to replace the abstract @{term "findzero_dom (f, n)"} by the more + concrete @{term "(x \ n \ f x = 0)"}, but the condition is still + there and it won't go away soon. + + In particular, the domain predicate guard the unfolding of our + function, since it is there as a condition in the @{text psimp} + rules. + + On the other hand, we must be happy about the domain predicate, + since it guarantees that all this is at all possible without losing + consistency. + + Now there is an important special case: We can actually get rid + of the condition in the simplification rules, \emph{if the function + is tail-recursive}. The reason is that for all tail-recursive + equations there is a total function satisfying them, even if they + are non-terminating. + + The function package internally does the right construction and can + derive the unconditional simp rules, if we ask it to do so. Luckily, + our @{const "findzero"} function is tail-recursive, so we can just go + back and add another option to the \cmd{function} command: + +\noindent\cmd{function} @{text "(domintros, tailrec) findzero :: \"(nat \ nat) \ nat \ nat\""}\\% +\cmd{where}\isanewline% +\ \ \ldots\\% + + + Now, we actually get the unconditional simplification rules, even + though the function is partial: +*} + +thm findzero.simps + +text {* + @{thm[display] findzero.simps} + + Of course these would make the simplifier loop, so we better remove + them from the simpset: +*} + +declare findzero.simps[simp del] + + +text {* \fixme{Code generation ???} *} + +section {* Nested recursion *} + +text {* + Recursive calls which are nested in one another frequently cause + complications, since their termination proof can depend on a partial + correctness property of the function itself. + + As a small example, we define the \qt{nested zero} function: +*} + +function nz :: "nat \ nat" +where + "nz 0 = 0" +| "nz (Suc n) = nz (nz n)" +by pat_completeness auto + +text {* + If we attempt to prove termination using the identity measure on + naturals, this fails: +*} + +termination + apply (relation "measure (\n. n)") + apply auto + +txt {* + We get stuck with the subgoal + + @{subgoals[display]} + + Of course this statement is true, since we know that @{const nz} is + the zero function. And in fact we have no problem proving this + property by induction. +*} +oops + +lemma nz_is_zero: "nz_dom n \ nz n = 0" + by (induct rule:nz.pinduct) auto + +text {* + We formulate this as a partial correctness lemma with the condition + @{term "nz_dom n"}. This allows us to prove it with the @{text + pinduct} rule before we have proved termination. With this lemma, + the termination proof works as expected: +*} + +termination + by (relation "measure (\n. n)") (auto simp: nz_is_zero) + +text {* + As a general strategy, one should prove the statements needed for + termination as a partial property first. Then they can be used to do + the termination proof. This also works for less trivial + examples. Figure \ref{f91} defines the well-known 91-function by + McCarthy \cite{?} and proves its termination. +*} + +text_raw {* +\begin{figure} +\begin{center} +\begin{minipage}{0.8\textwidth} +\isabellestyle{it} +\isastyle\isamarkuptrue +*} + +function f91 :: "nat => nat" +where + "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))" +by pat_completeness auto + +lemma f91_estimate: + assumes trm: "f91_dom n" + shows "n < f91 n + 11" +using trm by induct auto + +termination +proof + let ?R = "measure (\x. 101 - x)" + show "wf ?R" .. + + fix n :: nat assume "\ 100 < n" -- "Assumptions for both calls" + + thus "(n + 11, n) \ ?R" by simp -- "Inner call" + + assume inner_trm: "f91_dom (n + 11)" -- "Outer call" + with f91_estimate have "n + 11 < f91 (n + 11) + 11" . + with `\ 100 < n` show "(f91 (n + 11), n) \ ?R" by simp +qed + +text_raw {* +\isamarkupfalse\isabellestyle{tt} +\end{minipage}\end{center} +\caption{McCarthy's 91-function}\label{f91} +\end{figure} *} +section {* Higher-Order Recursion *} +text {* + Higher-order recursion occurs when recursive calls + are passed as arguments to higher-order combinators such as @{term + map}, @{term filter} etc. + As an example, imagine a data type of n-ary trees: +*} + +datatype 'a tree = + Leaf 'a +| Branch "'a tree list" + + +text {* \noindent We can define a map function for trees, using the predefined + map function for lists. *} -section {* Nested recursion *} +function treemap :: "('a \ 'a) \ 'a tree \ 'a tree" +where + "treemap f (Leaf n) = Leaf (f n)" +| "treemap f (Branch l) = Branch (map (treemap f) l)" +by pat_completeness auto text {* + We do the termination proof manually, to point out what happens + here: +*} + +termination proof + txt {* + + As usual, we have to give a wellfounded relation, such that the + arguments of the recursive calls get smaller. But what exactly are + the arguments of the recursive calls? Isabelle gives us the + subgoals + + @{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 + 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 +next + fix f l and x :: "'a tree" + assume "x \ set l" + thus "((f, x), (f, Branch l)) \ measure (size o snd)" + apply simp + txt {* + Simplification returns the following subgoal: + + @{subgoals[display,indent=0]} + + We are lacking a property about the function @{const + tree_list_size}, which was generated automatically at the + definition of the @{text tree} type. We should go back and prove + it, by induction. + *} + oops + + lemma tree_list_size[simp]: "x \ set l \ size x < Suc (tree_list_size l)" + by (induct l) auto + + text {* + Now the whole termination proof is automatic: + *} + + termination + by lexicographic_order +subsection {* Congruence Rules *} + +text {* + Let's come back to the question how Isabelle knows about @{const + map}. + + The knowledge about map is encoded in so-called congruence rules, + which are special theorems known to the \cmd{function} command. The + rule for map is + + @{thm[display] map_cong} + + You can read this in the following way: Two applications of @{const + map} are equal, if the list arguments are equal and the functions + coincide on the elements of the list. This means that for the value + @{term "map f l"} we only have to know how @{term f} behaves on + @{term l}. + + Usually, one such congruence rule is + needed for each higher-order construct that is used when defining + new functions. In fact, even basic functions like @{const + If} and @{const Let} are handeled by this mechanism. The congruence + rule for @{const If} states that the @{text then} branch is only + relevant if the condition is true, and the @{text else} branch only if it + is false: + + @{thm[display] if_cong} + + Congruence rules can be added to the + function package by giving them the @{term fundef_cong} attribute. + + Isabelle comes with predefined congruence rules for most of the + definitions. + But if you define your own higher-order constructs, you will have to + come up with the congruence rules yourself, if you want to use your + functions in recursive definitions. Since the structure of + congruence rules is a little unintuitive, here are some exercises: +*} +(*<*) +fun mapeven :: "(nat \ nat) \ nat list \ 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} + 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 + +*} + - FIXME *} + + +section {* Appendix: Predefined Congruence Rules *} + +(*<*) +syntax (Rule output) + "==>" :: "prop \ prop \ prop" + ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>") + + "_bigimpl" :: "asms \ prop \ prop" + ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>") + + "_asms" :: "prop \ asms \ asms" + ("\<^raw:\mbox{>_\<^raw:}\\>/ _") + + "_asm" :: "prop \ asms" ("\<^raw:\mbox{>_\<^raw:}>") + +definition +FixImp :: "prop \ prop \ prop" +where + "FixImp (PROP A) (PROP B) \ (PROP A \ PROP B)" +notation (output) + FixImp (infixr "\" 1) + +setup {* +let + val fix_imps = map_aterms (fn Const ("==>", T) => Const ("Functions.FixImp", T) | t => t) + fun transform t = Logic.list_implies (map fix_imps (Logic.strip_imp_prems t), Logic.strip_imp_concl t) +in + TermStyle.add_style "topl" (K transform) +end +*} +(*>*) + +subsection {* Basic Control Structures *} + +text {* + +@{thm_style[mode=Rule] topl if_cong} + +@{thm_style [mode=Rule] topl let_cong} + +*} + +subsection {* Data Types *} + +text {* + +For each \cmd{datatype} definition, a congruence rule for the case + combinator is registeres automatically. Here are the rules for + @{text "nat"} and @{text "list"}: + +\begin{center}@{thm_style[mode=Rule] topl nat.case_cong}\end{center} + +\begin{center}@{thm_style[mode=Rule] topl list.case_cong}\end{center} + +*} + +subsection {* List combinators *} + + +text {* + +@{thm_style[mode=Rule] topl map_cong} + +@{thm_style[mode=Rule] topl filter_cong} + +@{thm_style[mode=Rule] topl foldr_cong} + +@{thm_style[mode=Rule] topl foldl_cong} + +Similar: takewhile, dropwhile + +*} + +subsection {* Sets *} + + +text {* + +@{thm_style[mode=Rule] topl ball_cong} + +@{thm_style[mode=Rule] topl bex_cong} + +@{thm_style[mode=Rule] topl UN_cong} + +@{thm_style[mode=Rule] topl INT_cong} + +@{thm_style[mode=Rule] topl image_cong} + + +*} diff -r b469cf6dc531 -r 4b0bf04a4d68 doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex --- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex Thu May 17 23:00:06 2007 +0200 +++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex Thu May 17 23:03:47 2007 +0200 @@ -20,16 +20,14 @@ % \endisadelimtheory % -\isamarkupchapter{Defining Recursive Functions in Isabelle/HOL% -} -\isamarkuptrue% -% \isamarkupsection{Function Definition for Dummies% } \isamarkuptrue% % \begin{isamarkuptext}% -In most cases, defining a recursive function is just as simple as other definitions:% +In most cases, defining a recursive function is just as simple as other definitions: + + Like in functional programming, a function definition consists of a% \end{isamarkuptext}% \isamarkuptrue% \isacommand{fun}\isamarkupfalse% @@ -39,11 +37,16 @@ {\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline {\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ n\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}% \begin{isamarkuptext}% -The function always terminates, since the argument of gets smaller in every - recursive call. Termination is an - important requirement, since it prevents inconsistencies: From - the "definition" \isa{f{\isacharparenleft}n{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}n{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}} we could prove - \isa{{\isadigit{0}}\ \ {\isacharequal}\ {\isadigit{1}}} by subtracting \isa{f{\isacharparenleft}n{\isacharparenright}} on both sides. +The syntax is rather self-explanatory: We introduce a function by + giving its name, its type and a set of defining recursive + equations.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{isamarkuptext}% +The function always terminates, since its argument gets smaller in + every recursive call. Termination is an important requirement, since + it prevents inconsistencies: From the "definition" \isa{f{\isacharparenleft}n{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}n{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}} we could prove \isa{{\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}} by subtracting \isa{f{\isacharparenleft}n{\isacharparenright}} on both sides. Isabelle tries to prove termination automatically when a function is defined. We will later look at cases where this fails and see what to @@ -57,8 +60,8 @@ % \begin{isamarkuptext}% \label{patmatch} - Like in functional programming, functions can be defined by pattern - matching. At the moment we will only consider \emph{datatype + Like in functional programming, we can use pattern matching to + define functions. At the moment we will only consider \emph{constructor patterns}, which only consist of datatype constructors and variables. @@ -235,7 +238,7 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{termination}\isamarkupfalse% -\ \isanewline +\ sum\isanewline % \isadelimproof % @@ -252,7 +255,11 @@ \endisadelimproof % \begin{isamarkuptext}% -The \isa{relation} method takes a relation of +The \cmd{termination} command sets up the termination goal for the + specified function \isa{sum}. If the function name is omitted it + implicitly refers to the last function definition. + + The \isa{relation} method takes a relation of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}, where \isa{{\isacharprime}a} is the argument type of the function. If the function has multiple curried arguments, then these are packed together into a tuple, as it happened in the above @@ -320,6 +327,71 @@ % \endisadelimproof % +\isamarkupsubsection{Manual Termination Proofs% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The \isa{relation} method is often useful, but not + necessary. Since termination proofs are just normal Isabelle proofs, + they can also be carried out manually:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{function}\isamarkupfalse% +\ id\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}id\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}id\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ {\isacharparenleft}id\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ pat{\isacharunderscore}completeness\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +\isanewline +% +\endisadelimproof +\isanewline +\isacommand{termination}\isamarkupfalse% +\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{proof}\isamarkupfalse% +\ \isanewline +\ \ \isacommand{show}\isamarkupfalse% +\ {\isachardoublequoteopen}wf\ less{\isacharunderscore}than{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% +\isanewline +\isacommand{next}\isamarkupfalse% +\isanewline +\ \ \isacommand{fix}\isamarkupfalse% +\ n\ \isacommand{show}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isacharparenleft}n{\isacharcomma}\ Suc\ n{\isacharparenright}\ {\isasymin}\ less{\isacharunderscore}than{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ simp\isanewline +\isacommand{qed}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +Of course this is just a trivial example, but manual proofs can + sometimes be the only choice if faced with very hard termination problems.% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsection{Mutual Recursion% } \isamarkuptrue% @@ -506,8 +578,8 @@ shows the problem: Suppose we are modelling incomplete knowledge about the world by a - three-valued datatype, which has values for \isa{T}, \isa{F} - and \isa{X} for true, false and uncertain propositions.% + three-valued datatype, which has values \isa{T}, \isa{F} + and \isa{X} for true, false and uncertain propositions, respectively.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{datatype}\isamarkupfalse% @@ -520,10 +592,10 @@ \ And\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}P{\isadigit{3}}\ {\isasymRightarrow}\ P{\isadigit{3}}\ {\isasymRightarrow}\ P{\isadigit{3}}{\isachardoublequoteclose}\isanewline \isakeyword{where}\isanewline \ \ {\isachardoublequoteopen}And\ T\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}And\ p\ T\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}And\ p\ F\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}And\ F\ p\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}And\ X\ X\ {\isacharequal}\ X{\isachardoublequoteclose}% +{\isacharbar}\ {\isachardoublequoteopen}And\ p\ T\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}And\ p\ F\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}And\ F\ p\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}And\ X\ X\ {\isacharequal}\ X{\isachardoublequoteclose}% \begin{isamarkuptext}% This definition is useful, because the equations can directly be used as rules to simplify expressions. But the patterns overlap, e.g.~the @@ -544,15 +616,15 @@ And\ X\ X\ {\isacharequal}\ X} \vspace*{1em} - \noindent There are several problems with this approach: + \noindent There are several problems with this: \begin{enumerate} \item When datatypes have many constructors, there can be an explosion of equations. For \isa{And}, we get seven instead of - five equation, which can be tolerated, but this is just a small + five equations, which can be tolerated, but this is just a small example. - \item Since splitting makes the equations "more special", they + \item Since splitting makes the equations "less general", they do not always match in rewriting. While the term \isa{And\ x\ F} can be simplified to \isa{F} by the original specification, a (manual) case split on \isa{x} is now necessary. @@ -568,7 +640,7 @@ both \isa{f\ x\ {\isacharequal}\ True} and \isa{f\ x\ {\isacharequal}\ False} is a bad idea. So if we don't want Isabelle to mangle our definitions, we will have to prove that this is not necessary. By using the full - definition form withour the \cmd{sequential} option, we get this + definition form without the \cmd{sequential} option, we get this behaviour:% \end{isamarkuptext}% \isamarkuptrue% @@ -576,10 +648,10 @@ \ And{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}P{\isadigit{3}}\ {\isasymRightarrow}\ P{\isadigit{3}}\ {\isasymRightarrow}\ P{\isadigit{3}}{\isachardoublequoteclose}\isanewline \isakeyword{where}\isanewline \ \ {\isachardoublequoteopen}And{\isadigit{2}}\ T\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}And{\isadigit{2}}\ p\ T\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}And{\isadigit{2}}\ p\ F\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}And{\isadigit{2}}\ F\ p\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}And{\isadigit{2}}\ X\ X\ {\isacharequal}\ X{\isachardoublequoteclose}% +{\isacharbar}\ {\isachardoublequoteopen}And{\isadigit{2}}\ p\ T\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}And{\isadigit{2}}\ p\ F\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}And{\isadigit{2}}\ F\ p\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}And{\isadigit{2}}\ X\ X\ {\isacharequal}\ X{\isachardoublequoteclose}% \isadelimproof % \endisadelimproof @@ -642,15 +714,6 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsection{Non-constructor patterns% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -FIXME% -\end{isamarkuptext}% -\isamarkuptrue% -% \isamarkupsection{Partiality% } \isamarkuptrue% @@ -659,8 +722,490 @@ In HOL, all functions are total. A function \isa{f} applied to \isa{x} always has a value \isa{f\ x}, and there is no notion of undefinedness. + + This property of HOL is the reason why we have to do termination + proofs when defining functions: The termination proof justifies the + definition of the function by wellfounded recursion. - FIXME% + However, the \cmd{function} package still supports partiality. Let's + look at the following function which searches for a zero in the + function f.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{function}\isamarkupfalse% +\ findzero\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}findzero\ f\ n\ {\isacharequal}\ {\isacharparenleft}if\ f\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ n\ else\ findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ pat{\isacharunderscore}completeness\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +Clearly, any attempt of a termination proof must fail. And without + that, we do not get the usual rules \isa{findzero{\isachardot}simp} and + \isa{findzero{\isachardot}induct}. So what was the definition good for at all?% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Domain predicates% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The trick is that Isabelle has not only defined the function \isa{findzero}, but also + a predicate \isa{findzero{\isacharunderscore}dom} that characterizes the values where the function + terminates: the \emph{domain} of the function. In Isabelle/HOL, a + partial function is just a total function with an additional domain + predicate. Like with total functions, we get simplification and + induction rules, but they are guarded by the domain conditions and + called \isa{psimps} and \isa{pinduct}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{thm}\isamarkupfalse% +\ findzero{\isachardot}psimps% +\begin{isamarkuptext}% +\begin{isabelle}% +findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}\ {\isasymLongrightarrow}\isanewline +findzero\ {\isacharquery}f\ {\isacharquery}n\ {\isacharequal}\ {\isacharparenleft}if\ {\isacharquery}f\ {\isacharquery}n\ {\isacharequal}\ {\isadigit{0}}\ then\ {\isacharquery}n\ else\ findzero\ {\isacharquery}f\ {\isacharparenleft}Suc\ {\isacharquery}n{\isacharparenright}{\isacharparenright}% +\end{isabelle}% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{thm}\isamarkupfalse% +\ findzero{\isachardot}pinduct% +\begin{isamarkuptext}% +\begin{isabelle}% +{\isasymlbrakk}findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}a{\isadigit{0}}{\isachardot}{\isadigit{0}}{\isacharcomma}\ {\isacharquery}a{\isadigit{1}}{\isachardot}{\isadigit{0}}{\isacharparenright}{\isacharsemicolon}\isanewline +\isaindent{\ }{\isasymAnd}f\ n{\isachardot}\ {\isasymlbrakk}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isacharsemicolon}\ f\ n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ {\isacharquery}P\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ f\ n{\isasymrbrakk}\isanewline +{\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}a{\isadigit{0}}{\isachardot}{\isadigit{0}}\ {\isacharquery}a{\isadigit{1}}{\isachardot}{\isadigit{0}}% +\end{isabelle}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{isamarkuptext}% +As already mentioned, HOL does not support true partiality. All we + are doing here is using some tricks to make a total function appear + as if it was partial. We can still write the term \isa{findzero\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ {\isadigit{1}}{\isacharparenright}\ {\isadigit{0}}} and like any other term of type \isa{nat} it is equal + to some natural number, although we might not be able to find out + which one (we will discuss this further in \S\ref{default}). The + function is \emph{underdefined}. + + But it is enough defined to prove something about it. We can prove + that if \isa{findzero\ f\ n} + it terminates, it indeed returns a zero of \isa{f}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ findzero{\isacharunderscore}zero{\isacharcolon}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}findzero\ f\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\begin{isamarkuptxt}% +We apply induction as usual, but using the partial induction + rule:% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{apply}\isamarkupfalse% +\ {\isacharparenleft}induct\ f\ n\ rule{\isacharcolon}\ findzero{\isachardot}pinduct{\isacharparenright}% +\begin{isamarkuptxt}% +This gives the following subgoals: + + \begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}f\ n{\isachardot}\ {\isasymlbrakk}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isacharsemicolon}\ f\ n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}f\ n{\isachardot}\ }{\isasymLongrightarrow}\ f\ {\isacharparenleft}findzero\ f\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}% +\end{isabelle} + + The premise in our lemma was used to satisfy the first premise in + the induction rule. However, now we can also use \isa{findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}} as an assumption in the induction step. This + allows to unfold \isa{findzero\ f\ n} using the \isa{psimps} + rule, and the rest is trivial. Since \isa{psimps} rules carry the + \isa{{\isacharbrackleft}simp{\isacharbrackright}} attribute by default, we just need a single step:% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{apply}\isamarkupfalse% +\ simp\isanewline +\isacommand{done}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +Proofs about partial functions are often not harder than for total + functions. Fig.~\ref{findzero_isar} shows a slightly more + complicated proof written in Isar. It is verbose enough to show how + partiality comes into play: From the partial induction, we get an + additional domain condition hypothesis. Observe how this condition + is applied when calls to \isa{findzero} are unfolded.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{figure} +\begin{center} +\begin{minipage}{0.8\textwidth} +\isabellestyle{it} +\isastyle\isamarkuptrue +\isacommand{lemma}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isasymlbrakk}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isacharsemicolon}\ x\ {\isasymin}\ {\isacharbraceleft}n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ n{\isacharbraceright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ f\ x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{proof}\isamarkupfalse% +\ {\isacharparenleft}induct\ rule{\isacharcolon}\ findzero{\isachardot}pinduct{\isacharparenright}\isanewline +\ \ \isacommand{fix}\isamarkupfalse% +\ f\ n\ \isacommand{assume}\isamarkupfalse% +\ dom{\isacharcolon}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \isakeyword{and}\ IH{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharsemicolon}\ x\ {\isasymin}\ {\isacharbraceleft}Suc\ n{\isachardot}{\isachardot}{\isacharless}findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharbraceright}{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ f\ x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\ \ \ \ \isakeyword{and}\ x{\isacharunderscore}range{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharbraceleft}n{\isachardot}{\isachardot}{\isacharless}findzero\ f\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline +\ \ \isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isachardoublequoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\ \isanewline +\ \ \ \ \isacommand{assume}\isamarkupfalse% +\ {\isachardoublequoteopen}f\ n\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{with}\isamarkupfalse% +\ dom\ \isacommand{have}\isamarkupfalse% +\ {\isachardoublequoteopen}findzero\ f\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ simp\isanewline +\ \ \ \ \isacommand{with}\isamarkupfalse% +\ x{\isacharunderscore}range\ \isacommand{show}\isamarkupfalse% +\ False\ \isacommand{by}\isamarkupfalse% +\ auto\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\ \ \isanewline +\ \ \isacommand{from}\isamarkupfalse% +\ x{\isacharunderscore}range\ \isacommand{have}\isamarkupfalse% +\ {\isachardoublequoteopen}x\ {\isacharequal}\ n\ {\isasymor}\ x\ {\isasymin}\ {\isacharbraceleft}Suc\ n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ n{\isacharbraceright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ auto\isanewline +\ \ \isacommand{thus}\isamarkupfalse% +\ {\isachardoublequoteopen}f\ x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{assume}\isamarkupfalse% +\ {\isachardoublequoteopen}x\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{with}\isamarkupfalse% +\ {\isacharbackquoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse% +\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% +\ simp\isanewline +\ \ \isacommand{next}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{assume}\isamarkupfalse% +\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharbraceleft}Suc\ n{\isachardot}{\isachardot}{\isacharless}findzero\ f\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{with}\isamarkupfalse% +\ dom\ \isakeyword{and}\ {\isacharbackquoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ \isacommand{have}\isamarkupfalse% +\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharbraceleft}Suc\ n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ \isacommand{by}\isamarkupfalse% +\ simp\isanewline +\ \ \ \ \isacommand{with}\isamarkupfalse% +\ IH\ \isakeyword{and}\ {\isacharbackquoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% +\ simp\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\isacommand{qed}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupfalse\isabellestyle{tt} +\end{minipage}\end{center} +\caption{A proof about a partial function}\label{findzero_isar} +\end{figure} +% +\isamarkupsubsection{Partial termination proofs% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Now that we have proved some interesting properties about our + function, we should turn to the domain predicate and see if it is + actually true for some values. Otherwise we would have just proved + lemmas with \isa{False} as a premise. + + Essentially, we need some introduction rules for \isa{findzero{\isacharunderscore}dom}. The function package can prove such domain + introduction rules automatically. But since they are not used very + often (they are almost never needed if the function is total), they + are disabled by default for efficiency reasons. So we have to go + back and ask for them explicitly by passing the \isa{{\isacharparenleft}domintros{\isacharparenright}} option to the function package: + +\noindent\cmd{function} \isa{{\isacharparenleft}domintros{\isacharparenright}\ findzero\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}}\\% +\cmd{where}\isanewline% +\ \ \ldots\\ +\cmd{by} \isa{pat{\isacharunderscore}completeness\ auto}\\% + + + Now the package has proved an introduction rule for \isa{findzero{\isacharunderscore}dom}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{thm}\isamarkupfalse% +\ findzero{\isachardot}domintros% +\begin{isamarkuptext}% +\begin{isabelle}% +{\isacharparenleft}{\isadigit{0}}\ {\isacharless}\ {\isacharquery}f\ {\isacharquery}n\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ Suc\ {\isacharquery}n{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}% +\end{isabelle} + + Domain introduction rules allow to show that a given value lies in the + domain of a function, if the arguments of all recursive calls + are in the domain as well. They allow to do a \qt{single step} in a + termination proof. Usually, you want to combine them with a suitable + induction principle. + + Since our function increases its argument at recursive calls, we + need an induction principle which works \qt{backwards}. We will use + \isa{inc{\isacharunderscore}induct}, which allows to do induction from a fixed number + \qt{downwards}: + + \begin{isabelle}% +{\isasymlbrakk}{\isacharquery}i\ {\isasymle}\ {\isacharquery}j{\isacharsemicolon}\ {\isacharquery}P\ {\isacharquery}j{\isacharsemicolon}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}i\ {\isacharless}\ {\isacharquery}j{\isacharsemicolon}\ {\isacharquery}P\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ i{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}i% +\end{isabelle} + + Fig.~\ref{findzero_term} gives a detailed Isar proof of the fact + that \isa{findzero} terminates if there is a zero which is greater + or equal to \isa{n}. First we derive two useful rules which will + solve the base case and the step case of the induction. The + induction is then straightforward, except for the unusal induction + principle.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{figure} +\begin{center} +\begin{minipage}{0.8\textwidth} +\isabellestyle{it} +\isastyle\isamarkuptrue +\isacommand{lemma}\isamarkupfalse% +\ findzero{\isacharunderscore}termination{\isacharcolon}\isanewline +\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}x\ {\isachargreater}{\isacharequal}\ n{\isachardoublequoteclose}\ \isanewline +\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}f\ x\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{shows}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{proof}\isamarkupfalse% +\ {\isacharminus}\ \isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ base{\isacharcolon}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}rule\ findzero{\isachardot}domintros{\isacharparenright}\ {\isacharparenleft}simp\ add{\isacharcolon}{\isacharbackquoteopen}f\ x\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}{\isacharparenright}\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ step{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i{\isachardot}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ Suc\ i{\isacharparenright}\ \isanewline +\ \ \ \ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ i{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}rule\ findzero{\isachardot}domintros{\isacharparenright}\ simp\isanewline +\isanewline +\ \ \isacommand{from}\isamarkupfalse% +\ {\isacharbackquoteopen}x\ {\isasymge}\ n{\isacharbackquoteclose}\isanewline +\ \ \isacommand{show}\isamarkupfalse% +\ {\isacharquery}thesis\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\ {\isacharparenleft}induct\ rule{\isacharcolon}inc{\isacharunderscore}induct{\isacharparenright}\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}rule\ base{\isacharparenright}\isanewline +\ \ \isacommand{next}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{fix}\isamarkupfalse% +\ i\ \isacommand{assume}\isamarkupfalse% +\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ Suc\ i{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{thus}\isamarkupfalse% +\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ i{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}rule\ step{\isacharparenright}\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\isacommand{qed}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupfalse\isabellestyle{tt} +\end{minipage}\end{center} +\caption{Termination proof for \isa{findzero}}\label{findzero_term} +\end{figure} +% +\begin{isamarkuptext}% +Again, the proof given in Fig.~\ref{findzero_term} has a lot of + detail in order to explain the principles. Using more automation, we + can also have a short proof:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ findzero{\isacharunderscore}termination{\isacharunderscore}short{\isacharcolon}\isanewline +\ \ \isakeyword{assumes}\ zero{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isachargreater}{\isacharequal}\ n{\isachardoublequoteclose}\ \isanewline +\ \ \isakeyword{assumes}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}f\ x\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{shows}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{using}\isamarkupfalse% +\ zero\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ rule{\isacharcolon}inc{\isacharunderscore}induct{\isacharparenright}\ {\isacharparenleft}auto\ intro{\isacharcolon}\ findzero{\isachardot}domintros{\isacharparenright}% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +It is simple to combine the partial correctness result with the + termination lemma:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ findzero{\isacharunderscore}total{\isacharunderscore}correctness{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}f\ x\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}findzero\ f\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}blast\ intro{\isacharcolon}\ findzero{\isacharunderscore}zero\ findzero{\isacharunderscore}termination{\isacharparenright}% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupsubsection{Definition of the domain predicate% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Sometimes it is useful to know what the definition of the domain + predicate actually is. Actually, \isa{findzero{\isacharunderscore}dom} is just an + abbreviation: + + \begin{isabelle}% +findzero{\isacharunderscore}dom\ {\isasymequiv}\ acc\ findzero{\isacharunderscore}rel% +\end{isabelle} + + The domain predicate is the accessible part of a relation \isa{findzero{\isacharunderscore}rel}, which was also created internally by the function + package. \isa{findzero{\isacharunderscore}rel} is just a normal + inductively defined predicate, so we can inspect its definition by + looking at the introduction rules \isa{findzero{\isacharunderscore}rel{\isachardot}intros}. + In our case there is just a single rule: + + \begin{isabelle}% +{\isacharquery}f\ {\isacharquery}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}rel\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ Suc\ {\isacharquery}n{\isacharparenright}\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}% +\end{isabelle} + + The relation \isa{findzero{\isacharunderscore}rel}, expressed as a binary predicate, + describes the \emph{recursion relation} of the function + definition. The recursion relation is a binary relation on + the arguments of the function that relates each argument to its + recursive calls. In general, there is one introduction rule for each + recursive call. + + The predicate \isa{findzero{\isacharunderscore}dom} is the \emph{accessible part} of + that relation. An argument belongs to the accessible part, if it can + be reached in a finite number of steps. + + Since the domain predicate is just an abbreviation, you can use + lemmas for \isa{acc} and \isa{findzero{\isacharunderscore}rel} directly. Some + lemmas which are occasionally useful are \isa{accI}, \isa{acc{\isacharunderscore}downward}, and of course the introduction and elimination rules + for the recursion relation \isa{findzero{\isachardot}intros} and \isa{findzero{\isachardot}cases}.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{A Useful Special Case: Tail recursion% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The domain predicate is our trick that allows us to model partiality + in a world of total functions. The downside of this is that we have + to carry it around all the time. The termination proof above allowed + us to replace the abstract \isa{findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}} by the more + concrete \isa{n\ {\isasymle}\ x\ {\isasymand}\ f\ x\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}b{\isacharparenright}}, but the condition is still + there and it won't go away soon. + + In particular, the domain predicate guard the unfolding of our + function, since it is there as a condition in the \isa{psimp} + rules. + + On the other hand, we must be happy about the domain predicate, + since it guarantees that all this is at all possible without losing + consistency. + + Now there is an important special case: We can actually get rid + of the condition in the simplification rules, \emph{if the function + is tail-recursive}. The reason is that for all tail-recursive + equations there is a total function satisfying them, even if they + are non-terminating. + + The function package internally does the right construction and can + derive the unconditional simp rules, if we ask it to do so. Luckily, + our \isa{findzero} function is tail-recursive, so we can just go + back and add another option to the \cmd{function} command: + +\noindent\cmd{function} \isa{{\isacharparenleft}domintros{\isacharcomma}\ tailrec{\isacharparenright}\ findzero\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}}\\% +\cmd{where}\isanewline% +\ \ \ldots\\% + + + Now, we actually get the unconditional simplification rules, even + though the function is partial:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{thm}\isamarkupfalse% +\ findzero{\isachardot}simps% +\begin{isamarkuptext}% +\begin{isabelle}% +findzero\ {\isacharquery}f\ {\isacharquery}n\ {\isacharequal}\ {\isacharparenleft}if\ {\isacharquery}f\ {\isacharquery}n\ {\isacharequal}\ {\isadigit{0}}\ then\ {\isacharquery}n\ else\ findzero\ {\isacharquery}f\ {\isacharparenleft}Suc\ {\isacharquery}n{\isacharparenright}{\isacharparenright}% +\end{isabelle} + + Of course these would make the simplifier loop, so we better remove + them from the simpset:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{declare}\isamarkupfalse% +\ findzero{\isachardot}simps{\isacharbrackleft}simp\ del{\isacharbrackright}% +\begin{isamarkuptext}% +\fixme{Code generation ???}% \end{isamarkuptext}% \isamarkuptrue% % @@ -669,7 +1214,507 @@ \isamarkuptrue% % \begin{isamarkuptext}% -FIXME% +Recursive calls which are nested in one another frequently cause + complications, since their termination proof can depend on a partial + correctness property of the function itself. + + As a small example, we define the \qt{nested zero} function:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{function}\isamarkupfalse% +\ nz\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}nz\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}nz\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ nz\ {\isacharparenleft}nz\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ pat{\isacharunderscore}completeness\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +If we attempt to prove termination using the identity measure on + naturals, this fails:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{termination}\isamarkupfalse% +\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{apply}\isamarkupfalse% +\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline +\ \ \isacommand{apply}\isamarkupfalse% +\ auto% +\begin{isamarkuptxt}% +We get stuck with the subgoal + + \begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ nz{\isacharunderscore}dom\ n\ {\isasymLongrightarrow}\ nz\ n\ {\isacharless}\ Suc\ n% +\end{isabelle} + + Of course this statement is true, since we know that \isa{nz} is + the zero function. And in fact we have no problem proving this + property by induction.% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{oops}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +\isanewline +% +\endisadelimproof +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ nz{\isacharunderscore}is{\isacharunderscore}zero{\isacharcolon}\ {\isachardoublequoteopen}nz{\isacharunderscore}dom\ n\ {\isasymLongrightarrow}\ nz\ n\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ rule{\isacharcolon}nz{\isachardot}pinduct{\isacharparenright}\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +We formulate this as a partial correctness lemma with the condition + \isa{nz{\isacharunderscore}dom\ n}. This allows us to prove it with the \isa{pinduct} rule before we have proved termination. With this lemma, + the termination proof works as expected:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{termination}\isamarkupfalse% +\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ {\isacharparenleft}auto\ simp{\isacharcolon}\ nz{\isacharunderscore}is{\isacharunderscore}zero{\isacharparenright}% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +As a general strategy, one should prove the statements needed for + termination as a partial property first. Then they can be used to do + the termination proof. This also works for less trivial + examples. Figure \ref{f91} defines the well-known 91-function by + McCarthy \cite{?} and proves its termination.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{figure} +\begin{center} +\begin{minipage}{0.8\textwidth} +\isabellestyle{it} +\isastyle\isamarkuptrue +\isacommand{function}\isamarkupfalse% +\ f{\isadigit{9}}{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isacharequal}{\isachargreater}\ nat{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}f{\isadigit{9}}{\isadigit{1}}\ n\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharless}\ n\ then\ n\ {\isacharminus}\ {\isadigit{1}}{\isadigit{0}}\ else\ f{\isadigit{9}}{\isadigit{1}}\ {\isacharparenleft}f{\isadigit{9}}{\isadigit{1}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ pat{\isacharunderscore}completeness\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +\isanewline +% +\endisadelimproof +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ f{\isadigit{9}}{\isadigit{1}}{\isacharunderscore}estimate{\isacharcolon}\ \isanewline +\ \ \isakeyword{assumes}\ trm{\isacharcolon}\ {\isachardoublequoteopen}f{\isadigit{9}}{\isadigit{1}}{\isacharunderscore}dom\ n{\isachardoublequoteclose}\ \isanewline +\ \ \isakeyword{shows}\ {\isachardoublequoteopen}n\ {\isacharless}\ f{\isadigit{9}}{\isadigit{1}}\ n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{using}\isamarkupfalse% +\ trm\ \isacommand{by}\isamarkupfalse% +\ induct\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +\isanewline +% +\endisadelimproof +\isanewline +\isacommand{termination}\isamarkupfalse% +\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{proof}\isamarkupfalse% +\isanewline +\ \ \isacommand{let}\isamarkupfalse% +\ {\isacharquery}R\ {\isacharequal}\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{1}}\ {\isacharminus}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{show}\isamarkupfalse% +\ {\isachardoublequoteopen}wf\ {\isacharquery}R{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{fix}\isamarkupfalse% +\ n\ {\isacharcolon}{\isacharcolon}\ nat\ \isacommand{assume}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isasymnot}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharless}\ n{\isachardoublequoteclose}\ % +\isamarkupcmt{Assumptions for both calls% +} +\isanewline +\isanewline +\ \ \isacommand{thus}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharcomma}\ n{\isacharparenright}\ {\isasymin}\ {\isacharquery}R{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ simp\ % +\isamarkupcmt{Inner call% +} +\isanewline +\isanewline +\ \ \isacommand{assume}\isamarkupfalse% +\ inner{\isacharunderscore}trm{\isacharcolon}\ {\isachardoublequoteopen}f{\isadigit{9}}{\isadigit{1}}{\isacharunderscore}dom\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\ % +\isamarkupcmt{Outer call% +} +\isanewline +\ \ \isacommand{with}\isamarkupfalse% +\ f{\isadigit{9}}{\isadigit{1}}{\isacharunderscore}estimate\ \isacommand{have}\isamarkupfalse% +\ {\isachardoublequoteopen}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}\ {\isacharless}\ f{\isadigit{9}}{\isadigit{1}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% +\isanewline +\ \ \isacommand{with}\isamarkupfalse% +\ {\isacharbackquoteopen}{\isasymnot}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharless}\ n{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isacharparenleft}f{\isadigit{9}}{\isadigit{1}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharparenright}{\isacharcomma}\ n{\isacharparenright}\ {\isasymin}\ {\isacharquery}R{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ simp\ \isanewline +\isacommand{qed}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupfalse\isabellestyle{tt} +\end{minipage}\end{center} +\caption{McCarthy's 91-function}\label{f91} +\end{figure} +% +\isamarkupsection{Higher-Order Recursion% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Higher-order recursion occurs when recursive calls + are passed as arguments to higher-order combinators such as \isa{map}, \isa{filter} etc. + As an example, imagine a data type of n-ary trees:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{datatype}\isamarkupfalse% +\ {\isacharprime}a\ tree\ {\isacharequal}\ \isanewline +\ \ 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.% +\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 +\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 +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ pat{\isacharunderscore}completeness\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +We do the termination proof manually, to point out what happens + here:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{termination}\isamarkupfalse% +% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{proof}\isamarkupfalse% +% +\begin{isamarkuptxt}% +As usual, we have to give a wellfounded relation, such that the + arguments of the recursive calls get smaller. But what exactly are + the arguments of the recursive calls? Isabelle gives us the + subgoals + + \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% +\end{isabelle} + + So Isabelle seems to know that \isa{map} behaves nicely and only + applies the recursive call \isa{treemap\ f} 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% +\ simp\isanewline +\isacommand{next}\isamarkupfalse% +\isanewline +\ \ \isacommand{fix}\isamarkupfalse% +\ f\ l\ \isakeyword{and}\ x\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree{\isachardoublequoteclose}\isanewline +\ \ \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 +\ \ \ \ \isacommand{apply}\isamarkupfalse% +\ simp% +\begin{isamarkuptxt}% +Simplification returns the following subgoal: + + \begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ x{\isacharunderscore}{\isacharunderscore}\ {\isasymin}\ set\ l{\isacharunderscore}{\isacharunderscore}\ {\isasymLongrightarrow}\ size\ x{\isacharunderscore}{\isacharunderscore}\ {\isacharless}\ Suc\ {\isacharparenleft}tree{\isacharunderscore}list{\isacharunderscore}size\ l{\isacharunderscore}{\isacharunderscore}{\isacharparenright}% +\end{isabelle} + + We are lacking a property about the function \isa{tree{\isacharunderscore}list{\isacharunderscore}size}, which was generated automatically at the + definition of the \isa{tree} type. We should go back and prove + it, by induction.% +\end{isamarkuptxt}% +\isamarkuptrue% +\ \ \ \ \isacommand{oops}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\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 +% +\isadelimproof +\ \ \ \ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ l{\isacharparenright}\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +Now the whole termination proof is automatic:% +\end{isamarkuptext}% +\isamarkuptrue% +\ \ \isacommand{termination}\isamarkupfalse% +\ \isanewline +% +\isadelimproof +\ \ \ \ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ lexicographic{\isacharunderscore}order% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupsubsection{Congruence Rules% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Let's come back to the question how Isabelle knows about \isa{map}. + + The knowledge about map is encoded in so-called congruence rules, + which are special theorems known to the \cmd{function} command. The + rule for map is + + \begin{isabelle}% +{\isasymlbrakk}{\isacharquery}xs\ {\isacharequal}\ {\isacharquery}ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ {\isacharquery}ys\ {\isasymLongrightarrow}\ {\isacharquery}f\ x\ {\isacharequal}\ {\isacharquery}g\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ map\ {\isacharquery}f\ {\isacharquery}xs\ {\isacharequal}\ map\ {\isacharquery}g\ {\isacharquery}ys% +\end{isabelle} + + You can read this in the following way: Two applications of \isa{map} are equal, if the list arguments are equal and the functions + coincide on the elements of the list. This means that for the value + \isa{map\ f\ l} we only have to know how \isa{f} behaves on + \isa{l}. + + Usually, one such congruence rule is + needed for each higher-order construct that is used when defining + new functions. In fact, even basic functions like \isa{If} and \isa{Let} are handeled by this mechanism. The congruence + rule for \isa{If} states that the \isa{then} branch is only + relevant if the condition is true, and the \isa{else} branch only if it + is false: + + \begin{isabelle}% +{\isasymlbrakk}{\isacharquery}b\ {\isacharequal}\ {\isacharquery}c{\isacharsemicolon}\ {\isacharquery}c\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}u{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}c\ {\isasymLongrightarrow}\ {\isacharquery}y\ {\isacharequal}\ {\isacharquery}v{\isasymrbrakk}\isanewline +{\isasymLongrightarrow}\ {\isacharparenleft}if\ {\isacharquery}b\ then\ {\isacharquery}x\ else\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ {\isacharquery}c\ then\ {\isacharquery}u\ else\ {\isacharquery}v{\isacharparenright}% +\end{isabelle} + + Congruence rules can be added to the + function package by giving them the \isa{fundef{\isacharunderscore}cong} attribute. + + Isabelle comes with predefined congruence rules for most of the + definitions. + But if you define your own higher-order constructs, you will have to + come up with the congruence rules yourself, if you want to use your + functions in recursive definitions. Since the structure of + congruence rules is a little unintuitive, here are some exercises:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{exercise} + Find a suitable congruence rule for the following function which + maps only over the even numbers in a list: + + \begin{isabelle}% +mapeven\ {\isacharquery}f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\isasep\isanewline% +mapeven\ {\isacharquery}f\ {\isacharparenleft}{\isacharquery}x\ {\isacharhash}\ {\isacharquery}xs{\isacharparenright}\ {\isacharequal}\isanewline +{\isacharparenleft}if\ {\isacharquery}x\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}\ then\ {\isacharquery}f\ {\isacharquery}x\ {\isacharhash}\ mapeven\ {\isacharquery}f\ {\isacharquery}xs\ else\ {\isacharquery}x\ {\isacharhash}\ mapeven\ {\isacharquery}f\ {\isacharquery}xs{\isacharparenright}% +\end{isabelle} + \end{exercise} + + \begin{exercise} + What happens if the congruence rule for \isa{If} is + disabled by declaring \isa{if{\isacharunderscore}cong{\isacharbrackleft}fundef{\isacharunderscore}cong\ del{\isacharbrackright}}? + \end{exercise} + + Note that in some cases there is no \qt{best} congruence rule. + \fixme% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Appendix: Predefined Congruence Rules% +} +\isamarkuptrue% +% +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% +\isamarkupsubsection{Basic Control Structures% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\isa{\mbox{}\inferrule{\mbox{{\isacharquery}b\ {\isacharequal}\ {\isacharquery}c}\\\ \mbox{{\isacharquery}c\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}u}\\\ \mbox{{\isasymnot}\ {\isacharquery}c\ {\isasymLongrightarrow}\ {\isacharquery}y\ {\isacharequal}\ {\isacharquery}v}}{\mbox{{\isacharparenleft}if\ {\isacharquery}b\ then\ {\isacharquery}x\ else\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ {\isacharquery}c\ then\ {\isacharquery}u\ else\ {\isacharquery}v{\isacharparenright}}}} + +\isa{\mbox{}\inferrule{\mbox{{\isacharquery}M\ {\isacharequal}\ {\isacharquery}N}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isacharequal}\ {\isacharquery}N\ {\isasymLongrightarrow}\ {\isacharquery}f\ x\ {\isacharequal}\ {\isacharquery}g\ x}}{\mbox{Let\ {\isacharquery}M\ {\isacharquery}f\ {\isacharequal}\ Let\ {\isacharquery}N\ {\isacharquery}g}}}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Data Types% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +For each \cmd{datatype} definition, a congruence rule for the case + combinator is registeres automatically. Here are the rules for + \isa{nat} and \isa{list}: + +\begin{center}\isa{\mbox{}\inferrule{\mbox{{\isacharquery}M\ {\isacharequal}\ {\isacharquery}M{\isacharprime}}\\\ \mbox{{\isacharquery}M{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ {\isacharquery}f{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharequal}\ {\isacharquery}g{\isadigit{1}}{\isachardot}{\isadigit{0}}}\\\ \mbox{{\isasymAnd}nat{\isachardot}\ {\isacharquery}M{\isacharprime}\ {\isacharequal}\ Suc\ nat\ {\isasymLongrightarrow}\ {\isacharquery}f{\isadigit{2}}{\isachardot}{\isadigit{0}}\ nat\ {\isacharequal}\ {\isacharquery}g{\isadigit{2}}{\isachardot}{\isadigit{0}}\ nat}}{\mbox{nat{\isacharunderscore}case\ {\isacharquery}f{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharquery}f{\isadigit{2}}{\isachardot}{\isadigit{0}}\ {\isacharquery}M\ {\isacharequal}\ nat{\isacharunderscore}case\ {\isacharquery}g{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharquery}g{\isadigit{2}}{\isachardot}{\isadigit{0}}\ {\isacharquery}M{\isacharprime}}}}\end{center} + +\begin{center}\isa{\mbox{}\inferrule{\mbox{{\isacharquery}M\ {\isacharequal}\ {\isacharquery}M{\isacharprime}}\\\ \mbox{{\isacharquery}M{\isacharprime}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ {\isacharquery}f{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharequal}\ {\isacharquery}g{\isadigit{1}}{\isachardot}{\isadigit{0}}}\\\ \mbox{{\isasymAnd}a\ list{\isachardot}\ {\isacharquery}M{\isacharprime}\ {\isacharequal}\ a\ {\isacharhash}\ list\ {\isasymLongrightarrow}\ {\isacharquery}f{\isadigit{2}}{\isachardot}{\isadigit{0}}\ a\ list\ {\isacharequal}\ {\isacharquery}g{\isadigit{2}}{\isachardot}{\isadigit{0}}\ a\ list}}{\mbox{list{\isacharunderscore}case\ {\isacharquery}f{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharquery}f{\isadigit{2}}{\isachardot}{\isadigit{0}}\ {\isacharquery}M\ {\isacharequal}\ list{\isacharunderscore}case\ {\isacharquery}g{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharquery}g{\isadigit{2}}{\isachardot}{\isadigit{0}}\ {\isacharquery}M{\isacharprime}}}}\end{center}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{List combinators% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\isa{\mbox{}\inferrule{\mbox{{\isacharquery}xs\ {\isacharequal}\ {\isacharquery}ys}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ {\isacharquery}ys\ {\isasymLongrightarrow}\ {\isacharquery}f\ x\ {\isacharequal}\ {\isacharquery}g\ x}}{\mbox{map\ {\isacharquery}f\ {\isacharquery}xs\ {\isacharequal}\ map\ {\isacharquery}g\ {\isacharquery}ys}}} + +\isa{\mbox{}\inferrule{\mbox{{\isacharquery}xs\ {\isacharequal}\ {\isacharquery}ys}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ {\isacharquery}ys\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ {\isacharequal}\ {\isacharquery}Q\ x}}{\mbox{filter\ {\isacharquery}P\ {\isacharquery}xs\ {\isacharequal}\ filter\ {\isacharquery}Q\ {\isacharquery}ys}}} + +\isa{\mbox{}\inferrule{\mbox{{\isacharquery}a\ {\isacharequal}\ {\isacharquery}b}\\\ \mbox{{\isacharquery}l\ {\isacharequal}\ {\isacharquery}k}\\\ \mbox{{\isasymAnd}a\ x{\isachardot}\ x\ {\isasymin}\ set\ {\isacharquery}l\ {\isasymLongrightarrow}\ {\isacharquery}f\ x\ a\ {\isacharequal}\ {\isacharquery}g\ x\ a}}{\mbox{foldr\ {\isacharquery}f\ {\isacharquery}l\ {\isacharquery}a\ {\isacharequal}\ foldr\ {\isacharquery}g\ {\isacharquery}k\ {\isacharquery}b}}} + +\isa{\mbox{}\inferrule{\mbox{{\isacharquery}a\ {\isacharequal}\ {\isacharquery}b}\\\ \mbox{{\isacharquery}l\ {\isacharequal}\ {\isacharquery}k}\\\ \mbox{{\isasymAnd}a\ x{\isachardot}\ x\ {\isasymin}\ set\ {\isacharquery}l\ {\isasymLongrightarrow}\ {\isacharquery}f\ a\ x\ {\isacharequal}\ {\isacharquery}g\ a\ x}}{\mbox{foldl\ {\isacharquery}f\ {\isacharquery}a\ {\isacharquery}l\ {\isacharequal}\ foldl\ {\isacharquery}g\ {\isacharquery}b\ {\isacharquery}k}}} + +Similar: takewhile, dropwhile% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Sets% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\isa{\mbox{}\inferrule{\mbox{{\isacharquery}A\ {\isacharequal}\ {\isacharquery}B}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ {\isacharquery}B\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ {\isacharequal}\ {\isacharquery}Q\ x}}{\mbox{{\isacharparenleft}{\isasymforall}x{\isasymin}{\isacharquery}A{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}x{\isasymin}{\isacharquery}B{\isachardot}\ {\isacharquery}Q\ x{\isacharparenright}}}} + +\isa{\mbox{}\inferrule{\mbox{{\isacharquery}A\ {\isacharequal}\ {\isacharquery}B}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ {\isacharquery}B\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ {\isacharequal}\ {\isacharquery}Q\ x}}{\mbox{{\isacharparenleft}{\isasymexists}x{\isasymin}{\isacharquery}A{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}x{\isasymin}{\isacharquery}B{\isachardot}\ {\isacharquery}Q\ x{\isacharparenright}}}} + +\isa{\mbox{}\inferrule{\mbox{{\isacharquery}A\ {\isacharequal}\ {\isacharquery}B}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ {\isacharquery}B\ {\isasymLongrightarrow}\ {\isacharquery}C\ x\ {\isacharequal}\ {\isacharquery}D\ x}}{\mbox{{\isacharparenleft}{\isasymUnion}\isactrlbsub x{\isasymin}{\isacharquery}A\isactrlesub \ {\isacharquery}C\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymUnion}\isactrlbsub x{\isasymin}{\isacharquery}B\isactrlesub \ {\isacharquery}D\ x{\isacharparenright}}}} + +\isa{\mbox{}\inferrule{\mbox{{\isacharquery}A\ {\isacharequal}\ {\isacharquery}B}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ {\isacharquery}B\ {\isasymLongrightarrow}\ {\isacharquery}C\ x\ {\isacharequal}\ {\isacharquery}D\ x}}{\mbox{{\isacharparenleft}{\isasymInter}\isactrlbsub x{\isasymin}{\isacharquery}A\isactrlesub \ {\isacharquery}C\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymInter}\isactrlbsub x{\isasymin}{\isacharquery}B\isactrlesub \ {\isacharquery}D\ x{\isacharparenright}}}} + +\isa{\mbox{}\inferrule{\mbox{{\isacharquery}M\ {\isacharequal}\ {\isacharquery}N}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ {\isacharquery}N\ {\isasymLongrightarrow}\ {\isacharquery}f\ x\ {\isacharequal}\ {\isacharquery}g\ x}}{\mbox{{\isacharquery}f\ {\isacharbackquote}\ {\isacharquery}M\ {\isacharequal}\ {\isacharquery}g\ {\isacharbackquote}\ {\isacharquery}N}}}% \end{isamarkuptext}% \isamarkuptrue% % diff -r b469cf6dc531 -r 4b0bf04a4d68 doc-src/IsarAdvanced/Functions/Thy/document/isabelle.sty --- a/doc-src/IsarAdvanced/Functions/Thy/document/isabelle.sty Thu May 17 23:00:06 2007 +0200 +++ b/doc-src/IsarAdvanced/Functions/Thy/document/isabelle.sty Thu May 17 23:03:47 2007 +0200 @@ -31,6 +31,7 @@ \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup} \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}} +\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}} \newdimen\isa@parindent\newdimen\isa@parskip diff -r b469cf6dc531 -r 4b0bf04a4d68 doc-src/IsarAdvanced/Functions/functions.tex --- a/doc-src/IsarAdvanced/Functions/functions.tex Thu May 17 23:00:06 2007 +0200 +++ b/doc-src/IsarAdvanced/Functions/functions.tex Thu May 17 23:03:47 2007 +0200 @@ -1,14 +1,21 @@ %% $Id$ -\documentclass[12pt,a4paper,fleqn]{report} +\documentclass[11pt,a4paper,fleqn]{article} +\textwidth 15.93cm +\textheight 24cm +\oddsidemargin 0.0cm +\evensidemargin 0.0cm +\topmargin 0.0cm + \usepackage{latexsym,graphicx} -\usepackage{listings} \usepackage[refpage]{nomencl} \usepackage{../../iman,../../extra,../../isar,../../proof} \usepackage{Thy/document/isabelle,Thy/document/isabellesym} \usepackage{style} \usepackage{Thy/document/pdfsetup} +\usepackage{mathpartir} +\usepackage{amsthm} \newcommand{\cmd}[1]{\isacommand{#1}} @@ -45,17 +52,15 @@ \newcommand{\strong}[1]{{\bfseries #1}} \newcommand{\fixme}[1][!]{\strong{FIXME: #1}} -\lstset{basicstyle=\scriptsize\ttfamily, keywordstyle=\itshape, commentstyle=\itshape\sffamily, frame=shadowbox} -\newcommand{\lstsml}[1]{\lstset{language=ML}\lstinputlisting{#1}} -\newcommand{\lsthaskell}[1]{\lstset{language=Haskell}\lstinputlisting{#1}} +\newtheorem{exercise}{Exercise}{\bf}{\itshape} +%\newtheorem*{thmstar}{Theorem}{\bf}{\itshape} \hyphenation{Isabelle} \hyphenation{Isar} \isadroptag{theory} -\title{\includegraphics[scale=0.5]{isabelle_isar} - \\[4ex] Defining Recursive Functions in Isabelle/HOL} -\author{\emph{Alexander Krauss}} +\title{Defining Recursive Functions in Isabelle/HOL} +\author{Alexander Krauss} \isabellestyle{tt} @@ -66,16 +71,19 @@ \begin{abstract} This tutorial describes the use of the new \emph{function} package, - starting with very simple examples and the proceeding to the more - intricate ones. No familiarity with other definition facilities is - assumed. + which provides general recursive function definitions for Isabelle/HOL. + + +% starting with very simple examples and the proceeding to the more +% intricate ones. \end{abstract} -\thispagestyle{empty}\clearpage +%\thispagestyle{empty}\clearpage -\pagenumbering{roman} -\clearfirst +%\pagenumbering{roman} +%\clearfirst +\input{intro.tex} \input{Thy/document/Functions.tex} \begingroup diff -r b469cf6dc531 -r 4b0bf04a4d68 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu May 17 23:00:06 2007 +0200 +++ b/src/HOL/IsaMakefile Thu May 17 23:03:47 2007 +0200 @@ -636,9 +636,9 @@ ex/Reflection.thy ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy \ ex/Records.thy ex/Reflected_Presburger.thy ex/Refute_Examples.thy \ ex/SAT_Examples.thy ex/svc_oracle.ML ex/SVC_Oracle.thy \ - ex/Sudoku.thy ex/Tarski.thy ex/document/root.bib ex/document/root.tex \ - ex/mesontest2.ML ex/mesontest2.thy ex/reflection.ML ex/set.thy \ - ex/svc_funcs.ML ex/svc_test.thy Library/Parity.thy Library/GCD.thy + ex/Sudoku.thy ex/Tarski.thy ex/Unification.thy ex/document/root.bib \ + ex/document/root.tex ex/mesontest2.ML ex/mesontest2.thy ex/reflection.ML \ + ex/set.thy ex/svc_funcs.ML ex/svc_test.thy Library/Parity.thy Library/GCD.thy @$(ISATOOL) usedir $(OUT)/HOL ex