isabelle: src/ZF/Coind/BCR.thy@3ccaa11b6df9 (annotated)

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: ZF/Coind/BCR.thy
915 6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	2	ID: $Id$
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	3	Author: Jacob Frost, Cambridge University Computer Laboratory
915 6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	4	Copyright 1995 University of Cambridge
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	5	*)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	6
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	7	BCR = Values + Types +
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	8
945 23df3da5ffb5 Commented isof(c,t) lcp parents: 915 diff changeset	9	(*Basic correspondence relation -- not completely specified, as it is a
23df3da5ffb5 Commented isof(c,t) lcp parents: 915 diff changeset	10	parameter of the proof. A concrete version could be defined inductively.*)
915 6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	11
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	12	consts
1401 0c439768f45c removed quotes from consts and syntax sections clasohm parents: 1155 diff changeset	13	isof :: [i,i] => o
915 6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	14	rules
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	15	isof_app "[\| isof(c1,t_fun(t1,t2)); isof(c2,t1) \|] ==> isof(c_app(c1,c2),t2)"
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	16
945 23df3da5ffb5 Commented isof(c,t) lcp parents: 915 diff changeset	17	(Its extension to environments)
915 6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	18
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	19	consts
1401 0c439768f45c removed quotes from consts and syntax sections clasohm parents: 1155 diff changeset	20	isofenv :: [i,i] => o
945 23df3da5ffb5 Commented isof(c,t) lcp parents: 915 diff changeset	21	defs
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	22	isofenv_def "isofenv(ve,te) ==
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	23	ve_dom(ve) = te_dom(te) &
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	24	( ALL x:ve_dom(ve).
1155 928a16e02f9f removed \...\ inside strings clasohm parents: 945 diff changeset	25	EX c:Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
915 6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	26
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	27	end

author	wenzelm
	Thu, 14 Oct 1999 15:04:36 +0200
changeset 7866	3ccaa11b6df9
parent 1478	2b8c2a7547ab
child 11318	6536fb8c9fc6
permissions	-rw-r--r--