Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/atp-inputs/full_comb_inclS.tptp
author paulson
Thu, 21 Sep 2006 17:33:11 +0200
changeset 20661 46832fee1215
parent 19969 c72e2110c026
permissions -rw-r--r--
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions unless theorems differ by sorts alone, which should not matter. Also minor fixes to standard hashing.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19492
29c6cba140da added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff changeset 
     1
 
%ID: $Id$
29c6cba140da added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff changeset 
     2
 
%Author: Jia Meng, NICTA
29c6cba140da added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff changeset 
     3
 
%typed combinator reduction for full-types (include S)
29c6cba140da added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff changeset 
     4
 












29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




     5


%K P Q --> P













29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




     6


input_clause(a1,axiom,













29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




     7


[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(P,A)),tc_fun(B,A)),typeinfo(Q,B)),A),typeinfo(P,A))]).













29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




     8














29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




     9


%S P Q R --> P R (Q R)













29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    10


input_clause(a2,axiom,













29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    11


[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBS,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(tc_fun(A,B),tc_fun(A,C)))),typeinfo(P,tc_fun(A,tc_fun(B,C)))),tc_fun(tc_fun(A,B),tc_fun(A,C))),typeinfo(Q,tc_fun(A,B))),tc_fun(A,C)),typeinfo(R,A)),C),typeinfo(hAPP(typeinfo(hAPP(typeinfo(P,tc_fun(A,tc_fun(B,C))),typeinfo(R,A)),tc_fun(B,C)),typeinfo(hAPP(typeinfo(Q,tc_fun(A,B)),typeinfo(R,A)),B)),C))]).













29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    12














29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    13


%I P --> P













29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    14


input_clause(a3,axiom,













29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    15


[++equal(typeinfo(hAPP(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(P,T)),T),typeinfo(P,T))]).













29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    16














29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    17


%B P Q R --> P(Q R)













29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    18


input_clause(a4,axiom,













29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    19


[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBB,tc_fun(tc_fun(A,B),tc_fun(tc_fun(C,A),tc_fun(C,B)))),typeinfo(P,tc_fun(A,B))),tc_fun(tc_fun(C,A),tc_fun(C,B))),typeinfo(Q,tc_fun(C,A))),tc_fun(C,B)),typeinfo(R,C)),B),typeinfo(hAPP(typeinfo(P,tc_fun(A,B)),typeinfo(hAPP(typeinfo(Q,tc_fun(C,A)),typeinfo(R,C)),A)),B))]).













29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    20














29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    21














29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    22


%C P Q R --> P R Q













29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    23


input_clause(a5,axiom,













29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    24


[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBC,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))),typeinfo(P,tc_fun(A,tc_fun(B,C)))),tc_fun(B,tc_fun(A,C))),typeinfo(Q,B)),tc_fun(A,C)),typeinfo(R,A)),C),typeinfo(hAPP(typeinfo(hAPP(typeinfo(P,tc_fun(A,tc_fun(B,C))),typeinfo(R,A)),tc_fun(B,C)),typeinfo(Q,B)),C))]).













29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    25














29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    26


input_clause(a6,axiom,













29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    27


[--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)),













29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    28


++equal(typeinfo(X,A),typeinfo(Y,A))]).













29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    29









19969






c72e2110c026
Removed some incorrect axioms.



mengj


parents: 
19492

diff
changeset




    30


input_clause(a7,axiom,








19492






29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    31


[++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)),













29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    32


--equal(typeinfo(X,A),typeinfo(Y,A))]).













29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    33














29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.



mengj


parents: 

diff
changeset




    34
















isabelle