Stream: Beginner Questions

Topic: Functions that applies to theorems

Yiming Xu (Dec 11 2024 at 14:42):

I remember there are some functions that manipulates on theorems, say, give an iff thm, it turns A \equiv B into A ==>B or B ==>A. And there is also a function, maybe called conjunction1 conjunction2 or something like that, that takes a A /\ B into A and B.

I like them, but forgot their names, are they documented somewhere?

Mathias Fleury (Dec 11 2024 at 14:43):

iffD1 and iffD2

Mathias Fleury (Dec 11 2024 at 14:44):

find_theorems "?A = ?B ⟹ ?A ⟹ ?B"

Yiming Xu (Dec 11 2024 at 15:25):

Mathias Fleury said:

iffD1 and iffD2

Thanks! Is iffD1[OF sth] the only thing to do here? I saw somewhere it is possible to write sth[... a function] to take one direction of the sth.

Yiming Xu (Dec 11 2024 at 15:30):

Oh I found it in my old files.
sth[unfolded sth_def, THEN conjunct2,THEN conjunct2,THEN conjunct2,
THEN conjunct2]

Yiming Xu (Dec 11 2024 at 15:30):

And I can also do [THEN iffD1].

Manuel Eberl (Dec 19 2024 at 19:19):

Note that these things like OF, of, THEN, symmetric etc. are called attributes. In this form they typically transform one or more theorems in some way.

Yiming Xu (Dec 19 2024 at 20:23):

Manuel Eberl said:

Note that these things like OF, of, THEN, symmetric etc. are called attributes. In this form they typically transform one or more theorems in some way.

Thank you for the terminology! I asked an expert to look up these things, and the conclusion is that this is documented in
https://isabelle.in.tum.de/dist/Isabelle2024/doc/isar-ref.pdf
on page 323. There are very little of them and is not such flexible. I am then taught that unlike in HOL4, Isabelle intends to let the user write things out, and the community does not appreciate that style. (That is a bit sad for me, but I will live with it.)

Maximilian Vollath (Dec 20 2024 at 12:11):

Btw, is there a way to use, e.g. THEN, to split a rule into multiple conclusions?

lemma conj3: assumes "A ∧ B ∧ C" shows "A" "B" "C" sorry
lemma a: "(0::nat) < 3 ∧ (0::nat) < 6 ∧ (0::nat) < 9" sorry
thm a[THEN conj3] (* Error: Expected singleton fact "conj3" (length 3) *)

Kevin Kappelmann (Dec 20 2024 at 12:59):

How about conj3[OF a]?

Maximilian Vollath (Dec 20 2024 at 13:07):

Oops :laughter_tears: Yep that's exactly what I wanted

Yiming Xu (Dec 20 2024 at 19:13):

Nice! That is helpful as well!

Last updated: Dec 30 2024 at 16:22 UTC