src/Pure/Thy/thm_deps.ML
changeset 26185 e53165319347
parent 26138 dc578de1d3e9
child 26697 3b9eede40608
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Thu Feb 28 17:33:35 2008 +0100
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Thu Feb 28 17:34:15 2008 +0100
     1.3 @@ -15,6 +15,7 @@
     1.4    include BASIC_THM_DEPS
     1.5    val enable : unit -> unit
     1.6    val disable : unit -> unit
     1.7 +  val unused_thms : theory list option * theory list -> (string * thm) list
     1.8  end;
     1.9  
    1.10  structure ThmDeps : THM_DEPS =
    1.11 @@ -71,6 +72,39 @@
    1.12      (map snd (sort_wrt fst (Symtab.dest (fst
    1.13        (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, []))))));
    1.14  
    1.15 +fun unused_thms (opt_thys1, thys2) =
    1.16 +  let
    1.17 +    val thys = case opt_thys1 of
    1.18 +        NONE => thys2
    1.19 +      | SOME thys1 =>
    1.20 +          thys2 |>
    1.21 +          fold (curry (gen_union Theory.eq_thy)) (map Context.ancestors_of thys2) |>
    1.22 +          fold (subtract Theory.eq_thy) (thys1 :: map Context.ancestors_of thys1);
    1.23 +    val thms = maps PureThy.thms_of thys;
    1.24 +    val tab = fold Proofterm.thms_of_proof
    1.25 +      (map (Proofterm.strip_thm o proof_of o snd) thms) Symtab.empty;
    1.26 +    fun is_unused (s, thm) = case Symtab.lookup tab s of
    1.27 +        NONE => true
    1.28 +      | SOME ps => not (prop_of thm mem map fst ps);
    1.29 +    (* groups containing at least one used theorem *)
    1.30 +    val grps = fold (fn p as (_, thm) => if is_unused p then I else
    1.31 +      case PureThy.get_group thm of
    1.32 +        NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty;
    1.33 +    val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') =>
    1.34 +      if PureThy.get_kind thm mem [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK]
    1.35 +        andalso is_unused p
    1.36 +      then
    1.37 +        (case PureThy.get_group thm of
    1.38 +           NONE => (p :: thms, grps')
    1.39 +         | SOME grp =>
    1.40 +             (* do not output theorem if another theorem in group has been used *)
    1.41 +             if is_some (Symtab.lookup grps grp) then q
    1.42 +             (* output at most one unused theorem per group *)
    1.43 +             else if is_some (Symtab.lookup grps' grp) then q
    1.44 +             else (p :: thms, Symtab.update (grp, ()) grps'))
    1.45 +      else q) thms ([], Symtab.empty)
    1.46 +  in rev thms' end;
    1.47 +
    1.48  end;
    1.49  
    1.50  structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps;