Stream: Beginner Questions

Topic: Forward reasoning with equalities

Christian Zimmerer (Jun 01 2023 at 13:24):

I know that if we have two theorems 1: a ==> b and 2: b ==> c, they can be unified to a ==> c like this: 2[OF 1]. But is this also possible for equalities? E.g. if we have a = b and b ==> c, how can a ==> c be concluded by "forward reasoning" (or whatever the corresponding methodology is called)?

Zixuan Fan (Jun 01 2023 at 13:56):

I think you can try

unfolding \<open>a = b\<close>

or

apply (subst \<open>a = b\<close>)

Christian Zimmerer (Jun 01 2023 at 14:18):

Thank you for your response. I don't want to apply a substitution tactic, I want to directly insert the equality, e.g. for display in a thm command.

Mathias Fleury (Jun 02 2023 at 05:37):

Don't. Sorry, but Pure is not meant to do this kind of things. It is easier to write a new theorem for it.

But if need be:

context
  fixes a b c
  assumes A: "b = a" and B: "b ⟹ c"
begin
thm back_subst[of "λb. b ⟶ c", OF B[unfolded atomize_imp] A,
    unfolded atomize_imp[symmetric]]
(*a ⟹ c*)

Robin Cogan (Jun 02 2023 at 15:31):

Sorry, I've only just started learning Isabelle, so this is probably a dumb question, but what is wrong with:

context
  fixes a b c
  assumes A: "a = b" and B: "b ⟹ c"
begin
thm B[OF iffD1[OF A]]

Mathias Fleury (Jun 04 2023 at 08:44):

That works too

Mathias Fleury (Jun 04 2023 at 08:44):

But your approach would not work if instead b ⟹ c you would have P(b) ⟹ c.

Christian Zimmerer (Jun 15 2023 at 17:30):

Thank you, that was very instructive!

Last updated: Dec 21 2024 at 16:20 UTC