doc-src/TutorialI/todo.tobias
author nipkow
Tue Oct 17 13:28:57 2000 +0200 (2000-10-17)
changeset 10236 7626cb4e1407
parent 10217 e61e7e1eacaf
child 10237 875bf54b5d74
permissions -rw-r--r--
*** empty log message ***
nipkow@10177
     1
General questions
nipkow@10177
     2
=================
nipkow@10177
     3
nipkow@10177
     4
Here is an initial list:
nipkow@10177
     5
clarify, clarsimp, hyp_subst_tac, rename_tac, rotate_tac, split
nipkow@10177
     6
single step tactics: (e/d/f)rule, insert
nipkow@10177
     7
with instantiation: (e/d/f)rule_tac, insert_tac
nipkow@10177
     8
nipkow@10177
     9
Hide global names like Node.
nipkow@10177
    10
Why is comp needed in addition to op O?
nipkow@10177
    11
Explain in syntax section!
nipkow@10177
    12
nipkow@10177
    13
Implementation
nipkow@10177
    14
==============
nipkow@10177
    15
nipkow@10177
    16
swap in classical.ML has ugly name Pa in it. Rename.
nipkow@10177
    17
nipkow@10177
    18
Induction rules for int: int_le/ge_induct?
nipkow@10177
    19
Needed for ifak example. But is that example worth it?
nipkow@10177
    20
nipkow@10177
    21
Add map_cong?? (upto 10% slower)
nipkow@10177
    22
But we should install UN_cong and INT_cong too.
nipkow@10177
    23
nipkow@10177
    24
recdef: funny behaviour with map (see email to Konrad.Slind, Recdef/Nested1)
nipkow@10177
    25
nipkow@10177
    26
defs with = and pattern matching
nipkow@10177
    27
nipkow@10177
    28
use arith_tac in recdef to solve termination conditions?
nipkow@10177
    29
-> new example in Recdef/termination
nipkow@10177
    30
nipkow@10177
    31
a tactic for replacing a specific occurrence:
nipkow@10177
    32
apply(substitute [2] thm)
nipkow@10177
    33
nipkow@10186
    34
it would be nice if @term could deal with ?-vars.
nipkow@10186
    35
then a number of (unchecked!) @texts could be converted to @terms.
nipkow@10186
    36
nipkow@10189
    37
it would be nice if one could get id to the enclosing quotes in the [source] option.
nipkow@10189
    38
nipkow@10236
    39
arithmetic: allow mixed nat/int formulae
nipkow@10236
    40
-> simplify proof of part1 in Inductive/AB.thy
nipkow@10186
    41
nipkow@10177
    42
Minor fixes in the tutorial
nipkow@10177
    43
===========================
nipkow@10177
    44
nipkow@10177
    45
replace simp only split by split_tac.
nipkow@10177
    46
nipkow@10177
    47
get rid of use_thy?
nipkow@10177
    48
nipkow@10177
    49
Explain typographic conventions?
nipkow@10177
    50
nipkow@10177
    51
an example of induction: !y. A --> B --> C ??
nipkow@10177
    52
nipkow@10217
    53
