src/ZF/IMP/Evalc.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Evalc.ML	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,33 @@
+(*  Title: 	ZF/IMP/Evalc.ML
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+structure Evalc = Inductive_Fun    
+ (
+  val thy = Evalc0.thy;
+  val thy_name = "Evalc"
+  val rec_doms = [("evalc","com * (loc -> nat) * (loc -> nat)")];
+  val sintrs =
+      [
+	"[| sigma: loc -> nat |] ==> <skip,sigma> -c-> sigma",
+       	"[| m: nat; x: loc; <a,sigma> -a-> m |] ==> \
+\          <X(x) := a,sigma> -c-> sigma[m/x]" , 
+       "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==> \
+\          <c0 ; c1, sigma> -c-> sigma1",
+       "[| c1: com; <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> \
+\          <ifc b then c0 else c1, sigma> -c-> sigma1 ",
+       "[| c0 : com; <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> \
+\          <ifc b then c0 else c1, sigma> -c-> sigma1 ",
+       "[| c: com; <b, sigma> -b-> 0 |] ==> \
+\          <while b do c,sigma> -c-> sigma ",
+       "[| c : com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; \
+\          <while b do c, sigma2> -c-> sigma1 |] ==> \
+\          <while b do c, sigma> -c-> sigma1 "];
+
+  val monos = [];
+  val con_defs = [assign_def];
+  val type_intrs = [e-mail]@[SigmaI,if_type,lam_type,apply_type];
+  val type_elims = [SigmaE2,make_elim(Evala.dom_subset RS subsetD),
+                            make_elim(Evalb.dom_subset RS subsetD) ]);