Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-19 20:43:05 -0800 (Mon, 19 Dec 2005)
Revision: 8329
Log message:

      Well, this is a (very) partial approach to using list_of_fun
      by itself.
      
      I really believe this is absurd.  This approach is grundge-driven.
      In contrast, the vlist{| ... |} approach is purely forward-directed,
      reduce-driven, no destructor-driven tactics.
      
      With the direct list_of_fun approach, you need non-reduce-driven
      tactics like splitITE.  Here is an example.
      
         mk_bterm{'n; 'op; list_of_fun{i.
            bind{'m; x. if i = 0 then e0
                        else if i = 1 then e1
                        ...
                        else if i = n then en}; 'k}}
         --> grundge forward and push the bind into the ITE
         (hard to express in canonical form)
      
      So now, to prove compatible_shapes, split apart the operator shape;
      do a bunch of ITE reductions, etc.  Very grundgy.
      
      Now consider the vlist approach.
      
         mk_bterm{'n; 'op; subterms_bind{bind{'m; x. vlist{| e0[x]; ... en[x] |}}}}
         --> reduce subterms_bind (yes, that is a _reduce_)
         mk_bterm{'n; 'op; vlist{| bind{'m; x. e0[x]}; ...; bind{'m; x. en[x]} |}}
      
      Now *that* is obvious and beautiful.
      
      Here is the dogma I am espousing:
         - Express each transformation in its natural form.
         - It is preferable to implement as much of a transformation
           as possible with *theorems*, rather than tactics.
      
      Of course, the vlist implementation relies on list_of_fun.  However, I
      suggest that list_of_fun be viewed as assembly code, not to be purported
      to be ideal in all situations.
      
      Of course, I just want it to be beautiful.  If there is a beautiful
      list_of_fun approach, I'm all for it.  If I may ask, once you have done
      your coding, do a _serious_ comparison.