Theory Check_Planarity_Verification

section ‹Verififcation of a Planarity Checker›

theory Check_Planarity_Verification
imports
  "../Planarity/Graph_Genus"
  Setup_AutoCorres
  "HOL-Library.Rewrite"
begin

subsection  ‹Implementation Types›

type_synonym IVert = "nat"
type_synonym IEdge = "IVert × IVert"
type_synonym IGraph = "IVert list × IEdge list"

abbreviation (input) ig_edges :: "IGraph ⇒ IEdge list" where
  "ig_edges G ≡ snd G"

abbreviation (input) ig_verts :: "IGraph ⇒ IVert list" where
  "ig_verts G ≡ fst G"

definition ig_tail :: "IGraph ⇒ nat ⇒ IVert" where
  "ig_tail IG a = fst (ig_edges IG ! a)"

definition ig_head :: "IGraph ⇒ nat ⇒ IVert" where
  "ig_head IG a = snd (ig_edges IG ! a)"

type_synonym IMap = "(nat ⇒ nat) × (nat ⇒ nat) × (nat ⇒ nat)"

definition im_rev :: "IMap ⇒ (nat ⇒ nat)" where
  "im_rev iM = fst iM"

definition im_succ :: "IMap ⇒ (nat ⇒ nat)" where
  "im_succ iM = fst (snd iM)"

definition im_pred :: "IMap ⇒ (nat ⇒ nat)" where
  "im_pred iM = snd (snd iM)"


definition mk_graph :: "IGraph ⇒ (IVert, nat) pre_digraph" where
  "mk_graph IG ≡ ⦇
    verts = set (ig_verts IG),
    arcs = {0..< length (ig_edges IG)},
    tail = ig_tail IG,
    head = ig_head IG
  ⦈"

lemma mkg_simps:
  "verts (mk_graph IG) = set (ig_verts IG)"
  "tail (mk_graph IG) = ig_tail IG"
  "head (mk_graph IG) = ig_head IG"
  by (auto simp: mk_graph_def)

lemma arcs_mkg: "arcs (mk_graph IG) = {0..< length (ig_edges IG)}"
  by (auto simp: mk_graph_def)

lemma arc_to_ends_mkg: "arc_to_ends (mk_graph IG) a = ig_edges IG ! a"
  by (auto simp: arc_to_ends_def mkg_simps ig_tail_def ig_head_def)

definition mk_map :: "(_, nat) pre_digraph ⇒ IMap ⇒ nat pre_map" where
  "mk_map G iM ≡ ⦇
    edge_rev = perm_restrict (im_rev iM) (arcs G),
    edge_succ = perm_restrict (im_succ iM) (arcs G)
  ⦈"

lemma mkm_simps:
  "edge_rev (mk_map G iM) = perm_restrict (im_rev iM) (arcs G)"
  "edge_succ (mk_map G iM) = perm_restrict (im_succ iM) (arcs G)"
  by (auto simp: mk_map_def)

lemma es_eq_im: "a ∈ arcs (mk_graph iG) ⟹ edge_succ (mk_map (mk_graph iG) iM) a = im_succ iM a"
  by (auto simp: mkm_simps arcs_mkg perm_restrict_simps)


subsection ‹Implementation›

