# HG changeset patch
# User kleing
# Date 1016993811 -3600
# Node ID a59af3a83c613f5a535988b8a6b535ca37054776
# Parent  b57d926d1de26320ea0e73e8fec7084cc8cd5283
tuned

diff -r b57d926d1de2 -r a59af3a83c61 src/HOL/MicroJava/BV/JVM.thy
--- a/src/HOL/MicroJava/BV/JVM.thy	Sun Mar 24 14:06:21 2002 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Sun Mar 24 19:16:51 2002 +0100
@@ -102,13 +102,6 @@
 
 lemmas [iff del] = not_None_eq
 
-lemma non_empty_succs: "succs i pc \<noteq> []"
-  by (cases i) auto
-
-lemma non_empty:
-  "non_empty (\<lambda>pc. eff (bs!pc) G pc et)" 
-  by (simp add: non_empty_def eff_def non_empty_succs)
-
 theorem exec_pres_type:
   "wf_prog wf_mb S \<Longrightarrow> 
   pres_type (exec S maxs rT et bs) (size bs) (states S maxs maxr)"
@@ -391,12 +384,14 @@
     by (clarsimp simp add: not_Err_eq)
 
   from l bounded 
-  have bounded': "bounded (\<lambda>pc. eff (bs!pc) G pc et) (length phi')"
+  have "bounded (\<lambda>pc. eff (bs!pc) G pc et) (length phi')"
     by (simp add: exec_def check_bounded_is_bounded)  
