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)