chapter \<open>Exercise Sheet -- Week 11\<close>

theory Exercise11
  imports 
    Main
    "HOL-Library.Code_Target_Numeral" 
begin

text \<open>In the lecture trees have been used to store sets. In this exercise
  sheet we will use trees to implement maps, i.e., 
  partial functions from keys to values.\<close>

section \<open>Exercise 1 -- 4 points\<close>

text \<open>In this first exercise, the aim is to adapt or extend the known 
  tree implementation so that it can be used to implement maps.\<close>

datatype ('a,'b) tree = Leaf | Node "('a,'b) tree" 'a 'b "('a,'b) tree" 

fun set_t :: "('a,'b) tree \<Rightarrow> 'a set" where
  "set_t Leaf = {}" 
| "set_t (Node l x y r) = set_t l \<union> {x} \<union> set_t r" 

inductive ordered :: "('a :: linorder,'b) tree \<Rightarrow> bool" where
  oLeaf: "ordered Leaf" 
| oNode: "ordered l \<Longrightarrow> ordered r 
  \<Longrightarrow> Ball (set_t l) (\<lambda> y. y < x)
  \<Longrightarrow> Ball (set_t r) (\<lambda> y. y > x)
  \<Longrightarrow> ordered (Node l x y r)" 

fun lookup_t :: "('a :: linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
  "lookup_t t k = undefined" 

fun update_t :: "'a :: linorder \<Rightarrow> 'b \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
  "update_t k v t = undefined" 

definition empty_t :: "('a,'b)tree" where
  "empty_t = undefined" 


typedef (overloaded) ('a,'b)otree = "{ t :: ('a :: linorder,'b)tree. ordered t}" 
  by (auto intro: oLeaf)

setup_lifting type_definition_otree

lift_definition lookup_o :: "('a :: linorder,'b)otree \<Rightarrow> 'a \<Rightarrow> 'b option" is lookup_t .
lift_definition empty_o :: "('a :: linorder,'b)otree" is empty_t sorry
lift_definition update_o :: "('a :: linorder,'b)otree \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b)otree" is "\<lambda> t k v. update_t k v t" sorry

lemma empty_o[simp]: "lookup_o empty_o = (\<lambda> _. None)" sorry
lemma update_o[simp]: "lookup_o (update_o t k v) = (lookup_o t)(k := Some v)" sorry


section \<open>Exercise 2 -- 2 points\<close>

text \<open>One of the limitations in Isabelle's mechanism for data refinement via
  the code generator is that only one type-constructor can be refined.
  So, in particular it is not possible to directly refine the type
  @{typ "'a :: linorder \<Rightarrow> 'b option"} to implement it via ordered trees.

  To this end, we first introduce a separate type for maps, a copy of 
  @{typ "'a :: linorder \<Rightarrow> 'b option"}, which then can be refined.
  Here, we provide three operations on map: lookup, empty-map, and update.\<close>

typedef ('a,'b)map = "{ f :: 'a \<Rightarrow> 'b option. True}" by auto

setup_lifting type_definition_map

lift_definition lookup :: "('a,'b)map \<Rightarrow> 'a \<Rightarrow> 'b option" is "\<lambda> f. f" .
lift_definition empty_map :: "('a,'b)map" is "\<lambda> _. None" by auto
lift_definition update :: "('a,'b)map \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b)map" is "\<lambda> f x y. f (x := Some y)" by auto 

text \<open>We now want to implement these operations by the tree based operations.
  To this end, we first need to disable the lifting-setup for @{typ "('a,'b)otree"},
  because ordered trees should not be decomposed into their representative type
  by @{method transfer}, but only @{typ "('a,'b)map"}.\<close>

lifting_forget otree.lifting

text \<open>Define a constant 
  @{term "map_o :: ('a :: linorder,'b)otree \<Rightarrow> ('a,'b)map"},
  to convert an ordered tree into a map, use this as a pseudo-constructor
  for the @{typ "('a,'b)map"}-type, and provide code-equations that
  implement @{const lookup}, @{const empty_map} and @{const update}.\<close>

lemma empty_om[simp]: "map_o empty_o = empty_map" sorry

lemma update_om[simp]: "map_o (update_o t k v) = update (map_o t) k v" sorry

lemma lookup_om[simp]: "lookup_o t = lookup (map_o t)" sorry

code_datatype map_o

lemma [code]: "update = undefined" sorry
lemma [code]: "empty_map = undefined" sorry
lemma [code]: "lookup = undefined" sorry

definition "test xs = foldr ((\<lambda> (k,v) m. update m k v)) xs empty_map"

(* value should display some tree, if you also solved exercise 1 *)
value (code) "test [(3 :: int,True), (8,False), (10,True), (7,True), (3,False)]" 

section \<open>Exercise 3 -- 4 points\<close>

text \<open>Application: Dijkstra's Shortest-Path-Algorithm\<close>

text \<open>Below you find a (hopefully) correct implementation of Dijkstra's
  algorithm to compute the distances from a starting node to all other
  nodes. The implementation works as follows. 
  As input to the main loop there are a weighted graph \<open>G\<close>, 
  a set of nodes \<open>done\<close> which already have their final distance computed,
  a map \<open>dist\<close> that stores the currently computed distances,
  and a list \<open>todo\<close> of nodes which still need to be processed;
  moreover \<open>todo\<close> also contains the distances of these nodes and 
  \<open>todo\<close> is sorted w.r.t. the distance.

  The function \<open>process\<close> takes a list of successor nodes of 
  some selected note (including the edge-weights), and it updates both
  the distance map and the todo-list.\<close>

