diff -r 28e26f468f08 -r d955914193e0 src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Fri Aug 11 14:52:39 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Fri Aug 11 14:52:52 2000 +0200
@@ -10,61 +10,61 @@
 
 
 constdefs
-  is_approx :: "['a option list, 'a list] \\<Rightarrow> bool"
-  "is_approx a b \\<equiv> length a = length b \\<and> (\\<forall> n. n < length a \\<longrightarrow>
-                   (a!n = None \\<or> a!n = Some (b!n)))"
+  is_approx :: "['a option list, 'a list] \<Rightarrow> bool"
+  "is_approx a b \<equiv> length a = length b \<and> (\<forall> n. n < length a \<longrightarrow>
+                   (a!n = None \<or> a!n = Some (b!n)))"
   
-  contains_dead :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool"
-  "contains_dead ins cert phi pc \\<equiv>
-     Suc pc \\<notin> succs (ins!pc) pc \\<and> Suc pc < length phi \\<longrightarrow>
+  contains_dead :: "[instr list, certificate, method_type, p_count] \<Rightarrow> bool"
+  "contains_dead ins cert phi pc \<equiv>
+     Suc pc \<notin> succs (ins!pc) pc \<and> Suc pc < length phi \<longrightarrow>
      cert ! (Suc pc) = Some (phi ! Suc pc)"
 
-  contains_targets :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool"
-  "contains_targets ins cert phi pc \\<equiv> (
-     \\<forall> pc' \\<in> succs (ins!pc) pc. pc' \\<noteq> Suc pc \\<and> pc' < length phi \\<longrightarrow> 
+  contains_targets :: "[instr list, certificate, method_type, p_count] \<Rightarrow> bool"
+  "contains_targets ins cert phi pc \<equiv> (
+     \<forall> pc' \<in> succs (ins!pc) pc. pc' \<noteq> Suc pc \<and> pc' < length phi \<longrightarrow> 
      cert!pc' = Some (phi!pc'))" 
 
 
