src/ZF/Coind/BCR.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 11318 6536fb8c9fc6
permissions -rw-r--r--
expanded tabs
     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 
     9 (*Basic correspondence relation -- not completely specified, as it is a
    10   parameter of the proof.  A concrete version could be defined inductively.*)
    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 
    17 (*Its extension to environments*)
    18 
    19 consts
    20   isofenv :: [i,i] => o
    21 defs
    22   isofenv_def "isofenv(ve,te) ==                
    23    ve_dom(ve) = te_dom(te) &            
    24    ( ALL x:ve_dom(ve).                          
    25      EX c:Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
    26   
    27 end