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