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