summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Fri, 08 Jul 2005 11:38:53 +0200 | |

changeset 16761 | 99549528ce76 |

parent 16760 | 5c5f051aaaaa |

child 16762 | aafd23b47a5d |

proof needed updating because of arith

--- a/src/HOL/Extraction/Warshall.thy Fri Jul 08 11:38:30 2005 +0200 +++ b/src/HOL/Extraction/Warshall.thy Fri Jul 08 11:38:53 2005 +0200 @@ -5,7 +5,9 @@ header {* Warshall's algorithm *} -theory Warshall imports Main begin +theory Warshall +imports Main +begin text {* Derivation of Warshall's algorithm using program extraction, @@ -138,14 +140,12 @@ 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) + from Cons and False show "\<not> list_all (\<lambda>x. x < i) as" by (simp) 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) + show "list_all (\<lambda>x. x<i) (a#ys) \<and> is_path' r j (a#ys) i" by simp qed qed qed @@ -172,14 +172,13 @@ 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) + from snoc and False show "\<not> list_all (\<lambda>x. x < i) as" by simp 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) + by simp qed qed qed @@ -256,4 +255,3 @@ *} end -