doc-src/TutorialI/todo.tobias
author nipkow
Sun Nov 26 10:48:38 2000 +0100 (2000-11-26)
changeset 10520 bb9dfcc87951
parent 10509 ff24ac6678dd
child 10608 620647438780
permissions -rw-r--r--
*** empty log message ***
nipkow@10281
     1
Implementation
nipkow@10281
     2
==============
nipkow@10177
     3
nipkow@10177
     4
Why is comp needed in addition to op O?
nipkow@10177
     5
Explain in syntax section!
nipkow@10177
     6
nipkow@10281
     7
replace "simp only split" by "split_tac".
nipkow@10177
     8
nipkow@10281
     9
arithmetic: allow mixed nat/int formulae
nipkow@10281
    10
-> simplify proof of part1 in Inductive/AB.thy
nipkow@10177
    11
nipkow@10177
    12
Add map_cong?? (upto 10% slower)
nipkow@10177
    13
nipkow@10281
    14
Recdef: Get rid of function name in header.
nipkow@10281
    15
Support mutual recursion (Konrad?)
nipkow@10177
    16
nipkow@10177
    17
use arith_tac in recdef to solve termination conditions?
nipkow@10177
    18
-> new example in Recdef/termination
nipkow@10177
    19
nipkow@10177
    20
a tactic for replacing a specific occurrence:
nipkow@10177
    21
apply(substitute [2] thm)
nipkow@10177
    22
nipkow@10186
    23
it would be nice if @term could deal with ?-vars.
nipkow@10186
    24
then a number of (unchecked!) @texts could be converted to @terms.
nipkow@10186
    25
nipkow@10189
    26
it would be nice if one could get id to the enclosing quotes in the [source] option.
nipkow@10189
    27
nipkow@10281
    28
More predefined functions for datatypes: map?
nipkow@10281
    29
nipkow@10281
    30
Induction rules for int: int_le/ge_induct?
nipkow@10281
    31
Needed for ifak example. But is that example worth it?
nipkow@10281
    32
nipkow@10520
    33
proper mutual simplification
nipkow@10520
    34
nipkow@10520
    35
defs with = and pattern matching??
nipkow@10340
    36
nipkow@10186
    37
nipkow@10177
    38
Minor fixes in the tutorial
nipkow@10177
    39
===========================
nipkow@10177
    40
nipkow@10340
    41
explanation of term "contrapositive"/contraposition in Rules?
nipkow@10340
    42
Index the notion and maybe the rules contrapos_xy
nipkow@10340
    43
nipkow@10340
    44
Even: forward ref from problem with "Suc(Suc n) : even" to general solution in
nipkow@10340
    45
AdvancedInd section.
nipkow@10177
    46
nipkow@10281
    47
get rid of use_thy in tutorial?
nipkow@10177
    48
nipkow@10177
    49
Explain typographic conventions?
nipkow@10177
    50
nipkow@10509
    51
Orderings on numbers (with hint that it is overloaded):
nipkow@10520
    52
bounded quantifers ALL x<y, <=.
nipkow@10509
    53
nipkow@10177
    54
an example of induction: !y. A --> B --> C ??
nipkow@10177
    55
nipkow@10509
    56
Explain type_definition and mention pre-proved thms in subset.thy?
nipkow@10509
    57
-> Types/typedef
nipkow@10509
    58
nipkow@10177
    59
Appendix: Lexical: long ids.
nipkow@10177
    60
nipkow@10177
    61
Warning: infixes automatically become reserved words!
nipkow@10177
    62
nipkow@10177
    63
Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof?
nipkow@10177
    64
nipkow@10177
    65
mention split_split in advanced pair section.
nipkow@10177
    66
nipkow@10177
    67
recdef with nested recursion: either an example or at least a pointer to the
nipkow@10177
    68
literature. In Recdef/termination.thy, at the end.
nipkow@10177
    69
%FIXME, with one exception: nested recursion.
nipkow@10177
    70
nipkow@10186
    71
Syntax section: syntax annotations nor just for consts but also for constdefs and datatype.
nipkow@10186
    72
nipkow@10283
    73
Appendix with list functions.
nipkow@10283
    74
