Introducing fixed representation for a quotient type in Isabelle

Question

This question is better explained with an example. Suppose I want to prove the following lemma:

lemma int_inv: "(n::int) - (n::int) = (0::int)"

How I'd informally prove this is something along these lines:

Lemma: n - n = 0, for any integer n and 0 = abs_int(0,0).

Proof:
Let abs_int(a,b) = n for some fixed natural numbers a and b.
--- some complex and mind blowing argument here ---
That means it suffices to prove that a+b+0 = a+b+0, which is true by reflexivity.
QED.

However, I'm having trouble with the first step "Let abs_int(a,b) = n". The let statement doesn't seem to be made for this, as it only allows one term on the left side, so I'm lost at how I could introduce the variables a and b in an arbitrary representation for n.

How may I introduce a fixed reprensentation for a quotient type so I may use the variables in it?

---

Note: I know the statement above can be proved by auto, and the problem may be sidestepped by rewriting the lemma as "lemma int_inv: "Abs_integ(a,b) - Abs_integ(a,b) = (0::int)". However, I'm looking specifically for a way to prove by introducing an arbitrary representation in the proof.

Answer 1

You can introduce a concrete representation with the theorem int.abs_induct. However, you almost never want to do that manually.

The general method of proving statements about quotients is to first state an equivalent theorem about the underlying relation, and then use the transfer tool. It would've helped if your example wasn't automatically discharged by automation... in fact, let's create our own little int type so that it isn't:

theory Scratch
  imports Main
begin

quotient_type int = "nat × nat" / "intrel"
  morphisms Rep_Integ Abs_Integ
proof (rule equivpI)
  show "reflp intrel" by (auto simp: reflp_def)
  show "symp intrel" by (auto simp: symp_def)
  show "transp intrel" by (auto simp: transp_def)
qed

lift_definition sub :: "int ⇒ int ⇒ int"
  is "λ(x, y) (u, v). (x + v, y + u)"
  by auto

lift_definition zero :: "int" is "(0, 0)".

Now, we have

lemma int_inv: "sub n n = zero"
  apply transfer

proof (prove)
goal (1 subgoal):
 1. ⋀n. intrel ((case n of (x, y) ⇒ λ(u, v). (x + v, y + u)) n) (0, 0)

So, the version we want to prove is

lemma int_inv': "intrel ((case n of (x, y) ⇒ λ(u, v). (x + v, y + u)) n) (0, 0)"
  by (induct n) simp

Now we can transfer it with

lemma int_inv: "sub n n = zero"
  by transfer (fact int_inv')

Note that the transfer proof method is backtracking — this means that it will try many possible transfers until one of them succeeds. Note however, that this backtracking doesn't apply across separate apply commands. Thus you will always want to write a transfer proof as by transfer something_simple, instead of, say proof transfer.

You can see the many possible versions with

apply transfer
back back back back back

Note also, that if your theorem mentions constants about int which weren't defined with lift_definition, you will need to prove a transfer rule for them separately. There are some examples of that here.

In general, after defining a quotient you will want to "forget" about its underlying construction as soon as possible, proving enough properties by transfer so that the rest can be proven without peeking into your type's construction.