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

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

4 Relation: comp -> composition

6 replace "simp only split" by "split_tac".

8 Add map_cong?? (upto 10% slower)

10 Recdef: Get rid of function name in header.

11 Support mutual recursion (Konrad?)

13 use arith_tac in recdef to solve termination conditions?

14 -> new example in Recdef/termination

16 a tactic for replacing a specific occurrence:

17 apply(substitute [2] thm)

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

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

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

24 More predefined functions for datatypes: map?

26 Induction rules for int: int_le/ge_induct?

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

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

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

32 proper mutual simplification

34 defs with = and pattern matching??

37 Minor fixes in the tutorial

38 ===========================

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

41 Index the notion and maybe the rules contrapos_xy

43 Even: forward ref from problem with "Suc(Suc n) : even" to general solution in

44 AdvancedInd section.

46 get rid of use_thy in tutorial?

48 Explain typographic conventions?

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

51 bounded quantifers ALL x<y, <=.

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

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

56 -> Types/typedef

58 Appendix: Lexical: long ids.

60 Warning: infixes automatically become reserved words!

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

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.

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

70 Appendix with list functions.

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}

77 Minor additions to the tutorial, unclear where

78 ==============================================

80 Tacticals: , ? +

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

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

85 does more.)

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

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

90 An overview of the automatic methods: simp, auto, fast, blast, force,

91 clarify, clarsimp (intro, elim?)

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.

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

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

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

104 Possible exercises

105 ==================

107 Exercises

108 %\begin{exercise}

109 %Extend expressions by conditional expressions.

110 braucht wfrec!

111 %\end{exercise}

113 Nested inductive datatypes: another example/exercise:

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

116 insertion sort: primrec, later recdef

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?

124 Ind. sets: define ABC inductively and prove

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

127 Possible examples/case studies

128 ==============================

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?

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

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

140 propositional logic (soundness and completeness?),

141 predicate logic (soundness?),

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

144 Include forward reference in relevant section.

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

148 New book by Bird?

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

154 J Moore article Towards a ...

155 Mergesort, JVM

158 Additional topics

159 =================

161 Recdef with nested recursion?

163 Extensionality: applications in

164 - boolean expressions: valif o bool2if = value

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

167 A look at the library?

168 Map.

169 If WF is discussed, make a link to it from AdvancedInd.

171 Prototyping?

173 ==============================================================

174 Recdef:

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?

184 ----------

186 Partial rekursive functions / Nontermination

188 What appears to be the problem:

189 axiom f n = f n + 1

190 lemma False

191 apply(cut_facts_tac axiom, simp).

193 1. Guarded recursion

195 Scheme:

196 f x = if $x \in dom(f)$ then ... else arbitrary

198 Example: sum/fact: int -> int (for no good reason because we have nat)

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

203 [Alternative: include argument that is counted down

204 f x n = if n=0 then None else ...

205 Refer to Boyer and Moore]

207 More complex: same_fst

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

213 Prove wf ==> f(chase(f,x)) = chase(f,x)

215 2. While / Tail recursion

217 chase f x = fst(while (%(x,fx). x=fx) (%(x,fx). (fx,f fx)) (x,f x))

219 ==> unfold eqn for chase? Prove fixpoint property?

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

224 Mention prototyping?

225 ==============================================================