I have obtains-style lemma (those that look like induction or case analysis lemmas), and I want to compose them:
notepad begin
fix P Q Q1 Q2 R R'
assume lemma1: "⋀ thesis. P ⟹ (Q ⟹ thesis) ⟹ (R ⟹ thesis) ⟹ thesis"
assume lemma2: "⋀ thesis. Q ⟹ (Q1 ⟹ thesis) ⟹ (Q2 ⟹ thesis) ⟹ thesis"
assume lemma3: "⋀ thesis. R ⟹ (R' ⟹ thesis) ⟹ thesis"
thm lemma1[OF _ lemma2 lemma3]
end
This shows
P ⟹
(Q ⟹ Q) ⟹ (Q ⟹ Q1 ⟹ ?thesis) ⟹ (Q ⟹ Q2 ⟹ ?thesis) ⟹
(R ⟹ R) ⟹ (R ⟹ R' ⟹ ?thesis) ⟹
?thesis
but I’d like to get
P ⟹
(Q1 ⟹ ?thesis) ⟹ (Q2 ⟹ ?thesis) ⟹
(R' ⟹ ?thesis) ⟹
?thesis
Is that possible without having to spell out the lemma?