src/Doc/Tutorial/todo.tobias

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Tutorial/todo.tobias	Tue Aug 28 18:57:32 2012 +0200
@@ -0,0 +1,130 @@
+Implementation
+==============
+
+Add map_cong?? (upto 10% slower)
+
+a simp command for terms
+
+Recdef: Get rid of function name in header.
+Support mutual recursion (Konrad?)
+
+improve solver in simplifier: treat & and ! ...
+
+better 1 point rules:
+!x. !y. x = f y --> P x y  should reduce to  !y. P (f y) y.
+
+it would be nice if @term could deal with ?-vars.
+then a number of (unchecked!) @texts could be converted to @terms.
+
+it would be nice if one could get id to the enclosing quotes in the [source] option.
+
+More predefined functions for datatypes: map?
+
+Induction rules for int: int_le/ge_induct?
+Needed for ifak example. But is that example worth it?
+
+Komischerweise geht das Splitten von _Annahmen_ auch mit simp_tac, was
+ein generelles Feature ist, das man vielleicht mal abstellen sollte.
+
+proper mutual simplification
+
+defs with = and pattern matching??
+
+
+Minor fixes in the tutorial
+===========================
+
+Appendix: Lexical: long ids.
+
+Warning: infixes automatically become reserved words!
+
+Syntax section: syntax annotations not just for consts but also for constdefs and datatype.
+
+Appendix with list functions.
+
+All theory sources on the web?
+
+Possible exercises
+==================
+
+Exercises
+
+For extensionality (in Sets chapter): prove
+valif o norm = valif
+in If-expression case study (Ifexpr)
+
+Nested inductive datatypes: another example/exercise:
+ size(t) <= size(subst s t)?
+
+insertion sort: primrec, later recdef
+
+OTree:
+ first version only for non-empty trees:
+ Tip 'a | Node tree tree
+ Then real version?
+ First primrec, then recdef?
+
+Ind. sets: define ABC inductively and prove
+ABC = {rep A n @ rep B n @ rep C n. True}
+
+Partial rekursive functions / Nontermination:
+
+Exercise: ?! f. !i. f i = if i=0 then 1 else i*f(i-1)
+(What about sum? Is there one, a unique one?)
+
+Exercise
+Better(?) sum i = fst(while (%(s,i). i=0) (%(s,i). (s+i,i-1)) (0,i))
+Prove 0 <= i ==> sum i = i*(i+1) via while-rule
+
+Possible examples/case studies
+==============================
+
+Trie: Define functional version
+datatype ('a,'b)trie = Trie ('b option) ('a => ('a,'b)trie option)
+lookup t [] = value t
+lookup t (a#as) = case tries t a of None => None | Some s => lookup s as
+Maybe as an exercise?
+
+Trie: function for partial matches (prefixes). Needs sets for spec/proof.
+
+Sets via ordered list of intervals. (Isa/Interval(2))
+
+propositional logic (soundness and completeness?),
+predicate logic (soundness?),
+
+Tautology checker. Based on Ifexpr or prop.logic?
+Include forward reference in relevant section.
+
+Sorting with comp-parameter and with type class (<)
+
+Recdef:more example proofs:
+ if-normalization with measure function,
+ nested if-normalization,
+ quicksort
+ Trie?
+
+New book by Bird?
+
+Steps Towards Mechanizing Program Transformations Using PVS by N. Shankar,
+      Science of Computer Programming, 26(1-3):33-57, 1996. 
+You can get it from http://www.csl.sri.com/scp95.html
+
+J Moore article Towards a ...
+Mergesort, JVM
+
+
+Additional topics
+=================
+
+Recdef with nested recursion?
+
+Extensionality: applications in
+- boolean expressions: valif o bool2if = value
+- Advanced datatypes exercise subst (f o g) = subst f o subst g
+
+A look at the library?
+Map.
+
+Prototyping?
+
+==============================================================