src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.rls
changeset 41561 d1318f3c86ba
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.rls	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,27 @@
     1.4 +           /*********************************************************/
     1.5 +                           /*Proof Rule Declarations*/
     1.6 +    /*Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039*/
     1.7 +             /*Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.*/
     1.8 +           /*********************************************************/
     1.9 +
    1.10 +
    1.11 +                        /*DATE : 29-NOV-2010 14:30:10.98*/
    1.12 +
    1.13 +                  /*procedure Greatest_Common_Divisor.G_C_D*/
    1.14 +
    1.15 +
    1.16 +rule_family g_c_d_rules:
    1.17 +     X      requires [X:any] &
    1.18 +     X <= Y requires [X:ire, Y:ire] &
    1.19 +     X >= Y requires [X:ire, Y:ire].
    1.20 +
    1.21 +g_c_d_rules(1): integer__size >= 0 may_be_deduced.
    1.22 +g_c_d_rules(2): integer__first may_be_replaced_by -2147483648.
    1.23 +g_c_d_rules(3): integer__last may_be_replaced_by 2147483647.
    1.24 +g_c_d_rules(4): integer__base__first may_be_replaced_by -2147483648.
    1.25 +g_c_d_rules(5): integer__base__last may_be_replaced_by 2147483647.
    1.26 +g_c_d_rules(6): natural__size >= 0 may_be_deduced.
    1.27 +g_c_d_rules(7): natural__first may_be_replaced_by 0.
    1.28 +g_c_d_rules(8): natural__last may_be_replaced_by 2147483647.
    1.29 +g_c_d_rules(9): natural__base__first may_be_replaced_by -2147483648.
    1.30 +g_c_d_rules(10): natural__base__last may_be_replaced_by 2147483647.