6b98acfdba30c0f29bd93ec20eb4c89e63a9cb39
[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 Where_To_Move_Ex4.barE2 could be moved to theory "Where_To_Move_Ex2". 
93     Theorem Where_To_Move_Ex4.fooI2 could be moved to theory "Where_To_Move_Ex1". 
94     Theorem Where_To_Move_Ex4.foobar could be moved to theory "Where_To_Move_Ex3". 
95     Theorem Where_To_Move_Ex4.foobar2 is fine where it is
96
97 Installation
98 ------------
99
100  * Clone this repository somewhere, say to `~/isabelle/isa-where-to-move`.
101  * Add `"$HOME/isabelle/isa-where-to-move/Where_To_Move"` to your import list
102  * Done
103
104 Usage
105 -----
106
107  * `where_to_move`
108  
109    For all lemmas defined in the current module, give an indication where it should be
110    moved.
111
112    The logic is as follows: In the list of dependencies of the current theory,
113    find the first (i.e. most primitive) theory that contains all theories of
114    all lemmas used by the theorem in question.
115
116  * `where_to_move` ''thm''
117
118    The same, but for a specific theorem only.
119
120  * `theorems_used_by` ''thm''
121
122    Prints all theorems used by the given theorems. Can be useful to understand
123    why `where_to_move` suggests a particular choice.
124  
125
126 Bugs and shortcomings
127 ---------------------
128
129 These are the ones that I know about. If you have more, feel free to open an issue. 
130
131  * The output does not use proper markup, i.e. you cannot click on the theorem
132    names and theory names, which would make this even more useful.
133  * Definitions should be treated specially. Naturally, most `foo_def` lemmas can be moved to
134    `HOL` (they are (derived from) axioms, after all), but I usually do not want to
135    move definitions.
136  * Using `where_to_move OtherTheory.bar` will print `Theorem OtherTheory.bar
137    could be moved to theory "OtherTheory"`, which is not wrong, but slighly
138    unhelpful.
139  * The ML code could use some code review from someone more experienced with
140    SML and Isabelle/ML.
141  
142
143