Re: [isabelle] "done" fails to terminate



On Mon, 17 Dec 2012, John Wickerson wrote:

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

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

The 'done' is not a problem -- any other way to finish that proof puts the function package in a bad situation, e.g. 'sorry' at its start.

Technically, you are feeding a certain auxiliary result back into the definitional package, but it cannot cope with it. Someone who understands the function package better needs to take a closer look.


	Makarius


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