# HG changeset patch # User huffman # Date 1182461590 -7200 # Node ID 08e6c03b2a726cd2419bd0cc0063811c649a27d9 # Parent e28b41e8b7d4f105feaf1a5addc4eec576b96202 add thm antiquotations diff -r e28b41e8b7d4 -r 08e6c03b2a72 src/HOL/nat_simprocs.ML --- a/src/HOL/nat_simprocs.ML Thu Jun 21 23:28:44 2007 +0200 +++ b/src/HOL/nat_simprocs.ML Thu Jun 21 23:33:10 2007 +0200 @@ -11,7 +11,7 @@ (*Maps n to #n for n = 0, 1, 2*) val numeral_syms = - [nat_numeral_0_eq_0 RS sym, nat_numeral_1_eq_1 RS sym, numeral_2_eq_2 RS sym]; + [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym]; val numeral_sym_ss = HOL_ss addsimps numeral_syms; fun rename_numerals th = @@ -47,12 +47,12 @@ val trans_tac = Int_Numeral_Simprocs.trans_tac; val bin_simps = - [nat_numeral_0_eq_0 RS sym, nat_numeral_1_eq_1 RS sym, - add_nat_number_of, nat_number_of_add_left, - diff_nat_number_of, le_number_of_eq_not_less, - mult_nat_number_of, nat_number_of_mult_left, - less_nat_number_of, - @{thm Let_number_of}, nat_number_of] @ + [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, + @{thm add_nat_number_of}, @{thm nat_number_of_add_left}, + @{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less}, + @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, + @{thm less_nat_number_of}, + @{thm Let_number_of}, @{thm nat_number_of}] @ arith_simps @ rel_simps; fun prep_simproc (name, pats, proc) = @@ -137,8 +137,8 @@ val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq - ([nat_numeral_0_eq_0, numeral_1_eq_Suc_0, add_0, add_0_right, - mult_0, mult_0_right, mult_1, mult_1_right] @ contra_rules); + ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm add_0}, @{thm add_0_right}, + @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules); (*Like HOL_ss but with an ordering that brings numerals to the front @@ -157,7 +157,7 @@ val trans_tac = fn _ => trans_tac val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ - [Suc_eq_add_numeral_1_left] @ add_ac + [@{thm Suc_eq_add_numeral_1_left}] @ add_ac val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) @@ -174,8 +174,8 @@ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT - val bal_add1 = nat_eq_add_iff1 RS trans - val bal_add2 = nat_eq_add_iff2 RS trans + val bal_add1 = @{thm nat_eq_add_iff1} RS trans + val bal_add2 = @{thm nat_eq_add_iff2} RS trans ); structure LessCancelNumerals = CancelNumeralsFun @@ -183,8 +183,8 @@ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT - val bal_add1 = nat_less_add_iff1 RS trans - val bal_add2 = nat_less_add_iff2 RS trans + val bal_add1 = @{thm nat_less_add_iff1} RS trans + val bal_add2 = @{thm nat_less_add_iff2} RS trans ); structure LeCancelNumerals = CancelNumeralsFun @@ -192,8 +192,8 @@ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT - val bal_add1 = nat_le_add_iff1 RS trans - val bal_add2 = nat_le_add_iff2 RS trans + val bal_add1 = @{thm nat_le_add_iff1} RS trans + val bal_add2 = @{thm nat_le_add_iff2} RS trans ); structure DiffCancelNumerals = CancelNumeralsFun @@ -201,8 +201,8 @@ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv val mk_bal = HOLogic.mk_binop @{const_name HOL.minus} val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT - val bal_add1 = nat_diff_add_eq1 RS trans - val bal_add2 = nat_diff_add_eq2 RS trans + val bal_add1 = @{thm nat_diff_add_eq1} RS trans + val bal_add2 = @{thm nat_diff_add_eq2} RS trans ); @@ -241,11 +241,11 @@ val dest_sum = dest_Sucs_sum false val mk_coeff = mk_coeff val dest_coeff = dest_coeff - val left_distrib = left_add_mult_distrib RS trans + val left_distrib = @{thm left_add_mult_distrib} RS trans val prove_conv = Int_Numeral_Base_Simprocs.prove_conv_nohyps val trans_tac = fn _ => trans_tac - val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [Suc_eq_add_numeral_1] @ add_ac + val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ add_ac val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) @@ -271,7 +271,7 @@ val trans_tac = fn _ => trans_tac val norm_ss1 = num_ss addsimps - numeral_syms @ add_0s @ mult_1s @ [Suc_eq_add_numeral_1_left] @ add_ac + numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ add_ac val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) @@ -287,7 +287,7 @@ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Divides.div} val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT - val cancel = nat_mult_div_cancel1 RS trans + val cancel = @{thm nat_mult_div_cancel1} RS trans val neg_exchanges = false ) @@ -296,7 +296,7 @@ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT - val cancel = nat_mult_eq_cancel1 RS trans + val cancel = @{thm nat_mult_eq_cancel1} RS trans val neg_exchanges = false ) @@ -305,7 +305,7 @@ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT - val cancel = nat_mult_less_cancel1 RS trans + val cancel = @{thm nat_mult_less_cancel1} RS trans val neg_exchanges = true ) @@ -314,7 +314,7 @@ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT - val cancel = nat_mult_le_cancel1 RS trans + val cancel = @{thm nat_mult_le_cancel1} RS trans val neg_exchanges = true ) @@ -372,7 +372,7 @@ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT - val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_eq_cancel_disj + val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_eq_cancel_disj} ); structure LessCancelFactor = ExtractCommonTermFun @@ -380,7 +380,7 @@ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT - val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_less_cancel_disj + val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_less_cancel_disj} ); structure LeCancelFactor = ExtractCommonTermFun @@ -388,7 +388,7 @@ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT - val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_le_cancel_disj + val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_le_cancel_disj} ); structure DivideCancelFactor = ExtractCommonTermFun @@ -396,7 +396,7 @@ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Divides.div} val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT - val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_div_cancel_disj + val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_div_cancel_disj} ); val cancel_factor = @@ -525,15 +525,15 @@ (* reduce contradictory <= to False *) val add_rules = - [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, nat_0, nat_1, - add_nat_number_of, diff_nat_number_of, mult_nat_number_of, - eq_nat_number_of, less_nat_number_of, le_number_of_eq_not_less, - le_Suc_number_of,le_number_of_Suc, - less_Suc_number_of,less_number_of_Suc, - Suc_eq_number_of,eq_number_of_Suc, - mult_Suc, mult_Suc_right, - eq_number_of_0, eq_0_number_of, less_0_number_of, - of_int_number_of_eq, of_nat_number_of_eq, nat_number_of, if_True, if_False]; + [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, @{thm nat_0}, @{thm nat_1}, + @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of}, + @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less}, + @{thm le_Suc_number_of}, @{thm le_number_of_Suc}, + @{thm less_Suc_number_of}, @{thm less_number_of_Suc}, + @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc}, + @{thm mult_Suc}, @{thm mult_Suc_right}, + @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of}, + @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of}, @{thm if_True}, @{thm if_False}]; val simprocs = Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals;