Dijkstra - executable draft
authorlammich <lammich@in.tum.de>
Thu, 05 Jul 2018 18:32:01 +0200
changeset 69943 d5860fb818f1
parent 69942 3c344ec103ae
child 69944 de538a919227
Dijkstra - executable
Thys/Dijkstra.thy
Thys/RBT_Heap.thy
--- a/Thys/Dijkstra.thy	Wed Jul 04 19:00:02 2018 +0200
+++ b/Thys/Dijkstra.thy	Thu Jul 05 18:32:01 2018 +0200
@@ -1,6 +1,12 @@
 theory Dijkstra
-imports Main "HOL-Library.Extended_Nat" "HOL-Eisbach.Eisbach"
-  Prio_Map_Specs "HOL-Library.While_Combinator"
+imports 
+  Main 
+  "HOL-Library.Extended_Nat" 
+  "HOL-Eisbach.Eisbach"
+  Prio_Map_Specs 
+  "HOL-Library.While_Combinator"
+  RBT_Heap
+  "HOL-Data_Structures.RBT_Map"
 begin
 
 hide_const (open) connected
@@ -119,6 +125,7 @@
   fixes s :: 'v
 begin
   
+  (* TODO: Unused *)
   definition "relax \<equiv> \<lambda>(u,v) D. if D v > D u + w (u,v) then D(v := D u + w (u,v)) else D"
     
   definition "relax_adjs u D v \<equiv> min (D v) (D u + w (u,v))"
@@ -185,16 +192,16 @@
     assumes UNS: "u\<notin>S"
     assumes UNI: "D u < \<infinity>"
     assumes MIN: "\<forall>v. v\<notin>S \<longrightarrow> D u \<le> D v"
-    shows "D_invar (relax_adjs u D) (insert u S)"
+    shows "D_invar (relax_adjs u D) (Set.insert u S)"
     unfolding D_invar_def
   proof (intro conjI ballI allI)
     from maintain_upper_bound' I show "upper_bound (relax_adjs u D)" 
       unfolding D_invar_def by simp
   next
-    from I show "s \<in> insert u S" unfolding D_invar_def by simp
+    from I show "s \<in> Set.insert u S" unfolding D_invar_def by simp
   next
     fix v 
-    assume "v\<in>insert u S" 
+    assume "v\<in>Set.insert u S" 
     then show "relax_adjs u D v = \<delta> s v"
     proof safe
       assume "v\<in>S"
@@ -207,7 +214,7 @@
     qed
   next  
     fix v v'
-    assume "v\<in>insert u S" 
+    assume "v\<in>Set.insert u S" 
     then show "relax_adjs u D v' \<le> \<delta> s v + w (v, v')" "\<delta> s v < \<infinity>"
       (* TODO: Clean-up *)
       apply (auto simp: relax_adjs_def min_def)
@@ -264,7 +271,7 @@
     assumes I: "D_invar D S"
     assumes UNS: "u\<notin>S"
     assumes UNI: "D u < \<infinity>"
-    shows "unfinished_dnodes (insert u S) \<subset> unfinished_dnodes S"
+    shows "unfinished_dnodes (Set.insert u S) \<subset> unfinished_dnodes S"
   proof -
     from I have \<open>s\<in>S\<close> and UB: "upper_bound D" by (auto simp: D_invar_def)
   
@@ -367,8 +374,8 @@
     assumes UNS: "u\<notin>S"
     assumes UNI: "D u = enat du"
     
-    shows "coupling ((relax_adjs' u du V Q)(u:=None)) (V(u\<mapsto>du)) (relax_adjs u D) (insert u S)"
-      and "Q u = Some du" "V u = None"
+    shows "coupling ((relax_adjs' u du V Q)(u:=None)) (V(u\<mapsto>du)) (relax_adjs u D) (Set.insert u S)"
+      and "Q u = Some du" "V u = None" (* TODO: These are unused! *)
     using C unfolding coupling_def 
     apply -
     apply (all \<open>(intro ext conjI)?\<close>)
