equal
deleted
inserted
replaced
42 lemma PrimT_PrimT2: "(G \<turnstile> PrimT p \<preceq> xb) = (xb = PrimT p)" |
42 lemma PrimT_PrimT2: "(G \<turnstile> PrimT p \<preceq> xb) = (xb = PrimT p)" |
43 by (auto elim: widen.elims) |
43 by (auto elim: widen.elims) |
44 |
44 |
45 lemma is_tyI: |
45 lemma is_tyI: |
46 "[| is_type G T; wf_prog wf_mb G |] ==> is_ty G T" |
46 "[| is_type G T; wf_prog wf_mb G |] ==> is_ty G T" |
47 by (auto simp add: is_ty_def dest: subcls_C_Object |
47 by (auto simp add: is_ty_def intro: subcls_C_Object |
48 split: ty.splits ref_ty.splits) |
48 split: ty.splits ref_ty.splits) |
49 |
49 |
50 lemma is_type_conv: |
50 lemma is_type_conv: |
51 "wf_prog wf_mb G ==> is_type G T = is_ty G T" |
51 "wf_prog wf_mb G ==> is_type G T = is_ty G T" |
52 proof |
52 proof |