# HG changeset patch
# User kleing
# Date 1017942205 -7200
# Node ID d9feada9c486c97417dcb5556e862655b6ff9f88
# Parent  e7738aa7267f441cfa1aa4da561db20555446df5
tuned

diff -r e7738aa7267f -r d9feada9c486 src/HOL/MicroJava/BV/LBVCorrect.thy
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Thu Apr 04 17:32:52 2002 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Thu Apr 04 19:43:25 2002 +0200
@@ -8,30 +8,34 @@
 
 theory LBVCorrect = LBVSpec + Typing_Framework:
 
-locale lbvc = lbv +
+locale lbvs = lbv +
   fixes s0  :: 'a
   fixes c   :: "'a list"
   fixes ins :: "'b list"
   fixes phi :: "'a list" ("\<phi>")
   defines phi_def:
-  "\<phi> \<equiv>  map (\<lambda>pc. if c!pc = \<bottom> then wtl (take pc ins) c 0 s0 else c!pc) 
-        [0..length ins(]"
+  "\<phi> \<equiv> map (\<lambda>pc. if c!pc = \<bottom> then wtl (take pc ins) c 0 s0 else c!pc) 
+       [0..length ins(]"
+
+  assumes bounded: "bounded step (length ins)"
+  assumes cert: "cert_ok c (length ins) \<top> \<bottom> A"
+  assumes pres: "pres_type step (length ins) A"
 
 
-lemma (in lbvc) phi_None [intro?]:
+lemma (in lbvs) phi_None [intro?]:
   "\<lbrakk> pc < length ins; c!pc = \<bottom> \<rbrakk> \<Longrightarrow> \<phi> ! pc = wtl (take pc ins) c 0 s0"
   by (simp add: phi_def)
 
-lemma (in lbvc) phi_Some [intro?]:
+lemma (in lbvs) phi_Some [intro?]:
   "\<lbrakk> pc < length ins; c!pc \<noteq> \<bottom> \<rbrakk> \<Longrightarrow> \<phi> ! pc = c ! pc"
   by (simp add: phi_def)
 
-lemma (in lbvc) phi_len [simp]:
+lemma (in lbvs) phi_len [simp]:
   "length \<phi> = length ins"
   by (simp add: phi_def)
 
 
-lemma (in lbvc) wtl_suc_pc:
+lemma (in lbvs) wtl_suc_pc:
   assumes all: "wtl ins c 0 s0 \<noteq> \<top>" 
   assumes pc:  "pc+1 < length ins"
   shows "wtl (take (pc+1) ins) c 0 s0 <=_r \<phi>!(pc+1)"
@@ -42,37 +46,32 @@
 qed
 
 
-lemma (in lbvc) wtl_stable:
-  assumes
-    pres:    "pres_type step (length ins) A" and
-    s0_in_A: "s0 \<in> A" and
-    cert_ok: "cert_ok c (length ins) \<top> \<bottom> A" and
-    wtl:     "wtl ins c 0 s0 \<noteq> \<top>" and
-    pc:      "pc < length ins" and
-    bounded: "bounded step (length ins)"
+lemma (in lbvs) wtl_stable:
+  assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>" 
+  assumes s0:  "s0 \<in> A" 
+  assumes pc:  "pc < length ins" 
   shows "stable r step \<phi> pc"
 proof (unfold stable_def, clarify)
   fix pc' s' assume step: "(pc',s') \<in> set (step pc (\<phi> ! pc))" 
                       (is "(pc',s') \<in> set (?step pc)")
   
-  from step pc bounded have pc': "pc' < length ins"
-    by (unfold bounded_def) blast
+  from bounded pc step have pc': "pc' < length ins" by (rule boundedD)
 
   have tkpc: "wtl (take pc ins) c 0 s0 \<noteq> \<top>" (is "?s1 \<noteq> _") by (rule wtl_take)
   have s2: "wtl (take (pc+1) ins) c 0 s0 \<noteq> \<top>" (is "?s2 \<noteq> _") by (rule wtl_take)
   
-  from wtl pc have cert: "wtc c pc ?s1 \<noteq> \<top>" by (rule wtl_all)
+  from wtl pc have wt_s1: "wtc c pc ?s1 \<noteq> \<top>" by (rule wtl_all)
 
   have c_Some: "\<forall>pc t. pc < length ins \<longrightarrow> c!pc \<noteq> \<bottom> \<longrightarrow> \<phi>!pc = c!pc" 
     by (simp add: phi_def)
   have c_None: "c!pc = \<bottom> \<Longrightarrow> \<phi>!pc = ?s1" ..
 
-  from cert pc c_None c_Some
+  from wt_s1 pc c_None c_Some
   have inst: "wtc c pc ?s1  = wti c pc (\<phi>!pc)"
     by (simp add: wtc split: split_if_asm)
 
   have "?s1 \<in> A" by (rule wtl_pres) 
-  with pc c_Some cert_ok c_None
+  with pc c_Some cert c_None
   have "\<phi>!pc \<in> A" by (cases "c!pc = \<bottom>") (auto dest: cert_okD1)
   with pc pres
   have step_in_A: "snd`set (?step pc) \<subseteq> A" by (auto dest: pres_typeD2)
@@ -80,7 +79,7 @@
   show "s' <=_r \<phi>!pc'" 
   proof (cases "pc' = pc+1")
     case True
-    with pc' cert_ok
+    with pc' cert
     have cert_in_A: "c!(pc+1) \<in> A" by (auto dest: cert_okD1)
     from True pc' have pc1: "pc+1 < length ins" by simp
     with tkpc have "?s2 = wtc c pc ?s1" by - (rule wtl_Suc)
@@ -100,7 +99,7 @@
     finally show ?thesis by simp    
   next
     case False
-    from cert inst
+    from wt_s1 inst
     have "merge c pc (?step pc) (c!(pc+1)) \<noteq> \<top>" by (simp add: wti)
     with step_in_A
     have "\<forall>(pc', s')\<in>set (?step pc). pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" 
@@ -119,15 +118,14 @@
 qed
 
   
-lemma (in lbvc) phi_not_top:
+lemma (in lbvs) phi_not_top:
   assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"
-  assumes crt: "cert_ok c (length ins) \<top> \<bottom> A"
-  assumes pc: "pc < length ins"
+  assumes pc:  "pc < length ins"
   shows "\<phi>!pc \<noteq> \<top>"
 proof (cases "c!pc = \<bottom>")
   case False with pc
   have "\<phi>!pc = c!pc" ..
-  also from crt pc have "\<dots> \<noteq> \<top>" by (rule cert_okD4)
+  also from cert pc have "\<dots> \<noteq> \<top>" by (rule cert_okD4)
   finally show ?thesis .
 next
   case True with pc
@@ -137,11 +135,9 @@
 qed
     
 
-theorem (in lbvc) wtl_sound:
+theorem (in lbvs) wtl_sound:
   assumes "wtl ins c 0 s0 \<noteq> \<top>" 
-  assumes "bounded step (length ins)"
-  assumes "s0 \<in> A" and "cert_ok c (length ins) \<top> \<bottom> A"
-  assumes "pres_type step (length ins) A"
+  assumes "s0 \<in> A" 
   shows "\<exists>ts. wt_step r \<top> step ts"
 proof -  
   have "wt_step r \<top> step \<phi>"