avoid very specific code equation for card; corrected spelling
authorhaftmann
Thu Oct 13 23:35:15 2011 +0200 (2011-10-13)
changeset 45141b2eb87bd541b
parent 45140 339a8b3c4791
child 45142 97e81a8aa277
avoid very specific code equation for card; corrected spelling
src/HOL/Enum.thy
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/Enum.thy	Thu Oct 13 23:27:46 2011 +0200
     1.2 +++ b/src/HOL/Enum.thy	Thu Oct 13 23:35:15 2011 +0200
     1.3 @@ -759,11 +759,10 @@
     1.4  qed
     1.5  
     1.6  
     1.7 -subsection {* An executable card operator on finite types *}
     1.8 +subsection {* Transitive closure on relations over finite types *}
     1.9  
    1.10 -lemma [code]:
    1.11 -  "card R = length (filter R enum)"
    1.12 -  by (simp add: distinct_length_filter [OF enum_distinct] enum_UNIV Collect_def)
    1.13 +lemma [code]: "trancl (R :: (('a :: enum) \<times> 'a) set) = ntrancl (length (filter R enum) - 1) R"
    1.14 +  by (simp add: finite_trancl_ntranl distinct_length_filter [OF enum_distinct] enum_UNIV Collect_def)
    1.15  
    1.16  
    1.17  subsection {* Closing up *}
     2.1 --- a/src/HOL/Transitive_Closure.thy	Thu Oct 13 23:27:46 2011 +0200
     2.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Oct 13 23:35:15 2011 +0200
     2.3 @@ -1034,13 +1034,10 @@
     2.4      unfolding ntrancl_def by fastforce
     2.5  qed
     2.6  
     2.7 -lemma finnite_trancl_ntranl:
     2.8 +lemma finite_trancl_ntranl:
     2.9    "finite R \<Longrightarrow> trancl R = ntrancl (card R - 1) R"
    2.10    by (cases "card R") (auto simp add: trancl_finite_eq_rel_pow rel_pow_empty ntrancl_def)
    2.11  
    2.12 -lemma [code]: "trancl (R :: (('a :: finite) \<times> 'a) set) = ntrancl (card R - 1) R"
    2.13 -  by (simp add: finnite_trancl_ntranl)
    2.14 -
    2.15  
    2.16  subsection {* Acyclic relations *}
    2.17