src/HOL/Enum.thy
changeset 45119 055c6ff9c5c3
parent 45117 3911cf09899a
child 45140 339a8b3c4791
equal deleted inserted replaced
45118:7462f287189a 45119:055c6ff9c5c3
   764   [code]: "card R = length (filter R enum)"
   764   [code]: "card R = length (filter R enum)"
   765 by (simp add: distinct_length_filter[OF enum_distinct] enum_UNIV Collect_def)
   765 by (simp add: distinct_length_filter[OF enum_distinct] enum_UNIV Collect_def)
   766 
   766 
   767 subsection {* An executable (reflexive) transitive closure on finite relations *}
   767 subsection {* An executable (reflexive) transitive closure on finite relations *}
   768 
   768 
   769 text {* Definitions could be moved to Transitive_Closure if they are of more general use. *}
   769 text {* Definitions could be moved to Transitive Closure theory if they are of more general use. *}
   770 
   770 
   771 definition ntrancl :: "('a * 'a => bool) => nat => ('a * 'a => bool)"
   771 definition ntrancl :: "('a * 'a => bool) => nat => ('a * 'a => bool)"
   772 where
   772 where
   773  [code del]: "ntrancl R n = (UN i : {i. 0 < i & i <= (Suc n)}. R ^^ i)"
   773  [code del]: "ntrancl R n = (UN i : {i. 0 < i & i <= (Suc n)}. R ^^ i)"
   774 
   774