src/HOL/Bali/Value.thy
author wenzelm
Sun, 28 Aug 2005 16:04:44 +0200
changeset 17160 fb65eda72fc7
parent 16417 9bc16273c2d4
child 32960 69916a850301
permissions -rw-r--r--
removed obsolete arities;
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
    ID:         $Id$
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
    Author:     David von Oheimb
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     4
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
header {* Java values *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14981
diff changeset
     9
theory Value imports Type begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
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
    11
typedecl loc            --{* locations, i.e. abstract references on objects *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
datatype val
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
    14
	= Unit          --{* dummy result value of void methods *}
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
    15
	| Bool bool     --{* Boolean value *}
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
    16
	| Intg int      --{* integer value *}
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
    17
	| Null          --{* null reference *}
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
    18
	| Addr loc      --{* addresses, i.e. locations of objects *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
translations "val" <= (type) "Term.val"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
             "loc" <= (type) "Term.loc"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
consts   the_Bool   :: "val \<Rightarrow> bool"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
primrec "the_Bool (Bool b) = b"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
consts   the_Intg   :: "val \<Rightarrow> int"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
primrec "the_Intg (Intg i) = i"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
consts   the_Addr   :: "val \<Rightarrow> loc"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
primrec "the_Addr (Addr a) = a"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
types	dyn_ty      = "loc \<Rightarrow> ty option"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
  typeof        :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
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
    34
  defpval       :: "prim_ty \<Rightarrow> val"  --{* default value for primitive types *}
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
    35
  default_val   :: "     ty \<Rightarrow> val"  --{* default value for all types *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
primrec "typeof dt  Unit    = Some (PrimT Void)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
	"typeof dt (Bool b) = Some (PrimT Boolean)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
	"typeof dt (Intg i) = Some (PrimT Integer)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
	"typeof dt  Null    = Some NT"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
	"typeof dt (Addr a) = dt a"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
primrec	"defpval Void    = Unit"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
	"defpval Boolean = Bool False"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
	"defpval Integer = Intg 0"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
primrec	"default_val (PrimT pt) = defpval pt"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
	"default_val (RefT  r ) = Null"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
end