Email Gateway (Aug 19 2022 at 09:30): Email Gateway (Aug 19 2022 at 09:30):From: John Wickerson <jpw48@cam.ac.uk>
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
Email Gateway (Aug 19 2022 at 09:30):From: John Wickerson <jpw48@cam.ac.uk>
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
Email Gateway (Aug 19 2022 at 09:31):From: John Wickerson <jpw48@cam.ac.uk>
oops, sorry, please ignore my last email. it's still broken actually.
Email Gateway (Aug 19 2022 at 09:32):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 26 2024 at 04:17 UTC