This is a theorem (the Isabelle song)

sung to the tune of “I don’t like mondays”, with apologies to Boomtown Rats

Created at the Marktoberdorf Summer School 2013

The silicon chip inside her head
	gets switched to HOL
No pen and paper proofs today
	she’s gonna make it rigorous
And now I don’t understand it,
I always thought it was trivial
	but auto finds no proofs
	but there are some proofs
	what lemmas does she need to be shown?

Tell me why – this is a theorem
Tell me why – this is a theorem
Tell me why – this is a theorem
	I’m gonna prove the first goal now

An inductive fact is here assumed
	so I type induction x
and two new goals I have to show
	and the simplifier solved just one
The next case ain’t not obvious,
but it ain’t so neat to just type sorry
	and auto finds no proofs
	but there are some proofs
	what lemmas does she need oh oh oh oh

Tell me why – this is a theorem
Tell me why – this is a theorem
Tell me why – this is a theorem
	I’m gonna prove uh uh uh uhh the next goal now now now prove it all now

And sledgehammer stopped without a metis call
	And nitpick says its hopeless
So how could Gerwin show all the lemmas
	by induction and by auto
Trying arbitrary, ’cause Tobias told us
to better generalize
	but auto finds no proofs
	but there are some proofs
	what lemmas does she need to know know? oh oh oh

Tell me why – this is a theorem
Tell me why – this is a theorem
Tell me why – this is a  this is a  this is a  theorem
Tell me why – this is a  this is a  this is a  theorem
Tell me why – this is a theorem
	I’m gonna prove uh uh uh uhh the last goal now