definition "is_map iG iM ≡
  DO ecnt ← oreturn (length (snd iG));
     vcnt ← oreturn (length (fst iG));
     (i, revOk) ← owhile
      (λ(i, ok) s. i < ecnt ∧ ok)
      (λ(i, ok).
        DO
          j ← oreturn (im_rev iM i);
          revIn ← oreturn (j < length (ig_edges iG));
          revNeq ← oreturn (j ≠ i);
          revRevs ← oreturn (ig_edges iG ! j = prod.swap (ig_edges iG ! i));
          invol ← oreturn (im_rev iM j = i);
          oreturn (i + 1, revIn ∧ revNeq ∧ revRevs ∧ invol)
        OD)
      (0, True);
     (i, succPerm) ← owhile
      (λ(i, ok) s. i < ecnt ∧ ok)
      (λ(i, ok).
        DO
          j ← oreturn (im_succ iM i);
          succIn ← oreturn (j < length (ig_edges iG));
          succEnd ← oreturn (ig_tail iG i = ig_tail iG j);
          isPerm ← oreturn (im_pred iM j = i);
          oreturn (i + 1, succIn ∧ succEnd ∧ isPerm)
        OD)
      (0, True);
     (i, succOrbits, V, A) ← owhile
      (λ(i, ok, V, A) s. i < ecnt ∧ succPerm ∧ ok)
      (λ(i, ok, V, A).
        DO
          (x,V,A) ← ocondition (λ_. ig_tail iG i ∈ V)
            (oreturn (i ∈ A, V, A))
            (DO
              (A',j) ← owhile
                (λ(A',j) s. j ∉ A')
                (λ(A',j). DO
                    A' ← oreturn (insert j A');
                    j ← oreturn (im_succ iM j);
                    oreturn (A', j)
                  OD)
                ({},i);
              V ← oreturn (insert (ig_tail iG j) V);
              oreturn (True,V,A ∪ A')
            OD);
          oreturn (i + 1, x, V, A)
        OD)
      (0, True, {}, {});
     oreturn (revOk ∧ succPerm ∧ succOrbits)
  OD
"

definition isolated_nodes :: "IGraph ⇒ _ ⇒ nat option" where
"isolated_nodes iG ≡
  DO ecnt ← oreturn (length (snd iG));
     vcnt ← oreturn (length (fst iG));
     (i, nz) ←
     owhile
      (λ(i, nz) a. i < vcnt)
      (λ(i, nz).
          DO v ← oreturn (fst iG ! i);
             j ← oreturn 0;
             ret ← ocondition (λs. j < ecnt) (oreturn (ig_tail iG j ≠ v)) (oreturn False);
             ret ← ocondition (λs. ret) (oreturn (ig_head iG j ≠ v)) (oreturn ret);
             (j, _) ←
             owhile
              (λ(j, cond) a. cond)
              (λ(j, cond).
                  DO j ← oreturn (j + 1);
                     cond ← ocondition (λs. j < ecnt) (oreturn (ig_tail iG j ≠ v)) (oreturn False);
                     cond ← ocondition (λs. cond) (oreturn (ig_head iG j ≠ v)) (oreturn cond);
                     oreturn (j, cond)
                  OD)
              (j, ret);
             nz ← oreturn (if j = ecnt then nz + 1 else nz);
             oreturn (i + 1, nz)
          OD)
      (0, 0);
     oreturn nz
  OD"

definition face_cycles :: "IGraph ⇒ nat pre_map ⇒ _  ⇒ nat option" where
"face_cycles iG iM ≡
  DO ecnt ← oreturn (length (snd iG));
     (edge_info, c, i) ←
     owhile
      (λ(edge_info, c, i) s. i < ecnt)
      (λ(edge_info, c, i).
          DO (edge_info, c) ←
             ocondition (λs. i ∉ edge_info)
              (DO j ← oreturn i;
                  edge_info ← oreturn (insert j edge_info);
                  ret' ← oreturn (pre_digraph_map.face_cycle_succ iM j);
                  (edge_info, j) ←
                  owhile
                   (λ(edge_info, j) s. i ≠ j)
                   (λ(edge_info, j).
                       oreturn (insert j edge_info, pre_digraph_map.face_cycle_succ iM j))
                   (edge_info, ret');
                  oreturn (edge_info, c + 1)
               OD)
              (oreturn (edge_info, c));
             oreturn (edge_info, c, i + 1)
          OD)
      ({}, 0, 0);
     oreturn c
  OD"

definition "euler_genus iG iM c ≡
   DO n ← oreturn (length (ig_edges iG));
      m ← oreturn (length (ig_verts iG));
      nz ← isolated_nodes iG;
      fc ← face_cycles iG iM;
      oreturn ((int n div 2 + 2 * int c - int m - int nz - int fc) div 2)
   OD"

definition "certify iG iM c ≡
  DO
     map ← is_map iG iM;
     ocondition (λ_. map)
       (DO
          gen ← euler_genus iG (mk_map (mk_graph iG) iM) c;
          oreturn (gen = 0)
       OD)
       (oreturn False)
  OD"


subsection ‹Verification›

context begin
  interpretation Labeling_Syntax .
  lemma trivial_label: "P ⟹ CTXT IC CT OC P"
    unfolding LABEL_simps .
end

lemma ovalidNF_wp:
  assumes "ovalidNF P c (λr s. r = x)"
  shows "ovalidNF (λs. Q x s ∧ P s) c Q"
  using assms unfolding ovalidNF_def by auto

subsubsection ‹@{term is_map}›

definition "is_map_rev_ok_inv iG iM k ok ≡ ok ⟷ (∀i < k.
  im_rev iM i < length (ig_edges iG)
  ∧ ig_edges iG ! im_rev iM i = prod.swap (ig_edges iG ! i)
  ∧ im_rev iM i ≠ i
  ∧ im_rev iM (im_rev iM i) = i)
"

definition "is_map_succ_perm_inv iG iM k ok ≡ ok ⟷ (∀i < k.
  im_succ iM i < length (ig_edges iG)
  ∧ ig_tail iG (im_succ iM i) = ig_tail iG i
  ∧ im_pred iM (im_succ iM i) = i)
"

definition "is_map_succ_orbits_inv iG iM k ok V A ≡
  A = (⋃i<(if ok then k else k - 1). orbit (im_succ iM) i) ∧
  V = {ig_tail iG i | i. i<(if ok then k else k - 1)} ∧
  ok = (∀i < k. ∀j < k. ig_tail iG i = ig_tail iG j ⟶ j ∈ orbit (im_succ iM) i)
"

definition "is_map_succ_orbits_inner_inv iG iM i j A' ≡
  A' = (if i = j ∧ i ∉ A' then {} else {i} ∪ segment (im_succ iM) i j)
  ∧ j ∈ orbit (im_succ iM) i
"

definition "is_map_final iG k ok ≡ (ok ⟶ k = length (ig_edges iG)) ∧ k ≤ length (ig_edges iG)"

lemma bij_betwI_finite_dom:
  assumes "finite A" "f ∈ A → A" "⋀a. a ∈ A ⟹ g (f a) = a"
  shows "bij_betw f A A"
proof -
  have "inj_on f A" by (metis assms(3) inj_onI)
  moreover
  then have "f ` A = A" by (metis Pi_iff assms(1-2) endo_inj_surj image_subsetI)
  ultimately show ?thesis unfolding bij_betw_def by simp
qed

lemma permutesI_finite_dom:
  assumes "finite A"
  assumes "f ∈ A → A"
  assumes "⋀a. a ∉ A ⟹ f a = a"
  assumes "⋀a. a ∈ A ⟹ g (f a) = a"
  shows "f permutes A"
  using assms by (intro bij_imp_permutes bij_betwI_finite_dom)

lemma orbit_ss:
  assumes "f ∈ A → A" "a ∈ A"
  shows "orbit f a ⊆ A"
proof -
  { fix x assume "x ∈ orbit f a" then have "x ∈ A" using assms by induct auto }
  then show ?thesis by blast
qed

lemma segment_eq_orbit:
  assumes "y ∉ orbit f x" shows "segment f x y = orbit f x"
proof (intro set_eqI iffI)
  fix z assume "z ∈ segment f x y" then show "z ∈ orbit f x" by (rule segmentD_orbit)
next
  fix z assume "z ∈ orbit f x" then show "z ∈ segment f x y"
    using assms by induct (auto intro: segment.intros orbit_eqI elim: orbit.cases)
qed

lemma funpow_in_funcset:
  assumes "x ∈ A" "f ∈ A → A" shows "(f ^^ n) x ∈ A"
  using assms by (induct n) auto

lemma funpow_eq_funcset:
  assumes "x ∈ A" "f ∈ A → A" "⋀y. y ∈ A ⟹ f y = g y"
  shows "(f ^^ n) x = (g ^^ n) x"
  using assms by (induct n) (auto, metis funpow_in_funcset)

lemma funpow_dist1_eq_funcset:
  assumes "y ∈ orbit f x" "x ∈ A" "f ∈ A → A" "⋀y. y ∈ A ⟹ f y = g y"
  shows "funpow_dist1 f x y = funpow_dist1 g x y"
proof -
  have "y = (f ^^ funpow_dist1 f x y) x" by (metis assms(1) funpow_dist1_prop)
  also have "… = (g ^^ funpow_dist1 f x y) x" by (metis assms(2-) funpow_eq_funcset)
  finally have *: "y = (g ^^ funpow_dist1 f x y) x" .
  then have "(g ^^ funpow_dist1 g x y) x = y" by (metis funpow_dist1_prop1 zero_less_Suc)
  with * have gf: "funpow_dist1 g x y ≤ funpow_dist1 f x y"
    by (metis funpow_dist1_least not_le zero_less_Suc)

  have "(f ^^ funpow_dist1 g x y) x = y"
    using ‹(g ^^ funpow_dist1 g x y) x = y› by (metis assms(2-) funpow_eq_funcset)
  then have fg: "funpow_dist1 f x y ≤ funpow_dist1 g x y"
    using ‹y = (f ^^ _) x› by (metis funpow_dist1_least not_le zero_less_Suc)

  from gf fg show ?thesis by simp
qed

lemma segment_cong0:
  assumes "x ∈ A" "f ∈ A → A" "⋀y. y ∈ A ⟹ f y = g y" shows "segment f x y = segment g x y"
proof (cases "y ∈ orbit f x")
  case True
  moreover
  from assms have "orbit f x = orbit g x" by (rule orbit_cong0)
  moreover
  have "(f ^^ n) x = (g ^^ n) x ∧ (f ^^ n) x ∈ A" for n
    by (induct n rule: nat.induct) (insert assms, auto)
  ultimately show ?thesis
    using True by (auto simp: segment_altdef funpow_dist1_eq_funcset[OF _ assms])
next
  case False
  moreover from assms have "orbit f x = orbit g x" by (rule orbit_cong0)
  ultimately show ?thesis by (simp add: segment_eq_orbit)
qed

lemma rev_ok_final:
  assumes wf_iG: "wf_digraph (mk_graph iG)"
  assumes rev: "is_map_rev_ok_inv iG iM rev_i rev_ok" "is_map_final iG rev_i rev_ok"
  shows "rev_ok ⟷ bidirected_digraph (mk_graph iG) (edge_rev (mk_map (mk_graph iG) iM))" (is "?L ⟷ ?R")
proof
  assume "rev_ok"
  interpret wf_digraph "mk_graph iG" by (rule wf_iG)
  have rev_inv_sep:
      "⋀i. i < length (ig_edges iG) ⟹ im_rev iM i < length (ig_edges iG)"
      "⋀i. i < length (ig_edges iG) ⟹ ig_edges iG ! im_rev iM i = prod.swap (ig_edges iG ! i)"
      "⋀i. i < length (ig_edges iG) ⟹ im_rev iM i ≠ i"
      "⋀i. i < length (ig_edges iG) ⟹ im_rev iM (im_rev iM i) = i"
    using rev ‹rev_ok› by (auto simp: is_map_rev_ok_inv_def is_map_final_def)
  moreover
  { fix i assume "i < length (ig_edges iG)"
    then have "ig_tail iG (im_rev iM i) = ig_head iG i"
      using rev_inv_sep(2) by (cases "ig_edges iG ! i") (auto simp: ig_head_def ig_tail_def)
  }
  ultimately show ?R
    using wf by unfold_locales (auto simp: mkg_simps arcs_mkg mkm_simps perm_restrict_def)
next
  assume ?R
  let ?rev = "perm_restrict (im_rev iM) (arcs (mk_graph iG))"
  interpret bidirected_digraph "mk_graph iG" "perm_restrict (im_rev iM) (arcs (mk_graph iG))"
    using ‹?R› by (simp add: mkm_simps mkg_simps)
  have "⋀a. a ∈ arcs (mk_graph iG) ⟹ ?rev a ∈ arcs (mk_graph iG)"
       "⋀a. a ∈ arcs (mk_graph iG) ⟹
        arc_to_ends (mk_graph iG) (?rev a) = prod.swap (arc_to_ends (mk_graph iG) a)"
       "⋀a. a ∈ arcs (mk_graph iG) ⟹ ?rev a ≠ a"
       "⋀a. a ∈ arcs (mk_graph iG) ⟹ ?rev (?rev a) = a"
    by (auto simp: arev_dom)
  then show rev_ok
    using rev unfolding is_map_rev_ok_inv_def is_map_final_def
    by (simp add: perm_restrict_simps arcs_mkg arc_to_ends_mkg)
qed

locale is_map_postcondition0 =
  fixes iG iM rev_ok succ_i succ_ok
  assumes succ_perm: "is_map_succ_perm_inv iG iM succ_i succ_ok" "is_map_final iG succ_i succ_ok"
begin

  lemma succ_ok_tail_eq:
    "succ_ok ⟹ i < length (ig_edges iG) ⟹ ig_tail iG (im_succ iM i) = ig_tail iG i "
    using succ_perm unfolding is_map_succ_perm_inv_def is_map_final_def by auto

  lemma succ_ok_imp_pred:
    "succ_ok ⟹ i < length (ig_edges iG) ⟹ im_pred iM (im_succ iM i) = i"
    using succ_perm unfolding is_map_succ_perm_inv_def is_map_final_def by auto

  lemma succ_ok_imp_permutes:
    assumes "succ_ok"
    shows "edge_succ (mk_map (mk_graph iG) iM) permutes arcs (mk_graph iG)"
  proof -
    from assms have "∀a ∈ arcs (mk_graph iG). edge_succ (mk_map (mk_graph iG) iM) a ∈ arcs (mk_graph iG)"
      using succ_perm unfolding is_map_succ_perm_inv_def is_map_final_def
      by (auto simp: mkg_simps mkm_simps arcs_mkg perm_restrict_def)
    with succ_ok_imp_pred[OF assms] show ?thesis
      by - (rule permutesI_finite_dom[where g="im_pred iM"], auto simp: perm_restrict_simps mkm_simps arcs_mkg)
  qed

  lemma es_A2A: "succ_ok ⟹ edge_succ (mk_map (mk_graph iG) iM) ∈ arcs (mk_graph iG) → arcs (mk_graph iG)"
    using succ_ok_imp_permutes by (auto dest: permutes_in_image)

  lemma im_succ_le_length: "succ_ok ⟹ i < length (ig_edges iG) ⟹ im_succ iM i < length (ig_edges iG)"
    using is_map_final_def is_map_succ_perm_inv_def succ_perm(1) succ_perm(2) by auto

  lemma orbit_es_eq_im:
    "succ_ok ⟹ a ∈ arcs (mk_graph iG) ⟹ orbit (edge_succ (mk_map (mk_graph iG) iM)) a = orbit (im_succ iM) a"
    using _ es_A2A es_eq_im by (rule orbit_cong0)

  lemma segment_es_eq_im:
    "succ_ok ⟹ a ∈ arcs (mk_graph iG) ⟹ segment (edge_succ (mk_map (mk_graph iG) iM)) a b = segment (im_succ iM) a b"
    using _ es_A2A es_eq_im by (rule segment_cong0)


  lemma in_orbit_im_succE:
    assumes "j ∈ orbit (im_succ iM) i" "succ_ok" "i < length (ig_edges iG)"
    obtains "ig_tail iG j = ig_tail iG i" "j < length (ig_edges iG)"
    using assms es_A2A by induct (force simp add: succ_ok_tail_eq es_eq_im arcs_mkg)+

  lemma self_in_orbit_im_succ:
    assumes "succ_ok" "i < length (ig_edges iG)" shows "i ∈ orbit (im_succ iM) i"
  proof -
    have "i ∈ orbit (edge_succ (mk_map (mk_graph iG) iM)) i"
      using assms succ_ok_imp_permutes
      by (intro permutation_self_in_orbit) (auto simp: permutation_permutes arcs_mkg)
    with assms show ?thesis by (simp add:orbit_es_eq_im arcs_mkg)
  qed

end

locale is_map_postcondition = is_map_postcondition0 +
  fixes so_i so_ok V A
  assumes rev: "rev_ok ⟷ bidirected_digraph (mk_graph iG) (edge_rev (mk_map (mk_graph iG) iM))"
  assumes succ_orbits: "is_map_succ_orbits_inv iG iM so_i so_ok V A" "succ_ok ⟶ is_map_final iG so_i so_ok"
begin

  lemma ok_imp_digraph:
    assumes rev_ok succ_ok so_ok
    shows "digraph_map (mk_graph iG) (mk_map (mk_graph iG) iM)"
  proof -
    interpret bidirected_digraph "mk_graph iG" "edge_rev (mk_map (mk_graph iG) iM)"
      using ‹rev_ok› by (simp add: rev)

    from ‹succ_ok› have perm: "edge_succ (mk_map (mk_graph iG) iM) permutes arcs (mk_graph iG)"
      by (simp add: succ_ok_imp_permutes)
    from ‹succ_ok› have ig_tail: "⋀a. a ∈ arcs (mk_graph iG) ⟹ ig_tail iG (im_succ iM a) = ig_tail iG a"
      by (simp_all add: succ_ok_tail_eq arcs_mkg)

    { fix v assume "v ∈ verts (mk_graph iG)" "out_arcs (mk_graph iG) v ≠ {}"
      then obtain a where a: "a ∈ arcs (mk_graph iG)" "tail (mk_graph iG) a = v" by auto metis
      then have "out_arcs (mk_graph iG) v = {b ∈ arcs (mk_graph iG). ig_tail iG a = ig_tail iG b}"
        by (auto simp: mkg_simps)
      also have "… ⊆ orbit (im_succ iM) a"
      proof -
        have "(∀i<length (snd iG). ∀j<length (snd iG).
            ig_tail iG i = ig_tail iG j ⟶ j ∈ orbit (im_succ iM) i)"
          using ‹succ_ok ›‹so_ok› succ_orbits unfolding is_map_succ_orbits_inv_def is_map_final_def by metis
        with a show ?thesis by (auto simp: arcs_mkg)
      qed
      finally have "out_arcs (mk_graph iG) v ⊆ orbit (im_succ iM) a" .
      moreover
      have "orbit (im_succ iM) a ⊆ out_arcs (mk_graph iG) v"
      proof -
        { fix x assume "x ∈ orbit (im_succ iM) a" then have "tail (mk_graph iG) x = v"
            using a ig_tail
            apply induct
             apply (auto simp: mkg_simps intro: orbit.intros)
            by (metis ‹succ_ok› contra_subsetD orbit_es_eq_im permutes_orbit_subset perm)
        } moreover
        have "orbit (im_succ iM) a ⊆ arcs (mk_graph iG)"
          using _ a(1) apply (rule orbit_ss)
          using assms arcs_mkg is_map_final_def is_map_succ_perm_inv_def succ_perm(1) succ_perm(2) by auto
        ultimately
        show ?thesis by auto
      qed
      ultimately
      have "out_arcs (mk_graph iG) v = orbit (edge_succ (mk_map (mk_graph iG) iM)) a"
        using ‹succ_ok› a by (auto simp: orbit_es_eq_im)
      then
      have "cyclic_on (edge_succ (mk_map (mk_graph iG) iM)) (out_arcs (mk_graph iG) v)"
        unfolding cyclic_on_def using a by force
    }
    with perm show ?thesis
      using ‹rev_ok› by unfold_locales (auto simp: mkg_simps arcs_mkg)
  qed

  lemma digraph_imp_ok:
    assumes dm: "digraph_map (mk_graph iG) (mk_map (mk_graph iG) iM)"
    assumes pred: "⋀i. i < length (ig_edges iG) ⟹ im_pred iM (im_succ iM i) = i"
    obtains rev_ok succ_ok so_ok
  proof
    interpret dm: digraph_map "mk_graph iG" "mk_map (mk_graph iG) iM" by (fact dm)

    show rev_ok unfolding rev by unfold_locales

    show succ_ok
    proof -
      { fix i assume "i ∈ arcs (mk_graph iG)"
        then have
            "edge_succ (mk_map (mk_graph iG) iM) i ∈ arcs (mk_graph iG)"
            "tail (mk_graph iG) (edge_succ (mk_map (mk_graph iG) iM) i) = tail (mk_graph iG) i"
          by auto
        then have
            "im_succ iM i < length (snd iG)"
            "ig_tail iG (im_succ iM i) = ig_tail iG i"
          unfolding es_eq_im[OF ‹i ∈ arcs _›] by (auto simp: arcs_mkg mkg_simps)
      }
      then have "(∀i<length (ig_edges iG).
        im_succ iM i < length (snd iG) ∧
        ig_tail iG (im_succ iM i) = ig_tail iG i ∧ im_pred iM (im_succ iM i) = i)"
        using pred by (auto simp: arcs_mkg es_eq_im)
      with succ_perm show ?thesis
        unfolding is_map_succ_perm_inv_def is_map_final_def by simp
    qed

    show so_ok
    proof -
      { fix i j assume "i < length (ig_edges iG)" "j < length (ig_edges iG)" "ig_tail iG i = ig_tail iG j"
        then have A: "i ∈ arcs (mk_graph iG)" "j ∈ arcs (mk_graph iG)" "tail (mk_graph iG) i = tail (mk_graph iG) j"
          by (auto simp: mkg_simps arcs_mkg)
        then have "cyclic_on (edge_succ (mk_map (mk_graph iG) iM)) (out_arcs (mk_graph iG) (tail (mk_graph iG) i))"
          by (auto intro!: dm.edge_succ_cyclic)
        then have "orbit (edge_succ (mk_map (mk_graph iG) iM)) i = out_arcs (mk_graph iG) (ig_tail iG i)"
          by (simp add: ‹i ∈ arcs (mk_graph iG)› mkg_simps orbit_cyclic_eq3)
        then have "j ∈ orbit (edge_succ (mk_map (mk_graph iG) iM)) i" using A by (simp add: mkg_simps)
        also have "orbit (edge_succ (mk_map (mk_graph iG) iM)) i = orbit (im_succ iM) i"
          using ‹i ∈ arcs _›
          by (rule orbit_cong0) (fastforce, simp add: es_eq_im)
        finally have "j ∈ orbit (im_succ iM) i" .
      }
      then show ?thesis
        using succ_orbits unfolding is_map_succ_orbits_inv_def is_map_final_def
        by safe (simp_all only: ‹succ_ok› simp_thms)
    qed
  qed

