src/HOL/MicroJava/J/Value.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 41589 bbd861837ebc
child 58249 180f1b3508ed
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
     1
(*  Title:      HOL/MicroJava/J/Value.thy
41589
bbd861837ebc tuned headers;
wenzelm
parents: 39758
diff changeset
     2
    Author:     David von Oheimb, Technische Universitaet Muenchen
11070
cc421547e744 improved document (added headers etc)
oheimb
parents: 11026
diff changeset
     3
*)
9346
297dcbf64526 re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff changeset
     4
12911
704713ca07ea new document
kleing
parents: 12517
diff changeset
     5
header {* \isaheader{Java Values} *}
9346
297dcbf64526 re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff changeset
     6
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 12911
diff changeset
     7
theory Value imports Type begin
9346
297dcbf64526 re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff changeset
     8
24783
5a3e336a2e37 avoid internal names;
wenzelm
parents: 16417
diff changeset
     9
typedecl loc' -- "locations, i.e. abstract references on objects" 
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 12338
diff changeset
    10
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 12338
diff changeset
    11
datatype loc 
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 12338
diff changeset
    12
  = XcptRef xcpt -- "special locations for pre-allocated system exceptions"
24783
5a3e336a2e37 avoid internal names;
wenzelm
parents: 16417
diff changeset
    13
  | Loc loc'     -- "usual locations (references on objects)"
9346
297dcbf64526 re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff changeset
    14
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    15
datatype val
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 12338
diff changeset
    16
  = Unit        -- "dummy result value of void methods"
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 12338
diff changeset
    17
  | Null        -- "null reference"
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 12338
diff changeset
    18
  | Bool bool   -- "Boolean value"
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 12338
diff changeset
    19
  | Intg int    -- "integer value, name Intg instead of Int because
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 12338
diff changeset
    20
                   of clash with HOL/Set.thy" 
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 12338
diff changeset
    21
  | Addr loc    -- "addresses, i.e. locations of objects "
10061
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents
kleing
parents: 10042
diff changeset
    22
39758
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 24783
diff changeset
    23
primrec the_Bool :: "val => bool" where
10061
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents
kleing
parents: 10042
diff changeset
    24
  "the_Bool (Bool b) = b"
9346
297dcbf64526 re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff changeset
    25
39758
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 24783
diff changeset
    26
primrec the_Intg :: "val => int" where
10061
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents
kleing
parents: 10042
diff changeset
    27
  "the_Intg (Intg i) = i"
9346
297dcbf64526 re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff changeset
    28
39758
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 24783
diff changeset
    29
primrec the_Addr :: "val => loc" where
10061
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents
kleing
parents: 10042
diff changeset
    30
  "the_Addr (Addr a) = a"
9346
297dcbf64526 re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff changeset
    31
39758
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 24783
diff changeset
    32
primrec defpval :: "prim_ty => val"  -- "default value for primitive types" where
10061
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents
kleing
parents: 10042
diff changeset
    33
  "defpval Void    = Unit"
39758
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 24783
diff changeset
    34
| "defpval Boolean = Bool False"
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 24783
diff changeset
    35
| "defpval Integer = Intg 0"
9346
297dcbf64526 re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff changeset
    36
39758
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 24783
diff changeset
    37
primrec default_val :: "ty => val"   -- "default value for all types" where
10061
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents
kleing
parents: 10042
diff changeset
    38
  "default_val (PrimT pt) = defpval pt"
39758
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 24783
diff changeset
    39
| "default_val (RefT  r ) = Null"
9346
297dcbf64526 re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff changeset
    40
297dcbf64526 re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff changeset
    41
end