|
1 (* Title: ZF/IMP/Evalc.ML |
|
2 ID: $Id$ |
|
3 Author: Heiko Loetzbeyer & Robert Sandner, TUM |
|
4 Copyright 1994 TUM |
|
5 *) |
|
6 |
|
7 structure Evalc = Inductive_Fun |
|
8 ( |
|
9 val thy = Evalc0.thy; |
|
10 val thy_name = "Evalc" |
|
11 val rec_doms = [("evalc","com * (loc -> nat) * (loc -> nat)")]; |
|
12 val sintrs = |
|
13 [ |
|
14 "[| sigma: loc -> nat |] ==> <skip,sigma> -c-> sigma", |
|
15 "[| m: nat; x: loc; <a,sigma> -a-> m |] ==> \ |
|
16 \ <X(x) := a,sigma> -c-> sigma[m/x]" , |
|
17 "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==> \ |
|
18 \ <c0 ; c1, sigma> -c-> sigma1", |
|
19 "[| c1: com; <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> \ |
|
20 \ <ifc b then c0 else c1, sigma> -c-> sigma1 ", |
|
21 "[| c0 : com; <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> \ |
|
22 \ <ifc b then c0 else c1, sigma> -c-> sigma1 ", |
|
23 "[| c: com; <b, sigma> -b-> 0 |] ==> \ |
|
24 \ <while b do c,sigma> -c-> sigma ", |
|
25 "[| c : com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; \ |
|
26 \ <while b do c, sigma2> -c-> sigma1 |] ==> \ |
|
27 \ <while b do c, sigma> -c-> sigma1 "]; |
|
28 |
|
29 val monos = []; |
|
30 val con_defs = [assign_def]; |
|
31 val type_intrs = Bexp.intrs@Com.intrs@[SigmaI,if_type,lam_type,apply_type]; |
|
32 val type_elims = [SigmaE2,make_elim(Evala.dom_subset RS subsetD), |
|
33 make_elim(Evalb.dom_subset RS subsetD) ]); |