Types.thy

Types = WellForm + Exec +

datatype 
 prim = Integer 

datatype 
  Rt	= NT		
	| IT cname
	| CT cname
	| AT tys 
and
 tys	= PTS prim	
	| RTS (Rt list)

constdefs
 get_RTS :: "tys => Rt list"
 "get_RTS x == @rs. x = RTS rs"

types
 refs = Rt list

datatype
 tyOrVoid	= Void
		| TY tys
datatype
 any		= Unusable
		| US tys

syntax
 Prim :: "prim => any"	
 Refs :: "(Rt list) => any"	
translations
 "Prim p" == "US (PTS p)"
 "Prim" == "US o PTS"
 "Refs r" == "US (RTS r)"
 "Refs" == "US o RTS"

constdefs
 sup_any :: "[any,any] => bool" ("_ >= _")
 "a >= a' ==
    case a of
      Unusable => True
    | US ts    =>  case a' of 
		     Unusable => False
		   | US ts' => case ts of
	         		 PTS pr => ts=ts'
	       		       | RTS rs => ? rs'. ts' = RTS rs' &  set rs'  <=  set rs" 

consts
 fd2tys :: "[bytecode,field_desc] => tys"
primrec
 "fd2tys CFS I       = PTS Integer"
 "fd2tys CFS (L cn)  = RTS [if is_interface (CFS !! cn) then IT cn else CT cn]"		
 "fd2tys CFS (A fd)  = RTS [AT (fd2tys CFS fd)]"


syntax
 fd2any :: "[bytecode,field_desc] => any"
translations
"fd2any CFS fd" == "US (fd2tys CFS fd)"
"fd2any CFS" == "US o (fd2tys CFS)"

consts
 rd2tyOrVoid :: "[bytecode,return_desc] => tyOrVoid"
primrec
 "rd2tyOrVoid CFS (FT fd) = TY (fd2tys CFS fd)"
 "rd2tyOrVoid CFS V       = Void"

end

Theorems proved in Types.ML:

i < length l ==> (k ! i, l ! i) = zip k l ! i

length (zip k l) = length l

(map f xs = y # ys) = (? x xs'. xs = x # xs' & f x = y & map f xs' = ys)

x = Integer

X >= Prim Integer = (X = Unusable | X = Prim Integer)

X >= Refs rs' = (X = Unusable | (? rs. X = Refs rs & set rs' <= set rs))

fd2tys CFS fd = PTS pt ==> fd = I

fd2tys CFS fd = PTS pt ==> default_val fd = Intg #0

fd2tys CFS fd = RTS rt ==> default_val fd = Null

(rd2tyOrVoid CFS rd = Void) = (rd = V)

(rd2tyOrVoid CFS rd = TY tys) = (? fd. rd = FT fd & tys = fd2tys CFS fd)

get_RTS (RTS rt) = rt