src/ZF/IMP/Evala.ML
author wenzelm
Thu, 14 Oct 1999 15:04:36 +0200
changeset 7866 3ccaa11b6df9
parent 496 3fc829fa81d2
permissions -rw-r--r--
pdf: generate thumbnails if ISABELLE_THUMBPDF set;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
482
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
     1
(*  Title: 	ZF/IMP/Evala.ML
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
     2
    ID:         $Id$
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
     3
    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
     4
    Copyright   1994 TUM
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
     5
*)
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
     6
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
     7
structure Evala = Inductive_Fun
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
     8
 (
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
     9
  val thy = Evala0.thy;
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    10
  val thy_name="Evala";
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    11
  val rec_doms = [("evala","aexp * (loc -> nat) * nat")];
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    12
  val sintrs = 
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    13
      [
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    14
	"[| n:nat ; sigma:loc->nat |] ==> <N(n),sigma> -a-> n",
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    15
       	"[| x:loc;  sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x",
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    16
       	"[| <e,sigma> -a-> n; f: nat -> nat |] \
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    17
\           ==> <Op1(f,e),sigma> -a-> f`n" ,
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    18
       	"[| <e0,sigma> -a-> n0; <e1,sigma>  -a-> n1; \
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    19
\           f: (nat * nat) -> nat  |] \
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    20
\           ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"  ];
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    21
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    22
  val monos = [];
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    23
  val con_defs = [];
496
3fc829fa81d2 Inductive defs need no longer mention SigmaI/E2
lcp
parents: 482
diff changeset
    24
  val type_intrs = Aexp.intrs@[apply_funtype];
3fc829fa81d2 Inductive defs need no longer mention SigmaI/E2
lcp
parents: 482
diff changeset
    25
  val type_elims = []
482
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    26
 );