--- a/doc-src/TutorialI/todo.tobias Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,130 +0,0 @@
-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?
-
-==============================================================