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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
