1 (* Title: ZF/IMP/Evalb.ML |
|
2 ID: $Id$ |
|
3 Author: Heiko Loetzbeyer & Robert Sandner, TUM |
|
4 Copyright 1994 TUM |
|
5 *) |
|
6 |
|
7 structure Evalb = Inductive_Fun |
|
8 ( |
|
9 val thy = Evalb0.thy; |
|
10 val thy_name = "Evalb" |
|
11 val rec_doms = [("evalb","bexp * (loc -> nat) * bool")]; |
|
12 val sintrs = |
|
13 [ |
|
14 "[| sigma:loc -> nat |] ==> <true,sigma> -b-> 1", |
|
15 "[| sigma:loc -> nat |] ==> <false,sigma> -b-> 0", |
|
16 "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f: (nat*nat)->bool |] \ |
|
17 \ ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> ", |
|
18 "[| <b,sigma> -b-> w |] \ |
|
19 \ ==> <noti(b),sigma> -b-> not(w)", |
|
20 "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] \ |
|
21 \ ==> <b0 andi b1,sigma> -b-> (w0 and w1)", |
|
22 "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] \ |
|
23 \ ==> <b0 ori b1,sigma> -b-> (w0 or w1)" |
|
24 ]; |
|
25 |
|
26 val monos = []; |
|
27 val con_defs = []; |
|
28 val type_intrs = Bexp.intrs@[apply_funtype,and_type,or_type, |
|
29 bool_1I,bool_0I,not_type]; |
|
30 val type_elims = [make_elim(Evala.dom_subset RS subsetD) ]; |
|
31 ); |
|