Tautology

A tautology in logic is a formula or assertion that is true in every possible interpretation. An example of a tautology is "Either it will rain tomorrow, or it won't." No matter what happens, this statement will always be true.

Identitied

In mathematics, an identity is an equality relation A = B, such that A and B contain some variables and the equality holds for all values of the variables.

For example, in trigonometry, sin^2(x) + cos^2(x) = 1 is an identity because it is true for all values of x.

Isar proof of Language

Isar Proof of Language:

Isar (Intelligible semi-automated reasoning) is a language for structured proof documents that was specifically developed for Isabelle. It provides a human-readable and -understandable way to create formal proofs. A simple example would be a proof that "if A then A" is true:

proof -
  assume A: "A"
  show "A" by (rule A)
qed

The Simplifier

The Simplifier is a powerful tool in Isabelle's arsenal for automated proof. It simplifies goals based on a set of rewrite rules. The rules could be basic arithmetic simplifications like x + 0 = x, or something more complex like distributive laws a * (b + c) = a * b + a * c.

Example : Proof Elimination

Proof by elimination (also called proof by exhaustion) is a method in which you divide the possible cases into several mutually exclusive possibilities and prove each one separately. For example, if we want to prove that every natural number is either even or odd, we can do this using Isabelle/Isar like this:

theorem even_or_odd:
  "even n ∨ odd n"
proof (cases "even n")
  case True
  then show ?thesis by simp
next
  case False
  hence "odd n" by presburger
  then show ?thesis by simp
qed

In this proof, we divided the possibilities into "n is even" and "n is not even" and proved the statement for each case. The Simplifier was used to simplify the resulting expressions.