Written by Luka Kerr on November 30, 2020

Introduction

Theorem Provers

A theorem prover is the implementation of a formal logic on a computer. It can be:

• fully automated (propositional logic)
• automated, but not necessarily terminating (first order logic)
• with automation, but mainly interactive (higher order logic)

It also:

• is based on rules and axioms
• can deliver proofs

Theorem proving allows us to analyse systems and programs thoroughly, find design and specification errors early and give assurance that programs are correct.

This course will use Isabelle – a generic interactive proof assistant. This means it is:

• generic: not specialised to one particular logic
• interactive: more than just yes/no, you can interactively guide the system
• a proof assistant: helps to explore, find, and maintain proofs

Although, just because you prove something on a computer, does not make it necessarily correct. This is because:

• hardware could be faulty
• operating system could be faulty
• implementation runtime system could be faulty
• compiler could be faulty
• …

Meta Logic

The meta logic is a logic used to formalize another logic. Isabelle has a meta logic, specifically:

• $\bigwedge \ \equiv \ \forall$, the universal quantifier
• $\Longrightarrow \ \equiv \ \longrightarrow$, implication

$\lambda$-Calculus

The $\lambda$-calculus was created by Alonzo Church. It was originally meant as foundation of mathematics, is important applications in theoretical computer science and is the foundation of computability and functional programming.

Untyped $\lambda$-Calculus

The untyped $\lambda$-calculus is a turing complete model of computation that provides a simple way of writing down functions.

For example, instead of writing f(x) = x + 5, we write $f = \lambda x. \ x + 5$ which is a term and a nameless function that adds 5 to its parameter.

Function Application

To apply arguments to functions, we write $f \ a$, for example $(\lambda x. \ x + 5) \ a$. To evaluate this term, we replace $x$ by $a$.

Formal Specification

Formally, the untyped lambda calculus can be defined as:

Conventions

• Leave out parentheses where possible
• List variables instead of multiple $\lambda$

Rules

• Application binds to the left: $x \ y \ z = (x \ y) \ z \ne x \ (y \ z)$
• Abstraction binds to the right: $\lambda x. \ x \ y = \lambda x. \ (x \ y) \ne (\lambda x. \ x) \ y$

$\beta$-reduction

The process of $\beta$-reduction is simply to continuously replace the parameter by argument until you reach a point where you cannot anymore, known as the normal form.

$\beta$-conversion is defined as $s =_\beta t$ iff $\exists n. s \longrightarrow_\beta^\ast n \land t \longrightarrow_\beta^\ast n$, where $\longrightarrow_\beta^\ast$ is the transitive, reflexive closure of $\longrightarrow_\beta$.

A term $t$ is reducible if there is an $s$ such that $t \longrightarrow_\beta s$.

$\eta$-conversion

• $(\lambda x. \ t \ x) \longrightarrow_\eta t$ if $x \not\in FV(t)$
• $s \longrightarrow_\eta s^\prime \Longrightarrow (s \ t) \longrightarrow_\eta (s^\prime \ t)$
• $t \longrightarrow_\eta t^\prime \Longrightarrow (s \ t) \longrightarrow_\eta (s \ t^\prime)$
• $s \longrightarrow_\eta s^\prime \Longrightarrow (\lambda x. \ s) \longrightarrow_\eta (\lambda x. \ s^\prime)$

$s =_\eta t$ iff $\exists n. s \longrightarrow_\eta^\ast n \land t \longrightarrow_\eta^\ast n$, where $\longrightarrow_\beta^\ast$ is the transitive, reflexive closure of $\longrightarrow_\beta$.

Free Variables

In $(\lambda x. \ t)$, $x$ is a bound variable.

The free variables of a term are:

• $FV \ \{ x \} = \{ x \}$
• $FV \ \{ c \} = \{ \}$
• $FV \ \{ s \ t \} = FV(s) \cup FV(t)$
• $FV \ \{ \lambda x. \ t \} = FV(t) \setminus \{ x \}$

