src/HOL/NanoJava/Term.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 44375 dfc2e722fe47
child 58249 180f1b3508ed
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
     1
(*  Title:      HOL/NanoJava/Term.thy
41589
bbd861837ebc tuned headers;
wenzelm
parents: 16417
diff changeset
     2
    Author:     David von Oheimb, Technische Universitaet Muenchen
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
     3
*)
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
     4
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
     5
header "Statements and expression emulations"
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
     6
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 11565
diff changeset
     7
theory Term imports Main begin
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
     8
11558
6539627881e8 simplified vnam/vname, introduced fname, improved comments
oheimb
parents: 11507
diff changeset
     9
typedecl cname  --{* class    name *}
6539627881e8 simplified vnam/vname, introduced fname, improved comments
oheimb
parents: 11507
diff changeset
    10
typedecl mname  --{* method   name *}
6539627881e8 simplified vnam/vname, introduced fname, improved comments
oheimb
parents: 11507
diff changeset
    11
typedecl fname  --{* field    name *}
6539627881e8 simplified vnam/vname, introduced fname, improved comments
oheimb
parents: 11507
diff changeset
    12
typedecl vname  --{* variable name *}
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    13
44375
dfc2e722fe47 modernized specifications
krauss
parents: 41589
diff changeset
    14
axiomatization
dfc2e722fe47 modernized specifications
krauss
parents: 41589
diff changeset
    15
  This --{* This pointer *}
dfc2e722fe47 modernized specifications
krauss
parents: 41589
diff changeset
    16
  Par  --{* method parameter *}
11558
6539627881e8 simplified vnam/vname, introduced fname, improved comments
oheimb
parents: 11507
diff changeset
    17
  Res  :: vname --{* method result *}
44375
dfc2e722fe47 modernized specifications
krauss
parents: 41589
diff changeset
    18
 -- {* Inequality axioms are not required for the meta theory. *}
11558
6539627881e8 simplified vnam/vname, introduced fname, improved comments
oheimb
parents: 11507
diff changeset
    19
(*
44375
dfc2e722fe47 modernized specifications
krauss
parents: 41589
diff changeset
    20
where
11558
6539627881e8 simplified vnam/vname, introduced fname, improved comments
oheimb
parents: 11507
diff changeset
    21
  This_neq_Par [simp]: "This \<noteq> Par"
6539627881e8 simplified vnam/vname, introduced fname, improved comments
oheimb
parents: 11507
diff changeset
    22
  Par_neq_Res  [simp]: "Par \<noteq> Res"
6539627881e8 simplified vnam/vname, introduced fname, improved comments
oheimb
parents: 11507
diff changeset
    23
  Res_neq_This [simp]: "Res \<noteq> This"
6539627881e8 simplified vnam/vname, introduced fname, improved comments
oheimb
parents: 11507
diff changeset
    24
*)
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    25
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    26
datatype stmt
11558
6539627881e8 simplified vnam/vname, introduced fname, improved comments
oheimb
parents: 11507
diff changeset
    27
  = Skip                   --{* empty statement *}
11476
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    28
  | Comp       stmt stmt   ("_;; _"             [91,90   ] 90)
11565
ab004c0ecc63 Minor improvements, added Example
oheimb
parents: 11560
diff changeset
    29
  | Cond expr  stmt stmt   ("If '(_') _ Else _" [ 3,91,91] 91)
ab004c0ecc63 Minor improvements, added Example
oheimb
parents: 11560
diff changeset
    30
  | Loop vname stmt        ("While '(_') _"     [ 3,91   ] 91)
11560
46d0bde121ab marginally improved comments
oheimb
parents: 11558
diff changeset
    31
  | LAss vname expr        ("_ :== _"           [99,   95] 94) --{* local assignment *}
46d0bde121ab marginally improved comments
oheimb
parents: 11558
diff changeset
    32
  | FAss expr  fname expr  ("_.._:==_"          [95,99,95] 94) --{* field assignment *}
11558
6539627881e8 simplified vnam/vname, introduced fname, improved comments
oheimb
parents: 11507
diff changeset
    33
  | Meth "cname \<times> mname"   --{* virtual method *}
6539627881e8 simplified vnam/vname, introduced fname, improved comments
oheimb
parents: 11507
diff changeset
    34
  | Impl "cname \<times> mname"   --{* method implementation *}
11476
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    35
and expr
11558
6539627881e8 simplified vnam/vname, introduced fname, improved comments
oheimb
parents: 11507
diff changeset
    36
  = NewC cname       ("new _"        [   99] 95) --{* object creation  *}
6539627881e8 simplified vnam/vname, introduced fname, improved comments
oheimb
parents: 11507
diff changeset
    37
  | Cast cname expr                              --{* type cast        *}
6539627881e8 simplified vnam/vname, introduced fname, improved comments
oheimb
parents: 11507
diff changeset
    38
  | LAcc vname                                   --{* local access     *}
6539627881e8 simplified vnam/vname, introduced fname, improved comments
oheimb
parents: 11507
diff changeset
    39
  | FAcc expr  fname ("_.._"         [95,99] 95) --{* field access     *}
6539627881e8 simplified vnam/vname, introduced fname, improved comments
oheimb
parents: 11507
diff changeset
    40
  | Call cname expr mname expr                   
6539627881e8 simplified vnam/vname, introduced fname, improved comments
oheimb
parents: 11507
diff changeset
    41
                     ("{_}_.._'(_')" [99,95,99,95] 95) --{* method call *}
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    42
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    43
end
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    44