src/ZF/Coind/Dynamic.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.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     1
(*  Title:      ZF/Coind/Dynamic.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
Dynamic = Values +
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     8
6dae0daf57b7 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
  EvalRel :: i
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    11
inductive
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    12
  domains "EvalRel" <= "ValEnv * Exp * Val"
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    13
  intrs
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    14
    eval_constI
1155
928a16e02f9f removed \...\ inside strings
clasohm
parents: 915
diff changeset
    15
      " [| ve:ValEnv; c:Const |] ==>   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 915
diff changeset
    16
       <ve,e_const(c),v_const(c)>:EvalRel"
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    17
    eval_varI
1155
928a16e02f9f removed \...\ inside strings
clasohm
parents: 915
diff changeset
    18
      " [| ve:ValEnv; x:ExVar; x:ve_dom(ve) |] ==>   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 915
diff changeset
    19
       <ve,e_var(x),ve_app(ve,x)>:EvalRel" 
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    20
    eval_fnI
1155
928a16e02f9f removed \...\ inside strings
clasohm
parents: 915
diff changeset
    21
      " [| ve:ValEnv; x:ExVar; e:Exp |] ==>   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 915
diff changeset
    22
       <ve,e_fn(x,e),v_clos(x,e,ve)>:EvalRel "  
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    23
    eval_fixI
1155
928a16e02f9f removed \...\ inside strings
clasohm
parents: 915
diff changeset
    24
      " [| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val;   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 915
diff changeset
    25
          v_clos(x,e,ve_owr(ve,f,cl))=cl |] ==>   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 915
diff changeset
    26
       <ve,e_fix(f,x,e),cl>:EvalRel " 
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    27
    eval_appI1
1155
928a16e02f9f removed \...\ inside strings
clasohm
parents: 915
diff changeset
    28
      " [| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const;   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 915
diff changeset
    29
          <ve,e1,v_const(c1)>:EvalRel;   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 915
diff changeset
    30
          <ve,e2,v_const(c2)>:EvalRel |] ==>   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 915
diff changeset
    31
       <ve,e_app(e1,e2),v_const(c_app(c1,c2))>:EvalRel "
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    32
    eval_appI2
1155
928a16e02f9f removed \...\ inside strings
clasohm
parents: 915
diff changeset
    33
      " [| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val;   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 915
diff changeset
    34
          <ve,e1,v_clos(xm,em,vem)>:EvalRel;   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 915
diff changeset
    35
          <ve,e2,v2>:EvalRel;   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 915
diff changeset
    36
          <ve_owr(vem,xm,v2),em,v>:EvalRel |] ==>   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 915
diff changeset
    37
       <ve,e_app(e1,e2),v>:EvalRel "
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    38
  type_intrs "c_appI::ve_appI::ve_empI::ve_owrI::Exp.intrs@Val_ValEnv.intrs"
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    39
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    40
  
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    41
end