This repository contains the material accompanying the publication 'Structured development of implementations for divide-and-conquer specifications'[https://doi.org/10.1016/j.scico.2023.103011], and comprises the following theories for the Isabelle/HOL theorem prover (versions 2024, 2023 and 2022, see www.cl.cam.ac.uk/research/hvg/Isabelle and LICENSE for details):

• Preliminaries.thy -- the underlying framework
• DaC_synthesis.thy -- the divide-and-conquer design tactic with the relator deployed in the publication
• Powerset.thy -- an introductory example application of the tactic to power set construction
• Greedy.thy -- the case study concerning bases of finite matroids
• Scheduling.thy -- an application of the greedy tactic to a scheduling problem
• DaC_synthesis2.thy -- the same divide-and-conquer tactic but with a relator that fits to the quicksort strategy
• Quicksort.thy -- an application of the tactic resulting in a quicksort algorithm.