482
|
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 = [];
|
496
|
28 |
val type_intrs = Bexp.intrs@[apply_funtype,and_type,or_type,
|
482
|
29 |
bool_1I,bool_0I,not_type];
|
496
|
30 |
val type_elims = [make_elim(Evala.dom_subset RS subsetD) ];
|
482
|
31 |
);
|