Theory Jinja.Kildall_2

(*  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_2
imports SemilatAlg Kildall_1
begin



primrec propa :: "'s binop  (nat × 's) list  's list  nat set  's list * nat set"
where
  "propa f []      τs w = (τs,w)"
| "propa f (q'#qs) τs w = (let (q,τ) = q';
                             u = τ ⊔⇘fτs!q;
                             w' = (if u = τs!q then w else insert q w)
                         in propa f qs (τs[q := u]) w')"

definition iter :: "'s binop  's step_type 
          's list  nat set  's list × nat set"
where
  "iter f step τs w =
   while (λ(τs,w). w  {})
         (λ(τs,w). let p = SOME p. p  w
                   in propa f (step p (τs!p)) τs (w-{p}))
         (τs,w)"

definition unstables :: "'s ord  's step_type  's list  nat set"
where
  "unstables r step τs = {p. p < size τs  ¬stable r step τs p}"

definition kildall :: "'s ord  's binop  's step_type  's list  's list"
where
  "kildall r f step τs = fst(iter f step τs (unstables r step τs))"


(** propa **)
lemma (in Semilat) merges_incr_lemma:
 "xs. xs  nlists n A  ((p,x)set ps. p<size xs  x  A)  xs [⊑⇘r⇙] merges f ps xs"
  apply (induct ps)
   apply simp
   apply(insert orderI)
   apply (fastforce intro:le_list_refl')  
  apply simp
  apply clarify
  apply (rule order_trans)
       defer
       apply (erule list_update_incr)
        apply simp+     
  done       

(*>*)

lemma (in Semilat) merges_incr:
 " xs  nlists n A; (p,x)set ps. p<size xs  x  A  
   xs [⊑⇘r⇙] merges f ps xs"
  by (simp add: merges_incr_lemma)


lemma (in Semilat) merges_same_conv [rule_format]:
 "(xs. xs  nlists n A  ((p,x)set ps. p<size xs  xA)  
     (merges f ps xs = xs) = ((p,x)set ps. x ⊑⇘rxs!p))"
(*<*)
  apply (induct_tac ps)
   apply simp
  apply clarsimp
  apply (rename_tac p x ps xs)
  apply (rule iffI)
   apply (rule context_conjI)
    apply (subgoal_tac "xs[p := x ⊔⇘fxs!p] [⊑⇘r⇙] xs")
     apply (fastforce dest!: le_listD)  ―‹apply (force dest!: le_listD simp add: nth_list_update) ›
    apply (erule subst, rule merges_incr)
       apply (blast intro!: nlistsE_set intro: closedD nlistsE_length [THEN nth_in])
      apply clarify
      apply (rule conjI)
       apply simp
       apply (blast dest: boundedD)
      apply blast
   apply clarify
   apply (erule allE)
   apply (erule impE)
    apply assumption
   apply (drule bspec)
    apply assumption
   apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
   apply blast
  apply clarify 
  apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
  done
(*>*)

lemma decomp_propa:
  "ss w. ((q,t)set qs. q < size ss)  
   propa f qs ss w = 
   (merges f qs ss, {q. t.(q,t)set qs  t ⊔⇘fss!q  ss!q}  w)"
(*<*)
  apply (induct qs)
   apply simp   
  apply (simp (no_asm))
  apply clarify  
  apply simp
  apply (rule conjI) 
   apply blast
  apply (simp add: nth_list_update)
  apply blast
  done 
(*>*)

lemma (in Semilat) stable_pres_lemma:
shows "pres_type step n A; bounded step n; 
     ss  nlists n A; p  w; qw. q < n; 
     q. q < n  q  w  stable r step ss q; q < n; 
     s'. (q,s')  set (step p (ss!p))  s' ⊔⇘fss!q = ss!q; 
     q  w  q = p  
   stable r step (merges f (step p (ss!p)) ss) q"
(*<*)
  apply (unfold stable_def)
  apply (subgoal_tac "s'. (q,s')  set (step p (ss!p))  s' : A")
   prefer 2
   apply clarify
   apply (erule pres_typeD)
    prefer 3 apply assumption
    apply (rule nlistsE_nth_in)
     apply assumption
    apply simp
   apply simp
  apply simp
  apply clarify
  apply (subst nth_merges)
       apply simp
       apply (blast dest: boundedD)
      apply assumption
     apply clarify
     apply (rule conjI)
      apply (blast dest: boundedD)
     apply (erule pres_typeD)
       prefer 3 apply assumption
      apply simp
     apply simp
apply(subgoal_tac "q < length ss")
prefer 2 apply simp
  apply (frule nth_merges [of q _ _ "step p (ss!p)"]) (* fixme: why does method subst not work?? *)
