changed names of resource-1.3; added a note on homepage on release

old-examples/logic/Arithm.gf

@@ -0,0 +1,64 @@
+abstract Arithm = Logic ** {
+
+-- arithmetic
+fun 
+  Nat  : Dom ;
+data
+  Zero : Elem Nat ;
+  Succ : Elem Nat -> Elem Nat ;
+fun
+  EqNat : (m,n : Elem Nat) -> Prop ;
+  LtNat : (m,n : Elem Nat) -> Prop ;
+  Div   : (m,n : Elem Nat) -> Prop ;
+  Even  : Elem Nat -> Prop ;
+  Odd   : Elem Nat -> Prop ;
+  Prime : Elem Nat -> Prop ;
+
+  one  : Elem Nat ;
+  two  : Elem Nat ;
+  sum  : (m,n : Elem Nat) -> Elem Nat ;
+  prod : (m,n : Elem Nat) -> Elem Nat ;
+data
+  evax1 : Proof (Even Zero) ;
+  evax2 : (n : Elem Nat) -> Proof (Even n) -> Proof (Odd (Succ n)) ;
+  evax3 : (n : Elem Nat) -> Proof (Odd n)  -> Proof (Even (Succ n)) ;
+
+  eqax1 : Proof (EqNat Zero Zero) ;
+  eqax2 : (m,n : Elem Nat) -> Proof (EqNat m n) -> 
+             Proof (EqNat (Succ m) (Succ n)) ;
+fun
+  IndNat : (C : Elem Nat -> Prop) -> 
+             Proof (C Zero) -> 
+             ((x : Elem Nat) -> Hypo (C x) -> Proof (C (Succ x))) -> 
+                Proof (Univ Nat C) ;
+
+def 
+  one = Succ Zero ;
+  two = Succ one ;
+  sum m (Succ n) = Succ (sum m n) ;
+  sum m Zero = m ;
+  prod m (Succ n) = sum (prod m n) m ;
+  prod m Zero = Zero ;
+  LtNat m n = Exist Nat (\x -> EqNat n (sum m (Succ x))) ;
+  Div m n = Exist Nat (\x -> EqNat m (prod x n)) ;
+  Prime n = 
+    Conj (LtNat one n) 
+           (Univ Nat (\x -> Impl (Conj (LtNat one x) (Div n x)) (EqNat x n))) ;
+
+fun ex1 : Text ;
+def ex1 = 
+  ThmWithProof 
+    (Univ Nat (\x -> Disj (Even x) (Odd x))) 
+    (IndNat 
+       (\x -> Disj (Even x) (Odd x)) 
+       (DisjIl (Even Zero) (Odd Zero) evax1) 
+       (\x -> \h -> DisjE (Even x) (Odd x) (Disj (Even (Succ x)) (Odd (Succ x)))
+         (Hypoth (Disj (Even x) (Odd x)) h) 
+         (\a -> DisjIr (Even (Succ x)) (Odd (Succ x)) 
+            (evax2 x (Hypoth (Even x) a))) 
+         (\b -> DisjIl (Even (Succ x)) (Odd (Succ x)) 
+            (evax3 x (Hypoth (Odd x) b))
+         )
+       )
+     ) ;
+} ;

old-examples/logic/ArithmEng.gf

