## 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
```