miz3/Samples/bug1.ml

   1 horizon := -1;;
   2
   3 let FOO = thm `;
   4   !x n. x pow n = &1 <=> abs x = &1 /\ (x < &0 ==> EVEN n) \/ n = 0 [1]
   5   proof
   6     let x be real;
   7     let n be num;
   8     n = 0
   9     ==> (x pow n = &1 <=> abs x = &1 /\ (x < &0 ==> EVEN n) \/ n = 0) [2]
  10     proof
  11       assume n = 0 [3];
  12     qed by ASM_REWRITE_TAC[real_pow],3;
  13     ~(n = 0)
  14     ==> (x pow n = &1 <=> abs x = &1 /\ (x < &0 ==> EVEN n) \/ n = 0) [4]
  15     proof
  16       assume ~(n = 0) [5];
  17       abs x = &1 ==> (x pow n = &1 <=> abs x = &1 /\ (x < &0 ==> EVEN n)) [6]
  18       proof
  19         assume abs x = &1 [7];
  20         &1 < &0 ==> EVEN n [8] by REAL_ARITH_TAC,5;
  21         &1 pow n = &1 <=> &1 < &0 ==> EVEN n [9]
  22           by ASM_REWRITE_TAC[REAL_POW_NEG; REAL_POW_ONE],5 from 8;
  23         EVEN n ==> (&1 = &1 <=> -- &1 < &0 ==> T) [10]
  24         proof
  25           assume EVEN n [11];
  26         qed by ASM_REWRITE_TAC[],5,11;
  27         ~EVEN n ==> (-- &1 = &1 <=> -- &1 < &0 ==> F) [12]
  28         proof
  29           assume ~EVEN n [13];
  30           -- &1 = &1 <=> ~(-- &1 < &0) [14] by REAL_ARITH_TAC,5,13;
  31         qed by ASM_REWRITE_TAC[],5,13 from 14;
  32         (if EVEN n then &1 else -- &1) = &1 <=> -- &1 < &0 ==> EVEN n [15]
  33           by REPEAT COND_CASES_TAC,5 from 10,12;
  34         -- &1 pow n = &1 <=> -- &1 < &0 ==> EVEN n [16]
  35           by ASM_REWRITE_TAC[REAL_POW_NEG; REAL_POW_ONE],5 from 15;
  36         x pow n = &1 <=> x < &0 ==> EVEN n [17]
  37           by FIRST_X_ASSUM(DISJ_CASES_THEN SUBST1_TAC o MATCH_MP (REAL_ARITH (parse_term "abs x = a ==> x = a \\/ x = --a"))),5,7
  38           from 9,16;
  39         x pow n = &1 <=> abs x = &1 /\ (x < &0 ==> EVEN n) [18]
  40           by ASM_REWRITE_TAC[],5,7 from 17;
  41       qed by ALL_TAC,5,7 from 18;
  42       ~(abs x = &1)
  43       ==> (x pow n = &1 <=> abs x = &1 /\ (x < &0 ==> EVEN n)) [19]
  44       proof
  45         assume ~(abs x = &1) [20];
  46       qed by ASM_MESON_TAC[REAL_POW_EQ_1_IMP],5,20;
  47 ::                                                #2
  48 :: 2: inference time-out
  49     qed by ASM_REWRITE_TAC[real_pow],5 from 18;
  50 ::                                            #4
  51 :: 4: unknown label
  52   qed by ASM_CASES_TAC (parse_term "n = 0") from 2,4;`;;