Up to index of Isabelle/HOL/jsr
theory JType = WellForm + SetSemilat:(* Title: HOL/MicroJava/BV/JType.thy
ID: $Id: JType.html,v 1.1 2002/11/28 14:17:20 kleing Exp $
Author: Tobias Nipkow, Gerwin Klein
Copyright 2000 TUM
*)
header {* \isaheader{The Java Type System as Semilattice} *}
theory JType = WellForm + SetSemilat:
consts
boundedRA :: "nat × ty \<Rightarrow> bool"
recdef boundedRA "{}"
"boundedRA (mpc,RA pc) = (pc < mpc)"
"boundedRA v = True"
constdefs
init_tys :: "'c prog \<Rightarrow> nat \<Rightarrow> init_ty set"
"init_tys G maxpc \<equiv> {Init T |T. is_type G T \<and> boundedRA (maxpc+1,T)} \<union>
{UnInit C pc |C pc. is_class G C \<and> pc < maxpc} \<union>
{PartInit C |C. is_class G C}"
init_le :: "'c prog \<Rightarrow> init_ty ord" ("_ |- _ <=i _" [71,71,71] 70)
"G |- a <=i b \<equiv> case a of
Init t1 \<Rightarrow> (case b of Init t2 \<Rightarrow> G \<turnstile> t1 \<preceq> t2
| UnInit c n \<Rightarrow> False
| PartInit c \<Rightarrow> False)
| UnInit c1 n1 \<Rightarrow> a = b
| PartInit c1 \<Rightarrow> a = b"
lemma boundedRA_def2:
"boundedRA (mpc, T) =
((\<exists>pc. T = RA pc \<and> pc < mpc) \<or>
T \<in> RefT ` UNIV \<or>
T \<in> PrimT ` {Void,Integer,Boolean})"
apply (cases T)
apply auto
apply (case_tac prim_ty)
apply auto
done
lemma finite_classes:
"finite {C. is_class G C}"
proof -
have "{C. is_class G C} = dom (map_of G)"
by (auto simp add: is_class_def class_def dom_def)
thus ?thesis by (simp add: finite_dom_map_of)
qed
lemma finite_init_tys: "finite (init_tys G mpc)"
proof -
note finite_classes [simp, intro]
note finite_imageI [simp,intro]
have "{T. is_type G T \<and> boundedRA (mpc+1,T)} =
{Class C|C. is_class G C} \<union> {NT} \<union>
PrimT ` {Void,Integer,Boolean} \<union> {RA pc|pc. pc < mpc+1}"
by (auto simp add: boundedRA_def2 split: ref_ty.splits)
moreover
have "{Class C|C. is_class G C} = RefT ` ClassT ` {C. is_class G C}" by auto
hence "finite {Class C|C. is_class G C}" by simp
moreover
have "\<forall>n. {RA pc|pc. pc < Suc n} = {RA n} \<union> {RA pc|pc. pc < n}" by auto
hence "finite {RA pc|pc. pc < mpc+1}" by (induct mpc) auto
ultimately
have "finite {T. is_type G T \<and> boundedRA (mpc+1, T)}" by simp
moreover
have "{Init T|T. is_type G T \<and> boundedRA (mpc+1, T)} =
Init ` {T. is_type G T \<and> boundedRA (mpc+1, T)}" by auto
ultimately
have "finite {Init T|T. is_type G T \<and> boundedRA (mpc+1, T)}" by simp
moreover {
have "\<forall>n. {pc. pc < Suc n} = {n} \<union> {pc. pc < n}" by auto
hence "finite {pc. pc < mpc}" by (induct mpc) auto
moreover
have "{UnInit C pc |C pc. is_class G C \<and> pc < mpc} =
(\<lambda>(C,pc). UnInit C pc) ` ({C. is_class G C} × {pc. pc < mpc})"
by auto
ultimately
have "finite {UnInit C pc |C pc. is_class G C \<and> pc < mpc}" by simp
}
moreover
have "{PartInit C |C. is_class G C} = PartInit ` {C. is_class G C}" by auto
hence "finite {PartInit C |C. is_class G C}" by simp
ultimately
show ?thesis by (unfold init_tys_def) auto
qed
lemma acc_JType: "acc (op \<subseteq>) (Pow (init_tys G mpc))"
by (rule acc_set [OF finite_init_tys])
syntax (xsymbols)
init_le :: "['code prog,init_ty,init_ty] \<Rightarrow> bool" ("_ \<turnstile> _ \<preceq>i _" [71,71,71] 70)
lemma le_Init_Init [iff]:
"G \<turnstile> Init t1 \<preceq>i Init t2 = G \<turnstile> t1 \<preceq> t2"
by (unfold init_le_def) simp
lemma le_Init_UnInit [iff]:
"init_le G (Init t) (UnInit c n) = False"
by (unfold init_le_def) simp
lemma le_UnInit_Init [iff]:
"init_le G (UnInit c n) (Init t) = False"
by (unfold init_le_def) simp
lemma le_UnInit_UnInit [iff]:
"init_le G (UnInit c1 n1) (UnInit c2 n2) = (c1 = c2 \<and> n1 = n2)"
by (unfold init_le_def) simp
lemma init_le_Init:
"(G \<turnstile> Init t \<preceq>i x) = (\<exists>t'. x = Init t' \<and> G \<turnstile> t \<preceq> t')"
by (simp add: init_le_def split: init_ty.splits)
lemma init_le_Init2:
"(G \<turnstile> x \<preceq>i (Init t')) = (\<exists>t. x = Init t \<and> G \<turnstile> t \<preceq> t')"
by (cases x, auto simp add: init_le_def)
lemma init_le_UnInit [iff]:
"(G \<turnstile> UnInit C pc \<preceq>i x) = (x = UnInit C pc)"
by (cases x, auto simp add: init_le_def)
lemma init_le_UnInit2 [iff]:
"(G \<turnstile> T \<preceq>i (UnInit C pc)) = (T = UnInit C pc)"
by (cases T, auto simp add: init_le_def)
lemma init_le_PartInit [iff]:
"(G \<turnstile> PartInit C \<preceq>i x) = (x = PartInit C)"
by (cases x, auto simp add: init_le_def)
lemma init_le_PartInit2 [iff]:
"G \<turnstile> x \<preceq>i PartInit C = (x = PartInit C)"
by (cases x, auto simp add: init_le_def)
lemma init_refl [iff]: "init_le G x x"
by (auto simp add: init_le_def split: init_ty.split)
lemma init_trans [trans]:
"\<lbrakk> init_le G a b; init_le G b c \<rbrakk> \<Longrightarrow> init_le G a c"
by (auto intro: widen_trans
simp add: init_le_def split: init_ty.splits)
end
lemma boundedRA_def2:
boundedRA (mpc, T) =
((EX pc. T = RA pc & pc < mpc) |
T : range RefT | T : PrimT ` {Void, Integer, Boolean})
lemma finite_classes:
finite (Collect (is_class G))
lemma finite_init_tys:
finite (init_tys G mpc)
lemma acc_JType:
acc op <= (Pow (init_tys G mpc))
lemma le_Init_Init:
G |- Init t1 <=i Init t2 = G |- t1 <= t2
lemma le_Init_UnInit:
G |- Init t <=i UnInit c n = False
lemma le_UnInit_Init:
G |- UnInit c n <=i Init t = False
lemma le_UnInit_UnInit:
G |- UnInit c1 n1 <=i UnInit c2 n2 = (c1 = c2 & n1 = n2)
lemma init_le_Init:
G |- Init t <=i x = (EX t'. x = Init t' & G |- t <= t')
lemma init_le_Init2:
G |- x <=i Init t' = (EX t. x = Init t & G |- t <= t')
lemma init_le_UnInit:
G |- UnInit C pc <=i x = (x = UnInit C pc)
lemma init_le_UnInit2:
G |- T <=i UnInit C pc = (T = UnInit C pc)
lemma init_le_PartInit:
G |- PartInit C <=i x = (x = PartInit C)
lemma init_le_PartInit2:
G |- x <=i PartInit C = (x = PartInit C)
lemma init_refl:
G |- x <=i x
lemma init_trans:
[| G |- a <=i b; G |- b <=i c |] ==> G |- a <=i c