theory Partial_Functions
imports Setup "HOL-Library.Monad_Syntax"
begin

section ‹Partial Functions \label{sec:partial}›

text ‹We demonstrate three approaches to defining executable partial recursive functions,
 .e.\ functions that do not terminate for all inputs.
  main points are the definitions of the functions and the inductive proofs about them.

  concrete example represents a typical termination problem: following a data structure that
  contain cycles. We want to follow a mapping from ‹nat› to ‹nat› to the end
 until we leave its domain). The mapping is represented by a list ‹ns :: nat list›
  maps ‹n› to ‹ns ! n›.
  details of the example are in some sense irrelevant but make the exposition more realistic.
 , we hide most proofs or show only the characteristic opening.›

text ‹The list representation of the mapping can be abstracted to a relation.
  order @{term "(ns!n, n)"} is the order that @{const wf} expects.›

definition rel :: "nat list → (nat * nat) set" where
"rel ns = set(zip ns [0..<length ns])"

lemma finite_rel[simp]: "finite(rel ns)"
(*<*)by(simp add: rel_def)(*>*)

text ‹\noindent This relation should be acyclic
 to guarantee termination of the partial functions defined below.›


subsection ‹Tail recursion›

text ‹If a function is tail-recursive, an executable definition is easy:›

partial_function (tailrec) follow :: "nat list → nat → nat" where
"follow ns n = (if n < length ns then follow ns (ns!n) else n)"

text ‹Informing the code generator:›

declare follow.simps[code]

text ‹Now @{const follow} is executable:›

value "follow [1,2,3] 0"

text ‹For proofs about @{const follow} we need a @{const wf} relation on @{term "(ns,n)"} pairs
  decreases with each recursive call. The first component stays the same but must be acyclic.
  second component must decrease w.r.t @{const rel}:›

definition "rel_follow = same_fst (acyclic o rel) rel"

lemma wf_follow: "wf rel_follow"
(*<*)
by (auto intro: wf_same_fst simp: rel_follow_def finite_acyclic_wf)

text ‹A more explicit formulation of ‹rel_follow›:
  first component stays the same but must be acyclic.
  second component decreases w.r.t ‹rel›:›

lemma rel_follow_step:
  "[ m < length ms; acyclic (rel ms) ] ==> ((ms, ms ! m), (ms, m)) ∈ rel_follow"
by(force simp: rel_follow_def rel_def in_set_zip)
(*>*)

text ‹This is how you start an inductive proof about @{const follow} along @{const rel_follow}:›

lemma "acyclic(rel ms) ==> follow ms m = n ==> length ms ≤ n"
proof (induction "(ms,m)" arbitrary: m n rule: wf_induct_rule[OF wf_follow])
(*<*)
  case 1
  thus ?case using follow.simps rel_follow_step by fastforce
qed
(*>*)


subsection ‹Option›

text ‹If the function is not tail-recursive, not all is lost: if we rewrite it to return an ‹option›
 , it can still be defined. In this case @{term "Some x"} represents the result ‹x›
  @{term None} represents represents nontermination.
  example, counting the length of the chain represented by ‹ns› can be defined like this:›

partial_function (option) count :: "nat list → nat → nat option" where
"count ns n
= (if n < length ns then do {k ← count ns (ns!n); Some (k+1)} else Some 0)"

text ‹\noindent We use a Haskell-like ‹do› notation (import @{theory "HOL-Library.Monad_Syntax"})
  abbreviate the clumsy explicit

 noindent
 {term "case count ns (ns!n) of Some k → Some(k+1) | None → None"}.

 noindent
  branch ‹None → None› represents the requirement
  nontermination of a recursive call must lead to nontermination of the function.

  we can prove that @{const count} terminates for all acyclic maps:›

lemma "acyclic(rel ms) ==> ∃k. count ms m = Some k"
proof (induction "(ms,m)" arbitrary: ms m rule: wf_induct_rule[OF wf_follow])
(*<*)
  case 1
  thus ?case
    by (metis bind.bind_lunit count.simps rel_follow_step)
qed
(*>*)


subsection ‹Subtype›

text ‹In this approach we define a new type that contains only elements on which the function
  question terminates.
  our example that is the subtype of all ‹ns :: nat list› such that @{term "rel ns"} is acyclic.
  @{const follow} can be defined as a total function on that subtype.›

text ‹The subtype is not empty:›

lemma acyclic_rel_Nil: "acyclic(rel [])"
(*<*)by (simp add: rel_def acyclic_def)(*>*)

text ‹Definition of subtype ‹acyc›:›

typedef acyc = "{ns. acyclic(rel ns)}"
morphisms rep_acyc abs_acyc
using acyclic_rel_Nil by auto

text ‹\noindent This defines two functions @{term [source] "rep_acyc :: acyc → nat list"}
  @{const abs_acyc} ‹::› \mbox{@{typ "nat list → acyc"}}.
  @{const abs_acyc} is only defined on acyclic lists and not executable for that reason.
  ‹dlist› in Section~\ref{sec:partiality} is defined in the same manner.

  following command sets up infrastructure for lifting functions on @{typ "nat list"}
  @{typ acyc} (used by @{command_def lift_definition} below) cite‹"isabelle-isar-ref"›.›

