From 0c5f2c12880d339e51e5133c61216f233d5a9a7b Mon Sep 17 00:00:00 2001 From: aarne Date: Mon, 27 Nov 2006 21:03:15 +0000 Subject: [PATCH] more in ArithmEng --- examples/logic/Arithm.gf | 16 ++++++++-------- examples/logic/ArithmEng.gf | 25 +++++++++++++++---------- examples/logic/LexTheory.gf | 2 ++ examples/logic/LexTheoryEng.gf | 6 +++++- examples/logic/LogicI.gf | 16 +++++++++------- 5 files changed, 39 insertions(+), 26 deletions(-) diff --git a/examples/logic/Arithm.gf b/examples/logic/Arithm.gf index ff8212995..331a0d7c6 100644 --- a/examples/logic/Arithm.gf +++ b/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 - (LtNat one n) - (Univ Nat (\x -> Impl (Conj (LtNat one x) (Div n x)) (EqNat 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 = @@ -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))) diff --git a/examples/logic/ArithmEng.gf b/examples/logic/ArithmEng.gf index 94031fa9f..05526b365 100644 --- a/examples/logic/ArithmEng.gf +++ b/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"] ; --- Div = adj2 ["divisible by"] ; + 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) ; @@ -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"] ; - eqax2 m n c = {s = - c.s ++ ["by the second axiom of equality , the successor of"] ++ m.s ++ - ["is equal to the successor of"] ++ n.s} ; --} + eqax1 = + proof (by (ref (mkLabel ["the first axiom of equality ,"]))) + (mkS (predA2 (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 (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 ++ diff --git a/examples/logic/LexTheory.gf b/examples/logic/LexTheory.gf index 7355abab2..a7a7c9439 100644 --- a/examples/logic/LexTheory.gf +++ b/examples/logic/LexTheory.gf @@ -8,4 +8,6 @@ interface LexTheory = open Grammar in { hypothesis_N : N ; ifthen_DConj : DConj ; + defNP : Str -> NP ; + } diff --git a/examples/logic/LexTheoryEng.gf b/examples/logic/LexTheoryEng.gf index 29c2f21fc..165e1796d 100644 --- a/examples/logic/LexTheoryEng.gf +++ b/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 = <>} ; + } diff --git a/examples/logic/LogicI.gf b/examples/logic/LogicI.gf index 61d948607..09ffe661d 100644 --- a/examples/logic/LogicI.gf +++ b/examples/logic/LogicI.gf @@ -4,8 +4,7 @@ incomplete concrete LogicI of Logic = Prooftext, Grammar, Constructors, - Combinators, - ParamX --- + Combinators 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 ; -} \ No newline at end of file +}