# 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)]).