apply assumption
  apply clarify
  apply (rule conjI)
   apply (blast dest: boundedD)
  apply (erule pres_typeD)
     prefer 3 apply assumption
    apply simp
   apply simp
  apply (drule_tac P = "λx. (a, b)  set (step q x)" in subst)
   apply assumption

 apply (simp add: plusplus_empty)
 apply (cases "q  w")
  apply simp
  apply (rule ub1')
     apply (rule Semilat.intro)
     apply (rule semilat)
    apply clarify
    apply (rule pres_typeD)
       apply assumption
      prefer 3 apply assumption
     apply (blast intro: nlistsE_nth_in dest: boundedD)
    apply (blast intro: pres_typeD dest: boundedD)
   apply (blast intro: nlistsE_nth_in dest: boundedD)
  apply assumption

 apply simp
  apply (erule allE, erule impE, assumption, erule impE, assumption) 
  apply (rule order_trans)    
  apply fastforce
       defer     
       apply (rule pp_ub2)
        apply simp        
        apply clarify
        apply simp
        apply (rule pres_typeD)
           apply assumption
          prefer 3 
          apply assumption
         apply (blast intro: nlistsE_nth_in)
        apply (blast)
       apply (blast intro: nlistsE_nth_in dest: boundedD)
     prefer 4
  apply fastforce     
    apply (blast intro: nlistsE_nth_in dest: pres_typeD)
   apply (blast intro: nlistsE_nth_in dest: boundedD)
  apply(subgoal_tac "(q,t)  set (step p (ss!p)). q < n  t  A")

   apply (subgoal_tac "merges f (step p (ss!p)) ss  nlists n A")
  defer
    apply (blast dest:merges_preserves_type)
   defer
   apply (subgoal_tac "a < n")
  defer
    apply (blast intro: nlistsE_nth_in  boundedD )
   defer
  apply (subgoal_tac "merges f (step p (ss ! p)) ss ! a = 
      map snd (filter (λ(p', t'). p' = a) (step p (ss ! p))) ⨆⇘fss ! a")
    apply (fastforce  dest: nlistsE_nth_in ) (* slow *)
  apply (subgoal_tac "a < length ss")
    apply (fastforce dest:nth_merges)
   apply simp
  apply (intro strip)
  apply auto
  defer
   apply (auto intro:boundedD)
  apply (fastforce intro: nlistsE_nth_in dest:pres_typeD)
  done
(*>*)


lemma (in Semilat) merges_bounded_lemma:
 " mono r step n A; bounded step n; pres_type step n A; 
    (p',s')  set (step p (ss!p)). s'  A; ss  nlists n A; ts  nlists n A; p < n; 
    ss [⊑⇩r] ts; p. p < n  stable r step ts p  
   merges f (step p (ss!p)) ss [⊑⇩r] ts" 
(*<*)
  apply (unfold stable_def)
  apply (rule merges_pres_le_ub)
     apply simp
    apply simp
   prefer 2 apply assumption

  apply clarsimp
  apply (drule boundedD, assumption+)
  apply (erule allE, erule impE, assumption)
  apply (drule bspec, assumption)
  apply simp

  apply (drule monoD [of _ _ _ _ p "ss!p"  "ts!p"])
     apply assumption
    apply simp
   apply (simp add: le_listD)
  
  apply (drule lesub_step_typeD, assumption) 
  apply clarify
  apply (drule bspec, assumption)
  apply simp

  apply (rule order_trans)
       apply fastforce
      apply simp
     apply simp
    apply simp
   apply (auto intro:boundedD)

  apply (blast intro: nlistsE_nth_in dest:pres_typeD)
  done
(*>*)



(** iter **)
lemma termination_lemma: assumes "Semilat A r f"
shows " ss  nlists n A; (q,t)set qs. q<n  tA; pw   
      ss [⊏⇩r] merges f qs ss  
  merges f qs ss = ss  {q. t. (q,t)set qs  t ⊔⇘fss!q  ss!q}  (w-{p})  w"
(*<*) (is "PROP ?P")
proof -
  interpret Semilat A r f by fact
  show "PROP ?P"
  apply(insert semilat)
    apply (unfold lesssub_def)
    apply (simp (no_asm_simp) add: merges_incr)
    apply (rule impI)
    apply (rule merges_same_conv [THEN iffD1, elim_format]) 
    apply assumption+
      defer
      apply (rule sym, assumption)
     defer apply simp
     apply (subgoal_tac "q t. ¬((q, t)  set qs  t ⊔⇘fss ! q  ss ! q)")
     apply (blast intro!: psubsetI elim: equalityE)
     apply clarsimp
     apply (drule bspec, assumption) 
     apply (drule bspec, assumption)
     apply clarsimp
    done 
qed
(*>*)

end