Problem 2: Partition Refinement

· Uncategorized

The solution to this problem is written in Isabelle2013-2. The solution is a collection of primitive recursive functions. The Isabelle theory files are here: Problem2.

There are 3 files:

  • PartitionAlgorithm.thy – the implementation of the algorithm
  • PartitionProofs.thy - The definitions of the invariants and all proofs
  • PartitionTasks.thy – The proofs for the tasks.


Leave a Comment