46 |
46 |
47 (* unused_thms *) |
47 (* unused_thms *) |
48 |
48 |
49 fun unused_thms (base_thys, thys) = |
49 fun unused_thms (base_thys, thys) = |
50 let |
50 let |
51 fun add_fact (name, ths) = |
51 fun add_fact space (name, ths) = |
52 if exists (fn thy => PureThy.defined_fact thy name) base_thys then I |
52 if exists (fn thy => PureThy.defined_fact thy name) base_thys then I |
53 else fold_rev (fn th => (case Thm.get_name th of "" => I | a => cons (a, th))) ths; |
53 else |
|
54 let val {concealed, group, ...} = Name_Space.the_entry space name in |
|
55 fold_rev (fn th => |
|
56 (case Thm.get_name th of |
|
57 "" => I |
|
58 | a => cons (a, (th, concealed, group)))) ths |
|
59 end; |
|
60 fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts; |
|
61 |
54 val thms = |
62 val thms = |
55 fold (Facts.fold_static add_fact o PureThy.facts_of) thys [] |
63 fold (add_facts o PureThy.facts_of) thys [] |
56 |> sort_distinct (string_ord o pairself #1); |
64 |> sort_distinct (string_ord o pairself #1); |
57 |
65 |
58 val tab = |
66 val tab = |
59 Proofterm.fold_body_thms |
67 Proofterm.fold_body_thms |
60 (fn (name, prop, _) => name <> "" ? Symtab.insert_list (op =) (name, prop)) |
68 (fn (a, prop, _) => a <> "" ? Symtab.insert_list (op =) (a, prop)) |
61 (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty; |
69 (map (Proofterm.strip_thm o Thm.proof_body_of o #1 o #2) thms) Symtab.empty; |
62 fun is_unused (name, th) = |
70 |
63 not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th)); |
71 fun is_unused (a, th) = |
|
72 not (member (op aconv) (Symtab.lookup_list tab a) (Thm.prop_of th)); |
64 |
73 |
65 (* groups containing at least one used theorem *) |
74 (* groups containing at least one used theorem *) |
66 val grps = fold (fn p as (_, thm) => if is_unused p then I else |
75 val used_groups = fold (fn (a, (th, _, group)) => |
67 case Thm.get_group thm of |
76 if is_unused (a, th) then I |
68 NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty; |
77 else |
69 val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') => |
78 (case group of |
70 if member (op =) [Thm.theoremK, Thm.generatedK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm) |
79 NONE => I |
71 andalso is_unused p |
80 | SOME grp => Inttab.update (grp, ()))) thms Inttab.empty; |
|
81 val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, grps') => |
|
82 if member (op =) [Thm.theoremK, Thm.generatedK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] |
|
83 (Thm.get_kind th) andalso not concealed andalso is_unused (a, th) |
72 then |
84 then |
73 (case Thm.get_group thm of |
85 (case group of |
74 NONE => (p :: thms, grps') |
86 NONE => ((a, th) :: thms, grps') |
75 | SOME grp => |
87 | SOME grp => |
76 (* do not output theorem if another theorem in group has been used *) |
88 (* do not output theorem if another theorem in group has been used *) |
77 if Symtab.defined grps grp then q |
89 if Inttab.defined used_groups grp then q |
78 (* output at most one unused theorem per group *) |
90 (* output at most one unused theorem per group *) |
79 else if Symtab.defined grps' grp then q |
91 else if Inttab.defined grps' grp then q |
80 else (p :: thms, Symtab.update (grp, ()) grps')) |
92 else ((a, th) :: thms, Inttab.update (grp, ()) grps')) |
81 else q) thms ([], Symtab.empty) |
93 else q) thms ([], Inttab.empty) |
82 in rev thms' end; |
94 in rev thms' end; |
83 |
95 |
84 end; |
96 end; |
85 |
97 |