src/HOL/ex/PresburgerEx.thy
author paulson
Mon Jan 12 16:51:45 2004 +0100 (2004-01-12)
changeset 14353 79f9fbef9106
parent 13880 4f7f30f68926
child 14758 af3b71a46a1c
permissions -rw-r--r--
Added lemmas to Ring_and_Field with slightly modified simplification rules

Deleted some little-used integer theorems, replacing them by the generic ones
in Ring_and_Field

Consolidated integer powers
berghofe@13880
     1
(*  Title:      HOL/ex/PresburgerEx.thy
berghofe@13880
     2
    ID:         $Id$
berghofe@13880
     3
    Author:     Amine Chaieb, TU Muenchen
berghofe@13880
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
berghofe@13880
     5
berghofe@13880
     6
Some examples for Presburger Arithmetic
berghofe@13880
     7
*)
berghofe@13880
     8
berghofe@13880
     9
theory PresburgerEx = Main:
berghofe@13880
    10
paulson@14353
    11
theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x"
berghofe@13880
    12
  by presburger
berghofe@13880
    13
berghofe@13880
    14
theorem "!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==>
paulson@14353
    15
  (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
berghofe@13880
    16
  by presburger
berghofe@13880
    17
berghofe@13880
    18
theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==>  3 dvd z ==>
paulson@14353
    19
  2 dvd (y::int) ==> (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
berghofe@13880
    20
  by presburger
berghofe@13880
    21
paulson@14353
    22
theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x ";
berghofe@13880
    23
  by presburger
berghofe@13880
    24
paulson@14353
    25
text{*Very slow: about 55 seconds on a 1.8GHz machine.*}
paulson@14353
    26
theorem "\<forall>(x::nat). \<exists>(y::nat). y = 5 + x | x div 6 + 1= 2";
berghofe@13880
    27
  by presburger
berghofe@13880
    28
paulson@14353
    29
theorem "\<exists>(x::int). 0 < x" by presburger
berghofe@13880
    30
paulson@14353
    31
theorem "\<forall>(x::int) y. x < y --> 2 * x + 1 < 2 * y" by presburger
berghofe@13880
    32
 
paulson@14353
    33
theorem "\<forall>(x::int) y. 2 * x + 1 \<noteq> 2 * y" by presburger
berghofe@13880
    34
 
berghofe@13880
    35
theorem
paulson@14353
    36
   "\<exists>(x::int) y. 0 < x  & 0 \<le> y  & 3 * x - 5 * y = 1" by presburger
berghofe@13880
    37
paulson@14353
    38
theorem "~ (\<exists>(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
berghofe@13880
    39
  by presburger
berghofe@13880
    40
paulson@14353
    41
theorem "\<forall>(x::int). b < x --> a \<le> x"
berghofe@13880
    42
  apply (presburger no_quantify)
berghofe@13880
    43
  oops
berghofe@13880
    44
paulson@14353
    45
theorem "\<forall>(x::int). b < x --> a \<le> x"
berghofe@13880
    46
  apply (presburger no_quantify)
berghofe@13880
    47
  oops
berghofe@13880
    48
paulson@14353
    49
theorem "~ (\<exists>(x::int). False)"
berghofe@13880
    50
  by presburger
berghofe@13880
    51
paulson@14353
    52
theorem "\<forall>(x::int). (a::int) < 3 * x --> b < 3 * x"
berghofe@13880
    53
  apply (presburger no_quantify)
berghofe@13880
    54
  oops
berghofe@13880
    55
paulson@14353
    56
theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)" by presburger 
berghofe@13880
    57
paulson@14353
    58
theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)" by presburger 
berghofe@13880
    59
paulson@14353
    60
theorem "\<forall>(x::int). (2 dvd x) = (\<exists>(y::int). x = 2*y)" by presburger 
berghofe@13880
    61
  
paulson@14353
    62
theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))" by presburger 
paulson@14353
    63
paulson@14353
    64
theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))" by presburger 
berghofe@13880
    65
paulson@14353
    66
theorem "~ (\<forall>(x::int). 
paulson@14353
    67
            ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y+1) | 
paulson@14353
    68
             (\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17)
paulson@14353
    69
             --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))"
berghofe@13880
    70
  by presburger
berghofe@13880
    71
 
berghofe@13880
    72
theorem 
paulson@14353
    73
   "~ (\<forall>(i::int). 4 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
berghofe@13880
    74
  by presburger
berghofe@13880
    75
berghofe@13880
    76
theorem
paulson@14353
    77
    "\<forall>(i::int). 8 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)" 
paulson@14353
    78
  by presburger
berghofe@13880
    79
   
berghofe@13880
    80
theorem
paulson@14353
    81
   "\<exists>(j::int). \<forall>i. j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)"
paulson@14353
    82
  by presburger
berghofe@13880
    83
berghofe@13880
    84
theorem
paulson@14353
    85
   "~ (\<forall>j (i::int). j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
berghofe@13880
    86
  by presburger
berghofe@13880
    87
paulson@14353
    88
text{*Very slow: about 80 seconds on a 1.8GHz machine.*}
paulson@14353
    89
theorem "(\<exists>m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger
berghofe@13880
    90
paulson@14353
    91
theorem "(\<exists>m::int. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger
berghofe@13880
    92
berghofe@13880
    93
end