# HG changeset patch # User blanchet # Date 1303214698 -7200 # Node ID 10accf397ab603e0c14ad1faf2b1c35e0a5e7f3b # Parent 9465651c0db7175cff201162126f5f047a6f809b use "Spec_Rules" for finding axioms -- more reliable and cleaner diff -r 9465651c0db7 -r 10accf397ab6 src/HOL/Nitpick_Examples/Mini_Nits.thy --- 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 "\x. x = Not"} *} -ML {* none 1 @{prop "\ False"} *} -ML {* genuine 1 @{prop "\ True"} *} -ML {* none 1 @{prop "\ \ b \ b"} *} -ML {* none 1 @{prop True} *} -ML {* genuine 1 @{prop False} *} -ML {* genuine 1 @{prop "True \ False"} *} -ML {* none 1 @{prop "True \ \ False"} *} -ML {* none 5 @{prop "\x. x = x"} *} -ML {* none 5 @{prop "\x. x = x"} *} -ML {* none 1 @{prop "\x. x = y"} *} -ML {* genuine 2 @{prop "\x. x = y"} *} -ML {* none 1 @{prop "\x. x = y"} *} -ML {* none 2 @{prop "\x. x = y"} *} -ML {* none 2 @{prop "\x\'a \ 'a. x = x"} *} -ML {* none 2 @{prop "\x\'a \ 'a. x = y"} *} -ML {* genuine 2 @{prop "\x\'a \ 'a. x = y"} *} -ML {* none 2 @{prop "\x\'a \ '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 \ P x = P y"} *} -ML {* none 5 @{prop "(x\'a \ 'a) = y \ P x = P y"} *} -ML {* none 2 @{prop "(x\'a \ 'a) = y \ P x y = P y x"} *} -ML {* none 5 @{prop "\x\'a \ 'a. x = y \ P x = P y"} *} -ML {* none 2 @{prop "(x\'a \ 'a) = y \ P x = P y"} *} -ML {* none 2 @{prop "\x\'a \ 'a. x = y \ P x = P y"} *} -ML {* genuine 1 @{prop "(op =) X = Ex"} *} -ML {* none 2 @{prop "\x::'a \ 'a. x = x"} *} -ML {* none 1 @{prop "x = y"} *} -ML {* genuine 1 @{prop "x \ y"} *} -ML {* genuine 2 @{prop "x = y"} *} -ML {* genuine 1 @{prop "X \ Y"} *} -ML {* none 1 @{prop "P \ Q \ Q \ P"} *} -ML {* none 1 @{prop "P \ Q \ P"} *} -ML {* none 1 @{prop "P \ Q \ Q \ P"} *} -ML {* genuine 1 @{prop "P \ Q \ P"} *} -ML {* none 1 @{prop "(P \ Q) \ (\ P \ Q)"} *} -ML {* none 5 @{prop "{a} = {a, a}"} *} -ML {* genuine 2 @{prop "{a} = {a, b}"} *} -ML {* genuine 1 @{prop "{a} \ {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 \ c \ {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *} -ML {* none 5 @{prop "A \ B = (\x. A x \ B x)"} *} -ML {* none 5 @{prop "A \ B = (\x. A x \ B x)"} *} -ML {* none 5 @{prop "A - B = (\x. A x \ \ B x)"} *} -ML {* none 5 @{prop "\a b. (a, b) = (b, a)"} *} -ML {* genuine 2 @{prop "(a, b) = (b, a)"} *} -ML {* genuine 2 @{prop "(a, b) \ (b, a)"} *} -ML {* none 5 @{prop "\a b\'a \ 'a. (a, b) = (b, a)"} *} -ML {* genuine 2 @{prop "(a\'a \ 'a, b) = (b, a)"} *} -ML {* none 5 @{prop "\a b\'a \ 'a \ 'a. (a, b) = (b, a)"} *} -ML {* genuine 2 @{prop "(a\'a \ 'a \ 'a, b) \ (b, a)"} *} -ML {* none 5 @{prop "\a b\'a \ 'a. (a, b) = (b, a)"} *} -ML {* genuine 1 @{prop "(a\'a \ 'a, b) \ (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) \ 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) \ a"} *} -ML {* genuine 1 @{prop P} *} -ML {* genuine 1 @{prop "(\x. P) a"} *} -ML {* genuine 1 @{prop "(\x y z. P y x z) a b c"} *} -ML {* none 5 @{prop "\f. f = (\x. x) \ f y = y"} *} -ML {* genuine 1 @{prop "\f. f p \ p \ (\a b. f (a, b) = (a, b))"} *} -ML {* none 2 @{prop "\f. \a b. f (a, b) = (a, b)"} *} -ML {* none 3 @{prop "f = (\a b. (b, a)) \ f x y = (y, x)"} *} -ML {* genuine 2 @{prop "f = (\a b. (b, a)) \ f x y = (x, y)"} *} - -end diff -r 9465651c0db7 -r 10accf397ab6 src/HOL/Nitpick_Examples/Mono_Nits.thy --- 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 = diff -r 9465651c0db7 -r 10accf397ab6 src/HOL/Tools/Nitpick/nitpick.ML --- 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 = [] diff -r 9465651c0db7 -r 10accf397ab6 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 diff -r 9465651c0db7 -r 10accf397ab6 src/HOL/Tools/Nitpick/nitpick_model.ML --- 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} diff -r 9465651c0db7 -r 10accf397ab6 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- 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 **)