@@ -0,0 +1,66 @@
+--# -path=.:mathematical:present:prelude
+
+concrete ArithmEng of Arithm = LogicEng ** 
+  open
+    GrammarEng,
+    ParadigmsEng,
+    ProoftextEng,
+    MathematicalEng,
+    CombinatorsEng,
+    ConstructorsEng
+  in { 
+
+lin
+  Nat  = UseN  (regN "number") ;
+  Zero = UsePN (regPN "zero") ;
+  Succ = appN2 (regN2 "successor") ;
+
+  EqNat x y = mkS (predA2 (mkA2 (regA "equal") (mkPrep "to")) x y) ;
+  LtNat x y = mkS (predAComp (regA "equal") x y) ;
+  Div   x y = mkS (predA2 (mkA2 (regA "divisible") (mkPrep "by")) x y) ;
+  Even  x = mkS (predA (regA "even") x) ;
+  Odd   x = mkS (predA (regA "odd") x) ;
+  Prime x = mkS (predA (regA "prime") x) ;
+
+  one = UsePN (regPN "one") ;
+  two = UsePN (regPN "two") ;
+  sum = app (regN2 "sum") ;
+  prod = app (regN2 "product") ;
+
+  evax1 = 
+    proof (by (ref (mkLabel ["the first axiom of evenness ,"]))) 
+      (mkS (predA (regA "even") (UsePN (regPN "zero")))) ;
+  evax2 n c = 
+    appendText c 
+      (proof (by (ref (mkLabel ["the second axiom of evenness ,"]))) 
+        (mkS (predA (regA "odd") (appN2 (regN2 "successor") n)))) ;
+  evax3 n c = 
+    appendText c 
+      (proof (by (ref (mkLabel ["the third axiom of evenness ,"]))) 
+        (mkS (predA (regA "even") (appN2 (regN2 "successor") n)))) ;
+
+
+  eqax1 = 
+    proof (by (ref (mkLabel ["the first axiom of equality ,"]))) 
+      (mkS (pred (mkA2 (regA "equal") (mkPrep "to")) 
+         (UsePN (regPN "zero")) 
+         (UsePN (regPN "zero")))) ;
+
+  eqax2 m n c = 
+    appendText c 
+      (proof (by (ref (mkLabel ["the second axiom of equality ,"]))) 
+        (mkS (pred (mkA2 (regA "equal") (mkPrep "to")) 
+          (appN2 (regN2 "successor") m) (appN2 (regN2 "successor") n)))) ;
+
+  IndNat C d e = {s = 
+    ["we proceed by induction . for the basis ,"] ++ d.s ++ 
+    ["for the induction step, consider a number"] ++ C.$0 ++ 
+    ["and assume"] ++ C.s ++ 
+    --- "(" ++ e.$1 ++ ")" ++ 
+    "." ++ e.s ++ 
+    ["hence , for all numbers"] ++ C.$0 ++ "," ++ C.s ; lock_Text = <>} ;
+
+  ex1 = proof ["the first theorem and its proof"] ;
+
+} ;
+

old-examples/logic/LexTheory.gf

@@ -0,0 +1,13 @@
+interface LexTheory = open Grammar in {
+
+  oper
+    assume_VS : VS ;
+    case_N : N ;
+    contradiction_N : N ;
+    have_V2 : V2 ;
+    hypothesis_N : N ;
+    ifthen_DConj : DConj ;
+
+    defNP : Str -> NP ;
+
+}

old-examples/logic/LexTheoryEng.gf

@@ -0,0 +1,13 @@
+instance LexTheoryEng of LexTheory = open 
+  GrammarEng, ParadigmsEng, IrregEng, ParamX in {
+  oper
+    assume_VS = mkVS (regV "assume") ;
+    case_N = regN "case" ;
+    contradiction_N = regN "contradiction" ;
+    have_V2 = dirV2 have_V ;
+    hypothesis_N = mk2N "hypothesis" "hypotheses" ;
+    ifthen_DConj = {s1 = "if" ; s2 = "then" ; n = singular ; lock_DConj = <>} ;
+
+    defNP s = {s = \\_ => s ; a = {n = Sg ; p = P3} ; lock_NP = <>} ;
+
+}

old-examples/logic/Logic.gf

