Stream: Beginner Questions

Topic: Splitting conjunction


view this post on Zulip cai (Feb 07 2022 at 14:56):

If I have a theorem foos_conjunction "P1 ∧ P2 ∧ .. ∧ Pn" and want to split it into an indexable theorem list, how do I do this? My goal is to write foos(3) for P3 etc. - I can do it in the top-level with this:

ML ‹ML_Thms.bind_thms ("foos", BNF_FP_Util.split_conj_thm @{thm foos_conjunction})›

However, ML‹...› doesn't work in an Isar-proof. Is there another way? I feel like I am overcomplicating things here (I tried playing around with atomize_conj too). Of course, I could write foos_conjunction[THEN conjunct1] for P1 but for accessing Pn it will get messy real quick.

view this post on Zulip Mathias Fleury (Feb 07 2022 at 15:21):

why not split foos_conjunction directly?

view this post on Zulip cai (Feb 07 2022 at 15:41):

Can you elaborate please? Do you mean to repeatedly eliminate with conjE? I have theorems where I want to do thm1[OF P2 P3 P4] or thm2[OF P1 P5] and so on in that Isar proof. So I want to reference them within multiple sub-proofs.

view this post on Zulip Mathias Fleury (Feb 07 2022 at 16:00):

lemma foo_conjunctions:
   "P1" "P2" "P3" ...

view this post on Zulip cai (Feb 07 2022 at 16:09):

Ah, yes but it coming from an entry in AFP that I have no control over. I could copy it and modify accordingly actually.


Last updated: Sep 25 2022 at 23:25 UTC