[isabelle] BNFs and sort constraints



Dear BNF developers,

I'm looking for some information about the way the BNF package treats
sort constraints. This is going to be a footnote in a paper, maybe a bit
more.

Consider this typedef:

typedef (overloaded) 'a::plus id = "UNIV :: 'a set" by auto

(Please ignore for a moment that the sort constraint is entirely
unnecessary here.)

Observation #1:

"copy_bnf 'a id" fails with tactic errors and a THM exception. Should
this produce a better error message?

Observation #2:

"copy_bnf (dead 'a :: plus) id" gives a better error message, namely "No
live variables".

At this point I'm assuming that "copy_bnf" can't deal with sort constraints.

So let's try with raw "bnf".

Observation #3:

Some setup:

lift_definition map_id :: "('a::plus ⇒ 'b::plus) ⇒ 'a id ⇒ 'b id" is "λf
x. f x" .
lift_definition set_id :: "'a::plus id ⇒ 'a set" is "λx. {x}" .

bnf "'a::plus id"
bnf "'a id"

Both produce identical proof obligations. First subgoal after applying
"rule ext":

 1. ⋀x. map_id id x = id x

"x" does not have any sort constraints. So it is not provable (?).

Observation #4:

I can define

datatype ('a::plus) id = Id 'a

just fine, but "map_id" does not have any sort constraints (whereas "Id"
and "case_id" have them).

Could somebody shed some light onto how this works? I looked at some of
the papers but didn't find anything.

Cheers
Lars




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