LRI Équipe MODHEL Bât 650 Ada Lovelace, Université Paris Sud Rue Noetzlin, 91190 Gif-sur-Yvette, France
Isabelle cheat sheet

## Isar proofs

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


## Proof methods

NameParametersEffect
assumptionSolves {$⟦A_1;\cdots;A_m⟧\Longrightarrow A_k$} if {$k\in[1,m]$}
rulea ruleGoal: {$⟦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$}
frulea ruleGoal: {$⟦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$}
drulea ruleSame as frule, but removes {$U(A_j)$} (the {$A_j$} that was unified with {$P_1$})
erulea rulerule + drule at the same time (same unifier)