--- 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
*}
--- 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.
*)
--- 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 =
--- 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
--- 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 []
--- 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'}),
--- 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}
--- 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"
--- 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;
--- 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