Proving lemma in Isabelle

Question

I have a function

 fun exec :: "com ⇒ state ⇒ nat ⇒ state option" where
   "exec _ s 0 = None" 
 | "exec SKIP s (Suc f) = Some s" 
 | "exec (x::=v) s (Suc f) = Some (s(x:=aval v s))" 
 | "exec (c1;;c2) s (Suc f) = (
     case (exec c1 s f) of None ⇒ None | Some s' ⇒ exec c2 s' f)" 
 | "exec (IF b THEN c1 ELSE c2) s (Suc f) = 
     (if bval b s then exec c1 s f else exec c2 s f)" 
 | "exec (WHILE b DO c) s (Suc f) = (
     if bval b s then 
       (case (exec c s f) of 
         None ⇒ None | 
          Some s' ⇒ exec (WHILE b DO c) s' f) 
     else Some s)"

and I need to prove

lemma exec_imp_bigstep: "exec c s f = Some s' ⟹ (c,s) ⇒ s'"

holds. How can I do that? I tried induction, auto, blast, sledgehammer. But it seems a different approach is needed.

---

The Lemma says that there exist values for c and s, so that there exists a s' that is the result of function f with values c and s. I wonder why you need c and s in the Definition, and why you can not just write

lemma exec_imp_bigstep: "exec c f = Some s' ⟹ c ⇒ s'"

As to the proof, my idea would be to show that

lemma exec_imp_bigstep: "exec c s f = Some s' ⟹ (c,s) ⇒ s'" holds if

lemma exec_imp_bigstep: "exec c f = Some s' ⟹ c ⇒ s'" and lemma exec_imp_bigstep: "exec s f = Some s' ⟹ s ⇒ s'" .