69 fun thm_deps thms = |
70 fun thm_deps thms = |
70 Present.display_graph |
71 Present.display_graph |
71 (map snd (sort_wrt fst (Symtab.dest (fst |
72 (map snd (sort_wrt fst (Symtab.dest (fst |
72 (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, [])))))); |
73 (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, [])))))); |
73 |
74 |
|
75 fun unused_thms (opt_thys1, thys2) = |
|
76 let |
|
77 val thys = case opt_thys1 of |
|
78 NONE => thys2 |
|
79 | SOME thys1 => |
|
80 thys2 |> |
|
81 fold (curry (gen_union Theory.eq_thy)) (map Context.ancestors_of thys2) |> |
|
82 fold (subtract Theory.eq_thy) (thys1 :: map Context.ancestors_of thys1); |
|
83 val thms = maps PureThy.thms_of thys; |
|
84 val tab = fold Proofterm.thms_of_proof |
|
85 (map (Proofterm.strip_thm o proof_of o snd) thms) Symtab.empty; |
|
86 fun is_unused (s, thm) = case Symtab.lookup tab s of |
|
87 NONE => true |
|
88 | SOME ps => not (prop_of thm mem map fst ps); |
|
89 (* groups containing at least one used theorem *) |
|
90 val grps = fold (fn p as (_, thm) => if is_unused p then I else |
|
91 case PureThy.get_group thm of |
|
92 NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty; |
|
93 val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') => |
|
94 if PureThy.get_kind thm mem [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] |
|
95 andalso is_unused p |
|
96 then |
|
97 (case PureThy.get_group thm of |
|
98 NONE => (p :: thms, grps') |
|
99 | SOME grp => |
|
100 (* do not output theorem if another theorem in group has been used *) |
|
101 if is_some (Symtab.lookup grps grp) then q |
|
102 (* output at most one unused theorem per group *) |
|
103 else if is_some (Symtab.lookup grps' grp) then q |
|
104 else (p :: thms, Symtab.update (grp, ()) grps')) |
|
105 else q) thms ([], Symtab.empty) |
|
106 in rev thms' end; |
|
107 |
74 end; |
108 end; |
75 |
109 |
76 structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps; |
110 structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps; |
77 open BasicThmDeps; |
111 open BasicThmDeps; |