src/HOL/Nitpick.thy
changeset 64267 b9a1486e79be
parent 63882 018998c00003
child 65555 85ed070017b7
     1.1 --- a/src/HOL/Nitpick.thy	Sun Oct 16 22:43:51 2016 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Mon Oct 17 11:46:22 2016 +0200
     1.3 @@ -72,8 +72,8 @@
     1.4  definition card' :: "'a set \<Rightarrow> nat" where
     1.5    "card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0"
     1.6  
     1.7 -definition setsum' :: "('a \<Rightarrow> 'b::comm_monoid_add) \<Rightarrow> 'a set \<Rightarrow> 'b" where
     1.8 -  "setsum' f A \<equiv> if finite A then sum_list (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
     1.9 +definition sum' :: "('a \<Rightarrow> 'b::comm_monoid_add) \<Rightarrow> 'a set \<Rightarrow> 'b" where
    1.10 +  "sum' f A \<equiv> if finite A then sum_list (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
    1.11  
    1.12  inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" where
    1.13    "fold_graph' f z {} z" |
    1.14 @@ -224,7 +224,7 @@
    1.15  setup \<open>
    1.16    Nitpick_HOL.register_ersatz_global
    1.17      [(@{const_name card}, @{const_name card'}),
    1.18 -     (@{const_name setsum}, @{const_name setsum'}),
    1.19 +     (@{const_name sum}, @{const_name sum'}),
    1.20       (@{const_name fold_graph}, @{const_name fold_graph'}),
    1.21       (@{const_name wf}, @{const_name wf'}),
    1.22       (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
    1.23 @@ -232,14 +232,14 @@
    1.24  \<close>
    1.25  
    1.26  hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The FunBox PairBox Word prod
    1.27 -  refl' wf' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac
    1.28 +  refl' wf' card' sum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac
    1.29    zero_frac one_frac num denom norm_frac frac plus_frac times_frac uminus_frac number_of_frac
    1.30    inverse_frac less_frac less_eq_frac of_frac wf_wfrec wf_wfrec wfrec'
    1.31  
    1.32  hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
    1.33  
    1.34  hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold prod_def refl'_def wf'_def
    1.35 -  card'_def setsum'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
    1.36 +  card'_def sum'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
    1.37    size_list_simp nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
    1.38    num_def denom_def frac_def plus_frac_def times_frac_def uminus_frac_def
    1.39    number_of_frac_def inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def