search

isabelle-utp / interaction-trees

Interactions Trees in Isabelle/HOL and a CSP model
6 stars 1 forks source link

Non-exhaustive patterns in function pfun_entries #1

Closed RandallYe closed 2 years ago

RandallYe commented 3 years ago

As discussed in this issue https://github.com/isabelle-utp/Z_Toolkit/issues/2, the problem might be with the definition of the exception operator.

It seems the following part in the definition (pfun_entries (A ∩ pdom(F)) (fun_pfun (λ _. Q)))

(parsed as pfun_entries (A ∩ pdom F) (pfun_app (fun_pfun (λ_. Q))))

causes the issue. To be more specific, there is no code equation for fun_pfun \equiv pfun_entries UNIV.

The part could be simplified to (pfun_entries (A ∩ pdom(F)) (λ _. Q))

I cannot see a particular reason to use (fun_pfun (λ _. Q)) to transform a total function (λ _. Q) to a partial function, then apply pfun_app to transform the partial function back to a total function.

RandallYe commented 2 years ago

I have simplified the definition as discussed in (https://github.com/isabelle-utp/interaction-trees/issues/1#issue-964987943), and merged it into master. So close this issue.