Properties on the
and some
work nearly always the same way (and sledgehammer does not work well on them).
- Prove existence of a witness ;
- For the only: prove uniqueness of the witness ;
- Deduce with
theI
or someI
that the property holds on the value ;
- Prove the theorem you actually wanted to prove.
In your case that translates to proving that 5 is not a witness:
inductive_cases div2E: ‹div2 m n›
lemma "(THE m. div2 8 m) ≠ 5"
proof -
have ex_div2: ‹div2 8 4› (*1: witness*)
by (auto simp: numeral_eq_Suc div2.intros)
moreover have ‹div2 8 m ⟹ m = 4› for m (*2: uniqueness*)
by (force simp: numeral_eq_Suc elim: div2E)
ultimately have ‹div2 8 (THE x. div2 8 x)› (*3: property holds*)
by (rule theI)
(*4 use the property*)
then show ?thesis
by (force simp: numeral_eq_Suc elim: div2E)
qed
If you don't need the
, use some
instead, that avoids the very annoying uniqueness proof each time.
For your use case, I would advise to write the theorem as div2 8 m ⟹ m ≠ 5
, which is equivalent, but much easier to use and to prove.
lemma "div2 8 m ⟹ m ≠ 5"
by (force simp: numeral_eq_Suc elim: div2E)
For reusability:
- Factor step 3 in a separate lemma (if there is a meaningful way to express when an invert exists)
- Hide as much as possible
the
predicates by introducing definitions and avoid referring to the lambda-definition as much as possible.