-  fits :: "[instr list, certificate, method_type] \\<Rightarrow> bool"
-  "fits ins cert phi \\<equiv> is_approx cert phi \\<and> length ins < length phi \\<and>
-                            (\\<forall> pc. pc < length ins \\<longrightarrow>
-                                   contains_dead ins cert phi pc \\<and> 
+  fits :: "[instr list, certificate, method_type] \<Rightarrow> bool"
+  "fits ins cert phi \<equiv> is_approx cert phi \<and> length ins < length phi \<and>
+                            (\<forall> pc. pc < length ins \<longrightarrow>
+                                   contains_dead ins cert phi pc \<and> 
                                    contains_targets ins cert phi pc)"
 
-  is_target :: "[instr list, p_count] \\<Rightarrow> bool" 
-  "is_target ins pc \\<equiv> \\<exists> pc'. pc' < length ins \\<and> pc \\<in> succs (ins!pc') pc'"
+  is_target :: "[instr list, p_count] \<Rightarrow> bool" 
+  "is_target ins pc \<equiv> \<exists> pc'. pc' < length ins \<and> pc \<in> succs (ins!pc') pc'"
 
-  maybe_dead :: "[instr list, p_count] \\<Rightarrow> bool"
-  "maybe_dead ins pc \\<equiv> \\<exists> pc'. pc = pc'+1 \\<and> pc \\<notin> succs (ins!pc') pc'"
+  maybe_dead :: "[instr list, p_count] \<Rightarrow> bool"
+  "maybe_dead ins pc \<equiv> \<exists> pc'. pc = pc'+1 \<and> pc \<notin> succs (ins!pc') pc'"
 
-  mdot :: "[instr list, p_count] \\<Rightarrow> bool"
-  "mdot ins pc \\<equiv> maybe_dead ins pc \\<or> is_target ins pc"
+  mdot :: "[instr list, p_count] \<Rightarrow> bool"
+  "mdot ins pc \<equiv> maybe_dead ins pc \<or> is_target ins pc"
 
 
 consts
-  option_filter_n :: "['a list, nat \\<Rightarrow> bool, nat] \\<Rightarrow> 'a option list"
+  option_filter_n :: "['a list, nat \<Rightarrow> bool, nat] \<Rightarrow> 'a option list"
 primrec 
   "option_filter_n []    P n = []"  
   "option_filter_n (h#t) P n = (if (P n) then Some h # option_filter_n t P (n+1) 
                                          else None   # option_filter_n t P (n+1))"  
   
 constdefs 
-  option_filter :: "['a list, nat \\<Rightarrow> bool] \\<Rightarrow> 'a option list" 
-  "option_filter l P \\<equiv> option_filter_n l P 0" 
+  option_filter :: "['a list, nat \<Rightarrow> bool] \<Rightarrow> 'a option list" 
+  "option_filter l P \<equiv> option_filter_n l P 0" 
   
-  make_cert :: "[instr list, method_type] \\<Rightarrow> certificate"
-  "make_cert ins phi \\<equiv> option_filter phi (mdot ins)"
+  make_cert :: "[instr list, method_type] \<Rightarrow> certificate"
+  "make_cert ins phi \<equiv> option_filter phi (mdot ins)"
   
-  make_Cert :: "[jvm_prog, prog_type] \\<Rightarrow> prog_certificate"
-  "make_Cert G Phi \\<equiv>  \\<lambda> C sig.
-    let (C,x,y,mdecls) = \\<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \\<in> set G \\<and> Cl = C in
-      let (sig,rT,maxl,b) = \\<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \\<in> set mdecls \\<and> sg = sig in
+  make_Cert :: "[jvm_prog, prog_type] \<Rightarrow> prog_certificate"
+  "make_Cert G Phi \<equiv>  \<lambda> C sig.
+    let (C,x,y,mdecls) = \<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C in
+      let (sig,rT,maxl,b) = \<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig in
         make_cert b (Phi C sig)"
   
 
 lemmas [simp del] = split_paired_Ex
 
-lemma length_ofn [rulify]: "\\<forall>n. length (option_filter_n l P n) = length l"
+lemma length_ofn [rulify]: "\<forall>n. length (option_filter_n l P n) = length l"
   by (induct l) auto
 
 
@@ -72,7 +72,7 @@
 proof -
   {
     fix a n
-    have "\\<forall>n. is_approx (option_filter_n a P n) a" (is "?P a")
+    have "\<forall>n. is_approx (option_filter_n a P n) a" (is "?P a")
     proof (induct a)
       show "?P []" by (auto simp add: is_approx_def)
     
@@ -89,7 +89,7 @@
         assume "m < length (option_filter_n (l # ls) P n)"
         hence m: "m < Suc (length ls)" by (simp only: length_ofn) simp
       
-        show "option_filter_n (l # ls) P n ! m = None \\<or>
+        show "option_filter_n (l # ls) P n ! m = None \<or>
               option_filter_n (l # ls) P n ! m = Some ((l # ls) ! m)" 
         proof (cases "m")
           assume "m = 0"
@@ -102,7 +102,7 @@
             from m Suc
             show "m' < length (option_filter_n ls P (Suc n))" by (simp add: length_ofn)
           
-            assume "option_filter_n ls P (Suc n) ! m' = None \\<or> 
+            assume "option_filter_n ls P (Suc n) ! m' = None \<or> 
                     option_filter_n ls P (Suc n) ! m' = Some (ls ! m')"
             with m Suc
             show ?thesis by auto
@@ -117,12 +117,12 @@
 qed
 
 lemma option_filter_Some:
-"\\<lbrakk>n < length l; P n\\<rbrakk> \\<Longrightarrow> option_filter l P ! n = Some (l!n)"
+"\<lbrakk>n < length l; P n\<rbrakk> \<Longrightarrow> option_filter l P ! n = Some (l!n)"
 proof -
   
   assume 1: "n < length l" "P n"
 
-  have "\\<forall>n n'. n < length l \\<longrightarrow> P (n+n') \\<longrightarrow>  option_filter_n l P n' ! n = Some (l!n)"
+  have "\<forall>n n'. n < length l \<longrightarrow> P (n+n') \<longrightarrow>  option_filter_n l P n' ! n = Some (l!n)"
     (is "?P l")
   proof (induct l)
     show "?P []" by simp
@@ -154,13 +154,13 @@
   by (auto intro: option_filter_Some simp add: contains_dead_def mdot_def maybe_dead_def)
 
 lemma option_filter_contains_targets:
-"pc < length ins \\<Longrightarrow> contains_targets ins (option_filter phi (mdot ins)) phi pc"
+"pc < length ins \<Longrightarrow> contains_targets ins (option_filter phi (mdot ins)) phi pc"
 proof (unfold contains_targets_def, clarsimp)
  
   fix pc'
   assume "pc < length ins" 
-         "pc' \\<in> succs (ins ! pc) pc" 
-         "pc' \\<noteq> Suc pc" and
+         "pc' \<in> succs (ins ! pc) pc" 
+         "pc' \<noteq> Suc pc" and
     pc': "pc' < length phi"
 
   hence "is_target ins pc'" by (auto simp add: is_target_def)
@@ -172,7 +172,7 @@
   
 
 lemma fits_make_cert:
-  "length ins < length phi \\<Longrightarrow> fits ins (make_cert ins phi) phi"
+  "length ins < length phi \<Longrightarrow> fits ins (make_cert ins phi) phi"
 proof -
   assume l: "length ins < length phi"
 
@@ -194,25 +194,25 @@
 qed
 
 lemma fitsD: 
-"\\<lbrakk>fits ins cert phi; pc' \\<in> succs (ins!pc) pc; pc' \\<noteq> Suc pc; pc < length ins; pc' < length ins\\<rbrakk> 
-  \\<Longrightarrow> cert!pc' = Some (phi!pc')"
+"\<lbrakk>fits ins cert phi; pc' \<in> succs (ins!pc) pc; pc' \<noteq> Suc pc; pc < length ins; pc' < length ins\<rbrakk> 
+  \<Longrightarrow> cert!pc' = Some (phi!pc')"
 by (clarsimp simp add: fits_def contains_dead_def contains_targets_def)
 
 lemma fitsD2:
