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