(* Author: Gerwin Klein Copyright 1999 Technische Universitaet Muenchen *) section {* Correctness of the LBV *} theory LBVCorrect imports LBVSpec Typing_Framework begin locale lbvs = lbv + fixes s0 :: 'a ("s⇩_{0}") 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]" assumes bounded: "bounded step (length ins)" assumes cert: "cert_ok c (length ins) \<top> ⊥ A" assumes pres: "pres_type step (length ins) A" 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 lbvs) phi_Some [intro?]: "[| pc < length ins; c!pc ≠ ⊥ |] ==> φ ! pc = c ! pc" by (simp add: phi_def) lemma (in lbvs) phi_len [simp]: "length φ = length ins" by (simp add: phi_def) lemma (in lbvs) wtl_suc_pc: assumes all: "wtl ins c 0 s⇩_{0}≠ \<top>" assumes pc: "pc+1 < length ins" shows "wtl (take (pc+1) ins) c 0 s0 \<sqsubseteq>⇩_{r}φ!(pc+1)" proof - from all pc have "wtc c (pc+1) (wtl (take (pc+1) ins) c 0 s0) ≠ T" by (rule wtl_all) with pc show ?thesis by (simp add: phi_def wtc split: split_if_asm) qed lemma (in lbvs) wtl_stable: assumes wtl: "wtl ins c 0 s0 ≠ \<top>" 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 bounded pc step have pc': "pc' < length ins" by (rule boundedD) from wtl have tkpc: "wtl (take pc ins) c 0 s0 ≠ \<top>" (is "?s1 ≠ _") by (rule wtl_take) from wtl have s2: "wtl (take (pc+1) ins) c 0 s0 ≠ \<top>" (is "?s2 ≠ _") by (rule wtl_take) from wtl pc have wt_s1: "wtc c pc ?s1 ≠ \<top>" by (rule wtl_all) have c_Some: "∀pc t. pc < length ins --> c!pc ≠ ⊥ --> φ!pc = c!pc" by (simp add: phi_def) from pc have c_None: "c!pc = ⊥ ==> φ!pc = ?s1" .. 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) from pres cert s0 wtl pc have "?s1 ∈ A" by (rule wtl_pres) 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) show "s' <=_r φ!pc'" proof (cases "pc' = pc+1") case True 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) with inst have merge: "?s2 = merge c pc (?step pc) (c!(pc+1))" by (simp add: wti) also from s2 merge have "… ≠ \<top>" (is "?merge ≠ _") by simp with cert_in_A step_in_A have "?merge = (map snd [(p',t') \<leftarrow> ?step pc. p'=pc+1] ++_f (c!(pc+1)))" by (rule merge_not_top_s) finally have "s' <=_r ?s2" using step_in_A cert_in_A True step by (auto intro: pp_ub1') also from wtl pc1 have "?s2 <=_r φ!(pc+1)" by (rule wtl_suc_pc) also note True [symmetric] finally show ?thesis by simp next case False from wt_s1 inst have "merge c pc (?step pc) (c!(pc+1)) ≠ \<top>" by (simp add: wti) with step_in_A have "∀(pc', s')∈set (?step pc). pc'≠pc+1 --> s' <=_r c!pc'" by - (rule merge_not_top) with step False have ok: "s' <=_r c!pc'" by blast moreover from ok have "c!pc' = ⊥ ==> s' = ⊥" by simp moreover from c_Some pc' have "c!pc' ≠ ⊥ ==> φ!pc' = c!pc'" by auto ultimately show ?thesis by (cases "c!pc' = ⊥") auto qed qed lemma (in lbvs) phi_not_top: assumes wtl: "wtl ins c 0 s0 ≠ \<top>" assumes pc: "pc < length ins" shows "φ!pc ≠ \<top>" proof (cases "c!pc = ⊥") case False with pc have "φ!pc = c!pc" .. also from cert pc have "… ≠ \<top>" by (rule cert_okD4) finally show ?thesis . next case True with pc have "φ!pc = wtl (take pc ins) c 0 s0" .. also from wtl have "… ≠ \<top>" by (rule wtl_take) finally show ?thesis . qed lemma (in lbvs) phi_in_A: assumes wtl: "wtl ins c 0 s0 ≠ \<top>" assumes s0: "s0 ∈ A" shows "φ ∈ list (length ins) A" proof - { fix x assume "x ∈ set φ" then obtain xs ys where "φ = xs @ x # ys" by (auto simp add: in_set_conv_decomp) then obtain pc where pc: "pc < length φ" and x: "φ!pc = x" by (simp add: that [of "length xs"] nth_append) from pres cert wtl s0 pc have "wtl (take pc ins) c 0 s0 ∈ A" by (auto intro!: wtl_pres) moreover from pc have "pc < length ins" by simp with cert have "c!pc ∈ A" .. ultimately have "φ!pc ∈ A" using pc by (simp add: phi_def) hence "x ∈ A" using x by simp } hence "set φ ⊆ A" .. thus ?thesis by (unfold list_def) simp qed lemma (in lbvs) phi0: assumes wtl: "wtl ins c 0 s0 ≠ \<top>" assumes 0: "0 < length ins" shows "s0 <=_r φ!0" proof (cases "c!0 = ⊥") case True with 0 have "φ!0 = wtl (take 0 ins) c 0 s0" .. moreover have "wtl (take 0 ins) c 0 s0 = s0" by simp ultimately have "φ!0 = s0" by simp thus ?thesis by simp next case False with 0 have "phi!0 = c!0" .. moreover from wtl have "wtl (take 1 ins) c 0 s0 ≠ \<top>" by (rule wtl_take) with 0 False have "s0 <=_r c!0" by (auto simp add: neq_Nil_conv wtc split: split_if_asm) ultimately show ?thesis by simp qed theorem (in lbvs) wtl_sound: assumes wtl: "wtl ins c 0 s0 ≠ \<top>" assumes s0: "s0 ∈ A" shows "∃ts. wt_step r \<top> step ts" proof - have "wt_step r \<top> step φ" proof (unfold wt_step_def, intro strip conjI) fix pc assume "pc < length φ" then have pc: "pc < length ins" by simp with wtl show "φ!pc ≠ \<top>" by (rule phi_not_top) from wtl s0 pc show "stable r step φ pc" by (rule wtl_stable) qed thus ?thesis .. qed theorem (in lbvs) wtl_sound_strong: assumes wtl: "wtl ins c 0 s0 ≠ \<top>" assumes s0: "s0 ∈ A" assumes nz: "0 < length ins" shows "∃ts ∈ list (length ins) A. wt_step r \<top> step ts ∧ s0 <=_r ts!0" proof - from wtl s0 have "φ ∈ list (length ins) A" by (rule phi_in_A) moreover have "wt_step r \<top> step φ" proof (unfold wt_step_def, intro strip conjI) fix pc assume "pc < length φ" then have pc: "pc < length ins" by simp with wtl show "φ!pc ≠ \<top>" by (rule phi_not_top) from wtl s0 pc show "stable r step φ pc" by (rule wtl_stable) qed moreover from wtl nz have "s0 <=_r φ!0" by (rule phi0) ultimately show ?thesis by fast qed end