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.