end

lemma all_less_Suc_eq: "(∀x < Suc n. P x) ⟷ (∀x < n. P x) ∧ P n"
  by (auto elim: less_SucE)

lemma in_orbit_imp_in_segment:
  assumes "y ∈ orbit f x" "x ≠ y" "bij f" shows "y ∈ segment f x (f y)"
  using assms
proof induct
  case base then show ?case by (auto intro: segment.intros simp: bij_iff)
next
  case (step y)
  show ?case
  proof (cases "x = y")
    case True then show ?thesis using step by (auto intro: segment.intros simp: bij_iff)
  next
    case False
    with step have "f y ≠ f (f y)" by (metis bij_is_inj inv_f_f not_in_segment2)
    then show ?thesis using step False
      by (auto intro: segment.intros segment_step_2 bij_is_inj)
  qed
qed


lemma ovalidNF_is_map: "
  ovalidNF (λs. distinct (ig_verts iG) ∧ wf_digraph (mk_graph iG))
    (is_map iG iM)
  (λr s. r ⟷ digraph_map (mk_graph iG) (mk_map (mk_graph iG) iM) ∧ (∀i < length (ig_edges iG). im_pred iM (im_succ iM i) = i))
"
  unfolding is_map_def
  apply (rewrite
    in "oreturn (length (ig_edges iG)) |>> (λecnt. ⌑)"
    to "owhile_inv _ _ _
      (λ(i, ok) s. is_map_rev_ok_inv iG iM i ok
        ∧ i ≤ ecnt ∧ wf_digraph (mk_graph iG))
      (measure (λ(i, ok). ecnt - i))
    " owhile_inv_def[symmetric] )
  apply (rewrite
    in "owhile_inv _ _ _ _ _ |>> (λ(rev_i, rev_ok). ⌑)"
    in "oreturn (length (ig_edges iG)) |>> (λecnt. ⌑)"
    to "owhile_inv _ _ _
      (λ(i, ok) s. is_map_succ_perm_inv iG iM i ok
        ∧ rev_ok = bidirected_digraph (mk_graph iG) (edge_rev (mk_map (mk_graph iG) iM))
        ∧ i ≤ ecnt ∧ wf_digraph (mk_graph iG))
      (measure (λ(i, ok). ecnt - i))
    " owhile_inv_def[symmetric] )
  apply (rewrite
    in "owhile_inv _ _ _ _ _ |>> (λ(succ_i, succ_ok). ⌑)"
    in "owhile_inv _ _ _ _ _ |>> (λ(rev_i, rev_ok). ⌑)"
    in "oreturn (length (ig_edges iG)) |>> (λecnt. ⌑)"
    to "owhile_inv _ _ _
      (λ(i, ok, V, A) s. is_map_succ_orbits_inv iG iM i ok V A
        ∧ rev_ok = bidirected_digraph (mk_graph iG) (edge_rev (mk_map (mk_graph iG) iM))
        ∧ is_map_succ_perm_inv iG iM succ_i succ_ok ∧ is_map_final iG succ_i succ_ok
        ∧ i ≤ ecnt ∧ wf_digraph (mk_graph iG))
      (measure (λ(i, ok, V, A). ecnt - i))
    " owhile_inv_def[symmetric] )
  apply (rewrite
    in "owhile_inv _ (λ(i, ok, V, A). ⌑) _ _ _"
    in "owhile_inv _ _ _ _ _ |>> (λ(succ_i, succ_ok). ⌑)"
    in "owhile_inv _ _ _ _ _ |>> (λ(rev_i, rev_ok). ⌑)"
    in "oreturn (length (ig_edges iG)) |>> (λecnt. ⌑)"
    to "owhile_inv _ _ _
      (λ(A', j) s. is_map_succ_orbits_inner_inv iG iM i j A'
        ∧ ig_tail iG i ∉ V ∧ succ_ok ∧ ok ∧ is_map_succ_orbits_inv iG iM i ok V A
        ∧ rev_ok = bidirected_digraph (mk_graph iG) (edge_rev (mk_map (mk_graph iG) iM))
        ∧ is_map_succ_perm_inv iG iM succ_i succ_ok ∧ is_map_final iG succ_i succ_ok
        ∧ i < ecnt ∧ wf_digraph (mk_graph iG))
      (measure (λ(A',j). length (ig_edges iG) - card A'))
    " owhile_inv_def[symmetric] )
proof vcg_casify
  let ?es = "edge_succ (mk_map (mk_graph iG) iM)"

  { case weaken then show ?case by (auto simp: is_map_rev_ok_inv_def)
  }
  { case (while i ok)
    { case invariant
      case weaken then show ?case by (auto simp: is_map_rev_ok_inv_def elim: less_SucE)
    }
    { case wf show ?case by auto
    }
    { case postcondition
      then have "ok ⟷ bidirected_digraph (mk_graph iG) (edge_rev (mk_map (mk_graph iG) iM))"
        by (intro rev_ok_final) (auto simp: is_map_final_def)
      with postcondition show ?case by (auto simp: is_map_succ_perm_inv_def)
    }
  }
  case (bind _ rev_ok)
  { case (while i ok)
    { case invariant case weaken
      then show ?case by (auto simp: is_map_succ_perm_inv_def elim: less_SucE)
    }
    { case wf show ?case by auto
    }
    { case postcondition
      then show ?case by (auto simp: is_map_final_def is_map_succ_orbits_inv_def)
    }
  }
  case (bind succ_i succ_ok)
  { case (while i ok V A)
    { case invariant
      { case weaken
        then interpret pc0: is_map_postcondition0 iG iM rev_ok succ_i succ_ok
          by unfold_locales auto
        from weaken.loop_cond have "i < length (ig_edges iG)" succ_ok ok by auto
        with weaken.loop_inv have
            V: "V = {ig_tail iG k |k. k < i}" and
            A: "A = (⋃ k<i. orbit (im_succ iM) k)"
          by (simp_all add: is_map_succ_orbits_inv_def)
        show ?case
        proof branch_casify
          case "then" case g
          have V': "V = {ig_tail iG ia |ia. ia < (if i ∈ A then Suc i else Suc i - 1)}"
            using g ‹V = _› by (auto elim: less_SucE)

          have "is_map_succ_orbits_inv iG iM (Suc i) (i ∈ A) V A"
          proof (cases "i ∈ A")
            case True
            obtain j where j: "j < i" "i ∈ orbit (im_succ iM) j"
              using True ‹A = _› by auto
            have i_in_less_i: "∃x∈{..<i}. i ∈ orbit (im_succ iM) x"
              using True ‹A = _› by auto
            have A': "A = (⋃ i<if True then Suc i else Suc i - 1. orbit (im_succ iM) i)"
              using True unfolding ‹A = _› by (auto 4 3 intro: orbit_trans elim: less_SucE)

            have X: "∀k<i. ∀l<i. ig_tail iG k = ig_tail iG l ⟶ l ∈ orbit (im_succ iM) k"
              using weaken unfolding is_map_succ_orbits_inv_def by metis
            moreover
            { fix j assume j: "j < i" "ig_tail iG j = ig_tail iG i"
              from i_in_less_i obtain k where k: "k < i" "i ∈ orbit (im_succ iM) k" by auto
              then have "ig_tail iG k = ig_tail iG i"
                using ‹succ_ok› ‹i < _› by (auto elim: pc0.in_orbit_im_succE)
              then have "k ∈ orbit (im_succ iM) j"
                using j ‹ig_tail iG k = _› k X by auto
              then have "i ∈ orbit (im_succ iM) j" using k by (auto intro: orbit_trans)
            }
            ultimately
            have "∀k<Suc i. ∀l<Suc i. ig_tail iG k = ig_tail iG l ⟶ l ∈ orbit (im_succ iM) k"
              unfolding all_less_Suc_eq using ‹i < _› ‹succ_ok›
              by (auto intro: orbit_swap pc0.self_in_orbit_im_succ)
            with True show ?thesis
              by (simp only: A' V' simp_thms is_map_succ_orbits_inv_def)
          next
            case False

            from V g obtain j where j: "j < i" "ig_tail iG j = ig_tail iG i" by auto
            with False show ?thesis
              by (auto 0 3 simp: is_map_succ_orbits_inv_def V' A intro: exI[where x=j] exI[where x=i])
          qed
          then show ?case using weaken by auto
        next
          case "else" case g
          have "is_map_succ_orbits_inner_inv iG iM i i {}"
            unfolding is_map_succ_orbits_inner_inv_def
            using ‹succ_ok› ‹i < _› by (auto simp: pc0.self_in_orbit_im_succ)
          with g weaken show ?case by blast
        qed
      }
      { case "if" case else case (while A' i')
        { case invariant case weaken
          then interpret pc0: is_map_postcondition0 iG iM rev_ok succ_i succ_ok
            by unfold_locales auto
          have "succ_ok" "i < length (ig_edges iG)" "i' ∈ orbit (im_succ iM) i"
            using weaken by (auto simp: is_map_succ_orbits_inner_inv_def)
          have "i' < length (ig_edges iG)"
            using ‹i' ∈ _› ‹succ_ok› ‹i < _› by (rule pc0.in_orbit_im_succE)

          { assume "i' ∈ orbit (im_succ iM) i" "i ≠ i'"
            then have "i' ∈ orbit (?es) i"
              by (subst pc0.orbit_es_eq_im) (auto simp add: ‹succ_ok› ‹i < _› arcs_mkg)
            then have "i' ∈ segment (?es) i (?es i')"
              using ‹i ≠ i'› pc0.succ_ok_imp_permutes ‹succ_ok ›
              by (intro in_orbit_imp_in_segment) (auto simp: permutes_conv_has_dom)
            then have "i' ∈ segment (im_succ iM) i (im_succ iM i')"
              by (subst pc0.segment_es_eq_im[symmetric] es_eq_im[symmetric];
                  auto simp add: ‹succ_ok› ‹i < _› ‹i' < _› arcs_mkg)+
          } note X = this

          { fix x assume "x ∈ segment (im_succ iM) i i'" "i ≠ i'"
            then have "x ∈ segment (?es) i i'"
              by (subst pc0.segment_es_eq_im) (auto simp add: ‹succ_ok› ‹i < _› ‹i' < _› arcs_mkg)
            then have "x ∈ segment (?es) i (?es i')"
              using ‹i ≠ i'› pc0.succ_ok_imp_permutes ‹succ_ok ›
              by (auto simp: permutes_conv_has_dom bij_is_inj intro: segment_step_2)
            then have "x ∈ segment (im_succ iM) i (im_succ iM i')"
              by (subst pc0.segment_es_eq_im[symmetric] es_eq_im[symmetric];
                  auto simp add: ‹succ_ok› ‹i < _› ‹i' < _› arcs_mkg)+
          } note Y = this

          have Z: "is_map_succ_orbits_inner_inv iG iM i (im_succ iM i') (insert i' A')"
            using weaken unfolding is_map_succ_orbits_inner_inv_def
            by (auto dest: segment_step_2D X Y simp: orbit.intros segment1_empty split: if_splits)

          have "A' ⊆ orbit (im_succ iM) i"
            using weaken unfolding is_map_succ_orbits_inner_inv_def
            by (auto simp: pc0.self_in_orbit_im_succ dest: segmentD_orbit split: if_splits)
          also have "… ⊆ arcs (mk_graph iG)"
            by (rule orbit_ss) (auto simp: arcs_mkg pc0.im_succ_le_length ‹succ_ok› ‹i < _›)
          finally have "card A' < card (arcs (mk_graph iG))" "finite A'"
            using ‹i' ∉ A'›  ‹i' < _›
            by - (intro psubset_card_mono, auto simp: arcs_mkg intro: finite_subset)
          then have "card A' < length (ig_edges iG)" by (simp add: arcs_mkg)
          show ?case
            using weaken Z ‹card A' < length _› by (auto simp: card_insert_if ‹finite A'›)
        }
        { case wf show ?case by simp
        }
        { case postcondition
          then interpret pc0: is_map_postcondition0 iG iM rev_ok succ_i succ_ok
            by unfold_locales auto
          from postcondition have "ok" "succ_ok" "i < length (ig_edges iG)" by simp_all

          from postcondition
          have "i' ∈ A'"
              "A' = (if i = i' ∧ i ∉ A' then {} else {i} ∪ segment (im_succ iM) i i')"
              "i' ∈ orbit (im_succ iM) i"
              "ig_tail iG i ∉ V"
            by (simp_all add: is_map_succ_orbits_inner_inv_def)
          moreover
          then have "i = i'" by (simp split: if_splits add: not_in_segment2)
          ultimately
          have "A' = {i} ∪ segment (im_succ iM) i i" by simp
          also have "segment (im_succ iM) i i = segment ?es i i"
            by (auto simp: pc0.segment_es_eq_im ‹succ_ok› ‹i < _› arcs_mkg)
          also have "… = orbit ?es i - {i}"
            using pc0.succ_ok_imp_permutes ‹succ_ok›
            by (auto simp: permutation_permutes arcs_mkg intro!: segment_x_x_eq)
          also have "… = orbit (im_succ iM) i - {i}"
            by (auto simp: pc0.orbit_es_eq_im ‹succ_ok› ‹i < _› arcs_mkg)
          finally
          have A': "A' = orbit (im_succ iM) i"
            using ‹i < _› ‹succ_ok› by (auto simp: pc0.self_in_orbit_im_succ)

          from postcondition
          have "A = (⋃k<i. orbit (im_succ iM) k)"
            unfolding is_map_succ_orbits_inner_inv_def by (simp add: is_map_succ_orbits_inv_def)
          have "A ∪ A' = (⋃k<Suc i. orbit (im_succ iM) k)"
            unfolding A' ‹A = _› by (auto 2 3 elim: less_SucE)

          from postcondition have "V = {ig_tail iG ia |ia. ia < i}"
            by (auto simp: ‹ok› is_map_succ_orbits_inv_def)
          then have V': "insert (ig_tail iG i') V = {ig_tail iG ia |ia. ia < Suc i}"
            by (auto simp add: ‹i = i'› elim: less_SucE)

          have *: "⋀k. k < i ⟹ ig_tail iG k ≠ ig_tail iG i"
            using ‹V = _› ‹ig_tail iG i ∉ V› by auto

          from postcondition have "(∀k<i. ∀l<i. ig_tail iG k = ig_tail iG l ⟶ l ∈ orbit (im_succ iM) k)"
            by (simp add: is_map_succ_orbits_inv_def ‹ok›)
          then have X: "(∀k<Suc i. ∀l<Suc i. ig_tail iG k = ig_tail iG l ⟶ l ∈ orbit (im_succ iM) k)"
            by (auto simp add: all_less_Suc_eq pc0.self_in_orbit_im_succ ‹succ_ok› ‹i < _› dest: *)

          have "is_map_succ_orbits_inv iG iM (i + 1) True (insert (ig_tail iG i') V) (A ∪ A')"
            unfolding is_map_succ_orbits_inv_def by (simp add: ‹A ∪ A' = _› V' X)
          then show ?case
            using postcondition ‹i < _› by auto
        }
      }
    }
    { case wf show ?case by auto
    }
    { case postcondition
      interpret pc: is_map_postcondition iG iM rev_ok succ_i succ_ok i ok V A
        using postcondition by unfold_locales (auto simp: is_map_final_def)

      show ?case (is "?L = ?R")
        by (auto simp add: pc.ok_imp_digraph dest: pc.succ_ok_imp_pred elim: pc.digraph_imp_ok)
    }
  }
qed

declare ovalidNF_is_map[THEN ovalidNF_wp, THEN trivial_label, vcg_l]


subsubsection ‹@{term isolated_nodes}›

definition "inv_isolated_nodes s iG vcnt ecnt ≡
  vcnt = length (ig_verts iG)
  ∧ ecnt = length (ig_edges iG)
  ∧ distinct (ig_verts iG)
  ∧ sym_digraph (mk_graph iG)
  "

definition "inv_isolated_nodes_outer iG i nz ≡
  nz = card (pre_digraph.isolated_verts (mk_graph iG) ∩ set (take i (ig_verts iG)))"

definition "inv_isolated_nodes_inner iG v j ≡
  ∀k < j. v ≠ ig_tail iG k ∧ v ≠ ig_head iG k"

lemma (in sym_digraph) in_arcs_empty_iff:
  "in_arcs G v = {} ⟷ out_arcs G v = {}"
  by (auto simp: out_arcs_def in_arcs_def)
     (metis graph_symmetric in_arcs_imp_in_arcs_ends reachableE)+

lemma take_nth_distinct:
  "⟦distinct xs; n < length xs; xs ! n ∈ set (take n xs)⟧ ⟹ False"
  by (fastforce simp: distinct_conv_nth in_set_conv_nth)

lemma ovalidNF_isolated_nodes: "
  ovalidNF (λs. distinct (ig_verts iG) ∧ sym_digraph (mk_graph iG))
    (isolated_nodes iG)
  (λr s. r = (card (pre_digraph.isolated_verts (mk_graph iG))))"
  unfolding isolated_nodes_def
  apply (rewrite
    in "oreturn (length (ig_verts iG)) |>> (λvcnt. ⌑)"
    in "oreturn (length (ig_edges iG)) |>> (λecnt. ⌑)"
    to "owhile_inv _ _ _
      (λ(i, nz) s. inv_isolated_nodes s iG vcnt ecnt
            ∧ inv_isolated_nodes_outer iG i nz
            ∧ i ≤ vcnt)
      (measure (λ(i, nz). vcnt - i))
    " owhile_inv_def[symmetric] )
  apply (rewrite
    in "oreturn (fst iG ! i) |>> (λv. ⌑)"
    in "owhile_inv _ (λ(i, nz). ⌑)"
    in "oreturn (length (ig_verts iG)) |>> (λvcnt. ⌑)"
    in "oreturn (length (ig_edges iG)) |>> (λecnt. ⌑)"
    to "owhile_inv _ _ _
      (λ(j, ret) s. inv_isolated_nodes s iG vcnt ecnt
           ∧ inv_isolated_nodes_inner iG v j
           ∧ inv_isolated_nodes_outer iG i nz
           ∧ v = ig_verts iG ! i
           ∧ ret = (j < ecnt ∧ ig_tail iG j ≠ v ∧ ig_head iG j ≠ v)
           ∧ i < vcnt
           ∧ j ≤ ecnt)
      (measure (λ(j, ret). ecnt - j))
    " owhile_inv_def[symmetric])
proof vcg_casify
  case (weaken s)
  then show ?case
    by (auto simp: inv_isolated_nodes_def inv_isolated_nodes_outer_def)
next
  case (while i nz)
  { case invariant
    { case (weaken s')
      then show ?case unfolding BRANCH_def by (auto simp: inv_isolated_nodes_inner_def)
    next
      case bind
      case bind
      case (while j cond)
      { case invariant
        { case weaken
          show ?case
          proof branch_casify
            case "else" case "else" case g
            with weaken have "length (ig_edges iG) = j + 1" by linarith
            with weaken show ?case
              by (auto simp: inv_isolated_nodes_inner_def elim: less_SucE)
          qed (insert weaken, auto simp: inv_isolated_nodes_inner_def elim: less_SucE)
        }
      next
        case wf show ?case by auto
      next
        case postcondition
        interpret G: sym_digraph "mk_graph iG" using postcondition by (simp add: inv_isolated_nodes_def)

        have ?var using postcondition by auto

        let ?v = "ig_verts iG ! i"

        { assume A: "j = length (snd iG)"
          have "?v ∈ pre_digraph.isolated_verts (mk_graph iG)"
            using A postcondition by (auto simp: pre_digraph.isolated_verts_def mkg_simps inv_isolated_nodes_inner_def arcs_mkg)

          have "distinct (ig_verts iG)" "?v = ig_verts iG ! i" "i < length (ig_verts iG)"
            using postcondition by (auto simp: inv_isolated_nodes_def)
          then have "?v ∉ set (take i (ig_verts iG))"
            by (metis take_nth_distinct)

          have "Suc (card (pre_digraph.isolated_verts (mk_graph iG) ∩ set (take i (fst iG))))
              = card (insert ?v (pre_digraph.isolated_verts (mk_graph iG) ∩ set (take i (fst iG))))" (is "_ = card ?S")
            using ‹?v ∉ _› by simp
          also have "?S = pre_digraph.isolated_verts (mk_graph iG) ∩ set (take (Suc i) (fst iG))"
            using ‹?v ∈ _› ‹i < _› ‹?v = _› by (auto simp: take_Suc_conv_app_nth)
          finally
          have "inv_isolated_nodes_outer iG (Suc i) (Suc nz)"
            using postcondition by (auto simp: inv_isolated_nodes_outer_def)
        }
        moreover
        { assume A: "j ≠ length (snd iG)"

          then have *: "j ∈ (out_arcs (mk_graph iG) ?v ∪ in_arcs (mk_graph iG) ?v)"
            using postcondition by (auto simp: arcs_mkg mkg_simps ig_tail_def ig_head_def)
          then have "out_arcs (mk_graph iG) ?v ≠ {}"
            by (auto simp del: in_in_arcs_conv in_out_arcs_conv)
               (auto simp: G.in_arcs_empty_iff[symmetric])
          then have "?v ∉ pre_digraph.isolated_verts (mk_graph iG)"
            by (auto simp: pre_digraph.isolated_verts_def)
          then have "inv_isolated_nodes_outer iG (Suc i) nz"
            using postcondition by (auto simp: inv_isolated_nodes_outer_def take_Suc_conv_app_nth)
        }
        ultimately
        have ?inv using postcondition by auto
        from ‹?var› ‹?inv› show ?case by blast
      }
    }
  next
    case wf show ?case by auto
  next
    case postcondition
    have "pre_digraph.isolated_verts (mk_graph iG) ∩ set (fst iG) = pre_digraph.isolated_verts (mk_graph iG)"
      by (auto simp: pre_digraph.isolated_verts_def mkg_simps)
    with postcondition show ?case
      by (auto simp: inv_isolated_nodes_def inv_isolated_nodes_outer_def)
  }
qed

declare ovalidNF_isolated_nodes[THEN ovalidNF_wp, THEN trivial_label, vcg_l]



subsubsection ‹@{term face_cycles}›

definition "inv_face_cycles s iG iM ecnt ≡
  ecnt = length (ig_edges iG)
  ∧ digraph_map (mk_graph iG) iM
  "

definition fcs_upto :: "nat pre_map ⇒ nat ⇒ nat set set" where
  "fcs_upto iM i ≡ {pre_digraph_map.face_cycle_set iM k | k. k < i}"

definition "inv_face_cycles_outer s iG iM i c edge_info ≡
  let fcs = fcs_upto iM i in
  c = card fcs
  ∧ (∀k < length (ig_edges iG). k ∈ edge_info ⟷ k ∈ ⋃fcs)"

definition "inv_face_cycles_inner s iG iM i j c edge_info ≡
  j ∈ pre_digraph_map.face_cycle_set iM i
  ∧ c = card (fcs_upto iM i)
  ∧ i ∉ ⋃(fcs_upto iM i)
  ∧ (∀k < length (ig_edges iG). k ∈ edge_info ⟷
    (k ∈ ⋃(fcs_upto iM i)
    ∨ (∃l < funpow_dist1 (pre_digraph_map.face_cycle_succ iM) i j. (pre_digraph_map.face_cycle_succ iM ^^ l) i = k)))"

lemma finite_fcs_upto: "finite (fcs_upto iM i)"
  by (auto simp: fcs_upto_def)

lemma card_orbit_eq_funpow_dist1:
  assumes "x ∈ orbit f x" shows "card (orbit f x) = funpow_dist1 f x x"
proof -
  have "card (orbit f x) = card ((λn. (f ^^ n) x) ` {0..<funpow_dist1 f x x})"
    using assms by (simp only: orbit_conv_funpow_dist1[symmetric])
  also have "… = card {0..<funpow_dist1 f x x}"
    using assms by (intro card_image inj_on_funpow_dist1)
  finally show ?thesis by simp
qed

lemma funpow_dist1_le:
  assumes "y ∈ orbit f x" "x ∈ orbit f x"
  shows "funpow_dist1 f x y ≤ funpow_dist1 f x x"
    using assms by (intro funpow_dist1_le_self funpow_dist1_prop) simp_all

lemma funpow_dist1_le_card:
  assumes "y ∈ orbit f x" "x ∈ orbit f x"
  shows "funpow_dist1 f x y ≤ card (orbit f x)"
  using funpow_dist1_le[OF assms] using assms
  by (simp add: card_orbit_eq_funpow_dist1)

lemma (in digraph_map) funpow_dist1_le_card_fcs:
  assumes "b ∈ face_cycle_set a"
  shows "funpow_dist1 face_cycle_succ a b ≤ card (face_cycle_set a)"
  by (metis assms face_cycle_set_def face_cycle_set_self funpow_dist1_le_card)

lemma funpow_dist1_f_eq:
  assumes "b ∈ orbit f a" "a ∈ orbit f a" "a ≠ b"
  shows "funpow_dist1 f a (f b) = Suc (funpow_dist1 f a b)"
proof -
  have f_inj: "inj_on (λn. (f ^^ n) a) {0..<funpow_dist1 f a a}"
    by (rule inj_on_funpow_dist1) (rule assms)
  have "funpow_dist1 f a b ≤ funpow_dist1 f a a"
    using assms by (intro funpow_dist1_le)
  moreover
  have "funpow_dist1 f a b ≠ funpow_dist1 f a a"
    by (metis assms funpow_dist1_prop)
  ultimately
  have f_less: "funpow_dist1 f a b < funpow_dist1 f a a" by simp

  have f_Suc_eq: "(f ^^ Suc (funpow_dist1 f a b)) a = f b"
    using assms by (metis funpow.simps(2) o_apply funpow_dist1_prop)
  show ?thesis
  proof (cases "f b = a")
    case True
    then show ?thesis
      by (metis Suc_lessI f_Suc_eq f_less assms(2) funpow.simps(1) funpow_neq_less_funpow_dist1 id_apply old.nat.distinct(1) zero_less_Suc)
  next
    case False
    then have *: "Suc (funpow_dist1 f a b) < funpow_dist1 f a a"
      using f_Suc_eq by (metis assms(2) f_less funpow_dist1_prop le_less_Suc_eq less_Suc_eq_le not_less_eq)
    from f_inj have **: "⋀n. n < funpow_dist1 f a a ⟹ n ≠ Suc (funpow_dist1 f a b) ⟹ (f ^^ n) a ≠ f b"
      using f_Suc_eq by (auto dest!: inj_onD) (metis * assms(2) f_Suc_eq funpow_neq_less_funpow_dist1)
    show ?thesis
    proof (rule ccontr)
      assume A: "¬?thesis"
      have "(f ^^ (funpow_dist1 f a (f b))) a  = f b"
        using assms by (intro funpow_dist1_prop) (simp add: orbit.intros)
      with A ** have "funpow_dist1 f a a ≤ (funpow_dist1 f a (f b))"
        by (metis less_Suc_eq_le not_less_eq)
      then have "Suc (funpow_dist1 f a b) < (funpow_dist1 f a (f b))" using * by linarith
      then have "(f ^^ Suc (funpow_dist1 f a b)) a ≠ f b"
        by (intro funpow_dist1_least) simp_all
      then show False using f_Suc_eq by simp
    qed
  qed
qed

lemma (in -) funpow_dist1_less_f:
  assumes "b ∈ orbit f a" "a ∈ orbit f a" "a ≠ b"
  shows "funpow_dist1 f a b < funpow_dist1 f a (f b)"
  using assms by (simp add: funpow_dist1_f_eq)

lemma ovalidNF_face_cycles: "
  ovalidNF (λs. digraph_map (mk_graph iG) iM)
    (face_cycles iG iM)
  (λr s. r = card (pre_digraph_map.face_cycle_sets (mk_graph iG) iM))
"
  unfolding face_cycles_def
  apply (rewrite
    in "oreturn (length (ig_edges iG)) |>> (λecnt. ⌑)"
    to "owhile_inv _ _ _
          (λ(edge_info, c, i) s. inv_face_cycles s iG iM ecnt
            ∧ inv_face_cycles_outer s iG iM i c edge_info
            ∧ i ≤ ecnt)
          (measure (λ(edge_info, c, i). ecnt - i))
      " owhile_inv_def[symmetric]
  )
  apply (rewrite
    in "owhile_inv _ (λ(_, c, i). ⌑)"
    in "oreturn (length (ig_edges iG)) |>> (λecnt. ⌑)"
    to "owhile_inv _ _ _
          (λ(edge_info, j) s. inv_face_cycles s iG iM ecnt
            ∧ inv_face_cycles_inner s iG iM i j c edge_info
            ∧ i < ecnt)
          (measure (λ(edge_info, j). card (pre_digraph_map.face_cycle_set iM i) - funpow_dist1 (pre_digraph_map.face_cycle_succ iM) i j))
      " owhile_inv_def[symmetric]
  )
proof vcg_casify
  { case (weaken s)
    then show ?case by (auto simp add: inv_face_cycles_def inv_face_cycles_outer_def fcs_upto_def)
  }
  { case (while edge_info c i)
    { case (postcondition s)
      moreover have "fcs_upto iM (length (ig_edges iG))
          = pre_digraph_map.face_cycle_sets (mk_graph iG) iM"
        by (auto simp: pre_digraph_map.face_cycle_sets_def arcs_mkg fcs_upto_def)
      ultimately show ?case by (auto simp: inv_face_cycles_outer_def Let_def)
    }
    { case (invariant s)
      { case (weaken s')
        interpret G: digraph_map "mk_graph iG" iM
          using weaken by (auto simp: inv_face_cycles_def)
        show ?case
        proof branch_casify
          case else case g
          then have "G.face_cycle_set i ∈ {G.face_cycle_set k |k. k < i}"
            using weaken by (auto simp: inv_face_cycles_outer_def fcs_upto_def dest: G.face_cycle_eq)
          then have "{G.face_cycle_set k |k. k < Suc i} = {G.face_cycle_set k |k. k < i}"
            by (auto elim: less_SucE)
          then have "inv_face_cycles_outer s' iG iM (i + 1) c edge_info"
            using weaken unfolding inv_face_cycles_outer_def by (auto simp: fcs_upto_def)
          then have ?inv using weaken by auto
          then show ?case using weaken by auto
        next
          case "then" case g
          have fd1_triv: "⋀f x. funpow_dist1 f x (f x) = 1"
            by (simp add: funpow_dist_0)
          have fcs_in: "G.face_cycle_succ i ∈ G.face_cycle_set i"
            by (simp add: G.face_cycle_succ_inI)

          have i_not_in_fcs: "i ∉ ⋃(fcs_upto iM i)"
            using g weaken
            by (auto simp: inv_face_cycles_outer_def fcs_upto_def)

          from weaken show ?case
            unfolding inv_face_cycles_inner_def inv_face_cycles_outer_def
            using i_not_in_fcs by (auto simp: fd1_triv fcs_in fcs_upto_def)
        qed
      }
      { case "if" case "then"
        { case (while edge_info j)
          { case (postcondition s')

            interpret G: digraph_map "mk_graph iG" iM
              using postcondition by (auto simp: inv_face_cycles_def)

            have ?var using postcondition by auto

            have fu_Suc: "fcs_upto iM (Suc j) = fcs_upto iM j ∪ {G.face_cycle_set j}"
              by (auto simp: fcs_upto_def elim: less_SucE)
            moreover
            have "G.face_cycle_set j ∉ fcs_upto iM j" "c  = card (fcs_upto iM j)"
              using postcondition by (auto simp: inv_face_cycles_inner_def)
            ultimately
            have "Suc c = card (fcs_upto iM (Suc j))" by (simp add: finite_fcs_upto)

            have *: "∀k<length (snd iG). k ∈ edge_info ⟷ (∃x∈fcs_upto iM (Suc j). k ∈ x)"
            proof -
              have *: "j ∈ orbit G.face_cycle_succ j"
                by (simp add: G.face_cycle_set_def[symmetric])
              have "⋀k. (∃l<funpow_dist1 G.face_cycle_succ j j. (G.face_cycle_succ ^^ l) j = k) ⟷ (k ∈ G.face_cycle_set j)"
                by (auto simp: G.face_cycle_set_def orbit_conv_funpow_dist1[OF *])
              moreover
              from postcondition have "inv_face_cycles_inner s' iG iM j j c edge_info"
                by auto
              ultimately
              show ?thesis unfolding inv_face_cycles_inner_def fu_Suc by auto
            qed

            have ?inv using postcondition *
              by (auto simp: inv_face_cycles_outer_def ‹Suc c = _›)
            with ‹?var› show ?case by blast
          }
          { case (invariant s')
            { case (weaken s'')
              interpret G: digraph_map "mk_graph iG" iM
                using weaken by (auto simp: inv_face_cycles_def)
              have "j ∈ G.face_cycle_set i"
                using weaken by (auto simp: inv_face_cycles_inner_def)
              then have "j ∈ arcs (mk_graph iG)"
                by (metis G.face_cycle_set_def G.funpow_face_cycle_succ_no_arc G.in_face_cycle_setD
                  funpow_dist1_prop weaken.loop_cond)

              have A: "j ∈ pre_digraph_map.face_cycle_set iM i"
                using weaken by (auto simp: inv_face_cycles_inner_def)
              then have A': "(G.face_cycle_succ ^^ funpow_dist1 G.face_cycle_succ i j) i = j"
                by (intro funpow_dist1_prop) (simp add: G.face_cycle_set_def[symmetric])

              { fix k
                have *: "⋀i n f x . i < n ⟹ ∃j<n. (f ^^ j) x = (f ^^ i) x" by auto

                have "(∃l<funpow_dist1 G.face_cycle_succ i (G.face_cycle_succ j). (G.face_cycle_succ ^^ l) i = k)
                    ⟷ (∃l<Suc (funpow_dist1 G.face_cycle_succ i j). (G.face_cycle_succ ^^ l) i = k)" (is "?L ⟷ _")
                  using A ‹i ≠ j›
                  by (subst funpow_dist1_f_eq) (simp_all add: G.face_cycle_set_def[symmetric])
                also have "… ⟷ (∃l<funpow_dist1 G.face_cycle_succ i j. (G.face_cycle_succ ^^ l) i = k) ∨ k = j" (is "_ ⟷ ?R")
                  using A' by (fastforce elim: less_SucE
                    intro: * exI[where x="(funpow_dist1 G.face_cycle_succ i j)"])
                finally have "?L ⟷ ?R" .
              } note B = this

              have ?inv
                using weaken unfolding inv_face_cycles_inner_def B
                by (auto simp: G.face_cycle_succ_inI)

              have X: "funpow_dist1 G.face_cycle_succ i j < card (G.face_cycle_set i)"
              proof -
                have "funpow_dist1 G.face_cycle_succ i j ≤ funpow_dist1 G.face_cycle_succ i i"
                  using _ _ A unfolding G.face_cycle_set_def
                  apply (rule funpow_dist1_le_self)
                   apply (rule funpow_dist1_prop)
                   unfolding G.face_cycle_set_def[symmetric]
                   by simp_all
                moreover have "funpow_dist1 G.face_cycle_succ i j ≠ funpow_dist1 G.face_cycle_succ i i"
                  by (metis A G.face_cycle_set_def G.face_cycle_set_self funpow_dist1_prop
                    weaken.loop_cond)
                ultimately
                have "funpow_dist1 G.face_cycle_succ i j < funpow_dist1 G.face_cycle_succ i i"
                  by simp
                also have "… ≤ card (G.face_cycle_set i)"
                  by (rule G.funpow_dist1_le_card_fcs) simp
                finally show ?thesis .
              qed

              have ?var
                apply simp
                using _ X apply (rule diff_less_mono2)
                apply (rule funpow_dist1_less_f)
                  using ‹i ≠ j› A by (auto simp: G.face_cycle_set_def[symmetric])
              with ‹?inv› show ?case by blast
            }
          }
        }
      }
    }
  }
qed auto
declare ovalidNF_face_cycles[THEN ovalidNF_wp, THEN trivial_label, vcg_l]

lemma ovalidNF_euler_genus: "
  ovalidNF (λs. distinct (ig_verts iG) ∧ digraph_map (mk_graph iG) iM ∧ c = card (pre_digraph.sccs (mk_graph iG)))
    (euler_genus iG iM c)
  (λr s. r = pre_digraph_map.euler_genus (mk_graph iG) iM)
"
  unfolding euler_genus_def
proof vcg_casify
  case weaken
  have "distinct (ig_verts iG)" using weaken by simp
  interpret G: digraph_map "mk_graph iG" iM using weaken by simp
  have len_card:
      "length (ig_verts iG) = card (verts (mk_graph iG))"
      "length (ig_edges iG) = card (arcs (mk_graph iG))"
    using ‹distinct _› by (auto simp: mkg_simps arcs_mkg distinct_card)
  show ?case
    using weaken by (auto simp: G.euler_genus_def G.euler_char_def len_card)
qed

declare ovalidNF_euler_genus[THEN ovalidNF_wp, THEN trivial_label, vcg_l]

lemma ovalidNF_certify: "
  ovalidNF (λs. distinct (ig_verts iG) ∧ fin_digraph (mk_graph iG) ∧ c = card (pre_digraph.sccs (mk_graph iG)))
    (certify iG iM c)
  (λr s. r ⟷ pre_digraph_map.euler_genus (mk_graph iG) (mk_map (mk_graph iG) iM) = 0
    ∧ digraph_map (mk_graph iG) (mk_map (mk_graph iG) iM)
    ∧ (∀i < length (ig_edges iG). im_pred iM (im_succ iM i) = i) )
"
  unfolding certify_def
proof vcg_casify
  case weaken
  then interpret fin_digraph "mk_graph iG" by auto
  from weaken show ?case by (auto simp: BRANCH_def intro: wf_digraph)
qed

end