Be less verbose
[isa-where-to-move.git] / README.md
1 Where should I put this lemma?
2 ==============================
3
4 I usually work with many Isabelle theories, which form a DAG, and generally I
5 want auxillary lemmas to be proven as early as possible.
6
7 Disclaimer
8 ----------
9
10 This builds on infrastructure in Isabelle of which it is said that
11 [“None of this really works,
12 though.”](https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-December/msg00076.html).
13 Furthermore, I am not an experienced Isabelle programmer, so what I’m doing
14 might be wrong, inefficient and/or stupid. Use at your own risk (and/or submit
15 patches!).
16
17
18 Motivation
19 ----------
20
21 Consider these four files:
22
23     theory Where_To_Move_Ex1
24     imports Main
25     begin
26
27     definition "foo = True"
28
29     lemma fooI: foo unfolding foo_def..
30
31     end
32
33
34
35     theory Where_To_Move_Ex2
36     imports Main
37     begin
38
39     definition "bar = False"
40
41     lemma barE: "bar ==> P" unfolding bar_def by (erule FalseE)
42
43     end
44  
45
46     theory Where_To_Move_Ex3
47     imports Where_To_Move_Ex1 Where_To_Move_Ex2
48     begin
49     (* nothing here yet *)
50     end
51
52
53     theory Where_To_Move_Ex4
54     imports Where_To_Move_Ex3 WhereToMove 
55     begin
56
57     lemma fooI2: "foo" by (rule fooI)
58     lemma barE2: "bar \<Longrightarrow> P" by (rule barE)
59     lemma foobar: "foo \<and> \<not> bar"
60       apply rule
61       apply (rule fooI)
62       apply (rule notI)
63       apply (erule barE)
64       done
65     lemma foobar2: "foo \<and> \<not> bar"
66       apply rule
67       apply (rule fooI2)
68       apply (rule notI)
69       apply (erule barE2)
70       done
71
72     end
73
74 Seening this, my usual thoughts would be
75
76  * `fooI2` could just as well go to `Where_To_Move_Ex1` directly; it uses
77    nothing from the other theories.
78  * Similarly, `barE2` should go to `Where_To_Move_Ex2`.
79  * `foobar` cannot go to either `Where_To_Move_Ex1` nor `Where_To_Move_Ex2`. But it still
80    is not at a proper spot right now: The theory `Where_To_Move_Ex3` is more suitable.
81  * `foobar2` is, upon first glance, at the right spot, as it uses `fooI2` and
82    `barE2` from this module. *If* I would move `fooI2` and `barE2`, I would also be
83    able to move `foobar2`, but maybe I will not do that, so for now `foobar2`
84    stays where it is.
85
86 Example use
87 -----------
88
89 If I enter the command `where_to_move` at the end of the theory
90 `Where_To_Move_Ex4`, I will be given this somewhat helpful output:
91
92     Theorem barE2 could be moved to theory "Where_To_Move_Ex2". 
93     Theorem fooI2 could be moved to theory "Where_To_Move_Ex1". 
94     Theorem foobar could be moved to theory "Where_To_Move_Ex3". 
95
96 The output did not mention `foobar2`, but if I expliclty ask for it to be
97 checked using `where_to_move foobar2` I get
98
99     Theorem foobar2 is fine where it is.
100
101 Installation
102 ------------
103
104  * Clone this repository somewhere, say to `~/isabelle/isa-where-to-move`.
105  * Add `"$HOME/isabelle/isa-where-to-move/Where_To_Move"` to your import list
106  * Done
107
108 Usage
109 -----
110
111  * `where_to_move`
112  
113    For all lemmas defined in the current module, give an indication where it should be
114    moved.
115
116    The logic is as follows: In the list of dependencies of the current theory,
117    find the first (i.e. most primitive) theory that contains all theories of
118    all lemmas used by the theorem in question.
119
120  * `where_to_move` *thm*
121
122    The same, but for a specific theorem only.
123
124  * `theorems_used_by` *thm*
125
126    Prints all theorems used by the given theorems. Can be useful to understand
127    why `where_to_move` suggests a particular choice.
128  
129
130 Bugs and shortcomings
131 ---------------------
132
133 These are the ones that I know about. If you have more, feel free to open an issue. 
134
135  * In the output of `theorems_used_by`, if a theorem is actually a list of
136    them, and one is used, it prints the selector as part of the name
137    (`HOL.simp_thms_7`), which breaks the hyperlinking.
138  * Theory names are not clickable yet.
139  * Definitions should be treated specially. Naturally, most `foo_def` lemmas can be moved to
140    `HOL` (they are (derived from) axioms, after all), but I usually do not want to
141    move definitions.
142  * Using `where_to_move OtherTheory.bar` will print `Theorem OtherTheory.bar
143    could be moved to theory "OtherTheory"`, which is not wrong, but slighly
144    unhelpful.
145  * The interaction with locales is unexplored.
146  * Typing commands is an out-dated interface. Ideally, after activating this tool,
147    every proven lemma would be checked in the background and some wiggly lines would
148    indicate that this lemma could live somewhere else, similar to how `solve_direct` and
149    `nitpick` are run automatically.
150  * The installation suggestions make you enter the full path to the theory file
151    everytime you use it. Maybe it is possible to avoid this by registering this as
152    an *component*, but I could not make that work right away.
153  * The ML code could use some code review from someone more experienced with
154    SML and Isabelle/ML.
155    
156  
157
158