Isabelle cheat sheet

Isar proofs

proof -
  from some_fact have "P(x)" by simp
  thus ?thesis .
qed

Name	Parameters	Effect
assumption	—	Solves {$⟦A_1;\cdots;A_m⟧\Longrightarrow A_k$} if {$k\in[1,m]$}
rule	a rule	Goal: {$⟦A_1;\cdots;A_m⟧\Longrightarrow C$}, rule: {$⟦P_1;\cdots P_n⟧\Longrightarrow Q$} Unifies {$C$} and {$Q$} with {$U$}, replaces the goal with: {$⟦U(A_1);\cdots;U(A_m)⟧\Longrightarrow U(P_k)$} for {$k=1,\cdots,n$}
frule	a rule	Goal: {$⟦A_1;\cdots;A_m⟧\Longrightarrow C$}, rule: {$⟦P_1;\cdots P_n⟧\Longrightarrow Q$} Unifies {$P_1$} and {$A_j$} with {$U$} for some {$j$}, replaces the goal with: {$⟦U(A_1);\cdots;U(A_m);U(Q)⟧\Longrightarrow U(C)$} and {$⟦U(A_1);\cdots;U(A_m)⟧\Longrightarrow U(P_k)$} for {$k=2,\cdots,n$}
drule	a rule	Same as frule, but removes {$U(A_j)$} (the {$A_j$} that was unified with {$P_1$})
erule	a rule	rule + drule at the same time (same unifier)