1 General questions |
1 Implementation |
2 ================= |
2 ============== |
3 |
|
4 Here is an initial list: |
|
5 clarify, clarsimp, hyp_subst_tac, rename_tac, rotate_tac, split |
|
6 single step tactics: (e/d/f)rule, insert |
|
7 with instantiation: (e/d/f)rule_tac, insert_tac |
|
8 |
3 |
9 Hide global names like Node. |
4 Hide global names like Node. |
10 Why is comp needed in addition to op O? |
5 Why is comp needed in addition to op O? |
11 Explain in syntax section! |
6 Explain in syntax section! |
12 |
7 |
13 Implementation |
8 defs with = and pattern matching |
14 ============== |
9 |
15 |
10 replace "simp only split" by "split_tac". |
16 swap in classical.ML has ugly name Pa in it. Rename. |
11 |
|
12 arithmetic: allow mixed nat/int formulae |
|
13 -> simplify proof of part1 in Inductive/AB.thy |
|
14 |
|
15 Add map_cong?? (upto 10% slower) |
|
16 |
|
17 Recdef: Get rid of function name in header. |
|
18 Support mutual recursion (Konrad?) |
|
19 |
|
20 use arith_tac in recdef to solve termination conditions? |
|
21 -> new example in Recdef/termination |
|
22 |
|
23 a tactic for replacing a specific occurrence: |
|
24 apply(substitute [2] thm) |
|
25 |
|
26 it would be nice if @term could deal with ?-vars. |
|
27 then a number of (unchecked!) @texts could be converted to @terms. |
|
28 |
|
29 it would be nice if one could get id to the enclosing quotes in the [source] option. |
|
30 |
|
31 More predefined functions for datatypes: map? |
17 |
32 |
18 Induction rules for int: int_le/ge_induct? |
33 Induction rules for int: int_le/ge_induct? |
19 Needed for ifak example. But is that example worth it? |
34 Needed for ifak example. But is that example worth it? |
20 |
35 |
21 Add map_cong?? (upto 10% slower) |
|
22 But we should install UN_cong and INT_cong too. |
|
23 |
|
24 defs with = and pattern matching |
|
25 |
|
26 use arith_tac in recdef to solve termination conditions? |
|
27 -> new example in Recdef/termination |
|
28 |
|
29 a tactic for replacing a specific occurrence: |
|
30 apply(substitute [2] thm) |
|
31 |
|
32 it would be nice if @term could deal with ?-vars. |
|
33 then a number of (unchecked!) @texts could be converted to @terms. |
|
34 |
|
35 it would be nice if one could get id to the enclosing quotes in the [source] option. |
|
36 |
|
37 arithmetic: allow mixed nat/int formulae |
|
38 -> simplify proof of part1 in Inductive/AB.thy |
|
39 |
36 |
40 Minor fixes in the tutorial |
37 Minor fixes in the tutorial |
41 =========================== |
38 =========================== |
42 |
39 |
43 replace simp only split by split_tac. |
40 explanation of absence of contrapos_pn in Rules? |
44 |
41 |
45 get rid of use_thy? |
42 get rid of use_thy in tutorial? |
46 |
43 |
47 Explain typographic conventions? |
44 Explain typographic conventions? |
48 |
45 |
49 an example of induction: !y. A --> B --> C ?? |
46 an example of induction: !y. A --> B --> C ?? |
50 |
47 |
60 literature. In Recdef/termination.thy, at the end. |
57 literature. In Recdef/termination.thy, at the end. |
61 %FIXME, with one exception: nested recursion. |
58 %FIXME, with one exception: nested recursion. |
62 |
59 |
63 Syntax section: syntax annotations nor just for consts but also for constdefs and datatype. |
60 Syntax section: syntax annotations nor just for consts but also for constdefs and datatype. |
64 |
61 |
65 Prove EU exercise in CTL. |
|
66 |
|
67 |
62 |
68 Minor additions to the tutorial, unclear where |
63 Minor additions to the tutorial, unclear where |
69 ============================================== |
64 ============================================== |
70 |
65 |
71 Tacticals: , ? + |
66 Tacticals: , ? + |
72 |
67 |
73 "typedecl" is used in CTL/Base, but where is it introduced? |
|
74 In More Types chapter? Rephrase the CTL bit accordingly. |
|
75 |
|
76 print_simpset (-> print_simps?) |
|
77 (Another subsection Useful theorems, methods, and commands?) |
|
78 |
|
79 Mention that simp etc (big step tactics) insist on change? |
68 Mention that simp etc (big step tactics) insist on change? |
80 |
69 |
81 Rules: Introduce "by" (as a kind of shorthand for apply+done, except that it |
70 Rules: Introduce "by" (as a kind of shorthand for apply+done, except that it |
82 does more.) |
71 does more.) |
83 |
72 |
84 A list of further useful commands (rules? tricks?) |
73 A list of further useful commands (rules? tricks?) |
85 prefer, defer |
74 prefer, defer, print_simpset (-> print_simps?) |
86 |
75 |
87 An overview of the automatic methods: simp, auto, fast, blast, force, |
76 An overview of the automatic methods: simp, auto, fast, blast, force, |
88 clarify, clarsimp (intro, elim?) |
77 clarify, clarsimp (intro, elim?) |
89 |
78 |
90 Advanced Ind expects rule_format incl (no_asm) (which it currently explains!) |
79 Advanced Ind expects rule_format incl (no_asm) (which it currently explains!) |
132 |
121 |
133 Trie: function for partial matches (prefixes). Needs sets for spec/proof. |
122 Trie: function for partial matches (prefixes). Needs sets for spec/proof. |
134 |
123 |
135 Sets via ordered list of intervals. (Isa/Interval(2)) |
124 Sets via ordered list of intervals. (Isa/Interval(2)) |
136 |
125 |
137 Sets: PDL and CTL |
|
138 |
|
139 Ind. defs: Grammar (for same number of as and bs), |
|
140 propositional logic (soundness and completeness?), |
126 propositional logic (soundness and completeness?), |
141 predicate logic (soundness?), |
127 predicate logic (soundness?), |
142 CTL proof. |
|
143 |
128 |
144 Tautology checker. Based on Ifexpr or prop.logic? |
129 Tautology checker. Based on Ifexpr or prop.logic? |
145 Include forward reference in relevant section. |
130 Include forward reference in relevant section. |
146 |
131 |
147 Sorting with comp-parameter and with type class (<) |
132 Sorting with comp-parameter and with type class (<) |
157 |
142 |
158 |
143 |
159 Additional topics |
144 Additional topics |
160 ================= |
145 ================= |
161 |
146 |
162 Beef up recdef (see below). |
147 Recdef with nested recursion? |
163 Nested recursion? Mutual recursion? |
|
164 |
|
165 Nested inductive datatypes: better recursion and induction |
|
166 (see below) |
|
167 |
148 |
168 Extensionality: applications in |
149 Extensionality: applications in |
169 - boolean expressions: valif o bool2if = value |
150 - boolean expressions: valif o bool2if = value |
170 - Advanced datatypes exercise subst (f o g) = subst f o subst g |
151 - Advanced datatypes exercise subst (f o g) = subst f o subst g |
171 |
152 |
172 A look at the library? |
153 A look at the library? |
173 Functions. Relations. Lfp/Gfp. Map. |
154 Map. |
174 If WF is discussed, make a link to it from AdvancedInd. |
155 If WF is discussed, make a link to it from AdvancedInd. |
175 |
156 |
176 Prototyping? |
157 Prototyping? |
177 |
|
178 |
|
179 Isabelle |
|
180 ======== |
|
181 |
|
182 Get rid of function name in recdef header |
|
183 |
|
184 More predefined functions for datatypes: map? |
|
185 |
|
186 1 and 2 on nat? |
|
187 |
|
188 |
158 |
189 ============================================================== |
159 ============================================================== |
190 Recdef: |
160 Recdef: |
191 |
161 |
192 nested recursion |
162 nested recursion |