[logicchains]

Here's a specification of an increment function in Isabelle/HOL, the theorem prover used for SeL4, plus some other random lemmas about it:

    theory Scratch
      imports Main
    begin

    fun increment :: "int ⇒ int" where 
    "increment x = x + 1"

    lemma increment_increments:
      shows "increment x = x + 1"
      by simp

    lemma double_increment_adds_two:
      shows "increment (increment x) = x + 2"
      by simp

    lemma increment_sub_1_is_x:
      shows "increment x - 1 = x"
      by simp