diff -r 98f52cb93d93 -r ead84e90bfeb src/HOL/MicroJava/BV/JVM.thy
--- a/src/HOL/MicroJava/BV/JVM.thy	Sat Jan 06 21:31:37 2001 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Sun Jan 07 18:43:13 2001 +0100
@@ -7,30 +7,7 @@
 
 header "Kildall for the JVM"
 
-theory JVM = Kildall + JType + Opt + Product + DFA_err + StepMono + BVSpec:
-
-types state = "state_type option err"
-
-constdefs
- stk_esl :: "'c prog => nat => ty list esl"
-"stk_esl S maxs == upto_esl maxs (JType.esl S)"
-
- reg_sl :: "'c prog => nat => ty err list sl"
-"reg_sl S maxr == Listn.sl maxr (Err.sl (JType.esl S))"
-
- sl :: "'c prog => nat => nat => state sl"
-"sl S maxs maxr ==
- Err.sl(Opt.esl(Product.esl (stk_esl S maxs) (Err.esl(reg_sl S maxr))))"
-
- states :: "'c prog => nat => nat => state set"
-"states S maxs maxr == fst(sl S maxs maxr)"
-
- le :: "'c prog => nat => nat => state ord"
-"le S maxs maxr == fst(snd(sl S maxs maxr))"
-
- sup :: "'c prog => nat => nat => state binop"
-"sup S maxs maxr == snd(snd(sl S maxs maxr))"
-
+theory JVM = Kildall + JVMType + Opt + Product + DFA_err + StepMono + BVSpec:
 
 constdefs
   exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> instr list \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> state"
@@ -38,7 +15,7 @@
 
   kiljvm :: "jvm_prog => nat => nat => ty => instr list => state list => state list"
   "kiljvm G maxs maxr rT bs ==
-  kildall (sl G maxs maxr) (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc)"
+  kildall (JVMType.sl G maxs maxr) (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc)"
 
   wt_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool"
   "wt_kil G C pTs rT mxs mxl ins ==
@@ -52,102 +29,6 @@
   "wt_jvm_prog_kildall G ==
   wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b)). wt_kil G C (snd sig) rT maxs maxl b) G"
 
-lemma JVM_states_unfold: 
-  "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) <*>
-                                  list maxr (err(types S))))"
-  apply (unfold states_def JVM.sl_def Opt.esl_def Err.sl_def
-         stk_esl_def reg_sl_def Product.esl_def
-         Listn.sl_def upto_esl_def JType.esl_def Err.esl_def)
-  by simp
-
-
-lemma JVM_le_unfold:
- "le S m n == 
-  Err.le(Opt.le(Product.le(Listn.le(subtype S))(Listn.le(Err.le(subtype S)))))" 
-  apply (unfold JVM.le_def JVM.sl_def Opt.esl_def Err.sl_def
-         stk_esl_def reg_sl_def Product.esl_def  
-         Listn.sl_def upto_esl_def JType.esl_def Err.esl_def) 
-  by simp
-
-
-lemma Err_convert:
-  "Err.le (subtype G) a b = G \<turnstile> a <=o b"
-  by (auto simp add: Err.le_def sup_ty_opt_def lift_top_def lesub_def subtype_def
-           split: err.split)
-
-lemma loc_convert:
-  "Listn.le (Err.le (subtype G)) a b = G \<turnstile> a <=l b"
-  by (unfold Listn.le_def lesub_def sup_loc_def list_all2_def)
-     (simp add: Err_convert)
-
-lemma zip_map [rule_format]:
-  "\<forall>a. length a = length b --> 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 stk_convert:
-  "Listn.le (subtype G) a b = G \<turnstile> map OK a <=l map OK b"
-proof 
-  assume "Listn.le (subtype G) a b"
-
-  hence le: "list_all2 (subtype 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 "subtype G x y"
-      by (simp add: list_all2_def Ball_def)
-    with OK
-    have "G \<turnstile> x' <=o y'"
-      by (simp add: subtype_def)
-  }
-  
-  with le
-  show "G \<turnstile> map OK a <=l map OK b"
-    by (auto simp add: sup_loc_def list_all2_def)
-next
-  assume "G \<turnstile> map OK a <=l map OK b"
-
-  thus "Listn.le (subtype G) a b"
-    apply (unfold sup_loc_def list_all2_def Listn.le_def lesub_def)
-    apply (clarsimp simp add: zip_map subtype_def)
-    apply (drule bspec, assumption)
-    apply auto
-    done
-qed
-
-
-lemma state_conv:
-  "Product.le (Listn.le (subtype G)) (Listn.le (Err.le (subtype G))) a b = G \<turnstile> a <=s b"
-  by (unfold Product.le_def lesub_def sup_state_def)
-     (simp add: split_beta stk_convert loc_convert)
-
-lemma state_opt_conv:
-  "Opt.le (Product.le (Listn.le (subtype G)) (Listn.le (Err.le (subtype G)))) a b = G \<turnstile> a <=' b"
-  by (unfold Opt.le_def lesub_def sup_state_opt_def lift_bottom_def)
-     (auto simp add: state_conv split: option.split)
-
-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 state_opt_conv)
-
-lemma JVM_le_Err_conv:
-  "le G m n = Err.le (sup_state_opt G)"
-  apply (simp add: expand_fun_eq)
-  apply (unfold Err.le_def JVM_le_unfold lesub_def)
-  apply (clarsimp split: err.splits)
-  apply (simp add: state_opt_conv)
-  done
 
 lemma special_ex_swap_lemma [iff]: 
   "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"
