✔ Why is this not working? · Beginner Questions

Stream: Beginner Questions

Topic: ✔ Why is this not working?

Yoav Cohen (Jul 15 2026 at 14:32):

Yoav Cohen (Jul 15 2026 at 14:40):

curiously, it works if I use auto instead of .. (or more explicitly conjI) which is very weird

Kevin Kappelmann (Jul 15 2026 at 14:41):

B, C is not the same as B /\ C, and conjI is exactly the theorem allowing you to prove the latter from the former.

Yoav Cohen (Jul 15 2026 at 14:42):

I am trying to prove B /\ C from B, C using conjI and it is not working as you can see in the screenshot. Maybe this is a bug.

Kevin Kappelmann (Jul 15 2026 at 14:46):

You're passing C, B not B, C:

notepad
begin
  assume "A" "B"
  from ‹A› ‹B› have "A ∧ B" .. (*OK*)
  from ‹B› ‹A› have "A ∧ B" .. (*not OK*)
end

Yoav Cohen (Jul 15 2026 at 14:48):

I guess there is no rule overloading in isabelle, but is there really no conjI2 or something for these cases?

Kevin Kappelmann (Jul 15 2026 at 14:50):

You can prove that lemma if you like it.
In practice, people don't write such proofs because automation takes care of such irrelevances (so nobody misses the rule).
I don't know what you mean by rule overloading.

Yoav Cohen (Jul 15 2026 at 14:51):

rule overloading is where you cite the same rule and it functions as different rules depending on certain other factors. for example, one might cite iffD and it will choose iffD1 or iffD2 based on context (or something)

Notification Bot (Jul 15 2026 at 14:53):

Yoav Cohen has marked this topic as resolved.

Kevin Kappelmann (Jul 15 2026 at 14:54):

You can make a theorem collection iffD which contains iffD1 and iffD2: lemmas iffD = iffD1 iffD2.

Yoav Cohen (Jul 15 2026 at 14:54):

And then I can cite it as a rule?

Kevin Kappelmann (Jul 15 2026 at 14:55):

if by rule you mean an argument passed to the rule method, then yes.

Yoav Cohen (Jul 15 2026 at 14:55):

I am not sure what that means, I was just thinking like "by"

Yoav Cohen (Jul 15 2026 at 14:55):

oh you mean like (rule something)?

Kevin Kappelmann (Jul 15 2026 at 14:55):

like this:

lemma conj_swapI: "A ⟹ B ⟹ B ∧ A" by auto
lemmas conj_intros = conjI conj_swapI

notepad
begin
  assume "A" "B"
  from ‹A› ‹B› have "A ∧ B" by (rule conj_intros) (*OK*)
  from ‹B› ‹A› have "A ∧ B" by (rule conj_intros) (*OK*)
end