4 - (#2 * x) = #2 * - x is not proved by arith
6 Relation: comp -> composition
8 Add map_cong?? (upto 10% slower)
10 Recdef: Get rid of function name in header.
11 Support mutual recursion (Konrad?)
13 use arith_tac in recdef to solve termination conditions?
14 -> new example in Recdef/termination
16 a tactic for replacing a specific occurrence:
19 it would be nice if @term could deal with ?-vars.
20 then a number of (unchecked!) @texts could be converted to @terms.
22 it would be nice if one could get id to the enclosing quotes in the [source] option.
24 More predefined functions for datatypes: map?
26 Induction rules for int: int_le/ge_induct?
27 Needed for ifak example. But is that example worth it?
29 Komischerweise geht das Splitten von _Annahmen_ auch mit simp_tac, was
30 ein generelles Feature ist, das man vielleicht mal abstellen sollte.
32 proper mutual simplification
34 defs with = and pattern matching??
37 Minor fixes in the tutorial
38 ===========================
40 I guess we should say "HOL" everywhere, with a remark early on about the
41 differences between our HOL and the other one.
43 warning: simp of asms from l to r; may require reordering (rotate_tac)
45 Adjust FP textbook refs: new Bird, Hudak
46 Discrete math textbook: Rosen?
48 say something about "abbreviations" when defs are introduced.
50 adjust type of ^ in tab:overloading
52 an example of induction: !y. A --> B --> C ??
54 Explain type_definition and mention pre-proved thms in subset.thy?
57 Appendix: Lexical: long ids.
59 Warning: infixes automatically become reserved words!
61 Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof?
63 recdef with nested recursion: either an example or at least a pointer to the
64 literature. In Recdef/termination.thy, at the end.
65 %FIXME, with one exception: nested recursion.
67 Syntax section: syntax annotations nor just for consts but also for constdefs and datatype.
69 Appendix with list functions.
71 Move section on rule inversion further to the front, and combine
72 \subsection{Universal quantifiers in introduction rules}
73 \subsection{Continuing the `ground terms' example}
76 Minor additions to the tutorial, unclear where
77 ==============================================
87 For extensionality (in Sets chapter): prove
89 in If-expression case study (Ifexpr)
91 Nested inductive datatypes: another example/exercise:
92 size(t) <= size(subst s t)?
94 insertion sort: primrec, later recdef
97 first version only for non-empty trees:
98 Tip 'a | Node tree tree
100 First primrec, then recdef?
102 Ind. sets: define ABC inductively and prove
103 ABC = {rep A n @ rep B n @ rep C n. True}
105 Partial rekursive functions / Nontermination:
107 Exercise: ?! f. !i. f i = if i=0 then 1 else i*f(i-1)
108 (What about sum? Is there one, a unique one?)
111 Better(?) sum i = fst(while (%(s,i). i=0) (%(s,i). (s+i,i-1)) (0,i))
112 Prove 0 <= i ==> sum i = i*(i+1) via while-rule
114 Possible examples/case studies
115 ==============================
117 Trie: Define functional version
118 datatype ('a,'b)trie = Trie ('b option) ('a => ('a,'b)trie option)
119 lookup t [] = value t
120 lookup t (a#as) = case tries t a of None => None | Some s => lookup s as
121 Maybe as an exercise?
123 Trie: function for partial matches (prefixes). Needs sets for spec/proof.
125 Sets via ordered list of intervals. (Isa/Interval(2))
127 propositional logic (soundness and completeness?),
128 predicate logic (soundness?),
130 Tautology checker. Based on Ifexpr or prop.logic?
131 Include forward reference in relevant section.
133 Sorting with comp-parameter and with type class (<)
135 Recdef:more example proofs:
136 if-normalization with measure function,
137 nested if-normalization,
143 Steps Towards Mechanizing Program Transformations Using PVS by N. Shankar,
144 Science of Computer Programming, 26(1-3):33-57, 1996.
145 You can get it from http://www.csl.sri.com/scp95.html
147 J Moore article Towards a ...
154 Recdef with nested recursion?
156 Extensionality: applications in
157 - boolean expressions: valif o bool2if = value
158 - Advanced datatypes exercise subst (f o g) = subst f o subst g
160 A look at the library?
165 ==============================================================