src/ZF/Coind/Static.thy
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1478 2b8c2a7547ab
child 6141 a6922171b396
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.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     1
(*  Title:      ZF/Coind/Static.thy
916
d03bb9f50b3b 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
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     4
    Copyright   1995  University of Cambridge
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     5
*)
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     6
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     7
Static = BCR +
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     8
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     9
consts
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    10
  ElabRel :: i
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    11
inductive
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    12
  domains "ElabRel" <= "TyEnv * Exp * Ty"
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    13
  intrs
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    14
    elab_constI
1155
928a16e02f9f removed \...\ inside strings
clasohm
parents: 916
diff changeset
    15
      " [| te:TyEnv; c:Const; t:Ty; isof(c,t) |] ==>   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 916
diff changeset
    16
       <te,e_const(c),t>:ElabRel "
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    17
    elab_varI
1155
928a16e02f9f removed \...\ inside strings
clasohm
parents: 916
diff changeset
    18
      " [| te:TyEnv; x:ExVar; x:te_dom(te) |] ==>   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 916
diff changeset
    19
       <te,e_var(x),te_app(te,x)>:ElabRel "
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    20
    elab_fnI
1155
928a16e02f9f removed \...\ inside strings
clasohm
parents: 916
diff changeset
    21
      " [| te:TyEnv; x:ExVar; e:Exp; t1:Ty; t2:Ty;   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 916
diff changeset
    22
          <te_owr(te,x,t1),e,t2>:ElabRel |] ==>   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 916
diff changeset
    23
       <te,e_fn(x,e),t_fun(t1,t2)>:ElabRel "
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    24
    elab_fixI
1155
928a16e02f9f removed \...\ inside strings
clasohm
parents: 916
diff changeset
    25
      " [| te:TyEnv; f:ExVar; x:ExVar; t1:Ty; t2:Ty;   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 916
diff changeset
    26
          <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2>:ElabRel |] ==>   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 916
diff changeset
    27
       <te,e_fix(f,x,e),t_fun(t1,t2)>:ElabRel "
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    28
    elab_appI
1155
928a16e02f9f removed \...\ inside strings
clasohm
parents: 916
diff changeset
    29
      " [| te:TyEnv; e1:Exp; e2:Exp; t1:Ty; t2:Ty;   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 916
diff changeset
    30
          <te,e1,t_fun(t1,t2)>:ElabRel;   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 916
diff changeset
    31
          <te,e2,t1>:ElabRel |] ==>   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 916
diff changeset
    32
       <te,e_app(e1,e2),t2>:ElabRel "
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    33
  type_intrs "te_appI::Exp.intrs@Ty.intrs"
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    34
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    35
end
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    36
  
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    37
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    38
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    39
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    40
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    41
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    42
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    43
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    44
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    45
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    46
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    47
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    48
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    49
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    50
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    51
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    52
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    53
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    54
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    55
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    56
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    57