src/HOL/MicroJava/BV/LBVSpec.thy

 (*  Title:      HOL/MicroJava/BV/BVLightSpec.thy
     ID:         $Id$
     Author:     Gerwin Klein
     Copyright   1999 Technische Universitaet Muenchen
-
-Specification of a lightweight bytecode verifier
 *)
+
+header {* Specification of the LBV *}
+
 
 theory LBVSpec = BVSpec:;
 
 types
   certificate       = "state_type option list" 

 
 consts
  wtl_CH	:: "[check_object,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool"; 
 primrec
 "wtl_CH (Checkcast C) G s s' max_pc pc = 
-	(let (ST,LT) = s
+	(let (ST,LT) = s 
 	 in
 	 pc+1 < max_pc \\<and>
 	 is_class G C \\<and> 
 	 (\\<exists>rt ST'. ST = RefT rt # ST' \\<and>
                    (Class C # ST' , LT) = s'))";

  wtl_jvm_prog :: "[jvm_prog,prog_certificate] \\<Rightarrow> bool"
  "wtl_jvm_prog G cert \\<equiv> 
     wf_prog (\\<lambda>G C (sig,rT,maxl,b). 
                wtl_method G C (snd sig) rT maxl b (cert C sig)) G"; 
 
+text {* \medskip *}
+
 lemma rev_eq: "\\<lbrakk>length a = n; length x = n; rev a @ b # c = rev x @ y # z\\<rbrakk> \\<Longrightarrow> a = x \\<and> b = y \\<and> c = z";
-proof auto;
-qed;
+by auto;
 
 lemma wtl_inst_unique: 
 "wtl_inst i G rT s0 s1 cert max_pc pc \\<longrightarrow>
  wtl_inst i G rT s0 s1' cert max_pc pc \\<longrightarrow> s1 = s1'" (is "?P i");
 proof (induct i);

  case Invoke;
   have "\\<exists>x y. s0 = (x,y)"; by (simp);
   thus "wtl_inst (MI (Invoke mname list)) G rT s0 s1 cert max_pc pc \\<longrightarrow>
         wtl_inst (MI (Invoke mname list)) G rT s0 s1' cert max_pc pc \\<longrightarrow>
         s1 = s1'";
-  proof (elim);
+  proof elim;
     apply_end(clarsimp_tac, drule rev_eq, assumption+);
   qed auto;
  qed;
 case MR;
  show "?P (MR meth_ret)"; by (induct meth_ret) auto;

   case Nil;
   show "?P []"; by simp;
 
   case Cons;
   show "?P (a # list)"; 
-  proof (intro);
+  proof intro;
     fix s0; fix pc; 
     let "?o s0 s1" = "wtl_inst_option a G rT s0 s1 cert max_pc pc";
     let "?l l s1 s2 pc" = "wtl_inst_list l G rT s1 s2 cert max_pc pc"; 
     assume a: "?l (a#list) s0 s1 pc";
     assume b: "?l (a#list) s0 s1' pc";