theory Check_Connected_Impl
imports
  "~/P/afp/thys/Simpl/Vcg"
begin

text {* Implemenation *}

type_synonym IVertex = nat
type_synonym IEdge_Id = nat
type_synonym IEdge = "IVertex \<times> IVertex"
type_synonym IGraph = "nat \<times> nat \<times> (IEdge_Id \<Rightarrow> IEdge)" (* last vertex vs. set/list of vertices? *)

abbreviation iedge_cnt :: "IGraph \<Rightarrow> nat"
  where "iedge_cnt G \<equiv> fst (snd G)"

abbreviation iedges :: "IGraph \<Rightarrow> IEdge_Id \<Rightarrow> IEdge"
  where "iedges G \<equiv> snd (snd G)"

definition has_unique_edges_inv1 :: "IGraph \<Rightarrow> nat \<Rightarrow> bool" where
  "has_unique_edges_inv1 G k \<equiv> \<forall>i < k. \<forall>j < iedge_cnt G. i \<noteq> j \<longrightarrow> iedges G i \<noteq> iedges G j"

definition has_unique_edges_inv2 :: "IGraph \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
  "has_unique_edges_inv2 G i k \<equiv> \<forall>j < k. i \<noteq> j \<longrightarrow> iedges G i \<noteq> iedges G j"

procedures has_unique_edges (G :: IGraph | R :: bool)
  where
    i :: nat
    j :: nat
    e1 :: IEdge
    e2 :: IEdge
  in "
    ANNO G.
      \<lbrace> \<acute>G = G \<rbrace>
      \<acute>R :== True ;;
      \<acute>i :== 0 ;;
      TRY
        WHILE \<acute>i < iedge_cnt \<acute>G
        INV \<lbrace> has_unique_edges_inv1 \<acute>G \<acute>i  \<and> \<acute>i \<le> iedge_cnt \<acute>G \<and> \<acute>R = True \<and> \<acute>G = G\<rbrace>
        DO
          \<acute>e1 :== iedges \<acute>G \<acute>i ;;
          \<acute>j :== 0 ;;
          WHILE \<acute>j < iedge_cnt \<acute>G
          INV \<lbrace> has_unique_edges_inv2 \<acute>G \<acute>i \<acute>j \<and> \<acute>e1 = iedges \<acute>G \<acute>i \<and> \<acute>i < iedge_cnt \<acute>G \<and> \<acute>j \<le> iedge_cnt \<acute>G
            \<and> has_unique_edges_inv1 \<acute>G \<acute>i \<and> \<acute>R = True \<and> \<acute>G = G\<rbrace>
          DO
            \<acute>e2 :== iedges \<acute>G \<acute>j ;;
            IF \<acute>i \<noteq> \<acute>j \<and> fst \<acute>e1 = fst \<acute>e2 \<and> snd \<acute>e1 = snd \<acute>e2 THEN
              \<acute>R :== False ;;
              THROW
            FI ;;
            \<acute>j :== \<acute>j + 1
          OD ;;
          \<acute>i :== \<acute>i + 1
        OD
      CATCH SKIP END
      \<lbrace> \<acute>G = G \<and> \<acute>R = has_unique_edges_inv1 \<acute>G (iedge_cnt \<acute>G) \<rbrace>
   "

procedures is_proper_graph (G :: IGraph | R :: bool)
  "\<acute>R :== CALL has_unique_edges(\<acute>G)"

lemma has_unique_edges_inv1_step:
  "has_unique_edges_inv1 G (Suc i) \<longleftrightarrow> has_unique_edges_inv1 G i
    \<and> (\<forall>j < iedge_cnt G. i \<noteq> j \<longrightarrow> iedges G i \<noteq> iedges G j)"
by (auto simp: has_unique_edges_inv1_def less_Suc_eq)

lemma has_unique_edges_inv2_step:
  "has_unique_edges_inv2 G i (Suc j) \<longleftrightarrow> has_unique_edges_inv2 G i j
    \<and> (i \<noteq> j \<longrightarrow> iedges G i \<noteq> iedges G j)"
by (auto simp: has_unique_edges_inv2_def less_Suc_eq)

lemma (in has_unique_edges_impl) has_unique_edges_spec:
  "\<Gamma> \<turnstile> \<lbrace> \<acute>G = G \<rbrace> \<acute>R :== PROC has_unique_edges(\<acute>G) \<lbrace> \<acute>R = has_unique_edges_inv1 G (iedge_cnt G) \<rbrace>"
  apply vcg
  apply (simp_all add: has_unique_edges_inv1_step has_unique_edges_inv2_step)
  apply (auto simp add: has_unique_edges_inv1_def has_unique_edges_inv2_def prod_eq_iff)
  done

lemma (in has_unique_edges_impl)
  "\<Gamma> \<turnstile> \<lbrace> \<acute>G = G \<rbrace> \<acute>R :== CALL has_unique_edges(\<acute>G)
       \<lbrace> \<acute>R \<longleftrightarrow> has_unique_edges_inv1 G (iedge_cnt G) \<rbrace>"
  apply vcg_step
  apply vcg_step
  oops

end