src/HOL/IMPP/Com.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 42174 d0be2722ce9f
child 58249 180f1b3508ed
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 (*  Title:    HOL/IMPP/Com.thy
     2     Author:   David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
     3 *)
     4 
     5 header {* Semantics of arithmetic and boolean expressions, Syntax of commands *}
     6 
     7 theory Com
     8 imports Main
     9 begin
    10 
    11 type_synonym val = nat
    12   (* for the meta theory, this may be anything, but types cannot be refined later *)
    13 
    14 typedecl glb
    15 typedecl loc
    16 
    17 axiomatization
    18   Arg :: loc and
    19   Res :: loc
    20 
    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"
    31 
    32 typedecl pname
    33 
    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)
    43 
    44 consts bodies :: "(pname  *  com) list"(* finitely many procedure definitions *)
    45 definition
    46   body :: " pname ~=> com" where
    47   "body = map_of bodies"
    48 
    49 
    50 (* Well-typedness: all procedures called must exist *)
    51 
    52 inductive 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 
    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))"
    80 
    81 definition
    82   WT_bodies :: bool where
    83   "WT_bodies = (!(pn,b):set bodies. WT b)"
    84 
    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!]
   100 
   101 end