4 Add map_cong?? (upto 10% slower)
6 a simp command for terms
8 Recdef: Get rid of function name in header.
9 Support mutual recursion (Konrad?)
11 improve solver in simplifier: treat & and ! ...
14 !x. !y. x = f y --> P x y should reduce to !y. P (f y) y.
16 it would be nice if @term could deal with ?-vars.
17 then a number of (unchecked!) @texts could be converted to @terms.
19 it would be nice if one could get id to the enclosing quotes in the [source] option.
21 More predefined functions for datatypes: map?
23 Induction rules for int: int_le/ge_induct?
24 Needed for ifak example. But is that example worth it?
26 Komischerweise geht das Splitten von _Annahmen_ auch mit simp_tac, was
27 ein generelles Feature ist, das man vielleicht mal abstellen sollte.
29 proper mutual simplification
31 defs with = and pattern matching??
34 Minor fixes in the tutorial
35 ===========================
37 Appendix: Lexical: long ids.
39 Warning: infixes automatically become reserved words!
41 Syntax section: syntax annotations not just for consts but also for constdefs and datatype.
43 Appendix with list functions.
45 All theory sources on the web?
52 For extensionality (in Sets chapter): prove
54 in If-expression case study (Ifexpr)
56 Nested inductive datatypes: another example/exercise:
57 size(t) <= size(subst s t)?
59 insertion sort: primrec, later recdef
62 first version only for non-empty trees:
63 Tip 'a | Node tree tree
65 First primrec, then recdef?
67 Ind. sets: define ABC inductively and prove
68 ABC = {rep A n @ rep B n @ rep C n. True}
70 Partial rekursive functions / Nontermination:
72 Exercise: ?! f. !i. f i = if i=0 then 1 else i*f(i-1)
73 (What about sum? Is there one, a unique one?)
76 Better(?) sum i = fst(while (%(s,i). i=0) (%(s,i). (s+i,i-1)) (0,i))
77 Prove 0 <= i ==> sum i = i*(i+1) via while-rule
79 Possible examples/case studies
80 ==============================
82 Trie: Define functional version
83 datatype ('a,'b)trie = Trie ('b option) ('a => ('a,'b)trie option)
85 lookup t (a#as) = case tries t a of None => None | Some s => lookup s as
88 Trie: function for partial matches (prefixes). Needs sets for spec/proof.
90 Sets via ordered list of intervals. (Isa/Interval(2))
92 propositional logic (soundness and completeness?),
93 predicate logic (soundness?),
95 Tautology checker. Based on Ifexpr or prop.logic?
96 Include forward reference in relevant section.
98 Sorting with comp-parameter and with type class (<)
100 Recdef:more example proofs:
101 if-normalization with measure function,
102 nested if-normalization,
108 Steps Towards Mechanizing Program Transformations Using PVS by N. Shankar,
109 Science of Computer Programming, 26(1-3):33-57, 1996.
110 You can get it from http://www.csl.sri.com/scp95.html
112 J Moore article Towards a ...
119 Recdef with nested recursion?
121 Extensionality: applications in
122 - boolean expressions: valif o bool2if = value
123 - Advanced datatypes exercise subst (f o g) = subst f o subst g
125 A look at the library?
130 ==============================================================