Stream: Beginner Questions

Topic: Arguments become invalid when transferred into new documents

Chris_Y (Jul 10 2023 at 11:01):

Hi everyone, I encountered the issue that when I try to combine lemmas from separate documents together, some arguments which have been true suddenly become invalid. For example, I wrote:

define r1 where "r1 = 2*(1-2/m) - sqrt (4*(1-2/m)^2 + 8*(N - r)/m)"
define r2 where "r2 = 2*(1-2/m) + sqrt (4*(1-2/m)^2 + 8*(N - r)/m)"
have "r1 * r2 = (2*(1-2/m))^2 - (sqrt (4*(1-2/m)^2 + 8*(N - r)/m))^2" unfolding r1_def r2_def by algebra

This argument is completely valid when it's in the document that contains only this lemma, but when I copied it to the main document (which combines several lemmas), Isabelle says:

Failed to finish proof⌂:
goal (1 subgoal):
 1. (2 * (1 - 2 / m) - sqrt (4 * (1 - 2 / m)⇧2 + 8 * (N - r) / m)) *
    (2 * (1 - 2 / m) + sqrt (4 * (1 - 2 / m)⇧2 + 8 * (N - r) / m)) =
    (2 * (1 - 2 / m))⇧2 - (sqrt (4 * (1 - 2 / m)⇧2 + 8 * (N - r) / m))⇧2

I've double-checked that the imports are all the same and no previous variables are named r1 or r2. Does anyone know how to fix this? Thank you!

Miri (Jul 13 2023 at 15:30):

Hi I am not sure if this is the right place to ask this question,
I have a Definition of a Relation and I want to show that a tuple is part of this relation. The definition I have is :

definition R :: "int rel" where
"R = {(a,b). ∃n::int. a = b + n}"

I got to this point, but I don't know which rule to use:

then have "∃n::int. x = x + n" by auto
show "(x, x) ∈ R"

:)

Mathias Fleury (Jul 13 2023 at 15:34):

You need to use the definition

Mathias Fleury (Jul 13 2023 at 15:34):

this can be done with

apply (unfold R_def)

Mathias Fleury (Jul 13 2023 at 15:35):

(I assume that this is some kind of homework and I am not sure what kind of Isar constructs you are allowed to use)

Miri (Jul 13 2023 at 15:42):

how could i do that without apply?

Mathias Fleury (Jul 13 2023 at 15:49):

in more steps ;-)

Mathias Fleury (Jul 13 2023 at 15:50):

then have "(x, x) ∈ {(a,b). ∃n::int. a = b + n}"
    sorry
then "(x, x) ∈ R" by (unfold R_def)

Miri (Jul 13 2023 at 15:58):

thank you that helped ^-^

Jan van Brügge (Jul 13 2023 at 16:47):

Other than that you could also use the unfolding keyword, as in have ... unfolding R_def by ...

Last updated: Apr 28 2024 at 04:17 UTC