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