isabelle: src/HOL/Nunchaku.thy@934d4aed8497 (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
66637 809d40cfa4de correctly locate SMBC from Nunchaku blanchet parents: 66614 diff changeset	14	for CVC4, Kodkodi, and SMBC 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
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66637 diff changeset	32	ML_file \<open>Tools/Nunchaku/nunchaku_util.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66637 diff changeset	33	ML_file \<open>Tools/Nunchaku/nunchaku_collect.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66637 diff changeset	34	ML_file \<open>Tools/Nunchaku/nunchaku_problem.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66637 diff changeset	35	ML_file \<open>Tools/Nunchaku/nunchaku_translate.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66637 diff changeset	36	ML_file \<open>Tools/Nunchaku/nunchaku_model.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66637 diff changeset	37	ML_file \<open>Tools/Nunchaku/nunchaku_reconstruct.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66637 diff changeset	38	ML_file \<open>Tools/Nunchaku/nunchaku_display.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66637 diff changeset	39	ML_file \<open>Tools/Nunchaku/nunchaku_tool.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66637 diff changeset	40	ML_file \<open>Tools/Nunchaku/nunchaku.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66637 diff changeset	41	ML_file \<open>Tools/Nunchaku/nunchaku_commands.ML\<close>
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	paulson <lp15@cam.ac.uk>
	Wed, 26 Oct 2022 17:22:12 +0100
changeset 76376	934d4aed8497
parent 69605	a96320074298
child 82024	bbda3b4f3c99
permissions	-rw-r--r--