Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Moved the functional equality axioms to helper1 files.
authormengj
Wed, 20 Sep 2006 13:56:39 +0200
changeset 20645 5e28b8f2cb52
parent 20644 ff938c7b15e8
child 20646 02729d4d6e4a
Moved the functional equality axioms to helper1 files.
src/HOL/Tools/atp-inputs/const_helper1.dfg file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/const_helper1.tptp file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/full_helper1.dfg file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/full_helper1.tptp file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/par_helper1.dfg file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/par_helper1.tptp file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/u_helper1.dfg file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/u_helper1.tptp file | annotate | diff | comparison | revisions 
--- 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
--- 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)]).
 
--- 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
--- 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)))]).
--- 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
--- 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)]).
 
--- 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
--- 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)]).
isabelle