src/HOL/NanoJava/Term.thy

changed to full expressions with side effects

(*  Title:      HOL/NanoJava/Term.thy
    ID:         $Id$
    Author:     David von Oheimb
    Copyright   2001 Technische Universitaet Muenchen
*)

header "Statements and expression emulations"

theory Term = Main:

typedecl cname  (* class name *)
typedecl vnam   (* variable or field name *)
typedecl mname  (* method name *)
arities  cname :: "term"
         vnam  :: "term"
         mname :: "term"

datatype vname  (* variable for special names *)
  = This        (* This pointer *)
  | Param       (* method parameter *)
  | Res         (* method result *)
  | VName vnam 

datatype stmt
  = Skip                   (* empty statement *)
  | Comp       stmt stmt   ("_;; _"             [91,90   ] 90)
  | Cond expr  stmt stmt   ("If '(_') _ Else _" [99,91,91] 91)
  | Loop vname stmt        ("While '(_') _"     [99,91   ] 91)
  | LAss vname expr        ("_ :== _"           [99,   95] 94) (* local ass. *)
  | FAss expr  vnam expr   ("_.._:==_"          [95,99,95] 94) (* field ass. *)
  | Meth cname mname       (* virtual method *)
  | Impl cname mname       (* method implementation *)
and expr
  = NewC cname       ("new _"        [   99] 95) (* object creation  *)
  | Cast cname expr                              (* type cast        *)
  | LAcc vname                                   (* local access     *)
  | FAcc expr  vnam  ("_.._"         [95,99] 95) (* field access     *)
  | Call cname expr mname expr                   (* method call      *)
                     ("{_}_.._'(_')" [99,95,99,95] 95)


lemma pair_imageI [intro]: "(a, b) \<in> A ==> f a b : (%(a, b). f a b) ` A"
apply (rule_tac x = "(a,b)" in image_eqI)
apply  auto
done

end