author | wenzelm |
Sun, 11 Feb 2018 12:51:23 +0100 | |
changeset 67593 | 5efb88c90051 |
parent 67443 | 3abf6a722518 |
child 80914 | d97fdabd9e2b |
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 |
|
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 | 13 |
|
44375 | 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 | 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 |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63167
diff
changeset
|
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) |
|
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 | 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 | 42 |
|
43 |
end |
|
44 |