-"\\<lbrakk>fits ins cert phi; Suc pc \\<notin> succs (ins!pc) pc;  pc < length ins\\<rbrakk> 
-  \\<Longrightarrow> cert ! Suc pc = Some (phi ! Suc pc)"
+"\<lbrakk>fits ins cert phi; Suc pc \<notin> succs (ins!pc) pc;  pc < length ins\<rbrakk> 
+  \<Longrightarrow> cert ! Suc pc = Some (phi ! Suc pc)"
 by (clarsimp simp add: fits_def contains_dead_def contains_targets_def)
 
 
 lemma wtl_inst_mono:
-"\\<lbrakk>wtl_inst i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins; 
-  G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow> 
- \\<exists> s2'. wtl_inst (ins!pc) G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')";
+"\<lbrakk>wtl_inst i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins; 
+  G \<turnstile> s2 <=s s1; i = ins!pc\<rbrakk> \<Longrightarrow> 
+ \<exists> s2'. wtl_inst (ins!pc) G rT s2 s2' cert mpc pc \<and> (G \<turnstile> s2' <=s s1')"
 proof -
   assume pc:   "pc < length ins" "i = ins!pc"
   assume wtl:  "wtl_inst i G rT s1 s1' cert mpc pc"
   assume fits: "fits ins cert phi"
-  assume G:    "G \\<turnstile> s2 <=s s1"
+  assume G:    "G \<turnstile> s2 <=s s1"
   
   let "?step s" = "step (i, G, s)"
 
@@ -220,40 +220,40 @@
   have app: "app (i, G, rT, s2)" by (auto simp add: wtl_inst_def app_mono)
   
   from wtl G
-  have step: "succs i pc \\<noteq> {} \\<Longrightarrow> G \\<turnstile> the (?step s2) <=s the (?step s1)" 
+  have step: "succs i pc \<noteq> {} \<Longrightarrow> G \<turnstile> the (?step s2) <=s the (?step s1)" 
     by - (drule step_mono, auto simp add: wtl_inst_def)
   
   with app
-  have some: "succs i pc \\<noteq> {} \\<Longrightarrow> ?step s2 \\<noteq> None" by (simp add: app_step_some)
+  have some: "succs i pc \<noteq> {} \<Longrightarrow> ?step s2 \<noteq> None" by (simp add: app_step_some)
 
   {
     fix pc'
-    assume 0: "pc' \\<in> succs i pc" "pc' \\<noteq> pc+1"
-    hence "succs i pc \\<noteq> {}" by auto
-    hence "G \\<turnstile> the (?step s2) <=s the (?step s1)" by (rule step)
+    assume 0: "pc' \<in> succs i pc" "pc' \<noteq> pc+1"
+    hence "succs i pc \<noteq> {}" by auto
+    hence "G \<turnstile> the (?step s2) <=s the (?step s1)" by (rule step)
     also 
     from wtl 0
-    have "G \\<turnstile> the (?step s1) <=s the (cert!pc')"
+    have "G \<turnstile> the (?step s1) <=s the (cert!pc')"
       by (auto simp add: wtl_inst_def) 
     finally
-    have "G\\<turnstile> the (?step s2) <=s the (cert!pc')" .
+    have "G\<turnstile> the (?step s2) <=s the (cert!pc')" .
   } note cert = this
     
