My aim is to get a function constant f from a fact of the form ∀ x . ∃ y . P x y so that ∀ x . P x (f x). Here is how I do it manually:
theory Choose
imports
Main
begin
lemma
fixes P :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ bool"
shows True
proof -
(* Somehow obtained this fact *)
have I: "∀ n m :: nat . ∃ i j k . P n m i j k"
by sorry
(* Have to do the rest by hand *)
define F
where "F ≡ λ n m . SOME (i, j, k) . P n m i j k"
define i
where "i ≡ λ n m . fst (F n m)"
define j
where "j ≡ λ n m . fst (snd (F n m))"
define k
where "k ≡ λ n m . snd (snd (F n m))"
have "∀ n m . P n m (i n m) (j n m) (k n m)"
(* prove manually (luckily sledgehammer finds a proof)*)
(*...*)
qed
(* or alternatively: *)
lemma
fixes P :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ bool"
shows True
proof -
(* Somehow obtained this fact *)
have I: "∀ n m :: nat . ∃ i j k . P n m i j k"
by sorry
obtain i j k where "∀ n m . P n m (i n m) (j n m) (k n m)"
(* sledgehammer gives up (due to problem being too higher order?) *)
(* prove by hand :-( *)
(*...*)
qed
How to do this more ergonomically? Does Isabelle have something like Leans choose tactic (https://leanprover-community.github.io/mathlib_docs/tactics.html#choose) ? (Isabelles specification command only works on the top level :-( ).
(Sorry if this has been asked already, I didn't really find a good buzzword to search for this issue)
I don't think there is anything that automates this use case. You can avoid fiddling around with SOME by using the choice rule directly; it allows you to turn an ‘∀∃’ into a ‘∃∀’. However, you still have to convert P from a curried property with 5 arguments into a tupled one with two arguments first, and then unwrap the result again. I don't see a way around this. This is how I would have done it:
let ?P' = "λ(n,m). λ(i,j,k). P n m i j k"
have I: "∀n m. ∃i j k. P n m i j k"
sorry
hence "∀nm. ∃ijk. ?P' nm ijk"
by blast
hence "∃f. ∀nm. ?P' nm (f nm)"
by (rule choice) (* "by metis" also works *)
then obtain f where f: "?P' (n, m) (f (n, m))" for n m
by auto
define i where "i = (λn m. case f (n, m) of (i, j, k) ⇒ i)"
define j where "j = (λn m. case f (n, m) of (i, j, k) ⇒ j)"
define k where "k = (λn m. case f (n, m) of (i, j, k) ⇒ k)"
have ijk: "P n m (i n m) (j n m) (k n m)" for n m
using f[of n m] by (auto simp: i_def j_def k_def split: prod.splits)
In principle, I am sure this could be automated. I don't think there is any reason why the specification command should only work on the top level and not in local contexts or even Isar proofs, other than that it is old and nobody ever bothered to do it. That said, it would of course mean quite a bit of implementation effort and I for one have encountered situations like this relatively rarely and the boilerplate for applying choice by hand as above is not that bad.
But it would certainly be nice to have automation for this!