Proof Method. `frule` and `drule` [isa-0010]

November 28, 2025
Liam O'Connor

Given a goal $\llbracket X; A_1 \dots A_n \rrbracket \implies G$ and a theorem r $: \llbracket X; P_1 \dots P_n \rrbracket \implies Y$ , apply (frule r) replaces the goal with subgoals:

$\llbracket X; A_1 \dots A_n \rrbracket \implies P_1$
$\dots$
$\llbracket X; A_1 \dots A_n \rrbracket \implies P_n$
$\llbracket X; Y; A_1 \dots A_n \rrbracket \implies G$

The method drule is the same as frule except that it also deletes the assumption $X$ from the last subgoal.