src/HOL/MicroJava/BV/Kildall.thy

improved tracing of permutative rules.

(*  Title:      HOL/BCV/Kildall.thy
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   2000 TUM

Kildall's algorithm
*)

header "Kildall's Algorithm"

theory Kildall = Typing_Framework + While_Combinator:

constdefs
 pres_type :: "(nat => 's => 's) => nat => 's set => bool"
"pres_type step n A == !s:A. !p<n. step p s : A"

 mono :: "'s ord => (nat => 's => 's) => nat => 's set => bool"
"mono r step n A ==
 !s p t. s : A & p < n & s <=_r t --> step p s <=_r step p t"

consts
 iter :: "'s binop \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> (nat \<Rightarrow> nat list) \<Rightarrow>
          's list \<Rightarrow> nat set \<Rightarrow> 's list"
 propa :: "'s binop => nat list => 's => 's list => nat set => 's list * nat set"

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

defs iter_def:
"iter f step succs ss w ==
 fst(while (%(ss,w). w \<noteq> {})
           (%(ss,w). let p = SOME p. p : w
                     in propa f (succs p) (step p (ss!p)) ss (w-{p}))
           (ss,w))"

constdefs
 unstables ::
 "'s binop => (nat => 's => 's) => (nat => nat list) => 's list => nat set"
"unstables f step succs ss ==
 {p. p < size ss & (? q:set(succs p). step p (ss!p) +_f ss!q ~= ss!q)}"

 kildall :: "'s binop => (nat => 's => 's) => (nat => nat list)
             => 's list => 's list"
"kildall f step succs ss == iter f step succs ss (unstables f step succs ss)"

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


lemmas [simp] = Let_def le_iff_plus_unchanged [symmetric]


lemma pres_typeD:
  "[| pres_type step n A; s:A; p<n |] ==> step p s : A"
  by (unfold pres_type_def, blast)

lemma boundedD:
  "[| bounded succs n; p < n; q : set(succs p) |] ==> q < n"
  by (unfold bounded_def, blast)

lemma monoD:
  "[| mono r step n A; p < n; s:A; s <=_r t |] ==> step p s <=_r step p t"
  by (unfold mono_def, blast)

(** merges **)

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

lemma merges_preserves_type [rule_format, simp]:
  "[| semilat(A,r,f) |] ==> 
     !xs. xs : list n A --> x : A --> (!p : set ps. p<n) 
          --> merges f x ps xs : list n A"
  apply (frule semilatDclosedI)
  apply (unfold closed_def)
  apply (induct_tac ps)
  apply auto
  done

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

lemma merges_same_conv [rule_format]:
  "[| semilat(A,r,f) |] ==> 
     (!xs. xs : list n A --> x:A --> (!p:set ps. p<size xs) --> 
     (merges f x ps xs = xs) = (!p:set ps. x <=_r xs!p))"
  apply (induct_tac ps)
   apply simp
  apply clarsimp
  apply (rename_tac p ps xs)
  apply (rule iffI)
   apply (rule context_conjI)
    apply (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs")
     apply (force dest!: le_listD simp add: nth_list_update)
    apply (erule subst, rule merges_incr)
        apply assumption
       apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
     apply assumption
    apply simp
   apply clarify
   apply (rotate_tac -2)
   apply (erule allE)
   apply (erule impE)
    apply assumption
   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 clarify 
  apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
  done


lemma list_update_le_listI [rule_format]:
  "set xs <= A --> set ys <= A --> xs <=[r] ys --> p < size xs -->  
   x <=_r ys!p --> semilat(A,r,f) --> x:A --> 
   xs[p := x +_f xs!p] <=[r] ys"
  apply (unfold Listn.le_def lesub_def semilat_def)
  apply (simp add: list_all2_conv_all_nth nth_list_update)
  done

lemma merges_pres_le_ub:
  "[| semilat(A,r,f); t:A; set ts <= A; set ss <= A; 
     !p. p:set ps --> t <=_r ts!p; 
     !p. p:set ps --> p<size ts; 
     ss <=[r] ts |] 
  ==> merges f t ps ss <=[r] ts"
proof -
  { fix A r f t ts ps
    have
    "!!qs. [| semilat(A,r,f); set ts <= A; t:A; 
       !p. p:set ps --> t <=_r ts!p; 
       !p. p:set ps --> p<size ts |] ==> 
    set qs <= set ps  --> 
    (!ss. set ss <= A --> ss <=[r] ts --> merges f t 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 (simp (no_asm_simp) add: closedD)
    apply (simp add: list_update_le_listI)
    done
  } note this [dest]
  
  case antecedent
  thus ?thesis by blast
qed


lemma nth_merges [rule_format]:
  "[| semilat (A, r, f); t:A; p < n |] ==> !ss. ss : list n A --> 
     (!p:set ps. p<n) --> 
     (merges f t ps ss)!p = (if p : set ps then t +_f ss!p else ss!p)"
  apply (induct_tac "ps")
   apply simp
  apply (simp add: nth_list_update closedD listE_nth_in) 
  done


(** propa **)

lemma decomp_propa [rule_format]:
  "!ss w. (!q:set qs. q < size ss) --> 
   propa f qs t ss w = 
   (merges f t qs ss, {q. q:set qs & t +_f ss!q ~= ss!q} Un w)"
  apply (induct_tac qs)
   apply simp
  apply (simp (no_asm))
  apply clarify
  apply (rule conjI)
   apply (simp add: nth_list_update)
   apply blast
  apply (simp add: nth_list_update)
  apply blast
  done 

(** iter **)

lemma stable_pres_lemma:
  "[| semilat (A,r,f); pres_type step n A; bounded succs n; 
     ss : list n A; p : w; ! q:w. q < n; 
     ! q. q < n --> q ~: w --> stable r step succs ss q; q < n; 
     q : set (succs p) --> step p (ss ! p) +_f ss ! q = ss ! q; 
     q ~: w | q = p  |] 
  ==> stable r step succs (merges f (step p (ss!p)) (succs p) ss) q"
  apply (unfold stable_def)
  apply (subgoal_tac "step p (ss!p) : A")
   defer
   apply (blast intro: listE_nth_in pres_typeD)     
  apply simp
  apply clarify
  apply (subst nth_merges)
       apply assumption
      apply assumption
     prefer 2
     apply assumption
    apply (blast dest: boundedD)
   apply (blast dest: boundedD)  
  apply (subst nth_merges)
       apply assumption
      apply assumption
     prefer 2
     apply assumption
    apply (blast dest: boundedD)
   apply (blast dest: boundedD)  
  apply simp
  apply (rule conjI)
   apply clarify
   apply (blast intro!: semilat_ub1 semilat_ub2 listE_nth_in
                intro: order_trans dest: boundedD)
  apply (blast intro!: semilat_ub1 semilat_ub2 listE_nth_in
               intro: order_trans dest: boundedD)
  done

lemma merges_bounded_lemma [rule_format]:
  "[| semilat (A,r,f); mono r step n A; bounded succs n; 
     step p (ss!p) : A; ss : list n A; ts : list n A; p < n; 
     ss <=[r] ts; ! p. p < n --> stable r step succs ts p |] 
  ==> merges f (step p (ss!p)) (succs p) ss <=[r] ts"
  apply (unfold stable_def)
  apply (blast intro!: listE_set monoD listE_nth_in le_listD less_lengthI
               intro: merges_pres_le_ub order_trans
               dest: pres_typeD boundedD)
  done

lemma termination_lemma:  
  "[| semilat(A,r,f); ss : list n A; t:A; ! q:set qs. q < n; p:w |] ==> 
      ss <[r] merges f t qs ss | 
  merges f t qs ss = ss & {q. q:set qs & t +_f ss!q ~= ss!q} Un (w-{p}) < w"
  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)
   apply (simp cong add: conj_cong add: le_iff_plus_unchanged [symmetric])
   apply (blast intro!: psubsetI elim: equalityE)
  apply simp
  done

