diff options
| author | aarne <aarne@cs.chalmers.se> | 2006-11-27 21:03:15 +0000 |
|---|---|---|
| committer | aarne <aarne@cs.chalmers.se> | 2006-11-27 21:03:15 +0000 |
| commit | 0c5f2c12880d339e51e5133c61216f233d5a9a7b (patch) | |
| tree | 6058960ad196dd410184ccebf73ba4473830ef11 /examples/logic/Arithm.gf | |
| parent | 8cd9a329fa6d41849df4b7e8c2f19b34884cb547 (diff) | |
more in ArithmEng
Diffstat (limited to 'examples/logic/Arithm.gf')
| -rw-r--r-- | examples/logic/Arithm.gf | 16 |
1 files changed, 8 insertions, 8 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))) |