src/HOL/MicroJava/BV/LBVSpec.thy

 
 theory LBVSpec = Step :
 
 types
   certificate       = "state_type option list" 
-  class_certificate = "sig \\<Rightarrow> certificate"
-  prog_certificate  = "cname \\<Rightarrow> class_certificate"
+  class_certificate = "sig \<Rightarrow> certificate"
+  prog_certificate  = "cname \<Rightarrow> class_certificate"
 
 constdefs
-wtl_inst :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
-
-"wtl_inst i G rT s s' cert max_pc pc \\<equiv> app (i,G,rT,s) \\<and> 
+wtl_inst :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \<Rightarrow> bool"
+
+"wtl_inst i G rT s s' cert max_pc pc \<equiv> app (i,G,rT,s) \<and> 
                                        (let s'' = the (step (i,G,s)) in
-                                          (\\<forall> pc' \\<in> (succs i pc). pc' < max_pc \\<and>  
-                                             ((pc' \\<noteq> pc+1) \\<longrightarrow> cert!pc' \\<noteq> None \\<and> G \\<turnstile> s'' <=s the (cert!pc'))) \\<and>  
-                                          (if (pc+1) \\<in> (succs i pc) then  
+                                          (\<forall> pc' \<in> (succs i pc). pc' < max_pc \<and>  
+                                             ((pc' \<noteq> pc+1) \<longrightarrow> cert!pc' \<noteq> None \<and> G \<turnstile> s'' <=s the (cert!pc'))) \<and>  
+                                          (if (pc+1) \<in> (succs i pc) then  
                                              s' = s'' 
                                            else 
                                              cert ! (pc+1) = Some s'))" 
 
 lemma [simp]: 
-"succs i pc = {pc+1} \\<Longrightarrow> 
-  wtl_inst i G rT s s' cert max_pc pc = (app (i,G,rT,s) \\<and> pc+1 < max_pc \\<and> (s' = the (step (i,G,s))))"
+"succs i pc = {pc+1} \<Longrightarrow> 
+  wtl_inst i G rT s s' cert max_pc pc = (app (i,G,rT,s) \<and> pc+1 < max_pc \<and> (s' = the (step (i,G,s))))"
 by (unfold wtl_inst_def, auto)
 
 lemma [simp]:
-"succs i pc = {} \\<Longrightarrow> wtl_inst i G rT s s' cert max_pc pc = (app (i,G,rT,s) \\<and> cert!(pc+1) = Some s')"
+"succs i pc = {} \<Longrightarrow> wtl_inst i G rT s s' cert max_pc pc = (app (i,G,rT,s) \<and> cert!(pc+1) = Some s')"
 by (unfold wtl_inst_def, auto)
 
 
 constdefs
-wtl_inst_option :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
-"wtl_inst_option i G rT s0 s1 cert max_pc pc \\<equiv>
+wtl_inst_option :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \<Rightarrow> bool"
+"wtl_inst_option i G rT s0 s1 cert max_pc pc \<equiv>
      (case cert!pc of 
-          None     \\<Rightarrow> wtl_inst i G rT s0 s1 cert max_pc pc
-        | Some s0' \\<Rightarrow> (G \\<turnstile> s0 <=s s0') \\<and>
+          None     \<Rightarrow> wtl_inst i G rT s0 s1 cert max_pc pc
+        | Some s0' \<Rightarrow> (G \<turnstile> s0 <=s s0') \<and>
                       wtl_inst i G rT s0' s1 cert max_pc pc)"
   
 consts
- wtl_inst_list :: "[instr list,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
+ wtl_inst_list :: "[instr list,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \<Rightarrow> bool"
 primrec
   "wtl_inst_list [] G rT s0 s2 cert max_pc pc = (s0 = s2)"
 
   "wtl_inst_list (instr#is) G rT s0 s2 cert max_pc pc =
-     (\\<exists>s1. wtl_inst_option instr G rT s0 s1 cert max_pc pc \\<and> 
+     (\<exists>s1. wtl_inst_option instr G rT s0 s1 cert max_pc pc \<and> 
            wtl_inst_list is G rT s1 s2 cert max_pc (pc+1))"
 
 constdefs
- wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] \\<Rightarrow> bool" 
- "wtl_method G C pTs rT mxl ins cert \\<equiv> 
+ wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] \<Rightarrow> bool" 
+ "wtl_method G C pTs rT mxl ins cert \<equiv> 
 	let max_pc = length ins 
         in 
-	0 < max_pc \\<and>  
-        (\\<exists>s2. wtl_inst_list ins G rT 
+	0 < max_pc \<and>  
+        (\<exists>s2. wtl_inst_list ins G rT 
                             ([],(Some(Class C))#((map Some pTs))@(replicate mxl None))
                             s2 cert max_pc 0)"
 
- wtl_jvm_prog :: "[jvm_prog,prog_certificate] \\<Rightarrow> bool"
- "wtl_jvm_prog G cert \\<equiv> 
-    wf_prog (\\<lambda>G C (sig,rT,maxl,b). 
+ wtl_jvm_prog :: "[jvm_prog,prog_certificate] \<Rightarrow> bool"
+ "wtl_jvm_prog G cert \<equiv> 
+    wf_prog (\<lambda>G C (sig,rT,maxl,b). 
                wtl_method G C (snd sig) rT maxl b (cert C sig)) G" 
 
 text {* \medskip *}
 
-lemma rev_eq: "\\<lbrakk>length a = n; length x = n; rev a @ b # c = rev x @ y # z\\<rbrakk> \\<Longrightarrow> a = x \\<and> b = y \\<and> c = z"
+lemma rev_eq: "\<lbrakk>length a = n; length x = n; rev a @ b # c = rev x @ y # z\<rbrakk> \<Longrightarrow> a = x \<and> b = y \<and> c = z"
 by auto
 
 lemma wtl_inst_unique: 
-"wtl_inst i G rT s0 s1 cert max_pc pc \\<longrightarrow>
- wtl_inst i G rT s0 s1' cert max_pc pc \\<longrightarrow> s1 = s1'" (is "?P i")
+"wtl_inst i G rT s0 s1 cert max_pc pc \<longrightarrow>
+ wtl_inst i G rT s0 s1' cert max_pc pc \<longrightarrow> s1 = s1'" (is "?P i")
 by (unfold wtl_inst_def, auto)
 
 lemma wtl_inst_option_unique:
-"\\<lbrakk>wtl_inst_option i G rT s0 s1 cert max_pc pc; 
-  wtl_inst_option i G rT s0 s1' cert max_pc pc\\<rbrakk> \\<Longrightarrow> s1 = s1'"
+"\<lbrakk>wtl_inst_option i G rT s0 s1 cert max_pc pc; 
+  wtl_inst_option i G rT s0 s1' cert max_pc pc\<rbrakk> \<Longrightarrow> s1 = s1'"
 by (cases "cert!pc") (auto simp add: wtl_inst_unique wtl_inst_option_def)
 
 lemma wtl_inst_list_unique: 
-"\\<forall> s0 pc. wtl_inst_list is G rT s0 s1 cert max_pc pc \\<longrightarrow> 
- wtl_inst_list is G rT s0 s1' cert max_pc pc \\<longrightarrow> s1=s1'" (is "?P is")
-proof (induct "?P" "is") 
+"\<forall> s0 pc. wtl_inst_list is G rT s0 s1 cert max_pc pc \<longrightarrow> 
+ wtl_inst_list is G rT s0 s1' cert max_pc pc \<longrightarrow> s1=s1'" (is "?P is")
+proof (induct (open) ?P "is")
   case Nil
   show "?P []" by simp
 
   case Cons
   show "?P (a # list)" 

     show "s1 = s1'" by blast
   qed
 qed
         
 lemma wtl_partial:
-"\\<forall> pc' pc s. 
-   wtl_inst_list is G rT s s' cert mpc pc \\<longrightarrow> \
-   pc' < length is \\<longrightarrow> \
-   (\\<exists> a b s1. a @ b = is \\<and> length a = pc' \\<and> \
-              wtl_inst_list a G rT s  s1 cert mpc pc \\<and> \
+"\<forall> pc' pc s. 
+   wtl_inst_list is G rT s s' cert mpc pc \<longrightarrow> \
+   pc' < length is \<longrightarrow> \
+   (\<exists> a b s1. a @ b = is \<and> length a = pc' \<and> \
+              wtl_inst_list a G rT s  s1 cert mpc pc \<and> \
               wtl_inst_list b G rT s1 s' cert mpc (pc+length a))" (is "?P is")
-proof (induct "?P" "is")
+proof (induct (open) ?P "is")
   case Nil
   show "?P []" by auto
   
   case Cons
   show "?P (a#list)"
   proof (intro allI impI)
     fix pc' pc s
     assume length: "pc' < length (a # list)"
     assume wtl:    "wtl_inst_list (a # list) G rT s s' cert mpc pc"
-    show "\\<exists> a' b s1. 
-            a' @ b = a#list \\<and> length a' = pc' \\<and> \
-            wtl_inst_list a' G rT s  s1 cert mpc pc \\<and> \
+    show "\<exists> a' b s1. 
+            a' @ b = a#list \<and> length a' = pc' \<and> \
+            wtl_inst_list a' G rT s  s1 cert mpc pc \<and> \
             wtl_inst_list b G rT s1 s' cert mpc (pc+length a')"
-        (is "\\<exists> a b s1. ?E a b s1")
-    proof (cases "pc'")
+        (is "\<exists> a b s1. ?E a b s1")
+    proof (cases (open) pc')
       case 0
       with wtl
       have "?E [] (a#list) s" by simp
       thus ?thesis by blast
     next

     qed
   qed
 qed
 
 lemma "wtl_append1":
-"\\<lbrakk>wtl_inst_list x G rT s0 s1 cert (length (x@y)) 0; 
-  wtl_inst_list y G rT s1 s2 cert (length (x@y)) (length x)\\<rbrakk> \\<Longrightarrow>
+"\<lbrakk>wtl_inst_list x G rT s0 s1 cert (length (x@y)) 0; 
+  wtl_inst_list y G rT s1 s2 cert (length (x@y)) (length x)\<rbrakk> \<Longrightarrow>
   wtl_inst_list (x@y) G rT s0 s2 cert (length (x@y)) 0"
 proof -
   assume w:
     "wtl_inst_list x G rT s0 s1 cert (length (x@y)) 0"
     "wtl_inst_list y G rT s1 s2 cert (length (x@y)) (length x)"
 
   have
-    "\\<forall> pc s0. 
-    wtl_inst_list x G rT s0 s1 cert (pc+length (x@y)) pc \\<longrightarrow> 
-    wtl_inst_list y G rT s1 s2 cert (pc+length (x@y)) (pc+length x) \\<longrightarrow>
+    "\<forall> pc s0. 
+    wtl_inst_list x G rT s0 s1 cert (pc+length (x@y)) pc \<longrightarrow> 
+    wtl_inst_list y G rT s1 s2 cert (pc+length (x@y)) (pc+length x) \<longrightarrow>
     wtl_inst_list (x@y) G rT s0 s2 cert (pc+length (x@y)) pc" (is "?P x")
-  proof (induct "?P" "x")
+  proof (induct (open) ?P x)
     case Nil
     show "?P []" by simp
   next
     case Cons
     show "?P (a#list)" 

     from w show "wtl_inst_list x G rT s0 s1 cert (0+length (x @ y)) 0" by simp
   qed simp+
 qed
 
 lemma wtl_cons_appendl:
-"\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; 
+"\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; 
   wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a); 
-  wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\\<rbrakk> \\<Longrightarrow> 
+  wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\<rbrakk> \<Longrightarrow> 
   wtl_inst_list (a@i#b) G rT s0 s3 cert (length (a@i#b)) 0"
 proof -
   assume a: "wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0"
 
   assume "wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a)"

   with a
   show ?thesis by (rule wtl_append1)
 qed
 
 lemma "wtl_append":
-"\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; 
+"\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; 
   wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a); 
-  wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\\<rbrakk> \\<Longrightarrow> 
+  wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\<rbrakk> \<Longrightarrow> 
   wtl_inst_list (a@[i]) G rT s0 s2 cert (length (a@i#b)) 0"
 proof -
   assume a: "wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0"
   assume i: "wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a)"
   assume b: "wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))"
 
-  have "\\<forall> s0 pc. wtl_inst_list a G rT s0 s1 cert (pc+length (a@i#b)) pc \\<longrightarrow> 
-        wtl_inst_option i G rT s1 s2 cert (pc+length (a@i#b)) (pc + length a) \\<longrightarrow> 
-        wtl_inst_list b G rT s2 s3 cert (pc+length (a@i#b)) (Suc pc + length a) \\<longrightarrow> 
+  have "\<forall> s0 pc. wtl_inst_list a G rT s0 s1 cert (pc+length (a@i#b)) pc \<longrightarrow> 
+        wtl_inst_option i G rT s1 s2 cert (pc+length (a@i#b)) (pc + length a) \<longrightarrow> 
+        wtl_inst_list b G rT s2 s3 cert (pc+length (a@i#b)) (Suc pc + length a) \<longrightarrow> 
           wtl_inst_list (a@[i]) G rT s0 s2 cert (pc+length (a@i#b)) pc" (is "?P a")
-  proof (induct "?P" "a")
+  proof (induct (open) ?P a)
     case Nil
     show "?P []" by (simp del: split_paired_Ex)
     case Cons
-    show "?P (a#list)" (is "\\<forall>s0 pc. ?x s0 pc \\<longrightarrow> ?y s0 pc \\<longrightarrow> ?z s0 pc \\<longrightarrow> ?p s0 pc") 
+    show "?P (a#list)" (is "\<forall>s0 pc. ?x s0 pc \<longrightarrow> ?y s0 pc \<longrightarrow> ?z s0 pc \<longrightarrow> ?p s0 pc") 
     proof intro
       fix s0 pc
       assume y: "?y s0 pc"
       assume z: "?z s0 pc"
       assume "?x s0 pc"