Quelle Kildall.thy Sprache: Isabelle

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

section \<open>Kildall's Algorithm \label{sec:Kildall}\<close>

theory Kildall
imports SemilatAlg "HOL-Library.While_Combinator"
begin

primrec propa :: "'s binop \ (nat \ 's) list \ 's list \ nat set \ 's list * nat set" where
  "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')"

definition iter :: "'s binop \ 's step_type \ 's list \ nat set \ 's list \ nat set" where
  "iter f step ss w == while (%(ss,w). w \ {})
       (%(ss,w). let p = SOME p. p \<in> w
                 in propa f (step p (ss!p)) ss (w-{p}))
       (ss,w)"

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

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

primrec merges :: "'s binop \ (nat \ 's) list \ 's list \ 's list" where
  "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 [OF Semilat.intro, symmetric]

lemma (in Semilat) nth_merges:
"\ss. \p < length ss; ss \ list n A; \(p,t)\set ps. p t\A \ \
  (merges f ps ss)!p = map snd [(p',t') \<leftarrow> 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\<in>A" and ps': "?steptype ps'"
    by (cases p') auto
  assume "\ss. p< length ss \ ss \ list n A \ ?steptype ps' \ ?P ss ps'"
  from this [OF _ _ ps'] have 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 l
  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 [simp]: "size(merges f ps ss) = size ss"
  by (induct ps arbitrary: ss) auto

lemma (in Semilat) merges_preserves_type_lemma:
shows "\xs. xs \ list n A \ (\(p,x) \ set ps. p x\A)
          \<longrightarrow> merges f ps xs \<in> 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 x\A \
  \<Longrightarrow> merges f ps xs \<in> 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 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 x \ A \
  \<Longrightarrow> 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 x\A) \
     (merges f ps xs = xs) = (\<forall>(p,x)\<in>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 \<longrightarrow> x\<in>A \<longrightarrow> 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:
  assumes "set ts <= A" and "set ss <= A"
    and "\(p,t)\set ps. t <=_r ts!p \ t \ A \ p < size ts" and "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 <=_r ts!p \ t \ A \ p< size ts \ \
    set qs <= set ps  \<longrightarrow>
    (\<forall>ss. set ss <= A \<longrightarrow> ss <=[r] ts \<longrightarrow> 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]

  from assms show ?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. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> 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 \<in> list n A; p \<in> w; \<forall>q\<in>w. q < n;
     \<forall>q. q < n \<longrightarrow> q \<notin> w \<longrightarrow> stable r step ss q; q < n;
     \<forall>s'. (q,s') \<in> set (step p (ss ! p)) \<longrightarrow> s' +_f ss ! q = ss ! q;
     q \<notin> w \<or> q = p \<rbrakk>
  \<Longrightarrow> 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 (rule semilat)
    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;
    \<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n;
    ss <=[r] ts; \<forall>p. p < n \<longrightarrow> stable r step ts p \<rbrakk>
  \<Longrightarrow> 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:
  assumes semilat: "semilat (A, r, f)"
  shows "\ ss \ list n A; \(q,t)\set qs. q t\A; p\w \ \
  ss <[r] merges f qs ss \<or>
  merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un (w-{p}) < w" (is "PROP ?P")
proof -
  interpret Semilat A r f using assms by (rule Semilat.intro)
  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 +_f ss ! q \ ss ! q)")
    apply (blast elim: equalityE)
    apply clarsimp
    apply (drule bspec, assumption)
    apply (drule bspec, assumption)
    apply clarsimp
    done
qed

lemma iter_properties[rule_format]:
  assumes semilat: "semilat (A, r, f)"
  shows "\ acc r ; pres_type step n A; mono r step n A;
     bounded step n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A;
     \<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step ss0 p \<rbrakk> \<Longrightarrow>
   iter f step ss0 w0 = (ss',w')
   \<longrightarrow>
   ss' \ list n A \ stables r step ss' \ ss0 <=[r] ss' \
   (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss' <=[r] ts)"
  (is "PROP ?P")
proof -
  interpret Semilat A r f using assms by (rule Semilat.intro)
  show "PROP ?P" apply(insert semilat)
apply (unfold iter_def stables_def)
apply (rule_tac P = "%(ss,w).
ss \<in> list n A \<and> (\<forall>p<n. p \<notin> w \<longrightarrow> stable r step ss p) \<and> ss0 <=[r] ss \<and>
(\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step 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)

\<comment> \<open>Invariant holds initially:\<close>
apply (simp add:stables_def)

\<comment> \<open>Invariant is preserved:\<close>
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)

\<comment> \<open>Postcondition holds upon termination:\<close>
apply(clarsimp simp add: stables_def split_paired_all)

\<comment> \<open>Well-foundedness of the termination relation:\<close>
apply (rule wf_lex_prod)
apply (insert orderI [THEN acc_le_listI])
apply (simp add: acc_def lesssub_def wfp_wf_eq [symmetric])
apply (rule wf_finite_psubset)

\<comment> \<open>Loop decreases along termination relation:\<close>
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

qed

lemma kildall_properties:
assumes semilat: "semilat (A, r, f)"
shows "\ acc r; pres_type step n A; mono r step n A;
     bounded step n; ss0 \<in> list n A \<rbrakk> \<Longrightarrow>
  kildall r f step ss0 \<in> list n A \<and>
  stables r step (kildall r f step ss0) \<and>
  ss0 <=[r] kildall r f step ss0 \<and>
  (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow>
                 kildall r f step ss0 <=[r] ts)"
  (is "PROP ?P")
proof -
  interpret Semilat A r f using assms by (rule Semilat.intro)
  show "PROP ?P"
    apply (unfold kildall_def)
    apply(case_tac "iter f step ss0 (unstables r step ss0)")
    apply(simp)
    apply (rule iter_properties)
            apply (simp_all add: unstables_def stable_def)
    apply (rule semilat)
    done
qed

lemma is_bcv_kildall:
assumes semilat: "semilat (A, r, f)"
shows "\ acc r; top r T; pres_type step n A; bounded step n; mono r step n A \
  \<Longrightarrow> is_bcv r T step n A (kildall r f step)"
  (is "PROP ?P")
proof -
  interpret Semilat A r f using assms by (rule Semilat.intro)
  show "PROP ?P"
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
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.