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 ***
     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 get rid of use_thy in tutorial?
    44 
    45 Orderings on numbers (with hint that it is overloaded):
    46 bounded quantifers ALL x<y, <=.
    47 
    48 an example of induction: !y. A --> B --> C ??
    49 
    50 Explain type_definition and mention pre-proved thms in subset.thy?
    51 -> Types/typedef
    52 
    53 Appendix: Lexical: long ids.
    54 
    55 Warning: infixes automatically become reserved words!
    56 
    57 Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof?
    58 
    59 recdef with nested recursion: either an example or at least a pointer to the
    60 literature. In Recdef/termination.thy, at the end.
    61 %FIXME, with one exception: nested recursion.
    62 
    63 Syntax section: syntax annotations nor just for consts but also for constdefs and datatype.
    64 
    65 Appendix with list functions.
    66 
    67 Move section on rule inversion further to the front, and combine
    68 \subsection{Universal quantifiers in introduction rules}
    69 \subsection{Continuing the `ground terms' example}
    70 
    71 
    72 Minor additions to the tutorial, unclear where
    73 ==============================================
    74 
    75 unfold?
    76 
    77 Tacticals: , ? +
    78 Note: + is used in typedef section!
    79 
    80 A list of further useful commands (rules? tricks?)
    81 prefer, defer, print_simpset (-> print_simps?)
    82 
    83 demonstrate x : set xs in Sets. Or Tricks chapter?
    84 
    85 Appendix with HOL and Isar keywords.
    86 
    87 
    88 Possible exercises
    89 ==================
    90 
    91 Exercises
    92 
    93 For extensionality (in Sets chapter): prove
    94 valif o norm = valif
    95 in If-expression case study (Ifexpr)
    96 
    97 Nested inductive datatypes: another example/exercise:
    98  size(t) <= size(subst s t)?
    99 
   100 insertion sort: primrec, later recdef
   101 
   102 OTree:
   103  first version only for non-empty trees:
   104  Tip 'a | Node tree tree
   105  Then real version?
   106  First primrec, then recdef?
   107 
   108 Ind. sets: define ABC inductively and prove
   109 ABC = {rep A n @ rep B n @ rep C n. True}
   110 
   111 Partial rekursive functions / Nontermination:
   112 
   113 Exercise: ?! f. !i. f i = if i=0 then 1 else i*f(i-1)
   114 (What about sum? Is there one, a unique one?)
   115 
   116 Exercise
   117 Better(?) sum i = fst(while (%(s,i). i=0) (%(s,i). (s+i,i-1)) (0,i))
   118 Prove 0 <= i ==> sum i = i*(i+1) via while-rule
   119 
   120 Possible examples/case studies
   121 ==============================
   122 
   123 Trie: Define functional version
   124 datatype ('a,'b)trie = Trie ('b option) ('a => ('a,'b)trie option)
   125 lookup t [] = value t
   126 lookup t (a#as) = case tries t a of None => None | Some s => lookup s as
   127 Maybe as an exercise?
   128 
   129 Trie: function for partial matches (prefixes). Needs sets for spec/proof.
   130 
   131 Sets via ordered list of intervals. (Isa/Interval(2))
   132 
   133 propositional logic (soundness and completeness?),
   134 predicate logic (soundness?),
   135 
   136 Tautology checker. Based on Ifexpr or prop.logic?
   137 Include forward reference in relevant section.
   138 
   139 Sorting with comp-parameter and with type class (<)
   140 
   141 Recdef:more example proofs:
   142  if-normalization with measure function,
   143  nested if-normalization,
   144  quicksort
   145  Trie?
   146 
   147 New book by Bird?
   148 
   149 Steps Towards Mechanizing Program Transformations Using PVS by N. Shankar,
   150       Science of Computer Programming, 26(1-3):33-57, 1996. 
   151 You can get it from http://www.csl.sri.com/scp95.html
   152 
   153 J Moore article Towards a ...
   154 Mergesort, JVM
   155 
   156 
   157 Additional topics
   158 =================
   159 
   160 Recdef with nested recursion?
   161 
   162 Extensionality: applications in
   163 - boolean expressions: valif o bool2if = value
   164 - Advanced datatypes exercise subst (f o g) = subst f o subst g
   165 
   166 A look at the library?
   167 Map.
   168 
   169 Prototyping?
   170 
   171 ==============================================================