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.

Assumptions

It is based on 3 sets:

• Being in the farm (farm)
• Being a duck
• Being a rabbit

• and a function: is_leg_of : leg → animal.

  As axioms, we have:

Ground knowledge axioms

• Rabbits have 4 legs.
• Ducks have 2 legs.

Problem axioms

• All animals in the farm are rabbits or ducks.
• There are 100 animals in the farm.
• There are 260 legs in the farm

Extra axioms

That is, facts that are implicitely known but you need to state for Isabelle with Main theory to work:

• Rabbits and ducks are finite
• Rabbits and ducks are disjoint

Variables and equations

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.