Stream: Beginner Questions

Topic: Using "OF" regardless of the order

Yiming Xu (Nov 05 2024 at 09:09):

Sometimes I would encounter such a situation. I have an assumption looks like:

 n + 1 ≤ n + 1 ⟹
  Z (n + 1) w w' ⟹
  rel M ?m (w # ?ul) ⟹
  ∃ul'. rel M' ?m (w' # ul') ∧
        (∀u u'. (u, u') ∈ set (zip ?ul ul') ⟶ Z n u u')

The first assumption is very easy to kill, and I may have in the local context only rel w ul but not Z (n+1) w w' yet, and I would like turn it into:

n + 1 ≤ n + 1 ⟹
Z (n + 1) w w' ⟹
  ∃ul'. rel M' ?m (w' # ul') ∧
        (∀u u'. (u, u') ∈ set (zip ul ul') ⟶ Z n u u')

i.e. to skip the first two assumptions and call OF on the third assumption. Would that be possible?

Balazs Toth (Nov 05 2024 at 09:12):

You can do some_lemma[OF _ _ some_other_lemma]

Yiming Xu (Nov 05 2024 at 09:33):

Aha that works! Thanks!

Jonathan Julian Huerta y Munive (Nov 05 2024 at 11:37):

You can also use rotated e.g. thm Relation.single_valuedpD Relation.single_valuedpD[rotated -1, OF ] Relation.single_valuedpD[rotated 1, OF ]

Yiming Xu (Nov 05 2024 at 11:50):

Thanks! I just tried to see how it works! This is particularly good when there is only one assumption blocking the rest, in which case we can rotate it to the very end.

Yiming Xu (Nov 05 2024 at 11:52):

It would be helpful if all these things like "rotated" "unfolded" "rule_format" "THEN iffD1"... i.e. functions, are documented somewhere.

Kevin Kappelmann (Nov 05 2024 at 12:07):

Yiming Xu said:

It would be helpful if all these things like "rotated" "unfolded" "rule_format" "THEN iffD1"... i.e. functions, are documented somewhere.

they are documented here https://isabelle.in.tum.de/doc/isar-ref.pdf

Yiming Xu (Nov 05 2024 at 12:11):

Thanks! I see. The terminology of all these things is called "attribute".

Last updated: Dec 21 2024 at 16:20 UTC