src/HOL/nat_simprocs.ML
changeset 23471 08e6c03b2a72
parent 23164 69e55066dbca
child 23881 851c74f1bb69
     1.1 --- a/src/HOL/nat_simprocs.ML	Thu Jun 21 23:28:44 2007 +0200
     1.2 +++ b/src/HOL/nat_simprocs.ML	Thu Jun 21 23:33:10 2007 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  
     1.5  (*Maps n to #n for n = 0, 1, 2*)
     1.6  val numeral_syms =
     1.7 -       [nat_numeral_0_eq_0 RS sym, nat_numeral_1_eq_1 RS sym, numeral_2_eq_2 RS sym];
     1.8 +       [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym];
     1.9  val numeral_sym_ss = HOL_ss addsimps numeral_syms;
    1.10  
    1.11  fun rename_numerals th =
    1.12 @@ -47,12 +47,12 @@
    1.13  val trans_tac = Int_Numeral_Simprocs.trans_tac;
    1.14  
    1.15  val bin_simps =
    1.16 -     [nat_numeral_0_eq_0 RS sym, nat_numeral_1_eq_1 RS sym,
    1.17 -      add_nat_number_of, nat_number_of_add_left, 
    1.18 -      diff_nat_number_of, le_number_of_eq_not_less,
    1.19 -      mult_nat_number_of, nat_number_of_mult_left, 
    1.20 -      less_nat_number_of, 
    1.21 -      @{thm Let_number_of}, nat_number_of] @
    1.22 +     [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym,
    1.23 +      @{thm add_nat_number_of}, @{thm nat_number_of_add_left}, 
    1.24 +      @{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less},
    1.25 +      @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, 
    1.26 +      @{thm less_nat_number_of}, 
    1.27 +      @{thm Let_number_of}, @{thm nat_number_of}] @
    1.28       arith_simps @ rel_simps;
    1.29  
    1.30  fun prep_simproc (name, pats, proc) =
    1.31 @@ -137,8 +137,8 @@
    1.32  
    1.33  val simplify_meta_eq =
    1.34      Int_Numeral_Simprocs.simplify_meta_eq
    1.35 -        ([nat_numeral_0_eq_0, numeral_1_eq_Suc_0, add_0, add_0_right,
    1.36 -          mult_0, mult_0_right, mult_1, mult_1_right] @ contra_rules);
    1.37 +        ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm add_0}, @{thm add_0_right},
    1.38 +          @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules);
    1.39  
    1.40  
    1.41  (*Like HOL_ss but with an ordering that brings numerals to the front
    1.42 @@ -157,7 +157,7 @@
    1.43    val trans_tac         = fn _ => trans_tac
    1.44  
    1.45    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
    1.46 -    [Suc_eq_add_numeral_1_left] @ add_ac
    1.47 +    [@{thm Suc_eq_add_numeral_1_left}] @ add_ac
    1.48    val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
    1.49    fun norm_tac ss = 
    1.50      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    1.51 @@ -174,8 +174,8 @@
    1.52    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    1.53    val mk_bal   = HOLogic.mk_eq
    1.54    val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
    1.55 -  val bal_add1 = nat_eq_add_iff1 RS trans
    1.56 -  val bal_add2 = nat_eq_add_iff2 RS trans
    1.57 +  val bal_add1 = @{thm nat_eq_add_iff1} RS trans
    1.58 +  val bal_add2 = @{thm nat_eq_add_iff2} RS trans
    1.59  );
    1.60  
    1.61  structure LessCancelNumerals = CancelNumeralsFun
    1.62 @@ -183,8 +183,8 @@
    1.63    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    1.64    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
    1.65    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
    1.66 -  val bal_add1 = nat_less_add_iff1 RS trans
    1.67 -  val bal_add2 = nat_less_add_iff2 RS trans
    1.68 +  val bal_add1 = @{thm nat_less_add_iff1} RS trans
    1.69 +  val bal_add2 = @{thm nat_less_add_iff2} RS trans
    1.70  );
    1.71  
    1.72  structure LeCancelNumerals = CancelNumeralsFun
    1.73 @@ -192,8 +192,8 @@
    1.74    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    1.75    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
    1.76    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
    1.77 -  val bal_add1 = nat_le_add_iff1 RS trans
    1.78 -  val bal_add2 = nat_le_add_iff2 RS trans
    1.79 +  val bal_add1 = @{thm nat_le_add_iff1} RS trans
    1.80 +  val bal_add2 = @{thm nat_le_add_iff2} RS trans
    1.81  );
    1.82  
    1.83  structure DiffCancelNumerals = CancelNumeralsFun
    1.84 @@ -201,8 +201,8 @@
    1.85    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    1.86    val mk_bal   = HOLogic.mk_binop @{const_name HOL.minus}
    1.87    val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT
    1.88 -  val bal_add1 = nat_diff_add_eq1 RS trans
    1.89 -  val bal_add2 = nat_diff_add_eq2 RS trans
    1.90 +  val bal_add1 = @{thm nat_diff_add_eq1} RS trans
    1.91 +  val bal_add2 = @{thm nat_diff_add_eq2} RS trans
    1.92  );
    1.93  
    1.94  
    1.95 @@ -241,11 +241,11 @@
    1.96    val dest_sum          = dest_Sucs_sum false
    1.97    val mk_coeff          = mk_coeff
    1.98    val dest_coeff        = dest_coeff
    1.99 -  val left_distrib      = left_add_mult_distrib RS trans
   1.100 +  val left_distrib      = @{thm left_add_mult_distrib} RS trans
   1.101    val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
   1.102    val trans_tac         = fn _ => trans_tac
   1.103  
   1.104 -  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [Suc_eq_add_numeral_1] @ add_ac
   1.105 +  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ add_ac
   1.106    val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
   1.107    fun norm_tac ss =
   1.108      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   1.109 @@ -271,7 +271,7 @@
   1.110    val trans_tac         = fn _ => trans_tac
   1.111  
   1.112    val norm_ss1 = num_ss addsimps
   1.113 -    numeral_syms @ add_0s @ mult_1s @ [Suc_eq_add_numeral_1_left] @ add_ac
   1.114 +    numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ add_ac
   1.115    val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
   1.116    fun norm_tac ss =
   1.117      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   1.118 @@ -287,7 +287,7 @@
   1.119    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   1.120    val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   1.121    val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
   1.122 -  val cancel = nat_mult_div_cancel1 RS trans
   1.123 +  val cancel = @{thm nat_mult_div_cancel1} RS trans
   1.124    val neg_exchanges = false
   1.125  )
   1.126  
   1.127 @@ -296,7 +296,7 @@
   1.128    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   1.129    val mk_bal   = HOLogic.mk_eq
   1.130    val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   1.131 -  val cancel = nat_mult_eq_cancel1 RS trans
   1.132 +  val cancel = @{thm nat_mult_eq_cancel1} RS trans
   1.133    val neg_exchanges = false
   1.134  )
   1.135  
   1.136 @@ -305,7 +305,7 @@
   1.137    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   1.138    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   1.139    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   1.140 -  val cancel = nat_mult_less_cancel1 RS trans
   1.141 +  val cancel = @{thm nat_mult_less_cancel1} RS trans
   1.142    val neg_exchanges = true
   1.143  )
   1.144  
   1.145 @@ -314,7 +314,7 @@
   1.146    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   1.147    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   1.148    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   1.149 -  val cancel = nat_mult_le_cancel1 RS trans
   1.150 +  val cancel = @{thm nat_mult_le_cancel1} RS trans
   1.151    val neg_exchanges = true
   1.152  )
   1.153  
   1.154 @@ -372,7 +372,7 @@
   1.155    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   1.156    val mk_bal   = HOLogic.mk_eq
   1.157    val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   1.158 -  val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_eq_cancel_disj
   1.159 +  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_eq_cancel_disj}
   1.160  );
   1.161  
   1.162  structure LessCancelFactor = ExtractCommonTermFun
   1.163 @@ -380,7 +380,7 @@
   1.164    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   1.165    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   1.166    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   1.167 -  val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_less_cancel_disj
   1.168 +  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_less_cancel_disj}
   1.169  );
   1.170  
   1.171  structure LeCancelFactor = ExtractCommonTermFun
   1.172 @@ -388,7 +388,7 @@
   1.173    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   1.174    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   1.175    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   1.176 -  val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_le_cancel_disj
   1.177 +  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_le_cancel_disj}
   1.178  );
   1.179  
   1.180  structure DivideCancelFactor = ExtractCommonTermFun
   1.181 @@ -396,7 +396,7 @@
   1.182    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   1.183    val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   1.184    val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
   1.185 -  val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_div_cancel_disj
   1.186 +  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_div_cancel_disj}
   1.187  );
   1.188  
   1.189  val cancel_factor =
   1.190 @@ -525,15 +525,15 @@
   1.191  
   1.192  (* reduce contradictory <= to False *)
   1.193  val add_rules =
   1.194 -  [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, nat_0, nat_1,
   1.195 -   add_nat_number_of, diff_nat_number_of, mult_nat_number_of,
   1.196 -   eq_nat_number_of, less_nat_number_of, le_number_of_eq_not_less,
   1.197 -   le_Suc_number_of,le_number_of_Suc,
   1.198 -   less_Suc_number_of,less_number_of_Suc,
   1.199 -   Suc_eq_number_of,eq_number_of_Suc,
   1.200 -   mult_Suc, mult_Suc_right,
   1.201 -   eq_number_of_0, eq_0_number_of, less_0_number_of,
   1.202 -   of_int_number_of_eq, of_nat_number_of_eq, nat_number_of, if_True, if_False];
   1.203 +  [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, @{thm nat_0}, @{thm nat_1},
   1.204 +   @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
   1.205 +   @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
   1.206 +   @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
   1.207 +   @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
   1.208 +   @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
   1.209 +   @{thm mult_Suc}, @{thm mult_Suc_right},
   1.210 +   @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
   1.211 +   @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of}, @{thm if_True}, @{thm if_False}];
   1.212  
   1.213  val simprocs = Nat_Numeral_Simprocs.combine_numerals
   1.214    :: Nat_Numeral_Simprocs.cancel_numerals;