4 Relation: comp -> composition
6 Add map_cong?? (upto 10% slower)
8 Recdef: Get rid of function name in header.
9 Support mutual recursion (Konrad?)
11 use arith_tac in recdef to solve termination conditions?
12 -> new example in Recdef/termination
14 a tactic for replacing a specific occurrence:
17 it would be nice if @term could deal with ?-vars.
18 then a number of (unchecked!) @texts could be converted to @terms.
20 it would be nice if one could get id to the enclosing quotes in the [source] option.
22 More predefined functions for datatypes: map?
24 Induction rules for int: int_le/ge_induct?
25 Needed for ifak example. But is that example worth it?
27 Komischerweise geht das Splitten von _Annahmen_ auch mit simp_tac, was
28 ein generelles Feature ist, das man vielleicht mal abstellen sollte.
30 proper mutual simplification
32 defs with = and pattern matching??
35 Minor fixes in the tutorial
36 ===========================
38 adjust type of ^ in tab:overloading
40 explanation of term "contrapositive"/contraposition in Rules?
41 Index the notion and maybe the rules contrapos_xy
43 If Advanced and Types chapter ar swapped:
44 Make forward ref from ... = True in Axioms to preprocessor section.
46 get rid of use_thy in tutorial?
48 Orderings on numbers (with hint that it is overloaded):
49 bounded quantifers ALL x<y, <=.
51 an example of induction: !y. A --> B --> C ??
53 Explain type_definition and mention pre-proved thms in subset.thy?
56 Appendix: Lexical: long ids.
58 Warning: infixes automatically become reserved words!
60 Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof?
62 recdef with nested recursion: either an example or at least a pointer to the
63 literature. In Recdef/termination.thy, at the end.
64 %FIXME, with one exception: nested recursion.
66 Syntax section: syntax annotations nor just for consts but also for constdefs and datatype.
68 Appendix with list functions.
70 Move section on rule inversion further to the front, and combine
71 \subsection{Universal quantifiers in introduction rules}
72 \subsection{Continuing the `ground terms' example}
75 Minor additions to the tutorial, unclear where
76 ==============================================
79 Note: + is used in typedef section!
81 Mention that simp etc (big step tactics) insist on change?
83 Rules: Introduce "by" (as a kind of shorthand for apply+done, except that it
86 A list of further useful commands (rules? tricks?)
87 prefer, defer, print_simpset (-> print_simps?)
89 Advanced Ind expects rule_format incl (no_asm) (which it currently explains!)
90 Where explained? Should go into a separate section as Inductive needs it as
93 Where is "simplified" explained? Needed by Inductive/AB.thy
95 demonstrate x : set xs in Sets. Or Tricks chapter?
97 Appendix with HOL keywords. Say something about other keywords.
105 %Extend expressions by conditional expressions.
109 Nested inductive datatypes: another example/exercise:
110 size(t) <= size(subst s t)?
112 insertion sort: primrec, later recdef
115 first version only for non-empty trees:
116 Tip 'a | Node tree tree
118 First primrec, then recdef?
120 Ind. sets: define ABC inductively and prove
121 ABC = {rep A n @ rep B n @ rep C n. True}
123 Partial rekursive functions / Nontermination:
125 Exercise: ?! f. !i. f i = if i=0 then 1 else i*f(i-1)
126 (What about sum? Is there one, a unique one?)
129 Better(?) sum i = fst(while (%(s,i). i=0) (%(s,i). (s+i,i-1)) (0,i))
130 Prove 0 <= i ==> sum i = i*(i+1) via while-rule
132 Possible examples/case studies
133 ==============================
135 Trie: Define functional version
136 datatype ('a,'b)trie = Trie ('b option) ('a => ('a,'b)trie option)
137 lookup t [] = value t
138 lookup t (a#as) = case tries t a of None => None | Some s => lookup s as
139 Maybe as an exercise?
141 Trie: function for partial matches (prefixes). Needs sets for spec/proof.
143 Sets via ordered list of intervals. (Isa/Interval(2))
145 propositional logic (soundness and completeness?),
146 predicate logic (soundness?),
148 Tautology checker. Based on Ifexpr or prop.logic?
149 Include forward reference in relevant section.
151 Sorting with comp-parameter and with type class (<)
153 Recdef:more example proofs:
154 if-normalization with measure function,
155 nested if-normalization,
161 Steps Towards Mechanizing Program Transformations Using PVS by N. Shankar,
162 Science of Computer Programming, 26(1-3):33-57, 1996.
163 You can get it from http://www.csl.sri.com/scp95.html
165 J Moore article Towards a ...
172 Recdef with nested recursion?
174 Extensionality: applications in
175 - boolean expressions: valif o bool2if = value
176 - Advanced datatypes exercise subst (f o g) = subst f o subst g
178 A look at the library?
183 ==============================================================