| name | program-to-model-extractor |
| description | Extract abstract mathematical models from functional code (Haskell, OCaml, F#) for formal reasoning in Isabelle/HOL. Use when users need to: (1) Convert functional programs to Isabelle definitions, (2) Extract high-level algorithm essence from implementation code, (3) Generate formal specifications and properties from code, (4) Create verification-ready models that capture mathematical properties while abstracting away implementation details. Focuses on structural recursion, algebraic data types, higher-order functions, and invariant extraction. |
Program-to-Model Extractor
Extract high-level mathematical models from functional code for formal reasoning in Isabelle/HOL.
Overview
This skill transforms functional programs (Haskell, OCaml, F#) into abstract mathematical models suitable for formal verification in Isabelle/HOL. The extraction focuses on the algorithm's mathematical essence—capturing core properties, invariants, and structural patterns while abstracting away language-specific implementation details.
Extraction Workflow
1. Analyze the Source Code
Identify key elements:
- Data structures: Algebraic types, lists, trees, custom types
- Core functions: Main computational logic
- Recursion patterns: Structural, tail, mutual recursion
- Properties: What should be true about inputs/outputs?
2. Extract Data Types
Convert source language types to Isabelle datatypes:
-- Haskell
data Tree a = Leaf | Node a (Tree a) (Tree a)
(* Isabelle *)
datatype 'a tree = Leaf | Node "'a" "'a tree" "'a tree"
3. Model Functions
Choose the appropriate Isabelle construct:
For primitive recursion (terminates obviously):
fun length :: "'a list ⇒ nat" where
"length [] = 0" |
"length (x # xs) = 1 + length xs"
