doc-src/TutorialI/todo.tobias
author nipkow
Wed Jan 24 12:29:10 2001 +0100 (2001-01-24)
changeset 10971 6852682eaf16
parent 10855 140a1ed65665
child 10983 59961d32b1ae
permissions -rw-r--r--
*** empty log message ***
nipkow@10281
     1
Implementation
nipkow@10281
     2
==============
nipkow@10177
     3
nipkow@10608
     4
Relation: comp -> composition
nipkow@10177
     5
nipkow@10177
     6
Add map_cong?? (upto 10% slower)
nipkow@10177
     7
nipkow@10281
     8
Recdef: Get rid of function name in header.
nipkow@10281
     9
Support mutual recursion (Konrad?)
nipkow@10177
    10
nipkow@10177
    11
use arith_tac in recdef to solve termination conditions?
nipkow@10177
    12
-> new example in Recdef/termination
nipkow@10177
    13
nipkow@10177
    14
a tactic for replacing a specific occurrence:
nipkow@10654
    15
apply(subst [2] thm)
nipkow@10177
    16
nipkow@10186
    17
it would be nice if @term could deal with ?-vars.
nipkow@10186
    18
then a number of (unchecked!) @texts could be converted to @terms.
nipkow@10186
    19
nipkow@10189
    20
it would be nice if one could get id to the enclosing quotes in the [source] option.
nipkow@10189
    21
nipkow@10281
    22
More predefined functions for datatypes: map?
nipkow@10281
    23
nipkow@10281
    24
Induction rules for int: int_le/ge_induct?
nipkow@10281
    25
Needed for ifak example. But is that example worth it?
nipkow@10281
    26
nipkow@10608
    27
Komischerweise geht das Splitten von _Annahmen_ auch mit simp_tac, was
nipkow@10608
    28
ein generelles Feature ist, das man vielleicht mal abstellen sollte.
nipkow@10608
    29
nipkow@10520
    30
proper mutual simplification
nipkow@10520
    31
nipkow@10520
    32
defs with = and pattern matching??
nipkow@10340
    33
nipkow@10186
    34
nipkow@10177
    35
Minor fixes in the tutorial
nipkow@10177
    36
===========================
nipkow@10177
    37
nipkow@10654
    38
adjust type of ^ in tab:overloading
nipkow@10654
    39
nipkow@10340
    40
explanation of term "contrapositive"/contraposition in Rules?
nipkow@10340
    41
Index the notion and maybe the rules contrapos_xy
nipkow@10340
    42
nipkow@10281
    43
get rid of use_thy in tutorial?
nipkow@10177
    44
nipkow@10509
    45
Orderings on numbers (with hint that it is overloaded):
nipkow@10520
    46
bounded quantifers ALL x<y, <=.
nipkow@10509
    47
nipkow@10177
    48
an example of induction: !y. A --> B --> C ??
nipkow@10177
    49
nipkow@10509
    50
Explain type_definition and mention pre-proved thms in subset.thy?
nipkow@10509
    51
-> Types/typedef
nipkow@10509
    52
nipkow@10177
    53
Appendix: Lexical: long ids.
nipkow@10177
    54
nipkow@10177
    55
Warning: infixes automatically become reserved words!
nipkow@10177
    56
nipkow@10177
    57
Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof?
nipkow@10177
    58
nipkow@10177
    59
recdef with nested recursion: either an example or at least a pointer to the
nipkow@10177
    60
literature. In Recdef/termination.thy, at the end.
nipkow@10177
    61
%FIXME, with one exception: nested recursion.
nipkow@10177
    62
nipkow@10186
    63
Syntax section: syntax annotations nor just for consts but also for constdefs and datatype.
nipkow@10186
    64
nipkow@10283
    65
Appendix with list functions.
nipkow@10283
    66
nipkow@10520
    67
Move section on rule inversion further to the front, and combine
nipkow@10520
    68
\subsection{Universal quantifiers in introduction rules}
nipkow@10520
    69
