Email Gateway (Dec 06 2023 at 11:47): Email Gateway (Dec 06 2023 at 11:47):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Hi all,
I want to report a limitation of Isabelle that translates into a limitation of Sledgehammer, namely, there appears to be no way to reference chained facts via "using" once they have been unfolded via "unfolding". Example:
theory Scratch
imports Main
begin
axiomatization zero :: nat and p :: "nat ⇒ bool"
lemma z: "zero = 0"
sorry
lemma pz: "p zero"
sorry
lemma "p 0"
using pz unfolding z
using ‹p zero› ‹p 0›
Isabelle reports an error for ‹p 0›, even though the fact appears in the displayed proof state:
proof (prove)
using this:
p 0
goal (1 subgoal):
1. p 0
Is there any hope to be able to refer to such facts?
Best,
Jasmin
Last updated: Jan 04 2025 at 20:18 UTC