2
$\begingroup$

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?

$\endgroup$

1 Answer 1

2
$\begingroup$

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)
$\endgroup$
1
  • $\begingroup$ Paradoxically, the last one also counts as an Isar proof, although I quite dislike the name of the invoked rule. $\endgroup$ Commented Jul 29, 2023 at 12:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.