Quelle  Partial.thy

(*<*)theory Partial imports While_Combinator begin(*>*)

text‹\noindent Throughout this tutorial, we have emphasized
  all functions in HOL are total. We cannot hope to define
  partial functions, but must make them total. A straightforward
  is to lift the result type of the function from $\tau$ to
 \tau$~‹option› (see \ref{sec:option}), where @{term None} is
  if the function is applied to an argument not in its
 . Function @{term assoc} in \S\ref{sec:Trie} is a simple example.
  do not pursue this schema further because it should be clear
  it works. Its main drawback is that the result of such a lifted
  has to be unpacked first before it can be processed
 . Its main advantage is that you can distinguish if the
  was applied to an argument in its domain or not. If you do
  need to make this distinction, for example because the function is
  used outside its domain, it is easier to work with
 emph{underdefined}\index{functions!underdefined} functions: for
  arguments we only know that a result exists, but we do not
  what it is. When defining functions that are normally considered
 , underdefinedness turns out to be a very reasonable
 .

  have already seen an instance of underdefinedness by means of
 -exhaustive pattern matching: the definition of @{term last} in
 S\ref{sec:fun}. The same is allowed for \isacommand{primrec}
 ›

consts hd :: "'a list ==> 'a"
primrec "hd (x#xs) = x"

text‹\noindent
  it generates a warning.
  ordinary definitions allow underdefinedness, this time by means of
 :
 ›

definition subtract :: "nat ==> nat ==> nat" where
"n ≤ m ==> subtract m n ≡ m - n"

text‹
  rest of this section is devoted to the question of how to define
  recursive functions by other means than non-exhaustive pattern
 .
 ›

subsubsection‹Guarded Recursion›

text‹
 index{recursion!guarded}%
  \isacommand{primrec} nor \isacommand{recdef} allow to
  an equation with a condition in the way ordinary definitions do
 see @{const subtract} above). Instead we have to move the condition over
  the right-hand side of the equation. Given a partial function $f$
  should satisfy the recursion equation $f(x) = t$ over its domain
 dom(f)$, we turn this into the \isacommand{recdef}
 {prop[display]"f(x) = (if x ∈ dom(f) then t else arbitrary)"}
  @{term arbitrary} is a predeclared constant of type @{typ 'a}
  has no definition. Thus we know nothing about its value,
  is ideal for specifying underdefined functions on top of it.

  a simple example we define division on @{typ nat}:
 ›

consts divi :: "nat × nat ==> nat"
recdef divi "measure(λ(m,n). m)"
  "divi(m,0) = arbitrary"
  "divi(m,n) = (if m < n then 0 else divi(m-n,n)+1)"

text‹\noindent Of course we could also have defined
 {term"divi(m,0)"} to be some specific number, for example 0. The
  option is chosen for the predefined ‹div› function, which
  proofs at the expense of deviating from the
  mathematical division function.

  a more substantial example we consider the problem of searching a graph.
  simplicity our graph is given by a function @{term f} of
  @{typ"'a ==> 'a"} which
  each node to its successor; the graph has out-degree 1.
  task is to find the end of a chain, modelled by a node pointing to
 . Here is a first attempt:
 {prop[display]"find(f,x) = (if f x = x then x else find(f, f x))"}
  may be viewed as a fixed point finder or as the second half of the well
  \emph{Union-Find} algorithm.
  snag is that it may not terminate if @{term f} has non-trivial cycles.
  differently, the relation
 ›

definition step1 :: "('a ==> 'a) ==> ('a × 'a)set" where
  "step1 f ≡ {(y,x). y = f x ∧ y ≠ x}"

text‹\noindent
  be well-founded. Thus we make the following definition:
 ›

consts find :: "('a ==> 'a) × 'a ==> 'a"
recdef find "same_fst (λf. wf(step1 f)) step1"
  "find(f,x) = (if wf(step1 f)
                then if f x = x then x else find(f, f x)
                else arbitrary)"
(hints recdef_simp: step1_def)

