## Stream: Beginner Questions

### Topic: Proving lemma with definite description

#### Lekhani Ray (Jul 28 2022 at 19:59):

Hello!

I am trying to prove a lemma for plus with definite description

lemma (in th8a) th8_a: "∀f. q f ⟶ plus = f"

Isabelle cannot seem to recognize anything after this

Supporting context:

locale th8a = th1 +
assumes
"((∀x . p zero ∧ (∀x. p x ⟶ p (suc x))) ⟶ (∀x. p x))"
begin
definition
plus where plus_def: "plus = (THE f. ∀ x y. f x zero = x ∧ f x (suc y) = suc (f x y))"
definition
times where "times = (THE g. ∀ x y. g x zero = zero ∧ g x (suc y) = plus (g x y) x)"
end

fun (in th8a) q :: "('a ⇒ 'a ⇒ 'a) ⇒ bool"
where
"q f = (∀ x y. (f x zero = x ∧ f x (suc y) = suc (f x y)))"

lemma (in th8a) th8_a_2: "plus = (THE f. q f)"
done

Any pointers on how to move forward with lemma th8_a_2?

#### Mathias Fleury (Jul 29 2022 at 05:03):

You probably need theI

#### Mathias Fleury (Jul 29 2022 at 05:04):

But typically proofs on choice are very painful.

#### Manuel Eberl (Jul 29 2022 at 12:43):

My personal approach is:

1. hide the operator behind a definition (using definition on toplevel or define in an Isar proof)
2. prove unique exists (with the ∃! operator)
3. use the introduction rules for the operator (my favourite ones are theI', the1_equality, and someI_ex) to prove the properties that you expect
4. never unfold the definition of the operator again; just work with the derived properties

That involves a little bit of boilerplate once, but it is fairly pain free.

#### Mathias Fleury (Jul 29 2022 at 12:48):

The boilerplate part is what I called »painful«

#### Manuel Eberl (Jul 29 2022 at 12:52):

There's also the specification command, but it's a bit old-fashioned and only works on the toplevel. One could perhaps write a more modern version of that at some point…

#### Manuel Eberl (Jul 29 2022 at 12:53):

In an Isar proof, you can often also get away just using obtain (possibly combined with an application of the axiom of choice, which e.g. metis does very well automatically) instead of using SOME.

#### Lekhani Ray (Aug 03 2022 at 18:23):

Manuel Eberl said:

My personal approach is:

1. hide the operator behind a definition (using definition on toplevel or define in an Isar proof)
2. prove unique exists (with the ∃! operator)
3. use the introduction rules for the operator (my favourite ones are theI', the1_equality, and someI_ex) to prove the properties that you expect
4. never unfold the definition of the operator again; just work with the derived properties

That involves a little bit of boilerplate once, but it is fairly pain free.

With respect to point 2:
I have started with

lemma (in th8a) th8_a2: "∃! f. q f"
apply(rule theI' the1_equality someI_ex)
apply auto

where th8_a_2 is

lemma (in th8a) th8_a_2: "plus = (THE f. q f)"
done

Questions:

1. Does the order of the applications matter? [eg. If I switch the order of theI', the1_equality etc)
2. With every application of auto, the subgoals keep on increasing. What may be the reason?
3. Is the expression in the lemma the correct expression?

Thank you!

#### Lawrence Paulson (Aug 16 2022 at 09:47):

The rule method attempts the rules in the order given, from left to right. Put the most specific rules at the beginning.

The auto method is designed to do all of its work in one call. With rare exceptions, a second application of auto with the same arguments should fail.

Last updated: Dec 07 2023 at 20:16 UTC