--- a/src/HOL/ex/PresburgerEx.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/ex/PresburgerEx.thy Mon Jan 12 16:51:45 2004 +0100
@@ -8,79 +8,86 @@
theory PresburgerEx = Main:
-theorem "(ALL (y::int). (3 dvd y)) ==> ALL (x::int). b < x --> a <= x"
+theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x"
by presburger
theorem "!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==>
- (EX (x::int). 2*x = y) & (EX (k::int). 3*k = z)"
+ (\<exists>(x::int). 2*x = y) & (\<exists>(k::int). 3*k = z)"
by presburger
theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==> 3 dvd z ==>
- 2 dvd (y::int) ==> (EX (x::int). 2*x = y) & (EX (k::int). 3*k = z)"
+ 2 dvd (y::int) ==> (\<exists>(x::int). 2*x = y) & (\<exists>(k::int). 3*k = z)"
by presburger
-theorem "ALL (x::nat). EX (y::nat). (0::nat) <= 5 --> y = 5 + x ";
+theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x ";
by presburger
-theorem "ALL (x::nat). EX (y::nat). y = 5 + x | x div 6 + 1= 2";
+text{*Very slow: about 55 seconds on a 1.8GHz machine.*}
+theorem "\<forall>(x::nat). \<exists>(y::nat). y = 5 + x | x div 6 + 1= 2";
by presburger
-theorem "EX (x::int). 0 < x" by presburger
+theorem "\<exists>(x::int). 0 < x" by presburger
-theorem "ALL (x::int) y. x < y --> 2 * x + 1 < 2 * y" by presburger
+theorem "\<forall>(x::int) y. x < y --> 2 * x + 1 < 2 * y" by presburger
-theorem "ALL (x::int) y. ~(2 * x + 1 = 2 * y)" by presburger
+theorem "\<forall>(x::int) y. 2 * x + 1 \<noteq> 2 * y" by presburger
theorem
- "EX (x::int) y. 0 < x & 0 <= y & 3 * x - 5 * y = 1" by presburger
+ "\<exists>(x::int) y. 0 < x & 0 \<le> y & 3 * x - 5 * y = 1" by presburger
-theorem "~ (EX (x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
+theorem "~ (\<exists>(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
by presburger
-theorem "ALL (x::int). b < x --> a <= x"
+theorem "\<forall>(x::int). b < x --> a \<le> x"
apply (presburger no_quantify)
oops
-theorem "ALL (x::int). b < x --> a <= x"
+theorem "\<forall>(x::int). b < x --> a \<le> x"
apply (presburger no_quantify)
oops
-theorem "~ (EX (x::int). False)"
+theorem "~ (\<exists>(x::int). False)"
by presburger
-theorem "ALL (x::int). (a::int) < 3 * x --> b < 3 * x"
+theorem "\<forall>(x::int). (a::int) < 3 * x --> b < 3 * x"
apply (presburger no_quantify)
oops
-theorem "ALL (x::int). (2 dvd x) --> (EX (y::int). x = 2*y)" by presburger
+theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)" by presburger
-theorem "ALL (x::int). (2 dvd x) --> (EX (y::int). x = 2*y)" by presburger
+theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)" by presburger
-theorem "ALL (x::int). (2 dvd x) = (EX (y::int). x = 2*y)" by presburger
+theorem "\<forall>(x::int). (2 dvd x) = (\<exists>(y::int). x = 2*y)" by presburger
-theorem "ALL (x::int). ((2 dvd x) = (ALL (y::int). ~(x = 2*y + 1)))" by presburger
+theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))" by presburger
+
+theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))" by presburger
-theorem "ALL (x::int). ((2 dvd x) = (ALL (y::int). ~(x = 2*y + 1)))" by presburger
-
-theorem "~ (ALL (x::int). ((2 dvd x) = (ALL (y::int). ~(x = 2*y+1))| (EX (q::int) (u::int) i. 3*i + 2*q - u < 17) --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))"
+theorem "~ (\<forall>(x::int).
+ ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y+1) |
+ (\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17)
+ --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))"
by presburger
theorem
- "~ (ALL (i::int). 4 <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))"
+ "~ (\<forall>(i::int). 4 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
by presburger
theorem
- "ALL (i::int). 8 <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i)" by presburger
+ "\<forall>(i::int). 8 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)"
+ by presburger
theorem
- "EX (j::int). (ALL (i::int). j <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))" by presburger
+ "\<exists>(j::int). \<forall>i. j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)"
+ by presburger
theorem
- "~ (ALL j (i::int). j <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))"
+ "~ (\<forall>j (i::int). j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
by presburger
-theorem "(EX m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger
+text{*Very slow: about 80 seconds on a 1.8GHz machine.*}
+theorem "(\<exists>m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger
-theorem "(EX m::int. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger
+theorem "(\<exists>m::int. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger
end
\ No newline at end of file