removal of the nat_cancel_factor simproc
authorpaulson
Wed Jan 03 11:14:48 2001 +0100 (2001-01-03)
changeset 10766ace2ba2d4fd1
parent 10765 94aa0b568009
child 10767 8fa4aafa7314
removal of the nat_cancel_factor simproc
src/HOL/ROOT.ML
src/HOL/arith_data.ML
     1.1 --- a/src/HOL/ROOT.ML	Wed Jan 03 11:13:51 2001 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Wed Jan 03 11:14:48 2001 +0100
     1.3 @@ -27,7 +27,6 @@
     1.4  use "~~/src/Provers/clasimp.ML";
     1.5  use "~~/src/Provers/Arith/fast_lin_arith.ML";
     1.6  use "~~/src/Provers/Arith/cancel_sums.ML";
     1.7 -use "~~/src/Provers/Arith/cancel_factor.ML";
     1.8  use "~~/src/Provers/Arith/abel_cancel.ML";
     1.9  use "~~/src/Provers/Arith/assoc_fold.ML";
    1.10  use "~~/src/Provers/quantifier1.ML";
     2.1 --- a/src/HOL/arith_data.ML	Wed Jan 03 11:13:51 2001 +0100
     2.2 +++ b/src/HOL/arith_data.ML	Wed Jan 03 11:14:48 2001 +0100
     2.3 @@ -13,8 +13,6 @@
     2.4  sig
     2.5    val nat_cancel_sums_add: simproc list
     2.6    val nat_cancel_sums: simproc list
     2.7 -  val nat_cancel_factor: simproc list
     2.8 -  val nat_cancel: simproc list
     2.9  end;
    2.10  
    2.11  structure ArithData: ARITH_DATA =
    2.12 @@ -138,85 +136,31 @@
    2.13  
    2.14  
    2.15  
    2.16 -(** cancel common factor **)
    2.17 -
    2.18 -structure Factor =
    2.19 -struct
    2.20 -  val mk_sum = mk_norm_sum;
    2.21 -  val dest_sum = dest_sum;
    2.22 -  val prove_conv = prove_conv;
    2.23 -  val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac;
    2.24 -end;
    2.25 -
    2.26 -fun mk_cnat n = cterm_of (Theory.sign_of (the_context ())) (HOLogic.mk_nat n);
    2.27 -
    2.28 -fun gen_multiply_tac rule k =
    2.29 -  if k > 0 then
    2.30 -    rtac (instantiate' [] [None, Some (mk_cnat (k - 1))] (rule RS subst_equals)) 1
    2.31 -  else no_tac;
    2.32 -
    2.33 -
    2.34 -(* nat eq *)
    2.35 -
    2.36 -structure EqCancelFactor = CancelFactorFun
    2.37 -(struct
    2.38 -  open Factor;
    2.39 -  val mk_bal = HOLogic.mk_eq;
    2.40 -  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
    2.41 -  val multiply_tac = gen_multiply_tac Suc_mult_cancel1;
    2.42 -end);
    2.43 -
    2.44 -
    2.45 -(* nat less *)
    2.46 -
    2.47 -structure LessCancelFactor = CancelFactorFun
    2.48 -(struct
    2.49 -  open Factor;
    2.50 -  val mk_bal = HOLogic.mk_binrel "op <";
    2.51 -  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
    2.52 -  val multiply_tac = gen_multiply_tac Suc_mult_less_cancel1;
    2.53 -end);
    2.54 -
    2.55 -
    2.56 -(* nat le *)
    2.57 -
    2.58 -structure LeCancelFactor = CancelFactorFun
    2.59 -(struct
    2.60 -  open Factor;
    2.61 -  val mk_bal = HOLogic.mk_binrel "op <=";
    2.62 -  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
    2.63 -  val multiply_tac = gen_multiply_tac Suc_mult_le_cancel1;
    2.64 -end);
    2.65 -
    2.66 -
    2.67 -
    2.68  (** prepare nat_cancel simprocs **)
    2.69  
    2.70 -fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.termT);
    2.71 +fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) 
    2.72 +                                (s, HOLogic.termT);
    2.73  val prep_pats = map prep_pat;
    2.74  
    2.75  fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
    2.76  
    2.77 -val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"];
    2.78 -val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"];
    2.79 -val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"];
    2.80 -val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"];
    2.81 +val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", 
    2.82 +                         "m = Suc n"];
    2.83 +val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n",
    2.84 +                           "m < Suc n"];
    2.85 +val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", 
    2.86 +                         "Suc m <= n", "m <= Suc n"];
    2.87 +val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", 
    2.88 +                           "Suc m - n", "m - Suc n"];
    2.89  
    2.90  val nat_cancel_sums_add = map prep_simproc
    2.91 -  [("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
    2.92 +  [("nateq_cancel_sums",   eq_pats,   EqCancelSums.proc),
    2.93     ("natless_cancel_sums", less_pats, LessCancelSums.proc),
    2.94 -   ("natle_cancel_sums", le_pats, LeCancelSums.proc)];
    2.95 +   ("natle_cancel_sums",   le_pats,   LeCancelSums.proc)];
    2.96  
    2.97  val nat_cancel_sums = nat_cancel_sums_add @
    2.98    [prep_simproc("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)];
    2.99  
   2.100 -val nat_cancel_factor = map prep_simproc
   2.101 -  [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),
   2.102 -   ("natless_cancel_factor", less_pats, LessCancelFactor.proc),
   2.103 -   ("natle_cancel_factor", le_pats, LeCancelFactor.proc)];
   2.104 -
   2.105 -val nat_cancel = nat_cancel_factor @ nat_cancel_sums;
   2.106 -
   2.107  
   2.108  end;
   2.109  
   2.110 @@ -482,7 +426,7 @@
   2.111  (* theory setup *)
   2.112  
   2.113  val arith_setup =
   2.114 - [Simplifier.change_simpset_of (op addsimprocs) nat_cancel] @
   2.115 + [Simplifier.change_simpset_of (op addsimprocs) nat_cancel_sums] @
   2.116    init_lin_arith_data @
   2.117    [Simplifier.change_simpset_of (op addSolver)
   2.118     (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac),