# Theory Kildall

Up to index of Isabelle/HOL/MicroJava

theory Kildall
imports SemilatAlg While_Combinator
begin

    (*  Title:      HOL/MicroJava/BV/Kildall.thy
        ID:         $Id: Kildall.thy,v 1.21 2005/09/20 21:36:57 wenzelm Exp $
        Author:     Tobias Nipkow, Gerwin Klein
        Copyright   2000 TUM

    Kildall's algorithm
    *)

    header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *}

    theory Kildall imports SemilatAlg While_Combinator begin

    consts
     iter :: "'s binop => 's step_type =>
              's list => nat set => 's list × nat set"
     propa :: "'s binop => (nat × 's) list => 's list => nat set => 's list * nat set"

    primrec
    "propa f []      ss w = (ss,w)"
    "propa f (q'#qs) ss w = (let (q,t) = q';
                                 u = t +_f ss!q;
                                 w' = (if u = ss!q then w else insert q w)
                             in propa f qs (ss[q := u]) w')"

    defs iter_def:
    "iter f step ss w ==
     while (%(ss,w). w ≠ {})
           (%(ss,w). let p = SOME p. p ∈ w
                     in propa f (step p (ss!p)) ss (w-{p}))
           (ss,w)"

    constdefs
     unstables :: "'s ord => 's step_type => 's list => nat set"
    "unstables r step ss == {p. p < size ss ∧ ¬stable r step ss p}"

     kildall :: "'s ord => 's binop => 's step_type => 's list => 's list"
    "kildall r f step ss == fst(iter f step ss (unstables r step ss))"

    consts merges :: "'s binop => (nat × 's) list => 's list => 's list"
    primrec
    "merges f []      ss = ss"
    "merges f (p'#ps) ss = (let (p,s) = p' in merges f ps (ss[p := s +_f ss!p]))"

    lemmas [simp] = Let_def semilat.le_iff_plus_unchanged [symmetric]

    lemma (in semilat) nth_merges:
     "!!ss. [|p < length ss; ss ∈ list n A; ∀(p,t)∈set ps. p<n ∧ t∈A |] ==>
      (merges f ps ss)!p = map snd [(p',t') ∈ ps. p'=p] ++_f ss!p"
      (is "!!ss. [|_; _; ?steptype ps|] ==> ?P ss ps")
    proof (induct ps)
      show "!!ss. ?P ss []" by simp

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

      from ss ab
      have "ss[a := b +_f ss!a] ∈ list n A" by (simp add: closedD)
      moreover
      from calculation
      have "p < length (ss[a := b +_f ss!a])" by simp
      ultimately
      have "?P (ss[a := b +_f ss!a]) ps'" by (rule IH)
      with p' l
      show "?P ss (p'#ps')" by simp
    qed

    (** merges **)

    lemma length_merges [rule_format, simp]:
      "∀ss. size(merges f ps ss) = size ss"
      by (induct_tac ps, auto)

    lemma (in semilat) merges_preserves_type_lemma:
    shows "∀xs. xs ∈ list n A --> (∀(p,x) ∈ set ps. p<n ∧ x∈A)
              --> merges f ps xs ∈ list n A"
    apply (insert closedI)
    apply (unfold closed_def)
    apply (induct_tac ps)
     apply simp
    apply clarsimp
    done

    lemma (in semilat) merges_preserves_type [simp]:
     "[| xs ∈ list n A; ∀(p,x) ∈ set ps. p<n ∧ x∈A |]
      ==> merges f ps xs ∈ list n A"
    by (simp add: merges_preserves_type_lemma)

    lemma (in semilat) merges_incr_lemma:
     "∀xs. xs ∈ list n A --> (∀(p,x)∈set ps. p<size xs ∧ x ∈ A) --> xs <=[r] merges f ps xs"
    apply (induct_tac ps)
     apply simp
    apply simp
    apply clarify
    apply (rule order_trans)
      apply simp
     apply (erule list_update_incr)
      apply simp
     apply simp
    apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
    done

    lemma (in semilat) merges_incr:
     "[| xs ∈ list 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 ∈ list n A --> (∀(p,x)∈set ps. p<size xs ∧ x∈A) -->
         (merges f ps xs = xs) = (∀(p,x)∈set ps. x <=_r 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 +_f xs!p] <=[r] xs")
         apply (drule_tac p = p in le_listD)
          apply simp
         apply simp
        apply (erule subst, rule merges_incr)
           apply (blast intro!: listE_set intro: closedD listE_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 (in semilat) list_update_le_listI [rule_format]:
      "set xs <= A --> set ys <= A --> xs <=[r] ys --> p < size xs -->
       x <=_r ys!p --> x∈A --> xs[p := x +_f xs!p] <=[r] ys"
      apply(insert semilat)
      apply (unfold 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:
    shows "[| set ts <= A; set ss <= A;
             ∀(p,t)∈set ps. t <=_r ts!p ∧ t ∈ A ∧ p < size ts; ss <=[r] ts |]
      ==> merges f ps ss <=[r] ts"
    proof -
      { fix t ts ps
        have
        "!!qs. [|set ts <= A; ∀(p,t)∈set ps. t <=_r ts!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 (rotate_tac -2)
        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]

      case rule_context
      thus ?thesis by blast
    qed

    (** propa **)

    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 +_f ss!q ≠ ss!q} Un 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

    (** iter **)

    lemma (in semilat) stable_pres_lemma:
    shows "[|pres_type step n A; bounded step n;
         ss ∈ list 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' +_f 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 clarify
       apply (erule pres_typeD)
        prefer 3 apply assumption
        apply (rule listE_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 assumption
        apply clarify
        apply (rule pres_typeD)
           apply assumption
          prefer 3 apply assumption
         apply (blast intro: listE_nth_in dest: boundedD)
        apply (blast intro: pres_typeD dest: boundedD)
       apply (blast intro: listE_nth_in dest: boundedD)
      apply assumption

     apply simp
     apply (erule allE, erule impE, assumption, erule impE, assumption)
     apply (rule order_trans)
       apply simp
      defer
     apply (rule pp_ub2)(*
        apply assumption*)
       apply simp
       apply clarify
       apply simp
       apply (rule pres_typeD)
          apply assumption
         prefer 3 apply assumption
        apply (blast intro: listE_nth_in dest: boundedD)
       apply (blast intro: pres_typeD dest: boundedD)
      apply (blast intro: listE_nth_in dest: boundedD)
     apply blast
     done

    lemma (in semilat) merges_bounded_lemma:
     "[| mono r step n A; bounded step n;
        ∀(p',s') ∈ set (step p (ss!p)). s' ∈ A; ss ∈ list n A; ts ∈ list 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 (blast intro: order_trans)
      done

    lemma termination_lemma: includes semilat
    shows "[| ss ∈ list 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 +_f ss!q ≠ ss!q} Un (w-{p}) < w"
    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 +_f ss ! q ≠ ss ! q)")
       apply (blast intro!: psubsetI elim: equalityE)
       apply clarsimp
       apply (drule bspec, assumption)
       apply (drule bspec, assumption)
       apply clarsimp
      done

    lemma iter_properties[rule_format]: includes semilat
    shows "[| acc r ; pres_type step n A; mono r step n A;
         bounded step n; ∀p∈w0. p < n; ss0 ∈ list n A;
         ∀p<n. p ∉ w0 --> stable r step ss0 p |] ==>
       iter f step ss0 w0 = (ss',w')
       -->
       ss' ∈ list n A ∧ stables r step ss' ∧ ss0 <=[r] ss' ∧
       (∀ts∈list n A. ss0 <=[r] ts ∧ stables r step ts --> ss' <=[r] ts)"
    apply(insert semilat)
    apply (unfold iter_def stables_def)
    apply (rule_tac P = "%(ss,w).
     ss ∈ list n A ∧ (∀p<n. p ∉ w --> stable r step ss p) ∧ ss0 <=[r] ss ∧
     (∀ts∈list n A. ss0 <=[r] ts ∧ stables r step ts --> ss <=[r] ts) ∧
     (∀p∈w. p < n)" and
     r = "{(ss',ss) . ss <[r] ss'} <*lex*> finite_psubset"
           in while_rule)

    -- "Invariant holds initially:"
    apply (simp add:stables_def)

    -- "Invariant is preserved:"
    apply(simp add: stables_def split_paired_all)
    apply(rename_tac ss w)
    apply(subgoal_tac "(SOME p. p ∈ w) ∈ w")
     prefer 2; apply (fast intro: someI)
    apply(subgoal_tac "∀(q,t) ∈ set (step (SOME p. p ∈ w) (ss ! (SOME p. p ∈ w))). q < length ss ∧ t ∈ A")
     prefer 2
     apply clarify
     apply (rule conjI)
      apply(clarsimp, blast dest!: boundedD)
     apply (erule pres_typeD)
      prefer 3
      apply assumption
      apply (erule listE_nth_in)
      apply simp
     apply simp
    apply (subst decomp_propa)
     apply fast
    apply simp
    apply (rule conjI)
     apply (rule merges_preserves_type)
     apply blast
     apply clarify
     apply (rule conjI)
      apply(clarsimp, fast dest!: boundedD)
     apply (erule pres_typeD)
      prefer 3
      apply assumption
      apply (erule listE_nth_in)
      apply blast
     apply blast
    apply (rule conjI)
     apply clarify
     apply (blast intro!: stable_pres_lemma)
    apply (rule conjI)
     apply (blast intro!: merges_incr intro: le_list_trans)
    apply (rule conjI)
     apply clarsimp
     apply (blast intro!: merges_bounded_lemma)
    apply (blast dest!: boundedD)

    -- "Postcondition holds upon termination:"
    apply(clarsimp simp add: stables_def split_paired_all)

    -- "Well-foundedness of the termination relation:"
    apply (rule wf_lex_prod)
     apply (insert orderI [THEN acc_le_listI])
     apply (simp only: acc_def lesssub_def)
    apply (rule wf_finite_psubset)

    -- "Loop decreases along termination relation:"
    apply(simp add: stables_def split_paired_all)
    apply(rename_tac ss w)
    apply(subgoal_tac "(SOME p. p ∈ w) ∈ w")
     prefer 2; apply (fast intro: someI)
    apply(subgoal_tac "∀(q,t) ∈ set (step (SOME p. p ∈ w) (ss ! (SOME p. p ∈ w))). q < length ss ∧ t ∈ A")
     prefer 2
     apply clarify
     apply (rule conjI)
      apply(clarsimp, blast dest!: boundedD)
     apply (erule pres_typeD)
      prefer 3
      apply assumption
      apply (erule listE_nth_in)
      apply blast
     apply blast
    apply (subst decomp_propa)
     apply blast
    apply clarify
    apply (simp del: listE_length
        add: lex_prod_def finite_psubset_def
             bounded_nat_set_is_finite)
    apply (rule termination_lemma)
    apply assumption+
    defer
    apply assumption
    apply clarsimp
    done

    lemma kildall_properties: includes semilat
    shows "[| acc r; pres_type step n A; mono r step n A;
         bounded step n; ss0 ∈ list n A |] ==>
      kildall r f step ss0 ∈ list n A ∧
      stables r step (kildall r f step ss0) ∧
      ss0 <=[r] kildall r f step ss0 ∧
      (∀ts∈list n A. ss0 <=[r] ts ∧ stables r step ts -->
                     kildall r f step ss0 <=[r] ts)"
    apply (unfold kildall_def)
    apply(case_tac "iter f step ss0 (unstables r step ss0)")
    apply(simp)
    apply (rule iter_properties)
    by (simp_all add: unstables_def stable_def)

    lemma is_bcv_kildall: includes semilat
    shows "[| acc r; top r T; pres_type step n A; bounded step n; mono r step n A |]
      ==> is_bcv r T step n A (kildall r f step)"
    apply(unfold is_bcv_def wt_step_def)
    apply(insert semilat kildall_properties[of A])
    apply(simp add:stables_def)
    apply clarify
    apply(subgoal_tac "kildall r f step ss ∈ list n A")
     prefer 2 apply (simp(no_asm_simp))
    apply (rule iffI)
     apply (rule_tac x = "kildall r f step ss" in bexI)
      apply (rule conjI)
       apply (blast)
      apply (simp  (no_asm_simp))
     apply(assumption)
    apply clarify
    apply(subgoal_tac "kildall r f step ss!p <=_r ts!p")
     apply simp
    apply (blast intro!: le_listD less_lengthI)
    done

    end