A term $t$ is called closed if $FV(t) = \{ \}$.

Substitution

When substituting, if there are name collisions we simply rename bound variables.

• $x [ x \gets t ] = t$
• $y [ x \gets t ] = y$ if $x \ne y$
• $c [ x \gets t ] = c$
• $(s_1 \ s_2) [ x \gets t ] = (s_1 [x \gets t] \ s_2 [x \gets t])$
• $(\lambda x. \ s) [x \gets t] = (\lambda x. \ s)$
• $(\lambda x. \ s) [x \gets t] = (\lambda x. \ s[x \gets t])$ if $x \ne y$ and $y \not\in FV(t)$
• $(\lambda x. \ s) [x \gets t] = (\lambda x. \ s[y \gets z][x \gets t])$ if $x \ne y$ and $z \not\in FV(t) \cup FV(s)$

$\alpha$-conversion

$s =_\alpha t$ means $s = t$ up to renaming of bound variables.

Formally:

• $(\lambda x. \ t) \longrightarrow_\alpha (\lambda y. \ t[x \gets y])$ if $y \not\in FV(t)$
• $s \longrightarrow_\alpha s^\prime \Longrightarrow (s \ t) \longrightarrow_\alpha (s^\prime \ t)$
• $t \longrightarrow_\alpha t^\prime \Longrightarrow (s \ t) \longrightarrow_\alpha (s \ t^\prime)$
• $s \longrightarrow_\alpha s^\prime \Longrightarrow (\lambda x. \ s) \longrightarrow_\alpha (\lambda x. \ s^\prime)$

Also, $s =_\alpha t$ iff $s \longrightarrow_\alpha^\ast t$, where $\longrightarrow_\alpha^\ast$ is the transitive, reflexive closure of $\longrightarrow_\alpha$.

Typed $\lambda$-Calculus

Terms:

Types:

Context $\Gamma$: a function from variable and constant names to types.

A term $t$ has a type $\tau$ in context $\Gamma$: $\Gamma \vdash t :: \tau$. Such a term is well typed if there are $\Gamma$ and $\tau$ such that $\Gamma \vdash t :: \tau$ holds.

Type Checking Rules

Variables

$\dfrac{}{\Gamma \vdash x :: \Gamma(x)}$

Application

$\dfrac{\Gamma \vdash t_1 :: \tau_2 \Rightarrow \tau \quad \Gamma \vdash t_2 :: \tau_2}{\Gamma \vdash (t_1 \ t_2) :: \tau}$

Abstraction

$\dfrac{\Gamma[x \gets \tau_x] \vdash t :: \tau}{\Gamma \vdash (\lambda x. \ t) :: \tau_x \Rightarrow \tau}$

Most General Types

Each type correct term has a most general type. We have

Subject Reduction

Well typed terms stay well typed during $\beta$-reduction:

Natural Deduction

Rules

Safe & Unsafe Rules

Safe rules preserve provability: conjI, impI, notI, iffI, refl, ccontr, classical, conjE, disjE, allI, exE.

Unsafe rules can turn a provable goal into an unprovable one: disjI1, disjI2, impE, iffD1, iffD2, notE, allE, exI.

Safe rules should always be applied before unsafe ones.

Higher Order Logic

• Quantification over everything, including predicates
• Consistency by types
• Formula = term of type bool
• Definition built on $\lambda^\to$ with certain default types and constants

Default Types:

• $\texttt{bool}$
• $\_ \Rightarrow \_$
• $\texttt{ind}$

Default Constants:

• $\longrightarrow :: \texttt{bool} \Rightarrow \texttt{bool} \Rightarrow \texttt{bool}$
• $= :: \alpha \Rightarrow \alpha \Rightarrow \texttt{bool}$
• $\epsilon :: (\alpha \Rightarrow \texttt{bool}) \Rightarrow \alpha$

