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

author | berghofe |

Tue, 25 Mar 2003 09:50:53 +0100 | |

changeset 13880 | 4f7f30f68926 |

parent 13879 | 92c0973ac730 |

child 13881 | f63e2a057fd4 |

Added examples for Presburger arithmetic.

src/HOL/ex/PresburgerEx.thy | file | annotate | diff | comparison | revisions | |

src/HOL/ex/ROOT.ML | file | annotate | diff | comparison | revisions |

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/PresburgerEx.thy Tue Mar 25 09:50:53 2003 +0100 @@ -0,0 +1,86 @@ +(* Title: HOL/ex/PresburgerEx.thy + ID: $Id$ + Author: Amine Chaieb, TU Muenchen + License: GPL (GNU GENERAL PUBLIC LICENSE) + +Some examples for Presburger Arithmetic +*) + +theory PresburgerEx = Main: + +theorem "(ALL (y::int). (3 dvd y)) ==> ALL (x::int). b < x --> a <= 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)" + 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)" + by presburger + +theorem "ALL (x::nat). EX (y::nat). (0::nat) <= 5 --> y = 5 + x "; + by presburger + +theorem "ALL (x::nat). EX (y::nat). y = 5 + x | x div 6 + 1= 2"; + by presburger + +theorem "EX (x::int). 0 < x" by presburger + +theorem "ALL (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 + "EX (x::int) y. 0 < x & 0 <= y & 3 * x - 5 * y = 1" by presburger + +theorem "~ (EX (x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)" + by presburger + +theorem "ALL (x::int). b < x --> a <= x" + apply (presburger no_quantify) + oops + +theorem "ALL (x::int). b < x --> a <= x" + apply (presburger no_quantify) + oops + +theorem "~ (EX (x::int). False)" + by presburger + +theorem "ALL (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 "ALL (x::int). (2 dvd x) --> (EX (y::int). x = 2*y)" by presburger + +theorem "ALL (x::int). (2 dvd x) = (EX (y::int). x = 2*y)" 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)))" 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))))" + by presburger + +theorem + "~ (ALL (i::int). 4 <= i --> (EX (x::int) y. 0 <= x & 0 <= 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 + +theorem + "EX (j::int). (ALL (i::int). j <= i --> (EX (x::int) y. 0 <= x & 0 <= 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))" + by presburger + +theorem "(EX 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 + +end \ No newline at end of file