doc-src/TutorialI/todo.tobias
author huffman
Thu Apr 19 10:49:47 2012 +0200 (2012-04-19)
changeset 47579 28f6f4ad69bf
parent 12492 a4dd02e744e0
permissions -rw-r--r--
tuned lemmas (v)image_id;
removed duplicate of vimage_id
     1 Implementation
     2 ==============
     3 
     4 Add map_cong?? (upto 10% slower)
     5 
     6 a simp command for terms
     7 
     8 Recdef: Get rid of function name in header.
     9 Support mutual recursion (Konrad?)
    10 
    11 improve solver in simplifier: treat & and ! ...
    12 
    13 better 1 point rules:
    14 !x. !y. x = f y --> P x y  should reduce to  !y. P (f y) y.
    15 
    16 it would be nice if @term could deal with ?-vars.
    17 then a number of (unchecked!) @texts could be converted to @terms.
    18 
    19 it would be nice if one could get id to the enclosing quotes in the [source] option.
    20 
    21 More predefined functions for datatypes: map?
    22 
    23 Induction rules for int: int_le/ge_induct?
    24 Needed for ifak example. But is that example worth it?
    25 
    26 Komischerweise geht das Splitten von _Annahmen_ auch mit simp_tac, was
    27 ein generelles Feature ist, das man vielleicht mal abstellen sollte.
    28 
    29 proper mutual simplification
    30 
    31 defs with = and pattern matching??
    32 
    33 
    34 Minor fixes in the tutorial
    35 ===========================
    36 
    37 Appendix: Lexical: long ids.
    38 
    39 Warning: infixes automatically become reserved words!
    40 
    41 Syntax section: syntax annotations not just for consts but also for constdefs and datatype.
    42 
    43 Appendix with list functions.
    44 
    45 All theory sources on the web?
    46 
    47 Possible exercises
    48 ==================
    49 
    50 Exercises
    51 
    52 For extensionality (in Sets chapter): prove
    53 valif o norm = valif
    54 in If-expression case study (Ifexpr)
    55 
    56 Nested inductive datatypes: another example/exercise:
    57  size(t) <= size(subst s t)?
    58 
    59 insertion sort: primrec, later recdef
    60 
    61 OTree:
    62  first version only for non-empty trees:
    63  Tip 'a | Node tree tree
    64  Then real version?
    65  First primrec, then recdef?
    66 
    67 Ind. sets: define ABC inductively and prove
    68 ABC = {rep A n @ rep B n @ rep C n. True}
    69 
    70 Partial rekursive functions / Nontermination:
    71 
    72 Exercise: ?! f. !i. f i = if i=0 then 1 else i*f(i-1)
    73 (What about sum? Is there one, a unique one?)
    74 
    75 Exercise
    76 Better(?) sum i = fst(while (%(s,i). i=0) (%(s,i). (s+i,i-1)) (0,i))
    77 Prove 0 <= i ==> sum i = i*(i+1) via while-rule
    78 
    79 Possible examples/case studies
    80 ==============================
    81 
    82 Trie: Define functional version
    83 datatype ('a,'b)trie = Trie ('b option) ('a => ('a,'b)trie option)
    84 lookup t [] = value t
    85 lookup t (a#as) = case tries t a of None => None | Some s => lookup s as
    86 Maybe as an exercise?
    87 
    88 Trie: function for partial matches (prefixes). Needs sets for spec/proof.
    89 
    90 Sets via ordered list of intervals. (Isa/Interval(2))
    91 
    92 propositional logic (soundness and completeness?),
    93 predicate logic (soundness?),
    94 
    95 Tautology checker. Based on Ifexpr or prop.logic?
    96 Include forward reference in relevant section.
    97 
    98 Sorting with comp-parameter and with type class (<)
    99 
   100 Recdef:more example proofs:
   101  if-normalization with measure function,
   102  nested if-normalization,
   103  quicksort
   104  Trie?
   105 
   106 New book by Bird?
   107 
   108 Steps Towards Mechanizing Program Transformations Using PVS by N. Shankar,
   109       Science of Computer Programming, 26(1-3):33-57, 1996. 
   110 You can get it from http://www.csl.sri.com/scp95.html
   111 
   112 J Moore article Towards a ...
   113 Mergesort, JVM
   114 
   115 
   116 Additional topics
   117 =================
   118 
   119 Recdef with nested recursion?
   120 
   121 Extensionality: applications in
   122 - boolean expressions: valif o bool2if = value
   123 - Advanced datatypes exercise subst (f o g) = subst f o subst g
   124 
   125 A look at the library?
   126 Map.
   127 
   128 Prototyping?
   129 
   130 ==============================================================