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
.