--- 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>"