author nipkow Fri Jul 08 11:38:53 2005 +0200 (2005-07-08) changeset 16761 99549528ce76 parent 16760 5c5f051aaaaa child 16762 aafd23b47a5d
proof needed updating because of arith
```     1.1 --- a/src/HOL/Extraction/Warshall.thy	Fri Jul 08 11:38:30 2005 +0200
1.2 +++ b/src/HOL/Extraction/Warshall.thy	Fri Jul 08 11:38:53 2005 +0200
1.3 @@ -5,7 +5,9 @@
1.4
1.5  header {* Warshall's algorithm *}
1.6
1.7 -theory Warshall imports Main begin
1.8 +theory Warshall
1.9 +imports Main
1.10 +begin
1.11
1.12  text {*
1.13    Derivation of Warshall's algorithm using program extraction,
1.14 @@ -138,14 +140,12 @@
1.15        	proof
1.16  	  from Cons show "list_all (\<lambda>x. x < Suc i) as" by simp
1.17  	  from Cons show "is_path' r a as k" by simp
1.18 -	  from Cons and False show "\<not> list_all (\<lambda>x. x < i) as"
1.19 -	    by (simp, arith)
1.20 +	  from Cons and False show "\<not> list_all (\<lambda>x. x < i) as" by (simp)
1.21        	qed
1.22        	show ?thesis
1.23        	proof
1.24  	  from Cons False ys
1.25 -	  show "list_all (\<lambda>x. x < i) (a # ys) \<and> is_path' r j (a # ys) i"
1.26 -	    by (simp, arith)
1.27 +	  show "list_all (\<lambda>x. x<i) (a#ys) \<and> is_path' r j (a#ys) i" by simp
1.28        	qed
1.29        qed
1.30      qed
1.31 @@ -172,14 +172,13 @@
1.32        	proof
1.33  	  from snoc show "list_all (\<lambda>x. x < Suc i) as" by simp
1.34  	  from snoc show "is_path' r j as a" by simp
1.35 -	  from snoc and False show "\<not> list_all (\<lambda>x. x < i) as"
1.36 -	    by (simp, arith)
1.37 +	  from snoc and False show "\<not> list_all (\<lambda>x. x < i) as" by simp
1.38        	qed
1.39        	show ?thesis
1.40        	proof
1.41  	  from snoc False ys
1.42  	  show "list_all (\<lambda>x. x < i) (ys @ [a]) \<and> is_path' r i (ys @ [a]) k"
1.43 -	    by (simp, arith)
1.44 +	    by simp
1.45        	qed
1.46        qed
1.47      qed
1.48 @@ -256,4 +255,3 @@
1.49  *}
1.50
1.51  end
1.52 -
```