## 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: Feb 27 2024 at 08:17 UTC