# 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 \<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
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: "\<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
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 \<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
+