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.

why not split foos_conjunction directly?

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.

```
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: Sep 22 2023 at 08:19 UTC