--- a/src/HOL/Nitpick.thy Fri Jun 11 16:34:56 2010 +0200
+++ b/src/HOL/Nitpick.thy Fri Jun 11 17:05:11 2010 +0200
@@ -214,6 +214,10 @@
definition inverse_frac :: "'a \<Rightarrow> 'a" where
"inverse_frac q \<equiv> frac (denom q) (num q)"
+definition less_frac :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
+[nitpick_simp]:
+"less_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) < 0"
+
definition less_eq_frac :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
[nitpick_simp]:
"less_eq_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) \<le> 0"
@@ -245,7 +249,7 @@
wf' wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm
int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom
norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac
- less_eq_frac of_frac
+ less_frac less_eq_frac of_frac
hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
word
hide_fact (open) If_def Ex1_def split_def rtrancl_def rtranclp_def tranclp_def
@@ -254,6 +258,6 @@
list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
- inverse_frac_def less_eq_frac_def of_frac_def
+ inverse_frac_def less_frac_def less_eq_frac_def of_frac_def
end
--- a/src/HOL/Rat.thy Fri Jun 11 16:34:56 2010 +0200
+++ b/src/HOL/Rat.thy Fri Jun 11 17:05:11 2010 +0200
@@ -1182,15 +1182,16 @@
(@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
(@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}),
(@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
+ (@{const_name ord_rat_inst.less_rat}, @{const_name Nitpick.less_frac}),
(@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
(@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}),
(@{const_name field_char_0_class.Rats}, @{const_abbrev UNIV})]
*}
lemmas [nitpick_def] = inverse_rat_inst.inverse_rat
- number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_eq_rat
- plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat
- zero_rat_inst.zero_rat
+ number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_rat
+ ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat
+ uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat
subsection{* Float syntax *}
--- a/src/HOL/RealDef.thy Fri Jun 11 16:34:56 2010 +0200
+++ b/src/HOL/RealDef.thy Fri Jun 11 17:05:11 2010 +0200
@@ -1806,12 +1806,13 @@
(@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
(@{const_name number_real_inst.number_of_real}, @{const_name Nitpick.number_of_frac}),
(@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
+ (@{const_name ord_real_inst.less_real}, @{const_name Nitpick.less_eq_frac}),
(@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
*}
lemmas [nitpick_def] = inverse_real_inst.inverse_real
number_real_inst.number_of_real one_real_inst.one_real
- ord_real_inst.less_eq_real plus_real_inst.plus_real
+ ord_real_inst.less_real ord_real_inst.less_eq_real plus_real_inst.plus_real
times_real_inst.times_real uminus_real_inst.uminus_real
zero_real_inst.zero_real