Skip to content

Instantly share code, notes, and snippets.

@Cryolite

Cryolite/Scratch.thy

Last active May 18, 2020 14:23
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Cryolite/ce4781798f4509a320c9c85bef2ac3b3 to your computer and use it in GitHub Desktop.
Save Cryolite/ce4781798f4509a320c9c85bef2ac3b3 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Scratch.thy
theory Scratch
imports Main
begin
fun plus1 :: "nat ⇒ nat" where
"plus1 n = n + 1"
theorem plus1E:
assumes "plus1 x = y"
obtains "y = x + 1"
using assms by (rule plus1.elims[of x y], auto)
lemma
assumes "plus1 n = n + 2"
shows "False"
using assms by (elim plus1E, auto)
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment