src/HOL/NanoJava/Term.thy
author wenzelm
Sun, 11 Feb 2018 12:51:23 +0100
changeset 67593 5efb88c90051
parent 67443 3abf6a722518
child 80914 d97fdabd9e2b
permissions -rw-r--r--
clarified command-line defaults;
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
58889
5b7a9633cfa8 modernized header uniformly as section;
wenzelm
parents: 58310
diff changeset
     5
section "Statements and expression emulations"
11376
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
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 63167
diff changeset
     9
typedecl cname  \<comment> \<open>class    name\<close>
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 63167
diff changeset
    10
typedecl mname  \<comment> \<open>method   name\<close>
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 63167
diff changeset
    11
typedecl fname  \<comment> \<open>field    name\<close>
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 63167
diff changeset
    12
typedecl vname  \<comment> \<open>variable name\<close>
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    13
44375
dfc2e722fe47 modernized specifications
krauss
parents: 41589
diff changeset
    14
axiomatization
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 63167
diff changeset
    15
  This \<comment> \<open>This pointer\<close>
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 63167
diff changeset
    16
  Par  \<comment> \<open>method parameter\<close>
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 63167
diff changeset
    17
  Res  :: vname \<comment> \<open>method result\<close>
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
    18
 \<comment> \<open>Inequality axioms are not required for the meta theory.\<close>
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
58310
91ea607a34d8 updated news
blanchet
parents: 58249
diff changeset
    26
datatype stmt
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 63167
diff changeset
    27
  = Skip                   \<comment> \<open>empty statement\<close>
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)
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 63167
diff changeset
    31
  | LAss vname expr        ("_ :== _"           [99,   95] 94) \<comment> \<open>local assignment\<close>
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 63167
diff changeset
    32
  | FAss expr  fname expr  ("_.._:==_"          [95,99,95] 94) \<comment> \<open>field assignment\<close>
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 63167
diff changeset
    33
  | Meth "cname \<times> mname"   \<comment> \<open>virtual method\<close>
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 63167
diff changeset
    34
  | Impl "cname \<times> mname"   \<comment> \<open>method implementation\<close>
11476
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    35
and expr
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 63167
diff changeset
    36
  = NewC cname       ("new _"        [   99] 95) \<comment> \<open>object creation\<close>
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 63167
diff changeset
    37
  | Cast cname expr                              \<comment> \<open>type cast\<close>
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 63167
diff changeset
    38
  | LAcc vname                                   \<comment> \<open>local access\<close>
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 63167
diff changeset
    39
  | FAcc expr  fname ("_.._"         [95,99] 95) \<comment> \<open>field access\<close>
11558
6539627881e8 simplified vnam/vname, introduced fname, improved comments
oheimb
parents: 11507
diff changeset
    40
  | Call cname expr mname expr                   
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 63167
diff changeset
    41
                     ("{_}_.._'(_')" [99,95,99,95] 95) \<comment> \<open>method call\<close>
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