Stream: General

Topic: Meta-forall order

view this post on Zulip Mathias Fleury (Oct 02 2023 at 05:04):

Hi all,

I (or more precisely @Hanna Lachnitt ) is automatically generating theorems like the one below:

lemma H:
  fixes t s :: int
  shows "(s ≤ t) = ((0::int) ≤ t - s)"
  by auto

Is there any way to make sure that the order given by the fixes is respected? (I also tried ⋀, with the same result)

thm H[of t] (*how should t instantiate t here?*)

As we do ML instantiation I would prefer avoiding the H[where t=t] version.

view this post on Zulip Wenda Li (Oct 02 2023 at 13:27):

In the document, there is an attribute named params, for which I suspect could be useful. However, I have neither used it myself nor have I observed its usage within the standard library or AFP... I believe some Isabelle/ML hacks could solve the task, though I am not sure how to do it off the top of my head.

view this post on Zulip Mathias Fleury (Oct 02 2023 at 13:32):

which document do you mean?

view this post on Zulip Mathias Fleury (Oct 02 2023 at 13:41):

https://isabelle.in.tum.de/library/Doc/Isar_Ref/Proof.html?

Last updated: May 02 2024 at 01:06 UTC