From-List, and example. TODO: Combined correctness theorem for dijkstra o from_list, validity check for list (no multi-edges) draft
authorlammich <lammich@in.tum.de>
Thu, 05 Jul 2018 19:13:38 +0200
changeset 69944 de538a919227
parent 69943 d5860fb818f1
child 69945 c772b78fd6cd
From-List, and example. TODO: Combined correctness theorem for dijkstra o from_list, validity check for list (no multi-edges)
Thys/Dijkstra.thy
--- a/Thys/Dijkstra.thy	Thu Jul 05 18:32:01 2018 +0200
+++ b/Thys/Dijkstra.thy	Thu Jul 05 19:13:38 2018 +0200
@@ -864,17 +864,60 @@
 export_code dijkstra in SML 
 thm dijkstra_correct
   
+
+definition "valid_graph_rep l \<equiv> 
+  (\<forall>u d d' v. (u,v,d)\<in>set l \<and> (u,v,d')\<in>set l \<longrightarrow> d=d')
+\<and> distinct l
+  "
+
+definition "edges_undef l w \<equiv> \<forall>u v d. (u,v,d)\<in>set l \<longrightarrow> w (u,v) = \<infinity>"  
   
+lemma valid_graph_rep_simps[simp]:
+  "valid_graph_rep []"
+  "valid_graph_rep ((u,v,d) # l) \<longleftrightarrow> valid_graph_rep l \<and> (\<forall>d'. (u,v,d')\<notin>set l)"
+  by (auto simp: valid_graph_rep_def)
 
+lemma edges_undef_simps[simp]:
+  "edges_undef [] w"  
+  "edges_undef l (\<lambda>_. \<infinity>)"
+  "edges_undef ((u,v,d)#l) w \<longleftrightarrow> edges_undef l w \<and> w (u,v) = \<infinity>"
+  "edges_undef l (w((u,v) := enat d)) \<longleftrightarrow> edges_undef l w \<and> (\<forall>d'. (u,v,d')\<notin>set l)"  
+  by (auto simp: edges_undef_def)
+
+locale wgraph_from_list = adt_wgraph 
+begin
+
+  definition "from_list l \<equiv> fold (\<lambda>(u,v,d). add_edge (u,v) d) l empty_graph"
 
+  lemma from_list_correct_aux:
+    assumes "valid_graph_rep l"
+    assumes "edges_undef l (\<alpha> g)"
+    assumes "invar g"
+    defines "g' \<equiv> fold (\<lambda>(u,v,d). add_edge (u,v) d) l g"
+    shows "invar g'" "(\<forall>u v d. \<alpha> g' (u,v) = enat d \<longleftrightarrow> \<alpha> g (u,v) = enat d \<or> (u,v,d)\<in>set l)"
+    using assms(1-3) unfolding g'_def
+    apply (induction l arbitrary: g)
+    apply (auto simp: wgraph_specs split: if_splits)
+    done
 
+  lemma from_list_correct:
+    assumes "valid_graph_rep l"
+    shows "invar (from_list l)" "(u,v,d)\<in>set l \<longleftrightarrow> \<alpha> (from_list l) (u,v) = enat d"
+    unfolding from_list_def using from_list_correct_aux[OF assms, where g=empty_graph]
+    by (auto simp: wgraph_specs)
 
+end
+
+global_interpretation G: wgraph_from_list G.\<alpha> G.invar G.succ G.empty_graph G.add_edge
+  defines from_list = G.from_list
+  ..
+
+thm G.from_list_correct
+  
+export_code "G.from_list" in SML
 
 
-
-
-
+value "(dijkstra o G.from_list) [(1,2::nat,7),(1,3,1),(3,2,2)] 1"
 
-
-
-end
+  
+