src/ZF/Coind/BCR.thy
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1478 2b8c2a7547ab
child 11318 6536fb8c9fc6
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.

(*  Title:      ZF/Coind/BCR.thy
    ID:         $Id$
    Author:     Jacob Frost, Cambridge University Computer Laboratory
    Copyright   1995  University of Cambridge
*)

BCR = Values + Types +

(*Basic correspondence relation -- not completely specified, as it is a
  parameter of the proof.  A concrete version could be defined inductively.*)

consts
  isof :: [i,i] => o
rules
  isof_app "[| isof(c1,t_fun(t1,t2)); isof(c2,t1) |] ==> isof(c_app(c1,c2),t2)"

(*Its extension to environments*)

consts
  isofenv :: [i,i] => o
defs
  isofenv_def "isofenv(ve,te) ==                
   ve_dom(ve) = te_dom(te) &            
   ( ALL x:ve_dom(ve).                          
     EX c:Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
  
end