adjust Nitpick's handling of "<" on "rat"s and "reals"
authorblanchet
Fri Jun 11 17:05:11 2010 +0200 (2010-06-11)
changeset 3739718000f9d783e
parent 37396 18a1e9c7acb0
child 37398 e194213451c9
adjust Nitpick's handling of "<" on "rat"s and "reals"
src/HOL/Nitpick.thy
src/HOL/Rat.thy
src/HOL/RealDef.thy
     1.1 --- a/src/HOL/Nitpick.thy	Fri Jun 11 16:34:56 2010 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Fri Jun 11 17:05:11 2010 +0200
     1.3 @@ -214,6 +214,10 @@
     1.4  definition inverse_frac :: "'a \<Rightarrow> 'a" where
     1.5  "inverse_frac q \<equiv> frac (denom q) (num q)"
     1.6  
     1.7 +definition less_frac :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
     1.8 +[nitpick_simp]:
     1.9 +"less_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) < 0"
    1.10 +
    1.11  definition less_eq_frac :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
    1.12  [nitpick_simp]:
    1.13  "less_eq_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) \<le> 0"
    1.14 @@ -245,7 +249,7 @@
    1.15      wf' wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm
    1.16      int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom
    1.17      norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac
    1.18 -    less_eq_frac of_frac
    1.19 +    less_frac less_eq_frac of_frac
    1.20  hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
    1.21      word
    1.22  hide_fact (open) If_def Ex1_def split_def rtrancl_def rtranclp_def tranclp_def
    1.23 @@ -254,6 +258,6 @@
    1.24      list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
    1.25      zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
    1.26      plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
    1.27 -    inverse_frac_def less_eq_frac_def of_frac_def
    1.28 +    inverse_frac_def less_frac_def less_eq_frac_def of_frac_def
    1.29  
    1.30  end
     2.1 --- a/src/HOL/Rat.thy	Fri Jun 11 16:34:56 2010 +0200
     2.2 +++ b/src/HOL/Rat.thy	Fri Jun 11 17:05:11 2010 +0200
     2.3 @@ -1182,15 +1182,16 @@
     2.4      (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
     2.5      (@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}),
     2.6      (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
     2.7 +    (@{const_name ord_rat_inst.less_rat}, @{const_name Nitpick.less_frac}),
     2.8      (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
     2.9      (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}),
    2.10      (@{const_name field_char_0_class.Rats}, @{const_abbrev UNIV})]
    2.11  *}
    2.12  
    2.13  lemmas [nitpick_def] = inverse_rat_inst.inverse_rat
    2.14 -  number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_eq_rat
    2.15 -  plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat
    2.16 -  zero_rat_inst.zero_rat
    2.17 +  number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_rat
    2.18 +  ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat
    2.19 +  uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat
    2.20  
    2.21  subsection{* Float syntax *}
    2.22  
     3.1 --- a/src/HOL/RealDef.thy	Fri Jun 11 16:34:56 2010 +0200
     3.2 +++ b/src/HOL/RealDef.thy	Fri Jun 11 17:05:11 2010 +0200
     3.3 @@ -1806,12 +1806,13 @@
     3.4      (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
     3.5      (@{const_name number_real_inst.number_of_real}, @{const_name Nitpick.number_of_frac}),
     3.6      (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
     3.7 +    (@{const_name ord_real_inst.less_real}, @{const_name Nitpick.less_eq_frac}),
     3.8      (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
     3.9  *}
    3.10  
    3.11  lemmas [nitpick_def] = inverse_real_inst.inverse_real
    3.12      number_real_inst.number_of_real one_real_inst.one_real
    3.13 -    ord_real_inst.less_eq_real plus_real_inst.plus_real
    3.14 +    ord_real_inst.less_real ord_real_inst.less_eq_real plus_real_inst.plus_real
    3.15      times_real_inst.times_real uminus_real_inst.uminus_real
    3.16      zero_real_inst.zero_real
    3.17