src/HOL/IMPP/Com.thy
changeset 17477 ceb42ea2f223
parent 12338 de0f4a63baa5
child 19803 aa2581752afb
     1.1 --- a/src/HOL/IMPP/Com.thy	Sat Sep 17 19:17:35 2005 +0200
     1.2 +++ b/src/HOL/IMPP/Com.thy	Sat Sep 17 20:14:30 2005 +0200
     1.3 @@ -2,80 +2,89 @@
     1.4      ID:       $Id$
     1.5      Author:   David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
     1.6      Copyright 1999 TUM
     1.7 -
     1.8 -Semantics of arithmetic and boolean expressions, Syntax of commands
     1.9  *)
    1.10  
    1.11 -Com = Main +
    1.12 +header {* Semantics of arithmetic and boolean expressions, Syntax of commands *}
    1.13  
    1.14 -types	 val = nat   (* for the meta theory, this may be anything, but with
    1.15 +theory Com
    1.16 +imports Main
    1.17 +begin
    1.18 +
    1.19 +types    val = nat   (* for the meta theory, this may be anything, but with
    1.20                          current Isabelle, types cannot be refined later *)
    1.21 -types	 glb
    1.22 -         loc
    1.23 -arities	 (*val,*)glb,loc :: type
    1.24 -consts   Arg, Res :: loc
    1.25 +typedecl glb
    1.26 +typedecl loc
    1.27 +
    1.28 +consts
    1.29 +  Arg :: loc
    1.30 +  Res :: loc
    1.31  
    1.32  datatype vname  = Glb glb | Loc loc
    1.33 -types	 globs  = glb => val
    1.34 -	 locals = loc => val
    1.35 +types    globs  = "glb => val"
    1.36 +         locals = "loc => val"
    1.37  datatype state  = st globs locals
    1.38  (* for the meta theory, the following would be sufficient:
    1.39 -types    state
    1.40 -arities  state::type
    1.41 -consts   st:: [globs , locals] => state
    1.42 +typedecl state
    1.43 +consts   st :: "[globs , locals] => state"
    1.44  *)
    1.45 -types	 aexp   = state => val
    1.46 -	 bexp   = state => bool
    1.47 +types    aexp   = "state => val"
    1.48 +         bexp   = "state => bool"
    1.49  
    1.50 -types	pname
    1.51 -arities	pname  :: type
    1.52 +typedecl pname
    1.53  
    1.54  datatype com
    1.55        = SKIP
    1.56 -      | Ass   vname aexp	("_:==_"	        [65, 65    ] 60)
    1.57 -      | Local loc aexp com	("LOCAL _:=_ IN _"	[65,  0, 61] 60)
    1.58 -      | Semi  com  com		("_;; _"	        [59, 60    ] 59)
    1.59 -      | Cond  bexp com com	("IF _ THEN _ ELSE _"	[65, 60, 61] 60)
    1.60 -      | While bexp com		("WHILE _ DO _"		[65,     61] 60)
    1.61 +      | Ass   vname aexp        ("_:==_"                [65, 65    ] 60)
    1.62 +      | Local loc aexp com      ("LOCAL _:=_ IN _"      [65,  0, 61] 60)
    1.63 +      | Semi  com  com          ("_;; _"                [59, 60    ] 59)
    1.64 +      | Cond  bexp com com      ("IF _ THEN _ ELSE _"   [65, 60, 61] 60)
    1.65 +      | While bexp com          ("WHILE _ DO _"         [65,     61] 60)
    1.66        | BODY  pname
    1.67 -      | Call  vname pname aexp	("_:=CALL _'(_')"	[65, 65,  0] 60)
    1.68 +      | Call  vname pname aexp  ("_:=CALL _'(_')"       [65, 65,  0] 60)
    1.69  
    1.70  consts bodies :: "(pname  *  com) list"(* finitely many procedure definitions *)
    1.71         body   :: " pname ~=> com"
    1.72 -defs   body_def  "body == map_of bodies"
    1.73 +defs   body_def: "body == map_of bodies"
    1.74  
    1.75  
    1.76  (* Well-typedness: all procedures called must exist *)
    1.77 -consts WTs :: com set
    1.78 -syntax WT  :: com => bool
    1.79 +consts WTs :: "com set"
    1.80 +syntax WT  :: "com => bool"
    1.81  translations "WT c" == "c : WTs"
    1.82  
    1.83 -inductive WTs intrs
    1.84 +inductive WTs intros
    1.85  
    1.86 -    Skip    "WT SKIP"
    1.87 +    Skip:    "WT SKIP"
    1.88  
    1.89 -    Assign  "WT (X :== a)"
    1.90 +    Assign:  "WT (X :== a)"
    1.91  
    1.92 -    Local   "WT c ==>
    1.93 -             WT (LOCAL Y := a IN c)"
    1.94 +    Local:   "WT c ==>
    1.95 +              WT (LOCAL Y := a IN c)"
    1.96  
    1.97 -    Semi    "[| WT c0; WT c1 |] ==>
    1.98 -             WT (c0;; c1)"
    1.99 +    Semi:    "[| WT c0; WT c1 |] ==>
   1.100 +              WT (c0;; c1)"
   1.101  
   1.102 -    If      "[| WT c0; WT c1 |] ==>
   1.103 -             WT (IF b THEN c0 ELSE c1)"
   1.104 +    If:      "[| WT c0; WT c1 |] ==>
   1.105 +              WT (IF b THEN c0 ELSE c1)"
   1.106  
   1.107 -    While   "WT c ==>
   1.108 -             WT (WHILE b DO c)"
   1.109 +    While:   "WT c ==>
   1.110 +              WT (WHILE b DO c)"
   1.111  
   1.112 -    Body    "body pn ~= None ==>
   1.113 -             WT (BODY pn)"
   1.114 +    Body:    "body pn ~= None ==>
   1.115 +              WT (BODY pn)"
   1.116  
   1.117 -    Call    "WT (BODY pn) ==>
   1.118 -             WT (X:=CALL pn(a))"
   1.119 +    Call:    "WT (BODY pn) ==>
   1.120 +              WT (X:=CALL pn(a))"
   1.121 +
   1.122 +inductive_cases WTs_elim_cases:
   1.123 +  "WT SKIP"  "WT (X:==a)"  "WT (LOCAL Y:=a IN c)"
   1.124 +  "WT (c1;;c2)"  "WT (IF b THEN c1 ELSE c2)"  "WT (WHILE b DO c)"
   1.125 +  "WT (BODY P)"  "WT (X:=CALL P(a))"
   1.126  
   1.127  constdefs
   1.128    WT_bodies :: bool
   1.129 - "WT_bodies == !(pn,b):set bodies. WT b"
   1.130 +  "WT_bodies == !(pn,b):set bodies. WT b"
   1.131 +
   1.132 +ML {* use_legacy_bindings (the_context ()) *}
   1.133  
   1.134  end