Examples for program extraction in HOL.
--- /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 \<times> letter list) set"
+
+inductive emb
+intros
+ emb0 [CPure.intro]: "([], bs) \<in> emb"
+ emb1 [CPure.intro]: "(as, bs) \<in> emb \<Longrightarrow> (as, b # bs) \<in> emb"
+ emb2 [CPure.intro]: "(as, bs) \<in> emb \<Longrightarrow> (a # as, a # bs) \<in> emb"
+
+consts
+ L :: "letter list \<Rightarrow> letter list list set"
+
+inductive "L y"
+intros
+ L0 [CPure.intro]: "(w, y) \<in> emb \<Longrightarrow> w # ws \<in> L y"
+ L1 [CPure.intro]: "ws \<in> L y \<Longrightarrow> w # ws \<in> L y"
+
+consts
+ good :: "letter list list set"
+
+inductive good
+intros
+ good0 [CPure.intro]: "ws \<in> L w \<Longrightarrow> w # ws \<in> good"
+ good1 [CPure.intro]: "ws \<in> good \<Longrightarrow> w # ws \<in> good"
+
+consts
+ R :: "letter \<Rightarrow> (letter list list \<times> letter list list) set"
+
+inductive "R a"
+intros
+ R0 [CPure.intro]: "([], []) \<in> R a"
+ R1 [CPure.intro]: "(vs, ws) \<in> R a \<Longrightarrow> (w # vs, (a # w) # ws) \<in> R a"
+
+consts
+ T :: "letter \<Rightarrow> (letter list list \<times> letter list list) set"
+
+inductive "T a"
+intros
+ T0 [CPure.intro]: "a \<noteq> b \<Longrightarrow> (ws, zs) \<in> R b \<Longrightarrow> (w # zs, (a # w) # zs) \<in> T a"
+ T1 [CPure.intro]: "(ws, zs) \<in> T a \<Longrightarrow> (w # ws, (a # w) # zs) \<in> T a"
+ T2 [CPure.intro]: "a \<noteq> b \<Longrightarrow> (ws, zs) \<in> T a \<Longrightarrow> (ws, (b # w) # zs) \<in> T a"
+
+consts
+ bar :: "letter list list set"
+
+inductive bar
+intros
+ bar1 [CPure.intro]: "ws \<in> good \<Longrightarrow> ws \<in> bar"
+ bar2 [CPure.intro]: "(\<forall>w. w # ws \<in> bar) \<Longrightarrow> ws \<in> bar"
+
+theorem prop1: "([] # ws) \<in> bar" by rules
+
+theorem lemma1: "ws \<in> L as \<Longrightarrow> ws \<in> L (a # as)"
+ by (erule L.induct, rules+)
+
+theorem lemma2' [rule_format]: "(vs, ws) \<in> R a \<Longrightarrow> vs \<in> L as \<longrightarrow> ws \<in> 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) \<in> R a \<Longrightarrow> vs \<in> good \<longrightarrow> ws \<in> 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) \<in> T a \<Longrightarrow> vs \<in> L as \<longrightarrow> ws \<in> 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) \<in> T a \<Longrightarrow> ws \<in> good \<longrightarrow> zs \<in> 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) \<noteq> b \<Longrightarrow> (x = a \<Longrightarrow> P) \<Longrightarrow> (x = b \<Longrightarrow> P) \<Longrightarrow> 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 \<in> bar \<Longrightarrow> \<forall>ys. ys \<in> bar \<longrightarrow>
+ (\<forall>a b zs. a \<noteq> b \<longrightarrow> (xs, zs) \<in> T a \<longrightarrow> (ys, zs) \<in> T b \<longrightarrow> zs \<in> 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) \<in> R a \<Longrightarrow> ws \<noteq> [] \<longrightarrow> (ws, zs) \<in> 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) \<in> R a \<Longrightarrow> zs = []"
+ by (erule R.elims, simp+)
+
+theorem letter_eq_dec: "(a::letter) = b \<or> a \<noteq> 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 \<in> bar \<Longrightarrow> \<forall>zs. (xs, zs) \<in> R a \<longrightarrow> zs \<in> 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] \<in> bar"
+ apply (induct_tac w)
+ apply (rule prop1)
+ apply (rule prop3 [rule_format])
+ apply rules+
+ done
+
+theorem higman: "[] \<in> bar"
+ apply (rule bar2)
+ apply (rule allI)
+ apply (rule prop5)
+ done
+
+consts
+ is_prefix :: "'a list \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"
+
+primrec
+ "is_prefix [] f = True"
+ "is_prefix (x # xs) f = (x = f (length xs) \<and> is_prefix xs f)"
+
+theorem good_prefix_lemma:
+ "ws \<in> bar \<Longrightarrow> is_prefix ws f \<longrightarrow> (\<exists>vs. is_prefix vs f \<and> vs \<in> 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: "\<exists>vs. is_prefix vs f \<and> vs \<in> 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 \<Rightarrow> Bar"
+
+consts
+ bar_realizes :: "Bar \<Rightarrow> letter list list \<Rightarrow> bool"
+
+primrec
+ "bar_realizes (Good ws') ws = (ws = ws' \<and> ws' \<in> good)"
+ "bar_realizes (Bar ws' f) ws = (ws = ws' \<and> (\<forall>w. bar_realizes (f w) (w # ws')))"
+
+theorem Good_realizer: "ws \<in> good \<Longrightarrow> bar_realizes (Good ws) ws"
+ by simp
+
+theorem Bar_realizer:
+ "\<forall>w. bar_realizes (f w) (w # ws) \<Longrightarrow> bar_realizes (Bar ws f) ws"
+ by simp
+
+consts
+ bar_ind :: "Bar \<Rightarrow> (letter list list \<Rightarrow> 'a) \<Rightarrow>
+ (letter list list \<Rightarrow> (letter list \<Rightarrow> Bar \<times> 'a) \<Rightarrow> 'a) \<Rightarrow> 'a"
+
+primrec
+ "bar_ind (Good ws) f g = f ws"
+ "bar_ind (Bar ws f') f g = g ws (\<lambda>w. (f' w, bar_ind (f' w) f g))"
+
+theorem Bar_ind_realizer:
+ assumes bar: "bar_realizes r x"
+ and f: "\<And>ws. ws \<in> good \<Longrightarrow> P (f ws) ws"
+ and g: "\<And>ws f. (\<forall>w. bar_realizes (fst (f w)) (w # ws) \<and> P (snd (f w)) (w # ws)) \<Longrightarrow>
+ P (g ws f) ws"
+ shows "P (bar_ind r f g) x"
+proof -
+ have "\<And>x. bar_realizes r x \<Longrightarrow> 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 \<equiv> Type (TYPE(Bar))"
+
+realizability
+ "realizes r (w : bar) \<equiv> bar_realizes r w"
+
+realizers
+ bar1: "Good" "Good_realizer"
+
+ bar2: "Bar" "\<Lambda>ws f. Bar_realizer \<cdot> _ \<cdot> _"
+
+ bar.induct (P): "\<lambda>x P. bar_ind"
+ "\<Lambda>x P r (h1: _) f (h2: _) g.
+ Bar_ind_realizer \<cdot> _ \<cdot> _ \<cdot> (\<lambda>r x. realizes r (P x)) \<cdot> _ \<cdot> _ \<bullet> h1 \<bullet> h2"
+
+subsubsection {* Lists *}
+
+theorem list_ind_realizer:
+ assumes f: "P f []"
+ and g: "\<And>a as r. P r as \<Longrightarrow> 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): "\<lambda>P xs f g. list_rec f g xs"
+ "\<Lambda>P xs f (h: _) g. list_ind_realizer \<cdot> _ \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> h"
+
+subsubsection {* Letters *}
+
+theorem letter_exhaust_realizer:
+ "(y = A \<Longrightarrow> P r) \<Longrightarrow> (y = B \<Longrightarrow> P s) \<Longrightarrow> P (case y of A \<Rightarrow> r | B \<Rightarrow> s)"
+ by (case_tac y, simp+)
+
+realizers
+ letter.exhaust (P): "\<lambda>y P r s. case y of A \<Rightarrow> r | B \<Rightarrow> s"
+ "\<Lambda>y P r (h: _) s. letter_exhaust_realizer \<cdot> _ \<cdot> (\<lambda>x. realizes x P) \<cdot> _ \<cdot> _ \<bullet> 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
--- /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: "\<And>m::nat. n <= m \<Longrightarrow> n < m \<or> n = m"
+ apply (induct n)
+ apply (case_tac m)
+ apply simp
+ apply simp
+ apply (case_tac m)
+ apply simp
+ apply simp
+ done
+
+lemma division: "\<exists>r q. a = Suc b * q + r \<and> 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
--- /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");
--- /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 \<Longrightarrow> R y F \<Longrightarrow> R (case b of T \<Rightarrow> x | F \<Rightarrow> y) b"
+ by (induct b, simp_all)
+
+realizers
+ b.induct (P): "\<lambda>P b x y. (case b of T \<Rightarrow> x | F \<Rightarrow> y)"
+ "\<Lambda>P b x (h: _) y. b_ind_realizer \<cdot> (\<lambda>x b. realizes x (P b)) \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> h"
+
+consts
+ is_path' :: "('a \<Rightarrow> 'a \<Rightarrow> b) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
+
+primrec
+ "is_path' r x [] z = (r x z = T)"
+ "is_path' r x (y # ys) z = (r x y = T \<and> is_path' r y ys z)"
+
+constdefs
+ is_path :: "(nat \<Rightarrow> nat \<Rightarrow> b) \<Rightarrow> (nat * nat list * nat) \<Rightarrow>
+ nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+ "is_path r p i j k == fst p = j \<and> snd (snd p) = k \<and>
+ list_all (\<lambda>x. x < i) (fst (snd p)) \<and>
+ is_path' r (fst p) (fst (snd p)) (snd (snd p))"
+
+ conc :: "('a * 'a list * 'a) \<Rightarrow> ('a * 'a list * 'a) \<Rightarrow> ('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]:
+ "\<And>x. is_path' r x (ys @ [y]) z = (is_path' r x ys y \<and> r y z = T)"
+ by (induct ys) simp+
+
+theorem list_all_scoc [simp]: "list_all P (xs @ [x]) = (P x \<and> list_all P xs)"
+ by (induct xs, simp+, rules)
+
+theorem list_all_lemma:
+ "list_all P xs \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> list_all Q xs"
+proof -
+ assume PQ: "\<And>x. P x \<Longrightarrow> Q x"
+ show "list_all P xs \<Longrightarrow> 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: "\<And>p. is_path r p i j k \<Longrightarrow> 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: "\<And>p. is_path r p 0 j k \<Longrightarrow> 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 \<Longrightarrow> is_path' r i ys k \<Longrightarrow>
+ is_path' r j (xs @ i # ys) k"
+proof -
+ assume pys: "is_path' r i ys k"
+ show "\<And>j. is_path' r j xs i \<Longrightarrow> 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:
+ "\<And>p q. is_path r p i j i \<Longrightarrow> is_path r q i i k \<Longrightarrow>
+ 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:
+ "\<And>p. is_path r p (Suc i) j k \<Longrightarrow> ~ is_path r p i j k \<Longrightarrow>
+ (\<exists>q. is_path r q i j i) \<and> (\<exists>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 (\<lambda>x. x < Suc i) xs"
+ assume "is_path' r j xs k"
+ assume "\<not> list_all (\<lambda>x. x < i) xs"
+ show "(\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r j ys i) \<and>
+ (\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r i ys k)"
+ proof
+ show "\<And>j. list_all (\<lambda>x. x < Suc i) xs \<Longrightarrow> is_path' r j xs k \<Longrightarrow>
+ \<not> list_all (\<lambda>x. x < i) xs \<Longrightarrow>
+ \<exists>ys. list_all (\<lambda>x. x < i) ys \<and> 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 (\<lambda>x. x < i) [] \<and> 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 (\<lambda>x. x < i) ys \<and> is_path' r a ys i"
+ proof
+ from Cons show "list_all (\<lambda>x. x < Suc i) as" by simp
+ from Cons show "is_path' r a as k" by simp
+ from Cons and False show "\<not> list_all (\<lambda>x. x < i) as"
+ by (simp, arith)
+ qed
+ show ?thesis
+ proof
+ from Cons False ys
+ show "list_all (\<lambda>x. x < i) (a # ys) \<and> is_path' r j (a # ys) i"
+ by (simp, arith)
+ qed
+ qed
+ qed
+ show "\<And>k. list_all (\<lambda>x. x < Suc i) xs \<Longrightarrow> is_path' r j xs k \<Longrightarrow>
+ \<not> list_all (\<lambda>x. x < i) xs \<Longrightarrow>
+ \<exists>ys. list_all (\<lambda>x. x < i) ys \<and> 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 (\<lambda>x. x < i) [] \<and> 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 (\<lambda>x. x < i) ys \<and> is_path' r i ys a"
+ proof
+ from snoc show "list_all (\<lambda>x. x < Suc i) as" by simp
+ from snoc show "is_path' r j as a" by simp
+ from snoc and False show "\<not> list_all (\<lambda>x. x < i) as"
+ by (simp, arith)
+ qed
+ show ?thesis
+ proof
+ from snoc False ys
+ show "list_all (\<lambda>x. x < i) (ys @ [a]) \<and> is_path' r i (ys @ [a]) k"
+ by (simp, arith)
+ qed
+ qed
+ qed
+ qed
+qed
+
+theorem lemma5':
+ "\<And>p. is_path r p (Suc i) j k \<Longrightarrow> \<not> is_path r p i j k \<Longrightarrow>
+ \<not> (\<forall>q. \<not> is_path r q i j i) \<and> \<not> (\<forall>q'. \<not> is_path r q' i i k)"
+ by (rules dest: lemma5)
+
+theorem warshall:
+ "\<And>j k. \<not> (\<exists>p. is_path r p i j k) \<or> (\<exists>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 "\<exists>p. is_path r p 0 j k" ..
+ thus ?thesis ..
+ next
+ assume "r j k = F"
+ hence "r j k ~= T" by simp
+ hence "\<not> (\<exists>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: "\<not> (\<exists>p. is_path r p i j k)"
+ from Suc show ?case
+ proof
+ assume "\<not> (\<exists>p. is_path r p i j i)"
+ with h1 have "\<not> (\<exists>p. is_path r p (Suc i) j k)"
+ by (rules dest: lemma5')
+ thus ?case ..
+ next
+ assume "\<exists>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 "\<not> (\<exists>p. is_path r p i i k)"
+ with h1 have "\<not> (\<exists>p. is_path r p (Suc i) j k)"
+ by (rules dest: lemma5')
+ thus ?case ..
+ next
+ assume "\<exists>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 "\<exists>pq. is_path r pq (Suc i) j k" ..
+ thus ?case ..
+ qed
+ qed
+ next
+ assume "\<exists>p. is_path r p i j k"
+ hence "\<exists>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
+