more in ArithmEng

examples/logic/Arithm.gf

@@ -2,13 +2,11 @@ abstract Arithm = Logic ** {
 
 -- arithmetic
 fun 
-  Nat, Real  : Dom ;
+  Nat  : Dom ;
 data
   Zero : Elem Nat ;
   Succ : Elem Nat -> Elem Nat ;
 fun
-  trunc : Elem Real -> Elem Nat ;
-
   EqNat : (m,n : Elem Nat) -> Prop ;
   LtNat : (m,n : Elem Nat) -> Prop ;
   Div   : (m,n : Elem Nat) -> Prop ;
@@ -24,8 +22,10 @@ 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)) ;
+  eqax2 : (m,n : Elem Nat) -> Proof (EqNat m n) -> 
+             Proof (EqNat (Succ m) (Succ n)) ;
 fun
   IndNat : (C : Elem Nat -> Prop) -> 
              Proof (C Zero) -> 
@@ -41,9 +41,9 @@ def
   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 
+  Prime n = 
-              (LtNat one n) 
+    Conj (LtNat one n) 
-              (Univ Nat (\x -> Impl (Conj (LtNat one x) (Div n x)) (EqNat x n))) ;
+           (Univ Nat (\x -> Impl (Conj (LtNat one x) (Div n x)) (EqNat x n))) ;
 
 fun ex1 : Text ;
 def ex1 = 
@@ -52,7 +52,7 @@ def ex1 =
     (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))) 
+       (\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))) 

examples/logic/ArithmEng.gf

@@ -16,8 +16,8 @@ lin
   Succ = appN2 (regN2 "successor") ;
 
   EqNat x y = mkS (predA2 (mkA2 (regA "equal") (mkPrep "to")) x y) ;
---  LtNat = adj2 ["smaller than"] ;
+  LtNat x y = mkS (predAComp (regA "equal") x y) ;
---  Div   = adj2 ["divisible by"] ;
+  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) ;
@@ -33,19 +33,24 @@ lin
   evax2 n c = 
     appendText c 
       (proof (by (ref (mkLabel ["the second axiom of evenness ,"]))) 
-      (mkS (pred (regA "odd") (appN2 (regN2 "successor") (UsePN (regPN "zero")))))) ;
+        (mkS (pred (regA "odd") (appN2 (regN2 "successor") n)))) ;
   evax3 n c = 
     appendText c 
       (proof (by (ref (mkLabel ["the third axiom of evenness ,"]))) 
-      (mkS (pred (regA "even") (appN2 (regN2 "successor") (UsePN (regPN "zero")))))) ;
+        (mkS (pred (regA "even") (appN2 (regN2 "successor") n)))) ;
 
-{-
 
-  eqax1 = ss ["by the first axiom of equality , zero is equal to zero"] ;
+  eqax1 = 
-  eqax2 m n c = {s = 
+    proof (by (ref (mkLabel ["the first axiom of equality ,"]))) 
-    c.s ++ ["by the second axiom of equality , the successor of"] ++ m.s ++ 
+      (mkS (predA2 (mkA2 (regA "equal") (mkPrep "to")) 
-    ["is equal to the successor of"] ++ n.s} ;
+         (UsePN (regPN "zero")) 
--}
+         (UsePN (regPN "zero")))) ;
+
+  eqax2 m n c = 
+    appendText c 
+      (proof (by (ref (mkLabel ["the second axiom of equality ,"]))) 
+        (mkS (predA2 (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 ++ 

examples/logic/LexTheory.gf

@@ -8,4 +8,6 @@ interface LexTheory = open Grammar in {
     hypothesis_N : N ;
     ifthen_DConj : DConj ;
 
+    defNP : Str -> NP ;
+
 }

examples/logic/LexTheoryEng.gf

@@ -1,4 +1,5 @@
-instance LexTheoryEng of LexTheory = open GrammarEng,ParadigmsEng,IrregEng in {
+instance LexTheoryEng of LexTheory = open 
+  GrammarEng, ParadigmsEng, IrregEng, ParamX in {
   oper
     assume_VS = mkVS (regV "assume") ;
     case_N = regN "case" ;
@@ -6,4 +7,7 @@ instance LexTheoryEng of LexTheory = open GrammarEng,ParadigmsEng,IrregEng in {
     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 = <>} ;
+
 }

examples/logic/LogicI.gf

@@ -4,8 +4,7 @@ incomplete concrete LogicI of Logic =
     Prooftext, 
     Grammar, 
     Constructors, 
-    Combinators,
+    Combinators
-    ParamX ---
   in {
 
 lincat 
@@ -19,10 +18,12 @@ lincat
 lin
   ThmWithProof = theorem ;
 
+  Conj A B = coord and_Conj A B ;
   Disj A B = coord or_Conj A B ;
   Impl A B = coord ifthen_DConj A B ;
 
-  Abs = mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet IndefArt) contradiction_N)) ;
+  Abs = 
+    mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet IndefArt) contradiction_N)) ;
 
   Univ A B = 
     AdvS 
@@ -45,13 +46,14 @@ lin
         (proof therefore C)) ;
 
   ImplI A B b = 
-    proof (assumption A) (appendText b (proof therefore (coord ifthen_DConj A B))) ;
+    proof 
+      (assumption A) 
+      (appendText b (proof therefore (coord ifthen_DConj A B))) ;
 
   Hypoth A h = proof hypothesis A ;
 
 
---- this should not be here, but is needed for variables
 lindef
-  Elem s = {s = \\_ => s ; a = {n = Sg ; p = P3} ; lock_NP = <>} ;
+  Elem = defNP ;
 
-}
+}