Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-06 18:03:10 -0800 (Sun, 06 Nov 2005)
Revision: 8116
Log message:

      Returned to requiring wf of sequents, so that we don't need wf-subgoals
      in the object logic.
      
      This mostly completes the initial phase of the Filter_parse reflection.
      You can define a logic of syntax, or a logic of rules, or any mixture.
      
         reflected_logic foo_logic =
         struct
            declare typeclass AExp
            declare typeclass BExp
      
            declare A : AExp
            declare B{'e : AExp} : AExp
            declare C{a: AExp. 'e['a] : BExp} : BExp
      
            interactive c_intro :
               sequent { <H>; a: A >- 'e['a] } -->
               sequent { <H> >- C{a. 'e['a]} }
         end
      
      Declarations are processed as normal in this block, plus 3 new parts
      are added.  Only the reflected rule makes sense.
      
      Each declaration/rule produces 3 parts:
         1. A definition (unfold_X : X <--> <definition>)
         2. A wf-goal (interactive X_wf : X in ProofRule)
         3. An ITT rule:
            interactive X_itt :
               <H1> >- Provable{$`(<H>; a: A >- e[a])} -->
               <H1> >- Provable{$`(<H> >- C{a. e[a]})}
      
      Plus you get the complete logic, containing all the rules
      that were defined (an no others).
      
         define foo_logic <--> [A; B; C; c_intro]
         define Provable{'e} <-->
            Itt_hoas_sequent_native!Provable{Sequent; foo_logic; 'e}
      
      I haven't proved any theorems, so we'll see how that goes.