src/HOL/arith_data.ML
changeset 10766 ace2ba2d4fd1
parent 10718 c058f78c3544
child 10906 de95ba2760fe
     1.1 --- a/src/HOL/arith_data.ML	Wed Jan 03 11:13:51 2001 +0100
     1.2 +++ b/src/HOL/arith_data.ML	Wed Jan 03 11:14:48 2001 +0100
     1.3 @@ -13,8 +13,6 @@
     1.4  sig
     1.5    val nat_cancel_sums_add: simproc list
     1.6    val nat_cancel_sums: simproc list
     1.7 -  val nat_cancel_factor: simproc list
     1.8 -  val nat_cancel: simproc list
     1.9  end;
    1.10  
    1.11  structure ArithData: ARITH_DATA =
    1.12 @@ -138,85 +136,31 @@
    1.13  
    1.14  
    1.15  
    1.16 -(** cancel common factor **)
    1.17 -
    1.18 -structure Factor =
    1.19 -struct
    1.20 -  val mk_sum = mk_norm_sum;
    1.21 -  val dest_sum = dest_sum;
    1.22 -  val prove_conv = prove_conv;
    1.23 -  val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac;
    1.24 -end;
    1.25 -
    1.26 -fun mk_cnat n = cterm_of (Theory.sign_of (the_context ())) (HOLogic.mk_nat n);
    1.27 -
    1.28 -fun gen_multiply_tac rule k =
    1.29 -  if k > 0 then
    1.30 -    rtac (instantiate' [] [None, Some (mk_cnat (k - 1))] (rule RS subst_equals)) 1
    1.31 -  else no_tac;
    1.32 -
    1.33 -
    1.34 -(* nat eq *)
    1.35 -
    1.36 -structure EqCancelFactor = CancelFactorFun
    1.37 -(struct
    1.38 -  open Factor;
    1.39 -  val mk_bal = HOLogic.mk_eq;
    1.40 -  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
    1.41 -  val multiply_tac = gen_multiply_tac Suc_mult_cancel1;
    1.42 -end);
    1.43 -
    1.44 -
    1.45 -(* nat less *)
    1.46 -
    1.47 -structure LessCancelFactor = CancelFactorFun
    1.48 -(struct
    1.49 -  open Factor;
    1.50 -  val mk_bal = HOLogic.mk_binrel "op <";
    1.51 -  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
    1.52 -  val multiply_tac = gen_multiply_tac Suc_mult_less_cancel1;
    1.53 -end);
    1.54 -
    1.55 -
    1.56 -(* nat le *)
    1.57 -
    1.58 -structure LeCancelFactor = CancelFactorFun
    1.59 -(struct
    1.60 -  open Factor;
    1.61 -  val mk_bal = HOLogic.mk_binrel "op <=";
    1.62 -  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
    1.63 -  val multiply_tac = gen_multiply_tac Suc_mult_le_cancel1;
    1.64 -end);
    1.65 -
    1.66 -
    1.67 -
    1.68  (** prepare nat_cancel simprocs **)
    1.69  
    1.70 -fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.termT);
    1.71 +fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) 
    1.72 +                                (s, HOLogic.termT);
    1.73  val prep_pats = map prep_pat;
    1.74  
    1.75  fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
    1.76  
    1.77 -val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"];
    1.78 -val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"];
    1.79 -val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"];
    1.80 -val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"];
    1.81 +val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", 
    1.82 +                         "m = Suc n"];
    1.83 +val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n",
    1.84 +                           "m < Suc n"];
    1.85 +val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", 
    1.86 +                         "Suc m <= n", "m <= Suc n"];
    1.87 +val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", 
    1.88 +                           "Suc m - n", "m - Suc n"];
    1.89  
    1.90  val nat_cancel_sums_add = map prep_simproc
    1.91 -  [("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
    1.92 +  [("nateq_cancel_sums",   eq_pats,   EqCancelSums.proc),
    1.93     ("natless_cancel_sums", less_pats, LessCancelSums.proc),
    1.94 -   ("natle_cancel_sums", le_pats, LeCancelSums.proc)];
    1.95 +   ("natle_cancel_sums",   le_pats,   LeCancelSums.proc)];
    1.96  
    1.97  val nat_cancel_sums = nat_cancel_sums_add @
    1.98    [prep_simproc("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)];
    1.99  
   1.100 -val nat_cancel_factor = map prep_simproc
   1.101 -  [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),
   1.102 -   ("natless_cancel_factor", less_pats, LessCancelFactor.proc),
   1.103 -   ("natle_cancel_factor", le_pats, LeCancelFactor.proc)];
   1.104 -
   1.105 -val nat_cancel = nat_cancel_factor @ nat_cancel_sums;
   1.106 -
   1.107  
   1.108  end;
   1.109  
   1.110 @@ -482,7 +426,7 @@
   1.111  (* theory setup *)
   1.112  
   1.113  val arith_setup =
   1.114 - [Simplifier.change_simpset_of (op addsimprocs) nat_cancel] @
   1.115 + [Simplifier.change_simpset_of (op addsimprocs) nat_cancel_sums] @
   1.116    init_lin_arith_data @
   1.117    [Simplifier.change_simpset_of (op addSolver)
   1.118     (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac),