CODEWITHSUNDEEP
isabelle
pandaman
pandaman

Reputation: 215

How to let Isabelle "compute" THE output of an inductive predicate

I have an inductive predicate P that behaves like a partial function. In other words, P x y = P x y' ⟹ y = y'. I'd like to let Isabelle "compute" THE output of the predicate when proving theorems on a concrete value (for an example).

For example, let's say that we have the following predicate div2.

inductive div2 :: "nat ⇒ nat ⇒ bool" where
  Zero: "div2 0 0" |
  SS: "div2 n m ⟹ div2 (Suc (Suc n)) (Suc m)"
code_pred[show_modes] div2 .

How can I prove the following lemma without providing the output m (the term is too big to type in the actual case)?

lemma "(THE m. div2 8 m) ≠ 5"
  sorry

Upvotes: 0

Views: 266

Answers (1)

Mathias Fleury
Mathias Fleury

Reputation: 2261

Properties on the and some work nearly always the same way (and sledgehammer does not work well on them).

  1. Prove existence of a witness ;
  2. For the only: prove uniqueness of the witness ;
  3. Deduce with theI or someI that the property holds on the value ;
  4. 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.

Upvotes: 1

Related Questions