summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | kleing |

Thu, 04 Apr 2002 19:43:25 +0200 | |

changeset 13080 | d9feada9c486 |

parent 13079 | e7738aa7267f |

child 13081 | ab4a3aef3591 |

tuned

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