src/HOL/Nitpick.thy
changeset 37397 18000f9d783e
parent 37213 efcad7594872
child 37704 c6161bee8486
     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