Take occuring constants into account
authorJoachim Breitner <mail@joachim-breitner.de>
Fri, 19 Dec 2014 11:55:58 +0000 (12:55 +0100)
committerJoachim Breitner <mail@joachim-breitner.de>
Fri, 19 Dec 2014 11:55:58 +0000 (12:55 +0100)
README.md
Where_To_Move.thy
where_to_move.ML

index 3c21227..722bb42 100644 (file)
--- a/README.md
+++ b/README.md
@@ -114,8 +114,8 @@ Usage
    moved.
 
    The logic is as follows: In the list of dependencies of the current theory,
-   find the first (i.e. most primitive) theory that contains all theories of
-   all lemmas used by the theorem in question.
+   find the first (i.e. most primitive) theory that already contains all
+   constants occurring in the theorem, and all lemmas occurring in its proof.
 
  * `where_to_move` *thm*
 
@@ -126,6 +126,10 @@ Usage
    Prints all theorems used by the given theorems. Can be useful to understand
    why `where_to_move` suggests a particular choice.
 
+ * `constants_used_by` *thm*
+
+   Prints all constants occuring in a given theorem.
+
 
 Bugs and shortcomings
 ---------------------
@@ -135,9 +139,6 @@ These are the ones that I know about. If you have more, feel free to open an iss
  * In the output of `theorems_used_by`, if a theorem is actually a list of
    them, and one is used, it prints the selector as part of the name
    (`HOL.simp_thms_7`), which breaks the hyperlinking.
- * Definitions should be treated specially. Naturally, most `foo_def` lemmas can be moved to
-   `HOL` (they are (derived from) axioms, after all), but I usually do not want to
-   move definitions.
  * Using `where_to_move OtherTheory.bar` will print `Theorem OtherTheory.bar
    could be moved to theory "OtherTheory"`, which is not wrong, but slighly
    unhelpful.
index 4a2f0c2..37a98eb 100644 (file)
@@ -1,6 +1,7 @@
 theory Where_To_Move
 imports Pure
 keywords "theorems_used_by" :: diag
+     and "constants_used_by" :: diag
      and "where_to_move" :: diag
 begin
 
index 7c67b2c..e1539e0 100644 (file)
@@ -7,9 +7,11 @@ Utility commands to suggest lemma reorganisations.
 signature WHERE_TO_MOVE =
 sig
   val thms_used_by_thm : thm -> string list
+  val constants_used_by_thm : thm -> string list
   val theories_used_by_thm : theory -> thm -> theory list
   val theories_used_by_thms : theory -> thm list -> theory list
 
+  val constants_used_by_cmd : (string * Position.T) -> Toplevel.transition -> Toplevel.transition
   val theorems_used_by_cmd : (string * Position.T) -> Toplevel.transition -> Toplevel.transition
   val where_to_move_cmd : (string * Position.T) list option -> Toplevel.transition -> Toplevel.transition
 end
@@ -25,19 +27,23 @@ fun thms_used_by_thm thm =
   in thm |> Thm.proof_body_of |> Proofterm.strip_thm |> used_by_proof_body
   end;
 
+fun constants_used_by_thm thm =
+  let val term = Thm.prop_of thm
+      val consts = Term.add_const_names term []
+  in consts
+  end;
+
 fun nub ss = fold (fn x => Symtab.update (x, ())) ss Symtab.empty |> Symtab.keys;
 
-fun theories_used_by_thm thy thm =
-      thm |> thms_used_by_thm 
-          |> map (hd o Long_Name.explode) 
-          |> nub 
-          |> map (Context.this_theory thy);
+fun theories_used_by_thms thy thm =
+  let val thms = maps thms_used_by_thm thm
+      val consts = maps constants_used_by_thm thm
+      val theory_names = thms @ consts |> map (hd o Long_Name.explode) |> nub
+      val theories = theory_names |> map (Context.this_theory thy) 
+  in theories
+  end
 
-fun theories_used_by_thms thy thms =
-      thms |> maps thms_used_by_thm
-           |> map (hd o Long_Name.explode) 
-           |> nub 
-           |> map (Context.this_theory thy);
+fun theories_used_by_thm thy thm = theories_used_by_thms thy [thm]
 
 
 fun ok_for thys thy =
@@ -64,12 +70,34 @@ fun theorems_used_by_cmd arg = Toplevel.keep (fn state =>
     );
 
 
+fun pretty_const ctxt c =
+  let
+    val const_space = Consts.space_of (Sign.consts_of (Proof_Context.theory_of ctxt));
+    val markup = Name_Space.markup const_space c;
+  in
+    Pretty.mark markup (Pretty.str c)
+  end;
+
+fun constants_used_by_cmd arg = Toplevel.keep (fn state =>
+    let val ctxt = Toplevel.context_of state
+        val thy = Toplevel.theory_of state
+        val (_, thms) =  Facts.retrieve (Context.Proof ctxt) (Global_Theory.facts_of thy) arg
+    in thms |> maps constants_used_by_thm
+            |> map (pretty_const ctxt)
+            |> Pretty.commas
+            |> Pretty.paragraph
+            |> Pretty.writeln
+    end
+    );
+
+
 fun facts_of_theory thy =
   let val prev_thys = (Theory.parents_of thy) 
       val facts = Global_Theory.facts_of thy
       val thms =  Facts.dest_static false (map Global_Theory.facts_of prev_thys) facts
   in thms end;
 
+
 fun where_to_move_cmd args_o =
   Toplevel.keep ( fn state =>
     let val ctxt = Toplevel.context_of state
@@ -101,6 +129,10 @@ val _ = Outer_Syntax.improper_command @{command_spec "theorems_used_by"}
     "prints all theorems used by the given theorem"
     (Parse.position Parse.xname >> theorems_used_by_cmd);
 
+val _ = Outer_Syntax.improper_command @{command_spec "constants_used_by"} 
+    "prints all constants occurring in the given theorem"
+    (Parse.position Parse.xname >> constants_used_by_cmd);
+
 val _ = Outer_Syntax.improper_command @{command_spec "where_to_move"}
     "suggests a new location for the given theorem or, of none is given, all theorems in the current theory"
     (Scan.option (Scan.repeat1 (Parse.position Parse.xname)) >> where_to_move_cmd);