src/HOL/Nitpick.thy
changeset 35699 9ed327529a44
parent 35671 ed2c3830d881
child 35807 e4d1b5cbd429
     1.1 --- a/src/HOL/Nitpick.thy	Wed Mar 10 17:46:28 2010 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Wed Mar 10 19:21:59 2010 +0100
     1.3 @@ -96,10 +96,10 @@
     1.4                  else THE y. wfrec_rel R (%f x. F (Recdef.cut f R x) x) x y"
     1.5  
     1.6  definition card' :: "('a \<Rightarrow> bool) \<Rightarrow> nat" where
     1.7 -"card' X \<equiv> length (SOME xs. set xs = X \<and> distinct xs)"
     1.8 +"card' A \<equiv> if finite A then length (safe_Eps (\<lambda>xs. set xs = A \<and> distinct xs)) else 0"
     1.9  
    1.10  definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b" where
    1.11 -"setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
    1.12 +"setsum' f A \<equiv> if finite A then listsum (map f (safe_Eps (\<lambda>xs. set xs = A \<and> distinct xs))) else 0"
    1.13  
    1.14  inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
    1.15  "fold_graph' f z {} z" |