@@ -0,0 +1,60 @@
+-- many-sorted predicate calculus
+-- AR 1999, revised 2001 and 2006
+
+abstract Logic = {
+
+cat 
+  Prop ;       -- proposition
+  Dom ;        -- domain of quantification
+  Elem Dom ;   -- individual element of a domain
+  Proof Prop ; -- proof of a proposition
+  Hypo Prop ;  -- hypothesis of a proposition
+  Text ;       -- theorem with proof etc. 
+
+fun 
+  -- texts
+  Statement : Prop -> Text ;
+  ThmWithProof : (A : Prop) -> Proof A -> Text ;
+  ThmWithTrivialProof : (A : Prop) -> Proof A -> Text ;
+
+  -- logically complex propositions
+  Disj : (A,B : Prop) -> Prop ;
+  Conj : (A,B : Prop) -> Prop ;
+  Impl : (A,B : Prop) -> Prop ;
+  Abs  : Prop ;
+  Neg  : Prop -> Prop ;
+
+  Univ  : (A : Dom) -> (Elem A -> Prop) -> Prop ;
+  Exist : (A : Dom) -> (Elem A -> Prop) -> Prop ;
+ 
+  -- inference rules
+
+  ConjI  : (A,B : Prop) -> Proof A -> Proof B -> Proof (Conj A B) ;  
+  ConjEl : (A,B : Prop) -> Proof (Conj A B) -> Proof A ;
+  ConjEr : (A,B : Prop) -> Proof (Conj A B) -> Proof B ;
+  DisjIl : (A,B : Prop) -> Proof A -> Proof (Disj A B) ;
+  DisjIr : (A,B : Prop) -> Proof B -> Proof (Disj A B) ;
+  DisjE  : (A,B,C : Prop) -> Proof (Disj A B) -> 
+              (Hypo A -> Proof C) -> (Hypo B -> Proof C) -> Proof C ;
+  ImplI  : (A,B : Prop) -> (Hypo A -> Proof B) -> Proof (Impl A B) ;
+  ImplE  : (A,B : Prop) -> Proof (Impl A B) -> Proof A -> Proof B ;
+  NegI   : (A : Prop) -> (Hypo A -> Proof Abs) -> Proof (Neg A) ;
+  NegE   : (A : Prop) -> Proof (Neg A) -> Proof A -> Proof Abs ;
+  AbsE   : (C : Prop) -> Proof Abs -> Proof C ;
+  UnivI  : (A : Dom) -> (B : Elem A -> Prop) -> 
+              ((x : Elem A) -> Proof (B x)) -> Proof (Univ A B) ;
+  UnivE  : (A : Dom) -> (B : Elem A -> Prop) -> 
+              Proof (Univ A B) -> (a : Elem A) -> Proof (B a) ;
+  ExistI : (A : Dom) -> (B : Elem A -> Prop) -> 
+              (a : Elem A) -> Proof (B a) -> Proof (Exist A B) ;
+  ExistE : (A : Dom) -> (B : Elem A -> Prop) -> (C : Prop) -> 
+              Proof (Exist A B) -> ((x : Elem A) -> Proof (B x) -> Proof C) -> 
+              Proof C ;
+
+  -- use a hypothesis
+  Hypoth : (A : Prop) -> Hypo A -> Proof A ;
+
+  -- pronoun
+  Pron : (A : Dom) -> Elem A -> Elem A ;
+
+} ;

old-examples/logic/LogicEng.gf

@@ -0,0 +1,23 @@
+--# -path=.:mathematical:present:resource-1.0/api:prelude
+
+concrete LogicEng of Logic = LogicI with
+  (LexTheory = LexTheoryEng), 
+  (Prooftext = ProoftextEng),
+  (Grammar = GrammarEng), 
+  (Symbolic = SymbolicEng), 
+  (Symbol = SymbolEng), 
+  (Combinators = CombinatorsEng), 
+  (Constructors = ConstructorsEng), 
+  ;
+
+{-
+ImplI Abs Abs (\h -> DisjE Abs Abs Abs (DisjIr Abs Abs (Hypoth Abs h)) 
+(\x -> Hypoth Abs x) (\y -> Hypoth Abs y))
+
+assume that we have a contradiction . by the hypothesis we have a contradiction . 
+a fortiori we have a contradiction or we have a contradiction . 
+we have two cases. assume that we have a contradiction . 
+by the hypothesis we have a contradiction . assume that we have a contradiction . 
+by the hypothesis we have a contradiction . therefore we have a contradiction . 
+therefore if we have a contradiction then we have a contradiction .
+-}

old-examples/logic/LogicI.gf

@@ -0,0 +1,59 @@
+incomplete concrete LogicI of Logic = 
+  open 
+    LexTheory,
+    Prooftext, 
+    Grammar, 
+    Constructors, 
+    Combinators
+  in {
+
+lincat 
+  Prop  = Prooftext.Prop ;
+  Proof = Prooftext.Proof ;
+  Dom   = Typ ;
+  Elem  = Object ;
+  Hypo  = Label ;
+  Text  = Section ;
+
+lin
+  ThmWithProof = theorem ;
+
+  Conj = coord and_Conj ;
+  Disj = coord or_Conj ;
+  Impl = coord ifthen_DConj ;
+
+  Abs = 
+    mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet IndefArt) contradiction_N)) ;
+
+  Univ A B = 
+    AdvS 
+      (mkAdv for_Prep (mkNP all_Predet 
+        (mkNP (mkDet (PlQuant IndefArt)) (mkCN A (symb B.$0)))))
+      B ;
+
+  DisjIl A B a = proof a (proof afortiori (coord or_Conj A B)) ;
+  DisjIr A B b = proof b (proof afortiori (coord or_Conj A B)) ;
+
+  DisjE A B C c d e =
+    appendText
+      c 
+      (appendText
+        (appendText
+           (cases (mkNum n2)) 
+           (proofs 
+             (appendText (assumption A) d)
+             (appendText (assumption B) e)))
+        (proof therefore C)) ;
+
+  ImplI A B b = 
+    proof 
+      (assumption A) 
+      (appendText b (proof therefore (coord ifthen_DConj A B))) ;
+
+  Hypoth A h = proof hypothesis A ;
+
+
+lindef
+  Elem = defNP ;
+
+}