-  have "\\<exists>s2'. wtl_inst i G rT s2 s2' cert mpc pc \\<and> G \\<turnstile> s2' <=s s1'"
-  proof (cases "pc+1 \\<in> succs i pc")
+  have "\<exists>s2'. wtl_inst i G rT s2 s2' cert mpc pc \<and> G \<turnstile> s2' <=s s1'"
+  proof (cases "pc+1 \<in> succs i pc")
     case True
     with wtl
     have s1': "s1' = the (?step s1)" by (simp add: wtl_inst_def)
 
-    have "wtl_inst i G rT s2 (the (?step s2)) cert mpc pc \\<and> G \\<turnstile> (the (?step s2)) <=s s1'" 
-      (is "?wtl \\<and> ?G")
+    have "wtl_inst i G rT s2 (the (?step s2)) cert mpc pc \<and> G \<turnstile> (the (?step s2)) <=s s1'" 
+      (is "?wtl \<and> ?G")
     proof
       from True s1'
       show ?G by (auto intro: step)
 
       from True app wtl
       show ?wtl
-        by (clarsimp intro: cert simp add: wtl_inst_def)
+        by (clarsimp intro!: cert simp add: wtl_inst_def)
     qed
     thus ?thesis by blast
   next
@@ -262,8 +262,8 @@
     have "s1' = the (cert ! Suc pc)" by (simp add: wtl_inst_def)
 
     with False app wtl
-    have "wtl_inst i G rT s2 s1' cert mpc pc \\<and> G \\<turnstile> s1' <=s s1'"
-      by (clarsimp intro: cert simp add: wtl_inst_def)
+    have "wtl_inst i G rT s2 s1' cert mpc pc \<and> G \<turnstile> s1' <=s s1'"
+      by (clarsimp intro!: cert simp add: wtl_inst_def)
 
     thus ?thesis by blast
   qed
@@ -273,76 +273,76 @@
     
 
 lemma wtl_option_mono:
-"\\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; fits ins cert phi; 
-  pc < length ins; G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow> 
- \\<exists> s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')"
+"\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; fits ins cert phi; 
+  pc < length ins; G \<turnstile> s2 <=s s1; i = ins!pc\<rbrakk> \<Longrightarrow> 
+ \<exists> s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \<and> (G \<turnstile> s2' <=s s1')"
 proof -
   assume wtl:  "wtl_inst_option i G rT s1 s1' cert mpc pc" and
          fits: "fits ins cert phi" "pc < length ins"
-               "G \\<turnstile> s2 <=s s1" "i = ins!pc"
+               "G \<turnstile> s2 <=s s1" "i = ins!pc"
 
   show ?thesis
   proof (cases "cert!pc")
     case None
-    with wtl fits;
-    show ?thesis; 
-      by - (rule wtl_inst_mono [elimify], (simp add: wtl_inst_option_def)+);
+    with wtl fits
+    show ?thesis 
+      by - (rule wtl_inst_mono [elimify], (simp add: wtl_inst_option_def)+)
   next
     case Some
-    with wtl fits;
+    with wtl fits
 
-    have G: "G \\<turnstile> s2 <=s a"
+    have G: "G \<turnstile> s2 <=s a"
      by - (rule sup_state_trans, (simp add: wtl_inst_option_def)+)
 
     from Some wtl
-    have "wtl_inst i G rT a s1' cert mpc pc"; by (simp add: wtl_inst_option_def)
+    have "wtl_inst i G rT a s1' cert mpc pc" by (simp add: wtl_inst_option_def)
 
     with G fits
-    have "\\<exists> s2'. wtl_inst (ins!pc) G rT a s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')"
-      by - (rule wtl_inst_mono, (simp add: wtl_inst_option_def)+);
+    have "\<exists> s2'. wtl_inst (ins!pc) G rT a s2' cert mpc pc \<and> (G \<turnstile> s2' <=s s1')"
+      by - (rule wtl_inst_mono, (simp add: wtl_inst_option_def)+)
     
