Theory Kildall_1

(*  Title:      HOL/MicroJava/BV/Kildall.thy
    Author:     Tobias Nipkow, Gerwin Klein
    Copyright   2000 TUM

Kildall's algorithm.
*)

section ‹Kildall's Algorithm \label{sec:Kildall}›

theory Kildall_1
imports SemilatAlg
begin

primrec merges :: "'s binop  (nat × 's) list  's list  's list"
where
  "merges f []      τs = τs"
| "merges f (p'#ps) τs = (let (p,τ) = p' in merges f ps (τs[p := τ ⊔⇘fτs!p]))"


lemmas [simp] = Let_def Semilat.le_iff_plus_unchanged [OF Semilat.intro, symmetric]


lemma (in Semilat) nth_merges:
 "ss. p < length ss; ss  nlists n A; (p,t)set ps. p<n  tA  
  (merges f ps ss)!p = map snd [(p',t')  ps. p'=p] ⨆⇘fss!p"
  (is "ss. _; _; ?steptype ps  ?P ss ps")
(*<*)
proof (induct ps)
  show "ss. ?P ss []" by simp

  fix ss p' ps'
  assume ss: "ss  nlists n A"
  assume l:  "p < length ss"
  assume "?steptype (p'#ps')"
  then obtain a b where
    p': "p'=(a,b)" and ab: "a<n" "bA" and ps': "?steptype ps'"
    by (cases p') auto
  assume "ss. p< length ss  ss  nlists n A  ?steptype ps'  ?P ss ps'"
  hence IH: "ss. ss  nlists n A  p < length ss  ?P ss ps'" using ps' by iprover

  from ss ab
  have "ss[a := b ⊔⇘fss!a]  nlists n A" by (simp add: closedD)
  moreover
  with l have "p < length (ss[a := b ⊔⇘fss!a])" by simp
  ultimately
  have "?P (ss[a := b ⊔⇘fss!a]) ps'" by (rule IH)
  with p' l
  show "?P ss (p'#ps')" by simp
qed
(*>*)


(** merges **)

lemma length_merges [simp]:
  "ss. size(merges f ps ss) = size ss"
(*<*) by (induct ps, auto) (*>*)

lemma (in Semilat) merges_preserves_type_lemma:
shows "xs. xs  nlists n A  ((p,x)  set ps. p<n  xA)
          merges f ps xs  nlists n A"
(*<*)
apply (insert closedI)
apply (unfold closed_def)
apply (induct ps)
 apply simp
apply clarsimp
done
(*>*)

lemma (in Semilat) merges_preserves_type [simp]:
 " xs  nlists n A; (p,x)  set ps. p<n  xA 
   merges f ps xs  nlists n A"
by (simp add: merges_preserves_type_lemma)

lemma (in Semilat) list_update_le_listI [rule_format]:
  "set xs  A  set ys  A  xs [⊑⇘r⇙] ys  p < size xs   
   x ⊑⇘rys!p  xA  xs[p := x ⊔⇘fxs!p] [⊑⇘r⇙] ys"
(*<*)
  apply (insert semilat)
  apply (simp only: Listn.le_def lesub_def semilat_def)
  apply (simp add: list_all2_conv_all_nth nth_list_update)
  done
(*>*)

lemma (in Semilat) merges_pres_le_ub:
  assumes "set ts  A"  "set ss  A"
    "(p,t)set ps. t ⊑⇘rts!p  t  A  p < size ts"  "ss [⊑⇘r⇙] ts"
  shows "merges f ps ss [⊑⇘r⇙] ts"
(*<*)
proof -
  { fix t ts ps
    have
    "qs. set ts  A; (p,t)set ps. t ⊑⇘rts!p  t  A  p< size ts  
    set qs  set ps   
    (ss. set ss  A  ss [⊑⇘r⇙] ts  merges f qs ss [⊑⇘r⇙] ts)"
    apply (induct_tac qs)
     apply simp
    apply (simp (no_asm_simp))
    apply clarify
    apply simp
    apply (erule allE, erule impE, erule_tac [2] mp)
     apply (drule bspec, assumption)
     apply (simp add: closedD)
    apply (drule bspec, assumption)
    apply (simp add: list_update_le_listI)
    done 
  } note this [dest]  
  from assms show ?thesis by blast
qed
(*>*)




end