[isabelle-dev] smt2

[Jasmin Blanchette]

Hi Makarius,

> While experimenting with the increasingly useful Isabelle/ML IDE, I've found various spots that are awaiting further cleanup, renovation or demolition. Just some arbitrary examples:
> 
>  * HOL/SAT.thy with some related ML modules.  I've brushed this up
>    recently, e.g. to get module names vs. file names right.  Actual
>    external SAT solvers don't work, though, so it is not really usable.
> 
>    A candidate for HOL-ex?

I'm not sure about the external solvers, but last time I tried (some years ago) they did work. Irrespectively, "SAT.thy" also provides the "dpll" solver, which is used in the function package (for SCNP) and in Nitpick (grep "SatSolver" in "HOL/Tools"). Hence, most of this infrastructure is still used and somewhat alive. See also the "dptsat" solver in the AFP. (The more moribund part is the "sat" proof method, which is mostly subsumed by "smt".)

>  * HOL/Tools/choice_specification.ML which is loaded into
>    HOL/Hilbert_Choice.thy -- really old stuff that would require serious
>    renovation if actually used: 'ax_specification' with its unchecked
>    axiomatization is actually unsed, and 'specification' only by
>    HOL-Auth (and its many clones).
> 
>    A candidate for HOL-Library, after removing the axiomatic part?
>    Nitpick seems to have special tricks to cope with it, though.

These special tricks could be taken out. They're not vital in any way.

Another candidate is "Quickcheck_Narrowing.thy". Nothing in "HOL" seems to depend on it, and (please correct me if I'm mistaken) hardly anybody go into the trouble of setting up Quickcheck (and GHC) so that it uses the narrowing strategy. Also, narrowing adds some overhead for every datatype defined (in the form of additionally generated constants and theorems), so having it outside "HOL" would speed up not only building "HOL" but also running application theories (slightly).

Narrowing sounds like a good idea in principle, and Lukas was able to get nice results on some theories (e.g. red-black tree). Nonetheless, my impression is that the current implementation does not entirely fulfill the promise of symbolic reasoning. As an example of a surprising failure, "quickcheck [narrowing]" is unable to refute

    lemma "EX m. m ~= 0 & (ALL n. m ~= Suc n)"

On paper, narrowing can definitely do it: Symbolically take m = 0 and m = Suc ?x and show that both cases

    0 ~= 0 & (ALL n. 0 ~= Suc n)
    Suc ?x ~= 0 & (ALL n. Suc ?x ~= Suc n)

are false (in the second case, by "narrowing" ?x to "n").

Jasmin