-    with Some G;
-    show ?thesis; by (simp add: wtl_inst_option_def);
+    with Some G
+    show ?thesis by (simp add: wtl_inst_option_def)
   qed
 qed
 
 
     
 lemma wt_instr_imp_wtl_inst:
-"\\<lbrakk>wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi;
-  pc < length ins; length ins = max_pc\\<rbrakk> \\<Longrightarrow> 
-  \\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
+"\<lbrakk>wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi;
+  pc < length ins; length ins = max_pc\<rbrakk> \<Longrightarrow> 
+  \<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \<and> G \<turnstile> s <=s phi ! Suc pc"
 proof -
   assume wt:   "wt_instr (ins!pc) G rT phi max_pc pc" 
   assume fits: "fits ins cert phi"
   assume pc:   "pc < length ins" "length ins = max_pc"
 
   from wt 
-  have app: "app (ins!pc, G, rT, phi!pc)" by (simp add: wt_instr_def);
+  have app: "app (ins!pc, G, rT, phi!pc)" by (simp add: wt_instr_def)
 
   from wt pc
-  have pc': "!!pc'. pc' \\<in> succs (ins!pc) pc \\<Longrightarrow> pc' < length ins"
+  have pc': "!!pc'. pc' \<in> succs (ins!pc) pc \<Longrightarrow> pc' < length ins"
     by (simp add: wt_instr_def)
 
   let ?s' = "the (step (ins!pc,G, phi!pc))"
 
   from wt
-  have G: "!!pc'. pc' \\<in> succs (ins!pc) pc \\<Longrightarrow> G \\<turnstile> ?s' <=s phi ! pc'"
+  have G: "!!pc'. pc' \<in> succs (ins!pc) pc \<Longrightarrow> G \<turnstile> ?s' <=s phi ! pc'"
     by (simp add: wt_instr_def)
 
   from wt fits pc
