(*  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 = τ ⊔ τ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_elem 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 [⊑] merges f ps xs"
  apply (induct ps)
  apply auto[1]
  apply simp
  apply clarify
  apply (rule order_trans [OF _ list_update_incr])
         apply force
        apply simp+     
  done       

(*>*)

lemma (in Semilat) merges_incr:
 "[ xs ∈ nlists n A; ∀(p,x)∈set ps. p<size xs ∧ x ∈ A ]
  ==> xs [⊑] 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 ∧ x∈A) ⟶
     (merges f ps xs = xs) = (∀(p,x)∈set ps. x ⊑ xs!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 ⊔ xs!p] [⊑] xs")
     apply (fastforce dest!: le_listD)  ―‹apply (force dest!: le_listD simp add: nth_list_update) ›
    apply (smt (verit, ccfv_threshold) case_prodD case_prodI2 closed_f merges_incr
      nlistsE_length nlistsE_nth_in nlists_update_in_list)
   apply clarify
  using le_iff_plus_unchanged apply fastforce
  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 ⊔ ss!q ≠ ss!q} ∪ w)"
(*<*)
  by (induct qs; fastforce simp add: nth_list_update)
(*>*)

lemma (in Semilat) stable_pres_lemma:
shows "[pres_type step n A; bounded step n;
     ss ∈ nlists n A; p ∈ w; ∀q∈w. q < n;
     ∀q. q < n ⟶ q ∉ w ⟶ stable r step ss q; q < n;
     ∀s'. (q,s') ∈ set (step p (ss!p)) ⟶ s' ⊔ ss!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 (meson nlistsE_nth_in pres_typeD)
  apply simp
  apply clarify
  apply (subst nth_merges)
     apply simp
     apply (blast dest: boundedD)
    apply assumption
   apply clarify
  apply (metis boundedD nlistsE_nth_in pres_typeD)
  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 (metis boundedD nlistsE_nth_in pres_typeD)
  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 (smt (verit, ccfv_SIG) Semilat_axioms bounded_def nlistsE_length nlistsE_set
      nth_in old.prod.case pres_type_def ub1')

  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")
    apply (metis (lifting) boundedD nlistsE_length nlistsE_set nth_in
      nth_merges)
   apply (blast dest:merges_preserves_type)
  by (smt (verit, best) boundedD case_prodI2 nlistsE_nth_in pres_typeD)
    (*>*)


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
  by (meson nlistsE_nth_in pres_typeD trans_r)
(*>*)



(** iter **)
lemma termination_lemma: assumes "Semilat A r f"
shows "[ ss ∈ nlists n A; ∀(q,t)∈set qs. q<n ∧ t∈A; p∈w ] ==>
      ss [⊏_r] merges f qs ss ∨
  merges f qs ss = ss ∧ {q. ∃t. (q,t)∈set qs ∧ t ⊔ ss!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+
    apply fastforce
     apply force
     apply (subgoal_tac "∀q t. ¬((q, t) ∈ set qs ∧ t ⊔ ss ! q ≠ ss ! q)")
     apply (blast intro!: psubsetI elim: equalityE)
    by fastforce
qed
(*>*)

end