miz3/Samples/bug0.ml

   1 prioritize_num();;
   2
   3 let EGCD_INVARIANT = thm `;
   4   !m n d. d divides egcd(m,n) <=> d divides m /\ d divides n
   5   proof
   6     let m n be num;
   7     (!m'' n'.
   8          m'' + n' < m + n
   9          ==> (!d. d divides egcd (m'',n') <=>
  10              d divides m'' /\ d divides n'))
  11     ==> (!d. d divides egcd (m,n) <=> d divides m /\ d divides n) [1]
  12     proof
  13       assume !m'' n'.
  14                  m'' + n' < m + n
  15                  ==> (!d. d divides egcd (m'',n') <=>
  16                       d divides m'' /\ d divides n') [2];
  17       !d. d divides
  18           (if m = 0
  19            then n
  20            else
  21           if n = 0
  22           then m
  23           else if m <= n then egcd (m,n - m) else egcd (m - n,n)) <=>
  24           d divides m /\ d divides n [3]
  25       proof
  26         let d be num;
  27         m = 0 ==> (d divides n <=> d divides m /\ d divides n) [4]
  28           by DIVIDES_0;
  29         ~(m = 0)
  30         ==> (d divides
  31              (if n = 0
  32               then m
  33               else
  34              if m <= n then egcd (m,n - m) else egcd (m - n,n)) <=>
  35              d divides m /\ d divides n) [5]
  36         proof
  37           assume ~(m = 0) [6];
  38           n = 0 ==> (d divides m <=> d divides m /\ d divides n) [7]
  39             by DIVIDES_0;
  40           ~(n = 0)
  41           ==> (d divides
  42                (if m <= n then egcd (m,n - m) else egcd (m - n,n)) <=>
  43                d divides m /\ d divides n) [8]
  44           proof
  45             assume ~(n = 0) [9];
  46             m <= n
  47             ==> (d divides egcd (m,n - m) <=>
  48                  d divides m /\ d divides n) [10]
  49             proof
  50               assume m <= n;
  51               m + (n - m) < m + n by ARITH_TAC,6;
  52             qed by #;
  53             ~(m <= n)
  54             ==> (d divides egcd (m - n,n) <=>
  55                  d divides m /\ d divides n) [11]
  56             proof
  57               assume ~(m <= n);
  58               (m - n) + n < m + n by ARITH_TAC,9;
  59               d divides egcd (m - n,n) <=> d divides m - n /\ d divides n
  60                 by 2;
  61               ... <=> d divides (m - n) + n /\ d divides n by DIVIDES_ADD;
  62 ::                                                                       #1
  63 :: 1: inference error
  64             qed by 2,DIVIDES_SUB;
  65 ::                              #1
  66           qed by COND_CASES_TAC from 10,11;
  67         qed by COND_CASES_TAC from 7,8;
  68       qed by COND_CASES_TAC from 4,5;
  69     qed by ONCE_REWRITE_TAC[egcd] from 3;
  70   qed by WF_INDUCT_TAC (parse_term "m + n") from 1;
  71 ::                                                #1
  72 `;;