How to proceed in Isabelle when the goal has implications and existentials?

Question

I'm trying to write a proof in the Isabelle "structured style" and I'm not sure how to specify the value of existential variables. Specifically, I'm trying to expand the sorrys in this proof:

lemma division_theorem: "lt Zero n ⟹ ∃ q r. lt r n ∧ m = add (mul q n) r"
proof (induct m)
  case Zero
  then show ?case
    by (metis add_zero_right mul.simps(1)) 
next
  case (Suc m)
  then show ?case
  proof (cases "Suc r = n")
    case True
    then show ?thesis sorry
  next
    case False
    then show ?thesis sorry
  qed
qed

Zero, add, and mul are defined on a nat-like class that I made just for the purposes of writing simple number theory proofs, hopefully that is intuitive. I have done this in the "apply" style, so I'm familiar with how the proof is supposed to go, I'm just not understanding how to turn it into "structured" style.

So the goals generated by these cases are:

 1. (lt Zero n ⟹ ∃q r. lt r n ∧ m = add (mul q n) r) ⟹
    lt Zero n ⟹ cnat.Suc r = n ⟹ ∃q r. lt r n ∧ cnat.Suc m = add (mul q n) r
 2. (lt Zero n ⟹ ∃q r. lt r n ∧ m = add (mul q n) r) ⟹
    lt Zero n ⟹ cnat.Suc r ≠ n ⟹ ∃q r. lt r n ∧ cnat.Suc m = add (mul q n) r 

At a high level, for that first goal, I want to grab the q and r from the first existential, specify q' = Suc q and r' = Zero for the second existential, and let sledgehammer bash out precisely what mix of arithmetic lemmas to use to prove that it works. And then do that same for q' = q and r' = Suc r for the second case.

How can I do this? I have tried various mixes of obtain, rule exI, but I feel like I'm not understanding some basic mechanism here. Using the apply style this works when I apply subgoal_tac but it seems like that is unlikely to be the ideal method of solution here.

Answer 1

As you can see in the two goals generated by the command cases "Suc r = n", the occurrences of variable r in both the expressions cnat.Suc r = n and cnat.Suc r ≠ n are actually free and thus not related to the existentially quantified formula whatsoever. In order to "grab" the q and r from the induction hypothesis you need to use the obtain command. As a side remark, I suggest to use the induction method instead of the induct method so you can refer to the induction hypothesis as Suc.IH instead of Suc.hyps. Once you "grab" q and r from the induction hypothesis, you just need to prove that

1. lt r' n, and that
2. Suc m = add (mul q' n) r'

with q' and r' as defined for each of your two cases. Here is a (slightly incomplete) proof of your division theorem:

lemma division_theorem: "lt Zero n ⟹ ∃ q r. lt r n ∧ m = add (mul q n) r"
proof (induction m)
  case Zero
  then show ?case
    by (metis add_zero_right mul.simps(1)) 
next
  case (Suc m)
  (* "Grab" q and r from IH *)
  from ‹lt Zero n› and Suc.IH obtain q and r where "lt r n ∧ m = add (mul q n) r"
    by blast
  show ?case
  proof (cases "Suc r = n")
    case True
    (* In this case, we use q' = Suc q and r' = Zero as witnesses  *)
    from ‹Suc r = n› and ‹lt r n ∧ m = add (mul q n) r› have "Suc m = add (mul (Suc q) n) Zero"
      using add_comm by auto
    with ‹lt Zero n› show ?thesis
      by blast
  next
    case False
    (* In this case, we use q' = q and r' = Suc r as witnesses  *)
    from ‹lt r n ∧ m = add (mul q n) r› have "Suc m = add (mul q n) (Suc r)"
      by simp
    moreover have "lt (Suc r) n"
      sorry (* left as exercise :) *)
    ultimately show ?thesis
      by blast
  qed
qed