Quelle Refinement.thy Sprache: Isabelle

theory
imports
begin

section \<open>Program and datatype refinement \label{sec:refinement}\<close>

text
  Codespecifies (type
  allows choose code and datatype constructors,
  given that some very basicthese be implementedred-black-treestheory
  flexibility opens up java.lang.StringIndexOutOfBoundsException: Index 28 out of bounds for length 8
  the scope and quality of generated code dramatically.
\<close>

subsection \<open>Program refinement\<close>

text \<open>
  Program refinement works by choosing appropriate code equations
  explicitly (cf.~\secref{sec:equations}); as example, we use Fibonacci
  numbers:
\<close>

fun %quote fib :: "nat \ nat" where
    "fib 0 = 0"
  | "fib (Suc 0) = Suc 0"
  | "fib (Suc (Suc n)) = fib n + fib (Suc n)"

text \<open>
  \noindent The runtime of the corresponding code grows exponential due
  to two recursive calls:
\<close>

text %quote \<open>
  @{code_stmts fib constant: fib (Haskell)}
\<close>

text \<open>
  \noindent A more efficient implementation would use dynamic
  programming, e.g.~sharing of common intermediate results between
  recursive calls.  This idea is expressed by an auxiliary operation
  which computes a Fibonacci number and its successor simultaneously:
\<close>

definition %quote fib_step :: "nat \ nat \ nat" where
  "fib_step n = (fib (Suc n), fib n)"

text \<open>
  \noindent This operation can be implemented by recursion using
  dynamic programming:
\<close>

lemma %quote [code]:
  "fib_step 0 = (Suc 0, 0)"
  "fib_step (Suc n) = (let (m, q) = fib_step n in (m + q, m))"
  by (simp_all add: fib_step_def)

text \<open>
  \noindent What remains is to implement \<^const>\<open>fib\<close> by \<^const>\<open>fib_step\<close> as follows:
\<close>

lemma %quote [code]:
  "fib 0 = 0"
  "fib (Suc n) = fst (fib_step n)"
  by (simp_all add: fib_step_def)

text \<open>
  \noindent The resulting code shows only linear growth of runtime:
\<close>

text %quote \<open>
  @{code_stmts fib constant: fib fib_step (Haskell)}
\<close>

subsection \<open>Datatype refinement\<close>

text \<open>
  Selecting specific code equations \emph{and} datatype constructors
  leads to datatype refinement.  As an example, we will develop an
  alternative representation of the queue example given in
  \secref{sec:queue_example}.  The amortised representation is
  convenient for generating code but exposes its \qt{implementation}
  details, which may be cumbersome when proving theorems about it.
  Therefore, here is a simple, straightforward representation of
  queues:
\<close>

datatype %quote 'a queue = Queue "'a list"

definition %quote empty :: "'a queue" where
  "empty = Queue []"

primrec %quote enqueue :: "'a \ 'a queue \ 'a queue" where
  "enqueue x (Queue xs) = Queue (xs @ [x])"

fun %quote dequeue :: "'a queue \ 'a option \ 'a queue" where
    "dequeue (Queue []) = (None, Queue [])"
  | "dequeue (Queue (x # xs)) = (Some x, Queue xs)"

text \<open>
  \noindent This we can use directly for proving;  for executing,
  we provide an alternative characterisation:
\<close>

definition %quote AQueue :: "'a list \ 'a list \ 'a queue" where
  "AQueue xs ys = Queue (ys @ rev xs)"

code_datatype %quote AQueue

text \<open>
  \noindent Here we define a \qt{constructor} \<^const>\<open>AQueue\<close> which
  is defined in terms of \<open>Queue\<close> and interprets its arguments
  according to what the \emph{content} of an amortised queue is supposed
  to be.

  The prerequisite for datatype constructors is only syntactical: a
  constructor must be of type \<open>\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^sub>1 \<dots> \<alpha>\<^sub>n\<close> where \<open>{\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n}\<close> is exactly the set of \emph{all} type variables in
  \<open>\<tau>\<close>; then \<open>\<kappa>\<close> is its corresponding datatype.  The
  HOL datatype package by default registers any new datatype with its
  constructors, but this may be changed using @{command_def
  code_datatype}; the currently chosen constructors can be inspected
  using the @{command print_codesetup} command.

  Equipped with this, we are able to prove the following equations
  for our primitive queue operations which \qt{implement} the simple
  queues in an amortised fashion:
\<close>

lemma %quote empty_AQueue [code]:
  "empty = AQueue [] []"
  by (simp add: AQueue_def empty_def)

lemma %quote enqueue_AQueue [code]:
  "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
  by (simp add: AQueue_def)

lemma %quote dequeue_AQueue [code]:
  "dequeue (AQueue xs []) =
    (if xs = [] then (None, AQueue [] [])
    else dequeue (AQueue [] (rev xs)))"
  "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
  by (simp_all add: AQueue_def)

text \<open>
  \noindent It is good style, although no absolute requirement, to
  provide code equations for the original artefacts of the implemented
  type, if possible; in our case, these are the datatype constructor
  \<^const>\<open>Queue\<close> and the case combinator \<^const>\<open>case_queue\<close>:
\<close>

lemma %quote Queue_AQueue [code]:
  "Queue = AQueue []"
  by (simp add: AQueue_def fun_eq_iff)

lemma %quote case_queue_AQueue [code]:
  "case_queue f (AQueue xs ys) = f (ys @ rev xs)"
  by (simp add: AQueue_def)

text \<open>
  \noindent The resulting code looks as expected:
\<close>

text %quote \<open>
  @{code_stmts empty enqueue dequeue Queue case_queue (SML)}
\<close>

text \<open>
  The same techniques can also be applied to types which are not
  specified as datatypes, e.g.~type \<^typ>\<open>int\<close> is originally specified
  as quotient type by means of @{command_def typedef}, but for code
  generation constants allowing construction of binary numeral values
  are used as constructors for \<^typ>\<open>int\<close>.

  This approach however fails if the representation of a type demands
  invariants; this issue is discussed in the next section.
\<close>

subsection \<open>Datatype refinement involving invariants \label{sec:invariant}\<close>

text \<open>
  Datatype representation involving invariants require a dedicated
  setup for the type and its primitive operations.  As a running
  example, we implement a type \<^typ>\<open>'a dlist\<close> of lists consisting
  of distinct elements.

  The specification of \<^typ>\<open>'a dlist\<close> itself can be found in theory
  \<^theory>\<open>HOL-Library.Dlist\<close>.

  The first step is to decide on which representation the abstract
  type (in our example \<^typ>\<open>'a dlist\<close>) should be implemented.
  Here we choose \<^typ>\<open>'a list\<close>.  Then a conversion from the concrete
  type to the abstract type must be specified, here:
\<close>

text %quote \<open>
  \<^term_type>\<open>Dlist\<close>
\<close>

text \<open>
  \noindent Next follows the specification of a suitable \emph{projection},
  i.e.~a conversion from abstract to concrete type:
\<close>

text %quote \<open>
  \<^term_type>\<open>list_of_dlist\<close>
\<close>

text \<open>
  \noindent This projection must be specified such that the following
  \emph{abstract datatype certificate} can be proven:
\<close>

lemma %quote [code abstype]:
  "Dlist (list_of_dlist dxs) = dxs"
  by (fact Dlist_list_of_dlist)

text \<open>
  \noindent Note that so far the invariant on representations
  (\<^term_type>\<open>distinct\<close>) has never been mentioned explicitly:
  the invariant is only referred to implicitly: all values in
  set \<^term>\<open>{xs. list_of_dlist (Dlist xs) = xs}\<close> are invariant,
  and in our example this is exactly \<^term>\<open>{xs. distinct xs}\<close>.

  The primitive operations on \<^typ>\<open>'a dlist\<close> are specified
  indirectly using the projection \<^const>\<open>list_of_dlist\<close>.  For
  the empty \<open>dlist\<close>, \<^const>\<open>Dlist.empty\<close>, we finally want
  the code equation
\<close>

text %quote \<open>
  \<^term>\<open>Dlist.empty = Dlist []\<close>
\<close>

text \<open>
  \noindent This we have to prove indirectly as follows:
\<close>

lemma %quote [code]:
  "list_of_dlist Dlist.empty = []"
  by (fact list_of_dlist_empty)

text \<open>
  \noindent This equation logically encodes both the desired code
  equation and that the expression \<^const>\<open>Dlist\<close> is applied to obeys
  the implicit invariant.  Equations for insertion and removal are
  similar:
\<close>

lemma %quote [code]:
  "list_of_dlist (Dlist.insert x dxs) = List.insert x (list_of_dlist dxs)"
  by (fact list_of_dlist_insert)

lemma %quote [code]:
  "list_of_dlist (Dlist.remove x dxs) = remove1 x (list_of_dlist dxs)"
  by (fact list_of_dlist_remove)

text \<open>
  \noindent Then the corresponding code is as follows:
\<close>

text %quote \<open>
  @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (SML)}
\<close>

text \<open>
  To reduce manual work for datatype refinement, @{command_def lift_definition}
  is a valuable tool.  See the corresponding section in \<^cite>\<open>"isabelle-isar-ref"\<close>.

  See further \<^cite>\<open>"Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement"\<close>
  for the meta theory of datatype refinement involving invariants.

  Typical data structures implemented by representations involving
  invariants are available in the library, theory \<^theory>\<open>HOL-Library.Mapping\<close>
  specifies key-value-mappings (type \<^typ>\<open>('a, 'b) mapping\<close>);
  these can be implemented by red-black-trees (theory \<^theory>\<open>HOL-Library.RBT\<close>).
\<close>

end

quality100%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.