nipkow@10281: Implementation
nipkow@10281: ==============
nipkow@10177: 
nipkow@10608: Relation: comp -> composition
nipkow@10177: 
nipkow@10177: Add map_cong?? (upto 10% slower)
nipkow@10177: 
nipkow@10281: Recdef: Get rid of function name in header.
nipkow@10281: Support mutual recursion (Konrad?)
nipkow@10177: 
nipkow@10177: use arith_tac in recdef to solve termination conditions?
nipkow@10177: -> new example in Recdef/termination
nipkow@10177: 
nipkow@10177: a tactic for replacing a specific occurrence:
nipkow@10654: apply(subst [2] thm)
nipkow@10177: 
nipkow@10186: it would be nice if @term could deal with ?-vars.
nipkow@10186: then a number of (unchecked!) @texts could be converted to @terms.
nipkow@10186: 
nipkow@10189: it would be nice if one could get id to the enclosing quotes in the [source] option.
nipkow@10189: 
nipkow@10281: More predefined functions for datatypes: map?
nipkow@10281: 
nipkow@10281: Induction rules for int: int_le/ge_induct?
nipkow@10281: Needed for ifak example. But is that example worth it?
nipkow@10281: 
nipkow@10608: Komischerweise geht das Splitten von _Annahmen_ auch mit simp_tac, was
nipkow@10608: ein generelles Feature ist, das man vielleicht mal abstellen sollte.
nipkow@10608: 
nipkow@10520: proper mutual simplification
nipkow@10520: 
nipkow@10520: defs with = and pattern matching??
nipkow@10340: 
nipkow@10186: 
nipkow@10177: Minor fixes in the tutorial
nipkow@10177: ===========================
nipkow@10177: 
nipkow@10983: Adjust FP textbook refs: new Bird, Hudak
nipkow@10983: Discrete math textbook: Rosen?
nipkow@10983: 
nipkow@10983: say something about "abbreviations" when defs are introduced.
nipkow@10983: 
nipkow@10654: adjust type of ^ in tab:overloading
nipkow@10654: 
nipkow@10177: an example of induction: !y. A --> B --> C ??
nipkow@10177: 
nipkow@10509: Explain type_definition and mention pre-proved thms in subset.thy?
nipkow@10509: -> Types/typedef
nipkow@10509: 
nipkow@10177: Appendix: Lexical: long ids.
nipkow@10177: 
nipkow@10177: Warning: infixes automatically become reserved words!
nipkow@10177: 
nipkow@10177: Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof?
nipkow@10177: 
nipkow@10177: recdef with nested recursion: either an example or at least a pointer to the
nipkow@10177: literature. In Recdef/termination.thy, at the end.
nipkow@10177: %FIXME, with one exception: nested recursion.
nipkow@10177: 
nipkow@10186: Syntax section: syntax annotations nor just for consts but also for constdefs and datatype.
nipkow@10186: 
nipkow@10283: Appendix with list functions.
nipkow@10283: 
nipkow@10520: Move section on rule inversion further to the front, and combine
nipkow@10520: \subsection{Universal quantifiers in introduction rules}
nipkow@10520: \subsection{Continuing the `ground terms' example}
nipkow@10520: 
nipkow@10177: 
nipkow@10177: Minor additions to the tutorial, unclear where
nipkow@10177: ==============================================
nipkow@10177: 
nipkow@10855: unfold?
nipkow@10845: 
nipkow@10177: 
nipkow@10177: Possible exercises
nipkow@10177: ==================
nipkow@10177: 
nipkow@10177: Exercises
nipkow@10971: 
nipkow@10971: For extensionality (in Sets chapter): prove
nipkow@10971: valif o norm = valif
nipkow@10971: in If-expression case study (Ifexpr)
nipkow@10177: 
nipkow@10177: Nested inductive datatypes: another example/exercise:
nipkow@10177:  size(t) <= size(subst s t)?
nipkow@10177: 
nipkow@10177: insertion sort: primrec, later recdef
nipkow@10177: 
nipkow@10177: OTree:
nipkow@10177:  first version only for non-empty trees:
nipkow@10177:  Tip 'a | Node tree tree
nipkow@10177:  Then real version?
nipkow@10177:  First primrec, then recdef?
nipkow@10177: 
nipkow@10177: Ind. sets: define ABC inductively and prove
nipkow@10177: ABC = {rep A n @ rep B n @ rep C n. True}
nipkow@10177: 
nipkow@10654: Partial rekursive functions / Nontermination:
nipkow@10654: 
nipkow@10654: Exercise: ?! f. !i. f i = if i=0 then 1 else i*f(i-1)
nipkow@10654: (What about sum? Is there one, a unique one?)
nipkow@10654: 
nipkow@10654: Exercise
nipkow@10654: Better(?) sum i = fst(while (%(s,i). i=0) (%(s,i). (s+i,i-1)) (0,i))
nipkow@10654: Prove 0 <= i ==> sum i = i*(i+1) via while-rule
nipkow@10654: 
nipkow@10177: Possible examples/case studies
nipkow@10177: ==============================
nipkow@10177: 
nipkow@10177: Trie: Define functional version
nipkow@10177: datatype ('a,'b)trie = Trie ('b option) ('a => ('a,'b)trie option)
nipkow@10177: lookup t [] = value t
nipkow@10177: lookup t (a#as) = case tries t a of None => None | Some s => lookup s as
nipkow@10177: Maybe as an exercise?
nipkow@10177: 
nipkow@10177: Trie: function for partial matches (prefixes). Needs sets for spec/proof.
nipkow@10177: 
nipkow@10177: Sets via ordered list of intervals. (Isa/Interval(2))
nipkow@10177: 
nipkow@10177: propositional logic (soundness and completeness?),
nipkow@10177: predicate logic (soundness?),
nipkow@10177: 
nipkow@10177: Tautology checker. Based on Ifexpr or prop.logic?
nipkow@10177: Include forward reference in relevant section.
nipkow@10177: 
nipkow@10177: Sorting with comp-parameter and with type class (<)
nipkow@10177: 
nipkow@10654: Recdef:more example proofs:
nipkow@10654:  if-normalization with measure function,
nipkow@10654:  nested if-normalization,
nipkow@10654:  quicksort
nipkow@10654:  Trie?
nipkow@10654: 
nipkow@10177: New book by Bird?
nipkow@10177: 
nipkow@10177: Steps Towards Mechanizing Program Transformations Using PVS by N. Shankar,
nipkow@10177:       Science of Computer Programming, 26(1-3):33-57, 1996. 
nipkow@10177: You can get it from http://www.csl.sri.com/scp95.html
nipkow@10177: 
nipkow@10177: J Moore article Towards a ...
nipkow@10177: Mergesort, JVM
nipkow@10177: 
nipkow@10177: 
nipkow@10177: Additional topics
nipkow@10177: =================
nipkow@10177: 
nipkow@10281: Recdef with nested recursion?
nipkow@10177: 
nipkow@10177: Extensionality: applications in
nipkow@10177: - boolean expressions: valif o bool2if = value
nipkow@10177: - Advanced datatypes exercise subst (f o g) = subst f o subst g
nipkow@10177: 
nipkow@10177: A look at the library?
nipkow@10281: Map.
nipkow@10177: 
nipkow@10177: Prototyping?
nipkow@10177: 
nipkow@10177: ==============================================================