Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: dml022.cob Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/MicroJava/DFA/LBVComplete.thy
    Author:     Gerwin Klein
    Copyright   2000 Technische Universitaet Muenchen
*)

section \<open>Completeness of the LBV\<close>

theory LBVComplete
imports LBVSpec Typing_Framework
begin

definition is_target :: "['s step_type, 's list, nat] \ bool" where
  "is_target step phi pc' \
     (\<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (phi!pc)))"

definition make_cert :: "['s step_type, 's list, 's] \ 's certificate" where
  "make_cert step phi B =
     map (\<lambda>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 (\<lambda>pc. pc' \<noteq> pc+1 \<and> 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 \ \
  \<Longrightarrow> c!pc' = \<phi>!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 \ \ \
  \<Longrightarrow> c!pc = \<phi>!pc"
  by (auto simp add: cert_def make_cert_def nth_append)

lemma (in lbv) le_top [simp, intro]:
  "x <=_r \"
  using top by 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 \<forall>(pc', s')\<in>set ss1. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
      then (map snd [(p', t') \<leftarrow> ss1 . p'=pc+1]) ++_f x
      else \<top>)"
      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: if_split_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 \<forall>(pc', s')\<in>set ss2. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
      then map snd [(p', t') \<leftarrow> ss2 . p' = pc + 1] ++_f x
      else \<top>)"
      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: if_split_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 \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'
    then map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc
    else \<top>)" 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 \<phi>" by (rule boundedD)
    with s' suc_pc pc have "c!pc' = \<phi>!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')\<leftarrow> ?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: if_split_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 \<noteq> \<top>"
  (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 \<noteq> \<top>"
  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

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.