diff options
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/logic/Arithm.gf | 64 | ||||
| -rw-r--r-- | examples/logic/ArithmEng.gf | 61 | ||||
| -rw-r--r-- | examples/logic/LogicI.gf | 12 |
3 files changed, 135 insertions, 2 deletions
diff --git a/examples/logic/Arithm.gf b/examples/logic/Arithm.gf new file mode 100644 index 000000000..ff8212995 --- /dev/null +++ b/examples/logic/Arithm.gf @@ -0,0 +1,64 @@ +abstract Arithm = Logic ** { + +-- arithmetic +fun + Nat, Real : 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 ; + 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)) + ) + ) + ) ; +} ; diff --git a/examples/logic/ArithmEng.gf b/examples/logic/ArithmEng.gf new file mode 100644 index 000000000..94031fa9f --- /dev/null +++ b/examples/logic/ArithmEng.gf @@ -0,0 +1,61 @@ +--# -path=.:mathematical:present:resource-1.0/api: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 = adj2 ["smaller than"] ; +-- Div = adj2 ["divisible by"] ; + 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 = appColl (regN2 "sum") ; + prod = appColl (regN2 "product") ; + + evax1 = + proof (by (ref (mkLabel ["the first axiom of evenness ,"]))) + (mkS (pred (regA "even") (UsePN (regPN "zero")))) ; + evax2 n c = + appendText c + (proof (by (ref (mkLabel ["the second axiom of evenness ,"]))) + (mkS (pred (regA "odd") (appN2 (regN2 "successor") (UsePN (regPN "zero")))))) ; + evax3 n c = + appendText c + (proof (by (ref (mkLabel ["the third axiom of evenness ,"]))) + (mkS (pred (regA "even") (appN2 (regN2 "successor") (UsePN (regPN "zero")))))) ; + +{- + + 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} ; +-} + + 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"] ; + +} ; + diff --git a/examples/logic/LogicI.gf b/examples/logic/LogicI.gf index 182ed6ff5..61d948607 100644 --- a/examples/logic/LogicI.gf +++ b/examples/logic/LogicI.gf @@ -4,7 +4,8 @@ incomplete concrete LogicI of Logic = Prooftext, Grammar, Constructors, - Combinators + Combinators, + ParamX --- in { lincat @@ -24,7 +25,10 @@ lin Abs = mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet IndefArt) contradiction_N)) ; Univ A B = - mkS (mkAdv for_Prep (mkNP all_Predet (mkNP (mkDet IndefArt (mkCN A $0))))) 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)) ; @@ -46,4 +50,8 @@ lin 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 = <>} ; + }
\ No newline at end of file |