===============================================================================
Example of a theory developed with ECDs.

-Basic
    *carrier-NO carrier.
    *display(). //defines a display property for the ECD (in OM).

-Setoid <-(Basic)
    *symbols 
        -eq: This->This->This
        -element: This;
    *carrier

    *assertions            
        -eq_reflexibe  (type=axiom) {
        
         }        
        -eq_symmetric  (type=axiom) {
            For all a,b,c in This.ecdDisplay
            implies(and(eq(a,b),eq(b,c)),eq(a,c))
         }
        -eq_transitive (type=axiom) {
            For all a,b,c in This.ecdDisplay
            implies(and(eq(a,b),eq(b,c)),eq(a,c))
         }
    *display()

-Monoid <- (Setoid)
    *symbols 
        -times: (This->)*->This (variable number of arguments?). 
        -one: This (constant).
        -element().times(one,one) : This (0-ary function).        
         inherited from Setoid();
    *assertions            
        one_is_neutro (type=axiom) {
            for all a in This.ecdDisplay eq(times(a,e),a).
        }
        
        times_is_associative (type=axiom) {
            for all a,b,c in This.ecdDisplay 
            eq(times(a,times(b,c)),times(times(a,b),c)).
        }

-Group <- (Monoid)
    *symbols 
        inverse: This->This
    *assertions            
        inverse_def_prop (type=axiom) {
            for all a in This.ecdDisplay
            times(a,inverse(a))=one
        }

    
-Integers <- (Monoid, Group)
    *symbols 
        plus    inherits Group.times;
        times   inherits Monoid.times;
        zero    inherits Group.one;
        one     inherits Monoid.one;
    *assertions            
        inverse_def_prop (type=axiom) {
            for all a in This.ecdDisplay
            times(a,inverse(a))=one
        }

     *Boolean carrier (string tObject) {
        if ( isOMI(tObject ) ) 
            return true;
        else
            return false;
      }
        


