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