nipkow@10520
    75
Move section on rule inversion further to the front, and combine
nipkow@10520
    76
\subsection{Universal quantifiers in introduction rules}
nipkow@10520
    77
\subsection{Continuing the `ground terms' example}
nipkow@10520
    78
nipkow@10177
    79
nipkow@10177
    80
Minor additions to the tutorial, unclear where
nipkow@10177
    81
==============================================
nipkow@10177
    82
nipkow@10186
    83
Tacticals: , ? +
nipkow@10177
    84
nipkow@10177
    85
Mention that simp etc (big step tactics) insist on change?
nipkow@10177
    86
nipkow@10237
    87
Rules: Introduce "by" (as a kind of shorthand for apply+done, except that it
nipkow@10237
    88
does more.)
nipkow@10177
    89
nipkow@10177
    90
A list of further useful commands (rules? tricks?)
nipkow@10281
    91
prefer, defer, print_simpset (-> print_simps?)
nipkow@10177
    92
nipkow@10177
    93
An overview of the automatic methods: simp, auto, fast, blast, force,
nipkow@10177
    94
clarify, clarsimp (intro, elim?)
nipkow@10177
    95
nipkow@10237
    96
Advanced Ind expects rule_format incl (no_asm) (which it currently explains!)
nipkow@10242
    97
Where explained? Should go into a separate section as Inductive needs it as
nipkow@10242
    98
well.
nipkow@10237
    99
nipkow@10237
   100
Where is "simplified" explained? Needed by Inductive/AB.thy
nipkow@10177
   101
nipkow@10177
   102
demonstrate x : set xs in Sets. Or Tricks chapter?
nipkow@10177
   103
nipkow@10177
   104
Appendix with HOL keywords. Say something about other keywords.
nipkow@10177
   105
nipkow@10177
   106
nipkow@10177
   107
Possible exercises
nipkow@10177
   108
==================
nipkow@10177
   109
nipkow@10177
   110
Exercises
nipkow@10177
   111
%\begin{exercise}
nipkow@10177
   112
%Extend expressions by conditional expressions.
nipkow@10177
   113
braucht wfrec!
nipkow@10177
   114
%\end{exercise}
nipkow@10177
   115
nipkow@10177
   116
Nested inductive datatypes: another example/exercise:
nipkow@10177
   117
 size(t) <= size(subst s t)?
nipkow@10177
   118
nipkow@10177
   119
insertion sort: primrec, later recdef
nipkow@10177
   120
nipkow@10177
   121
OTree:
nipkow@10177
   122
 first version only for non-empty trees:
nipkow@10177
   123
 Tip 'a | Node tree tree
nipkow@10177
   124
 Then real version?
nipkow@10177
   125
 First primrec, then recdef?
nipkow@10177
   126
nipkow@10177
   127
Ind. sets: define ABC inductively and prove
nipkow@10177
   128
ABC = {rep A n @ rep B n @ rep C n. True}
nipkow@10177
   129
nipkow@10177
   130
Possible examples/case studies
nipkow@10177
   131
==============================
nipkow@10177
   132
nipkow@10177
   133
Trie: Define functional version
nipkow@10177
   134
datatype ('a,'b)trie = Trie ('b option) ('a => ('a,'b)trie option)
nipkow@10177
   135
lookup t [] = value t
nipkow@10177
   136
lookup t (a#as) = case tries t a of None => None | Some s => lookup s as
nipkow@10177
   137
Maybe as an exercise?
nipkow@10177
   138
nipkow@10177
   139
Trie: function for partial matches (prefixes). Needs sets for spec/proof.
nipkow@10177
   140
nipkow@10177
   141
Sets via ordered list of intervals. (Isa/Interval(2))
nipkow@10177
   142
nipkow@10177
   143
propositional logic (soundness and completeness?),
nipkow@10177
   144
predicate logic (soundness?),
nipkow@10177
   145
nipkow@10177
   146
Tautology checker. Based on Ifexpr or prop.logic?
nipkow@10177
   147
Include forward reference in relevant section.
nipkow@10177
   148
nipkow@10177
   149
Sorting with comp-parameter and with type class (<)
nipkow@10177
   150
nipkow@10177
   151
New book by Bird?
nipkow@10177
   152
nipkow@10177
   153
Steps Towards Mechanizing Program Transformations Using PVS by N. Shankar,
nipkow@10177
   154
      Science of Computer Programming, 26(1-3):33-57, 1996. 
nipkow@10177
   155
You can get it from http://www.csl.sri.com/scp95.html
nipkow@10177
   156
nipkow@10177
   157
J Moore article Towards a ...
nipkow@10177
   158
Mergesort, JVM
nipkow@10177
   159
nipkow@10177
   160
nipkow@10177
   161
Additional topics
nipkow@10177
   162
=================
nipkow@10177
   163
nipkow@10281
   164
Recdef with nested recursion?
nipkow@10177
   165
nipkow@10177
   166
Extensionality: applications in
nipkow@10177
   167
- boolean expressions: valif o bool2if = value
nipkow@10177
   168
- Advanced datatypes exercise subst (f o g) = subst f o subst g
nipkow@10177
   169
nipkow@10177
   170
A look at the library?
nipkow@10281
   171
Map.
nipkow@10177
   172
If WF is discussed, make a link to it from AdvancedInd.
nipkow@10177
   173
nipkow@10177
   174
Prototyping?
nipkow@10177
   175
nipkow@10177
   176
==============================================================
nipkow@10177
   177
Recdef:
nipkow@10177
   178
nipkow@10177
   179
nested recursion
nipkow@10177
   180
more example proofs:
nipkow@10177
   181
 if-normalization with measure function,
nipkow@10177
   182
 nested if-normalization,
nipkow@10177
   183
 quicksort
nipkow@10177
   184
 Trie?
nipkow@10177
   185
a case study?
nipkow@10177
   186
nipkow@10177
   187
----------
nipkow@10177
   188
nipkow@10177
   189
Partial rekursive functions / Nontermination
nipkow@10177
   190
nipkow@10177
   191
What appears to be the problem:
nipkow@10177
   192
axiom f n = f n + 1
nipkow@10177
   193
lemma False
nipkow@10177
   194
apply(cut_facts_tac axiom, simp).
nipkow@10177
   195
nipkow@10177
   196
1. Guarded recursion
nipkow@10177
   197
nipkow@10177
   198
Scheme:
nipkow@10177
   199
f x = if $x \in dom(f)$ then ... else arbitrary
nipkow@10177
   200
nipkow@10177
   201
Example: sum/fact: int -> int (for no good reason because we have nat)
nipkow@10177
   202
nipkow@10177
   203
Exercise: ?! f. !i. f i = if i=0 then 1 else i*f(i-1)
nipkow@10177
   204
(What about sum? Is there one, a unique one?)
nipkow@10177
   205
nipkow@10177
   206
[Alternative: include argument that is counted down
nipkow@10177
   207
 f x n = if n=0 then None else ...
nipkow@10177
   208
Refer to Boyer and Moore]
nipkow@10177
   209
nipkow@10177
   210
More complex: same_fst
nipkow@10177
   211
nipkow@10177
   212
chase(f,x) = if wf{(f x,x) . f x ~= x}
nipkow@10177
   213
             then if f x = x then x else chase(f,f x)
nipkow@10177
   214
             else arb
nipkow@10177
   215
nipkow@10177
   216
Prove wf ==> f(chase(f,x)) = chase(f,x)
nipkow@10177
   217
nipkow@10177
   218
2. While / Tail recursion
nipkow@10177
   219
nipkow@10177
   220
chase f x = fst(while (%(x,fx). x=fx) (%(x,fx). (fx,f fx)) (x,f x))
nipkow@10177
   221
nipkow@10177
   222
==> unfold eqn for chase? Prove fixpoint property?
nipkow@10177
   223
nipkow@10177
   224
Better(?) sum i = fst(while (%(s,i). i=0) (%(s,i). (s+i,i-1)) (0,i))
nipkow@10177
   225
Prove 0 <= i ==> sum i = i*(i+1) via while-rule
nipkow@10177
   226
nipkow@10177
   227
Mention prototyping?
nipkow@10177
   228
==============================================================