summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/IMPP/Com.thy

author | wenzelm |

Mon Aug 31 21:01:21 2015 +0200 (2015-08-31) | |

changeset 61069 | aefe89038dd2 |

parent 60754 | 02924903a6fd |

child 63167 | 0909deb8059b |

permissions | -rw-r--r-- |

prefer symbols;

1 (* Title: HOL/IMPP/Com.thy

2 Author: David von Oheimb (based on a theory by Tobias Nipkow et al), TUM

3 *)

5 section {* Semantics of arithmetic and boolean expressions, Syntax of commands *}

7 theory Com

8 imports Main

9 begin

11 type_synonym val = nat

12 (* for the meta theory, this may be anything, but types cannot be refined later *)

14 typedecl glb

15 typedecl loc

17 axiomatization

18 Arg :: loc and

19 Res :: loc

21 datatype vname = Glb glb | Loc loc

22 type_synonym globs = "glb => val"

23 type_synonym locals = "loc => val"

24 datatype state = st globs locals

25 (* for the meta theory, the following would be sufficient:

26 typedecl state

27 consts st :: "[globs , locals] => state"

28 *)

29 type_synonym aexp = "state => val"

30 type_synonym bexp = "state => bool"

32 typedecl pname

34 datatype 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)

44 consts bodies :: "(pname * com) list"(* finitely many procedure definitions *)

45 definition

46 body :: " pname \<rightharpoonup> com" where

47 "body = map_of bodies"

50 (* Well-typedness: all procedures called must exist *)

52 inductive WT :: "com => bool" where

54 Skip: "WT SKIP"

56 | Assign: "WT (X :== a)"

58 | Local: "WT c ==>

59 WT (LOCAL Y := a IN c)"

61 | Semi: "[| WT c0; WT c1 |] ==>

62 WT (c0;; c1)"

64 | If: "[| WT c0; WT c1 |] ==>

65 WT (IF b THEN c0 ELSE c1)"

67 | While: "WT c ==>

68 WT (WHILE b DO c)"

70 | Body: "body pn ~= None ==>

71 WT (BODY pn)"

73 | Call: "WT (BODY pn) ==>

74 WT (X:=CALL pn(a))"

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))"

81 definition

82 WT_bodies :: bool where

83 "WT_bodies = (!(pn,b):set bodies. WT b)"

86 ML {*

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 *}

91 lemma finite_dom_body: "finite (dom body)"

92 apply (unfold body_def)

93 apply (rule finite_dom_map_of)

94 done

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

102 declare WTs_elim_cases [elim!]

104 end