# HG changeset patch
# User streckem
# Date 1035382202 -7200
# Node ID 2950128b820698a3b92ad51acfac5f4b06b856a4
# Parent  b95d12325b510c6458d7cb12cb4dab14af0bf89e
First checkin of compiler

diff -r b95d12325b51 -r 2950128b8206 src/HOL/MicroJava/Comp/AuxLemmas.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy	Wed Oct 23 16:10:02 2002 +0200
@@ -0,0 +1,166 @@
+(*  Title:      HOL/MicroJava/Comp/AuxLemmas.thy
+    ID:         $Id$
+    Author:     Martin Strecker
+    Copyright   GPL 2002
+*)
+
+
+(* Auxiliary Lemmas *)
+
+theory AuxLemmas = JBasis:
+
+(**********************************************************************)
+(* List.thy *)
+(**********************************************************************)
+
+
+
+lemma foldr_foldl: "foldr f xs a = foldl (\<lambda> x y. (f y x)) a (rev xs)"
+by (induct xs, simp, simp)
+
+lemma foldl_foldr: "foldl f a xs = foldr (\<lambda> x y. (f y x)) (rev xs) a"
+by (simp add: foldr_foldl [of "(\<lambda> x y. (f y x))" "(rev xs)"])
+
+lemma foldr_append: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
+by (induct xs, auto)
+
+lemma app_nth_len [simp]: "(pre @ a # post) ! length pre = a"
+by (induct "pre") auto
+
+lemma app_nth_len_plus [simp]: "(pre @ post) ! ((length pre) + n) = post ! n"
+by (induct "pre") auto
+
+lemma app_nth_greater_len [rule_format (no_asm), simp]:
+ "\<forall> ind. length pre \<le> ind \<longrightarrow> (pre @ a # post) ! (Suc ind) = (pre @ post) ! ind"
+apply (induct "pre")
+apply auto
+apply (case_tac ind)
+apply auto
+done
+
+lemma list_update_length [simp]: "(xs @ a# ys)[length xs := b] = (xs @ b# ys)"
+by (induct xs, auto)
+
+
+lemma length_takeWhile: "v \<in> set xs \<Longrightarrow> length (takeWhile (%z. z~=v) xs) < length xs"
+by (induct xs, auto)
+
+lemma nth_length_takeWhile [simp]: 
+  "v \<in> set xs \<Longrightarrow> xs ! (length (takeWhile (%z. z~=v) xs)) = v"
+by (induct xs, auto)
+
+
+lemma map_fun_upd [simp]: "y \<notin> set xs \<Longrightarrow> map (f(y:=v)) xs = map f xs"
+by (induct xs, auto)
+
+lemma map_list_update [simp]:
+  "\<lbrakk> x \<in> set xs; distinct xs\<rbrakk> \<Longrightarrow> 
+  (map f xs) [length (takeWhile (\<lambda>z. z \<noteq> x) xs) := v] = 
+  map (f(x:=v)) xs"
+apply (induct xs)
+apply simp
+apply (case_tac "x=a")
+apply auto
+done
+
+
+(**********************************************************************)
+(* Product_Type.thy *)
+(**********************************************************************)
+
+
+lemma split_compose: "(split f) \<circ> (\<lambda> (a,b). ((fa a), (fb b))) =
+  (\<lambda> (a,b). (f (fa a) (fb b)))"
+by (simp add: split_def o_def)
+
+lemma split_iter: "(\<lambda> (a,b,c). ((g1 a), (g2 b), (g3 c))) = 
+        (\<lambda> (a,p). ((g1 a), (\<lambda> (b, c). ((g2 b), (g3 c))) p))"
+by (simp add: split_def o_def)
+
+
+(**********************************************************************)
+(* Set.thy *)
+(**********************************************************************)
+
+lemma singleton_in_set: "A = {a} \<Longrightarrow> a \<in> A" by simp
+
+(**********************************************************************)
+(* Map.thy *)
+(**********************************************************************)
+
+lemma the_map_upd: "(the \<circ> f(x\<mapsto>v)) = (the \<circ> f)(x:=v)"
+by (simp add: expand_fun_eq)
+
+lemma map_of_in_set: 
+  "(map_of xs x = None) = (x \<notin> set (map fst xs))"
+by (induct xs, auto)
+
+lemma map_map_upd [simp]: 
+  "y \<notin> set xs \<Longrightarrow> map (the \<circ> f(y\<mapsto>v)) xs = map (the \<circ> f) xs"
+by (simp add: the_map_upd)
+
+lemma map_map_upds [rule_format (no_asm), simp]: 
+"\<forall> f vs. (\<forall>y\<in>set ys. y \<notin> set xs) \<longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) xs = map (the \<circ> f) xs"
+apply (induct ys)
+apply simp
+apply (intro strip)
+apply (simp only: map_upds.simps)
+apply (subgoal_tac "\<forall>y\<in>set list. y \<notin> set xs")
+apply (subgoal_tac "a\<notin> set xs")
+apply (subgoal_tac "map (the \<circ> f(a\<mapsto>hd vs)(list[\<mapsto>]tl vs)) xs = map (the \<circ> f(a\<mapsto>hd vs)) xs")
+apply (simp only:)
+apply (erule map_map_upd)
+apply blast
+apply simp+
+done
+
+lemma map_upds_distinct [rule_format (no_asm), simp]: 
+  "\<forall> f vs. length ys = length vs \<longrightarrow> distinct ys \<longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) ys = vs"
+apply (induct ys)
+apply simp
+apply (intro strip)
+apply (case_tac vs)
+apply simp
+apply (simp only: map_upds.simps distinct.simps hd.simps tl.simps)
+apply clarify
+apply (simp only: map.simps map_map_upd)
+apply simp
+apply (simp add: o_def)
+done
+
+
+lemma map_of_map_as_map_upd [rule_format (no_asm)]: "distinct (map f zs) \<longrightarrow> 
+map_of (map (\<lambda> p. (f p, g p)) zs) = empty (map f zs [\<mapsto>] map g zs)"
+by (induct zs, auto)
+
+(* In analogy to Map.map_of_SomeD *)
+lemma map_upds_SomeD [rule_format (no_asm)]: 
+  "\<forall> m ys. (m(xs[\<mapsto>]ys)) k = Some y \<longrightarrow> k \<in> (set xs) \<or> (m k = Some y)"
+apply (induct xs)
+apply simp
+apply (case_tac "k = a")
+apply auto
+done
+
+lemma map_of_upds_SomeD: "(map_of m (xs[\<mapsto>]ys)) k = Some y 
+  \<Longrightarrow> k \<in> (set (xs @ map fst m))"
+by (auto dest: map_upds_SomeD map_of_SomeD fst_in_set_lemma)
+
+
+lemma map_of_map_prop [rule_format (no_asm)]: 
+  "(map_of (map f xs) k = Some v) \<longrightarrow> 
+  (\<forall> x \<in> set xs. (P1 x)) \<longrightarrow> 
+  (\<forall> x. (P1 x) \<longrightarrow> (P2 (f x))) \<longrightarrow>
+  (P2(k, v))"
+by (induct xs,auto)
+
+lemma map_of_map2: "\<forall> x \<in> set xs. (fst (f x)) = (fst x) \<Longrightarrow>
+  map_of (map f xs) a = option_map (\<lambda> b. (snd (f (a, b)))) (map_of xs a)"
+by (induct xs, auto)
+
+lemma option_map_of [simp]: "(option_map f (map_of xs k) = None) = ((map_of xs k) = None)"
+by (simp add: option_map_def split: option.split)
+
+
+
+end
diff -r b95d12325b51 -r 2950128b8206 src/HOL/MicroJava/Comp/CorrComp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Wed Oct 23 16:10:02 2002 +0200
@@ -0,0 +1,1309 @@
+(*  Title:      HOL/MicroJava/Comp/CorrComp.thy
+    ID:         $Id$
+    Author:     Martin Strecker
+    Copyright   GPL 2002
+*)
+
+(* Compiler correctness statement and proof *)
+
+theory CorrComp =  JTypeSafe + LemmasComp:
+
+
+
+(* If no exception is present after evaluation/execution, 
+  none can have been present before *)
+lemma eval_evals_exec_xcpt:
+ "((xs,ex,val,xs') \<in> Eval.eval G \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and>
+  ((xs,exs,vals,xs') \<in> Eval.evals G \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and>
+  ((xs,st,xs') \<in> Eval.exec G \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None)"
+by (induct rule: eval_evals_exec.induct, auto)
+
+
+(* instance of eval_evals_exec_xcpt for eval *)
+lemma eval_xcpt: "(xs,ex,val,xs') \<in> Eval.eval G \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
+ (is "?H1 \<Longrightarrow> ?H2 \<Longrightarrow> ?T")
+proof-
+  assume h1: ?H1
+  assume h2: ?H2
+  from h1 h2 eval_evals_exec_xcpt show "?T" by simp
+qed
+
+(* instance of eval_evals_exec_xcpt for evals *)
+lemma evals_xcpt: "(xs,exs,vals,xs') \<in> Eval.evals G \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
+ (is "?H1 \<Longrightarrow> ?H2 \<Longrightarrow> ?T")
+proof-
+  assume h1: ?H1
+  assume h2: ?H2
+  from h1 h2 eval_evals_exec_xcpt show "?T" by simp
+qed
+
+(* instance of eval_evals_exec_xcpt for exec *)
+lemma exec_xcpt: "(xs,st,xs') \<in> Eval.exec G \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
+ (is "?H1 \<Longrightarrow> ?H2 \<Longrightarrow> ?T")
+proof-
+  assume h1: ?H1
+  assume h2: ?H2
+  from h1 h2 eval_evals_exec_xcpt show "?T" by simp
+qed
+
+(**********************************************************************)
+
+theorem exec_all_trans: "\<lbrakk>(exec_all G s0 s1); (exec_all G s1 s2)\<rbrakk> \<Longrightarrow> (exec_all G s0 s2)"
+apply (auto simp: exec_all_def elim: Transitive_Closure.rtrancl_trans)
+done
+
+theorem exec_all_refl: "exec_all G s s"
+by (simp only: exec_all_def, rule rtrancl_refl)
+
+
+theorem exec_instr_in_exec_all:
+  "\<lbrakk> exec_instr i G hp stk lvars C S pc frs =  (None, hp', frs');
+             gis (gmb G C S) ! pc = i\<rbrakk>  \<Longrightarrow>
+       G \<turnstile> (None, hp, (stk, lvars, C, S, pc) # frs) -jvm\<rightarrow> (None, hp', frs')"
+apply (simp only: exec_all_def)
+apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl])
+apply (simp add: gis_def gmb_def)
+apply (case_tac frs', simp+)
+done
+
+theorem exec_all_one_step: "
+  \<lbrakk> gis (gmb G C S) = pre @ (i # post); pc0 = length pre;
+  (exec_instr i G hp0 stk0 lvars0 C S pc0 frs) = 
+  (None, hp1, (stk1,lvars1,C,S, Suc pc0)#frs) \<rbrakk>
+  \<Longrightarrow> 
+  G \<turnstile> (None, hp0, (stk0,lvars0,C,S, pc0)#frs) -jvm\<rightarrow> 
+  (None, hp1, (stk1,lvars1,C,S, Suc pc0)#frs)"
+apply (unfold exec_all_def)
+apply (rule r_into_rtrancl)
+apply (simp add: gis_def gmb_def split_beta)
+done
+
+
+(***********************************************************************)
+
+constdefs
+  progression :: "jvm_prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> 
+                 aheap \<Rightarrow> opstack \<Rightarrow> locvars \<Rightarrow>
+                 bytecode \<Rightarrow>
+                 aheap \<Rightarrow> opstack \<Rightarrow> locvars \<Rightarrow> 
+                 bool"
+  ("{_,_,_} \<turnstile> {_, _, _} >- _ \<rightarrow> {_, _, _}" [61,61,61,61,61,61,90,61,61,61]60)
+  "{G,C,S} \<turnstile> {hp0, os0, lvars0} >- instrs \<rightarrow> {hp1, os1, lvars1} ==
+  \<forall> pre post frs.
+  (gis (gmb G C S) = pre @ instrs @ post) \<longrightarrow>
+   G \<turnstile> (None,hp0,(os0,lvars0,C,S,length pre)#frs) -jvm\<rightarrow>
+       (None,hp1,(os1,lvars1,C,S,(length pre) + (length instrs))#frs)"
+
+
+
+lemma progression_call: 
+  "\<lbrakk> \<forall> pc frs.
+  exec_instr instr G hp0 os0 lvars0 C S pc frs =
+      (None, hp', (os', lvars', C', S', 0) # (fr pc) # frs) \<and> 
+  gis (gmb G C' S') = instrs' @ [Return] \<and> 
+  {G, C', S'} \<turnstile> {hp', os', lvars'} >- instrs' \<rightarrow> {hp'', os'', lvars''}  \<and>
+  exec_instr Return G hp'' os'' lvars'' C' S' (length instrs') 
+                                               ((fr pc) # frs) =
+      (None, hp2, (os2, lvars2, C, S, Suc pc) # frs) \<rbrakk> \<Longrightarrow>
+  {G, C, S} \<turnstile> {hp0, os0, lvars0} >-[instr]\<rightarrow> {hp2,os2,lvars2}"
+apply (simp only: progression_def)
+apply (intro strip)
+apply (drule_tac x="length pre" in spec)
+apply (drule_tac x="frs" in spec)
+apply clarify
+apply (rule exec_all_trans)
+apply (rule exec_instr_in_exec_all) apply simp
+apply simp
+apply (rule exec_all_trans)
+apply (simp only: append_Nil)
+apply (drule_tac x="[]" in spec)
+apply (simp only: list.simps)
+apply blast
+apply (rule exec_instr_in_exec_all)
+apply auto
+done
+
+
+lemma progression_transitive: 
+  "\<lbrakk> instrs_comb = instrs0 @ instrs1; 
+  {G, C, S} \<turnstile> {hp0, os0, lvars0} >- instrs0 \<rightarrow> {hp1, os1, lvars1};
+  {G, C, S} \<turnstile> {hp1, os1, lvars1} >- instrs1 \<rightarrow> {hp2, os2, lvars2} \<rbrakk>
+  \<Longrightarrow>
+  {G, C, S} \<turnstile> {hp0, os0, lvars0} >- instrs_comb \<rightarrow> {hp2, os2, lvars2}"
+apply (simp only: progression_def)
+apply (intro strip)
+apply (rule_tac "s1.0" = "Norm (hp1, (os1, lvars1, C, S, 
+                          length pre + length instrs0) # frs)"  
+       in exec_all_trans)
+apply (simp only: append_assoc)
+apply (erule thin_rl, erule thin_rl)
+apply (drule_tac x="pre @ instrs0" in spec)
+apply (simp add: add_assoc)
+done
+
+lemma progression_refl: 
+  "{G, C, S} \<turnstile> {hp0, os0, lvars0} >- [] \<rightarrow> {hp0, os0, lvars0}"
+apply (simp add: progression_def)
+apply (intro strip)
+apply (rule exec_all_refl)
+done
+
+lemma progression_one_step: "
+  \<forall> pc frs. 
+  (exec_instr i G hp0 os0 lvars0 C S pc frs) = 
+  (None, hp1, (os1,lvars1,C,S, Suc pc)#frs)
+  \<Longrightarrow> {G, C, S} \<turnstile> {hp0, os0, lvars0} >- [i] \<rightarrow> {hp1, os1, lvars1}"
+apply (unfold progression_def)
+apply (intro strip)
+apply simp
+apply (rule exec_all_one_step)
+apply auto
+done
+
+(*****)
+constdefs
+  jump_fwd :: "jvm_prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> 
+                 aheap \<Rightarrow> locvars \<Rightarrow> opstack \<Rightarrow> opstack \<Rightarrow> 
+                 instr \<Rightarrow> bytecode \<Rightarrow> bool"
+  "jump_fwd G C S hp lvars os0 os1 instr instrs ==
+  \<forall> pre post frs.
+  (gis (gmb G C S) = pre @ instr # instrs @ post) \<longrightarrow>
+   exec_all G (None,hp,(os0,lvars,C,S, length pre)#frs)
+    (None,hp,(os1,lvars,C,S,(length pre) + (length instrs) + 1)#frs)"
+
+
+lemma jump_fwd_one_step:
+  "\<forall> pc frs.
+  exec_instr instr G hp os0 lvars C S pc frs = 
+    (None, hp, (os1, lvars, C, S, pc + (length instrs) + 1)#frs)
+  \<Longrightarrow> jump_fwd G C S hp lvars os0 os1 instr instrs"
+apply (unfold jump_fwd_def)
+apply (intro strip)
+apply (rule exec_instr_in_exec_all)
+apply auto
+done
+
+
+lemma jump_fwd_progression_aux: 
+  "\<lbrakk> instrs_comb = instr # instrs0 @ instrs1; 
+     jump_fwd G C S hp lvars os0 os1 instr instrs0;
+     {G, C, S} \<turnstile> {hp, os1, lvars} >- instrs1 \<rightarrow> {hp2, os2, lvars2} \<rbrakk> 
+  \<Longrightarrow> {G, C, S} \<turnstile> {hp, os0, lvars} >- instrs_comb \<rightarrow> {hp2, os2, lvars2}"
+apply (simp only: progression_def jump_fwd_def)
+apply (intro strip)
+apply (rule_tac "s1.0" = "Norm(hp, (os1, lvars, C, S, length pre + length instrs0 + 1) # frs)" in exec_all_trans)
+apply (simp only: append_assoc)
+apply (subgoal_tac "pre @ (instr # instrs0 @ instrs1) @ post = pre @ instr # instrs0 @ (instrs1 @ post)")
+apply blast
+apply simp
+apply (erule thin_rl, erule thin_rl)
+apply (drule_tac x="pre @ instr # instrs0" in spec)
+apply (simp add: add_assoc)
+done
+
+
+lemma jump_fwd_progression:
+  "\<lbrakk> instrs_comb = instr # instrs0 @ instrs1; 
+  \<forall> pc frs.
+  exec_instr instr G hp os0 lvars C S pc frs = 
+    (None, hp, (os1, lvars, C, S, pc + (length instrs0) + 1)#frs);
+  {G, C, S} \<turnstile> {hp, os1, lvars} >- instrs1 \<rightarrow> {hp2, os2, lvars2} \<rbrakk> 
+  \<Longrightarrow> {G, C, S}  \<turnstile> {hp, os0, lvars} >- instrs_comb \<rightarrow> {hp2, os2, lvars2}"
+apply (rule jump_fwd_progression_aux)
+apply assumption
+apply (rule jump_fwd_one_step) apply assumption+
+done
+
+
+(* note: instrs and instr reversed wrt. jump_fwd *)
+constdefs
+  jump_bwd :: "jvm_prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> 
+                 aheap \<Rightarrow> locvars \<Rightarrow> opstack \<Rightarrow> opstack \<Rightarrow> 
+                 bytecode \<Rightarrow> instr \<Rightarrow> bool"
+  "jump_bwd G C S hp lvars os0 os1 instrs instr ==
+  \<forall> pre post frs.
+  (gis (gmb G C S) = pre @ instrs @ instr # post) \<longrightarrow>
+   exec_all G (None,hp,(os0,lvars,C,S, (length pre) + (length instrs))#frs)
+    (None,hp,(os1,lvars,C,S, (length pre))#frs)"
+
+
+lemma jump_bwd_one_step:
+  "\<forall> pc frs.
+  exec_instr instr G hp os0 lvars C S (pc + (length instrs)) frs = 
+    (None, hp, (os1, lvars, C, S, pc)#frs)
+  \<Longrightarrow> 
+  jump_bwd G C S hp lvars os0 os1 instrs instr"
+apply (unfold jump_bwd_def)
+apply (intro strip)
+apply (rule exec_instr_in_exec_all)
+apply auto
+done
+
+lemma jump_bwd_progression: 
+  "\<lbrakk> instrs_comb = instrs @ [instr]; 
+  {G, C, S} \<turnstile> {hp0, os0, lvars0} >- instrs \<rightarrow> {hp1, os1, lvars1};
+  jump_bwd G C S hp1 lvars1 os1 os2 instrs instr;
+  {G, C, S} \<turnstile> {hp1, os2, lvars1} >- instrs_comb \<rightarrow> {hp3, os3, lvars3} \<rbrakk> 
+  \<Longrightarrow> {G, C, S}  \<turnstile> {hp0, os0, lvars0} >- instrs_comb \<rightarrow> {hp3, os3, lvars3}"
+apply (simp only: progression_def jump_bwd_def)
+apply (intro strip)
+apply (rule exec_all_trans, force)
+apply (rule exec_all_trans, force)
+apply (rule exec_all_trans, force)
+apply simp
+apply (rule exec_all_refl)
+done
+
+
+(**********************************************************************)
+
+(* class C with signature S is defined in program G *)
+constdefs class_sig_defined :: "'c prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> bool"
+  "class_sig_defined G C S == 
+  is_class G C \<and> (\<exists> D rT mb. (method (G, C) S = Some (D, rT, mb)))"
+
+
+(* The environment of a java method body 
+  (characterized by class and signature) *)
+constdefs env_of_jmb :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> java_mb env"
+  "env_of_jmb G C S == 
+  (let (mn,pTs) = S;
+       (D,rT,(pns,lvars,blk,res)) = the(method (G, C) S) in
+  (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)))"
+
+lemma env_of_jmb_fst [simp]: "fst (env_of_jmb G C S) = G"
+by (simp add: env_of_jmb_def split_beta)
+
+
+(**********************************************************************)
+
+
+(* ### to be moved to one of the J/* files *)
+
+lemma method_preserves [rule_format (no_asm)]:
+  "\<lbrakk> wf_prog wf_mb G; is_class G C; 
+  \<forall> S rT mb. \<forall> cn \<in> fst ` set G. wf_mdecl wf_mb G cn (S,rT,mb)  \<longrightarrow> (P cn S (rT,mb))\<rbrakk>
+ \<Longrightarrow> \<forall> D. 
+  method (G, C) S = Some (D, rT, mb) \<longrightarrow> (P D S (rT,mb))"
+
+apply (frule WellForm.wf_subcls1)
+apply (rule subcls1_induct, assumption, assumption)
+
+apply (intro strip)
+apply ((drule spec)+, drule_tac x="Object" in bspec)
+apply (simp add: wf_prog_def wf_syscls_def)
+apply (subgoal_tac "D=Object") apply simp
+apply (drule mp)
+apply (frule_tac C=Object in method_wf_mdecl)
+ apply simp apply assumption apply simp apply assumption apply simp
+
+apply (subst method_rec) apply simp
+apply force
+apply assumption
+apply (simp only: override_def)
+apply (split option.split)
+apply (rule conjI)
+apply force
+apply (intro strip)
+apply (frule_tac
+  "P1.0" = "wf_mdecl wf_mb G Ca" and
+  "P2.0" = "%(S, (Da, rT, mb)). P Da S (rT, mb)" in map_of_map_prop)
+apply (force simp: wf_cdecl_def)
+
+apply clarify
+
+apply (simp only: class_def)
+apply (drule map_of_SomeD)+
+apply (frule_tac A="set G" and f=fst in imageI, simp)
+apply blast
+apply simp
+done
+
+
+lemma method_preserves_length:
+  "\<lbrakk> wf_java_prog G; is_class G C; 
+  method (G, C) (mn,pTs) = Some (D, rT, pns, lvars, blk, res)\<rbrakk>
+ \<Longrightarrow> length pns = length pTs"
+apply (frule_tac 
+  P="%D (mn,pTs) (rT, pns, lvars, blk, res). length pns = length pTs"
+  in method_preserves)
+apply (auto simp: wf_mdecl_def wf_java_mdecl_def)
+done
+
+(**********************************************************************)
+
+(* required for lemma wtpd_expr_call *)
+lemma ty_exprs_length [simp]: "(E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts)"
+apply (subgoal_tac "(E\<turnstile>e::T \<longrightarrow> True) \<and> (E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts) \<and> (E\<turnstile>s\<surd> \<longrightarrow> True)")
+apply blast
+apply (rule ty_expr_ty_exprs_wt_stmt.induct)
+apply auto
+done
+
+constdefs wtpd_expr :: "java_mb env \<Rightarrow> expr \<Rightarrow> bool"
+  "wtpd_expr E e == (\<exists> T. E\<turnstile>e :: T)"
+  wtpd_exprs :: "java_mb env \<Rightarrow> (expr list) \<Rightarrow> bool"
+  "wtpd_exprs E e == (\<exists> T. E\<turnstile>e [::] T)"
+  wtpd_stmt :: "java_mb env \<Rightarrow> stmt \<Rightarrow> bool" 
+  "wtpd_stmt E c == (E\<turnstile>c \<surd>)"
+
+lemma wtpd_expr_newc: "wtpd_expr E (NewC C) \<Longrightarrow> is_class (prg E) C"
+by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)
+
+lemma wtpd_expr_cast: "wtpd_expr E (Cast cn e) \<Longrightarrow> (wtpd_expr E e)"
+by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)
+
+lemma wtpd_expr_lacc: "\<lbrakk> wtpd_expr (env_of_jmb G C S) (LAcc vn);
+  class_sig_defined G C S \<rbrakk>
+  \<Longrightarrow> vn \<in> set (gjmb_plns (gmb G C S)) \<or> vn = This"
+apply (simp only: wtpd_expr_def env_of_jmb_def class_sig_defined_def galldefs)
+apply clarify
+apply (case_tac S)
+apply simp
+apply (erule ty_expr.cases)
+apply (auto dest: map_upds_SomeD map_of_SomeD fst_in_set_lemma)
+apply (drule map_upds_SomeD)
+apply (erule disjE)
+  apply assumption
+  apply (drule map_of_SomeD) apply (auto dest: fst_in_set_lemma)
+done
+
+lemma wtpd_expr_lass: "wtpd_expr E (vn::=e)
+  \<Longrightarrow> (vn \<noteq> This) & (wtpd_expr E (LAcc vn)) & (wtpd_expr E e)"
+by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)
+
+lemma wtpd_expr_facc: "wtpd_expr E ({fd}a..fn) 
+  \<Longrightarrow> (wtpd_expr E a)"
+by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)
+
+lemma wtpd_expr_fass: "wtpd_expr E ({fd}a..fn:=v) 
+  \<Longrightarrow> (wtpd_expr E ({fd}a..fn)) & (wtpd_expr E v)"
+by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)
+
+
+lemma wtpd_expr_binop: "wtpd_expr E (BinOp bop e1 e2)
+  \<Longrightarrow> (wtpd_expr E e1) & (wtpd_expr E e2)"
+by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)
+
+lemma wtpd_exprs_cons: "wtpd_exprs E (e # es)
+  \<Longrightarrow> (wtpd_expr E e) & (wtpd_exprs E es)"
+by (simp only: wtpd_exprs_def wtpd_expr_def, erule exE, erule ty_exprs.cases, auto)
+
+lemma wtpd_stmt_expr: "wtpd_stmt E (Expr e) \<Longrightarrow> (wtpd_expr E e)"
+by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto)
+
+lemma wtpd_stmt_comp: "wtpd_stmt E (s1;; s2) \<Longrightarrow> 
+   (wtpd_stmt E s1) &  (wtpd_stmt E s2)"
+by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto)
+
+lemma wtpd_stmt_cond: "wtpd_stmt E (If(e) s1 Else s2) \<Longrightarrow>
+   (wtpd_expr E e) & (wtpd_stmt E s1) &  (wtpd_stmt E s2)
+  & (E\<turnstile>e::PrimT Boolean)"
+by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto)
+
+lemma wtpd_stmt_loop: "wtpd_stmt E (While(e) s) \<Longrightarrow>
+   (wtpd_expr E e) & (wtpd_stmt E s) & (E\<turnstile>e::PrimT Boolean)"
+by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto)
+
+lemma wtpd_expr_call: "wtpd_expr E ({C}a..mn({pTs'}ps))
+  \<Longrightarrow> (wtpd_expr E a) & (wtpd_exprs E ps) 
+  & (length ps = length pTs') & (E\<turnstile>a::Class C)
+  & (\<exists> pTs md rT. 
+       E\<turnstile>ps[::]pTs & max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')})"
+apply (simp only: wtpd_expr_def wtpd_exprs_def)
+apply (erule exE)
+apply (ind_cases "E \<turnstile> {C}a..mn( {pTs'}ps) :: T")
+apply (auto simp: max_spec_preserves_length)
+done
+
+lemma wtpd_blk: 
+  "\<lbrakk> method (G, D) (md, pTs) = Some (D, rT, (pns, lvars, blk, res)); 
+  wf_prog wf_java_mdecl G; is_class G D \<rbrakk>
+ \<Longrightarrow> wtpd_stmt (env_of_jmb G D (md, pTs)) blk"
+apply (simp add: wtpd_stmt_def env_of_jmb_def)
+apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). (G, map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class D)) \<turnstile> blk \<surd> " in method_preserves)
+apply (auto simp: wf_mdecl_def wf_java_mdecl_def)
+done
+
+lemma wtpd_res: 
+  "\<lbrakk> method (G, D) (md, pTs) = Some (D, rT, (pns, lvars, blk, res)); 
+  wf_prog wf_java_mdecl G; is_class G D \<rbrakk>
+ \<Longrightarrow> wtpd_expr (env_of_jmb G D (md, pTs)) res"
+apply (simp add: wtpd_expr_def env_of_jmb_def)
+apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). \<exists>T. (G, map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class D)) \<turnstile> res :: T " in method_preserves)
+apply (auto simp: wf_mdecl_def wf_java_mdecl_def)
+done
+
+
+(**********************************************************************)
+
+
+(* Is there a more elegant proof? *)
+lemma evals_preserves_length:
+  "G\<turnstile> xs -es[\<succ>]vs-> (None, s) \<Longrightarrow> length es = length vs"
+apply (subgoal_tac 
+  "\<forall> xs'. (G \<turnstile> xk -xj\<succ>xi-> xh \<longrightarrow> True) & 
+  (G\<turnstile> xs -es[\<succ>]vs-> xs' \<longrightarrow>  (\<exists> s. (xs' = (None, s))) \<longrightarrow> 
+  length es = length vs) &
+  ((xc, xb, xa) \<in> Eval.exec G \<longrightarrow> True)")
+apply blast
+apply (rule allI)
+apply (rule Eval.eval_evals_exec.induct)
+apply auto
+done
+
+(***********************************************************************)
+
+(* required for translation of BinOp *)
+
+
+lemma progression_Eq : "{G, C, S} \<turnstile>
+  {hp, (v2 # v1 # os), lvars} 
+  >- [Ifcmpeq 3, LitPush (Bool False), Goto 2, LitPush (Bool True)] \<rightarrow>
+  {hp, (Bool (v1 = v2) # os), lvars}"
+apply (case_tac "v1 = v2")
+
+(* case v1 = v2 *)
+apply (rule_tac "instrs1.0" = "[LitPush (Bool True)]" in jump_fwd_progression)
+apply (auto simp: NatBin.nat_add_distrib)
+apply (rule progression_one_step) apply simp
+
+(* case v1 \<noteq> v2 *)
+apply (rule progression_one_step [THEN HOL.refl [THEN progression_transitive], simplified])
+apply auto
+apply (rule progression_one_step [THEN HOL.refl [THEN progression_transitive], simplified]) 
+apply auto
+apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression)
+apply (auto simp: NatBin.nat_add_distrib intro: progression_refl)
+done
+
+
+(**********************************************************************)
+
+
+(* to avoid automatic pair splits *)
+
+declare split_paired_All [simp del] split_paired_Ex [simp del]
+ML_setup {*
+simpset_ref() := simpset() delloop "split_all_tac"
+*}
+
+lemma distinct_method: "\<lbrakk> wf_java_prog G; is_class G C; 
+  method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk> \<Longrightarrow> 
+  distinct (gjmb_plns (gmb G C S))"
+apply (frule method_wf_mdecl [THEN conjunct2],  assumption, assumption)
+apply (case_tac S)
+apply (simp add: wf_mdecl_def wf_java_mdecl_def galldefs distinct_append)
+apply (simp add: unique_def map_of_in_set)
+apply blast
+done
+
+lemma distinct_method_if_class_sig_defined : 
+  "\<lbrakk> wf_java_prog G; class_sig_defined G C S \<rbrakk> \<Longrightarrow> 
+  distinct (gjmb_plns (gmb G C S))"
+by (auto intro: distinct_method simp: class_sig_defined_def)
+
+
+lemma method_yields_wf_java_mdecl: "\<lbrakk> wf_java_prog G; is_class G C;
+  method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk>  \<Longrightarrow> 
+  wf_java_mdecl G D (S,rT,(pns,lvars,blk,res))"
+apply (frule method_wf_mdecl)
+apply (auto simp: wf_mdecl_def)
+done
+
+(**********************************************************************)
+
+
+lemma progression_lvar_init_aux [rule_format (no_asm)]: "
+  \<forall> zs prfx lvals lvars0. 
+  lvars0 =  (zs @ lvars) \<longrightarrow>
+  (disjoint_varnames pns lvars0 \<longrightarrow>
+  (length lvars = length lvals) \<longrightarrow> 
+  (Suc(length pns + length zs) = length prfx) \<longrightarrow> 
+   ({cG, D, S} \<turnstile> 
+    {h, os, (prfx @ lvals)}
+    >- (concat (map (compInit (pns, lvars0, blk, res)) lvars)) \<rightarrow>
+    {h, os, (prfx @ (map (\<lambda>p. (default_val (snd p))) lvars))}))"
+apply simp
+apply (induct lvars)
+apply (clarsimp, rule progression_refl)
+apply (intro strip)
+apply (case_tac lvals) apply simp
+apply (simp (no_asm_simp) )
+
+apply (rule_tac "lvars1.0" = "(prfx @ [default_val (snd a)]) @ lista" in progression_transitive, rule HOL.refl)
+apply (case_tac a) apply (simp (no_asm_simp) add: compInit_def)
+apply (rule_tac "instrs0.0" = "[load_default_val b]" in progression_transitive, simp)
+apply (rule progression_one_step)
+apply (simp (no_asm_simp) add: load_default_val_def)
+apply (rule conjI, simp)+ apply (rule HOL.refl)
+
+apply (rule progression_one_step)
+apply (simp (no_asm_simp))
+apply (rule conjI, simp)+
+apply (simp add: index_of_var2)
+apply (drule_tac x="zs @ [a]" in spec) (* instantiate zs *)
+apply (drule mp, simp)
+apply (drule_tac x="(prfx @ [default_val (snd a)])" in spec) (* instantiate prfx *)
+apply auto
+done
+
+lemma progression_lvar_init [rule_format (no_asm)]: 
+  "\<lbrakk> wf_java_prog G; is_class G C;
+  method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk> \<Longrightarrow> 
+  length pns = length pvs \<longrightarrow> 
+  (\<forall> lvals. 
+  length lvars = length lvals \<longrightarrow>
+   {cG, D, S} \<turnstile>
+   {h, os, (a' # pvs @ lvals)}
+   >- (compInitLvars (pns, lvars, blk, res) lvars) \<rightarrow>
+   {h, os, (locvars_xstate G C S (Norm (h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))))})"
+apply (simp only: compInitLvars_def)
+apply (frule method_yields_wf_java_mdecl, assumption, assumption)
+
+apply (simp only: wf_java_mdecl_def)
+apply (subgoal_tac "(\<forall>y\<in>set pns. y \<notin> set (map fst lvars))")
+apply (simp add: init_vars_def locvars_xstate_def locvars_locals_def galldefs unique_def split_def map_of_map_as_map_upd)
+apply (intro strip)
+apply (simp (no_asm_simp) only: append_Cons [THEN sym])
+apply (rule progression_lvar_init_aux)
+apply (auto simp: unique_def map_of_in_set disjoint_varnames_def)
+done
+
+
+
+
+
+
+
+
+
+(**********************************************************************)
+
+constdefs
+  state_ok :: "java_mb env \<Rightarrow> xstate \<Rightarrow> bool"
+  "state_ok E xs == xs::\<preceq>E"
+
+
+lemma state_ok_eval: "\<lbrakk>state_ok E xs; wf_java_prog (prg E); wtpd_expr E e;
+  (prg E)\<turnstile>xs -e\<succ>v -> xs'\<rbrakk> \<Longrightarrow>  state_ok E xs'"
+apply (simp only: state_ok_def wtpd_expr_def)
+apply (erule exE)
+apply (case_tac xs', case_tac xs, simp only:)
+apply (rule eval_type_sound [THEN conjunct1])
+apply (rule HOL.refl)
+apply assumption
+apply (subgoal_tac "fst E \<turnstile> (gx xs, gs xs) -e\<succ>v-> (gx xs', gs xs')")
+apply assumption
+apply (auto simp: gx_def gs_def)
+done
+
+(* to be moved into JTypeSafe.thy *)
+lemma evals_type_sound: "!!E s s'.  
+  [| G\<turnstile>(x,s) -es[\<succ>]vs -> (x',s'); G=prg E; wf_java_prog G; (x,s)::\<preceq>E; E\<turnstile>es[::]Ts |]  
+  ==> (x',s')::\<preceq>E \<and> (x'=None --> list_all2 (conf G (heap s')) vs Ts)"
+apply( simp (no_asm_simp) only: split_tupled_all)
+apply (drule eval_evals_exec_type_sound 
+             [THEN conjunct2, THEN conjunct1, THEN mp, THEN spec, THEN mp])
+apply auto
+done
+
+lemma state_ok_evals: "\<lbrakk>state_ok E xs; wf_java_prog (prg E); wtpd_exprs E es;
+  (xs,es,vs,xs') \<in> Eval.evals (prg E)\<rbrakk> \<Longrightarrow>  state_ok E xs'"
+apply (simp only: state_ok_def wtpd_exprs_def)
+apply (erule exE)
+apply (case_tac xs) apply (case_tac xs') apply (simp only:)
+apply (rule evals_type_sound [THEN conjunct1])
+apply (auto simp: gx_def gs_def)
+done
+
+lemma state_ok_exec: "\<lbrakk>state_ok E xs; wf_java_prog (prg E); wtpd_stmt E st;
+  (xs,st,xs') \<in> Eval.exec (prg E)\<rbrakk> \<Longrightarrow>  state_ok E xs'"
+apply (simp only: state_ok_def wtpd_stmt_def)
+apply (case_tac xs', case_tac xs, simp only:)
+apply (rule exec_type_sound)
+apply (rule HOL.refl)
+apply assumption
+apply (subgoal_tac "((gx xs, gs xs), st, (gx xs', gs xs')) \<in> Eval.exec (fst E)")
+apply assumption
+apply (auto simp: gx_def gs_def)
+done
+
+
+lemma state_ok_init: 
+  "\<lbrakk> wf_java_prog G; state_ok (env_of_jmb G C S) (x, h, l); 
+  is_class G dynT;
+  method (G, dynT) (mn, pTs) = Some (md, rT, pns, lvars, blk, res);
+  list_all2 (conf G h) pvs pTs; G,h \<turnstile> a' ::\<preceq> Class md\<rbrakk>
+\<Longrightarrow>
+state_ok (env_of_jmb G md (mn, pTs)) (np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))"
+apply (frule method_in_md [THEN conjunct2], assumption+)
+apply (frule method_yields_wf_java_mdecl, assumption, assumption)
+apply (simp add: state_ok_def env_of_jmb_def gs_def conforms_def split_beta)
+apply (simp add: wf_java_mdecl_def)
+apply (rule conjI)
+apply (rule lconf_ext)
+apply (rule lconf_ext_list)
+apply (rule lconf_init_vars)
+apply (auto dest: Ball_set_table)
+apply (simp add: np_def xconf_raise_if)
+done
+
+
+lemma ty_exprs_list_all2 [rule_format (no_asm)]: 
+  "(\<forall> Ts. (E \<turnstile> es [::] Ts) = list_all2 (\<lambda>e T. E \<turnstile> e :: T) es Ts)"
+apply (rule list.induct)
+apply simp
+apply (rule allI)
+apply (rule iffI)
+  apply (ind_cases "E \<turnstile> [] [::] Ts", assumption)
+  apply simp apply (rule WellType.Nil)
+apply (simp add: list_all2_Cons1)
+apply (rule allI)
+apply (rule iffI)
+  apply (rename_tac a exs Ts)
+  apply (ind_cases "E \<turnstile> a # exs  [::] Ts") apply blast
+  apply (auto intro: WellType.Cons)
+done
+
+
+lemma conf_bool: "G,h \<turnstile> v::\<preceq>PrimT Boolean \<Longrightarrow> \<exists> b. v = Bool b"
+apply (simp add: conf_def)
+apply (erule exE)
+apply (case_tac v)
+apply (auto elim: widen.cases)
+done
+
+
+lemma class_expr_is_class: "\<lbrakk>E \<turnstile> e :: Class C; wf_prog wf_mb (prg E)\<rbrakk> 
+  \<Longrightarrow> is_class (prg E) C"
+by (case_tac E, auto dest: ty_expr_is_type)
+
+
+lemma max_spec_widen: "max_spec G C (mn, pTs) = {((md,rT),pTs')} \<Longrightarrow> 
+  list_all2 (\<lambda> T T'. G \<turnstile> T \<preceq> T') pTs pTs'"
+by (blast dest: singleton_in_set max_spec2appl_meths appl_methsD)
+
+
+lemma eval_conf: "\<lbrakk>G \<turnstile> s -e\<succ>v-> s'; wf_java_prog G; state_ok E s;
+  E\<turnstile>e::T; gx s' = None; prg E = G \<rbrakk> 
+  \<Longrightarrow> G,gh s'\<turnstile>v::\<preceq>T"
+apply (simp add: gh_def)
+apply (rule_tac x2="fst s" and "s2"="snd s"and "x'2"="fst s'"  
+  in eval_type_sound [THEN conjunct2 [THEN mp], simplified])
+apply (rule sym) apply assumption
+apply assumption
+apply (simp (no_asm_use) add: surjective_pairing [THEN sym])
+apply (simp only: state_ok_def gs_def)
+apply (case_tac s, simp)
+apply assumption
+apply (simp add: gx_def)
+done
+
+lemma evals_preserves_conf:
+  "\<lbrakk> G\<turnstile> s -es[\<succ>]vs-> s'; G,gh s \<turnstile> t ::\<preceq> T; E \<turnstile>es[::]Ts;
+  wf_java_prog G; state_ok E s; 
+  prg E = G \<rbrakk> \<Longrightarrow> G,gh s' \<turnstile> t ::\<preceq> T"
+apply (subgoal_tac "gh s\<le>| gh s'")
+apply (frule conf_hext, assumption, assumption)
+apply (frule eval_evals_exec_type_sound [THEN conjunct2 [THEN conjunct1 [THEN mp]]]) 
+apply (subgoal_tac "G \<turnstile> (gx s, (gh s, gl s)) -es[\<succ>]vs-> (gx s', (gh s', gl s'))")
+apply assumption
+apply (simp add: gx_def gh_def gl_def surjective_pairing [THEN sym])
+apply (case_tac E)
+apply (simp add: gx_def gs_def gh_def gl_def state_ok_def
+  surjective_pairing [THEN sym])
+done
+
+lemma eval_of_class: "\<lbrakk> G \<turnstile> s -e\<succ>a'-> s'; E \<turnstile> e :: Class C; 
+  wf_java_prog G; state_ok E s; gx s'=None; a' \<noteq> Null; G=prg E\<rbrakk>
+  \<Longrightarrow> (\<exists> lc. a' = Addr lc)"
+apply (case_tac s, case_tac s', simp)
+apply (frule eval_type_sound, (simp add: state_ok_def gs_def)+)
+apply (case_tac a')
+apply (auto simp: conf_def)
+done
+
+
+lemma dynT_subcls: 
+  "\<lbrakk> a' \<noteq> Null; G,h\<turnstile>a'::\<preceq> Class C; dynT = fst (the (h (the_Addr a')));
+  is_class G dynT; wf_prog wf_mb G \<rbrakk> \<Longrightarrow> G\<turnstile>dynT \<preceq>C C"
+apply (case_tac "C = Object")
+apply (simp, rule subcls_C_Object, assumption+)
+apply (frule non_np_objD, auto)
+done
+
+
+lemma method_defined: "\<lbrakk> 
+  m = the (method (G, dynT) (mn, pTs)); 
+  dynT = fst (the (h a)); is_class G dynT; wf_java_prog G; 
+  a' \<noteq> Null; G,h\<turnstile>a'::\<preceq> Class C; a = the_Addr a';
+  \<exists>pTsa md rT. max_spec G C (mn, pTsa) = {((md, rT), pTs)} \<rbrakk>
+\<Longrightarrow> (method (G, dynT) (mn, pTs)) = Some m"
+apply (erule exE)+
+apply (drule singleton_in_set, drule max_spec2appl_meths)
+apply (simp add: appl_methds_def)
+apply ((erule exE)+, (erule conjE)+, (erule exE)+)
+apply (drule widen_methd)
+apply assumption
+apply (rule dynT_subcls, assumption+, simp, assumption+)
+apply (erule exE)+ apply simp
+done
+
+
+
+(**********************************************************************)
+
+
+(* 1. any difference between locvars_xstate \<dots> and L ??? *)
+(* 2. possibly skip env_of_jmb ??? *)
+theorem compiler_correctness: 
+  "wf_java_prog G \<Longrightarrow>
+  ((xs,ex,val,xs') \<in> Eval.eval G \<longrightarrow>
+  gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow>
+  (\<forall> os CL S.
+  (class_sig_defined G CL S) \<longrightarrow> 
+  (wtpd_expr (env_of_jmb G CL S) ex) \<longrightarrow>
+  (state_ok (env_of_jmb G CL S) xs) \<longrightarrow>
+  ( {TranslComp.comp G, CL, S} \<turnstile>
+    {gh xs, os, (locvars_xstate G CL S xs)}
+    >- (compExpr (gmb G CL S) ex) \<rightarrow>
+    {gh xs', val#os, locvars_xstate G CL S xs'}))) \<and> 
+
+ ((xs,exs,vals,xs') \<in> Eval.evals G \<longrightarrow>
+  gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow>
+  (\<forall> os CL S.
+  (class_sig_defined G CL S) \<longrightarrow> 
+  (wtpd_exprs (env_of_jmb G CL S) exs) \<longrightarrow>
+  (state_ok (env_of_jmb G CL S) xs) \<longrightarrow>
+  ( {TranslComp.comp G, CL, S} \<turnstile>
+    {gh xs, os, (locvars_xstate G CL S xs)}
+    >- (compExprs (gmb G CL S) exs) \<rightarrow>
+    {gh xs', (rev vals)@os, (locvars_xstate G CL S xs')}))) \<and> 
+
+  ((xs,st,xs') \<in> Eval.exec G \<longrightarrow>
+   gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow>
+  (\<forall> os CL S.
+  (class_sig_defined G CL S) \<longrightarrow> 
+  (wtpd_stmt (env_of_jmb G CL S) st) \<longrightarrow>
+  (state_ok (env_of_jmb G CL S) xs) \<longrightarrow>
+  ( {TranslComp.comp G, CL, S} \<turnstile>
+    {gh xs, os, (locvars_xstate G CL S xs)}
+    >- (compStmt (gmb G CL S) st) \<rightarrow>
+    {gh xs', os, (locvars_xstate G CL S xs')})))"
+apply (rule Eval.eval_evals_exec.induct)
+
+(* case XcptE *)
+apply simp
+
+(* case NewC *) 
+apply clarify
+apply (frule wf_subcls1) (* establish  wf ((subcls1 G)^-1) *)
+apply (simp add: c_hupd_hp_invariant)
+apply (rule progression_one_step)
+apply (rotate_tac 1, drule sym) (* reverse equation (a, None) = new_Addr (fst s) *)
+apply (simp add: locvars_xstate_def locvars_locals_def comp_fields)
+
+
+(* case Cast *)
+apply (intro allI impI)
+apply simp
+apply (frule raise_if_NoneD)
+apply (frule wtpd_expr_cast)
+apply simp
+apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, simp)
+apply blast
+apply (rule progression_one_step)
+apply (simp add: raise_system_xcpt_def  gh_def comp_cast_ok)
+
+
+(* case Lit *)
+apply simp
+apply (intro strip)
+apply (rule progression_one_step)
+apply simp
+
+
+(* case BinOp *)
+apply (intro allI impI)
+apply (frule_tac xs=s1 in eval_xcpt, assumption) (* establish (gx s1 = None) *)
+apply (frule wtpd_expr_binop)
+(* establish (state_ok \<dots> s1) *)
+apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp)) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst) 
+
+
+apply (simp (no_asm_use) only: compExpr_compExprs.simps)
+apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e1" in progression_transitive, simp) apply blast
+apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e2" in progression_transitive, simp) apply blast
+apply (case_tac bop)
+  (*subcase bop = Eq *)  apply simp apply (rule progression_Eq)
+  (*subcase bop = Add *) apply simp apply (rule progression_one_step) apply simp
+
+
+(* case LAcc *)
+apply simp
+apply (intro strip)
+apply (rule progression_one_step)
+apply (simp add: locvars_xstate_def locvars_locals_def)
+apply (frule wtpd_expr_lacc)
+apply assumption
+apply (simp add: gl_def)
+apply (erule select_at_index)
+
+
+(* case LAss *)
+apply (intro allI impI)
+apply (frule wtpd_expr_lass, erule conjE, erule conjE)
+apply (simp add: compExpr_compExprs.simps)
+
+apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
+apply blast
+
+apply (rule_tac "instrs0.0" = "[Dup]" in progression_transitive, simp)
+apply (rule progression_one_step)
+apply (simp add: gh_def)
+apply (rule conjI, simp)+ apply simp
+apply (rule progression_one_step)
+apply (simp add: gh_def)
+(* the following falls out of the general scheme *)
+apply (frule wtpd_expr_lacc) apply assumption
+apply (rule update_at_index)
+apply (rule distinct_method_if_class_sig_defined) apply assumption
+apply assumption apply simp apply assumption
+
+
+(* case FAcc *)
+apply (intro allI impI)
+   (* establish x1 = None \<and> a' \<noteq> Null *)
+apply (simp (no_asm_use) only: gx_conv, frule np_NoneD)
+apply (frule wtpd_expr_facc)
+
+apply (simp (no_asm_use) only: compExpr_compExprs.simps)
+apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
+apply blast
+apply (rule progression_one_step)
+apply (simp add: gh_def)
+apply (case_tac "(the (fst s1 (the_Addr a')))")
+apply (simp add: raise_system_xcpt_def)
+
+
+(* case FAss *)
+apply (intro allI impI)
+apply (frule wtpd_expr_fass) apply (erule conjE) apply (frule wtpd_expr_facc)
+apply (simp only: c_hupd_xcpt_invariant) (* establish x2 = None *)
+   (* establish x1 = None  and  a' \<noteq> Null  *)
+apply (frule_tac xs="(np a' x1, s1)" in eval_xcpt)
+apply (simp only: gx_conv, simp only: gx_conv, frule np_NoneD, erule conjE)
+
+
+  (* establish (state_ok \<dots> (Norm s1)) *)
+apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst) 
+
+apply (simp only: compExpr_compExprs.simps)
+
+apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e1)" in progression_transitive, rule HOL.refl)
+apply fast (* blast does not seem to work - why? *)
+apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e2)" in progression_transitive, rule HOL.refl)
+apply fast
+apply (rule_tac "instrs0.0" = "[Dup_x1]" and "instrs1.0" = "[Putfield fn T]" in progression_transitive, simp)
+
+   (* Dup_x1 *)
+   apply (rule progression_one_step)
+   apply (simp add: gh_def)
+   apply (rule conjI, simp)+ apply simp
+
+
+   (* Putfield \<longrightarrow> still looks nasty*)
+   apply (rule progression_one_step)
+   apply simp
+   apply (case_tac "(the (fst s2 (the_Addr a')))")
+   apply (simp add: c_hupd_hp_invariant)
+   apply (case_tac s2)
+   apply (simp add: c_hupd_conv raise_system_xcpt_def)
+   apply (rule locvars_xstate_par_dep, rule HOL.refl)
+
+defer (* method call *)
+
+(* case XcptEs *)
+apply simp
+
+(* case Nil *)
+apply (simp add: compExpr_compExprs.simps)
+apply (intro strip)
+apply (rule progression_refl)
+
+(* case Cons *)
+apply (intro allI impI)
+apply (frule_tac xs=s1 in evals_xcpt, simp only: gx_conv) (* establish gx s1 = None *)
+apply (frule wtpd_exprs_cons)
+   (* establish (state_ok \<dots> (Norm s0)) *)
+apply (frule_tac e=e in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst)
+
+apply simp
+apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
+apply fast
+apply fast
+
+
+(* case Statement: exception *)
+apply simp
+
+(* case Skip *)
+apply (intro allI impI)
+apply simp
+apply (rule progression_refl)
+
+(* case Expr *)
+apply (intro allI impI)
+apply (frule wtpd_stmt_expr)
+apply simp
+apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
+apply fast
+apply (rule progression_one_step)
+apply simp
+
+(* case Comp *)
+apply (intro allI impI)
+apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *)
+apply (frule wtpd_stmt_comp)
+
+  (* establish (state_ok \<dots>  s1) *)
+apply (frule_tac st=c1 in state_ok_exec) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst)
+
+apply simp
+apply (rule_tac "instrs0.0" = "(compStmt (gmb G CL S) c1)" in progression_transitive, rule HOL.refl)
+apply fast
+apply fast
+
+
+(* case Cond *)
+apply (intro allI impI)
+apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *)
+apply (frule wtpd_stmt_cond, (erule conjE)+)
+(* establish (state_ok \<dots> s1) *)
+apply (frule_tac e=e in state_ok_eval) 
+apply (simp (no_asm_simp) only: env_of_jmb_fst)
+apply assumption 
+apply (simp (no_asm_use) only: env_of_jmb_fst) 
+(* establish G,gh s1\<turnstile>v::\<preceq>PrimT Boolean *)
+apply (frule eval_conf, assumption+, rule env_of_jmb_fst)
+apply (frule conf_bool) (* establish \<exists>b. v = Bool b *)
+apply (erule exE)
+
+apply simp
+apply (rule_tac "instrs0.0" = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
+apply (rule progression_one_step,  simp)
+apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
+
+apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
+apply fast
+
+apply (case_tac b)
+ (* case b= True *)
+apply simp
+apply (rule_tac "instrs0.0" = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c1)))]" in progression_transitive, simp)
+apply (rule progression_one_step) apply simp
+apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
+apply (rule_tac "instrs0.0" = "(compStmt (gmb G CL S) c1)" in progression_transitive, simp)
+apply fast
+apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression)
+apply (simp, rule conjI, (rule HOL.refl)+)
+apply simp apply (rule conjI, simp) apply (simp add: NatBin.nat_add_distrib)
+apply (rule progression_refl)
+
+ (* case b= False *)
+apply simp
+apply (rule_tac "instrs1.0" = "compStmt (gmb G CL S) c2" in jump_fwd_progression)
+apply (simp, rule conjI, (rule HOL.refl)+)
+apply (simp, rule conjI, rule HOL.refl, simp add: NatBin.nat_add_distrib)
+apply fast
+
+(* case exit Loop *)
+apply (intro allI impI)
+apply (frule wtpd_stmt_loop, (erule conjE)+)
+
+(* establish G,gh s1\<turnstile>v::\<preceq>PrimT Boolean *)
+apply (frule eval_conf, assumption+, rule env_of_jmb_fst)
+apply (frule conf_bool) (* establish \<exists>b. v = Bool b *)
+apply (erule exE)
+apply (case_tac b)
+
+ (* case b= True \<longrightarrow> contradiction *)
+apply simp
+
+ (* case b= False *)
+apply simp
+
+apply (rule_tac "instrs0.0" = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
+apply (rule progression_one_step)
+   apply simp 
+   apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
+
+apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
+apply fast
+apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression)
+apply (simp, rule conjI, rule HOL.refl, rule HOL.refl)
+apply (simp, rule conjI, rule HOL.refl, simp add: NatBin.nat_add_distrib)
+apply (rule progression_refl)
+
+
+(* case continue Loop *)
+apply (intro allI impI)
+apply (frule_tac xs=s2 in exec_xcpt, assumption) (* establish (gx s2 = None) *)
+apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *)
+apply (frule wtpd_stmt_loop, (erule conjE)+)
+
+(* establish (state_ok \<dots> s1) *)
+apply (frule_tac e=e in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst)
+(* establish (state_ok \<dots> s2) *)
+apply (frule_tac xs=s1 and st=c in state_ok_exec)
+apply (simp (no_asm_simp) only: env_of_jmb_fst) apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst)
+
+(* establish G,gh s1\<turnstile>v::\<preceq>PrimT Boolean *)
+apply (frule eval_conf, assumption+, rule env_of_jmb_fst)
+apply (frule conf_bool) (* establish \<exists>b. v = Bool b *)
+apply (erule exE)
+
+apply simp
+apply (rule jump_bwd_progression) 
+apply simp
+apply (rule conjI, (rule HOL.refl)+)
+
+apply (rule_tac "instrs0.0" = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
+apply (rule progression_one_step)
+   apply simp 
+   apply (rule conjI, simp)+ apply simp
+
+apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
+apply fast
+
+apply (case_tac b)
+ (* case b= True *)
+apply simp
+
+apply (rule_tac "instrs0.0" = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c)))]" in progression_transitive, simp)
+apply (rule progression_one_step) apply simp
+apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
+apply fast
+
+ (* case b= False \<longrightarrow> contradiction*)
+apply simp
+
+apply (rule jump_bwd_one_step)
+apply simp
+apply blast
+
+(*****)
+(* case method call *) defer (* !!! NEWC *)
+
+apply (intro allI impI)
+
+apply (frule_tac xs=s3 in eval_xcpt, simp only: gx_conv) (* establish gx s3 = None *)
+apply (frule exec_xcpt, assumption, simp (no_asm_use) only: gx_conv, frule np_NoneD) (* establish x = None \<and> a' \<noteq> Null *)
+apply (frule evals_xcpt, simp only: gx_conv) (* establish gx s1 = None *)
+
+apply (frule wtpd_expr_call, (erule conjE)+)
+
+
+(* assumptions about state_ok and is_class *)
+
+(* establish state_ok (env_of_jmb G CL S) s1 *)
+apply (frule_tac xs="Norm s0" and e=e in state_ok_eval)
+apply (simp (no_asm_simp) only: env_of_jmb_fst, assumption, simp (no_asm_use) only: env_of_jmb_fst)
+
+(* establish state_ok (env_of_jmb G CL S) (x, h, l) *)
+apply (frule_tac xs=s1 and xs'="(x, h, l)" in state_ok_evals)
+apply (simp (no_asm_simp) only: env_of_jmb_fst, assumption, simp only: env_of_jmb_fst)
+
+(* establish \<exists> lc. a' = Addr lc *)
+apply (frule (5) eval_of_class, rule env_of_jmb_fst [THEN sym])
+apply (subgoal_tac "G,h \<turnstile> a' ::\<preceq> Class C")
+apply (subgoal_tac "is_class G dynT")
+
+(* establish method (G, dynT) (mn, pTs) = Some(md, rT, pns, lvars, blk, res) *)
+apply (drule method_defined, assumption+)
+apply (simp only: env_of_jmb_fst)
+apply ((erule exE)+, erule conjE, (rule exI)+, assumption) 
+
+apply (subgoal_tac "is_class G md")
+apply (subgoal_tac "G\<turnstile>Class dynT \<preceq> Class md")
+apply (subgoal_tac " method (G, md) (mn, pTs) = Some (md, rT, pns, lvars, blk, res)")
+apply (subgoal_tac "list_all2 (conf G h) pvs pTs")
+
+(* establish state_ok (env_of_jmb G md (mn, pTs)) (np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a')) *)
+apply (subgoal_tac "G,h \<turnstile> a' ::\<preceq> Class dynT")
+apply (frule (2) conf_widen)
+apply (frule state_ok_init, assumption+)
+
+apply (subgoal_tac "class_sig_defined G md (mn, pTs)")
+apply (frule wtpd_blk, assumption, assumption)
+apply (frule wtpd_res, assumption, assumption)
+apply (subgoal_tac "state_ok (env_of_jmb G md (mn, pTs)) s3")
+
+(* establish method (TranslComp.comp G, md) (mn, pTs) =
+          Some (md, rT, compMethod (pns, lvars, blk, res)) *)
+apply (frule_tac C=md and D=md in comp_method, assumption, assumption)
+
+(* establish
+   method (TranslComp.comp G, dynT) (mn, pTs) =
+          Some (md, rT, compMethod (pns, lvars, blk, res)) *)
+ apply (frule_tac C=dynT and D=md in comp_method, assumption, assumption)
+ apply (simp only: fst_conv snd_conv)
+
+(* establish length pns = length pTs *)
+apply (frule method_preserves_length, assumption, assumption) 
+(* establish length pvs = length ps *)
+apply (frule evals_preserves_length [THEN sym])
+
+(** start evaluating subexpressions **)
+apply (simp (no_asm_use) only: compExpr_compExprs.simps)
+
+  (* evaluate e *)
+apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
+apply fast
+
+  (* evaluate parameters *)
+apply (rule_tac "instrs0.0" = "compExprs (gmb G CL S) ps" in progression_transitive, rule HOL.refl)
+apply fast
+
+  (* invokation *)
+apply (rule progression_call)
+apply (intro allI impI conjI)
+     (* execute Invoke statement *)
+apply (simp (no_asm_use) only: exec_instr.simps)
+apply (erule thin_rl, erule thin_rl, erule thin_rl)
+apply (simp add: compMethod_def raise_system_xcpt_def)
+apply (rule conjI, simp)+ apply (rule HOL.refl)
+
+     (* get instructions of invoked method *)
+apply (simp (no_asm_simp) add: gis_def gmb_def compMethod_def)
+
+       (* var. initialization *)
+apply (rule_tac "instrs0.0" = "(compInitLvars (pns, lvars, blk, res) lvars)" in progression_transitive, rule HOL.refl)
+apply (rule_tac C=md in progression_lvar_init, assumption, assumption, assumption)
+apply (simp (no_asm_simp)) (* length pns = length pvs *)
+apply (simp (no_asm_simp)) (* length lvars = length (replicate (length lvars) arbitrary) *)
+
+
+       (* body statement *)
+apply (rule_tac "instrs0.0" = "compStmt (pns, lvars, blk, res) blk" in progression_transitive, rule HOL.refl)
+apply (subgoal_tac "(pns, lvars, blk, res) = gmb G md (mn, pTs)")
+apply (simp (no_asm_simp))
+apply (simp only: gh_conv)
+apply ((drule mp, rule TrueI)+, (drule spec)+, (drule mp, assumption)+, assumption)
+apply (simp (no_asm_use))
+apply (simp (no_asm_simp) add: gmb_def)
+
+       (* return expression *) 
+apply (subgoal_tac "(pns, lvars, blk, res) = gmb G md (mn, pTs)")
+apply (simp (no_asm_simp))
+apply (simp only: gh_conv)
+apply ((drule mp, rule TrueI)+, (drule spec)+, (drule mp, assumption)+, assumption)
+apply (simp (no_asm_use))
+apply (simp (no_asm_simp) add: gmb_def)
+
+      (* execute return statement *)
+apply (simp (no_asm_use) add: gh_def locvars_xstate_def gl_def del: drop_append)
+apply (subgoal_tac "rev pvs @ a' # os = (rev (a' # pvs)) @ os")
+apply (simp only: drop_append)
+apply (simp (no_asm_simp))
+apply (simp (no_asm_simp))
+
+(* show state_ok \<dots> s3 *)
+apply (rule_tac xs = "(np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))" and st=blk in state_ok_exec)
+apply assumption apply (simp (no_asm_simp) only: env_of_jmb_fst) 
+apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst)
+
+(* show class_sig_defined G md (mn, pTs) *)
+apply (simp (no_asm_simp) add: class_sig_defined_def)
+
+(* show G,h \<turnstile> a' ::\<preceq> Class dynT *)
+apply (frule non_npD) apply assumption
+apply (erule exE)+ apply simp
+apply (rule conf_obj_AddrI) apply simp 
+apply (rule conjI, (rule HOL.refl)+)
+apply (rule widen_Class_Class [THEN iffD1], rule widen.refl)
+
+
+  (* show list_all2 (conf G h) pvs pTs *)
+apply (erule exE)+ apply (erule conjE)+
+apply (rule_tac Ts="pTsa" in conf_list_gext_widen) apply assumption
+apply (subgoal_tac "((gx s1, gs s1), ps, pvs, x, h, l) \<in> evals G")
+apply (frule_tac E="env_of_jmb G CL S" in evals_type_sound)
+apply (simp only: env_of_jmb_fst) 
+apply assumption apply (simp only: state_ok_def)
+apply (simp add: conforms_def xconf_def gs_def)
+apply simp
+apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [THEN sym])
+apply (simp (no_asm_use) only: ty_exprs_list_all2) apply simp
+apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [THEN sym])
+    (* list_all2 (\<lambda>T T'. G \<turnstile> T \<preceq> T') pTsa pTs *)
+    apply (rule max_spec_widen, simp only: env_of_jmb_fst)
+
+
+(* show method (G, md) (mn, pTs) = Some (md, rT, pns, lvars, blk, res) *)
+apply (frule method_in_md [THEN conjunct2], assumption+)
+
+  (* show G\<turnstile>Class dynT \<preceq> Class md *)
+apply (simp (no_asm_use) only: widen_Class_Class)
+apply (rule method_wf_mdecl [THEN conjunct1], assumption+)
+
+  (* is_class G md *)
+apply (rule method_in_md [THEN conjunct1], assumption+)
+
+  (* show is_class G dynT *)
+apply (frule non_npD) apply assumption
+apply (erule exE)+ apply (erule conjE)+
+apply simp
+apply (rule subcls_is_class2) apply assumption
+apply (frule class_expr_is_class) apply (simp only: env_of_jmb_fst)
+apply (simp only: env_of_jmb_fst)
+
+ (* show G,h \<turnstile> a' ::\<preceq> Class C *)
+apply (simp only: wtpd_exprs_def, erule exE)
+apply (frule evals_preserves_conf)
+apply (rule eval_conf, assumption+)
+apply (rule env_of_jmb_fst, assumption+)
+apply (rule env_of_jmb_fst)
+apply (simp only: gh_conv)
+done
+
+
+theorem compiler_correctness_eval: "
+  \<lbrakk> G \<turnstile> (None,hp,loc) -ex \<succ> val-> (None,hp',loc');
+  wf_java_prog G;
+  class_sig_defined G C S;
+  wtpd_expr (env_of_jmb G C S) ex;
+  (None,hp,loc) ::\<preceq> (env_of_jmb G C S) \<rbrakk> \<Longrightarrow>
+  {(TranslComp.comp G), C, S} \<turnstile> 
+    {hp, os, (locvars_locals G C S loc)}
+      >- (compExpr (gmb G C S) ex) \<rightarrow> 
+    {hp', val#os, (locvars_locals G C S loc')}"
+apply (frule compiler_correctness [THEN conjunct1])
+apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def state_ok_def)
+done
+
+theorem compiler_correctness_exec: "
+  \<lbrakk> ((None,hp,loc), st, (None,hp',loc')) \<in> Eval.exec G;
+  wf_java_prog G;
+  class_sig_defined G C S;
+  wtpd_stmt (env_of_jmb G C S) st;
+  (None,hp,loc) ::\<preceq> (env_of_jmb G C S) \<rbrakk> \<Longrightarrow>
+  {(TranslComp.comp G), C, S} \<turnstile> 
+    {hp, os, (locvars_locals G C S loc)}
+      >- (compStmt (gmb G C S) st) \<rightarrow>
+    {hp', os, (locvars_locals G C S loc')}"
+apply (frule compiler_correctness [THEN conjunct2 [THEN conjunct2]])
+apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def state_ok_def)
+done
+
+(**********************************************************************)
+
+
+(* reinstall pair splits *)
+declare split_paired_All [simp] split_paired_Ex [simp]
+ML_setup {*
+simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
+*}
+
+end
diff -r b95d12325b51 -r 2950128b8206 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Oct 23 16:10:02 2002 +0200
@@ -0,0 +1,2676 @@
+(*  Title:      HOL/MicroJava/Comp/CorrCompTp.thy
+    ID:         $Id$
+    Author:     Martin Strecker
+    Copyright   GPL 2002
+*)
+
+theory CorrCompTp =  LemmasComp + JVM + TypeInf + NatCanonify + Altern:
+
+
+declare split_paired_All [simp del]
+declare split_paired_Ex [simp del]
+
+
+(**********************************************************************)
+
+constdefs     
+   inited_LT :: "[cname, ty list, (vname \<times> ty) list] \<Rightarrow> locvars_type"
+  "inited_LT C pTs lvars == (OK (Class C))#((map OK pTs))@(map (Fun.comp OK snd) lvars)"
+   is_inited_LT :: "[cname, ty list, (vname \<times> ty) list, locvars_type] \<Rightarrow> bool"
+  "is_inited_LT C pTs lvars LT == (LT = (inited_LT C pTs lvars))"
+
+  local_env :: "[java_mb prog, cname, sig, vname list,(vname \<times> ty) list] \<Rightarrow> java_mb env"
+  "local_env G C S pns lvars == 
+     let (mn, pTs) = S in (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C))"
+
+lemma local_env_fst [simp]: "fst (local_env G C S pns lvars) = G"
+by (simp add: local_env_def split_beta)
+
+
+lemma wt_class_expr_is_class: "\<lbrakk> wf_prog wf_mb G; E \<turnstile> expr :: Class cname;
+  E = local_env G C (mn, pTs) pns lvars\<rbrakk>
+  \<Longrightarrow> is_class G cname "
+apply (subgoal_tac "((fst E), (snd E)) \<turnstile> expr :: Class cname")
+apply (frule ty_expr_is_type) apply simp
+apply simp apply (simp (no_asm_use))
+done
+
+
+
+(********************************************************************************)
+(**** Stuff about index ****)
+
+lemma local_env_snd: "
+  snd (local_env G C (mn, pTs) pns lvars) = map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)"
+by (simp add: local_env_def)
+
+
+
+lemma index_in_bounds: " length pns = length pTs \<Longrightarrow>
+  snd (local_env G C (mn, pTs) pns lvars) vname = Some T
+       \<Longrightarrow> index (pns, lvars, blk, res) vname < length (inited_LT C pTs lvars)"
+apply (simp add: local_env_snd index_def split_beta)
+apply (case_tac "vname = This")
+apply (simp add: inited_LT_def)
+apply simp
+apply (drule map_of_upds_SomeD)
+apply (drule length_takeWhile)
+apply (simp add: inited_LT_def)
+done
+
+
+lemma map_upds_append [rule_format (no_asm)]: 
+  "\<forall> x1s m. (length k1s = length x1s 
+  \<longrightarrow> m(k1s[\<mapsto>]x1s)(k2s[\<mapsto>]x2s) = m ((k1s@k2s)[\<mapsto>](x1s@x2s)))"
+apply (induct k1s)
+apply simp
+apply (intro strip)
+apply (subgoal_tac "\<exists> x xr. x1s = x # xr")
+apply clarify
+apply simp
+  (* subgoal *)
+apply (case_tac x1s)
+apply auto
+done
+
+
+lemma map_of_append [rule_format]: 
+  "\<forall> ys. (map_of ((rev xs) @ ys) = (map_of ys) ((map fst xs) [\<mapsto>] (map snd xs)))"
+apply (induct xs)
+apply simp
+apply (rule allI)
+apply (drule_tac x="a # ys" in spec)
+apply (simp only: rev.simps append_assoc append_Cons append_Nil
+  map.simps map_of.simps map_upds.simps hd.simps tl.simps)
+done
+
+lemma map_of_as_map_upds: "map_of (rev xs) = empty ((map fst xs) [\<mapsto>] (map snd xs))"
+by (rule map_of_append [of _ "[]", simplified])
+
+lemma map_of_rev: "unique xs \<Longrightarrow> map_of (rev xs) = map_of xs"
+apply (induct xs)
+apply simp
+apply (simp add: unique_def map_of_append map_of_as_map_upds [THEN sym])
+done
+
+lemma map_upds_rev [rule_format]: "\<forall> xs. (distinct ks \<longrightarrow> length ks = length xs 
+  \<longrightarrow> m (rev ks [\<mapsto>] rev xs) = m (ks [\<mapsto>] xs))"
+apply (induct ks)
+apply simp
+apply (intro strip)
+apply (subgoal_tac "\<exists> x xr. xs = x # xr")
+apply clarify
+apply (drule_tac x=xr in spec)
+apply (simp add: map_upds_append [THEN sym])
+  (* subgoal *)
+apply (case_tac xs)
+apply auto
+done
+
+lemma map_upds_takeWhile [rule_format]:
+  "\<forall> ks. (empty(rev ks[\<mapsto>]rev xs)) k = Some x \<longrightarrow> length ks = length xs \<longrightarrow>
+    xs ! length (takeWhile (\<lambda>z. z \<noteq> k) ks) = x"
+apply (induct xs)
+apply simp
+apply (intro strip)
+apply (subgoal_tac "\<exists> k' kr. ks = k' # kr")
+apply (clarify)
+apply (drule_tac x=kr in spec)
+apply (simp only: rev.simps)
+apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev list @ [a])) = empty (rev kr[\<mapsto>]rev list)([k'][\<mapsto>][a])")
+apply (simp only:)
+apply (case_tac "k' = k")
+apply simp
+apply simp 
+apply (case_tac "k = k'")
+apply simp
+apply (simp add: empty_def)
+apply (simp add: map_upds_append [THEN sym])
+apply (case_tac ks)
+apply auto
+done
+
+
+lemma local_env_inited_LT: "\<lbrakk> snd (local_env G C (mn, pTs) pns lvars) vname = Some T;
+  length pns = length pTs; distinct pns; unique lvars \<rbrakk>
+  \<Longrightarrow> (inited_LT C pTs lvars ! index (pns, lvars, blk, res) vname) = OK T"
+apply (simp add: local_env_snd index_def)
+apply (case_tac "vname = This")
+apply (simp add: inited_LT_def)
+apply (simp add: inited_LT_def)
+apply (simp (no_asm_simp) only: map_compose map_append [THEN sym] map.simps [THEN sym])
+apply (subgoal_tac "length (takeWhile (\<lambda>z. z \<noteq> vname) (pns @ map fst lvars)) < length (pTs @ map snd lvars)")
+apply (simp (no_asm_simp) only: List.nth_map ok_val.simps)
+apply (subgoal_tac "map_of lvars = map_of (map (\<lambda> p. (fst p, snd p)) lvars)")
+apply (simp only:)
+apply (subgoal_tac "distinct (map fst lvars)") 
+apply (frule_tac g=snd in AuxLemmas.map_of_map_as_map_upd)
+apply (simp only:)
+apply (simp add: map_upds_append)
+apply (frule map_upds_SomeD)
+apply (rule map_upds_takeWhile)
+apply (simp (no_asm_simp))
+apply (simp add: map_upds_append [THEN sym])
+apply (simp add: map_upds_rev)
+
+  (* show length (pns @ map fst lvars) = length (pTs @ map snd lvars) *)
+apply simp
+
+  (* show distinct (map fst lvars) *)
+apply (simp only: unique_def Fun.comp_def)
+
+  (* show map_of lvars = map_of (map (\<lambda>p. (fst p, snd p)) lvars) *)
+apply simp
+
+  (* show length (takeWhile (\<lambda>z. z \<noteq> vname) (pns @ map fst lvars)) < length (pTs @ map snd lvars) *)
+apply (drule map_of_upds_SomeD)
+apply (drule length_takeWhile)
+apply simp
+done
+
+
+lemma inited_LT_at_index_no_err: " i < length (inited_LT C pTs lvars)
+  \<Longrightarrow> inited_LT C pTs lvars ! i \<noteq> Err"
+apply (simp only: inited_LT_def)
+apply (simp only: map_compose map_append [THEN sym] map.simps [THEN sym] length_map)
+apply (simp only: nth_map)
+apply simp
+done
+
+
+lemma sup_loc_update_index: "
+  \<lbrakk> G \<turnstile> T \<preceq> T'; is_type G T'; length pns = length pTs; distinct pns; unique lvars;
+  snd (local_env G C (mn, pTs) pns lvars) vname = Some T' \<rbrakk>
+  \<Longrightarrow> 
+  comp G \<turnstile> 
+  inited_LT C pTs lvars [index (pns, lvars, blk, res) vname := OK T] <=l 
+  inited_LT C pTs lvars"
+apply (subgoal_tac " index (pns, lvars, blk, res) vname < length (inited_LT C pTs lvars)")
+apply (frule_tac blk=blk and res=res in local_env_inited_LT, assumption+)
+apply (rule sup_loc_trans)
+apply (rule_tac b="OK T'" in sup_loc_update)
+apply (simp add: comp_widen) 
+apply assumption
+apply (rule sup_loc_refl)
+apply (simp add: list_update_same_conv [THEN iffD2])
+  (* subgoal *)
+apply (rule index_in_bounds)
+apply simp+
+done
+
+
+(********************************************************************************)
+
+(* Preservation of ST and LT by compTpExpr / compTpStmt *)
+
+lemma sttp_of_comb_nil [simp]: "sttp_of (comb_nil sttp) = sttp"
+by (simp add: comb_nil_def)
+
+lemma mt_of_comb_nil [simp]: "mt_of (comb_nil sttp) = []"
+by (simp add: comb_nil_def)
+
+
+lemma sttp_of_comb [simp]: "sttp_of ((f1 \<box> f2) sttp) = sttp_of (f2 (sttp_of (f1 sttp)))"
+apply (case_tac "f1 sttp")
+apply (case_tac "(f2 (sttp_of (f1 sttp)))")
+apply (simp add: comb_def)
+done
+
+lemma mt_of_comb: "(mt_of ((f1 \<box> f2) sttp)) = 
+  (mt_of (f1 sttp)) @ (mt_of (f2 (sttp_of (f1 sttp))))"
+by (simp add: comb_def split_beta)
+
+
+lemma mt_of_comb_length [simp]: "\<lbrakk> n1 = length (mt_of (f1 sttp)); n1 \<le> n \<rbrakk>
+  \<Longrightarrow> (mt_of ((f1 \<box> f2) sttp) ! n) = (mt_of (f2 (sttp_of (f1 sttp))) ! (n - n1))"
+by (simp add: comb_def nth_append split_beta)
+
+
+lemma compTpExpr_Exprs_LT_ST: "
+  \<lbrakk>jmb = (pns, lvars, blk, res); 
+  wf_prog wf_java_mdecl G;
+  wf_java_mdecl G C ((mn, pTs), rT, jmb);
+  E = local_env G C (mn, pTs) pns lvars \<rbrakk>
+ \<Longrightarrow> 
+  (\<forall> ST LT T. 
+  E \<turnstile> ex :: T \<longrightarrow>
+  is_inited_LT C pTs lvars LT \<longrightarrow>
+  sttp_of (compTpExpr jmb G ex (ST, LT)) = (T # ST, LT))
+ \<and>
+ (\<forall> ST LT Ts. 
+  E \<turnstile> exs [::] Ts \<longrightarrow>
+  is_inited_LT C pTs lvars LT \<longrightarrow>
+  sttp_of (compTpExprs jmb G exs (ST, LT)) = ((rev Ts) @ ST, LT))"
+
+apply (rule expr.induct)
+
+(* expresssions *)
+
+(* NewC *) 
+apply (intro strip)
+apply (drule NewC_invers)
+apply (simp add: pushST_def)
+
+(* Cast *)
+apply (intro strip)
+apply (drule Cast_invers, clarify)
+apply ((drule_tac x=ST in spec), (drule spec)+, (drule mp, assumption)+)
+apply (simp add: replST_def split_beta)
+
+(* Lit *)
+apply (intro strip)
+apply (drule Lit_invers)
+apply (simp add: pushST_def)
+
+(* BinOp *)
+apply (intro strip)
+apply (drule BinOp_invers, clarify)
+apply (drule_tac x=ST in spec)
+apply (drule_tac x="Ta # ST" in spec)
+apply ((drule spec)+, (drule mp, assumption)+)
+  apply (case_tac binop)
+  apply (simp (no_asm_simp))
+    apply (simp (no_asm_simp) add: popST_def pushST_def)
+  apply (simp)
+    apply (simp (no_asm_simp) add: replST_def)
+
+
+(* LAcc *)
+apply (intro strip)
+apply (drule LAcc_invers)
+apply (simp add: pushST_def is_inited_LT_def)
+apply (simp add: wf_prog_def)
+apply (frule wf_java_mdecl_disjoint_varnames) 
+  apply (simp add: disjoint_varnames_def)
+apply (frule wf_java_mdecl_length_pTs_pns)
+apply (erule conjE)+
+apply (simp (no_asm_simp) add: local_env_inited_LT)
+
+(* LAss *)
+apply (intro strip)
+apply (drule LAss_invers, clarify)
+apply (drule LAcc_invers)
+apply ((drule_tac x=ST in spec), (drule spec)+, (drule mp, assumption)+)
+apply (simp add: popST_def dupST_def)
+
+(* FAcc *)
+apply (intro strip)
+apply (drule FAcc_invers, clarify)
+apply ((drule_tac x=ST in spec), (drule spec)+, (drule mp, assumption)+)
+apply (simp add: replST_def)
+
+  (* show   snd (the (field (G, cname) vname)) = T *)
+  apply (subgoal_tac "is_class G Ca")
+  apply (subgoal_tac "is_class G cname \<and> field (G, cname) vname = Some (cname, T)")
+  apply simp
+
+  (* show is_class G cname \<and> field (G, cname) vname = Some (cname, T) *)
+  apply (rule field_in_fd) apply assumption+
+  (* show is_class G Ca *)
+  apply (rule wt_class_expr_is_class, assumption+, rule HOL.refl)
+
+(* FAss *)
+apply (intro strip)
+apply (drule FAss_invers, clarify)
+apply (drule FAcc_invers, clarify)
+apply (drule_tac x=ST in spec)
+apply (drule_tac x="Class Ca # ST" in spec)
+apply ((drule spec)+, (drule mp, assumption)+)
+apply (simp add: popST_def dup_x1ST_def)
+
+
+(* Call *)
+apply (intro strip)
+apply (drule Call_invers, clarify)
+apply (drule_tac x=ST in spec)
+apply (drule_tac x="Class cname # ST" in spec)
+apply ((drule spec)+, (drule mp, assumption)+)
+apply (simp add: replST_def)
+
+
+(* expression lists *)
+(* nil *) 
+
+apply (intro strip)
+apply (drule Nil_invers)
+apply (simp add: comb_nil_def)
+
+(* cons *)
+
+apply (intro strip)
+apply (drule Cons_invers, clarify)
+apply (drule_tac x=ST in spec)
+apply (drule_tac x="T # ST" in spec)
+apply ((drule spec)+, (drule mp, assumption)+)
+apply simp
+
+done
+
+
+
+lemmas compTpExpr_LT_ST [rule_format (no_asm)] = 
+  compTpExpr_Exprs_LT_ST [THEN conjunct1]
+
+lemmas compTpExprs_LT_ST [rule_format (no_asm)] = 
+  compTpExpr_Exprs_LT_ST [THEN conjunct2]
+
+lemma compTpStmt_LT_ST [rule_format (no_asm)]: "
+  \<lbrakk> jmb = (pns,lvars,blk,res); 
+  wf_prog wf_java_mdecl G;
+  wf_java_mdecl G C ((mn, pTs), rT, jmb);
+  E = (local_env G C (mn, pTs) pns lvars)\<rbrakk> 
+\<Longrightarrow> (\<forall> ST LT.
+  E \<turnstile> s\<surd> \<longrightarrow>
+  (is_inited_LT C pTs lvars LT)
+\<longrightarrow> sttp_of (compTpStmt jmb G s (ST, LT)) = (ST, LT))"
+
+apply (rule stmt.induct)
+
+(* Skip *) 
+apply (intro strip)
+apply simp
+
+(* Expr *)
+apply (intro strip)
+apply (drule Expr_invers, erule exE)
+apply (simp (no_asm_simp) add: compTpExpr_LT_ST)
+apply (frule_tac ST=ST in compTpExpr_LT_ST, assumption+)
+apply (simp add: popST_def)
+
+(* Comp *)
+apply (intro strip)
+apply (drule Comp_invers, clarify)
+apply (simp (no_asm_use))
+apply simp
+
+(* Cond *)
+apply (intro strip)
+apply (drule Cond_invers)
+apply (erule conjE)+
+apply (drule_tac x=ST in spec)
+apply (drule_tac x=ST in spec)
+apply (drule spec)+ apply (drule mp, assumption)+
+apply (drule_tac ST="PrimT Boolean # ST" in compTpExpr_LT_ST, assumption+)
+apply (simp add: popST_def pushST_def nochangeST_def)
+
+(* Loop *)
+apply (intro strip)
+apply (drule Loop_invers)
+apply (erule conjE)+
+apply (drule_tac x=ST in spec)
+apply (drule spec)+ apply (drule mp, assumption)+
+apply (drule_tac ST="PrimT Boolean # ST" in compTpExpr_LT_ST, assumption+)
+apply (simp add: popST_def pushST_def nochangeST_def)
+done
+
+
+
+lemma compTpInit_LT_ST: "
+  sttp_of (compTpInit jmb (vn,ty) (ST, LT)) = (ST, LT[(index jmb vn):= OK ty])"
+by (simp add: compTpInit_def storeST_def pushST_def)
+
+
+lemma compTpInitLvars_LT_ST_aux [rule_format (no_asm)]:
+  "\<forall> pre lvars_pre lvars0.
+  jmb = (pns,lvars0,blk,res) \<and>
+  lvars0 = (lvars_pre @ lvars) \<and>
+  (length pns) + (length lvars_pre) + 1 = length pre \<and>
+  disjoint_varnames pns (lvars_pre @ lvars)
+  \<longrightarrow>
+sttp_of (compTpInitLvars jmb lvars (ST, pre @ replicate (length lvars) Err))
+    = (ST, pre @ map (Fun.comp OK snd) lvars)"
+apply (induct lvars)
+apply simp
+
+apply (intro strip)
+apply (subgoal_tac "\<exists> vn ty. a = (vn, ty)")
+  prefer 2 apply (simp (no_asm_simp)) 
+  apply ((erule exE)+, simp (no_asm_simp))
+
+apply (drule_tac x="pre @ [OK ty]" in spec)
+apply (drule_tac x="lvars_pre @ [a]" in spec)
+apply (drule_tac x="lvars0" in spec)
+apply (simp add: compTpInit_LT_ST index_of_var2)
+done
+
+lemma compTpInitLvars_LT_ST: 
+  "\<lbrakk> jmb = (pns, lvars, blk, res); wf_java_mdecl G C ((mn, pTs), rT, jmb) \<rbrakk>
+\<Longrightarrow>(sttp_of (compTpInitLvars jmb lvars (ST, start_LT C pTs (length lvars))))
+  = (ST, inited_LT C pTs lvars)"
+apply (simp add: start_LT_def inited_LT_def)
+apply (simp only: append_Cons [THEN sym])
+apply (rule compTpInitLvars_LT_ST_aux)
+apply (auto dest: wf_java_mdecl_length_pTs_pns wf_java_mdecl_disjoint_varnames)
+done
+
+
+
+(********************************************************************************)
+
+lemma max_of_list_elem: "x \<in> set xs \<Longrightarrow> x \<le> (max_of_list xs)"
+by (induct xs, auto intro: le_maxI1 simp: le_max_iff_disj max_of_list_def)
+
+lemma max_of_list_sublist: "set xs \<subseteq> set ys 
+  \<Longrightarrow> (max_of_list xs) \<le> (max_of_list ys)"
+by (induct xs, auto dest: max_of_list_elem simp: max_of_list_def)
+
+lemma max_of_list_append [simp]:
+  "max_of_list (xs @ ys) = max (max_of_list xs) (max_of_list ys)" 
+apply (simp add: max_of_list_def)
+apply (induct xs)
+apply simp
+apply simp
+apply arith
+done
+
+
+lemma app_mono_mxs: "\<lbrakk> app i G mxs rT pc et s; mxs \<le> mxs' \<rbrakk> 
+  \<Longrightarrow> app i G mxs' rT pc et s"
+apply (case_tac s)
+apply (simp add: app_def)
+apply (case_tac i)
+apply (auto intro: less_trans)
+done
+
+
+
+lemma err_mono [simp]: "A \<subseteq> B \<Longrightarrow> err A \<subseteq> err B"
+by (auto simp: err_def)
+
+lemma opt_mono [simp]: "A \<subseteq> B \<Longrightarrow> opt A \<subseteq> opt B"
+by (auto simp: opt_def)
+
+
+lemma states_mono: "\<lbrakk> mxs \<le> mxs' \<rbrakk>
+  \<Longrightarrow> states G mxs mxr \<subseteq> states G mxs' mxr"
+apply (simp add: states_def JVMType.sl_def)
+apply (simp add: Product.esl_def stk_esl_def reg_sl_def upto_esl_def Listn.sl_def Err.sl_def
+  JType.esl_def)
+apply (simp add: Err.esl_def Err.le_def Listn.le_def)
+apply (simp add: Product.le_def Product.sup_def Err.sup_def)
+apply (simp add: Opt.esl_def Listn.sup_def)
+apply (rule err_mono)
+apply (rule opt_mono)
+apply (rule Sigma_mono)
+apply (rule Union_mono)
+apply auto 
+done
+
+
+lemma check_type_mono: "\<lbrakk> check_type G mxs mxr s; mxs \<le> mxs' \<rbrakk> 
+  \<Longrightarrow> check_type G mxs' mxr s"
+apply (simp add: check_type_def)
+apply (frule_tac G=G and mxr=mxr in states_mono)
+apply auto
+done
+
+
+  (* wt is preserved when adding instructions/state-types at the end *)
+lemma wt_instr_prefix: "
+ \<lbrakk> wt_instr_altern (bc ! pc) cG rT mt mxs mxr max_pc et pc; 
+  bc' = bc @ bc_post; mt' = mt @ mt_post; 
+  mxs \<le> mxs'; max_pc \<le> max_pc'; 
+  pc < length bc; pc < length mt; 
+  max_pc = (length mt)\<rbrakk>
+\<Longrightarrow> wt_instr_altern (bc' ! pc) cG rT mt' mxs' mxr max_pc' et pc"
+apply (simp add: wt_instr_altern_def nth_append)
+apply (auto intro: app_mono_mxs check_type_mono)
+done
+
+
+(************************************************************************)
+
+
+
+lemma pc_succs_shift: "pc'\<in>set (succs i (pc'' + n))
+ \<Longrightarrow> ((pc' - n) \<in>set (succs i pc''))"
+apply (induct i)
+apply simp+
+  (* case Goto *)
+apply (simp only: nat_canonify)
+apply simp
+  (* case Ifcmpeq *)
+apply simp
+apply (erule disjE)
+apply simp
+apply (simp only: nat_canonify)
+apply simp
+  (* case Throw *)
+apply simp
+done
+
+
+lemma pc_succs_le: "\<lbrakk> pc' \<in> set (succs i (pc'' + n));   
+  \<forall> b. ((i = (Goto b) \<or> i=(Ifcmpeq b)) \<longrightarrow> 0 \<le> (int pc'' + b)) \<rbrakk> 
+  \<Longrightarrow> n \<le> pc'"
+apply (induct i)
+apply simp+
+  (* case Goto *)
+apply (simp only: nat_canonify)
+apply simp
+  (* case Ifcmpeq *)
+apply simp
+apply (erule disjE)
+apply simp
+apply (simp only: nat_canonify)
+apply simp
+  (* case Throw *)
+apply simp
+done
+
+
+(**********************************************************************)
+
+constdefs
+  offset_xcentry :: "[nat, exception_entry] \<Rightarrow> exception_entry"
+  "offset_xcentry == 
+      \<lambda> n (start_pc, end_pc, handler_pc, catch_type).
+          (start_pc + n, end_pc + n, handler_pc + n, catch_type)"
+
+  offset_xctable :: "[nat, exception_table] \<Rightarrow> exception_table"
+  "offset_xctable n == (map (offset_xcentry n))"
+
+lemma match_xcentry_offset [simp]: "
+  match_exception_entry G cn (pc + n) (offset_xcentry n ee) = 
+  match_exception_entry G cn pc ee"
+by (simp add: match_exception_entry_def offset_xcentry_def split_beta)
+
+lemma match_xctable_offset: "
+  (match_exception_table G cn (pc + n) (offset_xctable n et)) =
+  (option_map (\<lambda> pc'. pc' + n) (match_exception_table G cn pc et))"
+apply (induct et)
+apply (simp add: offset_xctable_def)+
+apply (case_tac "match_exception_entry G cn pc a")
+apply (simp add: offset_xcentry_def split_beta)+
+done
+
+
+lemma match_offset [simp]: "
+  match G cn (pc + n) (offset_xctable n et) = match G cn pc et"
+apply (induct et)
+apply (simp add: offset_xctable_def)+
+done
+
+lemma match_any_offset [simp]: "
+  match_any G (pc + n) (offset_xctable n et) = match_any G pc et"
+apply (induct et)
+apply (simp add: offset_xctable_def offset_xcentry_def split_beta)+
+done
+
+lemma app_mono_pc: "\<lbrakk> app i G mxs rT pc et s; pc'= pc + n \<rbrakk> 
+  \<Longrightarrow> app i G mxs rT pc' (offset_xctable n et) s"
+apply (case_tac s)
+apply (simp add: app_def)
+apply (case_tac i)
+apply (auto)
+done
+
+(**********************************************************************)
+
+  (* Currently: empty exception_table *)
+
+syntax
+  empty_et :: exception_table
+translations
+  "empty_et" => "[]"
+
+
+
+  (* move into Effect.thy *)
+lemma xcpt_names_Nil [simp]: "(xcpt_names (i, G, pc, [])) = []"
+by (induct i, simp_all)
+
+lemma xcpt_eff_Nil [simp]: "(xcpt_eff i G pc s []) = []"
+by (simp add: xcpt_eff_def)
+
+
+lemma app_jumps_lem: "\<lbrakk> app i cG mxs rT pc empty_et s; s=(Some st) \<rbrakk>
+  \<Longrightarrow>  \<forall> b. ((i = (Goto b) \<or> i=(Ifcmpeq b)) \<longrightarrow> 0 \<le> (int pc + b))"
+apply (simp only:)
+apply (induct i)
+apply auto
+done
+
+
+(* wt is preserved when adding instructions/state-types to the front *)
+lemma wt_instr_offset: "
+ \<lbrakk> \<forall> pc'' < length mt. 
+    wt_instr_altern ((bc@bc_post) ! pc'') cG rT (mt@mt_post) mxs mxr max_pc empty_et pc''; 
+  bc' = bc_pre @ bc @ bc_post; mt' = mt_pre @ mt @ mt_post; 
+  length bc_pre = length mt_pre; length bc = length mt;
+  length mt_pre \<le> pc; pc < length (mt_pre @ mt); 
+  mxs \<le> mxs'; max_pc + length mt_pre \<le> max_pc' \<rbrakk>
+\<Longrightarrow> wt_instr_altern (bc' ! pc) cG rT mt' mxs' mxr max_pc' empty_et pc"
+
+apply (simp add: wt_instr_altern_def)
+apply (subgoal_tac "\<exists> pc''. pc = pc'' + length mt_pre", erule exE)
+prefer 2 apply (rule_tac x="pc - length mt_pre" in exI, arith)
+
+apply (drule_tac x=pc'' in spec)
+apply (drule mp) apply arith	(* show pc'' < length mt *)
+apply clarify
+
+apply (rule conjI)
+  (* app *)
+  apply (simp add: nth_append)
+  apply (rule app_mono_mxs)
+  apply (frule app_mono_pc) apply (rule HOL.refl) apply (simp add: offset_xctable_def)
+  apply assumption+
+
+  (* check_type *)
+apply (rule conjI)
+apply (simp add: nth_append)
+apply (rule  check_type_mono) apply assumption+
+
+  (* ..eff.. *)
+apply (intro ballI)
+apply (subgoal_tac "\<exists> pc' s'. x = (pc', s')", (erule exE)+, simp)
+
+apply (case_tac s')
+  (* s' = None *)
+apply (simp add: eff_def nth_append norm_eff_def)
+apply (frule_tac x="(pc', None)" and  f=fst and b=pc' in rev_image_eqI) 
+  apply (simp (no_asm_simp))
+  apply (simp only: fst_conv image_compose [THEN sym] Fun.comp_def)
+  apply simp
+  apply (frule pc_succs_shift)
+apply (drule bspec, assumption)
+apply arith
+
+  (* s' = Some a *)
+apply (drule_tac x="(pc' - length mt_pre, s')" in bspec)
+
+  (* show  (pc' - length mt_pre, s') \<in> set (eff \<dots>) *)
+apply (simp add: eff_def)
+    (* norm_eff *)
+  apply (clarsimp simp: nth_append pc_succs_shift)
+
+  (* show P x of bspec *)
+apply simp
+  apply (subgoal_tac "length mt_pre \<le> pc'")
+  apply (simp add: nth_append) apply arith
+
+  (* subgoals *)
+apply (simp add: eff_def xcpt_eff_def)
+apply (clarsimp)
+apply (rule pc_succs_le) apply assumption+
+apply (subgoal_tac "\<exists> st. mt ! pc'' = Some st", erule exE)
+ apply (rule_tac s="Some st" and st=st and cG=cG and mxs=mxs and rT=rT
+        in app_jumps_lem)
+  apply (simp add: nth_append)+
+    (* subgoal \<exists> st. mt ! pc'' = Some st *)
+  apply (simp add: norm_eff_def option_map_def nth_append)
+  apply (case_tac "mt ! pc''")
+apply simp+
+done
+
+
+(**********************************************************************)
+
+
+constdefs
+  start_sttp_resp_cons :: "[state_type \<Rightarrow> method_type \<times> state_type] \<Rightarrow> bool"
+  "start_sttp_resp_cons f == 
+     (\<forall> sttp. let (mt', sttp') = (f sttp) in (\<exists>mt'_rest. mt' = Some sttp # mt'_rest))"
+
+  start_sttp_resp :: "[state_type \<Rightarrow> method_type \<times> state_type] \<Rightarrow> bool"
+  "start_sttp_resp f == (f = comb_nil) \<or> (start_sttp_resp_cons f)"
+
+lemma start_sttp_resp_comb_nil [simp]: "start_sttp_resp comb_nil"
+by (simp add: start_sttp_resp_def)
+
+lemma start_sttp_resp_cons_comb_cons [simp]: "start_sttp_resp_cons f 
+  \<Longrightarrow> start_sttp_resp_cons (f \<box> f')"
+apply (simp add: start_sttp_resp_cons_def comb_def split_beta)
+apply (rule allI)
+apply (drule_tac x=sttp in spec)
+apply auto
+done
+
+lemma start_sttp_resp_cons_comb_cons_r: "\<lbrakk> start_sttp_resp f; start_sttp_resp_cons f'\<rbrakk>
+  \<Longrightarrow> start_sttp_resp_cons (f \<box> f')"
+apply (simp add: start_sttp_resp_def)
+apply (erule disjE)
+apply simp+
+done
+
+lemma start_sttp_resp_cons_comb [simp]: "start_sttp_resp_cons f 
+  \<Longrightarrow> start_sttp_resp (f \<box> f')"
+by (simp add: start_sttp_resp_def)
+
+lemma start_sttp_resp_comb: "\<lbrakk> start_sttp_resp f; start_sttp_resp f' \<rbrakk>
+  \<Longrightarrow> start_sttp_resp (f \<box> f')"
+apply (simp add: start_sttp_resp_def)
+apply (erule disjE)
+apply simp
+apply (erule disjE)
+apply simp+
+done
+
+lemma start_sttp_resp_cons_nochangeST [simp]: "start_sttp_resp_cons nochangeST"
+by (simp add: start_sttp_resp_cons_def nochangeST_def)
+
+lemma start_sttp_resp_cons_pushST [simp]: "start_sttp_resp_cons (pushST Ts)"
+by (simp add: start_sttp_resp_cons_def pushST_def split_beta)
+
+lemma start_sttp_resp_cons_dupST [simp]: "start_sttp_resp_cons dupST"
+by (simp add: start_sttp_resp_cons_def dupST_def split_beta)
+
+lemma start_sttp_resp_cons_dup_x1ST [simp]: "start_sttp_resp_cons dup_x1ST"
+by (simp add: start_sttp_resp_cons_def dup_x1ST_def split_beta)
+
+lemma start_sttp_resp_cons_popST [simp]: "start_sttp_resp_cons (popST n)"
+by (simp add: start_sttp_resp_cons_def popST_def split_beta)
+
+lemma start_sttp_resp_cons_replST [simp]: "start_sttp_resp_cons (replST n tp)"
+by (simp add: start_sttp_resp_cons_def replST_def split_beta)
+
+lemma start_sttp_resp_cons_storeST [simp]: "start_sttp_resp_cons (storeST i tp)"
+by (simp add: start_sttp_resp_cons_def storeST_def split_beta)
+
+lemma start_sttp_resp_cons_compTpExpr [simp]: "start_sttp_resp_cons (compTpExpr jmb G ex)"
+apply (induct ex)
+apply simp+
+apply (simp add: start_sttp_resp_cons_def comb_def pushST_def split_beta) (* LAcc *)
+apply simp+
+done
+
+lemma start_sttp_resp_cons_compTpInit [simp]: "start_sttp_resp_cons (compTpInit jmb lv)"
+by (simp add: compTpInit_def split_beta)
+
+
+lemma start_sttp_resp_nochangeST [simp]: "start_sttp_resp nochangeST"
+by (simp add: start_sttp_resp_def)
+
+lemma start_sttp_resp_pushST [simp]: "start_sttp_resp (pushST Ts)"
+by (simp add: start_sttp_resp_def)
+
+lemma start_sttp_resp_dupST [simp]: "start_sttp_resp dupST"
+by (simp add: start_sttp_resp_def)
+
+lemma start_sttp_resp_dup_x1ST [simp]: "start_sttp_resp dup_x1ST"
+by (simp add: start_sttp_resp_def)
+
+lemma start_sttp_resp_popST [simp]: "start_sttp_resp (popST n)"
+by (simp add: start_sttp_resp_def)
+
+lemma start_sttp_resp_replST [simp]: "start_sttp_resp (replST n tp)"
+by (simp add: start_sttp_resp_def)
+
+lemma start_sttp_resp_storeST [simp]: "start_sttp_resp (storeST i tp)"
+by (simp add: start_sttp_resp_def)
+
+lemma start_sttp_resp_compTpExpr [simp]: "start_sttp_resp (compTpExpr jmb G ex)"
+by (simp add: start_sttp_resp_def)
+
+lemma start_sttp_resp_compTpExprs [simp]: "start_sttp_resp (compTpExprs jmb G exs)"
+by (induct exs, (simp add: start_sttp_resp_comb)+)
+
+lemma start_sttp_resp_compTpStmt [simp]: "start_sttp_resp (compTpStmt jmb G s)"
+by (induct s, (simp add: start_sttp_resp_comb)+)
+
+lemma start_sttp_resp_compTpInitLvars [simp]: "start_sttp_resp (compTpInitLvars jmb lvars)"
+by (induct lvars, simp+)
+
+
+
+
+  (* ********************************************************************** *)
+  (* length of compExpr/ compTpExprs *)
+  (* ********************************************************************** *)
+
+lemma length_comb [simp]:  "length (mt_of ((f1 \<box> f2) sttp)) = 
+  length (mt_of (f1 sttp)) + length (mt_of (f2 (sttp_of (f1 sttp))))"
+by (simp add: comb_def split_beta)
+
+
+lemma length_comb_nil [simp]: "length (mt_of (comb_nil sttp)) = 0"
+by (simp add: comb_nil_def)
+
+lemma length_nochangeST [simp]: "length (mt_of (nochangeST sttp)) = 1"
+by (simp add: nochangeST_def)
+
+lemma length_pushST [simp]: "length (mt_of (pushST Ts sttp)) = 1"
+by (simp add: pushST_def split_beta)
+
+lemma length_dupST [simp]: "length (mt_of (dupST sttp)) = 1"
+by (simp add: dupST_def split_beta)
+
+lemma length_dup_x1ST [simp]: "length (mt_of (dup_x1ST sttp)) = 1"
+by (simp add: dup_x1ST_def split_beta)
+
+lemma length_popST [simp]: "length (mt_of (popST n sttp)) = 1"
+by (simp add: popST_def split_beta)
+
+lemma length_replST [simp]: "length (mt_of (replST n tp sttp)) = 1"
+by (simp add: replST_def split_beta)
+
+lemma length_storeST [simp]: "length (mt_of (storeST i tp sttp)) = 1"
+by (simp add: storeST_def split_beta)
+
+
+lemma length_compTpExpr_Exprs [rule_format]: "
+  (\<forall> sttp. (length (mt_of (compTpExpr jmb G ex sttp)) = length (compExpr jmb ex)))
+  \<and> (\<forall> sttp. (length (mt_of (compTpExprs jmb G exs sttp)) = length (compExprs jmb exs)))"
+apply (rule  expr.induct)
+apply simp+
+apply (case_tac binop)
+apply simp+
+apply (simp add: pushST_def split_beta)
+apply simp+
+done
+
+lemma length_compTpExpr: "length (mt_of (compTpExpr jmb G ex sttp)) = length (compExpr jmb ex)"
+by (rule length_compTpExpr_Exprs [THEN conjunct1 [THEN spec]])
+
+lemma length_compTpExprs: "length (mt_of (compTpExprs jmb G exs sttp)) = length (compExprs jmb exs)"
+by (rule length_compTpExpr_Exprs [THEN conjunct2 [THEN spec]])
+
+lemma length_compTpStmt [rule_format]: "
+  (\<forall> sttp. (length (mt_of (compTpStmt jmb G s sttp)) = length (compStmt jmb s)))"
+apply (rule stmt.induct)
+apply (simp add: length_compTpExpr)+
+done
+
+
+lemma length_compTpInit: "length (mt_of (compTpInit jmb lv sttp)) = length (compInit jmb lv)"
+by (simp add: compTpInit_def compInit_def split_beta)
+
+lemma length_compTpInitLvars [rule_format]: 
+  "\<forall> sttp. length (mt_of (compTpInitLvars jmb lvars sttp)) = length (compInitLvars jmb lvars)"
+by (induct lvars,  (simp add: compInitLvars_def length_compTpInit split_beta)+)
+
+
+  (* ********************************************************************** *)
+  (* Correspondence bytecode - method types *)
+  (* ********************************************************************** *)
+
+syntax
+  ST_of :: "state_type \<Rightarrow> opstack_type"
+  LT_of :: "state_type \<Rightarrow> locvars_type"
+translations
+  "ST_of" => "fst"
+  "LT_of" => "snd"
+
+lemma states_lower:
+  "\<lbrakk> OK (Some (ST, LT)) \<in> states cG mxs mxr; length ST \<le> mxs\<rbrakk>
+  \<Longrightarrow> OK (Some (ST, LT)) \<in> states cG (length ST) mxr"
+apply (simp add: states_def JVMType.sl_def)
+apply (simp add: Product.esl_def stk_esl_def reg_sl_def upto_esl_def Listn.sl_def Err.sl_def
+  JType.esl_def)
+apply (simp add: Err.esl_def Err.le_def Listn.le_def)
+apply (simp add: Product.le_def Product.sup_def Err.sup_def)
+apply (simp add: Opt.esl_def Listn.sup_def)
+apply clarify
+apply auto
+done
+
+lemma check_type_lower:
+  "\<lbrakk> check_type cG mxs mxr (OK (Some (ST, LT))); length ST \<le> mxs\<rbrakk>
+  \<Longrightarrow>check_type cG (length ST) mxr (OK (Some (ST, LT)))"
+by (simp add: check_type_def states_lower)
+
+lemma max_same_iter [simp]: "max (x::'a::linorder) (max x y) = max x y"
+by (simp del: max_assoc add: max_assoc [THEN sym])
+
+  (* ******************************************************************* *)
+
+constdefs
+   bc_mt_corresp :: "
+  [bytecode, state_type \<Rightarrow> method_type \<times> state_type, state_type, jvm_prog, ty, nat, p_count]
+  \<Rightarrow> bool"
+
+  "bc_mt_corresp bc f sttp0 cG rT mxr idx ==
+  let (mt, sttp) = f sttp0 in
+  (length bc = length mt \<and> 
+    ((check_type cG (length (ST_of sttp0)) mxr (OK (Some sttp0))) \<longrightarrow>
+    (\<forall>  mxs. 
+     mxs = max_ssize (mt@[Some sttp]) \<longrightarrow>
+     (\<forall> pc. pc < idx \<longrightarrow> 
+      wt_instr_altern (bc ! pc) cG rT (mt@[Some sttp]) mxs mxr (length mt + 1) empty_et pc)
+     \<and> 
+     check_type cG mxs mxr (OK ((mt@[Some sttp]) ! idx)))))"
+
+
+lemma bc_mt_corresp_comb: "
+  \<lbrakk> bc' = (bc1@bc2); l' = (length bc');
+  bc_mt_corresp bc1 f1 sttp0 cG rT mxr (length bc1);
+  bc_mt_corresp bc2 f2 (sttp_of (f1 sttp0)) cG rT mxr (length bc2);
+  start_sttp_resp f2\<rbrakk>
+\<Longrightarrow> bc_mt_corresp bc' (f1 \<box> f2) sttp0 cG rT mxr l'"
+apply (subgoal_tac "\<exists> mt1 sttp1. (f1 sttp0) = (mt1, sttp1)", (erule exE)+)
+apply (subgoal_tac "\<exists> mt2 sttp2. (f2 sttp1) = (mt2, sttp2)", (erule exE)+)
+
+  (* unfold start_sttp_resp and make case distinction *)
+apply (simp only: start_sttp_resp_def)
+apply (erule disjE)
+  (* case f2 = comb_nil *)
+apply (simp add: bc_mt_corresp_def comb_nil_def start_sttp_resp_cons_def)
+apply (erule conjE)+
+apply (intro strip)
+apply simp
+
+  (* case start_sttp_resp_cons f2 *)
+apply (simp add: bc_mt_corresp_def comb_def start_sttp_resp_cons_def del: all_simps)
+apply (intro strip)
+apply (erule conjE)+
+apply (drule mp, assumption)
+apply (subgoal_tac "check_type cG (length (fst sttp1)) mxr (OK (Some sttp1))")
+apply (erule conjE)+
+apply (drule mp, assumption)
+apply (erule conjE)+
+
+apply (rule conjI)
+  (* show wt_instr  \<dots> *)
+
+apply (drule_tac x=sttp1 in spec, simp)
+apply (erule exE)
+apply (intro strip)
+apply (case_tac "pc < length mt1")
+
+  (* case pc < length mt1 *)
+apply (drule spec, drule mp, simp)
+apply simp 
+apply (rule_tac mt="mt1 @ [Some sttp1]" in wt_instr_prefix)
+  apply assumption+ apply (rule HOL.refl)
+  apply (simp (no_asm_simp))
+  apply (simp (no_asm_simp) add: max_ssize_def)
+  apply (simp add: max_of_list_def max_ac)
+  apply arith
+  apply (simp (no_asm_simp))+
+
+  (* case pc \<ge> length mt1 *)
+apply (rule_tac bc=bc2 and mt=mt2 and bc_post="[]" and mt_post="[Some sttp2]" 
+  and mxr=mxr 
+  in wt_instr_offset)
+apply simp
+apply (simp (no_asm_simp))+
+apply simp
+apply (simp add: max_ssize_def max_of_list_append) apply (simp (no_asm_simp) add: max_def)
+apply (simp (no_asm_simp))+
+
+  (* show check_type \<dots> *)
+apply (subgoal_tac "((mt2 @ [Some sttp2]) ! length bc2) = Some sttp2")
+apply (simp only:)
+apply (rule check_type_mono) apply assumption
+apply (simp (no_asm_simp)  add: max_ssize_def max_of_list_append max_ac)
+apply arith
+apply (simp add: nth_append)
+
+apply (erule conjE)+
+apply (case_tac sttp1)
+apply (simp add: check_type_def)
+apply (rule states_lower, assumption)
+apply (simp (no_asm_simp) add: max_ssize_def max_of_list_append)
+apply (simp (no_asm_simp) add: max_of_list_def ssize_sto_def max_def)
+apply (simp (no_asm_simp))+
+done
+
+
+lemma bc_mt_corresp_zero [simp]: "\<lbrakk> length (mt_of (f sttp)) = length bc; start_sttp_resp f\<rbrakk>
+  \<Longrightarrow> bc_mt_corresp bc f sttp cG rT mxr 0"
+apply (simp add: bc_mt_corresp_def start_sttp_resp_def split_beta)
+apply (erule disjE)
+apply (simp add: max_ssize_def max_of_list_def ssize_sto_def split_beta)
+apply (intro strip)
+apply (simp add: start_sttp_resp_cons_def split_beta)
+apply (drule_tac x=sttp in spec, erule exE)
+apply simp
+apply (rule check_type_mono, assumption)
+apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def split_beta)
+done
+
+  (* ********************************************************************** *)
+
+
+constdefs
+  mt_sttp_flatten :: "method_type \<times> state_type \<Rightarrow> method_type"
+  "mt_sttp_flatten mt_sttp == (mt_of mt_sttp) @ [Some (sttp_of mt_sttp)]"
+
+
+lemma mt_sttp_flatten_length [simp]: "n = (length (mt_of (f sttp)))
+ \<Longrightarrow> (mt_sttp_flatten (f sttp)) ! n = Some (sttp_of (f sttp))"
+by (simp add: mt_sttp_flatten_def)
+
+lemma mt_sttp_flatten_comb: "(mt_sttp_flatten ((f1 \<box> f2) sttp)) = 
+  (mt_of (f1 sttp)) @ (mt_sttp_flatten (f2 (sttp_of (f1 sttp))))"
+by (simp add: mt_sttp_flatten_def comb_def split_beta)
+
+lemma mt_sttp_flatten_comb_length [simp]: "\<lbrakk> n1 = length (mt_of (f1 sttp)); n1 \<le> n \<rbrakk>
+  \<Longrightarrow> (mt_sttp_flatten ((f1 \<box> f2) sttp) ! n) = (mt_sttp_flatten (f2 (sttp_of (f1 sttp))) ! (n - n1))"
+by (simp add: mt_sttp_flatten_comb nth_append)
+
+lemma mt_sttp_flatten_comb_zero [simp]: "start_sttp_resp f 
+  \<Longrightarrow> (mt_sttp_flatten (f sttp)) ! 0 = Some sttp"
+apply (simp only: start_sttp_resp_def)
+apply (erule disjE)
+apply (simp add: comb_nil_def mt_sttp_flatten_def)
+apply (simp add: start_sttp_resp_cons_def mt_sttp_flatten_def split_beta)
+apply (drule_tac x=sttp in spec)
+apply (erule exE)
+apply simp
+done
+
+
+(* move into prelude -- compare with nat_int_length *)
+lemma int_outside_right: "0 \<le> (m::int) \<Longrightarrow> m + (int n) = int ((nat m) + n)"
+by simp
+
+lemma int_outside_left: "0 \<le> (m::int) \<Longrightarrow> (int n) + m = int (n + (nat m))"
+by simp
+
+
+
+
+  (* ********************************************************************** *)
+  (* bc_mt_corresp for individual instructions                              *)
+  (* ---------------------------------------------------------------------- *)
+
+lemma less_Suc [simp] : "n \<le> k \<Longrightarrow> (k < Suc n) = (k = n)"
+  by arith
+
+lemmas check_type_simps = check_type_def states_def JVMType.sl_def
+   Product.esl_def stk_esl_def reg_sl_def upto_esl_def Listn.sl_def Err.sl_def
+  JType.esl_def Err.esl_def Err.le_def Listn.le_def Product.le_def Product.sup_def Err.sup_def
+  Opt.esl_def Listn.sup_def
+
+
+lemma check_type_push: "\<lbrakk> 
+  is_class cG cname; check_type cG (length ST) mxr (OK (Some (ST, LT))) \<rbrakk>
+  \<Longrightarrow> check_type cG (Suc (length ST)) mxr (OK (Some (Class cname # ST, LT)))"
+apply (simp add: check_type_simps)
+apply clarify
+apply (rule_tac x="Suc (length ST)" in exI)
+apply simp+
+done
+
+lemma bc_mt_corresp_New: "\<lbrakk>is_class cG cname \<rbrakk>
+  \<Longrightarrow> bc_mt_corresp [New cname] (pushST [Class cname]) (ST, LT) cG rT mxr (Suc 0)"
+apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
+    max_ssize_def max_of_list_def ssize_sto_def max_def 
+    eff_def norm_eff_def)
+apply (intro strip)
+apply (rule conjI)
+apply (rule check_type_mono, assumption, simp)
+apply (simp add: check_type_push)
+done
+
+lemma bc_mt_corresp_Pop: "
+  bc_mt_corresp [Pop] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
+  apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
+  apply (simp add: max_ssize_def ssize_sto_def max_of_list_def) 
+  apply (simp add: max_def)
+  apply (simp add: check_type_simps)
+  apply clarify
+  apply (rule_tac x="(length ST)" in exI)
+  apply simp+
+  done
+
+lemma bc_mt_corresp_Checkcast: "\<lbrakk> is_class cG cname; sttp = (ST, LT); 
+  (\<exists>rT STo. ST = RefT rT # STo) \<rbrakk>
+  \<Longrightarrow> bc_mt_corresp [Checkcast cname] (replST (Suc 0) (Class cname)) sttp cG rT mxr (Suc 0)"
+  apply (erule exE)+
+  apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
+  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def)
+  apply (simp add: check_type_simps)
+  apply clarify
+  apply (rule_tac x="Suc (length STo)" in exI)
+  apply simp+
+  done
+
+
+lemma bc_mt_corresp_LitPush: "\<lbrakk> typeof (\<lambda>v. None) val = Some T \<rbrakk>
+  \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T]) sttp cG rT mxr (Suc 0)"
+apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
+  apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
+                 max_ssize_def max_of_list_def ssize_sto_def max_def
+                 eff_def norm_eff_def)
+  apply (intro strip)
+  apply (rule conjI)
+  apply (rule check_type_mono, assumption, simp)
+  apply (simp add: check_type_simps)
+apply clarify
+apply (rule_tac x="Suc (length ST)" in exI)
+apply simp
+apply (drule sym)
+apply (case_tac val)
+apply simp+
+done
+
+
+lemma bc_mt_corresp_LitPush_CT: "\<lbrakk> typeof (\<lambda>v. None) val = Some T \<and> cG \<turnstile> T \<preceq> T';
+  is_type cG T' \<rbrakk>
+  \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T']) sttp cG rT mxr (Suc 0)"
+apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
+  apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
+                 max_ssize_def max_of_list_def ssize_sto_def max_def
+                 eff_def norm_eff_def)
+  apply (intro strip)
+  apply (rule conjI)
+  apply (rule check_type_mono, assumption, simp)
+  apply (simp add: check_type_simps)
+  apply (simp add: sup_state_Cons)
+apply clarify
+apply (rule_tac x="Suc (length ST)" in exI)
+apply simp
+apply simp+
+done
+
+lemma bc_mt_corresp_Load: "\<lbrakk> i < length LT; LT ! i \<noteq> Err; mxr = length LT \<rbrakk>
+  \<Longrightarrow> bc_mt_corresp [Load i] 
+         (\<lambda>(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)"
+apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
+                 max_ssize_def max_of_list_def ssize_sto_def max_def
+                 eff_def norm_eff_def)
+  apply (intro strip)
+  apply (rule conjI)
+  apply (rule check_type_mono, assumption, simp)
+apply (simp add: check_type_simps)
+apply clarify
+apply (rule_tac x="Suc (length ST)" in exI)
+apply (simp (no_asm_simp))
+  apply (simp only: err_def)
+  apply (frule listE_nth_in) apply assumption
+apply (subgoal_tac "LT ! i \<in> {x. \<exists>y\<in>types cG. x = OK y}")
+apply (drule CollectD) apply (erule bexE)
+apply (simp (no_asm_simp) )
+apply blast
+apply blast
+done
+
+
+lemma bc_mt_corresp_Store_init: "\<lbrakk> i < length LT \<rbrakk>
+  \<Longrightarrow> bc_mt_corresp [Store i] (storeST i T) (T # ST, LT) cG rT mxr (Suc 0)"
+ apply (simp add: bc_mt_corresp_def storeST_def wt_instr_altern_def eff_def norm_eff_def)
+  apply (simp add: max_ssize_def  max_of_list_def )
+  apply (simp add: ssize_sto_def) apply (simp add: max_def)
+  apply (intro strip)
+apply (simp add: check_type_simps)
+apply clarify
+apply (rule conjI)
+apply (rule_tac x="(length ST)" in exI)
+apply simp+
+done
+
+
+
+lemma bc_mt_corresp_Store: "\<lbrakk> i < length LT; cG  \<turnstile>  LT[i := OK T] <=l LT \<rbrakk>
+  \<Longrightarrow> bc_mt_corresp [Store i] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
+  apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
+  apply (simp add: sup_state_conv)
+  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
+  apply (simp add: max_def)
+ apply (intro strip)
+apply (simp add: check_type_simps)
+apply clarify
+apply (rule_tac x="(length ST)" in exI)
+apply simp+
+done
+
+
+lemma bc_mt_corresp_Dup: "
+  bc_mt_corresp [Dup] dupST (T # ST, LT) cG rT mxr (Suc 0)"
+ apply (simp add: bc_mt_corresp_def dupST_def wt_instr_altern_def
+                 max_ssize_def max_of_list_def ssize_sto_def max_def
+                 eff_def norm_eff_def)
+  apply (intro strip)
+  apply (rule conjI)
+  apply (rule check_type_mono, assumption, simp)
+apply (simp add: check_type_simps)
+apply clarify
+apply (rule_tac x="Suc (Suc (length ST))" in exI)
+apply simp+
+done
+
+lemma bc_mt_corresp_Dup_x1: "
+  bc_mt_corresp [Dup_x1] dup_x1ST (T1 # T2 # ST, LT) cG rT mxr (Suc 0)"
+  apply (simp add: bc_mt_corresp_def dup_x1ST_def wt_instr_altern_def
+                 max_ssize_def max_of_list_def ssize_sto_def max_def
+                 eff_def norm_eff_def)
+  apply (intro strip)
+  apply (rule conjI)
+  apply (rule check_type_mono, assumption, simp)
+apply (simp add: check_type_simps)
+apply clarify
+apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI)
+apply simp+
+done
+
+
+
+lemma bc_mt_corresp_IAdd: "
+  bc_mt_corresp [IAdd] (replST 2 (PrimT Integer)) 
+         (PrimT Integer # PrimT Integer # ST, LT) cG rT mxr (Suc 0)"
+  apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
+  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def)
+  apply (simp add: check_type_simps)
+  apply clarify
+  apply (rule_tac x="Suc (length ST)" in exI)
+  apply simp+
+  done
+
+lemma bc_mt_corresp_Getfield: "\<lbrakk> wf_prog wf_mb G; 
+  field (G, C) vname = Some (cname, T);  is_class G C \<rbrakk>
+  \<Longrightarrow> bc_mt_corresp [Getfield vname cname] 
+        (replST (Suc 0) (snd (the (field (G, cname) vname))))
+        (Class C # ST, LT) (comp G) rT mxr (Suc 0)"
+  apply (frule wf_subcls1)
+  apply (frule field_in_fd, assumption+)
+  apply (frule widen_field, assumption+)
+  apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
+  apply (simp add: comp_field [THEN sym] comp_subcls1 [THEN sym] comp_widen [THEN sym] comp_is_class [THEN sym])
+  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
+  apply (intro strip)
+apply (simp add: check_type_simps)
+apply clarify
+apply (rule_tac x="Suc (length ST)" in exI)
+apply simp+
+apply (simp only: comp_is_type [THEN sym])
+apply (rule_tac C=cname in fields_is_type)
+apply (simp add: field_def)
+apply (drule JBasis.table_of_remap_SomeD)+
+apply assumption+
+done
+
+lemma bc_mt_corresp_Putfield: "\<lbrakk> wf_prog wf_mb G; 
+  field (G, C) vname = Some (cname, Ta); G \<turnstile> T \<preceq> Ta; is_class G C \<rbrakk>
+  \<Longrightarrow> bc_mt_corresp [Putfield vname cname] (popST 2) (T # Class C # T # ST, LT)
+           (comp G) rT mxr (Suc 0)"
+  apply (frule wf_subcls1)
+  apply (frule field_in_fd, assumption+)
+  apply (frule widen_field, assumption+)
+  apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
+  apply (simp add: comp_field [THEN sym] comp_subcls1 [THEN sym] comp_widen [THEN sym] comp_is_class [THEN sym])
+  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def)
+
+  apply (intro strip)
+apply (simp add: check_type_simps)
+apply clarify
+apply (rule_tac x="Suc (length ST)" in exI)
+apply simp+
+done
+
+
+
+lemma Call_app: "\<lbrakk> wf_prog wf_mb G; is_class G cname;
+STs = rev pTsa @ Class cname # ST;
+max_spec G cname (mname, pTsa) = {((md, T), pTs')} \<rbrakk>
+  \<Longrightarrow> app (Invoke cname mname pTs') (comp G) (length (T # ST)) rT 0 empty_et (Some (STs, LTs))"
+  apply (subgoal_tac "(\<exists>mD' rT' comp_b. 
+    method (comp G, cname) (mname, pTs') = Some (mD', rT', comp_b))")
+  apply (simp add: comp_is_class)
+  apply (rule_tac x=pTsa in exI)
+  apply (rule_tac x="Class cname" in exI)
+  apply (simp add: max_spec_preserves_length comp_is_class [THEN sym])
+  apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
+  apply (simp add: comp_widen list_all2_def)
+  apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
+  apply (rule exI)+
+  apply (rule comp_method)
+  apply assumption+
+  done
+
+
+lemma bc_mt_corresp_Invoke: "\<lbrakk> wf_prog wf_mb G; 
+  max_spec G cname (mname, pTsa) = {((md, T), fpTs)};
+  is_class G cname \<rbrakk>
+ \<Longrightarrow> bc_mt_corresp [Invoke cname mname fpTs] (replST (Suc (length pTsa)) T)
+           (rev pTsa @ Class cname # ST, LT) (comp G) rT mxr (Suc 0)"
+  apply (simp add: bc_mt_corresp_def wt_instr_altern_def eff_def norm_eff_def)
+  apply (simp add: replST_def del: appInvoke)
+  apply (intro strip)
+  apply (rule conjI)
+
+  -- "app"
+  apply (rule Call_app [THEN app_mono_mxs]) apply assumption+
+    apply (rule HOL.refl) apply assumption
+    apply (simp add: max_ssize_def max_of_list_elem ssize_sto_def)
+
+  -- "<=s"
+  apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
+  apply (frule comp_method, assumption+)
+  apply (simp add: max_spec_preserves_length [THEN sym])
+
+  -- "check_type"
+apply (simp add: max_ssize_def ssize_sto_def max_def)
+apply (simp add: max_of_list_def)
+apply (subgoal_tac "(max (length pTsa + length ST) (length ST)) = (length pTsa + length ST)")
+apply simp
+apply (simp add: check_type_simps)
+apply clarify
+apply (rule_tac x="Suc (length ST)" in exI)
+apply simp+
+apply (simp only: comp_is_type [THEN sym])
+apply (frule method_wf_mdecl) apply assumption apply assumption
+apply (simp add: wf_mdecl_def wf_mhead_def)
+apply (simp add: max_def)
+  done
+
+
+lemma wt_instr_Ifcmpeq: "\<lbrakk>Suc pc < max_pc; 
+  0 \<le> (int pc + i);  nat (int pc + i) < max_pc;
+  (mt_sttp_flatten f ! pc = Some (ts#ts'#ST,LT)) \<and> 
+  ((\<exists>p. ts = PrimT p \<and> ts' = PrimT p) \<or> (\<exists>r r'. ts = RefT r \<and> ts' = RefT r'));
+  mt_sttp_flatten f ! Suc pc = Some (ST,LT);
+  mt_sttp_flatten f ! nat (int pc + i) = Some (ST,LT);
+  check_type (TranslComp.comp G) mxs mxr (OK (Some (ts # ts' # ST, LT))) \<rbrakk>
+    \<Longrightarrow>  wt_instr_altern (Ifcmpeq i) (comp G) rT  (mt_sttp_flatten f) mxs mxr max_pc empty_et pc"
+by (simp  add: wt_instr_altern_def eff_def norm_eff_def)
+
+
+lemma wt_instr_Goto: "\<lbrakk> 0 \<le> (int pc + i); nat (int pc + i) < max_pc;
+  mt_sttp_flatten f ! nat (int pc + i) = (mt_sttp_flatten f ! pc);
+  check_type (TranslComp.comp G) mxs mxr (OK (mt_sttp_flatten f ! pc)) \<rbrakk>
+  \<Longrightarrow> wt_instr_altern (Goto i) (comp G) rT  (mt_sttp_flatten f) mxs mxr max_pc empty_et pc"
+apply (case_tac "(mt_sttp_flatten f ! pc)")
+apply (simp  add: wt_instr_altern_def eff_def norm_eff_def app_def xcpt_app_def)+
+done
+
+
+
+
+  (* ********************************************************************** *)
+
+
+
+lemma bc_mt_corresp_comb_inside: "
+  \<lbrakk> 
+  bc_mt_corresp bc' f' sttp0 cG rT mxr l1;
+  bc' = (bc1@bc2@bc3); f'= (f1 \<box> f2 \<box> f3); 
+  l1 = (length bc1); l12 = (length (bc1@bc2));
+  bc_mt_corresp bc2 f2 (sttp_of (f1 sttp0)) cG rT mxr (length bc2);
+  length bc1 = length (mt_of (f1 sttp0));
+  start_sttp_resp f2; start_sttp_resp f3\<rbrakk>
+\<Longrightarrow> bc_mt_corresp bc' f' sttp0 cG rT mxr l12"
+apply (subgoal_tac "\<exists> mt1 sttp1. (f1 sttp0) = (mt1, sttp1)", (erule exE)+)
+apply (subgoal_tac "\<exists> mt2 sttp2. (f2 sttp1) = (mt2, sttp2)", (erule exE)+)
+apply (subgoal_tac "\<exists> mt3 sttp3. (f3 sttp2) = (mt3, sttp3)", (erule exE)+)
+
+  (* unfold start_sttp_resp and make case distinction *)
+apply (simp only: start_sttp_resp_def)
+apply (erule_tac Q="start_sttp_resp_cons f2" in disjE)
+  (* case f2 = comb_nil *)
+apply (simp add: bc_mt_corresp_def comb_nil_def start_sttp_resp_cons_def)
+
+  (* case start_sttp_resp_cons f2 *)
+apply (simp add: bc_mt_corresp_def comb_def start_sttp_resp_cons_def)
+apply (drule_tac x=sttp1 in spec, simp, erule exE)
+apply (intro strip, (erule conjE)+)
+
+
+  (* get rid of all check_type info *)
+apply (subgoal_tac "check_type cG (length (fst sttp1)) mxr (OK (Some sttp1))")
+apply (subgoal_tac "check_type cG (max_ssize (mt2 @ [Some sttp2])) mxr (OK (Some sttp2))")
+apply (subgoal_tac "check_type cG (max_ssize (mt1 @ mt2 @ mt3 @ [Some sttp3])) mxr
+           (OK ((mt2 @ mt3 @ [Some sttp3]) ! length mt2))")
+apply simp
+
+
+
+apply (intro strip, (erule conjE)+)
+apply (case_tac "pc < length mt1")
+
+  (* case pc < length mt1 *)
+apply (drule spec, drule mp, assumption)
+apply assumption
+
+  (* case pc \<ge> length mt1 *)
+  (* case distinction on start_sttp_resp f3 *)
+apply (erule_tac P="f3 = comb_nil" in disjE)
+
+  (* case f3 = comb_nil *)
+apply (subgoal_tac "mt3 = [] \<and> sttp2 = sttp3")  apply (erule conjE)+
+apply (subgoal_tac "bc3=[]")
+
+apply (rule_tac bc_pre=bc1 and bc=bc2 and bc_post=bc3
+  and mt_pre=mt1 and mt=mt2 and mt_post="mt3@ [Some sttp3]" 
+  and mxs="(max_ssize (mt2 @ [(Some sttp2)]))"
+  and max_pc="(Suc (length mt2))"
+  in wt_instr_offset)
+  apply simp
+  apply (rule HOL.refl)+
+  apply (simp (no_asm_simp))+
+
+  apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append)
+    apply (rule max_of_list_sublist)
+    apply (simp (no_asm_simp) only: set_append set.simps map.simps) apply blast
+  apply (simp (no_asm_simp))
+  apply simp			(* subgoal bc3 = [] *)
+  apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> sttp2 = sttp3 *)
+
+  (* case start_sttp_resp_cons f3 *)
+apply (subgoal_tac "\<exists>mt3_rest. (mt3 = Some sttp2 # mt3_rest)", erule exE)
+apply (rule_tac bc_pre=bc1 and bc=bc2 and bc_post=bc3
+  and mt_pre=mt1 and mt=mt2 and mt_post="mt3@ [Some sttp3]" 
+  and mxs="(max_ssize (mt2 @ [Some sttp2]))"
+  and max_pc="(Suc (length mt2))"
+  in wt_instr_offset)
+apply (intro strip)
+apply (rule_tac bc=bc2 and mt="(mt2 @ [Some sttp2])"
+  and mxs="(max_ssize (mt2 @ [Some sttp2]))"
+  and max_pc="(Suc (length mt2))"
+  in wt_instr_prefix)
+
+
+     (* preconditions of  wt_instr_prefix *)
+  apply simp
+  apply (rule HOL.refl)
+  apply (simp (no_asm_simp))+
+  apply simp+
+     (* (some) preconditions of  wt_instr_offset *)
+  apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append)
+  apply (rule max_of_list_sublist)
+    apply (simp (no_asm_simp) only: set_append set.simps map.simps) apply blast
+  apply (simp (no_asm_simp))
+
+apply (drule_tac x=sttp2 in spec, simp) (* subgoal \<exists>mt3_rest. \<dots> *)
+
+  (* subgoals check_type*)
+  (* \<dots> ! length mt2 *)
+apply simp
+
+apply (erule_tac P="f3 = comb_nil" in disjE)
+
+  (* -- case f3 = comb_nil *)
+apply (subgoal_tac "mt3 = [] \<and> sttp2 = sttp3")  apply (erule conjE)+
+apply simp
+apply (rule check_type_mono, assumption)
+apply (simp only: max_ssize_def) apply (rule max_of_list_sublist) apply (simp (no_asm_simp))
+apply blast
+  apply simp			(* subgoal bc3 = [] *)
+  apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> sttp2 = sttp3 *)
+
+
+  (* -- case start_sttp_resp_cons f3 *)
+apply (subgoal_tac "\<exists>mt3_rest. (mt3 = Some sttp2 # mt3_rest)", erule exE)
+apply (simp (no_asm_simp) add: nth_append)
+apply (erule conjE)+
+apply (rule check_type_mono, assumption)
+apply (simp only: max_ssize_def) apply (rule max_of_list_sublist) apply (simp (no_asm_simp))
+apply blast
+apply (drule_tac x=sttp2 in spec, simp) (* subgoal \<exists>mt3_rest. \<dots> *)
+
+
+  (* subgoal check_type \<dots> Some sttp2 *)
+apply (simp add: nth_append)
+
+  (* subgoal check_type \<dots> Some sttp1 *)
+apply (simp add: nth_append)
+apply (erule conjE)+
+apply (case_tac "sttp1", simp)
+apply (rule check_type_lower) apply assumption
+apply (simp (no_asm_simp) add: max_ssize_def ssize_sto_def)
+apply (simp (no_asm_simp) add: max_of_list_def max_def)
+
+  (* subgoals \<exists> ... *)
+apply (rule surj_pair)+
+done
+
+
+  (* ******************** *)
+constdefs 
+  contracting :: "(state_type \<Rightarrow> method_type \<times> state_type) \<Rightarrow> bool"
+  "contracting f == (\<forall> ST LT. 
+                    let (ST', LT') = sttp_of (f (ST, LT)) 
+                    in (length ST' \<le> length ST \<and> set ST' \<subseteq> set ST  \<and>
+                        length LT' = length LT \<and> set LT' \<subseteq> set LT))"
+
+
+  (* ### possibly move into HOL *)
+lemma set_drop_Suc [rule_format]: "\<forall> xs. set (drop (Suc n) xs) \<subseteq> set (drop n xs)"
+apply (induct n)
+apply simp
+apply (intro strip)
+apply (rule list.induct)
+apply simp
+apply simp apply blast
+apply (intro strip)
+apply (rule_tac 
+  P="\<lambda> xs. set (drop (Suc (Suc n)) xs) \<subseteq> set (drop (Suc n) xs)" in list.induct)
+apply simp+
+done
+
+lemma set_drop_le [rule_format,simp]: "\<forall> n xs. n \<le> m \<longrightarrow> set (drop m xs) \<subseteq> set (drop n xs)"
+apply (induct m)
+apply simp
+apply (intro strip)
+apply (subgoal_tac "na \<le> n \<or> na = Suc n")
+apply (erule disjE)
+apply (frule_tac x=na in spec, drule_tac x=xs in spec, drule mp, assumption)
+apply (rule set_drop_Suc [THEN subset_trans], assumption)
+apply auto
+done
+
+lemma set_drop [simp] : "set (drop m xs) \<subseteq> set xs"
+apply (rule_tac B="set (drop 0 xs)" in subset_trans)
+apply (rule set_drop_le)
+apply simp+
+done
+
+
+
+lemma contracting_popST [simp]: "contracting (popST n)"
+by (simp add: contracting_def popST_def)
+
+lemma contracting_nochangeST [simp]: "contracting nochangeST"
+by (simp add: contracting_def nochangeST_def)
+
+
+lemma check_type_contracting: "\<lbrakk> check_type cG mxs mxr (OK (Some sttp)); contracting f\<rbrakk> 
+  \<Longrightarrow> check_type cG mxs mxr (OK (Some (sttp_of (f sttp))))"
+apply (subgoal_tac "\<exists> ST LT. sttp = (ST, LT)", (erule exE)+)
+apply (simp add: check_type_simps contracting_def)
+apply clarify
+apply (drule_tac x=ST in spec, drule_tac x=LT in spec)
+apply (case_tac "(sttp_of (f (ST, LT)))")
+apply simp
+apply (erule conjE)+
+
+apply (drule listE_set)+
+apply (rule conjI)
+apply (rule_tac x="length a" in exI) apply simp
+apply (rule listI) apply simp apply blast
+apply (rule listI) apply simp apply blast
+apply auto
+done
+
+  (* ******************** *)
+
+
+lemma bc_mt_corresp_comb_wt_instr: "
+  \<lbrakk> bc_mt_corresp bc' f' sttp0 cG rT mxr l1;
+  bc' = (bc1@[inst]@bc3); f'= (f1 \<box> f2 \<box> f3); 
+  l1 = (length bc1); 
+  length bc1 = length (mt_of (f1 sttp0));
+  length (mt_of (f2 (sttp_of (f1 sttp0)))) = 1;
+  start_sttp_resp_cons f1; start_sttp_resp_cons f2; start_sttp_resp f3;
+
+  check_type cG (max_ssize (mt_sttp_flatten (f' sttp0))) mxr
+             (OK ((mt_sttp_flatten (f' sttp0)) ! (length bc1)))
+  \<longrightarrow>
+  wt_instr_altern inst cG rT 
+      (mt_sttp_flatten (f' sttp0)) 
+      (max_ssize (mt_sttp_flatten (f' sttp0)))
+      mxr
+      (Suc (length bc'))
+      empty_et
+      (length bc1);
+  contracting f2
+ \<rbrakk>
+\<Longrightarrow> bc_mt_corresp bc' f' sttp0 cG rT mxr (length (bc1@[inst]))"
+apply (subgoal_tac "\<exists> mt1 sttp1. (f1 sttp0) = (mt1, sttp1)", (erule exE)+)
+apply (subgoal_tac "\<exists> mt2 sttp2. (f2 sttp1) = (mt2, sttp2)", (erule exE)+)
+apply (subgoal_tac "\<exists> mt3 sttp3. (f3 sttp2) = (mt3, sttp3)", (erule exE)+)
+
+apply (simp add: bc_mt_corresp_def comb_def start_sttp_resp_cons_def
+  mt_sttp_flatten_def)
+
+apply (intro strip, (erule conjE)+)
+apply (drule mp, assumption)+ apply (erule conjE)+
+apply (drule mp, assumption)
+apply (rule conjI)
+
+  (* wt_instr \<dots> *)
+apply (intro strip)
+apply (case_tac "pc < length mt1")
+
+  (* case pc < length mt1 *)
+apply (drule spec, drule mp, assumption)
+apply assumption
+
+  (* case pc \<ge> length mt1 *)
+apply (subgoal_tac "pc = length mt1") prefer 2 apply arith
+apply (simp only:)
+apply (simp add: nth_append mt_sttp_flatten_def)
+
+
+  (* check_type \<dots> *)
+apply (simp add: start_sttp_resp_def)
+apply (drule_tac x="sttp0" in spec, simp, erule exE)
+apply (drule_tac x="sttp1" in spec, simp, erule exE)
+
+apply (subgoal_tac "check_type cG (max_ssize (mt1 @ mt2 @ mt3 @ [Some sttp3])) mxr 
+                    (OK (Some (sttp_of (f2 sttp1))))")
+
+apply (simp only:)
+
+apply (erule disjE)
+    (* case f3 = comb_nil *)
+apply (subgoal_tac "((mt1 @ mt2 @ mt3 @ [Some sttp3]) ! Suc (length mt1)) = (Some (snd (f2 sttp1)))")apply (subgoal_tac "mt3 = [] \<and> sttp2 = sttp3")  apply (erule conjE)+
+apply (simp add: nth_append)
+apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> sttp2 = sttp3 *)
+apply (simp add: nth_append comb_nil_def) (* subgoal \<dots> ! Suc (length mt1) *)
+
+    (* case start_sttp_resp_cons f3 *)
+apply (simp add: start_sttp_resp_cons_def)  
+apply (drule_tac x="sttp2" in spec, simp, erule exE)
+apply (simp  add: nth_append)
+
+  (* subgoal check_type *)
+apply (rule check_type_contracting)
+apply (subgoal_tac "((mt1 @ mt2 @ mt3 @ [Some sttp3]) ! length mt1) = (Some sttp1)")
+apply (simp add: nth_append)
+apply (simp add: nth_append)
+
+apply assumption
+
+(* subgoals *)
+apply (rule surj_pair)+
+done
+
+
+lemma compTpExpr_LT_ST_rewr [simp]: "\<lbrakk>
+  wf_java_prog G;
+  wf_java_mdecl G C ((mn, pTs), rT, (pns, lvars, blk, res));
+  local_env G C (mn, pTs) pns lvars \<turnstile> ex :: T;
+  is_inited_LT C pTs lvars LT\<rbrakk>
+\<Longrightarrow> sttp_of (compTpExpr (pns, lvars, blk, res) G ex (ST, LT)) = (T # ST, LT)"
+apply (rule compTpExpr_LT_ST)
+apply auto
+done
+
+
+
+
+lemma wt_method_compTpExpr_Exprs_corresp: "
+  \<lbrakk> jmb = (pns,lvars,blk,res); 
+  wf_prog wf_java_mdecl G;
+  wf_java_mdecl G C ((mn, pTs), rT, jmb);
+  E = (local_env G C (mn, pTs) pns lvars)\<rbrakk> 
+\<Longrightarrow> 
+ (\<forall> ST LT T bc' f'.
+  E \<turnstile> ex :: T \<longrightarrow>  
+  (is_inited_LT C pTs lvars LT) \<longrightarrow>
+  bc' = (compExpr jmb ex) \<longrightarrow>
+  f' = (compTpExpr jmb G ex)
+  \<longrightarrow> bc_mt_corresp bc' f' (ST, LT) (comp G) rT (length LT) (length bc'))
+ \<and>
+ (\<forall> ST LT Ts.
+  E \<turnstile> exs [::] Ts \<longrightarrow>
+  (is_inited_LT C pTs lvars LT) 
+  \<longrightarrow> bc_mt_corresp (compExprs jmb exs) (compTpExprs jmb G exs) (ST, LT) (comp G) rT (length LT) (length (compExprs jmb exs)))"
+
+apply (rule  expr.induct)
+
+
+(* expresssions *)
+
+(* NewC *)
+apply (intro allI impI)
+apply (simp only:)
+apply (drule NewC_invers)
+apply (simp (no_asm_use))
+apply (rule bc_mt_corresp_New)
+apply (simp add: comp_is_class)
+
+(* Cast *)
+apply (intro allI impI)
+apply (simp only:)
+apply (drule Cast_invers)
+apply clarify
+apply (simp (no_asm_use))
+apply (rule bc_mt_corresp_comb) apply (rule HOL.refl, simp (no_asm_simp), blast)
+apply (simp (no_asm_simp), rule bc_mt_corresp_Checkcast)
+apply (simp add: comp_is_class)
+apply (simp only: compTpExpr_LT_ST)
+apply blast
+apply (simp add: start_sttp_resp_def)
+
+(* Lit *)
+apply (intro allI impI)
+apply (simp only:)
+apply (drule Lit_invers)
+(* apply (simp (no_asm_use)) *)
+apply simp
+apply (rule bc_mt_corresp_LitPush)
+   apply assumption
+
+
+(* BinOp *)
+
+apply (intro allI impI)
+apply (simp (no_asm_simp) only:)
+apply (drule BinOp_invers, erule exE, (erule conjE)+)
+apply (case_tac binop)
+apply (simp (no_asm_simp))
+
+  (* case Eq *)
+apply (subgoal_tac "bc_mt_corresp bc' f' (ST, LT) (comp G) rT (length LT) 0")
+prefer 2
+  apply (rule bc_mt_corresp_zero) apply (simp add: length_compTpExpr) 
+  apply (simp (no_asm_simp))
+
+apply (drule_tac "bc1.0"="[]" and "bc2.0" = "compExpr jmb expr1" 
+  and "f1.0"=comb_nil and "f2.0" = "compTpExpr jmb G expr1" 
+  in bc_mt_corresp_comb_inside)
+  apply (simp (no_asm_simp))+
+  apply blast
+  apply (simp (no_asm_simp) add: length_compTpExpr)+
+
+apply (drule_tac "bc2.0" = "compExpr jmb expr2" and "f2.0" = "compTpExpr jmb G expr2" 
+  in bc_mt_corresp_comb_inside)
+  apply (simp (no_asm_simp))+
+  apply (simp only: compTpExpr_LT_ST)
+  apply (simp (no_asm_simp) add: length_compTpExpr)
+  apply (simp (no_asm_simp))
+  apply (simp (no_asm_simp))
+
+apply (drule_tac "bc1.0" = "compExpr jmb expr1 @ compExpr jmb expr2" 
+    and inst = "Ifcmpeq 3" and "bc3.0" = "[LitPush (Bool False),Goto 2, LitPush (Bool True)]"
+  and "f1.0"="compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2"
+  and "f2.0"="popST 2" and "f3.0"="pushST [PrimT Boolean] \<box> popST 1 \<box> pushST [PrimT Boolean]"
+  in bc_mt_corresp_comb_wt_instr)
+  apply (simp (no_asm_simp) add: length_compTpExpr)+
+
+    (* wt_instr *)
+  apply (intro strip)
+  apply (simp (no_asm_simp) add: wt_instr_altern_def length_compTpExpr eff_def)
+  apply (simp (no_asm_simp) add: norm_eff_def)
+  apply (simp (no_asm_simp) only: int_outside_left nat_int)
+  apply (simp (no_asm_simp) add: length_compTpExpr)
+  apply (simp only: compTpExpr_LT_ST)+
+  apply (simp add: eff_def norm_eff_def popST_def pushST_def mt_sttp_flatten_def)
+  apply (case_tac Ta) apply (simp (no_asm_simp)) apply (simp (no_asm_simp))
+  apply (rule contracting_popST)		(* contracting (popST 2)  *)
+
+apply (drule_tac "bc1.0" = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3]"
+  and "bc2.0" = "[LitPush (Bool False)]" 
+  and "bc3.0" = "[Goto 2, LitPush (Bool True)]" 
+  and "f1.0" = "compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2"
+  and "f2.0" = "pushST [PrimT Boolean]" 
+  and "f3.0" = "popST (Suc 0) \<box> pushST [PrimT Boolean]"
+  in bc_mt_corresp_comb_inside)
+  apply (simp (no_asm_simp))+
+  apply (simp add: compTpExpr_LT_ST_rewr popST_def)
+  apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush) apply (simp (no_asm_simp))
+  apply (simp (no_asm_simp) add: length_compTpExpr)
+  apply (simp (no_asm_simp))
+  apply (simp (no_asm_simp) add: start_sttp_resp_def)
+
+
+apply (drule_tac "bc1.0" = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3, LitPush (Bool False)]" 
+    and inst = "Goto 2" and "bc3.0" = "[LitPush (Bool True)]"
+  and "f1.0"="compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2 \<box> pushST [PrimT Boolean]"
+  and "f2.0"="popST 1" and "f3.0"="pushST [PrimT Boolean]"
+  in bc_mt_corresp_comb_wt_instr)
+  apply (simp (no_asm_simp) add: length_compTpExpr)+
+
+    (* wt_instr *)
+  apply (simp (no_asm_simp) add: wt_instr_altern_def length_compTpExpr)
+  apply (simp (no_asm_simp) add: eff_def norm_eff_def)
+  apply (simp (no_asm_simp) only: int_outside_right nat_int)
+  apply (simp (no_asm_simp) add: length_compTpExpr)
+  apply (simp only: compTpExpr_LT_ST)+
+  apply (simp add: eff_def norm_eff_def popST_def pushST_def)
+  apply (rule contracting_popST)		(* contracting (popST 1) *)
+
+apply (drule_tac 
+  "bc1.0" = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3, LitPush (Bool False), Goto 2]" 
+  and "bc2.0" = "[LitPush (Bool True)]"
+  and "bc3.0" = "[]"
+  and "f1.0" = "compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2 \<box> 
+                pushST [PrimT Boolean] \<box> popST (Suc 0)"
+  and "f2.0" = "pushST [PrimT Boolean]"
+  and "f3.0" = "comb_nil" 
+  in bc_mt_corresp_comb_inside)
+  apply (simp (no_asm_simp))+
+  apply (simp add: compTpExpr_LT_ST_rewr popST_def) 
+  apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush) apply (simp (no_asm_simp))
+  apply (simp (no_asm_simp) add: length_compTpExpr)
+  apply (simp (no_asm_simp) add: start_sttp_resp_def)
+  apply (simp (no_asm_simp))
+
+apply simp
+
+  (* case Add *)
+apply simp
+apply (rule bc_mt_corresp_comb) apply (rule HOL.refl) apply simp apply blast
+apply (rule bc_mt_corresp_comb, rule HOL.refl) 
+   apply (simp only: compTpExpr_LT_ST) 
+apply (simp only: compTpExpr_LT_ST) apply blast
+
+apply (simp only: compTpExpr_LT_ST)
+apply simp
+apply (rule bc_mt_corresp_IAdd)
+apply (simp (no_asm_simp) add: start_sttp_resp_def)
+apply (simp (no_asm_simp) add: start_sttp_resp_def)
+
+
+  (* LAcc *)
+apply (intro allI impI)
+apply (simp only:)
+apply (drule LAcc_invers)
+apply (frule wf_java_mdecl_length_pTs_pns)
+apply clarify
+apply (simp add: is_inited_LT_def)
+apply (rule bc_mt_corresp_Load)
+  apply (rule index_in_bounds) apply simp apply assumption
+  apply (rule inited_LT_at_index_no_err)
+  apply (rule index_in_bounds) apply simp apply assumption
+apply (rule HOL.refl)
+
+
+  (* LAss *)
+apply (intro allI impI)
+apply (simp only:)
+apply (drule LAss_invers, erule exE, (erule conjE)+)
+apply (drule LAcc_invers)
+apply (frule wf_java_mdecl_disjoint_varnames, simp add: disjoint_varnames_def)
+apply (frule wf_java_mdecl_length_pTs_pns)
+apply clarify
+apply (simp (no_asm_use))
+apply (rule bc_mt_corresp_comb) apply (rule HOL.refl, simp (no_asm_simp), blast)
+apply (rule_tac "bc1.0"="[Dup]" and "bc2.0"="[Store (index (pns, lvars, blk, res) vname)]" 
+       and "f1.0"="dupST" and "f2.0"="popST (Suc 0)"
+       in bc_mt_corresp_comb) 
+  apply (simp (no_asm_simp))+
+  apply (rule bc_mt_corresp_Dup)
+  apply (simp only: compTpExpr_LT_ST)
+  apply (simp add: dupST_def is_inited_LT_def)
+  apply (rule bc_mt_corresp_Store)
+  apply (rule index_in_bounds)
+    apply simp apply assumption
+  apply (rule sup_loc_update_index, assumption+) 
+    apply simp apply assumption+
+apply (simp add: start_sttp_resp_def)
+apply (simp add: start_sttp_resp_def)
+
+  (* FAcc *)
+apply (intro allI impI)
+apply (simp only:)
+apply (drule FAcc_invers)
+apply clarify
+apply (simp (no_asm_use))
+apply (rule bc_mt_corresp_comb) apply (rule HOL.refl, simp (no_asm_simp), blast) 
+  apply (simp (no_asm_simp))
+  apply (rule bc_mt_corresp_Getfield) apply assumption+
+     apply (rule wt_class_expr_is_class, assumption+) apply (rule HOL.refl)
+apply (simp (no_asm_simp) add: start_sttp_resp_def)
+
+
+  (* FAss *)
+apply (intro allI impI)
+apply (simp only:)
+apply (drule FAss_invers, erule exE, (erule conjE)+)
+apply (drule FAcc_invers)
+apply clarify
+apply (simp (no_asm_use))
+apply (rule bc_mt_corresp_comb) apply (rule HOL.refl) apply simp apply blast
+  apply (simp only: compTpExpr_LT_ST)
+apply (rule bc_mt_corresp_comb, (rule HOL.refl)+) apply blast
+  apply (simp only: compTpExpr_LT_ST)
+apply (rule_tac "bc1.0"="[Dup_x1]" and "bc2.0"="[Putfield vname cname]" in bc_mt_corresp_comb) 
+  apply (simp (no_asm_simp))+
+apply (rule bc_mt_corresp_Dup_x1)
+  apply (simp (no_asm_simp) add: dup_x1ST_def)
+apply (rule bc_mt_corresp_Putfield) apply assumption+
+     apply (rule wt_class_expr_is_class, assumption+) apply (rule HOL.refl)
+apply (simp (no_asm_simp) add: start_sttp_resp_def)
+apply (simp (no_asm_simp) add: start_sttp_resp_def)
+apply (simp (no_asm_simp) add: start_sttp_resp_def)
+
+(* Call *)
+apply (intro allI impI)
+apply (simp only:)
+apply (drule Call_invers)
+apply clarify
+apply (simp (no_asm_use))
+apply (rule bc_mt_corresp_comb) apply (rule HOL.refl) apply simp apply blast
+  apply (simp only: compTpExpr_LT_ST)
+apply (rule bc_mt_corresp_comb, (rule HOL.refl)+) apply blast
+  apply (simp only: compTpExprs_LT_ST)
+  apply (simp (no_asm_simp))
+apply (rule bc_mt_corresp_Invoke) apply assumption+
+  apply (rule wt_class_expr_is_class, assumption+) apply (rule HOL.refl)
+apply (simp (no_asm_simp) add: start_sttp_resp_def)
+apply (rule start_sttp_resp_comb) 
+  apply (simp (no_asm_simp))
+  apply (simp (no_asm_simp) add: start_sttp_resp_def)
+
+
+(* expression lists *)
+(* nil *) 
+
+apply (intro allI impI)
+apply (drule Nil_invers)
+apply simp
+
+(* cons *)
+
+apply (intro allI impI)
+apply (drule Cons_invers, (erule exE)+, (erule conjE)+)
+apply clarify
+apply (simp (no_asm_use))
+apply (rule bc_mt_corresp_comb) apply (rule HOL.refl) apply simp apply blast
+  apply (simp only: compTpExpr_LT_ST)
+apply blast
+apply simp
+
+done
+
+
+lemmas wt_method_compTpExpr_corresp [rule_format (no_asm)] = 
+  wt_method_compTpExpr_Exprs_corresp [THEN conjunct1]
+
+
+  (* ********************************************************************** *)
+
+
+
+
+lemma wt_method_compTpStmt_corresp [rule_format (no_asm)]: "
+  \<lbrakk> jmb = (pns,lvars,blk,res); 
+  wf_prog wf_java_mdecl G;
+  wf_java_mdecl G C ((mn, pTs), rT, jmb);
+  E = (local_env G C (mn, pTs) pns lvars)\<rbrakk> 
+\<Longrightarrow> 
+ (\<forall> ST LT T bc' f'.
+  E \<turnstile> s\<surd> \<longrightarrow>
+  (is_inited_LT C pTs lvars LT) \<longrightarrow>
+  bc' = (compStmt jmb s) \<longrightarrow>
+  f' = (compTpStmt jmb G s)
+  \<longrightarrow> bc_mt_corresp bc' f' (ST, LT) (comp G) rT (length LT) (length bc'))"
+
+apply (rule stmt.induct)
+
+(* Skip *) 
+apply (intro allI impI)
+apply simp
+
+
+(* Expr *)
+apply (intro allI impI)
+apply (drule Expr_invers, erule exE)
+apply (simp (no_asm_simp))
+apply (rule bc_mt_corresp_comb) apply (rule HOL.refl, simp (no_asm_simp))
+apply (rule wt_method_compTpExpr_corresp) apply assumption+
+apply (simp add: compTpExpr_LT_ST [of _ pns lvars blk res])+
+apply (rule bc_mt_corresp_Pop)
+apply (simp add: start_sttp_resp_def)
+
+
+(* Comp *)
+apply (intro allI impI)
+apply (drule Comp_invers)
+apply clarify
+apply (simp (no_asm_use))
+apply (rule bc_mt_corresp_comb) apply (rule HOL.refl) 
+   apply (simp (no_asm_simp)) apply blast
+apply (simp only: compTpStmt_LT_ST) 
+apply (simp (no_asm_simp))
+
+(* Cond *)
+apply (intro allI impI)
+apply (simp (no_asm_simp) only:)
+apply (drule Cond_invers, (erule conjE)+)
+apply (simp (no_asm_simp))
+
+apply (subgoal_tac "bc_mt_corresp bc' f' (ST, LT) (comp G) rT (length LT) 0")
+prefer 2 
+apply (rule bc_mt_corresp_zero) 
+  apply (simp (no_asm_simp) add: length_compTpStmt length_compTpExpr)
+  apply (simp (no_asm_simp))
+
+apply (drule_tac "bc1.0"="[]" and "bc2.0" = "[LitPush (Bool False)]" 
+  and "bc3.0"="compExpr jmb expr @ Ifcmpeq (2 + int (length (compStmt jmb stmt1))) #
+            compStmt jmb stmt1 @ Goto (1 + int (length (compStmt jmb stmt2))) #
+            compStmt jmb stmt2" 
+  and "f1.0"=comb_nil and "f2.0" = "pushST [PrimT Boolean]" 
+  and "f3.0"="compTpExpr jmb G expr \<box> popST 2 \<box> compTpStmt jmb G stmt1 \<box>
+            nochangeST \<box> compTpStmt jmb G stmt2"
+  in bc_mt_corresp_comb_inside)
+  apply (simp (no_asm_simp))+
+  apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush)
+  apply (simp (no_asm_simp) add: start_sttp_resp_def)+
+
+apply (drule_tac "bc1.0"="[LitPush (Bool False)]" and "bc2.0" = "compExpr jmb expr"
+  and "bc3.0"="Ifcmpeq (2 + int (length (compStmt jmb stmt1))) #
+            compStmt jmb stmt1 @ Goto (1 + int (length (compStmt jmb stmt2))) #
+            compStmt jmb stmt2" 
+  and "f1.0"="pushST [PrimT Boolean]" and "f2.0" = "compTpExpr jmb G expr"
+  and "f3.0"="popST 2 \<box> compTpStmt jmb G stmt1 \<box>
+            nochangeST \<box> compTpStmt jmb G stmt2"
+  in bc_mt_corresp_comb_inside)
+  apply (simp (no_asm_simp))+
+  apply (simp (no_asm_simp)  add: pushST_def)
+  apply (rule  wt_method_compTpExpr_corresp) apply assumption+ 
+      apply (simp (no_asm_simp))+
+
+
+apply (drule_tac "bc1.0" = "[LitPush (Bool False)] @ compExpr jmb expr" 
+    and inst = "Ifcmpeq (2 + int (length (compStmt jmb stmt1)))" 
+  and "bc3.0" = "compStmt jmb stmt1 @ Goto (1 + int (length (compStmt jmb stmt2))) #
+            compStmt jmb stmt2"
+  and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr" and "f2.0" = "popST 2"
+  and "f3.0"="compTpStmt jmb G stmt1 \<box> nochangeST \<box> compTpStmt jmb G stmt2"
+  in bc_mt_corresp_comb_wt_instr)
+  apply (simp (no_asm_simp) add: length_compTpExpr)+
+  apply (simp (no_asm_simp) add: start_sttp_resp_comb)
+
+    (* wt_instr *)
+  apply (intro strip)
+  apply (rule_tac ts="PrimT Boolean" and ts'="PrimT Boolean" 
+    and ST=ST and LT=LT 
+    in wt_instr_Ifcmpeq)
+  apply (simp (no_asm_simp))
+  apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
+  apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
+    (* current pc *)
+  apply (simp add: length_compTpExpr pushST_def)
+  apply (simp only: compTpExpr_LT_ST) 
+    (* Suc pc *)
+  apply (simp add: length_compTpExpr pushST_def)
+  apply (simp add: popST_def start_sttp_resp_comb)
+    (* jump goal *)
+  apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
+  apply (simp add: length_compTpExpr pushST_def)
+  apply (simp add: popST_def start_sttp_resp_comb length_compTpStmt)
+  apply (simp only: compTpStmt_LT_ST)
+  apply (simp add: nochangeST_def)
+    (* check_type *)
+  apply (subgoal_tac "
+    (mt_sttp_flatten (f' (ST, LT)) ! length ([LitPush (Bool False)] @ compExpr jmb expr)) = 
+    (Some (PrimT Boolean # PrimT Boolean # ST, LT))")
+  apply (simp only:)
+  apply (simp (no_asm_simp)) apply (rule trans, rule mt_sttp_flatten_comb_length) 
+    apply (rule HOL.refl) apply (simp (no_asm_simp) add: length_compTpExpr)
+    apply (simp (no_asm_simp) add: length_compTpExpr pushST_def)
+    apply (simp only: compTpExpr_LT_ST_rewr) 
+    (* contracting\<dots> *)
+  apply (rule contracting_popST)
+
+apply (drule_tac 
+  "bc1.0"="[LitPush (Bool False)] @ compExpr jmb expr @ 
+           [Ifcmpeq (2 + int (length (compStmt jmb stmt1)))] " 
+  and "bc2.0" = "compStmt jmb stmt1"
+  and "bc3.0"="Goto (1 + int (length (compStmt jmb stmt2))) # compStmt jmb stmt2"
+  and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2" 
+  and "f2.0" = "compTpStmt jmb G stmt1"
+  and "f3.0"="nochangeST \<box> compTpStmt jmb G stmt2"
+  in bc_mt_corresp_comb_inside)
+  apply (simp (no_asm_simp))+
+  apply (simp (no_asm_simp) add: pushST_def popST_def compTpExpr_LT_ST)
+  apply (simp only: compTpExpr_LT_ST)
+  apply (simp (no_asm_simp))
+  apply (simp (no_asm_simp) add: length_compTpExpr)+
+
+
+apply (drule_tac "bc1.0" = "[LitPush (Bool False)] @ compExpr jmb expr @ [Ifcmpeq (2 + int (length (compStmt jmb stmt1)))] @ compStmt jmb stmt1" 
+    and inst = "Goto (1 + int (length (compStmt jmb stmt2)))"
+  and "bc3.0" = "compStmt jmb stmt2"
+  and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box> 
+              compTpStmt jmb G stmt1" 
+  and "f2.0" = "nochangeST"
+  and "f3.0"="compTpStmt jmb G stmt2"
+  in bc_mt_corresp_comb_wt_instr)
+  apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)+
+  apply (intro strip)
+  apply (rule wt_instr_Goto)
+  apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
+  apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
+    (* \<dots> ! nat (int pc + i) = \<dots> ! pc *)
+  apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
+  apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)
+  apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def)
+  apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
+  apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def)
+  apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
+  apply (simp only:)
+  apply (simp add: length_compTpExpr length_compTpStmt)
+  apply (rule contracting_nochangeST)
+
+
+apply (drule_tac 
+  "bc1.0"= "[LitPush (Bool False)] @ compExpr jmb expr @ 
+            [Ifcmpeq (2 + int (length (compStmt jmb stmt1)))] @ 
+            compStmt jmb stmt1 @ [Goto (1 + int (length (compStmt jmb stmt2)))]"
+  and "bc2.0" = "compStmt jmb stmt2"
+  and "bc3.0"="[]"
+  and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box> 
+              compTpStmt jmb G stmt1 \<box> nochangeST"
+  and "f2.0" = "compTpStmt jmb G stmt2"
+  and "f3.0"="comb_nil"
+  in bc_mt_corresp_comb_inside)
+  apply (simp (no_asm_simp))+
+  apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def compTpExpr_LT_ST)
+  apply (simp only: compTpExpr_LT_ST)
+  apply (simp (no_asm_simp))
+  apply (simp only: compTpStmt_LT_ST)
+  apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)+
+
+apply simp
+
+
+(* Loop *)
+apply (intro allI impI)
+apply (simp (no_asm_simp) only:)
+apply (drule Loop_invers, (erule conjE)+)
+apply (simp (no_asm_simp))
+
+apply (subgoal_tac "bc_mt_corresp bc' f' (ST, LT) (comp G) rT (length LT) 0")
+prefer 2 
+apply (rule bc_mt_corresp_zero) 
+  apply (simp (no_asm_simp) add: length_compTpStmt length_compTpExpr)
+  apply (simp (no_asm_simp))
+
+apply (drule_tac "bc1.0"="[]" and "bc2.0" = "[LitPush (Bool False)]" 
+  and "bc3.0"="compExpr jmb expr @ Ifcmpeq (2 + int (length (compStmt jmb stmt))) #
+            compStmt jmb stmt @ 
+            [Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]" 
+  and "f1.0"=comb_nil and "f2.0" = "pushST [PrimT Boolean]" 
+  and "f3.0"="compTpExpr jmb G expr \<box> popST 2 \<box> compTpStmt jmb G stmt \<box> nochangeST"
+  in bc_mt_corresp_comb_inside)
+  apply (simp (no_asm_simp))+
+  apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush)
+  apply (simp (no_asm_simp) add: start_sttp_resp_def)+
+
+apply (drule_tac "bc1.0"="[LitPush (Bool False)]" and "bc2.0" = "compExpr jmb expr"
+  and "bc3.0"="Ifcmpeq (2 + int (length (compStmt jmb stmt))) #
+            compStmt jmb stmt @ 
+            [Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]" 
+  and "f1.0"="pushST [PrimT Boolean]" and "f2.0" = "compTpExpr jmb G expr"
+  and "f3.0"="popST 2 \<box> compTpStmt jmb G stmt \<box> nochangeST"
+  in bc_mt_corresp_comb_inside)
+  apply (simp (no_asm_simp))+
+  apply (simp (no_asm_simp)  add: pushST_def)
+  apply (rule  wt_method_compTpExpr_corresp) apply assumption+ 
+      apply (simp (no_asm_simp))+
+
+
+apply (drule_tac "bc1.0" = "[LitPush (Bool False)] @ compExpr jmb expr" 
+    and inst = "Ifcmpeq (2 + int (length (compStmt jmb stmt)))" 
+  and "bc3.0" = "compStmt jmb stmt @ 
+       [Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]"
+  and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr" and "f2.0" = "popST 2"
+  and "f3.0"="compTpStmt jmb G stmt \<box> nochangeST"
+  in bc_mt_corresp_comb_wt_instr)
+  apply (simp (no_asm_simp) add: length_compTpExpr)+
+  apply (simp (no_asm_simp) add: start_sttp_resp_comb)
+
+    (* wt_instr *)
+  apply (intro strip)
+  apply (rule_tac ts="PrimT Boolean" and ts'="PrimT Boolean" 
+    and ST=ST and LT=LT 
+    in wt_instr_Ifcmpeq)
+  apply (simp (no_asm_simp))
+  apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
+  apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
+    (* current pc *)
+  apply (simp add: length_compTpExpr pushST_def)
+  apply (simp only: compTpExpr_LT_ST) 
+    (* Suc pc *)
+  apply (simp add: length_compTpExpr pushST_def)
+  apply (simp add: popST_def start_sttp_resp_comb)
+    (* jump goal *)
+  apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
+  apply (simp add: length_compTpExpr pushST_def)
+  apply (simp add: popST_def start_sttp_resp_comb length_compTpStmt)
+  apply (simp only: compTpStmt_LT_ST)
+  apply (simp add: nochangeST_def)
+    (* check_type *)
+  apply (subgoal_tac "
+    (mt_sttp_flatten (f' (ST, LT)) ! length ([LitPush (Bool False)] @ compExpr jmb expr)) = 
+    (Some (PrimT Boolean # PrimT Boolean # ST, LT))")
+  apply (simp only:)
+  apply (simp (no_asm_simp)) apply (rule trans, rule mt_sttp_flatten_comb_length) 
+    apply (rule HOL.refl) apply (simp (no_asm_simp) add: length_compTpExpr)
+    apply (simp (no_asm_simp) add: length_compTpExpr pushST_def)
+    apply (simp only: compTpExpr_LT_ST_rewr) 
+    (* contracting\<dots> *)
+  apply (rule contracting_popST)
+
+apply (drule_tac 
+  "bc1.0"="[LitPush (Bool False)] @ compExpr jmb expr @ 
+           [Ifcmpeq (2 + int (length (compStmt jmb stmt)))] " 
+  and "bc2.0" = "compStmt jmb stmt"
+  and "bc3.0"="[Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]"
+  and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2" 
+  and "f2.0" = "compTpStmt jmb G stmt"
+  and "f3.0"="nochangeST"
+  in bc_mt_corresp_comb_inside)
+  apply (simp (no_asm_simp))+
+  apply (simp (no_asm_simp) add: pushST_def popST_def compTpExpr_LT_ST)
+  apply (simp only: compTpExpr_LT_ST)
+  apply (simp (no_asm_simp))
+  apply (simp (no_asm_simp) add: length_compTpExpr)+
+
+
+apply (drule_tac "bc1.0" = "[LitPush (Bool False)] @ compExpr jmb expr @ [Ifcmpeq (2 + int (length (compStmt jmb stmt)))] @ compStmt jmb stmt" 
+    and inst = "Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))"
+  and "bc3.0" = "[]"
+  and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box> 
+              compTpStmt jmb G stmt" 
+  and "f2.0" = "nochangeST"
+  and "f3.0"="comb_nil"
+  in bc_mt_corresp_comb_wt_instr)
+  apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)+ 
+  apply (intro strip)
+  apply (rule wt_instr_Goto)
+  apply (simp (no_asm_simp) add: nat_canonify)
+  apply (simp (no_asm_simp) add: nat_canonify)
+    (* \<dots> ! nat (int pc + i) = \<dots> ! pc *)
+  apply (simp (no_asm_simp) add: nat_canonify)
+  apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)
+  apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def)
+  apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
+  apply (simp (no_asm_simp) only: int_outside_right nat_int)
+  apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)
+  apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
+  apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def)
+  apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)
+  apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
+
+  apply (simp add: length_compTpExpr length_compTpStmt) (* check_type *)
+    apply (simp add: pushST_def popST_def compTpExpr_LT_ST compTpStmt_LT_ST)
+  apply (rule contracting_nochangeST)
+apply simp
+
+done
+
+
+  (**********************************************************************************)
+
+
+
+lemma wt_method_compTpInit_corresp: "\<lbrakk> jmb = (pns,lvars,blk,res); 
+  wf_java_mdecl G C ((mn, pTs), rT, jmb); mxr = length LT;
+  length LT = (length pns) + (length lvars) + 1;  vn \<in> set (map fst lvars);
+  bc = (compInit jmb (vn,ty)); f = (compTpInit jmb (vn,ty));
+  is_type G ty \<rbrakk>
+  \<Longrightarrow> bc_mt_corresp bc f (ST, LT) (comp G) rT mxr (length bc)"
+apply (simp add: compInit_def compTpInit_def split_beta)
+apply (rule_tac "bc1.0"="[load_default_val ty]" and "bc2.0"="[Store (index jmb vn)]" 
+  in bc_mt_corresp_comb) 
+  apply simp+
+  apply (simp add: load_default_val_def)
+   apply (rule typeof_default_val [THEN exE]) 
+
+  apply (rule bc_mt_corresp_LitPush_CT) apply assumption
+    apply (simp add: comp_is_type)
+apply (simp add: pushST_def)
+  apply (rule bc_mt_corresp_Store_init)
+  apply simp
+  apply (rule index_length_lvars [THEN conjunct2])
+apply auto
+done
+
+
+lemma wt_method_compTpInitLvars_corresp_aux [rule_format (no_asm)]: "
+  \<forall> lvars_pre lvars0 ST LT.
+  jmb = (pns,lvars0,blk,res) \<and>
+  lvars0 = (lvars_pre @ lvars) \<and>
+  length LT = (length pns) + (length lvars0) + 1 \<and>
+  wf_java_mdecl G C ((mn, pTs), rT, jmb)
+ \<longrightarrow> bc_mt_corresp (compInitLvars jmb lvars) (compTpInitLvars jmb lvars) (ST, LT) (comp G) rT 
+       (length LT) (length (compInitLvars jmb lvars))"
+apply (induct lvars)
+apply (simp add: compInitLvars_def)
+
+apply (intro strip, (erule conjE)+)
+apply (subgoal_tac "\<exists> vn ty. a = (vn, ty)")
+  prefer 2 apply (simp (no_asm_simp)) 
+  apply ((erule exE)+, simp (no_asm_simp))
+apply (drule_tac x="lvars_pre @ [a]" in spec)
+apply (drule_tac x="lvars0" in spec)
+apply (simp (no_asm_simp) add: compInitLvars_def)
+apply (rule_tac "bc1.0"="compInit jmb a" and "bc2.0"="compInitLvars jmb list"
+  in bc_mt_corresp_comb)
+apply (simp (no_asm_simp) add: compInitLvars_def)+
+
+apply (rule_tac vn=vn and ty=ty in wt_method_compTpInit_corresp)
+apply assumption+
+apply (simp (no_asm_simp))+ 
+apply (simp add: wf_java_mdecl_def)	(* is_type G ty *)
+apply (simp add: compTpInit_def storeST_def pushST_def)
+apply simp
+done
+
+
+lemma wt_method_compTpInitLvars_corresp: "\<lbrakk> jmb = (pns,lvars,blk,res); 
+  wf_java_mdecl G C ((mn, pTs), rT, jmb);
+  length LT = (length pns) + (length lvars) + 1; mxr = (length LT);
+  bc = (compInitLvars jmb lvars); f= (compTpInitLvars jmb lvars) \<rbrakk>
+  \<Longrightarrow> bc_mt_corresp bc f (ST, LT) (comp G) rT mxr (length bc)"
+apply (simp only:)
+apply (subgoal_tac "bc_mt_corresp (compInitLvars (pns, lvars, blk, res) lvars)
+        (compTpInitLvars (pns, lvars, blk, res) lvars) (ST, LT) (TranslComp.comp G) rT
+        (length LT) (length (compInitLvars (pns, lvars, blk, res) lvars))")
+apply simp
+apply (rule_tac lvars_pre="[]" in wt_method_compTpInitLvars_corresp_aux)
+apply auto
+done
+
+
+  (**********************************************************************************)
+
+
+
+lemma wt_method_comp_wo_return: "\<lbrakk> wf_prog wf_java_mdecl G;
+  wf_java_mdecl G C ((mn, pTs), rT, jmb); 
+  bc = compInitLvars jmb lvars @ compStmt jmb blk @ compExpr jmb res;
+  jmb = (pns,lvars,blk,res); 
+  f = (compTpInitLvars jmb lvars \<box> compTpStmt jmb G blk \<box> compTpExpr jmb G res);
+  sttp = (start_ST, start_LT C pTs (length lvars));
+  li = (length (inited_LT C pTs lvars))
+  \<rbrakk>
+\<Longrightarrow> bc_mt_corresp bc f sttp (comp G) rT  li (length bc)"
+apply (subgoal_tac "\<exists> E. (E = (local_env G C (mn, pTs) pns lvars) \<and> E \<turnstile> blk \<surd> \<and> 
+                         (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))")
+   apply (erule exE, (erule conjE)+)+
+apply (simp only:)
+apply (rule bc_mt_corresp_comb) apply (rule HOL.refl)+
+
+  (* InitLvars *)
+apply (rule wt_method_compTpInitLvars_corresp) 
+   apply assumption+
+   apply (simp only:)
+   apply (simp (no_asm_simp) add: start_LT_def) 
+       apply (rule wf_java_mdecl_length_pTs_pns, assumption)
+   apply (simp (no_asm_simp) only: start_LT_def)
+   apply (simp (no_asm_simp) add: inited_LT_def)+
+
+apply (rule bc_mt_corresp_comb) apply (rule HOL.refl)+
+   apply (simp (no_asm_simp) add: compTpInitLvars_LT_ST)
+
+     (* stmt *)
+apply (simp only: compTpInitLvars_LT_ST)
+apply (subgoal_tac "(Suc (length pTs + length lvars)) = (length (inited_LT C pTs lvars))")
+   prefer 2 apply (simp (no_asm_simp) add: inited_LT_def)
+apply (simp only:)
+apply (rule_tac s=blk in wt_method_compTpStmt_corresp)
+   apply assumption+
+   apply (simp only:)+
+   apply (simp (no_asm_simp) add: is_inited_LT_def)
+   apply (simp only:)+
+
+     (* expr *)
+apply (simp only: compTpInitLvars_LT_ST compTpStmt_LT_ST is_inited_LT_def)
+apply (subgoal_tac "(Suc (length pTs + length lvars)) = (length (inited_LT C pTs lvars))")
+   prefer 2 apply (simp (no_asm_simp) add: inited_LT_def)
+apply (simp only:)
+apply (rule_tac ex=res in wt_method_compTpExpr_corresp)
+   apply assumption+
+   apply (simp only:)+
+   apply (simp (no_asm_simp) add: is_inited_LT_def)
+   apply (simp only:)+
+
+     (* start_sttp_resp *)
+apply (simp add: start_sttp_resp_comb)+
+
+  (* subgoal *)
+apply (simp add: wf_java_mdecl_def local_env_def) 
+done
+
+
+  (**********************************************************************************)
+
+
+
+lemma check_type_start: "\<lbrakk> wf_mhead cG (mn, pTs) rT; is_class cG C\<rbrakk>
+  \<Longrightarrow> check_type cG (length start_ST) (Suc (length pTs + mxl))
+              (OK (Some (start_ST, start_LT C pTs mxl)))"
+apply (simp add: check_type_def wf_mhead_def start_ST_def start_LT_def)
+apply (simp add: check_type_simps)
+apply (simp only: list_def)
+apply (auto simp: err_def)
+apply (subgoal_tac "set (replicate mxl Err) \<subseteq>  {Err}")
+apply blast
+apply (rule subset_replicate)
+done
+
+
+lemma wt_method_comp_aux: "\<lbrakk>   bc' = bc @ [Return]; f' = (f \<box> nochangeST);
+  bc_mt_corresp bc f sttp0 cG rT (1+length pTs+mxl) (length bc);
+  start_sttp_resp_cons f';
+  sttp0 = (start_ST, start_LT C pTs mxl);
+  mxs = max_ssize (mt_of (f' sttp0));
+  wf_mhead cG (mn, pTs) rT; is_class cG C;
+  sttp_of (f sttp0) = (T # ST, LT);
+
+  check_type cG mxs (1+length pTs+mxl) (OK (Some (T # ST, LT))) \<longrightarrow>
+  wt_instr_altern Return cG rT (mt_of (f' sttp0)) mxs (1+length pTs+mxl) 
+         (Suc (length bc)) empty_et (length bc)
+\<rbrakk>
+\<Longrightarrow> wt_method_altern cG C pTs rT mxs mxl bc' empty_et (mt_of (f' sttp0))"
+apply (subgoal_tac "check_type cG (length start_ST) (Suc (length pTs + mxl))
+              (OK (Some (start_ST, start_LT C pTs mxl)))")
+apply (subgoal_tac "check_type cG mxs (1+length pTs+mxl) (OK (Some (T # ST, LT)))")
+
+apply (simp add: wt_method_altern_def)
+
+  (* length (.. f ..) = length bc *)
+apply (rule conjI)
+apply (simp add: bc_mt_corresp_def split_beta)
+
+  (* check_bounded *)
+apply (rule conjI)
+apply (simp add: bc_mt_corresp_def split_beta check_bounded_def) 
+apply (erule conjE)+
+apply (intro strip)
+apply (subgoal_tac "pc < (length bc) \<or> pc = length bc")
+  apply (erule disjE)
+    (* case  pc < length bc *)
+    apply (subgoal_tac "(bc' ! pc) = (bc ! pc)")
+    apply (simp add: wt_instr_altern_def eff_def)
+      (* subgoal *)
+    apply (simp add: nth_append)
+    (* case  pc = length bc *)
+    apply (subgoal_tac "(bc' ! pc) = Return")
+    apply (simp add: wt_instr_altern_def)
+      (* subgoal *)
+    apply (simp add: nth_append)
+
+    (* subgoal pc < length bc \<or> pc = length bc *)
+apply arith
+
+  (* wt_start *)
+apply (rule conjI)
+apply (simp add: wt_start_def start_sttp_resp_cons_def split_beta)
+  apply (drule_tac x=sttp0 in spec) apply (erule exE)
+  apply (simp add: mt_sttp_flatten_def start_ST_def start_LT_def)
+
+  (* wt_instr *)
+apply (intro strip)
+apply (subgoal_tac "pc < (length bc) \<or> pc = length bc")
+apply (erule disjE)
+
+  (* pc < (length bc) *)
+apply (simp (no_asm_use) add: bc_mt_corresp_def mt_sttp_flatten_def split_beta)
+apply (erule conjE)+
+apply (drule mp, assumption)+
+apply (erule conjE)+
+apply (drule spec, drule mp, assumption)
+apply (simp add: nth_append)
+apply (simp (no_asm_simp) add: comb_def split_beta nochangeST_def)
+
+  (* pc = length bc *)
+apply (simp add: nth_append)
+
+  (* subgoal pc < (length bc) \<or> pc = length bc *)
+apply arith
+
+  (* subgoals *)
+apply (simp (no_asm_use) add: bc_mt_corresp_def split_beta)
+apply (subgoal_tac "check_type cG (length (fst sttp0)) (Suc (length pTs + mxl))
+         (OK (Some sttp0))")
+apply ((erule conjE)+, drule mp, assumption)
+apply (simp add: nth_append)
+apply (simp (no_asm_simp) add: comb_def nochangeST_def split_beta)
+apply (simp (no_asm_simp))
+
+apply (rule check_type_start, assumption+)
+done
+
+
+lemma wt_instr_Return: "\<lbrakk>fst f ! pc = Some (T # ST, LT); (G \<turnstile> T \<preceq> rT); pc < max_pc;
+  check_type (TranslComp.comp G) mxs mxr (OK (Some (T # ST, LT)))
+  \<rbrakk>
+  \<Longrightarrow> wt_instr_altern Return (comp G) rT  (mt_of f) mxs mxr max_pc empty_et pc"
+  apply (case_tac "(mt_of f ! pc)")
+  apply (simp  add: wt_instr_altern_def eff_def norm_eff_def app_def)+
+  apply (drule sym)
+  apply (simp add: comp_widen xcpt_app_def)
+  done
+
+
+theorem wt_method_comp: "
+  \<lbrakk> wf_java_prog G; (C, D, fds, mths) \<in> set G; jmdcl \<in> set mths;
+  jmdcl = ((mn,pTs), rT, jmb);
+  mt = (compTpMethod G C jmdcl);
+  (mxs, mxl, bc, et) = mtd_mb (compMethod G C jmdcl) \<rbrakk>
+  \<Longrightarrow> wt_method (comp G) C pTs rT mxs mxl bc et mt"
+
+  (* show statement for wt_method_altern *)
+apply (rule wt_method_altern_wt_method)
+
+apply (subgoal_tac "wf_java_mdecl G C jmdcl")
+apply (subgoal_tac "wf_mhead G (mn, pTs) rT")
+apply (subgoal_tac "is_class G C")
+apply (subgoal_tac "\<forall> jmb. \<exists> pns lvars blk res. jmb = (pns, lvars, blk, res)")
+   apply (drule_tac x=jmb in spec, (erule exE)+)
+apply (subgoal_tac "\<exists> E. (E = (local_env G C (mn, pTs) pns lvars) \<and> E \<turnstile> blk \<surd> \<and> 
+                         (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))")
+   apply (erule exE, (erule conjE)+)+
+apply (simp add: compMethod_def compTpMethod_def split_beta)
+apply (rule_tac T=T and LT="inited_LT C pTs lvars" and ST=start_ST in wt_method_comp_aux)
+
+  (* bc *)
+apply (simp only: append_assoc [THEN sym])
+
+  (* comb *)
+apply (simp only: comb_assoc [THEN sym])
+
+  (* bc_corresp *)
+apply (rule wt_method_comp_wo_return)
+  apply assumption+
+  apply (simp (no_asm_use) only: append_assoc)
+  apply (rule HOL.refl)
+  apply (simp (no_asm_simp))+
+  apply (simp (no_asm_simp) add: inited_LT_def)
+
+  (* start_sttp_resp *)
+apply (simp add: start_sttp_resp_cons_comb_cons_r)+
+
+  (* wf_mhead / is_class *)
+apply (simp add: wf_mhead_def comp_is_type)
+apply (simp add: comp_is_class)
+
+  (* sttp_of .. = (T # ST, LT) *)
+apply (simp (no_asm_simp) add: compTpInitLvars_LT_ST compTpExpr_LT_ST compTpStmt_LT_ST is_inited_LT_def)
+apply (subgoal_tac "(snd (compTpInitLvars (pns, lvars, blk, res) lvars
+                              (start_ST, start_LT C pTs (length lvars))))
+                = (start_ST, inited_LT C pTs lvars)") 
+   prefer 2 apply (rule compTpInitLvars_LT_ST) apply (rule HOL.refl) apply assumption
+apply (simp only:)
+apply (subgoal_tac "(snd (compTpStmt (pns, lvars, blk, res) G blk
+                       (start_ST, inited_LT C pTs lvars))) 
+                = (start_ST, inited_LT C pTs lvars)") 
+   prefer 2 apply (erule conjE)+
+   apply (rule compTpStmt_LT_ST) apply (rule HOL.refl) apply assumption+
+   apply (simp only:)+ apply (simp (no_asm_simp) add: is_inited_LT_def)
+apply (simp only:)
+apply (rule compTpExpr_LT_ST) apply (rule HOL.refl) apply assumption+
+   apply (simp only:)+ apply (simp (no_asm_simp) add: is_inited_LT_def)
+
+
+   (* Return *)
+apply (intro strip)
+apply (rule_tac T=T and ST=start_ST and LT="inited_LT C pTs lvars" in wt_instr_Return)
+apply (simp (no_asm_simp) add: nth_append 
+  length_compTpInitLvars length_compTpStmt length_compTpExpr)
+apply (simp only: compTpInitLvars_LT_ST compTpStmt_LT_ST compTpExpr_LT_ST 
+  nochangeST_def)
+apply (simp only: is_inited_LT_def compTpStmt_LT_ST compTpExpr_LT_ST)
+apply (simp (no_asm_simp))+
+apply simp
+
+  (* subgoal \<exists> E. \<dots> *)
+apply (simp add: wf_java_mdecl_def local_env_def)
+
+  (* subgoal jmb = (\<dots>) *)
+apply (simp only: split_paired_All, simp)
+
+  (* subgoal is_class / wf_mhead / wf_java_mdecl *)
+apply (rule methd [THEN conjunct2]) apply assumption+ apply (simp only:)
+apply (rule wf_prog_wf_mhead, assumption+) apply (simp only:)
+apply (rule wf_java_prog_wf_java_mdecl, assumption+)
+
+done
+
+
+  (**********************************************************************************)
+
+
+
+lemma comp_set_ms: "(C, D, fs, cms)\<in>set (comp G) 
+  \<Longrightarrow> \<exists> ms. (C, D, fs, ms) \<in>set G   \<and> cms = map (compMethod G C) ms"
+by (auto simp: comp_def compClass_def)
+
+lemma method_body_source: "\<lbrakk> wf_prog wf_mb G; is_class G C;  method (comp G, C) sig = Some (D, rT, cmb) \<rbrakk>  
+  \<Longrightarrow>  (\<exists> mb. method (G, C) sig = Some (D, rT, mb))"
+apply (simp add: comp_method_eq comp_method_result_def)
+apply (case_tac "method (G, C) sig")
+apply auto
+done
+
+
+  (* MAIN THEOREM: 
+  Methodtype computed by comp is correct for bytecode generated by compTp *)
+theorem wt_prog_comp: "wf_java_prog G  \<Longrightarrow> wt_jvm_prog (comp G) (compTp G)"
+apply (simp add: wf_prog_def)
+apply (subgoal_tac "wf_java_prog G") prefer 2 apply (simp add: wf_prog_def)
+apply (simp (no_asm_simp) add: wf_prog_def wt_jvm_prog_def)
+apply (simp add:  comp_unique comp_wf_syscls wf_cdecl_def)
+apply clarify
+apply (frule comp_set_ms)
+apply clarify
+apply (drule bspec, assumption)
+apply (simp add: comp_wf_fdecl)
+apply (simp add: wf_mdecl_def)
+
+apply (rule conjI)
+apply (rule ballI)
+apply (subgoal_tac "\<exists> sig rT mb. x = (sig, rT, mb)") prefer 2 apply (case_tac x, simp)
+apply (erule exE)+
+apply (simp (no_asm_simp) add: compMethod_def split_beta)
+apply (erule conjE)+
+apply (drule_tac x="(sig, rT, mb)" in bspec) apply simp
+apply (rule conjI)
+apply (simp add: comp_wf_mhead)
+apply (rule_tac mn="fst sig" and pTs="snd sig" in wt_method_comp)
+  apply assumption+
+  apply simp
+apply (simp (no_asm_simp) add: compTp_def)
+apply (simp (no_asm_simp) add: compMethod_def split_beta)
+apply (frule WellForm.methd) apply assumption+
+apply simp
+apply simp
+apply (simp add: compMethod_def split_beta)
+
+apply (rule conjI)
+apply (rule unique_map_fst [THEN iffD1]) 
+  apply (simp (no_asm_simp) add: compMethod_def split_beta) apply simp
+
+apply clarify
+apply (rule conjI) apply (simp add: comp_is_class)
+apply (rule conjI) apply (simp add: comp_subcls)
+apply (simp add: compMethod_def split_beta)
+apply (intro strip) 
+  apply (drule_tac x=x in bspec, assumption, drule_tac x="D'" in spec, drule_tac x="rT'" in spec)
+  apply (erule exE)
+
+apply (frule method_body_source) apply assumption+
+apply (drule mp, assumption)
+apply (simp add: comp_widen)
+done
+
+
+
+
+  (**********************************************************************************)
+
+declare split_paired_All [simp add]
+declare split_paired_Ex [simp add]
+
+
+end
diff -r b95d12325b51 -r 2950128b8206 src/HOL/MicroJava/Comp/DefsComp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/Comp/DefsComp.thy	Wed Oct 23 16:10:02 2002 +0200
@@ -0,0 +1,76 @@
+(*  Title:      HOL/MicroJava/Comp/DefsComp.thy
+    ID:         $Id$
+    Author:     Martin Strecker
+    Copyright   GPL 2002
+*)
+
+(* Definitions for accessing parts of methods, states etc. *)
+
+theory DefsComp = JVMExec:
+
+
+
+constdefs
+  method_rT :: "cname \<times> ty \<times> 'c \<Rightarrow> ty"
+  "method_rT mtd == (fst (snd mtd))"
+
+
+constdefs
+(* g = get *)
+  gx :: "xstate \<Rightarrow> val option"  "gx \<equiv> fst"
+  gs :: "xstate \<Rightarrow> state"  "gs \<equiv> snd"
+  gh :: "xstate \<Rightarrow> aheap"        "gh \<equiv> fst\<circ>snd"
+  gl :: "xstate \<Rightarrow> State.locals" "gl \<equiv> snd\<circ>snd"
+
+  gmb :: "'a prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> 'a"
+    "gmb G cn si \<equiv> snd(snd(the(method (G,cn) si)))"
+  gis :: "jvm_method \<Rightarrow> bytecode"
+    "gis \<equiv> fst \<circ> snd \<circ> snd"
+  glvs :: "java_mb \<Rightarrow> State.locals \<Rightarrow> locvars"
+    "glvs jmb loc \<equiv> map (the\<circ>loc) (gjmb_plns jmb)"
+
+(* jmb = aus einem JavaMaethodBody *)
+  gjmb_pns  :: "java_mb \<Rightarrow> vname list"     "gjmb_pns \<equiv> fst"
+  gjmb_lvs  :: "java_mb \<Rightarrow> (vname\<times>ty)list" "gjmb_lvs \<equiv> fst\<circ>snd"
+  gjmb_blk  :: "java_mb \<Rightarrow> stmt"           "gjmb_blk \<equiv> fst\<circ>snd\<circ>snd"
+  gjmb_res  :: "java_mb \<Rightarrow> expr"           "gjmb_res \<equiv> snd\<circ>snd\<circ>snd"
+  gjmb_plns :: "java_mb \<Rightarrow> vname list"
+    "gjmb_plns \<equiv> \<lambda>jmb. gjmb_pns jmb @ map fst (gjmb_lvs jmb)"
+  
+lemmas gdefs = gx_def gh_def gl_def gmb_def gis_def glvs_def
+lemmas gjmbdefs = gjmb_pns_def gjmb_lvs_def gjmb_blk_def gjmb_res_def gjmb_plns_def
+
+lemmas galldefs = gdefs gjmbdefs
+
+
+
+constdefs 
+  locvars_locals :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> State.locals \<Rightarrow> locvars"
+  "locvars_locals G C S lvs == the (lvs This) # glvs (gmb G C S) lvs"
+
+  locals_locvars :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> locvars \<Rightarrow> State.locals"
+  "locals_locvars G C S lvs == 
+  empty ((gjmb_plns (gmb G C S))[\<mapsto>](tl lvs)) (This\<mapsto>(hd lvs))"
+
+  locvars_xstate :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> xstate \<Rightarrow> locvars"
+  "locvars_xstate G C S xs == locvars_locals G C S (gl xs)"
+
+
+lemma locvars_xstate_par_dep: 
+  "lv1 = lv2 \<Longrightarrow> 
+  locvars_xstate G C S (xcpt1, hp1, lv1) = locvars_xstate G C S (xcpt2, hp2, lv2)"
+by (simp add: locvars_xstate_def gl_def)
+
+
+
+
+(**********************************************************************)
+(* Conversions *)
+
+
+lemma gx_conv [simp]: "gx (xcpt, s) = xcpt" by (simp add: gx_def)
+
+lemma gh_conv [simp]: "gh (xcpt, h, l) = h" by (simp add: gh_def)
+
+
+end
diff -r b95d12325b51 -r 2950128b8206 src/HOL/MicroJava/Comp/Index.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/Comp/Index.thy	Wed Oct 23 16:10:02 2002 +0200
@@ -0,0 +1,139 @@
+(*  Title:      HOL/MicroJava/Comp/Index.thy
+    ID:         $Id$
+    Author:     Martin Strecker
+    Copyright   GPL 2002
+*)
+
+(* Index of variable in list of parameter names and local variables *)
+
+theory Index =  AuxLemmas + DefsComp:
+
+(*indexing a variable name among all variable declarations in a method body*)
+constdefs
+ index :: "java_mb => vname => nat"
+ "index ==  \<lambda> (pn,lv,blk,res) v.
+  if v = This
+  then 0 
+  else Suc (length (takeWhile (\<lambda> z. z~=v) (pn @ map fst lv)))"
+
+
+lemma index_length_pns: "
+  \<lbrakk> i = index (pns,lvars,blk,res) vn;
+  wf_java_mdecl G C ((mn,pTs),rT, (pns,lvars,blk,res)); 
+  vn \<in> set pns\<rbrakk> 
+  \<Longrightarrow> 0 < i \<and> i < Suc (length pns)"
+apply (simp add: wf_java_mdecl_def index_def)
+apply (subgoal_tac "vn \<noteq> This")
+apply (auto intro: length_takeWhile)
+done
+
+lemma index_length_lvars: "
+  \<lbrakk> i = index (pns,lvars,blk,res) vn;
+  wf_java_mdecl G C ((mn,pTs),rT, (pns,lvars,blk,res)); 
+  vn \<in> set (map fst lvars)\<rbrakk> 
+  \<Longrightarrow> (length pns) < i \<and> i < Suc((length pns) + (length lvars))"
+apply (simp add: wf_java_mdecl_def index_def)
+apply (subgoal_tac "vn \<noteq> This")
+apply simp
+apply (subgoal_tac "\<forall> x \<in> set pns. (\<lambda>z. z \<noteq> vn) x")
+apply (simp add: takeWhile_append2)
+apply (subgoal_tac "length (takeWhile (\<lambda>z. z \<noteq> vn) (map fst lvars)) < length (map fst lvars)")
+apply simp
+apply (rule length_takeWhile)
+apply simp
+apply (simp add: map_of_in_set)
+apply (intro strip notI) apply simp apply blast
+done
+
+
+(***  index  ***)
+
+lemma select_at_index : 
+  "x \<in> set (gjmb_plns (gmb G C S)) \<or> x = This 
+  \<Longrightarrow> (the (loc This) # glvs (gmb G C S) loc) ! (index (gmb G C S) x) = 
+     the (loc x)"
+apply (simp only: index_def gjmb_plns_def)
+apply (case_tac "(gmb G C S)")
+apply (simp add: galldefs del: set_append map_append)
+apply (case_tac b, simp add: gmb_def gjmb_lvs_def del: set_append map_append)
+apply (intro strip)
+apply (simp del: set_append map_append)
+apply (frule length_takeWhile)
+apply (frule_tac f = "(the \<circ> loc)" in nth_map)
+apply simp
+done
+
+lemma update_at_index: "
+  \<lbrakk> distinct (gjmb_plns (gmb G C S)); 
+  x \<in> set (gjmb_plns (gmb G C S)); x \<noteq> This \<rbrakk> \<Longrightarrow> 
+  locvars_xstate G C S (Norm (h, l))[index (gmb G C S) x := val] =
+          locvars_xstate G C S (Norm (h, l(x\<mapsto>val)))"
+apply (simp only: locvars_xstate_def locvars_locals_def index_def)
+apply (case_tac "(gmb G C S)", simp)
+apply (case_tac b, simp)
+apply (rule conjI)
+apply (simp add: gl_def)
+apply (intro strip, simp)
+apply (simp add: galldefs del: set_append map_append)
+apply (auto simp: the_map_upd)
+done
+
+
+(* !!!! incomprehensible: why can't List.takeWhile_append2 be applied the same 
+  way in the second case as in the first case ? *)
+lemma index_of_var: "\<lbrakk> xvar \<notin> set pns; xvar \<notin> set (map fst zs); xvar \<noteq> This \<rbrakk>
+  \<Longrightarrow> index (pns, zs @ ((xvar, xval) # xys), blk, res) xvar = Suc (length pns + length zs)"
+apply (simp add: index_def)
+apply (subgoal_tac "(\<And>x. ((x \<in> (set pns)) \<Longrightarrow> ((\<lambda>z. (z \<noteq> xvar))x)))")
+apply (simp add: List.takeWhile_append2)
+apply (subgoal_tac "(takeWhile (\<lambda>z. z \<noteq> xvar) (map fst zs @ xvar # map fst xys)) = map fst zs @ (takeWhile (\<lambda>z. z \<noteq> xvar) (xvar # map fst xys))")
+apply simp
+apply (rule List.takeWhile_append2)
+apply auto
+done
+
+
+
+
+(* The following def should replace the conditions in WellType.thy / wf_java_mdecl
+*)
+constdefs 
+  disjoint_varnames :: "[vname list, (vname \<times> ty) list] \<Rightarrow> bool"
+(* This corresponds to the original def in wf_java_mdecl:
+  "disjoint_varnames pns lvars \<equiv> 
+  nodups pns \<and> unique lvars \<and> This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and> 
+	(\<forall>pn\<in>set pns. map_of lvars pn = None)"
+*)
+
+  "disjoint_varnames pns lvars \<equiv> 
+  distinct pns \<and> unique lvars \<and> This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and> 
+  (\<forall>pn\<in>set pns. pn \<notin> set (map fst lvars))"
+
+
+lemma index_of_var2: "
+  disjoint_varnames pns (lvars_pre @ (vn, ty) # lvars_post)
+  \<Longrightarrow> index (pns, lvars_pre @ (vn, ty) # lvars_post, blk, res) vn =
+  Suc (length pns + length lvars_pre)"
+apply (simp add: disjoint_varnames_def index_def unique_def distinct_append)
+apply (subgoal_tac "vn \<noteq> This", simp)
+apply (subgoal_tac
+  "takeWhile (\<lambda>z. z \<noteq> vn) (map fst lvars_pre @ vn # map fst lvars_post) =
+  map fst lvars_pre @ takeWhile (\<lambda>z. z \<noteq> vn) (vn # map fst lvars_post)")
+apply simp 
+apply (rule List.takeWhile_append2)
+apply auto
+done
+
+lemma wf_java_mdecl_disjoint_varnames: 
+  "wf_java_mdecl G C (S,rT,(pns,lvars,blk,res)) 
+  \<Longrightarrow> disjoint_varnames pns lvars"
+apply (case_tac S)
+apply (simp add: wf_java_mdecl_def disjoint_varnames_def  map_of_in_set)
+done
+
+lemma wf_java_mdecl_length_pTs_pns: 
+  "wf_java_mdecl G C ((mn, pTs), rT, pns, lvars, blk, res)
+  \<Longrightarrow> length pTs = length pns"
+by (simp add: wf_java_mdecl_def)
+
+end
diff -r b95d12325b51 -r 2950128b8206 src/HOL/MicroJava/Comp/LemmasComp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Wed Oct 23 16:10:02 2002 +0200
@@ -0,0 +1,429 @@
+(*  Title:      HOL/MicroJava/Comp/LemmasComp.thy
+    ID:         $Id$
+    Author:     Martin Strecker
+    Copyright   GPL 2002
+*)
+
+(* Lemmas for compiler correctness proof *)
+
+theory LemmasComp = TranslComp:
+
+(**********************************************************************)
+(* misc lemmas *)
+
+lemma split_pairs: "(\<lambda>(a,b). (F a b)) (ab) = F (fst ab) (snd ab)"
+proof -
+  have "(\<lambda>(a,b). (F a b)) (fst ab,snd ab) = F (fst ab) (snd ab)"
+    by (simp add: split_def)
+  then show ?thesis by simp
+qed
+
+
+lemma c_hupd_conv: 
+  "c_hupd h' (xo, (h,l)) = (xo, (if xo = None then h' else h),l)"
+by (simp add: c_hupd_def)
+
+lemma gl_c_hupd [simp]: "(gl (c_hupd h xs)) = (gl xs)"
+by (simp add: gl_def c_hupd_def split_pairs)
+
+lemma c_hupd_xcpt_invariant [simp]: "gx (c_hupd h' (xo, st)) = xo"
+by (case_tac st, simp only: c_hupd_conv gx_conv)
+
+(* not added to simpset because of interference with c_hupd_conv *)
+lemma c_hupd_hp_invariant: "gh (c_hupd hp (None, st)) = hp"
+by (case_tac st, simp add: c_hupd_conv gh_def)
+
+
+(**********************************************************************)
+(* invariance of properties under compilation *)
+
+lemma comp_class_imp:
+  "(class G C = Some(D, fs, ms)) \<Longrightarrow> 
+  (class (comp G) C = Some(D, fs, map (compMethod G C) ms))"
+apply (simp add: class_def comp_def compClass_def)
+apply (rule HOL.trans)
+apply (rule map_of_map2)
+apply auto
+done
+
+lemma comp_class_None: 
+"(class G C = None) = (class (comp G) C = None)"
+apply (simp add: class_def comp_def compClass_def)
+apply (simp add: map_of_in_set)
+apply (simp add: image_compose [THEN sym] o_def split_beta del: image_compose)
+done
+
+lemma comp_is_class: "is_class G C = is_class (comp G) C"
+by (case_tac "class G C", auto simp: is_class_def comp_class_None dest: comp_class_imp)
+
+
+lemma comp_is_type: "is_type G T = is_type (comp G) T"
+  by ((cases T),simp,(induct G)) ((simp),(simp only: comp_is_class),(simp add: comp_is_class),(simp only: comp_is_class))
+
+lemma SIGMA_cong: "\<lbrakk> A = B; !!x. x \<in> B \<Longrightarrow> C x = D x \<rbrakk> \<Longrightarrow> (\<Sigma> x \<in> A. C x) = (\<Sigma> x \<in> B. D x)"
+by auto
+
+lemma comp_classname: "is_class G C \<Longrightarrow> fst (the (class G C)) = fst (the (class (comp G) C))"
+by (case_tac "class G C", auto simp: is_class_def dest: comp_class_imp)
+
+
+lemma comp_subcls1: "subcls1 G = subcls1 (comp G)"
+apply (simp add: subcls1_def2 comp_is_class)
+apply (rule SIGMA_cong, simp)
+apply (simp add: comp_is_class [THEN sym])
+apply (simp add: comp_classname)
+done
+
+lemma comp_subcls: "(subcls1 G)^* = (subcls1 (comp G))^*"
+  by (induct G) (simp_all add: comp_def comp_subcls1)
+
+lemma comp_widen: "((ty1,ty2) \<in> widen G) = ((ty1,ty2) \<in> widen (comp G))"
+  apply rule
+  apply (cases "(ty1,ty2)" G rule: widen.cases) 
+  apply (simp_all add: comp_subcls widen.null)
+  apply (cases "(ty1,ty2)" "comp G" rule: widen.cases) 
+  apply (simp_all add: comp_subcls widen.null)
+  done
+
+lemma comp_cast: "((ty1,ty2) \<in> cast G) = ((ty1,ty2) \<in> cast (comp G))"
+  apply rule
+  apply (cases "(ty1,ty2)" G rule: cast.cases)
+  apply (simp_all add: comp_subcls cast.widen cast.subcls)
+  apply (cases "(ty1,ty2)" "comp G" rule: cast.cases) 
+  apply (simp_all add: comp_subcls cast.widen cast.subcls)
+  done
+
+lemma comp_cast_ok: "cast_ok G = cast_ok (comp G)"
+  by (simp add: expand_fun_eq cast_ok_def comp_widen)
+
+
+lemma comp_wf_fdecl: "wf_fdecl G fd  \<Longrightarrow> wf_fdecl (comp G) fd"
+apply (case_tac fd)
+apply (simp add: wf_fdecl_def comp_is_type)
+done
+
+lemma comp_wf_syscls: "wf_syscls G = wf_syscls (comp G)"
+apply (simp add: wf_syscls_def comp_def compClass_def split_beta)
+apply (simp only: image_compose [THEN sym])
+apply (subgoal_tac "(Fun.comp fst (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls). (C, cno, fdls, map (compMethod G C) jmdls))) = fst")
+(*
+apply (subgoal_tac "(fst o (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls). (C, cno, fdls, map (compMethod G C) jmdls))) = fst")
+*)
+apply (simp del: image_compose)
+apply (simp add: expand_fun_eq split_beta)
+done
+
+
+lemma comp_wf_mhead: "wf_mhead G S rT =  wf_mhead (comp G) S rT"
+by (simp add: wf_mhead_def split_beta comp_is_type)
+
+lemma comp_wf_mdecl: "\<lbrakk> wf_mdecl wf_mb G C jmdl;
+  (wf_mb G C jmdl) \<longrightarrow> (wf_mb_comp (comp G) C (compMethod G C jmdl)) \<rbrakk> 
+ \<Longrightarrow> 
+  wf_mdecl wf_mb_comp (comp G) C (compMethod G C jmdl)"
+by (simp add: wf_mdecl_def wf_mhead_def comp_is_type split_beta compMethod_def)
+
+
+lemma comp_class_rec: " wf ((subcls1 G)^-1) \<Longrightarrow> 
+class_rec (comp G) C t f = 
+  class_rec G C t (\<lambda> C' fs' ms' r'. f C' fs' (map (compMethod G C') ms') r')"
+apply (rule_tac a = C in  wf_induct) apply assumption
+apply (subgoal_tac "wf ((subcls1 (comp G))\<inverse>)")
+apply (subgoal_tac "(class G x = None) \<or> (\<exists> D fs ms. (class G x = Some (D, fs, ms)))")
+apply (erule disjE)
+
+  (* case class G x = None *)
+apply (simp (no_asm_simp) add: class_rec_def comp_subcls1 wfrec cut_apply)
+apply (simp add: comp_class_None)
+
+  (* case \<exists> D fs ms. (class G x = Some (D, fs, ms)) *)
+apply (erule exE)+
+apply (frule comp_class_imp)
+apply (frule_tac G="comp G" and C=x and t=t and f=f in class_rec_lemma)
+  apply assumption
+apply (frule_tac G=G and C=x and t=t 
+   and f="(\<lambda>C' fs' ms'. f C' fs' (map (compMethod G C') ms'))" in class_rec_lemma)
+  apply assumption
+apply (simp only:)
+
+apply (case_tac "x = Object")
+  apply simp
+  apply (frule subcls1I, assumption)
+    apply (drule_tac x=D in spec, drule mp, simp)
+    apply simp
+
+  (* subgoals *)
+apply (case_tac "class G x")
+apply auto
+apply (simp add: comp_subcls1)
+done
+
+lemma comp_fields: "wf ((subcls1 G)^-1) \<Longrightarrow> 
+  fields (G,C) = fields (comp G,C)" 
+by (simp add: fields_def comp_class_rec)
+
+lemma comp_field: "wf ((subcls1 G)^-1) \<Longrightarrow> 
+  field (G,C) = field (comp G,C)" 
+by (simp add: field_def comp_fields)
+
+
+
+lemma class_rec_relation [rule_format (no_asm)]: "\<lbrakk>  wf_prog wf_mb G;
+  \<forall> fs ms. R (f1 Object fs ms t1) (f2 Object fs ms t2);
+   \<forall> C fs ms r1 r2. (R r1 r2) \<longrightarrow> (R (f1 C fs ms r1) (f2 C fs ms r2)) \<rbrakk>
+  \<Longrightarrow> ((class G C) \<noteq> None) \<longrightarrow> 
+  R (class_rec G C t1 f1) (class_rec G C t2 f2)"
+apply (frule wf_subcls1) (* establish wf ((subcls1 G)^-1) *)
+apply (rule_tac a = C in  wf_induct) apply assumption
+apply (intro strip)
+apply (subgoal_tac "(\<exists>D rT mb. class G x = Some (D, rT, mb))")
+  apply (erule exE)+
+apply (frule_tac C=x and t=t1 and f=f1 in class_rec_lemma)
+  apply assumption
+apply (frule_tac C=x and t=t2 and f=f2 in class_rec_lemma)
+  apply assumption
+apply (simp only:)
+
+apply (case_tac "x = Object")
+  apply simp
+  apply (frule subcls1I, assumption)
+    apply (drule_tac x=D in spec, drule mp, simp)
+    apply simp
+    apply (subgoal_tac "(\<exists>D' rT' mb'. class G D = Some (D', rT', mb'))")
+    apply blast
+
+  (* subgoals *)
+
+apply (frule class_wf) apply assumption
+apply (simp add: wf_cdecl_def is_class_def)
+
+apply (simp add: subcls1_def2 is_class_def)
+done
+
+
+syntax
+  mtd_mb :: "cname \<times> ty \<times> 'c \<Rightarrow> 'c"
+translations
+  "mtd_mb" => "Fun.comp snd snd"
+
+
+lemma map_of_map_fst: "\<lbrakk> map_of (map f xs) k = Some e; inj f;
+  \<forall>x\<in>set xs. fst (f x) = fst x; \<forall>x\<in>set xs. fst (g x) = fst x \<rbrakk>
+  \<Longrightarrow>  map_of (map g xs) k = Some (snd (g ((inv f) (k, e))))"
+apply (induct xs)
+apply simp
+apply (simp del: split_paired_All)
+apply (case_tac "k = fst a")
+apply (simp del: split_paired_All)
+apply (subgoal_tac "(fst a, e)  = f a")
+apply simp
+apply (rule_tac s= "(fst (f a), snd (f a))" in trans)
+apply simp
+apply (rule surjective_pairing [THEN sym])
+apply (simp del: split_paired_All)
+done
+
+
+lemma comp_method [rule_format (no_asm)]: "\<lbrakk> wf_prog wf_mb G; is_class G C\<rbrakk> \<Longrightarrow> 
+  (method (G, C) S) = Some (D, rT, mb) \<longrightarrow> 
+  (method (comp G, C) S) = Some (D, rT, mtd_mb (compMethod G D (S, rT, mb)))"
+apply (simp add: method_def)
+apply (frule wf_subcls1)
+apply (simp add: comp_class_rec)
+apply (simp add: map_compose [THEN sym] split_iter split_compose del: map_compose)
+apply (rule_tac R="%x y. (x S) = Some (D, rT, mb) \<longrightarrow> (y S) = Some (D, rT, snd (snd (compMethod G D (S, rT, mb))))" in  class_rec_relation) apply assumption
+
+apply (intro strip)
+apply simp
+
+apply (frule_tac f="(\<lambda>(s, m). (s, Object, m))" 
+  and g="(Fun.comp (\<lambda>(s, m). (s, Object, m)) (compMethod G Object))" in map_of_map_fst)
+(*
+apply (frule_tac f="(\<lambda>(s, m). (s, Object, m))" 
+  and g="((\<lambda>(s, m). (s, Object, m)) \<circ> compMethod G Object)" in map_of_map_fst)
+*)
+apply (simp add: inj_on_def)
+apply (simp add: split_beta compMethod_def)
+apply (simp add: split_beta compMethod_def)
+apply (simp only:)
+apply (subgoal_tac "(inv (\<lambda>(s, m). (s, Object, m)) (S, D, rT, mb)) = (S, rT, mb)")
+apply (simp only:)
+apply (simp add: compMethod_def split_beta)
+apply (simp add: map_of_map) apply (erule exE)+ apply simp
+apply (simp add: map_of_map) apply (erule exE)+ apply simp
+apply (rule inv_f_eq) apply (simp add: inj_on_def) apply simp
+
+apply (intro strip)
+apply (simp add: override_Some_iff map_of_map del: split_paired_Ex)
+apply (subgoal_tac "\<forall>x\<in>set ms. fst ((Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca)) x) = fst x")
+(*
+apply (subgoal_tac "\<forall>x\<in>set ms. fst (((\<lambda>(s, m). (s, Ca, m)) \<circ> compMethod G Ca) x) = fst x")
+*)
+apply (erule disjE)
+apply (rule disjI1)
+apply (simp add: map_of_map2)
+apply (simp (no_asm_simp) add: compMethod_def split_beta)
+
+apply (rule disjI2)
+apply (simp add: map_of_map2)
+
+  -- "subgoal"
+apply (simp (no_asm_simp) add: compMethod_def split_beta)
+
+apply (simp add: is_class_def)
+done
+
+
+constdefs comp_method_result :: "java_mb prog \<Rightarrow> sig \<Rightarrow> 
+  (cname \<times> ty \<times> java_mb) option \<Rightarrow> (cname \<times> ty \<times> jvm_method) option"
+  "comp_method_result G S m ==  case m of 
+    None \<Rightarrow> None
+  | Some (D, rT, mb) \<Rightarrow> Some (D, rT, mtd_mb (compMethod G D (S, rT, mb)))"
+
+
+lemma map_of_map_compMethod: "map_of (map (\<lambda>(s, m). (s, C, m)) (map (compMethod G C) ms)) S =
+          (case map_of (map (\<lambda>(s, m). (s, C, m)) ms) S of None \<Rightarrow> None
+           | Some (D, rT, mb) \<Rightarrow> Some (D, rT, mtd_mb (compMethod G D (S, rT, mb))))"
+apply (induct ms)
+apply simp
+apply (simp only: map_compose [THEN sym])
+apply (simp add: o_def split_beta del: map.simps)
+apply (simp (no_asm_simp) only: map.simps map_of.simps)
+apply (simp add: compMethod_def split_beta)
+done
+
+  (* the following is more expressive than comp_method and should replace it *)
+lemma comp_method_eq [rule_format (no_asm)]: "wf_prog wf_mb G \<Longrightarrow> is_class G C \<longrightarrow>
+method (comp G, C) S = comp_method_result G S (method (G,C) S)"
+apply (subgoal_tac "wf ((subcls1 G)^-1)") prefer 2 apply (rule wf_subcls1, assumption) 
+
+apply (rule subcls_induct)
+apply assumption
+apply (intro strip)
+apply (subgoal_tac "\<exists> D fs ms. class G C = Some (D, fs, ms)") 
+   prefer 2 apply (simp add: is_class_def)
+apply (erule exE)+
+
+apply (case_tac "C = Object")
+
+  (* C = Object *)
+apply (subst method_rec_lemma) apply assumption+ apply simp 
+apply (subst method_rec_lemma) apply (frule comp_class_imp) apply assumption+ 
+   apply (simp add: comp_subcls1) 
+apply (simp add: comp_method_result_def)
+apply (rule map_of_map_compMethod) 
+
+  (* C \<noteq> Object *)
+apply (subgoal_tac "(C, D) \<in> (subcls1 G)\<^sup>+") 
+   prefer 2 apply (frule subcls1I, assumption+) apply blast
+apply (subgoal_tac "is_class G D")
+apply (drule spec, drule mp, assumption, drule mp, assumption)
+apply (frule wf_subcls1) 
+apply (subgoal_tac "wf ((subcls1 (comp G))\<inverse>)")
+apply (frule_tac G=G in method_rec_lemma, assumption)
+apply (frule comp_class_imp)
+apply (frule_tac G="comp G" in method_rec_lemma, assumption)
+apply (simp only:)
+apply (simp (no_asm_simp) add: comp_method_result_def expand_fun_eq)
+
+apply (case_tac "(method (G, D) ++  map_of (map (\<lambda>(s, m). (s, C, m)) ms)) S")
+
+  (* case None *)
+apply (simp (no_asm_simp) add: override_None)
+apply (simp add: map_of_map_compMethod comp_method_result_def) 
+
+  (* case Some *)
+apply (simp add: override_Some_iff)
+apply (erule disjE)
+  apply (simp add: split_beta map_of_map_compMethod)
+  apply (simp add: override_def comp_method_result_def map_of_map_compMethod)
+
+  (* show subgoals *)
+apply (simp add: comp_subcls1) 
+  (* show is_class G D *)
+apply (simp add: wf_prog_def wf_cdecl_def)
+apply (subgoal_tac "(C, D, fs, ms)\<in>set G")
+apply blast
+apply (simp add: class_def map_of_SomeD)
+done
+
+  (* ### this proof is horrid and has to be redone *)
+lemma unique_map_fst [rule_format]: "(\<forall> x \<in> set xs. (fst x = fst (f x) )) \<longrightarrow>
+  unique xs = unique (map f xs)"
+apply (induct_tac "xs")
+apply simp
+apply (intro strip)
+apply simp
+apply (case_tac a, simp)
+apply (case_tac "f (aa, b)")
+apply (simp only:)
+apply (simp only: unique_Cons)
+
+apply simp
+apply (subgoal_tac "(\<exists>y. (ab, y) \<in> set list) = (\<exists>y. (ab, y) \<in> f ` set list)")
+apply blast
+apply (rule iffI)
+
+apply clarify
+apply (rule_tac x="(snd (f(ab, y)))" in exI)
+apply simp
+apply (subgoal_tac "(ab, snd (f (ab, y))) = (fst (f (ab, y)), snd (f (ab, y)))")
+apply (simp only:)
+apply (simp add: surjective_pairing [THEN sym])
+apply (subgoal_tac "fst (f (ab, y)) = fst (ab, y)")
+apply simp
+apply (drule bspec) apply assumption apply simp
+
+apply clarify
+apply (drule bspec) apply assumption apply simp
+apply (subgoal_tac "ac = ab")
+apply simp
+apply blast
+apply (drule sym)
+apply (drule sym)
+apply (drule_tac f=fst in arg_cong)
+apply simp
+done
+
+lemma comp_unique: "unique G = unique (comp G)"
+apply (simp add: comp_def)
+apply (rule unique_map_fst)
+apply (simp add: compClass_def split_beta)
+done
+
+
+(**********************************************************************)
+  (* DIVERSE OTHER LEMMAS *)
+(**********************************************************************)
+
+
+(* already proved less elegantly in CorrComp.thy;
+  to be moved into a common super-theory *)
+lemma max_spec_preserves_length:
+  "max_spec G C (mn, pTs) = {((md,rT),pTs')} 
+  \<Longrightarrow> length pTs = length pTs'"
+apply (frule max_spec2mheads)
+apply (erule exE)+
+apply (simp add: list_all2_def)
+done
+
+
+(* already proved in CorrComp.thy \<longrightarrow> into common supertheory *)
+lemma ty_exprs_length [simp]: "(E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts)"
+apply (subgoal_tac "(E\<turnstile>e::T \<longrightarrow> True) \<and> (E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts) \<and> (E\<turnstile>s\<surd> \<longrightarrow> True)")
+apply blast
+apply (rule ty_expr_ty_exprs_wt_stmt.induct)
+apply auto
+done
+
+
+lemma max_spec_preserves_method_rT [simp]:
+  "max_spec G C (mn, pTs) = {((md,rT),pTs')}
+  \<Longrightarrow> method_rT (the (method (G, C) (mn, pTs'))) = rT"
+apply (frule max_spec2mheads)
+apply (erule exE)+
+apply (simp add: method_rT_def)
+done
+
+
+end
diff -r b95d12325b51 -r 2950128b8206 src/HOL/MicroJava/Comp/NatCanonify.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/Comp/NatCanonify.thy	Wed Oct 23 16:10:02 2002 +0200
@@ -0,0 +1,44 @@
+(*  Title:      HOL/MicroJava/Comp/NatCanonify.thy
+    ID:         $Id$
+    Author:     Martin Strecker
+    Copyright   GPL 2002
+*)
+
+theory NatCanonify = Main:
+
+(************************************************************************)
+  (* Canonizer for converting nat to int *)
+(************************************************************************)
+
+lemma nat_add_canonify: "(n1::nat) + n2 = nat ((int n1) + (int n2))"
+by (simp add: nat_add_distrib)
+
+lemma nat_mult_canonify: "(n1::nat) * n2 = nat ((int n1) * (int n2))"
+by (simp add: nat_mult_distrib)
+
+lemma nat_diff_canonify: "(n1::nat) - n2 = 
+  nat (if (int n1) \<le> (int n2) then 0 else (int n1) - (int n2))"
+by (simp add: zdiff_int nat_int)
+
+lemma nat_le_canonify: "((n1::nat) \<le> n2) = ((int n1) \<le> (int n2))"
+by arith
+
+lemma nat_less_canonify: "((n1::nat) < n2) = ((int n1) < (int n2))"
+by arith
+
+lemma nat_eq_canonify: "((n1::nat) = n2) = ((int n1) = (int n2))"
+by arith
+
+lemma nat_if_canonify: "(if b then (n1::nat) else n2) =
+  nat (if b then (int n1) else (int n2))"
+by simp
+
+lemma int_nat_canonify: "(int (nat n)) = (if 0 \<le> n then n else 0)"
+by simp
+
+lemmas nat_canonify = 
+  nat_add_canonify nat_mult_canonify nat_diff_canonify 
+  nat_le_canonify nat_less_canonify nat_eq_canonify nat_if_canonify 
+  int_nat_canonify nat_int
+
+end
diff -r b95d12325b51 -r 2950128b8206 src/HOL/MicroJava/Comp/TranslComp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/Comp/TranslComp.thy	Wed Oct 23 16:10:02 2002 +0200
@@ -0,0 +1,130 @@
+(*  Title:      HOL/MicroJava/Comp/TranslComp.thy
+    ID:         $Id$
+    Author:     Martin Strecker
+    Copyright   GPL 2002
+*)
+
+(* Compiling MicroJava into MicroJVM -- Translation functions *)
+
+theory TranslComp =  TranslCompTp:
+
+
+(* parameter java_mb only serves to define function index later *)
+consts
+ compExpr  :: "java_mb => expr      => instr list"
+ compExprs :: "java_mb => expr list => instr list"
+ compStmt  :: "java_mb => stmt      => instr list"
+
+
+
+(**********************************************************************)
+(** code generation for expressions **)
+
+primrec
+(*class instance creation*)
+"compExpr jmb (NewC c) = [New c]"
+
+(*type cast*)
+"compExpr jmb (Cast c e) = compExpr jmb e @ [Checkcast c]" 
+
+
+(*literals*)
+"compExpr jmb (Lit val) = [LitPush val]" 
+
+      
+(* binary operation *)                         
+"compExpr jmb (BinOp bo e1 e2) = compExpr jmb e1 @ compExpr jmb e2 @ 
+  (case bo of Eq => [Ifcmpeq 3,LitPush(Bool False),Goto 2,LitPush(Bool True)]
+            | Add => [IAdd])" 
+
+(*local variable*)
+"compExpr jmb (LAcc vn) = [Load (index jmb vn)]" 
+
+
+(*assignement*)
+"compExpr jmb (vn::=e) = compExpr jmb e @ [Dup , Store (index jmb vn)]" 
+
+
+(*field access*)
+"compExpr jmb ( {cn}e..fn ) = compExpr jmb e @ [Getfield fn cn]"
+
+
+(*field assignement - expected syntax:  {_}_.._:=_ *)
+"compExpr jmb (FAss cn e1 fn e2 ) = 
+       compExpr jmb e1 @ compExpr jmb e2 @ [Dup_x1 , Putfield fn cn]"
+
+
+(*method call*)
+"compExpr jmb (Call cn e1 mn X ps) = 
+        compExpr jmb e1 @ compExprs jmb ps @ [Invoke cn mn X]"
+
+
+(** code generation expression lists **)
+
+"compExprs jmb []     = []"
+
+"compExprs jmb (e#es) = compExpr jmb e @ compExprs jmb es"
+
+  
+
+primrec
+(** code generation for statements **)
+
+"compStmt jmb Skip = []"			
+
+"compStmt jmb (Expr e) = ((compExpr jmb e) @ [Pop])"
+
+"compStmt jmb (c1;; c2) = ((compStmt jmb c1) @ (compStmt jmb c2))"
+
+"compStmt jmb (If(e) c1 Else c2) =
+	(let cnstf = LitPush (Bool False);
+             cnd   = compExpr jmb e;
+	     thn   = compStmt jmb c1;
+	     els   = compStmt jmb c2;
+	     test  = Ifcmpeq (int(length thn +2)); 
+	     thnex = Goto (int(length els +1))
+	 in
+	 [cnstf] @ cnd @ [test] @ thn @ [thnex] @ els)"
+
+"compStmt jmb (While(e) c) =
+	(let cnstf = LitPush (Bool False);
+             cnd   = compExpr jmb e;
+	     bdy   = compStmt jmb c;
+	     test  = Ifcmpeq (int(length bdy +2)); 
+	     loop  = Goto (-(int((length bdy) + (length cnd) +2)))
+	 in
+	 [cnstf] @ cnd @ [test] @ bdy @ [loop])"
+
+(**********************************************************************)
+
+(*compiling methods, classes and programs*) 
+
+(*initialising a single variable*)
+constdefs
+ load_default_val :: "ty => instr"
+"load_default_val ty == LitPush (default_val ty)"
+
+ compInit :: "java_mb => (vname * ty) => instr list"
+"compInit jmb == \<lambda> (vn,ty). [load_default_val ty, Store (index jmb vn)]"
+
+ compInitLvars :: "[java_mb, (vname \<times> ty) list] \<Rightarrow> bytecode"
+ "compInitLvars jmb lvars == concat (map (compInit jmb) lvars)"
+
+  compMethod :: "java_mb prog \<Rightarrow> cname \<Rightarrow> java_mb mdecl \<Rightarrow> jvm_method mdecl"
+  "compMethod G C jmdl == let (sig, rT, jmb) = jmdl;
+                        (pns,lvars,blk,res) = jmb;
+                        mt = (compTpMethod G C jmdl);
+                        bc = compInitLvars jmb lvars @ 
+                             compStmt jmb blk @ compExpr jmb res @
+                             [Return]
+                  in (sig, rT, max_ssize mt, length lvars, bc, [])"
+
+  compClass :: "java_mb prog => java_mb cdecl=> jvm_method cdecl"
+  "compClass G == \<lambda> (C,cno,fdls,jmdls). (C,cno,fdls, map (compMethod G C) jmdls)"
+
+  comp :: "java_mb prog => jvm_prog"
+  "comp G == map (compClass G) G"
+
+end
+
+
diff -r b95d12325b51 -r 2950128b8206 src/HOL/MicroJava/Comp/TranslCompTp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/Comp/TranslCompTp.thy	Wed Oct 23 16:10:02 2002 +0200
@@ -0,0 +1,191 @@
+(*  Title:      HOL/MicroJava/Comp/TranslCompTp.thy
+    ID:         $Id$
+    Author:     Martin Strecker
+    Copyright   GPL 2002
+*)
+
+theory TranslCompTp =  JVMType + Index:
+
+
+(**********************************************************************)
+
+
+constdefs
+  comb :: "['a \<Rightarrow> 'b list \<times> 'c, 'c \<Rightarrow> 'b list \<times> 'd, 'a] \<Rightarrow> 'b list \<times> 'd" 
+  "comb == (\<lambda> f1 f2 x0. let (xs1, x1) = f1 x0; 
+                            (xs2, x2) = f2 x1 
+                        in  (xs1 @ xs2, x2))"
+  comb_nil :: "'a \<Rightarrow> 'b list \<times> 'a"
+  "comb_nil a == ([], a)"
+
+syntax (xsymbols)
+  "comb" :: "['a \<Rightarrow> 'b list \<times> 'c, 'c \<Rightarrow> 'b list \<times> 'd, 'a] \<Rightarrow> 'b list \<times> 'd"    
+            (infixr "\<box>" 55)
+
+lemma comb_nil_left [simp]: "comb_nil \<box> f = f"
+by (simp add: comb_def comb_nil_def split_beta)
+
+lemma comb_nil_right [simp]: "f \<box> comb_nil = f"
+by (simp add: comb_def comb_nil_def split_beta)
+
+lemma comb_assoc [simp]: "(fa \<box> fb) \<box> fc = fa \<box> (fb \<box> fc)"
+by (simp add: comb_def split_beta)
+
+lemma comb_inv: "(xs', x') = (f1 \<box> f2) x0 \<Longrightarrow>
+  \<exists> xs1 x1 xs2 x2. (xs1, x1) = (f1 x0) \<and> (xs2, x2) = f2 x1 \<and> xs'= xs1 @ xs2 \<and> x'=x2"
+apply (case_tac "f1 x0")
+apply (case_tac "f2 x1")
+apply (simp add: comb_def split_beta)
+done
+
+(**********************************************************************)
+
+syntax
+  mt_of		:: "method_type \<times> state_type \<Rightarrow> method_type"
+  sttp_of	:: "method_type \<times> state_type \<Rightarrow> state_type"
+
+translations
+  "mt_of"     => "fst"
+  "sttp_of"   => "snd"
+
+consts
+  compTpExpr  :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr
+                   \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
+
+  compTpExprs :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr list
+                   \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
+
+  compTpStmt  :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> stmt
+                   \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
+
+
+constdefs
+  nochangeST :: "state_type \<Rightarrow> method_type \<times> state_type"
+  "nochangeST sttp == ([Some sttp], sttp)"
+  pushST :: "[ty list, state_type] \<Rightarrow> method_type \<times> state_type"
+  "pushST tps == (\<lambda> (ST, LT). ([Some (ST, LT)], (tps @ ST, LT)))"
+  dupST :: "state_type \<Rightarrow> method_type \<times> state_type"
+  "dupST == (\<lambda> (ST, LT). ([Some (ST, LT)], (hd ST # ST, LT)))"
+  dup_x1ST :: "state_type \<Rightarrow> method_type \<times> state_type"
+  "dup_x1ST == (\<lambda> (ST, LT). ([Some (ST, LT)], 
+                             (hd ST # hd (tl ST) # hd ST # (tl (tl ST)), LT)))"
+  popST :: "[nat, state_type] \<Rightarrow> method_type \<times> state_type"
+  "popST n == (\<lambda> (ST, LT). ([Some (ST, LT)], (drop n ST, LT)))"
+  replST :: "[nat, ty, state_type] \<Rightarrow> method_type \<times> state_type"
+  "replST n tp == (\<lambda> (ST, LT). ([Some (ST, LT)], (tp # (drop n ST), LT)))"
+
+  storeST :: "[nat, ty, state_type] \<Rightarrow> method_type \<times> state_type"
+  "storeST i tp == (\<lambda> (ST, LT). ([Some (ST, LT)], (tl ST, LT [i:= OK tp])))"
+
+
+(* Expressions *)
+
+primrec
+
+  "compTpExpr jmb G (NewC c) = pushST [Class c]"
+
+  "compTpExpr jmb G (Cast c e) = 
+  (compTpExpr jmb G e) \<box> (replST 1 (Class c))"
+
+  "compTpExpr jmb G (Lit val) = pushST [the (typeof (\<lambda>v. None) val)]"
+
+  "compTpExpr jmb G (BinOp bo e1 e2) = 
+     (compTpExpr jmb G e1) \<box> (compTpExpr jmb G e2) \<box> 
+     (case bo of 
+       Eq => popST 2 \<box> pushST [PrimT Boolean] \<box> popST 1 \<box> pushST [PrimT Boolean]
+     | Add => replST 2 (PrimT Integer))"
+
+  "compTpExpr jmb G (LAcc vn) = (\<lambda> (ST, LT). 
+      pushST [ok_val (LT ! (index jmb vn))] (ST, LT))"
+
+  "compTpExpr jmb G (vn::=e) = 
+      (compTpExpr jmb G e) \<box> dupST \<box> (popST 1)"
+
+
+  "compTpExpr jmb G ( {cn}e..fn ) = 
+      (compTpExpr jmb G e) \<box> replST 1 (snd (the (field (G,cn) fn)))"
+
+  "compTpExpr jmb G (FAss cn e1 fn e2 ) = 
+      (compTpExpr jmb G e1) \<box> (compTpExpr jmb G e2) \<box> dup_x1ST \<box> (popST 2)"
+
+
+  "compTpExpr jmb G ({C}a..mn({fpTs}ps)) =
+       (compTpExpr jmb G a) \<box> (compTpExprs jmb G ps) \<box> 
+       (replST ((length ps) + 1) (method_rT (the (method (G,C) (mn,fpTs)))))"
+
+
+(* Expression lists *)
+
+  "compTpExprs jmb G [] = comb_nil"
+
+  "compTpExprs jmb G (e#es) = (compTpExpr jmb G e) \<box> (compTpExprs jmb G es)"
+
+
+(* Statements *)
+primrec
+   "compTpStmt jmb G Skip = comb_nil"
+
+   "compTpStmt jmb G (Expr e) =  (compTpExpr jmb G e) \<box> popST 1"
+
+   "compTpStmt jmb G (c1;; c2) = (compTpStmt jmb G c1) \<box> (compTpStmt jmb G c2)"
+
+   "compTpStmt jmb G (If(e) c1 Else c2) = 
+      (pushST [PrimT Boolean]) \<box> (compTpExpr jmb G e) \<box> popST 2 \<box>
+      (compTpStmt jmb G c1) \<box> nochangeST \<box> (compTpStmt jmb G c2)"
+
+   "compTpStmt jmb G (While(e) c) = 
+      (pushST [PrimT Boolean]) \<box> (compTpExpr jmb G e) \<box> popST 2 \<box>
+      (compTpStmt jmb G c) \<box> nochangeST"
+
+constdefs
+  compTpInit  :: "java_mb \<Rightarrow> (vname * ty)
+                   \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
+  "compTpInit jmb == (\<lambda> (vn,ty). (pushST [ty]) \<box>  (storeST (index jmb vn) ty))"
+
+consts
+  compTpInitLvars :: "[java_mb, (vname \<times> ty) list] 
+                   \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
+
+primrec 
+  "compTpInitLvars jmb [] = comb_nil"
+  "compTpInitLvars jmb (lv#lvars) = (compTpInit jmb lv) \<box> (compTpInitLvars jmb lvars)"
+
+constdefs
+   start_ST :: "opstack_type"
+  "start_ST == []"
+
+   start_LT :: "cname \<Rightarrow> ty list \<Rightarrow> nat \<Rightarrow> locvars_type"
+  "start_LT C pTs n ==  (OK (Class C))#((map OK pTs))@(replicate n Err)"
+
+  compTpMethod  :: "[java_mb prog, cname, java_mb mdecl] \<Rightarrow> method_type"
+  "compTpMethod G C == \<lambda> ((mn,pTs),rT, jmb). 
+                         let (pns,lvars,blk,res) = jmb
+                         in (mt_of
+                            ((compTpInitLvars jmb lvars \<box> 
+                              compTpStmt jmb G blk \<box> 
+                              compTpExpr jmb G res \<box>
+                              nochangeST)
+                                (start_ST, start_LT C pTs (length lvars))))"
+
+  compTp :: "java_mb prog => prog_type"
+  "compTp G C sig == let (D, rT, jmb) = (the (method (G, C) sig))
+                      in compTpMethod G C (sig, rT, jmb)"
+
+
+
+(**********************************************************************)
+  (* Computing the maximum stack size from the method_type *)
+
+constdefs
+  ssize_sto :: "(state_type option) \<Rightarrow> nat"
+  "ssize_sto sto ==  case sto of None \<Rightarrow> 0 | (Some (ST, LT)) \<Rightarrow> length ST"
+
+  max_of_list :: "nat list \<Rightarrow> nat"
+  "max_of_list xs == foldr max xs 0"
+
+  max_ssize :: "method_type \<Rightarrow> nat"
+  "max_ssize mt == max_of_list (map ssize_sto mt)"
+
+
+end
+
diff -r b95d12325b51 -r 2950128b8206 src/HOL/MicroJava/Comp/TypeInf.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/Comp/TypeInf.thy	Wed Oct 23 16:10:02 2002 +0200
@@ -0,0 +1,185 @@
+(*  Title:      HOL/MicroJava/Comp/TypeInf.thy
+    ID:         $Id$
+    Author:     Martin Strecker
+    Copyright   GPL 2002
+*)
+
+(* Exact position in theory hierarchy still to be determined *)
+theory TypeInf =  WellType:
+
+
+
+(**********************************************************************)
+;
+
+(*** Inversion of typing rules -- to be moved into WellType.thy
+     Also modify the wtpd_expr_\<dots> proofs in CorrComp.thy ***)
+
+lemma NewC_invers: "E\<turnstile>NewC C::T 
+  \<Longrightarrow> T = Class C \<and> is_class (prg E) C"
+by (erule ty_expr.cases, auto)
+
+lemma Cast_invers: "E\<turnstile>Cast D e::T
+  \<Longrightarrow> \<exists> C. T = Class D \<and> E\<turnstile>e::Class C \<and> is_class (prg E) D \<and> prg E\<turnstile>C\<preceq>? D"
+by (erule ty_expr.cases, auto)
+
+lemma Lit_invers: "E\<turnstile>Lit x::T
+  \<Longrightarrow> typeof (\<lambda>v. None) x = Some T"
+by (erule ty_expr.cases, auto)
+
+lemma LAcc_invers: "E\<turnstile>LAcc v::T
+  \<Longrightarrow> localT E v = Some T \<and> is_type (prg E) T"
+by (erule ty_expr.cases, auto)
+
+lemma BinOp_invers: "E\<turnstile>BinOp bop e1 e2::T'
+  \<Longrightarrow> \<exists> T. E\<turnstile>e1::T \<and> E\<turnstile>e2::T \<and> 
+            (if bop = Eq then T' = PrimT Boolean
+                        else T' = T \<and> T = PrimT Integer)"
+by (erule ty_expr.cases, auto)
+
+lemma LAss_invers: "E\<turnstile>v::=e::T'
+  \<Longrightarrow> \<exists> T. v ~= This \<and> E\<turnstile>LAcc v::T \<and> E\<turnstile>e::T' \<and> prg E\<turnstile>T'\<preceq>T"
+by (erule ty_expr.cases, auto)
+
+lemma FAcc_invers: "E\<turnstile>{fd}a..fn::fT
+  \<Longrightarrow> \<exists> C. E\<turnstile>a::Class C \<and> field (prg E,C) fn = Some (fd,fT)"
+by (erule ty_expr.cases, auto)
+
+lemma FAss_invers: "E\<turnstile>{fd}a..fn:=v::T' 
+\<Longrightarrow> \<exists> T. E\<turnstile>{fd}a..fn::T \<and> E\<turnstile>v ::T' \<and> prg E\<turnstile>T'\<preceq>T"
+by (erule ty_expr.cases, auto)
+
+lemma Call_invers: "E\<turnstile>{C}a..mn({pTs'}ps)::rT
+  \<Longrightarrow> \<exists> pTs md. 
+  E\<turnstile>a::Class C \<and> E\<turnstile>ps[::]pTs \<and> max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')}"
+by (erule ty_expr.cases, auto)
+
+
+lemma Nil_invers: "E\<turnstile>[] [::] Ts \<Longrightarrow> Ts = []"
+by (erule ty_exprs.cases, auto)
+
+lemma Cons_invers: "E\<turnstile>e#es[::]Ts \<Longrightarrow> 
+  \<exists> T Ts'. Ts = T#Ts' \<and> E \<turnstile>e::T \<and> E \<turnstile>es[::]Ts'"
+by (erule ty_exprs.cases, auto)
+
+
+lemma Expr_invers: "E\<turnstile>Expr e\<surd> \<Longrightarrow> \<exists> T. E\<turnstile>e::T"
+by (erule wt_stmt.cases, auto)
+
+lemma Comp_invers: "E\<turnstile>s1;; s2\<surd> \<Longrightarrow> E\<turnstile>s1\<surd> \<and> E\<turnstile>s2\<surd>"
+by (erule wt_stmt.cases, auto)
+
+lemma Cond_invers: "E\<turnstile>If(e) s1 Else s2\<surd> 
+  \<Longrightarrow> E\<turnstile>e::PrimT Boolean \<and> E\<turnstile>s1\<surd> \<and> E\<turnstile>s2\<surd>"
+by (erule wt_stmt.cases, auto)
+
+lemma Loop_invers: "E\<turnstile>While(e) s\<surd>
+  \<Longrightarrow> E\<turnstile>e::PrimT Boolean \<and> E\<turnstile>s\<surd>"
+by (erule wt_stmt.cases, auto)
+
+
+(**********************************************************************)
+
+
+declare split_paired_All [simp del]
+declare split_paired_Ex [simp del]
+
+(* Uniqueness of types property *)
+
+lemma uniqueness_of_types: "
+  (\<forall> E T1 T2. E\<turnstile>e :: T1 \<longrightarrow> E\<turnstile>e :: T2 \<longrightarrow> T1 = T2) \<and>
+  (\<forall> E Ts1 Ts2. E\<turnstile>es [::] Ts1 \<longrightarrow> E\<turnstile>es [::] Ts2 \<longrightarrow> Ts1 = Ts2)"
+
+apply (rule expr.induct)
+
+(* NewC *)
+apply (intro strip) 
+apply (erule ty_expr.cases) apply simp+
+apply (erule ty_expr.cases) apply simp+
+
+(* Cast *)
+apply (intro strip) 
+apply (erule ty_expr.cases) apply simp+
+apply (erule ty_expr.cases) apply simp+
+
+(* Lit *)
+apply (intro strip) 
+apply (erule ty_expr.cases) apply simp+
+apply (erule ty_expr.cases) apply simp+
+
+(* BinOp *)
+apply (intro strip)
+apply (case_tac binop)
+(* Eq *)
+apply (erule ty_expr.cases) apply simp+
+apply (erule ty_expr.cases) apply simp+
+(* Add *)
+apply (erule ty_expr.cases) apply simp+
+apply (erule ty_expr.cases) apply simp+
+
+(* LAcc *)
+apply (intro strip) 
+apply (erule ty_expr.cases) apply simp+
+apply (erule ty_expr.cases) apply simp+
+
+(* LAss *)
+apply (intro strip) 
+apply (erule ty_expr.cases) apply simp+
+apply (erule ty_expr.cases) apply simp+
+
+
+(* FAcc *)
+apply (intro strip)
+apply (drule FAcc_invers)+ apply (erule exE)+ 
+  apply (subgoal_tac "C = Ca", simp) apply blast
+
+
+(* FAss *)
+apply (intro strip)
+apply (drule FAss_invers)+ apply (erule exE)+ apply (erule conjE)+
+apply (drule FAcc_invers)+ apply (erule exE)+ apply blast 
+
+
+(* Call *)
+apply (intro strip)
+apply (drule Call_invers)+ apply (erule exE)+ apply (erule conjE)+
+apply (subgoal_tac "pTs = pTsa", simp) apply blast
+
+(* expression lists *)
+apply (intro strip)
+apply (erule ty_exprs.cases)+ apply simp+
+
+apply (intro strip)
+apply (erule ty_exprs.cases, simp)
+apply (erule ty_exprs.cases, simp)
+apply (subgoal_tac "e = ea", simp) apply simp
+done
+
+
+lemma uniqueness_of_types_expr [rule_format (no_asm)]: "
+  (\<forall> E T1 T2. E\<turnstile>e :: T1 \<longrightarrow> E\<turnstile>e :: T2 \<longrightarrow> T1 = T2)"
+by (rule uniqueness_of_types [THEN conjunct1])
+
+lemma uniqueness_of_types_exprs [rule_format (no_asm)]: "
+  (\<forall> E Ts1 Ts2. E\<turnstile>es [::] Ts1 \<longrightarrow> E\<turnstile>es [::] Ts2 \<longrightarrow> Ts1 = Ts2)"
+by (rule uniqueness_of_types [THEN conjunct2])
+
+
+  
+
+constdefs 
+  inferred_tp  :: "[java_mb env, expr] \<Rightarrow> ty"
+  "inferred_tp E e == (SOME T. E\<turnstile>e :: T)"
+  inferred_tps :: "[java_mb env, expr list] \<Rightarrow> ty list"
+  "inferred_tps E es == (SOME Ts. E\<turnstile>es [::] Ts)"
+
+(* get inferred type(s) for well-typed term *)
+lemma inferred_tp_wt: "E\<turnstile>e :: T \<Longrightarrow> (inferred_tp E e) = T"
+by (auto simp: inferred_tp_def intro: uniqueness_of_types_expr)
+
+lemma inferred_tps_wt: "E\<turnstile>es [::] Ts \<Longrightarrow> (inferred_tps E es) = Ts"
+by (auto simp: inferred_tps_def intro: uniqueness_of_types_exprs)
+
+
+end
+