src/HOL/IMPP/Com.thy
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 27362 a6dc1769fdda
child 41589 bbd861837ebc
permissions -rw-r--r--
moved global ML bindings to global place;
     1 (*  Title:    HOL/IMPP/Com.thy
     2     ID:       $Id$
     3     Author:   David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
     4     Copyright 1999 TUM
     5 *)
     6 
     7 header {* Semantics of arithmetic and boolean expressions, Syntax of commands *}
     8 
     9 theory Com
    10 imports Main
    11 begin
    12 
    13 types    val = nat   (* for the meta theory, this may be anything, but with
    14                         current Isabelle, types cannot be refined later *)
    15 typedecl glb
    16 typedecl loc
    17 
    18 axiomatization
    19   Arg :: loc and
    20   Res :: loc
    21 
    22 datatype vname  = Glb glb | Loc loc
    23 types    globs  = "glb => val"
    24          locals = "loc => val"
    25 datatype state  = st globs locals
    26 (* for the meta theory, the following would be sufficient:
    27 typedecl state
    28 consts   st :: "[globs , locals] => state"
    29 *)
    30 types    aexp   = "state => val"
    31          bexp   = "state => bool"
    32 
    33 typedecl pname
    34 
    35 datatype com
    36       = SKIP
    37       | Ass   vname aexp        ("_:==_"                [65, 65    ] 60)
    38       | Local loc aexp com      ("LOCAL _:=_ IN _"      [65,  0, 61] 60)
    39       | Semi  com  com          ("_;; _"                [59, 60    ] 59)
    40       | Cond  bexp com com      ("IF _ THEN _ ELSE _"   [65, 60, 61] 60)
    41       | While bexp com          ("WHILE _ DO _"         [65,     61] 60)
    42       | BODY  pname
    43       | Call  vname pname aexp  ("_:=CALL _'(_')"       [65, 65,  0] 60)
    44 
    45 consts bodies :: "(pname  *  com) list"(* finitely many procedure definitions *)
    46 definition
    47   body :: " pname ~=> com" where
    48   "body = map_of bodies"
    49 
    50 
    51 (* Well-typedness: all procedures called must exist *)
    52 
    53 inductive WT  :: "com => bool" where
    54 
    55     Skip:    "WT SKIP"
    56 
    57   | Assign:  "WT (X :== a)"
    58 
    59   | Local:   "WT c ==>
    60               WT (LOCAL Y := a IN c)"
    61 
    62   | Semi:    "[| WT c0; WT c1 |] ==>
    63               WT (c0;; c1)"
    64 
    65   | If:      "[| WT c0; WT c1 |] ==>
    66               WT (IF b THEN c0 ELSE c1)"
    67 
    68   | While:   "WT c ==>
    69               WT (WHILE b DO c)"
    70 
    71   | Body:    "body pn ~= None ==>
    72               WT (BODY pn)"
    73 
    74   | Call:    "WT (BODY pn) ==>
    75               WT (X:=CALL pn(a))"
    76 
    77 inductive_cases WTs_elim_cases:
    78   "WT SKIP"  "WT (X:==a)"  "WT (LOCAL Y:=a IN c)"
    79   "WT (c1;;c2)"  "WT (IF b THEN c1 ELSE c2)"  "WT (WHILE b DO c)"
    80   "WT (BODY P)"  "WT (X:=CALL P(a))"
    81 
    82 definition
    83   WT_bodies :: bool where
    84   "WT_bodies = (!(pn,b):set bodies. WT b)"
    85 
    86 
    87 ML {* val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl] *}
    88 
    89 lemma finite_dom_body: "finite (dom body)"
    90 apply (unfold body_def)
    91 apply (rule finite_dom_map_of)
    92 done
    93 
    94 lemma WT_bodiesD: "[| WT_bodies; body pn = Some b |] ==> WT b"
    95 apply (unfold WT_bodies_def body_def)
    96 apply (drule map_of_SomeD)
    97 apply fast
    98 done
    99 
   100 declare WTs_elim_cases [elim!]
   101 
   102 end