@@ -377,7 +384,7 @@
     assume \<alpha>: "D = Abs_enat \<circ> V ++ Q" "S = dom V" 
        and DD: "dom V \<inter> dom Q = {}"
      
-    show "insert u S = dom (V(u \<mapsto> du))"   
+    show "Set.insert u S = dom (V(u \<mapsto> du))"   
       by (auto simp: \<alpha>)
        
     show [simp]: "Q u = Some du" "V u = None" 
@@ -493,29 +500,30 @@
 end
   
 
+definition "edges w \<equiv> {(u,v) . w (u,v) \<noteq> \<infinity>}"
+
 locale adt_wgraph =
   fixes \<alpha> :: "'g \<Rightarrow> ('v,enat) wgraph"
     and invar :: "'g \<Rightarrow> bool"
     and succ :: "'g \<Rightarrow> 'v \<Rightarrow> (nat\<times>'v) list"
     and empty_graph :: 'g
     and add_edge :: "'v\<times>'v \<Rightarrow> nat \<Rightarrow> 'g \<Rightarrow> 'g"
-  assumes succ_correct: "invar g \<Longrightarrow> set (succ g v) = {(d,v). \<alpha> g (u,v) = enat d}"
+  assumes succ_correct: "invar g \<Longrightarrow> set (succ g u) = {(d,v). \<alpha> g (u,v) = enat d}"
   assumes empty_graph_correct:
     "invar empty_graph"
     "\<alpha> empty_graph = (\<lambda>_. \<infinity>)"
   assumes add_edge_correct:
-    "invar g \<Longrightarrow> invar (add_edge e d g)"
-    "invar g \<Longrightarrow> \<alpha> (add_edge e d g) = (\<alpha> g)(e:=enat d)"
+    "invar g \<Longrightarrow> \<alpha> g e = \<infinity> \<Longrightarrow> invar (add_edge e d g)"
+    "invar g \<Longrightarrow> \<alpha> g e = \<infinity> \<Longrightarrow> \<alpha> (add_edge e d g) = (\<alpha> g)(e:=enat d)"
 begin
 
-  definition "edges g \<equiv> {(u,v) . (\<alpha> g) (u,v) \<noteq> \<infinity>}"
   
   lemmas wgraph_specs = succ_correct empty_graph_correct add_edge_correct
   
 end
 
 locale adt_finite_wgraph = adt_wgraph where \<alpha>=\<alpha> for \<alpha> :: "'g \<Rightarrow> ('v,enat) wgraph" +
-  assumes finite: "finite (edges g)"
+  assumes finite: "invar g \<Longrightarrow> finite (edges (\<alpha> g))"
 
 locale Dijkstra_Impl_Adts = 
   G: adt_finite_wgraph G_invar G_succ G_empty G_add G_\<alpha>
@@ -545,16 +553,20 @@
 
 end
 
-locale Dijkstra_Impl = Dijkstra_Impl_Adts where G_\<alpha> = G_\<alpha>  
+locale Dijkstra_Impl_Defs = Dijkstra_Impl_Adts where G_\<alpha> = G_\<alpha>
   + Dijkstra \<open>G_\<alpha> g\<close> s
-  for G_\<alpha> :: "'g \<Rightarrow> ('v,enat) wgraph" and g s 
+  for G_\<alpha> :: "'g \<Rightarrow> ('v::linorder,enat) wgraph" and g s 
+
+
+locale Dijkstra_Impl = Dijkstra_Impl_Defs where G_\<alpha> = G_\<alpha>  
+  for G_\<alpha> :: "'g \<Rightarrow> ('v::linorder,enat) wgraph" 
   +
   assumes G_invar[simp]: "G_invar g"
 begin  
   lemma finite_all_dnodes[simp, intro!]: "finite all_dnodes"
   proof -  
