Re: [isabelle] [Isabelle2014-RC0] lift_definition no longer works in context with assumptions



See now 179b9c43fe84.

On 07/07/2014 03:22 PM, Andreas Lochbihler wrote:
While porting my theories to Isabelle2014-RC4, I got stuck on some
lift_definition commands. In Isabelle2013-2, it was possible to issue a
lift_definition command inside an unnamed context with assumptions
(below is a minimal artificial example). In Isabelle2014-RC0, I do not
get lift_definition to work, because it always raises the following error.

exception THM 0 raised (line 112 of "conjunction.ML"):
   dest_conjunction
   0 < ?n ⟹
   (Scratch.bar ?n = Abs_pos ?n &&& Rep_pos (Scratch.bar ?n) = ?n) &&&
   TERM TYPE(nat) &&& TERM TYPE(pos)

As the example shows, I need the assumption in lift_definition's proof
obligation. How am I supposed to do this in Isabelle2014?

Best,
Andreas


theory Scratch imports "~~/src/HOL/Main" begin

typedef pos = "{n :: nat. n > 0}" by auto
setup_lifting (no_code) type_definition_pos

context
   fixes n :: nat
   assumes "n > 0"
begin

lift_definition bar :: "pos" is "n" by fact






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