# HG changeset patch
# User mengj
# Date 1158753399 -7200
# Node ID 5e28b8f2cb525203f2bc55c790c02ddb7859b014
# Parent  ff938c7b15e8cd6914832f2c69655656ce327d60
Moved the functional equality axioms to helper1 files.

diff -r ff938c7b15e8 -r 5e28b8f2cb52 src/HOL/Tools/atp-inputs/const_helper1.dfg
--- a/src/HOL/Tools/atp-inputs/const_helper1.dfg	Wed Sep 20 13:54:03 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/const_helper1.dfg	Wed Sep 20 13:56:39 2006 +0200
@@ -1,10 +1,21 @@
 %ID: $Id$
 %Author: Jia Meng, NICTA
-%extensionality for const-types-only
+%functional equality and extensionality for const-types-only
+
+clause(
+forall([A, X, Y],
+or( not(hBOOL(hAPP(hAPP(fequal(A),X),Y))),
+    equal(X,Y))),
+a9 ).
+
+clause(
+forall([A, X, Y],
+or( not(equal(X,Y)),
+    hBOOL(hAPP(hAPP(fequal(A),X),Y)))),
+a10 ).
 
 clause(
 forall([A, B, F, G],
 or( not(equal(hAPP(F,hAPP(hAPP(hEXTENT(A,B),F),G)),hAPP(G,hAPP(hAPP(hEXTENT(A,B),F),G)))),
     equal(F,G))),
-a18 ).
-
+a11 ).
\ No newline at end of file
diff -r ff938c7b15e8 -r 5e28b8f2cb52 src/HOL/Tools/atp-inputs/const_helper1.tptp
--- a/src/HOL/Tools/atp-inputs/const_helper1.tptp	Wed Sep 20 13:54:03 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/const_helper1.tptp	Wed Sep 20 13:56:39 2006 +0200
@@ -1,8 +1,14 @@
 %ID: $Id$
 %Author: Jia Meng, NICTA
-%extensionality for const-types-only
+%functional equality and extensionality for const-types-only
+
+input_clause(a9,axiom,
+[--hBOOL(hAPP(hAPP(fequal(A),X),Y)),++equal(X,Y)]).
 
-input_clause(a18,axiom,
+input_clause(a10,axiom,
+[++hBOOL(hAPP(hAPP(fequal(A),X),Y)),--equal(X,Y)]).
+
+input_clause(a11,axiom,
 [--equal(hAPP(F,hAPP(hAPP(hEXTENT(A,B),F),G)),hAPP(G,hAPP(hAPP(hEXTENT(A,B),F),G))),
 ++equal(F,G)]).
 
diff -r ff938c7b15e8 -r 5e28b8f2cb52 src/HOL/Tools/atp-inputs/full_helper1.dfg
--- a/src/HOL/Tools/atp-inputs/full_helper1.dfg	Wed Sep 20 13:54:03 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/full_helper1.dfg	Wed Sep 20 13:56:39 2006 +0200
@@ -1,10 +1,21 @@
 %ID: $Id$
 %Author: Jia Meng, NICTA
-%extensionality for full-types
+%functional equality and extensionality for full-types
+
+clause(
+forall([A, X, Y],
+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))),
+    equal(typeinfo(X,A),typeinfo(Y,A)))),
+a9 ).
+
+clause(
+forall([A, X, Y],
+or( not(equal(typeinfo(X,A),typeinfo(Y,A))),
+    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)))),
+a10 ).
 
 clause(
 forall([A, B, F, G],
 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))),
     equal(typeinfo(F,tc_fun(A,B)),typeinfo(G,tc_fun(A,B))))),
-a18 ).
-
+a11 ).
\ No newline at end of file
diff -r ff938c7b15e8 -r 5e28b8f2cb52 src/HOL/Tools/atp-inputs/full_helper1.tptp
--- a/src/HOL/Tools/atp-inputs/full_helper1.tptp	Wed Sep 20 13:54:03 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/full_helper1.tptp	Wed Sep 20 13:56:39 2006 +0200
@@ -1,7 +1,15 @@
 %ID: $Id$
 %Author: Jia Meng, NICTA
-%extensionality for full-types
+%functional equality and extensionality for full-types
+
+input_clause(a9,axiom,
+[--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)),
+++equal(typeinfo(X,A),typeinfo(Y,A))]).
 
-input_clause(a18,axiom,
+input_clause(a10,axiom,
+[++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)),
+--equal(typeinfo(X,A),typeinfo(Y,A))]).
+
+input_clause(a11,axiom,
 [--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)),
 ++equal(typeinfo(F,tc_fun(A,B)),typeinfo(G,tc_fun(A,B)))]).
