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:
definition
on toplevel or define
in an Isar proof)∃!
operator)theI'
, the1_equality
, and someI_ex
) to prove the properties that you expectThat 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 ordefine
in an Isar proof)- prove unique exists (with the
∃!
operator)- use the introduction rules for the operator (my favourite ones are
theI'
,the1_equality
, andsomeI_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:
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: Oct 12 2024 at 20:18 UTC