14 |
14 |
15 val trace = Unsynchronized.ref false; |
15 val trace = Unsynchronized.ref false; |
16 fun trace_msg s = if !trace then tracing s else (); |
16 fun trace_msg s = if !trace then tracing s else (); |
17 |
17 |
18 val mir_ss = |
18 val mir_ss = |
19 let val ths = map thm ["real_of_int_inject", "real_of_int_less_iff", "real_of_int_le_iff"] |
19 let val ths = [@{thm "real_of_int_inject"}, @{thm "real_of_int_less_iff"}, @{thm "real_of_int_le_iff"}] |
20 in @{simpset} delsimps ths addsimps (map (fn th => th RS sym) ths) |
20 in @{simpset} delsimps ths addsimps (map (fn th => th RS sym) ths) |
21 end; |
21 end; |
22 |
22 |
23 val nT = HOLogic.natT; |
23 val nT = HOLogic.natT; |
24 val nat_arith = map thm ["add_nat_number_of", "diff_nat_number_of", |
24 val nat_arith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"}, |
25 "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"]; |
25 @{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"}, @{thm "less_nat_number_of"}]; |
26 |
26 |
27 val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0", |
27 val comp_arith = [@{thm "Let_def"}, @{thm "if_False"}, @{thm "if_True"}, @{thm "add_0"}, |
28 "add_Suc", "add_number_of_left", "mult_number_of_left", |
28 @{thm "add_Suc"}, @{thm "add_number_of_left"}, @{thm "mult_number_of_left"}, |
29 "Suc_eq_plus1"])@ |
29 @{thm "Suc_eq_plus1"}] @ |
30 (map (fn s => thm s RS sym) ["numeral_1_eq_1", "numeral_0_eq_0"]) |
30 (map (fn th => th RS sym) [@{thm "numeral_1_eq_1"}, @{thm "numeral_0_eq_0"}]) |
31 @ @{thms arith_simps} @ nat_arith @ @{thms rel_simps} |
31 @ @{thms arith_simps} @ nat_arith @ @{thms rel_simps} |
32 val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, |
32 val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, |
33 @{thm "real_of_nat_number_of"}, |
33 @{thm "real_of_nat_number_of"}, |
34 @{thm "real_of_nat_Suc"}, @{thm "real_of_nat_one"}, @{thm "real_of_one"}, |
34 @{thm "real_of_nat_Suc"}, @{thm "real_of_nat_one"}, @{thm "real_of_one"}, |
35 @{thm "real_of_int_zero"}, @{thm "real_of_nat_zero"}, |
35 @{thm "real_of_int_zero"}, @{thm "real_of_nat_zero"}, |