1 (* Title: HOL/BCV/JType.thy |
1 (* Title: HOL/MicroJava/BV/JType.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow, Gerwin Klein |
3 Author: Tobias Nipkow, Gerwin Klein |
4 Copyright 2000 TUM |
4 Copyright 2000 TUM |
5 *) |
5 *) |
6 |
6 |
7 header "Java Type System as Semilattice" |
7 header "The Java Type System as Semilattice" |
8 |
8 |
9 theory JType = WellForm + Err: |
9 theory JType = WellForm + Err: |
10 |
10 |
11 constdefs |
11 constdefs |
12 is_ref :: "ty => bool" |
12 is_ref :: "ty => bool" |
13 "is_ref T == case T of PrimT t => False | RefT r => True" |
13 "is_ref T == case T of PrimT t => False | RefT r => True" |
14 |
14 |
15 sup :: "'c prog => ty => ty => ty err" |
15 sup :: "'c prog => ty => ty => ty err" |
16 "sup G T1 T2 == |
16 "sup G T1 T2 == |
17 case T1 of PrimT P1 => (case T2 of PrimT P2 => (if P1 = P2 then OK (PrimT P1) else Err) | RefT R => Err) |
17 case T1 of PrimT P1 => (case T2 of PrimT P2 => |
|
18 (if P1 = P2 then OK (PrimT P1) else Err) | RefT R => Err) |
18 | RefT R1 => (case T2 of PrimT P => Err | RefT R2 => |
19 | RefT R1 => (case T2 of PrimT P => Err | RefT R2 => |
19 (case R1 of NullT => (case R2 of NullT => OK NT | ClassT C => OK (Class C)) |
20 (case R1 of NullT => (case R2 of NullT => OK NT | ClassT C => OK (Class C)) |
20 | ClassT C => (case R2 of NullT => OK (Class C) |
21 | ClassT C => (case R2 of NullT => OK (Class C) |
21 | ClassT D => OK (Class (some_lub ((subcls1 G)^* ) C D)))))" |
22 | ClassT D => OK (Class (some_lub ((subcls1 G)^* ) C D)))))" |
22 |
23 |
23 subtype :: "'c prog => ty => ty => bool" |
24 subtype :: "'c prog => ty => ty => bool" |
24 "subtype G T1 T2 == G \<turnstile> T1 \<preceq> T2" |
25 "subtype G T1 T2 == G \<turnstile> T1 \<preceq> T2" |
25 |
26 |
26 is_ty :: "'c prog => ty => bool" |
27 is_ty :: "'c prog => ty => bool" |