src/HOL/Finite_Set.thy
changeset 44831 4ea848959340
parent 43991 f4a7697011c5
child 44835 ff6b9eb9c5ef
equal deleted inserted replaced
44830:f710ce327b08 44831:4ea848959340
   484 lemma finite_code [code]: "finite (A \<Colon> 'a set) \<longleftrightarrow> True"
   484 lemma finite_code [code]: "finite (A \<Colon> 'a set) \<longleftrightarrow> True"
   485   by simp
   485   by simp
   486 
   486 
   487 end
   487 end
   488 
   488 
   489 instance unit :: finite proof
       
   490 qed (simp add: UNIV_unit)
       
   491 
       
   492 instance bool :: finite proof
       
   493 qed (simp add: UNIV_bool)
       
   494 
       
   495 instance prod :: (finite, finite) finite proof
   489 instance prod :: (finite, finite) finite proof
   496 qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
   490 qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
   497 
       
   498 lemma finite_option_UNIV [simp]:
       
   499   "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
       
   500   by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
       
   501 
       
   502 instance option :: (finite) finite proof
       
   503 qed (simp add: UNIV_option_conv)
       
   504 
   491 
   505 lemma inj_graph: "inj (%f. {(x, y). y = f x})"
   492 lemma inj_graph: "inj (%f. {(x, y). y = f x})"
   506   by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff)
   493   by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff)
   507 
   494 
   508 instance "fun" :: (finite, finite) finite
   495 instance "fun" :: (finite, finite) finite
   517       by (rule finite_subset)
   504       by (rule finite_subset)
   518     show "inj ?graph" by (rule inj_graph)
   505     show "inj ?graph" by (rule inj_graph)
   519   qed
   506   qed
   520 qed
   507 qed
   521 
   508 
       
   509 instance bool :: finite proof
       
   510 qed (simp add: UNIV_bool)
       
   511 
       
   512 instance unit :: finite proof
       
   513 qed (simp add: UNIV_unit)
       
   514 
   522 instance sum :: (finite, finite) finite proof
   515 instance sum :: (finite, finite) finite proof
   523 qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
   516 qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
       
   517 
       
   518 lemma finite_option_UNIV [simp]:
       
   519   "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
       
   520   by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
       
   521 
       
   522 instance option :: (finite) finite proof
       
   523 qed (simp add: UNIV_option_conv)
   524 
   524 
   525 
   525 
   526 subsection {* A basic fold functional for finite sets *}
   526 subsection {* A basic fold functional for finite sets *}
   527 
   527 
   528 text {* The intended behaviour is
   528 text {* The intended behaviour is