isabelle: src/HOL/Nunchaku.thy@1f1c5d85d232 (annotated)

66614 1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years blanchet parents: 66163 diff changeset	1	(* Title: HOL/Nunchaku.thy
1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years blanchet parents: 66163 diff changeset	2	Author: Jasmin Blanchette, VU Amsterdam
1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years blanchet parents: 66163 diff changeset	3	Copyright 2015, 2016, 2017
64389 6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	4
6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	5	Nunchaku: Yet another counterexample generator for Isabelle/HOL.
6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	6
66614 1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years blanchet parents: 66163 diff changeset	7	Nunchaku relies on an external program of the same name. The sources are
1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years blanchet parents: 66163 diff changeset	8	available at
64389 6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	9
6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	10	https://github.com/nunchaku-inria
64407 5c5b9d945625 proper Nunchaku setup to use CVC4 and Kodkod blanchet parents: 64389 diff changeset	11
64469 488d4e627238 added Nunchaku component and tuned Nunchaku integration accordingly blanchet parents: 64407 diff changeset	12	The "$NUNCHAKU_HOME" environment variable must be set to the absolute path to
488d4e627238 added Nunchaku component and tuned Nunchaku integration accordingly blanchet parents: 64407 diff changeset	13	the directory containing the "nunchaku" executable. The Isabelle components
66163 45d3d43abee7 added 'solvers' option to Nunchaku blanchet parents: 64469 diff changeset	14	for CVC4 and Kodkodi are necessary to use these backend solvers.
64389 6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	15	*)
6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	16
6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	17	theory Nunchaku
66614 1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years blanchet parents: 66163 diff changeset	18	imports Nitpick
64389 6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	19	keywords
6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	20	"nunchaku" :: diag and
6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	21	"nunchaku_params" :: thy_decl
6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	22	begin
6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	23
6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	24	consts unreachable :: 'a
6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	25
6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	26	definition The_unsafe :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" where
6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	27	"The_unsafe = The"
6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	28
6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	29	definition rmember :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" where
6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	30	"rmember A x \<longleftrightarrow> x \<in> A"
6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	31
66614 1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years blanchet parents: 66163 diff changeset	32	ML_file "Tools/Nunchaku/nunchaku_util.ML"
1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years blanchet parents: 66163 diff changeset	33	ML_file "Tools/Nunchaku/nunchaku_collect.ML"
1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years blanchet parents: 66163 diff changeset	34	ML_file "Tools/Nunchaku/nunchaku_problem.ML"
1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years blanchet parents: 66163 diff changeset	35	ML_file "Tools/Nunchaku/nunchaku_translate.ML"
1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years blanchet parents: 66163 diff changeset	36	ML_file "Tools/Nunchaku/nunchaku_model.ML"
1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years blanchet parents: 66163 diff changeset	37	ML_file "Tools/Nunchaku/nunchaku_reconstruct.ML"
1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years blanchet parents: 66163 diff changeset	38	ML_file "Tools/Nunchaku/nunchaku_display.ML"
1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years blanchet parents: 66163 diff changeset	39	ML_file "Tools/Nunchaku/nunchaku_tool.ML"
1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years blanchet parents: 66163 diff changeset	40	ML_file "Tools/Nunchaku/nunchaku.ML"
1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years blanchet parents: 66163 diff changeset	41	ML_file "Tools/Nunchaku/nunchaku_commands.ML"
64389 6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	42
6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	43	hide_const (open) unreachable The_unsafe rmember
6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	44
6273d4c8325b added Nunchaku integration blanchet parents: diff changeset	45	end

author	blanchet
	Fri, 08 Sep 2017 00:01:36 +0200
changeset 66614	1f1c5d85d232
parent 66163	src/HOL/Nunchaku/Nunchaku.thy@45d3d43abee7
child 66637	809d40cfa4de
permissions	-rw-r--r--