Definitions:

• $\texttt{True} \equiv (\lambda x :: \texttt{bool}. \ x) = (\lambda x. \ x)$
• $\texttt{All} \ P \equiv P = (\lambda x . \ \texttt{True})$
• $\texttt{Ex} \ P \equiv \forall Q. (\forall x. \ P \ x \longrightarrow Q) \longrightarrow Q$
• $\texttt{False} \equiv \forall P . \ P$
• $\neg P \equiv P \longrightarrow \texttt{False}$
• $P \land Q \equiv \forall R. \ (P \longrightarrow Q \longrightarrow R) \longrightarrow R$
• $P \lor Q \equiv \forall R. \ (P \longrightarrow R) \longrightarrow (Q \longrightarrow R) \longrightarrow R$
• $\texttt{If} \ P \ x \ y \equiv \texttt{SOME} \ z. \ (P = \texttt{True} \longrightarrow z = x) \land (P = \texttt{False} \longrightarrow z = y)$
• $\texttt{inj} \ f \equiv \forall x \ y. \ f \ x = f \ y \longrightarrow x = y$
• $\texttt{surj} \ f \equiv \forall y. \ \exists x. \ y = f \ x$

Axioms:

Isar

A typical Isar proof looks like:

proof
  assume formula0
  have formula1 by simp
  ...
  have formulan by blast
  show formula(n + 1) by ...
qed

which proves formula0 implies formula(n + 1).

proof

• proof <method> <statement>* qed
• proof <method>: applies method to the stated goal
• proof applies a single rule that fits
• proof - does nothing to the goal

Modes

• [prove]
  • goal has been stated, proof needs to follow
• [state]
  • proof block has opened or subgoal has been proved, new from statement, goal statement or assumptions can follow
• [chain]
  • from statement has been made, goal statement needs to follow

Backward & Forward

• Backward reasoning: have A /\ B proof
  • proof picks an intro rule automatically
  • conclusion of rule must unify with A /\ B
• Forward reasoning: assume AB: "A /\ B"; from AB have "..." proof
  • now proof picks an elimination rule automatically
  • trigger by from
  • first assumption of rule must unify with AB

General case: from A1 ... An have R proof

• first n assumptions of rule must unify with A1 ... An
• conclusion of rule must unify with R

Fix & Obtain

• fix v1 ... vn
  • introduces new arbitrary but fixed variables
• obtain v1 ... vn where <prop> <proof
  • introduces new variables together with property

Abbreviations

• this: the previous fact proved or assumed
• then: from this
• thus: then show
• hence: then have
• with A1 ... An: from A1 ... An this
• ?thesis: the last enclosing goal statement

Moreover & Ultimately

• moreover have Pn instead of have Xn: Pn

Term Rewriting

Given a set of equations $l_1 = r_1$, $l_2 = r_2$, …, $l_n = r_n$, does equation $l = r$ hold?

The idea of term rewriting is to use equations as reduction rules, i.e. $l_1 \longrightarrow r_1$, $l_2 \longrightarrow r_2$, …, $l_n \longrightarrow r_n$ to help decide whether $l = r$ by deciding $l \overset{\ast}{\longleftrightarrow} r$.

Arrow Definitions

• $\overset{0}{\longrightarrow} \ = \{ (x, \ y) \mid x = y \}$: identity
• $\overset{n + 1}{\longrightarrow} \ = \ \overset{n}{\longrightarrow} \circ \longrightarrow$: $n + 1$ fold composition
• $\overset{+}{\longrightarrow} \ = \bigcup_{i > 0} \overset{i}{\longrightarrow}$: transitive closure
• $\overset{\ast}{\longrightarrow} \ = \ \overset{+}{\longrightarrow} \cup \overset{0}{\longrightarrow}$: reflexive transitive closure
• $\overset{=}{\longrightarrow} \ = \ \longrightarrow \cup \overset{0}{\longrightarrow}$: reflexive closure
• $\overset{-1}{\longrightarrow} \ = \{ (y, \ x) \mid x \longrightarrow y \}$: inverse
• $\longleftarrow \ = \ \overset{-1}{\longrightarrow}$: inverse
• $\longleftrightarrow \ = \ \longleftarrow \cup \longrightarrow$: symmetric closure

