Up to index of Isabelle/HOL/MicroJava
theory Kildall(* 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)