setup_lifting type_definition_acyc

text ‹This is how @{const follow} can be defined on @{typ acyc}:›

function follow2 :: "acyc → nat → nat" where
"follow2 ac n
= (let ns = rep_acyc ac in if n < length ns then follow2 ac (ns!n) else n)"
by pat_completeness auto

text ‹Now we prepare for the termination proof.
 Relation ‹rel_follow2› is almost identical to @{const rel_follow}.›

definition "rel_follow2 = same_fst (acyclic o rel o rep_acyc) (rel o rep_acyc)"

lemma wf_follow2: "wf rel_follow2"
(*<*)
by (auto intro: wf_same_fst simp add: rel_follow2_def finite_acyclic_wf)

text ‹A more explicit formulation of ‹rel_follow2›:›

lemma rel_follow2_step:
  "[ ns = rep_acyc ac; m < length ns; acyclic (rel ns) ] ==> ((ac, ns ! m), (ac, m)) ∈ rel_follow2"
by(force simp add: rel_follow2_def rel_def in_set_zip)
(*>*)

text ‹Here comes the actual termination proof:›

termination follow2
proof
  show "wf rel_follow2"
(*<*)    by (auto intro: wf_same_fst simp add: rel_follow2_def finite_acyclic_wf)(*>*)

next
  show "∧ac n ns. [ ns = rep_acyc ac; n < length ns ]
              ==> ((ac, ns ! n), (ac, n)) ∈ rel_follow2"
(*<*)    using rel_follow2_step rep_acyc by simp(*>*)

qed

text ‹Inductive proofs about @{const follow2} can now simply use computation induction:›

lemma "follow2 ac m = n ==> length (rep_acyc ac) ≤ n"
proof (induction ac m arbitrary: n rule: follow2.induct)
(*<*)
  case 1
  thus ?case by (metis (full_types) follow2.simps linorder_not_le)
qed
(*>*)

text ‹A complication with the subtype approach is that injection into the subtype
 function ‹abs_acyc› in our example) is not executable. But to call @{const follow2},
  need an argument of type ‹acyc› and we need to obtain it in an executable manner.
  are two approaches.›

text ‹In the first approach we check wellformedness (i.e. acyclicity) explicitly.
  check needs to be executable (which @{const acyclic} and @{const rel} are).
  the check fails, @{term "[]"} is returned (which is acyclic).›

lift_definition is_acyc :: "nat list → acyc" is 
  "λns. if acyclic(rel ns) then ns else []"
(*<*)by (auto simp: acyclic_rel_Nil)(*>*)

text ‹\noindent This works because we can easily prove that for any ‹ns›,
 the ‹λ›-term produces an acyclic list.
  it requires the possibly expensive check @{prop "acyclic(rel ns)"}.›

definition "follow_test ns n = follow2 (is_acyc ns) n"

text ‹The relation is acyclic (a chain):›

value "follow_test [1,2,3] 1"

text ‹In the second approach, wellformedness of the argument is guaranteed by construction.
  our example ‹[1..<n+1]› represents an acyclic chain ‹i ↦ i+1››

lemma acyclic_chain: "acyclic (rel [1..<n+1])"
(*<*)
apply(induction n)
 apply (simp add: rel_def acyclic_def)
apply (auto simp add: rel_def)
by (metis atLeast_upt lessI lessThan_iff order_less_asym' rtranclE set_zip_rightD)
(*>*)

text ‹›
lift_definition acyc_chain :: "nat → acyc" is "λn. [1..<n+1]"
(*<*)by (use acyclic_chain in auto)(*>*)

text ‹›
definition "follow_chain m n = follow2 (acyc_chain m) n"

value "follow_chain 5 1"

text ‹The subtype approach requires neither tail-recursion nor ‹option› but you cannot easily modify
  of the subtype except via existing functions on the subtype. Otherwise you need to inject
  value into the subtype and that injection is not computable.
 ›
(*<*)
text ‹The problem with subtypes: the Abs function must not be used explicitly.
  can be avoided by using ‹lift_definition›. Example:›

typedef nat1 = "{n::nat. n > 0}"
by auto
print_theorems

setup_lifting type_definition_nat1

(* just boiler plate *)
lift_definition mk1 :: "nat → nat1" is 
  "λn. if n>0 then n else 1"
by auto

lift_definition g :: "nat1 → nat1" is
"λn. if n ≥ 2 then n-1 else n"
by auto
print_theorems
text ‹This generates
 ‹g.rep_eq: Rep_nat1 (g x) = (if 2 ≤ Rep_nat1 x then Rep_nat1 x - 1 else Rep_nat1 x)›
  is acceptable as an abstract code eqn. The manual definition of
 ‹g n1 = (let n = Rep_nat1 n1 in if 2 ≤ n then Abs_nat1 (n - 1) else Abs_nat1 n)›
  non-executable but ‹g.rep_eq› can be derived from it.›

value "g (mk1 3)"

text ‹However, this trick does not work when passing an Abs-term as an argument,
  in a recursive call, because the Abs-term is `hidden' by the function call.›
(*>*)
end