Set theory reasoning of the ducks and rabbits problem

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.

AttachmentSize
Farm.thy5.67 KB