+  hence bounded': "bounded (exec G maxs rT et bs) (length bs)"
+    by (auto intro: bounded_lift simp add: exec_def l)
   with wt_err_step
   have "wt_app_eff (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT pc et) 
                    (\<lambda>pc. eff (bs!pc) G pc et) (map ok_val phi')"
-    by (auto intro: wt_err_imp_wt_app_eff simp add: l exec_def non_empty)
+    by (auto intro: wt_err_imp_wt_app_eff simp add: l exec_def)
   with instrs l le bounded'
   have "wt_method G C pTs rT maxs mxl bs et (map ok_val phi')"
     apply (unfold wt_method_def wt_app_eff_def)
@@ -409,8 +404,9 @@
     apply (erule allE, erule impE, assumption)
     apply (elim conjE)
     apply (clarsimp simp add: lesub_def wt_instr_def)
-    apply (unfold bounded_def)
-    apply blast    
+    apply (simp add: exec_def)
+    apply (drule bounded_err_stepD, assumption+)
+    apply blast
     done
 
   thus ?thesis by blast
diff -r b57d926d1de2 -r a59af3a83c61 src/HOL/MicroJava/BV/Kildall_Lift.thy
--- a/src/HOL/MicroJava/BV/Kildall_Lift.thy	Sun Mar 24 14:06:21 2002 +0100
+++ b/src/HOL/MicroJava/BV/Kildall_Lift.thy	Sun Mar 24 19:16:51 2002 +0100
@@ -11,12 +11,6 @@
 "app_mono r app n A ==
  \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> app p t \<longrightarrow> app p s"
 
-
-lemma in_map_sndD: "(a,b) \<in> set (map_snd f xs) \<Longrightarrow> \<exists>b'. (a,b') \<in> set xs"
-  apply (induct xs)
-  apply (auto simp add: map_snd_def)
-  done
-
 lemma bounded_lift:
   "bounded step n \<Longrightarrow> bounded (err_step n app step) n"
   apply (unfold bounded_def err_step_def error_def)
@@ -26,18 +20,6 @@
   apply (auto simp add: map_snd_def split: split_if_asm)
   done
 
-lemma boundedD2:
-  "bounded (err_step n app step) n \<Longrightarrow> 
-  p < n \<Longrightarrow>  app p a \<Longrightarrow> (q,b) \<in> set (step p a) \<Longrightarrow> 
-  q < n"
-  apply (simp add: bounded_def err_step_def)
-  apply (erule allE, erule impE, assumption)
-  apply (erule_tac x = "OK a" in allE, drule bspec)
-   apply (simp add: map_snd_def)
-   apply fast
-  apply simp
-  done
-
 lemma le_list_map_OK [simp]:
   "\<And>b. map OK a <=[Err.le r] map OK b = (a <=[r] b)"
   apply (induct a)
@@ -73,7 +55,7 @@
  apply clarify
  apply (drule in_map_sndD)
  apply clarify
- apply (drule boundedD2, assumption+)
+ apply (drule bounded_err_stepD, assumption+)
  apply (rule exI [of _ Err])
  apply simp
 apply simp
@@ -94,7 +76,7 @@
 apply clarify
 apply (drule in_map_sndD)
 apply clarify
-apply (drule boundedD2, assumption+)
+apply (drule bounded_err_stepD, assumption+)
 apply (rule exI [of _ Err])
 apply simp
 done
diff -r b57d926d1de2 -r a59af3a83c61 src/HOL/MicroJava/BV/Typing_Framework_err.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Sun Mar 24 14:06:21 2002 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Sun Mar 24 19:16:51 2002 +0100
@@ -18,70 +18,93 @@
 "wt_app_eff r app step ts \<equiv>
   \<forall>p < size ts. app p (ts!p) \<and> (\<forall>(q,t) \<in> set (step p (ts!p)). t <=_r ts!q)"
 
+
 map_snd :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'c) list"
 "map_snd f \<equiv> map (\<lambda>(x,y). (x, f y))"
 
 error :: "nat \<Rightarrow> (nat \<times> 'a err) list"
 "error n \<equiv> map (\<lambda>x. (x,Err)) [0..n(]"
 
+
 err_step :: "nat \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's err step_type"
 "err_step n app step p t \<equiv> 
   case t of 
     Err   \<Rightarrow> error n
   | OK t' \<Rightarrow> if app p t' then map_snd OK (step p t') else error n"
 
-non_empty :: "'s step_type \<Rightarrow> bool"
-"non_empty step \<equiv> \<forall>p t. step p t \<noteq> []"
-
-
 lemmas err_step_defs = err_step_def map_snd_def error_def
 
-lemma non_emptyD:
-  "non_empty step \<Longrightarrow> \<exists>q t'. (q,t') \<in> set(step p t)"
-proof (unfold non_empty_def)
-  assume "\<forall>p t. step p t \<noteq> []"
-  hence "step p t \<noteq> []" by blast
-  then obtain x xs where "step p t = x#xs"
-    by (auto simp add: neq_Nil_conv)
-  hence "x \<in> set(step p t)" by simp
-  thus ?thesis by (cases x) blast
-qed
+lemma bounded_err_stepD:
+  "bounded (err_step n app step) n \<Longrightarrow> 
+  p < n \<Longrightarrow>  app p a \<Longrightarrow> (q,b) \<in> set (step p a) \<Longrightarrow> 
+  q < n"
+  apply (simp add: bounded_def err_step_def)
+  apply (erule allE, erule impE, assumption)
+  apply (erule_tac x = "OK a" in allE, drule bspec)
+   apply (simp add: map_snd_def)
+   apply fast
+  apply simp
+  done
+
+
+lemma in_map_sndD: "(a,b) \<in> set (map_snd f xs) \<Longrightarrow> \<exists>b'. (a,b') \<in> set xs"
+  apply (induct xs)
+  apply (auto simp add: map_snd_def)
+  done
 
 
+lemma bounded_err_stepI:
+  "\<forall>p. p < n \<longrightarrow> (\<forall>s. ap p s \<longrightarrow> (\<forall>(q,s') \<in> set (step p s). q < n))
+  \<Longrightarrow> bounded (err_step n ap step) n"
+apply (unfold bounded_def)
+apply clarify
+apply (simp add: err_step_def split: err.splits)
+apply (simp add: error_def)
+ apply blast
+apply (simp split: split_if_asm) 
+ apply (blast dest: in_map_sndD)
+apply (simp add: error_def)
+apply blast
+done
+
+
+text {*
+  There used to be a condition here that each instruction must have a
+  successor. This is not needed any more, because the definition of
+  @{term error} trivially ensures that there is a successor for
+  the critical case where @{term app} does not hold. 
+*}
 lemma wt_err_imp_wt_app_eff:
-  assumes b:  "bounded step (size ts)"
-  assumes n:  "non_empty step"
   assumes wt: "wt_err_step r (err_step (size ts) app step) ts"
+  assumes b:  "bounded (err_step (size ts) app step) (size ts)"
   shows "wt_app_eff r app step (map ok_val ts)"
 proof (unfold wt_app_eff_def, intro strip, rule conjI)
   fix p assume "p < size (map ok_val ts)"
   hence lp: "p < size ts" by simp
+  hence ts: "0 < size ts" by (cases p) auto
+  hence err: "(0,Err) \<in> set (error (size ts))" by (simp add: error_def)
 
   from wt lp
   have [intro?]: "\<And>p. p < size ts \<Longrightarrow> ts ! p \<noteq> Err" 
     by (unfold wt_err_step_def wt_step_def) simp
 
   show app: "app p (map ok_val ts ! p)"
-  proof -
-    from wt lp 
-    obtain s where
+  proof (rule ccontr)
+    from wt lp obtain s where
       OKp:  "ts ! p = OK s" and
       less: "\<forall>(q,t) \<in> set (err_step (size ts) app step p (ts!p)). t <=_(Err.le r) ts!q"
       by (unfold wt_err_step_def wt_step_def stable_def) 
          (auto iff: not_Err_eq)
-    
-    from n obtain q t where q: "(q,t) \<in> set(step p s)"
-      by (blast dest: non_emptyD) 
-    
-    from lp b q
-    have lq: "q < size ts" by (unfold bounded_def) blast
-    hence "ts!q \<noteq> Err" ..
-    then obtain s' where OKq: "ts ! q = OK s'" by (auto iff: not_Err_eq)      
-
-    with OKp less q lp have "app p s"
-      by (auto simp add: err_step_defs split: err.split_asm split_if_asm)      
-
-    with lp OKp show ?thesis by simp
+    assume "\<not> app p (map ok_val ts ! p)"
+    with OKp lp have "\<not> app p s" by simp
+    with OKp have "err_step (size ts) app step p (ts!p) = error (size ts)" 
+      by (simp add: err_step_def)    
+    with err ts obtain q where 
+      "(q,Err) \<in> set (err_step (size ts) app step p (ts!p))" and
+      q: "q < size ts" by auto    
+    with less have "ts!q = Err" by auto
+    moreover from q have "ts!q \<noteq> Err" ..
+    ultimately show False by blast
   qed
   
   show "\<forall>(q,t)\<in>set(step p (map ok_val ts ! p)). t <=_r map ok_val ts ! q" 
@@ -95,8 +118,7 @@
       by (unfold wt_err_step_def wt_step_def stable_def) 
          (auto iff: not_Err_eq)
 
-    from lp b q
-    have lq: "q < size ts" by (unfold bounded_def) blast
+    from b lp app q have lq: "q < size ts" by (rule bounded_err_stepD)
     hence "ts!q \<noteq> Err" ..
     then obtain s' where OKq: "ts ! q = OK s'" by (auto iff: not_Err_eq)
 
diff -r b57d926d1de2 -r a59af3a83c61 src/HOL/MicroJava/document/root.bib
--- a/src/HOL/MicroJava/document/root.bib	Sun Mar 24 14:06:21 2002 +0100
+++ b/src/HOL/MicroJava/document/root.bib	Sun Mar 24 19:16:51 2002 +0100
@@ -66,3 +66,28 @@
         note = {ECOOP2000 Workshop proceedings available from \url{http://www.informatik.fernuni-hagen.de/pi5/publications.html}},
         url       = {\url{http://www4.in.tum.de/~nipkow/pubs/lbv.html}}
 }
+
+
+@article{KleinN-CPE01,
+        author = "Gerwin Klein and Tobias Nipow",
+        title = "Verified Lightweight Bytecode Verification",
+        journal = "Concurrency and Computation: Practice and Experience",
+        year = "2001",
+        volume = "13",
+        number = "13",
+        editor = "Gary T. Leavens and Susan Eisenbach",
+        pages = "1133-1151",
+        url = {http://www4.informatik.tu-muenchen.de/~kleing/papers/cpe01.html},
+        abstract = {Eva and Kristoffer Rose proposed a (sparse) annotation of Java Virtual
+Machine code with types to enable a one-pass verification of welltypedness.
+We have formalized a variant of their proposal in the theorem prover
+Isabelle/HOL and proved soundness and completeness.},
+        note = {Invited contribution to special issue on Formal Techniques for Java},
+}
+
+
+@inproceedings{Nipkow-FOSSACS01,author={Tobias Nipkow},
+title={Verified Bytecode Verifiers},booktitle=
+{Foundations of Software Science and Computation Structures (FOSSACS 2001)},
+editor={F. Honsell},publisher=Springer,series=LNCS,volume=2030,
+pages={347--363},year=2001}