blob: 2a91c5ed035d7e8d881f357bdef2612a3df997aa (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
|
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) -> Proof (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))) ;
Abs = Abs ;
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)))
(Hypo (Disj (Even x) (Odd x)) h)
(\a -> DisjIr (Even (succ x)) (Odd (succ x))
(evax2 x (Hypo (Even x) a)))
(\b -> DisjIl (Even (succ x)) (Odd (succ x))
(evax3 x (Hypo (Odd x) b))
)
)
) ;
} ;
|
