Proving Skip: "(SKIP,s)⇒ s" terminates in Isabelle

Question

How can I show that "(SKIP,s)⇒ s", which is a rule of the Big Step Semantics, terminates in Isabelle?

Big Step Semantics is defined as follows "(SKIP,s)⇒ s" is one command.

  inductive big_step :: "com × state ⇒ state ⇒ bool" where
 Skip: "(SKIP,s) ⇒ s" |
 Assign: "(x ::= a,s) ⇒ s(x := aval a s)" |
 Seq: "⟦ (c⇩1,s⇩1) ⇒ s⇩2;  (c⇩2,s⇩2) ⇒ s⇩3 ⟧ ⟹ (c⇩1;;c⇩2, s⇩1) ⇒ s⇩3" |
 IfTrue: "⟦ bval b s;  (c⇩1,s) ⇒ t ⟧ ⟹ (IF b THEN c⇩1 ELSE c⇩2, s) ⇒ t" |
 IfFalse: "⟦ ¬bval b s;  (c⇩2,s) ⇒ t ⟧ ⟹ (IF b THEN c⇩1 ELSE c⇩2, s) ⇒ t" |

I used the formal definition for total correctness

 ⊫ {P} c {Q} ≡ ∀s. P s ⟶ (∃ t. (c, s) ⇒ t ∧ Q t)

so that my Lemma now has the following form:

 lemma "skip: {P} skip {Q} ≡ ∀s. P s ⟶ (∃ t. (skip, s) ⇒ t ∧ Q t)"

Is that definition of the Lemma correct to show that it terminates?