fun remove_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  "remove_first f [] = []"
| "remove_first f (x # xs) = (if f x then xs else x # remove_first f xs)"

fun process :: "nat \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> nat option) \<Rightarrow> ('a \<times> nat) list \<Rightarrow> ('a \<times> nat) list \<Rightarrow> 
  ('a \<Rightarrow> nat option) \<times> ('a \<times> nat) list" where
  "process dn done dist todos [] = (dist, todos)" 
| "process dn done dist todos ((s,d_ns) # succs) = 
     \<comment> \<open>already processed node?\<close>
     (if s \<in> done then process dn done dist todos succs 
     \<comment> \<open>is there already some distance computed\<close>
       else let ds_new = dn + d_ns in case dist s of 
     \<comment> \<open>if not, store the distance and update todo-list\<close>
         None \<Rightarrow> process dn done (dist (s := Some ds_new)) (insort_key snd (s,ds_new) todos) succs
     \<comment> \<open>if yes, compare the new alternative and update on demand\<close>
       | Some ds \<Rightarrow> if ds \<le> ds_new then process dn done dist todos succs
               else let todos' = insort_key snd (s,ds_new) (remove_first ((=) s o fst) todos)
                  in process dn done (dist (s := Some ds_new)) todos' succs)" 

partial_function (tailrec) dijkstra_main :: 
  "('a \<Rightarrow> ('a \<times> nat) list) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> nat option) \<Rightarrow> ('a \<times> nat) list \<Rightarrow> ('a \<Rightarrow> nat option)" where
  [code]: "dijkstra_main G done dist todos = (case todos of [] \<Rightarrow> dist
   | ((n,dn) # todos') \<Rightarrow> let done' = insert n done;
       (dist',todo') = process dn done' dist todos' (G n)
     in dijkstra_main G done' dist' todo')" 

definition dijkstra :: "('a \<Rightarrow> ('a \<times> nat) list) \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> nat option)" where
  "dijkstra G start_node = dijkstra_main G {} ((\<lambda> _. None)(start_node := Some 0)) [(start_node,0)]" 

text \<open>Although @{const dijkstra} is already executable our aim is to create a more efficient version of
  the algorithm where the distance function of type @{typ "'a \<Rightarrow> nat option"} is implemented 
  via @{typ "('a,nat)map"} where then internally the ordered trees are used.

  To this end, we reformulate a variant of @{const process} which operates
  on maps.\<close>

fun process' :: "nat \<Rightarrow> 'a set \<Rightarrow> ('a,nat)map \<Rightarrow> ('a \<times> nat) list \<Rightarrow> ('a \<times> nat) list \<Rightarrow> 
  ('a,nat)map \<times> ('a \<times> nat) list" where
  "process' dn done dist todos [] = (dist, todos)" 
| "process' dn done dist todos ((s,d_ns) # succs) = 
     (if s \<in> done then process' dn done dist todos succs
       else let ds_new = dn + d_ns in case lookup dist s of 
         None \<Rightarrow> process' dn done (update dist s ds_new) (insort_key snd (s,ds_new) todos) succs
       | Some ds \<Rightarrow> if ds \<le> ds_new then process' dn done dist todos succs
               else let todos' = insort_key snd (s,ds_new) (remove_first ((=) s o fst) todos)
                  in process' dn done (update dist s ds_new) todos' succs)" 

text \<open>Task 1 (2 points): Establish the following relation-ship between @{const process} and @{const process'}.\<close>

lemma process_to_process': 
  "process dn done (lookup dist) todos succs = map_prod lookup id (process' dn done dist todos succs)" 
  sorry

text \<open>For the main-function, we just define the primed-version as an instance
  of the unprimed main-function.\<close>
definition dijkstra_main' :: "('a \<Rightarrow> ('a \<times> nat) list) \<Rightarrow> 'a set \<Rightarrow> ('a,nat)map \<Rightarrow> ('a \<times> nat) list \<Rightarrow> ('a \<Rightarrow> nat option)" where
  "dijkstra_main' G done dist todos = dijkstra_main G done (lookup dist) todos" 

text \<open>Task 2 (2 points): Complete the following code-equation which refers
  to @{const process'} and @{const dijkstra_main'} in the right-hand side,
  (and not to @{const process} and @{const dijkstra_main}), 
  and prove it ...\<close>

lemma dijkstra_main_simp[code]: "dijkstra_main' G done dist todos = undefined" 
  sorry

text \<open>... and similarly provide a code-equation for @{const dijkstra} which invokes 
  @{const dijkstra_main'} in its right-hand side.\<close>

lemma [code]: "dijkstra G s = dijkstra_main' G undefined undefined undefined" sorry 



text \<open>If you solved all exercises, the code should now contain a tree-based 
  implementation of the algorithm.\<close>
export_code dijkstra in Haskell module_name Dijkstra

definition test_graph :: "int \<Rightarrow> (int \<times> nat) list" where 
  "test_graph = (\<lambda> n. if n = 1 then [(2,7), (3,9), (6,14)] else
     if n = 2 then [(1,7), (3,10), (4,15)] else
     if n = 3 then [(1,9), (6,2), (4,11), (2,10)] else
     if n = 4 then [(3,11), (5,6), (2,15)] else
     if n = 5 then [(6,9), (4,6)] else
     if n = 6 then [(1,14), (3,2), (5,9)] else
      [])"  

value "let s = 1 in (''distances from node '', s, '' are '', 
  map (dijkstra test_graph s) [1..6])" 
end