-  have cert: "!!pc'. \\<lbrakk>pc' \\<in> succs (ins!pc) pc; pc' < max_pc; pc' \\<noteq> pc+1\\<rbrakk> 
-    \\<Longrightarrow> cert!pc' \\<noteq> None \\<and> G \\<turnstile> ?s' <=s the (cert!pc')"
+  have cert: "!!pc'. \<lbrakk>pc' \<in> succs (ins!pc) pc; pc' < max_pc; pc' \<noteq> pc+1\<rbrakk> 
+    \<Longrightarrow> cert!pc' \<noteq> None \<and> G \<turnstile> ?s' <=s the (cert!pc')"
     by (auto dest: fitsD simp add: wt_instr_def)
 
   show ?thesis
-  proof (cases "pc+1 \\<in> succs (ins!pc) pc")
+  proof (cases "pc+1 \<in> succs (ins!pc) pc")
     case True
 
-    have "wtl_inst (ins!pc) G rT (phi!pc) ?s' cert max_pc pc \\<and> G \\<turnstile> ?s' <=s phi ! Suc pc" (is "?wtl \\<and> ?G")
+    have "wtl_inst (ins!pc) G rT (phi!pc) ?s' cert max_pc pc \<and> G \<turnstile> ?s' <=s phi ! Suc pc" (is "?wtl \<and> ?G")
     proof 
       from True
-      show "G \\<turnstile> ?s' <=s phi ! Suc pc"  by (simp add: G)
+      show "G \<turnstile> ?s' <=s phi ! Suc pc"  by (simp add: G)
 
       from True fits app pc cert pc'
       show "?wtl"
@@ -356,7 +356,7 @@
 
     case False
     with fits app pc cert pc'
-    have "wtl_inst (ins ! pc) G rT (phi ! pc) ?s'' cert max_pc pc \\<and> G \\<turnstile> ?s'' <=s phi ! Suc pc" 
+    have "wtl_inst (ins ! pc) G rT (phi ! pc) ?s'' cert max_pc pc \<and> G \<turnstile> ?s'' <=s phi ! Suc pc" 
       by (auto dest: fitsD2 simp add: wtl_inst_def)
 
     thus ?thesis by blast
@@ -365,32 +365,32 @@
 
   
 lemma wt_instr_imp_wtl_option:
-"\\<lbrakk>fits ins cert phi; pc < length ins; wt_instr (ins!pc) G rT phi max_pc pc;  max_pc = length ins\\<rbrakk> \\<Longrightarrow> 
- \\<exists> s. wtl_inst_option (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
+"\<lbrakk>fits ins cert phi; pc < length ins; wt_instr (ins!pc) G rT phi max_pc pc;  max_pc = length ins\<rbrakk> \<Longrightarrow> 
+ \<exists> s. wtl_inst_option (ins!pc) G rT (phi!pc) s cert max_pc pc \<and> G \<turnstile> s <=s phi ! Suc pc"
 proof -
   assume fits : "fits ins cert phi" "pc < length ins" 
          and "wt_instr (ins!pc) G rT phi max_pc pc" 
-             "max_pc = length ins";
+             "max_pc = length ins"
 
-  hence * : "\\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
-    by - (rule wt_instr_imp_wtl_inst, simp+);
+  hence * : "\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \<and> G \<turnstile> s <=s phi ! Suc pc"
+    by - (rule wt_instr_imp_wtl_inst, simp+)
   
-  show ?thesis;
-  proof (cases "cert ! pc");
-    case None;
-    with *;
-    show ?thesis; by (simp add: wtl_inst_option_def);
+  show ?thesis
+  proof (cases "cert ! pc")
+    case None
+    with *
+    show ?thesis by (simp add: wtl_inst_option_def)
 
-  next;
-    case Some;
+  next
+    case Some
 
-    from fits; 
-    have "pc < length phi"; by (clarsimp simp add: fits_def);
-    with fits Some;
-    have "cert ! pc = Some (phi!pc)"; by (auto simp add: fits_def is_approx_def);
+    from fits 
+    have "pc < length phi" by (clarsimp simp add: fits_def)
+    with fits Some
+    have "cert ! pc = Some (phi!pc)" by (auto simp add: fits_def is_approx_def)
      
-    with *; 
-    show ?thesis; by (simp add: wtl_inst_option_def);
+    with * 
+    show ?thesis by (simp add: wtl_inst_option_def)
   qed
 qed
 
@@ -401,13 +401,13 @@
 *}
 
 theorem wt_imp_wtl_inst_list:
-"\\<forall> pc. (\\<forall>pc'. pc' < length all_ins \\<longrightarrow> wt_instr (all_ins ! pc') G rT phi (length all_ins) pc') \\<longrightarrow>   
-       fits all_ins cert phi \\<longrightarrow> 
-       (\\<exists>l. pc = length l \\<and> all_ins = l@ins) \\<longrightarrow>  
-       pc < length all_ins \\<longrightarrow>      
-       (\\<forall> s. (G \\<turnstile> s <=s (phi!pc)) \\<longrightarrow> 
-             (\\<exists>s'. wtl_inst_list ins G rT s s' cert (length all_ins) pc))" 
-(is "\\<forall>pc. ?wt \\<longrightarrow> ?fits \\<longrightarrow> ?l pc ins \\<longrightarrow> ?len pc \\<longrightarrow> ?wtl pc ins" is "\\<forall>pc. ?C pc ins" is "?P ins") 
+"\<forall> pc. (\<forall>pc'. pc' < length all_ins \<longrightarrow> wt_instr (all_ins ! pc') G rT phi (length all_ins) pc') \<longrightarrow>   
+       fits all_ins cert phi \<longrightarrow> 
+       (\<exists>l. pc = length l \<and> all_ins = l@ins) \<longrightarrow>  
+       pc < length all_ins \<longrightarrow>      
+       (\<forall> s. (G \<turnstile> s <=s (phi!pc)) \<longrightarrow> 
+             (\<exists>s'. wtl_inst_list ins G rT s s' cert (length all_ins) pc))" 
+(is "\<forall>pc. ?wt \<longrightarrow> ?fits \<longrightarrow> ?l pc ins \<longrightarrow> ?len pc \<longrightarrow> ?wtl pc ins" is "\<forall>pc. ?C pc ins" is "?P ins") 
 proof (induct "?P" "ins")
   case Nil
   show "?P []" by simp
@@ -418,10 +418,10 @@
   show "?P (i#ins')" 
   proof (intro allI impI, elim exE conjE)
     fix pc s l
-    assume wt  : "\\<forall>pc'. pc' < length all_ins \\<longrightarrow> 
+    assume wt  : "\<forall>pc'. pc' < length all_ins \<longrightarrow> 
                         wt_instr (all_ins ! pc') G rT phi (length all_ins) pc'"
     assume fits: "fits all_ins cert phi"
-    assume G   : "G \\<turnstile> s <=s phi ! pc"
+    assume G   : "G \<turnstile> s <=s phi ! pc"
     assume l   : "pc < length all_ins"
 
     assume pc  : "all_ins = l@i#ins'" "pc = length l"
@@ -434,25 +434,25 @@
     with fits l 
     obtain s1 where
           "wtl_inst_option (all_ins!pc) G rT (phi!pc) s1 cert (length all_ins) pc" and
-      s1: "G \\<turnstile> s1 <=s phi ! (Suc pc)"
+      s1: "G \<turnstile> s1 <=s phi ! (Suc pc)"
       by - (drule wt_instr_imp_wtl_option, assumption+, simp, elim exE conjE, simp) 
     
     with fits l
     obtain s2 where
       o:  "wtl_inst_option (all_ins!pc) G rT s s2 cert (length all_ins) pc" 
-      and "G \\<turnstile> s2 <=s s1"
+      and "G \<turnstile> s2 <=s s1"
       by - (drule wtl_option_mono, assumption+, simp, elim exE conjE, rule that) 
 
     with s1
-    have G': "G \\<turnstile> s2 <=s phi ! (Suc pc)"
+    have G': "G \<turnstile> s2 <=s phi ! (Suc pc)"
       by - (rule sup_state_trans, auto)
 
     from Cons
     have "?C (Suc pc) ins'" by blast
     with wt fits pc
-    have IH: "?len (Suc pc) \\<longrightarrow> ?wtl (Suc pc) ins'" by auto
+    have IH: "?len (Suc pc) \<longrightarrow> ?wtl (Suc pc) ins'" by auto
 
-    show "\\<exists>s'. wtl_inst_list (i#ins') G rT s s' cert (length all_ins) pc"
+    show "\<exists>s'. wtl_inst_list (i#ins') G rT s s' cert (length all_ins) pc"
     proof (cases "?len (Suc pc)")
       case False
       with pc
@@ -475,70 +475,70 @@
   
 
 lemma fits_imp_wtl_method_complete:
-"\\<lbrakk>wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wtl_method G C pTs rT mxl ins cert"
+"\<lbrakk>wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\<rbrakk> \<Longrightarrow> wtl_method G C pTs rT mxl ins cert"
 by (simp add: wt_method_def wtl_method_def del: split_paired_Ex)
-   (rule wt_imp_wtl_inst_list [rulify, elimify], auto simp add: wt_start_def simp del: split_paired_Ex); 
+   (rule wt_imp_wtl_inst_list [rulify, elimify], auto simp add: wt_start_def simp del: split_paired_Ex) 
 
 
 lemma wtl_method_complete:
-"\\<lbrakk>wt_method G C pTs rT mxl ins phi; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wtl_method G C pTs rT mxl ins (make_cert ins phi)";
-proof -;
-  assume * : "wt_method G C pTs rT mxl ins phi" "wf_prog wf_mb G";
+"\<lbrakk>wt_method G C pTs rT mxl ins phi; wf_prog wf_mb G\<rbrakk> \<Longrightarrow> wtl_method G C pTs rT mxl ins (make_cert ins phi)"
+proof -
+  assume * : "wt_method G C pTs rT mxl ins phi" "wf_prog wf_mb G"
   
-  hence "fits ins (make_cert ins phi) phi";
-    by - (rule fits_make_cert, simp add: wt_method_def);
+  hence "fits ins (make_cert ins phi) phi"
+    by - (rule fits_make_cert, simp add: wt_method_def)
 
-  with *;
-  show ?thesis; by - (rule fits_imp_wtl_method_complete);
-qed;
+  with *
+  show ?thesis by - (rule fits_imp_wtl_method_complete)
+qed
 
 lemma unique_set:
-"(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (a',b',c',d') \\<in> set l \\<longrightarrow> a = a' \\<longrightarrow> b=b' \\<and> c=c' \\<and> d=d'";
-  by (induct "l") auto;
+"(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (a',b',c',d') \<in> set l \<longrightarrow> a = a' \<longrightarrow> b=b' \<and> c=c' \<and> d=d'"
+  by (induct "l") auto
 
 lemma unique_epsilon:
-"(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (\\<epsilon> (a',b',c',d'). (a',b',c',d') \\<in> set l \\<and> a'=a) = (a,b,c,d)";
-  by (auto simp add: unique_set);
+"(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (\<epsilon> (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)"
+  by (auto simp add: unique_set)
 
 
-theorem wtl_complete: "\\<lbrakk>wt_jvm_prog G Phi\\<rbrakk> \\<Longrightarrow> wtl_jvm_prog G (make_Cert G Phi)";
-proof (simp only: wt_jvm_prog_def);
+theorem wtl_complete: "\<lbrakk>wt_jvm_prog G Phi\<rbrakk> \<Longrightarrow> wtl_jvm_prog G (make_Cert G Phi)"
+proof (simp only: wt_jvm_prog_def)
 
-  assume wfprog: "wf_prog (\\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G";
+  assume wfprog: "wf_prog (\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G"
 
-  thus ?thesis; 
-  proof (simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def wf_mdecl_def, auto);
-    fix a aa ab b ac ba ad ae bb; 
-    assume 1 : "\\<forall>(C,sc,fs,ms)\\<in>set G.
-             Ball (set fs) (wf_fdecl G) \\<and>
-             unique fs \\<and>
-             (\\<forall>(sig,rT,mb)\\<in>set ms. wf_mhead G sig rT \\<and> (\\<lambda>(maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) mb) \\<and>
-             unique ms \\<and>
-             (case sc of None \\<Rightarrow> C = Object
-              | Some D \\<Rightarrow>
-                  is_class G D \\<and>
-                  (D, C) \\<notin> (subcls1 G)^* \\<and>
-                  (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
-             "(a, aa, ab, b) \\<in> set G";
+  thus ?thesis 
+  proof (simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def wf_mdecl_def, auto)
+    fix a aa ab b ac ba ad ae bb 
+    assume 1 : "\<forall>(C,sc,fs,ms)\<in>set G.
+             Ball (set fs) (wf_fdecl G) \<and>
+             unique fs \<and>
+             (\<forall>(sig,rT,mb)\<in>set ms. wf_mhead G sig rT \<and> (\<lambda>(maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) mb) \<and>
+             unique ms \<and>
+             (case sc of None \<Rightarrow> C = Object
+              | Some D \<Rightarrow>
+                  is_class G D \<and>
+                  (D, C) \<notin> (subcls1 G)^* \<and>
+                  (\<forall>(sig,rT,b)\<in>set ms. \<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') \<longrightarrow> G\<turnstile>rT\<preceq>rT'))"
+             "(a, aa, ab, b) \<in> set G"
   
-    assume uG : "unique G"; 
-    assume b  : "((ac, ba), ad, ae, bb) \\<in> set b";
+    assume uG : "unique G" 
+    assume b  : "((ac, ba), ad, ae, bb) \<in> set b"
 
-    from 1;
-    show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))";
-    proof (rule bspec [elimify], clarsimp);
-      assume ub : "unique b";
-      assume m: "\\<forall>(sig,rT,mb)\\<in>set b. wf_mhead G sig rT \\<and> (\\<lambda>(maxl,b). wt_method G a (snd sig) rT maxl b (Phi a sig)) mb"; 
-      from m b;
-      show ?thesis;
-      proof (rule bspec [elimify], clarsimp);
-        assume "wt_method G a ba ad ae bb (Phi a (ac, ba))";         
-        with wfprog uG ub b 1;
-        show ?thesis;
-          by - (rule wtl_method_complete [elimify], assumption+, simp add: make_Cert_def unique_epsilon);
-      qed; 
-    qed;
-  qed;
+    from 1
+    show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))"
+    proof (rule bspec [elimify], clarsimp)
+      assume ub : "unique b"
+      assume m: "\<forall>(sig,rT,mb)\<in>set b. wf_mhead G sig rT \<and> (\<lambda>(maxl,b). wt_method G a (snd sig) rT maxl b (Phi a sig)) mb" 
+      from m b
+      show ?thesis
+      proof (rule bspec [elimify], clarsimp)
+        assume "wt_method G a ba ad ae bb (Phi a (ac, ba))"         
+        with wfprog uG ub b 1
+        show ?thesis
+          by - (rule wtl_method_complete [elimify], assumption+, simp add: make_Cert_def unique_epsilon)
+      qed 
+    qed
+  qed
 qed
 
 lemmas [simp] = split_paired_Ex