-    have "all_dnodes \<subseteq> snd ` G.edges g"
-      by (fastforce simp: all_dnodes_def G.edges_def image_iff)
+    have "all_dnodes \<subseteq> snd ` edges (G_\<alpha> g)"
+      by (fastforce simp: all_dnodes_def edges_def image_iff)
     also have "finite \<dots>" by (auto simp: G.finite)
     finally (finite_subset) show ?thesis .
   qed
@@ -563,7 +575,7 @@
     using finite_subset[OF unfinished_nodes_subset] by auto
     
 
-  definition "Q_decrease_key v d Q \<equiv> case Q_lookup Q v of 
+  definition (in Dijkstra_Impl_Defs) "Q_decrease_key v d Q \<equiv> case Q_lookup Q v of 
     None \<Rightarrow> Q_update v d Q
   | Some d' \<Rightarrow> Q_update v (min d d') Q"
    
@@ -573,7 +585,9 @@
       and "Q_lookup (Q_decrease_key v d Q) = decrease_key v d (Q_lookup Q)"
     by (auto simp: Q_decrease_key_def decrease_key_def split: option.split)  
     
-  definition "Q_relax_adjs1 l du V Q = fold (\<lambda>(d,v) Q. if M_lookup V v \<noteq> None then Q else Q_decrease_key v (du+d) Q) l Q"
+  (* TODO: Local definition in lemma? *)  
+  definition (in Dijkstra_Impl_Defs)
+    "Q_relax_adjs1 l du V Q = fold (\<lambda>(d,v) Q. if M_lookup V v \<noteq> None then Q else Q_decrease_key v (du+d) Q) l Q"
   
   lemma Q_relax_adjs1[simp]:
     assumes "Q_invar Q"
@@ -584,7 +598,7 @@
     apply (clarsimp simp: Q_relax_adjs1_def relax_adjs''_def; safe; simp)
     done
 
-  definition "Q_relax_adjs u du V Q \<equiv> Q_relax_adjs1 (G_succ g u) du V Q"   
+  definition (in Dijkstra_Impl_Defs) "Q_relax_adjs u du V Q \<equiv> Q_relax_adjs1 (G_succ g u) du V Q"   
   
   lemma Q_relax_adjs[simp]:
     assumes [simp]: "Q_invar Q"
@@ -593,14 +607,16 @@
     apply (rule relax_adjs''_refine)
     by simp
     
-  definition "D_invar_impl Q V \<equiv> 
+  definition (in Dijkstra_Impl_Defs) "D_invar_impl Q V \<equiv> 
     Q_invar Q \<and> M_invar V \<and> D_invar' (Q_lookup Q) (M_lookup V)"
 
-  definition "Q_initQ \<equiv> fold (\<lambda>(d,v) Q. if s=v then Q else Q_update v d Q) (G_succ g s) Q_empty"
+  definition (in Dijkstra_Impl_Defs)
+    "Q_initQ s' \<equiv> fold (\<lambda>(d,v) Q. if s'=v then Q else Q_update v d Q) (G_succ g s') Q_empty"
     
+  definition (in Dijkstra_Impl_Defs) "test \<equiv> (Q_initQ s)"  
             
   lemma Q_init_Q[simp]:
-    shows "Q_invar Q_initQ" "Q_lookup Q_initQ = initQ"
+    shows "Q_invar (Q_initQ s)" "Q_lookup (Q_initQ s) = initQ"
   proof -
     let ?QiQ = "fold (\<lambda>(d,v) Q. if s=v then Q else Q_update v d Q)"
     let ?iQ' = "fold (\<lambda>(d,v) Q. if s=v then Q else Q(v\<mapsto>d))"
@@ -612,28 +628,29 @@
       apply clarsimp
       done
       
