Quelle  LBVCorrect.thy

(*
    Author:     Gerwin Klein
    Copyright   1999 Technische Universitaet Muenchen
*)

section ‹Correctness of the LBV›

theory LBVCorrect
imports LBVSpec Typing_Framework_1
begin

locale lbvs = lbv +
  fixes s₀  :: '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₀ 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₀"
(*<*) 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₀ ≠ ⊤" 
  assumes pc:  "pc+1 < size ins"
  assumes sA: "s₀ ∈ A" 
  shows "wtl (take (pc+1) ins) c 0 s₀ ⊑_r τs!(pc+1)"
(*<*)
proof -
  from all pc
  have "wtc c (pc+1) (wtl (take (pc+1) ins) c 0 s₀) ≠ T" by (rule wtl_all)
  with pc show ?thesis using sA pres cert all wtl_pres by (simp add: phi_def wtc split: if_split_asm)
qed
(*>*)

lemma (in lbvs) wtl_stable:
  assumes wtl: "wtl ins c 0 s₀ ≠ ⊤" 
  assumes s₀:  "s₀ ∈ 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₀ ≠ ⊤" (is "?s₁ ≠ _") using wtl by (rule wtl_take)
  have s₂: "wtl (take (pc+1) ins) c 0 s₀ ≠ ⊤" (is "?s₂ ≠ _") using wtl by (rule wtl_take)
  
  from wtl pc have wt_s₁: "wtc c pc ?s₁ ≠ ⊤" 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₁" using pc ..

  from wt_s₁ pc c_None c_Some
  have inst: "wtc c pc ?s₁ = wti c pc (τs!pc)"
    by (simp add: wtc split: if_split_asm)

  have "?s₁ ∈ A" using pres cert s₀ 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)
  then have inA1: "s' ∈ A" using step by auto

  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 pres cert s₀ wtl have inA2: "wtl (take (pc + 1) ins) c 0 s₀ ∈ A" by (auto dest:wtl_pres)

    have c_None': "c!(pc +1)= ⊥ ==> τs!(pc + 1)= ?s₂" using pc1 ..
    have "?s₂ ∈ A" using pres cert s₀ wtl pc1 by (rule wtl_pres)
    with pc1 c_Some cert c_None'
    have inA3: "τs!(pc+1) ∈ A" by (cases "c!(pc+1) = ⊥") (auto dest: cert_okD1)

    from pc1 tkpc have "?s₂ = wtc c pc ?s₁" by - (rule wtl_Suc)
    with inst 
    have merge: "?s₂ = merge c pc (?step pc) (c!(pc+1))" by (simp add: wti)
    also from s₂ merge have "… ≠ ⊤" (is "?merge ≠ _") by simp
    with cert_in_A step_in_A
    have "?merge = (map snd [(p',t') ← ?step pc. p'=pc+1] ⊔ c!(pc+1))"
      by (rule merge_not_top_s) 
    finally have "s' ⊑_r ?s₂" using step_in_A cert_in_A True step 
      by (auto intro: pp_ub1')
    also from wtl pc1 have "?s₂ ⊑_r τs!(pc+1)" using s₀ by (auto dest: wtl_suc_pc)
    also note True [symmetric]
    finally show ?thesis  using inA1 inA2 inA3 by simp    
  next
    case False
    from wt_s₁ 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' = ⊥" using inA1 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₀ ≠ ⊤" 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₀" ..
  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₀ ≠ ⊤" and s₀: "s₀ ∈ A"
  shows "τs ∈ nlists (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₀ pc 
    have "wtl (take pc ins) c 0 s₀ ∈ 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 nlists_def) simp
qed
(*>*)

lemma (in lbvs) phi0:
  assumes wtl: "wtl ins c 0 s₀ ≠ ⊤" and 0: "0 < size ins" and s₀: "s₀ ∈ A" 
  shows "s₀ ⊑_r τs!0"
(*<*)
proof (cases "c!0 = ⊥")
  case True
  with 0 have "τs!0 = wtl (take 0 ins) c 0 s₀" ..
  moreover have "wtl (take 0 ins) c 0 s₀ = s₀" by simp
  ultimately have "τs!0 = s₀" by simp
  thus ?thesis using s₀ by simp
next
  case False
  with 0 have "τs!0 = c!0" ..
  moreover 
  have "wtl (take 1 ins) c 0 s₀ ≠ ⊤" using wtl by (rule wtl_take)
  with 0 False 
  have "s₀ ⊑_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₀ ≠ ⊤" and s₀: "s₀ ∈ 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₀ 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₀ ≠ ⊤" 
  assumes s₀: "s₀ ∈ A" and ins: "0 < size ins"
  shows "∃τs ∈ nlists (size ins) A. wt_step r ⊤ step τs ∧ s₀ ⊑_r τs!0"
(*<*)
proof -
  have "τs ∈ nlists (size ins) A" using wtl s₀ 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₀ and pc show "stable r step τs pc" by (rule wtl_stable)
  qed
  moreover from wtl ins have "s₀ ⊑_r τs!0" using s₀  by (rule phi0)
  ultimately show ?thesis by fast
qed
(*>*)

end