src/HOL/Tools/Quickcheck/find_unused_assms.ML
author wenzelm
Mon Mar 31 12:35:39 2014 +0200 (2014-03-31 ago)
changeset 56334 6b3739fee456
parent 56161 300f613060b0
child 58893 9e0ecb66d6a7
permissions -rw-r--r--
some shortcuts for chunks, which sometimes avoid bulky string output;
     1 (*  Title:      HOL/Tools/Quickcheck/find_unused_assms.ML
     2     Author:     Lukas Bulwahn, TU Muenchen
     3 
     4 Finding unused assumptions in lemmas (using Quickcheck).
     5 *)
     6 
     7 signature FIND_UNUSED_ASSMS =
     8 sig
     9   val find_unused_assms : Proof.context -> string -> (string * int list list option) list
    10   val print_unused_assms : Proof.context -> string option -> unit
    11 end
    12 
    13 structure Find_Unused_Assms : FIND_UNUSED_ASSMS =
    14 struct
    15 
    16 fun thms_of thy thy_name = Global_Theory.all_thms_of thy false
    17   |> filter (fn (_, th) => Context.theory_name (theory_of_thm th) = thy_name)
    18 
    19 fun do_while P f s list =
    20   if P s then
    21     let val s' = f s
    22     in do_while P f s' (cons s' list) end
    23   else list
    24 
    25 fun drop_indexes is xs =
    26   fold_index (fn (i, x) => if member (op =) is i then I else cons x) xs []
    27 
    28 fun find_max_subsets [] = []
    29   | find_max_subsets (ss :: sss) = ss ::
    30       (find_max_subsets (map (filter_out (fn s => exists (fn s' => subset (op =) (s, s')) ss)) sss))
    31 
    32 
    33 (* main functionality *)
    34 
    35 fun find_unused_assms ctxt thy_name =
    36   let
    37     val ctxt' = ctxt
    38        |> Config.put Quickcheck.abort_potential true
    39        |> Config.put Quickcheck.quiet true
    40     val all_thms =
    41       filter (fn (s, _) => length (Long_Name.explode s) = 2)  (* FIXME !? *)
    42         (thms_of (Proof_Context.theory_of ctxt) thy_name)
    43     fun check_single conjecture =
    44       (case try (Quickcheck.test_terms ctxt' (true, true) []) [(conjecture, [])] of
    45         SOME (SOME _) => false
    46       | SOME NONE => true
    47       | NONE => false)
    48     fun build X Ss =
    49       fold
    50         (fn S => fold
    51           (fn x =>
    52             if member (op =) S x then I
    53             else insert (eq_set (op =)) (insert (op =) x S)) X) Ss []
    54     fun check (s, th) =
    55       (case Logic.strip_horn (prop_of (Thm.unvarify_global th)) of
    56         ([], _) => (s, NONE)
    57       | (ts, t) =>
    58           let
    59             fun mk_conjecture is = Logic.list_implies (drop_indexes is ts, t)
    60             val singles = filter (check_single o mk_conjecture o single) (0 upto (length ts - 1))
    61             val multiples =
    62               do_while (not o null)
    63                 (fn I => filter (check_single o mk_conjecture) (build singles I))
    64                 (map single singles) [(map single singles)]
    65             val maximals = flat (find_max_subsets multiples)
    66           in
    67             (s, SOME maximals)
    68           end)
    69   in
    70     rev (Par_List.map check all_thms)
    71   end
    72 
    73 
    74 (* printing results *)
    75 
    76 local
    77 
    78 fun pretty_indexes is =
    79   Pretty.block
    80     (flat (separate [Pretty.str " and", Pretty.brk 1]
    81       (map (fn i => [Pretty.str (string_of_int (i + 1))]) (sort int_ord is))))
    82 
    83 fun pretty_thm (s, set_of_indexes) =
    84   Pretty.block (Pretty.str s :: Pretty.str ":" :: Pretty.brk 1 ::
    85     Pretty.str "unnecessary assumption(s) " ::
    86     separate (Pretty.str " or ") (map pretty_indexes set_of_indexes))
    87 
    88 in
    89 
    90 fun print_unused_assms ctxt opt_thy_name =
    91   let
    92     val thy_name = the_default (Context.theory_name (Proof_Context.theory_of ctxt)) opt_thy_name
    93     val results = find_unused_assms ctxt thy_name
    94     val total = length results
    95     val with_assumptions = length (filter (is_some o snd) results)
    96     val with_superfluous_assumptions =
    97       map_filter (fn (_, NONE) => NONE | (_, SOME []) => NONE | (s, SOME r) => SOME (s, r)) results
    98 
    99     val msg =
   100       "Found " ^ string_of_int (length with_superfluous_assumptions) ^
   101       " theorems with (potentially) superfluous assumptions"
   102     val end_msg =
   103       "Checked " ^ string_of_int with_assumptions ^ " theorems with assumptions (" ^
   104       string_of_int total ^ " total) in the theory " ^ quote thy_name
   105   in
   106     [Pretty.str (msg ^ ":"), Pretty.str ""] @
   107     map pretty_thm with_superfluous_assumptions @
   108     [Pretty.str "", Pretty.str end_msg]
   109   end |> Pretty.writeln_chunks
   110 
   111 end
   112 
   113 val _ =
   114   Outer_Syntax.improper_command @{command_spec "find_unused_assms"}
   115     "find theorems with (potentially) superfluous assumptions"
   116     (Scan.option Parse.name >> (fn name =>
   117       Toplevel.keep (fn state => print_unused_assms (Toplevel.context_of state) name)))
   118 
   119 end