lemma while_properties:
  "\<lbrakk> semilat(A,r,f); acc r ; pres_type step n A; mono r step n A;
     bounded succs n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A;
     \<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step succs ss0 p \<rbrakk> \<Longrightarrow>
   ss' = fst(while (%(ss,w). w \<noteq> {})
         (%(ss,w). let p = SOME p. p \<in> w
                   in propa f (succs p) (step p (ss!p)) ss (w-{p})) (ss0,w0))
   \<longrightarrow>
   ss' \<in> list n A \<and> stables r step succs ss' \<and> ss0 <=[r] ss' \<and>
   (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step succs ts \<longrightarrow> ss' <=[r] ts)"
apply (unfold stables_def)
apply (rule_tac P = "%(ss,w).
 ss \<in> list n A \<and> (\<forall>p<n. p \<notin> w \<longrightarrow> stable r step succs ss p) \<and> ss0 <=[r] ss \<and>
 (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step succs ts \<longrightarrow> ss <=[r] ts) \<and>
 (\<forall>p\<in>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 \<in> w) \<in> w")
 prefer 2; apply (fast intro: someI)
apply(subgoal_tac "step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w)) \<in> A")
 prefer 2; apply (blast intro: pres_typeD listE_nth_in dest: boundedD);
  apply (subgoal_tac "\<forall>q\<in>set(succs (SOME p. p \<in> w)). q < size ss")
 prefer 2;  apply(clarsimp, blast dest!: boundedD)
apply (subst decomp_propa)
 apply blast
apply simp
apply (rule conjI)
 apply (blast intro: merges_preserves_type dest: boundedD);
apply (rule conjI)
 apply (blast intro!: stable_pres_lemma)
apply (rule conjI)
 apply (blast intro!: merges_incr intro: le_list_trans)
apply (rule conjI)
 apply clarsimp
 apply (best 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 (drule (1) semilatDorderI [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 \<in> w) \<in> w")
 prefer 2; apply (fast intro: someI)
apply(subgoal_tac "step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w)) \<in> A")
 prefer 2; apply (blast intro: pres_typeD listE_nth_in dest: boundedD);
  apply (subgoal_tac "\<forall>q\<in>set(succs (SOME p. p \<in> w)). q < n")
 prefer 2;  apply(clarsimp, blast dest!: boundedD)
apply (subst decomp_propa)
 apply clarsimp
apply clarify
apply (simp del: listE_length
    add: lex_prod_def finite_psubset_def decomp_propa termination_lemma
         bounded_nat_set_is_finite)
done

lemma iter_properties:
  "\<lbrakk> semilat(A,r,f); acc r ; pres_type step n A; mono r step n A;
     bounded succs n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A;
     \<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step succs ss0 p \<rbrakk> \<Longrightarrow>
  iter f step succs ss0 w0 : list n A \<and>
  stables r step succs (iter f step succs ss0 w0) \<and>
  ss0 <=[r] iter f step succs ss0 w0 \<and>
  (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step succs ts \<longrightarrow>
                 iter f step succs ss0 w0 <=[r] ts)"
apply(simp add:iter_def del:Let_def)
by(rule while_properties[THEN mp,OF _ _ _ _ _ _ _ _ refl])

lemma kildall_properties:
  "\<lbrakk> semilat(A,r,f); acc r; pres_type step n A; mono r step n A;
     bounded succs n; ss0 \<in> list n A \<rbrakk> \<Longrightarrow>
  kildall f step succs ss0 : list n A \<and>
  stables r step succs (kildall f step succs ss0) \<and>
  ss0 <=[r] kildall f step succs ss0 \<and>
  (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step succs ts \<longrightarrow>
                 kildall f step succs ss0 <=[r] ts)";
apply (unfold kildall_def)
apply (rule iter_properties)
apply (simp_all add: unstables_def stable_def)
apply (blast intro!: le_iff_plus_unchanged [THEN iffD2] listE_nth_in
             dest: boundedD pres_typeD)
done

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

end