src/HOL/Nitpick.thy
 changeset 44278 1220ecb81e8f parent 44016 51184010c609 child 45140 339a8b3c4791
1.1 --- a/src/HOL/Nitpick.thy	Thu Aug 18 13:25:17 2011 +0200
1.2 +++ b/src/HOL/Nitpick.thy	Thu Aug 18 13:55:26 2011 +0200
1.3 @@ -76,19 +76,19 @@
1.4  definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
1.5  "prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
1.7 -definition refl' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.8 +definition refl' :: "('a \<times> 'a) set \<Rightarrow> bool" where
1.9  "refl' r \<equiv> \<forall>x. (x, x) \<in> r"
1.11 -definition wf' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.12 +definition wf' :: "('a \<times> 'a) set \<Rightarrow> bool" where
1.13  "wf' r \<equiv> acyclic r \<and> (finite r \<or> unknown)"
1.15 -definition card' :: "('a \<Rightarrow> bool) \<Rightarrow> nat" where
1.16 +definition card' :: "'a set \<Rightarrow> nat" where
1.17  "card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0"
1.19 -definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b" where
1.20 +definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> 'a set \<Rightarrow> 'b" where
1.21  "setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
1.23 -inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
1.24 +inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" where
1.25  "fold_graph' f z {} z" |
1.26  "\<lbrakk>x \<in> A; fold_graph' f z (A - {x}) y\<rbrakk> \<Longrightarrow> fold_graph' f z A (f x y)"