Theory Check_Non_Planarity_Impl

section ‹Implementation of a Non-Planarity Checker›

theory Check_Non_Planarity_Impl
imports
  Simpl.Vcg
  Simpl_Anno
  Graph_Theory.Graph_Theory
begin

subsection ‹An abstract graph datatype›

type_synonym ig_vertex = nat
type_synonym ig_edge = "ig_vertex × ig_vertex"

typedef IGraph = "{(vs :: ig_vertex list, es :: ig_edge list). distinct vs}"
  by auto

definition ig_verts :: "IGraph ⇒ ig_vertex list" where
  "ig_verts G ≡ fst (Rep_IGraph G)"

definition ig_arcs :: "IGraph ⇒ ig_edge list" where
  "ig_arcs G ≡ snd (Rep_IGraph G)"

definition ig_verts_cnt :: "IGraph ⇒ nat"
  where "ig_verts_cnt G ≡ length (ig_verts G)"

definition ig_arcs_cnt :: "IGraph ⇒ nat"
  where "ig_arcs_cnt G ≡ length (ig_arcs G)"

declare ig_verts_cnt_def[simp]
declare ig_arcs_cnt_def[simp]

definition IGraph_inv :: "IGraph ⇒ bool" where
  "IGraph_inv G ≡ (∀e ∈ set (ig_arcs G). fst e ∈ set (ig_verts G) ∧ snd e ∈ set (ig_verts G))"

definition ig_empty :: "IGraph" where
  "ig_empty ≡ Abs_IGraph ([],[])"

definition ig_add_v :: "IGraph ⇒ ig_vertex ⇒ IGraph" where
  "ig_add_v G v = (if v ∈ set (ig_verts G) then G else Abs_IGraph (ig_verts G @ [v], ig_arcs G ))"

definition ig_add_e :: "IGraph ⇒ ig_vertex ⇒ ig_vertex ⇒ IGraph" where
  "ig_add_e G u v ≡ Abs_IGraph (ig_verts G, ig_arcs G @ [(u,v)])"

definition ig_in_out_arcs :: "IGraph ⇒ ig_vertex ⇒ ig_edge list" where
  "ig_in_out_arcs G u ≡ filter (λe. fst e = u ∨ snd e = u) (ig_arcs G)"

definition ig_opposite :: "IGraph ⇒ ig_edge ⇒ ig_vertex ⇒ ig_vertex" where
  "ig_opposite G e u = (if fst e = u then snd e else fst e)"

definition ig_neighbors :: "IGraph => ig_vertex => ig_vertex set" where
  "ig_neighbors G u ≡ {v ∈ set (ig_verts G). (u,v) ∈ set (ig_arcs G) ∨ (v,u) ∈ set (ig_arcs G)}"



subsection ‹Code›

procedures is_subgraph (G :: IGraph, H :: IGraph | R :: bool)
  where
    i :: nat
    v :: "ig_vertex"
    ends :: "ig_edge"
  in "
    TRY
      ´i :== 0 ;;
      WHILE ´i < ig_verts_cnt ´G INV named_loop ''verts''
      DO
        ´v :== ig_verts ´G ! ´i ;;
        IF ´v ∉ set (ig_verts ´H) THEN
          RAISE ´R :== False
        FI ;;
        ´i :== ´i + 1
      OD ;;

      ´i :== 0 ;;
      WHILE ´i < ig_arcs_cnt ´G INV named_loop ''arcs''
      DO
        ´ends :== ig_arcs ´G ! ´i ;;
        IF ´ends ∉ set (ig_arcs ´H) ∧ (snd ´ends, fst ´ends) ∉ set (ig_arcs ´H) THEN
          RAISE ´R :== False
        FI ;;
        IF fst ´ends ∉ set (ig_verts ´G) ∨ snd ´ends ∉ set (ig_verts ´G) THEN
          RAISE ´R :== False
        FI ;;
        ´i :== ´i + 1
      OD ;;
      ´R :== True
    CATCH SKIP END
  "

procedures is_loopfree (G :: IGraph | R :: bool)
  where
    i :: nat
    ends :: "ig_edge"
    edge_map :: "ig_edge ⇒ bool"
  in "
    TRY
      ´i :== 0 ;;
      WHILE ´i < ig_arcs_cnt ´G INV named_loop ''loop''
      DO
        ´ends :== ig_arcs ´G ! ´i ;;
        IF fst ´ends = snd ´ends THEN
          RAISE ´R :== False
        FI ;;
        ´i :== ´i + 1
      OD ;;
      ´R :== True
    CATCH SKIP END
  "


procedures select_nodes (G :: IGraph | R :: IGraph)
  where
    i :: nat
    v :: ig_vertex
  in "
    ´R :== ig_empty ;;

    ´i :== 0 ;;
    WHILE ´i < ig_verts_cnt ´G
    INV named_loop ''loop''
    DO
      ´v :== ig_verts ´G ! ´i ;;
      IF 2 < card (ig_neighbors ´G ´v) THEN
        ´R :== ig_add_v ´R ´v
      FI ;;
      ´i :== ´i + 1
    OD
  "

