equal
deleted
inserted
replaced
33 |
33 |
34 (* main functionality *) |
34 (* main functionality *) |
35 |
35 |
36 fun find_unused_assms ctxt thy_name = |
36 fun find_unused_assms ctxt thy_name = |
37 let |
37 let |
|
38 val thy = Proof_Context.theory_of ctxt |
38 val ctxt' = ctxt |
39 val ctxt' = ctxt |
39 |> Config.put Quickcheck.abort_potential true |
40 |> Config.put Quickcheck.abort_potential true |
40 |> Config.put Quickcheck.quiet true |
41 |> Config.put Quickcheck.quiet true |
41 val all_thms = |
42 val all_thms = |
42 filter (fn (s, _) => length (Long_Name.explode s) = 2) (* FIXME !? *) |
43 filter (fn (s, _) => length (Long_Name.explode s) = 2) (* FIXME !? *) |
43 (thms_of (Proof_Context.theory_of ctxt) thy_name) |
44 (thms_of thy thy_name) |
44 fun check_single conjecture = |
45 fun check_single conjecture = |
45 (case try (Quickcheck.test_terms ctxt' (true, true) []) [(conjecture, [])] of |
46 (case try (Quickcheck.test_terms ctxt' (true, true) []) [(conjecture, [])] of |
46 SOME (SOME _) => false |
47 SOME (SOME _) => false |
47 | SOME NONE => true |
48 | SOME NONE => true |
48 | NONE => false) |
49 | NONE => false) |
51 (fn S => fold |
52 (fn S => fold |
52 (fn x => |
53 (fn x => |
53 if member (op =) S x then I |
54 if member (op =) S x then I |
54 else insert (eq_set (op =)) (insert (op =) x S)) X) Ss [] |
55 else insert (eq_set (op =)) (insert (op =) x S)) X) Ss [] |
55 fun check (s, th) = |
56 fun check (s, th) = |
56 (case Logic.strip_horn (Thm.prop_of (Thm.unvarify_global th)) of |
57 (case Logic.strip_horn (Thm.prop_of (Thm.unvarify_global thy th)) of |
57 ([], _) => (s, NONE) |
58 ([], _) => (s, NONE) |
58 | (ts, t) => |
59 | (ts, t) => |
59 let |
60 let |
60 fun mk_conjecture is = Logic.list_implies (drop_indexes is ts, t) |
61 fun mk_conjecture is = Logic.list_implies (drop_indexes is ts, t) |
61 val singles = filter (check_single o mk_conjecture o single) (0 upto (length ts - 1)) |
62 val singles = filter (check_single o mk_conjecture o single) (0 upto (length ts - 1)) |