diff -r ff938c7b15e8 -r 5e28b8f2cb52 src/HOL/Tools/atp-inputs/par_helper1.dfg
--- a/src/HOL/Tools/atp-inputs/par_helper1.dfg	Wed Sep 20 13:54:03 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/par_helper1.dfg	Wed Sep 20 13:56:39 2006 +0200
@@ -1,9 +1,21 @@
 %ID: $Id$
 %Author: Jia Meng, NICTA
-%extensionality for partial types
+%functional equality and extensionality for partial types
+
+clause(
+forall([A, X, Y],
+or( not(hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool)))),
+    equal(X,Y))),
+a9 ).
+
+clause(
+forall([A, X, Y],
+or( not(equal(X,Y)),
+    hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool))))),
+a10 ).
 
 clause(
 forall([A, B, F, G],
 or( not(equal(hAPP(F,hAPP(hAPP(hEXTENT,F,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),G,tc_fun(tc_fun(A,B),A)),tc_fun(A,B)),hAPP(G,hAPP(hAPP(hEXTENT,F,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),G,tc_fun(tc_fun(A,B),A)),tc_fun(A,B)))),
     equal(F,G))),
-a18 ).
+a11 ).
\ No newline at end of file
diff -r ff938c7b15e8 -r 5e28b8f2cb52 src/HOL/Tools/atp-inputs/par_helper1.tptp
--- a/src/HOL/Tools/atp-inputs/par_helper1.tptp	Wed Sep 20 13:54:03 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/par_helper1.tptp	Wed Sep 20 13:56:39 2006 +0200
@@ -1,8 +1,16 @@
 %ID: $Id$
 %Author: Jia Meng, NICTA
-%extensionality for partial types
+%functional equality and extensionality for partial types
+
+input_clause(a9,axiom,
+[--hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool))),
+++equal(X,Y)]).
 
-input_clause(a18,axiom,
+input_clause(a10,axiom,
+[++hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool))),
+--equal(X,Y)]).
+
+input_clause(a11,axiom,
 [--equal(hAPP(F,hAPP(hAPP(hEXTENT,F,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),G,tc_fun(tc_fun(A,B),A)),tc_fun(A,B)),hAPP(G,hAPP(hAPP(hEXTENT,F,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),G,tc_fun(tc_fun(A,B),A)),tc_fun(A,B))),
 ++equal(F,G)]).
 
diff -r ff938c7b15e8 -r 5e28b8f2cb52 src/HOL/Tools/atp-inputs/u_helper1.dfg
--- a/src/HOL/Tools/atp-inputs/u_helper1.dfg	Wed Sep 20 13:54:03 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/u_helper1.dfg	Wed Sep 20 13:56:39 2006 +0200
@@ -1,10 +1,21 @@
 %ID: $Id$
 %Author: Jia Meng, NICTA
-%extensionality, untyped
+%functional equality and extensionality, untyped
+
+clause(
+forall([X, Y],
+or( not(hBOOL(hAPP(hAPP(fequal,X),Y))),
+    equal(X,Y))),
+a9 ).
+
+clause(
+forall([X, Y],
+or( not(equal(X,Y)),
+    hBOOL(hAPP(hAPP(fequal,X),Y)))),
+a10 ).
 
 clause(
 forall([F, G],
 or( not(equal(hAPP(F,hAPP(hAPP(hEXTENT,F),G)),hAPP(G,hAPP(hAPP(hEXTENT,F),G)))),
     equal(F,G))),
-a18 ).
-
+a11 ).
\ No newline at end of file
diff -r ff938c7b15e8 -r 5e28b8f2cb52 src/HOL/Tools/atp-inputs/u_helper1.tptp
--- a/src/HOL/Tools/atp-inputs/u_helper1.tptp	Wed Sep 20 13:54:03 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/u_helper1.tptp	Wed Sep 20 13:56:39 2006 +0200
@@ -1,8 +1,14 @@
 %ID: $Id$
 %Author: Jia Meng, NICTA
-%extensionality, untyped
+%functional equality and extensionality, untyped
+
+input_clause(a9,axiom,
+[--hBOOL(hAPP(hAPP(fequal,X),Y)),++equal(X,Y)]).
 
-input_clause(a18,axiom,
+input_clause(a10,axiom,
+[++hBOOL(hAPP(hAPP(fequal,X),Y)),--equal(X,Y)]).
+
+input_clause(a11,axiom,
 [--equal(hAPP(F,hAPP(hAPP(hEXTENT,F),G)),hAPP(G,hAPP(hAPP(hEXTENT,F),G))),
 ++equal(F,G)]).