Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Referencing chained facts after "unfolding"

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: Apr 29 2024 at 04:18 UTC