How do I do for-all introduction in Isabelle?

Question

It's pretty easy to prove something like this:

theory Scratch imports Main begin

theorem "foldl (λ x y. x) a b = a"
  apply (induction b)
  by auto

However, rewording the theorem using the universal quantifier makes it not work any more:

theorem "∀ a b. foldl (λ x y. x) a b = a"
  apply (rule allI, rule allI)
  apply (induction b)  (* Unable to figure out induct rule *)
  by auto              (* Failed to apply initial proof method *)

The b in induction b appears to be a separate b to the b in the goal. (This is a guess, from looking at how more complicated examples behave.) When I try to use a simpler example (e.g. ∀ x :: nat. x < x + 1), by simp just solves it automatically – which means I can't see how it's done.

How can I introduce variables in Isabelle?

Answer 1

You have just successfully did $\forall$-introduction after the first apply. But sometimes using rule is too low-level.

After that command, your goal reads ⋀a b. foldl (λx y. x) a b = a, in which meta-quantified variables can be read as for arbitrary a,b. But they are still quantified, so there's no such a (free) variable b on scope. So, when you want to prove something about arbitrary values, you fix some a and b and proceed:

theorem ‹∀ a b. foldl (λ x y. x) a b = a›
proof (clarify)  ― ‹\<^term>‹safe› also works here›
  fix a b
  show ‹foldl (λx y. x) a b = a›
    by (induction b) simp_all
qed

The clarify method does exactly that: clears universal quantifiers, implication antecedents, and the like. safe applies all eponymous rules (i.e., that give you an equivalent goal). And I've changed the comment and quote styles to a more modern one.

---

EDIT. The above is an Isar answer (which is the recommended idiom for writing Isabelle proofs). Without using Isar, you were probably expecting something like:

theorem ‹∀ a b. foldl (λ x y. x) a b = a›
  apply (intro allI)
  apply (rule List.induct_list012)
  by simp_all

where intro repeatedly applies the listed introduction rules. (I found the list induction rule by Ctrl-b completion.) But then you could use the even simpler:

theorem ‹∀ a b. foldl (λ x y. x) a b = a›
  by (auto intro:List.induct_list012)