Dijkstra wrapper with consistency check on list draft
authorlammich <lammich@in.tum.de>
Fri, 06 Jul 2018 00:22:56 +0200
changeset 69945 c772b78fd6cd
parent 69944 de538a919227
child 69946 ed7c67f266ac
Dijkstra wrapper with consistency check on list
Thys/Dijkstra.thy
--- a/Thys/Dijkstra.thy	Thu Jul 05 19:13:38 2018 +0200
+++ b/Thys/Dijkstra.thy	Fri Jul 06 00:22:56 2018 +0200
@@ -865,30 +865,53 @@
 thm dijkstra_correct
   
 
+text \<open>A list represents a graph if there are no multi-edges or duplicate edges\<close>
 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>"  
+text \<open>Alternative characterization: all node pairs must be distinct\<close>
+lemma valid_graph_rep_code[code]: "valid_graph_rep l \<longleftrightarrow> distinct (map (\<lambda>(u,v,_). (u,v)) l)"  
+  by (auto simp: valid_graph_rep_def distinct_map inj_on_def)
   
 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)
+  
+text \<open>For a valid graph representation, there is exactly one graph that corresponds to it\<close>  
+lemma valid_graph_rep_ex1: "valid_graph_rep l \<Longrightarrow> \<exists>! w. \<forall>u v d. w (u,v) = enat d \<longleftrightarrow> (u,v,d)\<in>set l"  
+  unfolding valid_graph_rep_code
+  apply (auto)
+  subgoal 
+    apply (rule exI[where x="\<lambda>(u,v). if \<exists>d. (u,v,d)\<in>set l then enat (SOME d. (u,v,d)\<in>set l) else \<infinity>"])
+    apply (auto intro: someI simp: distinct_map inj_on_def split: prod.splits; blast)
+    done    
+  subgoal for w w'
+    apply (auto del: ext intro!: ext)
+    by (metis (mono_tags, hide_lams) not_enat_eq)
+  done  
 
-locale wgraph_from_list = adt_wgraph 
+text \<open>We define this graph using determinate choice\<close>  
+definition "wgraph_of_list l \<equiv> \<lambda>(u,v). if \<exists>d. (u,v,d)\<in>set l then enat (THE d. (u,v,d)\<in>set l) else \<infinity>"  
+    
+  
+locale wgraph_from_list_algo = adt_wgraph 
 begin
 
   definition "from_list l \<equiv> fold (\<lambda>(u,v,d). add_edge (u,v) d) l empty_graph"
 
+  definition "edges_undef l w \<equiv> \<forall>u v d. (u,v,d)\<in>set l \<longrightarrow> w (u,v) = \<infinity>"  
+    
+  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)
+  
   lemma from_list_correct_aux:
     assumes "valid_graph_rep l"
     assumes "edges_undef l (\<alpha> g)"
@@ -906,18 +929,37 @@
     unfolding from_list_def using from_list_correct_aux[OF assms, where g=empty_graph]
     by (auto simp: wgraph_specs)
 
+  lemma from_list_correct':
+    assumes "valid_graph_rep l"
+    shows "invar (from_list l)" "\<alpha> (from_list l) = wgraph_of_list l"
+    using from_list_correct[OF assms] valid_graph_rep_ex1[OF assms]
+    unfolding wgraph_of_list_def 
+    by fastforce+
+    
 end
 
-global_interpretation G: wgraph_from_list G.\<alpha> G.invar G.succ G.empty_graph G.add_edge
+global_interpretation G: wgraph_from_list_algo 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
 
 
+thm dijkstra_correct
+
+definition "dijkstra_list l s \<equiv> if valid_graph_rep l then Some (dijkstra (from_list l) s) else None"
+
+lemma "case dijkstra_list l s of
+  None \<Rightarrow> \<not>valid_graph_rep l
+| Some D \<Rightarrow> valid_graph_rep l \<and> M.invar D \<and> (\<forall>u d. lookup D u = Some d \<longleftrightarrow> WGraph.\<delta> (wgraph_of_list l) s u = enat d)"
+  unfolding dijkstra_list_def
+  by (auto simp: dijkstra_correct G.from_list_correct')
+
+
+
 value "(dijkstra o G.from_list) [(1,2::nat,7),(1,3,1),(3,2,2)] 1"
 
-  
-  
+value "dijkstra_list [(1::nat,2,7),(1,3,1),(3,2,2)] 1"
+
+
+end