cai (Feb 07 2022 at 14:56): 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.
Mathias Fleury (Feb 07 2022 at 15:21):why not split foos_conjunction directly?
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.
Mathias Fleury (Feb 07 2022 at 16:00):lemma foo_conjunctions:
"P1" "P2" "P3" ...
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: Apr 19 2024 at 12:27 UTC