src/HOL/Enum.thy
changeset 45140 339a8b3c4791
parent 45119 055c6ff9c5c3
child 45141 b2eb87bd541b
equal deleted inserted replaced
45139:bdcaa3f3a2f4 45140:339a8b3c4791
   756   }
   756   }
   757   from this show ?thesis
   757   from this show ?thesis
   758     unfolding enum_the_def by (auto split: list.split)
   758     unfolding enum_the_def by (auto split: list.split)
   759 qed
   759 qed
   760 
   760 
       
   761 
   761 subsection {* An executable card operator on finite types *}
   762 subsection {* An executable card operator on finite types *}
   762 
   763 
   763 lemma
       
   764   [code]: "card R = length (filter R enum)"
       
   765 by (simp add: distinct_length_filter[OF enum_distinct] enum_UNIV Collect_def)
       
   766 
       
   767 subsection {* An executable (reflexive) transitive closure on finite relations *}
       
   768 
       
   769 text {* Definitions could be moved to Transitive Closure theory if they are of more general use. *}
       
   770 
       
   771 definition ntrancl :: "('a * 'a => bool) => nat => ('a * 'a => bool)"
       
   772 where
       
   773  [code del]: "ntrancl R n = (UN i : {i. 0 < i & i <= (Suc n)}. R ^^ i)"
       
   774 
       
   775 lemma [code]:
   764 lemma [code]:
   776   "ntrancl (R :: 'a * 'a => bool) 0 = R"
   765   "card R = length (filter R enum)"
   777 proof
   766   by (simp add: distinct_length_filter [OF enum_distinct] enum_UNIV Collect_def)
   778   show "R <= ntrancl R 0"
   767 
   779     unfolding ntrancl_def by fastforce
       
   780 next
       
   781   { 
       
   782     fix i have "(0 < i & i <= Suc 0) = (i = 1)" by auto
       
   783   }
       
   784   from this show "ntrancl R 0 <= R"
       
   785     unfolding ntrancl_def by auto
       
   786 qed
       
   787 
       
   788 lemma [code]:
       
   789   "ntrancl (R :: 'a * 'a => bool) (Suc n) = (ntrancl R n) O (Id Un R)"
       
   790 proof
       
   791   {
       
   792     fix a b
       
   793     assume "(a, b) : ntrancl R (Suc n)"
       
   794     from this obtain i where "0 < i" "i <= Suc (Suc n)" "(a, b) : R ^^ i"
       
   795       unfolding ntrancl_def by auto
       
   796     have "(a, b) : ntrancl R n O (Id Un R)"
       
   797     proof (cases "i = 1")
       
   798       case True
       
   799       from this `(a, b) : R ^^ i` show ?thesis
       
   800         unfolding ntrancl_def by auto
       
   801     next
       
   802       case False
       
   803       from this `0 < i` obtain j where j: "i = Suc j" "0 < j"
       
   804         by (cases i) auto
       
   805       from this `(a, b) : R ^^ i` obtain c where c1: "(a, c) : R ^^ j" and c2:"(c, b) : R"
       
   806         by auto
       
   807       from c1 j `i <= Suc (Suc n)` have "(a, c): ntrancl R n"
       
   808         unfolding ntrancl_def by fastforce
       
   809       from this c2 show ?thesis by fastforce
       
   810     qed
       
   811   }
       
   812   from this show "ntrancl R (Suc n) <= ntrancl R n O (Id Un R)" by auto
       
   813 next
       
   814   show "ntrancl R n O (Id Un R) <= ntrancl R (Suc n)"
       
   815     unfolding ntrancl_def by fastforce
       
   816 qed
       
   817 
       
   818 lemma [code]: "trancl (R :: ('a :: finite) * 'a => bool) = ntrancl R (card R - 1)"
       
   819 by (cases "card R") (auto simp add: trancl_finite_eq_rel_pow rel_pow_empty ntrancl_def)
       
   820 
       
   821 (* a copy of Nitpick.rtrancl_unfold, should be moved to Transitive_Closure *)
       
   822 lemma [code]: "r^* = (r^+)^="
       
   823 by simp
       
   824 
   768 
   825 subsection {* Closing up *}
   769 subsection {* Closing up *}
   826 
   770 
   827 code_abort enum_the
   771 code_abort enum_the
   828 
   772