(* Title: HOL/MicroJava/DFA/LBVComplete.thy Author: Gerwin Klein Copyright 2000 Technische Universitaet Muenchen *) section ‹Completeness of the LBV› theory LBVComplete imports LBVSpec Typing_Framework begin definition is_target :: "['s step_type, 's list, nat] ⇒ bool" where "is_target step phi pc' ⟷ (∃pc s'. pc' ≠ pc+1 ∧ pc < length phi ∧ (pc',s') ∈ set (step pc (phi!pc)))" definition make_cert :: "['s step_type, 's list, 's] ⇒ 's certificate" where "make_cert step phi B = map (λpc. if is_target step phi pc then phi!pc else B) [0..<length phi] @ [B]" lemma [code]: "is_target step phi pc' = list_ex (λpc. pc' ≠ pc+1 ∧ List.member (map fst (step pc (phi!pc))) pc') [0..<length phi]" by (force simp: list_ex_iff member_def is_target_def) locale lbvc = lbv + fixes phi :: "'a list" ("φ") fixes c :: "'a list" defines cert_def: "c ≡ make_cert step φ ⊥" assumes mono: "mono r step (length φ) A" assumes pres: "pres_type step (length φ) A" assumes phi: "∀pc < length φ. φ!pc ∈ A ∧ φ!pc ≠ ⊤" assumes bounded: "bounded step (length φ)" assumes B_neq_T: "⊥ ≠ ⊤" lemma (in lbvc) cert: "cert_ok c (length φ) ⊤ ⊥ A" proof (unfold cert_ok_def, intro strip conjI) note [simp] = make_cert_def cert_def nth_append show "c!length φ = ⊥" by simp fix pc assume pc: "pc < length φ" from pc phi B_A show "c!pc ∈ A" by simp from pc phi 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 (φ!pc)); pc' ≠ pc+1; pc < length φ; pc' < length φ ⟧ ⟹ c!pc' = φ!pc'" by (auto simp add: cert_def make_cert_def nth_append is_target_def) lemma (in lbvc) cert_approx [intro?]: "⟦ pc < length φ; c!pc ≠ ⊥ ⟧ ⟹ c!pc = φ!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: "ss2 ≤|r| ss1" assumes x: "x ∈ A" assumes ss1: "snd`set ss1 ⊆ A" assumes ss2: "snd`set ss2 ⊆ A" shows "merge c pc ss2 x <=_r merge c pc ss1 x" (is "?s2 <=_r ?s1") proof- have "?s1 = ⊤ ⟹ ?thesis" by simp moreover { assume merge: "?s1 ≠ T" from x ss1 have "?s1 = (if ∀(pc', s')∈set ss1. pc' ≠ pc + 1 ⟶ s' <=_r c!pc' then (map snd [(p', t') ← ss1 . p'=pc+1]) ++_f x else ⊤)" by (rule merge_def) with merge obtain app: "∀(pc',s')∈set ss1. pc' ≠ pc+1 ⟶ s' <=_r c!pc'" (is "?app ss1") and sum: "(map snd [(p',t') ← ss1 . p' = pc+1] ++_f x) = ?s1" (is "?map ss1 ++_f x = _" is "?sum ss1 = _") by (simp split: split_if_asm) from app less have "?app ss2" by (blast dest: trans_r lesub_step_typeD) moreover { from ss1 have map1: "set (?map ss1) ⊆ A" by auto with x have "?sum ss1 ∈ A" by (auto intro!: plusplus_closed semilat) with sum have "?s1 ∈ 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 ss1). x <=_r ?sum ss1" by clarify (rule pp_ub1) with sum have "∀x ∈ set (?map ss1). x <=_r ?s1" by simp with less have "∀x ∈ set (?map ss2). x <=_r ?s1" by (fastforce dest!: mapD lesub_step_typeD intro: trans_r) moreover from map1 x have "x <=_r (?sum ss1)" by (rule pp_ub2) with sum have "x <=_r ?s1" by simp moreover from ss2 have "set (?map ss2) ⊆ A" by auto ultimately have "?sum ss2 <=_r ?s1" using x by - (rule pp_lub) } moreover from x ss2 have "?s2 = (if ∀(pc', s')∈set ss2. pc' ≠ pc + 1 ⟶ s' <=_r c!pc' then map snd [(p', t') ← ss2 . p' = pc + 1] ++_f x else ⊤)" by (rule merge_def) ultimately have ?thesis by simp } ultimately show ?thesis by (cases "?s1 = ⊤") auto qed lemma (in lbvc) wti_mono: assumes less: "s2 <=_r s1" assumes pc: "pc < length φ" assumes s1: "s1 ∈ A" assumes s2: "s2 ∈ A" shows "wti c pc s2 <=_r wti c pc s1" (is "?s2' <=_r ?s1'") proof - from mono pc s2 less have "step pc s2 ≤|r| step pc s1" by (rule monoD) moreover from cert B_A pc have "c!Suc pc ∈ A" by (rule cert_okD3) moreover from pres s1 pc have "snd`set (step pc s1) ⊆ A" by (rule pres_typeD2) moreover from pres s2 pc have "snd`set (step pc s2) ⊆ A" by (rule pres_typeD2) ultimately show ?thesis by (simp add: wti merge_mono) qed lemma (in lbvc) wtc_mono: assumes less: "s2 <=_r s1" assumes pc: "pc < length φ" assumes s1: "s1 ∈ A" assumes s2: "s2 ∈ A" shows "wtc c pc s2 <=_r wtc c pc s1" (is "?s2' <=_r ?s1'") proof (cases "c!pc = ⊥") case True moreover from less pc s1 s2 have "wti c pc s2 <=_r wti c pc s1" by (rule wti_mono) ultimately show ?thesis by (simp add: wtc) next case False have "?s1' = ⊤ ⟹ ?thesis" by simp moreover { assume "?s1' ≠ ⊤" with False have c: "s1 <=_r c!pc" by (simp add: wtc split: split_if_asm) with less have "s2 <=_r c!pc" .. with False c have ?thesis by (simp add: wtc) } ultimately show ?thesis by (cases "?s1' = ⊤") auto qed lemma (in lbv) top_le_conv [simp]: "⊤ <=_r x = (x = ⊤)" using semilat by (simp add: top) lemma (in lbv) neq_top [simp, elim]: "⟦ x <=_r y; y ≠ ⊤ ⟧ ⟹ x ≠ ⊤" by (cases "x = T") auto lemma (in lbvc) stable_wti: assumes stable: "stable r step φ pc" assumes pc: "pc < length φ" shows "wti c pc (φ!pc) ≠ ⊤" proof - let ?step = "step pc (φ!pc)" from stable have less: "∀(q,s')∈set ?step. s' <=_r φ!q" by (simp add: stable_def) from cert B_A pc have cert_suc: "c!Suc pc ∈ A" by (rule cert_okD3) moreover from phi pc have "φ!pc ∈ A" by simp from pres this 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 φ!pc'" by auto also from bounded pc s' have "pc' < length φ" by (rule boundedD) with s' suc_pc pc have "c!pc' = φ!pc'" .. hence "φ!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 = length φ ∨ Suc pc < length φ" 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 = length φ" 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 < length φ" from pc' phi have "φ!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 φ!Suc pc" by auto moreover from pc' have "c!Suc pc <=_r φ!Suc pc" by (cases "c!Suc pc = ⊥") (auto dest: cert_approx) ultimately have "?map ++_f c!Suc pc <=_r φ!Suc pc" by (rule pp_lub) moreover from pc' phi have "φ!Suc pc ≠ ⊤" by simp ultimately show ?thesis 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 φ pc" assumes suc_pc: "Suc pc < length φ" shows "wti c pc (φ!pc) <=_r φ!Suc pc" (is "?wti <=_r _") proof - let ?step = "step pc (φ!pc)" from stable have less: "∀(q,s')∈set ?step. s' <=_r φ!q" by (simp add: stable_def) from suc_pc have pc: "pc < length φ" by simp with cert B_A have cert_suc: "c!Suc pc ∈ A" by (rule cert_okD3) moreover from phi pc have "φ!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 phi have "φ!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 φ!Suc pc" by auto moreover from suc_pc have "c!Suc pc <=_r φ!Suc pc" by (cases "c!Suc pc = ⊥") (auto dest: cert_approx) ultimately have "?sum <=_r φ!Suc pc" by (rule pp_lub) } finally show ?thesis . qed lemma (in lbvc) stable_wtc: assumes stable: "stable r step phi pc" assumes pc: "pc < length φ" shows "wtc c pc (φ!pc) ≠ ⊤" proof - from stable pc have wti: "wti c pc (φ!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 = φ!pc" .. with False wti show ?thesis by (simp add: wtc) qed qed lemma (in lbvc) wtc_less: assumes stable: "stable r step φ pc" assumes suc_pc: "Suc pc < length φ" shows "wtc c pc (φ!pc) <=_r φ!Suc pc" (is "?wtc <=_r _") proof (cases "c!pc = ⊥") case True moreover from stable suc_pc have "wti c pc (φ!pc) <=_r φ!Suc pc" by (rule wti_less) ultimately show ?thesis by (simp add: wtc) next case False from suc_pc have pc: "pc < length φ" by simp with stable have "?wtc ≠ ⊤" by (rule stable_wtc) with False have "?wtc = wti c pc (c!pc)" by (unfold wtc) (simp split: split_if_asm) also from pc False have "c!pc = φ!pc" .. finally have "?wtc = wti c pc (φ!pc)" . also from stable suc_pc have "wti c pc (φ!pc) <=_r φ!Suc pc" by (rule wti_less) finally show ?thesis . qed lemma (in lbvc) wt_step_wtl_lemma: assumes wt_step: "wt_step r ⊤ step φ" shows "⋀pc s. pc+length ls = length φ ⟹ s <=_r φ!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+length ls=length φ ⟹ s <=_r φ!pc ⟹ s ∈ A ⟹ s≠⊤ ⟹ ?wtl ls pc s ≠ ⊤" moreover assume pc_l: "pc + length (i#ls) = length φ" hence suc_pc_l: "Suc pc + length ls = length φ" by simp ultimately have IH: "⋀s. s <=_r φ!Suc pc ⟹ s ∈ A ⟹ s ≠ ⊤ ⟹ ?wtl ls (Suc pc) s ≠ ⊤" . from pc_l obtain pc: "pc < length φ" by simp with wt_step have stable: "stable r step φ pc" by (simp add: wt_step_def) from this pc have wt_phi: "wtc c pc (φ!pc) ≠ ⊤" by (rule stable_wtc) assume s_phi: "s <=_r φ!pc" from phi pc have phi_pc: "φ!pc ∈ A" by simp assume s: "s ∈ A" with s_phi pc phi_pc have wt_s_phi: "wtc c pc s <=_r wtc c pc (φ!pc)" by (rule wtc_mono) with wt_phi have wt_s: "wtc c pc s ≠ ⊤" 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 < length φ" by (auto simp add: neq_Nil_conv) with stable have "wtc c pc (phi!pc) <=_r φ!Suc pc" by (rule wtc_less) with wt_s_phi have "wtc c pc s <=_r φ!Suc pc" by (rule 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 s 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 φ" and s: "s <=_r φ!0" "s ∈ A" "s ≠ ⊤" and len: "length ins = length phi" shows "wtl ins c 0 s ≠ ⊤" proof - from len have "0+length ins = length phi" by simp from wt this s show ?thesis by (rule wt_step_wtl_lemma) qed end