summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Doc/Tutorial/todo.tobias

author | wenzelm |

Mon, 07 Oct 2013 21:24:44 +0200 | |

changeset 54313 | da2e6282a4f5 |

parent 48985 | 5386df44a037 |

permissions | -rw-r--r-- |

native executable even for Linux, to avoid surprises with file managers opening executable script as text file;

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? ==============================================================