# [isabelle] "done" fails to terminate

```Hi Isabelle,

My theory file (see below) gets stuck at the word "done". On the line preceding "done", the proof state says...

proof (prove): step 2

goal:
No subgoals!

... so it feels like there is nothing left to do. What's going on?

Thanks for any assistance,
John

---

theory scratch imports
Main
begin

definition fst3 :: "'a × 'b × 'c ⇒ 'a"
where "fst3 ≡ fst"

definition snd3 :: "'a × 'b × 'c ⇒ 'b"
where "snd3 ≡ fst ∘ snd"

definition thd3 :: "'a × 'b × 'c ⇒ 'c"
where "thd3 ≡ snd ∘ snd"

typedecl assertion

typedecl command
consts Choose :: "command ⇒ command ⇒ command"
consts Loop :: "command ⇒ command"
consts Skip :: "command"
consts Seq :: "command ⇒ command ⇒ command" (infixr ";;" 55)

typedecl node

datatype assnode =
Rib "assertion"
| Exists_dia "string" "diagram"
and comnode =
Com "command"
| Choose_dia "diagram" "diagram"
| Loop_dia "diagram"
and diagram =
Graph "node list" "node ⇒ assnode" "(node list × comnode × node list) list"
type_synonym labelling = "node ⇒ assnode"
type_synonym edge = "node list × comnode × node list"

fun lins :: "diagram ⇒ ((node + edge) list) set"
where
"lins (Graph V Λ E) = {π .
(distinct π)
∧ (set π = (set V) <+> (set E))
∧ (∀i j v e.
i < length π ∧ j < length π ∧ π!i = Inl v ∧ π!j = Inr e ∧ v ∈ set (fst3 e)
⟶ i<j)
∧ (∀j k w e.
j < length π ∧ k < length π ∧ π!j = Inr e ∧ π!k = Inl w ∧ w ∈ set (thd3 e)
⟶ j<k) }"

function
coms_dia :: "diagram ⇒ command set" and
coms_ass :: "assnode ⇒ command set" and
coms_com :: "comnode ⇒ command set"
where
"coms_ass (Rib p) = {Skip}"
| "coms_ass (Exists_dia x G) = coms_dia G"
| "coms_com (Com c) = {c}"
| "coms_com (Choose_dia G H) = {Choose c d | c d .
c ∈ coms_dia G ∧ d ∈ coms_dia H}"
| "coms_com (Loop_dia G) = { Loop c | c . c ∈ coms_dia G}"
| "coms_dia (Graph V Λ E) = { foldr (op ;;) cs Skip | cs .
∃π ∈ lins (Graph V Λ E) . ∀i<length cs.
(cs!i) ∈ (case (π!i) of
Inl v ⇒ coms_ass (Λ v) |
Inr e ⇒ coms_com (snd3 e)) }"
apply pat_completeness
apply clarify+
done

end

```

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