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