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