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"
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)