src/HOL/Tools/Nitpick/nitpick.ML
changeset 55888 cac1add157e8
parent 55539 0819931d652d
child 55889 6bfbec3dff62
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Mar 03 16:44:46 2014 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Mar 03 22:33:22 2014 +0100
     1.3 @@ -21,7 +21,6 @@
     1.4       boxes: (typ option * bool option) list,
     1.5       finitizes: (typ option * bool option) list,
     1.6       monos: (typ option * bool option) list,
     1.7 -     stds: (typ option * bool) list,
     1.8       wfs: (styp option * bool option) list,
     1.9       sat_solver: string,
    1.10       blocking: bool,
    1.11 @@ -107,7 +106,6 @@
    1.12     boxes: (typ option * bool option) list,
    1.13     finitizes: (typ option * bool option) list,
    1.14     monos: (typ option * bool option) list,
    1.15 -   stds: (typ option * bool) list,
    1.16     wfs: (styp option * bool option) list,
    1.17     sat_solver: string,
    1.18     blocking: bool,
    1.19 @@ -227,8 +225,8 @@
    1.20              error "You must import the theory \"Nitpick\" to use Nitpick"
    1.21  *)
    1.22      val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
    1.23 -         boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
    1.24 -         verbose, overlord, spy, user_axioms, assms, whacks, merge_type_vars,
    1.25 +         boxes, finitizes, monos, wfs, sat_solver, falsify, debug, verbose,
    1.26 +         overlord, spy, user_axioms, assms, whacks, merge_type_vars,
    1.27           binary_ints, destroy_constrs, specialize, star_linear_preds,
    1.28           total_consts, needs, peephole_optim, datatype_sym_break,
    1.29           kodkod_sym_break, tac_timeout, max_threads, show_datatypes,
    1.30 @@ -291,7 +289,7 @@
    1.31      val original_max_potential = max_potential
    1.32      val original_max_genuine = max_genuine
    1.33      val max_bisim_depth = fold Integer.max bisim_depths ~1
    1.34 -    val case_names = case_const_names ctxt stds
    1.35 +    val case_names = case_const_names ctxt
    1.36      val defs = def_assm_ts @ all_defs_of thy subst
    1.37      val nondefs = all_nondefs_of ctxt subst
    1.38      val def_tables = const_def_tables ctxt subst defs
    1.39 @@ -306,12 +304,11 @@
    1.40      val ersatz_table = ersatz_table ctxt
    1.41      val hol_ctxt as {wf_cache, ...} =
    1.42        {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
    1.43 -       stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
    1.44 -       whacks = whacks, binary_ints = binary_ints,
    1.45 -       destroy_constrs = destroy_constrs, specialize = specialize,
    1.46 -       star_linear_preds = star_linear_preds, total_consts = total_consts,
    1.47 -       needs = needs, tac_timeout = tac_timeout, evals = evals,
    1.48 -       case_names = case_names, def_tables = def_tables,
    1.49 +       wfs = wfs, user_axioms = user_axioms, debug = debug, whacks = whacks,
    1.50 +       binary_ints = binary_ints, destroy_constrs = destroy_constrs,
    1.51 +       specialize = specialize, star_linear_preds = star_linear_preds,
    1.52 +       total_consts = total_consts, needs = needs, tac_timeout = tac_timeout,
    1.53 +       evals = evals, case_names = case_names, def_tables = def_tables,
    1.54         nondef_table = nondef_table, nondefs = nondefs, simp_table = simp_table,
    1.55         psimp_table = psimp_table, choice_spec_table = choice_spec_table,
    1.56         intro_table = intro_table, ground_thm_table = ground_thm_table,
    1.57 @@ -359,7 +356,6 @@
    1.58      val (sel_names, nonsel_names) =
    1.59        List.partition (is_sel o nickname_of) const_names
    1.60      val sound_finitizes = none_true finitizes
    1.61 -    val standard = forall snd stds
    1.62  (*
    1.63      val _ =
    1.64        List.app (print_g o string_for_nut ctxt) (nondef_us @ def_us @ need_us)
    1.65 @@ -380,7 +376,7 @@
    1.66                   ". " ^ extra))
    1.67        end
    1.68      fun is_type_fundamentally_monotonic T =
    1.69 -      (is_datatype ctxt stds T andalso not (is_quot_type ctxt T) andalso
    1.70 +      (is_datatype ctxt T andalso not (is_quot_type ctxt T) andalso
    1.71         (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
    1.72        is_number_type ctxt T orelse is_bit_type T
    1.73      fun is_type_actually_monotonic T =
    1.74 @@ -406,8 +402,7 @@
    1.75            SOME (SOME b) => b
    1.76          | _ => is_type_kind_of_monotonic T
    1.77      fun is_datatype_deep T =
    1.78 -      not standard orelse T = @{typ unit} orelse T = nat_T orelse
    1.79 -      is_word_type T orelse
    1.80 +      T = @{typ unit} orelse T = nat_T orelse is_word_type T orelse
    1.81        exists (curry (op =) T o domain_type o type_of) sel_names
    1.82      val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
    1.83                   |> sort Term_Ord.typ_ord
    1.84 @@ -416,7 +411,7 @@
    1.85           exists (member (op =) [nat_T, int_T]) all_Ts then
    1.86          print_v (K "The option \"binary_ints\" will be ignored because of the \
    1.87                     \presence of rationals, reals, \"Suc\", \"gcd\", or \"lcm\" \
    1.88 -                   \in the problem or because of the \"non_std\" option.")
    1.89 +                   \in the problem.")
    1.90        else
    1.91          ()
    1.92      val _ =
    1.93 @@ -441,7 +436,7 @@
    1.94        else
    1.95          ()
    1.96      val (deep_dataTs, shallow_dataTs) =
    1.97 -      all_Ts |> filter (is_datatype ctxt stds)
    1.98 +      all_Ts |> filter (is_datatype ctxt)
    1.99               |> List.partition is_datatype_deep
   1.100      val finitizable_dataTs =
   1.101        (deep_dataTs |> filter_out (is_finite_type hol_ctxt)
   1.102 @@ -454,26 +449,6 @@
   1.103                           "Nitpick can use a more precise finite encoding."))
   1.104        else
   1.105          ()
   1.106 -    (* This detection code is an ugly hack. Fortunately, it is used only to
   1.107 -       provide a hint to the user. *)
   1.108 -    fun is_struct_induct_step (name, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
   1.109 -      not (null fixes) andalso
   1.110 -      exists (String.isSuffix ".hyps" o Name_Space.full_name Name_Space.default_naming o fst) assumes andalso
   1.111 -      exists (exists (curry (op =) name o shortest_name o fst)
   1.112 -              o datatype_constrs hol_ctxt) deep_dataTs
   1.113 -    val likely_in_struct_induct_step =
   1.114 -      exists is_struct_induct_step (Proof_Context.dest_cases ctxt)
   1.115 -    val _ = if standard andalso likely_in_struct_induct_step then
   1.116 -              pprint_nt (fn () => Pretty.blk (0,
   1.117 -                  pstrs "Hint: To check that the induction hypothesis is \
   1.118 -                        \general enough, try this command: " @
   1.119 -                  [Pretty.mark
   1.120 -                    (Active.make_markup Markup.sendbackN
   1.121 -                      {implicit = false, properties = [Markup.padding_command]})
   1.122 -                    (Pretty.blk (0,
   1.123 -                       pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
   1.124 -            else
   1.125 -              ()
   1.126  (*
   1.127      val _ = print_g "Monotonic types:"
   1.128      val _ = List.app (print_g o string_for_type ctxt) mono_Ts
   1.129 @@ -649,9 +624,7 @@
   1.130                    "scope.");
   1.131                NONE)
   1.132  
   1.133 -    val das_wort_model =
   1.134 -      (if falsify then "counterexample" else "model")
   1.135 -      |> not standard ? prefix "nonstandard "
   1.136 +    val das_wort_model = if falsify then "counterexample" else "model"
   1.137  
   1.138      val scopes = Unsynchronized.ref []
   1.139      val generated_scopes = Unsynchronized.ref []
   1.140 @@ -704,7 +677,7 @@
   1.141                Pretty.indent indent_size reconstructed_model]);
   1.142           print_t (K "% SZS output end FiniteModel");
   1.143           if genuine then
   1.144 -           (if check_genuine andalso standard then
   1.145 +           (if check_genuine then
   1.146                case prove_hol_model scope tac_timeout free_names sel_names
   1.147                                     rel_table bounds (assms_prop ()) of
   1.148                  SOME true =>
   1.149 @@ -722,13 +695,6 @@
   1.150                 | NONE => print "No confirmation by \"auto\"."
   1.151              else
   1.152                ();
   1.153 -            if not standard andalso likely_in_struct_induct_step then
   1.154 -              print "The existence of a nonstandard model suggests that the \
   1.155 -                    \induction hypothesis is not general enough or may even be \
   1.156 -                    \wrong. See the Nitpick manual's \"Inductive Properties\" \
   1.157 -                    \section for details (\"isabelle doc nitpick\")."
   1.158 -            else
   1.159 -              ();
   1.160              if has_lonely_bool_var orig_t then
   1.161                print "Hint: Maybe you forgot a colon after the lemma's name?"
   1.162              else if has_syntactic_sorts orig_t then
   1.163 @@ -1018,13 +984,8 @@
   1.164          else if max_genuine = original_max_genuine then
   1.165            if max_potential = original_max_potential then
   1.166              (print_t (K "% SZS status Unknown");
   1.167 -             print_nt (fn () =>
   1.168 -                 "Nitpick found no " ^ das_wort_model ^ "." ^
   1.169 -                 (if not standard andalso likely_in_struct_induct_step then
   1.170 -                    " This suggests that the induction hypothesis might be \
   1.171 -                    \general enough to prove this subgoal."
   1.172 -                  else
   1.173 -                    "")); if skipped > 0 then unknownN else noneN)
   1.174 +             print_nt (fn () => "Nitpick found no " ^ das_wort_model ^ ".");
   1.175 +             if skipped > 0 then unknownN else noneN)
   1.176            else
   1.177              (print_nt (fn () =>
   1.178                   excipit ("could not find a" ^