• $\overset{+}{\longleftrightarrow} \ = \bigcup_{i > 0} \overset{i}{\longleftrightarrow}$: symmetric closure

• $\overset{\ast}{\longrightarrow} \ = \ \overset{+}{\longleftrightarrow} \cup \overset{0}{\longleftrightarrow}$: reflexive transitive symmetric closure

Deciding $l \overset{\ast}{\longleftrightarrow} r$

To decide whether $l \overset{\ast}{\longleftrightarrow} r$ holds, we look for an $n$ such that $l \overset{\ast}{\longrightarrow} n$ and $r \overset{\ast}{\longrightarrow} n$.

Although, there may not be a suitable $n$. This decision only works for systems where the Church-Rosser property holds:

Confluence

If terms in a system can be rewritten in more than one way to yield the same result, then the system is confluent.

Termination

• $\longrightarrow$ is terminating if there are no infinite reduction chains
• $\longrightarrow$ is normalising if each element has a normal form
• $\longrightarrow$ is convergent if it is both terminating and confluent

When each rule application makes terms simpler in some way, then $\longrightarrow$ is terminating. More formally, $\longrightarrow$ is terminating when there is a well founded order $<$ on terms for which $s < t$ whenever $t \longrightarrow s$. An order is well founded if there is no infinite decreasing chains $a_1 > a_2 > \dots$.

In practice, it is often easier to consider just the rewrite rules by themselves, rather than their application to an arbitrary term $t$. To do this, we show for each rule $l_i = r_i$, that $r_i < l_i$. This requires a term $u$ to become smaller whenever any subterm of $u$ is made smaller. Formally, this means that $<$ is required to be monotonic with respect to the structure of terms: $s < t \longrightarrow u[s] < u[t]$. This is true for most orders that don’t treat certain parts of terms as special cases.

Term Rewriting In Isabelle

The term rewriting engine in Isabelle is called the simplifier. To use it, we write apply simp. The simplifier uses simplification rules and applies them from left to right until no rule is applicable. Both termination and confluence is not guaranteed.

Equations can be turned into simplication rules by adding the [simp] attribute, or they can be added/deleted locally using apply (simp add: <rules>) or apply (simp del: <rules>). Certain rules can be applied alone using apply (simp only: <rules>).

Applying A Rewrite Rule

A rule $l \longrightarrow r$ is applicable to a term $t[s]$ if there is a substitution $\sigma$ such that $\sigma \ l = s$. The resulting term is $t[\sigma \ r]$, and we have $t[s] = t[\sigma \ r]$.

Conditional Term Rewriting

Rewrite rules can be conditional, where $\llbracket P_1, \dots, P_n \rrbracket \implies l = r$ is applicable to a term $t[s]$ with $\sigma$ if $\sigma \ l = s$ and $\sigma \ P_1, \dots, \sigma \ P_n$ are provable by rewriting.

Rewriting With Assumptions

Isabelle uses assumptions in rewriting, this can lead to non-termination. There are options we can pass to simp to disable this:

• (simp (no_asm)): use and simplify assumptions
• (simp (no_asm_use)): ignore assumptions
• (simp (no_asm_simp)): use, but do not simplify assumptions

Orthogonal Rewriting Systems

• A rule $l \longrightarrow r$ is left-linear if no variable occurs twice in $l$
• A rewrite system is left-linear if all rules are

A system is orthogonal if it is left-linear and has no critical pairs. Orthogonal rewrite systems are confluent.