-    from aux show "Q_invar Q_initQ" unfolding Q_initQ_def by auto
+    from aux show "Q_invar (Q_initQ s)" unfolding Q_initQ_def by auto
       
-    from aux have "Q_lookup Q_initQ = initQ' (G_succ g s)"    
+    from aux have "Q_lookup (Q_initQ s) = initQ' (G_succ g s)"    
       unfolding Q_initQ_def initQ'_def by auto
     also have "\<dots> = initQ" by (rule initQ'_refine) auto
-    finally show "Q_lookup Q_initQ = initQ" .
+    finally show "Q_lookup (Q_initQ s) = initQ" .
   qed
   
   
   term Q_getmin
   
-  definition "dijkstra_loop \<equiv> while (\<lambda>(Q,V). \<not> Q_is_empty Q) (\<lambda>(Q,V). 
-    let
-      (u,du) = Q_getmin Q;
-      Q = Q_relax_adjs u du V Q;
-      Q = Q_delete u Q;
-      V = M_update u du V
-    in
-      (Q,V)
-  ) (Q_initQ,M_update s 0 M_empty)"
+  definition (in Dijkstra_Impl_Defs) 
+    "dijkstra_loop \<equiv> while (\<lambda>(Q,V). \<not> Q_is_empty Q) (\<lambda>(Q,V). 
+      let
+        (u,du) = Q_getmin Q;
+        Q = Q_relax_adjs u du V Q;
+        Q = Q_delete u Q;
+        V = M_update u du V
+      in
+        (Q,V)
+    ) (Q_initQ s,M_update s 0 M_empty)"
   
-  definition "dijkstra \<equiv> snd dijkstra_loop"
+  definition (in Dijkstra_Impl_Defs) "dijkstra \<equiv> snd dijkstra_loop"
   
   lemma transfer_preconditions:
     assumes "coupling Q V D S"
