1 (* Title: HOL/MicroJava/J/Example.thy |
1 (* Title: HOL/MicroJava/J/Example.thy |
2 Author: David von Oheimb |
2 Author: David von Oheimb |
3 Copyright 1999 Technische Universitaet Muenchen |
3 Copyright 1999 Technische Universitaet Muenchen |
4 *) |
4 *) |
5 |
5 |
6 section {* Example MicroJava Program *} |
6 section \<open>Example MicroJava Program\<close> |
7 |
7 |
8 theory Example imports SystemClasses Eval begin |
8 theory Example imports SystemClasses Eval begin |
9 |
9 |
10 text {* |
10 text \<open> |
11 The following example MicroJava program includes: |
11 The following example MicroJava program includes: |
12 class declarations with inheritance, hiding of fields, and overriding of |
12 class declarations with inheritance, hiding of fields, and overriding of |
13 methods (with refined result type), |
13 methods (with refined result type), |
14 instance creation, local assignment, sequential composition, |
14 instance creation, local assignment, sequential composition, |
15 method call with dynamic binding, literal values, |
15 method call with dynamic binding, literal values, |
32 Base e=new Ext(); |
32 Base e=new Ext(); |
33 e.foo(null); |
33 e.foo(null); |
34 } |
34 } |
35 } |
35 } |
36 \end{verbatim} |
36 \end{verbatim} |
37 *} |
37 \<close> |
38 |
38 |
39 datatype cnam' = Base' | Ext' |
39 datatype cnam' = Base' | Ext' |
40 datatype vnam' = vee' | x' | e' |
40 datatype vnam' = vee' | x' | e' |
41 |
41 |
42 text {* |
42 text \<open> |
43 @{text cnam'} and @{text vnam'} are intended to be isomorphic |
43 @{text cnam'} and @{text vnam'} are intended to be isomorphic |
44 to @{text cnam} and @{text vnam} |
44 to @{text cnam} and @{text vnam} |
45 *} |
45 \<close> |
46 |
46 |
47 axiomatization cnam' :: "cnam' => cname" |
47 axiomatization cnam' :: "cnam' => cname" |
48 where |
48 where |
49 inj_cnam': "(cnam' x = cnam' y) = (x = y)" and |
49 inj_cnam': "(cnam' x = cnam' y) = (x = y)" and |
50 surj_cnam': "\<exists>m. n = cnam' m" |
50 surj_cnam': "\<exists>m. n = cnam' m" |
376 schematic_goal wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile> |
376 schematic_goal wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile> |
377 Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>" |
377 Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>" |
378 apply (rule ty_expr_ty_exprs_wt_stmt.intros) -- ";;" |
378 apply (rule ty_expr_ty_exprs_wt_stmt.intros) -- ";;" |
379 apply (rule t) -- "Expr" |
379 apply (rule t) -- "Expr" |
380 apply (rule t) -- "LAss" |
380 apply (rule t) -- "LAss" |
381 apply simp -- {* @{text "e \<noteq> This"} *} |
381 apply simp -- \<open>@{text "e \<noteq> This"}\<close> |
382 apply (rule t) -- "LAcc" |
382 apply (rule t) -- "LAcc" |
383 apply (simp (no_asm)) |
383 apply (simp (no_asm)) |
384 apply (simp (no_asm)) |
384 apply (simp (no_asm)) |
385 apply (rule t) -- "NewC" |
385 apply (rule t) -- "NewC" |
386 apply (simp (no_asm)) |
386 apply (simp (no_asm)) |