lemmas

      Let s f == f s

      [| semilat (A1, r1, f1); x1 ∈ A1; y1 ∈ A1 |]
      ==> (x1 +_f1 y1 = y1) = (x1 <=_r1 y1)

lemmas

      Let s f == f s

      [| semilat (A1, r1, f1); x1 ∈ A1; y1 ∈ A1 |]
      ==> (x1 +_f1 y1 = y1) = (x1 <=_r1 y1)

lemma nth_merges:

      [| semilat (A, r, f); p < length ss; ss ∈ list n A;
         ∀(p, t)∈set ps. p < n ∧ t ∈ A |]
      ==> merges f ps ss ! p = map snd [(p', t')∈ps . p' = p] ++_f ss ! p

lemma length_merges:

      length (merges f ps ss) = length ss

lemma merges_preserves_type_lemma:

      semilat (A, r, f)
      ==> ∀xs. xs ∈ list n A -->
               (∀(p, x)∈set ps. p < n ∧ x ∈ A) --> merges f ps xs ∈ list n A

lemma merges_preserves_type:

      [| semilat (A, r, f); xs ∈ list n A; ∀(p, x)∈set ps. p < n ∧ x ∈ A |]
      ==> merges f ps xs ∈ list n A

lemma merges_incr_lemma:

      semilat (A, r, f)
      ==> ∀xs. xs ∈ list n A -->
               (∀(p, x)∈set ps. p < length xs ∧ x ∈ A) --> xs <=[r] merges f ps xs

lemma merges_incr:

      [| semilat (A, r, f); xs ∈ list n A; ∀(p, x)∈set ps. p < length xs ∧ x ∈ A |]
      ==> xs <=[r] merges f ps xs

lemma merges_same_conv:

      semilat (A, r, f)
      ==> ∀xs. xs ∈ list n A -->
               (∀(p, x)∈set ps. p < length xs ∧ x ∈ A) -->
               (merges f ps xs = xs) = (∀(p, x)∈set ps. x <=_r xs ! p)

lemma list_update_le_listI:

      semilat (A, r, f)
      ==> set xs ⊆ A -->
          set ys ⊆ A -->
          xs <=[r] ys -->
          p < length xs --> x <=_r ys ! p --> x ∈ A --> xs[p := x +_f xs ! p] <=[r] ys

lemma merges_pres_le_ub:

      [| semilat (A, r, f); set ts ⊆ A; set ss ⊆ A;
         ∀(p, t)∈set ps. t <=_r ts ! p ∧ t ∈ A ∧ p < length ts; ss <=[r] ts |]
      ==> merges f ps ss <=[r] ts

lemma decomp_propa:

      ∀(q, t)∈set qs. q < length ss
      ==> propa f qs ss w =
          (merges f qs ss, {q. ∃t. (q, t) ∈ set qs ∧ t +_f ss ! q ≠ ss ! q} ∪ w)

lemma stable_pres_lemma:

      [| semilat (A, r, f); pres_type step n A; bounded step n; ss ∈ list n A; p ∈ w;
         ∀q∈w. q < n; ∀q<n. q ∉ w --> stable r step ss q; q < n;
         ∀s'. (q, s') ∈ set (step p (ss ! p)) --> s' +_f ss ! q = ss ! q;
         q ∉ w ∨ q = p |]
      ==> stable r step (merges f (step p (ss ! p)) ss) q

