8177
|
1 |
(* Title: HOL/IMPP/Com.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
|
|
4 |
Copyright 1999 TUM
|
|
5 |
*)
|
|
6 |
|
17477
|
7 |
header {* Semantics of arithmetic and boolean expressions, Syntax of commands *}
|
8177
|
8 |
|
17477
|
9 |
theory Com
|
|
10 |
imports Main
|
|
11 |
begin
|
|
12 |
|
|
13 |
types val = nat (* for the meta theory, this may be anything, but with
|
8177
|
14 |
current Isabelle, types cannot be refined later *)
|
17477
|
15 |
typedecl glb
|
|
16 |
typedecl loc
|
|
17 |
|
|
18 |
consts
|
|
19 |
Arg :: loc
|
|
20 |
Res :: loc
|
8177
|
21 |
|
|
22 |
datatype vname = Glb glb | Loc loc
|
17477
|
23 |
types globs = "glb => val"
|
|
24 |
locals = "loc => val"
|
8177
|
25 |
datatype state = st globs locals
|
|
26 |
(* for the meta theory, the following would be sufficient:
|
17477
|
27 |
typedecl state
|
|
28 |
consts st :: "[globs , locals] => state"
|
8177
|
29 |
*)
|
17477
|
30 |
types aexp = "state => val"
|
|
31 |
bexp = "state => bool"
|
8177
|
32 |
|
17477
|
33 |
typedecl pname
|
8177
|
34 |
|
|
35 |
datatype com
|
|
36 |
= SKIP
|
17477
|
37 |
| Ass vname aexp ("_:==_" [65, 65 ] 60)
|
|
38 |
| Local loc aexp com ("LOCAL _:=_ IN _" [65, 0, 61] 60)
|
|
39 |
| Semi com com ("_;; _" [59, 60 ] 59)
|
|
40 |
| Cond bexp com com ("IF _ THEN _ ELSE _" [65, 60, 61] 60)
|
|
41 |
| While bexp com ("WHILE _ DO _" [65, 61] 60)
|
8177
|
42 |
| BODY pname
|
17477
|
43 |
| Call vname pname aexp ("_:=CALL _'(_')" [65, 65, 0] 60)
|
8177
|
44 |
|
|
45 |
consts bodies :: "(pname * com) list"(* finitely many procedure definitions *)
|
|
46 |
body :: " pname ~=> com"
|
17477
|
47 |
defs body_def: "body == map_of bodies"
|
8177
|
48 |
|
|
49 |
|
|
50 |
(* Well-typedness: all procedures called must exist *)
|
17477
|
51 |
consts WTs :: "com set"
|
|
52 |
syntax WT :: "com => bool"
|
8177
|
53 |
translations "WT c" == "c : WTs"
|
|
54 |
|
17477
|
55 |
inductive WTs intros
|
8177
|
56 |
|
17477
|
57 |
Skip: "WT SKIP"
|
8177
|
58 |
|
17477
|
59 |
Assign: "WT (X :== a)"
|
8177
|
60 |
|
17477
|
61 |
Local: "WT c ==>
|
|
62 |
WT (LOCAL Y := a IN c)"
|
8177
|
63 |
|
17477
|
64 |
Semi: "[| WT c0; WT c1 |] ==>
|
|
65 |
WT (c0;; c1)"
|
8177
|
66 |
|
17477
|
67 |
If: "[| WT c0; WT c1 |] ==>
|
|
68 |
WT (IF b THEN c0 ELSE c1)"
|
8177
|
69 |
|
17477
|
70 |
While: "WT c ==>
|
|
71 |
WT (WHILE b DO c)"
|
8177
|
72 |
|
17477
|
73 |
Body: "body pn ~= None ==>
|
|
74 |
WT (BODY pn)"
|
8177
|
75 |
|
17477
|
76 |
Call: "WT (BODY pn) ==>
|
|
77 |
WT (X:=CALL pn(a))"
|
|
78 |
|
|
79 |
inductive_cases WTs_elim_cases:
|
|
80 |
"WT SKIP" "WT (X:==a)" "WT (LOCAL Y:=a IN c)"
|
|
81 |
"WT (c1;;c2)" "WT (IF b THEN c1 ELSE c2)" "WT (WHILE b DO c)"
|
|
82 |
"WT (BODY P)" "WT (X:=CALL P(a))"
|
8177
|
83 |
|
|
84 |
constdefs
|
|
85 |
WT_bodies :: bool
|
17477
|
86 |
"WT_bodies == !(pn,b):set bodies. WT b"
|
|
87 |
|
19803
|
88 |
|
|
89 |
ML {* val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl] *}
|
|
90 |
|
|
91 |
lemma finite_dom_body: "finite (dom body)"
|
|
92 |
apply (unfold body_def)
|
|
93 |
apply (rule finite_dom_map_of)
|
|
94 |
done
|
|
95 |
|
|
96 |
lemma WT_bodiesD: "[| WT_bodies; body pn = Some b |] ==> WT b"
|
|
97 |
apply (unfold WT_bodies_def body_def)
|
|
98 |
apply (drule map_of_SomeD)
|
|
99 |
apply fast
|
|
100 |
done
|
|
101 |
|
|
102 |
declare WTs_elim_cases [elim!]
|
8177
|
103 |
|
|
104 |
end
|