--- a/src/HOL/Tools/Nitpick/HISTORY Mon Nov 23 22:59:48 2009 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY Tue Nov 24 10:33:21 2009 +0100
@@ -10,8 +10,8 @@
* Optimized Kodkod encoding of datatypes whose constructors don't appear in
the formula to falsify
* Added support for codatatype view of datatypes
- * Fixed soundness bugs related to sets, sets of sets, and (co)inductive
- predicates
+ * Fixed soundness bugs related to sets, sets of sets, (co)inductive
+ predicates, typedefs, and "finite"
* Fixed monotonicity check
* Fixed error when processing definitions
* Fixed error in "star_linear_preds" optimization
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Nov 23 22:59:48 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Nov 24 10:33:21 2009 +0100
@@ -251,7 +251,7 @@
val intro_table = inductive_intro_table ctxt def_table
val ground_thm_table = ground_theorem_table thy
val ersatz_table = ersatz_table thy
- val (ext_ctxt as {skolems, special_funs, wf_cache, ...}) =
+ val (ext_ctxt as {wf_cache, ...}) =
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
user_axioms = user_axioms, debug = debug, wfs = wfs,
destroy_constrs = destroy_constrs, specialize = specialize,
@@ -296,11 +296,9 @@
handle TYPE (_, Ts, ts) =>
raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
- val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t
- val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq)
- def_ts
- val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) Eq)
- nondef_ts
+ val core_u = nut_from_term ext_ctxt Eq core_t
+ val def_us = map (nut_from_term ext_ctxt DefEq) def_ts
+ val nondef_us = map (nut_from_term ext_ctxt Eq) nondef_ts
val (free_names, const_names) =
fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
val (sel_names, nonsel_names) =
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Nov 23 22:59:48 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Nov 24 10:33:21 2009 +0100
@@ -496,7 +496,7 @@
type typedef_info =
{rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
set_def: thm option, prop_of_Rep: thm, set_name: string,
- Rep_inverse: thm option}
+ Abs_inverse: thm option, Rep_inverse: thm option}
(* theory -> string -> typedef_info *)
fun typedef_info thy s =
@@ -505,13 +505,14 @@
Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
|> Logic.varify,
- set_name = @{const_name Frac}, Rep_inverse = NONE}
+ set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
else case Typedef.get_info thy s of
- SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Rep_inverse,
- ...} =>
+ SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
+ Rep_inverse, ...} =>
SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
- set_name = set_prefix ^ s, Rep_inverse = SOME Rep_inverse}
+ set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
+ Rep_inverse = SOME Rep_inverse}
| NONE => NONE
(* FIXME: use antiquotation for "code_numeral" below or detect "rep_datatype",
@@ -1288,11 +1289,13 @@
end
| NONE => []
end
-(* theory -> styp -> term *)
-fun inverse_axiom_for_rep_fun thy (x as (_, T)) =
+(* theory -> styp -> term list *)
+fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
let val abs_T = domain_type T in
- typedef_info thy (fst (dest_Type abs_T)) |> the |> #Rep_inverse |> the
- |> prop_of |> Refute.specialize_type thy x
+ typedef_info thy (fst (dest_Type abs_T)) |> the
+ |> pairf #Abs_inverse #Rep_inverse
+ |> pairself (Refute.specialize_type thy x o prop_of o the)
+ ||> single |> op ::
end
(* theory -> int * styp -> term *)
@@ -1493,14 +1496,7 @@
let
val (const, ts) =
if is_built_in_const fast_descrs x then
- if s = @{const_name finite} then
- if is_finite_type ext_ctxt (domain_type T) then
- (Abs ("A", domain_type T, @{const True}), ts)
- else case ts of
- [Const (@{const_name top}, _)] => (@{const False}, [])
- | _ => (Const x, ts)
- else
- (Const x, ts)
+ (Const x, ts)
else case AList.lookup (op =) case_names s of
SOME n =>
let
@@ -2475,7 +2471,7 @@
list_comb (f (),
map Bound (length trunk_arg_Ts - 1 downto 0))
in
- List.foldl absdummy
+ List.foldr absdummy
(Const (set_oper, [set_T, set_T] ---> set_T)
$ app pos $ app neg) trunk_arg_Ts
end
@@ -3063,8 +3059,8 @@
(extra_table def_table s) x)
|> add_axioms_for_term depth
(Const (mate_of_rep_fun thy x))
- |> add_maybe_def_axiom depth
- (inverse_axiom_for_rep_fun thy x)
+ |> fold (add_def_axiom depth)
+ (inverse_axioms_for_rep_fun thy x)
else
accum |> user_axioms <> SOME false
? fold (add_nondef_axiom depth)
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Nov 23 22:59:48 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Nov 24 10:33:21 2009 +0100
@@ -106,7 +106,7 @@
val name_ord : (nut * nut) -> order
val the_name : 'a NameTable.table -> nut -> 'a
val the_rel : nut NameTable.table -> nut -> Kodkod.n_ary_index
- val nut_from_term : theory -> bool -> special_fun list -> op2 -> term -> nut
+ val nut_from_term : extended_context -> op2 -> term -> nut
val choose_reps_for_free_vars :
scope -> nut list -> rep NameTable.table -> nut list * rep NameTable.table
val choose_reps_for_consts :
@@ -464,8 +464,8 @@
fun factorize (z as (Type ("*", _), _)) = maps factorize [mk_fst z, mk_snd z]
| factorize z = [z]
-(* theory -> bool -> special_fun list -> op2 -> term -> nut *)
-fun nut_from_term thy fast_descrs special_funs eq =
+(* extended_context -> op2 -> term -> nut *)
+fun nut_from_term (ext_ctxt as {thy, fast_descrs, special_funs, ...}) eq =
let
(* string list -> typ list -> term -> nut *)
fun aux eq ss Ts t =
@@ -596,7 +596,11 @@
Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
| (Const (@{const_name Suc}, T), []) => Cst (Suc, T, Any)
| (Const (@{const_name finite}, T), [t1]) =>
- Op1 (Finite, bool_T, Any, sub t1)
+ (if is_finite_type ext_ctxt (domain_type T) then
+ Cst (True, bool_T, Any)
+ else case t1 of
+ Const (@{const_name top}, _) => Cst (False, bool_T, Any)
+ | _ => Op1 (Finite, bool_T, Any, sub t1))
| (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
| (Const (@{const_name zero_nat_inst.zero_nat}, T), []) =>
Cst (Num 0, T, Any)
@@ -678,7 +682,7 @@
| NONE => if null ts then ConstName (s, T, Any)
else do_apply t0 ts)
| (Free (s, T), []) => FreeName (s, T, Any)
- | (Var _, []) => raise TERM ("Nitpick_Nut.nut_from_term", [t])
+ | (Var _, []) => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
| (Bound j, []) =>
BoundName (length Ts - j - 1, nth Ts j, Any, nth ss j)
| (Abs (s, T, t1), []) =>
--- a/src/HOL/Transitive_Closure.thy Mon Nov 23 22:59:48 2009 +0100
+++ b/src/HOL/Transitive_Closure.thy Tue Nov 24 10:33:21 2009 +0100
@@ -33,6 +33,11 @@
r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+"
| trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a, c) : r^+"
+declare rtrancl_def [nitpick_def del]
+ rtranclp_def [nitpick_def del]
+ trancl_def [nitpick_def del]
+ tranclp_def [nitpick_def del]
+
notation
rtranclp ("(_^**)" [1000] 1000) and
tranclp ("(_^++)" [1000] 1000)