search

wimmers / poly-reductions

Polynomial-time reductions in Isabelle/HOL
2 stars 13 forks source link

refine reduction from `HOL` to `HOL-Nat` #37

Open BilelGho opened 3 years ago

BilelGho commented 3 years ago

HOL-nat is a specification over HOL functions. a HOL function or definition is HOL-nat if the argument(s) type as well as the return type are exclusively nat and all the call-back functions are HOL.

A refined function takes the same arguments as the original function,encoded as natural numbers, and returns the same the result, also encoded as a natural number.

In this branch a refinement of the already developed the reduction of a IMP- program (a polynomially bounded verificator for a NP problem) to a SAT formula is implemented. The equivalence between the initial function and the refined one is verified.

mabdula commented 3 years ago

Does this have a nat version of the theorem main_hol_lemma? I couldn't find that