src/HOL/Tools/nat_numeral_simprocs.ML
changeset 45668 0ea1c705eebb
parent 45463 9a588a835c1e
child 47108 2a1953f0d20d
equal deleted inserted replaced
45661:ec6ba4b1f6d5 45668:0ea1c705eebb
    25 structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS =
    25 structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS =
    26 struct
    26 struct
    27 
    27 
    28 (*Maps n to #n for n = 0, 1, 2*)
    28 (*Maps n to #n for n = 0, 1, 2*)
    29 val numeral_syms = [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym];
    29 val numeral_syms = [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym];
    30 val numeral_sym_ss = HOL_ss addsimps numeral_syms;
    30 val numeral_sym_ss = HOL_basic_ss addsimps numeral_syms;
    31 
    31 
    32 val rename_numerals = simplify numeral_sym_ss o Thm.transfer @{theory};
    32 val rename_numerals = simplify numeral_sym_ss o Thm.transfer @{theory};
    33 
    33 
    34 (*Utilities*)
    34 (*Utilities*)
    35 
    35 
    62      [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym,
    62      [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym,
    63       @{thm add_nat_number_of}, @{thm nat_number_of_add_left}, 
    63       @{thm add_nat_number_of}, @{thm nat_number_of_add_left}, 
    64       @{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less},
    64       @{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less},
    65       @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, 
    65       @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, 
    66       @{thm less_nat_number_of}, 
    66       @{thm less_nat_number_of}, 
       
    67       @{thm if_True}, @{thm if_False}, @{thm not_False_eq_True},
    67       @{thm Let_number_of}, @{thm nat_number_of}] @
    68       @{thm Let_number_of}, @{thm nat_number_of}] @
    68      @{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps};
    69      @{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps};
    69 
    70 
    70 
    71 
    71 (*** CancelNumerals simprocs ***)
    72 (*** CancelNumerals simprocs ***)
   166   val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   167   val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   167   fun norm_tac ss = 
   168   fun norm_tac ss = 
   168     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   169     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   169     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   170     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   170 
   171 
   171   val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
   172   val numeral_simp_ss = HOL_basic_ss addsimps add_0s @ bin_simps;
   172   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss));
   173   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss));
   173   val simplify_meta_eq  = simplify_meta_eq
   174   val simplify_meta_eq  = simplify_meta_eq
   174   val prove_conv = Arith_Data.prove_conv
   175   val prove_conv = Arith_Data.prove_conv
   175 end;
   176 end;
   176 
   177 
   231   val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   232   val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   232   fun norm_tac ss =
   233   fun norm_tac ss =
   233     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   234     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   234     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   235     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   235 
   236 
   236   val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
   237   val numeral_simp_ss = HOL_basic_ss addsimps add_0s @ bin_simps;
   237   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   238   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   238   val simplify_meta_eq = simplify_meta_eq
   239   val simplify_meta_eq = simplify_meta_eq
   239 end;
   240 end;
   240 
   241 
   241 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   242 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   256   val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   257   val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   257   fun norm_tac ss =
   258   fun norm_tac ss =
   258     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   259     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   259     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   260     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   260 
   261 
   261   val numeral_simp_ss = HOL_ss addsimps bin_simps
   262   val numeral_simp_ss = HOL_basic_ss addsimps bin_simps
   262   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   263   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   263   val simplify_meta_eq = simplify_meta_eq
   264   val simplify_meta_eq = simplify_meta_eq
   264   val prove_conv = Arith_Data.prove_conv
   265   val prove_conv = Arith_Data.prove_conv
   265 end;
   266 end;
   266 
   267 
   337   val dest_sum = dest_prod
   338   val dest_sum = dest_prod
   338   val mk_coeff = mk_coeff
   339   val mk_coeff = mk_coeff
   339   val dest_coeff = dest_coeff
   340   val dest_coeff = dest_coeff
   340   val find_first = find_first_t []
   341   val find_first = find_first_t []
   341   val trans_tac = Numeral_Simprocs.trans_tac
   342   val trans_tac = Numeral_Simprocs.trans_tac
   342   val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   343   val norm_ss = HOL_basic_ss addsimps mult_1s @ @{thms mult_ac}
   343   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   344   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   344   val simplify_meta_eq  = cancel_simplify_meta_eq
   345   val simplify_meta_eq  = cancel_simplify_meta_eq
   345   fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
   346   fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
   346 end;
   347 end;
   347 
   348