@@ -208,7 +89,7 @@
 
 theorem exec_mono:
   "wf_prog wf_mb G ==>
-  mono (JVM.le G maxs maxr) (exec G maxs rT bs) (size bs) (states G maxs maxr)"
+  mono (JVMType.le G maxs maxr) (exec G maxs rT bs) (size bs) (states G maxs maxr)"
   apply (unfold mono_def)
   apply clarify
   apply (unfold lesub_def)
@@ -227,8 +108,8 @@
   done
 
 theorem semilat_JVM_slI:
-  "[| wf_prog wf_mb G |] ==> semilat(sl G maxs maxr)"
-  apply (unfold JVM.sl_def stk_esl_def reg_sl_def)
+  "[| wf_prog wf_mb G |] ==> semilat (JVMType.sl G maxs maxr)"
+  apply (unfold JVMType.sl_def stk_esl_def reg_sl_def)
   apply (rule semilat_opt)
   apply (rule err_semilat_Product_esl)
   apply (rule err_semilat_upto_esl)
@@ -239,16 +120,14 @@
   done
 
 lemma sl_triple_conv:
-  "sl G maxs maxr == 
-  (states G maxs maxr, le G maxs maxr, sup G maxs maxr)"
-  by (simp (no_asm) add: states_def JVM.le_def JVM.sup_def)
+  "JVMType.sl G maxs maxr == 
+  (states G maxs maxr, JVMType.le G maxs maxr, JVMType.sup G maxs maxr)"
+  by (simp (no_asm) add: states_def JVMType.le_def JVMType.sup_def)
 
 
-ML_setup {* bind_thm ("wf_subcls1", wf_subcls1); *}
-
 theorem is_bcv_kiljvm:
   "[| wf_prog wf_mb G; bounded (\<lambda>pc. succs (bs!pc) pc) (size bs) |] ==> 
-      is_bcv (JVM.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc)
+      is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc)
              (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT bs)"
   apply (unfold kiljvm_def sl_triple_conv)
   apply (rule is_bcv_kildall)
@@ -295,7 +174,7 @@
 
   from wf bounded
   have bcv:
-    "is_bcv (le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc)
+    "is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc)
             (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT bs)"
     by (rule is_bcv_kiljvm)
 
@@ -328,14 +207,14 @@
   with bcv success result 
   have 
     "\<exists>ts\<in>list (length bs) (states G maxs maxr).
-         ?start <=[le G maxs maxr] ts \<and>
-         welltyping (JVM.le G maxs maxr) Err (JVM.exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) ts"
+         ?start <=[JVMType.le G maxs maxr] ts \<and>
+         welltyping (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) ts"
     by (unfold is_bcv_def) auto
 
   then obtain phi' where
     l: "phi' \<in> list (length bs) (states G maxs maxr)" and
-    s: "?start <=[le G maxs maxr] phi'" and
-    w: "welltyping (le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) phi'"
+    s: "?start <=[JVMType.le G maxs maxr] phi'" and
+    w: "welltyping (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) phi'"
     by blast
    
   hence dynamic:
@@ -343,7 +222,7 @@
     by (simp add: dynamic_wt_def exec_def JVM_le_Err_conv)
 
   from s
-  have le: "le G maxs maxr (?start ! 0) (phi'!0)"    
+  have le: "JVMType.le G maxs maxr (?start ! 0) (phi'!0)"    
     by (drule_tac p=0 in le_listD) (simp add: lesub_def)+
 
   from l
@@ -356,7 +235,7 @@
 
   with instrs l
   have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0"
-    by clarsimp
+    by (clarsimp simp add: not_Err_eq)
 
   from l bounded
   have "bounded (\<lambda>pc. succs (bs ! pc) pc) (length phi')"
@@ -434,7 +313,7 @@
 
   from wf bounded
   have is_bcv: 
-    "is_bcv (JVM.le G maxs ?maxr) Err (exec G maxs rT bs) ?succs 
+    "is_bcv (JVMType.le G maxs ?maxr) Err (exec G maxs rT bs) ?succs 
             (size bs) (states G maxs ?maxr) (kiljvm G maxs ?maxr rT bs)"
     by (rule is_bcv_kiljvm)