src/HOL/Int.thy

 proof
   fix z show "of_int z = id z"
     by (cases z rule: int_diff_cases, simp)
 qed
 
+
+instance int :: no_top
+  apply default
+  apply (rule_tac x="x + 1" in exI)
+  apply simp
+  done
+
+instance int :: no_bot
+  apply default
+  apply (rule_tac x="x - 1" in exI)
+  apply simp
+  done
 
 subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
 
 lift_definition nat :: "int \<Rightarrow> nat" is "\<lambda>(x, y). x - y"
   by auto