Theory Jinja.LBVComplete

(*  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 ss2 {⊑⇘r⇙} set ss1"
  assumes x:     "x  A"
  assumes ss1:   "snd`set ss1  A"
  assumes ss2:   "snd`set ss2  A"
  assumes boun:  "x(fst`set ss1). x < size τs"
  assumes cert:  "cert_ok c (size τs) T B 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]) ⨆⇘fx
      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] ⨆⇘fx) = ?s1" 
           (is "?map ss1 ⨆⇘fx = _" is "?sum ss1 = _")
      by (simp split: if_split_asm)

    have "?app ss2"  
    proof(intro strip, clarsimp )
      fix a b
      assume a_b: "(a, b)  set ss2" and neq: "a  Suc pc"       
      from less a_b obtain y where y: "(a, y)  set ss1 " and b_lt_y: "b ⊑⇩r y" by (blast dest:lesub_step_typeD)
      with app have "a  pc + 1  y ⊑⇘rc!a" by auto
      with neq have "y ⊑⇘rc!a" by auto
      moreover from y ss1 have "y  A" by auto
      moreover from a_b ss2 have "b  A" by auto
      moreover from y boun cert have "c!a  A" by (auto dest:cert_okD1)
      ultimately show "b ⊑⇘rc!a" using b_lt_y by (auto intro:trans_r)        
    qed    

    moreover {
      from ss1 have map1: "set (?map ss1)  A" by auto
      with x and semilat Semilat_axioms 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 ⊑⇩r ?sum ss1" by clarify (rule pp_ub1)
      with sum have "x  set (?map ss1). x ⊑⇩r ?s1" by simp
      then have "x  set (?map ss2). x ⊑⇩r ?s1"
      proof(intro strip, clarsimp)
        fix b
        assume xa: "xa. (Suc pc, xa) set ss1  xa ⊑⇘rmerge c pc ss1 x"
           and b: "(Suc pc, b)  set ss2"
        from less b obtain y where y: "(Suc pc, y)  set ss1 " and b_lt_y: "b ⊑⇩r y" by (blast dest:lesub_step_typeD)
        from y xa have "y ⊑⇘rmerge c pc ss1 x" by auto
        moreover from y ss1 have "y  A" by auto
        moreover from b ss2 have "b  A" by auto
        moreover from ss1 x have "merge c pc ss1 x  A" by (auto intro:merge_pres)
        ultimately show "b ⊑⇘rmerge c pc ss1 x" using b_lt_y by (auto intro:trans_r) 
      qed
      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] ⨆⇘fx
      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 < size τs" and s1: "s1  A" and s2: "s2  A"
  shows "wti c pc s2 ⊑⇩r wti c pc s1" (is "?s2' ⊑⇩r ?s1'")
(*<*)
proof -
  from bounded pc have "(q,τ)  set(step pc s1). q < size τs" by (simp add:bounded_def)
  then have u: "q  fst ` set (step pc s1). q < size τs" by auto
  from mono pc s2 less have "set (step pc s2) {⊑⇘r⇙} set (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 using cert u by (simp add: wti merge_mono)
qed 
(*>*)

lemma (in lbvc) wtc_mono:
  assumes less: "s2 ⊑⇩r s1"
  assumes pc: "pc < size τs" and s1: "s1  A" and 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
  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 s2  A"  using pres wtc_pres pc s2 by auto
  have "?s1' =   ?thesis" by simp
  moreover {
    assume "?s1'  " 
    with False have c: "s1 ⊑⇩r c!pc" by (simp add: wtc split: if_split_asm)
    from semilat have "order r A" by auto
    from this less c s2 s1 c_pc_inA have "s2 ⊑⇩r c!pc" by (rule order_trans)
    with False c have ?thesis using inA by (simp add: wtc)
  }
  ultimately show ?thesis by (cases "?s1' = ") 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] ⨆⇘fc!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] ⨆⇘fc!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 ⨆⇘fc!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] ⨆⇘fc!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