Email Gateway (Aug 19 2022 at 15:04): Email Gateway (Aug 19 2022 at 15:04):From: Ondřej Kunčar <kuncar@in.tum.de>
See now 179b9c43fe84.
Email Gateway (Aug 19 2022 at 15:13):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Last updated: Apr 24 2024 at 20:16 UTC