src/HOL/NanoJava/Term.thy
author oheimb
Wed Aug 08 12:36:48 2001 +0200 (2001-08-08)
changeset 11476 06c1998340a8
parent 11376 bf98ad1c22c6
child 11486 8f32860eac3a
permissions -rw-r--r--
changed to full expressions with side effects
oheimb@11376
     1
(*  Title:      HOL/NanoJava/Term.thy
oheimb@11376
     2
    ID:         $Id$
oheimb@11376
     3
    Author:     David von Oheimb
oheimb@11376
     4
    Copyright   2001 Technische Universitaet Muenchen
oheimb@11376
     5
*)
oheimb@11376
     6
oheimb@11376
     7
header "Statements and expression emulations"
oheimb@11376
     8
oheimb@11376
     9
theory Term = Main:
oheimb@11376
    10
oheimb@11376
    11
typedecl cname  (* class name *)
oheimb@11376
    12
typedecl vnam   (* variable or field name *)
oheimb@11376
    13
typedecl mname  (* method name *)
oheimb@11376
    14
arities  cname :: "term"
oheimb@11376
    15
         vnam  :: "term"
oheimb@11376
    16
         mname :: "term"
oheimb@11376
    17
oheimb@11376
    18
datatype vname  (* variable for special names *)
oheimb@11376
    19
  = This        (* This pointer *)
oheimb@11376
    20
  | Param       (* method parameter *)
oheimb@11376
    21
  | Res         (* method result *)
oheimb@11376
    22
  | VName vnam 
oheimb@11376
    23
oheimb@11376
    24
datatype stmt
oheimb@11376
    25
  = Skip                   (* empty statement *)
oheimb@11476
    26
  | Comp       stmt stmt   ("_;; _"             [91,90   ] 90)
oheimb@11476
    27
  | Cond expr  stmt stmt   ("If '(_') _ Else _" [99,91,91] 91)
oheimb@11376
    28
  | Loop vname stmt        ("While '(_') _"     [99,91   ] 91)
oheimb@11476
    29
  | LAss vname expr        ("_ :== _"           [99,   95] 94) (* local ass. *)
oheimb@11476
    30
  | FAss expr  vnam expr   ("_.._:==_"          [95,99,95] 94) (* field ass. *)
oheimb@11376
    31
  | Meth cname mname       (* virtual method *)
oheimb@11376
    32
  | Impl cname mname       (* method implementation *)
oheimb@11476
    33
and expr
oheimb@11476
    34
  = NewC cname       ("new _"        [   99] 95) (* object creation  *)
oheimb@11476
    35
  | Cast cname expr                              (* type cast        *)
oheimb@11476
    36
  | LAcc vname                                   (* local access     *)
oheimb@11476
    37
  | FAcc expr  vnam  ("_.._"         [95,99] 95) (* field access     *)
oheimb@11476
    38
  | Call cname expr mname expr                   (* method call      *)
oheimb@11476
    39
                     ("{_}_.._'(_')" [99,95,99,95] 95)
oheimb@11376
    40
oheimb@11476
    41
oheimb@11376
    42
lemma pair_imageI [intro]: "(a, b) \<in> A ==> f a b : (%(a, b). f a b) ` A"
oheimb@11376
    43
apply (rule_tac x = "(a,b)" in image_eqI)
oheimb@11376
    44
apply  auto
oheimb@11376
    45
done
oheimb@11376
    46
oheimb@11376
    47
end
oheimb@11376
    48