(* Title:KoenigsbergBridge.thy Author:Wenda Li *) theory KoenigsbergBridge imports MoreGraph begin section‹Definition of Eulerian trails and circuits› definition (in valid_unMultigraph) is_Eulerian_trail:: "'v⇒('v,'w) path⇒'v⇒ bool" where "is_Eulerian_trail v ps v'≡ is_trail v ps v' ∧ edges (rem_unPath ps G) = {}" definition (in valid_unMultigraph) is_Eulerian_circuit:: "'v ⇒ ('v,'w) path ⇒ 'v ⇒ bool" where "is_Eulerian_circuit v ps v'≡ (v=v') ∧ (is_Eulerian_trail v ps v')" section‹Necessary conditions for Eulerian trails and circuits› lemma (in valid_unMultigraph) euclerian_rev: "is_Eulerian_trail v' (rev_path ps) v=is_Eulerian_trail v ps v' " proof - have "is_trail v' (rev_path ps) v=is_trail v ps v'" by (metis is_trail_rev) moreover have "edges (rem_unPath (rev_path ps) G)=edges (rem_unPath ps G)" by (metis rem_unPath_graph) ultimately show ?thesis unfolding is_Eulerian_trail_def by auto qed (*Necessary conditions for Eulerian circuits*) theorem (in valid_unMultigraph) euclerian_cycle_ex: assumes "is_Eulerian_circuit v ps v'" "finite V" "finite E" shows "∀v∈V. even (degree v G)" proof - obtain v ps v' where cycle:"is_Eulerian_circuit v ps v'" using assms by auto hence "edges (rem_unPath ps G) = {}" unfolding is_Eulerian_circuit_def is_Eulerian_trail_def by simp moreover have "nodes (rem_unPath ps G)=nodes G" by auto ultimately have "rem_unPath ps G = G ⦇edges:={}⦈" by auto hence "num_of_odd_nodes (rem_unPath ps G) = 0" by (metis assms(2) odd_nodes_no_edge) moreover have "v=v'" by (metis ‹is_Eulerian_circuit v ps v'› is_Eulerian_circuit_def) hence "num_of_odd_nodes (rem_unPath ps G)=num_of_odd_nodes G" by (metis assms(2) assms(3) cycle is_Eulerian_circuit_def is_Eulerian_trail_def rem_UnPath_cycle) ultimately have "num_of_odd_nodes G=0" by auto moreover have "finite(odd_nodes_set G)" using ‹finite V› unfolding odd_nodes_set_def by auto ultimately have "odd_nodes_set G = {}" unfolding num_of_odd_nodes_def by auto thus ?thesis unfolding odd_nodes_set_def by auto qed (*Necessary conditions for Eulerian trails*) theorem (in valid_unMultigraph) euclerian_path_ex: assumes "is_Eulerian_trail v ps v'" "finite V" "finite E" shows "(∀v∈V. even (degree v G)) ∨ (num_of_odd_nodes G =2)" proof - obtain v ps v' where path:"is_Eulerian_trail v ps v'" using assms by auto hence "edges (rem_unPath ps G) = {}" unfolding is_Eulerian_trail_def by simp moreover have "nodes (rem_unPath ps G)=nodes G" by auto ultimately have "rem_unPath ps G = G ⦇edges:={}⦈" by auto hence odd_nodes: "num_of_odd_nodes (rem_unPath ps G) = 0" by (metis assms(2) odd_nodes_no_edge) have "v≠v' ⟹ ?thesis" proof (cases "even(degree v' G)") case True assume "v≠v'" have "is_trail v ps v'" by (metis is_Eulerian_trail_def path) hence "num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G + (if even (degree v G) then 2 else 0)" using rem_UnPath_even True ‹finite V› ‹finite E› ‹v≠v'› by auto hence "num_of_odd_nodes G + (if even (degree v G) then 2 else 0)=0" using odd_nodes by auto hence "num_of_odd_nodes G = 0" by auto moreover have "finite(odd_nodes_set G)" using ‹finite V› unfolding odd_nodes_set_def by auto ultimately have "odd_nodes_set G = {}" unfolding num_of_odd_nodes_def by auto thus ?thesis unfolding odd_nodes_set_def by auto next case False assume "v≠v'" have "is_trail v ps v'" by (metis is_Eulerian_trail_def path) hence "num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G + (if odd (degree v G) then -2 else 0)" using rem_UnPath_odd False ‹finite V› ‹finite E› ‹v≠v'› by auto hence odd_nodes_if: "num_of_odd_nodes G + (if odd (degree v G) then -2 else 0)=0" using odd_nodes by auto have "odd (degree v G) ⟹ ?thesis" proof - assume "odd (degree v G)" hence "num_of_odd_nodes G = 2" using odd_nodes_if by auto thus ?thesis by simp qed moreover have "even(degree v G) ⟹ ?thesis" proof - assume "even (degree v G)" hence "num_of_odd_nodes G = 0" using odd_nodes_if by auto moreover have "finite(odd_nodes_set G)" using ‹finite V› unfolding odd_nodes_set_def by auto ultimately have "odd_nodes_set G = {}" unfolding num_of_odd_nodes_def by auto thus ?thesis unfolding odd_nodes_set_def by auto qed ultimately show ?thesis by auto qed moreover have "v=v'⟹ ?thesis" by (metis assms(2) assms(3) euclerian_cycle_ex is_Eulerian_circuit_def path) ultimately show ?thesis by auto qed section‹Specific case of the Konigsberg Bridge Problem› (*to denote the four landmasses*)