(* Author: Gerwin Klein Copyright 1999 Technische Universitaet Muenchen *) section ‹Correctness of the LBV› theory LBVCorrect imports LBVSpec Typing_Framework begin locale lbvs = lbv + fixes s⇩_{0}:: 'a fixes c :: "'a list" fixes ins :: "'b list" fixes τs :: "'a list" defines phi_def: "τs ≡ map (λpc. if c!pc = ⊥ then wtl (take pc ins) c 0 s⇩_{0}else c!pc) [0..<size ins]" assumes bounded: "bounded step (size ins)" assumes cert: "cert_ok c (size ins) ⊤ ⊥ A" assumes pres: "pres_type step (size ins) A" lemma (in lbvs) phi_None [intro?]: "⟦ pc < size ins; c!pc = ⊥ ⟧ ⟹ τs!pc = wtl (take pc ins) c 0 s⇩_{0}" (*<*) by (simp add: phi_def) (*>*) lemma (in lbvs) phi_Some [intro?]: "⟦ pc < size ins; c!pc ≠ ⊥ ⟧ ⟹ τs!pc = c!pc" (*<*) by (simp add: phi_def) (*>*) lemma (in lbvs) phi_len [simp]: "size τs = size ins" (*<*) by (simp add: phi_def) (*>*) lemma (in lbvs) wtl_suc_pc: assumes all: "wtl ins c 0 s⇩_{0}≠ ⊤" assumes pc: "pc+1 < size ins" shows "wtl (take (pc+1) ins) c 0 s⇩_{0}⊑⇩r τs!(pc+1)" (*<*) proof - from all pc have "wtc c (pc+1) (wtl (take (pc+1) ins) c 0 s⇩_{0}) ≠ T" by (rule wtl_all) with pc show ?thesis by (simp add: phi_def wtc split: if_split_asm) qed (*>*) lemma (in lbvs) wtl_stable: assumes wtl: "wtl ins c 0 s⇩_{0}≠ ⊤" assumes s⇩_{0}: "s⇩_{0}∈ A" and pc: "pc < size ins" shows "stable r step τs pc" (*<*) proof (unfold stable_def, clarify) fix pc' s' assume step: "(pc',s') ∈ set (step pc (τs ! pc))" (is "(pc',s') ∈ set (?step pc)") from bounded pc step have pc': "pc' < size ins" by (rule boundedD) have tkpc: "wtl (take pc ins) c 0 s⇩_{0}≠ ⊤" (is "?s⇩_{1}≠ _") using wtl by (rule wtl_take) have s⇩_{2}: "wtl (take (pc+1) ins) c 0 s⇩_{0}≠ ⊤" (is "?s⇩_{2}≠ _") using wtl by (rule wtl_take) from wtl pc have wt_s⇩_{1}: "wtc c pc ?s⇩_{1}≠ ⊤" by (rule wtl_all) have c_Some: "∀pc t. pc < size ins ⟶ c!pc ≠ ⊥ ⟶ τs!pc = c!pc" by (simp add: phi_def) have c_None: "c!pc = ⊥ ⟹ τs!pc = ?s⇩_{1}" using pc .. from wt_s⇩_{1}pc c_None c_Some have inst: "wtc c pc ?s⇩_{1}= wti c pc (τs!pc)" by (simp add: wtc split: if_split_asm) have "?s⇩_{1}∈ A" using pres cert s⇩_{0}wtl pc by (rule wtl_pres) with pc c_Some cert c_None have "τs!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 τs!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 < size ins" by simp with tkpc have "?s⇩_{2}= wtc c pc ?s⇩_{1}" by - (rule wtl_Suc) with inst have merge: "?s⇩_{2}= merge c pc (?step pc) (c!(pc+1))" by (simp add: wti) also from s⇩_{2}merge have "… ≠ ⊤" (is "?merge ≠ _") by simp with cert_in_A step_in_A have "?merge = (map snd [(p',t') ← ?step pc. p'=pc+1] ⨆⇘f⇙ c!(pc+1))" by (rule merge_not_top_s) finally have "s' ⊑⇩r ?s⇩_{2}" using step_in_A cert_in_A True step by (auto intro: pp_ub1') also from wtl pc1 have "?s⇩_{2}⊑⇩r τs!(pc+1)" by (rule wtl_suc_pc) also note True [symmetric] finally show ?thesis by simp next case False from wt_s⇩_{1}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'" 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' ≠ ⊥ ⟹ τs!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 s⇩_{0}≠ ⊤" and pc: "pc < size ins" shows "τs!pc ≠ ⊤" (*<*) proof (cases "c!pc = ⊥") case False with pc have "τs!pc = c!pc" .. also from cert pc have "… ≠ ⊤" by (rule cert_okD4) finally show ?thesis . next case True with pc have "τs!pc = wtl (take pc ins) c 0 s⇩_{0}" .. also from wtl have "… ≠ ⊤" by (rule wtl_take) finally show ?thesis . qed (*>*) lemma (in lbvs) phi_in_A: assumes wtl: "wtl ins c 0 s⇩_{0}≠ ⊤" and s⇩_{0}: "s⇩_{0}∈ A" shows "τs ∈ list (size ins) A" (*<*) proof - { fix x assume "x ∈ set τs" then obtain xs ys where "τs = xs @ x # ys" by (auto simp add: in_set_conv_decomp) then obtain pc where pc: "pc < size τs" and x: "τs!pc = x" by (simp add: that [of "size xs"] nth_append) from pres cert wtl s⇩_{0}pc have "wtl (take pc ins) c 0 s⇩_{0}∈ A" by (auto intro!: wtl_pres) moreover from pc have "pc < size ins" by simp with cert have "c!pc ∈ A" .. ultimately have "τs!pc ∈ A" using pc by (simp add: phi_def) hence "x ∈ A" using x by simp } hence "set τs ⊆ A" .. thus ?thesis by (unfold list_def) simp qed (*>*) lemma (in lbvs) phi0: assumes wtl: "wtl ins c 0 s⇩_{0}≠ ⊤" and 0: "0 < size ins" shows "s⇩_{0}⊑⇩r τs!0" (*<*) proof (cases "c!0 = ⊥") case True with 0 have "τs!0 = wtl (take 0 ins) c 0 s⇩_{0}" .. moreover have "wtl (take 0 ins) c 0 s⇩_{0}= s⇩_{0}" by simp ultimately have "τs!0 = s⇩_{0}" by simp thus ?thesis by simp next case False with 0 have "τs!0 = c!0" .. moreover have "wtl (take 1 ins) c 0 s⇩_{0}≠ ⊤" using wtl by (rule wtl_take) with 0 False have "s⇩_{0}⊑⇩r c!0" by (auto simp add: neq_Nil_conv wtc split: if_split_asm) ultimately show ?thesis by simp qed (*>*) theorem (in lbvs) wtl_sound: assumes wtl: "wtl ins c 0 s⇩_{0}≠ ⊤" and s⇩_{0}: "s⇩_{0}∈ A" shows "∃τs. wt_step r ⊤ step τs" (*<*) proof - have "wt_step r ⊤ step τs" proof (unfold wt_step_def, intro strip conjI) fix pc assume "pc < size τs" then obtain pc: "pc < size ins" by simp with wtl show "τs!pc ≠ ⊤" by (rule phi_not_top) from wtl s⇩_{0}pc show "stable r step τs pc" by (rule wtl_stable) qed thus ?thesis .. qed (*>*) theorem (in lbvs) wtl_sound_strong: assumes wtl: "wtl ins c 0 s⇩_{0}≠ ⊤" assumes s⇩_{0}: "s⇩_{0}∈ A" and ins: "0 < size ins" shows "∃τs ∈ list (size ins) A. wt_step r ⊤ step τs ∧ s⇩_{0}⊑⇩r τs!0" (*<*) proof - have "τs ∈ list (size ins) A" using wtl s⇩_{0}by (rule phi_in_A) moreover have "wt_step r ⊤ step τs" proof (unfold wt_step_def, intro strip conjI) fix pc assume "pc < size τs" then obtain pc: "pc < size ins" by simp with wtl show "τs!pc ≠ ⊤" by (rule phi_not_top) from wtl s⇩_{0}and pc show "stable r step τs pc" by (rule wtl_stable) qed moreover from wtl ins have "s⇩_{0}⊑⇩r τs!0" by (rule phi0) ultimately show ?thesis by fast qed (*>*) end