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

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

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 get rid of use_thy in tutorial?

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

46 bounded quantifers ALL x<y, <=.

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

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

51 -> Types/typedef

53 Appendix: Lexical: long ids.

55 Warning: infixes automatically become reserved words!

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

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.

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

65 Appendix with list functions.

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}

72 Minor additions to the tutorial, unclear where

73 ==============================================

75 unfold?

77 Tacticals: , ? +

78 Note: + is used in typedef section!

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

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

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

85 Appendix with HOL and Isar keywords.

88 Possible exercises

89 ==================

91 Exercises

93 For extensionality (in Sets chapter): prove

94 valif o norm = valif

95 in If-expression case study (Ifexpr)

97 Nested inductive datatypes: another example/exercise:

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

100 insertion sort: primrec, later recdef

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?

108 Ind. sets: define ABC inductively and prove

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

111 Partial rekursive functions / Nontermination:

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

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

120 Possible examples/case studies

121 ==============================

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?

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

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

133 propositional logic (soundness and completeness?),

134 predicate logic (soundness?),

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

137 Include forward reference in relevant section.

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

141 Recdef:more example proofs:

142 if-normalization with measure function,

143 nested if-normalization,

144 quicksort

145 Trie?

147 New book by Bird?

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

153 J Moore article Towards a ...

154 Mergesort, JVM

157 Additional topics

158 =================

160 Recdef with nested recursion?

162 Extensionality: applications in

163 - boolean expressions: valif o bool2if = value

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

166 A look at the library?

167 Map.

169 Prototyping?

171 ==============================================================