# How do I do for-all introduction in Isabelle?

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?

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)

• Paradoxically, the last one also counts as an Isar proof, although I quite dislike the name of the invoked rule. Commented Jul 29, 2023 at 12:30