Convert.thy

Back to the index of BV_ASCII

Convert = Types +

consts
 wideRefConvertible :: "[bytecode,Rt,Rt] => bool" 
 wideRefsConvertible :: "[bytecode,Rt list,Rt list] => bool" 
 invoConvertible :: "[bytecode,tys,tys] => bool"

primrec
 "wideRefConvertible CFS NT ref = True"
 "wideRefConvertible CFS (IT inm) ref = 
	((? inm'. ref=IT inm' &  (inm',inm) : (d_superinterface_rel CFS)^*)
	 |  (ref=CT Object))"
 "wideRefConvertible CFS (CT cn) ref = 
	((? inm. ref=IT inm &  implements (CFS, cn, inm))
	 |  (? cn'. ref=CT cn' &  (cn',cn) : (d_superclass_rel CFS)^*))"
 "wideRefConvertible CFS (AT ts) ref = 
	((ref=CT Object) 
	 |  (? ts'. ref=AT ts' &  invoConvertible CFS ts ts'))"

 "wideRefsConvertible CFS [] rs = True"
 "wideRefsConvertible CFS (r#rs) rs' = ((? r':set rs'. wideRefConvertible CFS r r') 
					&  wideRefsConvertible CFS rs rs' )"

 "invoConvertible CFS (PTS pt) ts' = (ts'=PTS pt)"
 "invoConvertible CFS (RTS rs) ts' = (? rs'. ts'=RTS rs' &   wideRefsConvertible CFS rs rs')"

constdefs
 assConvertible :: "[bytecode,tys,tys] => bool"
 "assConvertible == invoConvertible"

end

Theorems proved in Convert.ML:

compatible_imp_invoConvertible

[| wf_classfiles CFS; compatible CFS fd fd' |] ==> invoConvertible CFS (fd2tys CFS fd) (fd2tys CFS fd')
  [term]

wf_cs5

[| wf_classfiles CFS; CFS cn ~= None |] ==> get_thisclass CFS !! cn = cn

is_defined_get_fields_lemma

[| wf_classfiles CFS; is_class CFS fc; get_fields CFS !! fc (fc', fn) ~= None |] ==> fc' = fc

is_not_defined_get_fields_lemma

[| wf_classfiles CFS; is_class CFS fc; fc' ~= fc |] ==> get_fields CFS !! fc (fc', fn) = None

get_fields_impl_get_all_fields3

[| wf_classfiles CFS; is_class CFS fc; wideRefConvertible CFS (CT cn) (CT fc);
   get_fields CFS !! fc (fc, fn) = Some fd |]
==> get_all_fields (CFS, cn) (fc, fn) = Some fd

Convertible_refl

wideRefConvertible CFS r r &
invoConvertible CFS t t & (! rs'. set rs <= set rs' --> wideRefsConvertible CFS rs rs')

wideRefConvertible_AT

wideRefConvertible CFS (AT ts) r ==> r = CT Object | (? ts'. r = AT ts' & invoConvertible CFS ts ts')

wideRefinvoonvertible_disj

invoConvertible CFS ts ts'
==> (? pt. ts = PTS pt & ts' = ts) |
    (? rs rs'. ts = RTS rs & ts' = RTS rs' & wideRefsConvertible CFS rs rs')

wideRefConvertible_CT_Object

[| wf_classfiles CFS; wideRefConvertible CFS (CT Object) r |] ==> r = CT Object

wRC

wideRefsConvertible CFS rs rs' = (! r:set rs. Bex (set rs') (wideRefConvertible CFS r))

Convertible_trans

wf_classfiles CFS
==> (! r' r''.
        wideRefConvertible CFS r r' --> wideRefConvertible CFS r' r'' --> wideRefConvertible CFS r r'') &
    (! t' t''. invoConvertible CFS t t' --> invoConvertible CFS t' t'' --> invoConvertible CFS t t'') &
    (! rs' rs''.
        wideRefsConvertible CFS rs rs' -->
        wideRefsConvertible CFS rs' rs'' --> wideRefsConvertible CFS rs rs'')

wf_cs9

[| wf_classfiles CFS; (sc, cn) : (d_superclass_rel CFS)^* |] ==> method_over_ok CFS cn sc

dyn_class_None

[| wf_classfiles CFS; is_class CFS cn; get_methods CFS !! cn ml = None; cn ~= Object;
   get_superclass CFS !! cn = sc |]
==> dyn_class (CFS, ml, cn) = dyn_class (CFS, ml, sc)

dyn_class_not_None

[| wf_classfiles CFS; is_class CFS cn; get_methods CFS !! cn ml ~= None |]
==> dyn_class (CFS, ml, cn) = cn

get_methods_None_Some_imp_neq

[| get_methods CFS !! cn ml = None; get_methods CFS !! mc ml = Some x |] ==> cn ~= mc

method_over_ok_lemma

[| method_over_ok CFS cn si; get_methods CFS !! si ml = Some (rd, ins);
   get_methods CFS !! cn ml ~= None |]
==> ? ins'. get_methods CFS !! cn ml = Some (rd, ins')

fd2ty_RT_AT

[| fd2tys CFS (get_obj_type obj) = RTS rs; ! r:set rs. wideRefConvertible CFS r (AT t') |]
==> ? fd ad. obj = Arr fd ad & invoConvertible CFS (fd2tys CFS fd) t'