Chengsong Tan (Feb 05 2024 at 12:43): Chengsong Tan (Feb 05 2024 at 12:43):Hi,
I was trying to prove a lemma with many conjuncts: P ==> a /\ b /\ c ....
I was wondering if there's a nice way in Isar that allows me to prove each conjunct as a subgoal in a localised way.
I tried to follow
lemma my_lemma: "A ∧ B ⟹ B ∧ A"
proof -
assume "A ∧ B " thus "B" ..
next
assume "A ∧ B" thus "A" ..
qed
from the textbook of Isar (https://courses.grainger.illinois.edu/cs576/sp2015/doc/isar-overview.pdf)
however it doesn't work.
Isabelle says "failed to refine any pending goal" on the thus keyword.
Any ideas how to fix this?
Best wishes,
Chengsong
Mathias Fleury (Feb 05 2024 at 12:47):Remove the "-" after proof.
Mathias Fleury (Feb 05 2024 at 12:48):The hyphen means "do not anything to my goal". Hence the conjuction is not split.
Chengsong Tan (Feb 05 2024 at 14:55):Mathias Fleury said:
The hyphen means "do not anything to my goal". Hence the conjuction is not split.
Thanks Mathias! I am now trying this:
lemma my_lemma: "A ∧ B ∧ C ⟹ B ∧ A ∧ C"
proof
assume "A ∧ B ∧ C " thus "B" by simp
next
assume "A ∧ B ∧ C" thus "A" by simp
qed
However the second thus already gives a "not able to refine any pending goal" error.
Mathias Fleury (Feb 05 2024 at 16:23):the standard rule use by proof is applied only once, splitting only one conjunction, not two
Mathias Fleury (Feb 05 2024 at 16:23):If you look at the state panel you will see exactly what comes out of the default rule
Mathias Fleury (Feb 05 2024 at 16:24):lemma my_lemma: "A ∧ B ∧ C ⟹ B ∧ A ∧ C"
proof (intro conjI)
assume "A ∧ B ∧ C " thus "B" by simp
next
assume "A ∧ B ∧ C" thus "A" by simp
next
assume "A ∧ B ∧ C" thus "C" by simp
qed
Mathias Fleury said:
the standard rule use by proof is applied only once, splitting only one conjunction, not two
Thank you! That makes sense.
Last updated: Apr 28 2024 at 04:17 UTC