(* Title: HOL/MicroJava/BV/LBVComplete.thy Author: Gerwin Klein Copyright 2000 Technische Universitaet Muenchen *) section ‹Completeness of the LBV› theory LBVComplete imports LBVSpec Typing_Framework_1 begin definition is_target :: "'s step_type ⇒ 's list ⇒ nat ⇒ bool" where "is_target step τs pc' ⟷ (∃pc s'. pc' ≠ pc+1 ∧ pc < size τs ∧ (pc',s') ∈ set (step pc (τs!pc)))" definition make_cert :: "'s step_type ⇒ 's list ⇒ 's ⇒ 's certificate" where "make_cert step τs B = map (λpc. if is_target step τs pc then τs!pc else B) [0..<size τs] @ [B]" lemma [code]: "is_target step τs pc' = list_ex (λpc. pc' ≠ pc+1 ∧ List.member (map fst (step pc (τs!pc))) pc') [0..<size τs]" (*<*) apply (simp add: list_ex_iff is_target_def member_def) apply force done (*>*) locale lbvc = lbv + fixes τs :: "'a list" fixes c :: "'a list" defines cert_def: "c ≡ make_cert step τs ⊥" assumes mono: "mono r step (size τs) A" assumes pres: "pres_type step (size τs) A" assumes τs: "∀pc < size τs. τs!pc ∈ A ∧ τs!pc ≠ ⊤" assumes bounded: "bounded step (size τs)" assumes B_neq_T: "⊥ ≠ ⊤" lemma (in lbvc) cert: "cert_ok c (size τs) ⊤ ⊥ A" (*<*) proof (unfold cert_ok_def, intro strip conjI) note [simp] = make_cert_def cert_def nth_append show "c!size τs = ⊥" by simp fix pc assume pc: "pc < size τs" from pc τs B_A show "c!pc ∈ A" by simp from pc τs B_neq_T show "c!pc ≠ ⊤" by simp qed (*>*) lemmas [simp del] = split_paired_Ex lemma (in lbvc) cert_target [intro?]: "⟦ (pc',s') ∈ set (step pc (τs!pc)); pc' ≠ pc+1; pc < size τs; pc' < size τs ⟧ ⟹ c!pc' = τs!pc'" (*<*) by (auto simp add: cert_def make_cert_def nth_append is_target_def) (*>*) lemma (in lbvc) cert_approx [intro?]: "⟦ pc < size τs; c!pc ≠ ⊥ ⟧ ⟹ c!pc = τs!pc" (*<*) by (auto simp add: cert_def make_cert_def nth_append) (*>*) lemma (in lbv) le_top [simp, intro]: "x <=_r ⊤" (*<*) by (insert top) simp (*>*) lemma (in lbv) merge_mono: assumes less: "set ss⇩_{2}{⊑⇘r⇙} set ss⇩_{1}" assumes x: "x ∈ A" assumes ss⇩_{1}: "snd`set ss⇩_{1}⊆ A" assumes ss⇩_{2}: "snd`set ss⇩_{2}⊆ A" assumes boun: "∀x∈(fst`set ss⇩_{1}). x < size τs" assumes cert: "cert_ok c (size τs) T B A" shows "merge c pc ss⇩_{2}x ⊑⇩r merge c pc ss⇩_{1}x" (is "?s⇩_{2}⊑⇩r ?s⇩_{1}") (*<*) proof- have "?s⇩_{1}= ⊤ ⟹ ?thesis" by simp moreover { assume merge: "?s⇩_{1}≠ T" from x ss⇩_{1}have "?s⇩_{1}= (if ∀(pc',s')∈set ss⇩_{1}. pc' ≠ pc + 1 ⟶ s' ⊑⇩r c!pc' then (map snd [(p', t') ← ss⇩_{1}. p'=pc+1]) ⨆⇘f⇙ x else ⊤)" by (rule merge_def) with merge obtain app: "∀(pc',s')∈set ss⇩_{1}. pc' ≠ pc+1 ⟶ s' ⊑⇩r c!pc'" (is "?app ss⇩_{1}") and sum: "(map snd [(p',t') ← ss⇩_{1}. p' = pc+1] ⨆⇘f⇙ x) = ?s⇩_{1}" (is "?map ss⇩_{1}⨆⇘f⇙ x = _" is "?sum ss⇩_{1}= _") by (simp split: if_split_asm) have "?app ss⇩_{2}" proof(intro strip, clarsimp ) fix a b assume a_b: "(a, b) ∈ set ss⇩_{2}" and neq: "a ≠ Suc pc" from less a_b obtain y where y: "(a, y) ∈ set ss⇩_{1}" and b_lt_y: "b ⊑⇩r y" by (blast dest:lesub_step_typeD) with app have "a ≠ pc + 1 ⟶ y ⊑⇘r⇙ c!a" by auto with neq have "y ⊑⇘r⇙ c!a" by auto moreover from y ss⇩_{1}have "y ∈ A" by auto moreover from a_b ss⇩_{2}have "b ∈ A" by auto moreover from y boun cert have "c!a ∈ A" by (auto dest:cert_okD1) ultimately show "b ⊑⇘r⇙ c!a" using b_lt_y by (auto intro:trans_r) qed moreover { from ss⇩_{1}have map1: "set (?map ss⇩_{1}) ⊆ A" by auto with x and semilat Semilat_axioms have "?sum ss⇩_{1}∈ A" by (auto intro!: plusplus_closed) with sum have "?s⇩_{1}∈ A" by simp moreover have mapD: "⋀x ss. x ∈ set (?map ss) ⟹ ∃p. (p,x) ∈ set ss ∧ p=pc+1" by auto from x map1 have "∀x ∈ set (?map ss⇩_{1}). x ⊑⇩r ?sum ss⇩_{1}" by clarify (rule pp_ub1) with sum have "∀x ∈ set (?map ss⇩_{1}). x ⊑⇩r ?s⇩_{1}" by simp then have "∀x ∈ set (?map ss⇩_{2}). x ⊑⇩r ?s⇩_{1}" proof(intro strip, clarsimp) fix b assume xa: "∀xa. (Suc pc, xa) ∈set ss⇩_{1}⟶ xa ⊑⇘r⇙ merge c pc ss⇩_{1}x" and b: "(Suc pc, b) ∈ set ss⇩_{2}" from less b obtain y where y: "(Suc pc, y) ∈ set ss⇩_{1}" and b_lt_y: "b ⊑⇩r y" by (blast dest:lesub_step_typeD) from y xa have "y ⊑⇘r⇙ merge c pc ss⇩_{1}x" by auto moreover from y ss⇩_{1}have "y ∈ A" by auto moreover from b ss⇩_{2}have "b ∈ A" by auto moreover from ss⇩_{1}x have "merge c pc ss⇩_{1}x ∈ A" by (auto intro:merge_pres) ultimately show "b ⊑⇘r⇙ merge c pc ss⇩_{1}x" using b_lt_y by (auto intro:trans_r) qed moreover from map1 x have "x ⊑⇩r (?sum ss⇩_{1})" by (rule pp_ub2) with sum have "x ⊑⇩r ?s⇩_{1}" by simp moreover from ss⇩_{2}have "set (?map ss⇩_{2}) ⊆ A" by auto ultimately have "?sum ss⇩_{2}⊑⇩r ?s⇩_{1}" using x by - (rule pp_lub) } moreover from x ss⇩_{2}have "?s⇩_{2}= (if ∀(pc', s')∈set ss⇩_{2}. pc' ≠ pc + 1 ⟶ s' ⊑⇩r c!pc' then map snd [(p', t') ← ss⇩_{2}. p' = pc + 1] ⨆⇘f⇙ x else ⊤)" by (rule merge_def) ultimately have ?thesis by simp } ultimately show ?thesis by (cases "?s⇩_{1}= ⊤") auto qed (*>*) lemma (in lbvc) wti_mono: assumes less: "s⇩_{2}⊑⇩r s⇩_{1}" assumes pc: "pc < size τs" and s⇩_{1}: "s⇩_{1}∈ A" and s⇩_{2}: "s⇩_{2}∈ A" shows "wti c pc s⇩_{2}⊑⇩r wti c pc s⇩_{1}" (is "?s⇩_{2}' ⊑⇩r ?s⇩_{1}'") (*<*) proof - from bounded pc have "∀(q,τ) ∈ set(step pc s⇩_{1}). q < size τs" by (simp add:bounded_def) then have u: "∀q ∈ fst ` set (step pc s⇩_{1}). q < size τs" by auto from mono pc s⇩_{2}less have "set (step pc s⇩_{2}) {⊑⇘r⇙} set (step pc s⇩_{1})" by (rule monoD) moreover from cert B_A pc have "c!Suc pc ∈ A" by (rule cert_okD3) moreover from pres s⇩_{1}pc have "snd`set (step pc s⇩_{1}) ⊆ A" by (rule pres_typeD2) moreover from pres s⇩_{2}pc have "snd`set (step pc s⇩_{2}) ⊆ A" by (rule pres_typeD2) ultimately show ?thesis using cert u by (simp add: wti merge_mono) qed (*>*) lemma (in lbvc) wtc_mono: assumes less: "s⇩_{2}⊑⇩r s⇩_{1}" assumes pc: "pc < size τs" and s⇩_{1}: "s⇩_{1}∈ A" and s⇩_{2}: "s⇩_{2}∈ A" shows "wtc c pc s⇩_{2}⊑⇩r wtc c pc s⇩_{1}" (is "?s⇩_{2}' ⊑⇩r ?s⇩_{1}'") (*<*) proof (cases "c!pc = ⊥") case True moreover from less pc s⇩_{1}s⇩_{2}have "wti c pc s⇩_{2}⊑⇩r wti c pc s⇩_{1}" by (rule wti_mono) ultimately show ?thesis by (simp add: wtc) next case False with pc have "c!pc = τs!pc" using cert_approx by auto with τs pc have c_pc_inA: "c!pc ∈ A" by auto moreover from cert B_A pc have "c ! (pc + 1) ∈ A" by (auto dest: cert_okD3) ultimately have inA: "wtc c pc s⇩_{2}∈ A" using pres wtc_pres pc s⇩_{2}by auto have "?s⇩_{1}' = ⊤ ⟹ ?thesis" by simp moreover { assume "?s⇩_{1}' ≠ ⊤" with False have c: "s⇩_{1}⊑⇩r c!pc" by (simp add: wtc split: if_split_asm) from semilat have "order r A" by auto from this less c s⇩_{2}s⇩_{1}c_pc_inA have "s⇩_{2}⊑⇩r c!pc" by (rule order_trans) with False c have ?thesis using inA by (simp add: wtc) } ultimately show ?thesis by (cases "?s⇩_{1}' = ⊤") auto qed (*>*) lemma (in lbv) top_le_conv [simp]: "x ∈ A ⟹ ⊤ ⊑⇩r x = (x = ⊤)" (*<*) apply(subgoal_tac "order r A") apply (insert semilat T_A top) apply (rule top_le_conv) apply assumption+ apply (simp add:semilat_def) done (*>*) lemma (in lbv) neq_top [simp, elim]: "⟦ x ⊑⇩r y; y ≠ ⊤; y ∈ A ⟧ ⟹ x ≠ ⊤" (*<*) by (cases "x = T") auto (*>*) lemma (in lbvc) stable_wti: assumes stable: "stable r step τs pc" and pc: "pc < size τs" shows "wti c pc (τs!pc) ≠ ⊤" (*<*) proof - let ?step = "step pc (τs!pc)" from stable have less: "∀(q,s')∈set ?step. s' ⊑⇩r τs!q" by (simp add: stable_def) from cert B_A pc have cert_suc: "c!Suc pc ∈ A" by (rule cert_okD3) moreover from τs pc have "τs!pc ∈ A" by simp with pres pc have stepA: "snd`set ?step ⊆ A" by - (rule pres_typeD2) ultimately have "merge c pc ?step (c!Suc pc) = (if ∀(pc',s')∈set ?step. pc'≠pc+1 ⟶ s' ⊑⇩r c!pc' then map snd [(p',t') ← ?step.p'=pc+1] ⨆⇘f⇙ c!Suc pc else ⊤)" unfolding mrg_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms]) moreover { fix pc' s' assume s': "(pc',s') ∈ set ?step" and suc_pc: "pc' ≠ pc+1" with less have "s' ⊑⇩r τs!pc'" by auto also from bounded pc s' have "pc' < size τs" by (rule boundedD) with s' suc_pc pc have "c!pc' = τs!pc'" .. hence "τs!pc' = c!pc'" .. finally have "s' ⊑⇩r c!pc'" . } hence "∀(pc',s')∈set ?step. pc'≠pc+1 ⟶ s' ⊑⇩r c!pc'" by auto moreover from pc have "Suc pc = size τs ∨ Suc pc < size τs" by auto hence "map snd [(p',t') ← ?step.p'=pc+1] ⨆⇘f⇙ c!Suc pc ≠ ⊤" (is "?map ⨆⇘f⇙ _ ≠ _") proof (rule disjE) assume pc': "Suc pc = size τs" with cert have "c!Suc pc = ⊥" by (simp add: cert_okD2) moreover from pc' bounded pc have "∀(p',t')∈set ?step. p'≠pc+1" by clarify (drule boundedD, auto) hence "[(p',t') ← ?step. p'=pc+1] = []" by (blast intro: filter_False) hence "?map = []" by simp ultimately show ?thesis by (simp add: B_neq_T) next assume pc': "Suc pc < size τs" from pc' τs have τs_inA: "τs!Suc pc ∈ A" by simp moreover note cert_suc moreover from stepA have "set ?map ⊆ A" by auto moreover have "⋀s. s ∈ set ?map ⟹ ∃t. (Suc pc, t) ∈ set ?step" by auto with less have "∀s' ∈ set ?map. s' ⊑⇩r τs!Suc pc" by auto moreover from pc' τs_inA have "c!Suc pc ⊑⇩r τs!Suc pc" by (cases "c!Suc pc = ⊥") (auto dest: cert_approx) ultimately have "?map ⨆⇘f⇙ c!Suc pc ⊑⇩r τs!Suc pc" by (rule pp_lub) moreover from pc' τs have "τs!Suc pc ≠ ⊤" by simp ultimately show ?thesis using τs_inA by auto qed ultimately have "merge c pc ?step (c!Suc pc) ≠ ⊤" by simp thus ?thesis by (simp add: wti) qed (*>*) lemma (in lbvc) wti_less: assumes stable: "stable r step τs pc" and suc_pc: "Suc pc < size τs" shows "wti c pc (τs!pc) ⊑⇩r τs!Suc pc" (is "?wti ⊑⇩r _") (*<*) proof - let ?step = "step pc (τs!pc)" from stable have less: "∀(q,s')∈set ?step. s' ⊑⇩r τs!q" by (simp add: stable_def) from suc_pc have pc: "pc < size τs" by simp with cert B_A have cert_suc: "c!Suc pc ∈ A" by (rule cert_okD3) moreover from τs pc have "τs!pc ∈ A" by simp with pres pc have stepA: "snd`set ?step ⊆ A" by - (rule pres_typeD2) moreover from stable pc have "?wti ≠ ⊤" by (rule stable_wti) hence "merge c pc ?step (c!Suc pc) ≠ ⊤" by (simp add: wti) ultimately have "merge c pc ?step (c!Suc pc) = map snd [(p',t') ← ?step.p'=pc+1] ⨆⇘f⇙ c!Suc pc" by (rule merge_not_top_s) hence "?wti = …" (is "_ = (?map ⨆⇘f⇙ _)" is "_ = ?sum") by (simp add: wti) also { from suc_pc τs have τs_inA: "τs!Suc pc ∈ A" by simp moreover note cert_suc moreover from stepA have "set ?map ⊆ A" by auto moreover have "⋀s. s ∈ set ?map ⟹ ∃t. (Suc pc, t) ∈ set ?step" by auto with less have "∀s' ∈ set ?map. s' ⊑⇩r τs!Suc pc" by auto moreover from suc_pc τs_inA have "c!Suc pc ⊑⇩r τs!Suc pc" by (cases "c!Suc pc = ⊥") (auto dest: cert_approx) ultimately have "?sum ⊑⇩r τs!Suc pc" by (rule pp_lub) } finally show ?thesis . qed (*>*) lemma (in lbvc) stable_wtc: assumes stable: "stable r step τs pc" and pc: "pc < size τs" shows "wtc c pc (τs!pc) ≠ ⊤" (*<*) proof - from stable pc have wti: "wti c pc (τs!pc) ≠ ⊤" by (rule stable_wti) show ?thesis proof (cases "c!pc = ⊥") case True with wti show ?thesis by (simp add: wtc) next case False with pc have "c!pc = τs!pc" .. with False wti τs pc show ?thesis by (simp add: wtc) qed qed (*>*) lemma (in lbvc) wtc_less: assumes stable: "stable r step τs pc" and suc_pc: "Suc pc < size τs" shows "wtc c pc (τs!pc) ⊑⇩r τs!Suc pc" (is "?wtc ⊑⇩r _") (*<*) proof (cases "c!pc = ⊥") case True moreover from stable suc_pc have "wti c pc (τs!pc) ⊑⇩r τs!Suc pc" by (rule wti_less) ultimately show ?thesis by (simp add: wtc) next case False from suc_pc have pc: "pc < size τs" by simp with stable have "?wtc ≠ ⊤" by (rule stable_wtc) with False have "?wtc = wti c pc (c!pc)" by (unfold wtc) (simp split: if_split_asm) also from pc False have "c!pc = τs!pc" .. finally have "?wtc = wti c pc (τs!pc)" . also from stable suc_pc have "wti c pc (τs!pc) ⊑⇩r τs!Suc pc" by (rule wti_less) finally show ?thesis . qed (*>*) lemma (in lbvc) wt_step_wtl_lemma: assumes wt_step: "wt_step r ⊤ step τs" shows "⋀pc s. pc+size ls = size τs ⟹ s ⊑⇩r τs!pc ⟹ s ∈ A ⟹ s≠⊤ ⟹ wtl ls c pc s ≠ ⊤" (is "⋀pc s. _ ⟹ _ ⟹ _ ⟹ _ ⟹ ?wtl ls pc s ≠ _") (*<*) proof (induct ls) fix pc s assume "s≠⊤" thus "?wtl [] pc s ≠ ⊤" by simp next fix pc s i ls assume "⋀pc s. pc+size ls=size τs ⟹ s ⊑⇩r τs!pc ⟹ s ∈ A ⟹ s≠⊤ ⟹ ?wtl ls pc s ≠ ⊤" moreover assume pc_l: "pc + size (i#ls) = size τs" hence suc_pc_l: "Suc pc + size ls = size τs" by simp ultimately have IH: "⋀s. s ⊑⇩r τs!Suc pc ⟹ s ∈ A ⟹ s ≠ ⊤ ⟹ ?wtl ls (Suc pc) s ≠ ⊤" . from pc_l obtain pc: "pc < size τs" by simp with wt_step have stable: "stable r step τs pc" by (simp add: wt_step_def) moreover note pc ultimately have wt_τs: "wtc c pc (τs!pc) ≠ ⊤" by (rule stable_wtc) assume s_τs: "s ⊑⇩r τs!pc" assume sA: "s ∈ A" from τs pc have τs_pc:"τs!pc ∈ A" by auto moreover from cert pc have c1: "c!pc ∈ A" by (rule cert_okD1) moreover from cert B_A pc have c2: "c!Suc pc ∈ A" by (rule cert_okD3) ultimately have wtc1: "wtc c pc (τs!pc) ∈ A" and wtc2: "wtc c pc s ∈ A" using pres sA pc by (auto intro:wtc_pres) from s_τs pc τs_pc sA have wt_s_τs: "wtc c pc s ⊑⇩r wtc c pc (τs!pc)" by (rule wtc_mono) with wt_τs have wt_s: "wtc c pc s ≠ ⊤" using wtc1 by simp moreover assume s: "s ≠ ⊤" ultimately have "ls = [] ⟹ ?wtl (i#ls) pc s ≠ ⊤" by simp moreover { assume "ls ≠ []" with pc_l have suc_pc: "Suc pc < size τs" by (auto simp add: neq_Nil_conv) with stable have t: "wtc c pc (τs!pc) ⊑⇩r τs!Suc pc" by (rule wtc_less) from suc_pc τs have "τs!Suc pc ∈ A" by auto with t wt_s_τs wtc1 wtc2 have "wtc c pc s ⊑⇩r τs!Suc pc" by (auto intro: trans_r) moreover from cert suc_pc have "c!pc ∈ A" "c!(pc+1) ∈ A" by (auto simp add: cert_ok_def) from pres this sA pc have "wtc c pc s ∈ A" by (rule wtc_pres) ultimately have "?wtl ls (Suc pc) (wtc c pc s) ≠ ⊤" using IH wt_s by blast with s wt_s have "?wtl (i#ls) pc s ≠ ⊤" by simp } ultimately show "?wtl (i#ls) pc s ≠ ⊤" by (cases ls) blast+ qed (*>*) theorem (in lbvc) wtl_complete: assumes wt: "wt_step r ⊤ step τs" assumes s: "s ⊑⇩r τs!0" "s ∈ A" "s ≠ ⊤" and eq: "size ins = size τs" shows "wtl ins c 0 s ≠ ⊤" (*<*) proof - from eq have "0+size ins = size τs" by simp from wt this s show ?thesis by (rule wt_step_wtl_lemma) qed (*>*) end