Specification Techniques

Sets

Type 'a set sets over type 'a.

• {}, {a, b, c, d}, {x. P x}
• $e \in A$, $A \subseteq B$
• $A \cup B$, $A \cap B$, $A - B$, $-A$
• $\bigcup x \in A. \ B \ x$, $\bigcap x \in A. \ B \ x$, $\bigcap A$, $\bigcup A$
• $\{ i .. j \}$
• insert :: 'a => 'a set => 'a set
• … and so on

Introducing Theorems

• Definitions
  • definition x where "..." introduces a new lemma called x_def
• Proofs
  • lemma "..."

Introducing Types

• typedecl: by name only
  • typedecl names introduces a new type names without any further assumptions
• type synonym: by abbreviation
  • type_synonym 'a rel = "'a => 'a => bool" introduces abbreviation rel for existing type
• typedef: by definition as a set
  • typedef new_type = "{ some set }" <proof> introduces a new type as a subset of an existing type
  • the proof shows that the set on the right hand side is non-empty

Inductive Definitions

The rules

define a set $X \subseteq A$.

Given a set of rules $R \subseteq A \ \text{set} \times A$, we can apply $R$ to a set $B$: $\hat{R} \ B \equiv \{ x . \ \exists H. \ (H, x) \in R \land H \subseteq B \}$.

The set $B$ is $R$-closed iff $\hat{R} \ B \subseteq B$, and $X$ is the least $R$-closed subset of A.

Rule Induction

Datatypes

Datatypes must be definable as a set, and can’t have nested recursion.

Every datatype introduces a case construct, where in general there is one case per constructor. The syntax apply (case_tac t) creates $k$ subgoals, one for each constructor.

Recursion

In HOL, all functions must be total. Primitive recursion functions in Isabelle guarantee termination structurally. A primitive recursive function can be introduced with primrec.

Induction

Structural Induction

$P \ xs$ holds for all lists $xs$ if

• $P \ Nil$
• and for arbitrary $x$ and $xs$, $P \ xs \implies P \ (x \sharp xs)$

A general proof method for induction is (induct x), where x must be a free variable in the first subgoal, and the type of x must be a datatype.

Theorems about recursive functions are proved by induction.

fun

Defining a recursive function using fun allows for high expressiveness, but a termination proof may fail. In genera, fun is

• more permissive than primrec
• generates more theorems than primrec
• may fail to prove termination

Each fun definition induces an induction principle. For each equation, show $P$ holds for the left hand side, provided $P$ holds for each recursive call on the right hand size.

Isabelle tries to prove termination automatically, which works in most cases but may fail. In this case, termination can be proved seperately.

Automation

Sledgehammer

• Connects Isabelle with ATPs and SMT solvers: E, SPASS, Vampire, CVC3, Yices, Z3
• Simple to invocate
  • users don’t need to select or know facts
  • or ensure the problem is first-order
  • or know anything about the automated prover
• Exploits local parallelism and remote servers

Reconstruction

We don’t want to trust the external provers. Need to check/reconstruct proof.

• Re-find using Metis: usually fast and reliable (sometimes too slow)
• Rerun external prover for trusted replay: used for SMT, re-runs prover each time
• Recheck stored explicit external representation of proof: used for SMT, no need to re-run, fragile
• Recast into structured Isar proof: fast, not always readable

Disproof

Testing cannot prove theorems, but it can refute conjectures. Usage with quickcheck

Quickcheck

Lightweight validation by testing.

• Motivated by Haskell’s QuickCheck
• Uses Isabelle’s code generator
• Fast
• Runs in background, proves you wrong as you type

Covers a number of testing approaches:

• Random and exhausing testing
• Smart test data generators
• Narrowing-based (symbolic) testing

Nitpick

Finite model finder based on SAT. Soundly approximates infinite types. Usage with nitpick.

Hoare Logic

