# Re: [isabelle] "done" fails to terminate

```Hi again,

Just to add: I found that if I expand the final "apply clarify" into the full "fix/assume/show" version, then everything works fine.

john

On 17 Dec 2012, at 08:48, John Wickerson wrote:

> 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.