Re: [isabelle] "done" fails to terminate



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






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