src/HOL/Tools/Quickcheck/find_unused_assms.ML
changeset 70117 5ae2f266885f
parent 70116 3d580b5c4aee
     1.1 --- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Thu Apr 11 12:05:36 2019 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Thu Apr 11 12:18:03 2019 +0200
     1.3 @@ -6,8 +6,9 @@
     1.4  
     1.5  signature FIND_UNUSED_ASSMS =
     1.6  sig
     1.7 -  val find_unused_assms : Proof.context -> string -> (string * int list list option) list
     1.8 -  val print_unused_assms : Proof.context -> string option -> unit
     1.9 +  val check_unused_assms: Proof.context -> string * thm -> string * int list list option
    1.10 +  val find_unused_assms: Proof.context -> string -> (string * int list list option) list
    1.11 +  val print_unused_assms: Proof.context -> string option -> unit
    1.12  end
    1.13  
    1.14  structure Find_Unused_Assms : FIND_UNUSED_ASSMS =
    1.15 @@ -33,16 +34,12 @@
    1.16  
    1.17  (* main functionality *)
    1.18  
    1.19 -fun find_unused_assms ctxt thy_name =
    1.20 +fun check_unused_assms ctxt =
    1.21    let
    1.22      val thy = Proof_Context.theory_of ctxt
    1.23      val ctxt' = ctxt
    1.24         |> Config.put Quickcheck.abort_potential true
    1.25         |> Config.put Quickcheck.quiet true
    1.26 -    val all_thms =
    1.27 -      thms_of thy thy_name
    1.28 -      |> filter (fn (s, _) => length (Long_Name.explode s) = 2)  (* FIXME !? *)
    1.29 -      |> sort_by #1
    1.30      fun check_single conjecture =
    1.31        (case try (Quickcheck.test_terms ctxt' (true, true) []) [(conjecture, [])] of
    1.32          SOME (SOME _) => false
    1.33 @@ -54,9 +51,9 @@
    1.34            (fn x =>
    1.35              if member (op =) S x then I
    1.36              else insert (eq_set (op =)) (insert (op =) x S)) X) Ss []
    1.37 -    fun check (s, th) =
    1.38 +    fun check (name, th) =
    1.39        (case Logic.strip_horn (Thm.prop_of (Thm.unvarify_global thy th)) of
    1.40 -        ([], _) => (s, NONE)
    1.41 +        ([], _) => (name, NONE)
    1.42        | (ts, t) =>
    1.43            let
    1.44              fun mk_conjecture is = Logic.list_implies (drop_indexes is ts, t)
    1.45 @@ -66,12 +63,18 @@
    1.46                  (fn I => filter (check_single o mk_conjecture) (build singles I))
    1.47                  (map single singles) [(map single singles)]
    1.48              val maximals = flat (find_max_subsets multiples)
    1.49 -          in
    1.50 -            (s, SOME maximals)
    1.51 -          end)
    1.52 -  in
    1.53 -    rev (Par_List.map check all_thms)
    1.54 -  end
    1.55 +          in (name, SOME maximals) end)
    1.56 +  in check end
    1.57 +
    1.58 +fun find_unused_assms ctxt thy_name =
    1.59 +  let
    1.60 +    val thy = Proof_Context.theory_of ctxt
    1.61 +    val all_thms =
    1.62 +      thms_of thy thy_name
    1.63 +      |> filter (fn (name, _) => length (Long_Name.explode name) = 2)  (* FIXME !? *)
    1.64 +      |> sort_by #1
    1.65 +    val check = check_unused_assms ctxt
    1.66 +  in rev (Par_List.map check all_thms) end
    1.67  
    1.68  
    1.69  (* printing results *)
    1.70 @@ -83,9 +86,9 @@
    1.71      (flat (separate [Pretty.str " and", Pretty.brk 1]
    1.72        (map (fn i => [Pretty.str (string_of_int (i + 1))]) (sort int_ord is))))
    1.73  
    1.74 -fun pretty_thm (s, set_of_indexes) =
    1.75 -  Pretty.block (Pretty.str s :: Pretty.str ":" :: Pretty.brk 1 ::
    1.76 -    Pretty.str "unnecessary assumption(s) " ::
    1.77 +fun pretty_thm (name, set_of_indexes) =
    1.78 +  Pretty.block (Pretty.str name :: Pretty.str ":" :: Pretty.brk 1 ::
    1.79 +    Pretty.str "unnecessary assumption " ::
    1.80      separate (Pretty.str " or ") (map pretty_indexes set_of_indexes))
    1.81  
    1.82  in
    1.83 @@ -97,7 +100,8 @@
    1.84      val total = length results
    1.85      val with_assumptions = length (filter (is_some o snd) results)
    1.86      val with_superfluous_assumptions =
    1.87 -      map_filter (fn (_, NONE) => NONE | (_, SOME []) => NONE | (s, SOME r) => SOME (s, r)) results
    1.88 +      results |> map_filter
    1.89 +        (fn (_, NONE) => NONE | (_, SOME []) => NONE | (name, SOME r) => SOME (name, r))
    1.90  
    1.91      val msg =
    1.92        "Found " ^ string_of_int (length with_superfluous_assumptions) ^