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.6  
     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.10  
    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.14  
    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.18  
    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.22  
    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)"
    1.27