(* Title: HOL/Extraction/Warshall.thy ID: $Id: Warshall.thy,v 1.6 2005/09/23 14:05:42 nipkow Exp $ Author: Stefan Berghofer, TU Muenchen *) header {* Warshall's algorithm *} theory Warshall imports Main begin text {* Derivation of Warshall's algorithm using program extraction, based on Berger, Schwichtenberg and Seisenberger \cite{Berger-JAR-2001}. *} datatype b = T | F consts is_path' :: "('a => 'a => b) => 'a => 'a list => 'a => bool" primrec "is_path' r x [] z = (r x z = T)" "is_path' r x (y # ys) z = (r x y = T ∧ is_path' r y ys z)" constdefs is_path :: "(nat => nat => b) => (nat * nat list * nat) => nat => nat => nat => bool" "is_path r p i j k == fst p = j ∧ snd (snd p) = k ∧ list_all (λx. x < i) (fst (snd p)) ∧ is_path' r (fst p) (fst (snd p)) (snd (snd p))" conc :: "('a * 'a list * 'a) => ('a * 'a list * 'a) => ('a * 'a list * 'a)" "conc p q == (fst p, fst (snd p) @ fst q # fst (snd q), snd (snd q))" theorem is_path'_snoc [simp]: "!!x. is_path' r x (ys @ [y]) z = (is_path' r x ys y ∧ r y z = T)" by (induct ys) simp+ theorem list_all_scoc [simp]: "list_all P (xs @ [x]) = (P x ∧ list_all P xs)" by (induct xs, simp+, iprover) theorem list_all_lemma: "list_all P xs ==> (!!x. P x ==> Q x) ==> list_all Q xs" proof - assume PQ: "!!x. P x ==> Q x" show "list_all P xs ==> list_all Q xs" proof (induct xs) case Nil show ?case by simp next case (Cons y ys) hence Py: "P y" by simp from Cons have Pys: "list_all P ys" by simp show ?case by simp (rule conjI PQ Py Cons Pys)+ qed qed theorem lemma1: "!!p. is_path r p i j k ==> is_path r p (Suc i) j k" apply (unfold is_path_def) apply (simp cong add: conj_cong add: split_paired_all) apply (erule conjE)+ apply (erule list_all_lemma) apply simp done theorem lemma2: "!!p. is_path r p 0 j k ==> r j k = T" apply (unfold is_path_def) apply (simp cong add: conj_cong add: split_paired_all) apply (case_tac "aa") apply simp+ done theorem is_path'_conc: "is_path' r j xs i ==> is_path' r i ys k ==> is_path' r j (xs @ i # ys) k" proof - assume pys: "is_path' r i ys k" show "!!j. is_path' r j xs i ==> is_path' r j (xs @ i # ys) k" proof (induct xs) case (Nil j) hence "r j i = T" by simp with pys show ?case by simp next case (Cons z zs j) hence jzr: "r j z = T" by simp from Cons have pzs: "is_path' r z zs i" by simp show ?case by simp (rule conjI jzr Cons pzs)+ qed qed theorem lemma3: "!!p q. is_path r p i j i ==> is_path r q i i k ==> is_path r (conc p q) (Suc i) j k" apply (unfold is_path_def conc_def) apply (simp cong add: conj_cong add: split_paired_all) apply (erule conjE)+ apply (rule conjI) apply (erule list_all_lemma) apply simp apply (rule conjI) apply (erule list_all_lemma) apply simp apply (rule is_path'_conc) apply assumption+ done theorem lemma5: "!!p. is_path r p (Suc i) j k ==> ~ is_path r p i j k ==> (∃q. is_path r q i j i) ∧ (∃q'. is_path r q' i i k)" proof (simp cong add: conj_cong add: split_paired_all is_path_def, (erule conjE)+) fix xs assume "list_all (λx. x < Suc i) xs" assume "is_path' r j xs k" assume "¬ list_all (λx. x < i) xs" show "(∃ys. list_all (λx. x < i) ys ∧ is_path' r j ys i) ∧ (∃ys. list_all (λx. x < i) ys ∧ is_path' r i ys k)" proof show "!!j. list_all (λx. x < Suc i) xs ==> is_path' r j xs k ==> ¬ list_all (λx. x < i) xs ==> ∃ys. list_all (λx. x < i) ys ∧ is_path' r j ys i" (is "PROP ?ih xs") proof (induct xs) case Nil thus ?case by simp next case (Cons a as j) show ?case proof (cases "a=i") case True show ?thesis proof from True and Cons have "r j i = T" by simp thus "list_all (λx. x < i) [] ∧ is_path' r j [] i" by simp qed next case False have "PROP ?ih as" by (rule Cons) then obtain ys where ys: "list_all (λx. x < i) ys ∧ is_path' r a ys i" proof from Cons show "list_all (λx. x < Suc i) as" by simp from Cons show "is_path' r a as k" by simp from Cons and False show "¬ list_all (λx. x < i) as" by (simp) qed show ?thesis proof from Cons False ys show "list_all (λx. x<i) (a#ys) ∧ is_path' r j (a#ys) i" by simp qed qed qed show "!!k. list_all (λx. x < Suc i) xs ==> is_path' r j xs k ==> ¬ list_all (λx. x < i) xs ==> ∃ys. list_all (λx. x < i) ys ∧ is_path' r i ys k" (is "PROP ?ih xs") proof (induct xs rule: rev_induct) case Nil thus ?case by simp next case (snoc a as k) show ?case proof (cases "a=i") case True show ?thesis proof from True and snoc have "r i k = T" by simp thus "list_all (λx. x < i) [] ∧ is_path' r i [] k" by simp qed next case False have "PROP ?ih as" by (rule snoc) then obtain ys where ys: "list_all (λx. x < i) ys ∧ is_path' r i ys a" proof from snoc show "list_all (λx. x < Suc i) as" by simp from snoc show "is_path' r j as a" by simp from snoc and False show "¬ list_all (λx. x < i) as" by simp qed show ?thesis proof from snoc False ys show "list_all (λx. x < i) (ys @ [a]) ∧ is_path' r i (ys @ [a]) k" by simp qed qed qed qed qed theorem lemma5': "!!p. is_path r p (Suc i) j k ==> ¬ is_path r p i j k ==> ¬ (∀q. ¬ is_path r q i j i) ∧ ¬ (∀q'. ¬ is_path r q' i i k)" by (iprover dest: lemma5) theorem warshall: "!!j k. ¬ (∃p. is_path r p i j k) ∨ (∃p. is_path r p i j k)" proof (induct i) case (0 j k) show ?case proof (cases "r j k") assume "r j k = T" hence "is_path r (j, [], k) 0 j k" by (simp add: is_path_def) hence "∃p. is_path r p 0 j k" .. thus ?thesis .. next assume "r j k = F" hence "r j k ~= T" by simp hence "¬ (∃p. is_path r p 0 j k)" by (iprover dest: lemma2) thus ?thesis .. qed next case (Suc i j k) thus ?case proof assume h1: "¬ (∃p. is_path r p i j k)" from Suc show ?case proof assume "¬ (∃p. is_path r p i j i)" with h1 have "¬ (∃p. is_path r p (Suc i) j k)" by (iprover dest: lemma5') thus ?case .. next assume "∃p. is_path r p i j i" then obtain p where h2: "is_path r p i j i" .. from Suc show ?case proof assume "¬ (∃p. is_path r p i i k)" with h1 have "¬ (∃p. is_path r p (Suc i) j k)" by (iprover dest: lemma5') thus ?case .. next assume "∃q. is_path r q i i k" then obtain q where "is_path r q i i k" .. with h2 have "is_path r (conc p q) (Suc i) j k" by (rule lemma3) hence "∃pq. is_path r pq (Suc i) j k" .. thus ?case .. qed qed next assume "∃p. is_path r p i j k" hence "∃p. is_path r p (Suc i) j k" by (iprover intro: lemma1) thus ?case .. qed qed extract warshall text {* The program extracted from the above proof looks as follows @{thm [display, eta_contract=false] warshall_def [no_vars]} The corresponding correctness theorem is @{thm [display] warshall_correctness [no_vars]} *} end
theorem is_path'_snoc:
is_path' r x (ys @ [y]) z = (is_path' r x ys y ∧ r y z = T)
theorem list_all_scoc:
list_all P (xs @ [x]) = (P x ∧ list_all P xs)
theorem list_all_lemma:
[| list_all P xs; !!x. P x ==> Q x |] ==> list_all Q xs
theorem lemma1:
is_path r p i j k ==> is_path r p (Suc i) j k
theorem lemma2:
is_path r p 0 j k ==> r j k = T
theorem is_path'_conc:
[| is_path' r j xs i; is_path' r i ys k |] ==> is_path' r j (xs @ i # ys) k
theorem lemma3:
[| is_path r p i j i; is_path r q i i k |] ==> is_path r (conc p q) (Suc i) j k
theorem lemma5:
[| is_path r p (Suc i) j k; ¬ is_path r p i j k |] ==> (∃q. is_path r q i j i) ∧ (∃q'. is_path r q' i i k)
theorem lemma5':
[| is_path r p (Suc i) j k; ¬ is_path r p i j k |] ==> ¬ (∀q. ¬ is_path r q i j i) ∧ ¬ (∀q'. ¬ is_path r q' i i k)
theorem warshall:
¬ (∃p. is_path r p i j k) ∨ (∃p. is_path r p i j k)