Up to index of Isabelle/HOL/verificard
theory JVMType = Opt + Product + Listn + JType:(* Title: HOL/MicroJava/BV/JVM.thy
ID: $Id: JVMType.thy,v 1.1.2.10 2002/07/11 17:54:41 kleing Exp $
Author: Gerwin Klein
Copyright 2000 TUM
*)
header {* \isaheader{The JVM Type System as Semilattice} *}
theory JVMType = Opt + Product + Listn + JType:
types
locvars_type = "init_ty err list"
opstack_type = "init_ty list"
state_type = "opstack_type × locvars_type"
state_bool = "state_type × bool"
address_type = "state_bool set"
state = "address_type err" -- "for Kildall"
method_type = "address_type list" -- "for BVSpec"
class_type = "sig \<Rightarrow> method_type"
prog_type = "cname \<Rightarrow> class_type"
constdefs
address_types :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> address_type"
"address_types G maxs maxr maxpc \<equiv>
((Union {list n (init_tys G maxpc) |n. n \<le> maxs}) × list maxr (err (init_tys G maxpc))) × {True,False}"
states :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state set"
"states G maxs maxr maxpc \<equiv> err (Pow (address_types G maxs maxr maxpc))"
sl :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state sl"
"sl G maxs maxr maxpc \<equiv> SetSemilat.sl (address_types G maxs maxr maxpc)"
constdefs
le :: "state ord"
"le \<equiv> Err.le (op \<subseteq>)"
sup :: "state binop"
"sup \<equiv> lift2 (\<lambda>x y. OK (x \<union> y))"
lemma sl_def2:
"sl G mxs mxr mpc \<equiv> (states G mxs mxr mpc, le, sup)"
by (unfold sl_def SetSemilat.sl_def Err.sl_def
Err.esl_def sup_def states_def le_def) simp
lemma states_def2:
"states G mxs mxr mpc \<equiv> fst (sl G mxs mxr mpc)"
by (unfold sl_def2) simp
lemma le_def2:
"le \<equiv> fst (snd (sl G mxs mxr mpc))"
by (unfold sl_def2) simp
lemma sup_def2:
"sup \<equiv> snd (snd (sl G mxs mxr mpc))"
by (unfold sl_def2) simp
lemma finite_list [intro!]:
assumes A: "finite A"
shows "finite (list n A)"
proof (induct n)
have "list 0 A = {[]}" by auto
thus "finite (list 0 A)" by simp
next
fix n assume "finite (list n A)"
moreover
have "list (Suc n) A = split Cons ` (A × list n A)"
by (unfold list_def) (auto simp add: length_Suc_conv)
ultimately
show "finite (list (Suc n) A)" using A
by (auto intro: finite_imageI)
qed
lemma finite_Union [intro!]:
"finite X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> finite x) \<Longrightarrow> finite (Union X)"
by (simp add: Union_def)
lemma finite_count [intro!,simp]:
"finite {f x|x. x \<le> (n::nat)}"
proof (induct n)
show "finite {f x |x. x \<le> 0}" by simp
next
fix n assume "finite {f x |x. x \<le> n}"
moreover
have "{f x |x. x \<le> Suc n} = {f (Suc n)} \<union> {f x |x. x \<le> n}"
proof
show "{f (Suc n)} \<union> {f x |x. x \<le> n} \<subseteq> {f x |x. x \<le> Suc n}" by auto
{ fix y assume "y \<in> {f x |x. x \<le> Suc n}"
then obtain x where y: "y = f x" and "x \<le> Suc n" by auto
hence "x \<le> n \<or> x = Suc n" by auto
with y have "y \<in> {f (Suc n)} \<union> {f x |x. x \<le> n}" by auto
}
thus "{f x |x. x \<le> Suc n} \<subseteq> {f (Suc n)} \<union> {f x |x. x \<le> n}" ..
qed
ultimately
show "finite {f x |x. x \<le> Suc n}" by simp
qed
lemma finite_Union_list [intro!]:
"finite A \<Longrightarrow> finite (Union {list n A|n. n \<le> m})"
by auto
lemma finite_productI [intro!]:
"finite A \<Longrightarrow> finite B \<Longrightarrow> finite (A × B)"
by (erule finite_induct) auto
lemma finite_err [iff]:
"finite (err A) = finite A"
proof -
have "err A = insert Err (OK`A)" by (unfold err_def) auto
moreover have "inj_on OK A" by (unfold inj_on_def) auto
ultimately show ?thesis by (auto intro: finite_imageI dest: finite_imageD)
qed
lemma semilat_JVM: "semilat (sl G mxs mxr mpc)"
by (unfold sl_def) (rule semilat_set)
lemma finite_address_types: "finite (address_types G mxs mxr mpc)"
apply (insert finite_init_tys [of G mpc])
apply (unfold address_types_def)
apply auto
done
lemma acc_JVM: "acc le (states G mxs mxr mpc)"
apply (unfold states_def le_def)
apply (rule acc_err)
apply (rule acc_set)
apply (rule finite_address_types)
done
end
(*
constdefs
sup_ty_opt :: "['code prog,init_ty err,init_ty err] \<Rightarrow> bool"
("_ |- _ <=o _" [71,71] 70)
"sup_ty_opt G == Err.le (init_le G)"
sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool"
("_ |- _ <=l _" [71,71] 70)
"sup_loc G == Listn.le (sup_ty_opt G)"
sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"
("_ |- _ <=s _" [71,71] 70)
"sup_state G == Product.le (Listn.le (init_le G)) (sup_loc G)"
sup_state_bool :: "['code prog,state_bool,state_bool] \<Rightarrow> bool"
("_ |- _ <=b _" [71,71] 70)
"sup_state_bool G == Product.le (sup_state G) (op =)"
sup_state_opt :: "['code prog,state_bool option,state_bool option] \<Rightarrow> bool"
("_ |- _ <=' _" [71,71] 70)
"sup_state_opt G == Opt.le (sup_state_bool G)"
syntax (xsymbols)
sup_ty_opt :: "['code prog,init_ty err,init_ty err] \<Rightarrow> bool"
("_ \<turnstile> _ <=o _" [71,71] 70)
sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool"
("_ \<turnstile> _ <=l _" [71,71] 70)
sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"
("_ \<turnstile> _ <=s _" [71,71] 70)
sup_state_bool :: "['code prog,state_bool,state_bool] \<Rightarrow> bool"
("_ \<turnstile> _ <=b _" [71,71] 70)
sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool"
("_ \<turnstile> _ <=' _" [71,71] 70)
lemma UNIV_bool: "UNIV = {True,False}"
by blast
lemma JVM_states_unfold:
"states G maxs maxr == err(opt(((Union {list n (init_tys G) |n. n <= maxs}) <*>
list maxr (err(init_tys G))) <*> {True,False}))"
by (unfold states_def sl_def Opt.esl_def Err.sl_def
stk_esl_def reg_sl_def Product.esl_def
Listn.sl_def upto_esl_def Init.esl_def Err.esl_def TrivLat.esl_def)
(simp add: UNIV_bool)
lemma JVM_le_unfold:
"le G m n ==
Err.le(Opt.le(Product.le(Product.le(Listn.le(init_le G))
(Listn.le(Err.le(init_le G))))(op =)))"
apply (unfold le_def sl_def Opt.esl_def Err.sl_def
stk_esl_def reg_sl_def Product.esl_def
Listn.sl_def upto_esl_def Init.esl_def Err.esl_def TrivLat.esl_def)
by simp
lemma JVM_le_convert:
"le G m n (OK t1) (OK t2) = G \<turnstile> t1 <=' t2"
by (simp add: JVM_le_unfold Err.le_def lesub_def sup_state_opt_def
sup_state_def sup_loc_def sup_ty_opt_def sup_state_bool_def)
lemma JVM_le_Err_conv:
"le G m n = Err.le (sup_state_opt G)"
by (unfold sup_state_opt_def sup_state_def sup_state_bool_def sup_loc_def
sup_ty_opt_def JVM_le_unfold) simp
lemma zip_map [rule_format]:
"\<forall>a. length a = length b \<longrightarrow>
zip (map f a) (map g b) = map (\<lambda>(x,y). (f x, g y)) (zip a b)"
apply (induct b)
apply simp
apply clarsimp
apply (case_tac aa)
apply simp+
done
lemma [simp]: "Err.le r (OK a) (OK b) = r a b"
by (simp add: Err.le_def lesub_def)
lemma stk_convert:
"Listn.le (init_le G) a b = G \<turnstile> map OK a <=l map OK b"
proof
assume "Listn.le (init_le G) a b"
hence le: "list_all2 (init_le G) a b"
by (unfold Listn.le_def lesub_def)
{ fix x' y'
assume "length a = length b"
"(x',y') \<in> set (zip (map OK a) (map OK b))"
then
obtain x y where OK:
"x' = OK x" "y' = OK y" "(x,y) \<in> set (zip a b)"
by (auto simp add: zip_map)
with le
have "init_le G x y"
by (simp add: list_all2_def Ball_def)
with OK
have "G \<turnstile> x' <=o y'"
by (simp add: sup_ty_opt_def)
}
with le
show "G \<turnstile> map OK a <=l map OK b"
by (unfold sup_loc_def Listn.le_def lesub_def list_all2_def) auto
next
assume "G \<turnstile> map OK a <=l map OK b"
thus "Listn.le (init_le G) a b"
apply (unfold sup_loc_def list_all2_def Listn.le_def lesub_def)
apply (clarsimp simp add: zip_map)
apply (drule bspec, assumption)
apply (auto simp add: sup_ty_opt_def init_le_def)
done
qed
lemma sup_state_conv:
"(G \<turnstile> s1 <=s s2) ==
(G \<turnstile> map OK (fst s1) <=l map OK (fst s2)) \<and> (G \<turnstile> snd s1 <=l snd s2)"
by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def split_beta)
lemma subtype_refl [simp]:
"subtype G t t"
by (simp add: subtype_def)
theorem sup_ty_opt_refl [simp]:
"G \<turnstile> t <=o t"
by (simp add: sup_ty_opt_def Err.le_def lesub_def split: err.split)
lemma le_list_refl2 [simp]:
"(\<And>xs. r xs xs) \<Longrightarrow> Listn.le r xs xs"
by (induct xs, auto simp add: Listn.le_def lesub_def)
theorem sup_loc_refl [simp]:
"G \<turnstile> t <=l t"
by (simp add: sup_loc_def)
theorem sup_state_refl [simp]:
"G \<turnstile> s <=s s"
by (auto simp add: sup_state_def Product.le_def lesub_def)
theorem sup_state_opt_refl [simp]:
"G \<turnstile> s <=' s"
by (simp add: sup_state_opt_def sup_state_bool_def Product.le_def
Opt.le_def lesub_def split: option.split)
theorem anyConvErr [simp]:
"(G \<turnstile> Err <=o any) = (any = Err)"
by (simp add: sup_ty_opt_def Err.le_def split: err.split)
theorem OKanyConvOK [simp]:
"(G \<turnstile> (OK ty') <=o (OK ty)) = (G \<turnstile> ty' \<preceq>i ty)"
by (simp add: sup_ty_opt_def Err.le_def lesub_def)
lemma sup_ty_opt_OK:
"G \<turnstile> x <=o OK y = (\<exists>x'. x = OK x' \<and> G \<turnstile> x' \<preceq>i y)"
by (cases x, auto)
lemma widen_PrimT_conv1 [simp]:
"\<lbrakk> G \<turnstile> S \<preceq> T; S = PrimT x\<rbrakk> \<Longrightarrow> T = PrimT x"
by (auto elim: widen.elims)
theorem sup_PTS_eq:
"(G \<turnstile> OK (Init (PrimT p)) <=o X) = (X=Err \<or> X = OK (Init (PrimT p)))"
by (auto simp add: sup_ty_opt_def Err.le_def lesub_def init_le_def
subtype_def JType.esl_def
split: err.splits init_ty.splits)
theorem sup_loc_Nil [iff]:
"(G \<turnstile> [] <=l XT) = (XT=[])"
by (simp add: sup_loc_def Listn.le_def)
theorem sup_loc_Cons [iff]:
"(G \<turnstile> (Y#YT) <=l XT) = (\<exists>X XT'. XT=X#XT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT <=l XT'))"
by (simp add: sup_loc_def Listn.le_def lesub_def list_all2_Cons1)
theorem sup_loc_Cons2:
"(G \<turnstile> YT <=l (X#XT)) = (\<exists>Y YT'. YT=Y#YT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT' <=l XT))"
by (simp add: sup_loc_def Listn.le_def lesub_def list_all2_Cons2)
theorem sup_loc_length:
"G \<turnstile> a <=l b \<Longrightarrow> length a = length b"
proof -
assume G: "G \<turnstile> a <=l b"
have "\<forall>b. (G \<turnstile> a <=l b) \<longrightarrow> length a = length b"
by (induct a, auto)
with G
show ?thesis by blast
qed
theorem sup_loc_nth:
"\<lbrakk> G \<turnstile> a <=l b; n < length a \<rbrakk> \<Longrightarrow> G \<turnstile> (a!n) <=o (b!n)"
proof -
assume a: "G \<turnstile> a <=l b" "n < length a"
have "\<forall> n b. (G \<turnstile> a <=l b) \<longrightarrow> n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))"
(is "?P a")
proof (induct a)
show "?P []" by simp
fix x xs assume IH: "?P xs"
show "?P (x#xs)"
proof (intro strip)
fix n b
assume "G \<turnstile> (x # xs) <=l b" "n < length (x # xs)"
with IH
show "G \<turnstile> ((x # xs) ! n) <=o (b ! n)"
by - (cases n, auto)
qed
qed
with a
show ?thesis by blast
qed
theorem all_nth_sup_loc:
"\<forall>b. length a = length b \<longrightarrow> (\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n)))
\<longrightarrow> (G \<turnstile> a <=l b)" (is "?P a")
proof (induct a)
show "?P []" by simp
fix l ls assume IH: "?P ls"
show "?P (l#ls)"
proof (intro strip)
fix b
assume f: "\<forall>n. n < length (l # ls) \<longrightarrow> (G \<turnstile> ((l # ls) ! n) <=o (b ! n))"
assume l: "length (l#ls) = length b"
then obtain b' bs where b: "b = b'#bs"
by - (cases b, simp, simp add: neq_Nil_conv, rule that)
with f
have "\<forall>n. n < length ls \<longrightarrow> (G \<turnstile> (ls!n) <=o (bs!n))"
by auto
with f b l IH
show "G \<turnstile> (l # ls) <=l b"
by auto
qed
qed
theorem sup_loc_append:
"length a = length b \<Longrightarrow>
(G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))"
proof -
assume l: "length a = length b"
have "\<forall>b. length a = length b \<longrightarrow> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and>
(G \<turnstile> x <=l y))" (is "?P a")
proof (induct a)
show "?P []" by simp
fix l ls assume IH: "?P ls"
show "?P (l#ls)"
proof (intro strip)
fix b
assume "length (l#ls) = length (b::init_ty err list)"
with IH
show "(G \<turnstile> ((l#ls)@x) <=l (b@y)) = ((G \<turnstile> (l#ls) <=l b) \<and> (G \<turnstile> x <=l y))"
by - (cases b, auto)
qed
qed
with l
show ?thesis by blast
qed
theorem sup_loc_rev [simp]:
"(G \<turnstile> (rev a) <=l rev b) = (G \<turnstile> a <=l b)"
proof -
have "\<forall>b. (G \<turnstile> (rev a) <=l rev b) = (G \<turnstile> a <=l b)" (is "\<forall>b. ?Q a b" is "?P a")
proof (induct a)
show "?P []" by simp
fix l ls assume IH: "?P ls"
{
fix b
have "?Q (l#ls) b"
proof (cases (open) b)
case Nil
thus ?thesis by (auto dest: sup_loc_length)
next
case Cons
show ?thesis
proof
assume "G \<turnstile> (l # ls) <=l b"
thus "G \<turnstile> rev (l # ls) <=l rev b"
by (clarsimp simp add: Cons IH sup_loc_length sup_loc_append)
next
assume "G \<turnstile> rev (l # ls) <=l rev b"
hence G: "G \<turnstile> (rev ls @ [l]) <=l (rev list @ [a])"
by (simp add: Cons)
hence "length (rev ls) = length (rev list)"
by (auto dest: sup_loc_length)
from this G
obtain "G \<turnstile> rev ls <=l rev list" "G \<turnstile> l <=o a"
by (simp add: sup_loc_append)
thus "G \<turnstile> (l # ls) <=l b"
by (simp add: Cons IH)
qed
qed
}
thus "?P (l#ls)" by blast
qed
thus ?thesis by blast
qed
theorem sup_loc_update [rule_format]:
"\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow>
(G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x")
proof (induct x)
show "?P []" by simp
fix l ls assume IH: "?P ls"
show "?P (l#ls)"
proof (intro strip)
fix n y
assume "G \<turnstile>a <=o b" "G \<turnstile> (l # ls) <=l y" "n < length y"
with IH
show "G \<turnstile> (l # ls)[n := a] <=l y[n := b]"
by - (cases n, auto simp add: sup_loc_Cons2 list_all2_Cons1)
qed
qed
theorem sup_state_length [simp]:
"G \<turnstile> s2 <=s s1 \<Longrightarrow>
length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
by (auto dest: sup_loc_length
simp add: sup_state_def stk_convert lesub_def Product.le_def);
theorem sup_state_append_snd:
"length a = length b \<Longrightarrow>
(G \<turnstile> (i,a@x) <=s (j,b@y)) = ((G \<turnstile> (i,a) <=s (j,b)) \<and> (G \<turnstile> (i,x) <=s (j,y)))"
by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def
sup_loc_append)
theorem sup_state_append_fst:
"length a = length b \<Longrightarrow>
(G \<turnstile> (a@x,i) <=s (b@y,j)) = ((G \<turnstile> (a,i) <=s (b,j)) \<and> (G \<turnstile> (x,i) <=s (y,j)))"
by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_append)
theorem sup_state_Cons1:
"(G \<turnstile> (x#xt, a) <=s (yt, b)) =
(\<exists>y yt'. yt=y#yt' \<and> (G \<turnstile> x \<preceq>i y) \<and> (G \<turnstile> (xt,a) <=s (yt',b)))"
by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def map_eq_Cons)
theorem sup_state_Cons2:
"(G \<turnstile> (xt, a) <=s (y#yt, b)) =
(\<exists>x xt'. xt=x#xt' \<and> (G \<turnstile> x \<preceq>i y) \<and> (G \<turnstile> (xt',a) <=s (yt,b)))"
by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def
map_eq_Cons sup_loc_Cons2)
theorem sup_state_ignore_fst:
"G \<turnstile> (a, x) <=s (b, y) \<Longrightarrow> G \<turnstile> (c, x) <=s (c, y)"
by (simp add: sup_state_def lesub_def Product.le_def)
theorem sup_state_rev_fst:
"(G \<turnstile> (rev a, x) <=s (rev b, y)) = (G \<turnstile> (a, x) <=s (b, y))"
proof -
have m: "\<And>f x. map f (rev x) = rev (map f x)" by (simp add: rev_map)
show ?thesis by (simp add: m sup_state_def stk_convert lesub_def Product.le_def)
qed
lemma sup_state_opt_None_any [iff]:
"(G \<turnstile> None <=' any) = True"
by (simp add: sup_state_opt_def Opt.le_def split: option.split)
lemma sup_state_opt_any_None [iff]:
"(G \<turnstile> any <=' None) = (any = None)"
by (simp add: sup_state_opt_def Opt.le_def split: option.split)
lemma sup_state_opt_Some_Some [iff]:
"(G \<turnstile> (Some a) <=' (Some b)) = (G \<turnstile> a <=b b)"
by (simp add: sup_state_opt_def Opt.le_def lesub_def del: split_paired_Ex)
lemma sup_state_opt_any_Some [iff]:
"(G \<turnstile> (Some a) <=' any) = (\<exists>b. any = Some b \<and> G \<turnstile> a <=b b)"
by (simp add: sup_state_opt_def Opt.le_def lesub_def split: option.split)
lemma sup_state_opt_Some_any:
"(G \<turnstile> any <=' (Some b)) = (any = None \<or> (\<exists>a. any = Some a \<and> G \<turnstile> a <=b b))"
by (simp add: sup_state_opt_def Opt.le_def lesub_def split: option.split)
lemma sup_state_bool_conv[iff]:
"(G \<turnstile> (a,b) <=b (c,d)) = ((G \<turnstile> a <=s c) \<and> b = d)"
by (simp add: sup_state_bool_def Product.le_def lesub_def)
theorem sup_ty_opt_trans [trans]:
"\<lbrakk>G \<turnstile> a <=o b; G \<turnstile> b <=o c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=o c"
by (auto intro: init_trans
simp add: sup_ty_opt_def Err.le_def lesub_def subtype_def
split: err.splits)
theorem sup_loc_trans [trans]:
"\<lbrakk>G \<turnstile> a <=l b; G \<turnstile> b <=l c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=l c"
proof -
assume G: "G \<turnstile> a <=l b" "G \<turnstile> b <=l c"
hence "\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (c!n))"
proof (intro strip)
fix n
assume n: "n < length a"
with G
have "G \<turnstile> (a!n) <=o (b!n)"
by - (rule sup_loc_nth)
also
from n G
have "G \<turnstile> \<dots> <=o (c!n)"
by - (rule sup_loc_nth, auto dest: sup_loc_length)
finally
show "G \<turnstile> (a!n) <=o (c!n)" .
qed
with G
show ?thesis
by (auto intro!: all_nth_sup_loc [rule_format] dest!: sup_loc_length)
qed
theorem sup_state_trans [trans]:
"\<lbrakk>G \<turnstile> a <=s b; G \<turnstile> b <=s c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=s c"
by (auto intro: sup_loc_trans
simp add: sup_state_def stk_convert Product.le_def lesub_def)
theorem sup_state_bool_trans [trans]:
"\<lbrakk>G \<turnstile> a <=b b; G \<turnstile> b <=b c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=b c"
by (auto intro: sup_state_trans
simp add: sup_state_bool_def Product.le_def lesub_def)
theorem sup_state_opt_trans [trans]:
"\<lbrakk>G \<turnstile> a <=' b; G \<turnstile> b <=' c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=' c"
by (auto intro: sup_state_trans
simp add: sup_state_opt_def Opt.le_def lesub_def
split: option.splits)
*)
lemma sl_def2:
JVMType.sl G mxs mxr mpc == (states G mxs mxr mpc, JVMType.le, JVMType.sup)
lemma states_def2:
states G mxs mxr mpc == fst (JVMType.sl G mxs mxr mpc)
lemma le_def2:
JVMType.le == fst (snd (JVMType.sl G mxs mxr mpc))
lemma sup_def2:
JVMType.sup == snd (snd (JVMType.sl G mxs mxr mpc))
lemma
finite A ==> finite (list n A)
lemma finite_Union:
[| finite X; !!x. x : X ==> finite x |] ==> finite (Union X)
lemma finite_count:
finite {f x |x. x <= n}
lemma finite_Union_list:
finite A ==> finite (Union {list n A |n. n <= m})
lemma finite_productI:
[| finite A; finite B |] ==> finite (A <*> B)
lemma finite_err:
finite (err A) = finite A
lemma semilat_JVM:
semilat (JVMType.sl G mxs mxr mpc)
lemma finite_address_types:
finite (address_types G mxs mxr mpc)
lemma acc_JVM:
acc JVMType.le (states G mxs mxr mpc)