lemma merges_bounded_lemma:

      [| semilat (A, r, f); SemilatAlg.mono r step n A; bounded step n;
         ∀(p', s')∈set (step p (ss ! p)). s' ∈ A; ss ∈ list n A; ts ∈ list n A; p < n;
         ss <=[r] ts; ∀p<n. stable r step ts p |]
      ==> merges f (step p (ss ! p)) ss <=[r] ts

lemma termination_lemma:

      [| semilat (A, r, f); ss ∈ list 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 +_f ss ! q ≠ ss ! q} ∪ (w - {p}) ⊂ w

lemma iter_properties:

      [| semilat (A, r, f); acc r; pres_type step n A; SemilatAlg.mono r step n A;
         bounded step n; ∀p∈w0.0. p < n; ss0.0 ∈ list n A;
         ∀p<n. p ∉ w0.0 --> stable r step ss0.0 p |]
      ==> iter f step ss0.0 w0.0 = (ss', w') -->
          ss' ∈ list n A ∧
          stables r step ss' ∧
          ss0.0 <=[r] ss' ∧
          (∀ts∈list n A. ss0.0 <=[r] ts ∧ stables r step ts --> ss' <=[r] ts)

lemma kildall_properties:

      [| semilat (A, r, f); acc r; pres_type step n A; SemilatAlg.mono r step n A;
         bounded step n; ss0.0 ∈ list n A |]
      ==> kildall r f step ss0.0 ∈ list n A ∧
          stables r step (kildall r f step ss0.0) ∧
          ss0.0 <=[r] kildall r f step ss0.0 ∧
          (∀ts∈list n A.
              ss0.0 <=[r] ts ∧ stables r step ts --> kildall r f step ss0.0 <=[r] ts)

lemma is_bcv_kildall:

      [| semilat (A, r, f); acc r; top r T; pres_type step n A; bounded step n;
         SemilatAlg.mono r step n A |]
      ==> is_bcv r T step n A (kildall r f step)