src/HOL/Nunchaku/Nunchaku.thy
author blanchet
Mon Oct 24 22:42:07 2016 +0200 (2016-10-24)
changeset 64389 6273d4c8325b
child 64407 5c5b9d945625
permissions -rw-r--r--
added Nunchaku integration
blanchet@64389
     1
(*  Title:      HOL/Nunchaku/Nunchaku.thy
blanchet@64389
     2
    Author:     Jasmin Blanchette, Inria Nancy, LORIA, MPII
blanchet@64389
     3
    Copyright   2015, 2016
blanchet@64389
     4
blanchet@64389
     5
Nunchaku: Yet another counterexample generator for Isabelle/HOL.
blanchet@64389
     6
blanchet@64389
     7
Nunchaku relies on an external program of the same name. The program is still
blanchet@64389
     8
being actively developed. The sources are available at
blanchet@64389
     9
blanchet@64389
    10
    https://github.com/nunchaku-inria
blanchet@64389
    11
*)
blanchet@64389
    12
blanchet@64389
    13
theory Nunchaku
blanchet@64389
    14
imports Main
blanchet@64389
    15
keywords
blanchet@64389
    16
  "nunchaku" :: diag and
blanchet@64389
    17
  "nunchaku_params" :: thy_decl
blanchet@64389
    18
begin
blanchet@64389
    19
blanchet@64389
    20
consts unreachable :: 'a
blanchet@64389
    21
blanchet@64389
    22
definition The_unsafe :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" where
blanchet@64389
    23
  "The_unsafe = The"
blanchet@64389
    24
blanchet@64389
    25
definition rmember :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" where
blanchet@64389
    26
  "rmember A x \<longleftrightarrow> x \<in> A"
blanchet@64389
    27
blanchet@64389
    28
ML_file "Tools/nunchaku_util.ML"
blanchet@64389
    29
ML_file "Tools/nunchaku_collect.ML"
blanchet@64389
    30
ML_file "Tools/nunchaku_problem.ML"
blanchet@64389
    31
ML_file "Tools/nunchaku_translate.ML"
blanchet@64389
    32
ML_file "Tools/nunchaku_model.ML"
blanchet@64389
    33
ML_file "Tools/nunchaku_reconstruct.ML"
blanchet@64389
    34
ML_file "Tools/nunchaku_display.ML"
blanchet@64389
    35
ML_file "Tools/nunchaku_tool.ML"
blanchet@64389
    36
ML_file "Tools/nunchaku.ML"
blanchet@64389
    37
ML_file "Tools/nunchaku_commands.ML"
blanchet@64389
    38
blanchet@64389
    39
hide_const (open) unreachable The_unsafe rmember
blanchet@64389
    40
blanchet@64389
    41
end