procedures find_endpoint (G :: IGraph, H :: IGraph,  v_tail :: ig_vertex, v_next :: ig_vertex | R :: "ig_vertex option")
  where
    found :: bool
    i :: nat
    len :: nat
    io_arcs :: "ig_edge list"
    v0 :: ig_vertex
    v1 :: ig_vertex
    vt :: ig_vertex
  in "
    TRY
      IF ´v_tail = ´v_next THEN RAISE ´R :== None FI ;;
      ´v0 :== ´v_tail ;;
      ´v1 :== ´v_next ;;
      ´len :== 1 ;;
      WHILE ´v1 ∉ set (ig_verts ´H)
      INV named_loop ''path''
      DO
        ´io_arcs :== ig_in_out_arcs ´G ´v1 ;;
        ´i :== 0 ;;
        ´found :== False ;;
        WHILE ´found = False ∧ ´i < length ´io_arcs
        INV named_loop ''arcs''
        DO
          ´vt :== ig_opposite ´G (´io_arcs ! ´i) ´v1 ;;
          IF ´vt ≠ ´v0 THEN
            ´found :== True ;;
            ´v0 :== ´v1 ;;
            ´v1 :== ´vt
          FI ;;
          ´i :== ´i + 1
        OD ;;
        ´len :== ´len + 1 ;;
        IF ¬ ´found THEN RAISE ´R :== None FI
      OD ;;
      IF ´v1 = ´v_tail THEN RAISE ´R :== None FI ;;
      ´R :== Some ´v1
    CATCH SKIP END
  "

procedures contract (G :: IGraph, H :: IGraph | R :: "IGraph")
  where
    i :: nat
    j :: nat
    u :: ig_vertex
    v :: ig_vertex
    vo :: "ig_vertex option"
    io_arcs :: "ig_edge list"
  in "
    ´i :== 0 ;;
    WHILE ´i < ig_verts_cnt ´H
    INV named_loop ''iter_nodes''
    DO
      ´u :== ig_verts ´H ! ´i ;;
      ´io_arcs :== ig_in_out_arcs ´G ´u ;;

      ´j :== 0 ;;
      WHILE ´j < length ´io_arcs
      INV named_loop ''iter_adj''
      DO
        ´v :== ig_opposite ´G (´io_arcs ! ´j) ´u ;;
        ´vo :== CALL find_endpoint(´G, ´H, ´u, ´v) ;;
        IF ´vo ≠ None THEN
          ´H :== ig_add_e ´H ´u (the ´vo)
        FI ;;
        ´j :== ´j + 1
      OD ;;
      ´i :== ´i + 1
    OD ;;
    ´R :== ´H
  "

procedures is_K33 (G :: IGraph | R :: bool)
  where
    i :: nat
    j :: nat
    u :: ig_vertex
    v :: ig_vertex
    blue :: "ig_vertex ⇒ bool"
    blue_cnt :: nat
    io_arcs :: "ig_edge list"
  in "
    TRY
      IF ig_verts_cnt ´G ≠ 6 THEN RAISE ´R :== False FI ;;
      ´blue :== (λ_. False) ;;

      ´u :== ig_verts ´G ! 0 ;;
      ´i :== 0 ;;
      ´io_arcs :== ig_in_out_arcs ´G ´u ;;

      WHILE ´i < length ´io_arcs INV named_loop ''colorize''
      DO
        ´v :== ig_opposite ´G (´io_arcs ! ´i) ´u ;;
        ´blue :== ´blue(´v := True) ;;
        ´i :== ´i + 1
      OD ;;

      ´blue_cnt :== 0 ;;
      ´i :== 0 ;;
      WHILE ´i < ig_verts_cnt ´G INV named_loop ''component_size''
      DO
        IF ´blue (ig_verts ´G ! ´i) THEN ´blue_cnt :== ´blue_cnt + 1 FI ;;
        ´i :== ´i + 1
      OD ;;
      IF ´blue_cnt ≠ 3 THEN RAISE ´R :== False FI ;;

      ´i :== 0 ;;
      WHILE ´i < ig_verts_cnt ´G INV named_loop ''connected_outer''
      DO
        ´u :== ig_verts ´G ! ´i ;;
        ´j :== 0 ;;
        WHILE ´j < ig_verts_cnt ´G INV named_loop ''connected_inner''
        DO
          ´v :== ig_verts ´G ! ´j ;;
          IF ¬((´blue ´u = ´blue ´v) ⟷ (´u, ´v) ∉ set (ig_arcs ´G)) THEN RAISE ´R :== False FI ;;
          ´j :== ´j + 1
        OD ;;
        ´i :== ´i + 1
      OD ;;
      ´R :== True
    CATCH SKIP END
  "

procedures is_K5 (G :: IGraph | R :: bool)
  where
    i :: nat
    j :: nat
    u :: ig_vertex
  in "
    TRY
      IF ig_verts_cnt ´G ≠ 5 THEN RAISE ´R :== False FI ;;
      ´i :== 0 ;;
      WHILE ´i < 5 INV named_loop ''outer_loop''
        DO
        ´u :== ig_verts ´G ! ´i ;;
        ´j :== 0 ;;
        WHILE ´j < 5 INV named_loop ''inner_loop''
        DO
          IF ¬(´i ≠ ´j ⟷ (´u, ig_verts ´G ! ´j) ∈ set (ig_arcs ´G))
          THEN
            RAISE ´R :== False
          FI ;;
          ´j :== ´j + 1
        OD ;;
        ´i :== ´i + 1
      OD ;;
      ´R :== True
    CATCH SKIP END
  "

procedures check_kuratowski (G :: IGraph, K :: IGraph | R :: bool)
  where
    H :: IGraph
  in "
    TRY
      ´R :== CALL is_subgraph(´K, ´G) ;;
      IF ¬´R THEN RAISE ´R :== False FI ;;
      ´R :== CALL is_loopfree(´K) ;;
      IF ¬´R THEN RAISE ´R :== False FI ;;
      ´H :== CALL select_nodes(´K) ;;
      ´H :== CALL contract(´K, ´H) ;;
      ´R :== CALL is_K5(´H) ;;
      IF ´R THEN RAISE ´R :== True FI ;;
      ´R :== CALL is_K33(´H)
    CATCH SKIP END
  "



end