Theory ExampleInstantiations

section ‹Example Instantiations›

text ‹
  This section provides a few example instantiations for the locales to show that they are not empty.
›

theory ExampleInstantiations
imports TreewidthCompleteGraph begin

datatype Vertices = u0 | v0 | w0

text ‹The empty graph is a tree.›
definition "T1 ≡ ⦇ verts = {}, arcs = {} ⦈"
interpretation Graph_T1: Graph T1 unfolding T1_def by standard simp_all
interpretation Tree_T1: Tree T1
  by (rule Tree.intro, simp add: Graph_T1.Graph_axioms, standard, unfold T1_def, simp)
     (metis T1_def Graph_T1.cycle_def equals0D simps(2))

text ‹The complete graph with 2 vertices.›
definition "T2 ≡ ⦇ verts = {u0, v0}, arcs = {(u0,v0),(v0,u0)} ⦈"
lemma Graph_T2: "Graph T2" unfolding T2_def by standard auto
lemma Tree_T2: "Tree T2"
proof-
  interpret Graph T2 using Graph_T2 .
  show ?thesis proof
    fix v w assume "v ∈ V⇘T2⇙" "w ∈ V⇘T2⇙" thus "connected v w"
      by (metis T2_def connected_def connected_edge empty_iff insert_iff last.simps list.discI
          list.sel(1) path_singleton simps(1,2))
  next
    fix xs :: "Vertices list"
    {
      fix x y
      assume "cycle xs" and xy: "(x = v0 ∧ y = u0) ∨ (x = u0 ∧ y = v0)" and "hd xs = x"
      hence "last xs = y"
        by (metis T2_def cycleE distinct.simps(2) distinct_singleton insert_iff list.set(1)
            prod.inject simps(2))
      moreover have "⋀v. v ∈ set xs ⟹ v = x ∨ v = y" using ‹cycle xs› xy
        by (metis cycle_def walk_in_V T2_def empty_iff insertE insert_absorb insert_subset
            select_convs(1))
      ultimately have "xs = [x,y]" using ‹cycle xs› xy
        by (metis cycleE distinct_length_2_or_more last.simps list.exhaust_sel list.set_sel(1)
            list.set_sel(2) no_loops)
      hence False using ‹cycle xs› unfolding cycle_def by simp
    }
    thus "¬cycle xs" by (metis T2_def cycleE empty_iff insertE prod.inject simps(2))
  qed
qed
text ‹As expected, the treewidth of the complete graph with 2 vertices is 1.

  Note that we use ‹Graph.treewidth_complete_graph› here and not ‹treewidth_tree›.
  This is because ‹treewidth_tree› requires the vertex set of the graph to be a set of
  natural numbers, which is not the case here.›
lemma T2_complete: "⟦ v ∈ V⇘T2⇙; w ∈ V⇘T2⇙; v ≠ w ⟧ ⟹ v →⇘T2⇙ w" unfolding T2_def by auto
lemma treewidth_T2: "Graph.treewidth T2 = 1"
  using Graph.treewidth_complete_graph[OF Graph_T2] T2_complete unfolding T2_def by simp

text ‹The complete graph with 3 vertices.›
definition "T3 ≡ ⦇ verts = {u0, v0, w0}, arcs = {(u0,v0),(v0,u0),(v0,w0),(w0,v0),(w0,u0),(u0,w0)} ⦈"
lemma Graph_T3: "Graph T3" unfolding T3_def by standard auto
text ‹@{term "[u0, v0, w0]"} is a cycle in @{const "T3"}, so @{const "T3"} is not a tree.›
lemma Not_Tree_T3: "¬Tree T3" proof
  assume "Tree T3" then interpret Tree T3 .
  let ?xs = "[u0, v0, w0]"
  have "path ?xs" by (metis T3_def Vertices.distinct(1,3,5)
    distinct_length_2_or_more distinct_singleton insert_iff simps(2) walk.Cons walk_2)
  moreover have "(hd ?xs, last ?xs) ∈ arcs T3" by (simp add: T3_def)
  ultimately show False using meeting_paths_produce_cycle no_cycles walk_2
    by (metis distinct_length_2_or_more last_ConsL last_ConsR list.sel(1))
qed

lemma T3_complete: "⟦ v ∈ V⇘T3⇙; w ∈ V⇘T3⇙; v ≠ w ⟧ ⟹ v →⇘T3⇙ w" unfolding T3_def by auto
lemma treewidth_T3: "Graph.treewidth T3 = 2"
  using Graph.treewidth_complete_graph[OF Graph_T3] T3_complete unfolding T3_def by simp

text ‹We omit a concrete example for the ‹TreeDecomposition› locale because
  ‹tree_decomposition_exists› already shows that it is non-empty.›

end