text‹\noindent
  recursion equation itself should be clear enough: it is our aborted
  attempt augmented with a check that there are no non-trivial loops.
  express the required well-founded relation we employ the
  combinator @{term same_fst} of type
 {text[display]"('a ==> bool) ==> ('a ==> ('b×'b)set) ==> (('a×'b) × ('a×'b))set"}
  as
 {thm[display]same_fst_def[no_vars]}
  combinator is designed for
  functions on pairs where the first component of the argument is
  unchanged to all recursive calls. Given a constraint on the first
  and a relation on the second component, @{term same_fst} builds the
  relation on pairs. The theorem
 {thm[display]wf_same_fst[no_vars]}
  known to the well-foundedness prover of \isacommand{recdef}. Thus
 -foundedness of the relation given to \isacommand{recdef} is immediate.
 , each recursive call descends along that relation: the first
  stays unchanged and the second one descends along @{term"step1
 "}. The proof requires unfolding the definition of @{const step1},
  specified in the \isacommand{hints} above.

  you will then derive the following conditional variant from
  recursion equation:
 ›

lemma [simp]:
  "wf(step1 f) ==> find(f,x) = (if f x = x then x else find(f, f x))"
by simp

text‹\noindent Then you should disable the original recursion equation:›

declare find.simps[simp del]

text‹
  about such underdefined functions is like that for other
  functions. Here is a simple example of recursion induction:
 ›

lemma "wf(step1 f) ⟶ f(find(f,x)) = find(f,x)"
apply(induct_tac f x rule: find.induct)
apply simp
done

subsubsection‹The {\tt\slshape while} Combinator›

text‹If the recursive function happens to be tail recursive, its
  becomes a triviality if based on the predefined \cdx{while}
 . The latter lives in the Library theory \thydx{While_Combinator}.
  which is not part of {text Main} but needs to
  be included explicitly among the ancestor theories.

  @{term while} is of type ‹('a ==> bool) ==> ('a ==> 'a) ==> 'a›
  satisfies the recursion equation @{thm[display]while_unfold[no_vars]}
  is, @{term"while b c s"} is equivalent to the imperative program
 begin{verbatim}
 x := s; while b(x) do x := c(x); return x
 end{verbatim}
  general, @{term s} will be a tuple or record. As an example
  the following definition of function @{const find}:
 ›

definition find2 :: "('a ==> 'a) ==> 'a ==> 'a" where
  "find2 f x ≡
   fst(while (λ(x,x'). x' ≠ x) (λ(x,x'). (x',f x')) (x,f x))"

text‹\noindent
  loop operates on two ``local variables'' @{term x} and @{term x'}
  the ``current'' and the ``next'' value of function @{term f}.
  are initialized with the global @{term x} and @{term"f x"}. At the
  @{term fst} selects the local @{term x}.

  the definition of tail recursive functions via @{term while} avoids
  proofs, there is no free lunch. When proving properties of
  defined by @{term while}, termination rears its ugly head
 . Here is \tdx{while_rule}, the well known proof rule for total
  of loops expressed with @{term while}:
 {thm[display,margin=50]while_rule[no_vars]} @{term P} needs to be true of
  initial state @{term s} and invariant under @{term c} (premises 1
 ~2). The post-condition @{term Q} must become true when leaving the loop
 premise~3). And each loop iteration must descend along a well-founded
  @{term r} (premises 4 and~5).

  us now prove that @{const find2} does indeed find a fixed point. Instead
  induction we apply the above while rule, suitably instantiated.
  the final premise of @{thm[source]while_rule} is left unproved
  ‹auto› but falls to ‹simp›:
 ›

lemma lem: "wf(step1 f) ==>
  ∃y. while (λ(x,x'). x' ≠ x) (λ(x,x'). (x',f x')) (x,f x) = (y,y) ∧
       f y = y"
apply(rule_tac P = "λ(x,x'). x' = f x" and
               r = "inv_image (step1 f) fst" in while_rule)
apply auto
apply(simp add: inv_image_def step1_def)
done

text‹
  theorem itself is a simple consequence of this lemma:
 ›

theorem "wf(step1 f) ==> f(find2 f x) = find2 f x"
apply(drule_tac x = x in lem)
apply(auto simp add: find2_def)
done

text‹Let us conclude this section on partial functions by a
  of the merits of the @{term while} combinator. We have
  seen that the advantage of not having to
  a termination argument when defining a function via @{term
 } merely puts off the evil hour. On top of that, tail recursive
  tend to be more complicated to reason about. So why use
 {term while} at all? The only reason is executability: the recursion
  for @{term while} is a directly executable functional
 . This is in stark contrast to guarded recursion as introduced
  which requires an explicit test @{prop"x ∈ dom f"} in the
  body. Unless @{term dom} is trivial, this leads to a
  that is impossible to execute or prohibitively slow.
 , if you are aiming for an efficiently executable definition
  a partial function, you are likely to need @{term while}.
 ›

(*<*)end(*>*)