482
|
1 |
(* Title: ZF/IMP/Com.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Heiko Loetzbeyer & Robert Sandner, TUM
|
|
4 |
Copyright 1994 TUM
|
|
5 |
*)
|
|
6 |
|
511
|
7 |
open Com;
|
|
8 |
|
|
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 ]);
|
|
12 |
|
|
13 |
val type_cs = ZF_cs addSEs [make_elim(evala.dom_subset RS subsetD),
|
|
14 |
make_elim(evalb.dom_subset RS subsetD),
|
|
15 |
make_elim(evalc.dom_subset RS subsetD)];
|
|
16 |
|
|
17 |
(********** type_intrs for evala **********)
|
|
18 |
|
|
19 |
val evala_type_intrs =
|
|
20 |
map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
|
|
21 |
["!!a.<a,sigma> -a-> n ==> a:aexp","!!a.<a,sigma> -a-> n ==> sigma:loc->nat",
|
|
22 |
"!!a.<a,sigma> -a-> n ==> n:nat"];
|
|
23 |
|
|
24 |
|
|
25 |
(********** type_intrs for evalb **********)
|
482
|
26 |
|
511
|
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 **********)
|
482
|
34 |
|
511
|
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 |
];
|