Up to index of Isabelle/HOL/objinit
theory Init = JType + JVMState:(* Title: HOL/MicroJava/BV/Init.thy
ID: $Id: Init.html,v 1.1 2002/11/28 14:12:09 kleing Exp $
Author: Gerwin Klein
Copyright 2001 TUM
*)
header {* \isaheader{Java Type System with Object Initialization} *}
(* fixme: init_ty is declared in JVMState *)
theory Init = JType + JVMState:
text {*
@{term init_ty} is still a (error) semilattice:
*}
constdefs
init_tys :: "'c prog \<Rightarrow> init_ty set"
"init_tys G == {x. \<exists>y \<in> (fst (JType.esl G)). x = Init y} \<union>
{x. \<exists>c n. x = UnInit c n} \<union> {x. \<exists>c. x = PartInit c}"
init_le :: "'c prog \<Rightarrow> init_ty ord" ("_ \<turnstile> _ \<preceq>i _" [71,71] 70)
"G \<turnstile> a \<preceq>i b == case a of
Init t1 \<Rightarrow> (case b of Init t2 \<Rightarrow> fst (snd (JType.esl G)) t1 t2
| UnInit c n \<Rightarrow> False
| PartInit c \<Rightarrow> False)
| UnInit c1 n1 \<Rightarrow> a = b
| PartInit c1 \<Rightarrow> a = b"
sup :: "'c prog \<Rightarrow> init_ty \<Rightarrow> init_ty \<Rightarrow> init_ty err"
"sup G a b ==
case a of
Init t1 \<Rightarrow> (case b of Init t2 \<Rightarrow> (case snd (snd (JType.esl G)) t1 t2 of
Err \<Rightarrow> Err | OK x \<Rightarrow> OK (Init x))
| UnInit c n \<Rightarrow> Err
| PartInit c \<Rightarrow> Err)
| UnInit c1 n1 \<Rightarrow> (case b of Init t \<Rightarrow> Err
| UnInit c2 n2 \<Rightarrow> (if a=b then OK a else Err)
| PartInit c2 \<Rightarrow> Err)
| PartInit c1 \<Rightarrow> (case b of Init t \<Rightarrow> Err
| UnInit c2 n2 \<Rightarrow> Err
| PartInit c2 \<Rightarrow> (if a=b then OK a else Err))"
esl :: "'c prog \<Rightarrow> init_ty esl"
"esl G == (init_tys G, init_le G, sup G)"
syntax (HTML)
init_le :: "['code prog,init_ty,init_ty] \<Rightarrow> bool" ("_ |- _ <=i _")
lemma le_Init_Init [iff]:
"init_le G (Init t1) (Init t2) = subtype G t1 t2"
by (unfold init_le_def JType.esl_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 JType.esl_def subtype_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 JType.esl_def subtype_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 [simp]: "init_le G x x"
by (auto simp add: init_le_def JType.esl_def subtype_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 JType.esl_def subtype_def
split: init_ty.splits)
lemma ac_order_init:
"acyclic (subcls1 G) \<Longrightarrow> order (init_le G)"
proof -
assume "acyclic (subcls1 G)"
hence "order (subtype G)"
by (rule order_widen)
hence [simp]: "\<And>x y. \<lbrakk> init_le G x y; init_le G y x \<rbrakk> \<Longrightarrow> x = y"
apply (unfold init_le_def JType.esl_def)
apply (simp split: init_ty.splits)
apply (unfold order_def lesub_def)
apply blast
done
show ?thesis
by (unfold order_def lesub_def) (auto intro: init_trans)
qed
lemma order_init:
"wf_prog wf_mb G \<Longrightarrow> order (init_le G)"
by (drule acyclic_subcls1, rule ac_order_init)
lemma wf_converse_subcls1_impl_acc_init:
"wf ((subcls1 G)¯) \<Longrightarrow> acc (init_le G)"
proof -
assume "wf ((subcls1 G)¯)"
hence "acc (subtype G)"
by (rule wf_converse_subcls1_impl_acc_subtype)
hence s: "\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. subtype G z y \<and> z \<noteq> y \<longrightarrow> y \<notin> Q)"
by (simp add: acc_def lesub_def le_def lesssub_def wf_eq_minimal)
{ fix Q x assume not_empty: "x \<in> (Q::init_ty set)"
let ?Q = "{t. Init t \<in> Q}"
have "\<exists>z\<in>Q. \<forall>y. (G \<turnstile> z \<preceq>i y) \<and> z \<noteq> y \<longrightarrow> y \<notin> Q"
proof (cases "\<exists>t. Init t \<in> Q")
case False with not_empty
show ?thesis
by (simp add: init_le_def JType.esl_def split: init_ty.split) blast
next
case True
hence "\<exists>t. t \<in> ?Q" by simp
with s obtain z where
"z\<in>?Q" "\<forall>y. subtype G z y \<and> z \<noteq> y \<longrightarrow> y \<notin> ?Q"
by - (erule allE, erule impE, blast+)
with not_empty
show ?thesis
by (simp add: init_le_def JType.esl_def split: init_ty.split) blast
qed
}
thus ?thesis
by (simp add: acc_def lesub_def le_def lesssub_def wf_eq_minimal)
qed
lemma err_closed_init:
"wf_prog wf_mb G \<Longrightarrow> closed (err (init_tys G)) (lift2 (sup G))"
proof -
assume wf: "wf_prog wf_mb G"
then obtain
"single_valued (subcls1 G)"
"acyclic (subcls1 G)"
by (blast dest: acyclic_subcls1 single_valued_subcls1)
with wf
have "closed (err (types G)) (lift2 (JType.sup G))"
by (rule closed_err_types)
hence [intro?]:
"\<And>x y. \<lbrakk> x\<in>err (types G); y\<in>err (types G) \<rbrakk>
\<Longrightarrow> lift2 (JType.sup G) x y \<in> err (types G)"
by (unfold closed_def plussub_def) blast
{ fix t1 t2
assume "Init t1 \<in> init_tys G" "Init t2 \<in> init_tys G"
then obtain
"OK t1 \<in> err (types G)" "OK t2 \<in> err (types G)"
by (unfold init_tys_def JType.esl_def) simp
hence "lift2 (JType.sup G) (OK t1) (OK t2) \<in> err (types G)" ..
moreover
fix t assume "JType.sup G t1 t2 = OK t"
ultimately
have "t \<in> types G"
by (unfold lift2_def) simp
hence "Init t \<in> init_tys G"
by (unfold init_tys_def JType.esl_def) simp
} note this [intro]
show ?thesis
by (unfold closed_def plussub_def lift2_def sup_def JType.esl_def)
(auto split: err.split init_ty.split)
qed
lemma err_semilat_init:
"wf_prog wf_mb G \<Longrightarrow> err_semilat (esl G)"
proof -
assume wf: "wf_prog wf_mb G"
moreover
from wf obtain sa:
"single_valued (subcls1 G)"
"acyclic (subcls1 G)"
by (blast dest: acyclic_subcls1 single_valued_subcls1)
with wf
have [simp]: "\<And>x y c. \<lbrakk> x \<in> types G; y \<in> types G; JType.sup G x y = OK c \<rbrakk>
\<Longrightarrow> subtype G x c \<and> subtype G y c"
by (simp add: sup_subtype_greater)
{ fix x y
assume err: "x\<in>err (init_tys G)" "y\<in>err (init_tys G)"
{ fix a b c
assume ok: "x = OK a" "y = OK b"
moreover
from ok err
have "a \<in> init_tys G \<and> b \<in> init_tys G"
by blast
moreover
assume "sup G a b = OK c"
ultimately
have "init_le G a c \<and> init_le G b c"
by (unfold init_le_def sup_def JType.esl_def init_tys_def)
(auto split: init_ty.splits split_if_asm err.splits)
}
hence "Err.le (init_le G) x (lift2 (sup G) x y) \<and>
Err.le (init_le G) y (lift2 (sup G) x y)"
by (simp add: Err.le_def lift2_def lesub_def split: err.split)
}
moreover
{ have [intro]:
"\<And>a b c. \<lbrakk> init_le G a c; init_le G b c; sup G a b = Err \<rbrakk> \<Longrightarrow> False"
by (unfold sup_def init_le_def JType.esl_def)
(auto intro: sup_exists split: init_ty.split_asm err.split_asm)
{ fix x y z s
assume "x \<in> init_tys G" "y \<in> init_tys G" "z \<in> init_tys G"
"init_le G x z" "init_le G y z" "sup G x y = OK s"
with wf sa
have "init_le G s z"
by (unfold init_le_def sup_def init_tys_def JType.esl_def)
(auto intro: sup_subtype_smallest split: init_ty.split_asm err.split_asm)
} note this [intro]
fix x y z
assume "x\<in>err (init_tys G)" "y\<in>err (init_tys G)" "z\<in>err (init_tys G)"
"Err.le (init_le G) x z" "Err.le (init_le G) y z"
hence "Err.le (init_le G) (lift2 (sup G) x y) z"
by (unfold lesub_def plussub_def Err.le_def lift2_def JType.esl_def)
(auto split: err.splits)
}
ultimately
show ?thesis
by (unfold semilat_def Err.sl_def esl_def plussub_def lesub_def)
(simp add: err_closed_init order_init)
qed
end
lemma le_Init_Init:
G |- Init t1 <=i Init t2 = subtype 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
lemma ac_order_init:
acyclic (subcls1 G) ==> order (init_le G)
lemma order_init:
wf_prog wf_mb G ==> order (init_le G)
lemma wf_converse_subcls1_impl_acc_init:
wf ((subcls1 G)^-1) ==> acc (init_le G)
lemma err_closed_init:
wf_prog wf_mb G ==> closed (err (init_tys G)) (lift2 (Init.sup G))
lemma err_semilat_init:
wf_prog wf_mb G ==> semilat (sl (Init.esl G))