# HG changeset patch # User blanchet # Date 1268813683 -3600 # Node ID e4d1b5cbd4292a7fe20924802ac5ab24b0e84b55 # Parent a814cccce0b86624fb4935c37600452214f8782c added support for "specification" and "ax_specification" constructs to Nitpick diff -r a814cccce0b8 -r e4d1b5cbd429 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Mar 16 08:45:08 2010 +0100 +++ b/src/HOL/HOL.thy Wed Mar 17 09:14:43 2010 +0100 @@ -1999,8 +1999,6 @@ subsubsection {* Nitpick setup *} -text {* This will be relocated once Nitpick is moved to HOL. *} - ML {* structure Nitpick_Defs = Named_Thms ( @@ -2022,6 +2020,11 @@ val name = "nitpick_intro" val description = "introduction rules for (co)inductive predicates as needed by Nitpick" ) +structure Nitpick_Choice_Specs = Named_Thms +( + val name = "nitpick_choice_specs" + val description = "choice specification of constants as needed by Nitpick" +) *} setup {* @@ -2029,6 +2032,7 @@ #> Nitpick_Simps.setup #> Nitpick_Psimps.setup #> Nitpick_Intros.setup + #> Nitpick_Choice_Specs.setup *} diff -r a814cccce0b8 -r e4d1b5cbd429 src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Tue Mar 16 08:45:08 2010 +0100 +++ b/src/HOL/Nitpick.thy Wed Mar 17 09:14:43 2010 +0100 @@ -1,6 +1,6 @@ (* Title: HOL/Nitpick.thy Author: Jasmin Blanchette, TU Muenchen - Copyright 2008, 2009 + Copyright 2008, 2009, 2010 Nitpick: Yet another counterexample generator for Isabelle/HOL. *) diff -r a814cccce0b8 -r e4d1b5cbd429 src/HOL/Nitpick_Examples/Mono_Nits.thy --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Mar 16 08:45:08 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Wed Mar 17 09:14:43 2010 +0100 @@ -25,10 +25,11 @@ fast_descrs = false, tac_timeout = NONE, evals = [], case_names = [], def_table = def_table, nondef_table = Symtab.empty, user_nondefs = [], simp_table = Unsynchronized.ref Symtab.empty, psimp_table = Symtab.empty, - intro_table = Symtab.empty, ground_thm_table = Inttab.empty, - ersatz_table = [], skolems = Unsynchronized.ref [], - special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [], - wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []} + choice_spec_table = Symtab.empty, intro_table = Symtab.empty, + ground_thm_table = Inttab.empty, ersatz_table = [], + skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [], + unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [], + constr_cache = Unsynchronized.ref []} (* term -> bool *) fun is_mono t = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a} ([t], []) fun is_const t = diff -r a814cccce0b8 -r e4d1b5cbd429 src/HOL/Tools/Nitpick/HISTORY --- a/src/HOL/Tools/Nitpick/HISTORY Tue Mar 16 08:45:08 2010 +0100 +++ b/src/HOL/Tools/Nitpick/HISTORY Wed Mar 17 09:14:43 2010 +0100 @@ -5,6 +5,7 @@ * Added and implemented "finitize" option to improve the precision of infinite datatypes based on a monotonicity analysis * Added support for quotient types + * Added support for "specification" and "ax_specification" constructs * Added support for local definitions (for "function" and "termination" proofs) * Added support for term postprocessors diff -r a814cccce0b8 -r e4d1b5cbd429 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Mar 16 08:45:08 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Mar 17 09:14:43 2010 +0100 @@ -276,6 +276,9 @@ val nondef_table = const_nondef_table (built_in_nondefs @ user_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_table val ground_thm_table = ground_theorem_table thy val ersatz_table = ersatz_table thy @@ -289,9 +292,9 @@ case_names = case_names, def_table = def_table, nondef_table = nondef_table, user_nondefs = user_nondefs, simp_table = simp_table, psimp_table = psimp_table, - intro_table = intro_table, ground_thm_table = ground_thm_table, - ersatz_table = ersatz_table, skolems = Unsynchronized.ref [], - special_funs = Unsynchronized.ref [], + 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 frees = Term.add_frees assms_t [] diff -r a814cccce0b8 -r e4d1b5cbd429 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Mar 16 08:45:08 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Mar 17 09:14:43 2010 +0100 @@ -37,6 +37,7 @@ user_nondefs: term list, simp_table: const_table Unsynchronized.ref, psimp_table: const_table, + choice_spec_table: const_table, intro_table: const_table, ground_thm_table: term list Inttab.table, ersatz_table: (string * string) list, @@ -180,6 +181,8 @@ val const_nondef_table : term list -> const_table val const_simp_table : Proof.context -> (term * term) list -> const_table val const_psimp_table : Proof.context -> (term * term) list -> const_table + val const_choice_spec_table : + Proof.context -> (term * term) list -> const_table val inductive_intro_table : Proof.context -> (term * term) list -> const_table -> const_table val ground_theorem_table : theory -> term list Inttab.table @@ -197,6 +200,10 @@ val is_equational_fun : hol_context -> styp -> bool val is_constr_pattern_lhs : theory -> term -> bool val is_constr_pattern_formula : theory -> term -> bool + val nondef_props_for_const : + theory -> bool -> const_table -> styp -> term list + val is_choice_spec_fun : hol_context -> styp -> bool + val is_choice_spec_axiom : theory -> const_table -> term -> bool val codatatype_bisim_axioms : hol_context -> typ -> term list val is_well_founded_inductive_pred : hol_context -> styp -> bool val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term @@ -241,6 +248,7 @@ user_nondefs: term list, simp_table: const_table Unsynchronized.ref, psimp_table: const_table, + choice_spec_table: const_table, intro_table: const_table, ground_thm_table: term list Inttab.table, ersatz_table: (string * string) list, @@ -1441,18 +1449,6 @@ | NONE => t) | t => t) -(* term -> string * term *) -fun pair_for_prop t = - case term_under_def t of - Const (s, _) => (s, t) - | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t']) - -(* (Proof.context -> term list) -> Proof.context -> (term * term) list - -> const_table *) -fun table_for get ctxt subst = - ctxt |> get |> map (pair_for_prop o subst_atomic subst) - |> AList.group (op =) |> Symtab.make - (* theory -> (typ option * bool) list -> (string * int) list *) fun case_const_names thy stds = Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) => @@ -1514,6 +1510,67 @@ SOME t' => is_constr_pattern_lhs thy t' | NONE => false +(* Similar to "Refute.specialize_type" but returns all matches rather than only + the first (preorder) match. *) +(* theory -> styp -> term -> term list *) +fun multi_specialize_type thy slack (s, T) t = + let + (* term -> (typ * term) list -> (typ * term) list *) + fun aux (Const (s', T')) ys = + if s = s' then + ys |> (if AList.defined (op =) ys T' then + I + else + cons (T', Refute.monomorphic_term + (Sign.typ_match thy (T', T) Vartab.empty) t) + handle Type.TYPE_MATCH => I + | Refute.REFUTE _ => + if slack then + I + else + raise NOT_SUPPORTED ("too much polymorphism in \ + \axiom involving " ^ quote s)) + else + ys + | aux _ ys = ys + in map snd (fold_aterms aux t []) end +(* theory -> bool -> const_table -> styp -> term list *) +fun nondef_props_for_const thy slack table (x as (s, _)) = + these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x) + +(* term -> term *) +fun unvarify_term (t1 $ t2) = unvarify_term t1 $ unvarify_term t2 + | unvarify_term (Var ((s, 0), T)) = Free (s, T) + | unvarify_term (Abs (s, T, t')) = Abs (s, T, unvarify_term t') + | unvarify_term t = t +(* theory -> term -> term *) +fun axiom_for_choice_spec thy = + unvarify_term + #> Object_Logic.atomize_term thy + #> Choice_Specification.close_form + #> HOLogic.mk_Trueprop +(* hol_context -> styp -> bool *) +fun is_choice_spec_fun ({thy, def_table, nondef_table, choice_spec_table, ...} + : hol_context) x = + case nondef_props_for_const thy true choice_spec_table x of + [] => false + | ts => case def_of_const thy def_table x of + SOME (Const (@{const_name Eps}, _) $ _) => true + | SOME _ => false + | NONE => + let val ts' = nondef_props_for_const thy true nondef_table x in + length ts' = length ts andalso + forall (fn t => + exists (curry (op aconv) (axiom_for_choice_spec thy t)) + ts') ts + end + +(* theory -> const_table -> term -> bool *) +fun is_choice_spec_axiom thy choice_spec_table t = + Symtab.exists (fn (_, ts) => + exists (curry (op aconv) t o axiom_for_choice_spec thy) ts) + choice_spec_table + (** Constant unfolding **) (* theory -> (typ option * bool) list -> int * styp -> term *) @@ -1700,7 +1757,8 @@ else (Const x, ts) end - else if is_equational_fun hol_ctxt x then + else if is_equational_fun hol_ctxt x orelse + is_choice_spec_fun hol_ctxt x then (Const x, ts) else case def_of_const thy def_table x of SOME def => @@ -1719,29 +1777,45 @@ (** Axiom extraction/generation **) +(* term -> string * term *) +fun pair_for_prop t = + case term_under_def t of + Const (s, _) => (s, t) + | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t']) +(* (Proof.context -> term list) -> Proof.context -> (term * term) list + -> const_table *) +fun def_table_for get ctxt subst = + ctxt |> get |> map (pair_for_prop o subst_atomic subst) + |> AList.group (op =) |> Symtab.make +(* term -> string * term *) +fun paired_with_consts t = map (rpair t) (Term.add_const_names t []) (* Proof.context -> (term * term) list -> term list -> const_table *) fun const_def_table ctxt subst ts = - table_for (map prop_of o Nitpick_Defs.get) ctxt subst + def_table_for (map prop_of o Nitpick_Defs.get) ctxt subst |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t)) (map pair_for_prop ts) (* term list -> const_table *) fun const_nondef_table ts = - fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts [] - |> AList.group (op =) |> Symtab.make + fold (append o paired_with_consts) ts [] |> AList.group (op =) |> Symtab.make (* Proof.context -> (term * term) list -> const_table *) -val const_simp_table = table_for (map prop_of o Nitpick_Simps.get) -val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get) +val const_simp_table = def_table_for (map prop_of o Nitpick_Simps.get) +val const_psimp_table = def_table_for (map prop_of o Nitpick_Psimps.get) +fun const_choice_spec_table ctxt subst = + map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt) + |> const_nondef_table (* Proof.context -> (term * term) list -> const_table -> const_table *) fun inductive_intro_table ctxt subst def_table = - table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt) - def_table o prop_of) - o Nitpick_Intros.get) ctxt subst + def_table_for + (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt) + def_table o prop_of) + o Nitpick_Intros.get) ctxt subst (* theory -> term list Inttab.table *) fun ground_theorem_table thy = fold ((fn @{const Trueprop} $ t1 => is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1) | _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty +(* TODO: Move to "Nitpick.thy" *) val basic_ersatz_table = [(@{const_name prod_case}, @{const_name split}), (@{const_name card}, @{const_name card'}), diff -r a814cccce0b8 -r e4d1b5cbd429 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Mar 16 08:45:08 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Mar 17 09:14:43 2010 +0100 @@ -917,9 +917,9 @@ debug, binary_ints, destroy_constrs, specialize, skolemize, star_linear_preds, uncurry, fast_descrs, tac_timeout, evals, case_names, def_table, nondef_table, - user_nondefs, simp_table, psimp_table, intro_table, - ground_thm_table, ersatz_table, skolems, special_funs, - unrolled_preds, wf_cache, constr_cache}, + user_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, card_assigns, bits, bisim_depth, datatypes, ofs} : scope) formats all_frees free_names sel_names nonsel_names rel_table bounds = let @@ -936,10 +936,11 @@ case_names = case_names, def_table = def_table, nondef_table = nondef_table, user_nondefs = user_nondefs, simp_table = simp_table, psimp_table = psimp_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} + 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 a814cccce0b8 -r e4d1b5cbd429 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Mar 16 08:45:08 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Mar 17 09:14:43 2010 +0100 @@ -938,35 +938,6 @@ (** Axiom selection **) -(* Similar to "Refute.specialize_type" but returns all matches rather than only - the first (preorder) match. *) -(* theory -> styp -> term -> term list *) -fun multi_specialize_type thy slack (s, T) t = - let - (* term -> (typ * term) list -> (typ * term) list *) - fun aux (Const (s', T')) ys = - if s = s' then - ys |> (if AList.defined (op =) ys T' then - I - else - cons (T', Refute.monomorphic_term - (Sign.typ_match thy (T', T) Vartab.empty) t) - handle Type.TYPE_MATCH => I - | Refute.REFUTE _ => - if slack then - I - else - raise NOT_SUPPORTED ("too much polymorphism in \ - \axiom involving " ^ quote s)) - else - ys - | aux _ ys = ys - in map snd (fold_aterms aux t []) end - -(* theory -> bool -> const_table -> styp -> term list *) -fun nondef_props_for_const thy slack table (x as (s, _)) = - these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x) - (* 'a Symtab.table -> 'a list *) fun all_table_entries table = Symtab.fold (append o snd) table [] (* const_table -> string -> const_table *) @@ -985,8 +956,8 @@ (* hol_context -> term -> term list * term list * bool * bool *) fun axioms_for_term (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms, - fast_descrs, evals, def_table, nondef_table, user_nondefs, - ...}) t = + fast_descrs, evals, def_table, nondef_table, + choice_spec_table, user_nondefs, ...}) t = let type accumulator = styp list * (term list * term list) (* (term list * term list -> term list) @@ -1047,6 +1018,9 @@ else if is_equational_fun hol_ctxt x then fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x) accum + else if is_choice_spec_fun hol_ctxt x then + fold (add_nondef_axiom depth) + (nondef_props_for_const thy true choice_spec_table x) accum else if is_abs_fun thy x then if is_quot_type thy (range_type T) then raise NOT_SUPPORTED "\"Abs_\" function of quotient type" diff -r a814cccce0b8 -r e4d1b5cbd429 src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Mar 16 08:45:08 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Mar 17 09:14:43 2010 +0100 @@ -293,8 +293,9 @@ (* string -> string *) fun maybe_quote y = let val s = unyxml y in - y |> (not (is_long_identifier (perhaps (try (unprefix "'")) s)) orelse - OuterKeyword.is_keyword s) ? quote + y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso + not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse + OuterKeyword.is_keyword s) ? quote end end; diff -r a814cccce0b8 -r e4d1b5cbd429 src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Tue Mar 16 08:45:08 2010 +0100 +++ b/src/HOL/Tools/choice_specification.ML Wed Mar 17 09:14:43 2010 +0100 @@ -6,6 +6,7 @@ signature CHOICE_SPECIFICATION = sig + val close_form : term -> term val add_specification: string option -> (bstring * xstring * bool) list -> theory * thm -> theory * thm end @@ -15,6 +16,10 @@ (* actual code *) +fun close_form t = + fold_rev (fn (s, T) => fn t => HOLogic.mk_all (s, T, t)) + (map dest_Free (OldTerm.term_frees t)) t + local fun mk_definitional [] arg = arg | mk_definitional ((thname,cname,covld)::cos) (thy,thm) = @@ -120,8 +125,7 @@ val frees = OldTerm.term_frees prop val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees orelse error "Specificaton: Only free variables of sort 'type' allowed" - val prop_closed = fold_rev (fn (vname, T) => fn prop => - HOLogic.mk_all (vname, T, prop)) (map dest_Free frees) prop + val prop_closed = close_form prop in (prop_closed,frees) end @@ -190,7 +194,8 @@ args |> apsnd (remove_alls frees) |> apsnd undo_imps |> apsnd Drule.export_without_context - |> Thm.theory_attributes (map (Attrib.attribute thy) atts) + |> Thm.theory_attributes (map (Attrib.attribute thy) + (Attrib.internal (K Nitpick_Choice_Specs.add) :: atts)) |> add_final |> Library.swap end