proof needed updating because of arith
authornipkow
Fri Jul 08 11:38:53 2005 +0200 (2005-07-08)
changeset 1676199549528ce76
parent 16760 5c5f051aaaaa
child 16762 aafd23b47a5d
proof needed updating because of arith
src/HOL/Extraction/Warshall.thy
     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 -