author | mengj |
Wed, 20 Sep 2006 13:56:39 +0200 | |
changeset 20645 | 5e28b8f2cb52 |
parent 19717 | 2742cec21579 |
permissions | -rw-r--r-- |
19717 | 1 |
%ID: $Id$ |
2 |
%Author: Jia Meng, NICTA |
|
20645
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
3 |
%functional equality and extensionality for full-types |
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
4 |
|
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
5 |
clause( |
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
6 |
forall([A, X, Y], |
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
7 |
or( not(hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool))), |
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
8 |
equal(typeinfo(X,A),typeinfo(Y,A)))), |
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
9 |
a9 ). |
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
10 |
|
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
11 |
clause( |
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
12 |
forall([A, X, Y], |
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
13 |
or( not(equal(typeinfo(X,A),typeinfo(Y,A))), |
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
14 |
hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)))), |
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
15 |
a10 ). |
19717 | 16 |
|
17 |
clause( |
|
18 |
forall([A, B, F, G], |
|
19 |
or( not(equal(typeinfo(hAPP(typeinfo(F,tc_fun(A,B)),typeinfo(hAPP(typeinfo(hAPP(typeinfo(hEXTENT,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),typeinfo(F,tc_fun(A,B))),tc_fun(tc_fun(A,B),A)),typeinfo(G,tc_fun(A,B))),A)),B),typeinfo(hAPP(typeinfo(G,tc_fun(A,B)),typeinfo(hAPP(typeinfo(hAPP(typeinfo(hEXTENT,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),typeinfo(F,tc_fun(A,B))),tc_fun(tc_fun(A,B),A)),typeinfo(G,tc_fun(A,B))),A)),B))), |
|
20 |
equal(typeinfo(F,tc_fun(A,B)),typeinfo(G,tc_fun(A,B))))), |
|
20645
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
21 |
a11 ). |