Some time ago I managed to build a theory supporting the Farm problem in Isabelle/HOL (attached below)
I wasn't expecting such a toil but lack of detailed documentation and a wicked simplifier made my life miserable for a whole week.
It is based on 3 sets:
and a function: is_leg_of : leg → animal.
As axioms, we have:
That is, facts that are implicitely known but you need to state for Isabelle with Main
theory to work:
Let R
be the number of rabbits in the farm and D
the number of ducks in the farm. With the preceding axioms, we were able to produce Isabelle-certified proofs that
R + D = 100
and
2*D + 4*R = 260
and then deduce that R=30
and D=70
.
Attachment | Size |
---|---|
Farm.thy | 5.67 KB |