# 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" ("\") defines phi_def: - "\ \ map (\pc. if c!pc = \ then wtl (take pc ins) c 0 s0 else c!pc) - [0..length ins(]" + "\ \ map (\pc. if c!pc = \ 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) \ \ A" + assumes pres: "pres_type step (length ins) A" -lemma (in lbvc) phi_None [intro?]: +lemma (in lbvs) phi_None [intro?]: "\ pc < length ins; c!pc = \ \ \ \ ! 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?]: "\ pc < length ins; c!pc \ \ \ \ \ ! pc = c ! pc" by (simp add: phi_def) -lemma (in lbvc) phi_len [simp]: +lemma (in lbvs) phi_len [simp]: "length \ = 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 \ \" assumes pc: "pc+1 < length ins" shows "wtl (take (pc+1) ins) c 0 s0 <=_r \!(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 \ A" and - cert_ok: "cert_ok c (length ins) \ \ A" and - wtl: "wtl ins c 0 s0 \ \" and - pc: "pc < length ins" and - bounded: "bounded step (length ins)" +lemma (in lbvs) wtl_stable: + assumes wtl: "wtl ins c 0 s0 \ \" + assumes s0: "s0 \ A" + assumes pc: "pc < length ins" shows "stable r step \ pc" proof (unfold stable_def, clarify) fix pc' s' assume step: "(pc',s') \ set (step pc (\ ! pc))" (is "(pc',s') \ 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 \ \" (is "?s1 \ _") by (rule wtl_take) have s2: "wtl (take (pc+1) ins) c 0 s0 \ \" (is "?s2 \ _") by (rule wtl_take) - from wtl pc have cert: "wtc c pc ?s1 \ \" by (rule wtl_all) + from wtl pc have wt_s1: "wtc c pc ?s1 \ \" by (rule wtl_all) have c_Some: "\pc t. pc < length ins \ c!pc \ \ \ \!pc = c!pc" by (simp add: phi_def) have c_None: "c!pc = \ \ \!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 (\!pc)" by (simp add: wtc split: split_if_asm) have "?s1 \ A" by (rule wtl_pres) - with pc c_Some cert_ok c_None + with pc c_Some cert c_None have "\!pc \ A" by (cases "c!pc = \") (auto dest: cert_okD1) with pc pres have step_in_A: "snd`set (?step pc) \ A" by (auto dest: pres_typeD2) @@ -80,7 +79,7 @@ show "s' <=_r \!pc'" proof (cases "pc' = pc+1") case True - with pc' cert_ok + with pc' cert have cert_in_A: "c!(pc+1) \ 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)) \ \" by (simp add: wti) with step_in_A have "\(pc', s')\set (?step pc). pc'\pc+1 \ 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 \ \" - assumes crt: "cert_ok c (length ins) \ \ A" - assumes pc: "pc < length ins" + assumes pc: "pc < length ins" shows "\!pc \ \" proof (cases "c!pc = \") case False with pc have "\!pc = c!pc" .. - also from crt pc have "\ \ \" by (rule cert_okD4) + also from cert pc have "\ \ \" 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 \ \" - assumes "bounded step (length ins)" - assumes "s0 \ A" and "cert_ok c (length ins) \ \ A" - assumes "pres_type step (length ins) A" + assumes "s0 \ A" shows "\ts. wt_step r \ step ts" proof - have "wt_step r \ step \"