author  wenzelm 
Sat, 15 Nov 2008 21:31:36 +0100  
changeset 28810  e915ab11fe52 
parent 27865  27a8ad9612a3 
child 28814  463c9e9111ae 
permissions  rwrr 
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

1 
(* Title: Pure/Thy/thm_deps.ML 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

2 
ID: $Id$ 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

3 
Author: Stefan Berghofer, TU Muenchen 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

4 

fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

5 
Visualize dependencies of theorems. 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

6 
*) 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

7 

fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

8 
signature THM_DEPS = 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

9 
sig 
26697  10 
val thm_deps: thm list > unit 
11 
val unused_thms: theory list * theory list > (string * thm) list 

7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

12 
end; 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

13 

26697  14 
structure ThmDeps: THM_DEPS = 
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

15 
struct 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

16 

26697  17 
(* thm_deps *) 
18 

28810  19 
fun add_dep ((name, _, _), PBody {thms = thms', ...}) = 
20 
name <> "" ? 

21 
Graph.new_node (name, ()) #> 

22 
fold (fn (_, ((name', _, _), _)) => name <> "" ? Graph.add_edge (name', name)) thms'; 

26697  23 

7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

24 
fun thm_deps thms = 
28810  25 
let 
26 
val graph = Proofterm.fold_body_thms add_dep (map Thm.proof_of thms) Graph.empty; 

27 
fun add_entry (name, (_, (preds, _))) = 

28 
let 

29 
val prefix = #1 (Library.split_last (NameSpace.explode name)); 

30 
val session = 

31 
(case prefix of 

32 
a :: _ => 

33 
(case ThyInfo.lookup_theory a of 

34 
SOME thy => 

35 
(case Present.session_name thy of 

36 
"" => [] 

37 
 session => [session]) 

38 
 NONE => []) 

39 
 _ => ["global"]); 

40 
val entry = 

41 
{name = Sign.base_name name, 

42 
ID = name, 

43 
dir = space_implode "/" (session @ prefix), 

44 
unfold = false, 

45 
path = "", 

46 
parents = preds}; 

47 
in cons entry end; 

48 
in Present.display_graph (sort_wrt #ID (Graph.fold add_entry graph [])) end; 

26697  49 

50 

51 
(* unused_thms *) 

52 

53 
fun unused_thms (base_thys, thys) = 

26185  54 
let 
26697  55 
fun add_fact (name, ths) = 
56 
if exists (fn thy => PureThy.defined_fact thy name) base_thys then I 

57 
else fold_rev (fn th => (case Thm.get_name th of "" => I  a => cons (a, th))) ths; 

26699  58 
val thms = 
59 
fold (Facts.fold_static add_fact o PureThy.facts_of) thys [] 

60 
> sort_distinct (string_ord o pairself #1); 

28810  61 

62 
val tab = Proofterm.fold_body_thms 

63 
(fn ((name, prop, _), _) => name <> "" ? Symtab.insert_list (op =) (name, prop)) 

26697  64 
(map (Proofterm.strip_thm o Thm.proof_of o snd) thms) Symtab.empty; 
28810  65 
fun is_unused (name, th) = 
66 
not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th)); 

67 

26185  68 
(* groups containing at least one used theorem *) 
69 
val grps = fold (fn p as (_, thm) => if is_unused p then I else 

27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
26699
diff
changeset

70 
case Thm.get_group thm of 
26185  71 
NONE => I  SOME grp => Symtab.update (grp, ())) thms Symtab.empty; 
72 
val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') => 

27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
26699
diff
changeset

73 
if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm) 
26185  74 
andalso is_unused p 
75 
then 

27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
26699
diff
changeset

76 
(case Thm.get_group thm of 
26185  77 
NONE => (p :: thms, grps') 
78 
 SOME grp => 

79 
(* do not output theorem if another theorem in group has been used *) 

26697  80 
if Symtab.defined grps grp then q 
26185  81 
(* output at most one unused theorem per group *) 
26697  82 
else if Symtab.defined grps' grp then q 
26185  83 
else (p :: thms, Symtab.update (grp, ()) grps')) 
84 
else q) thms ([], Symtab.empty) 

85 
in rev thms' end; 

86 

7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

87 
end; 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

88 