The idea of Hoare Logic is to describe the meaning of program by pre/post conditions. Together, a program with these pre and post conditions is known as a Hoare Triple:

To prove properties about programs, we have rules that directly work on such triples.

Partial correctness: $\models \{ P \} \ C \ \{ Q \} \equiv \forall \sigma \ \sigma^\prime. \ P \ \sigma \land \langle c, \sigma \rangle \to \sigma^\prime \longrightarrow Q \ \sigma^\prime$.

Total correctness: $\models \{ P \} \ C \ \{ Q \} \equiv (\forall \sigma \ \sigma^\prime. \ P \ \sigma \land \langle c, \sigma \rangle \to \sigma^\prime \longrightarrow Q \ \sigma^\prime) \land (\forall \sigma. \ P \ \sigma \longrightarrow \exists \sigma^\prime. \ \langle c, \sigma \rangle \to \sigma^\prime)$

Soundness: $\vdash \{ P \} \ C \ \{ Q \} \implies \models \{ P \} \ C \ \{ Q \}$.

Soundness can be proved by rule induction on $\vdash \{ P \} \ C \ \{ Q \}$.

Invariants

For programs with loops, we need to find a correct invariant $P$, with which we annotate the program with so that Hoare rules can be applied automatically.

Weakest Preconditions

Verification Conditions

The triple $\{ \mathbf{pre} \ C \ Q \} \ C \ \{ Q \}$ is only true under certain conditions, called verification conditions $vc \ C \ Q$. We also have $vc \ C \ Q \land (P \implies \mathbf{pre} \ C \ Q) \implies \{ P \} \ C \ \{ Q \}$.

Proofs About Programs

Deep Embeddings

A deep embedding is a seperate representation of language terms and their semantics.

This allows for proof of general theorems about the language, not just of programs, usually by structural induction over the syntax type.

A disadvantage is that semantically equivalent programs are not obviously equal, and many concepts already present in the logic must be reinvented.

Shallow Embeddings

A shallow embedding represents only the semantics, directly in the logic. It includes a definition for each language construct, giving its semantics. Programs are represented as instances of these definitions.

A shallow embedding is suitable for (a useful fragment of) C.

State Monad

The state monad can express lots of C ideas:

• Access to volatile variables, external APIs: Nondeterminism
• Undefined behaviour: Failure
• Early exit (return, break, continue): Exceptional control flow

A tool called AutoCorres produces a verified translation from deeply embedded C to a monadic representation specifically designed for humans to do proofs over.

The state monad models the semantics of a deterministic computation as a function: $s \Rightarrow (\alpha \times s)$. The computation operates over a state of type $s$ which includes all global variables, external devices etc. The computation also yields a return value of type $\alpha$ which models exit statuses, return values etc.

A function return is provided that represents the computation that leaves the state unchanged and returns its argument: $\texttt{return} \ x \equiv \lambda s. \ (x, s)$.

Basic Operations

• get ($\texttt{get} \equiv \lambda s. \ (s, s)$): returns the entire state without modifying it
• put ($\texttt{put} \equiv \lambda _. \ ((), s)$): replaces the state and returns the unit value $()$
• bind ($\texttt{c »= d} \equiv \lambda s. \ \mathbf{let} \ (r, s^\prime) = c \ s \ \mathbf{in} \ d \ r \ s^\prime$): sequences two computations; 2nd takes the first’s result
• gets ($\texttt{gets f} \equiv \texttt{get »=} \ (\lambda s. \ \texttt{return} \ (f s))$): returns a projection of the state; leaves state unchanged
• modify ($\texttt{modify f} \equiv \texttt{get »=} \ (\lambda s. \ \texttt{put} \ (f s))$): applies its argument to modify the state; returns $()$

Laws

Formally, a monad $M$ is a type constructor with two operations: $\texttt{return} :: \alpha \Rightarrow M \ \alpha$ and $\texttt{bind} :: M \ \alpha \Rightarrow (\alpha \Rightarrow M \ \beta) \Rightarrow M \ \beta$.

