author | wenzelm |
Mon, 03 Oct 2016 20:26:32 +0200 | |
changeset 64025 | ff4910ced9ba |
parent 63167 | 0909deb8059b |
child 67443 | 3abf6a722518 |
permissions | -rw-r--r-- |
11376 | 1 |
(* Title: HOL/NanoJava/Term.thy |
41589 | 2 |
Author: David von Oheimb, Technische Universitaet Muenchen |
11376 | 3 |
*) |
4 |
||
58889 | 5 |
section "Statements and expression emulations" |
11376 | 6 |
|
16417 | 7 |
theory Term imports Main begin |
11376 | 8 |
|
63167 | 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> |
|
11376 | 13 |
|
44375 | 14 |
axiomatization |
63167 | 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> |
|
11558
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11507
diff
changeset
|
19 |
(* |
44375 | 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 | 25 |
|
58310 | 26 |
datatype stmt |
63167 | 27 |
= Skip \<comment>\<open>empty statement\<close> |
11476 | 28 |
| Comp stmt stmt ("_;; _" [91,90 ] 90) |
11565 | 29 |
| Cond expr stmt stmt ("If '(_') _ Else _" [ 3,91,91] 91) |
30 |
| Loop vname stmt ("While '(_') _" [ 3,91 ] 91) |
|
63167 | 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> |
|
11476 | 35 |
and expr |
63167 | 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> |
|
11558
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11507
diff
changeset
|
40 |
| Call cname expr mname expr |
63167 | 41 |
("{_}_.._'(_')" [99,95,99,95] 95) \<comment>\<open>method call\<close> |
11376 | 42 |
|
43 |
end |
|
44 |