Isabelle/HOL Support Wiki

This page contains usage examples for attributes (or directives).

Consider rule/theorem mp:

$\quad [|\ ?P \longrightarrow ?Q; ?P\ |] \Longrightarrow ?Q$.

Using

  
  mp [of _ "C ∨ D"]
  

yields the more specific theorem

$\quad [|\ ?P \longrightarrow C \vee D; ?P\ |] \Longrightarrow C \vee D$.

Note that $C, D$ are no longer schematic variables but specific terms.

Consider rule/theorem mp:

$\quad [|\ ?P \longrightarrow ?Q; ?P\ |] \Longrightarrow ?Q$.

Using

  
  mp [where Q="C ∨ D"]
  

yields the more specific theorem

$\quad [|\ ?P \longrightarrow C \vee D; ?P\ |] \Longrightarrow C \vee D$.

Note that $C, D$ are no longer schematic variables but specific terms.

Consider rule subst:

$\quad [|\ ?s = ?t; ?P ?s\ |]\quad \Longrightarrow\quad ?P ?t$

Note that you can use this rule only to substitute from left to right, not the reverse. Using OF together with theorem sym ($?s = ?t\ \Longrightarrow\ ?t = ?s$), i.e.

  subst [OF sym]

yields

$\quad [|\ ?t = ?s; ?P ?s\ |]\quad \Longrightarrow\quad ?P ?t$

which allows substitutions from right to left.