Hello!

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

```
lemma (in th8a) th8_a: "∀f. q f ⟶ plus = f"
apply(simp add: th8_a_2 plus_def)
```

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)"
apply(simp add: plus_def)
done
```

Any pointers on how to move forward with lemma th8_a_2?

You probably need `theI`

But typically proofs on choice are very painful.

My personal approach is:

- hide the operator behind a definition (using
`definition`

on toplevel or`define`

in an Isar proof) - prove unique exists (with the
`∃!`

operator) - use the introduction rules for the operator (my favourite ones are
`theI'`

,`the1_equality`

, and`someI_ex`

) to prove the properties that you expect - 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.

The boilerplate part is what I called »painful«

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…

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`

.

Manuel Eberl said:

My personal approach is:

- hide the operator behind a definition (using
`definition`

on toplevel or`define`

in an Isar proof)- prove unique exists (with the
`∃!`

operator)- use the introduction rules for the operator (my favourite ones are
`theI'`

,`the1_equality`

, and`someI_ex`

) to prove the properties that you expect- 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.

Thank you both @Manuel Eberl and @Mathias Fleury for your comments.

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(simp add: th8_a_2)
apply auto
```

where th8_a_2 is

```
lemma (in th8a) th8_a_2: "plus = (THE f. q f)"
apply(simp add: plus_def)
done
```

Questions:

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

Thank you!

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