src/HOL/Nunchaku/Nunchaku.thy

more robust;

(*  Title:      HOL/Nunchaku/Nunchaku.thy
    Author:     Jasmin Blanchette, Inria Nancy, LORIA, MPII
    Copyright   2015, 2016

Nunchaku: Yet another counterexample generator for Isabelle/HOL.

Nunchaku relies on an external program of the same name. The program is still
being actively developed. The sources are available at

    https://github.com/nunchaku-inria

The "$NUNCHAKU_HOME" environment variable must be set to the absolute path to
the directory containing the "nunchaku" executable. The Isabelle components
for CVC4 and Kodkodi are necessary to use these backend solvers.
*)

theory Nunchaku
imports Main
keywords
  "nunchaku" :: diag and
  "nunchaku_params" :: thy_decl
begin

consts unreachable :: 'a

definition The_unsafe :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" where
  "The_unsafe = The"

definition rmember :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" where
  "rmember A x \<longleftrightarrow> x \<in> A"

ML_file "Tools/nunchaku_util.ML"
ML_file "Tools/nunchaku_collect.ML"
ML_file "Tools/nunchaku_problem.ML"
ML_file "Tools/nunchaku_translate.ML"
ML_file "Tools/nunchaku_model.ML"
ML_file "Tools/nunchaku_reconstruct.ML"
ML_file "Tools/nunchaku_display.ML"
ML_file "Tools/nunchaku_tool.ML"
ML_file "Tools/nunchaku.ML"
ML_file "Tools/nunchaku_commands.ML"

hide_const (open) unreachable The_unsafe rmember

end