Re: [isabelle] Isabelle2014-RC0: lift_definition ignores no_code

With Isabelle2014-RC1 approaching, I would like to revive this questions
as I am also, so to speak, a »stake holder« of the theories where this
problem occurs.

a) is this a deliberate change? (There is however no entry containing
»lift« in the NEWS).
b) if not, what shall we do about it?  Someone must put on the helmet
and dig into to investigate,


On 07.07.2014 16:37, Andreas Lochbihler wrote:
> In Isabelle2014-RC0, lift_definition sometimes forgets that the
> setup_lifting declaration has been given the (no_code) option. When that
> happens, I get bogus code equations in the code generator setup which
> break the value command, because even NBE then complains about sort
> constraints being violated. Below is an example that works in
> Isabelle2013-2, but not in Isabelle2014-RC0. Of course, I can manually
> delete the code equations, but it would be nicer if lift_definition
> could just stick to what setup_lifting has been told.
> theory Scratch imports "~~/src/HOL/Main" begin
> typedef ('a, 'b) foo = "{f :: 'a ⇒ 'b. ∀x. f x = undefined}" sorry
> setup_lifting (no_code) type_definition_foo
> lift_definition make :: "('a ⇒ 'b) ⇒ ('a, 'b) foo"
>   is "λg. if ∀x. g x = undefined then g else (λ_. undefined)" sorry
> definition bar where "bar = make (λx :: nat. 0 :: nat)"
> value "bar"
> (* evaluates in Isabelle2013-2 to "make (λu. 0)",
> but raises the following error message in Isabelle2014-RC0:
> Wellsortedness error
> (in code equation bar ≡ make (λx. zero_nat_inst.zero_nat),
> with dependency "Pure.dummy_pattern" -> "bar"):
> Type nat not of sort enum
> No type arity nat :: enum
> *)
> Best,
> Andreas


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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