--- a/src/HOL/Nitpick_Examples/Mini_Nits.thy Tue Apr 19 12:22:59 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,108 +0,0 @@
-(* Title: HOL/Nitpick_Examples/Mini_Nits.thy
- Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009, 2010
-
-Examples featuring Minipick, the minimalistic version of Nitpick.
-*)
-
-header {* Examples Featuring Minipick, the Minimalistic Version of Nitpick *}
-
-theory Mini_Nits
-imports Main
-begin
-
-ML {*
-exception FAIL
-
-val has_kodkodi = (getenv "KODKODI" <> "")
-
-fun minipick n t =
- map (fn k => Minipick.kodkod_problem_from_term @{context} (K k) t) (1 upto n)
- |> Minipick.solve_any_kodkod_problem @{theory}
-fun minipick_expect expect n t =
- if has_kodkodi then
- if minipick n t = expect then () else raise FAIL
- else
- ()
-val none = minipick_expect "none"
-val genuine = minipick_expect "genuine"
-val unknown = minipick_expect "unknown"
-*}
-
-ML {* genuine 1 @{prop "x = Not"} *}
-ML {* none 1 @{prop "\<exists>x. x = Not"} *}
-ML {* none 1 @{prop "\<not> False"} *}
-ML {* genuine 1 @{prop "\<not> True"} *}
-ML {* none 1 @{prop "\<not> \<not> b \<longleftrightarrow> b"} *}
-ML {* none 1 @{prop True} *}
-ML {* genuine 1 @{prop False} *}
-ML {* genuine 1 @{prop "True \<longleftrightarrow> False"} *}
-ML {* none 1 @{prop "True \<longleftrightarrow> \<not> False"} *}
-ML {* none 5 @{prop "\<forall>x. x = x"} *}
-ML {* none 5 @{prop "\<exists>x. x = x"} *}
-ML {* none 1 @{prop "\<forall>x. x = y"} *}
-ML {* genuine 2 @{prop "\<forall>x. x = y"} *}
-ML {* none 1 @{prop "\<exists>x. x = y"} *}
-ML {* none 2 @{prop "\<exists>x. x = y"} *}
-ML {* none 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = x"} *}
-ML {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
-ML {* genuine 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = y"} *}
-ML {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
-ML {* none 1 @{prop "All = Ex"} *}
-ML {* genuine 2 @{prop "All = Ex"} *}
-ML {* none 1 @{prop "All P = Ex P"} *}
-ML {* genuine 2 @{prop "All P = Ex P"} *}
-ML {* none 5 @{prop "x = y \<longrightarrow> P x = P y"} *}
-ML {* none 5 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x = P y"} *}
-ML {* none 2 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x y = P y x"} *}
-ML {* none 5 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y \<longrightarrow> P x = P y"} *}
-ML {* none 2 @{prop "(x\<Colon>'a \<Rightarrow> 'a) = y \<longrightarrow> P x = P y"} *}
-ML {* none 2 @{prop "\<exists>x\<Colon>'a \<Rightarrow> 'a. x = y \<longrightarrow> P x = P y"} *}
-ML {* genuine 1 @{prop "(op =) X = Ex"} *}
-ML {* none 2 @{prop "\<forall>x::'a \<Rightarrow> 'a. x = x"} *}
-ML {* none 1 @{prop "x = y"} *}
-ML {* genuine 1 @{prop "x \<longleftrightarrow> y"} *}
-ML {* genuine 2 @{prop "x = y"} *}
-ML {* genuine 1 @{prop "X \<subseteq> Y"} *}
-ML {* none 1 @{prop "P \<and> Q \<longleftrightarrow> Q \<and> P"} *}
-ML {* none 1 @{prop "P \<and> Q \<longrightarrow> P"} *}
-ML {* none 1 @{prop "P \<or> Q \<longleftrightarrow> Q \<or> P"} *}
-ML {* genuine 1 @{prop "P \<or> Q \<longrightarrow> P"} *}
-ML {* none 1 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"} *}
-ML {* none 5 @{prop "{a} = {a, a}"} *}
-ML {* genuine 2 @{prop "{a} = {a, b}"} *}
-ML {* genuine 1 @{prop "{a} \<noteq> {a, b}"} *}
-ML {* none 5 @{prop "{}\<^sup>+ = {}"} *}
-ML {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
-ML {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
-ML {* none 5 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
-ML {* none 5 @{prop "A \<union> B = (\<lambda>x. A x \<or> B x)"} *}
-ML {* none 5 @{prop "A \<inter> B = (\<lambda>x. A x \<and> B x)"} *}
-ML {* none 5 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"} *}
-ML {* none 5 @{prop "\<exists>a b. (a, b) = (b, a)"} *}
-ML {* genuine 2 @{prop "(a, b) = (b, a)"} *}
-ML {* genuine 2 @{prop "(a, b) \<noteq> (b, a)"} *}
-ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a. (a, b) = (b, a)"} *}
-ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a, b) = (b, a)"} *}
-ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a \<times> 'a. (a, b) = (b, a)"} *}
-ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"} *}
-ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<Rightarrow> 'a. (a, b) = (b, a)"} *}
-ML {* genuine 1 @{prop "(a\<Colon>'a \<Rightarrow> 'a, b) \<noteq> (b, a)"} *}
-ML {* none 5 @{prop "fst (a, b) = a"} *}
-ML {* none 1 @{prop "fst (a, b) = b"} *}
-ML {* genuine 2 @{prop "fst (a, b) = b"} *}
-ML {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
-ML {* none 5 @{prop "snd (a, b) = b"} *}
-ML {* none 1 @{prop "snd (a, b) = a"} *}
-ML {* genuine 2 @{prop "snd (a, b) = a"} *}
-ML {* genuine 2 @{prop "snd (a, b) \<noteq> a"} *}
-ML {* genuine 1 @{prop P} *}
-ML {* genuine 1 @{prop "(\<lambda>x. P) a"} *}
-ML {* genuine 1 @{prop "(\<lambda>x y z. P y x z) a b c"} *}
-ML {* none 5 @{prop "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"} *}
-ML {* genuine 1 @{prop "\<exists>f. f p \<noteq> p \<and> (\<forall>a b. f (a, b) = (a, b))"} *}
-ML {* none 2 @{prop "\<exists>f. \<forall>a b. f (a, b) = (a, b)"} *}
-ML {* none 3 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (y, x)"} *}
-ML {* genuine 2 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (x, y)"} *}
-
-end
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Apr 19 12:22:59 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Apr 19 14:04:58 2011 +0200
@@ -23,14 +23,13 @@
val stds = [(NONE, true)]
val subst = []
val case_names = case_const_names ctxt stds
-val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst
+val defs = all_defs_of thy subst
+val nondefs = all_nondefs_of ctxt subst
val def_tables = const_def_tables ctxt subst defs
-val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
+val nondef_table = const_nondef_table nondefs
val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
val psimp_table = const_psimp_table ctxt subst
val choice_spec_table = const_choice_spec_table ctxt subst
-val user_nondefs =
- user_nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
val intro_table = inductive_intro_table ctxt subst def_tables
val ground_thm_table = ground_theorem_table thy
val ersatz_table = ersatz_table ctxt
@@ -40,13 +39,13 @@
whacks = [], binary_ints = SOME false, destroy_constrs = true,
specialize = false, star_linear_preds = false, total_consts = NONE,
needs = NONE, tac_timeout = NONE, evals = [], case_names = case_names,
- def_tables = def_tables, nondef_table = nondef_table,
- user_nondefs = user_nondefs, simp_table = simp_table,
- psimp_table = psimp_table, choice_spec_table = choice_spec_table,
- intro_table = intro_table, ground_thm_table = ground_thm_table,
- ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
- special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
- wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
+ def_tables = def_tables, nondef_table = nondef_table, nondefs = nondefs,
+ simp_table = simp_table, psimp_table = psimp_table,
+ choice_spec_table = choice_spec_table, intro_table = intro_table,
+ ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
+ skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
+ unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
+ constr_cache = Unsynchronized.ref []}
val binarize = false
fun is_mono t =
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Apr 19 12:22:59 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Apr 19 14:04:58 2011 +0200
@@ -270,14 +270,15 @@
val original_max_genuine = max_genuine
val max_bisim_depth = fold Integer.max bisim_depths ~1
val case_names = case_const_names ctxt stds
- val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst
+ val defs = all_defs_of thy subst
+ val nondefs = all_nondefs_of ctxt subst
val def_tables = const_def_tables ctxt subst defs
- val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
+ val nondef_table = const_nondef_table nondefs
val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
val psimp_table = const_psimp_table ctxt subst
val choice_spec_table = const_choice_spec_table ctxt subst
- val user_nondefs =
- user_nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
+ val nondefs =
+ nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
val intro_table = inductive_intro_table ctxt subst def_tables
val ground_thm_table = ground_theorem_table thy
val ersatz_table = ersatz_table ctxt
@@ -289,11 +290,11 @@
star_linear_preds = star_linear_preds, total_consts = total_consts,
needs = needs, tac_timeout = tac_timeout, evals = evals,
case_names = case_names, def_tables = def_tables,
- nondef_table = nondef_table, user_nondefs = user_nondefs,
- simp_table = simp_table, psimp_table = psimp_table,
- choice_spec_table = choice_spec_table, intro_table = intro_table,
- ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
- skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
+ nondef_table = nondef_table, nondefs = nondefs, simp_table = simp_table,
+ psimp_table = psimp_table, choice_spec_table = choice_spec_table,
+ intro_table = intro_table, ground_thm_table = ground_thm_table,
+ ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
+ special_funs = Unsynchronized.ref [],
unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
constr_cache = Unsynchronized.ref []}
val pseudo_frees = []
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Apr 19 12:22:59 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Apr 19 14:04:58 2011 +0200
@@ -34,7 +34,7 @@
case_names: (string * int) list,
def_tables: const_table * const_table,
nondef_table: const_table,
- user_nondefs: term list,
+ nondefs: term list,
simp_table: const_table Unsynchronized.ref,
psimp_table: const_table,
choice_spec_table: const_table,
@@ -181,8 +181,8 @@
val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
val special_bounds : term list -> (indexname * typ) list
val is_funky_typedef : Proof.context -> typ -> bool
- val all_axioms_of :
- Proof.context -> (term * term) list -> term list * term list * term list
+ val all_defs_of : theory -> (term * term) list -> term list
+ val all_nondefs_of : Proof.context -> (term * term) list -> term list
val arity_of_built_in_const :
theory -> (typ option * bool) list -> styp -> int option
val is_built_in_const :
@@ -267,7 +267,7 @@
case_names: (string * int) list,
def_tables: const_table * const_table,
nondef_table: const_table,
- user_nondefs: term list,
+ nondefs: term list,
simp_table: const_table Unsynchronized.ref,
psimp_table: const_table,
choice_spec_table: const_table,
@@ -1255,9 +1255,6 @@
is_frac_type ctxt (Type (s, []))
fun is_funky_typedef ctxt (Type (s, _)) = is_funky_typedef_name ctxt s
| is_funky_typedef _ _ = false
-fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
- $ Const (@{const_name TYPE}, _)) = true
- | is_arity_type_axiom _ = false
fun is_typedef_axiom ctxt boring (@{const "==>"} $ _ $ t2) =
is_typedef_axiom ctxt boring t2
| is_typedef_axiom ctxt boring
@@ -1266,21 +1263,15 @@
$ Const _ $ _)) =
boring <> is_funky_typedef_name ctxt s andalso is_typedef ctxt s
| is_typedef_axiom _ _ _ = false
-val is_class_axiom =
- Logic.strip_horn #> swap #> op :: #> forall (can Logic.dest_of_class)
(* Distinguishes between (1) constant definition axioms, (2) type arity and
typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
Typedef axioms are uninteresting to Nitpick, because it can retrieve them
using "typedef_info". *)
-fun partition_axioms_by_definitionality ctxt axioms def_names =
- let
- val axioms = sort (fast_string_ord o pairself fst) axioms
- val defs = Ord_List.inter (fast_string_ord o apsnd fst) def_names axioms
- val nondefs =
- Ord_List.subtract (fast_string_ord o apsnd fst) def_names axioms
- |> filter_out ((is_arity_type_axiom orf is_typedef_axiom ctxt true) o snd)
- in pairself (map snd) (defs, nondefs) end
+fun filter_defs def_names =
+ sort (fast_string_ord o pairself fst)
+ #> Ord_List.inter (fast_string_ord o apsnd fst) def_names
+ #> map snd
(* Ideally we would check against "Complex_Main", not "Refute", but any theory
will do as long as it contains all the "axioms" and "axiomatization"
@@ -1302,36 +1293,32 @@
| do_eq _ = false
in do_eq end
-fun all_axioms_of ctxt subst =
+fun all_defs_of thy subst =
let
- val thy = Proof_Context.theory_of ctxt
- val axioms_of_thys =
- maps Thm.axioms_of
- #> map (apsnd (subst_atomic subst o prop_of))
- #> filter_out (is_class_axiom o snd)
- val specs = Defs.all_specifications_of (Theory.defs_of thy)
- val def_names = specs |> maps snd |> map_filter #def
- |> Ord_List.make fast_string_ord
+ val def_names =
+ thy |> Theory.defs_of
+ |> Defs.all_specifications_of
+ |> maps snd |> map_filter #def
+ |> Ord_List.make fast_string_ord
val thys = thy :: Theory.ancestors_of thy
- val (built_in_thys, user_thys) = List.partition is_built_in_theory thys
- val built_in_axioms = axioms_of_thys built_in_thys
- val user_axioms = axioms_of_thys user_thys
- val (built_in_defs, built_in_nondefs) =
- partition_axioms_by_definitionality ctxt built_in_axioms def_names
- ||> filter (is_typedef_axiom ctxt false)
- val (user_defs, user_nondefs) =
- partition_axioms_by_definitionality ctxt user_axioms def_names
- val (built_in_nondefs, user_nondefs) =
- List.partition (is_typedef_axiom ctxt false) user_nondefs
- |>> append built_in_nondefs
- val defs =
- (thy |> Global_Theory.all_thms_of
- |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd)
- |> map (prop_of o snd)
- |> filter_out is_trivial_definition
- |> filter is_plain_definition) @
- user_defs @ built_in_defs
- in (defs, built_in_nondefs, user_nondefs) end
+ in
+ (* FIXME: avoid relying on "Thm.definitionK" *)
+ (thy |> Global_Theory.all_thms_of
+ |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd)
+ |> map (subst_atomic subst o prop_of o snd)
+ |> filter_out is_trivial_definition
+ |> filter is_plain_definition) @
+ (thys |> maps Thm.axioms_of
+ |> map (apsnd (subst_atomic subst o prop_of))
+ |> filter_defs def_names)
+ end
+
+fun all_nondefs_of ctxt subst =
+ ctxt |> Spec_Rules.get
+ |> filter (curry (op =) Spec_Rules.Unknown o fst)
+ |> maps (snd o snd)
+ |> filter_out (is_built_in_theory o theory_of_thm)
+ |> map (subst_atomic subst o prop_of)
fun arity_of_built_in_const thy stds (s, T) =
if s = @{const_name If} then
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Apr 19 12:22:59 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Apr 19 14:04:58 2011 +0200
@@ -865,7 +865,7 @@
({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
debug, whacks, binary_ints, destroy_constrs, specialize,
star_linear_preds, total_consts, needs, tac_timeout,
- evals, case_names, def_tables, nondef_table, user_nondefs,
+ evals, case_names, def_tables, nondef_table, nondefs,
simp_table, psimp_table, choice_spec_table, intro_table,
ground_thm_table, ersatz_table, skolems, special_funs,
unrolled_preds, wf_cache, constr_cache}, binarize,
@@ -884,13 +884,12 @@
star_linear_preds = star_linear_preds, total_consts = total_consts,
needs = needs, tac_timeout = tac_timeout, evals = evals,
case_names = case_names, def_tables = def_tables,
- nondef_table = nondef_table, user_nondefs = user_nondefs,
- simp_table = simp_table, psimp_table = psimp_table,
- choice_spec_table = choice_spec_table, intro_table = intro_table,
- ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
- skolems = skolems, special_funs = special_funs,
- unrolled_preds = unrolled_preds, wf_cache = wf_cache,
- constr_cache = constr_cache}
+ nondef_table = nondef_table, nondefs = nondefs, simp_table = simp_table,
+ psimp_table = psimp_table, choice_spec_table = choice_spec_table,
+ intro_table = intro_table, ground_thm_table = ground_thm_table,
+ ersatz_table = ersatz_table, skolems = skolems,
+ special_funs = special_funs, unrolled_preds = unrolled_preds,
+ wf_cache = wf_cache, constr_cache = constr_cache}
val scope =
{hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Apr 19 12:22:59 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Apr 19 14:04:58 2011 +0200
@@ -889,7 +889,7 @@
fun axioms_for_term
(hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
evals, def_tables, nondef_table, choice_spec_table,
- user_nondefs, ...}) assm_ts neg_t =
+ nondefs, ...}) assm_ts neg_t =
let
val (def_assm_ts, nondef_assm_ts) =
List.partition (assumption_exclusively_defines_free assm_ts) assm_ts
@@ -1030,8 +1030,8 @@
\add_axioms_for_sort", [t]))
class_axioms
in fold (add_nondef_axiom depth) monomorphic_class_axioms end
- val (mono_user_nondefs, poly_user_nondefs) =
- List.partition (null o Term.hidden_polymorphism) user_nondefs
+ val (mono_nondefs, poly_nondefs) =
+ List.partition (null o Term.hidden_polymorphism) nondefs
val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
evals
val (seen, (defs, nondefs)) =
@@ -1039,13 +1039,11 @@
|> add_axioms_for_term 1 neg_t
|> fold_rev (add_nondef_axiom 1) nondef_assm_ts
|> fold_rev (add_def_axiom 1) eval_axioms
- |> user_axioms = SOME true ? fold (add_nondef_axiom 1) mono_user_nondefs
+ |> user_axioms = SOME true ? fold (add_nondef_axiom 1) mono_nondefs
val defs = defs @ special_congruence_axioms hol_ctxt seen
val got_all_mono_user_axioms =
- (user_axioms = SOME true orelse null mono_user_nondefs)
- in
- (neg_t :: nondefs, defs, got_all_mono_user_axioms, null poly_user_nondefs)
- end
+ (user_axioms = SOME true orelse null mono_nondefs)
+ in (neg_t :: nondefs, defs, got_all_mono_user_axioms, null poly_nondefs) end
(** Simplification of constructor/selector terms **)