2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Heiko Loetzbeyer & Robert Sandner, TUM |
3 Author: Heiko Loetzbeyer & Robert Sandner, TUM |
4 Copyright 1994 TUM |
4 Copyright 1994 TUM |
5 *) |
5 *) |
6 |
6 |
7 structure Com = Datatype_Fun |
7 open Com; |
8 ( |
|
9 val thy = Bexp.thy; |
|
10 val thy_name = "Com"; |
|
11 val rec_specs = |
|
12 [ |
|
13 ( |
|
14 "com", "univ(aexp Un bexp)", |
|
15 [ |
|
16 (["skip"], "i", NoSyn), |
|
17 ([":="], "[i,i] => i", Infixl 60), |
|
18 ([";"], "[i,i] => i", Infixl 60), |
|
19 (["whileC"], "[i,i] => i", Mixfix("while _ do _",[],60)), |
|
20 (["ifC"], "[i,i,i] => i", |
|
21 Mixfix("ifc _ then _ else _",[],60)) |
|
22 ] |
|
23 ) |
|
24 ]; |
|
25 |
8 |
26 val rec_styp = "i"; |
9 val assign_type = prove_goalw Com.thy [assign_def] |
|
10 "!!n. [| sigma:loc -> nat; n:nat |] ==> sigma[n/x] : loc -> nat" |
|
11 (fn _ => [ fast_tac (ZF_cs addIs [apply_type,lam_type,if_type]) 1 ]); |
27 |
12 |
28 val sintrs = |
13 val type_cs = ZF_cs addSEs [make_elim(evala.dom_subset RS subsetD), |
29 [ |
14 make_elim(evalb.dom_subset RS subsetD), |
30 "skip : com", |
15 make_elim(evalc.dom_subset RS subsetD)]; |
31 "[| x:loc; a:aexp|] ==> X(x) := a : com", |
16 |
32 "[| c0:com; c1:com|] ==> c0 ; c1 : com", |
17 (********** type_intrs for evala **********) |
33 "[| b:bexp; c:com|] ==> while b do c : com", |
18 |
34 "[| b:bexp; c0:com; c1:com|] ==> ifc b then c0 else c1 : com" |
19 val evala_type_intrs = |
35 ]; |
20 map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)])) |
36 val monos = []; |
21 ["!!a.<a,sigma> -a-> n ==> a:aexp","!!a.<a,sigma> -a-> n ==> sigma:loc->nat", |
37 val type_intrs = datatype_intrs@Aexp.intrs; |
22 "!!a.<a,sigma> -a-> n ==> n:nat"]; |
38 val type_elims = datatype_elims |
23 |
39 ); |
24 |
|
25 (********** type_intrs for evalb **********) |
|
26 |
|
27 val evalb_type_intrs = |
|
28 map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)])) |
|
29 ["!!b.<b,sigma> -b-> w ==> b:bexp","!!b.<b,sigma> -b-> w ==> sigma:loc->nat", |
|
30 "!!b.<b,sigma> -b-> w ==> w:bool"]; |
|
31 |
|
32 |
|
33 (********** type_intrs for evalb **********) |
|
34 |
|
35 val evalc_type_intrs = |
|
36 map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)])) |
|
37 ["!!c.<c,sigma> -c-> sigma' ==> c:com", |
|
38 "!!c.<c,sigma> -c-> sigma' ==> sigma:loc->nat", |
|
39 "!!c.<c,sigma> -c-> sigma' ==> sigma':loc->nat"]; |
|
40 |
|
41 |
|
42 val op_type_intrs = evala_type_intrs@evalb_type_intrs@evalc_type_intrs; |
|
43 |
|
44 |
|
45 val aexp_elim_cases = |
|
46 [ |
|
47 evala.mk_cases aexp.con_defs "<N(n),sigma> -a-> i", |
|
48 evala.mk_cases aexp.con_defs "<X(x),sigma> -a-> i", |
|
49 evala.mk_cases aexp.con_defs "<Op1(f,e),sigma> -a-> i", |
|
50 evala.mk_cases aexp.con_defs "<Op2(f,a1,a2),sigma> -a-> i" |
|
51 ]; |