--- a/src/HOL/MicroJava/BV/Err.thy Mon Mar 18 11:47:03 2002 +0100
+++ b/src/HOL/MicroJava/BV/Err.thy Wed Mar 20 13:21:07 2002 +0100
@@ -135,14 +135,14 @@
"~(Err <_(le r) x)"
by (simp add: lesssub_def lesub_def le_def split: err.split)
-lemma semilat_errI:
+lemma semilat_errI [intro]:
"semilat(A,r,f) \<Longrightarrow> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
apply (unfold semilat_Def closed_def plussub_def lesub_def
lift2_def Err.le_def err_def)
apply (simp split: err.split)
done
-lemma err_semilat_eslI:
+lemma err_semilat_eslI [intro, simp]:
"\<And>L. semilat L \<Longrightarrow> err_semilat(esl L)"
apply (unfold sl_def esl_def)
apply (simp (no_asm_simp) only: split_tupled_all)
--- a/src/HOL/MicroJava/BV/Kildall.thy Mon Mar 18 11:47:03 2002 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy Wed Mar 20 13:21:07 2002 +0100
@@ -8,22 +8,8 @@
header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *}
-theory Kildall = Typing_Framework + While_Combinator + Product:
-
+theory Kildall = SemilatAlg + While_Combinator:
-syntax "@lesubstep_type" :: "(nat \<times> 's) list \<Rightarrow> 's ord \<Rightarrow> (nat \<times> 's) list \<Rightarrow> bool"
- ("(_ /<=|_| _)" [50, 0, 51] 50)
-translations
- "x <=|r| y" == "x <=[(Product.le (op =) r)] y"
-
-
-constdefs
- pres_type :: "'s step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
-"pres_type step n A == \<forall>s\<in>A. \<forall>p<n. \<forall>(q,s')\<in>set (step p s). s' \<in> A"
-
- mono :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
-"mono r step n A ==
- \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> step p s <=|r| step p t"
consts
iter :: "'s binop \<Rightarrow> 's step_type \<Rightarrow>
@@ -60,12 +46,6 @@
lemmas [simp] = Let_def le_iff_plus_unchanged [symmetric]
-consts
- "@plusplussub" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
-primrec
- "[] ++_f y = y"
- "(x#xs) ++_f y = xs ++_f (x +_f y)"
-
lemma nth_merges:
"\<And>ss. \<lbrakk> semilat (A, r, f); p < length ss; ss \<in> list n A;
\<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow>
@@ -97,18 +77,6 @@
qed
-lemma pres_typeD:
- "\<lbrakk> pres_type step n A; s\<in>A; p<n; (q,s')\<in>set (step p s) \<rbrakk> \<Longrightarrow> s' \<in> A"
- by (unfold pres_type_def, blast)
-
-lemma boundedD:
- "\<lbrakk> bounded step n; p < n; (q,t) : set (step p xs) \<rbrakk> \<Longrightarrow> q < n"
- by (unfold bounded_def, blast)
-
-lemma monoD:
- "\<lbrakk> mono r step n A; p < n; s\<in>A; s <=_r t \<rbrakk> \<Longrightarrow> step p s <=|r| step p t"
- by (unfold mono_def, blast)
-
(** merges **)
lemma length_merges [rule_format, simp]:
@@ -250,113 +218,6 @@
(** iter **)
-lemma plusplus_closed:
- "\<And>y. \<lbrakk>semilat (A, r, f); set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> x ++_f y \<in> A"
-proof (induct x)
- show "\<And>y. y \<in> A \<Longrightarrow> [] ++_f y \<in> A" by simp
- fix y x xs
- assume sl: "semilat (A, r, f)" and y: "y \<in> A" and xs: "set (x#xs) \<subseteq> A"
- assume IH: "\<And>y. \<lbrakk>semilat (A, r, f); set xs \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> xs ++_f y \<in> A"
- from xs obtain x: "x \<in> A" and "set xs \<subseteq> A" by simp
- from sl x y have "(x +_f y) \<in> A" by (simp add: closedD)
- with sl xs have "xs ++_f (x +_f y) \<in> A" by - (rule IH)
- thus "(x#xs) ++_f y \<in> A" by simp
-qed
-
-lemma ub2: "\<And>y. \<lbrakk>semilat (A, r, f); set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r x ++_f y"
-proof (induct x)
- show "\<And>y. semilat(A, r, f) \<Longrightarrow> y <=_r [] ++_f y" by simp
-
- fix y a l
- assume sl: "semilat (A, r, f)"
- assume y: "y \<in> A"
- assume "set (a#l) \<subseteq> A"
- then obtain a: "a \<in> A" and x: "set l \<subseteq> A" by simp
- assume "\<And>y. \<lbrakk>semilat (A, r, f); set l \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r l ++_f y"
- hence IH: "\<And>y. y \<in> A \<Longrightarrow> y <=_r l ++_f y" .
-
- from sl have "order r" .. note order_trans [OF this, trans]
-
- from sl a y have "y <=_r a +_f y" by (rule semilat_ub2)
- also
- from sl a y have "a +_f y \<in> A" by (simp add: closedD)
- hence "(a +_f y) <=_r l ++_f (a +_f y)" by (rule IH)
- finally
- have "y <=_r l ++_f (a +_f y)" .
- thus "y <=_r (a#l) ++_f y" by simp
-qed
-
-
-lemma ub1:
- "\<And>y. \<lbrakk>semilat (A, r, f); set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
-proof (induct ls)
- show "\<And>y. x \<in> set [] \<Longrightarrow> x <=_r [] ++_f y" by simp
-
- fix y s ls
- assume sl: "semilat (A, r, f)"
- hence "order r" .. note order_trans [OF this, trans]
- assume "set (s#ls) \<subseteq> A"
- then obtain s: "s \<in> A" and ls: "set ls \<subseteq> A" by simp
- assume y: "y \<in> A"
-
- assume
- "\<And>y. \<lbrakk>semilat (A, r, f); set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
- hence IH: "\<And>y. x \<in> set ls \<Longrightarrow> y \<in> A \<Longrightarrow> x <=_r ls ++_f y" .
-
- assume "x \<in> set (s#ls)"
- then obtain xls: "x = s \<or> x \<in> set ls" by simp
- moreover {
- assume xs: "x = s"
- from sl s y have "s <=_r s +_f y" by (rule semilat_ub1)
- also
- from sl s y have "s +_f y \<in> A" by (simp add: closedD)
- with sl ls have "(s +_f y) <=_r ls ++_f (s +_f y)" by (rule ub2)
- finally
- have "s <=_r ls ++_f (s +_f y)" .
- with xs have "x <=_r ls ++_f (s +_f y)" by simp
- }
- moreover {
- assume "x \<in> set ls"
- hence "\<And>y. y \<in> A \<Longrightarrow> x <=_r ls ++_f y" by (rule IH)
- moreover
- from sl s y
- have "s +_f y \<in> A" by (simp add: closedD)
- ultimately
- have "x <=_r ls ++_f (s +_f y)" .
- }
- ultimately
- have "x <=_r ls ++_f (s +_f y)" by blast
- thus "x <=_r (s#ls) ++_f y" by simp
-qed
-
-
-lemma ub1':
- "\<lbrakk>semilat (A, r, f); \<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk>
- \<Longrightarrow> b <=_r map snd [(p', t')\<in>S. p' = a] ++_f y"
-proof -
- let "b <=_r ?map ++_f y" = ?thesis
-
- assume "semilat (A, r, f)" "y \<in> A"
- moreover
- assume "\<forall>(p,s) \<in> set S. s \<in> A"
- hence "set ?map \<subseteq> A" by auto
- moreover
- assume "(a,b) \<in> set S"
- hence "b \<in> set ?map" by (induct S, auto)
- ultimately
- show ?thesis by - (rule ub1)
-qed
-
-
-
-lemma plusplus_empty:
- "\<forall>s'. (q, s') \<in> set S \<longrightarrow> s' +_f ss ! q = ss ! q \<Longrightarrow>
- (map snd [(p', t')\<in> S. p' = q] ++_f ss ! q) = ss ! q"
-apply (induct S)
-apply auto
-done
-
-
lemma stable_pres_lemma:
"\<lbrakk> semilat (A,r,f); pres_type step n A; bounded step n;
ss \<in> list n A; p \<in> w; \<forall>q\<in>w. q < n;
@@ -435,23 +296,6 @@
done
-lemma lesub_step_type:
- "\<And>b x y. a <=|r| b \<Longrightarrow> (x,y) \<in> set a \<Longrightarrow> \<exists>y'. (x, y') \<in> set b \<and> y <=_r y'"
-apply (induct a)
- apply simp
-apply simp
-apply (case_tac b)
- apply simp
-apply simp
-apply (erule disjE)
- apply clarify
- apply (simp add: lesub_def)
- apply blast
-apply clarify
-apply blast
-done
-
-
lemma merges_bounded_lemma:
"\<lbrakk> semilat (A,r,f); mono r step n A; bounded step n;
\<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n;
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Mon Mar 18 11:47:03 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Wed Mar 20 13:21:07 2002 +0100
@@ -6,288 +6,224 @@
header {* \isaheader{Correctness of the LBV} *}
-(* This theory is currently broken. The port to exceptions
- didn't make it into the Isabelle 2001 release. It is included for
- documentation only. See Isabelle 99-2 for a working copy of this
- theory. *)
-
-
-theory LBVCorrect = BVSpec + LBVSpec:
-
-lemmas [simp del] = split_paired_Ex split_paired_All
+theory LBVCorrect = LBVSpec + Typing_Framework:
constdefs
-fits :: "[method_type,instr list,jvm_prog,ty,state_type option,nat,nat,exception_table,certificate] \<Rightarrow> bool"
-"fits phi is G rT s0 maxs maxr et cert ==
- (\<forall>pc s1. pc < length is \<longrightarrow>
- (wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s0 = OK s1 \<longrightarrow>
- (case cert!pc of None \<Rightarrow> phi!pc = s1
- | Some t \<Rightarrow> phi!pc = Some t)))"
+fits :: "'s option list \<Rightarrow> 's certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow>
+ 's steptype \<Rightarrow> 's option \<Rightarrow> 'a list \<Rightarrow> bool"
+"fits phi cert f r step s0 is \<equiv>
+ length phi = length is \<and>
+ (\<forall>pc s. pc < length is -->
+ (wtl_inst_list (take pc is) cert f r step 0 s0 = OK s \<longrightarrow>
+ (case cert!pc of None => phi!pc = s
+ | Some t => phi!pc = Some t)))"
-constdefs
-make_phi :: "[instr list,jvm_prog,ty,state_type option,nat,nat,exception_table,certificate] \<Rightarrow> method_type"
-"make_phi is G rT s0 maxs maxr et cert ==
+make_phi :: "'s certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow>
+ 's steptype \<Rightarrow> 's option \<Rightarrow> 'a list \<Rightarrow> 's option list"
+"make_phi cert f r step s0 is \<equiv>
map (\<lambda>pc. case cert!pc of
- None \<Rightarrow> ok_val (wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s0)
- | Some t \<Rightarrow> Some t) [0..length is(]"
-
+ None => ok_val (wtl_inst_list (take pc is) cert f r step 0 s0)
+ | Some t => Some t) [0..length is(]"
-lemma fitsD_None:
- "\<lbrakk>fits phi is G rT s0 mxs mxr et cert; pc < length is;
- wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s0 = OK s1;
- cert ! pc = None\<rbrakk> \<Longrightarrow> phi!pc = s1"
+lemma fitsD_None [intro?]:
+ "\<lbrakk> fits phi cert f r step s0 is; pc < length is;
+ wtl_inst_list (take pc is) cert f r step 0 s0 = OK s;
+ cert!pc = None \<rbrakk> \<Longrightarrow> phi!pc = s"
by (auto simp add: fits_def)
-lemma fitsD_Some:
- "\<lbrakk>fits phi is G rT s0 mxs mxr et cert; pc < length is;
- wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s0 = OK s1;
- cert ! pc = Some t\<rbrakk> \<Longrightarrow> phi!pc = Some t"
+lemma fitsD_Some [intro?]:
+ "\<lbrakk> fits phi cert f r step s0 is; pc < length is;
+ wtl_inst_list (take pc is) cert f r step 0 s0 = OK s;
+ cert!pc = Some t \<rbrakk> \<Longrightarrow> phi!pc = Some t"
by (auto simp add: fits_def)
lemma make_phi_Some:
- "\<lbrakk> pc < length is; cert!pc = Some t \<rbrakk> \<Longrightarrow>
- make_phi is G rT s0 mxs mxr et cert ! pc = Some t"
+ "pc < length is \<Longrightarrow> cert!pc = Some t \<Longrightarrow>
+ make_phi cert f r step s0 is ! pc = Some t"
by (simp add: make_phi_def)
lemma make_phi_None:
- "\<lbrakk> pc < length is; cert!pc = None \<rbrakk> \<Longrightarrow>
- make_phi is G rT s0 mxs mxr et cert ! pc =
- ok_val (wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s0)"
+ "pc < length is \<Longrightarrow> cert!pc = None \<Longrightarrow>
+ make_phi cert f r step s0 is ! pc =
+ ok_val (wtl_inst_list (take pc is) cert f r step 0 s0)"
+ by (simp add: make_phi_def)
+
+lemma make_phi_len:
+ "length (make_phi cert f r step s0 is) = length is"
by (simp add: make_phi_def)
lemma exists_phi:
- "\<exists>phi. fits phi is G rT s0 mxs mxr et cert"
+ "\<exists>phi. fits phi cert f r step s0 is"
proof -
- have "fits (make_phi is G rT s0 mxs mxr et cert) is G rT s0 mxs mxr et cert"
- by (auto simp add: fits_def make_phi_Some make_phi_None
+ have "fits (make_phi cert f r step s0 is) cert f r step s0 is"
+ by (auto simp add: fits_def make_phi_Some make_phi_None make_phi_len
split: option.splits)
thus ?thesis by fast
qed
-lemma fits_lemma1:
- "\<lbrakk> wtl_inst_list is G rT cert mxs mxr (length is) et 0 s = OK s'; fits phi is G rT s mxs mxr et cert \<rbrakk>
+lemma fits_lemma1 [intro?]:
+ "\<lbrakk>wtl_inst_list is cert f r step 0 s \<noteq> Err; fits phi cert f r step s is\<rbrakk>
\<Longrightarrow> \<forall>pc t. pc < length is \<longrightarrow> cert!pc = Some t \<longrightarrow> phi!pc = Some t"
proof (intro strip)
fix pc t
- assume "wtl_inst_list is G rT cert mxs mxr (length is) et 0 s = OK s'"
+ assume "wtl_inst_list is cert f r step 0 s \<noteq> Err"
then obtain s'' where
- "wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s = OK s''"
+ "wtl_inst_list (take pc is) cert f r step 0 s = OK s''"
by (blast dest: wtl_take)
moreover
- assume "fits phi is G rT s mxs mxr et cert"
- "pc < length is"
- "cert ! pc = Some t"
+ assume "fits phi cert f r step s is"
+ "pc < length is" "cert ! pc = Some t"
ultimately
show "phi!pc = Some t" by (auto dest: fitsD_Some)
qed
lemma wtl_suc_pc:
- "\<lbrakk> wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err;
- wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s = OK s';
- wtl_cert (is!pc) G rT s' cert mxs mxr (length is) et pc = OK s'';
- fits phi is G rT s mxs mxr et cert; Suc pc < length is \<rbrakk> \<Longrightarrow>
- G \<turnstile> s'' <=' phi ! Suc pc"
+ assumes
+ semi: "err_semilat (A,r,f)" and
+ all: "wtl_inst_list is cert f r step 0 s0 \<noteq> Err" and
+ wtl: "wtl_inst_list (take pc is) cert f r step 0 s0 = OK s'" and
+ cert: "wtl_cert cert f r step pc s' = OK s''" and
+ fits: "fits phi cert f r step s0 is" and
+ pc: "pc+1 < length is"
+ shows "OK s'' \<le>|r OK (phi!(pc+1))"
proof -
-
- assume all: "wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err"
- assume fits: "fits phi is G rT s mxs mxr et cert"
+ from wtl cert pc
+ have wts: "wtl_inst_list (take (pc+1) is) cert f r step 0 s0 = OK s''"
+ by (rule wtl_Suc)
+ moreover
+ from all pc
+ have "\<exists>s' s''. wtl_inst_list (take (pc+1) is) cert f r step 0 s0 = OK s' \<and>
+ wtl_cert cert f r step (pc+1) s' = OK s''"
+ by (rule wtl_all)
+ ultimately
+ obtain x where "wtl_cert cert f r step (pc+1) s'' = OK x" by auto
+ hence "\<And>t. cert!(pc+1) = Some t \<Longrightarrow> OK s'' \<le>|r OK (cert!(pc+1))"
+ by (simp add: wtl_cert_def split: split_if_asm)
+ also from fits pc wts
+ have "\<And>t. cert!(pc+1) = Some t \<Longrightarrow> cert!(pc+1) = phi!(pc+1)"
+ by (auto dest!: fitsD_Some)
+ finally have "\<And>t. cert!(pc+1) = Some t \<Longrightarrow> OK s'' \<le>|r OK (phi!(pc+1))" .
+ moreover
+ from fits pc wts have "cert!(pc+1) = None \<Longrightarrow> s'' = phi!(pc+1)"
+ by (rule fitsD_None [symmetric])
+ with semi have "cert!(pc+1) = None \<Longrightarrow> OK s'' \<le>|r OK (phi!(pc+1))" by simp
+ ultimately
+ show "OK s'' \<le>|r OK (phi!(pc+1))" by (cases "cert!(pc+1)", blast+)
+qed
- assume wtl: "wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s = OK s'" and
- wtc: "wtl_cert (is!pc) G rT s' cert mxs mxr (length is) et pc = OK s''" and
- pc: "Suc pc < length is"
-
- hence wts:
- "wtl_inst_list (take (Suc pc) is) G rT cert mxs mxr (length is) et 0 s = OK s''"
- by (rule wtl_Suc)
-
- from all
- have app:
- "wtl_inst_list (take (Suc pc) is@drop (Suc pc) is) G rT cert mxs mxr (length is) et 0 s \<noteq> Err"
- by simp
+lemma wtl_stable:
+ assumes
+ semi: "err_semilat (A,r,f)" and
+ pres: "pres_type step (length is) (err (opt A))" and
+ s0_in_A: "s0 \<in> opt A" and
+ cert_ok: "cert_ok cert (length is) A" and
+ fits: "fits phi cert f r step s0 is" and
+ wtl: "wtl_inst_list is cert f r step 0 s0 \<noteq> Err" and
+ pc: "pc < length is" and
+ bounded: "bounded step (length is)"
+ shows "stable (Err.le (Opt.le r)) step (map OK phi) pc"
+proof (unfold stable_def, clarify)
+ fix pc' s' assume step: "(pc',s') \<in> set (step pc ((map OK phi) ! pc))"
+ (is "(pc',s') \<in> set (?step pc)")
+
+ from step pc bounded have pc': "pc' < length is"
+ by (unfold bounded_def) blast
+
+ from wtl pc obtain s1 s2 where
+ tkpc: "wtl_inst_list (take pc is) cert f r step 0 s0 = OK s1" and
+ cert: "wtl_cert cert f r step pc s1 = OK s2"
+ by - (drule wtl_all, auto)
- from pc
- have "0 < length (drop (Suc pc) is)"
- by simp
- then obtain l ls where
- "drop (Suc pc) is = l#ls"
- by (auto simp add: neq_Nil_conv simp del: length_drop)
- with app wts pc
- obtain x where
- "wtl_cert l G rT s'' cert mxs mxr (length is) et (Suc pc) = OK x"
- by (auto simp add: wtl_append min_def simp del: append_take_drop_id)
+ have c_Some: "\<forall>pc t. pc < length is \<longrightarrow> cert!pc = Some t \<longrightarrow> phi!pc = Some t" ..
+ have c_None: "cert!pc = None \<Longrightarrow> phi!pc = s1" ..
+
+ from cert pc c_None c_Some
+ have inst: "wtl_inst cert f r step pc (phi!pc) = OK s2"
+ by (simp add: wtl_cert_def split: option.splits split_if_asm)
+
+ from semi have "order (Err.le (Opt.le r))" by simp note order_trans [OF this, trans]
+
+ from pc fits have [simp]: "map OK phi!pc = OK (phi!pc)" by (simp add: fits_def)
+ from pc' fits have [simp]: "map OK phi!pc' = OK (phi!pc')" by (simp add: fits_def)
+
+ have "s1 \<in> opt A" by (rule wtl_inst_list_pres)
+ with pc c_Some cert_ok c_None
+ have "phi!pc \<in> opt A" by (cases "cert!pc") (auto dest: cert_okD)
+ with pc pres
+ have step_in_A: "\<forall>(pc',s') \<in> set (?step pc). s' \<in> err (opt A)"
+ by (auto dest: pres_typeD)
- hence c1: "\<And>t. cert!Suc pc = Some t \<Longrightarrow> G \<turnstile> s'' <=' cert!Suc pc"
- by (simp add: wtl_cert_def split: split_if_asm)
- moreover
- from fits pc wts
- have c2: "\<And>t. cert!Suc pc = Some t \<Longrightarrow> phi!Suc pc = cert!Suc pc"
- by - (drule fitsD_Some, auto)
- moreover
- from fits pc wts
- have c3: "cert!Suc pc = None \<Longrightarrow> phi!Suc pc = s''"
- by (rule fitsD_None)
- ultimately
- show ?thesis by (cases "cert!Suc pc", auto)
+ show "s' \<le>|r (map OK phi) ! pc'"
+ proof (cases "pc' = pc+1")
+ case True
+ with pc' cert_ok
+ have cert_in_A: "OK (cert!(pc+1)) \<in> err (opt A)" by (auto dest: cert_okD)
+ from inst
+ have ok: "OK s2 = merge cert f r pc (?step pc) (OK (cert!(pc+1)))"
+ by (simp add: wtl_inst_def)
+ also
+ have "\<dots> = (map snd [(p',t')\<in>?step pc. p'=pc+1] ++|f (OK (cert!(pc+1))))"
+ using cert_in_A step_in_A semi ok
+ by - (drule merge_def, auto split: split_if_asm)
+ finally
+ have "s' \<le>|r OK s2"
+ using semi step_in_A cert_in_A True step by (auto intro: ub1')
+ also
+ from True pc' have "pc+1 < length is" by simp
+ with semi wtl tkpc cert fits
+ have "OK s2 \<le>|r (OK (phi ! (pc+1)))" by (rule wtl_suc_pc)
+ also note True [symmetric]
+ finally show ?thesis by simp
+ next
+ case False
+ from inst
+ have "\<forall>(pc', s')\<in>set (?step pc). pc'\<noteq>pc+1 \<longrightarrow> s' \<le>|r OK (cert!pc')"
+ by (unfold wtl_inst_def) (rule merge_ok, simp)
+ with step False
+ have ok: "s' \<le>|r (OK (cert!pc'))" by blast
+ moreover
+ from ok
+ have "cert!pc' = None \<longrightarrow> s' = OK None" by auto
+ moreover
+ from c_Some pc'
+ have "cert!pc' \<noteq> None \<longrightarrow> phi!pc' = cert!pc'" by auto
+ ultimately
+ show ?thesis by auto
+ qed
qed
-lemma wtl_fits_wt:
- "\<lbrakk> wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err;
- fits phi is G rT s mxs mxr et cert; pc < length is \<rbrakk> \<Longrightarrow>
- wt_instr (is!pc) G rT phi mxs (length is) et pc"
-proof -
- assume fits: "fits phi is G rT s mxs mxr et cert"
- assume pc: "pc < length is" and
- wtl: "wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err"
- then obtain s' s'' where
- w: "wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s = OK s'" and
- c: "wtl_cert (is!pc) G rT s' cert mxs mxr (length is) et pc = OK s''"
- by - (drule wtl_all, auto)
-
- from fits wtl pc have cert_Some:
- "\<And>t pc. \<lbrakk> pc < length is; cert!pc = Some t \<rbrakk> \<Longrightarrow> phi!pc = Some t"
- by (auto dest: fits_lemma1)
-
- from fits wtl pc have cert_None: "cert!pc = None \<Longrightarrow> phi!pc = s'"
- by - (drule fitsD_None)
-
- from pc c cert_None cert_Some
- have wti: "wtl_inst (is ! pc) G rT (phi!pc) cert mxs mxr (length is) et pc = OK s''"
- by (auto simp add: wtl_cert_def split: split_if_asm option.splits)
-
- -- "we now must show that @{text wt_instr} holds; the definition
- of @{text wt_instr} is: @{thm [display] wt_instr_def[no_vars]}"
-
- { fix pc' r
- assume pc': "(pc',r) \<in> set (eff (is!pc) G pc et (phi!pc))"
+lemma wtl_fits:
+ "wtl_inst_list is cert f r step 0 s0 \<noteq> Err \<Longrightarrow>
+ fits phi cert f r step s0 is \<Longrightarrow>
+ err_semilat (A,r,f) \<Longrightarrow>
+ bounded step (length is) \<Longrightarrow>
+ pres_type step (length is) (err (opt A)) \<Longrightarrow>
+ s0 \<in> opt A \<Longrightarrow>
+ cert_ok cert (length is) A \<Longrightarrow>
+ wt_step (Err.le (Opt.le r)) Err step (map OK phi)"
+ apply (unfold wt_step_def)
+ apply (intro strip)
+ apply (rule conjI, simp)
+ apply (rule wtl_stable)
+ apply assumption+
+ apply (simp add: fits_def)
+ apply assumption
+ done
- with wti have less: "pc' < length is" by (simp add: wtl_inst_OK) blast
-
- have "G \<turnstile> r <=' phi ! pc'"
- proof (cases "pc' = Suc pc")
- case False
- with wti pc'
- have G: "G \<turnstile> r <=' cert ! pc'" by (simp add: wtl_inst_OK) blast
- hence "cert!pc' = None \<Longrightarrow> r = None" by simp
- hence "cert!pc' = None \<Longrightarrow> ?thesis" by simp
- moreover {
- fix t assume "cert!pc' = Some t"
- with less have "phi!pc' = cert!pc'" by (simp add: cert_Some)
- with G have ?thesis by simp
- }
- ultimately show ?thesis by blast
- next
- case True
- with pc' wti
- have "G \<turnstile> r <=' s''" sorry
- also
- from wtl w fits c pc
- have "Suc pc < length is \<Longrightarrow> G \<turnstile> s'' <=' phi ! Suc pc"
- by - (rule wtl_suc_pc)
- with True less
- have "G \<turnstile> s'' <=' phi ! Suc pc" by blast
- finally show ?thesis by (simp add: True)
- qed
- }
- with wti show ?thesis
- by (auto simp add: wtl_inst_OK wt_instr_def)
+
+theorem wtl_sound:
+ assumes "wtl_inst_list is cert f r step 0 s0 \<noteq> Err"
+ assumes "err_semilat (A,r,f)" and "bounded step (length is)"
+ assumes "s0 \<in> opt A" and "cert_ok cert (length is) A"
+ assumes "pres_type step (length is) (err (opt A))"
+ shows "\<exists>ts. wt_step (Err.le (Opt.le r)) Err step ts"
+proof -
+ obtain phi where "fits phi cert f r step s0 is" by (insert exists_phi) fast
+ have "wt_step (Err.le (Opt.le r)) Err step (map OK phi)" by (rule wtl_fits)
+ thus ?thesis ..
qed
-
-lemma fits_first:
- "\<lbrakk> 0 < length is; wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err;
- fits phi is G rT s mxs mxr et cert \<rbrakk> \<Longrightarrow>
- G \<turnstile> s <=' phi ! 0"
-proof -
- assume wtl: "wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err"
- assume fits: "fits phi is G rT s mxs mxr et cert"
- assume pc: "0 < length is"
-
- from wtl
- have wt0: "wtl_inst_list (take 0 is) G rT cert mxs mxr (length is) et 0 s = OK s"
- by simp
-
- with fits pc
- have "cert!0 = None \<Longrightarrow> phi!0 = s"
- by (rule fitsD_None)
- moreover
- from fits pc wt0
- have "\<And>t. cert!0 = Some t \<Longrightarrow> phi!0 = cert!0"
- by - (drule fitsD_Some, auto)
- moreover
- from pc
- obtain x xs where "is = x#xs"
- by (auto simp add: neq_Nil_conv)
- with wtl
- obtain s' where
- "wtl_cert x G rT s cert mxs mxr (length is) et 0 = OK s'"
- by auto
- hence
- "\<And>t. cert!0 = Some t \<Longrightarrow> G \<turnstile> s <=' cert!0"
- by (simp add: wtl_cert_def split: split_if_asm)
-
- ultimately
- show ?thesis
- by (cases "cert!0") auto
-qed
-
-
-lemma wtl_method_correct:
-"wtl_method G C pTs rT mxs mxl et ins cert \<Longrightarrow> \<exists> phi. wt_method G C pTs rT mxs mxl ins et phi"
-proof (unfold wtl_method_def, simp only: Let_def, elim conjE)
- let "?s0" = "Some ([], OK (Class C) # map OK pTs @ replicate mxl Err)"
- assume pc: "0 < length ins"
- assume wtl: "wtl_inst_list ins G rT cert mxs mxl (length ins) et 0 ?s0 \<noteq> Err"
-
- obtain phi where fits: "fits phi ins G rT ?s0 mxs mxl et cert"
- by (rule exists_phi [elim_format]) blast
-
- with wtl
- have allpc:
- "\<forall>pc. pc < length ins \<longrightarrow> wt_instr (ins ! pc) G rT phi mxs (length ins) et pc"
- by (blast intro: wtl_fits_wt)
-
- from pc wtl fits
- have "wt_start G C pTs mxl phi"
- by (unfold wt_start_def) (rule fits_first)
-
- with pc allpc
- show ?thesis by (auto simp add: wt_method_def)
-qed
-
-
-theorem wtl_correct:
- "wtl_jvm_prog G cert \<Longrightarrow> \<exists> Phi. wt_jvm_prog G Phi"
-proof -
- assume wtl: "wtl_jvm_prog G cert"
-
- let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in
- SOME phi. wt_method G C (snd sig) rT maxs maxl ins et phi"
-
- { fix C S fs mdecls sig rT code
- assume "(C,S,fs,mdecls) \<in> set G" "(sig,rT,code) \<in> set mdecls"
- moreover
- from wtl obtain wf_mb where "wf_prog wf_mb G"
- by (auto simp add: wtl_jvm_prog_def)
- ultimately
- have "method (G,C) sig = Some (C,rT,code)"
- by (simp add: methd)
- } note this [simp]
-
- from wtl
- have "wt_jvm_prog G ?Phi"
- apply (clarsimp simp add: wt_jvm_prog_def wtl_jvm_prog_def wf_prog_def wf_cdecl_def)
- apply (drule bspec, assumption)
- apply (clarsimp simp add: wf_mdecl_def)
- apply (drule bspec, assumption)
- apply (clarsimp dest!: wtl_method_correct)
- apply (rule someI, assumption)
- done
-
- thus ?thesis
- by blast
-qed
-
end
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Mon Mar 18 11:47:03 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Wed Mar 20 13:21:07 2002 +0100
@@ -6,154 +6,215 @@
header {* \isaheader{The Lightweight Bytecode Verifier} *}
-theory LBVSpec = Effect + Kildall:
+theory LBVSpec = SemilatAlg + Opt:
+
+
+syntax
+ "@lesuberropt" :: "'a option err \<Rightarrow> 'a ord \<Rightarrow> 'a option err \<Rightarrow> 'a option err ord"
+ ("_ \<le>|_ _" [50,50,51] 50)
-text {*
- The Lightweight Bytecode Verifier with exceptions has not
- made it completely into the Isabelle 2001 release. Currently
- there is only the specification itself available. The proofs of
- soundness and completeness are broken (they still need to be
- ported to the exception version). Both theories are included
- for documentation (but they don't work for this specification),
- please see the Isabelle 99-2 release for a working copy, or
- \url{http://isabelle.in.tum.de/verificard} for the most recent
- development of \mJava.
-*}
+ "@superropt" :: "'a option err \<Rightarrow> 'a ebinop \<Rightarrow> 'a option err \<Rightarrow> 'a option err binop"
+ ("_ +|_ _" [50,50,51] 50)
+
+ "@supsuperropt" :: "'a option err list \<Rightarrow> 'a ebinop \<Rightarrow> 'a option err \<Rightarrow> 'a option err binop"
+ ("_ ++|_ _" [50,50,51] 50)
+
+translations
+ "a \<le>|r b" == "a <=_(Err.le (Opt.le r)) b"
+ "a +|f b" == "a +_(Err.lift2 (Opt.sup f)) b"
+ "a ++|f b" == "a ++_(Err.lift2 (Opt.sup f)) b"
+
types
- certificate = "state_type option list"
- class_certificate = "sig \<Rightarrow> certificate"
- prog_certificate = "cname \<Rightarrow> class_certificate"
+ 's certificate = "'s option list"
+ 's steptype = "'s option err step_type"
consts
- merge :: "[jvm_prog, p_count, nat, nat, p_count, certificate, (nat \<times> (state_type option)) list, state] \<Rightarrow> state"
+merge :: "'s certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow> nat \<Rightarrow>
+ (nat \<times> 's option err) list \<Rightarrow> 's option err \<Rightarrow> 's option err"
primrec
- "merge G pc mxs mxr max_pc cert [] x = x"
- "merge G pc mxs mxr max_pc cert (s#ss) x = (let (pc',s') = s in
- if pc' < max_pc \<and> pc' = pc+1 then
- merge G pc mxs mxr max_pc cert ss (OK s' +_(sup G mxs mxr) x)
- else if pc' < max_pc \<and> G \<turnstile> s' <=' cert!pc' then
- merge G pc mxs mxr max_pc cert ss x
- else Err)"
+"merge cert f r pc [] x = x"
+"merge cert f r pc (s#ss) x = (let (pc',s') = s in
+ merge cert f r pc ss (if pc'=pc+1 then (s' +|f x)
+ else if s' \<le>|r (OK (cert!pc')) then x
+ else Err))"
-constdefs
- wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,nat,nat,p_count,exception_table,p_count]
- \<Rightarrow> state_type option err"
- "wtl_inst i G rT s cert maxs maxr max_pc et pc ==
- if app i G maxs rT pc et s then
- merge G pc maxs maxr max_pc cert (eff i G pc et s) (OK (cert!(pc+1)))
- else Err"
+constdefs
+wtl_inst :: "'s certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow>
+ 's steptype \<Rightarrow> nat \<Rightarrow> 's option \<Rightarrow> 's option err"
+"wtl_inst cert f r step pc s \<equiv> merge cert f r pc (step pc (OK s)) (OK (cert!(pc+1)))"
- wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,nat,nat,p_count,exception_table,p_count]
- \<Rightarrow> state_type option err"
- "wtl_cert i G rT s cert maxs maxr max_pc et pc ==
- case cert!pc of
- None \<Rightarrow> wtl_inst i G rT s cert maxs maxr max_pc et pc
- | Some s' \<Rightarrow> if G \<turnstile> s <=' (Some s') then
- wtl_inst i G rT (Some s') cert maxs maxr max_pc et pc
- else Err"
+wtl_cert :: "'s certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow>
+ 's steptype \<Rightarrow> nat \<Rightarrow> 's option \<Rightarrow> 's option err"
+"wtl_cert cert f r step pc s \<equiv>
+ case cert!pc of
+ None \<Rightarrow> wtl_inst cert f r step pc s
+ | Some s' \<Rightarrow> if OK s \<le>|r (OK (Some s')) then wtl_inst cert f r step pc (Some s') else Err"
consts
- wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,nat,nat,p_count,exception_table,p_count,
- state_type option] \<Rightarrow> state_type option err"
+wtl_inst_list :: "'a list \<Rightarrow> 's certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow>
+ 's steptype \<Rightarrow> nat \<Rightarrow> 's option \<Rightarrow> 's option err"
primrec
- "wtl_inst_list [] G rT cert maxs maxr max_pc et pc s = OK s"
- "wtl_inst_list (i#is) G rT cert maxs maxr max_pc et pc s =
- (let s' = wtl_cert i G rT s cert maxs maxr max_pc et pc in
- strict (wtl_inst_list is G rT cert maxs maxr max_pc et (pc+1)) s')"
-
+"wtl_inst_list [] cert f r step pc s = OK s"
+"wtl_inst_list (i#ins) cert f r step pc s =
+ (let s' = wtl_cert cert f r step pc s in
+ strict (wtl_inst_list ins cert f r step (pc+1)) s')"
+
+
constdefs
- wtl_method :: "[jvm_prog,cname,ty list,ty,nat,nat,exception_table,instr list,certificate] \<Rightarrow> bool"
- "wtl_method G C pTs rT mxs mxl et ins cert ==
- let max_pc = length ins
- in
- 0 < max_pc \<and>
- wtl_inst_list ins G rT cert mxs mxl max_pc et 0
- (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) \<noteq> Err"
+ cert_ok :: "'s certificate \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
+ "cert_ok cert n A \<equiv> \<forall>i < n. cert!i \<in> opt A"
+
+lemma cert_okD:
+ "cert_ok cert n A \<Longrightarrow> pc < n \<Longrightarrow> cert!pc \<in> opt A"
+ by (unfold cert_ok_def) fast
+
+
+declare Let_def [simp]
+
+section "more semilattice lemmas"
+
+(*
+lemma sup_top [simp]:
+ assumes sl: "semilat (A,r,f)"
+ assumes set: "x \<in> A" "t \<in> A"
+ assumes top: "top r t"
+ shows "x +_f t = t"
+proof -
+ from sl have "order r" ..
+ moreover from top have "x +_f t <=_r t" ..
+ moreover from sl set have "t <=_r x +_f t" by simp
+ ultimately show ?thesis by (rule order_antisym)
+qed
+
+lemma plusplussup_top:
+ "semilat (A,r,f) \<Longrightarrow> top r Err \<Longrightarrow> set xs \<subseteq> A \<Longrightarrow> Err \<in> A \<Longrightarrow> xs ++_f Err = Err"
+ by (induct xs) auto
+*)
+
+lemma err_semilatDorderI [simp, intro]:
+ "err_semilat (A,r,f) \<Longrightarrow> order r"
+ apply (simp add: Err.sl_def)
+ apply (rule order_le_err [THEN iffD1])
+ apply (rule semilatDorderI)
+ apply assumption
+ done
+
+lemma err_opt_semilat [simp,elim]:
+ "err_semilat (A,r,f) \<Longrightarrow> semilat (err (opt A), Err.le (Opt.le r), lift2 (Opt.sup f))"
+proof -
+ assume "err_semilat (A,r,f)"
+ hence "err_semilat (Opt.esl (A,r,f))" ..
+ thus ?thesis by (simp add: Err.sl_def Opt.esl_def)
+qed
+
+lemma plusplus_erropt_Err [simp]:
+ "xs ++|f Err = Err"
+ by (induct xs) auto
+
+
+section "merge"
+
+lemma merge_Err [simp]:
+ "merge cert f r pc ss Err = Err"
+ by (induct ss) auto
- wtl_jvm_prog :: "[jvm_prog,prog_certificate] \<Rightarrow> bool"
- "wtl_jvm_prog G cert ==
- wf_prog (\<lambda>G C (sig,rT,maxs,maxl,b,et). wtl_method G C (snd sig) rT maxs maxl et b (cert C sig)) G"
+lemma merge_ok:
+ "\<And>x. merge cert f r pc ss x = OK s \<Longrightarrow>
+ \<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc')))"
+ (is "\<And>x. ?merge ss x \<Longrightarrow> ?P ss")
+proof (induct ss)
+ show "?P []" by simp
+next
+ fix x l ls assume merge: "?merge (l#ls) x"
+ moreover
+ obtain pc' s' where [simp]: "l = (pc',s')" by (cases l)
+ ultimately
+ obtain x' where "?merge ls x'" by simp
+ assume "\<And>x. ?merge ls x \<Longrightarrow> ?P ls" hence "?P ls" .
+ moreover
+ from merge
+ have "pc' \<noteq> pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))" by (simp split: split_if_asm)
+ ultimately
+ show "?P (l#ls)" by simp
+qed
+
+lemma merge_def:
+ assumes semi: "err_semilat (A,r,f)"
+ shows
+ "\<And>x. x \<in> err (opt A) \<Longrightarrow> \<forall>(pc', s') \<in> set ss. s' \<in> err (opt A) \<Longrightarrow>
+ merge cert f r pc ss x =
+ (if \<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))) then
+ map snd [(p',t') \<in> ss. p'=pc+1] ++|f x
+ else Err)"
+ (is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?merge ss x = ?if ss x" is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?P ss x")
+proof (induct ss)
+ fix x show "?P [] x" by simp
+next
+ fix x assume x: "x \<in> err (opt A)"
+ fix l::"nat \<times> 'a option err" and ls
+ assume "\<forall>(pc', s') \<in> set (l#ls). s' \<in> err (opt A)"
+ then obtain l: "snd l \<in> err (opt A)" and ls: "\<forall>(pc', s') \<in> set ls. s' \<in> err (opt A)" by auto
+ assume "\<And>x. x \<in> err (opt A) \<Longrightarrow> \<forall>(pc',s') \<in> set ls. s' \<in> err (opt A) \<Longrightarrow> ?P ls x"
+ hence IH: "\<And>x. x \<in> err (opt A) \<Longrightarrow> ?P ls x" .
+ obtain pc' s' where [simp]: "l = (pc',s')" by (cases l)
+ hence "?merge (l#ls) x = ?merge ls
+ (if pc'=pc+1 then s' +|f x else if s' \<le>|r (OK (cert!pc')) then x else Err)"
+ (is "?merge (l#ls) x = ?merge ls ?if'")
+ by simp
+ also have "\<dots> = ?if ls ?if'"
+ proof -
+ from l have "s' \<in> err (opt A)" by simp
+ with x semi have "(s' +|f x) \<in> err (opt A)" by (fast intro: closedD)
+ with x have "?if' \<in> err (opt A)" by auto
+ hence "?P ls ?if'" by (rule IH) thus ?thesis by simp
+ qed
+ also have "\<dots> = ?if (l#ls) x"
+ proof (cases "\<forall>(pc', s')\<in>set (l#ls). pc' \<noteq> pc + 1 \<longrightarrow> s' \<le>|r OK (cert ! pc')")
+ case True
+ hence "\<forall>(pc', s')\<in>set ls. pc' \<noteq> pc + 1 \<longrightarrow> s' \<le>|r (OK (cert ! pc'))" by auto
+ moreover
+ from True have
+ "map snd [(p',t')\<in>ls . p'=pc+1] ++|f ?if' =
+ (map snd [(p',t')\<in>l#ls . p'=pc+1] ++|f x)"
+ by simp
+ ultimately
+ show ?thesis using True by simp
+ next
+ case False thus ?thesis by auto
+ qed
+ finally show "?P (l#ls) x" .
+qed
+
+lemma merge_ok_s:
+ assumes sl: "err_semilat (A,r,f)"
+ assumes x: "x \<in> err (opt A)"
+ assumes ss: "\<forall>(pc', s') \<in> set ss. s' \<in> err (opt A)"
+ assumes m: "merge cert f r pc ss x = OK s"
+ shows "merge cert f r pc ss x = (map snd [(p',t') \<in> ss. p'=pc+1] ++|f x)"
+proof -
+ from m have "\<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc')))"
+ by (rule merge_ok)
+ with sl x ss m show ?thesis by - (drule merge_def, auto split: split_if_asm)
+qed
+
+section "wtl-inst-list"
lemmas [iff] = not_Err_eq
-lemma if_eq_cases:
- "(P \<Longrightarrow> x = z) \<Longrightarrow> (\<not>P \<Longrightarrow> y = z) \<Longrightarrow> (if P then x else y) = z"
- by simp
-
-lemma merge_def:
- "\<And>x. merge G pc mxs mxr max_pc cert ss x =
- (if \<forall>(pc',s') \<in> set ss. pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> s' <=' cert!pc') then
- map (OK \<circ> snd) [(p',t') \<in> ss. p'=pc+1] ++_(sup G mxs mxr) x
- else Err)" (is "\<And>x. ?merge ss x = ?if ss x" is "\<And>x. ?P ss x")
-proof (induct ss)
- show "\<And>x. ?P [] x" by simp
-next
- have OK_snd: "(\<lambda>u. OK (snd u)) = OK \<circ> snd" by (rule ext) auto
- fix x ss and s::"nat \<times> (state_type option)"
- assume IH: "\<And>x. ?P ss x"
- obtain pc' s' where s: "s = (pc',s')" by (cases s)
- hence "?merge (s#ss) x = ?merge ((pc',s')#ss) x" by hypsubst (rule refl)
- also
- have "\<dots> = (if pc' < max_pc \<and> pc' = pc+1 then
- ?merge ss (OK s' +_(sup G mxs mxr) x)
- else if pc' < max_pc \<and> G \<turnstile> s' <=' cert!pc' then
- ?merge ss x
- else Err)"
- (is "_ = (if ?pc' then ?merge ss (_ +_?f _) else if ?G then _ else _)")
- by simp
- also
- let "if ?all ss then _ else _" = "?if ss x"
- have "\<dots> = ?if ((pc',s')#ss) x"
- proof (cases "?pc'")
- case True
- hence "?all (((pc',s')#ss)) = (pc+1 < max_pc \<and> ?all ss)" by simp
- with True
- have "?if ss (OK s' +_?f x) = ?if ((pc',s')#ss) x" by (auto simp add: OK_snd)
- hence "?merge ss (OK s' +_?f x) = ?if ((pc',s')#ss) x" by (simp only: IH)
- with True show ?thesis by (fast intro: if_eq_cases)
- next
- case False
- have "(if ?G then ?merge ss x else Err) = ?if ((pc',s')#ss) x"
- proof (cases ?G)
- assume G: ?G with False
- have "?if ss x = ?if ((pc',s')#ss) x" by (auto simp add: OK_snd)
- hence "?merge ss x = ?if ((pc',s')#ss) x" by (simp only: IH)
- with G show ?thesis by (fast intro: if_eq_cases)
- next
- assume G: "\<not>?G"
- with False have "Err = ?if ((pc',s')#ss) x" by auto
- with G show ?thesis by (fast intro: if_eq_cases)
- qed
- with False show ?thesis by (fast intro: if_eq_cases)
- qed
- also from s have "\<dots> = ?if (s#ss) x" by hypsubst (rule refl)
- finally show "?P (s#ss) x" .
-qed
-
-
-lemma wtl_inst_OK:
-"(wtl_inst i G rT s cert mxs mxr max_pc et pc = OK s') = (
- app i G mxs rT pc et s \<and>
- (\<forall>(pc',r) \<in> set (eff i G pc et s).
- pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> r <=' cert!pc')) \<and>
- map (OK \<circ> snd) [(p',t') \<in> (eff i G pc et s). p'=pc+1]
- ++_(sup G mxs mxr) (OK (cert!(pc+1))) = OK s')"
- by (auto simp add: wtl_inst_def merge_def split: split_if_asm)
-
lemma wtl_Cons:
- "wtl_inst_list (i#is) G rT cert maxs maxr max_pc et pc s \<noteq> Err =
- (\<exists>s'. wtl_cert i G rT s cert maxs maxr max_pc et pc = OK s' \<and>
- wtl_inst_list is G rT cert maxs maxr max_pc et (pc+1) s' \<noteq> Err)"
+ "wtl_inst_list (i#is) cert f r step pc s \<noteq> Err =
+ (\<exists>s'. wtl_cert cert f r step pc s = OK s' \<and>
+ wtl_inst_list is cert f r step (pc+1) s' \<noteq> Err)"
by (auto simp del: split_paired_Ex)
lemma wtl_append:
-"\<forall> s pc. (wtl_inst_list (a@b) G rT cert mxs mxr mpc et pc s = OK s') =
- (\<exists>s''. wtl_inst_list a G rT cert mxs mxr mpc et pc s = OK s'' \<and>
- wtl_inst_list b G rT cert mxs mxr mpc et (pc+length a) s'' = OK s')"
- (is "\<forall> s pc. ?C s pc a" is "?P a")
+"\<forall>s pc. (wtl_inst_list (a@b) cert f r step pc s = OK s') =
+ (\<exists>s''. wtl_inst_list a cert f r step pc s = OK s'' \<and>
+ wtl_inst_list b cert f r step (pc+length a) s'' = OK s')"
+ (is "\<forall>s pc. ?C s pc a" is "?P a")
proof (induct ?P a)
show "?P []" by simp
next
@@ -162,28 +223,28 @@
proof (intro allI)
fix s pc
show "?C s pc (x#xs)"
- proof (cases "wtl_cert x G rT s cert mxs mxr mpc et pc")
+ proof (cases "wtl_cert cert f r step pc s")
case Err thus ?thesis by simp
next
- fix s0 assume "wtl_cert x G rT s cert mxs mxr mpc et pc = OK s0"
- with IH have "?C s0 (Suc pc) xs" by blast
+ case (OK s0)
+ with IH have "?C s0 (pc+1) xs" by blast
thus ?thesis by (simp!)
qed
qed
qed
lemma wtl_take:
- "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s'' \<Longrightarrow>
- \<exists>s'. wtl_inst_list (take pc' is) G rT cert mxs mxr mpc et pc s = OK s'"
+ "wtl_inst_list is cert f r step pc s = OK s'' \<Longrightarrow>
+ \<exists>s'. wtl_inst_list (take pc' is) cert f r step pc s = OK s'"
+ (is "?wtl is = _ \<Longrightarrow> _")
proof -
- assume "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s''"
- hence "wtl_inst_list (take pc' is @ drop pc' is) G rT cert mxs mxr mpc et pc s = OK s''"
- by simp
+ assume "?wtl is = OK s''"
+ hence "?wtl (take pc' is @ drop pc' is) = OK s''" by simp
thus ?thesis by (auto simp add: wtl_append simp del: append_take_drop_id)
qed
lemma take_Suc:
- "\<forall>n. n < length l \<longrightarrow> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
+ "\<forall>n. n < length l --> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
proof (induct l)
show "?P []" by simp
next
@@ -197,39 +258,137 @@
qed
lemma wtl_Suc:
- "\<lbrakk> wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s';
- wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s'';
- Suc pc < length is \<rbrakk> \<Longrightarrow>
- wtl_inst_list (take (Suc pc) is) G rT cert maxs maxr (length is) et 0 s = OK s''"
+ assumes "wtl_inst_list (take pc is) cert f r step 0 s = OK s'"
+ "wtl_cert cert f r step pc s' = OK s''" and
+ suc: "pc+1 < length is"
+ shows "wtl_inst_list (take (pc+1) is) cert f r step 0 s = OK s''"
proof -
- assume "wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s'"
- "wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s''"
- "Suc pc < length is"
- hence "take (Suc pc) is = (take pc is)@[is!pc]" by (simp add: take_Suc)
+ from suc have "take (pc+1) is=(take pc is)@[is!pc]" by (simp add: take_Suc)
thus ?thesis by (simp! add: wtl_append min_def)
qed
lemma wtl_all:
- "\<lbrakk> wtl_inst_list is G rT cert maxs maxr (length is) et 0 s \<noteq> Err;
- pc < length is \<rbrakk> \<Longrightarrow>
- \<exists>s' s''. wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s' \<and>
- wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s''"
+ assumes
+ all: "wtl_inst_list is cert f r step 0 s \<noteq> Err" (is "?wtl is \<noteq> _") and
+ pc: "pc < length is"
+ shows
+ "\<exists>s' s''. wtl_inst_list (take pc is) cert f r step 0 s = OK s' \<and>
+ wtl_cert cert f r step pc s' = OK s''"
proof -
- assume all: "wtl_inst_list is G rT cert maxs maxr (length is) et 0 s \<noteq> Err"
-
- assume pc: "pc < length is"
- hence "0 < length (drop pc is)" by simp
+ from pc have "0 < length (drop pc is)" by simp
then obtain i r where Cons: "drop pc is = i#r"
by (auto simp add: neq_Nil_conv simp del: length_drop)
hence "i#r = drop pc is" ..
- with all have take:
- "wtl_inst_list (take pc is@i#r) G rT cert maxs maxr (length is) et 0 s \<noteq> Err"
- by simp
-
+ with all have take: "?wtl (take pc is@i#r) \<noteq> Err" by simp
from pc have "is!pc = drop pc is ! 0" by simp
with Cons have "is!pc = i" by simp
with take pc show ?thesis by (auto simp add: wtl_append min_def)
qed
+section "preserves-type"
+
+lemma merge_pres:
+ assumes semi: "err_semilat (A,r,f)"
+ assumes s0_A: "\<forall>(pc', s')\<in>set ss. s' \<in> err (opt A)"
+ assumes x_A: "x \<in> err (opt A)"
+ assumes merge:"merge cert f r pc ss x = OK s'"
+ shows "s' \<in> opt A"
+proof -
+ from s0_A
+ have "set (map snd [(p', t')\<in>ss . p'=pc+1]) \<subseteq> err (opt A)" by auto
+ with semi x_A
+ have "(map snd [(p', t')\<in>ss . p'=pc+1] ++|f x) \<in> err (opt A)"
+ by (auto intro!: plusplus_closed)
+ also {
+ note merge
+ also from semi x_A s0_A
+ have "merge cert f r pc ss x =
+ (if \<forall>(pc', s')\<in>set ss. pc' \<noteq> pc + 1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))
+ then map snd [(p', t')\<in>ss . p'=pc+1] ++|f x else Err)"
+ by (rule merge_def)
+ finally have "(map snd [(p', t')\<in>ss . p'=pc+1] ++|f x) = OK s'"
+ by (simp split: split_if_asm)
+ }
+ finally show ?thesis by simp
+qed
+
+
+
+lemma wtl_inst_pres [intro?]:
+ assumes semi: "err_semilat (A,r,f)"
+ assumes pres: "pres_type step n (err (opt A))"
+ assumes cert: "cert!(pc+1) \<in> opt A"
+ assumes s_A: "s \<in> opt A"
+ assumes pc: "pc < n"
+ assumes wtl: "wtl_inst cert f r step pc s = OK s'"
+ shows "s' \<in> opt A"
+proof -
+ from pres pc s_A
+ have "\<forall>(q, s')\<in>set (step pc (OK s)). s' \<in> err (opt A)"
+ by (unfold pres_type_def) blast
+ moreover
+ from cert have "OK (cert!(pc+1)) \<in> err (opt A)" by simp
+ moreover
+ from wtl
+ have "merge cert f r pc (step pc (OK s)) (OK (cert!(pc+1))) = OK s'"
+ by (unfold wtl_inst_def) simp
+ ultimately
+ show "s' \<in> opt A" using semi by - (rule merge_pres)
+qed
+
+
+lemma wtl_cert_pres:
+ assumes "err_semilat (A,r,f)"
+ assumes "pres_type step n (err (opt A))"
+ assumes "cert!pc \<in> opt A" and "cert!(pc+1) \<in> opt A"
+ assumes "s \<in> opt A" and "pc < n"
+ assumes wtc: "wtl_cert cert f r step pc s = OK s'"
+ shows "s' \<in> opt A"
+proof -
+ have "wtl_inst cert f r step pc s = OK s' \<Longrightarrow> s' \<in> opt A" ..
+ moreover
+ have "wtl_inst cert f r step pc (cert!pc) = OK s' \<Longrightarrow> s' \<in> opt A" ..
+ ultimately
+ show ?thesis using wtc
+ by (unfold wtl_cert_def) (simp split: option.splits split_if_asm)
+qed
+
+lemma wtl_inst_list_pres:
+ assumes semi: "err_semilat (A,r,f)"
+ assumes pres: "pres_type step (length is) (err (opt A))"
+ assumes cert: "cert_ok cert (length is) A"
+ assumes s: "s \<in> opt A"
+ assumes all: "wtl_inst_list is cert f r step 0 s \<noteq> Err"
+ shows "\<And>s'. pc < length is \<Longrightarrow> wtl_inst_list (take pc is) cert f r step 0 s = OK s'
+ \<Longrightarrow> s' \<in> opt A" (is "\<And>s'. ?len pc \<Longrightarrow> ?wtl pc s' \<Longrightarrow> ?A s'")
+proof (induct pc)
+ from s show "\<And>s'. ?wtl 0 s' \<Longrightarrow> ?A s'" by simp
+next
+ fix s' n
+ assume "Suc n < length is"
+ then obtain "n < length is" by simp
+ with all obtain s1 s2 where
+ "wtl_inst_list (take n is) cert f r step 0 s = OK s1"
+ "wtl_cert cert f r step n s1 = OK s2"
+ by - (drule wtl_all, auto)
+
+ assume "?wtl (Suc n) s'"
+ moreover
+ have n1: "n+1 < length is" by simp
+ hence "?wtl (n+1) s2" by - (rule wtl_Suc)
+ ultimately
+ have [simp]: "s2 = s'" by simp
+
+ assume IH: "\<And>s'. n < length is \<Longrightarrow> ?wtl n s' \<Longrightarrow> s' \<in> opt A"
+ hence "s1 \<in> opt A" .
+ moreover
+ from cert have "cert!n \<in> opt A" by (rule cert_okD)
+ moreover
+ from cert n1 have "cert!(n+1) \<in> opt A" by (rule cert_okD)
+ ultimately
+ have "s2 \<in> opt A" using semi pres by - (rule wtl_cert_pres)
+ thus "s' \<in> opt A" by simp
+qed
+
end
--- a/src/HOL/MicroJava/BV/Opt.thy Mon Mar 18 11:47:03 2002 +0100
+++ b/src/HOL/MicroJava/BV/Opt.thy Wed Mar 20 13:21:07 2002 +0100
@@ -101,7 +101,7 @@
done
-lemma semilat_opt:
+lemma semilat_opt [intro, simp]:
"\<And>L. err_semilat L \<Longrightarrow> err_semilat (Opt.esl L)"
proof (unfold Opt.esl_def Err.sl_def, simp add: split_tupled_all)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/SemilatAlg.thy Wed Mar 20 13:21:07 2002 +0100
@@ -0,0 +1,181 @@
+(* Title: HOL/MicroJava/BV/SemilatAlg.thy
+ ID: $Id$
+ Author: Gerwin Klein
+ Copyright 2002 Technische Universitaet Muenchen
+*)
+
+header {* \isaheader{More on Semilattices} *}
+
+theory SemilatAlg = Typing_Framework + Product:
+
+
+syntax "@lesubstep_type" :: "(nat \<times> 's) list \<Rightarrow> 's ord \<Rightarrow> (nat \<times> 's) list \<Rightarrow> bool"
+ ("(_ /<=|_| _)" [50, 0, 51] 50)
+translations
+ "x <=|r| y" == "x <=[(Product.le (op =) r)] y"
+
+consts
+ "@plusplussub" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
+primrec
+ "[] ++_f y = y"
+ "(x#xs) ++_f y = xs ++_f (x +_f y)"
+
+
+constdefs
+ bounded :: "'s step_type \<Rightarrow> nat \<Rightarrow> bool"
+"bounded step n == !p<n. !s. !(q,t):set(step p s). q<n"
+
+ pres_type :: "'s step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
+"pres_type step n A == \<forall>s\<in>A. \<forall>p<n. \<forall>(q,s')\<in>set (step p s). s' \<in> A"
+
+ mono :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
+"mono r step n A ==
+ \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> step p s <=|r| step p t"
+
+
+lemma pres_typeD:
+ "\<lbrakk> pres_type step n A; s\<in>A; p<n; (q,s')\<in>set (step p s) \<rbrakk> \<Longrightarrow> s' \<in> A"
+ by (unfold pres_type_def, blast)
+
+lemma monoD:
+ "\<lbrakk> mono r step n A; p < n; s\<in>A; s <=_r t \<rbrakk> \<Longrightarrow> step p s <=|r| step p t"
+ by (unfold mono_def, blast)
+
+lemma boundedD:
+ "\<lbrakk> bounded step n; p < n; (q,t) : set (step p xs) \<rbrakk> \<Longrightarrow> q < n"
+ by (unfold bounded_def, blast)
+
+
+lemma list_update_le_listI [rule_format]:
+ "set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> xs <=[r] ys \<longrightarrow> p < size xs \<longrightarrow>
+ x <=_r ys!p \<longrightarrow> semilat(A,r,f) \<longrightarrow> x\<in>A \<longrightarrow>
+ xs[p := x +_f xs!p] <=[r] ys"
+ apply (unfold Listn.le_def lesub_def semilat_def)
+ apply (simp add: list_all2_conv_all_nth nth_list_update)
+ done
+
+
+lemma plusplus_closed:
+ "\<And>y. \<lbrakk>semilat (A, r, f); set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> x ++_f y \<in> A"
+proof (induct x)
+ show "\<And>y. y \<in> A \<Longrightarrow> [] ++_f y \<in> A" by simp
+ fix y x xs
+ assume sl: "semilat (A, r, f)" and y: "y \<in> A" and xs: "set (x#xs) \<subseteq> A"
+ assume IH: "\<And>y. \<lbrakk>semilat (A, r, f); set xs \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> xs ++_f y \<in> A"
+ from xs obtain x: "x \<in> A" and "set xs \<subseteq> A" by simp
+ from sl x y have "(x +_f y) \<in> A" by (simp add: closedD)
+ with sl xs have "xs ++_f (x +_f y) \<in> A" by - (rule IH)
+ thus "(x#xs) ++_f y \<in> A" by simp
+qed
+
+lemma ub2: "\<And>y. \<lbrakk>semilat (A, r, f); set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r x ++_f y"
+proof (induct x)
+ show "\<And>y. semilat(A, r, f) \<Longrightarrow> y <=_r [] ++_f y" by simp
+
+ fix y a l
+ assume sl: "semilat (A, r, f)"
+ assume y: "y \<in> A"
+ assume "set (a#l) \<subseteq> A"
+ then obtain a: "a \<in> A" and x: "set l \<subseteq> A" by simp
+ assume "\<And>y. \<lbrakk>semilat (A, r, f); set l \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r l ++_f y"
+ hence IH: "\<And>y. y \<in> A \<Longrightarrow> y <=_r l ++_f y" .
+
+ from sl have "order r" .. note order_trans [OF this, trans]
+
+ from sl a y have "y <=_r a +_f y" by (rule semilat_ub2)
+ also
+ from sl a y have "a +_f y \<in> A" by (simp add: closedD)
+ hence "(a +_f y) <=_r l ++_f (a +_f y)" by (rule IH)
+ finally
+ have "y <=_r l ++_f (a +_f y)" .
+ thus "y <=_r (a#l) ++_f y" by simp
+qed
+
+
+lemma ub1:
+ "\<And>y. \<lbrakk>semilat (A, r, f); set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
+proof (induct ls)
+ show "\<And>y. x \<in> set [] \<Longrightarrow> x <=_r [] ++_f y" by simp
+
+ fix y s ls
+ assume sl: "semilat (A, r, f)"
+ hence "order r" .. note order_trans [OF this, trans]
+ assume "set (s#ls) \<subseteq> A"
+ then obtain s: "s \<in> A" and ls: "set ls \<subseteq> A" by simp
+ assume y: "y \<in> A"
+
+ assume
+ "\<And>y. \<lbrakk>semilat (A, r, f); set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
+ hence IH: "\<And>y. x \<in> set ls \<Longrightarrow> y \<in> A \<Longrightarrow> x <=_r ls ++_f y" .
+
+ assume "x \<in> set (s#ls)"
+ then obtain xls: "x = s \<or> x \<in> set ls" by simp
+ moreover {
+ assume xs: "x = s"
+ from sl s y have "s <=_r s +_f y" by (rule semilat_ub1)
+ also
+ from sl s y have "s +_f y \<in> A" by (simp add: closedD)
+ with sl ls have "(s +_f y) <=_r ls ++_f (s +_f y)" by (rule ub2)
+ finally
+ have "s <=_r ls ++_f (s +_f y)" .
+ with xs have "x <=_r ls ++_f (s +_f y)" by simp
+ }
+ moreover {
+ assume "x \<in> set ls"
+ hence "\<And>y. y \<in> A \<Longrightarrow> x <=_r ls ++_f y" by (rule IH)
+ moreover
+ from sl s y
+ have "s +_f y \<in> A" by (simp add: closedD)
+ ultimately
+ have "x <=_r ls ++_f (s +_f y)" .
+ }
+ ultimately
+ have "x <=_r ls ++_f (s +_f y)" by blast
+ thus "x <=_r (s#ls) ++_f y" by simp
+qed
+
+
+lemma ub1':
+ "\<lbrakk>semilat (A, r, f); \<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk>
+ \<Longrightarrow> b <=_r map snd [(p', t')\<in>S. p' = a] ++_f y"
+proof -
+ let "b <=_r ?map ++_f y" = ?thesis
+
+ assume "semilat (A, r, f)" "y \<in> A"
+ moreover
+ assume "\<forall>(p,s) \<in> set S. s \<in> A"
+ hence "set ?map \<subseteq> A" by auto
+ moreover
+ assume "(a,b) \<in> set S"
+ hence "b \<in> set ?map" by (induct S, auto)
+ ultimately
+ show ?thesis by - (rule ub1)
+qed
+
+
+
+lemma plusplus_empty:
+ "\<forall>s'. (q, s') \<in> set S \<longrightarrow> s' +_f ss ! q = ss ! q \<Longrightarrow>
+ (map snd [(p', t')\<in> S. p' = q] ++_f ss ! q) = ss ! q"
+apply (induct S)
+apply auto
+done
+
+
+lemma lesub_step_type:
+ "\<And>b x y. a <=|r| b \<Longrightarrow> (x,y) \<in> set a \<Longrightarrow> \<exists>y'. (x, y') \<in> set b \<and> y <=_r y'"
+apply (induct a)
+ apply simp
+apply simp
+apply (case_tac b)
+ apply simp
+apply simp
+apply (erule disjE)
+ apply clarify
+ apply (simp add: lesub_def)
+ apply blast
+apply clarify
+apply blast
+done
+
+end
--- a/src/HOL/MicroJava/BV/Typing_Framework.thy Mon Mar 18 11:47:03 2002 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework.thy Wed Mar 20 13:21:07 2002 +0100
@@ -15,9 +15,6 @@
's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
constdefs
- bounded :: "'s step_type \<Rightarrow> nat \<Rightarrow> bool"
-"bounded step n == !p<n. !s. !(q,t):set(step p s). q<n"
-
stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat \<Rightarrow> bool"
"stable r step ss p == !(q,s'):set(step p (ss!p)). s' <=_r ss!q"
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy Mon Mar 18 11:47:03 2002 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy Wed Mar 20 13:21:07 2002 +0100
@@ -7,7 +7,7 @@
header {* \isaheader{Static and Dynamic Welltyping} *}
-theory Typing_Framework_err = Typing_Framework:
+theory Typing_Framework_err = Typing_Framework + SemilatAlg:
constdefs
--- a/src/HOL/MicroJava/ROOT.ML Mon Mar 18 11:47:03 2002 +0100
+++ b/src/HOL/MicroJava/ROOT.ML Wed Mar 20 13:21:07 2002 +0100
@@ -13,9 +13,8 @@
use_thy "JVM";
use_thy "BVSpecTypeSafe";
use_thy "BVExample";
-use_thy "LBVSpec";
+use_thy "LBVCorrect";
(* momentarily broken:
-use_thy "LBVCorrect";
use_thy "LBVComplete";
*)