(* Title: HOL/IMPP/Com.thy ID: $Id: Com.thy,v 1.3 2005/09/17 18:14:30 wenzelm Exp $ Author: David von Oheimb (based on a theory by Tobias Nipkow et al), TUM Copyright 1999 TUM *) header {* Semantics of arithmetic and boolean expressions, Syntax of commands *} theory Com imports Main begin types val = nat (* for the meta theory, this may be anything, but with current Isabelle, types cannot be refined later *) typedecl glb typedecl loc consts Arg :: loc Res :: loc datatype vname = Glb glb | Loc loc types globs = "glb => val" locals = "loc => val" datatype state = st globs locals (* for the meta theory, the following would be sufficient: typedecl state consts st :: "[globs , locals] => state" *) types aexp = "state => val" bexp = "state => bool" typedecl pname datatype com = SKIP | Ass vname aexp ("_:==_" [65, 65 ] 60) | Local loc aexp com ("LOCAL _:=_ IN _" [65, 0, 61] 60) | Semi com com ("_;; _" [59, 60 ] 59) | Cond bexp com com ("IF _ THEN _ ELSE _" [65, 60, 61] 60) | While bexp com ("WHILE _ DO _" [65, 61] 60) | BODY pname | Call vname pname aexp ("_:=CALL _'(_')" [65, 65, 0] 60) consts bodies :: "(pname * com) list"(* finitely many procedure definitions *) body :: " pname ~=> com" defs body_def: "body == map_of bodies" (* Well-typedness: all procedures called must exist *) consts WTs :: "com set" syntax WT :: "com => bool" translations "WT c" == "c : WTs" inductive WTs intros Skip: "WT SKIP" Assign: "WT (X :== a)" Local: "WT c ==> WT (LOCAL Y := a IN c)" Semi: "[| WT c0; WT c1 |] ==> WT (c0;; c1)" If: "[| WT c0; WT c1 |] ==> WT (IF b THEN c0 ELSE c1)" While: "WT c ==> WT (WHILE b DO c)" Body: "body pn ~= None ==> WT (BODY pn)" Call: "WT (BODY pn) ==> WT (X:=CALL pn(a))" inductive_cases WTs_elim_cases: "WT SKIP" "WT (X:==a)" "WT (LOCAL Y:=a IN c)" "WT (c1;;c2)" "WT (IF b THEN c1 ELSE c2)" "WT (WHILE b DO c)" "WT (BODY P)" "WT (X:=CALL P(a))" constdefs WT_bodies :: bool "WT_bodies == !(pn,b):set bodies. WT b" ML {* use_legacy_bindings (the_context ()) *} end
lemmas WTs_elim_cases:
[| WT SKIP; P |] ==> P
[| WT (X:==a); P |] ==> P
[| WT (LOCAL Y:=a IN c); WT c ==> P |] ==> P
[| WT (c1.0;; c2.0); [| WT c1.0; WT c2.0 |] ==> P |] ==> P
[| WT (IF b THEN c1.0 ELSE c2.0); [| WT c1.0; WT c2.0 |] ==> P |] ==> P
[| WT (WHILE b DO c); WT c ==> P |] ==> P
[| WT (BODY Pa); !!y. body Pa = Some y ==> P |] ==> P
[| WT (X:=CALL Pa(a)); WT (BODY Pa) ==> P |] ==> P
theorem finite_dom_body:
finite (dom body)
theorem WT_bodiesD:
[| WT_bodies; body pn = Some b |] ==> WT b