*To*: isabelle-users Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] "done" fails to terminate*From*: John Wickerson <jpw48 at cam.ac.uk>*Date*: Mon, 17 Dec 2012 09:34:31 +0100*In-reply-to*: <F75A38B7-5312-46B9-A628-BF2360C30FD3@cam.ac.uk>*References*: <2FA7A950-C750-46D6-9F3C-E45D1CFB82EB@cam.ac.uk> <F75A38B7-5312-46B9-A628-BF2360C30FD3@cam.ac.uk>

oops, sorry, please ignore my last email. it's still broken actually. On 17 Dec 2012, at 09:30, John Wickerson wrote: > 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 > >

**References**:**[isabelle] "done" fails to terminate***From:*John Wickerson

**Re: [isabelle] "done" fails to terminate***From:*John Wickerson

- Previous by Date: Re: [isabelle] "done" fails to terminate
- Next by Date: [isabelle] Feature request: definition on crtl+hover
- Previous by Thread: Re: [isabelle] "done" fails to terminate
- Next by Thread: Re: [isabelle] "done" fails to terminate
- Cl-isabelle-users December 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list