old-examples/logic/Prooftext.gf

@@ -0,0 +1,86 @@
+interface Prooftext = open 
+  Grammar, 
+  LexTheory,
+  Symbolic,
+  Symbol, 
+  (C=ConstructX),
+  Constructors, 
+  Combinators 
+  in {
+
+oper
+  Chapter  = Text ;
+  Section  = Text ;
+  Sections = Text ;
+  Decl     = Text ;
+  Decls    = Text ;
+  Prop     = S ;
+  Branching= S ;
+  Proof    = Text ;
+  Proofs   = Text ;
+  Typ      = CN ;
+  Object   = NP ;
+  Label    = NP ;
+  Adverb   = PConj ;
+  Ref      = NP ;
+  Refs     = [NP] ;
+  Number   = Num ;
+
+  chapter : Label -> Sections -> Chapter 
+    = \title,jments -> 
+        appendText (mkText (mkPhr (mkUtt title)) TEmpty) jments ;
+
+  definition : Decls -> Object -> Object -> Section 
+    = \decl,a,b -> 
+        appendText decl (mkText (mkPhr (mkUtt (mkS (pred b a)))) TEmpty) ;
+
+  theorem : Prop -> Proof -> Section 
+    = \prop,prf -> appendText (mkText (mkPhr prop) TEmpty) prf ;
+
+  assumption : Prop -> Decl 
+    = \p -> 
+        mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS p)))) TEmpty ;
+
+  declaration : Object -> Typ -> Decl
+    = \a,ty ->
+        mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS (mkS (pred ty a)))))) TEmpty ;
+
+  proof = overload {
+    proof : Prop -> Proof 
+      = \p -> mkText (mkPhr p) TEmpty ;
+    proof : Str -> Proof
+      = \s -> {s = s ++ "." ; lock_Text = <>} ;
+    proof : Adverb -> Prop -> Proof
+      = \a,p -> mkText (mkPhr a (mkUtt p) NoVoc) TEmpty ;
+    proof : Decl -> Proof
+      = \d -> d ;
+    proof : Proof -> Proof -> Proof
+      = appendText ;
+    proof : Branching -> Proofs -> Proof
+      = \b,ps -> mkText (mkPhr b) ps
+    } ;
+
+  proofs : Proof -> Proof -> Proofs 
+    = appendText ;
+
+  cases : Num -> Branching 
+    = \n -> 
+        mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet n) case_N)) ;
+
+  by : Ref -> Adverb 
+    = \h -> C.mkPConj (mkAdv by8means_Prep h).s ;
+  therefore : Adverb
+    = therefore_PConj ;
+  afortiori : Adverb
+    = C.mkPConj ["a fortiori"] ;
+  hypothesis : Adverb
+    = C.mkPConj (mkAdv by8means_Prep (mkNP (mkDet DefArt) hypothesis_N)).s ;
+
+  ref : Label -> Ref
+    = \h -> h ;
+  refs : Refs -> Ref
+    = \rs -> mkNP and_Conj rs ;
+
+  mkLabel : Str -> Label ;
+
+}

old-examples/logic/ProoftextEng.gf

@@ -0,0 +1,19 @@
+--# -path=.:mathematical:present:resource-1.0/api:prelude
+
+instance ProoftextEng of Prooftext = 
+  open 
+    LexTheoryEng, 
+    GrammarEng, 
+    SymbolicEng, 
+    SymbolEng, 
+    (C=ConstructX),
+    CombinatorsEng, 
+    ConstructorsEng,
+    (P=ParadigmsEng)
+  in {
+
+oper
+  mkLabel : Str -> Label = \s -> UsePN (P.regPN s) ;
+
+
+}

old-examples/logic/Theory.gf

