isabelle: src/HOL/Tools/atp-inputs/full_helper1.dfg@46832fee1215 (annotated)

19717 2742cec21579 Helper files in DFG format. mengj parents: diff changeset	1	%ID: $Id$
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	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 2742cec21579 Helper files in DFG format. mengj parents: diff changeset	16
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	17	clause(
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	18	forall([A, B, F, G],
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	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))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	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 ).

author	paulson
	Thu, 21 Sep 2006 17:33:11 +0200
changeset 20661	46832fee1215
parent 20645	5e28b8f2cb52
permissions	-rw-r--r--