# HG changeset patch # User blanchet # Date 1259055201 -3600 # Node ID 6cc01403f78ac37e37ec71a78b86796ae5327258 # Parent 8dfc55999130b016d8a54709c656f0d552976085# Parent e5e7faaed7adbfe8c44b90d996e6f883c3c6c26a merge diff -r e5e7faaed7ad -r 6cc01403f78a src/HOL/Tools/Nitpick/HISTORY --- 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 diff -r e5e7faaed7ad -r 6cc01403f78a src/HOL/Tools/Nitpick/nitpick.ML --- 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) = diff -r e5e7faaed7ad -r 6cc01403f78a src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 \ 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) diff -r e5e7faaed7ad -r 6cc01403f78a src/HOL/Tools/Nitpick/nitpick_nut.ML --- 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), []) => diff -r e5e7faaed7ad -r 6cc01403f78a src/HOL/Transitive_Closure.thy --- 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)