@@ -0,0 +1,47 @@
+abstract Theory = {
+
+  cat
+    Chapter ;
+    Jment ;
+    [Jment] {0} ;
+    Decl ;
+    [Decl] {0} ;
+    Prop ;
+    Proof ;
+    [Proof] {2} ;
+    Branch ;
+    Typ ;
+    Obj ;
+    Label ;
+    Ref ;
+    [Ref] ;
+    Adverb ;
+    Number ;
+    
+  fun
+    Chap       : Label -> [Jment] -> Chapter ;          -- title, text
+
+    JDefObj    : [Decl] -> Obj -> Obj -> Jment ;        -- a = b (G)
+    JDefObjTyp : [Decl] -> Typ -> Obj -> Obj -> Jment ; -- a = b : A (G)
+    JDefProp   : [Decl] -> Prop -> Prop -> Jment ;      -- A = B : Prop (G)
+    JThm       : [Decl] -> Prop -> Proof -> Jment ;     -- p : P (G)
+
+    DProp      : Prop  -> Decl ;                        -- assume P
+    DPropLabel : Label -> Prop -> Label ;               -- assume P (h)
+    DTyp       : Obj   -> Typ -> Decl ;                 -- let x,y be T
+
+    PProp      : Prop -> Proof ;                        -- P.
+    PAdvProp   : Adverb -> Prop -> Proof ;              -- Hence, P.
+    PDecl      : Decl -> Proof ;                        -- Assume P.
+    PBranch    : Branch -> [Proof] -> Proof ;           -- By cases: P1 P2
+
+    BCases     : Number -> Branch ;                     -- We have n cases.
+    
+    ARef       : Ref -> Adverb ;                        -- by Thm 2
+    AHence     : Adverb ;                               -- therefore
+    AAFort     : Adverb ;                               -- a fortiori
+
+    RLabel     : Label -> Ref ;                         -- Thm 2
+    RMany      : [Ref] -> Ref ;                         -- Thm 2 and Lemma 4
+
+}

old-examples/logic/TheoryEng.gf

@@ -0,0 +1,10 @@
+--# -path=.:mathematical:present:resource-1.0/api:prelude
+
+concrete TheoryEng of Theory = TheoryI with
+  (LexTheory = LexTheoryEng), 
+  (Grammar = GrammarEng), 
+  (Symbolic = SymbolicEng), 
+  (Symbol = SymbolEng), 
+  (Combinators = CombinatorsEng), 
+  (Constructors = ConstructorsEng), 
+  ;

old-examples/logic/TheoryI.gf

@@ -0,0 +1,56 @@
+incomplete concrete TheoryI of Theory = 
+  open 
+    LexTheory,
+    Grammar, 
+    Symbolic, 
+    Symbol,
+    Combinators, 
+    Constructors, 
+    (C=ConstructX),
+    Prelude 
+  in {
+
+lincat
+  Chapter = Text ;
+  Jment   = Text ;
+  Decl    = Text ;
+  Prop    = S ;
+  Branch  = S ;
+  Proof   = Text ;
+  [Proof] = Text ;
+  Typ     = CN ;
+  Obj     = NP ;
+  Label   = NP ;
+  Adverb  = PConj ;
+  Ref     = NP ;
+  [Ref]   = [NP] ;
+  Number  = Num ;
+
+lin
+  Chap title jments = 
+    appendText (mkText (mkPhr (mkUtt title)) TEmpty) jments ;
+
+  JDefObj decl a b = 
+    appendText decl (mkUtt (mkS (pred b a))) ;
+
+  DProp p = 
+    mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS p)))) TEmpty ;
+  DTyp a ty = --- x pro a: refresh bug
+    mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS (mkS (pred ty a)))))) TEmpty ;
+
+  PProp p = mkText (mkPhr p) TEmpty ;
+  PAdvProp a p = mkText (mkPhr a (mkUtt p) NoVoc) TEmpty ;
+  PDecl d = d ;
+  PBranch b ps = mkText (mkPhr b) ps ;
+
+  BCases n = 
+    mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet (mkNum n2)) case_N)) ;
+
+  ARef h = mkAdv by8means_Prep h ;
+  AHence = therefore_PConj ;
+  AAFort = C.mkPConj ["a fortiori"] ;
+
+  RLabel h = h ;
+  RMany rs = mkNP and_Conj rs ;
+
+}