# HG changeset patch
# User blanchet
# Date 1276268711 -7200
# Node ID 18000f9d783ef6603ddb0c831334492394770a76
# Parent  18a1e9c7acb055860a468272f32f3231bc39b7dd
adjust Nitpick's handling of "<" on "rat"s and "reals"

diff -r 18a1e9c7acb0 -r 18000f9d783e src/HOL/Nitpick.thy
--- 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
diff -r 18a1e9c7acb0 -r 18000f9d783e src/HOL/Rat.thy
--- 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 *}
 
diff -r 18a1e9c7acb0 -r 18000f9d783e src/HOL/RealDef.thy
--- 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