# HG changeset patch # User webertj # Date 1090517592 -7200 # Node ID a6cd1a4547511068a7404aa1ff21b3d2c2ba0117 # Parent 277b3a4da3411bbb85fec2ea7c8ec4b5ceb79ba2 minor formatting fixes diff -r 277b3a4da341 -r a6cd1a454751 src/HOL/ex/PresburgerEx.thy --- a/src/HOL/ex/PresburgerEx.thy Thu Jul 22 17:37:31 2004 +0200 +++ b/src/HOL/ex/PresburgerEx.thy Thu Jul 22 19:33:12 2004 +0200 @@ -18,21 +18,24 @@ 2 dvd (y::int) ==> (\(x::int). 2*x = y) & (\(k::int). 3*k = z)" by presburger -theorem "\(x::nat). \(y::nat). (0::nat) \ 5 --> y = 5 + x "; +theorem "\(x::nat). \(y::nat). (0::nat) \ 5 --> y = 5 + x " by presburger text{*Very slow: about 55 seconds on a 1.8GHz machine.*} -theorem "\(x::nat). \(y::nat). y = 5 + x | x div 6 + 1= 2"; +theorem "\(x::nat). \(y::nat). y = 5 + x | x div 6 + 1= 2" + by presburger + +theorem "\(x::int). 0 < x" by presburger -theorem "\(x::int). 0 < x" by presburger - -theorem "\(x::int) y. x < y --> 2 * x + 1 < 2 * y" by presburger +theorem "\(x::int) y. x < y --> 2 * x + 1 < 2 * y" + by presburger -theorem "\(x::int) y. 2 * x + 1 \ 2 * y" by presburger +theorem "\(x::int) y. 2 * x + 1 \ 2 * y" + by presburger -theorem - "\(x::int) y. 0 < x & 0 \ y & 3 * x - 5 * y = 1" by presburger +theorem "\(x::int) y. 0 < x & 0 \ y & 3 * x - 5 * y = 1" + by presburger theorem "~ (\(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)" by presburger @@ -41,10 +44,6 @@ apply (presburger (no_quantify)) oops -theorem "\(x::int). b < x --> a \ x" - apply (presburger (no_quantify)) - oops - theorem "~ (\(x::int). False)" by presburger @@ -52,15 +51,17 @@ apply (presburger (no_quantify)) oops -theorem "\(x::int). (2 dvd x) --> (\(y::int). x = 2*y)" by presburger +theorem "\(x::int). (2 dvd x) --> (\(y::int). x = 2*y)" + by presburger -theorem "\(x::int). (2 dvd x) --> (\(y::int). x = 2*y)" by presburger +theorem "\(x::int). (2 dvd x) --> (\(y::int). x = 2*y)" + by presburger -theorem "\(x::int). (2 dvd x) = (\(y::int). x = 2*y)" by presburger - -theorem "\(x::int). ((2 dvd x) = (\(y::int). x \ 2*y + 1))" by presburger +theorem "\(x::int). (2 dvd x) = (\(y::int). x = 2*y)" + by presburger -theorem "\(x::int). ((2 dvd x) = (\(y::int). x \ 2*y + 1))" by presburger +theorem "\(x::int). ((2 dvd x) = (\(y::int). x \ 2*y + 1))" + by presburger theorem "~ (\(x::int). ((2 dvd x) = (\(y::int). x \ 2*y+1) | @@ -68,25 +69,23 @@ --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))" by presburger -theorem - "~ (\(i::int). 4 \ i --> (\x y. 0 \ x & 0 \ y & 3 * x + 5 * y = i))" +theorem "~ (\(i::int). 4 \ i --> (\x y. 0 \ x & 0 \ y & 3 * x + 5 * y = i))" by presburger -theorem - "\(i::int). 8 \ i --> (\x y. 0 \ x & 0 \ y & 3 * x + 5 * y = i)" - by presburger - -theorem - "\(j::int). \i. j \ i --> (\x y. 0 \ x & 0 \ y & 3 * x + 5 * y = i)" +theorem "\(i::int). 8 \ i --> (\x y. 0 \ x & 0 \ y & 3 * x + 5 * y = i)" by presburger -theorem - "~ (\j (i::int). j \ i --> (\x y. 0 \ x & 0 \ y & 3 * x + 5 * y = i))" +theorem "\(j::int). \i. j \ i --> (\x y. 0 \ x & 0 \ y & 3 * x + 5 * y = i)" + by presburger + +theorem "~ (\j (i::int). j \ i --> (\x y. 0 \ x & 0 \ y & 3 * x + 5 * y = i))" by presburger text{*Very slow: about 80 seconds on a 1.8GHz machine.*} -theorem "(\m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger +theorem "(\m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2" + by presburger -theorem "(\m::int. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger +theorem "(\m::int. n = 2 * m) --> (n + 1) div 2 = n div 2" + by presburger -end \ No newline at end of file +end