summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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 ==============

4 Relation: comp -> composition

6 Add map_cong?? (upto 10% slower)

8 Recdef: Get rid of function name in header.

9 Support mutual recursion (Konrad?)

11 use arith_tac in recdef to solve termination conditions?

12 -> new example in Recdef/termination

14 a tactic for replacing a specific occurrence:

15 apply(subst [2] thm)

17 it would be nice if @term could deal with ?-vars.

18 then a number of (unchecked!) @texts could be converted to @terms.

20 it would be nice if one could get id to the enclosing quotes in the [source] option.

22 More predefined functions for datatypes: map?

24 Induction rules for int: int_le/ge_induct?

25 Needed for ifak example. But is that example worth it?

27 Komischerweise geht das Splitten von _Annahmen_ auch mit simp_tac, was

28 ein generelles Feature ist, das man vielleicht mal abstellen sollte.

30 proper mutual simplification

32 defs with = and pattern matching??

35 Minor fixes in the tutorial

36 ===========================

38 adjust type of ^ in tab:overloading

40 explanation of term "contrapositive"/contraposition in Rules?

41 Index the notion and maybe the rules contrapos_xy

43 If Advanced and Types chapter ar swapped:

44 Make forward ref from ... = True in Axioms to preprocessor section.

46 get rid of use_thy in tutorial?

48 Orderings on numbers (with hint that it is overloaded):

49 bounded quantifers ALL x<y, <=.

51 an example of induction: !y. A --> B --> C ??

53 Explain type_definition and mention pre-proved thms in subset.thy?

54 -> Types/typedef

56 Appendix: Lexical: long ids.

58 Warning: infixes automatically become reserved words!

60 Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof?

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.

66 Syntax section: syntax annotations nor just for consts but also for constdefs and datatype.

68 Appendix with list functions.

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}

75 Minor additions to the tutorial, unclear where

76 ==============================================

78 Tacticals: , ? +

79 Note: + is used in typedef section!

81 Mention that simp etc (big step tactics) insist on change?

83 Rules: Introduce "by" (as a kind of shorthand for apply+done, except that it

84 does more.)

86 A list of further useful commands (rules? tricks?)

87 prefer, defer, print_simpset (-> print_simps?)

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.

93 Where is "simplified" explained? Needed by Inductive/AB.thy

95 demonstrate x : set xs in Sets. Or Tricks chapter?

97 Appendix with HOL keywords. Say something about other keywords.

100 Possible exercises

101 ==================

103 Exercises

104 %\begin{exercise}

105 %Extend expressions by conditional expressions.

106 braucht wfrec!

107 %\end{exercise}

109 Nested inductive datatypes: another example/exercise:

110 size(t) <= size(subst s t)?

112 insertion sort: primrec, later recdef

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?

120 Ind. sets: define ABC inductively and prove

121 ABC = {rep A n @ rep B n @ rep C n. True}

123 Partial rekursive functions / Nontermination:

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?)

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

132 Possible examples/case studies

133 ==============================

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?

141 Trie: function for partial matches (prefixes). Needs sets for spec/proof.

143 Sets via ordered list of intervals. (Isa/Interval(2))

145 propositional logic (soundness and completeness?),

146 predicate logic (soundness?),

148 Tautology checker. Based on Ifexpr or prop.logic?

149 Include forward reference in relevant section.

151 Sorting with comp-parameter and with type class (<)

153 Recdef:more example proofs:

154 if-normalization with measure function,

155 nested if-normalization,

156 quicksort

157 Trie?

159 New book by Bird?

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

165 J Moore article Towards a ...

166 Mergesort, JVM

169 Additional topics

170 =================

172 Recdef with nested recursion?

174 Extensionality: applications in

175 - boolean expressions: valif o bool2if = value

176 - Advanced datatypes exercise subst (f o g) = subst f o subst g

178 A look at the library?

179 Map.

181 Prototyping?

183 ==============================================================