Proving existence in Isabelle/HOL in this example

Question

I'm trying to learn how to use Isabelle/Isar with HOL, and I decided a good way to do that would be to develop some elementary number theory. I defined my own plus and times operations so that proof methods wouldn't be doing all the work for me as there's already plenty proved about +, * in Main. My versions are defined as:

fun p:: "nat ⇒ nat ⇒ nat" (infix "⊕" 80) where
  p_0: "0 ⊕ n =n" |
  p_rec: " (Suc m) ⊕ n = Suc (m ⊕ n)"

fun t:: "nat ⇒ nat ⇒ nat" (infix "⊗" 90) where
  t_0: "0 ⊗ n= 0" |
  t_rec: "Suc m ⊗ n = n + m ⊗ n"

and I've already shown that multiplication and addition are commutative the distributive law holds. Then I tried to show the following:

lemma euclidean_division_existence: "∃q r. n=q⊗m⊕r"
proof (induction n)
  case 0
  have "0= 0 ⊗ m" by auto
  hence "∃q. 0 =q ⊗ m" by auto

but it's telling me it can't finish the proof of the last step. I've tried various things, but I can't figure out how to tell Isabelle I just gave it a witness for the existence statement I'm trying to prove. How can I make Isabelle recognize that?

Edit:

xanonec helped me get past this step, but I immediately got stuck on the next step by a seemingly similar problem. Ultimately I want to show:

"∃ q r. 0 = q ⊗ m⊕r"

but I can't figure out how to simultaneously introduce the two existentially quantified variable from

"0 = 0 ⊗ m ⊕ 0"

user9716869 user9716869 · Accepted Answer · 2019-09-28T21:31:50

A suitable strategy for the solution could be a direct rule application (in jEdit you can cntrl+LMB or cmd+LMB on exI to navigate to its statement):

lemma euclidean_division_existence: "∃q r. n=q⊗m⊕r"
proof(induction n)
  case 0
  have "0 = 0 ⊗ m" by auto
  hence "∃q. 0 = q ⊗ m" by (rule exI)    
qed

More generally, in many similar cases sledgehammer can find a suitable (but, often, suboptimal) proof. A tutorial on the use of sledgehammer is a part of the official documentation of Isabelle. Also, I would like to suggest the following resources: "Concrete Semantics with Isabelle/HOL" by Tobias Nipkow and Gerwin Klein and "A Proof Assistant for Higher-Order Logic" by Tobias Nipkow et al.

An update following an amendment made to the statement of the question

The following listing presents a proof that relies only on the most basic methods and direct rule application:

lemma euclidean_division_existence: "∃q r. n=q⊗m⊕r"
proof (induction n)
  case 0 show ?case
  proof-
    have "0 = 0 ⊗ m ⊕ 0" by simp
    then have "∃r. 0 = 0 ⊗ m ⊕ r" by (rule exI)
    then show "∃q r. 0 = q ⊗ m ⊕ r" by (rule exI) 
  qed
  case (Suc n) show ?case sorry
qed

However, if you can afford to rely more on proof automation, then you can use metis to prove the entire theorem:

lemma euclidean_division_existence: "∃q r. n=q⊗m⊕r" by (metis p_0 t_0)

Proving existence in Isabelle/HOL in this example

1 Answers