1125 |
1125 |
1126 subsection \<open>Setup for Nitpick\<close> |
1126 subsection \<open>Setup for Nitpick\<close> |
1127 |
1127 |
1128 declaration \<open> |
1128 declaration \<open> |
1129 Nitpick_HOL.register_frac_type @{type_name rat} |
1129 Nitpick_HOL.register_frac_type @{type_name rat} |
1130 [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}), |
1130 [(@{const_name Abs_Rat}, @{const_name Nitpick.Abs_Frac}), |
1131 (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}), |
1131 (@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}), |
1132 (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}), |
1132 (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}), |
1133 (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}), |
1133 (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}), |
1134 (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}), |
1134 (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}), |
1135 (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}), |
1135 (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}), |
1136 (@{const_name ord_rat_inst.less_rat}, @{const_name Nitpick.less_frac}), |
1136 (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}), |
1137 (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}), |
1137 (@{const_name ord_rat_inst.less_rat}, @{const_name Nitpick.less_frac}), |
1138 (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac})] |
1138 (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}), |
|
1139 (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac})] |
1139 \<close> |
1140 \<close> |
1140 |
1141 |
1141 lemmas [nitpick_unfold] = inverse_rat_inst.inverse_rat |
1142 lemmas [nitpick_unfold] = inverse_rat_inst.inverse_rat |
1142 one_rat_inst.one_rat ord_rat_inst.less_rat |
1143 one_rat_inst.one_rat ord_rat_inst.less_rat |
1143 ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat |
1144 ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat |