1.1 --- a/doc-src/TutorialI/todo.tobias	Wed Dec 13 09:32:55 2000 +0100
     1.2 +++ b/doc-src/TutorialI/todo.tobias	Wed Dec 13 09:39:53 2000 +0100
     1.3 @@ -3,8 +3,6 @@
     1.4  
     1.5  Relation: comp -> composition
     1.6  
     1.7 -replace "simp only split" by "split_tac".
     1.8 -
     1.9  Add map_cong?? (upto 10% slower)
    1.10  
    1.11  Recdef: Get rid of function name in header.
    1.12 @@ -14,7 +12,7 @@
    1.13  -> new example in Recdef/termination
    1.14  
    1.15  a tactic for replacing a specific occurrence:
    1.16 -apply(substitute [2] thm)
    1.17 +apply(subst [2] thm)
    1.18  
    1.19  it would be nice if @term could deal with ?-vars.
    1.20  then a number of (unchecked!) @texts could be converted to @terms.
    1.21 @@ -37,16 +35,16 @@
    1.22  Minor fixes in the tutorial
    1.23  ===========================
    1.24  
    1.25 +adjust type of ^ in tab:overloading
    1.26 +
    1.27  explanation of term "contrapositive"/contraposition in Rules?
    1.28  Index the notion and maybe the rules contrapos_xy
    1.29  
    1.30 -Even: forward ref from problem with "Suc(Suc n) : even" to general solution in
    1.31 -AdvancedInd section.
    1.32 +If Advanced and Types chapter ar swapped:
    1.33 +Make forward ref from ... = True in Axioms to preprocessor section.
    1.34  
    1.35  get rid of use_thy in tutorial?
    1.36  
    1.37 -Explain typographic conventions?
    1.38 -
    1.39  Orderings on numbers (with hint that it is overloaded):
    1.40  bounded quantifers ALL x<y, <=.
    1.41  
    1.42 @@ -78,6 +76,7 @@
    1.43  ==============================================
    1.44  
    1.45  Tacticals: , ? +
    1.46 +Note: + is used in typedef section!
    1.47  
    1.48  Mention that simp etc (big step tactics) insist on change?
    1.49  
    1.50 @@ -87,9 +86,6 @@
    1.51  A list of further useful commands (rules? tricks?)
    1.52  prefer, defer, print_simpset (-> print_simps?)
    1.53  
    1.54 -An overview of the automatic methods: simp, auto, fast, blast, force,
    1.55 -clarify, clarsimp (intro, elim?)
    1.56 -
    1.57  Advanced Ind expects rule_format incl (no_asm) (which it currently explains!)
    1.58  Where explained? Should go into a separate section as Inductive needs it as
    1.59  well.
    1.60 @@ -124,6 +120,15 @@
    1.61  Ind. sets: define ABC inductively and prove
    1.62  ABC = {rep A n @ rep B n @ rep C n. True}
    1.63  
    1.64 +Partial rekursive functions / Nontermination:
    1.65 +
    1.66 +Exercise: ?! f. !i. f i = if i=0 then 1 else i*f(i-1)
    1.67 +(What about sum? Is there one, a unique one?)
    1.68 +
    1.69 +Exercise
    1.70 +Better(?) sum i = fst(while (%(s,i). i=0) (%(s,i). (s+i,i-1)) (0,i))
    1.71 +Prove 0 <= i ==> sum i = i*(i+1) via while-rule
    1.72 +
    1.73  Possible examples/case studies
    1.74  ==============================
    1.75  
    1.76 @@ -145,6 +150,12 @@
    1.77  
    1.78  Sorting with comp-parameter and with type class (<)
    1.79  
    1.80 +Recdef:more example proofs:
    1.81 + if-normalization with measure function,
    1.82 + nested if-normalization,
    1.83 + quicksort
    1.84 + Trie?
    1.85 +
    1.86  New book by Bird?
    1.87  
    1.88  Steps Towards Mechanizing Program Transformations Using PVS by N. Shankar,
    1.89 @@ -166,60 +177,7 @@
    1.90  
    1.91  A look at the library?
    1.92  Map.
    1.93 -If WF is discussed, make a link to it from AdvancedInd.
    1.94  
    1.95  Prototyping?
    1.96  
    1.97  ==============================================================
    1.98 -Recdef:
    1.99 -
   1.100 -nested recursion
   1.101 -more example proofs:
   1.102 - if-normalization with measure function,
   1.103 - nested if-normalization,
   1.104 - quicksort
   1.105 - Trie?
   1.106 -a case study?
   1.107 -
   1.108 -----------
   1.109 -
   1.110 -Partial rekursive functions / Nontermination
   1.111 -
   1.112 -What appears to be the problem:
   1.113 -axiom f n = f n + 1
   1.114 -lemma False
   1.115 -apply(cut_facts_tac axiom, simp).
   1.116 -
   1.117 -1. Guarded recursion
   1.118 -
   1.119 -Scheme:
   1.120 -f x = if $x \in dom(f)$ then ... else arbitrary
   1.121 -
   1.122 -Example: sum/fact: int -> int (for no good reason because we have nat)
   1.123 -
   1.124 -Exercise: ?! f. !i. f i = if i=0 then 1 else i*f(i-1)
   1.125 -(What about sum? Is there one, a unique one?)
   1.126 -
   1.127 -[Alternative: include argument that is counted down
   1.128 - f x n = if n=0 then None else ...
   1.129 -Refer to Boyer and Moore]
   1.130 -
   1.131 -More complex: same_fst
   1.132 -
   1.133 -chase(f,x) = if wf{(f x,x) . f x ~= x}
   1.134 -             then if f x = x then x else chase(f,f x)
   1.135 -             else arb
   1.136 -
   1.137 -Prove wf ==> f(chase(f,x)) = chase(f,x)
   1.138 -
   1.139 -2. While / Tail recursion
   1.140 -
   1.141 -chase f x = fst(while (%(x,fx). x=fx) (%(x,fx). (fx,f fx)) (x,f x))
   1.142 -
   1.143 -==> unfold eqn for chase? Prove fixpoint property?
   1.144 -
   1.145 -Better(?) sum i = fst(while (%(s,i). i=0) (%(s,i). (s+i,i-1)) (0,i))
   1.146 -Prove 0 <= i ==> sum i = i*(i+1) via while-rule
   1.147 -
   1.148 -Mention prototyping?
   1.149 -==============================================================