# HG changeset patch # User berghofe # Date 1027259082 -7200 # Node ID d20a4e67afc8d29f1a599216f7d4112c3d32b8ff # Parent eeac2bbfe95820e5c54e5918450bf6bf58a29745 Examples for program extraction in HOL. diff -r eeac2bbfe958 -r d20a4e67afc8 src/HOL/Extraction/Higman.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Extraction/Higman.thy Sun Jul 21 15:44:42 2002 +0200 @@ -0,0 +1,452 @@ +(* Title: HOL/Extraction/Higman.thy + ID: $Id$ + Author: Stefan Berghofer, TU Muenchen + Monika Seisenberger, LMU Muenchen +*) + +header {* Higman's lemma *} + +theory Higman = Main: + +text {* + Formalization by Stefan Berghofer and Monika Seisenberger, + based on Coquand and Fridlender \cite{Coquand93}. +*} + +datatype letter = A | B + +consts + emb :: "(letter list \ letter list) set" + +inductive emb +intros + emb0 [CPure.intro]: "([], bs) \ emb" + emb1 [CPure.intro]: "(as, bs) \ emb \ (as, b # bs) \ emb" + emb2 [CPure.intro]: "(as, bs) \ emb \ (a # as, a # bs) \ emb" + +consts + L :: "letter list \ letter list list set" + +inductive "L y" +intros + L0 [CPure.intro]: "(w, y) \ emb \ w # ws \ L y" + L1 [CPure.intro]: "ws \ L y \ w # ws \ L y" + +consts + good :: "letter list list set" + +inductive good +intros + good0 [CPure.intro]: "ws \ L w \ w # ws \ good" + good1 [CPure.intro]: "ws \ good \ w # ws \ good" + +consts + R :: "letter \ (letter list list \ letter list list) set" + +inductive "R a" +intros + R0 [CPure.intro]: "([], []) \ R a" + R1 [CPure.intro]: "(vs, ws) \ R a \ (w # vs, (a # w) # ws) \ R a" + +consts + T :: "letter \ (letter list list \ letter list list) set" + +inductive "T a" +intros + T0 [CPure.intro]: "a \ b \ (ws, zs) \ R b \ (w # zs, (a # w) # zs) \ T a" + T1 [CPure.intro]: "(ws, zs) \ T a \ (w # ws, (a # w) # zs) \ T a" + T2 [CPure.intro]: "a \ b \ (ws, zs) \ T a \ (ws, (b # w) # zs) \ T a" + +consts + bar :: "letter list list set" + +inductive bar +intros + bar1 [CPure.intro]: "ws \ good \ ws \ bar" + bar2 [CPure.intro]: "(\w. w # ws \ bar) \ ws \ bar" + +theorem prop1: "([] # ws) \ bar" by rules + +theorem lemma1: "ws \ L as \ ws \ L (a # as)" + by (erule L.induct, rules+) + +theorem lemma2' [rule_format]: "(vs, ws) \ R a \ vs \ L as \ ws \ L (a # as)" + apply (erule R.induct) + apply (rule impI) + apply (erule L.elims) + apply simp+ + apply (rule impI) + apply (erule L.elims) + apply simp_all + apply (rule L0) + apply (erule emb2) + apply (erule L1) + done + +theorem lemma2 [rule_format]: "(vs, ws) \ R a \ vs \ good \ ws \ good" + apply (erule R.induct) + apply rules + apply (rule impI) + apply (erule good.elims) + apply simp_all + apply (rule good0) + apply (erule lemma2') + apply assumption + apply (erule good1) + done + +theorem lemma3' [rule_format]: + "(vs, ws) \ T a \ vs \ L as \ ws \ L (a # as)" + apply (erule T.induct) + apply (rule impI) + apply (erule L.elims) + apply simp_all + apply (rule L0) + apply (erule emb2) + apply (rule L1) + apply (erule lemma1) + apply (rule impI) + apply (erule L.elims) + apply simp_all + apply rules+ + done + +theorem lemma3 [rule_format]: "(ws, zs) \ T a \ ws \ good \ zs \ good" + apply (erule T.induct) + apply (rule impI) + apply (erule good.elims) + apply simp_all + apply (rule good0) + apply (erule lemma1) + apply (erule good1) + apply (rule impI) + apply (erule good.elims) + apply simp_all + apply (rule good0) + apply (erule lemma3') + apply rules+ + done + +theorem letter_cases: + "(a::letter) \ b \ (x = a \ P) \ (x = b \ P) \ P" + apply (case_tac a) + apply (case_tac b) + apply (case_tac x, simp, simp) + apply (case_tac x, simp, simp) + apply (case_tac b) + apply (case_tac x, simp, simp) + apply (case_tac x, simp, simp) + done + +theorem prop2: + "xs \ bar \ \ys. ys \ bar \ + (\a b zs. a \ b \ (xs, zs) \ T a \ (ys, zs) \ T b \ zs \ bar)" + apply (erule bar.induct) + apply (rule allI impI)+ + apply (rule bar1) + apply (rule lemma3) + apply assumption+ + apply (rule allI, rule impI) + apply (erule bar.induct) + apply (rule allI impI)+ + apply (rule bar1) + apply (rule lemma3, assumption, assumption) + apply (rule allI impI)+ + apply (rule bar2) + apply (rule allI) + apply (induct_tac w) + apply (rule prop1) + apply (rule_tac x=aa in letter_cases, assumption) + apply hypsubst + apply (erule_tac x=list in allE) + apply (erule conjE) + apply (erule_tac x=wsa in allE, erule impE) + apply (rule bar2) + apply rules + apply (erule allE, erule allE, erule_tac x="(a # list) # zs" in allE, + erule impE, assumption) + apply (erule impE) + apply (rule T1) + apply assumption + apply (erule mp) + apply (rule T2) + apply (erule not_sym) + apply assumption + apply hypsubst + apply (rotate_tac 1) + apply (erule_tac x=list in allE) + apply (erule conjE) + apply (erule allE, erule allE, erule_tac x="(b # list) # zs" in allE, + erule impE) + apply assumption + apply (erule impE) + apply (rule T2) + apply assumption + apply assumption + apply (erule mp) + apply (rule T1) + apply assumption + done + +theorem lemma4 [rule_format]: "(ws, zs) \ R a \ ws \ [] \ (ws, zs) \ T a" + apply (erule R.induct) + apply rules + apply (rule impI) + apply (case_tac vs) + apply (erule R.elims) + apply simp + apply (case_tac a) + apply (rule_tac b=B in T0) + apply simp + apply (rule R0) + apply (rule_tac b=A in T0) + apply simp + apply (rule R0) + apply simp + apply (rule T1) + apply (erule mp) + apply simp + done + +theorem R_nil: "([], zs) \ R a \ zs = []" + by (erule R.elims, simp+) + +theorem letter_eq_dec: "(a::letter) = b \ a \ b" + apply (case_tac a) + apply (case_tac b) + apply simp + apply simp + apply (case_tac b) + apply simp + apply simp + done + +theorem prop3: "xs \ bar \ \zs. (xs, zs) \ R a \ zs \ bar" + apply (erule bar.induct) + apply (rule allI impI)+ + apply (rule bar1) + apply (rule lemma2) + apply assumption+ + apply (rule allI impI)+ + apply (case_tac ws) + apply simp + apply (drule R_nil) + apply simp_all + apply rules + apply (rule bar2) + apply (rule allI) + apply (induct_tac w) + apply (rule prop1) + apply (rule_tac a1=aaa and b1=a in disjE [OF letter_eq_dec]) + apply rules + apply (rule_tac xs="aa # list" and ys="lista # zs" and zs="(aaa # lista) # zs" + and b=aaa in prop2 [rule_format]) + apply (rule bar2) + apply rules + apply assumption + apply (erule not_sym) + apply (rule T2) + apply (erule not_sym) + apply (erule lemma4) + apply simp + apply (rule T0) + apply assumption+ + done + +theorem prop5: "[w] \ bar" + apply (induct_tac w) + apply (rule prop1) + apply (rule prop3 [rule_format]) + apply rules+ + done + +theorem higman: "[] \ bar" + apply (rule bar2) + apply (rule allI) + apply (rule prop5) + done + +consts + is_prefix :: "'a list \ (nat \ 'a) \ bool" + +primrec + "is_prefix [] f = True" + "is_prefix (x # xs) f = (x = f (length xs) \ is_prefix xs f)" + +theorem good_prefix_lemma: + "ws \ bar \ is_prefix ws f \ (\vs. is_prefix vs f \ vs \ good)" + apply (erule bar.induct) + apply rules + apply (rule impI) + apply (erule_tac x="f (length ws)" in allE) + apply (erule conjE) + apply (erule impE) + apply simp + apply assumption + done + +theorem good_prefix: "\vs. is_prefix vs f \ vs \ good" + apply (insert higman) + apply (drule good_prefix_lemma) + apply simp + done + + +subsection {* Realizers *} + +subsubsection {* Bar induction *} + +datatype Bar = + Good "letter list list" + | Bar "letter list list" "letter list \ Bar" + +consts + bar_realizes :: "Bar \ letter list list \ bool" + +primrec + "bar_realizes (Good ws') ws = (ws = ws' \ ws' \ good)" + "bar_realizes (Bar ws' f) ws = (ws = ws' \ (\w. bar_realizes (f w) (w # ws')))" + +theorem Good_realizer: "ws \ good \ bar_realizes (Good ws) ws" + by simp + +theorem Bar_realizer: + "\w. bar_realizes (f w) (w # ws) \ bar_realizes (Bar ws f) ws" + by simp + +consts + bar_ind :: "Bar \ (letter list list \ 'a) \ + (letter list list \ (letter list \ Bar \ 'a) \ 'a) \ 'a" + +primrec + "bar_ind (Good ws) f g = f ws" + "bar_ind (Bar ws f') f g = g ws (\w. (f' w, bar_ind (f' w) f g))" + +theorem Bar_ind_realizer: + assumes bar: "bar_realizes r x" + and f: "\ws. ws \ good \ P (f ws) ws" + and g: "\ws f. (\w. bar_realizes (fst (f w)) (w # ws) \ P (snd (f w)) (w # ws)) \ + P (g ws f) ws" + shows "P (bar_ind r f g) x" +proof - + have "\x. bar_realizes r x \ P (bar_ind r f g) x" + apply (induct r) + apply simp + apply (rules intro: f) + apply simp + apply (rule g) + apply simp + done + thus ?thesis . +qed + +extract_type + "typeof bar \ Type (TYPE(Bar))" + +realizability + "realizes r (w : bar) \ bar_realizes r w" + +realizers + bar1: "Good" "Good_realizer" + + bar2: "Bar" "\ws f. Bar_realizer \ _ \ _" + + bar.induct (P): "\x P. bar_ind" + "\x P r (h1: _) f (h2: _) g. + Bar_ind_realizer \ _ \ _ \ (\r x. realizes r (P x)) \ _ \ _ \ h1 \ h2" + +subsubsection {* Lists *} + +theorem list_ind_realizer: + assumes f: "P f []" + and g: "\a as r. P r as \ P (g a as r) (a # as)" + shows "P (list_rec f g xs) xs" + apply (induct xs) + apply simp + apply (rule f) + apply simp + apply (rule g) + apply assumption + done + +realizers + list.induct (P): "\P xs f g. list_rec f g xs" + "\P xs f (h: _) g. list_ind_realizer \ _ \ _ \ _ \ _ \ h" + +subsubsection {* Letters *} + +theorem letter_exhaust_realizer: + "(y = A \ P r) \ (y = B \ P s) \ P (case y of A \ r | B \ s)" + by (case_tac y, simp+) + +realizers + letter.exhaust (P): "\y P r s. case y of A \ r | B \ s" + "\y P r (h: _) s. letter_exhaust_realizer \ _ \ (\x. realizes x P) \ _ \ _ \ h" + + +subsection {* Extracting the program *} + +extract good_prefix + +text {* + Program extracted from the proof of @{text good_prefix}: + @{thm [display] good_prefix_def [no_vars]} + Corresponding correctness theorem: + @{thm [display] good_prefix_correctness [no_vars]} + Program extracted from the proof of @{text good_prefix_lemma}: + @{thm [display] good_prefix_lemma_def [no_vars]} + Program extracted from the proof of @{text higman}: + @{thm [display] higman_def [no_vars]} + Program extracted from the proof of @{text prop5}: + @{thm [display] prop5_def [no_vars]} + Program extracted from the proof of @{text prop1}: + @{thm [display] prop1_def [no_vars]} + Program extracted from the proof of @{text prop2}: + @{thm [display] prop2_def [no_vars]} + Program extracted from the proof of @{text prop3}: + @{thm [display] prop3_def [no_vars]} +*} + +generate_code + test = good_prefix + +ML {* +val a = 16807.0; +val m = 2147483647.0; + +fun nextRand seed = + let val t = a*seed + in t - m * real (Real.floor(t/m)) end; + +fun mk_word seed l = + let + val r = nextRand seed; + val i = Real.round (r / m * 10.0); + in if i > 7 andalso l > 2 then (r, []) else + apsnd (cons (if i mod 2 = 0 then A else B)) (mk_word r (l+1)) + end; + +fun f s id0 = mk_word s 0 + | f s (Suc n) = f (fst (mk_word s 0)) n; + +val g1 = snd o (f 20000.0); + +val g2 = snd o (f 50000.0); + +fun f1 id0 = [A,A] + | f1 (Suc id0) = [B] + | f1 (Suc (Suc id0)) = [A,B] + | f1 _ = []; + +fun f2 id0 = [A,A] + | f2 (Suc id0) = [B] + | f2 (Suc (Suc id0)) = [B,A] + | f2 _ = []; + +val xs1 = test g1; +val xs2 = test g2; +val xs3 = test f1; +val xs4 = test f2; +*} + +end diff -r eeac2bbfe958 -r d20a4e67afc8 src/HOL/Extraction/QuotRem.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Extraction/QuotRem.thy Sun Jul 21 15:44:42 2002 +0200 @@ -0,0 +1,55 @@ +(* Title: HOL/Extraction/QuotRem.thy + ID: $Id$ + Author: Stefan Berghofer, TU Muenchen +*) + +header {* Quotient and remainder *} + +theory QuotRem = Main: + +text {* Derivation of quotient and remainder using program extraction. *} + +consts_code + arbitrary :: sumbool ("{* Left *}") + +lemma le_lt_eq_dec: "\m::nat. n <= m \ n < m \ n = m" + apply (induct n) + apply (case_tac m) + apply simp + apply simp + apply (case_tac m) + apply simp + apply simp + done + +lemma division: "\r q. a = Suc b * q + r \ r <= b" + apply (induct a) + apply (rule_tac x = 0 in exI) + apply (rule_tac x = 0 in exI) + apply simp + apply (erule exE) + apply (erule exE) + apply (erule conjE) + apply (drule le_lt_eq_dec) + apply (erule disjE) + apply (rule_tac x = "Suc r" in exI) + apply (rule_tac x = q in exI) + apply simp + apply (rule_tac x = 0 in exI) + apply (rule_tac x = "Suc q" in exI) + apply simp + done + +extract division + +text {* + The program extracted from the above proof looks as follows + @{thm [display] division_def [no_vars]} + The corresponding correctness theorem is + @{thm [display] division_correctness [no_vars]} +*} + +generate_code + test = "division 9 2" + +end diff -r eeac2bbfe958 -r d20a4e67afc8 src/HOL/Extraction/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Extraction/ROOT.ML Sun Jul 21 15:44:42 2002 +0200 @@ -0,0 +1,13 @@ +(* Title: HOL/Extraction/ROOT.ML + ID: $Id$ + +Examples for program extraction in Higher-Order Logic. +*) + +if HOL_proofs < 2 then + warning "HOL proof terms required for running extraction examples" +else + (proofs := 2; + time_use_thy "QuotRem"; + time_use_thy "Warshall"; + time_use_thy "Higman"); diff -r eeac2bbfe958 -r d20a4e67afc8 src/HOL/Extraction/Warshall.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Extraction/Warshall.thy Sun Jul 21 15:44:42 2002 +0200 @@ -0,0 +1,267 @@ +(* Title: HOL/Extraction/Warshall.thy + ID: $Id$ + Author: Stefan Berghofer, TU Muenchen +*) + +header {* Warshall's algorithm *} + +theory Warshall = Main: + +text {* + Derivation of Warshall's algorithm using program extraction, + based on Berger, Schwichtenberg and Seisenberger \cite{Berger-JAR-2001}. +*} + +datatype b = T | F + +theorem b_ind_realizer: + "R x T \ R y F \ R (case b of T \ x | F \ y) b" + by (induct b, simp_all) + +realizers + b.induct (P): "\P b x y. (case b of T \ x | F \ y)" + "\P b x (h: _) y. b_ind_realizer \ (\x b. realizes x (P b)) \ _ \ _ \ _ \ h" + +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+, rules) + +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, arith) + 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, arith) + 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, arith) + 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, arith) + 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 (rules 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 (rules 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 (rules 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 (rules 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 (rules intro: lemma1) + thus ?case .. + qed +qed + +extract warshall + +text {* + The program extracted from the above proof looks as follows + @{thm [display] warshall_def [no_vars]} + The corresponding correctness theorem is + @{thm [display] warshall_correctness [no_vars]} +*} + +end +