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