src/HOL/Bali/Value.thy
author wenzelm
Fri, 18 Feb 2011 16:36:42 +0100
changeset 41778 5f79a9e42507
parent 37956 ee939247b2fb
child 58249 180f1b3508ed
permissions -rw-r--r--
modernized specifications;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12857
a4386cc9b1c3 tuned header;
wenzelm
parents: 12854
diff changeset
     1
(*  Title:      HOL/Bali/Value.thy
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     2
    Author:     David von Oheimb
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     4
header {* Java values *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14981
diff changeset
     8
theory Value imports Type begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12858
diff changeset
    10
typedecl loc            --{* locations, i.e. abstract references on objects *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
datatype val
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 17160
diff changeset
    13
        = Unit          --{* dummy result value of void methods *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 17160
diff changeset
    14
        | Bool bool     --{* Boolean value *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 17160
diff changeset
    15
        | Intg int      --{* integer value *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 17160
diff changeset
    16
        | Null          --{* null reference *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 17160
diff changeset
    17
        | Addr loc      --{* addresses, i.e. locations of objects *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    20
primrec the_Bool :: "val \<Rightarrow> bool"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    21
  where "the_Bool (Bool b) = b"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    22
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    23
primrec the_Intg :: "val \<Rightarrow> int"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    24
  where "the_Intg (Intg i) = i"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    25
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    26
primrec the_Addr :: "val \<Rightarrow> loc"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    27
  where "the_Addr (Addr a) = a"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
41778
5f79a9e42507 modernized specifications;
wenzelm
parents: 37956
diff changeset
    29
type_synonym dyn_ty = "loc \<Rightarrow> ty option"
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    30
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    31
primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    32
where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    33
  "typeof dt  Unit = Some (PrimT Void)"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    34
| "typeof dt (Bool b) = Some (PrimT Boolean)"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    35
| "typeof dt (Intg i) = Some (PrimT Integer)"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    36
| "typeof dt  Null = Some NT"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    37
| "typeof dt (Addr a) = dt a"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    39
primrec defpval :: "prim_ty \<Rightarrow> val"  --{* default value for primitive types *}
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    40
where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    41
  "defpval Void = Unit"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    42
| "defpval Boolean = Bool False"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    43
| "defpval Integer = Intg 0"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    45
primrec default_val :: "ty \<Rightarrow> val"  --{* default value for all types *}
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    46
where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    47
  "default_val (PrimT pt) = defpval pt"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    48
| "default_val (RefT  r ) = Null"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
end