src/HOL/nat_simprocs.ML
changeset 23881 851c74f1bb69
parent 23471 08e6c03b2a72
child 23969 ef782bbf2d09
     1.1 --- a/src/HOL/nat_simprocs.ML	Fri Jul 20 14:28:05 2007 +0200
     1.2 +++ b/src/HOL/nat_simprocs.ML	Fri Jul 20 14:28:25 2007 +0200
     1.3 @@ -125,15 +125,15 @@
     1.4  
     1.5  
     1.6  (*Simplify 1*n and n*1 to n*)
     1.7 -val add_0s  = map rename_numerals [add_0, add_0_right];
     1.8 +val add_0s  = map rename_numerals [@{thm add_0}, @{thm add_0_right}];
     1.9  val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}];
    1.10  
    1.11  (*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
    1.12  
    1.13  (*And these help the simproc return False when appropriate, which helps
    1.14    the arith prover.*)
    1.15 -val contra_rules = [add_Suc, add_Suc_right, Zero_not_Suc, Suc_not_Zero,
    1.16 -                    le_0_eq];
    1.17 +val contra_rules = [@{thm add_Suc}, @{thm add_Suc_right}, @{thm Zero_not_Suc},
    1.18 +  @{thm Suc_not_Zero}, @{thm le_0_eq}];
    1.19  
    1.20  val simplify_meta_eq =
    1.21      Int_Numeral_Simprocs.simplify_meta_eq
    1.22 @@ -157,8 +157,8 @@
    1.23    val trans_tac         = fn _ => trans_tac
    1.24  
    1.25    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
    1.26 -    [@{thm Suc_eq_add_numeral_1_left}] @ add_ac
    1.27 -  val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
    1.28 +    [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
    1.29 +  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
    1.30    fun norm_tac ss = 
    1.31      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    1.32      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    1.33 @@ -181,8 +181,8 @@
    1.34  structure LessCancelNumerals = CancelNumeralsFun
    1.35   (open CancelNumeralsCommon
    1.36    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    1.37 -  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
    1.38 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
    1.39 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
    1.40 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
    1.41    val bal_add1 = @{thm nat_less_add_iff1} RS trans
    1.42    val bal_add2 = @{thm nat_less_add_iff2} RS trans
    1.43  );
    1.44 @@ -190,8 +190,8 @@
    1.45  structure LeCancelNumerals = CancelNumeralsFun
    1.46   (open CancelNumeralsCommon
    1.47    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    1.48 -  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
    1.49 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
    1.50 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
    1.51 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
    1.52    val bal_add1 = @{thm nat_le_add_iff1} RS trans
    1.53    val bal_add2 = @{thm nat_le_add_iff2} RS trans
    1.54  );
    1.55 @@ -245,8 +245,8 @@
    1.56    val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
    1.57    val trans_tac         = fn _ => trans_tac
    1.58  
    1.59 -  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ add_ac
    1.60 -  val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
    1.61 +  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
    1.62 +  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
    1.63    fun norm_tac ss =
    1.64      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    1.65      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    1.66 @@ -271,8 +271,8 @@
    1.67    val trans_tac         = fn _ => trans_tac
    1.68  
    1.69    val norm_ss1 = num_ss addsimps
    1.70 -    numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ add_ac
    1.71 -  val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
    1.72 +    numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
    1.73 +  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
    1.74    fun norm_tac ss =
    1.75      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    1.76      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    1.77 @@ -303,8 +303,8 @@
    1.78  structure LessCancelNumeralFactor = CancelNumeralFactorFun
    1.79   (open CancelNumeralFactorCommon
    1.80    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    1.81 -  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
    1.82 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
    1.83 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
    1.84 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
    1.85    val cancel = @{thm nat_mult_less_cancel1} RS trans
    1.86    val neg_exchanges = true
    1.87  )
    1.88 @@ -312,8 +312,8 @@
    1.89  structure LeCancelNumeralFactor = CancelNumeralFactorFun
    1.90   (open CancelNumeralFactorCommon
    1.91    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    1.92 -  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
    1.93 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
    1.94 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
    1.95 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
    1.96    val cancel = @{thm nat_mult_le_cancel1} RS trans
    1.97    val neg_exchanges = true
    1.98  )
    1.99 @@ -363,7 +363,7 @@
   1.100    val dest_coeff        = dest_coeff
   1.101    val find_first        = find_first_t []
   1.102    val trans_tac         = fn _ => trans_tac
   1.103 -  val norm_ss = HOL_ss addsimps mult_1s @ mult_ac
   1.104 +  val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   1.105    fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   1.106    end;
   1.107  
   1.108 @@ -378,16 +378,16 @@
   1.109  structure LessCancelFactor = ExtractCommonTermFun
   1.110   (open CancelFactorCommon
   1.111    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   1.112 -  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   1.113 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   1.114 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   1.115 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   1.116    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_less_cancel_disj}
   1.117  );
   1.118  
   1.119  structure LeCancelFactor = ExtractCommonTermFun
   1.120   (open CancelFactorCommon
   1.121    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   1.122 -  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   1.123 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   1.124 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   1.125 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   1.126    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_le_cancel_disj}
   1.127  );
   1.128