Theory Introduction

(*  Title: A efficiently computable formalisation of Dijkstra's algorithm       
    Author: Benedikt Nordhoff <bnord01 at>, 
            Peter Lammich <lammich at>
section "Introduction and Overview"

theory Introduction 
imports Main

text_raw ‹\label{thy:Introduction}›
text ‹
  Dijkstra's algorithm cite"Dijk59" is an algorithm used to
  find shortest paths from one given vertex to all other vertices in a
  non-negatively weighted graph.  
  The implementation of the algorithm is meant to be an application
  of our extensions to the Isabelle Collections Framework (ICF)
  cite"L09_collections" and "LL10" and "NKP10". Moreover, it serves as a test case 
  for our data refinement framework cite"refinement_framework".
  We use ICF-Maps to efficiently represent the graph and
  result and the newly introduced unique priority queues for the work

  For a documentation of the refinement framework see cite"refinement_framework",
  that also contains a userguide and some simpler examples.

  The development utilizes a stepwise refinement approach. Starting from an
  abstract algorithm that has a nice correctness proof, we stepwise refine
  the algorithm until we end up with an efficient implementation, for that 
  we generate code using Isabelle/HOL's code generatorcite"Haft09" and "HaNi10".
  \paragraph{Structure of the Submission.}
  The abstract version of the algorithm with the correctness proof, as well
  as the main refinement steps are contained in the theory \texttt{Dijkstra}.
  The refinement steps involving the ICF and code generation are contained in
  The theory \texttt{Infty} contains an extension of numbers with an infinity
  The theory \texttt{Graph} contains a formalization of graphs, paths, and
  related concepts.
  The theories \texttt{GraphSpec,GraphGA,GraphByMap,HashGraphImpl} contain an
  ICF-style specification of graphs.
  The theory \texttt{Test} contains a small performance test on random graphs.
  It uses the ML-code generated by the code generator.