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
```