\subsection{Continuing the `ground terms' example}
nipkow@10520
    70
nipkow@10177
    71
nipkow@10177
    72
Minor additions to the tutorial, unclear where
nipkow@10177
    73
==============================================
nipkow@10177
    74
nipkow@10855
    75
unfold?
nipkow@10845
    76
nipkow@10186
    77
Tacticals: , ? +
nipkow@10654
    78
Note: + is used in typedef section!
nipkow@10177
    79
nipkow@10177
    80
A list of further useful commands (rules? tricks?)
nipkow@10281
    81
prefer, defer, print_simpset (-> print_simps?)
nipkow@10177
    82
nipkow@10177
    83
demonstrate x : set xs in Sets. Or Tricks chapter?
nipkow@10177
    84
nipkow@10676
    85
Appendix with HOL and Isar keywords.
nipkow@10177
    86
nipkow@10177
    87
nipkow@10177
    88
Possible exercises
nipkow@10177
    89
==================
nipkow@10177
    90
nipkow@10177
    91
Exercises
nipkow@10971
    92
nipkow@10971
    93
For extensionality (in Sets chapter): prove
nipkow@10971
    94
valif o norm = valif
nipkow@10971
    95
in If-expression case study (Ifexpr)
nipkow@10177
    96
nipkow@10177
    97
Nested inductive datatypes: another example/exercise:
nipkow@10177
    98
 size(t) <= size(subst s t)?
nipkow@10177
    99
nipkow@10177
   100
insertion sort: primrec, later recdef
nipkow@10177
   101
nipkow@10177
   102
OTree:
nipkow@10177
   103
 first version only for non-empty trees:
nipkow@10177
   104
 Tip 'a | Node tree tree
nipkow@10177
   105
 Then real version?
nipkow@10177
   106
 First primrec, then recdef?
nipkow@10177
   107
nipkow@10177
   108
Ind. sets: define ABC inductively and prove
nipkow@10177
   109
ABC = {rep A n @ rep B n @ rep C n. True}
nipkow@10177
   110
nipkow@10654
   111
Partial rekursive functions / Nontermination:
nipkow@10654
   112
nipkow@10654
   113
Exercise: ?! f. !i. f i = if i=0 then 1 else i*f(i-1)
nipkow@10654
   114
(What about sum? Is there one, a unique one?)
nipkow@10654
   115
nipkow@10654
   116
Exercise
nipkow@10654
   117
Better(?) sum i = fst(while (%(s,i). i=0) (%(s,i). (s+i,i-1)) (0,i))
nipkow@10654
   118
Prove 0 <= i ==> sum i = i*(i+1) via while-rule
nipkow@10654
   119
nipkow@10177
   120
Possible examples/case studies
nipkow@10177
   121
==============================
nipkow@10177
   122
nipkow@10177
   123
Trie: Define functional version
nipkow@10177
   124
datatype ('a,'b)trie = Trie ('b option) ('a => ('a,'b)trie option)
nipkow@10177
   125
lookup t [] = value t
nipkow@10177
   126
lookup t (a#as) = case tries t a of None => None | Some s => lookup s as
nipkow@10177
   127
Maybe as an exercise?
nipkow@10177
   128
nipkow@10177
   129
Trie: function for partial matches (prefixes). Needs sets for spec/proof.
nipkow@10177
   130
nipkow@10177
   131
Sets via ordered list of intervals. (Isa/Interval(2))
nipkow@10177
   132
nipkow@10177
   133
propositional logic (soundness and completeness?),
nipkow@10177
   134
predicate logic (soundness?),
nipkow@10177
   135
nipkow@10177
   136
Tautology checker. Based on Ifexpr or prop.logic?
nipkow@10177
   137
Include forward reference in relevant section.
nipkow@10177
   138
nipkow@10177
   139
Sorting with comp-parameter and with type class (<)
nipkow@10177
   140
nipkow@10654
   141
Recdef:more example proofs:
nipkow@10654
   142
 if-normalization with measure function,
nipkow@10654
   143
 nested if-normalization,
nipkow@10654
   144
 quicksort
nipkow@10654
   145
 Trie?
nipkow@10654
   146
nipkow@10177
   147
New book by Bird?
nipkow@10177
   148
nipkow@10177
   149
Steps Towards Mechanizing Program Transformations Using PVS by N. Shankar,
nipkow@10177
   150
      Science of Computer Programming, 26(1-3):33-57, 1996. 
nipkow@10177
   151
You can get it from http://www.csl.sri.com/scp95.html
nipkow@10177
   152
nipkow@10177
   153
J Moore article Towards a ...
nipkow@10177
   154
Mergesort, JVM
nipkow@10177
   155
nipkow@10177
   156
nipkow@10177
   157
Additional topics
nipkow@10177
   158
=================
nipkow@10177
   159
nipkow@10281
   160
Recdef with nested recursion?
nipkow@10177
   161
nipkow@10177
   162
Extensionality: applications in
nipkow@10177
   163
- boolean expressions: valif o bool2if = value
nipkow@10177
   164
- Advanced datatypes exercise subst (f o g) = subst f o subst g
nipkow@10177
   165
nipkow@10177
   166
A look at the library?
nipkow@10281
   167
Map.
nipkow@10177
   168
nipkow@10177
   169
Prototyping?
nipkow@10177
   170
nipkow@10177
   171
==============================================================