|
915
|
1 |
(* Title: ZF/Coind/BCR.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Jacob Frost, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 1995 University of Cambridge
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
BCR = Values + Types +
|
|
|
8 |
|
|
945
|
9 |
(*Basic correspondence relation -- not completely specified, as it is a
|
|
|
10 |
parameter of the proof. A concrete version could be defined inductively.*)
|
|
915
|
11 |
|
|
|
12 |
consts
|
|
|
13 |
isof :: "[i,i] => o"
|
|
|
14 |
rules
|
|
|
15 |
isof_app "[| isof(c1,t_fun(t1,t2)); isof(c2,t1) |] ==> isof(c_app(c1,c2),t2)"
|
|
|
16 |
|
|
945
|
17 |
(*Its extension to environments*)
|
|
915
|
18 |
|
|
|
19 |
consts
|
|
|
20 |
isofenv :: "[i,i] => o"
|
|
945
|
21 |
defs
|
|
|
22 |
isofenv_def "isofenv(ve,te) == \
|
|
|
23 |
\ ve_dom(ve) = te_dom(te) & \
|
|
|
24 |
\ ( ALL x:ve_dom(ve). \
|
|
915
|
25 |
\ EX c:Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
|
|
|
26 |
|
|
|
27 |
end
|