# HG changeset patch # User blanchet # Date 1271160538 -7200 # Node ID 186fcdb8d00fb2d2476b10e5061dda937ed71961 # Parent 890e60829e59e7713aced0ef94426806bb7e58cc# Parent a3d8d5329438e45c2bbe7602ea776f9d3aebcf4d merged diff -r 890e60829e59 -r 186fcdb8d00f doc-src/Nitpick/nitpick.tex --- 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. diff -r 890e60829e59 -r 186fcdb8d00f src/HOL/Tools/Nitpick/nitpick.ML --- 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 diff -r 890e60829e59 -r 186fcdb8d00f src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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)). diff -r 890e60829e59 -r 186fcdb8d00f src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- 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 diff -r 890e60829e59 -r 186fcdb8d00f src/HOL/Tools/Nitpick/nitpick_nut.ML --- 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) => diff -r 890e60829e59 -r 186fcdb8d00f src/HOL/Tools/Nitpick/nitpick_rep.ML --- 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