@@ -670,12 +687,12 @@
       
     have COUPLING': "coupling 
         ((relax_adjs' u du (M_lookup V) (Q_lookup Q))(u := None)) (M_lookup V(u \<mapsto> du)) 
-        (relax_adjs u D) (insert u S)"  
+        (relax_adjs u D) (Set.insert u S)"  
       using coupling_step(1)[OF COUPLING \<open>u\<notin>S\<close> \<open>D u = enat du\<close>] by auto
       
     show "D_invar_impl (Q_delete u (Q_relax_adjs u du V Q)) (M_update u du V)"
       using maintain_D_invar[OF \<open>D_invar D S\<close> \<open>u\<notin>S\<close>] ABS_PRE
-      using coupling_step(1)[OF COUPLING \<open>u\<notin>S\<close> \<open>D u = enat du\<close>, simplified]
+      using COUPLING'
       by (auto simp: D_invar_impl_def D_invar'_def)
     
     show "unfinished_dnodes' (M_lookup (M_update u du V)) \<subset> unfinished_dnodes' (M_lookup V) \<and>
@@ -700,4 +717,164 @@
     
 end       
 
+(*
+  Maps with to-list interface.
+  Iterations can be optimized by deforestation lemmas in a later step ... 
+  even in code-generator preprocessor.
+*)
+locale Iterable_Map = Map +
+  fixes to_list :: "'m \<Rightarrow> ('k \<times> 'v) list"  
+  assumes map_to_list: "invar m \<Longrightarrow> lookup m = map_of (to_list m) \<and> distinct (map fst (to_list m))"
+
+locale Iterable_Ordered_Map = Iterable_Map +
+  assumes map_to_list_sorted: "invar m \<Longrightarrow> sorted1 (to_list m)"
+  
+context Map_by_Ordered begin  
+  
+  sublocale Iterable_Ordered_Map empty update delete lookup invar inorder
+    apply unfold_locales
+    unfolding invar_def
+    apply (auto simp: inorder_lookup distinct_if_sorted)
+    done
+
+end  
+
+
+fun the_default :: "'a \<Rightarrow> 'a option \<Rightarrow> 'a" where
+  "the_default d None = d"
+| "the_default _ (Some x) = x"
+
+
+lemma distinct_map_snd_inj: "distinct (map snd l) \<Longrightarrow> (a,b)\<in>set l \<Longrightarrow> (a',b)\<in>set l \<Longrightarrow> a=a'"
+  by (metis distinct_map inj_onD prod.sel(2) prod.simps(1))
+
+(* TODO: Move *)   
+lemma edges_empty[simp]: "edges (\<lambda>_. \<infinity>) = {}" by (auto simp: edges_def)
+lemma edges_insert[simp]: "edges (g(e:=enat d)) = Set.insert e (edges g)" by (auto simp: edges_def)
+
+lemma prod_case_const[simp]: "case_prod (\<lambda>_ _. c) = (\<lambda>_. c)" by auto
+
+locale wgraph_by_map = 
+  M: Map M_empty M_update M_delete M_lookup M_invar 
+  
+  for M_empty M_update M_delete and M_lookup :: "'m \<Rightarrow> 'v \<Rightarrow> ((nat\<times>'v) list) option" and M_invar 
+begin
+  definition \<alpha> :: "'m \<Rightarrow> ('v,enat) wgraph" where
+    "\<alpha> g \<equiv> \<lambda>(u,v). case M_lookup g u of 
+      None \<Rightarrow> \<infinity> 
+    | Some l \<Rightarrow> if \<exists>d. (d,v)\<in>set l then enat (SOME d. (d,v)\<in>set l) else \<infinity>"
+
+  definition invar :: "'m \<Rightarrow> bool" where
+    "invar g \<equiv> M_invar g \<and> (\<forall>l\<in>ran (M_lookup g). distinct (map snd l)) \<and> finite (edges (\<alpha> g))"
+
+  definition succ :: "'m \<Rightarrow> 'v \<Rightarrow> (nat \<times> 'v) list" where
+    "succ g v = the_default [] (M_lookup g v)"
+    
+  definition empty_graph :: "'m" where "empty_graph = M_empty"
+  
+  definition add_edge :: "'v\<times>'v \<Rightarrow> nat \<Rightarrow> 'm \<Rightarrow> 'm" where
+    "add_edge \<equiv> \<lambda>(u,v) d g. M_update u ((d,v) # the_default [] (M_lookup g u)) g"
+  
+  sublocale adt_finite_wgraph invar succ empty_graph add_edge \<alpha>
+    apply unfold_locales
+    subgoal for g u
+      apply (cases "M_lookup g u")
+      apply (auto 
+        simp: invar_def \<alpha>_def succ_def ran_def
+        intro: distinct_map_snd_inj someI
+        split: option.splits
+      )
+      done
+    subgoal by (auto simp: invar_def \<alpha>_def empty_graph_def add_edge_def M.map_specs split: option.split)
+    subgoal by (auto simp: invar_def \<alpha>_def empty_graph_def add_edge_def M.map_specs split: option.split)
+  proof -    
+    (* Explicit proof to nicely handle finiteness constraint, using already proved shape of abstract result *)
+    fix g e d
+    assume A: "invar g" "\<alpha> g e = \<infinity>"
+    then show AAE: "\<alpha> (add_edge e d g) = (\<alpha> g)(e := enat d)"
+      by (auto 
+        simp: invar_def \<alpha>_def add_edge_def M.map_specs
+        split: option.splits if_splits prod.splits
+      )
+    
+    from A show "invar (add_edge e d g)"  
+      apply (simp add: invar_def AAE)
+      by (force
+        simp: invar_def \<alpha>_def empty_graph_def add_edge_def M.map_specs ran_def
+        split: option.splits if_splits prod.splits)      
+  qed (simp add: invar_def)     
+
+end  
+
+
+global_interpretation 
+  G: wgraph_by_map RBT_Set.empty RBT_Map.update RBT_Map.delete Lookup2.lookup RBT_Map.M.invar
+  defines G_empty = G.empty_graph
+      and G_add_edge = G.add_edge
+      and G_succ = G.succ
+  by unfold_locales
+print_theorems
+
+export_code G_empty G_succ G_add_edge in SML
+
+
+
+global_interpretation Dijkstra_Impl_Adts
+  G.\<alpha> G.invar G.succ G.empty_graph G.add_edge
+  RBT_Set.empty RBT_Map.update RBT_Map.delete Lookup2.lookup RBT_Map.M.invar
+  RBT_Heap.empty RBT_Heap.update RBT_Heap.delete RBT_Heap.PM.invar Lookup2.lookup RBT_Heap.rbt_is_empty RBT_Heap.rbt_getmin
+  ..
+
+global_interpretation D: Dijkstra_Impl_Defs  
+  G.invar G.succ G.empty_graph G.add_edge
+  RBT_Set.empty RBT_Map.update RBT_Map.delete Lookup2.lookup RBT_Map.M.invar
+  RBT_Heap.empty RBT_Heap.update RBT_Heap.delete RBT_Heap.PM.invar Lookup2.lookup RBT_Heap.rbt_is_empty RBT_Heap.rbt_getmin
+  G.\<alpha> g s for g and s::"'v::linorder"
+  defines dijkstra = D.dijkstra
+      and dijkstra_loop = D.dijkstra_loop
+      and Q_relax_adjs = D.Q_relax_adjs
+      and Q_relax_adjs1 = D.Q_relax_adjs1
+      and Q_initQ = D.Q_initQ
+      and Q_decrease_key = D.Q_decrease_key
+      and test = D.test
+  ..
+  
+(* TODO: Why is this fix necessary? *)
+lemmas [code] =    
+  D.dijkstra_def D.dijkstra_loop_def  
+  
+context
+  fixes g
+  assumes [simp]: "G.invar g"  
+begin  
+  
+  interpretation AUX: Dijkstra_Impl
+    G.invar G.succ G.empty_graph G.add_edge
+    RBT_Set.empty RBT_Map.update RBT_Map.delete Lookup2.lookup RBT_Map.M.invar
+    RBT_Heap.empty RBT_Heap.update RBT_Heap.delete RBT_Heap.PM.invar Lookup2.lookup RBT_Heap.rbt_is_empty RBT_Heap.rbt_getmin
+    g s G.\<alpha> for s
+    by unfold_locales simp_all
+  
+  lemmas dijkstra_correct = AUX.dijkstra_correct[folded dijkstra_def]
+  
+end  
+  
+  
+  
+export_code dijkstra in SML 
+thm dijkstra_correct
+  
+  
+
+
+
+
+
+
+
+
+
+
+
+
 end
--- a/Thys/RBT_Heap.thy	Wed Jul 04 19:00:02 2018 +0200
+++ b/Thys/RBT_Heap.thy	Thu Jul 05 18:32:01 2018 +0200
@@ -422,13 +422,14 @@
 lemma rbt_is_empty: "rbt_is_empty t \<longleftrightarrow> inorder t = []"
   by (cases t) (auto simp: rbt_is_empty_def)
 
-
+definition empty where "empty = Leaf"
+  
 interpretation PM: PrioMap_by_Ordered
-where empty = Leaf and lookup = lookup and update = update and delete = delete
+where empty = empty and lookup = lookup and update = update and delete = delete
 and inorder = inorder and inv = "rbt" and is_empty = rbt_is_empty and getmin = rbt_getmin
   apply standard
   apply (auto simp add: lookup_map_of inorder_update inorder_delete rbt_update rbt_delete rbt_Leaf
-    simp: rbt_is_empty dest: rbt_getmin_ismin)
+    simp: rbt_is_empty empty_def dest: rbt_getmin_ismin)
   done