Advanced Ind expects rule_format incl (no_asm) (which it currently explains!
nipkow@10217
    54
Where explained?
nipkow@10177
    55
nipkow@10177
    56
Appendix: Lexical: long ids.
nipkow@10177
    57
nipkow@10177
    58
Warning: infixes automatically become reserved words!
nipkow@10177
    59
nipkow@10177
    60
Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof?
nipkow@10177
    61
nipkow@10177
    62
mention split_split in advanced pair section.
nipkow@10177
    63
nipkow@10177
    64
recdef with nested recursion: either an example or at least a pointer to the
nipkow@10177
    65
literature. In Recdef/termination.thy, at the end.
nipkow@10177
    66
%FIXME, with one exception: nested recursion.
nipkow@10177
    67
nipkow@10186
    68
Syntax section: syntax annotations nor just for consts but also for constdefs and datatype.
nipkow@10186
    69
nipkow@10186
    70
Prove EU exercise in CTL.
nipkow@10177
    71
nipkow@10177
    72
nipkow@10177
    73
Minor additions to the tutorial, unclear where
nipkow@10177
    74
==============================================
nipkow@10177
    75
nipkow@10186
    76
Tacticals: , ? +
nipkow@10177
    77
nipkow@10186
    78
"typedecl" is used in CTL/Base, but where is it introduced?
nipkow@10186
    79
In More Types chapter? Rephrase the CTL bit accordingly.
nipkow@10177
    80
nipkow@10177
    81
print_simpset (-> print_simps?)
nipkow@10177
    82
(Another subsection Useful theorems, methods, and commands?)
nipkow@10177
    83
nipkow@10177
    84
Mention that simp etc (big step tactics) insist on change?
nipkow@10177
    85
nipkow@10177
    86
Explain what "by" and "." really do, and introduce "done".
nipkow@10177
    87
nipkow@10177
    88
A list of further useful commands (rules? tricks?)
nipkow@10177
    89
prefer, defer
nipkow@10177
    90
nipkow@10177
    91
An overview of the automatic methods: simp, auto, fast, blast, force,
nipkow@10177
    92
clarify, clarsimp (intro, elim?)
nipkow@10177
    93
nipkow@10177
    94
explain rulify before induction section?
nipkow@10177
    95
nipkow@10177
    96
demonstrate x : set xs in Sets. Or Tricks chapter?
nipkow@10177
    97
nipkow@10177
    98
Appendix with HOL keywords. Say something about other keywords.
nipkow@10177
    99
nipkow@10177
   100
nipkow@10177
   101
Possible exercises
nipkow@10177
   102
==================
nipkow@10177
   103
nipkow@10177
   104
Exercises
nipkow@10177
   105
%\begin{exercise}
nipkow@10177
   106
%Extend expressions by conditional expressions.
nipkow@10177
   107
braucht wfrec!
nipkow@10177
   108
%\end{exercise}
nipkow@10177
   109
nipkow@10177
   110
Nested inductive datatypes: another example/exercise:
nipkow@10177
   111
 size(t) <= size(subst s t)?
nipkow@10177
   112
nipkow@10177
   113
insertion sort: primrec, later recdef
nipkow@10177
   114
nipkow@10177
   115
OTree:
nipkow@10177
   116
 first version only for non-empty trees:
nipkow@10177
   117
 Tip 'a | Node tree tree
nipkow@10177
   118
 Then real version?
nipkow@10177
   119
 First primrec, then recdef?
nipkow@10177
   120
nipkow@10177
   121
Ind. sets: define ABC inductively and prove
nipkow@10177
   122
ABC = {rep A n @ rep B n @ rep C n. True}
nipkow@10177
   123
nipkow@10177
   124
Possible examples/case studies
nipkow@10177
   125
==============================
nipkow@10177
   126
nipkow@10177
   127
Trie: Define functional version
nipkow@10177
   128
datatype ('a,'b)trie = Trie ('b option) ('a => ('a,'b)trie option)
nipkow@10177
   129
lookup t [] = value t
nipkow@10177
   130
lookup t (a#as) = case tries t a of None => None | Some s => lookup s as
nipkow@10177
   131
Maybe as an exercise?
nipkow@10177
   132
nipkow@10177
   133
Trie: function for partial matches (prefixes). Needs sets for spec/proof.
nipkow@10177
   134
nipkow@10177
   135
Sets via ordered list of intervals. (Isa/Interval(2))
nipkow@10177
   136
nipkow@10177
   137
Sets: PDL and CTL
nipkow@10177
   138
nipkow@10177
   139
Ind. defs: Grammar (for same number of as and bs),
nipkow@10177
   140
propositional logic (soundness and completeness?),
nipkow@10177
   141
predicate logic (soundness?),
nipkow@10177
   142
CTL proof.
nipkow@10177
   143
nipkow@10177
   144
Tautology checker. Based on Ifexpr or prop.logic?
nipkow@10177
   145
Include forward reference in relevant section.
nipkow@10177
   146
nipkow@10177
   147
Sorting with comp-parameter and with type class (<)
nipkow@10177
   148
nipkow@10177
   149
New book by Bird?
nipkow@10177
   150
nipkow@10177
   151
Steps Towards Mechanizing Program Transformations Using PVS by N. Shankar,
nipkow@10177
   152
      Science of Computer Programming, 26(1-3):33-57, 1996. 
nipkow@10177
   153
You can get it from http://www.csl.sri.com/scp95.html
nipkow@10177
   154
nipkow@10177
   155
J Moore article Towards a ...
nipkow@10177
   156
Mergesort, JVM
nipkow@10177
   157
nipkow@10177
   158
nipkow@10177
   159
Additional topics
nipkow@10177
   160
=================
nipkow@10177
   161
nipkow@10177
   162
Beef up recdef (see below).
nipkow@10177
   163
Nested recursion? Mutual recursion?
nipkow@10177
   164
nipkow@10177
   165
Nested inductive datatypes: better recursion and induction
nipkow@10177
   166
(see below)
nipkow@10177
   167
nipkow@10177
   168
Extensionality: applications in
nipkow@10177
   169
- boolean expressions: valif o bool2if = value
nipkow@10177
   170
- Advanced datatypes exercise subst (f o g) = subst f o subst g
nipkow@10177
   171
nipkow@10177
   172
A look at the library?
nipkow@10177
   173
Functions. Relations. Lfp/Gfp. Map.
nipkow@10177
   174
If WF is discussed, make a link to it from AdvancedInd.
nipkow@10177
   175
nipkow@10177
   176
Prototyping?
nipkow@10177
   177
nipkow@10177
   178
nipkow@10177
   179
Isabelle
nipkow@10177
   180
========
nipkow@10177
   181
nipkow@10177
   182
Get rid of function name in recdef header
nipkow@10177
   183
nipkow@10177
   184
More predefined functions for datatypes: map?
nipkow@10177
   185
nipkow@10177
   186
1 and 2 on nat?
nipkow@10177
   187
nipkow@10177
   188
nipkow@10177
   189
==============================================================
nipkow@10177
   190
Nested inductive datatypes: better recursion and induction
nipkow@10177
   191
nipkow@10177
   192
Show how to derive simpler primrec functions using eg map. Text:
nipkow@10177
   193
nipkow@10177
   194
Returning to the definition of \texttt{subst}, we have to admit that it does
nipkow@10177
   195
not really need the auxiliary \texttt{substs} function. The \texttt{App}-case
nipkow@10177
   196
can directly be expressed as
nipkow@10177
   197
\begin{ttbox}
nipkow@10177
   198
\input{Datatype/appmap}\end{ttbox}
nipkow@10177
   199
Although Isabelle insists on the more verbose version, we can easily {\em
nipkow@10177
   200
  prove} that the \texttt{map}-equation holds: simply by induction on
nipkow@10177
   201
\texttt{ts} followed by \texttt{Auto_tac}.
nipkow@10177
   202
lemma "subst s (App f ts) = App f (map (subst s) ts)";
nipkow@10177
   203
by(induct_tac ts, auto);
nipkow@10177
   204
nipkow@10177
   205
Now explain how to remove old eqns from simpset by naming them.
nipkow@10177
   206
But: the new eqn only helps if the induction schema is also modified
nipkow@10177
   207
accordingly:
nipkow@10177
   208
nipkow@10177
   209
val prems =
nipkow@10177
   210
Goal "[| !!v. P(Var v); !!f ts. (!!t. t : set ts ==> P t) ==> P(App f ts) |] \
nipkow@10177
   211
\     ==> P t & (!t: set ts. P t)";
nipkow@10177
   212
by(induct_tac "t ts" 1);
nipkow@10177
   213
brs prems 1;
nipkow@10177
   214
brs prems 1;
nipkow@10177
   215
by(Blast_tac 1);
nipkow@10177
   216
by(Simp_tac 1);
nipkow@10177
   217
by(Asm_simp_tac 1);
nipkow@10177
   218
nipkow@10177
   219
Now the following exercise has an easy proof:
nipkow@10177
   220
nipkow@10177
   221
\begin{exercise}
nipkow@10177
   222
  Define a function \texttt{rev_term} of type \texttt{term -> term} that
nipkow@10177
   223
  recursively reverses the order of arguments of all function symbols in a
nipkow@10177
   224
  term. Prove that \texttt{rev_term(rev_term t) = t}.
nipkow@10177
   225
\end{exercise}
nipkow@10177
   226
nipkow@10177
   227
==============================================================
nipkow@10177
   228
Recdef:
nipkow@10177
   229
nipkow@10177
   230
nested recursion
nipkow@10177
   231
more example proofs:
nipkow@10177
   232
 if-normalization with measure function,
nipkow@10177
   233
 nested if-normalization,
nipkow@10177
   234
 quicksort
nipkow@10177
   235
 Trie?
nipkow@10177
   236
a case study?
nipkow@10177
   237
nipkow@10177
   238
A separate subsection on recdef beyond measure, eg <*lex*> and psubset.
nipkow@10177
   239
Example: some finite fixpoint computation? MC, Grammar?
nipkow@10177
   240
How to modify wf-prover?
nipkow@10177
   241
nipkow@10177
   242
----------
nipkow@10177
   243
nipkow@10177
   244
Partial rekursive functions / Nontermination
nipkow@10177
   245
nipkow@10177
   246
What appears to be the problem:
nipkow@10177
   247
axiom f n = f n + 1
nipkow@10177
   248
lemma False
nipkow@10177
   249
apply(cut_facts_tac axiom, simp).
nipkow@10177
   250
nipkow@10177
   251
1. Guarded recursion
nipkow@10177
   252
nipkow@10177
   253
Scheme:
nipkow@10177
   254
f x = if $x \in dom(f)$ then ... else arbitrary
nipkow@10177
   255
nipkow@10177
   256
Example: sum/fact: int -> int (for no good reason because we have nat)
nipkow@10177
   257
nipkow@10177
   258
Exercise: ?! f. !i. f i = if i=0 then 1 else i*f(i-1)
nipkow@10177
   259
(What about sum? Is there one, a unique one?)
nipkow@10177
   260
nipkow@10177
   261
[Alternative: include argument that is counted down
nipkow@10177
   262
 f x n = if n=0 then None else ...
nipkow@10177
   263
Refer to Boyer and Moore]
nipkow@10177
   264
nipkow@10177
   265
More complex: same_fst
nipkow@10177
   266
nipkow@10177
   267
chase(f,x) = if wf{(f x,x) . f x ~= x}
nipkow@10177
   268
             then if f x = x then x else chase(f,f x)
nipkow@10177
   269
             else arb
nipkow@10177
   270
nipkow@10177
   271
Prove wf ==> f(chase(f,x)) = chase(f,x)
nipkow@10177
   272
nipkow@10177
   273
2. While / Tail recursion
nipkow@10177
   274
nipkow@10177
   275
chase f x = fst(while (%(x,fx). x=fx) (%(x,fx). (fx,f fx)) (x,f x))
nipkow@10177
   276
nipkow@10177
   277
==> unfold eqn for chase? Prove fixpoint property?
nipkow@10177
   278
nipkow@10177
   279
Better(?) sum i = fst(while (%(s,i). i=0) (%(s,i). (s+i,i-1)) (0,i))
nipkow@10177
   280
Prove 0 <= i ==> sum i = i*(i+1) via while-rule
nipkow@10177
   281
nipkow@10177
   282
Mention prototyping?
nipkow@10177
   283
==============================================================