Up to index of Isabelle/HOL/arrays
theory JType = WellForm + SetSemilat + JVMState:(* Title: HOL/MicroJava/BV/JType.thy
ID: $Id: JType.html,v 1.1 2002/11/28 16:11:18 kleing Exp $
Author: Tobias Nipkow, Gerwin Klein
Copyright 2000 TUM
*)
header {* \isaheader{The Java Type System as Semilattice} *}
theory JType = WellForm + SetSemilat + JVMState:
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) \<and> dim T \<le> max_dim \<and> (isArray T \<longrightarrow> noRA 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 dim_0:
"{T. dim T = 0} =
{Class C|C. True} \<union> {NT} \<union> PrimT ` {Void,Integer,Boolean} \<union> {RA pc|pc. True}"
apply simp
apply auto
apply (case_tac x)
apply auto
apply (case_tac prim_ty)
apply auto
apply (case_tac ref_ty)
apply auto
done
lemma dim_Suc:
"(dim T = Suc n) = (\<exists>T'. T = T'.[] \<and> dim T' = n)"
apply (cases T)
apply simp
apply (case_tac ref_ty)
apply auto
done
lemma boundedRAI1:
"¬is_RA T \<Longrightarrow> boundedRA (n,T)"
apply (cases T)
apply auto
apply (case_tac prim_ty)
apply auto
done
lemma noRA_isnotRA:
"noRA T \<Longrightarrow> ¬is_RA T"
by (cases T, auto)
lemma boundedRAI2:
"noRA T \<Longrightarrow> boundedRA (n,T)"
by (simp add: boundedRAI1 noRA_isnotRA)
lemma not_isArray:
"dim T = 0 = (¬isArray T)"
apply (cases T)
apply auto
apply (case_tac ref_ty)
apply auto
apply (case_tac ref_ty)
apply auto
done
lemma isArray_def:
"isArray T = (\<exists>T'. T = T'.[])"
apply (cases T)
apply auto
apply (case_tac ref_ty)
apply auto
done
lemma finite_types:
"finite {T. is_type G T \<and> boundedRA (mpc+1,T) \<and> dim T \<le> n \<and> (isArray T \<longrightarrow> noRA T)}"
(is "finite (?set n)")
proof (induct n)
note finite_classes [simp, intro]
note finite_imageI [simp,intro]
have "?set 0 =
{T. dim T = 0} \<inter> {T. is_type G T \<and> boundedRA (mpc+1,T)}"
by (auto simp add: not_isArray)
also have "{T. dim T = 0} =
{Class C|C. True} \<union> {NT} \<union> PrimT ` {Void,Integer,Boolean} \<union> {RA pc|pc. True}"
by (rule dim_0)
also have "\<dots> \<inter> {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
finally have "?set 0 = \<dots>" .
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
show "finite (?set 0)" by simp
next
case (Suc n)
have "?set (Suc n) \<subseteq> ?set n \<union> (RefT o ArrayT) ` ?set n"
proof
fix T assume "T \<in> ?set (Suc n)"
then obtain T:
"is_type G T" "boundedRA (Suc mpc, T)" "dim T \<le> Suc n" "isArray T \<longrightarrow> noRA T"
by simp
{ assume "isArray T"
then obtain T' where "T = T'.[]" by (clarsimp simp add: isArray_def)
with T have "T \<in> (RefT \<circ> ArrayT) ` ?set n" by (auto simp add: boundedRAI2)
} moreover {
assume "¬isArray T"
with T have "T \<in> ?set n" by (simp, simp add: not_isArray [symmetric])
} ultimately
show "T \<in> ?set n \<union> (RefT \<circ> ArrayT) ` ?set n" by (cases) auto
qed
thus "finite (?set (Suc n))" using Suc
by (blast intro: finite_subset finite_UnI finite_imageI)
qed
lemma finite_init_tys: "finite (init_tys G mpc)"
proof -
note finite_classes [simp, intro]
note finite_imageI [simp,intro]
let "?P T" =
"is_type G T \<and> boundedRA (mpc+1,T) \<and> dim T \<le> max_dim \<and> (isArray T \<longrightarrow> noRA T)"
have "{Init T|T. ?P T} = Init ` {T. ?P T}" by auto
moreover
have "finite {T. ?P T}" by (rule finite_types)
ultimately
have "finite {Init T|T. ?P 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 dim_0:
{T. dim T = 0} =
{Class C |C. True} Un {NT} Un PrimT ` {Void, Integer, Boolean} Un
{RA pc |pc. True}
lemma dim_Suc:
(dim T = Suc n) = (EX T'. T = T'.[] & dim T' = n)
lemma boundedRAI1:
¬ is_RA T ==> boundedRA (n, T)
lemma noRA_isnotRA:
noRA T ==> ¬ is_RA T
lemma boundedRAI2:
noRA T ==> boundedRA (n, T)
lemma not_isArray:
(dim T = 0) = (¬ isArray T)
lemma isArray_def:
isArray T = (EX T'. T = T'.[])
lemma finite_types:
finite
{T. is_type G T & boundedRA (mpc + 1, T) & dim T <= n & (isArray T --> noRA T)}
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