================================================================================
                    OBJECTIVES
                    ==========


    What do we want with the ECDs?
    
    1-Define symbols and their signatures. What are these signatures?
  
      Somehow we have to provide a way to define lambda expressions.

      We have the Small Type System for OpenMath from Davenport:

      or  

      Olga's OpenMath Strong Type System: disadvantages we need additional 
      CDs for new types

      OpenMath is used to specify the types (don't like that).


      (
        <BIND>
        </BIND>
      )


================================================================================
                    DEFINITIONS
                    ===========

-What do we define in a ECD?
    -symbols. 
            Symbols have a signature.

    -The carrier is a function accepting only one argument. It returns true 
     if the argument corresponds to an entity of the Universe. The value of the 
     argument is an XML encoded OpenMath object?

           


================================================================================
                    PROBLEMS
                    ========

-For instance, we define a theorem for monoids were all the assertions are 
 stated in terms of Monid.one and Monid.times symbols. Then in Integers we 
 define a mapping Group.times-->Integers.plus and Group.one-->Integers.zero
 then we would like to be able to get (automatically) replace * by + 
 and 1 by 0.

 (possible solution: state assertions in a parametric form).
    
  assertion( ) {
    
  }
    
  

================================================================================
                     OMDoc
                     =====

Theories.

1-<symbol>. Define OpenMath symbol. Attributes: 
    -id unique within a theory.
    -kind="type|object|sort".  (object default).
    -scope="global|local" (exported or not exported outside the theory).

    childrem:
    -<commonname lang="">name</commonname>*
    -<type system="simple-typed|sts">name</type>*

2-axioms: (specify constraints in symbols).
    Attr: 
        -id="", 
        -generated-by.
    Childrem:
        -CMP*
        -FMP

3-definition (complete meaning to groups of symbols (in term of already defined 
              ones. It's more complex than axion).

    Attributes:
        -id=""
        -for="symbol id"
        -type= 

            simple. FMP contains a formula that can be substituted for the 
            symbol specified in the for attribute.

            inductive: for inductive definition. The symbol specified in for 
            attribute may appear in the body of the FMP. Its not completely 
            clear the explanation given in omdoc.ps (at least to me).
        
            recursive: (variant of inductive case). use of <requation>
            
            <requation>
                <patern>plus(x,0)</patern>
                <value>x</value>
            </requation>
            
            <requation>
                <patern>plus(x,suc(y))</patern>
                <value>suc(plus(x,y))</value>
            </requation>

            <mesure> or <ordering> can be used to provide evidence of the 
            termination of the recursion.
            
            implicit: an implicit definition (as a solution to a set of 
            logical formulas)
            <FMP>exp'=exp ^ pex(0)=1</FMP>
            use just-by attribute of definition to point to a proof.

            'obj': an openmath object representing the object.

4-assertion. A statement (proved or not). Attributes:

            type="theorem|proposition|lemma|corollary|postulate|conjecture|
                  false-conjecture|obligation|asumption|formula"

5-<alternative>. Attributes: 

                entails, entailed-by point to definitions containing the 
                necessary entailments.

                entails-thm, entailed-by-thm. the theorem providing the 
                necessary justifications.

6-<example>  Attributes: 

            for="" definition (symbol?) of assertion for which it is an example.
            type="for|against"
            assertion="" a reference to the assetrtion that formally states
                        that the example is realy an example.
 
7-<proof>   Attributes:

            id=""
            for= reference to other assertion or derive proof step.
            theory="".

Proof children.
    -<derive>  Derive new claims from already known ones, assertions, or 
    axioms in the current theory (or from the sumption in the assertion 
    under consideration)
            -CMP*
            -FMP
            -method (xref to the Omdoc definition of the method). 
             May accept children.

    -<hypotesis> Local Hypotesis. Attributes:
            -discharges-in (where the hyotesis is dscharged).

    -<conclude> A specialized derive. Last step of the prove.

    -<metacomment> A side comment (does help to clarify but is not essential).
                   Attr. id. 
                   children: CMP*
    -<method>      point to xref where the method is defined. It may contain 
                   elements.

    -<premise>  xref refers t the proof or local asumption methods. 
                DAG of the rpoof.
    

-<proofobject> used to encode formal proofs.


Abstract Data Types.
--------------------

8-<adt> Used to declare a set of sorts (sets declared as the closure of a 
  group of constructors) and selectors (partial inverses of the constructors).

  Attr:
        -type="free|generated|loose"
        -id=
        -style=

 Children:
        -<sortedef>

Esto es una especie the galimatias.


OmDoc Theories.
---------------

9-<theory> Attr:
            -id=""
            -style=

        children:    
        
            -<imports> Attr: 
                -id=
                -from = source theory (from where axioms, symbols, 
                        definitions, will be imported)
                -type="global"
                -hiding = list of symbols to hide.

Simple inheritance: all symbols, axioms, definitions, are inherited 
(type="global"?).

Inheritace via translation.
---------------------------

In this case the <imports> element may have a childrem.

    -<morphism> define a morphism between theories.
        Attr:
            -base=points to another morphism (Page 56 it is not clear end 
             of first paragragh).

        childrem: 
            -<requation> This the define symbol mapping 
                         (e.g group.plus->ring.times).
                -<paterm>
                -<value>


(Theory inclusion, Theory morphism).

10-<theory-inclusion> Attr:
            -id=""
            -from="source theory"
            -to="target theory"
            -by="list of assertions justifying the inclusion"
            
            children:
                
            -CMP*
            -<morphism> (see morphism before).

Local version <axiom-inclusion> axioms and definitions.
    -<obligation> point to a proof  obligation.
    -<path-just>? justify the axiom inlusion by refering to other axiom- or 
                  theory-inclusions.

*This part about theory inclusion is not completely clear.

(Parametric thoeries).

Not very clear.