tools-only Isabelle/HOL Lemma Discovery
Comprehensive guide for discovering and using lemmas in Isabelle/HOL.
Automatic Lemma Discovery
Sledgehammer
Sledgehammer is Isabelle's most powerful automatic proof tool that searches for relevant lemmas.
Basic usage:
lemma "P"
by sledgehammer
With timeout:
lemma "P"
by (sledgehammer [timeout = 60])
Selecting provers:
lemma "P"
by (sledgehammer [provers = e spass z3])
Example:
lemma "length (xs @ ys) = length xs + length ys"
by sledgehammer
(* Sledgehammer finds: by (simp add: length_append) *)
Try and Try0
Quick proof search tactics.
try: Attempts various proof methods
lemma "sorted []"
by try
try0: Faster version, tries only basic tactics
lemma "x + 0 = x"
by try0
Finding Existing Lemmas
Find Theorems
Search for lemmas by pattern or name.
By pattern:
find_theorems "length (_ @ _)"
(* Finds: length_append, length_append_singleton, etc. *)
By name:
find_theorems name: "append"
(* Finds all lemmas with "append" in name *)
With constraints:
find_theorems "length ?xs = ?n" "?xs @ ?ys"
(* Finds lemmas matching both patterns *)
Excluding patterns:
find_theorems "_ + _" -"_ * _"
(* Finds addition lemmas, excluding multiplication *)
Print Theorems
List all available theorems.
print_theorems
(* Lists all theorems in current context *)
Common Lemma Patterns
List Lemmas
Append properties:
lemma append_Nil: "xs @ [] = xs"
lemma append_Nil2: "[] @ xs = xs"
lemma append_assoc: "(xs @ ys) @ zs = xs @ (ys @ zs)"
lemma length_append: "length (xs @ ys) = length xs + length ys"
Map properties:
lemma map_append: "map f (xs @ ys) = map f xs @ map f ys"
lemma map_map: "map f (map g xs) = map (f ∘ g) xs"
lemma map_ident: "map id xs = xs"
lemma length_map: "length (map f xs) = length xs"
Filter properties:
lemma filter_append: "filter P (xs @ ys) = filter P xs @ filter P ys"
lemma filter_filter: "filter P (filter Q xs) = filter (λx. P x ∧ Q x) xs"
lemma length_filter_le: "length (filter P xs) ≤ length xs"
Reverse properties:
lemma rev_append: "rev (xs @ ys) = rev ys @ rev xs"
lemma rev_rev_ident: "rev (rev xs) = xs"
lemma length_rev: "length (rev xs) = length xs"
Arithmetic Lemmas
Addition:
lemma add_0: "0 + n = n"
lemma add_0_right: "n + 0 = n"
lemma add_commute: "m + n = n + m"
lemma add_assoc: "(m + n) + p = m + (n + p)"
lemma add_left_cancel: "k + m = k + n ⟹ m = n"
Multiplication:
lemma mult_0: "0 * n = 0"
lemma mult_1: "1 * n = n"
lemma mult_commute: "m * n = n * m"
lemma mult_assoc: "(m * n) * p = m * (n * p)"
lemma mult_distrib: "(m + n) * p = m * p + n * p"
Ordering:
lemma le_refl: "n ≤ n"
lemma le_trans: "⟦ i ≤ j; j ≤ k ⟧ ⟹ i ≤ k"
lemma le_antisym: "⟦ m ≤ n; n ≤ m ⟧ ⟹ m = n"
lemma add_le_mono: "⟦ i ≤ j; k ≤ l ⟧ ⟹ i + k ≤ j + l"
Set Lemmas
Basic operations:
lemma Un_empty: "A ∪ {} = A"
lemma Un_commute: "A ∪ B = B ∪ A"
lemma Un_assoc: "(A ∪ B) ∪ C = A ∪ (B ∪ C)"
lemma Int_empty: "A ∩ = {}"
lemma Int_commute: "A ∩ B = B ∩ A"
Membership:
lemma mem_Un: "x ∈ A ∪ B ⟷ x ∈ A ∨ x ∈ B"
lemma mem_Int: "x ∈ A ∩ B ⟷ x ∈ A ∧ x ∈ B"
lemma mem_Diff: "x ∈ A - B ⟷ x ∈ A ∧ x ∉ B"
Induction Lemmas
Strengthening Induction Hypotheses
Problem: Induction hypothesis too weak.
Pattern: Generalize the statement.
Example:
(* Too specific *)
lemma "sum_upto n = n * (n + 1) div 2"
(* Fails: need to generalize *)
(* Generalized with accumulator *)
lemma sum_upto_acc: "sum_upto_acc n acc = acc + n * (n + 1) div 2"
proof (induction n arbitrary: acc)
case 0
then show ?case by simp
next
case (Suc n)
then show ?case by simp
qed
Mutual Induction
Pattern: Prove multiple properties simultaneously.
Example:
lemma even_odd:
"even n ⟷ ¬ odd n"
"odd n ⟷ ¬ even n"
proof (induction n)
case 0
then show "even 0 ⟷ ¬ odd 0" by simp
then show "odd 0 ⟷ ¬ even 0" by simp
next
case (Suc n)
then show "even (Suc n) ⟷ ¬ odd (Suc n)" by simp
then show "odd (Suc n) ⟷ ¬ even (Suc n)" by simp
qed
Rule Induction
Pattern: Induction on inductively defined predicates.
Example:
inductive even :: "nat ⇒ bool" where
even_0: "even 0" |
even_SS: "even n ⟹ even (Suc (Suc n))"
lemma even_double: "even n ⟹ ∃k. n = 2 * k"
proof (induction rule: even.induct)
case even_0
then show ?case by (rule exI[of _ 0]) simp
next
case (even_SS n)
then obtain k where "n = 2 * k" by blast
then show ?case by (rule exI[of _ "Suc k"]) simp
qed
Simplification Lemmas
Adding to Simpset
Declare as simp rule:
declare my_lemma [simp]
Conditional simp rule:
lemma my_cond_simp [simp]: "P ⟹ f x = g x"
Remove from simpset:
declare my_lemma [simp del]
Rewrite Lemmas
Pattern: Equations for simplification.
Example:
lemma comp_apply [simp]: "(f ∘ g) x = f (g x)"
by (simp add: comp_def)
lemma id_apply [simp]: "id x = x"
by (simp add: id_def)
lemma const_apply [simp]: "const c x = c"
by (simp add: const_def)
Case Analysis Lemmas
Split Rules
Pattern: Case split for conditional expressions.
Example:
lemma if_split: "P (if c then x else y) = ((c ⟶ P x) ∧ (¬c ⟶ P y))"
by auto
lemma case_split: "P (case xs of [] ⇒ a | _ ⇒ b) =
((xs = [] ⟶ P a) ∧ (xs ≠ [] ⟶ P b))"
by (cases xs) auto
Exhaustiveness Lemmas
Pattern: Cover all cases of a datatype.
Example:
lemma list_cases: "xs = [] ∨ (∃y ys. xs = y # ys)"
by (cases xs) auto
lemma nat_cases: "n = 0 ∨ (∃m. n = Suc m)"
by (cases n) auto
Proof Automation
Auto and Simp
auto: Applies classical reasoning and simplification
lemma "P ∧ Q ⟹ Q ∧ P"
by auto
simp: Applies simplification rules
lemma "xs @ [] = xs"
by simp
simp with additional rules:
lemma "..."
by (simp add: my_lemma1 my_lemma2)
Blast and Force
blast: Fast classical reasoner
lemma "⟦ P ⟶ Q; Q ⟶ R; P ⟧ ⟹ R"
by blast
force: Combines auto and blast
lemma "..."
by force
Clarify and Safe
clarify: Performs safe steps without splitting
lemma "..."
by clarify
safe: Performs all safe steps
lemma "..."
by safe
Specialized Lemmas
Monotonicity Lemmas
Pattern: Preserve ordering.
Example:
lemma map_mono: "⟦ ∀x ∈ set xs. f x ≤ g x ⟧ ⟹
map f xs ≤ map g xs"
by (induction xs) auto
lemma filter_mono: "⟦ ∀x. P x ⟶ Q x ⟧ ⟹
set (filter P xs) ⊆ set (filter Q xs)"
by auto
Injectivity Lemmas
Pattern: Function is injective.
Example:
lemma Suc_inject: "Suc m = Suc n ⟹ m = n"
by simp
lemma Cons_inject: "x # xs = y # ys ⟹ x = y ∧ xs = ys"
by simp
Distinctness Lemmas
Pattern: Constructors are distinct.
Example:
lemma Nil_not_Cons: "[] ≠ x # xs"
by simp
lemma Zero_not_Suc: "0 ≠ Suc n"
by simp
Lemma Discovery Workflow
Step 1: Try Automatic Tools
lemma "goal"
by sledgehammer
(* or *)
by try
(* or *)
by auto
Step 2: Search for Relevant Lemmas
find_theorems "pattern"
Step 3: Manual Proof with Lemmas
lemma "goal"
proof -
have "intermediate" by (simp add: lemma1)
then show ?thesis by (simp add: lemma2)
qed
Step 4: Identify Missing Lemmas
If proof fails, identify what's missing and propose new lemma.
Example: Complete Discovery
Goal:
lemma "length (filter P (map f xs)) ≤ length xs"
Attempt 1:
proof (induction xs)
case Nil
then show ?case by simp
next
case (Cons x xs)
(* Stuck: need lemma about length of filter *)
then show ?case sorry
qed
Search for lemmas:
find_theorems "length (filter _ _)"
(* Finds: length_filter_le *)
Attempt 2:
proof (induction xs)
case Nil
then show ?case by simp
next
case (Cons x xs)
(* Still stuck: need lemma about filter and map *)
then show ?case sorry
qed
Propose new lemma:
lemma filter_map: "filter P (map f xs) = map f (filter (P ∘ f) xs)"
proof (induction xs)
case Nil
then show ?case by simp
next
case (Cons x xs)
then show ?case by (auto simp: comp_def)
qed
Final proof:
lemma "length (filter P (map f xs)) ≤ length xs"
proof -
have "length (filter P (map f xs)) = length (map f (filter (P ∘ f) xs))"
by (simp add: filter_map)
also have "... = length (filter (P ∘ f) xs)"
by (simp add: length_map)
also have "... ≤ length xs"
by (rule length_filter_le)
finally show ?thesis .
qed