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