src/HOL/Proofs/Extraction/Warshall.thy
author wenzelm
Mon, 25 Feb 2013 12:17:50 +0100
changeset 51272 9c8d63b4b6be
parent 39157 b98909faaea8
child 58272 61d94335ef6c
permissions -rw-r--r--
prefer stateless 'ML_val' for tests;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39157
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 37599
diff changeset
     1
(*  Title:      HOL/Proofs/Extraction/Warshall.thy
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
     2
    Author:     Stefan Berghofer, TU Muenchen
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
     3
*)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
     4
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
     5
header {* Warshall's algorithm *}
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
     6
16761
99549528ce76 proof needed updating because of arith
nipkow
parents: 16417
diff changeset
     7
theory Warshall
99549528ce76 proof needed updating because of arith
nipkow
parents: 16417
diff changeset
     8
imports Main
99549528ce76 proof needed updating because of arith
nipkow
parents: 16417
diff changeset
     9
begin
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    10
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    11
text {*
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    12
  Derivation of Warshall's algorithm using program extraction,
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    13
  based on Berger, Schwichtenberg and Seisenberger \cite{Berger-JAR-2001}.
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    14
*}
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    15
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    16
datatype b = T | F
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    17
25976
11c6811f232c modernized primrec;
wenzelm
parents: 23373
diff changeset
    18
primrec
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    19
  is_path' :: "('a \<Rightarrow> 'a \<Rightarrow> b) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
25976
11c6811f232c modernized primrec;
wenzelm
parents: 23373
diff changeset
    20
where
11c6811f232c modernized primrec;
wenzelm
parents: 23373
diff changeset
    21
    "is_path' r x [] z = (r x z = T)"
11c6811f232c modernized primrec;
wenzelm
parents: 23373
diff changeset
    22
  | "is_path' r x (y # ys) z = (r x y = T \<and> is_path' r y ys z)"
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    23
25976
11c6811f232c modernized primrec;
wenzelm
parents: 23373
diff changeset
    24
definition
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    25
  is_path :: "(nat \<Rightarrow> nat \<Rightarrow> b) \<Rightarrow> (nat * nat list * nat) \<Rightarrow>
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    26
    nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
25976
11c6811f232c modernized primrec;
wenzelm
parents: 23373
diff changeset
    27
where
11c6811f232c modernized primrec;
wenzelm
parents: 23373
diff changeset
    28
  "is_path r p i j k \<longleftrightarrow> fst p = j \<and> snd (snd p) = k \<and>
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    29
     list_all (\<lambda>x. x < i) (fst (snd p)) \<and>
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    30
     is_path' r (fst p) (fst (snd p)) (snd (snd p))"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    31
25976
11c6811f232c modernized primrec;
wenzelm
parents: 23373
diff changeset
    32
definition
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    33
  conc :: "('a * 'a list * 'a) \<Rightarrow> ('a * 'a list * 'a) \<Rightarrow> ('a * 'a list * 'a)"
25976
11c6811f232c modernized primrec;
wenzelm
parents: 23373
diff changeset
    34
where
11c6811f232c modernized primrec;
wenzelm
parents: 23373
diff changeset
    35
  "conc p q = (fst p, fst (snd p) @ fst q # fst (snd q), snd (snd q))"
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    36
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    37
theorem is_path'_snoc [simp]:
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    38
  "\<And>x. is_path' r x (ys @ [y]) z = (is_path' r x ys y \<and> r y z = T)"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    39
  by (induct ys) simp+
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    40
37599
b8e3400dab19 tuned syntax
haftmann
parents: 32960
diff changeset
    41
theorem list_all_scoc [simp]: "list_all P (xs @ [x]) \<longleftrightarrow> P x \<and> list_all P xs"
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 16761
diff changeset
    42
  by (induct xs, simp+, iprover)
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    43
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    44
theorem list_all_lemma: 
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    45
  "list_all P xs \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> list_all Q xs"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    46
proof -
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    47
  assume PQ: "\<And>x. P x \<Longrightarrow> Q x"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    48
  show "list_all P xs \<Longrightarrow> list_all Q xs"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    49
  proof (induct xs)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    50
    case Nil
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    51
    show ?case by simp
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    52
  next
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    53
    case (Cons y ys)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    54
    hence Py: "P y" by simp
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    55
    from Cons have Pys: "list_all P ys" by simp
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    56
    show ?case
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    57
      by simp (rule conjI PQ Py Cons Pys)+
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    58
  qed
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    59
qed
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    60
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    61
theorem lemma1: "\<And>p. is_path r p i j k \<Longrightarrow> is_path r p (Suc i) j k"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    62
  apply (unfold is_path_def)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    63
  apply (simp cong add: conj_cong add: split_paired_all)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    64
  apply (erule conjE)+
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    65
  apply (erule list_all_lemma)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    66
  apply simp
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    67
  done
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    68
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    69
theorem lemma2: "\<And>p. is_path r p 0 j k \<Longrightarrow> r j k = T"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    70
  apply (unfold is_path_def)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    71
  apply (simp cong add: conj_cong add: split_paired_all)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    72
  apply (case_tac "aa")
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    73
  apply simp+
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    74
  done
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    75
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    76
theorem is_path'_conc: "is_path' r j xs i \<Longrightarrow> is_path' r i ys k \<Longrightarrow>
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    77
  is_path' r j (xs @ i # ys) k"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    78
proof -
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    79
  assume pys: "is_path' r i ys k"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    80
  show "\<And>j. is_path' r j xs i \<Longrightarrow> is_path' r j (xs @ i # ys) k"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    81
  proof (induct xs)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    82
    case (Nil j)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    83
    hence "r j i = T" by simp
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    84
    with pys show ?case by simp
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    85
  next
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    86
    case (Cons z zs j)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    87
    hence jzr: "r j z = T" by simp
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    88
    from Cons have pzs: "is_path' r z zs i" by simp
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    89
    show ?case
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    90
      by simp (rule conjI jzr Cons pzs)+
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    91
  qed
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    92
qed
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    93
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    94
theorem lemma3:
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    95
  "\<And>p q. is_path r p i j i \<Longrightarrow> is_path r q i i k \<Longrightarrow>
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    96
   is_path r (conc p q) (Suc i) j k"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    97
  apply (unfold is_path_def conc_def)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    98
  apply (simp cong add: conj_cong add: split_paired_all)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    99
  apply (erule conjE)+
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   100
  apply (rule conjI)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   101
  apply (erule list_all_lemma)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   102
  apply simp
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   103
  apply (rule conjI)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   104
  apply (erule list_all_lemma)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   105
  apply simp
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   106
  apply (rule is_path'_conc)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   107
  apply assumption+
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   108
  done
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   109
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   110
theorem lemma5:
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   111
  "\<And>p. is_path r p (Suc i) j k \<Longrightarrow> ~ is_path r p i j k \<Longrightarrow>
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   112
   (\<exists>q. is_path r q i j i) \<and> (\<exists>q'. is_path r q' i i k)"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   113
proof (simp cong add: conj_cong add: split_paired_all is_path_def, (erule conjE)+)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   114
  fix xs
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 17604
diff changeset
   115
  assume asms:
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 17604
diff changeset
   116
    "list_all (\<lambda>x. x < Suc i) xs"
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 17604
diff changeset
   117
    "is_path' r j xs k"
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 17604
diff changeset
   118
    "\<not> list_all (\<lambda>x. x < i) xs"
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   119
  show "(\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r j ys i) \<and>
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   120
    (\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r i ys k)"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   121
  proof
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   122
    show "\<And>j. list_all (\<lambda>x. x < Suc i) xs \<Longrightarrow> is_path' r j xs k \<Longrightarrow>
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   123
      \<not> list_all (\<lambda>x. x < i) xs \<Longrightarrow>
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   124
    \<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r j ys i" (is "PROP ?ih xs")
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   125
    proof (induct xs)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   126
      case Nil
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   127
      thus ?case by simp
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   128
    next
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   129
      case (Cons a as j)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   130
      show ?case
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   131
      proof (cases "a=i")
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   132
        case True
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   133
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   134
        proof
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   135
          from True and Cons have "r j i = T" by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   136
          thus "list_all (\<lambda>x. x < i) [] \<and> is_path' r j [] i" by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   137
        qed
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   138
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   139
        case False
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   140
        have "PROP ?ih as" by (rule Cons)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   141
        then obtain ys where ys: "list_all (\<lambda>x. x < i) ys \<and> is_path' r a ys i"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   142
        proof
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   143
          from Cons show "list_all (\<lambda>x. x < Suc i) as" by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   144
          from Cons show "is_path' r a as k" by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   145
          from Cons and False show "\<not> list_all (\<lambda>x. x < i) as" by (simp)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   146
        qed
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   147
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   148
        proof
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   149
          from Cons False ys
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   150
          show "list_all (\<lambda>x. x<i) (a#ys) \<and> is_path' r j (a#ys) i" by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   151
        qed
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   152
      qed
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   153
    qed
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   154
    show "\<And>k. list_all (\<lambda>x. x < Suc i) xs \<Longrightarrow> is_path' r j xs k \<Longrightarrow>
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   155
      \<not> list_all (\<lambda>x. x < i) xs \<Longrightarrow>
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   156
      \<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r i ys k" (is "PROP ?ih xs")
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   157
    proof (induct xs rule: rev_induct)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   158
      case Nil
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   159
      thus ?case by simp
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   160
    next
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   161
      case (snoc a as k)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   162
      show ?case
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   163
      proof (cases "a=i")
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   164
        case True
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   165
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   166
        proof
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   167
          from True and snoc have "r i k = T" by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   168
          thus "list_all (\<lambda>x. x < i) [] \<and> is_path' r i [] k" by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   169
        qed
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   170
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   171
        case False
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   172
        have "PROP ?ih as" by (rule snoc)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   173
        then obtain ys where ys: "list_all (\<lambda>x. x < i) ys \<and> is_path' r i ys a"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   174
        proof
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   175
          from snoc show "list_all (\<lambda>x. x < Suc i) as" by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   176
          from snoc show "is_path' r j as a" by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   177
          from snoc and False show "\<not> list_all (\<lambda>x. x < i) as" by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   178
        qed
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   179
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   180
        proof
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   181
          from snoc False ys
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   182
          show "list_all (\<lambda>x. x < i) (ys @ [a]) \<and> is_path' r i (ys @ [a]) k"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   183
            by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   184
        qed
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   185
      qed
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   186
    qed
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 17604
diff changeset
   187
  qed (rule asms)+
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   188
qed
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   189
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   190
theorem lemma5':
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   191
  "\<And>p. is_path r p (Suc i) j k \<Longrightarrow> \<not> is_path r p i j k \<Longrightarrow>
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   192
   \<not> (\<forall>q. \<not> is_path r q i j i) \<and> \<not> (\<forall>q'. \<not> is_path r q' i i k)"
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 16761
diff changeset
   193
  by (iprover dest: lemma5)
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   194
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   195
theorem warshall: 
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   196
  "\<And>j k. \<not> (\<exists>p. is_path r p i j k) \<or> (\<exists>p. is_path r p i j k)"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   197
proof (induct i)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   198
  case (0 j k)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   199
  show ?case
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   200
  proof (cases "r j k")
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   201
    assume "r j k = T"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   202
    hence "is_path r (j, [], k) 0 j k"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   203
      by (simp add: is_path_def)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   204
    hence "\<exists>p. is_path r p 0 j k" ..
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   205
    thus ?thesis ..
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   206
  next
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   207
    assume "r j k = F"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   208
    hence "r j k ~= T" by simp
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   209
    hence "\<not> (\<exists>p. is_path r p 0 j k)"
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 16761
diff changeset
   210
      by (iprover dest: lemma2)
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   211
    thus ?thesis ..
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   212
  qed
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   213
next
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   214
  case (Suc i j k)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   215
  thus ?case
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   216
  proof
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   217
    assume h1: "\<not> (\<exists>p. is_path r p i j k)"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   218
    from Suc show ?case
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   219
    proof
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   220
      assume "\<not> (\<exists>p. is_path r p i j i)"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   221
      with h1 have "\<not> (\<exists>p. is_path r p (Suc i) j k)"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   222
        by (iprover dest: lemma5')
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   223
      thus ?case ..
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   224
    next
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   225
      assume "\<exists>p. is_path r p i j i"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   226
      then obtain p where h2: "is_path r p i j i" ..
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   227
      from Suc show ?case
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   228
      proof
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   229
        assume "\<not> (\<exists>p. is_path r p i i k)"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   230
        with h1 have "\<not> (\<exists>p. is_path r p (Suc i) j k)"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   231
          by (iprover dest: lemma5')
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   232
        thus ?case ..
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   233
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   234
        assume "\<exists>q. is_path r q i i k"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   235
        then obtain q where "is_path r q i i k" ..
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   236
        with h2 have "is_path r (conc p q) (Suc i) j k" 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   237
          by (rule lemma3)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   238
        hence "\<exists>pq. is_path r pq (Suc i) j k" ..
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 29823
diff changeset
   239
        thus ?case ..
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   240
      qed
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   241
    qed
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   242
  next
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   243
    assume "\<exists>p. is_path r p i j k"
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   244
    hence "\<exists>p. is_path r p (Suc i) j k"
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 16761
diff changeset
   245
      by (iprover intro: lemma1)
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   246
    thus ?case ..
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   247
  qed
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   248
qed
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   249
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   250
extract warshall
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   251
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   252
text {*
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   253
  The program extracted from the above proof looks as follows
13671
eec2582923f6 Eta contraction is now switched off when printing extracted program.
berghofe
parents: 13471
diff changeset
   254
  @{thm [display, eta_contract=false] warshall_def [no_vars]}
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   255
  The corresponding correctness theorem is
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   256
  @{thm [display] warshall_correctness [no_vars]}
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   257
*}
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   258
51272
9c8d63b4b6be prefer stateless 'ML_val' for tests;
wenzelm
parents: 39157
diff changeset
   259
ML_val "@{code warshall}"
27982
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   260
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
   261
end