-
Notifications
You must be signed in to change notification settings - Fork 3
/
theory_hol.dk
43 lines (36 loc) · 2.47 KB
/
theory_hol.dk
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
Set : Type.
bool : Set.
fun : (Set -> (Set -> Set)).
injective El : (Set -> Type).
[a,b] El (fun a b) --> El a -> El b.
el : A : Set -> El A.
choice : A : Set -> El (fun (fun A bool) A).
ex1 : A : Set -> El (fun (fun A bool) bool).
not : El (fun bool bool).
F : El bool.
or : El (fun bool (fun bool bool)).
ex : A : Set -> El (fun (fun A bool) bool).
all : A : Set -> El (fun (fun A bool) bool).
imp : El (fun bool (fun bool bool)).
and : El (fun bool (fun bool bool)).
T : El bool.
eq : A : Set -> El (fun A (fun A bool)).
injective Prf : El bool -> Type.
def fun_ext : a : Set -> b : Set -> f : El (fun a b) -> g : El (fun a b) -> (x : El a -> Prf (eq b (f x) (g x))) -> Prf (eq (fun a b) f g).
def prop_ext : p : El bool -> q : El bool -> (Prf p -> Prf q) -> (Prf q -> Prf p) -> Prf (eq bool p q).
def REFL : a : Set -> t : El a -> Prf (eq a t t).
def MK_COMB : a : Set -> b : Set -> s : El (fun a b) -> t : El (fun a b) -> u : El a -> v : El a -> Prf (eq (fun a b) s t) -> Prf (eq a u v) -> Prf (eq b (s u) (t v)).
def EQ_MP : p : El bool -> q : El bool -> Prf (eq bool p q) -> Prf p -> Prf q.
def TRANS : a : Set -> x : El a -> y : El a -> z : El a -> Prf (eq a x y) -> Prf (eq a y z) -> Prf (eq a x z) := a : Set => x : El a => y : El a => z : El a => xy : Prf (eq a x y) => yz : Prf (eq a y z) => EQ_MP (eq a x y) (eq a x z) (MK_COMB a bool (eq a x) (eq a x) y z (REFL (fun a bool) (eq a x)) yz) xy.
def SYM : a : Set -> x : El a -> y : El a -> Prf (eq a x y) -> Prf (eq a y x) := a : Set => x : El a => y : El a => xy : Prf (eq a x y) => EQ_MP (eq a x x) (eq a y x) (MK_COMB a bool (eq a x) (eq a y) x x (MK_COMB a (fun a bool) (eq a) (eq a) x y (REFL (fun a (fun a bool)) (eq a)) xy) (REFL a x)) (REFL a x).
[p,q] Prf (imp p q) --> Prf p -> Prf q.
[a,p] Prf (all a p) --> x : El a -> Prf (p x).
def top_intro : Prf T.
def and_intro : p : El bool -> Prf p -> q : El bool -> Prf q -> Prf (and p q).
def and_elim1 : p : El bool -> q : El bool -> Prf (and p q) -> Prf p.
def and_elim2 : p : El bool -> q : El bool -> Prf (and p q) -> Prf q.
def ex_intro : a : Set -> p : (El a -> El bool) -> t : El a -> Prf (p t) -> Prf (ex a p).
def ex_elim : a : Set -> p : (El a -> El bool) -> Prf (ex a p) -> r : El bool -> (x : El a -> Prf (p x) -> Prf r) -> Prf r.
def or_intro1 : p : El bool -> Prf p -> q : El bool -> Prf (or p q).
def or_intro2 : p : El bool -> q : El bool -> Prf q -> Prf (or p q).
def or_elim : p : El bool -> q : El bool -> Prf (or p q) -> r : El bool -> (Prf p -> Prf r) -> (Prf q -> Prf r) -> Prf r.