src/HOL/Nitpick.thy
changeset 56643 41d3596d8a64
parent 55642 63beb38e9258
child 57231 dca8d06ecbba
     1.1 --- a/src/HOL/Nitpick.thy	Wed Apr 23 10:23:26 2014 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Wed Apr 23 10:23:27 2014 +0200
     1.3 @@ -113,9 +113,8 @@
     1.4  
     1.5  declare nat.case [nitpick_simp del]
     1.6  
     1.7 -lemma list_size_simp [nitpick_simp]:
     1.8 -"list_size f xs = (if xs = [] then 0
     1.9 -                   else Suc (f (hd xs) + list_size f (tl xs)))"
    1.10 +lemma size_list_simp [nitpick_simp]:
    1.11 +"size_list f xs = (if xs = [] then 0 else Suc (f (hd xs) + size_list f (tl xs)))"
    1.12  "size xs = (if xs = [] then 0 else Suc (size (tl xs)))"
    1.13  by (cases xs) auto
    1.14  
    1.15 @@ -145,8 +144,9 @@
    1.16  definition Frac :: "int \<times> int \<Rightarrow> bool" where
    1.17  "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> int_gcd a b = 1"
    1.18  
    1.19 -axiomatization Abs_Frac :: "int \<times> int \<Rightarrow> 'a"
    1.20 -           and Rep_Frac :: "'a \<Rightarrow> int \<times> int"
    1.21 +axiomatization
    1.22 +  Abs_Frac :: "int \<times> int \<Rightarrow> 'a" and
    1.23 +  Rep_Frac :: "'a \<Rightarrow> int \<times> int"
    1.24  
    1.25  definition zero_frac :: 'a where
    1.26  "zero_frac \<equiv> Abs_Frac (0, 1)"
    1.27 @@ -244,7 +244,7 @@
    1.28  hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
    1.29      prod_def refl'_def wf'_def card'_def setsum'_def
    1.30      fold_graph'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
    1.31 -    list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
    1.32 +    size_list_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
    1.33      zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
    1.34      plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
    1.35      inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def