482
|
1 |
(* Title: ZF/IMP/Evala.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Heiko Loetzbeyer & Robert Sandner, TUM
|
|
4 |
Copyright 1994 TUM
|
|
5 |
*)
|
|
6 |
|
|
7 |
structure Evala = Inductive_Fun
|
|
8 |
(
|
|
9 |
val thy = Evala0.thy;
|
|
10 |
val thy_name="Evala";
|
|
11 |
val rec_doms = [("evala","aexp * (loc -> nat) * nat")];
|
|
12 |
val sintrs =
|
|
13 |
[
|
|
14 |
"[| n:nat ; sigma:loc->nat |] ==> <N(n),sigma> -a-> n",
|
|
15 |
"[| x:loc; sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x",
|
|
16 |
"[| <e,sigma> -a-> n; f: nat -> nat |] \
|
|
17 |
\ ==> <Op1(f,e),sigma> -a-> f`n" ,
|
|
18 |
"[| <e0,sigma> -a-> n0; <e1,sigma> -a-> n1; \
|
|
19 |
\ f: (nat * nat) -> nat |] \
|
|
20 |
\ ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>" ];
|
|
21 |
|
|
22 |
val monos = [];
|
|
23 |
val con_defs = [];
|
|
24 |
val type_intrs = Aexp.intrs@[SigmaI,apply_funtype];
|
|
25 |
val type_elims = [SigmaE2]
|
|
26 |
);
|