--- a/doc-src/Nitpick/nitpick.tex Tue Apr 13 11:54:05 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex Tue Apr 13 14:08:58 2010 +0200
@@ -1445,8 +1445,8 @@
(\!\begin{aligned}[t]%
& \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
& \textit{Branch}~\xi_1~\xi_2 := \xi_2)\end{aligned}$ \\[2\smallskipamount]
-The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps
-even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}'').
+The existence of a nonstandard model suggests that the induction hypothesis is not general enough or may even
+be wrong. See the Nitpick manual's ``Inductive Properties'' section for details (``\textit{isabelle doc nitpick}'').
\postw
Reading the Nitpick manual is a most excellent idea.
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Apr 13 11:54:05 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Apr 13 14:08:58 2010 +0200
@@ -225,13 +225,15 @@
o Pretty.chunks o cons (Pretty.str "") o single
o Pretty.mark Markup.hilite
else
- priority o Pretty.string_of
+ (fn s => (priority s; if debug then tracing s else ()))
+ o Pretty.string_of
(* (unit -> Pretty.T) -> unit *)
fun pprint_m f = () |> not auto ? pprint o f
fun pprint_v f = () |> verbose ? pprint o f
fun pprint_d f = () |> debug ? pprint o f
(* string -> unit *)
val print = pprint o curry Pretty.blk 0 o pstrs
+ val print_g = pprint o Pretty.str
(* (unit -> string) -> unit *)
val print_m = pprint_m o K o plazy
val print_v = pprint_v o K o plazy
@@ -265,8 +267,8 @@
val original_max_potential = max_potential
val original_max_genuine = max_genuine
(*
- val _ = priority ("*** " ^ Syntax.string_of_term ctxt orig_t)
- val _ = List.app (fn t => priority ("*** " ^ Syntax.string_of_term ctxt t))
+ val _ = print_g ("*** " ^ Syntax.string_of_term ctxt orig_t)
+ val _ = List.app (fn t => print_g ("*** " ^ Syntax.string_of_term ctxt t))
orig_assm_ts
*)
val max_bisim_depth = fold Integer.max bisim_depths ~1
@@ -338,7 +340,7 @@
| _ => false) finitizes)
val standard = forall snd stds
(*
- val _ = List.app (priority o string_for_nut ctxt) (nondef_us @ def_us)
+ val _ = List.app (print_g o string_for_nut ctxt) (nondef_us @ def_us)
*)
val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
@@ -431,10 +433,10 @@
else
()
(*
- val _ = priority "Monotonic types:"
- val _ = List.app (priority o string_for_type ctxt) mono_Ts
- val _ = priority "Nonmonotonic types:"
- val _ = List.app (priority o string_for_type ctxt) nonmono_Ts
+ val _ = print_g "Monotonic types:"
+ val _ = List.app (print_g o string_for_type ctxt) mono_Ts
+ val _ = print_g "Nonmonotonic types:"
+ val _ = List.app (print_g o string_for_type ctxt) nonmono_Ts
*)
val need_incremental = Int.max (max_potential, max_genuine) >= 2
@@ -472,10 +474,10 @@
raise TOO_LARGE ("Nitpick.pick_them_nits_in_term.\
\problem_for_scope", "too large scope")
(*
- val _ = priority "Offsets:"
+ val _ = print_g "Offsets:"
val _ = List.app (fn (T, j0) =>
- priority (string_for_type ctxt T ^ " = " ^
- string_of_int j0))
+ print_g (string_for_type ctxt T ^ " = " ^
+ string_of_int j0))
(Typtab.dest ofs)
*)
val all_exact = forall (is_exact_type datatypes true) all_Ts
@@ -504,7 +506,7 @@
val nondef_us = map (choose_reps_in_nut scope unsound rep_table false)
nondef_us
(*
- val _ = List.app (priority o string_for_nut ctxt)
+ val _ = List.app (print_g o string_for_nut ctxt)
(free_names @ sel_names @ nonsel_names @
nondef_us @ def_us)
*)
@@ -658,9 +660,9 @@
();
if not standard andalso likely_in_struct_induct_step then
print "The existence of a nonstandard model suggests that the \
- \induction hypothesis is not general enough or perhaps \
- \even wrong. See the \"Inductive Properties\" section of \
- \the Nitpick manual for details (\"isabelle doc nitpick\")."
+ \induction hypothesis is not general enough or may even be \
+ \wrong. See the Nitpick manual's \"Inductive Properties\" \
+ \section for details (\"isabelle doc nitpick\")."
else
();
if has_syntactic_sorts orig_t then
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Apr 13 11:54:05 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Apr 13 14:08:58 2010 +0200
@@ -1265,9 +1265,8 @@
boring <> is_funky_typedef_name thy s andalso is_typedef thy s
| is_typedef_axiom _ _ _ = false
(* term -> bool *)
-fun is_class_axiom t =
- (t |> Logic.strip_horn |> swap |> op :: |> map Logic.dest_of_class; true)
- handle TERM _ => 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)).
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Apr 13 11:54:05 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Apr 13 14:08:58 2010 +0200
@@ -1431,16 +1431,22 @@
else if is_Cst Unrep u2 then to_compare_with_unrep u1 true_atom
else kk_nat_less (to_integer u1) (to_integer u2)
| @{typ int} => kk_int_less (to_integer u1) (to_integer u2)
- | _ => double_rel_rel_let kk
- (fn r1 => fn r2 =>
- kk_rel_if
- (fold kk_and (map_filter (fn (u, r) =>
- if is_opt_rep (rep_of u) then SOME (kk_some r)
- else NONE) [(u1, r1), (u2, r2)]) KK.True)
- (atom_from_formula kk bool_j0 (KK.LT (pairself
- (int_expr_from_atom kk (type_of u1)) (r1, r2))))
- KK.None)
- (to_r u1) (to_r u2))
+ | _ =>
+ let
+ val R1 = Opt (Atom (card_of_rep (rep_of u1),
+ offset_of_type ofs (type_of u1)))
+ in
+ double_rel_rel_let kk
+ (fn r1 => fn r2 =>
+ kk_rel_if
+ (fold kk_and (map_filter (fn (u, r) =>
+ if is_opt_rep (rep_of u) then SOME (kk_some r)
+ else NONE) [(u1, r1), (u2, r2)]) KK.True)
+ (atom_from_formula kk bool_j0 (KK.LT (pairself
+ (int_expr_from_atom kk (type_of u1)) (r1, r2))))
+ KK.None)
+ (to_rep R1 u1) (to_rep R1 u2)
+ end)
| Op2 (The, _, R, u1, u2) =>
if is_opt_rep R then
let val r1 = to_opt (Func (unopt_rep R, bool_atom_R)) u1 in
@@ -1854,40 +1860,42 @@
oper (KK.IntReg 0) (KK.IntReg 1))]))))
end
(* rep -> rep -> KK.rel_expr -> nut -> KK.rel_expr *)
- and to_apply res_R func_u arg_u =
- case unopt_rep (rep_of func_u) of
- Unit =>
- let val j0 = offset_of_type ofs (type_of func_u) in
+ and to_apply (R as Formula _) func_u arg_u =
+ raise REP ("Nitpick_Kodkod.to_apply", [R])
+ | to_apply res_R func_u arg_u =
+ case unopt_rep (rep_of func_u) of
+ Unit =>
+ let val j0 = offset_of_type ofs (type_of func_u) in
+ to_guard [arg_u] res_R
+ (rel_expr_from_rel_expr kk res_R (Atom (1, j0)) (KK.Atom j0))
+ end
+ | Atom (1, j0) =>
to_guard [arg_u] res_R
- (rel_expr_from_rel_expr kk res_R (Atom (1, j0)) (KK.Atom j0))
- end
- | Atom (1, j0) =>
- to_guard [arg_u] res_R
- (rel_expr_from_rel_expr kk res_R (Atom (1, j0)) (to_r func_u))
- | Atom (k, _) =>
- let
- val dom_card = card_of_rep (rep_of arg_u)
- val ran_R = Atom (exact_root dom_card k,
- offset_of_type ofs (range_type (type_of func_u)))
- in
- to_apply_vect dom_card ran_R res_R (to_vect dom_card ran_R func_u)
- arg_u
- end
- | Vect (1, R') =>
- to_guard [arg_u] res_R
- (rel_expr_from_rel_expr kk res_R R' (to_r func_u))
- | Vect (k, R') => to_apply_vect k R' res_R (to_r func_u) arg_u
- | Func (R, Formula Neut) =>
- to_guard [arg_u] res_R (rel_expr_from_formula kk res_R
- (kk_subset (to_opt R arg_u) (to_r func_u)))
- | Func (Unit, R2) =>
- to_guard [arg_u] res_R
- (rel_expr_from_rel_expr kk res_R R2 (to_r func_u))
- | Func (R1, R2) =>
- rel_expr_from_rel_expr kk res_R R2
- (kk_n_fold_join kk true R1 R2 (to_opt R1 arg_u) (to_r func_u))
- |> body_rep R2 = Formula Neut ? to_guard [arg_u] res_R
- | _ => raise NUT ("Nitpick_Kodkod.to_apply", [func_u])
+ (rel_expr_from_rel_expr kk res_R (Atom (1, j0)) (to_r func_u))
+ | Atom (k, _) =>
+ let
+ val dom_card = card_of_rep (rep_of arg_u)
+ val ran_R = Atom (exact_root dom_card k,
+ offset_of_type ofs (range_type (type_of func_u)))
+ in
+ to_apply_vect dom_card ran_R res_R (to_vect dom_card ran_R func_u)
+ arg_u
+ end
+ | Vect (1, R') =>
+ to_guard [arg_u] res_R
+ (rel_expr_from_rel_expr kk res_R R' (to_r func_u))
+ | Vect (k, R') => to_apply_vect k R' res_R (to_r func_u) arg_u
+ | Func (R, Formula Neut) =>
+ to_guard [arg_u] res_R (rel_expr_from_formula kk res_R
+ (kk_subset (to_opt R arg_u) (to_r func_u)))
+ | Func (Unit, R2) =>
+ to_guard [arg_u] res_R
+ (rel_expr_from_rel_expr kk res_R R2 (to_r func_u))
+ | Func (R1, R2) =>
+ rel_expr_from_rel_expr kk res_R R2
+ (kk_n_fold_join kk true R1 R2 (to_opt R1 arg_u) (to_r func_u))
+ |> body_rep R2 = Formula Neut ? to_guard [arg_u] res_R
+ | _ => raise NUT ("Nitpick_Kodkod.to_apply", [func_u])
(* int -> rep -> rep -> KK.rel_expr -> nut *)
and to_apply_vect k R' res_R func_r arg_u =
let
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Apr 13 11:54:05 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Apr 13 14:08:58 2010 +0200
@@ -1130,8 +1130,8 @@
if is_boolean_type T then
bool_rep polar opt
else
- smart_range_rep ofs T1 (fn () => card_of_type card_assigns T)
- (unopt_rep R1)
+ lazy_range_rep ofs T1 (fn () => card_of_type card_assigns T)
+ (unopt_rep R1)
|> opt ? opt_rep ofs T
in s_op2 Apply T ran_R u1 u2 end
| Op2 (Lambda, T, _, u1, u2) =>
--- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Tue Apr 13 11:54:05 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Tue Apr 13 14:08:58 2010 +0200
@@ -34,7 +34,7 @@
val is_one_rep : rep -> bool
val is_lone_rep : rep -> bool
val dest_Func : rep -> rep * rep
- val smart_range_rep : int Typtab.table -> typ -> (unit -> int) -> rep -> rep
+ val lazy_range_rep : int Typtab.table -> typ -> (unit -> int) -> rep -> rep
val binder_reps : rep -> rep list
val body_rep : rep -> rep
val one_rep : int Typtab.table -> typ -> rep -> rep
@@ -153,16 +153,16 @@
fun dest_Func (Func z) = z
| dest_Func R = raise REP ("Nitpick_Rep.dest_Func", [R])
(* int Typtab.table -> typ -> (unit -> int) -> rep -> rep *)
-fun smart_range_rep _ _ _ Unit = Unit
- | smart_range_rep _ _ _ (Vect (_, R)) = R
- | smart_range_rep _ _ _ (Func (_, R2)) = R2
- | smart_range_rep ofs T ran_card (Opt R) =
- Opt (smart_range_rep ofs T ran_card R)
- | smart_range_rep ofs (Type (@{type_name fun}, [_, T2])) _ (Atom (1, _)) =
+fun lazy_range_rep _ _ _ Unit = Unit
+ | lazy_range_rep _ _ _ (Vect (_, R)) = R
+ | lazy_range_rep _ _ _ (Func (_, R2)) = R2
+ | lazy_range_rep ofs T ran_card (Opt R) =
+ Opt (lazy_range_rep ofs T ran_card R)
+ | lazy_range_rep ofs (Type (@{type_name fun}, [_, T2])) _ (Atom (1, _)) =
Atom (1, offset_of_type ofs T2)
- | smart_range_rep ofs (Type (@{type_name fun}, [_, T2])) ran_card (Atom _) =
+ | lazy_range_rep ofs (Type (@{type_name fun}, [_, T2])) ran_card (Atom _) =
Atom (ran_card (), offset_of_type ofs T2)
- | smart_range_rep _ _ _ R = raise REP ("Nitpick_Rep.smart_range_rep", [R])
+ | lazy_range_rep _ _ _ R = raise REP ("Nitpick_Rep.lazy_range_rep", [R])
(* rep -> rep list *)
fun binder_reps (Func (R1, R2)) = R1 :: binder_reps R2