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