Also, a >>= b is infix notation for bind a b, and a >>= (\x. b x) is often written as do { x <- a; b x }.

The laws are:

• return-left: (return x >>= f) = f x
• return-right: (m >>= return) = m
• bind-assoc: ((a >>= b) >>= c) = (a >>= (\x. b x >>= c))

State Monad With Failure

$s \Rightarrow ((\alpha \times s) \times \texttt{bool})$

Nondeterministic State Monad With Failure

$s \Rightarrow ((\alpha \times s) \ \texttt{set} \times \texttt{bool})$

Where computations return a set of possible results.

C Verification

wp

The syntax apply (wp <extra-wp-rules>) is a tactic for automatic application of weakest precondition rules. When used with AutoCorres, it allows for automated reasoning about C programs.

AutoCorres

AutoCorres reduces the pain in reasoning about C code. It is self-certifying, in that it produces Isabelle theorems proving its own correctness.

Word Abstraction

Word abstraction converts a C integer into an Isabelle integer, and a C unsigned into an Isabelle natural number. Guards are inserted to ensure absence of unsigned underflow and overflow.

Isabelle

General Schema

lemma name: "<goal>"
  apply <method>
  apply <method>
  ...
  done

Sequential application of methods until all subgoals are solved.

Theories

theory MyTh
import ImpThy1 ... ImpThyn
begin
...
end

• MyTh is name of theory, and must live in MyTh.thy
• ImpThyi is the name of imported theories
• Usually, theory MyTh imports Main begin ... end will suffice

Rules

• apply assumption: proves $\llbracket B_1; \dots; B_m \rrbracket \implies C$ by unifying $C$ with one of $B_i$

Intro Rules

Decompose formulae to the right of $\implies$.

• apply (rule <intro-rule>)
• Applying rule $\llbracket A_1; \dots; A_n \rrbracket \implies A$ to subgoal $C$:
  • unifies $A$ and $C$
  • replaces $C$ with $n$ new subgoals $A_1, \dots A_n$

Elimination Rules

Decompose formulae on the left of $\implies$.

• apply (erule <elim-rule>)
• Applying rule $\llbracket A_1; \dots; A_n \rrbracket \implies A$ means if $A_1$ is known and $A$ wants to be proven, it suffices to show $A_2, \dots A_n$
• Applying rule $\llbracket A_1; \dots; A_n \rrbracket \implies A$ to subgoal $C$:
  • Like rule but also unifies first premise of rule with an assumption and eliminates that assumption

Cases

• apply (case_tac <term>): case distinctions on arbitrary terms

Instantiating Rules

• apply (rule_tac x=<term> in <rule>) or apply (erule_tac x=<term> in <rule>).
• Like rule, but ?x in <rule> is instantiated by <term> before application.

Renaming Parameters

• (rename tac x1 ... xn): renames the rightmost (inner) n parameters to x1 ... xn

Forward Proofs

• apply (frule <rule>): used when the first premise of theorem matches a premise of the current goal
• apply (drule <rule>): like frule except it deletes the matching premise

Automation

• apply (intro <intro-rules>): repeatedly applies intro rules
• apply (intro <elim-rules>): repeatedly applies elimination rules
• apply safe: applies all safe rules
• apply clarify: applies all safe rules that do not split the goal
• apply blast: an automatic tableaux prover that works on first-order logic
• apply auto: applies automated tools to look for solution
• apply fast: another automatic search tactic
• apply force: like auto, but only for the first goal
• apply fastforce: a combination of fast and force
• apply simp: simplifies current goal using term rewriting
• apply (simp add <theorems>): like the simplifier, but tells the simplifier to use additional theorems as well
• apply clarsimp: a combination of clarify and simp
• apply arith: automatically solves linear arithmetic problems