src/HOL/NanoJava/Term.thy
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 63167 0909deb8059b
child 67443 3abf6a722518
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/NanoJava/Term.thy
     2     Author:     David von Oheimb, Technische Universitaet Muenchen
     3 *)
     4 
     5 section "Statements and expression emulations"
     6 
     7 theory Term imports Main begin
     8 
     9 typedecl cname  \<comment>\<open>class    name\<close>
    10 typedecl mname  \<comment>\<open>method   name\<close>
    11 typedecl fname  \<comment>\<open>field    name\<close>
    12 typedecl vname  \<comment>\<open>variable name\<close>
    13 
    14 axiomatization
    15   This \<comment>\<open>This pointer\<close>
    16   Par  \<comment>\<open>method parameter\<close>
    17   Res  :: vname \<comment>\<open>method result\<close>
    18  \<comment> \<open>Inequality axioms are not required for the meta theory.\<close>
    19 (*
    20 where
    21   This_neq_Par [simp]: "This \<noteq> Par"
    22   Par_neq_Res  [simp]: "Par \<noteq> Res"
    23   Res_neq_This [simp]: "Res \<noteq> This"
    24 *)
    25 
    26 datatype stmt
    27   = Skip                   \<comment>\<open>empty statement\<close>
    28   | Comp       stmt stmt   ("_;; _"             [91,90   ] 90)
    29   | Cond expr  stmt stmt   ("If '(_') _ Else _" [ 3,91,91] 91)
    30   | Loop vname stmt        ("While '(_') _"     [ 3,91   ] 91)
    31   | LAss vname expr        ("_ :== _"           [99,   95] 94) \<comment>\<open>local assignment\<close>
    32   | FAss expr  fname expr  ("_.._:==_"          [95,99,95] 94) \<comment>\<open>field assignment\<close>
    33   | Meth "cname \<times> mname"   \<comment>\<open>virtual method\<close>
    34   | Impl "cname \<times> mname"   \<comment>\<open>method implementation\<close>
    35 and expr
    36   = NewC cname       ("new _"        [   99] 95) \<comment>\<open>object creation\<close>
    37   | Cast cname expr                              \<comment>\<open>type cast\<close>
    38   | LAcc vname                                   \<comment>\<open>local access\<close>
    39   | FAcc expr  fname ("_.._"         [95,99] 95) \<comment>\<open>field access\<close>
    40   | Call cname expr mname expr                   
    41                      ("{_}_.._'(_')" [99,95,99,95] 95) \<comment>\<open>method call\<close>
    42 
    43 end
    44