# [isabelle] VCG of Simpl throws exception

```Hi,

```
I'm trying to verify some simple program using the Simpl theory from the AFP (2011-1 ), but I stumbled on some (probably technical) problem:
```
I have a procedure for which I proved the following specification:

lemma (in has_unique_edges_impl) has_unique_edges_spec:
"Γ ⊢ ⦃ ´G = G ⦄
´R :== PROC has_unique_edges(´G)
⦃ ´R = has_unique_edges_inv1 G (iedge_cnt G) ⦄"

Now, I try to prove some properties about a call to this procedure:

lemma (in has_unique_edges_impl)
"Γ ⊢ ⦃ ´G = G ⦄ ´R :== CALL has_unique_edges(´G)
⦃ ´R = has_unique_edges_inv1 G (iedge_cnt G) ⦄"
apply vcg

This fails with:

```
exception TERM raised (line 3260 of "/home/noschinl/P/afp/thys/Simpl/hoare.ML"):
```FunSplitState.fold_state_prop
x

```
Instead I tried single-stepping, which generates a number of flex-flex pairs:
```
apply vcg_step

goal (1 subgoal):
1. ⦃´G = G⦄
⊆ ⦃´G = ?G21 () ∧
(∀t. ⇗t⇖R = has_unique_edges_inv1 (?G19 ()) (iedge_cnt (?G18 ())) ⟶
⇗t⇖R = has_unique_edges_inv1 G (iedge_cnt G))⦄
flex-flex pairs:
?G21 () =?= ?G20 ()
?G20 () =?= ?G9 ()
?G19 () =?= ?G17 ()
?G18 () =?= ?G16 ()
?G17 () =?= ?G8 ()
?G16 () =?= ?G7 ()
?G9 () =?= ?G7 ()
?G8 () =?= ?G7 ()

```
And the next vcg_step produces the error above. So, is this an error in the VCG or has my spec some unexpected format?
```
-- Lars

 Occurs also with Isabelle 42298c5d33b1 and AFP db765d7a8922
```
```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 (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
```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.