Theory LBVComplete

(*  Title:      HOL/MicroJava/BV/LBVComplete.thy
    ID:         $Id: LBVComplete.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Gerwin Klein
    Copyright   2000 Technische Universitaet Muenchen
*)

header {* \isaheader{Completeness of the LBV} *}

theory LBVComplete = LBVSpec + Typing_Framework:

constdefs
  is_target :: "['s step_type, 's list, nat] => bool" 
  "is_target step τs pc' ≡
     ∃pc s'. pc' ≠ pc+1 ∧ pc < size τs ∧ (pc',s') ∈ set (step pc (τs!pc))"

  make_cert :: "['s step_type, 's list, 's] => 's certificate"
  "make_cert step τs B ≡ 
     map (λpc. if is_target step τs pc then τs!pc else B) [0..size τs(] @ [B]"

text {*
  For the code generator:
*}
constdefs
  list_ex :: "('a => bool) => 'a list => bool"
  "list_ex P xs ≡ ∃x ∈ set xs. P x"

lemma [code]: "list_ex P [] = False" by (simp add: list_ex_def)
lemma [code]: "list_ex P (x#xs) = (P x ∨ list_ex P xs)" by (simp add: list_ex_def)

lemma [code]:
  "is_target step τs pc' =
  list_ex (λpc. pc' ≠ pc+1 ∧ pc' mem (map fst (step pc (τs!pc)))) [0..size τs(]"
(*<*)
  apply (simp add: list_ex_def is_target_def set_mem_eq)
  apply force
  done
(*>*)

locale (open) 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 ≠ \<top>"
  assumes bounded: "bounded step (size τs)"

  assumes B_neq_T: "⊥ ≠ \<top>" 


lemma (in lbvc) cert: "cert_ok c (size τs) \<top> ⊥ 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 ≠ \<top>" 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 \<top>"
(*<*) by (insert top) simp (*>*)
  
lemma (in lbv) merge_mono:
  assumes less:  "set ss2 {\<sqsubseteq>r} set ss1"
  assumes x:     "x ∈ A"
  assumes ss1:   "snd`set ss1 ⊆ A"
  assumes ss2:   "snd`set ss2 ⊆ A"
  shows "merge c pc ss2 x \<sqsubseteq>r merge c pc ss1 x" (is "?s2 \<sqsubseteq>r ?s1")
(*<*)
proof-
  have "?s1 = \<top> ==> ?thesis" by simp
  moreover {
    assume merge: "?s1 ≠ T" 
    from x ss1 have "?s1 =
      (if ∀(pc',s')∈set ss1. pc' ≠ pc + 1 --> s' \<sqsubseteq>r c!pc'
      then (map snd [(p', t')∈ss1 . p'=pc+1]) \<Squnion>f x
      else \<top>)" by (rule merge_def)  
    with merge obtain
      app: "∀(pc',s')∈set ss1. pc' ≠ pc+1 --> s' \<sqsubseteq>r c!pc'" 
           (is "?app ss1") and
      sum: "(map snd [(p',t')∈ss1 . p' = pc+1] \<Squnion>f x) = ?s1" 
           (is "?map ss1 \<Squnion>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)
      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 \<sqsubseteq>r ?sum ss1" by clarify (rule pp_ub1)
      with sum have "∀x ∈ set (?map ss1). x \<sqsubseteq>r ?s1" by simp
      with less have "∀x ∈ set (?map ss2). x \<sqsubseteq>r ?s1"
        by (fastsimp dest!: mapD lesub_step_typeD intro: trans_r)
      moreover from map1 x have "x \<sqsubseteq>r (?sum ss1)" by (rule pp_ub2)
      with sum have "x \<sqsubseteq>r ?s1" by simp
      moreover from ss2 have "set (?map ss2) ⊆ A" by auto
      ultimately  have "?sum ss2 \<sqsubseteq>r ?s1" using x by - (rule pp_lub)
    }
    moreover from x ss2 have "?s2 =
      (if ∀(pc', s')∈set ss2. pc' ≠ pc + 1 --> s' \<sqsubseteq>r c!pc'
      then map snd [(p', t')∈ss2 . p' = pc + 1] \<Squnion>f x
      else \<top>)" by (rule merge_def)
    ultimately have ?thesis by simp
  }
  ultimately show ?thesis by (cases "?s1 = \<top>") auto
qed
(*>*)

lemma (in lbvc) wti_mono:
  assumes less: "s2 \<sqsubseteq>r s1"
  assumes pc: "pc < size τs" and s1: "s1 ∈ A" and s2: "s2 ∈ A"
  shows "wti c pc s2 \<sqsubseteq>r wti c pc s1" (is "?s2' \<sqsubseteq>r ?s1'")
(*<*)
proof -
  from mono s2 have "set (step pc s2) {\<sqsubseteq>r} set (step pc s1)" by - (rule monoD)
  moreover from pc cert 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 \<sqsubseteq>r s1"
  assumes pc: "pc < size τs" and s1: "s1 ∈ A" and s2: "s2 ∈ A"
  shows "wtc c pc s2 \<sqsubseteq>r wtc c pc s1" (is "?s2' \<sqsubseteq>r ?s1'")
(*<*)
proof (cases "c!pc = ⊥")
  case True 
  moreover have "wti c pc s2 \<sqsubseteq>r wti c pc s1" by (rule wti_mono)
  ultimately show ?thesis by (simp add: wtc)
next
  case False
  have "?s1' = \<top> ==> ?thesis" by simp
  moreover {
    assume "?s1' ≠ \<top>" 
    with False have c: "s1 \<sqsubseteq>r c!pc" by (simp add: wtc split: split_if_asm)
    with less have "s2 \<sqsubseteq>r c!pc" ..
    with False c have ?thesis by (simp add: wtc)
  }
  ultimately show ?thesis by (cases "?s1' = \<top>") auto
qed
(*>*)

lemma (in lbv) top_le_conv [simp]: "\<top> \<sqsubseteq>r x = (x = \<top>)"
(*<*) by (insert semilat) (simp add: top top_le_conv)  (*>*)

lemma (in lbv) neq_top [simp, elim]: "[| x \<sqsubseteq>r y; y ≠ \<top> |] ==> x ≠ \<top>"
(*<*) 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) ≠ \<top>"
(*<*)
proof -
  let ?step = "step pc (τs!pc)"
  from stable 
  have less: "∀(q,s')∈set ?step. s' \<sqsubseteq>r τs!q" by (simp add: stable_def)
  
  from cert 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' \<sqsubseteq>r c!pc'
    then map snd [(p',t')∈?step.p'=pc+1] \<Squnion>f c!Suc pc
    else \<top>)" by (rule merge_def)
  moreover {
    fix pc' s' assume s': "(pc',s') ∈ set ?step" and suc_pc: "pc' ≠ pc+1"
    with less have "s' \<sqsubseteq>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' \<sqsubseteq>r c!pc'" .
  } hence "∀(pc',s')∈set ?step. pc'≠pc+1 --> s' \<sqsubseteq>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] \<Squnion>f c!Suc pc ≠ \<top>" (is "?map \<Squnion>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!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' \<sqsubseteq>r τs!Suc pc" by auto
    moreover from pc' have "c!Suc pc \<sqsubseteq>r τs!Suc pc" 
      by (cases "c!Suc pc = ⊥") (auto dest: cert_approx)
    ultimately have "?map \<Squnion>f c!Suc pc \<sqsubseteq>r τs!Suc pc" by (rule pp_lub)
    moreover from pc' τs have "τs!Suc pc ≠ \<top>" by simp
    ultimately show ?thesis by auto
  qed
  ultimately have "merge c pc ?step (c!Suc pc) ≠ \<top>" 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) \<sqsubseteq>r τs!Suc pc" (is "?wti \<sqsubseteq>r _")
(*<*)
proof -
  let ?step = "step pc (τs!pc)"

  from stable
  have less: "∀(q,s')∈set ?step. s' \<sqsubseteq>r τs!q" by (simp add: stable_def)
   
  from suc_pc have pc: "pc < size τs" by simp
  with cert 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 ≠ \<top>" by (rule stable_wti)
  hence "merge c pc ?step (c!Suc pc) ≠ \<top>" by (simp add: wti)
  ultimately
  have "merge c pc ?step (c!Suc pc) =
    map snd [(p',t')∈?step.p'=pc+1] \<Squnion>f c!Suc pc" by (rule merge_not_top_s) 
  hence "?wti = …" (is "_ = (?map \<Squnion>f _)" is "_ = ?sum") by (simp add: wti)
  also {
    from suc_pc τs have "τ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' \<sqsubseteq>r τs!Suc pc" by auto
    moreover from suc_pc have "c!Suc pc \<sqsubseteq>r τs!Suc pc"
      by (cases "c!Suc pc = ⊥") (auto dest: cert_approx)
    ultimately have "?sum \<sqsubseteq>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) ≠ \<top>"
(*<*)
proof -
  have wti: "wti c pc (τs!pc) ≠ \<top>" 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 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) \<sqsubseteq>r τs!Suc pc" (is "?wtc \<sqsubseteq>r _")
(*<*)
proof (cases "c!pc = ⊥")
  case True
  moreover have "wti c pc (τs!pc) \<sqsubseteq>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
  hence "?wtc ≠ \<top>" 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 = τs!pc" .. 
  finally have "?wtc = wti c pc (τs!pc)" .
  also have "wti c pc (τs!pc) \<sqsubseteq>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 \<top> step τs"
  shows "!!pc s. pc+size ls = size τs ==> s \<sqsubseteq>r τs!pc ==> s ∈ A ==> s≠\<top> ==>
                wtl ls c pc s ≠ \<top>"
  (is "!!pc s. _ ==> _ ==> _ ==> _ ==> ?wtl ls pc s ≠ _")
(*<*)
proof (induct ls)
  fix pc s assume "s≠\<top>" thus "?wtl [] pc s ≠ \<top>" by simp
next
  fix pc s i ls
  assume "!!pc s. pc+size ls=size τs ==> s \<sqsubseteq>r τs!pc ==> s ∈ A ==> s≠\<top> ==> 
                  ?wtl ls pc s ≠ \<top>"
  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 \<sqsubseteq>r τs!Suc pc ==> s ∈ A ==> s ≠ \<top> ==> ?wtl ls (Suc pc) s ≠ \<top>" .

  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 assume s_τs: "s \<sqsubseteq>r τs!pc"
  ultimately have wt_τs: "wtc c pc (τs!pc) ≠ \<top>" by - (rule stable_wtc)

  from τs pc have τs_pc: "τs!pc ∈ A" by simp
  moreover assume s: "s ∈ A"
  ultimately 
  have wt_s_τs: "wtc c pc s \<sqsubseteq>r wtc c pc (τs!pc)" using s_τs by - (rule wtc_mono)
  with wt_τs have wt_s: "wtc c pc s ≠ \<top>" by simp
  moreover assume s: "s ≠ \<top>" 
  ultimately have "ls = [] ==> ?wtl (i#ls) pc s ≠ \<top>" 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 "wtc c pc (τs!pc) \<sqsubseteq>r τs!Suc pc" by (rule wtc_less)
    with wt_s_τs have "wtc c pc s \<sqsubseteq>r τs!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)
    with pres have "wtc c pc s ∈ A" by (rule wtc_pres)
    ultimately have "?wtl ls (Suc pc) (wtc c pc s) ≠ \<top>" using IH wt_s by blast
    with s wt_s have "?wtl (i#ls) pc s ≠ \<top>" by simp 
  }
  ultimately show "?wtl (i#ls) pc s ≠ \<top>" by (cases ls) blast+
qed
(*>*)

theorem (in lbvc) wtl_complete:
  assumes "wt_step r \<top> step τs"
  assumes "s \<sqsubseteq>r τs!0" and "s ∈ A" and "s ≠ \<top>" and "size ins = size τs"
  shows "wtl ins c 0 s ≠ \<top>"
(*<*)
proof -  
  have "0+size ins = size τs" by simp
  thus ?thesis by - (rule wt_step_wtl_lemma)
qed
(*>*)

end